mostly parsing tweaks

README.md

@@ -1,14 +1,20 @@
 
-- [ ] Add PRINTME / ?
+We're stopping at zoo4.
 
-Parser is in place.
-Ditched well-scoped for now.
 
-Fixed more issues, started processing stuff, we need real example code.
+- [ ] look into Lennart.newt issues
+- [ ] Type at point for the editor
+- [ ] add operators to parser state
+  - (Are we going to run this on LHS too?)
 
-Need to sort out eval. Currently List doesn't get substituted. We should make sure we're CBV. I guess I could always subst (or glue?) since we're head normal form. We need actual values (∏) for checking.
+- [ ] Data
-
+  - [ ] Read data as real constructors
-ok, our kovacs eval puts the arg in the environment and continues. So CBN, but maybe duplicate work (for our version).
+  - [ ] Typecheck / eval the same
+  - [ ] Add elimination / case
+    - [ ] Maybe some test cases from pi-forall
+- [ ] Code Gen
+- [ ] Less expansion
+  - Can we not expand top level - expand in unification and matching pi types?
 
 So smalltt has TopVar with a Level. typechecking binders end up as top too.
 
@@ -54,6 +60,16 @@ Parser:
 - [ ] check (either check at _ or infer and let it throw)
 - [ ] nf (ditto, but print value. WHNF for now    )
 - [ ] operators / mixfix
+  - Maybe put operators in parser state and update, ideally we'd have mixfix though
+  - how does agda handle clashes between names and mixfix?
+  - it seems to allow overlap: if, if_then, if_then_else_
+
+Testing:
+
+- [ ] black box testing
+  - [ ] bug.newt should fail with a certain parse error, but there will be noise, so look for specific error?
+  - [ ] zoo?.newt should complete successfully
+  - [ ]
 
 Misc:
 - [x] vscode support for .newt
@@ -86,6 +102,7 @@ Forward:
 - [ ] LSP?
 - [ ] white box testing
 - [ ] switches on logging
+- [ ] Add PRINTME / ? - Does it check and fake success? I don't think we can infer.
 
 ----
 

newt/eq.newt

@@ -2,7 +2,7 @@ module Equality
 
 -- Leibniz equality
 Eq : {A : U} -> A -> A -> U
-Eq = \ {A} x y => (P : A -> U) -> P x -> P y
+Eq = \ x y => (P : A -> U) -> P x -> P y
 
 refl : {A : U} {x : A} -> Eq x x
 refl = \ P Px => Px
@@ -10,8 +10,6 @@ refl = \ P Px => Px
 trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
 trans = \ Exy Eyz => Eyz (\ w => Eq x w) Exy
 
--- This version has a universe issue, see Abel et al for
--- a better one
 sym : {A : U} {x y : A} -> Eq x y -> Eq y x
 sym = \ Exy => Exy (\ z => Eq z x) refl
 

newt/zoo2.newt

@@ -9,6 +9,12 @@ const = \A B x y => x
 Nat : U
 Nat = (N : U) -> (N -> N) -> N -> N
 
+zero : Nat
+zero = \ _ s z => z
+
+succ : Nat -> Nat
+succ = \ n ty s z => s (n ty s z)
+
 -- need Nat to reduce (and syntax highlighting)
 five : Nat
 five = \ N s z => s (s (s (s (s z))))

src/Lib/Check.idr

@@ -110,7 +110,7 @@ parameters (ctx: Context)
       (VMeta i sp, t'           ) => solve l i sp t'
       (VU, VU) => pure ()
       -- REVIEW consider quoting back
-      _ => error [DS "unify failed", DS (show t'), DS "=?=", DS (show u') ]
+      _ => error [DS "unify failed \{show t'} =?= \{show u'} \n  env is \{show ctx.env}" ]
 
 insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
@@ -192,11 +192,12 @@ infer ctx (RApp t u icit) = do
         else error [DS "IcitMismatch \{show icit} \{show icit'}"]
 
     -- If it's not a VPi, try to unify it with a VPi
+    -- TODO test case to cover this.
     tty => do
       putStrLn "unify PI for \{show tty}"
       a <- eval ctx.env CBN !(freshMeta ctx)
-      b <- MkClosure ctx.env <$> freshMeta (extend ctx "x" ?hole)
+      b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a)
-      unify ctx 0 tty (VPi "x" icit a b)
+      unify ctx 0 tty (VPi ":ins" icit a b)
       pure (a,b)
 
   u <- check ctx u a

src/Lib/Parser.idr

@@ -71,12 +71,8 @@ atom = withPos (RU <$ keyword "U"
 
 -- Argument to a Spine
 pArg : Parser (Icit,Raw)
-pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces term
+pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces typeExpr
 
---
--- atom is lit or ident
-
-data Fixity = InfixL | InfixR | Infix
 
 -- starter pack, but we'll move some to prelude
 operators : List (String, Int, Fixity)
@@ -87,6 +83,7 @@ operators = [
   ("*",5,InfixL),
   ("/",5,InfixL)
 ]
+
 parseApp : Parser Raw
 parseApp = do
   hd <- atom
@@ -195,11 +192,14 @@ ibind = do
     -- getPos is a hack here, I would like to position at the name...
     pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RImplicit) ty)) names
 
+arrow : Parser Unit
+arrow = sym "->" <|> sym "→"
+
 -- Collect a bunch of binders (A : U) {y : A} -> ...
 binders : Parser Raw
 binders = do
   binds <- many (ibind <|> ebind)
-  sym "->"
+  arrow
   commit
   scope <- typeExpr
   pure $ foldr mkBind scope (join binds)
@@ -210,7 +210,7 @@ binders = do
 typeExpr = binders
   <|> do
         exp <- term
-        scope <- optional (sym "->" *> mustWork typeExpr)
+        scope <- optional (arrow *> mustWork typeExpr)
         case scope of
           Nothing      => pure exp
           -- consider Maybe String to represent missing

src/Lib/Parser/Impl.idr

@@ -1,5 +1,13 @@
 module Lib.Parser.Impl
 
+-- For some reason I'm doing Idris' commit / mustWork dance here, even though it
+-- seems to be painful
+
+-- Probably would like to do "did consume anything" on the input, but we might need
+-- something other than a token list
+
+-- TODO see what Kovacs' flatparse does for error handling / <|>
+
 import Lib.Token
 import Data.String
 import Data.Nat
@@ -8,6 +16,9 @@ public export
 TokenList : Type
 TokenList = List BTok
 
+public export
+data Fixity = InfixL | InfixR | Infix
+
 -- I was going to use a record, but we're peeling this off of bounds at the moment.
 public export
 SourcePos : Type
@@ -131,13 +142,9 @@ export
 commit : Parser ()
 commit = P $ \toks,com,col => OK () toks True
 
-export
-defer : (() -> (Parser a)) -> Parser a
-defer f = P $ \toks,com,col => runP (f ()) toks com col
-
 mutual
   export some : Parser a -> Parser (List a)
-  some p = defer $ \_ => [| p :: many p|] --(::) <$> p <*> many p)
+  some p = (::) <$> p <*> many p
 
   export many : Parser a -> Parser (List a)
   many p = some p <|> pure []

src/Lib/Tokenizer.idr

@@ -5,7 +5,7 @@ import Text.Lexer.Tokenizer
 import Lib.Token
 
 keywords : List String
-keywords = ["let", "in", "where", "case", "of", "data"]
+keywords = ["let", "in", "where", "case", "of", "data", "U"]
 
 specialOps : List String
 specialOps = ["->", ":", "=>"]

src/Lib/Types.idr

@@ -156,6 +156,10 @@ Show Val where
   show (VPi str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
   show VU = "U"
 
+
+public export
+data Binder = Bind String BD Val
+
 public export
 Env : Type
 Env = List Val
@@ -250,6 +254,8 @@ record TopContext where
   metas : IORef MetaContext
   -- metas : TODO
 
+
+
 -- we'll use this for typechecking, but need to keep a TopContext around too.
 public export
 record Context where