Termination checking

7 files changed, 376 insertions, 1 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index 33af4a82..2312a047 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -56,6 +56,7 @@ signature COMPILER = sig
 
     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 @@ signature COMPILER = sig
     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 --git a/src/compiler.sml b/src/compiler.sml
index 1578da71..f408837d 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -363,12 +363,19 @@ val elaborate = {
 
 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 --git a/src/list_util.sig b/src/list_util.sig
index 3340fffc..26ec72c1 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -44,4 +44,6 @@ signature LIST_UTIL = sig
     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 --git a/src/list_util.sml b/src/list_util.sml
index f9826ab4..235a9654 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -163,4 +163,19 @@ fun foldri f i ls =
         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 --git a/src/sources b/src/sources
index 6c1c7ac8..0a3761d5 100644
--- a/src/sources
+++ b/src/sources
@@ -44,6 +44,9 @@ disjoint.sml
 elaborate.sig
 elaborate.sml
 
+termination.sig
+termination.sml
+
 expl.sml
 
 expl_util.sig
diff --git a/src/termination.sig b/src/termination.sig
new file mode 100644
index 00000000..1de00f1d
--- /dev/null
+++ b/src/termination.sig
@@ -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 --git a/src/termination.sml b/src/termination.sml
new file mode 100644
index 00000000..18ff0785
--- /dev/null
+++ b/src/termination.sml
@@ -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