adamc@313: (* Copyright (c) 2008, Adam Chlipala adamc@313: * All rights reserved. adamc@313: * adamc@313: * Redistribution and use in source and binary forms, with or without adamc@313: * modification, are permitted provided that the following conditions are met: adamc@313: * adamc@313: * - Redistributions of source code must retain the above copyright notice, adamc@313: * this list of conditions and the following disclaimer. adamc@313: * - Redistributions in binary form must reproduce the above copyright notice, adamc@313: * this list of conditions and the following disclaimer in the documentation adamc@313: * and/or other materials provided with the distribution. adamc@313: * - The names of contributors may not be used to endorse or promote products adamc@313: * derived from this software without specific prior written permission. adamc@313: * adamc@313: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@313: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@313: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@313: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@313: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@313: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@313: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@313: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@313: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@313: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@313: * POSSIBILITY OF SUCH DAMAGE. adamc@313: *) adamc@313: adamc@313: structure Termination :> TERMINATION = struct adamc@313: adamc@313: open Elab adamc@313: adamc@313: structure E = ElabEnv adamc@313: structure IM = IntBinaryMap adamc@410: structure IS = IntBinarySet adamc@313: adamc@313: datatype pedigree = adamc@313: Func of int adamc@313: | Arg of int * int * con adamc@313: | Subarg of int * int * con adamc@313: | Rabble adamc@313: adamc@313: fun p2s p = adamc@313: case p of adamc@313: Func i => "Func" ^ Int.toString i adamc@313: | Arg (i, j, _) => "Arg" ^ Int.toString i ^ "," ^ Int.toString j adamc@313: | Subarg (i, j, _) => "Subarg" ^ Int.toString i ^ "," ^ Int.toString j adamc@313: | Rabble => "Rabble" adamc@313: adamc@313: fun declOk' env (d, loc) = adamc@313: case d of adamc@313: DValRec vis => adamc@313: let adamc@313: val nfns = length vis adamc@313: adamc@313: val fenv = ListUtil.foldli (fn (i, (_, j, _, _), fenv) => IM.insert (fenv, j, i)) IM.empty vis adamc@313: adamc@313: fun namesEq ((c1, _), (c2, _)) = adamc@313: case (c1, c2) of adamc@313: (CName s1, CName s2) => s1 = s2 adamc@313: | (CRel n1, CRel n2) => n1 = n2 adamc@313: | (CNamed n1, CNamed n2) => n1 = n2 adamc@313: | (CModProj n1, CModProj n2) => n1 = n2 adamc@313: | _ => false adamc@313: adamc@313: fun patCon pc = adamc@313: let adamc@313: fun unravel (t, _) = adamc@313: case t of adamc@313: TCFun (_, _, _, t) => unravel t adamc@313: | TFun (dom, _) => dom adamc@313: | _ => raise Fail "Termination: Unexpected constructor type" adamc@313: in adamc@313: case pc of adamc@313: PConVar i => adamc@313: let adamc@313: val (_, t) = E.lookupENamed env i adamc@313: in adamc@313: unravel t adamc@313: end adamc@313: | PConProj (m1, ms, x) => adamc@313: let adamc@313: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@313: in adamc@313: case E.projectVal env {str = str, sgn = sgn, field = x} of adamc@313: NONE => raise Fail "Termination: Bad constructor projection" adamc@313: | SOME t => unravel t adamc@313: end adamc@313: end adamc@313: adamc@313: fun pat penv (p, (pt, _)) = adamc@313: let adamc@313: fun con (i, j, pc, pt') = pat penv (Subarg (i, j, patCon pc), pt') adamc@313: adamc@313: fun record (i, j, t, xps) = adamc@313: case t of adamc@313: (TRecord (CRecord (_, xts), _), _) => adamc@313: foldl (fn ((x, pt', _), penv) => adamc@313: let adamc@313: val p' = adamc@313: case List.find (fn (x', _) => adamc@313: namesEq ((CName x, ErrorMsg.dummySpan), x')) xts of adamc@313: NONE => Rabble adamc@313: | SOME (_, t) => Subarg (i, j, t) adamc@313: in adamc@313: pat penv (p', pt') adamc@313: end) penv xps adamc@313: | _ => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps adamc@313: in adamc@313: case (p, pt) of adamc@313: (_, PWild) => penv adamc@313: | (_, PVar _) => p :: penv adamc@313: | (_, PPrim _) => penv adamc@313: | (_, PCon (_, _, _, NONE)) => penv adamc@313: | (Arg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt') adamc@313: | (Subarg (i, j, _), PCon (_, pc, _, SOME pt')) => con (i, j, pc, pt') adamc@313: | (_, PCon (_, _, _, SOME pt')) => pat penv (Rabble, pt') adamc@313: | (Arg (i, j, t), PRecord xps) => record (i, j, t, xps) adamc@313: | (Subarg (i, j, t), PRecord xps) => record (i, j, t, xps) adamc@313: | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps adamc@313: end adamc@313: adamc@410: fun exp parent (penv, calls) e = adamc@313: let adamc@313: val default = (Rabble, calls) adamc@313: adamc@313: fun apps () = adamc@313: let adamc@313: fun combiner calls e = adamc@313: case #1 e of adamc@314: EApp ((ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (ECApp ( adamc@314: (EModProj (m, [], "tag"), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: _), _), adamc@314: (ERecord xets, _)) => adamc@314: let adamc@314: val checkName = adamc@314: case E.lookupStrNamed env m of adamc@314: ("Basis", _) => (fn x : con => case #1 x of adamc@314: CName s => s = "Link" adamc@314: orelse s = "Action" adamc@314: | _ => false) adamc@314: | _ => (fn _ => false) adamc@314: adamc@314: val calls = foldl (fn ((x, e, _), calls) => adamc@314: if checkName x then adamc@314: calls adamc@314: else adamc@410: #2 (exp parent (penv, calls) e)) calls xets adamc@314: in adamc@314: (Rabble, [Rabble], calls) adamc@314: end adamc@314: adamc@314: | EApp (e1, e2) => adamc@313: let adamc@313: val (p1, ps, calls) = combiner calls e1 adamc@410: val (p2, calls) = exp parent (penv, calls) e2 adamc@313: adamc@313: val p = case p1 of adamc@313: Rabble => Rabble adamc@313: | Arg _ => Rabble adamc@313: | Subarg (i, j, (TFun (_, ran), _)) => Subarg (i, j, ran) adamc@313: | Subarg _ => Rabble adamc@313: | Func _ => Rabble adamc@313: in adamc@313: (p, ps @ [p2], calls) adamc@313: end adamc@313: | ECApp (e, _) => adamc@313: let adamc@313: val (p, ps, calls) = combiner calls e adamc@313: adamc@313: val p = case p of adamc@313: Rabble => Rabble adamc@313: | Arg _ => Rabble adamc@313: | Subarg (i, j, (TCFun (_, _, _, ran), _)) => Subarg (i, j, ran) adamc@313: | Subarg _ => Rabble adamc@313: | Func _ => Rabble adamc@313: in adamc@313: (p, ps, calls) adamc@313: end adamc@623: | EKApp (e, _) => combiner calls e adamc@313: | _ => adamc@313: let adamc@410: val (p, calls) = exp parent (penv, calls) e adamc@313: in adamc@313: (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; adamc@313: print (p2s p ^ "\n");*) adamc@313: (p, [p], calls) adamc@313: end adamc@313: adamc@313: val (p, ps, calls) = combiner calls e adamc@313: adamc@313: val calls = adamc@313: case ps of adamc@313: [] => raise Fail "Termination: Empty ps" adamc@313: | f :: ps => adamc@313: case f of adamc@410: Func i => (parent, i, ps) :: calls adamc@313: | _ => calls adamc@313: in adamc@313: (p, calls) adamc@313: end adamc@313: in adamc@313: case #1 e of adamc@313: EPrim _ => default adamc@313: | ERel n => (List.nth (penv, n), calls) adamc@313: | ENamed n => adamc@313: let adamc@313: val p = case IM.find (fenv, n) of adamc@313: NONE => Rabble adamc@313: | SOME n' => Func n' adamc@313: in adamc@313: (p, calls) adamc@313: end adamc@313: | EModProj _ => default adamc@314: adamc@313: | EApp _ => apps () adamc@313: | EAbs (_, _, _, e) => adamc@313: let adamc@410: val (_, calls) = exp parent (Rabble :: penv, calls) e adamc@313: in adamc@313: (Rabble, calls) adamc@313: end adamc@313: | ECApp _ => apps () adamc@313: | ECAbs (_, _, _, e) => adamc@313: let adamc@410: val (_, calls) = exp parent (penv, calls) e adamc@313: in adamc@313: (Rabble, calls) adamc@313: end adamc@623: | EKApp _ => apps () adamc@623: | EKAbs (_, e) => adamc@623: let adamc@623: val (_, calls) = exp parent (penv, calls) e adamc@623: in adamc@623: (Rabble, calls) adamc@623: end adamc@313: adamc@313: | ERecord xets => adamc@313: let adamc@410: val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets adamc@313: in adamc@313: (Rabble, calls) adamc@313: end adamc@313: | EField (e, x, _) => adamc@313: let adamc@410: val (p, calls) = exp parent (penv, calls) e adamc@313: val p = adamc@313: case p of adamc@313: Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) => adamc@313: (case List.find (fn (x', _) => namesEq (x, x')) xts of adamc@313: NONE => Rabble adamc@313: | SOME (_, t) => Subarg (i, j, t)) adamc@313: | _ => Rabble adamc@313: in adamc@313: (p, calls) adamc@313: end adamc@313: | ECut (e, _, _) => adamc@313: let adamc@410: val (_, calls) = exp parent (penv, calls) e adamc@313: in adamc@313: (Rabble, calls) adamc@313: end adamc@493: | ECutMulti (e, _, _) => adamc@493: let adamc@493: val (_, calls) = exp parent (penv, calls) e adamc@493: in adamc@493: (Rabble, calls) adamc@493: end adamc@445: | EConcat (e1, _, e2, _) => adamc@339: let adamc@410: val (_, calls) = exp parent (penv, calls) e1 adamc@410: val (_, calls) = exp parent (penv, calls) e2 adamc@339: in adamc@339: (Rabble, calls) adamc@339: end adamc@313: adamc@313: | ECase (e, pes, _) => adamc@313: let adamc@410: val (p, calls) = exp parent (penv, calls) e adamc@313: adamc@313: val calls = foldl (fn ((pt, e), calls) => adamc@313: let adamc@313: val penv = pat penv (p, pt) adamc@410: val (_, calls) = exp parent (penv, calls) e adamc@313: in adamc@313: calls adamc@313: end) calls pes adamc@313: in adamc@313: (Rabble, calls) adamc@313: end adamc@313: adamc@313: | EError => (Rabble, calls) adamc@410: | EUnif (ref (SOME e)) => exp parent (penv, calls) e adamc@313: | EUnif (ref NONE) => (Rabble, calls) adamc@448: adamc@825: | ELet (eds, e, _) => adamc@453: let adamc@453: fun extPenv ((ed, _), penv) = adamc@453: case ed of adamc@453: EDVal _ => Rabble :: penv adamc@453: | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis adamc@453: in adamc@453: exp parent (foldl extPenv penv eds, calls) e adamc@453: end adamc@313: end adamc@313: adamc@313: fun doVali (i, (_, f, _, e), calls) = adamc@313: let adamc@313: fun unravel (e, j, penv) = adamc@313: case #1 e of adamc@313: EAbs (_, t, _, e) => adamc@313: unravel (e, j + 1, Arg (i, j, t) :: penv) adamc@313: | ECAbs (_, _, _, e) => adamc@313: unravel (e, j, penv) adamc@410: | _ => (j, #2 (exp f (penv, calls) e)) adamc@313: in adamc@313: unravel (e, 0, []) adamc@313: end adamc@313: adamc@313: val (ns, calls) = ListUtil.foldliMap doVali [] vis adamc@313: adamc@410: fun isRecursive (from, to, _) = adamc@410: let adamc@410: fun search (at, soFar) = adamc@410: at = from adamc@410: orelse List.exists (fn (from', to', _) => adamc@410: from' = at adamc@410: andalso not (IS.member (soFar, to')) adamc@410: andalso search (to', IS.add (soFar, to'))) adamc@410: calls adamc@410: in adamc@410: search (to, IS.empty) adamc@410: end adamc@410: adamc@410: val calls = List.filter isRecursive calls adamc@410: adamc@313: fun search (ns, choices) = adamc@313: case ns of adamc@313: [] => adamc@313: let adamc@313: val choices = rev choices adamc@313: in adamc@410: List.all (fn (_, f, args) => adamc@313: let adamc@313: val recArg = List.nth (choices, f) adamc@313: adamc@313: fun isDatatype (t, _) = adamc@313: case t of adamc@313: CNamed _ => true adamc@313: | CModProj _ => true adamc@313: | CApp (t, _) => isDatatype t adamc@313: | _ => false adamc@313: in adamc@313: length args > recArg andalso adamc@313: case List.nth (args, recArg) of adamc@313: Subarg (i, j, t) => isDatatype t andalso j = List.nth (choices, i) adamc@313: | _ => false adamc@313: end) calls adamc@313: end adamc@313: | n :: ns' => adamc@313: let adamc@313: fun search' i = adamc@313: i < n andalso (search (ns', i :: choices) orelse search' (i + 1)) adamc@313: in adamc@313: search' 0 adamc@313: end adamc@313: in adamc@313: if search (ns, []) then adamc@313: () adamc@313: else adamc@313: ErrorMsg.errorAt loc "Can't prove termination of recursive function(s)" adamc@313: end adamc@313: adamc@313: | DStr (_, _, _, (StrConst ds, _)) => ignore (foldl declOk env ds) adamc@313: adamc@313: | _ => () adamc@313: adamc@313: and declOk (d, env) = adamc@313: (declOk' env d; adamc@313: E.declBinds env d) adamc@313: adamc@313: fun check ds = ignore (foldl declOk E.empty ds) adamc@313: adamc@313: end