Add more stuff to equality and more logging

Need to get names in there though.

README.md

@@ -1,4 +1,6 @@
 
+- [ ] Add PRINTME / ?
+
 Parser is in place.
 Ditched well-scoped for now.
 
@@ -36,10 +38,13 @@ When I self host, I'll have to drop or implement typeclasses. I do understand au
 
 Ok, for code gen, I think I'll need something like primitive values and definitely primitive functions. For v0, I could leave the holes as undefined and if there is a function with that name, it's magically FFI.
 
-
 Questions:
 - [ ] Code gen or data next?
 - [ ] Should I write this up properly?
+- [ ] Erased values?
+  - pi-forall handles this, so it's probably not too crazy. She won't go near implicits and I think I understand why.
+  - I don't think I Want to go full QTT at the moment
+  - Is erased different from 0/many?
 
 Parser:
 - [x] parser for block comments

newt/eq.newt

@@ -1,22 +1,29 @@
 module Equality
 
--- we don't have implicits yet, so this won't typecheck
+-- Leibniz equality
 
 Eq : {A : U} -> A -> A -> U
-Eq = \ {A} => \ x => \ y => (P : A -> U) -> P x -> P y
+Eq = \ {A} x y => (P : A -> U) -> P x -> P y
 
 refl : {A : U} {x : A} -> Eq x x
 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
+
+sym : {A : U} {x y : A} -> Eq x y -> Eq y x
+sym = \ Exy => Exy (\ z => Eq z x) refl
+
 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} ->
--- J : {A : U} {x y : A} (eq : Eq x y) ->
+--     {C : (x y : A) -> Eq x y -> U} ->
--- (mot : (x : A) (P : Eq x y) -> U)
+--     (c : (x : _) -> C x x refl) ->
--- (b : mot y refl) ->
+--     (x y : A) ->
--- mot x eq
+--     (p : Eq x y) ->
+--     C x y p
+-- J = \ c x y eq => eq (\ z => C x z _) (c x)

src/Lib/Check.idr

@@ -24,57 +24,58 @@ forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
--- return renaming, the position is the new VVar
-invert : Nat -> SnocList Val -> M (List Nat)
-invert lvl sp = go sp []
-  where
-    go : SnocList Val -> List Nat -> M (List Nat)
-    go [<] acc = pure $ reverse acc
-    go (xs :< VVar k [<]) acc = do
-      if elem k acc
-        then throwError $ E (0,0) "non-linear pattern"
-        else go xs (k :: acc)
-    go _ _ = throwError $ E (0,0) "non-variable in pattern"
-
--- we have to "lift" the renaming when we go under a lambda
--- I think that essentially means our domain ix are one bigger, since we're looking at lvl
--- in the codomain, so maybe we can just keep that value
-rename : Nat -> List Nat -> Nat -> Val  -> M  Tm
-rename meta ren lvl v = go ren lvl v
-  where
-    go : List Nat -> Nat -> Val  -> M  Tm
-    goSpine : List Nat -> Nat -> Tm -> SnocList Val  -> M  Tm
-    goSpine ren lvl tm [<] = pure tm
-    goSpine ren lvl tm (xs :< x) = do
-      xtm <- go ren lvl x
-      goSpine ren lvl (App tm xtm) xs
-
-    go ren lvl (VVar k sp) = case findIndex (== k) ren of
-      Nothing => throwError $ E (0,0) "scope/skolem thinger"
-      Just x => goSpine ren lvl (Bnd $ cast x) sp
-    go ren lvl (VRef nm sp) = goSpine ren lvl (Ref nm Nothing) sp
-    go ren lvl (VMeta ix sp) = if ix == meta
-      then throwError $ E (0,0) "meta occurs check"
-      else goSpine ren lvl (Meta ix) sp
-    go ren lvl (VLam n t) = pure (Lam n !(go (lvl :: ren) (S lvl) !(t $$ VVar lvl [<])))
-    go ren lvl (VPi n icit ty tm) = pure (Pi n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar lvl [<])))
-    go ren lvl VU = pure U
-
-lams : Nat -> Tm -> Tm
-lams 0 tm = tm
-lams (S k) tm = Lam "arg:\{show k}" (lams k tm)
-
-solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
-solve l m sp t = do
-  ren <- invert l sp
-  tm <- rename m ren l t
-  let tm = lams (length sp) tm
-  top <- get
-  soln <- eval [] CBN tm
-  solveMeta top m soln
-  pure ()
-
 parameters (ctx: Context)
+  -- return renaming, the position is the new VVar
+  invert : Nat -> SnocList Val -> M (List Nat)
+  invert lvl sp = go sp []
+    where
+      go : SnocList Val -> List Nat -> M (List Nat)
+      go [<] acc = pure $ reverse acc
+      go (xs :< VVar k [<]) acc = do
+        if elem k acc
+          then error [DS "non-linear pattern"]
+          else go xs (k :: acc)
+      go _ _ = error [DS "non-variable in pattern"]
+
+  -- we have to "lift" the renaming when we go under a lambda
+  -- I think that essentially means our domain ix are one bigger, since we're looking at lvl
+  -- in the codomain, so maybe we can just keep that value
+  rename : Nat -> List Nat -> Nat -> Val  -> M  Tm
+  rename meta ren lvl v = go ren lvl v
+    where
+      go : List Nat -> Nat -> Val  -> M  Tm
+      goSpine : List Nat -> Nat -> Tm -> SnocList Val  -> M  Tm
+      goSpine ren lvl tm [<] = pure tm
+      goSpine ren lvl tm (xs :< x) = do
+        xtm <- go ren lvl x
+        goSpine ren lvl (App tm xtm) xs
+
+      go ren lvl (VVar k sp) = case findIndex (== k) ren of
+        Nothing => error [DS "scope/skolem thinger"]
+        Just x => goSpine ren lvl (Bnd $ cast x) sp
+      go ren lvl (VRef nm sp) = goSpine ren lvl (Ref nm Nothing) sp
+      go ren lvl (VMeta ix sp) = if ix == meta
+        then error [DS "meta occurs check"]
+        else goSpine ren lvl (Meta ix) sp
+      go ren lvl (VLam n t) = pure (Lam n !(go (lvl :: ren) (S lvl) !(t $$ VVar lvl [<])))
+      go ren lvl (VPi n icit ty tm) = pure (Pi n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar lvl [<])))
+      go ren lvl VU = pure U
+
+  lams : Nat -> Tm -> Tm
+  lams 0 tm = tm
+  lams (S k) tm = Lam "arg:\{show k}" (lams k tm)
+
+
+  solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
+  solve l m sp t = do
+    ren <- invert l sp
+    tm <- rename m ren l t
+    let tm = lams (length sp) tm
+    top <- get
+    soln <- eval [] CBN tm
+    solveMeta top m soln
+    pure ()
+
   unify : (l : Nat) -> Val -> Val  -> M  ()
 
   unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
@@ -147,6 +148,10 @@ check ctx tm ty with (force ty)
     ty' <- b $$ var
     sc <- check (extend ctx nm' a) tm ty'
     pure $ Lam nm' sc
+  -- TODO Work in progress
+  -- I'd like to continue and also this is useless without some var names
+  check ctx RHole _ | ty = do
+    error [DS "hole has type \{show ty}"]
   check ctx tm _ | ty = do
     -- We need to insert if it's not a Lam
     -- TODO figure out why the exception is here (cribbed from kovacs)
@@ -158,6 +163,7 @@ check ctx tm ty with (force ty)
     unify ctx ctx.lvl ty' ty
     pure tm'
 
+
 infer ctx (RVar nm) = go 0 ctx.types
   where
     go : Nat -> Vect n (String, Val)  -> M  (Tm, Val)
@@ -218,7 +224,7 @@ infer ctx (RLam nm icit tm) = do
   pure $ (Lam nm tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
   -- error {ctx} [DS "can't infer lambda"]
 
-infer ctx RHole = do
+infer ctx RImplicit = do
   ty <- freshMeta ctx
   vty <- eval ctx.env CBN ty
   tm <- freshMeta ctx
@@ -231,6 +237,6 @@ infer ctx tm = error [DS "Implement infer \{show tm}"]
 -- infer ctx (RLit (LInt i)) = ?rhs_11
 -- infer ctx (RLit (LBool x)) = ?rhs_12
 -- infer ctx (RCase tm xs) = ?rhs_9
--- infer ctx RHole = ?todo_meta2
+-- infer ctx RImplicit = ?todo_meta2
 -- The idea here is to insert a hole for a parse error
 -- infer ctx (RParseError str) = ?todo_insert_meta

src/Lib/Parser.idr

@@ -4,7 +4,7 @@ import Lib.Types
 -- The SourcePos stuff is awkward later on. We might want bounds on productions
 -- But we might want to consider something more generic and closer to lean?
 
--- app: foo {a} a b 
+-- app: foo {a} a b
 -- lam: λ {A} {b : A} (c : Blah) d e f => something
 -- lam: \ {A} {b : A} (c : Blah) d e f => something
 -- pi: (A : Set) -> {b : A} -> (c : Foo b) -> c -> bar d
@@ -25,7 +25,7 @@ import Data.Maybe
 -- so holes and all that
 
 -- After the parser runs, see below, take a break and finish pi-forall
--- exercises.  There is some fill in the parser stuff that may show 
+-- exercises.  There is some fill in the parser stuff that may show
 -- the future.
 
 ident = token Ident
@@ -53,7 +53,7 @@ lit = do
   t <- token Number
   pure $ RLit (LInt (cast t))
 
--- typeExpr is term with arrows. 
+-- typeExpr is term with arrows.
 export typeExpr : Parser Raw
 export term : (Parser Raw)
 
@@ -63,9 +63,10 @@ withPos p = RSrcPos <$> getPos <*> p
 -- the inside of Raw
 atom : Parser Raw
 atom = withPos (RU <$ keyword "U"
-              <|> RVar <$> ident 
+              <|> RVar <$> ident
               <|> lit
-              <|> RHole <$ keyword "_")
+              <|> RImplicit <$ keyword "_"
+              <|> RHole <$ keyword "?")
     <|> parens typeExpr
 
 -- Argument to a Spine
@@ -91,12 +92,12 @@ parseApp = do
   hd <- atom
   rest <- many pArg
   pure $ foldl (\a, (c,b) => RApp a b c) hd rest
-  
+
 parseOp : Parser Raw
 parseOp = parseApp >>= go 0
   where
     go : Int -> Raw -> Parser Raw
-    go prec left = 
+    go prec left =
       do
         op <- token Oper
         let Just (p,fix) = lookup op operators
@@ -115,8 +116,8 @@ letExpr = do
   alts <- startBlock $ someSame $ letAssign
   keyword' "in"
   scope <- typeExpr
-  
+
-  pure $ foldl (\ acc, (n,v) => RLet n RHole v acc) scope alts
+  pure $ foldl (\ acc, (n,v) => RLet n RImplicit v acc) scope alts
   where
     letAssign : Parser (Name,Raw)
     letAssign = do
@@ -186,18 +187,20 @@ ebind = do
 ibind : Parser (List (String, Icit, Raw))
 ibind = do
   sym "{"
-  names <- some ident
+  mustWork $ do
-  ty <- optional (sym ":" >> typeExpr)
+    names <- some ident
-  pos <- getPos
+    ty <- optional (sym ":" >> typeExpr)
-  sym "}"
+    pos <- getPos
-  -- getPos is a hack here, I would like to position at the name... 
+    sym "}"
-  pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RHole) ty)) names
+    -- getPos is a hack here, I would like to position at the name...
+    pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RImplicit) ty)) names
 
 -- Collect a bunch of binders (A : U) {y : A} -> ...
 binders : Parser Raw
-binders = do  
+binders = do
   binds <- many (ibind <|> ebind)
   sym "->"
+  commit
   scope <- typeExpr
   pure $ foldr mkBind scope (join binds)
   where
@@ -274,4 +277,3 @@ data ReplCmd =
 export parseRepl : Parser ReplCmd
 parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr
   <|> Check <$ keyword "#check" <*> typeExpr
-  

src/Main.idr

@@ -7,6 +7,7 @@ import Control.Monad.State
 import Data.List
 import Data.String
 import Data.Vect
+import Data.IORef
 import Lib.Check
 import Lib.Parser
 import Lib.Parser.Impl
@@ -31,7 +32,6 @@ App, but we have a way to make that work on javascript.
 
 I still want to stay in MonadError outside this file though.
 
-
 -}
 
 
@@ -73,6 +73,14 @@ processDecl (Def nm raw) = do
   putStrLn "vty is \{show vty}"
   tm <- check (mkCtx ctx.metas) raw vty
   putStrLn "Ok \{show tm}"
+
+  mc <- readIORef ctx.metas
+  for_ mc.metas $ \case
+    (Solved k x) => pure ()
+    (Unsolved (l,c) k xs) => do
+      -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}"
+      throwError $ E (l,c) "Unsolved meta \{show k}"
+
   put (addDef ctx nm tm ty)
 
 processDecl (DCheck tm ty) = do

src/Syntax.idr

@@ -39,7 +39,9 @@ data Raw : Type where
   RAnn  : (tm : Raw) -> (ty : Raw) -> Raw
   RLit : Literal -> Raw
   RCase : (scrut : Raw) -> (alts : List CaseAlt) -> Raw
+  RImplicit : Raw
   RHole : Raw
+  -- not used, but intended to allow error recovery
   RParseError : String -> Raw
 
 %name Raw tm
@@ -50,7 +52,7 @@ public export
 data Decl : Type where
 
 Telescope: Type
-Telescope = List Decl -- pi-forall, always typeSig? 
+Telescope = List Decl -- pi-forall, always typeSig?
 
 data ConstrDef = MkCDef Name Telescope
 
@@ -116,7 +118,8 @@ Show CaseAlt where
 
 covering
 Show Raw where
-  show RHole = "_"
+  show RImplicit = "_"
+  show RHole = "?"
   show (RVar name) = foo ["RVar", show name]
   show (RAnn t ty) = foo [ "RAnn", show t, show ty]
   show (RLit x) = foo [ "RLit", show x]
@@ -149,12 +152,12 @@ Pretty Raw where
     asDoc p (RApp x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
     asDoc p RU = text "U"
     asDoc p (RPi Nothing Explicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi (Just x) Explicit ty scope) = 
+    asDoc p (RPi (Just x) Explicit ty scope) =
       par p 1 $ text "(" <+> text x <+> text ":" <+> asDoc p ty <+> text ")" <+> text "->" <+/> asDoc p scope
     asDoc p (RPi nm Implicit ty scope) =
       par p 1 $ text "{" <+> text (fromMaybe "_" nm) <+> text ":" <+> asDoc p ty <+> text "}" <+> text "->" <+/> asDoc 1 scope
-    asDoc p (RLet x v ty scope) = 
+    asDoc p (RLet x v ty scope) =
-      par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty 
+      par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty
           <+> text "=" <+> asDoc p v
           <+/> text "in" <+> asDoc p scope
     asDoc p (RSrcPos x y) = asDoc p y
@@ -164,10 +167,11 @@ Pretty Raw where
     asDoc p (RLit (LInt i)) = text $ show i
     asDoc p (RLit (LBool x)) = text $ show x
     asDoc p (RCase x xs) = text "TODO - RCase"
-    asDoc p RHole = text "_"
+    asDoc p RImplicit = text "_"
+    asDoc p RHole = text "?"
     asDoc p (RParseError str) = text "ParseError \{str}"
-    
+
-export 
+export
 Pretty Module where
   pretty (MkModule name decls) =
     text "module" <+> text name </> stack (map doDecl decls)
@@ -176,6 +180,6 @@ Pretty Module where
         doDecl (TypeSig nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
         doDecl (Def nm tm) = text nm <+> text "=" <+> nest 2 (pretty tm)
         doDecl (DImport nm) = text "import" <+> text nm ++ line
-        -- the behavior of nest is kinda weird, I have to do the nest before/around the </>. 
+        -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
         doDecl (Data nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
         doDecl (DCheck x y) = text "#check" <+> pretty x <+> ":" <+> pretty y