| EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
| EALam (x', _, b') => x <> x' andalso freeIn x b'
+ | EIf (e1, e2, e3) => freeIn x e1 orelse freeIn x e2 orelse freeIn x e3
+
local
val freshCount = ref 0
in
else
(EALam (x', p, subst x e b'), loc)
+ | EIf (b1, b2, b3) => (EIf (subst x e b1, subst x e b2, subst x e b3), loc)
+
fun findPrim (e, _) =
case e of
EApp (f, x) =>
(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
+
end