Add if..then..else
[hcoop/domtool2.git] / src / tycheck.sml
index 8d35e2d..f68100f 100644 (file)
@@ -1,5 +1,5 @@
 (* HCoop Domtool (http://hcoop.sourceforge.net/)
- * Copyright (c) 2006, Adam Chlipala
+ * Copyright (c) 2006-2007, Adam Chlipala
  *
  * This program is free software; you can redistribute it and/or
  * modify it under the terms of the GNU General Public License
@@ -24,6 +24,10 @@ open Ast Print Env
 
 structure SM = StringMap
 
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
 local
     val unifCount = ref 0
 in
@@ -43,119 +47,6 @@ fun newUnif () =
     end
 end
            
-exception UnequalDomains
-         
-fun eqRecord f (r1, r2) =
-    (SM.appi (fn (k, v1) =>
-                case SM.find (r2, k) of
-                    NONE => raise UnequalDomains
-                  | SOME v2 =>
-                    if f (v1, v2) then
-                        ()
-                    else
-                        raise UnequalDomains) r1;
-     SM.appi (fn (k, v2) =>
-                case SM.find (r1, k) of
-                    NONE => raise UnequalDomains
-                  | SOME v1 =>
-                    if f (v1, v2) then
-                        ()
-                    else
-                        raise UnequalDomains) r2;
-     true)
-    handle UnequalDomains => false
-
-fun eqPred ((p1, _), (p2, _)) =
-    case (p1, p2) of
-       (CRoot, CRoot) => true
-      | (CConst s1, CConst s2) => s1 = s2
-      | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
-      | (CNot p1, CNot p2) => eqPred (p1, p2)
-      | (CAnd (p1, q1), CAnd (p2, q2)) =>
-       eqPred (p1, p2) andalso eqPred (q1, q2)
-
-      | _ => false
-
-fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
-    case (t1, t2) of
-       (TBase s1, TBase s2) => s1 = s2
-      | (TList t1, TList t2) => eqTy (t1, t2)
-      | (TArrow (d1, r1), TArrow (d2, r2)) =>
-       eqTy (d1, d2) andalso eqTy (r1, r2)
-
-      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
-       eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
-       andalso eqRecord eqTy (r1, r2)
-
-      | (TNested (p1, q1), TNested (p2, q2)) =>
-       eqPred (p1, p2) andalso eqTy (q1, q2)
-
-      | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
-      | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
-
-      | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
-
-      | (TError, TError) => true
-
-      | _ => false
-
-datatype unification_error =
-        UnifyPred of pred * pred
-       | UnifyTyp of typ * typ
-       | UnifyOccurs of string * typ
-
-exception Unify of unification_error
-
-datatype type_error =
-        WrongType of string * exp * typ * typ * unification_error option
-       | WrongForm of string * string * exp * typ * unification_error option
-       | UnboundVariable of string
-       | WrongPred of string * pred * pred
-
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
-                                       [PD.string s, PD.space 1, d]))
-
-fun describe_unification_error t ue =
-    case ue of
-       UnifyPred (p1, p2) =>
-       (print "Reason: Incompatible contexts.\n";
-        preface ("Have:", p_pred p1);
-        preface ("Need:", p_pred p2))
-      | UnifyTyp (t1, t2) =>
-       if eqTy (t, t1) then
-           ()
-       else
-           (print "Reason: Incompatible types.\n";
-            preface ("Have:", p_typ t1);
-            preface ("Need:", p_typ t2))
-      | UnifyOccurs (name, t') =>
-       if eqTy (t, t') then
-           ()
-       else
-           (print "Reason: Occurs check failed for ";
-            print name;
-            print " in:\n";
-            printd (p_typ t))
-
-fun describe_type_error loc te =
-    case te of
-       WrongType (place, e, t1, t2, ueo) =>
-       (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
-        preface (" Expression:", p_exp e);
-        preface ("Actual type:", p_typ t1);
-        preface ("Needed type:", p_typ t2);
-        Option.app (describe_unification_error t1) ueo)
-      |        WrongForm (place, form, e, t, ueo) =>
-       (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
-        preface ("Expression:", p_exp e);
-        preface ("      Type:", p_typ t);
-        Option.app (describe_unification_error t) ueo)
-      | UnboundVariable name =>
-       ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
-      |        WrongPred (place, p1, p2) =>
-       (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
-        preface ("Have:", p_pred p1);
-        preface ("Need:", p_pred p2))
 
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
@@ -173,6 +64,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
 
@@ -206,7 +99,7 @@ fun subPred (p1, p2) =
 fun subRecord f (r1, r2) =
     SM.appi (fn (k, v2) =>
                case SM.find (r1, k) of
-                   NONE => raise UnequalDomains
+                   NONE => raise Describe.UnequalDomains
                  | SOME v1 => f (v1, v2)) r2
 
 fun occurs u (t, _) =
@@ -281,17 +174,50 @@ fun whnorm (tAll as (t, loc)) =
        TUnif (_, ref (SOME tAll)) => whnorm tAll
       | _ => tAll
 
+fun baseCondition t =
+    case whnorm t of
+       (TBase name, _) => typeRule name
+      | (TList t, _) =>
+       (case baseCondition t of
+            NONE => NONE
+          | SOME f => SOME (fn (EList ls, _) => List.all f ls
+                             | _ => false))
+      | _ => NONE
+
+fun simplifyKindOf e =
+    case e of
+       (EApp ((EVar s, _), e'), _) =>
+       (case Env.function s of
+            NONE => e
+          | SOME f =>
+            case f [e'] of
+                NONE => e
+              | SOME e => e)
+      | _ => e
+
 fun hasTyp (e, t1, t2) =
-    case whnorm t2 of
-       (TBase name, _) =>
-       (case typeRule name of
-            NONE => subTyp (t1, t2)
-          | SOME rule =>
-            if rule e then
-                ()
-            else
-                subTyp (t1, t2))
-      | _ => subTyp (t1, t2)
+    if (case baseCondition t2 of
+           NONE => false
+         | SOME rule => rule (simplifyKindOf e)) then
+       ()
+    else
+       subTyp (t1, t2)
+
+fun checkPred G (p, loc) =
+    let
+       val err = ErrorMsg.error (SOME loc)
+    in
+       case p of
+           CRoot => ()
+         | CConst s =>
+           if lookupContext G s then
+               ()
+           else
+               err ("Unbound context " ^ s)
+         | CPrefix p => checkPred G p
+         | CNot p => checkPred G p
+         | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
+    end
 
 fun checkTyp G (tAll as (t, loc)) =
     let
@@ -306,16 +232,40 @@ fun checkTyp G (tAll as (t, loc)) =
                 (TError, loc))
          | TList t => (TList (checkTyp G t), loc)
          | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
-         | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
-                                          SM.map (checkTyp G) r), loc)
-         | TNested (p, t) => (TNested (p, checkTyp G t), loc)
+         | TAction (p, d, r) => (checkPred G p;
+                                 (TAction (p, SM.map (checkTyp G) d,
+                                           SM.map (checkTyp G) r), loc))
+         | TNested (p, t) => (checkPred G p;
+                              (TNested (p, checkTyp G t), loc))
          | TError => raise Fail "TError in parser-generated type"
          | TUnif _ => raise Fail "TUnif in parser-generated type"
     end
 
+fun envVarSetFrom v (e, _) =
+    case e of
+       ESet (v', e) =>
+       if v = v' then
+           SOME e
+       else
+           NONE
+      | EGet (_, _, _, e) => envVarSetFrom v e
+      | ESeq es => foldr (fn (e, found) =>
+                            case found of
+                                SOME _ => found
+                              | NONE => envVarSetFrom v e)
+                        NONE es
+      | ELocal (_, e) => envVarSetFrom v e
+
+      | _ => NONE
+
+fun ununify (tAll as (t, _)) =
+    case t of
+       TUnif (_, ref (SOME t)) => ununify t
+      | _ => tAll
+
 fun checkExp G (eAll as (e, loc)) =
     let
-       val dte = describe_type_error loc
+       val dte = Describe.describe_type_error loc
     in
        case e of
            EInt _ => (TBase "int", loc)
@@ -386,6 +336,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
@@ -395,14 +362,18 @@ fun checkExp G (eAll as (e, loc)) =
                          SM.insert (SM.empty, evar, t)),
                 loc)
            end
-         | EGet (x, evar, rest) =>
+         | EGet (x, topt, evar, rest) =>
            let
                val xt = (newUnif (), loc)
                val G' = bindVal G (x, xt, NONE)
 
                val rt = whnorm (checkExp G' rest)
            in
-               case rt of
+               case topt of
+                   NONE => ()
+                 | SOME t => subTyp (xt, checkTyp G t);
+
+               case ununify rt of
                    (TAction (p, d, r), _) =>
                    (case SM.find (d, evar) of
                         NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
@@ -446,21 +417,25 @@ fun checkExp G (eAll as (e, loc)) =
                                                        (case SM.find (d', name) of
                                                             NONE => SM.insert (d', name, t)
                                                           | SOME t' =>
-                                                            (subTyp (t, t')
+                                                            ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t, t')
+                                                                | SOME e => hasTyp (e, t, t'))
                                                              handle Unify ue =>
                                                                     dte (WrongType ("Shared environment variable",
                                                                                     (EVar name, loc),
-                                                                                    t,
                                                                                     t',
+                                                                                    t,
                                                                                     SOME ue));
                                                              d'))
                                                      | SOME t' =>
-                                                       (subTyp (t, t')
+                                                       ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t, t')
+                                                                | SOME e => hasTyp (e, t, t'))
                                                         handle Unify ue =>
                                                                dte (WrongType ("Shared environment variable",
                                                                                (EVar name, loc),
-                                                                               t,
                                                                                t',
+                                                                               t,
                                                                                SOME ue));
                                                         d'))
                                                d1 d2
@@ -504,21 +479,25 @@ fun checkExp G (eAll as (e, loc)) =
                                                        (case SM.find (d', name) of
                                                             NONE => SM.insert (d', name, t)
                                                           | SOME t' =>
-                                                            (subTyp (t, t')
+                                                            ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t', t)
+                                                                | SOME e => hasTyp (e, t', t))
                                                              handle Unify ue =>
                                                                     dte (WrongType ("Shared environment variable",
                                                                                     (EVar name, loc),
-                                                                                    t,
                                                                                     t',
+                                                                                    t,
                                                                                     SOME ue));
                                                              d'))
                                                      | SOME t' =>
-                                                       (subTyp (t, t')
+                                                       ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t', t)
+                                                                | SOME e => hasTyp (e, t', t))
                                                         handle Unify ue =>
                                                                dte (WrongType ("Shared environment variable",
                                                                                (EVar name, loc),
-                                                                               t,
                                                                                t',
+                                                                               t,
                                                                                SOME ue));
                                                         d'))
                                                d1 d2
@@ -592,6 +571,33 @@ fun checkExp G (eAll as (e, loc)) =
 
          | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
                               SM.empty, SM.empty), loc)
+
+         | EIf (e1, e2, e3) =>
+           let
+               val t = (newUnif (), loc)
+
+               val t1 = checkExp G e1
+               val t2 = checkExp G e2
+               val t3 = checkExp G e3
+               val bool = (TBase "bool", loc)
+           in
+               (subTyp (t1, bool))
+               handle Unify ue =>
+                      dte (WrongType ("\"If\" test",
+                                      e1,
+                                      t1,
+                                      bool,
+                                      SOME ue));
+               subTyp (t2, t);
+               (subTyp (t3, t))
+               handle Unify ue =>
+                      dte (WrongType ("\"Else\" case",
+                                      eAll,
+                                      t3,
+                                      t2,
+                                      SOME ue));
+               t
+           end
     end
 
 exception Ununif
@@ -632,14 +638,24 @@ fun checkUnit G (eAll as (_, loc)) =
            ununif t
            handle Ununif =>
                   (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
-                   printd (p_typ t);
+                   output (p_typ t);
                    t)
     end
 
 fun checkDecl G (d, _, loc) =
     case d of
-       DExternType name => bindType G name
-      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+       DExternType name =>
+       if !externFlag then
+           bindType G name
+       else
+           (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
+            G)
+      | DExternVal (name, t) =>
+       if !externFlag then
+           bindVal G (name, checkTyp G t, NONE)
+       else
+           (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
+            G)
       | DVal (name, to, e) =>
        let
            val to =
@@ -651,16 +667,67 @@ fun checkDecl G (d, _, loc) =
        in
            hasTyp (e, t, to)
            handle Unify ue =>
-                  describe_type_error loc
-                                      (WrongType ("Bound value",
-                                                  e,
-                                                  t,
-                                                  to,
-                                                  SOME ue));
+                  Describe.describe_type_error loc
+                                               (WrongType ("Bound value",
+                                                           e,
+                                                           t,
+                                                           to,
+                                                           SOME ue));
            bindVal G (name, to, SOME e)
        end
+      | DContext name => bindContext G name
+
+fun printActionDiffs {have, need} =
+    case (ununif have, ununif need) of
+       ((TAction (p1, in1, out1), loc), (TAction (p2, in2, out2), _)) =>
+       let
+           fun checkPreds () =
+               if predImplies (p1, p2) then
+                   ()
+               else
+                   (ErrorMsg.error (SOME loc) "Files provides the wrong kind of configuration.";
+                    preface ("Have:", p_pred p1);
+                    preface ("Need:", p_pred p2))
+
+           fun checkIn () =
+               SM.appi (fn (name, t) =>
+                           case SM.find (in2, name) of
+                               NONE => (ErrorMsg.error (SOME loc) "An unavailable environment variable is used.";
+                                        print ("Name: " ^ name ^ "\n");
+                                        preface ("Type:", p_typ t))
+                             | SOME t' =>
+                               subTyp (t', t)
+                               handle Unify _ =>
+                                      (ErrorMsg.error (SOME loc) "Wrong type for environment variable.";
+                                       print ("          Name: " ^ name ^ "\n");
+                                       preface ("      Has type:", p_typ t');
+                                       preface ("Used with type:", p_typ t)))
+                       in1
+                       
+           fun checkOut () =
+               SM.appi (fn (name, t) =>
+                           case SM.find (out1, name) of
+                               NONE => (ErrorMsg.error (SOME loc) "Missing an output environment variable.";
+                                        print ("Name: " ^ name ^ "\n");
+                                        preface ("Type:", p_typ t))
+                             | SOME t' =>
+                               subTyp (t', t)
+                               handle Unify _ =>
+                                      (ErrorMsg.error (SOME loc) "Wrong type for output environment variable.";
+                                       print ("     Name: " ^ name ^ "\n");
+                                       preface (" Has type:", p_typ t');
+                                       preface ("Need type:", p_typ t)))
+                       out2
+       in
+           checkPreds ();
+           checkIn ();
+           checkOut ();
+           true
+       end
+       
+      | _ => false
 
-fun checkFile G tInit (ds, eo) =
+fun checkFile G tInit (_, ds, eo) =
     let
        val G' = foldl (fn (d, G) => checkDecl G d) G ds
     in
@@ -671,10 +738,11 @@ fun checkFile G tInit (ds, eo) =
                val t = checkExp G' e
            in
                hasTyp (e, t, tInit)
-               handle Unify ue =>
-                      (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
-                       preface ("Actual:", p_typ t);
-                       preface ("Needed:", p_typ tInit))
+               handle Unify _ =>
+                      if printActionDiffs {have = t, need = tInit} then
+                          ()
+                      else
+                          ErrorMsg.error (SOME loc) "File ends in something that isn't a directive."                      
            end;
        G'
     end