From c0f9262c9aee98e95551a3e30e48c27ca978d7e3 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 16 Jul 2024 08:10:43 -0700
Subject: [PATCH] nf the types, block comments, more eq example now that we
 have implicits

---
 README.md             |  9 ++++++---
 newt/eq.newt          | 17 ++++++++++++-----
 src/Lib/Compile.idr   |  2 +-
 src/Lib/Tokenizer.idr |  3 ++-
 src/Main.idr          |  5 +++--
 5 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/README.md b/README.md
index a693c11..1c5e9a5 100644
--- a/README.md
+++ b/README.md
@@ -42,10 +42,12 @@ Questions:
 - [ ] Should I write this up properly?
 
 Parser:
-- [ ] parser for block comments
+- [x] parser for block comments
 - [x] import statement
 - [x] def
 - [x] simple decl
+- [ ] check (either check at _ or infer and let it throw)
+- [ ] nf (ditto, but print value. WHNF for now    )
 
 Misc:
 - [x] vscode support for .newt
@@ -65,10 +67,10 @@ Misc:
 - [x] figure out context representation - Global context?
 - [x] type checking / elab
   - What does this represent? The basics, implicits? pattern unification?
-- [ ] symbolic execution
-  - why did I put this here? Is it just for `eval`?  We do have CBN in place, we could eval inferrable
+- [ ] check for unsolved metas (after each def or at end?)
 - [ ] compilation
   - I'm thinking I get data working first
+- [ ] repl
 - [ ] write tests
 - [ ] Split up code better
 
@@ -77,6 +79,7 @@ Forward:
 - [ ] Switch to query-based?
 - [ ] LSP?
 - [ ] white box testing
+- [ ] switches on logging
 
 ----
 
diff --git a/newt/eq.newt b/newt/eq.newt
index 5936b82..e35d8e5 100644
--- a/newt/eq.newt
+++ b/newt/eq.newt
@@ -6,10 +6,17 @@ Eq : {A : U} -> A -> A -> U
 Eq = \ {A} => \ x => \ y => (P : A -> U) -> P x -> P y
 
 refl : {A : U} {x : A} -> Eq x x
-refl = \ {A} => \ {x} => x
+refl = \ P Px => Px
+
+id : {A} -> A -> A
+id = \ x => x
+
+coerce : {A B : U} -> Eq A B -> A -> B
+-- coerce refl a = a
+coerce = \ EqAB a => EqAB id a
 
 -- can I write J without pattern matching?
-J : {A : U} {x y : A} (eq : Eq x y) ->
-(mot : (x : A) (P : Eq x y) -> U)
-(b : mot y refl) -> 
-mot x eq
+-- J : {A : U} {x y : A} (eq : Eq x y) ->
+-- (mot : (x : A) (P : Eq x y) -> U)
+-- (b : mot y refl) ->
+-- mot x eq
diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr
index ea7eca0..1294c88 100644
--- a/src/Lib/Compile.idr
+++ b/src/Lib/Compile.idr
@@ -23,4 +23,4 @@ compile l (App t u) = compile l t <+> "(" <+> compile l u <+> ")"
 
 compile l U = "undefined"
 compile l (Pi str icit t u) = "undefined"
-compile l (Meta k) = ?fixme_zonk
+compile l (Meta k) = text "ZONKME \{show k}"
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index f0d97d0..2daea88 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -28,6 +28,7 @@ rawTokens
   <|> match (some digit) (Tok Number)
   <|> match (is '#' <+> many alpha) (Tok Pragma)
   <|> match (lineComment (exact "--")) (Tok Space)
+  <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space)
   <|> match (some opChar) (\s => Tok Oper s)
   <|> match symbol (Tok Symbol)
   <|> match spaces (Tok Space)
@@ -38,4 +39,4 @@ notSpace _ = True
 
 export
 tokenise : String -> List BTok
-tokenise = filter notSpace . fst . lex rawTokens 
+tokenise = filter notSpace . fst . lex rawTokens
diff --git a/src/Main.idr b/src/Main.idr
index dda436b..5112637 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -51,8 +51,9 @@ processDecl (TypeSig nm tm) = do
   putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas) tm VU
-  putStrLn "got \{show ty}"
-  modify $ claim nm ty
+  ty' <- nf [] ty
+  putStrLn "got \{show ty'}"
+  modify $ claim nm ty'
 
 -- FIXME - this should be in another file
 processDecl (Def nm raw) = do