changeset 238:44a1663ad893

Checking for well-formed 'val rec'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 13:13:16 -0400
parents 9182068c9d7c
children fc6f04889bf2
files src/elaborate.sml tests/recBad.lac
diffstat 2 files changed, 25 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/elaborate.sml	Thu Aug 28 12:58:11 2008 -0400
+++ b/src/elaborate.sml	Thu Aug 28 13:13:16 2008 -0400
@@ -1033,6 +1033,7 @@
      | DuplicatePatField of ErrorMsg.span * string
      | Unresolvable of ErrorMsg.span * L'.con
      | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
+     | IllegalRec of string * L'.exp
 
 fun expError env err =
     case err of
@@ -1082,6 +1083,10 @@
       | Unresolvable (loc, c) =>
         (ErrorMsg.errorAt loc "Can't resolve type class instance";
          eprefaces' [("Class constraint", p_con env c)])
+      | IllegalRec (x, e) =>
+        (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
+         eprefaces' [("Variable", PD.string x),
+                     ("Expression", p_exp env e)])
          
 fun checkCon (env, denv) e c1 c2 =
     unifyCons (env, denv) c1 c2
@@ -2826,6 +2831,13 @@
         end
       | L.DValRec vis =>
         let
+            fun allowable (e, _) =
+                case e of
+                    L.EAbs _ => true
+                  | L.ECAbs (_, _, _, e) => allowable e
+                  | L.EDisjoint (_, _, e) => allowable e
+                  | _ => false
+
             val (vis, gs) = ListUtil.foldlMap
                                 (fn ((x, co, e), gs) =>
                                     let
@@ -2849,6 +2861,10 @@
                                                                           
                                                       val gs2 = checkCon (env, denv) e' et c'
                                                   in
+                                                      if allowable e then
+                                                          ()
+                                                      else
+                                                          expError env (IllegalRec (x, e'));
                                                       ((x, n, c', e'), gs1 @ enD gs2 @ gs)
                                                   end) gs vis
         in
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/recBad.lac	Thu Aug 28 13:13:16 2008 -0400
@@ -0,0 +1,9 @@
+datatype list a = Nil | Cons of a * list a
+
+val rec append : t ::: Type -> list t -> list t -> list t = fn t ::: Type => fn ls1 => fn ls2 =>
+        case ls1 of
+            Nil => ls2
+          | Cons (h, t) => Cons (h, append t ls2)
+
+(*val rec ones : list int = Cons (1, ones)*)
+val rec ones : unit -> list int = fn () => Cons (1, ones ())