# HG changeset patch # User Adam Chlipala # Date 1220975193 14400 # Node ID e0ed0d4dabc9114c89404a1a0170bf4890245c72 # Parent f387d12193ba85c9b7d79a61206049b026ddd284 Termination checking diff -r f387d12193ba -r e0ed0d4dabc9 src/compiler.sig --- a/src/compiler.sig Tue Sep 09 09:15:00 2008 -0400 +++ b/src/compiler.sig Tue Sep 09 11:46:33 2008 -0400 @@ -56,6 +56,7 @@ val parse : (job, Source.file) phase val elaborate : (Source.file, Elab.file) phase + val termination : (Elab.file, Elab.file) phase val explify : (Elab.file, Expl.file) phase val corify : (Expl.file, Core.file) phase val shake : (Core.file, Core.file) phase @@ -74,6 +75,7 @@ val toParseJob : (string, job) transform val toParse : (string, Source.file) transform val toElaborate : (string, Elab.file) transform + val toTermination : (string, Elab.file) transform val toExplify : (string, Expl.file) transform val toCorify : (string, Core.file) transform val toShake1 : (string, Core.file) transform diff -r f387d12193ba -r e0ed0d4dabc9 src/compiler.sml --- a/src/compiler.sml Tue Sep 09 09:15:00 2008 -0400 +++ b/src/compiler.sml Tue Sep 09 11:46:33 2008 -0400 @@ -363,12 +363,19 @@ val toElaborate = transform elaborate "elaborate" o toParse +val termination = { + func = (fn file => (Termination.check file; file)), + print = ElabPrint.p_file ElabEnv.empty +} + +val toTermination = transform termination "termination" o toElaborate + val explify = { func = Explify.explify, print = ExplPrint.p_file ExplEnv.empty } -val toExplify = transform explify "explify" o toElaborate +val toExplify = transform explify "explify" o toTermination val corify = { func = Corify.corify, diff -r f387d12193ba -r e0ed0d4dabc9 src/list_util.sig --- a/src/list_util.sig Tue Sep 09 09:15:00 2008 -0400 +++ b/src/list_util.sig Tue Sep 09 11:46:33 2008 -0400 @@ -44,4 +44,6 @@ val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b val foldri : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b + val foldliMap : (int * 'data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + end diff -r f387d12193ba -r e0ed0d4dabc9 src/list_util.sml --- a/src/list_util.sml Tue Sep 09 09:15:00 2008 -0400 +++ b/src/list_util.sml Tue Sep 09 11:46:33 2008 -0400 @@ -163,4 +163,19 @@ foldli (fn (n, x, s) => f (len - n - 1, x, s)) i (rev ls) end +fun foldliMap f s = + let + fun fm (n, ls', s) ls = + case ls of + nil => (rev ls', s) + | h :: t => + let + val (h', s') = f (n, h, s) + in + fm (n + 1, h' :: ls', s') t + end + in + fm (0, [], s) + end + end diff -r f387d12193ba -r e0ed0d4dabc9 src/sources --- a/src/sources Tue Sep 09 09:15:00 2008 -0400 +++ b/src/sources Tue Sep 09 11:46:33 2008 -0400 @@ -44,6 +44,9 @@ elaborate.sig elaborate.sml +termination.sig +termination.sml + expl.sml expl_util.sig diff -r f387d12193ba -r e0ed0d4dabc9 src/termination.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/termination.sig Tue Sep 09 11:46:33 2008 -0400 @@ -0,0 +1,32 @@ +(* 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. + *) + +signature TERMINATION = sig + + val check : Elab.file -> unit + +end diff -r f387d12193ba -r e0ed0d4dabc9 src/termination.sml --- /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 diff -r f387d12193ba -r e0ed0d4dabc9 tests/termination.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/termination.ur Tue Sep 09 11:46:33 2008 -0400 @@ -0,0 +1,28 @@ +datatype list a = Nil | Cons of a * list a + +fun isNil (t ::: Type) (ls : list t) : bool = + case ls of + Nil => True + | Cons _ => False + +fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t = + case ls1 of + Nil => ls2 + | Cons (x, ls1') => Cons (x, append ls1' ls2) + +fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t = + case ls1 of + Nil => ls2 + | Cons (x, ls1') => Cons (x, appendR ls2 ls1') + +(*fun naughty (t ::: Type) (ls : list t) : list t = naughty ls*) + +fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t = + case ls1 of + Nil => ls2 + | Cons (x, ls1') => Cons (x, append2 ls2 ls1') + +and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t = + case ls1 of + Nil => ls2 + | Cons (x, ls1') => Cons (x, append1 ls1' ls2) diff -r f387d12193ba -r e0ed0d4dabc9 tests/termination.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/termination.urp Tue Sep 09 11:46:33 2008 -0400 @@ -0,0 +1,5 @@ +debug +database dbname=test +exe /tmp/webapp + +termination