- case rt of
- (TAction (p, d, _), _) =>
- (TAction (p, d, SM.empty), loc)
- | (TError, _) => rt
- | _ => (dte (WrongForm ("Body of local action",
+ 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 ("Action to be sequenced",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ => (dte (WrongForm ("Action to be sequenced",