+
+ | EALam (x, p, e) =>
+ let
+ val p' = checkPred G p
+
+ val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+ val t' = whnorm (checkExp G' e)
+ in
+ case t' of
+ (TAction _, _) => (TNested (p, t'), loc)
+ | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
+ "action",
+ e,
+ t',
+ NONE));
+ (TError, loc))
+ end
+
+ | ESet (evar, e) =>
+ let
+ val t = checkExp G e
+ in
+ (TAction ((CPrefix (CRoot, loc), loc),
+ SM.empty,
+ SM.insert (SM.empty, evar, t)),
+ loc)
+ end
+ | 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 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)
+ | SOME xt' =>
+ (subTyp (xt', xt)
+ handle Unify ue =>
+ dte (WrongType ("Retrieved environment variable",
+ (EVar x, loc),
+ xt',
+ xt,
+ SOME ue));
+ rt))
+ | (TError, _) => rt
+ | _ => (dte (WrongForm ("Body of environment variable read",
+ "action",
+ rest,
+ rt,
+ NONE));
+ (TError, loc))
+ end
+
+ | ESeq [] => raise Fail "Empty ESeq"
+ | ESeq [e1] => checkExp G e1
+ | ESeq (e1 :: rest) =>
+ let
+ val e2 = (ESeq rest, loc)
+
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
+ in
+ case t1 of
+ (TAction (p1, d1, r1), _) =>
+ (case t2 of
+ (TAction (p2, d2, r2), _) =>
+ let
+ val p' = predSimpl (CAnd (p1, p2), loc)
+
+ val d' = SM.foldli (fn (name, t, d') =>
+ case SM.find (r1, name) of
+ NONE =>
+ (case SM.find (d', name) of
+ NONE => SM.insert (d', name, t)
+ | SOME t' =>
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t, t')
+ | SOME e => hasTyp (e, t, t'))
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t',
+ t,
+ SOME ue));
+ d'))
+ | SOME t' =>
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t, t')
+ | SOME e => hasTyp (e, t, t'))
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t',
+ t,
+ SOME ue));
+ d'))
+ d1 d2
+
+ val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
+ r1 r2
+ in
+ (TAction (p', d', r'), loc)
+ end
+ | (TError, _) => t2
+ | _ => (dte (WrongForm ("First action to be sequenced",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ => (dte (WrongForm ("Second action to be sequenced",
+ "action",
+ e1,
+ t1,
+ NONE));
+ (TError, loc))
+ end
+
+ | ELocal (e1, e2) =>
+ let
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
+ in
+ case t1 of
+ (TAction (p1, d1, r1), _) =>
+ (case t2 of
+ (TAction (p2, d2, r2), _) =>
+ let
+ val p' = predSimpl (CAnd (p1, p2), loc)
+
+ val d' = SM.foldli (fn (name, t, d') =>
+ case SM.find (r1, name) of
+ NONE =>
+ (case SM.find (d', name) of
+ NONE => SM.insert (d', name, t)
+ | SOME t' =>
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t', t)
+ | SOME e => hasTyp (e, t', t))
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t',
+ t,
+ SOME ue));
+ d'))
+ | SOME t' =>
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t', t)
+ | SOME e => hasTyp (e, t', t))
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t',
+ t,
+ SOME ue));
+ d'))
+ d1 d2
+ in
+ (TAction (p', d', r2), loc)
+ end
+ | (TError, _) => t2
+ | _ => (dte (WrongForm ("Body of local settings",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ => (dte (WrongForm ("Local settings",
+ "action",
+ e1,
+ t1,
+ NONE));
+ (TError, loc))
+ end
+
+
+ | EWith (e1, e2) =>
+ let
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
+ in
+ case t1 of
+ (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
+ (case t2 of
+ (TAction (p, d, r), _) =>
+ if predImplies (pd, p) then
+ let
+ val combineRecs =
+ SM.unionWithi (fn (name, t1, t2) =>
+ (subTyp (t1, t2)
+ handle Unify ue =>
+ dte (WrongType ("Environment variable",
+ (EVar name, loc),
+ t1,
+ t2,
+ SOME ue));
+ t2))
+ in
+ (TAction (pr, combineRecs (d, d1),
+ combineRecs (r, r1)), loc)
+ end
+ else
+ (dte (WrongPred ("nested action",
+ pd,
+ p));
+ (TError, loc))
+ | (TError, _) => t2
+ | _ =>
+ (dte (WrongForm ("Body of nested action",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ =>
+ (dte (WrongForm ("Container of nested action",
+ "action",
+ e1,
+ t1,
+ NONE));
+ (TError, loc))
+ end
+
+ | 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