From f225d0ecbde07bef37337c943aad8d9ffda2a5bf Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 2 Nov 2024 21:42:08 -0700
Subject: [PATCH] Print meta info for claims and data, update sample code

---
 TODO.md                 |  4 +--
 aoc2023/Day2.newt       |  2 +-
 newt/Combinatory.newt   | 64 ++++++++++++++++++++++++++++++-----------
 src/Lib/ProcessDecl.idr | 49 +++++++++++++++++++------------
 4 files changed, 80 insertions(+), 39 deletions(-)

diff --git a/TODO.md b/TODO.md
index cd0e9e3..7c54d3b 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,13 +1,13 @@
 
 ## TODO
 
-- [ ] Allow unicode operators/names
-  - refactored parser to prep for this
+- [x] Allow unicode operators/names
 - [ ] Web tool
   - edit, view output, view js, run js, monaco would be nice.
   - need to shim out Buffer
 - [x] get rid of stray INFO from auto resolution
 - [ ] handle if_then_else_ style mixfix
+- [ ] Check for shadowing when declaring dcon
 - [ ] Search should look at context
 - [ ] records
 - [ ] copattern matching
diff --git a/aoc2023/Day2.newt b/aoc2023/Day2.newt
index 0f00e8d..7e2cbde 100644
--- a/aoc2023/Day2.newt
+++ b/aoc2023/Day2.newt
@@ -85,7 +85,7 @@ part2 : List Game -> Int
 part2 Nil = 0
 part2 (MkGame n parts :: rest) =
   case foldl maxd (0,0,0) parts of
-    (a,b,c) => a*b*c + part2 rest
+    (a,b,c) => a * b * c + part2 rest
 
 run : String -> Dummy
 run fn =
diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt
index 15781e6..def1065 100644
--- a/newt/Combinatory.newt
+++ b/newt/Combinatory.newt
@@ -1,5 +1,7 @@
 module Combinatory
 
+-- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+
 data Unit : U where
   MkUnit : Unit
 
@@ -34,7 +36,7 @@ data Term : Ctx -> Type -> U where
   Lam : {Γ : Ctx} {σ τ : Type} -> Term (σ :: Γ) τ -> Term Γ (σ ~> τ)
   Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
 
--- FIXME, I'm not getting an error for Nil, but it's shadowing Nil
+-- FIXME, I wasn't getting an error when I had Nil shadowing Nil
 infixr 7 _:::_
 data Env : Ctx -> U where
   ENil : Env Nil
@@ -44,26 +46,54 @@ data Env : Ctx -> U where
 -- I suspect something is being split before it's ready
 
 -- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
--- lookup Z (x ::: y) = x
--- lookup (S i) (x ::: env) = lookup i env
+-- lookup Here (x ::: y) = x
+-- lookup (There i) (x ::: env) = lookup i env
 
 
--- lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
--- lookup2 (x ::: y) Here = x
--- lookup2 (x ::: env) (There i) = lookup2 env i
+lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
+lookup2 (x ::: y) Here = x
+lookup2 (x ::: env) (There i) = lookup2 env i
 
--- -- MixFix - this was ⟦_⟧
--- eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
--- eval (App t u) env = ? -- (eval t env) (eval u env)
--- eval (Lam t) env = \ x => ? -- eval t (x ::: env)
--- eval (Var i) env = lookup2 env i
+-- TODO MixFix - this was ⟦_⟧
+eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+-- TODO unification error in direct application
+eval (App t u) env = -- (eval t env) (eval u env)
+  let a = (eval t env)
+      b = (eval u env)
+   in a b
+eval (Lam t) env = \ x => eval t (x ::: env)
+eval (Var i) env = lookup2 env i
 
--- something really strange here, the arrow in the goal type is backwards...
-foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ))
-foo {σ} {τ} {ξ} = ? -- \ x y => x
+data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
+  S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
+  K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> τ ~> σ) (\ env => \ x y => x)
+  I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x)
+  B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x))
+  C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g)
+  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup2 env i)
+  CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
 
--- data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
---   -- S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
---   K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> τ ~> σ) (\ env => \ x => \ y => x)
+sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
+  Comb Γ (σ ~> τ ~> ρ) f →
+  Comb Γ (σ ~> τ) x →
+  Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y))
+-- sapp (CApp K t) I = t
+-- sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
+-- sapp (CApp K t) u = CApp (CApp B t) u
+-- sapp t (CApp K u) = CApp (CApp C t) u
+-- sapp t u = CApp (CApp S t) u
 
+abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))
+abs S = CApp K S
+abs K = CApp K K
+abs I = CApp K I
+abs B = CApp K B
+abs C = CApp K C
+abs (CApp t u) = sapp (abs t) (abs u)
+abs (CVar Here) = ? -- I
+abs (CVar (There i)) = ? -- CApp K (Var i)
 
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+translate (App t u) = ? -- CApp (translate t) (translate u)
+translate (Lam t) = abs (translate t)
+translate (Var i) = CVar i
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 53d7da5..e089467 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -95,6 +95,28 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
 solveAutos mlen (_ :: es) = solveAutos mlen es
 
 
+logMetas : Nat -> M ()
+logMetas mstart = do
+  -- FIXME, now this isn't logged for Sig / Data.
+  top <- get
+  mc <- readIORef top.metas
+  let mlen = length mc.metas `minus` mstart
+  for_ (take mlen mc.metas) $ \case
+    (Solved fc k soln) => info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
+    (Unsolved fc k ctx ty User cons) => do
+      ty' <- quote ctx.lvl ty
+      let names = (toList $ map fst ctx.types)
+      -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
+      env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}"
+      let msg = "\{unlines (toList $ reverse env)}  -----------\n  \{pprint names ty'}\n  \{showTm ty'}"
+      info fc "User Hole\n\{msg}"
+    (Unsolved (l,c) k ctx ty kind cons) => do
+      tm <- quote ctx.lvl !(forceMeta ty)
+      -- Now that we're collecting errors, maybe we simply check at the end
+      -- TODO - log constraints?
+      addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
+
+
 export
 processDecl : Decl -> M ()
 
@@ -103,6 +125,8 @@ processDecl (PMixFix{})  = pure ()
 
 processDecl (TypeSig fc names tm) = do
   top <- get
+  mc <- readIORef top.metas
+  let mstart = length mc.metas
   for_ names $ \nm => do
     let Nothing := lookup nm top
       | _ => error fc "\{show nm} is already defined"
@@ -115,6 +139,7 @@ processDecl (TypeSig fc names tm) = do
   -- ty' <- nf [] ty
   -- putStrLn "nf \{pprint [] ty'}"
   for_ names $ \nm => modify $ setDef nm ty Axiom
+  logMetas mstart
 
 processDecl (PType fc nm ty) = do
   top <- get
@@ -153,28 +178,12 @@ processDecl (Def fc nm clauses) = do
   solveAutos mlen (take mlen mc.metas)
 
   -- Expand metas
-  -- tm' <- nf [] tm  -- TODO - nf that expands all metas, Day1.newt is a test case
+  -- tm' <- nf [] tm  -- TODO - make nf that expands all metas, Day1.newt is a test case
   tm' <- zonk top 0 [] tm
   putStrLn "NF \{pprint[] tm'}"
-
-  mc <- readIORef top.metas
-  for_ (take mlen mc.metas) $ \case
-    (Solved fc k soln) => info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
-    (Unsolved fc k ctx ty User cons) => do
-      ty' <- quote ctx.lvl ty
-      let names = (toList $ map fst ctx.types)
-      -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
-      env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}"
-      let msg = "\{unlines (toList $ reverse env)}  -----------\n  \{pprint names ty'}\n  \{showTm ty'}"
-      info fc "User Hole\n\{msg}"
-    (Unsolved (l,c) k ctx ty kind cons) => do
-      tm <- quote ctx.lvl !(forceMeta ty)
-      -- Now that we're collecting errors, maybe we simply check at the end
-      -- TODO - log constraints?
-      addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
-
   debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
   modify $ setDef nm ty (Fn tm')
+  logMetas mstart
 
 processDecl (DCheck fc tm ty) = do
   putStrLn "----- DCheck"
@@ -195,6 +204,8 @@ processDecl (Data fc nm ty cons) = do
   putStrLn "-----"
   putStrLn "process data \{nm}"
   top <- get
+  mc <- readIORef top.metas
+  let mstart = length mc.metas
   tyty <- check (mkCtx top.metas fc) ty (VU fc)
   modify $ setDef nm tyty Axiom
   cnames <- for cons $ \x => case x of
@@ -218,7 +229,7 @@ processDecl (Data fc nm ty cons) = do
       _ => throwError $ E (0,0) "expected constructor declaration"
   putStrLn "setDef \{nm}  TCon \{show $ join cnames}"
   modify $ setDef nm tyty (TCon (join cnames))
-  pure ()
+  logMetas mstart
   where
     checkDeclType : Tm -> M ()
     checkDeclType (U _) = pure ()