- 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' =>
+ (subTyp (t, t')
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t,
+ t',
+ SOME ue));
+ d'))
+ | SOME t' =>
+ (subTyp (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",