(* 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 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 printActionDiffs {have, need} =
| _ => false
-fun checkFile G tInit (_, ds, eo) =
+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 _ =>