X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/492c1cff68a2da969a559627725369c211470c92..411a85f26421358c20b11839310cce6caff8cf77:/src/tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index fa006df..007a0fe 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -14,7 +14,7 @@ * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. -*) + *) (* Domtool configuration language type checking *) @@ -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 @@ -112,9 +116,6 @@ datatype type_error = | 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) => @@ -173,6 +174,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 @@ -281,6 +284,40 @@ 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 hasTyp (e, t1, t2) = + if (case baseCondition t2 of + NONE => false + | SOME rule => rule 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 val err = ErrorMsg.error (SOME loc) @@ -294,13 +331,32 @@ 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 checkExp G (eAll as (e, loc)) = let val dte = describe_type_error loc @@ -316,7 +372,7 @@ fun checkExp G (eAll as (e, loc)) = let val t' = checkExp G e' in - (subTyp (t', t); + (hasTyp (eAll, t', t); if isError t' then (TList (TError, loc), loc) else @@ -356,8 +412,8 @@ fun checkExp G (eAll as (e, loc)) = val tf = checkExp G func val ta = checkExp G arg in - (subTyp (tf, (TArrow (dom, ran), loc)); - subTyp (ta, dom) + (hasTyp (func, tf, (TArrow (dom, ran), loc)); + hasTyp (arg, ta, dom) handle Unify ue => dte (WrongType ("Function argument", arg, @@ -374,6 +430,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 @@ -434,21 +507,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 @@ -492,21 +569,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 @@ -626,8 +707,18 @@ fun checkUnit G (eAll as (_, loc)) = 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 = @@ -637,7 +728,7 @@ fun checkDecl G (d, _, loc) = val t = checkExp G e in - subTyp (t, to) + hasTyp (e, t, to) handle Unify ue => describe_type_error loc (WrongType ("Bound value", @@ -647,8 +738,9 @@ fun checkDecl G (d, _, loc) = SOME ue)); bindVal G (name, to, SOME e) end + | DContext name => bindContext G name -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 @@ -658,7 +750,7 @@ fun checkFile G tInit (ds, eo) = let val t = checkExp G' e in - subTyp (t, tInit) + hasTyp (e, t, tInit) handle Unify ue => (ErrorMsg.error (SOME loc) "Bad type for final expression of source file."; preface ("Actual:", p_typ t);