From 0e599837dc143a863b36d978db3ae96a54e872fa Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 30 Aug 2022 12:21:44 +0200 Subject: [PATCH] fix developBeta --- src/Juvix/Compiler/Core/Extra.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs index 93f2e2ff6b..e2c0bd4bfc 100644 --- a/src/Juvix/Compiler/Core/Extra.hs +++ b/src/Juvix/Compiler/Core/Extra.hs @@ -56,12 +56,14 @@ shift m = umapN go _ -> n -- substitute a term t for the free variable with de Bruijn index 0, avoiding --- variable capture +-- variable capture; shifts all free variabes with de Bruijn index > 0 by -1 (as +-- if the topmost binder was removed) subst :: Node -> Node -> Node subst t = umapN go where go k n = case n of Var _ idx | idx == k -> shift k t + Var i idx | idx > k -> Var i (idx - 1) _ -> n -- reduce all beta redexes present in a term and the ones created immediately