(* HCoop Domtool (http://hcoop.sourceforge.net/)
* Copyright (c) 2006-2007, Adam Chlipala
+ * Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
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
SOME ue));
bindVal G (name, to, SOME e)
end
+ | DEnv (name, to, e) =>
+ let
+ val to =
+ case to of
+ NONE => (newUnif (), loc)
+ | SOME to => checkTyp G to
+
+ val t = checkExp G e
+ in
+ hasTyp (e, t, to)
+ handle Unify ue =>
+ Describe.describe_type_error loc
+ (WrongType ("Dynamically bound value",
+ e,
+ t,
+ to,
+ SOME ue));
+ bindInitialDynEnvVal G (name, to, e)
+ end
| DContext name => bindContext G name
-fun checkFile G tInit (_, ds, eo) =
+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 (prog as (_, ds, eo)) =
let
val G' = foldl (fn (d, G) => checkDecl G d) G ds
+
+ fun tInitial prog env =
+ (* This should likely only take the dynamic env as an argument *)
+ let
+ fun allSets (e, _) =
+ case e of
+ ESkip => true
+ | ESet _ => true
+ | ESeq es => List.all allSets es
+ | _ => false
+
+ val dmy = ErrorMsg.dummyLoc
+
+ fun bodyType (_, _, SOME e) =
+ if allSets e then
+ (CPrefix (CRoot, dmy), dmy)
+ else
+ (CRoot, dmy)
+ | bodyType _ = (CRoot, dmy)
+ in
+ (TAction (bodyType prog,
+ Env.initialDynEnvTypes env,
+ StringMap.empty),
+ dmy)
+ end
+
in
case eo of
NONE => ()
| SOME (e as (_, loc)) =>
let
val t = checkExp G' e
+ val tInit = tInitial prog G'
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
HCoop / hcoop / domtool2.git / blobdiff