X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/6bb366c5a60247419dce5cbce4a5c034fa2f1e5c..d300166d083192ef3d4242013adcef345b0126f3:/src/tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index f1c90dc..8889540 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 @@ -43,116 +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 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 @@ -205,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, _) = @@ -290,10 +184,21 @@ fun baseCondition t = | _ => 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) = if (case baseCondition t2 of NONE => false - | SOME rule => rule e) then + | SOME rule => rule (simplifyKindOf e)) then () else subTyp (t1, t2) @@ -343,7 +248,7 @@ fun envVarSetFrom v (e, _) = SOME e else NONE - | EGet (_, _, e) => envVarSetFrom v e + | EGet (_, _, _, e) => envVarSetFrom v e | ESeq es => foldr (fn (e, found) => case found of SOME _ => found @@ -353,9 +258,14 @@ fun 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) @@ -431,7 +341,7 @@ fun checkExp G (eAll as (e, loc)) = val p' = checkPred G p val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE) - val t' = checkExp G' e + val t' = whnorm (checkExp G' e) in case t' of (TAction _, _) => (TNested (p, t'), loc) @@ -452,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) @@ -697,14 +611,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 = @@ -716,12 +640,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