unification seems to work for kovacs examples

README.md

@@ -12,45 +12,65 @@ So smalltt has TopVar with a Level. typechecking binders end up as top too.
 
 Also delayed unfolded values for top or solved metas. This looks like glue - all the bits for the top and a cached value (it's keeping top as values).
 
-We need metas next.  SmallTT has a metactx in context as a mutable array.
+REVIEW the delayed unfolding, we're being aggressive for now. This may have been necessary until unification was in place, now we can decide to further unfold during unification.
 
-We extend the context and then drop it, so we need soemthing mutable.
+metas are assoc list, can probably just be list, but we'd need to do level/index math for the lookup.
 
-It's in top context and he pulls stuff down to context as needed. I'm overthinking this. I'm reluctant to copy Idris because resolved names are not compatible with query based, but everybody is using an array...
+They are in separate MetaContext wrapped in an IORef. I'm reluctant to copy Idris because resolved names are not compatible with query based, but everybody is using an array...
 
-I'd kinda like to see array run in js...
+Idris has a common array for metas and defs but that might be a problem if I go query based someday.
 
-Idris does a common array for metas and defs. 
+Prettier was missing a Lazy.  I'm still fairly faithful to the paper, but might want to refactor that to push the computation down into the `if`.
 
-Prettier was missing a Lazy.
+Zoo3 runs now, I had to fix meta / meta unification.
 
-Zoo3, mostly runs aside from eqTest. 
+I've added a bunch of info logs for the editor support.
+
+Zoo4 examples run now.
+
+Maybe do `data` next.  There is a crude version in place, we'll want to fix that, typecheck the new stuff, and then add cases. (Maybe introduce eliminators.)
+
+When I generate code, I'll eventually run up against the erased thing. (I'll want to erase some of the stuff that is compile time.)  But we'll generate code and decide how far we need to take this.  It's probably pointless to just reproduce Idris.
+
+When I self host, I'll have to drop or implement typeclasses. I do understand auto enough to make it happen.
+
+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?
 
 Parser:
-- [x] unify broken for zoo3 `cons`
 - [ ] parser for block comments
 - [x] import statement
 - [x] def
 - [x] simple decl
-- [x] List not in scope
+
+Misc:
 - [x] vscode support for .newt
-- [ ] Should I switch this back over to the App monad?
 - [x] Error object like pi-forall
-- [ ] Get implicits working
+  - [ ] I think I'll need to go with non-generic error type once I need to do something other than print them
+- [x] Get unification working (zoo3)
+- [x] Get implicits working (zoo4)
 - [x] Replace on define
 - [x] more sugar on lambdas
 - [ ] tests for parsing and pretty printing
+- [ ] white box tests for internals
+  - Maybe look at narya for examples of what I should be testing
 - [ ] inductive types
-  - [ ] read data definitions 1/2 done
+  - read data definitions 1/2 done
 - [x] read files
 - [x] process a file
 - [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
 - [ ] compilation
-
+  - I'm thinking I get data working first
 - [ ] write tests
+- [ ] Split up code better
 
 Forward:
 

newt-vscode/src/extension.ts

@@ -27,9 +27,9 @@ export function activate(context: vscode.ExtensionContext) {
 
       for (let i = 0; i < lines.length; i++) {
         const line = lines[i];
-        const match = line.match(/ERROR at \((\d+), (\d+)\): (.*)/);
+        const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\): (.*)/);
         if (match) {
-          let [_full, line, column, message] = match;
+          let [_full, kind, line, column, message] = match;
           let lnum = Number(line);
           let cnum = Number(column);
           let start = new vscode.Position(lnum, cnum);
@@ -47,7 +47,7 @@ export function activate(context: vscode.ExtensionContext) {
           ) {
             message += "\n" + lines[++i];
           }
-          const severity = vscode.DiagnosticSeverity.Error;
+          const severity = kind === 'ERROR' ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information
           const diag = new vscode.Diagnostic(range, message, severity);
           diagnostics.push(diag);
         }

newt/zoo3.newt

@@ -54,23 +54,5 @@ hundred = mul ten ten
 thousand : Nat
 thousand = mul ten hundred
 
--- All of these fail, but are they funext?
+eqTest : Eq _ hundred hundred
--- works for zoo3, but maybe I'm expanding stuff too eagerly
+eqTest = refl _ _
-
--- eq : Eq _ true true
--- eq = refl
-
--- eqTest2 : Eq _ five five
--- eqTest2 = refl
-
--- -- This one breaks
--- eqTest : Eq _ hundred hundred
--- -- eqTest = refl _ _
-
--- Add the rest
-
-
--- unify (%pi _ E (%var 3 []) (%cl [(%var 6 []), (%var 3 []), (%var 0 []), (%var 2 []), (%var 1 []), (%var 0 [])] (Bnd 2))) with 
---       (%pi _ E (%var 2 []) (%cl [(%var 6 []), (%var 2 []), (%var 0 []), (%var 1 []), (%var 0 [])] (Bnd 2)))
--- ->    (%pi _ E (%var 3 []) (%cl [(%var 6 []), (%var 3 []), (%var 0 []), (%var 2 []), (%var 1 []), (%var 0 [])] (Bnd 2))) with 
---       (%pi _ E (%var 2 []) (%cl [(%var 6 []), (%var 2 []), (%var 0 []), (%var 1 []), (%var 0 [])] (Bnd 2)))

src/Lib/Check.idr

@@ -21,7 +21,7 @@ data PRen = PR Nat Nat (List Nat)
 forceMeta : Val -> M Val
 -- TODO - need to look up metas
 forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
-  (Unsolved k xs) => pure (VMeta ix sp)
+  (Unsolved pos k xs) => pure (VMeta ix sp)
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
@@ -63,7 +63,7 @@ rename meta ren lvl v = go ren lvl v
 
 lams : Nat -> Tm -> Tm
 lams 0 tm = tm
-lams (S k) tm = Lam "arg\{show k}" Explicit (lams k tm)
+lams (S k) tm = Lam "arg:\{show k}" Explicit (lams k tm)
 
 solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
 solve l m sp t = do
@@ -75,15 +75,19 @@ solve l m sp t = do
   solveMeta top m soln
   pure ()
 
-unify : (l : Nat) -> Val -> Val  -> M  ()
+parameters (ctx: Context)
+  unify : (l : Nat) -> Val -> Val  -> M  ()
 
-unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
+  unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
-unifySpine l False _ _ = throwError $ E (0,0) "unify failed"
+  unifySpine l False _ _ = error [DS "unify failed at head"] -- unreachable now
-unifySpine l True [<] [<] = pure ()
+  unifySpine l True [<] [<] = pure ()
-unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
+  unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
-unifySpine l True _ _ = throwError $ E (0,0) "meta spine length mismatch"
+  unifySpine l True _ _ = error [DS "meta spine length mismatch"]
 
-unify l t u = do
+  unify l t u = do
+    putStrLn "Unify \{show ctx.lvl}"
+    putStrLn "  \{show l} \{show t}"
+    putStrLn "  =?= \{show u}"
     t' <- forceMeta t
     u' <- forceMeta u
     case (t',u') of
@@ -91,37 +95,68 @@ unify l t u = do
       (t,           VLam _ _ t'  ) => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
       (VLam _ _ t,  t'           ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
       (VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar l [<]) !(b' $$ VVar l [<])
-    (VVar k sp,   VVar k' sp'  ) => unifySpine l (k == k') sp sp'
+      (VVar k sp,   VVar k' sp'  ) =>
-    (VRef n sp,   VRef n' sp'  ) => unifySpine l (n == n') sp sp'
+        if k == k' then unifySpine l (k == k') sp sp'
-    (VMeta i sp,  VMeta i' sp' ) => unifySpine l (i == i') sp sp'
+        else error [DS "vvar mismatch \{show k} \{show k'}"]
-
+      (VRef k sp,   VRef k' sp'  ) =>
+        if k == k' then unifySpine l (k == k') sp sp'
+        else error [DS "vref mismatch \{show k} \{show k'}"]
+      (VMeta k sp,  VMeta k' sp' ) =>
+        if k == k' then unifySpine l (k == k') sp sp'
+        else solve l k sp (VMeta k' sp')
       (t,           VMeta i' sp') => solve l i' sp' t
       (VMeta i sp, t'           ) => solve l i sp t'
       (VU, VU) => pure ()
-    _ => throwError $ E (0,0) "unify failed"
+      -- REVIEW consider quoting back
+      _ => error [DS "unify failed", DS (show t'), DS "=?=", DS (show u') ]
 
+insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
+insert ctx tm ty = do
+  case !(forceMeta ty) of
+    VPi x Implicit a b => do
+      m <- freshMeta ctx
+      mv <- eval ctx.env CBN m
+      insert ctx (App tm m) !(b $$ mv)
+    va => pure (tm, va)
 
 export
 infer : Context -> Raw  -> M  (Tm, Val)
 
 export
 check : Context -> Raw -> Val  -> M  Tm
-check ctx (RSrcPos x tm) ty = check ({pos := x} ctx) tm ty
+check ctx tm ty with (force ty)
-check ctx (RLam nm icit tm) ty = case ty of                    
+  check ctx (RSrcPos x tm) _ | ty = check ({pos := x} ctx) tm ty
-                  (VPi pinm icit a b) => do
+  check ctx t@(RLam nm icit tm) _ | ty = case ty of
-                    -- TODO icit
+          (VPi nm' icit' a b) => do
+            putStrLn "icits \{nm} \{show icit} \{nm'} \{show icit'}"
+            if icit == icit' then do
                 let var = VVar (length ctx.env) [<]
                 let ctx' = extend ctx nm a
                 tm' <- check ctx' tm !(b $$ var)
                 pure $ Lam nm icit tm'
+              else if icit' == Implicit then do
+                let var = VVar (length ctx.env) [<]
+                ty' <- b $$ var
+                sc <- check (extend ctx nm' a) t ty'
+                pure $ Lam nm' icit' sc
+              else
+                error [(DS "Icity issue checking \{show t} at \{show ty}")]
           other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
-check ctx tm ty = do
+  check ctx tm _ | (VPi nm' Implicit a b) = do
-  (tm', ty') <- infer ctx tm
+    putStrLn "XXX edge \{show tm} against VPi"
-  -- This is where the conversion check / pattern unification go
+    let var = VVar (length ctx.env) [<]
-  unify ctx.lvl ty' ty
+    ty' <- b $$ var
-  -- if quote 0 ty /= quote 0 ty' then
+    sc <- check (extend ctx nm' a) tm ty'
-  --     error [DS "type mismatch got", DD (quote 0 ty'), DS "expected", DD (quote 0 ty)]
+    pure $ Lam nm' Implicit sc
-  --   else pure tm'
+  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)
+    (tm', ty') <- case !(infer ctx tm) of
+      (tm'@(Lam{}),ty') => pure (tm', ty')
+      (tm', ty') => insert ctx tm' ty'
+    putStrLn "infer \{show tm} to \{show tm'} : \{show ty'} expect \{show ty}"
+    when( ctx.lvl /= length ctx.env) $ error [DS "level mismatch \{show ctx.lvl} \{show ctx.env}"]
+    unify ctx ctx.lvl ty' ty
     pure tm'
 
 infer ctx (RVar nm) = go 0 ctx.types
@@ -136,12 +171,31 @@ infer ctx (RVar nm) = go 0 ctx.types
   -- need environment of name -> type..
 infer ctx (RApp t u icit) = do
   -- icit will be used for insertion, lets get this working first...
+
+  (icit, t, tty) <- case the Icit icit of
+      Explicit => do
         (t, tty) <- infer ctx t
-  case tty of
+        (t, tty) <- insert ctx t tty
-    (VPi str icit' a b) => do
+        pure (Explicit, t, tty)
+      Implicit => do
+        (t, tty) <- infer ctx t
+        pure (Implicit, t, tty)
+
+  (a,b) <- case !(forceMeta tty) of
+    (VPi str icit' a b) => if icit' == icit then pure (a,b)
+        else error [DS "IcitMismatch \{show icit} \{show icit'}"]
+
+    -- If it's not a VPi, try to unify it with a VPi
+    tty => do
+      putStrLn "unify PI for \{show tty}"
+      a <- eval ctx.env CBN !(freshMeta ctx)
+      b <- MkClosure ctx.env <$> freshMeta (extend ctx "x" ?hole)
+      unify ctx 0 tty (VPi "x" icit a b)
+      pure (a,b)
+
   u <- check ctx u a
   pure (App t u, !(b $$ !(eval ctx.env CBN u)))
-    _ => error [DS "Expected Pi type"]
+
 infer ctx RU = pure (U, VU) -- YOLO
 infer ctx (RPi nm icit ty ty2) = do
   ty' <- check ctx ty VU
@@ -157,7 +211,14 @@ infer ctx (RAnn tm rty) = do
   tm <- check ctx tm vty
   pure (tm, vty)
 
-infer ctx (RLam str icit tm) = error [DS "can't infer lambda"]
+infer ctx (RLam nm icit tm) = do
+  a <- freshMeta ctx >>= eval ctx.env CBN
+  let ctx' = extend ctx nm a
+  (tm', b) <- infer ctx' tm
+  putStrLn "make lam for \{show nm} scope \{show tm'} : \{show b}"
+  pure $ (Lam nm icit tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
+  -- error {ctx} [DS "can't infer lambda"]
+
 infer ctx RHole = do
   ty <- freshMeta ctx
   vty <- eval ctx.env CBN ty

src/Lib/Parser.idr

@@ -14,6 +14,7 @@ import Lib.Token
 import Lib.Parser.Impl
 import Syntax
 import Data.List
+import Data.Maybe
 
 -- There is the whole core vs surface thing here.
 -- might be best to do core first/ Technically don't
@@ -186,10 +187,11 @@ ibind : Parser (List (String, Icit, Raw))
 ibind = do
   sym "{"
   names <- some ident
-  sym ":"
+  ty <- optional (sym ":" >> typeExpr)
-  ty <- typeExpr
+  pos <- getPos
   sym "}"
-  pure $ map (\name => (name, Explicit, ty)) names
+  -- getPos is a hack here, I would like to position at the name... 
+  pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RHole) ty)) names
 
 -- Collect a bunch of binders (A : U) {y : A} -> ...
 binders : Parser Raw

src/Lib/Parser/Impl.idr

@@ -125,7 +125,7 @@ pred : (BTok -> Bool) -> String -> Parser String
 pred f msg = P $ \toks,com,col =>
   case toks of
     (t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} vt:\{value t}") toks com
-    [] => Fail False (error toks "eof") toks com
+    [] => Fail False (error toks "\{msg} at EOF") toks com
 
 export
 commit : Parser ()

src/Lib/Prettier.idr

@@ -13,6 +13,7 @@ export
 data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
 
 ||| `DOC` is an intermediate form used during layout/rendering
+||| The capitalization is the opposite of the paper.
 data DOC = EMPTY | TEXT String DOC | LINE Nat DOC
 
 flatten : Doc -> Doc

src/Lib/TT.idr

@@ -3,6 +3,9 @@
 -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
 -- or drop the indices for now.
 
+-- ***
+-- Kovacs has icity on App, and passes it around, but I'm not sure where it is needed since the insertion happens based on Raw.
+
 module Lib.TT
 -- For SourcePos
 import Lib.Parser.Impl
@@ -34,17 +37,21 @@ export
 error' : String -> M a
 error' msg = throwError $ E (0,0) msg
 
+-- order does indeed matter on the meta arguments
+-- because of dependent types (if we want something well-typed back out)
 
 export
 freshMeta : Context -> M Tm
 freshMeta ctx = do
   mc <- readIORef ctx.metas
-  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved mc.next ctx.bds ::) } mc
+  putStrLn "INFO at \{show ctx.pos}: fresh meta \{show mc.next}"
+  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved ctx.pos mc.next ctx.bds ::) } mc
   pure $ applyBDs 0 (Meta mc.next) ctx.bds
   where
   -- hope I got the right order here :)
   applyBDs : Nat -> Tm -> List BD -> Tm
   applyBDs k t [] = t
+  -- review the order here
   applyBDs k t (Bound :: xs) = App (applyBDs (S k) t xs) (Bnd k)
   applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
 
@@ -57,7 +64,7 @@ lookupMeta ix = do
   where
     go : List MetaEntry -> M MetaEntry
     go [] = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved k ys) :: xs) = if k == ix then pure meta else go xs
+    go (meta@(Unsolved _ k ys) :: xs) = if k == ix then pure meta else go xs
     go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs
 
 export
@@ -69,8 +76,10 @@ solveMeta ctx ix tm = do
   where
     go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
     go [] _ = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved k _) :: xs) lhs = if k == ix 
+    go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
-      then pure $ lhs <>> (Solved k tm :: xs)
+      then do
+        putStrLn "INFO at \{show pos}: solve \{show k} as \{show tm}"
+        pure $ lhs <>> (Solved k tm :: xs)
       else go xs (lhs :< meta)
     go (meta@(Solved k _) :: xs) lhs = if k == ix
       then error' "Meta \{show ix} already solved!"
@@ -146,7 +155,7 @@ eval env mode (App t u) = vapp !(eval env mode t) !(eval env mode u)
 eval env mode U = pure VU
 eval env mode (Meta i) =
   case !(lookupMeta i) of
-        (Unsolved k xs) => pure $ VMeta i [<]
+        (Unsolved _ k xs) => pure $ VMeta i [<]
         (Solved k t) => pure $ t
 eval env mode (Lam x icit t) = pure $ VLam x icit (MkClosure env t)
 eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure env b)

src/Lib/Types.idr

@@ -28,6 +28,11 @@ data Icit = Implicit | Explicit
 
 %name Icit icit
 
+export
+Show Icit where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+
 public export
 data BD = Bound | Defined
 
@@ -41,6 +46,7 @@ data Tm : Type where
   -- kovacs optimization, I think we can App out meta instead
   -- InsMeta : Nat -> List BD -> Tm
   Lam : Name -> Icit -> Tm -> Tm
+  -- Do we need to remember Icit here?
   App : Tm -> Tm -> Tm
   U   : Tm
   Pi  : Name -> Icit -> Tm -> Tm -> Tm
@@ -57,7 +63,8 @@ Show Tm where
   show (App t u) = "(\{show t} \{show u})"
   show (Meta i) = "(Meta \{show i})"
   show U = "U"
-  show (Pi str icit t u) = "(∏ \{str} : \{show t} => \{show u})"
+  show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
+  show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
   show (Let str icit t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
 
 -- I can't really show val because it's HOAS...
@@ -126,9 +133,6 @@ data Val : Type where
   VPi : Name -> Icit -> Lazy Val -> Closure -> Val
   VU : Val
 
-Show Icit where
-  show Implicit = "I"
-  show Explicit = "E"
 
 Show Closure
 
@@ -138,7 +142,8 @@ Show Val where
   show (VRef nm sp) = "(%ref \{nm} \{show sp})"
   show (VMeta ix sp) = "(%meta \{show ix} \{show sp})"
   show (VLam str icit x) = "(%lam \{str} \{show icit} \{show x})"
-  show (VPi str icit x y) = "(%pi \{str} \{show icit} \{show x} \{show y})"
+  show (VPi str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
+  show (VPi str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
   show VU = "U"
 
 public export
@@ -182,9 +187,14 @@ Can I get val back? Do we need to quote? What happens if we don't?
 
 -}
 
--- FIXME remove List BD
 public export
-data MetaEntry = Unsolved Nat (List BD) | Solved Nat Val
+data MetaEntry = Unsolved SourcePos Nat (List BD) | Solved Nat Val
+
+export
+covering
+Show MetaEntry where
+  show (Unsolved pos k xs) = "Unsolved \{show pos} \{show k}"
+  show (Solved k x) = "Solved \{show k} \{show x}"
 
 public export
 record MetaContext where

src/Main.idr

@@ -48,6 +48,7 @@ dumpContext top = do
 processDecl : Decl -> M ()
 processDecl (TypeSig nm tm) = do
   top <- get
+  putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas) tm VU
   putStrLn "got \{show ty}"
@@ -55,6 +56,7 @@ processDecl (TypeSig nm tm) = do
 
 -- FIXME - this should be in another file
 processDecl (Def nm raw) = do
+  putStrLn "-----"
   putStrLn "def \{show nm}"
   ctx <- get
   let pos = case raw of
@@ -67,6 +69,7 @@ processDecl (Def nm raw) = do
     | _ => throwError $ E pos "\{nm} already defined"
   putStrLn "check \{nm} = \{show raw} at \{show $ ty}"
   vty <- eval empty CBN ty
+  putStrLn "vty is \{show vty}"
   tm <- check (mkCtx ctx.metas) raw vty
   putStrLn "Ok \{show tm}"
   put (addDef ctx nm tm ty)

src/Syntax.idr

@@ -114,11 +114,6 @@ Show Pattern where
 Show CaseAlt where
   show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
 
-Show Icit where
-  show Implicit = "Implicit"
-  show Explicit = "Explicit"
-  -- show Eq = "Eq"
-
 covering
 Show Raw where
   show RHole = "_"