implicits working, but _slow_

.gitignore

@@ -1,2 +1,4 @@
 build/
 *.*~ATTIC
+\#*
+*~

Makefile

@@ -1,9 +1,12 @@
 SRCS=$(shell find src -name "*.idr")
 
-all: build/exec/newt
+all: build/exec/newt build/exec/newt.js
 
 build/exec/newt: ${SRCS}
 	idris2 --build newt.ipkg
 
+build/exec/newt.js: ${SRCS}
+	idris2 --cg node -o newt.js -p contrib -c src/Main.idr
+
 test: build/exec/newt
 	build/exec/newt newt/*.newt

README.md

@@ -24,7 +24,12 @@ Idris does a common array for metas and defs.
 
 
 
+Something exponential is going on with zoo3.newt.  Adding code makes it quickly worse. 
+
+
 Parser:
+- [x] unify broken for zoo3 `cons`
+- [ ] parser for block comments
 - [x] import statement
 - [x] def
 - [x] simple decl

newt/zoo3.newt

@@ -5,3 +5,52 @@ id = \ A x => x
 
 List : U -> U
 List = \ A => (L : _) -> (A -> L -> L) -> L -> L
+
+nil : (A : _) -> List A
+nil = \ A L cons nil => nil
+
+cons : (A : _) -> A -> List A -> List A
+cons = \A x xs L cons nil => cons x (xs _ cons nil)
+
+Bool : U
+Bool = (B : _) -> B -> B -> B
+
+true : Bool
+true = \ B t f => t
+
+false : Bool
+false = \ B t f => f
+
+not : Bool -> Bool
+not = \ b B t f => b B f t
+
+Eq : (A : _) -> A -> A -> U
+Eq = \A x y => (P : A -> U) -> P x -> P y
+
+refl : (A : _) (x : A) -> Eq A x x
+refl = \ A x p px => px
+
+list1 : List Bool
+list1 = cons _ true (cons _ false (nil _))
+
+-- 9 sec
+
+
+Nat : U
+Nat = (N : U) -> (N -> N) -> N -> N
+
+-- 30 sec
+
+-- five : Nat
+-- five = \ N s z => s (s (s (s (s z))))
+
+-- add : Nat -> Nat -> Nat
+-- add = \ a b N s z => a N s (b N s z)
+
+-- 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

@@ -7,6 +7,7 @@ import Lib.Prettier
 import Data.List
 import Data.Vect
 import Data.String
+import Lib.Types
 import Lib.TT
 import Lib.TopContext
 import Syntax
@@ -16,29 +17,21 @@ import Syntax
 data PRen = PR Nat Nat (List Nat)
 
 -- IORef for metas needs IO
-parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m} (top : TopContext)
 
-  -- unify : Nat -> Val -> Val -> m ()
+forceMeta : Val -> M Val
-  -- unify l (VLam _ _ t) (VLam _ _ u) = unify (l + 1) (t $$ VVar l) (u $$ VVar l)
-  -- unify l t            (VLam _ _ u) = unify (l + 1) (vapp t (VVar l)) (u $$ VVar l)
-  -- unify l (VVar k) u = ?unify_rhs_0
-  -- unify l (VRef str mt) u = ?unify_rhs_1
-  -- unify l (VMeta k) u = ?unify_rhs_2
-  -- unify l (VApp x y) u = ?unify_rhs_3
-  -- unify l (VPi str icit x y) u = ?unify_rhs_5
-  -- unify l VU u = ?unify_rhs_6
-
-  forceMeta : Val -> Val
 -- TODO - need to look up metas
-  forceMeta x = x
+forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
+  (Unsolved k xs) => pure (VMeta ix sp)
+  (Solved k t) => vappSpine t sp
+forceMeta x = pure x
 
 -- return renaming, the position is the new VVar
-  invert : Nat -> List Val -> m (List Nat)
+invert : Nat -> SnocList Val -> M (List Nat)
 invert lvl sp = go sp []
   where
-      go : List Val -> List Nat -> m (List Nat)
+    go : SnocList Val -> List Nat -> M (List Nat)
-      go [] acc = pure acc
+    go [<] acc = pure $ reverse acc
-      go ((VVar k []) :: xs) acc = do
+    go (xs :< VVar k [<]) acc = do
       if elem k acc 
         then throwError $ E (0,0) "non-linear pattern"
         else go xs (k :: acc)
@@ -47,13 +40,13 @@ parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m}
 -- 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 : Nat ->  List Nat -> Nat -> Val  -> M  Tm
 rename meta ren lvl v = go ren lvl v
   where
-      go : List Nat -> Nat -> Val -> m Tm
+    go : List Nat -> Nat -> Val  -> M  Tm
-      goSpine : List Nat -> Nat -> Tm -> List Val -> m Tm
+    goSpine : List Nat -> Nat -> Tm -> SnocList Val  -> M  Tm
-      goSpine ren lvl tm [] = pure tm
+    goSpine ren lvl tm [<] = pure tm
-      goSpine ren lvl tm (x :: xs) = do
+    goSpine ren lvl tm (xs :< x) = do
       xtm <- go ren lvl x
       goSpine ren lvl (App tm xtm) xs
 
@@ -64,35 +57,40 @@ parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m}
     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 icit t) = pure (Lam n icit !(go (lvl :: ren) (S lvl) (t $$ VVar lvl [])))
+    go ren lvl (VLam n icit t) = pure (Lam n icit !(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 (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 : Nat -> Tm -> Tm
-  -- lams 0 tm = tm
+lams 0 tm = tm
-  -- lams (S k) tm = Lam 
+lams (S k) tm = Lam "arg\{show k}" Explicit (lams k tm)
 
-  solve : Nat -> Nat -> List Val -> Val -> m ()
+solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
 solve l m sp t = do
   ren <- invert l sp
   tm <- rename m ren l t
-    printLn "solution to \{show m} is \{show tm}"
+  let tm = lams (length sp) tm
-
+  top <- get
+  soln <- eval [] CBN tm
+  solveMeta top m soln
   pure ()
 
-  unify : (l : Nat) -> Val -> Val -> m ()
+unify : (l : Nat) -> Val -> Val  -> M  ()
 
-  unifySpine : Nat -> Bool -> List Val -> List Val -> m ()
+unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
 unifySpine l False _ _ = throwError $ E (0,0) "unify failed"
-  unifySpine l True [] [] = pure ()
+unifySpine l True [<] [<] = pure ()
-  unifySpine l True (x :: xs) (y :: ys) = 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"
 
-  unify l t u = case (forceMeta t, forceMeta u) of
+unify l t u = do
-    (VLam _ _ t,  VLam _ _ t'  ) => unify (l + 1) (t $$ VVar l []) (t' $$ VVar l [])
+  t' <- forceMeta t
-    (t,           VLam _ _ t'  ) => unify (l + 1) (t `vapp` VVar l []) (t' $$ VVar l [])
+  u' <- forceMeta u
-    (VLam _ _ t,  t'           ) => unify (l + 1) (t $$ VVar l []) (t' `vapp` VVar l [])
+  case (t',u') of
-    (VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) (b $$ VVar l []) (b' $$ VVar l [])
+    (VLam _ _ t,  VLam _ _ t'  ) => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
+    (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'
     (VRef n sp,   VRef n' sp'  ) => unifySpine l (n == n') sp sp'
     (VMeta i sp,  VMeta i' sp' ) => unifySpine l (i == i') sp sp'
@@ -104,19 +102,19 @@ parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m}
 
 
 export
-  infer : Context -> Raw -> m (Tm, Val)
+infer : Context -> Raw  -> M  (Tm, Val)
 
 export
-  check : Context -> Raw -> Val -> m Tm
+check : Context -> Raw -> Val  -> M  Tm
 check ctx (RSrcPos x tm) ty = check ({pos := x} ctx) tm ty
 check ctx (RLam nm icit tm) ty = case ty of                    
                   (VPi pinm icit a b) => do
                     -- TODO icit
-                      let var = VVar (length ctx.env) []
+                    let var = VVar (length ctx.env) [<]
                     let ctx' = extend ctx nm a
-                      tm' <- check ctx' tm (b $$ var)
+                    tm' <- check ctx' tm !(b $$ var)
                     pure $ Lam nm icit tm'
-                    other => error [(DS "Expected pi type, got \{show $ quote 0 ty}")]
+                  other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
 check ctx tm ty = do
   (tm', ty') <- infer ctx tm
   -- This is where the conversion check / pattern unification go
@@ -125,12 +123,13 @@ parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m}
   --     error [DS "type mismatch got", DD (quote 0 ty'), DS "expected", DD (quote 0 ty)]
   --   else pure tm'
   pure tm'
+
 infer ctx (RVar nm) = go 0 ctx.types
   where
-      go : Nat -> Vect n (String, Val) -> m (Tm, Val)
+    go : Nat -> Vect n (String, Val)  -> M  (Tm, Val)
-      go i [] = case lookup nm top of
+    go i [] = case lookup nm !(get) of
-        Just (MkEntry name ty (Fn t)) => pure (Ref nm (Just t), eval [] CBN ty)
+      Just (MkEntry name ty (Fn t)) => pure (Ref nm (Just t), !(eval [] CBN ty))
-        Just (MkEntry name ty _) => pure (Ref nm Nothing, eval [] CBN ty)
+      Just (MkEntry name ty _) => pure (Ref nm Nothing, !(eval [] CBN ty))
       Nothing => error [DS "\{show nm} not in scope"]
     go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty) 
       else go (i + 1) xs
@@ -141,27 +140,27 @@ parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m}
   case tty of
     (VPi str icit' a b) => do
       u <- check ctx u a
-        pure (App t u, b $$ eval ctx.env CBN t)
+      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
-    let vty' := eval ctx.env CBN ty'
+  vty' <- eval ctx.env CBN ty'
   let nm := fromMaybe "_" nm
   ty2' <- check (extend ctx nm vty') ty2 VU
   pure (Pi nm icit ty' ty2', VU)
-  infer ctx (RLet str tm tm1 tm2) = ?rhs_5
+infer ctx (RLet str tm tm1 tm2) = error [DS "implement RLet"]
 infer ctx (RSrcPos x tm) = infer ({pos := x} ctx) tm
 infer ctx (RAnn tm rty) = do
   ty <- check ctx rty VU
-    let vty = eval ctx.env CBN ty 
+  vty <- eval ctx.env CBN ty 
   tm <- check ctx tm vty
   pure (tm, vty)
 
 infer ctx (RLam str icit tm) = error [DS "can't infer lambda"]
 infer ctx RHole = do
   ty <- freshMeta ctx
-    let vty = eval ctx.env CBN ty
+  vty <- eval ctx.env CBN ty
   tm <- freshMeta ctx
   pure (tm, vty)
   

src/Lib/Parser.idr

@@ -1,5 +1,5 @@
 module Lib.Parser
-import Lib.TT
+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?
@@ -241,9 +241,14 @@ parseData = do
   -- TODO - turn decls into something more useful
   pure $ Data name ty decls
 
+-- Not sure what I want here.
+-- I can't get a Tm without a type, and then we're covered by the other stuff
+parseNorm : Parser Decl
+parseNorm = DCheck <$ keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
+
 export
 parseDecl : Parser Decl
-parseDecl = parseImport <|> parseSig <|> parseDef <|> parseData
+parseDecl = parseImport <|> parseSig <|> parseDef <|> parseNorm <|> parseData
 
 export
 parseMod : Parser Module

src/Lib/TT.idr

@@ -7,7 +7,7 @@ module Lib.TT
 -- For SourcePos
 import Lib.Parser.Impl
 import Lib.Prettier
-
+import Lib.Types
 import Control.Monad.Error.Interface
 
 import Data.IORef
@@ -16,302 +16,7 @@ import Data.List
 import Data.Vect
 import Data.SortedMap
 
-public export
+-- Errors cribbed from pi-forall
-Name : Type
-Name = String
-
-public export
-data Icit = Implicit | Explicit
-
-%name Icit icit
-
-public export
-data BD = Bound | Defined
-
-
-public export
-data Tm : Type where
-  Bnd : Nat -> Tm
-  -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
-  Ref : String -> Maybe Tm -> Tm
-  Meta : Nat -> Tm
-  -- kovacs optimization, I think we can App out meta instead
-  -- InsMeta : Nat -> List BD -> Tm
-  Lam : Name -> Icit -> Tm -> Tm
-  App : Tm -> Tm -> Tm
-  U   : Tm
-  Pi  : Name -> Icit -> Tm -> Tm -> Tm
-  Let : Name -> Icit -> Tm -> Tm -> Tm -> Tm
-
-%name Tm t, u, v
-
-public export
-Show Tm where
-  show (Bnd k) = "(Bnd \{show k})"
-  show (Ref str _) = "(Ref \{show str})"
-  show (Lam nm Implicit t) = "(λ {\{nm}} => \{show  t})"
-  show (Lam nm Explicit t) = "(λ \{nm}  => \{show  t})"
-  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 (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...
-
--- TODO derive
-export 
-Eq Icit where
-  Implicit == Implicit = True
-  Explicit == Explicit = True
-  _ == _ = False
-
-||| Eq on Tm. We've got deBruijn indices, so I'm not comparing names
-export
-Eq (Tm) where
-  -- (Local x) == (Local y) = x == y
-  (Bnd x) == (Bnd y) = x == y
-  (Ref x _) == (Ref y _) = x == y
-  (Lam n icit t) == (Lam n' icit' t') = icit == icit' && t == t'
-  (App t u) == App t' u' = t == t' && u == u'
-  U == U = True
-  (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
-  (Let n icit t u v) == (Let n' icit' t' u' v') = t == t' && u == u' && v == v'
-  _ == _ = False
-
-public export
-Pretty Tm where
-  pretty (Bnd k) = ?rhs_0
-  pretty (Ref str mt) = text str
-  pretty (Meta k) = text "?m\{show k}"
-  pretty (Lam str Implicit t) = text "(\\ {\{str}} => " <+> pretty t <+> ")"
-  pretty (Lam str Explicit t) = text "(\\ \{str} => " <+> pretty t <+> ")"
-  pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
-  pretty U = "U"
-  pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> "=>" <+> pretty u <+> ")"
-  pretty (Let str icit t u v) = text "let" <+> text str <+> ":" <+> pretty t <+> "=" <+> pretty u
-
--- public export
--- data Closure : Nat -> Type
-data Val : Type
-
-
--- IS/TypeTheory.idr is calling this a Kripke function space
--- Yaffle, IS/TypeTheory use a function here.
--- Kovacs, Idris use Env and Tm
-
--- in cctt kovacs refers to this choice as defunctionalization vs HOAS
--- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization
--- the tradeoff is access to internals of the function
-
--- Yaffle is vars -> vars here
-
-
-public export
-data Closure : Type
-
-public export
-data Val : Type where
-  -- This will be local / flex with spine.
-  VVar : (k : Nat) -> (sp : List Val) -> Val
-  -- I wanted the Maybe Tm in here, but for now we're always expanding.
-  -- Maybe this is where I glue
-  VRef : (nm : String) -> (sp : List Val) -> Val
-  -- we'll need to look this up in ctx with IO
-  VMeta : (ix : Nat) -> (sp : List Val) -> Val
-  VLam : Name -> Icit -> Closure -> Val
-  VPi : Name -> Icit -> Lazy Val -> Closure -> Val
-  VU : Val
-
-public export
-Env : Type
-Env = List Val
-
-public export
-data Mode = CBN | CBV
-
-export
-eval : Env -> Mode -> Tm -> Val
-
-data Closure = MkClosure Env Tm
-
-public export
-($$) : {auto mode : Mode} -> Closure -> Val -> Val
-($$) (MkClosure env tm) u = eval (u :: env) mode tm
-
-public export
-infixl 8 $$
-
-export
-vapp : Val -> Val -> Val
-vapp (VLam _ icit t) u = t $$ u
-vapp (VVar k sp) u = VVar k (u :: sp)
-vapp (VRef nm sp) u = VRef nm (u :: sp)
-vapp (VMeta k sp) u = VMeta k (u :: sp)
-vapp _ _ = ?throw_impossible
-
-bind : Val -> Env -> Env
-bind v env = v :: env
-
--- Do we want a def in here instead?  We'll need DCon/TCon eventually
--- I need to be aggressive about reduction, I guess. I'll figure it out
--- later, maybe need lazy glued values.
-eval env mode (Ref x (Just tm)) = eval env mode tm
-eval env mode (Ref x Nothing) = VRef x []
-eval env mode (App (Ref x (Just tm)) u) = vapp (eval env mode tm) (eval env mode u)
-eval env mode (App t u) = vapp (eval env mode t) (eval env mode u)
-eval env mode U = VU
-eval env mode (Meta i) = VMeta i []
-eval env mode (Lam x icit t) = VLam x icit (MkClosure env t)
-eval env mode (Pi x icit a b) = VPi x icit (eval env mode a) (MkClosure env b)
-eval env mode (Let x icit ty t u) = eval (eval env mode t :: env) mode u
-eval env mode (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index
-                   in rval
-
-export
-quote : (lvl : Nat) -> Val -> Tm
-
-quoteSp : (lvl : Nat) -> Tm -> List Val -> Tm
-quoteSp lvl t [] = t
-quoteSp lvl t (x :: xs) = quoteSp lvl (App t (quote lvl x)) xs
-
-quote l (VVar k sp) = quoteSp l (Bnd ((l `minus` k) `minus` 1)) sp -- level to index
-quote l (VMeta i sp) = quoteSp l (Meta i) sp
-quote l (VLam x icit t) = Lam x icit (quote (S l) (t $$ VVar l []))
-quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b $$ VVar l []))
-quote l VU = U
-quote l (VRef n sp) = quoteSp l (Ref n Nothing) sp
-
--- Can we assume closed terms?
--- ezoo only seems to use it at [], but essentially does this:
-export
-nf : Env -> Tm -> Tm
-nf env t = quote (length env) (eval env CBN t)
-
-
-{-
-smalltt
-
-smalltt gets into weird haskell weeds in eval - shifting top level to the left
-and tagging meta vs top with a bit.
-
-I think something subtle is going on with laziness on Elaboration.hs:300
-yeah, and define is even inlined.
-
-So it has a top context, and clears out almost everything for processing a def in
-a different kind of context.
-
-we very much need an idea of local context for metas. I don't want to abstract over
-the entire program.
-
-So I guess we have top and local then?
-
-With haskell syntax. I think we can have Axiom for claims and rewrite to def later.
-
-Hmm, so given ezoo, if I'm going simple, I could keep BDs short, and use the normal
-context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value? 
-
-ok, so with just one context, Env is List Val and we're getting Tm back from type checking.
-
-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
-
-public export
-record MetaContext where
-  constructor MC
-  metas : List MetaEntry
-  next : Nat
-
-
-public export
-data Def = Axiom | TCon (List String) | DCon Nat | Fn Tm
-
-Show Def where
-  show Axiom = "axiom"
-  show (TCon strs) = "TCon \{show strs}"
-  show (DCon k) = "DCon \{show k}"
-  show (Fn t) = "Fn \{show t}"
-
-||| entry in the top level context
-public export
-record TopEntry where
-  constructor MkEntry
-  name : String
-  type : Tm
-  def : Def
-
--- FIXME snoc
-
-export
-Show TopEntry where
-  show (MkEntry name type def) = "\{name} : \{show type} := \{show def}"
-
-||| Top level context.
-||| Most of the reason this is separate is to have a different type
-||| `Def` for the entries.
-|||
-||| The price is that we have names in addition to levels. Do we want to
-||| expand these during conversion?
-public export
-record TopContext where
-  constructor MkTop
-  -- We'll add a map later?
-  defs : List TopEntry
-  metas : IORef MetaContext
-  -- metas : TODO
-
--- we'll use this for typechecking, but need to keep a TopContext around too.
-public export
-record Context where
-  constructor MkCtx
-  lvl : Nat
-  -- shall we use lvl as an index?
-  env : Env                  -- Values in scope
-  types : Vect lvl (String, Val) -- types and names in scope
-  -- so we'll try "bds" determines length of local context
-  bds  : List BD          -- bound or defined
-  pos : SourcePos            -- the last SourcePos that we saw
-  
-  -- We only need this here if we don't pass TopContext
-  -- top : TopContext
-  metas : IORef MetaContext
-
-export
-freshMeta : HasIO m => Context -> m Tm
-freshMeta ctx = do
-  mc <- readIORef ctx.metas
-  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved 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
-  applyBDs k t (Bound :: xs) = applyBDs (S k) (App t (Bnd k)) xs
-  applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
-
--- solveMeta : HasIO m => Context -> m Tm
--- solveMeta ctx = do
---   mc <- readIORef ctx.metas
-  
-
--- we need more of topcontext later - Maybe switch it up so we're not passing
--- around top
-export
-mkCtx : IORef MetaContext -> Context
-mkCtx metas = MkCtx 0 [] [] [] (0,0) metas
-
-export partial
-Show Context where
-  show ctx = "Context \{show $ map fst $ ctx.types}"
-
--- TODO Pretty Context
-
--- idea cribbed from pi-forall
 public export
 data ErrorSeg : Type where
   DD : Pretty a => a -> ErrorSeg
@@ -322,15 +27,67 @@ toDoc (DD x) = pretty x
 toDoc (DS str) = text str
 
 export
-error : {0 m : Type -> Type} -> {auto _ : MonadError Error m} ->
+error : {auto ctx : Context} -> List ErrorSeg -> M a
-    {auto ctx : Context} -> List ErrorSeg -> m a
 error xs = throwError $ E ctx.pos (render 80 $ spread $ map toDoc xs)
 
+export
+error' : String -> M a
+error' msg = throwError $ E (0,0) msg
+
+
+export
+freshMeta : Context -> M Tm
+freshMeta ctx = do
+  mc <- readIORef ctx.metas
+  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved 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
+  applyBDs k t (Bound :: xs) = App (applyBDs (S k) t xs) (Bnd k)
+  applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
+
+export
+lookupMeta : Nat -> M MetaEntry
+lookupMeta ix = do
+  ctx <- get
+  mc <- readIORef ctx.metas
+  go mc.metas
+  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@(Solved k x) :: xs) = if k == ix then pure meta else go xs
+
+export
+solveMeta : TopContext -> Nat -> Val -> M ()
+solveMeta ctx ix tm = do
+  mc <- readIORef ctx.metas
+  metas <- go mc.metas [<]
+  writeIORef ctx.metas $ {metas := metas} mc
+  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 
+      then 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!"
+      else go xs (lhs :< meta)
+
+export partial
+Show Context where
+  show ctx = "Context \{show $ map fst $ ctx.types}"
+
+-- TODO Pretty Context
+
+
 ||| add a binding to environment
 export
 extend : Context -> String -> Val -> Context
 extend ctx name ty =
-    { lvl $= S, env $= (VVar ctx.lvl [] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
+    { lvl $= S, env $= (VVar ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
     
 -- I guess we define things as values?
 export
@@ -340,12 +97,86 @@ define ctx name val ty =
 
 
 -- not used
-lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} ->
+lookup : Context -> String -> M Val
-      Context -> String -> m Val
 lookup ctx nm = go ctx.types
   where
-    go : Vect n (String,Val) -> m Val
+    go : Vect n (String,Val) -> M Val
-    go [] = throwError "Name \{nm} not in scope"
+    go [] = error' "Name \{nm} not in scope"
     go ((n, ty) :: xs) = if n == nm then pure ty else go xs
 
 
+-- Need to wire in the metas...
+-- if it's top / ctx / IORef, I also need IO...
+-- if I want errors, I need m anyway.  I've already got an error down there.
+
+
+
+export
+eval : Env -> Mode -> Tm -> M Val
+
+public export
+($$) : {auto mode : Mode} -> Closure -> Val -> M Val
+($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm
+
+public export
+infixl 8 $$
+
+export
+vapp : Val -> Val -> M Val
+vapp (VLam _ icit t) u = t $$ u
+vapp (VVar k sp) u = pure $ VVar k (sp :< u)
+vapp (VRef nm sp) u = pure $ VRef nm (sp :< u)
+vapp (VMeta k sp) u = pure $ VMeta k (sp :< u)
+vapp t u = error' "impossible in vapp \{show t} to \{show u}"
+
+export
+vappSpine : Val -> SnocList Val -> M Val
+vappSpine t [<] = pure t
+vappSpine t (xs :< x) = vapp !(vappSpine t xs) x
+
+bind : Val -> Env -> Env
+bind v env = v :: env
+
+-- Do we want a def in here instead?  We'll need DCon/TCon eventually
+-- I need to be aggressive about reduction, I guess. I'll figure it out
+-- later, maybe need lazy glued values.
+eval env mode (Ref x (Just tm)) = eval env mode tm
+eval env mode (Ref x Nothing) = pure $ VRef x [<]
+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 [<]
+        (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)
+eval env mode (Let x icit ty t u) = eval (!(eval env mode t) :: env) mode u
+eval env mode (Bnd i) = case getAt i env of
+  Just rval => pure rval
+  Nothing => error' "Bad deBruin index \{show i}"
+  
+export
+quote : (lvl : Nat) -> Val -> M Tm
+
+quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm
+quoteSp lvl t [<] = pure t
+quoteSp lvl t (xs :< x) = 
+  pure $ App !(quoteSp lvl t xs) !(quote lvl x)
+  -- quoteSp lvl (App t !(quote lvl x)) xs  -- snoc says previous is right
+
+quote l (VVar k sp) = if k < l
+  then quoteSp l (Bnd ((l `minus` k) `minus` 1)) sp -- level to index
+  else ?borken
+quote l (VMeta i sp) = quoteSp l (Meta i) sp
+quote l (VLam x icit t) = pure $ Lam x icit !(quote (S l) !(t $$ VVar l [<]))
+quote l (VPi x icit a b) = pure $ Pi x icit !(quote l a) !(quote (S l) !(b $$ VVar l [<]))
+quote l VU = pure U
+quote l (VRef n sp) = quoteSp l (Ref n Nothing) sp
+
+-- Can we assume closed terms?
+-- ezoo only seems to use it at [], but essentially does this:
+export
+nf : Env -> Tm -> M Tm
+nf env t = quote (length env) !(eval env CBN t)
+
+

src/Lib/TopContext.idr

@@ -1,7 +1,7 @@
 module Lib.TopContext
 
 import Data.String
-import Lib.TT
+import Lib.Types
 import Data.IORef
 
 -- I want unique ids, to be able to lookup, update, and a Ref so

src/Lib/Types.idr

@@ -0,0 +1,258 @@
+module Lib.Types
+-- I'm not sure this is related, or just a note to self (Presheaves on Porpoise)
+
+-- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
+-- or drop the indices for now.
+
+-- For SourcePos
+import Lib.Parser.Impl
+import Lib.Prettier
+
+import public Control.Monad.Error.Either
+import public Control.Monad.Error.Interface
+import public Control.Monad.State
+
+import Data.IORef
+import Data.Fin
+import Data.List
+import Data.SnocList
+import Data.Vect
+import Data.SortedMap
+
+public export
+Name : Type
+Name = String
+
+public export
+data Icit = Implicit | Explicit
+
+%name Icit icit
+
+public export
+data BD = Bound | Defined
+
+
+public export
+data Tm : Type where
+  Bnd : Nat -> Tm
+  -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
+  Ref : String -> Maybe Tm -> Tm
+  Meta : Nat -> Tm
+  -- kovacs optimization, I think we can App out meta instead
+  -- InsMeta : Nat -> List BD -> Tm
+  Lam : Name -> Icit -> Tm -> Tm
+  App : Tm -> Tm -> Tm
+  U   : Tm
+  Pi  : Name -> Icit -> Tm -> Tm -> Tm
+  Let : Name -> Icit -> Tm -> Tm -> Tm -> Tm
+
+%name Tm t, u, v
+
+public export
+Show Tm where
+  show (Bnd k) = "(Bnd \{show k})"
+  show (Ref str _) = "(Ref \{show str})"
+  show (Lam nm Implicit t) = "(\\ {\{nm}} => \{show  t})"
+  show (Lam nm Explicit t) = "(\\ \{nm}  => \{show  t})"
+  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 (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...
+
+-- TODO derive
+export 
+Eq Icit where
+  Implicit == Implicit = True
+  Explicit == Explicit = True
+  _ == _ = False
+
+||| Eq on Tm. We've got deBruijn indices, so I'm not comparing names
+export
+Eq (Tm) where
+  -- (Local x) == (Local y) = x == y
+  (Bnd x) == (Bnd y) = x == y
+  (Ref x _) == (Ref y _) = x == y
+  (Lam n icit t) == (Lam n' icit' t') = icit == icit' && t == t'
+  (App t u) == App t' u' = t == t' && u == u'
+  U == U = True
+  (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
+  (Let n icit t u v) == (Let n' icit' t' u' v') = t == t' && u == u' && v == v'
+  _ == _ = False
+
+public export
+Pretty Tm where
+  pretty (Bnd k) = ?rhs_0
+  pretty (Ref str mt) = text str
+  pretty (Meta k) = text "?m\{show k}"
+  pretty (Lam str Implicit t) = text "(\\ {\{str}} => " <+> pretty t <+> ")"
+  pretty (Lam str Explicit t) = text "(\\ \{str} => " <+> pretty t <+> ")"
+  pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
+  pretty U = "U"
+  pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> "=>" <+> pretty u <+> ")"
+  pretty (Let str icit t u v) = text "let" <+> text str <+> ":" <+> pretty t <+> "=" <+> pretty u
+
+-- public export
+-- data Closure : Nat -> Type
+data Val : Type
+
+
+-- IS/TypeTheory.idr is calling this a Kripke function space
+-- Yaffle, IS/TypeTheory use a function here.
+-- Kovacs, Idris use Env and Tm
+
+-- in cctt kovacs refers to this choice as defunctionalization vs HOAS
+-- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization
+-- the tradeoff is access to internals of the function
+
+-- Yaffle is vars -> vars here
+
+
+public export
+data Closure : Type
+
+public export
+data Val : Type where
+  -- This will be local / flex with spine.
+  VVar : (k : Nat) -> (sp : SnocList Val) -> Val
+  -- I wanted the Maybe Tm in here, but for now we're always expanding.
+  -- Maybe this is where I glue
+  VRef : (nm : String) -> (sp : SnocList Val) -> Val
+  -- we'll need to look this up in ctx with IO
+  VMeta : (ix : Nat) -> (sp : SnocList Val) -> Val
+  VLam : Name -> Icit -> Closure -> Val
+  VPi : Name -> Icit -> Lazy Val -> Closure -> Val
+  VU : Val
+
+Show Icit where
+  show Implicit = "I"
+  show Explicit = "E"
+
+Show Closure
+
+covering export
+Show Val where
+  show (VVar k sp) = "(%var \{show k} \{show sp})"
+  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 VU = "U"
+
+public export
+Env : Type
+Env = List Val
+
+public export
+data Mode = CBN | CBV
+
+public export
+data Closure = MkClosure Env Tm
+
+covering
+Show Closure where
+  show (MkClosure xs t) = "(%cl \{show xs} \{show t})"
+{-
+smalltt
+
+smalltt gets into weird haskell weeds in eval - shifting top level to the left
+and tagging meta vs top with a bit.
+
+I think something subtle is going on with laziness on Elaboration.hs:300
+yeah, and define is even inlined.
+
+So it has a top context, and clears out almost everything for processing a def in
+a different kind of context.
+
+we very much need an idea of local context for metas. I don't want to abstract over
+the entire program.
+
+So I guess we have top and local then?
+
+With haskell syntax. I think we can have Axiom for claims and rewrite to def later.
+
+Hmm, so given ezoo, if I'm going simple, I could keep BDs short, and use the normal
+context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value? 
+
+ok, so with just one context, Env is List Val and we're getting Tm back from type checking.
+
+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
+
+public export
+record MetaContext where
+  constructor MC
+  metas : List MetaEntry
+  next : Nat
+
+
+public export
+data Def = Axiom | TCon (List String) | DCon Nat | Fn Tm
+
+Show Def where
+  show Axiom = "axiom"
+  show (TCon strs) = "TCon \{show strs}"
+  show (DCon k) = "DCon \{show k}"
+  show (Fn t) = "Fn \{show t}"
+
+||| entry in the top level context
+public export
+record TopEntry where
+  constructor MkEntry
+  name : String
+  type : Tm
+  def : Def
+
+-- FIXME snoc
+
+export
+Show TopEntry where
+  show (MkEntry name type def) = "\{name} : \{show type} := \{show def}"
+
+||| Top level context.
+||| Most of the reason this is separate is to have a different type
+||| `Def` for the entries.
+|||
+||| The price is that we have names in addition to levels. Do we want to
+||| expand these during normalization?
+public export
+record TopContext where
+  constructor MkTop
+  -- We'll add a map later?
+  defs : List TopEntry
+  metas : IORef MetaContext
+  -- metas : TODO
+
+-- we'll use this for typechecking, but need to keep a TopContext around too.
+public export
+record Context where
+  constructor MkCtx
+  lvl : Nat
+  -- shall we use lvl as an index?
+  env : Env                  -- Values in scope
+  types : Vect lvl (String, Val) -- types and names in scope
+  -- so we'll try "bds" determines length of local context
+  bds  : List BD          -- bound or defined
+  pos : SourcePos            -- the last SourcePos that we saw
+  
+  -- We only need this here if we don't pass TopContext
+  -- top : TopContext
+  metas : IORef MetaContext
+
+
+public export
+M : Type -> Type
+M = (StateT TopContext (EitherT Impl.Error IO))
+
+-- we need more of topcontext later - Maybe switch it up so we're not passing
+-- around top
+export
+mkCtx : IORef MetaContext -> Context
+mkCtx metas = MkCtx 0 [] [] [] (0,0) metas

src/Main.idr

@@ -14,6 +14,7 @@ import Lib.Prettier
 import Lib.Token
 import Lib.Tokenizer
 import Lib.TopContext
+import Lib.Types
 import Lib.TT
 import Syntax
 import Syntax
@@ -33,9 +34,6 @@ I still want to stay in MonadError outside this file though.
 
 -}
 
-M : Type -> Type
-M = (StateT TopContext (EitherT Impl.Error IO))
-
 
 dumpContext : TopContext -> M ()
 dumpContext top = do
@@ -51,7 +49,7 @@ processDecl : Decl -> M ()
 processDecl (TypeSig nm tm) = do
   top <- get
   putStrLn "TypeSig \{nm} \{show tm}"
-  ty <- check top (mkCtx top.metas) tm VU
+  ty <- check (mkCtx top.metas) tm VU
   putStrLn "got \{show ty}"
   modify $ claim nm ty
 
@@ -69,17 +67,34 @@ processDecl (Def nm raw) = do
   let (MkEntry name ty Axiom) := entry
     | _ => throwError $ E pos "\{nm} already defined"
   putStrLn "check \{nm} = \{show raw} at \{show $ ty}"
-  let vty = eval empty CBN ty
+  vty <- eval empty CBN ty
-  tm <- check ctx (mkCtx ctx.metas) raw vty
+  tm <- check (mkCtx ctx.metas) raw vty
   putStrLn "Ok \{show tm}"
   put (addDef ctx nm tm ty)
 
+processDecl (DCheck tm ty) = do
+  
+  top <- get
+  putStrLn "check \{show tm} at \{show ty}"
+  ty' <- check (mkCtx top.metas) tm VU
+  putStrLn "got type \{show ty'}"
+  vty <- eval [] CBN ty'
+  res <- check (mkCtx top.metas) ty vty
+  putStrLn "got \{show res}"
+  norm <- nf [] res
+  putStrLn "norm \{show norm}"
+  -- top <- get
+  -- ctx <- mkCtx top.metas
+  -- I need a type to check against 
+  -- norm <- nf [] x
+  putStrLn "NF "
+
 processDecl (DImport str) = throwError $ E (0,0) "import not implemented"
 
 processDecl (Data nm ty cons) = do
   -- It seems like the FC for the errors are not here?
   ctx <- get
-  tyty <- check ctx (mkCtx ctx.metas) ty VU
+  tyty <- check (mkCtx ctx.metas) ty VU
   -- TODO check tm is VU or Pi ending in VU
   -- Maybe a pi -> binders function
   -- TODO we're putting in axioms, we need constructors
@@ -91,7 +106,7 @@ processDecl (Data nm ty cons) = do
       (TypeSig nm' tm) => do
           ctx <- get
           -- TODO check pi type ending in full tyty application
-          dty <- check ctx (mkCtx ctx.metas) tm VU
+          dty <- check (mkCtx ctx.metas) tm VU
           modify $ claim nm' dty
       _ => throwError $ E (0,0) "expected TypeSig"
   

src/Syntax.idr

@@ -4,7 +4,7 @@ import Data.String
 import Data.Maybe
 import Lib.Parser.Impl
 import Lib.Prettier
-import Lib.TT
+import Lib.Types
 
 public export
 data Raw : Type where
@@ -58,6 +58,7 @@ data Decl
   = TypeSig Name Raw
   | Def Name Raw
   | DImport Name
+  | DCheck Raw Raw
   | Data Name Raw (List Decl)
 
 public export
@@ -94,6 +95,7 @@ Show Decl where
   show (Def str x) = foo ["Def", show str, show x]
   show (Data str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DImport str) = foo ["DImport", show str]
+  show (DCheck x y) = foo ["DCheck", show x, show y]
 
 export covering
 Show Module where
@@ -181,3 +183,4 @@ Pretty Module where
         doDecl (DImport nm) = text "import" <+> text nm ++ line
         -- 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