+fun baseCondition t =
+ case whnorm t of
+ (TBase name, _) => typeRule name
+ | (TList t, _) =>
+ (case baseCondition t of
+ NONE => NONE
+ | SOME f => SOME (fn (EList ls, _) => List.all f ls
+ | _ => false))
+ | _ => NONE
+
+fun hasTyp (e, t1, t2) =
+ if (case baseCondition t2 of
+ NONE => false
+ | SOME rule => rule e) then
+ ()
+ else
+ subTyp (t1, t2)
+
+fun checkPred G (p, loc) =
+ let
+ val err = ErrorMsg.error (SOME loc)
+ in
+ case p of
+ CRoot => ()
+ | CConst s =>
+ if lookupContext G s then
+ ()
+ else
+ err ("Unbound context " ^ s)
+ | CPrefix p => checkPred G p
+ | CNot p => checkPred G p
+ | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
+ end
+
+fun checkTyp G (tAll as (t, loc)) =
+ let
+ val err = ErrorMsg.error (SOME loc)
+ in
+ case t of
+ TBase name =>
+ if lookupType G name then
+ tAll
+ else
+ (err ("Unbound type name " ^ name);
+ (TError, loc))
+ | TList t => (TList (checkTyp G t), loc)
+ | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
+ | TAction (p, d, r) => (checkPred G p;
+ (TAction (p, SM.map (checkTyp G) d,
+ SM.map (checkTyp G) r), loc))
+ | TNested (p, t) => (checkPred G p;
+ (TNested (p, checkTyp G t), loc))
+ | TError => raise Fail "TError in parser-generated type"
+ | TUnif _ => raise Fail "TUnif in parser-generated type"
+ end
+
+fun envVarSetFrom v (e, _) =
+ case e of
+ ESet (v', e) =>
+ if v = v' then
+ SOME e
+ else
+ NONE
+ | EGet (_, _, e) => envVarSetFrom v e
+ | ESeq es => foldr (fn (e, found) =>
+ case found of
+ SOME _ => found
+ | NONE => envVarSetFrom v e)
+ NONE es
+ | ELocal (_, e) => envVarSetFrom v e
+
+ | _ => NONE
+