From 46ddbc1f91713db28b34789a45dc83c088bf1ae6 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 6 Jul 2024 14:23:41 -0400
Subject: [PATCH] Preliminary work on data and holes

---
 Makefile                                  |   2 +-
 README.md                                 |  21 +++-
 newt-vscode/package.json                  |  37 ++++--
 newt-vscode/syntaxes/newt.tmLanguage.json |  44 ++-----
 newt.ipkg                                 |   2 +-
 newt/data.newt                            |  14 +++
 {eg => newt}/eq.newt                      |   0
 {eg => newt}/ex.newt                      |   0
 {eg => newt}/zoo2.newt                    |   1 +
 newt/zoo3.newt                            |   7 ++
 src/Lib/Check.idr                         |  35 +++++-
 src/Lib/Parser.idr                        |  10 +-
 src/Lib/Parser/Impl.idr                   |   4 +
 src/Lib/TT.idr                            | 144 ++++++++++++++++++----
 src/Lib/TopContext.idr                    |  49 ++------
 src/Main.idr                              |  72 ++++++++---
 src/Syntax.idr                            |  38 +++---
 17 files changed, 311 insertions(+), 169 deletions(-)
 create mode 100644 newt/data.newt
 rename {eg => newt}/eq.newt (100%)
 rename {eg => newt}/ex.newt (100%)
 rename {eg => newt}/zoo2.newt (97%)
 create mode 100644 newt/zoo3.newt

diff --git a/Makefile b/Makefile
index 55ffbe5..6250b0e 100644
--- a/Makefile
+++ b/Makefile
@@ -6,4 +6,4 @@ build/exec/newt: ${SRCS}
 	idris2 --build newt.ipkg
 
 test: build/exec/newt
-	build/exec/newt
+	build/exec/newt newt/*.newt
diff --git a/README.md b/README.md
index 9267efa..3d7a9a4 100644
--- a/README.md
+++ b/README.md
@@ -12,6 +12,15 @@ 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.
+
+We extend the context and then drop it, so we need soemthing mutable.
+
+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...
+
+I'd kinda like to see array run in js...
+
+Idris does a common array for metas and defs. 
 
 
 
@@ -20,14 +29,15 @@ Parser:
 - [x] def
 - [x] simple decl
 - [x] List not in scope
-- [ ] vscode support for .newt
+- [x] vscode support for .newt
 - [ ] Should I switch this back over to the App monad?
-- [ ] Error object like pi-forall
+- [x] Error object like pi-forall
 - [ ] Get implicits working
 - [x] Replace on define
 - [x] more sugar on lambdas
 - [ ] tests for parsing and pretty printing
 - [ ] inductive types
+  - [ ] read data definitions 1/2 done
 - [x] read files
 - [x] process a file
 - [x] figure out context representation - Global context?
@@ -43,5 +53,8 @@ Forward:
 - [ ] Switch to query-based?
 - [ ] LSP?
 - [ ] white box testing
-- 
-f
+
+----
+
+pi-forall sticks equality into scope as something like let. Not sure if this is compatible with deBruijn.  Possibly if we have everything at elab time?  But if `x = y` then previous stuff has a different `x`?
+
diff --git a/newt-vscode/package.json b/newt-vscode/package.json
index 2f2ce72..8f9bc75 100644
--- a/newt-vscode/package.json
+++ b/newt-vscode/package.json
@@ -1,9 +1,14 @@
 {
   "name": "newt-vscode",
+  "publisher": "dunhamsteve",
   "displayName": "newt-vscode",
   "description": "newt language support",
   "version": "0.0.1",
   "license": "MIT",
+  "repository": {
+    "type": "git",
+    "url": "https://github.com/dunhamsteve/newt"
+  },
   "engines": {
     "vscode": "^1.91.0"
   },
@@ -11,27 +16,35 @@
     "Programming Languages"
   ],
   "activationEvents": [
+    "onLanguage:newt"
   ],
   "main": "./dist/extension.js",
   "contributes": {
-    "languages": [{
-      "id": "newt",
-      "aliases": ["newt", "newt"],
-      "extensions": ["newt"],
-      "configuration": "./language-configuration.json"
-    }],
-    "grammars": [{
-      "language": "newt",
-      "scopeName": "source.newt",
-      "path": "./syntaxes/newt.tmLanguage.json"
-    }],
+    "languages": [
+      {
+        "id": "newt",
+        "aliases": [
+          "newt"
+        ],
+        "extensions": [
+          "newt"
+        ],
+        "configuration": "./language-configuration.json"
+      }
+    ],
+    "grammars": [
+      {
+        "language": "newt",
+        "scopeName": "source.newt",
+        "path": "./syntaxes/newt.tmLanguage.json"
+      }
+    ],
     "commands": [
       {
         "command": "newt-vscode.check",
         "title": "Check newt file"
       }
     ]
-
   },
   "scripts": {
     "vscode:prepublish": "npm run package",
diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json
index 19faf7b..750cc08 100644
--- a/newt-vscode/syntaxes/newt.tmLanguage.json
+++ b/newt-vscode/syntaxes/newt.tmLanguage.json
@@ -3,46 +3,20 @@
   "name": "newt",
   "scopeName": "source.newt",
   "patterns": [
-	{
-		"name": "comment.block.newt",
-		"begin": "/-",
-		"end": "`-/",
-		"contentName": "comment.block.newt"
-	},
-	{
+    {
+      "name": "comment.block.newt",
+      "begin": "/-",
+      "end": "-/",
+      "contentName": "comment.block.newt"
+    },
+    {
       "name": "comment.line.newt",
       "begin": "--",
       "end": "\\n"
-  },
-	{
-      "name": "variable.other.constant",
-      "match": "([\\w]+)\\."
-    },
-    {
-      "name": "entity.name.variable",
-      "match": "\\.([\\w]+)"
-    },
-	{
-		"name": "punctuation",
-		"match": ":|=>|\\"
-	},
-    {
-      "name": "keyword.other.operator.newt",
-      "match": "[\\p{Math}:!#$%&*+.,/<=>?@\\^|-]+"
-    },
-
-    {
-      "name": "keyword.command.newt",
-      "match": "\\b(module)\\b"
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data)\\b"
-    },
-    // {
-    //   "name": "variable.other.constant.newt",
-    //   "match": "\\b(Type|Id|refl|sym|Gel|ungel)\\b",
-	  // "comment": "These are in the emacs mode, but some are user defined"
-    // }
+      "match": "\\b(data|where|case|of|let|in|U|module)\\b"
+    }
   ]
 }
diff --git a/newt.ipkg b/newt.ipkg
index 3acd574..7fc9326 100644
--- a/newt.ipkg
+++ b/newt.ipkg
@@ -13,7 +13,7 @@ authors = "Steve Dunham"
 -- langversion
 
 -- packages to add to search path
-depends = contrib, base, elab-util
+depends = contrib, base
 
 -- modules to install
 -- modules =
diff --git a/newt/data.newt b/newt/data.newt
new file mode 100644
index 0000000..8cd2802
--- /dev/null
+++ b/newt/data.newt
@@ -0,0 +1,14 @@
+module Data
+
+-- The code to handle this is full of TODO
+-- stuff is not checked and it's not read as data, just
+-- type signatures.
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+-- My initial version of this needed unbound implicits
+data Maybe : U -> U where
+  Nothing : {a : U} -> Maybe a
+  Just : {a : U} -> a -> Maybe a
diff --git a/eg/eq.newt b/newt/eq.newt
similarity index 100%
rename from eg/eq.newt
rename to newt/eq.newt
diff --git a/eg/ex.newt b/newt/ex.newt
similarity index 100%
rename from eg/ex.newt
rename to newt/ex.newt
diff --git a/eg/zoo2.newt b/newt/zoo2.newt
similarity index 97%
rename from eg/zoo2.newt
rename to newt/zoo2.newt
index 0e82569..47dfff2 100644
--- a/eg/zoo2.newt
+++ b/newt/zoo2.newt
@@ -29,3 +29,4 @@ thousand : Nat
 thousand = mul ten hundred
 
 -- and then nf / eval of hundred
+-- #nf hundred
diff --git a/newt/zoo3.newt b/newt/zoo3.newt
new file mode 100644
index 0000000..e19ffdd
--- /dev/null
+++ b/newt/zoo3.newt
@@ -0,0 +1,7 @@
+module Zoo3
+
+id : (A : _) -> A -> A
+id = \ A x => x
+
+List : U -> U
+List = \ A => (L : _) -> (A -> L -> L) -> L -> L
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 43f369e..81a9f94 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -3,14 +3,30 @@ module Lib.Check
 import Control.Monad.Error.Interface
 import Control.Monad.Identity
 import Lib.Parser.Impl
+import Lib.Prettier
 import Data.Vect
 import Data.String
 import Lib.TT
 import Lib.TopContext
 import Syntax
 
--- cribbed this, it avoids MonadError String m => everywhere
-parameters {0 m : Type -> Type} {auto _ : MonadError Error m} (top : TopContext)
+
+
+
+-- IORef for metas needs IO
+parameters {0 m : Type -> Type} {auto _ : HasIO m} {auto _ : MonadError Error m} (top : TopContext)
+
+  -- unify : Nat -> Val -> Val -> m ()
+  -- 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
+
+
   export
   infer : Context -> Raw -> m (Tm, Val)
 
@@ -20,7 +36,7 @@ parameters {0 m : Type -> Type} {auto _ : MonadError Error m} (top : TopContext)
   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)
                       pure $ Lam nm icit tm'
@@ -32,8 +48,10 @@ parameters {0 m : Type -> Type} {auto _ : MonadError Error m} (top : TopContext)
                     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
+    -- unify ctx.lvl ty' ty
     if quote 0 ty /= quote 0 ty' then
-        error [DS "type mismatch"]
+        error [DS "type mismatch got", DD (quote 0 ty'), DS "expected", DD (quote 0 ty)]
       else pure tm'
 
   infer ctx (RVar nm) = go 0 ctx.types
@@ -70,8 +88,13 @@ parameters {0 m : Type -> Type} {auto _ : MonadError Error m} (top : TopContext)
     pure (tm, vty)
 
   infer ctx (RLam str icit tm) = error [DS "can't infer lambda"]
-
-  infer ctx _ = error [DS "TODO"]
+  infer ctx RHole = do
+    ty <- freshMeta ctx
+    let vty = eval ctx.env CBN ty
+    tm <- freshMeta ctx
+    pure (tm, vty)
+    
+  infer ctx tm = error [DS "Implement infer \{show tm}"]
 
   -- I don't have types for these yet...
   -- infer ctx (RLit (LString str)) = ?rhs_10
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 10f7265..1808143 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -237,7 +237,8 @@ parseData = do
   keyword ":"
   ty <- typeExpr
   keyword "where"
-  decls <- startBlock $ someSame $ parseSig
+  commit
+  decls <- startBlock $ manySame $ parseSig
   -- TODO - turn decls into something more useful
   pure $ Data name ty decls
 
@@ -252,9 +253,8 @@ parseMod = do
   name <- ident
   -- probably should be manySame, and we want to start with col -1
   -- if we enforce blocks indent more than parent
-  decls <- startBlock $ someSame $ parseDecl
-  pure $ MkModule name [] decls
-
+  decls <- startBlock $ manySame $ parseDecl
+  pure $ MkModule name decls
 
 public export
 data ReplCmd =
@@ -268,4 +268,4 @@ data ReplCmd =
 export parseRepl : Parser ReplCmd
 parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr
   <|> Check <$ keyword "#check" <*> typeExpr
-  
+  
\ No newline at end of file
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index 8b93225..a98bb53 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -179,6 +179,10 @@ export
 someSame : Parser a -> Parser (List a)
 someSame pa = some $ sameLevel pa
 
+export
+manySame : Parser a -> Parser (List a)
+manySame pa = many $ sameLevel pa
+
 ||| requires a token to be indented?
 export
 indented : Parser a -> Parser a
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 506c5bc..239974d 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -7,8 +7,11 @@ module Lib.TT
 -- For SourcePos
 import Lib.Parser.Impl
 import Lib.Prettier
+import Lib.Metas
 
 import Control.Monad.Error.Interface
+
+import Data.IORef
 import Data.Fin
 import Data.List
 import Data.Vect
@@ -23,11 +26,18 @@ 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
@@ -43,6 +53,7 @@ Show Tm where
   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}"
@@ -69,6 +80,18 @@ Eq (Tm) where
   (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
@@ -91,9 +114,12 @@ data Closure : Type
 public export
 data Val : Type where
   -- This will be local / flex with spine.
-  VVar : Nat -> Val
-  VRef : String -> Maybe Tm -> Val
-  VApp : Val ->  Lazy (Val) -> Val
+  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
@@ -120,7 +146,10 @@ infixl 8 $$
 export
 vapp : Val -> Val -> Val
 vapp (VLam _ icit t) u = t $$ u
-vapp t u = VApp 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
@@ -129,10 +158,11 @@ bind v env = v :: env
 -- 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 Nothing
+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
@@ -141,14 +171,19 @@ eval env mode (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index
 
 export
 quote : (lvl : Nat) -> Val -> Tm
-quote l (VVar k) = Bnd ((l `minus` k) `minus` 1) -- level to index
-quote l (VApp t u) = App (quote l t) (quote l u)
-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 tm) = Ref n tm
 
--- how are we using this?  Can we assume completely closed?
+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
@@ -186,7 +221,53 @@ Can I get val back? Do we need to quote? What happens if we don't?
 
 -}
 
-data BD = Bound | Defined
+
+public export
+data MetaEntry = Unsolved Nat (List BD) | Solved Nat Tm (List BD)
+
+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
@@ -198,12 +279,30 @@ record Context where
   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
-empty : Context
-empty = MkCtx 0 [] [] [] (0,0)
+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
+
+-- 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
@@ -211,8 +310,6 @@ Show Context where
 
 -- TODO Pretty Context
 
-
-
 -- idea cribbed from pi-forall
 public export
 data ErrorSeg : Type where
@@ -231,14 +328,15 @@ error xs = throwError $ E ctx.pos (render 80 $ spread $ map toDoc xs)
 ||| add a binding to environment
 export
 extend : Context -> String -> Val -> Context
-extend (MkCtx lvl env types bds pos) name ty =
-    MkCtx (S lvl) (VVar lvl :: env) ((name, ty) :: types) (Bound :: bds) pos
-
+extend ctx name ty =
+    { lvl $= S, env $= (VVar ctx.lvl [] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
+    
 -- I guess we define things as values?
 export
 define : Context -> String -> Val -> Val -> Context
-define (MkCtx lvl env types bds pos) name val ty =
-  MkCtx (S lvl) (val :: env) ((name, ty) :: types) (Defined :: bds) pos
+define ctx name val ty =
+  { lvl $= S, env $= (val ::), types $= ((name,ty) ::), bds $= (Defined ::) } ctx
+
 
 -- not used
 lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} ->
diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr
index 604e97f..4202e2b 100644
--- a/src/Lib/TopContext.idr
+++ b/src/Lib/TopContext.idr
@@ -2,43 +2,10 @@ module Lib.TopContext
 
 import Data.String
 import Lib.TT
+import Data.IORef
 
-
-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
-
+-- I want unique ids, to be able to lookup, update, and a Ref so
+-- I don't need good Context discipline. (I seem to have made mistakes already.)
 
 export
 lookup : String -> TopContext -> Maybe TopEntry
@@ -51,15 +18,15 @@ lookup nm top = go top.defs
 -- Maybe pretty print?
 export
 Show TopContext where
-  show (MkTop defs) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]"
+  show (MkTop defs metas) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]"
 
 public export
-empty : TopContext
-empty = MkTop []
+empty : HasIO m => m TopContext
+empty = pure $ MkTop [] !(newIORef (MC [] 0))
 
 public export
-claim : TopContext -> String -> Tm -> TopContext
-claim tc name ty = { defs $= (MkEntry name ty Axiom ::) } tc
+claim : String -> Tm -> TopContext -> TopContext
+claim name ty = { defs $= (MkEntry name ty Axiom ::) }
 
 -- TODO update existing, throw, etc.
 
diff --git a/src/Main.idr b/src/Main.idr
index 58ca7b7..e435314 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -1,20 +1,20 @@
 module Main
 
 -- import Control.App
+import Control.Monad.Error.Either
+import Control.Monad.Error.Interface
+import Control.Monad.State
+import Data.List
 import Data.String
 import Data.Vect
-import Data.List
-import Control.Monad.Error.Interface
-import Control.Monad.Error.Either
-import Control.Monad.State
 import Lib.Check
 import Lib.Parser
 import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Token
 import Lib.Tokenizer
-import Lib.TT
 import Lib.TopContext
+import Lib.TT
 import Syntax
 import Syntax
 import System
@@ -25,13 +25,14 @@ import System.File
 
 Main2.idr has an older App attempt without the code below.
 
-App was not compatible with javascript, but I have a remedy for
-that now. 
+It has a repl, so we might want to re-integrate that code. And it uses
+App, but we have a way to make that work on javascript.
+
+I still want to stay in MonadError outside this file though.
+
 
 -}
 
--- TODO We're shadowing Control.App.Error do we want that?
-
 M : Type -> Type
 M = (StateT TopContext (EitherT Impl.Error IO))
 
@@ -48,29 +49,58 @@ dumpContext top = do
 
 processDecl : Decl -> M ()
 processDecl (TypeSig nm tm) = do
-  ctx <- get
+  top <- get
   putStrLn "TypeSig \{nm} \{show tm}"
-  ty <- check ctx empty tm VU
+  ty <- check top (mkCtx top.metas) tm VU
   putStrLn "got \{show ty}"
-  
-  put $ claim ctx nm ty
+  modify $ claim nm ty
 
+-- FIXME - this should be in another file
 processDecl (Def nm raw) = do
+  let m : MonadError Error M := %search
   putStrLn "def \{show nm}"
   ctx <- get
+  let pos = case raw of
+        RSrcPos pos _ => pos
+        _ => (0,0)
+
   let Just entry = lookup nm ctx
-    | Nothing => throwError $ E (0,0) "skip def \{nm} without Decl"
+    | Nothing => throwError $ E pos "skip def \{nm} without Decl"
   let (MkEntry name ty Axiom) := entry
-    -- FIXME error
-    | _ => throwError $ E (0,0) "\{nm} already defined"
+    | _ => throwError $ E pos "\{nm} already defined"
   putStrLn "check \{nm} = \{show raw} at \{show $ ty}"
   let vty = eval empty CBN ty
-  Right tm <- pure $ the (Either Impl.Error Tm) (check ctx empty raw vty)
-    | Left err => throwError err
+  tm <- check ctx (mkCtx ctx.metas) raw vty
   putStrLn "Ok \{show tm}"
   put (addDef ctx nm tm ty)
+
+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
+  -- TODO check tm is VU or Pi ending in VU
+  -- Maybe a pi -> binders function
+  -- TODO we're putting in axioms, we need constructors
+  -- for each constructor, check and add
+  modify $ claim nm tyty
+  ctx <- get
+  for_ cons $ \x => case x of
+      -- expecting tm to be a Pi type
+      (TypeSig nm' tm) => do
+          ctx <- get
+          -- TODO check pi type ending in full tyty application
+          dty <- check ctx (mkCtx ctx.metas) tm VU
+          modify $ claim nm' dty
+      _ => throwError $ E (0,0) "expected TypeSig"
   
-processDecl decl = putStrLn "skip \{show decl}"
+  pure ()
+  where
+    checkDeclType : Tm -> M ()
+    checkDeclType U = pure ()
+    checkDeclType (Pi str icit t u) = checkDeclType u
+    checkDeclType _ = throwError $ E (0,0) "data type doesn't return U"
 
 processFile : String -> M ()
 processFile fn = do
@@ -100,6 +130,8 @@ main' = do
 
 main : IO ()
 main = do
-  Right _  <- runEitherT $ runStateT empty $ main'
+  -- we'll need to reset for each file, etc.
+  ctx <- empty
+  Right _  <- runEitherT $ runStateT ctx $ main'
     | Left (E (c, r) str) => putStrLn "Error: \{show c} \{show r} \{show str}"
   putStrLn "done"
diff --git a/src/Syntax.idr b/src/Syntax.idr
index fb4988d..1ab2d60 100644
--- a/src/Syntax.idr
+++ b/src/Syntax.idr
@@ -27,22 +27,20 @@ data Pattern
 public export
 data CaseAlt = MkAlt Pattern Raw
 
--- TODO redo this with names for documentation
-
-data Raw
-  = RVar Name
-  | RLam String Icit Raw
-  | RApp Raw Raw Icit
-  | RU
-  | RPi (Maybe Name) Icit Raw Raw
-  | RLet Name Raw Raw Raw
-  | RSrcPos SourcePos Raw
-
-  | RAnn Raw Raw
-  | RLit Literal
-  | RCase Raw (List CaseAlt)
-  | RHole
-  | RParseError String
+data Raw : Type where
+  RVar : (nm : Name) -> Raw
+  RLam : (nm : String) -> (icit : Icit) -> (ty : Raw) -> Raw
+  RApp : (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw
+  RU   : Raw
+  RPi  : (nm : Maybe Name) -> (icit : Icit) -> (ty : Raw) -> (sc : Raw) -> Raw
+  RLet : (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
+  -- REVIEW do we want positions on terms?
+  RSrcPos : SourcePos -> Raw -> Raw
+  RAnn  : (tm : Raw) -> (ty : Raw) -> Raw
+  RLit : Literal -> Raw
+  RCase : (scrut : Raw) -> (alts : List CaseAlt) -> Raw
+  RHole : Raw
+  RParseError : String -> Raw
 
 %name Raw tm
 
@@ -66,7 +64,6 @@ public export
 record Module where
   constructor MkModule
   name : Name
-  imports : List Name
   decls : List Decl
 
 foo : List String -> String
@@ -98,10 +95,9 @@ Show Decl where
   show (Data str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DImport str) = foo ["DImport", show str]
 
-
 export covering
 Show Module where
-  show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
+  show (MkModule name decls) = foo ["MkModule", show name, show decls]
 
 Show RigCount where
   show Rig0 = "Rig0"
@@ -172,11 +168,11 @@ Pretty Raw where
     asDoc p (RLit (LBool x)) = text $ show x
     asDoc p (RCase x xs) = text "TODO - RCase"
     asDoc p RHole = text "_"
-    asDoc p (RParseError str) = text "PraseError \{str}"
+    asDoc p (RParseError str) = text "ParseError \{str}"
     
 export 
 Pretty Module where
-  pretty (MkModule name imports decls) =
+  pretty (MkModule name decls) =
     text "module" <+> text name </> stack (map doDecl decls)
       where
         doDecl : Decl -> Doc