# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220966100 14400
# Node ID f387d12193ba85c9b7d79a61206049b026ddd284
# Parent  9ad92047a49988118cb526259f466f08932b8346
Datatype positivity check

diff -r 9ad92047a499 -r f387d12193ba src/elaborate.sml
--- a/src/elaborate.sml	Sun Sep 07 15:40:42 2008 -0400
+++ b/src/elaborate.sml	Tue Sep 09 09:15:00 2008 -0400
@@ -1766,6 +1766,7 @@
 datatype decl_error =
          KunifsRemain of L'.decl list
        | CunifsRemain of L'.decl list
+       | Nonpositive of L'.decl
 
 fun lspan [] = ErrorMsg.dummySpan
   | lspan ((_, loc) :: _) = loc
@@ -1778,6 +1779,9 @@
       | CunifsRemain ds =>
         (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
          eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+      | Nonpositive d =>
+        (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
+         eprefaces' [("Decl", p_decl env d)])
 
 datatype sgn_error =
          UnboundSgn of ErrorMsg.span * string
@@ -2739,6 +2743,68 @@
       | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
 
 
+fun positive self =
+    let
+        open L
+
+        fun none (c, _) =
+            case c of
+                CAnnot (c, _) => none c
+
+              | TFun (c1, c2) => none c1 andalso none c2
+              | TCFun (_, _, _, c) => none c
+              | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+              | TRecord c => none c
+
+              | CVar ([], x) => x <> self
+              | CVar _ => true
+              | CApp (c1, c2) => none c1 andalso none c2
+              | CAbs _ => false
+              | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+
+              | CName _ => true
+
+              | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
+              | CConcat (c1, c2) => none c1 andalso none c2
+              | CFold => true
+
+              | CUnit => true
+
+              | CTuple cs => List.all none cs
+              | CProj (c, _) => none c
+
+              | CWild _ => false                
+
+        fun pos (c, _) =
+            case c of
+                CAnnot (c, _) => pos c
+
+              | TFun (c1, c2) => none c1 andalso pos c2
+              | TCFun (_, _, _, c) => pos c
+              | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+              | TRecord c => pos c
+
+              | CVar _ => true
+              | CApp (c1, c2) => pos c1 andalso none c2
+              | CAbs _ => false
+              | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+
+              | CName _ => true
+
+              | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
+              | CConcat (c1, c2) => pos c1 andalso pos c2
+              | CFold => true
+
+              | CUnit => true
+
+              | CTuple cs => List.all pos cs
+              | CProj (c, _) => pos c
+
+              | CWild _ => false
+    in
+        pos
+    end
+
 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
     let
         (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
@@ -2760,6 +2826,11 @@
                 end
               | L.DDatatype (x, xs, xcs) =>
                 let
+                    val positive = List.all (fn (_, to) =>
+                                                case to of
+                                                    NONE => true
+                                                  | SOME t => positive x t) xcs
+
                     val k = (L'.KType, loc)
                     val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
                     val (env, n) = E.pushCNamed env x k' NONE
@@ -2797,8 +2868,14 @@
                             (SS.empty, env, []) xcs
 
                     val env = E.pushDatatype env n xs xcs
+                    val d' = (L'.DDatatype (x, n, xs, xcs), loc)
                 in
-                    ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs' @ gs))
+                    if positive then
+                        ()
+                    else
+                        declError env (Nonpositive d');
+
+                    ([d'], (env, denv, gs' @ gs))
                 end
 
               | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
diff -r 9ad92047a499 -r f387d12193ba tests/datatype.ur
--- a/tests/datatype.ur	Sun Sep 07 15:40:42 2008 -0400
+++ b/tests/datatype.ur	Tue Sep 09 09:15:00 2008 -0400
@@ -11,3 +11,6 @@
 
 val nil = Nil
 val l1 = Cons {Head = 0, Tail = nil}
+
+datatype term = App of term * term | Abs of term -> term
+
diff -r 9ad92047a499 -r f387d12193ba tests/datatype.urp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/datatype.urp	Tue Sep 09 09:15:00 2008 -0400
@@ -0,0 +1,5 @@
+debug
+database dbname=test
+exe /tmp/webapp
+
+datatype