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