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
+val ununify = Describe.ununify
+
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)
(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,
(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,
| 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
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