| ESkip => false
| ESet (_, e) => freeIn x e
- | EGet (x', _, b') => x <> x' andalso freeIn x b'
+ | EGet (x', _, _, b') => x <> x' andalso freeIn x b'
| ESeq es => List.exists (freeIn x) es
| ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
| EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
| ESkip => bAll
| ESet (v, b) => (ESet (v, subst x e b), loc)
- | EGet (x', v, b') =>
+ | EGet (x', topt, v, b') =>
if x = x' then
bAll
else if freeIn x' e then
let
val x'' = freshVar ()
in
- (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc)
+ (EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc)
end
else
- (EGet (x', v, subst x e b'), loc)
+ (EGet (x', topt, v, subst x e b'), loc)
| ESeq es => (ESeq (map (subst x e) es), loc)
| ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
| EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
| ESkip => eAll
| ESet (v, b) => (ESet (v, reduceExp G b), loc)
- | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc)
+ | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc)
| ESeq es => (ESeq (map (reduceExp G) es), loc)
| ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
| EWith (e1, e2) =>