X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/095de39e1be653dcb6438d19c719bd7797e0772a..e1b99e23f8d30efc7842ee006e0ff3ef0347b7df:/src/tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index ac9fad5..6f62a6c 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -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 @@ -99,61 +103,6 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) = | _ => 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 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 (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2) @@ -170,6 +119,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 @@ -334,9 +285,26 @@ fun checkTyp G (tAll as (t, loc)) = | 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 + val dte = Describe.describe_type_error loc in case e of EInt _ => (TBase "int", loc) @@ -407,6 +375,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 @@ -467,21 +452,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 @@ -525,21 +514,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 @@ -659,8 +652,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 = @@ -672,12 +675,12 @@ 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