Fix a bug when renaming variables during ANF translation

When a binding like:

  let v = u

arose during the translation, the ANF could would simply rename v to
u. However, it was only doing it in the 'body' portion of the code,
not an associated context.
This commit is contained in:
Dan Doel 2022-03-30 17:21:32 -04:00
parent 7163508b62
commit ca1509a7b7
3 changed files with 104 additions and 1 deletions

View File

@ -1116,6 +1116,23 @@ fls, tru :: Var v => ANormal v
fls = TCon Ty.booleanRef 0 []
tru = TCon Ty.booleanRef 1 []
renameCtx :: Var v => v -> v -> Ctx v -> (Ctx v, Bool)
renameCtx v u (d, ctx) | (ctx, b) <- rn [] ctx = ((d, ctx), b)
where
swap w | w == v = u | otherwise = w
rn acc [] = (reverse acc, False)
rn acc (ST d vs ccs b : es)
| any (== v) vs = (reverse acc ++ e : es, True)
| otherwise = rn (e : acc) es
where
e = ST d vs ccs $ ABTN.rename v u b
rn acc (LZ w f as : es)
| w == v = (reverse acc ++ e : es, True)
| otherwise = rn (e : acc) es
where
e = LZ w (swap <$> f) (swap <$> as)
anfBlock :: Var v => Term v a -> ANFM v (Ctx v, DNormal v)
anfBlock (Var' v) = pure (mempty, pure $ TVar v)
anfBlock (If' c t f) = do
@ -1270,7 +1287,9 @@ anfBlock (Let1Named' v b e) =
anfBlock b >>= \case
(bctx, (Direct, TVar u)) -> do
(ectx, ce) <- anfBlock e
pure (bctx <> ectx, ABTN.rename v u <$> ce)
(ectx, shaded) <- pure $ renameCtx v u ectx
ce <- pure $ if shaded then ce else ABTN.rename v u <$> ce
pure (bctx <> ectx, ce)
(bctx, (d0, cb)) -> bindLocal [v] $ do
(ectx, ce) <- anfBlock e
d <- bindDirection d0

View File

@ -0,0 +1,33 @@
```ucm:hide
.> builtins.merge
```
This tests a variable related bug in the ANF compiler.
The nested let would get flattened out, resulting in:
bar = result
which would be handled by renaming. However, the _context_ portion of
the rest of the code was not being renamed correctly, so `bar` would
remain in the definition of `baz`.
```unison
foo _ =
id x = x
bar = let
Debug.watch "hello" "hello"
result = 5
Debug.watch "goodbye" "goodbye"
result
baz = id bar
baz
> !foo
```
```ucm
.> add
```

View File

@ -0,0 +1,51 @@
This tests a variable related bug in the ANF compiler.
The nested let would get flattened out, resulting in:
bar = result
which would be handled by renaming. However, the _context_ portion of
the rest of the code was not being renamed correctly, so `bar` would
remain in the definition of `baz`.
```unison
foo _ =
id x = x
bar = let
Debug.watch "hello" "hello"
result = 5
Debug.watch "goodbye" "goodbye"
result
baz = id bar
baz
> !foo
```
```ucm
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
foo : ∀ _. _ -> Nat
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
11 | > !foo
5
```
```ucm
.> add
⍟ I've added these definitions:
foo : ∀ _. _ -> Nat
```