From 60abe813dc4aa8631ba6e49418ffbb6c45833fca Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 14 Nov 2024 16:28:40 -0800
Subject: [PATCH] better names on solutions

---
 TODO.md                 |  2 ++
 newt/Combinatory.newt   |  3 +++
 src/Lib/Elab.idr        | 13 ++++++++-----
 src/Lib/ProcessDecl.idr |  4 ++--
 4 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/TODO.md b/TODO.md
index 74bd5e3..039ffab 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,8 @@
 
 ## TODO
 
+- [ ] improve test driver
+  - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
 - [x] Bad module name error has FC 0,0 instead of the module or name
 - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt
index 09dfa9c..b4cbc83 100644
--- a/newt/Combinatory.newt
+++ b/newt/Combinatory.newt
@@ -2,6 +2,9 @@ module Combinatory
 
 -- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
 
+-- This does not fully typecheck in newt yet, but is adopted from a working Idris file. It
+-- seems to do a good job exposing bugs.
+
 data Unit : U where
   MkUnit : Unit
 
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 38399ed..8333277 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -170,14 +170,17 @@ rename meta ren lvl v = go ren lvl v
     go ren lvl (VLet fc name val body) =
       pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) body)
 
-lams : Nat -> Tm -> Tm
-lams 0 tm = tm
--- REVIEW can I get better names in here?
-lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm)
+lams : Nat -> List String -> Tm -> Tm
+lams 0 _ tm = tm
+lams (S k) [] tm = Lam emptyFC "arg_\{show k}" (lams k [] tm)
+lams (S k) (x :: xs) tm = Lam emptyFC x (lams k xs tm)
 
 export
 unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult
 
+(.boundNames) : Context -> List String
+ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ toList $ zip ctx.bds (map fst ctx.types)
+
 export
 solve : Env -> (k : Nat) -> SnocList Val -> Val -> M  ()
 solve env m sp t = do
@@ -201,7 +204,7 @@ solve env m sp t = do
   catchError {e=Error} (do
     tm <- rename m ren l t
 
-    let tm = lams (length sp) tm
+    let tm = lams (length sp) (reverse ctx_.boundNames) tm
     top <- get
     soln <- eval [] CBN tm
 
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index ee7d7e4..db196fa 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -154,10 +154,10 @@ logMetas mstart = do
       -- FIXME in Combinatory, the val doesn't match environment?
       let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
       msgs <- for cons $ \ (MkMc fc env sp val) => do
-            putStrLn "  ENV \{show env}"
-            pure "  (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}"
+            pure "  * (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}"
       addError $ E (l,c) $ unlines ([msg] ++ msgs)
 
+
 export
 processDecl : Decl -> M ()