X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/e1b99e23f8d30efc7842ee006e0ff3ef0347b7df..06bd821502f57dcb4ef89295b221fc2b9a4f1ae3:/src/tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index 6f62a6c..12efce3 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -47,61 +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 fun predImplies (p1All as (p1, _), p2All as (p2, _)) = case (p1, p2) of @@ -154,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, _) = @@ -239,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) @@ -292,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 @@ -302,6 +258,8 @@ fun envVarSetFrom v (e, _) = | _ => NONE +val ununify = Describe.ununify + fun checkExp G (eAll as (e, loc)) = let val dte = Describe.describe_type_error loc @@ -401,14 +359,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) @@ -481,14 +443,14 @@ fun checkExp G (eAll as (e, loc)) = (TAction (p', d', r'), loc) end | (TError, _) => t2 - | _ => (dte (WrongForm ("Action to be sequenced", + | _ => (dte (WrongForm ("First action to be sequenced", "action", e2, t2, NONE)); (TError, loc))) | (TError, _) => t1 - | _ => (dte (WrongForm ("Action to be sequenced", + | _ => (dte (WrongForm ("Second action to be sequenced", "action", e1, t1, @@ -540,14 +502,14 @@ fun checkExp G (eAll as (e, loc)) = (TAction (p', d', r2), loc) end | (TError, _) => t2 - | _ => (dte (WrongForm ("Action to be sequenced", + | _ => (dte (WrongForm ("Body of local settings", "action", e2, t2, NONE)); (TError, loc))) | (TError, _) => t1 - | _ => (dte (WrongForm ("Action to be sequenced", + | _ => (dte (WrongForm ("Local settings", "action", e1, t1, @@ -606,6 +568,32 @@ fun checkExp G (eAll as (e, loc)) = | ESkip => (TAction ((CPrefix (CRoot, loc), loc), SM.empty, SM.empty), loc) + + | EIf (e1, e2, e3) => + let + 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, t3); t3) + handle Unify _ => + ((subTyp (t3, t2); t2) + handle Unify ue => + (dte (WrongType ("\"else\" case", + eAll, + t3, + t2, + SOME ue)); + (TError, loc))) + end end exception Ununif @@ -646,7 +634,7 @@ 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 @@ -685,6 +673,56 @@ fun checkDecl G (d, _, loc) = 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) = let val G' = foldl (fn (d, G) => checkDecl G d) G ds @@ -696,10 +734,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