better names on solutions

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.

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
 

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
 

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 ()