From 699a4bd575aedaf93364773b9f817356d7f0aaf4 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 17 Sep 2024 06:27:55 -0700
Subject: [PATCH] elaborate let

---
 TODO.md              |  2 +-
 src/Lib/Check.idr    | 10 +++++++++-
 tests/black/let.newt |  6 ++++++
 3 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 tests/black/let.newt

diff --git a/TODO.md b/TODO.md
index 9b91586..aa18faf 100644
--- a/TODO.md
+++ b/TODO.md
@@ -5,7 +5,7 @@ I may be done with `U` - I keep typing `Type`.
 
 - [x] switch from commit/mustWork to checking progress
 - [x] type constructors are no longer generated?  And seem to have 0 arity.
-- [ ] raw let is not yet implemented (although define used by case tree building)
+- [x] raw let is not yet implemented (although define used by case tree building)
 - [x] there is some zero argument application in generated code
 - [x] get equality.newt to work
   - [x] broken again because I added J, probably need to constrain scrutinee to value
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 57c5689..84af462 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -650,7 +650,15 @@ infer ctx (RPi fc nm icit ty ty2) = do
   let nm := fromMaybe "_" nm
   ty2' <- check (extend ctx nm vty') ty2 (VU fc)
   pure (Pi fc nm icit ty' ty2', (VU fc))
-infer ctx (RLet fc nm ty v sc) = error fc "implement RLet"
+infer ctx (RLet fc nm ty v sc) = do
+  ty' <- check ctx ty (VU emptyFC)
+  vty <- eval ctx.env CBN ty'
+  v' <- check ctx v vty
+  vv <- eval ctx.env CBN v'
+  let ctx' = define ctx nm vv vty
+  (sc',scty) <- infer ctx' sc
+  pure $ (Let fc nm v' sc', scty)
+
 infer ctx (RAnn fc tm rty) = do
   ty <- check ctx rty (VU fc)
   vty <- eval ctx.env CBN ty
diff --git a/tests/black/let.newt b/tests/black/let.newt
new file mode 100644
index 0000000..f29206c
--- /dev/null
+++ b/tests/black/let.newt
@@ -0,0 +1,6 @@
+module Let
+
+ptype Int
+
+foo : Int -> Int
+foo n = let x = 42 in x