Merge pull request #35 from ToposInstitute/nested-let

Fix issue with nested let bindings
ToposInstitute · Jul 3, 2023 · b0fd023 · b0fd023
2 parents ae4d001 + a605c1c
commit b0fd023
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 1 deletion.
diff --git a/lib/refiner/rules/Var.ml b/lib/refiner/rules/Var.ml
@@ -14,7 +14,10 @@ let let_bind ?(name = `Anon) (tm : Syn.tac) (f : Var.tac -> Chk.tac) =
   Chk.rule @@ fun rtp ->
   let (vtp, etm) = Syn.run tm in
   let vtm = Eff.eval etm in
-  let body = Chk.run (Var.concrete ~name vtp vtm f) rtp in
+  let body =
+    Var.concrete ~name vtp vtm @@ fun v ->
+    Chk.run (f v) rtp
+  in
   Let (name, etm, body)
 
 let negative (cell : Cell.neg) =

diff --git a/test/let/polytt-lib b/test/let/polytt-lib
@@ -0,0 +1 @@
+{ "format": "1.0.0" }
diff --git a/test/let/test-let.poly b/test/let/test-let.poly
@@ -0,0 +1,9 @@
+def add : ℕ → ℕ → ℕ :=
+  λ m n → elim (λ _ → ℕ) n (λ _ n → succ n) m
+
+def nested-let : ℕ :=
+  let x := 4 in
+  let y := 5 in
+  add x y
+
+#normalize nested-let
diff --git a/test/test.expected b/test/test.expected
@@ -16,6 +16,9 @@ Normal Form: λ P Q → λ ~> FIXME λ pf⁺ → (fst (snd pf⁺ (fst pf⁺)) ,
 Normal Form: (12 , λ <7> → (succ (succ <7>) , (3 , <7>)))
 Normal Form: λ P Q → λ ~> FIXME λ pq⁺ → ((fst pq⁺ , λ _ → snd pq⁺) , λ <3> → (fst <3> , snd <3>)) FIXME
 Normal Form: λ S T A B → #{ .get, .set } → { .get = S → A, .set = S → B → T } _
+--------------------[test-let.poly]--------------------
+
+Normal Form: 9
 --------------------[a.poly]--------------------
 
 --------------------[b.poly]--------------------