summaryrefslogtreecommitdiff
path: root/src/termination.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/termination.sml')
-rw-r--r--src/termination.sml396
1 files changed, 396 insertions, 0 deletions
diff --git a/src/termination.sml b/src/termination.sml
new file mode 100644
index 0000000..f0ec46d
--- /dev/null
+++ b/src/termination.sml
@@ -0,0 +1,396 @@
+(* 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
+structure IS = IntBinarySet
+
+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
+ (_, 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 parent (penv, calls) e =
+ let
+ val default = (Rabble, calls)
+
+ fun apps () =
+ let
+ fun combiner calls e =
+ case #1 e of
+ EApp ((ECApp (
+ (ECApp (
+ (ECApp (
+ (ECApp (
+ (ECApp (
+ (ECApp (
+ (ECApp (
+ (ECApp (
+ (EModProj (m, [], "tag"), _),
+ _), _),
+ _), _),
+ _), _),
+ _), _),
+ _), _),
+ _), _),
+ _), _),
+ _), _),
+ (ERecord xets, _)) =>
+ let
+ val checkName =
+ case E.lookupStrNamed env m of
+ ("Basis", _) => (fn x : con => case #1 x of
+ CName s => s = "Link"
+ orelse s = "Action"
+ | _ => false)
+ | _ => (fn _ => false)
+
+ val calls = foldl (fn ((x, e, _), calls) =>
+ if checkName x then
+ calls
+ else
+ #2 (exp parent (penv, calls) e)) calls xets
+ in
+ (Rabble, [Rabble], calls)
+ end
+
+ | EApp (e1, e2) =>
+ let
+ val (p1, ps, calls) = combiner calls e1
+ val (p2, calls) = exp parent (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
+ | EKApp (e, _) => combiner calls e
+ | _ =>
+ let
+ val (p, calls) = exp parent (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 => (parent, 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 parent (Rabble :: penv, calls) e
+ in
+ (Rabble, calls)
+ end
+ | ECApp _ => apps ()
+ | ECAbs (_, _, _, e) =>
+ let
+ val (_, calls) = exp parent (penv, calls) e
+ in
+ (Rabble, calls)
+ end
+ | EKApp _ => apps ()
+ | EKAbs (_, e) =>
+ let
+ val (_, calls) = exp parent (penv, calls) e
+ in
+ (Rabble, calls)
+ end
+
+ | ERecord xets =>
+ let
+ val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets
+ in
+ (Rabble, calls)
+ end
+ | EField (e, x, _) =>
+ let
+ val (p, calls) = exp parent (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 parent (penv, calls) e
+ in
+ (Rabble, calls)
+ end
+ | ECutMulti (e, _, _) =>
+ let
+ val (_, calls) = exp parent (penv, calls) e
+ in
+ (Rabble, calls)
+ end
+ | EConcat (e1, _, e2, _) =>
+ let
+ val (_, calls) = exp parent (penv, calls) e1
+ val (_, calls) = exp parent (penv, calls) e2
+ in
+ (Rabble, calls)
+ end
+
+ | ECase (e, pes, _) =>
+ let
+ val (p, calls) = exp parent (penv, calls) e
+
+ val calls = foldl (fn ((pt, e), calls) =>
+ let
+ val penv = pat penv (p, pt)
+ val (_, calls) = exp parent (penv, calls) e
+ in
+ calls
+ end) calls pes
+ in
+ (Rabble, calls)
+ end
+
+ | EError => (Rabble, calls)
+ | EUnif (ref (SOME e)) => exp parent (penv, calls) e
+ | EUnif (ref NONE) => (Rabble, calls)
+
+ | ELet (eds, e, _) =>
+ let
+ fun extPenv ((ed, _), penv) =
+ case ed of
+ EDVal _ => Rabble :: penv
+ | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis
+ in
+ exp parent (foldl extPenv penv eds, calls) e
+ end
+ 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 f (penv, calls) e))
+ in
+ unravel (e, 0, [])
+ end
+
+ val (ns, calls) = ListUtil.foldliMap doVali [] vis
+
+ fun isRecursive (from, to, _) =
+ let
+ fun search (at, soFar) =
+ at = from
+ orelse List.exists (fn (from', to', _) =>
+ from' = at
+ andalso not (IS.member (soFar, to'))
+ andalso search (to', IS.add (soFar, to')))
+ calls
+ in
+ search (to, IS.empty)
+ end
+
+ val calls = List.filter isRecursive calls
+
+ 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-25 16:00:03 +0000