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
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, _) =
| _ => 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)
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
| _ => 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.describe_type_error 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)
ununif t
handle Ununif =>
(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
- printd (p_typ t);
+ output (p_typ t);
t)
end
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
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