Fix type-checking of nested config functions

[hcoop/domtool2.git] / src / tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 6d58e43..9467b64 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -170,6 +170,8 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
       | (_, CPrefix p2) => predImplies (p1All, p2)
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
+      | (CRoot, CNot (CConst _, _)) => true
+      | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
 
       | _ => false
 
@@ -424,6 +426,23 @@ fun checkExp G (eAll as (e, loc)) =
                        (TError, loc))
            end
 
+         | EALam (x, p, e) =>
+           let
+               val p' = checkPred G p
+
+               val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+               val t' = whnorm (checkExp G' e)
+           in
+               case t' of
+                   (TAction _, _) => (TNested (p, t'), loc)
+                 | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
+                                         "action",
+                                         e,
+                                         t',
+                                         NONE));
+                         (TError, loc))
+           end
+
          | ESet (evar, e) =>
            let
                val t = checkExp G e