- | EWith (e1, e2) => (EWith (reduceExp G e1, reduceExp G e2), loc)
+ | EWith (e1, e2) =>
+ let
+ val e1' = reduceExp G e1
+ val e2' = reduceExp G e2
+ in
+ case e1' of
+ (EALam (x, _, b), _) => reduceExp G (subst x e2' b)
+ | _ => (EWith (e1', e2'), loc)
+ end
+ | EALam (x, p, e) =>
+ let
+ val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+ in
+ (EALam (x, p, reduceExp G' e), loc)
+ end
+
+ | EIf (e1, e2, e3) =>
+ let
+ val e1' = reduceExp G e1
+ fun e2' () = reduceExp G e2
+ fun e3' () = reduceExp G e3
+ in
+ case e1' of
+ (EVar "true", _) => e2' ()
+ | (EVar "false", _) => e3' ()
+ | _ => (EIf (e1', e2' (), e3' ()), loc)
+ end