nf the types, block comments, more eq example now that we have implicits

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

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

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}"

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

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