anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-12 14:28:08 +03:00
Code Issues Projects Releases Wiki Activity

Fix de Bruijn indices in rmap (#1898)

Browse Source 
There was a subtle bug in `rmap` when `recur` was called on a variable.
This PR fixes it.
This commit is contained in:
Łukasz Czajka 2023-03-17 13:11:36 +01:00 committed by GitHub
parent 3dac3c87c9
commit bd17e957a1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 48 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
src/Juvix/Compiler/Core/Extra/Recursors/RMap.hs
View File

@ -66,21 +66,7 @@ rmapG coll f = go mempty 0 (coll ^. cEmpty)
go binders bl c n = f recur c n go binders bl c n = f recur c n
where where
recur :: c -> [BinderChange] -> Node -> m Node recur :: c -> [BinderChange] -> Node -> m Node
recur c' changes = \case recur c' changes =
NVar v ->
return $
maybe
(NVar v {_varIndex = getBinderIndex bl lvl})
(shift (bl - lvl))
mnode
where
(lvl, mnode) = BL.lookup (v ^. varIndex) binders
n' ->
let ni = destruct n'
in reassembleDetails ni <$> mapM goChild (ni ^. nodeChildren)
where
goChild :: NodeChild -> m Node
goChild ch =
let (bl', rbs, rbs') = let (bl', rbs, rbs') =
foldl' foldl'
( \(l, bs, acc) chg -> case chg of ( \(l, bs, acc) chg -> case chg of
@ -90,10 +76,26 @@ rmapG coll f = go mempty 0 (coll ^. cEmpty)
) )
(bl, [], []) (bl, [], [])
changes changes
cbs = map (\l -> (l, Nothing)) [bl' .. bl' + ch ^. childBindersNum - 1] binders' = BL.prepend rbs' binders
binders' = BL.prependRev cbs (BL.prepend rbs' binders) in \case
NVar v ->
return $
maybe
(NVar v {_varIndex = getBinderIndex bl' lvl})
(shift (bl' - lvl))
mnode
where
(lvl, mnode) = BL.lookup (v ^. varIndex) binders'
n' ->
let ni = destruct n'
in reassembleDetails ni <$> mapM goChild (ni ^. nodeChildren)
where
goChild :: NodeChild -> m Node
goChild ch =
let cbs = map (\l -> (l, Nothing)) [bl' .. bl' + ch ^. childBindersNum - 1]
binders'' = BL.prependRev cbs binders'
in go in go
binders' binders''
(bl' + ch ^. childBindersNum) (bl' + ch ^. childBindersNum)
((coll ^. cCollect) (length rbs + ch ^. childBindersNum, reverse rbs ++ ch ^. childBinders) c') ((coll ^. cCollect) (length rbs + ch ^. childBindersNum, reverse rbs ++ ch ^. childBinders) c')
(ch ^. childNode) (ch ^. childNode)

15
test/Core/Recursor/RMap.hs
View File

@ -28,6 +28,9 @@ tests =
addLambdas addLambdas
[ ( mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkVar' 1, mkVar' 0]), [ ( mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkVar' 1, mkVar' 0]),
mkLambdas' [mkDynamic', mkTypeInteger', mkDynamic', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0]) mkLambdas' [mkDynamic', mkTypeInteger', mkDynamic', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0])
),
( mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkVar' 1),
mkLambdas' [mkDynamic', mkTypeInteger', mkDynamic', mkTypeInteger'] (mkVar' 2)
) )
], ],
UnitTest UnitTest
@ -38,6 +41,9 @@ tests =
), ),
( mkLambda' mkTypeInteger' $ mkLet' mkTypeInteger' (mkVar' 0) $ mkLambda' mkTypeInteger' $ mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0], ( mkLambda' mkTypeInteger' $ mkLet' mkTypeInteger' (mkVar' 0) $ mkLambda' mkTypeInteger' $ mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0],
mkLets' [(mkTypeInteger', mkConstant' (ConstInteger 0)), (mkTypeInteger', mkVar' 0), (mkTypeInteger', mkConstant' (ConstInteger 2))] (mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0]) mkLets' [(mkTypeInteger', mkConstant' (ConstInteger 0)), (mkTypeInteger', mkVar' 0), (mkTypeInteger', mkConstant' (ConstInteger 2))] (mkBuiltinApp' OpIntAdd [mkVar' 2, mkVar' 0])
),
( mkLambda' mkTypeInteger' $ mkVar' 0,
mkLet' mkTypeInteger' (mkConstant' (ConstInteger 0)) (mkVar' 0)
) )
], ],
UnitTest UnitTest
@ -45,6 +51,15 @@ tests =
removeLambdas removeLambdas
[ ( mkLambdas' [mkTypeInteger', mkTypeInteger', mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkBuiltinApp' OpIntAdd [mkVar' 3, mkVar' 1], mkVar' 2]), [ ( mkLambdas' [mkTypeInteger', mkTypeInteger', mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkBuiltinApp' OpIntAdd [mkVar' 3, mkVar' 1], mkVar' 2]),
mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkBuiltinApp' OpIntAdd [mkVar' 1, mkVar' 0], mkVar' 1]) mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkBuiltinApp' OpIntAdd [mkBuiltinApp' OpIntAdd [mkVar' 1, mkVar' 0], mkVar' 1])
),
( mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkVar' 0),
mkLambda' mkTypeInteger' (mkVar' 0)
),
( mkLambdas' [mkTypeInteger', mkTypeInteger', mkTypeInteger', mkTypeInteger'] (mkVar' 2),
mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkVar' 1)
),
( mkLambdas' [mkTypeInteger', mkTypeInteger', mkTypeInteger'] (mkVar' 1),
mkLambdas' [mkTypeInteger', mkTypeInteger'] (mkVar' 1)
) )
] ]
] ]