move idris version to orig and newt version to src.

Development is being done on the newt version now.

orig/Lib/Common.idr

@@ -0,0 +1,154 @@
+module Lib.Common
+
+import Data.String
+import Data.Nat
+import Data.Maybe
+import public Data.SortedMap
+
+-- l is environment size, this works for both lvl2ix and ix2lvl
+public export
+lvl2ix : Nat -> Nat -> Nat
+lvl2ix l k = minus (minus l k) 1
+
+hexChars : List Char
+hexChars = unpack "0123456789ABCDEF"
+
+-- export
+hexDigit : Nat -> Char
+hexDigit v = fromMaybe ' ' (getAt (mod v 16) hexChars)
+
+export
+toHex : Nat -> List Char
+toHex 0 = []
+toHex v = snoc (toHex (div v 16)) (hexDigit v)
+
+export
+quoteString : String -> String
+quoteString str = pack $ encode (unpack str) [< '"']
+  where
+    encode : List Char -> SnocList Char -> List Char
+    encode [] acc = acc <>> ['"']
+    encode ('"' :: cs) acc = encode cs (acc :< '\\' :< '"')
+    encode ('\n' :: cs) acc = encode cs (acc :< '\\' :< 'n')
+    encode ('\\' :: cs) acc = encode cs (acc :< '\\' :< '\\')
+    encode (c :: cs) acc =
+      let v : Nat = cast c in
+      if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
+      else encode cs (acc :< c)
+
+public export
+data Json : Type where
+  JsonObj : List (String, Json) -> Json
+  JsonStr : String -> Json
+  JsonBool : Bool -> Json
+  JsonInt : Int -> Json
+  JsonArray : List Json -> Json
+
+export
+renderJson : Json -> String
+renderJson (JsonObj xs) = "{" ++ joinBy "," (map renderPair xs) ++ "}"
+  where
+    renderPair : (String,Json) -> String
+    renderPair (k,v) = quoteString k ++ ":" ++ renderJson v
+renderJson (JsonStr str) = quoteString str
+renderJson (JsonBool x) = ifThenElse x "true" "false"
+renderJson (JsonInt i) = cast i
+renderJson (JsonArray xs) = "[" ++ joinBy "," (map renderJson xs) ++ "]"
+
+public export
+interface ToJSON a where
+  toJson : a -> Json
+
+export
+ToJSON String where
+  toJson = JsonStr
+
+export
+ToJSON Int where
+  toJson = JsonInt
+
+public export
+record FC where
+  constructor MkFC
+  file : String
+  start : (Int,Int)
+
+export
+ToJSON FC where
+  toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil)
+
+export
+fcLine : FC -> Int
+fcLine (MkFC file (l, c)) = l
+
+export
+fcCol : FC -> Int
+fcCol (MkFC file (l, c)) = c
+
+public export
+interface HasFC a where
+  getFC : a -> FC
+
+%name FC fc
+
+export
+emptyFC : FC
+emptyFC = MkFC "" (0,0)
+
+-- Error of a parse
+public export
+data Error
+  = E FC String
+  | Postpone FC Nat String
+%name Error err
+
+export
+Show FC where
+  show fc = "\{fc.file}:\{show fc.start}"
+
+public export
+showError : String -> Error -> String
+showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src)
+  where
+    go : Int -> List String -> String
+    go l [] = ""
+    go l (x :: xs) =
+      if l == fcLine fc then
+        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
+      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      else go (l + 1) xs
+showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
+  where
+    go : Int -> List String -> String
+    go l [] = ""
+    go l (x :: xs) =
+      if l == fcLine fc then
+        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
+      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      else go (l + 1) xs
+
+public export
+data Fixity = InfixL | InfixR | Infix
+
+export
+Show Fixity where
+  show InfixL = "infixl"
+  show InfixR = "infixr"
+  show Infix = "infix"
+
+
+public export
+record OpDef where
+  constructor MkOp
+  opname : String
+  prec : Int
+  fix : Fixity
+  isPrefix : Bool
+  ||| rule is everything after the first part of the operator, splitting on `_`
+  ||| a normal infix operator will have a trailing `""` which will match to
+  ||| prec / prec - 1
+  rule : List String
+
+public export
+Operators : Type
+Operators = SortedMap String OpDef

orig/Lib/Compile.idr

@@ -0,0 +1,349 @@
+-- TODO Audit how much "outside" stuff could pile up in the continuation.
+module Lib.Compile
+
+import Lib.Types
+import Lib.Prettier
+import Lib.CompileExp
+import Lib.TopContext
+import Data.String
+import Data.Maybe
+import Data.Nat
+
+data Kind = Plain | Return | Assign String
+
+data JSStmt : Kind -> Type
+data JSExp : Type
+
+data JAlt : Type where
+  JConAlt : String -> JSStmt e -> JAlt
+  JDefAlt : JSStmt e -> JAlt
+  JLitAlt : JSExp -> JSStmt e -> JAlt
+
+data JSExp : Type where
+  LitArray : List JSExp -> JSExp
+  LitObject : List (String, JSExp) -> JSExp
+  LitString : String -> JSExp
+  LitInt : Int -> JSExp
+  Apply : JSExp -> List JSExp -> JSExp
+  Var : String -> JSExp
+  JLam : List String -> JSStmt Return -> JSExp
+  JUndefined : JSExp
+  Index : JSExp -> JSExp -> JSExp
+  Dot : JSExp -> String -> JSExp
+
+data JSStmt : Kind -> Type where
+  -- Maybe make this a snoc...
+  JSnoc : JSStmt Plain -> JSStmt a -> JSStmt a
+  JPlain : JSExp -> JSStmt Plain
+  JConst : (nm : String) -> JSExp -> JSStmt Plain
+  JReturn : JSExp -> JSStmt Return
+  JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain  -- need somebody to assign
+  JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm)
+  -- TODO - switch to Nat tags
+  -- FIXME add e to JAlt (or just drop it?)
+  JCase : JSExp -> List JAlt -> JSStmt a
+  -- throw can't be used
+  JError : String -> JSStmt a
+
+Cont e = JSExp -> JSStmt e
+
+||| JSEnv contains `Var` for binders or `Dot` for destructured data. It
+||| used to translate binders
+record JSEnv where
+  constructor MkEnv
+  env : List JSExp
+  depth : Nat
+
+push : JSEnv -> JSExp -> JSEnv
+push env exp = { env $= (exp ::) } env
+
+empty : JSEnv
+empty = MkEnv [] Z
+
+litToJS : Literal -> JSExp
+litToJS (LString str) = LitString str
+litToJS (LChar c) = LitString $ cast c
+litToJS (LInt i) = LitInt i
+
+-- Stuff nm.h1, nm.h2, ... into environment
+-- TODO consider JSExp instead of nm, so we can have $foo.h1 instead of assigning a sc.
+mkEnv : String -> Nat -> JSEnv -> List String -> JSEnv
+mkEnv nm k env [] = env
+mkEnv nm k env (x :: xs) = mkEnv nm (S k) (push env (Dot (Var nm) "h\{show k}")) xs
+
+envNames : Env -> List String
+
+||| given a name, find a similar one that doesn't shadow in Env
+freshName : String -> JSEnv -> String
+freshName nm env = if free env.env nm then nm else go nm 1
+  where
+    free : List JSExp -> String -> Bool
+    free [] nm = True
+    free (Var n :: xs) nm = if n == nm then False else free xs nm
+    free (_ :: xs) nm = free xs nm
+
+    go : String -> Nat -> String
+    go nm k = let nm' = "\{nm}\{show k}" in if free env.env nm' then nm' else go nm (S k)
+
+freshName' : String -> JSEnv -> (String, JSEnv)
+freshName' nm env =
+  let nm' = freshName nm env -- "\{nm}$\{show $ length env}"
+      env' = push env (Var nm')
+  in (nm', env')
+
+freshNames : List String -> JSEnv -> (List String, JSEnv)
+freshNames nms env = go nms env [<]
+  where
+    go : List Name -> JSEnv -> SnocList Name -> (List String, JSEnv)
+    go Nil env acc = (acc <>> Nil, env)
+    go (n :: ns) env acc =
+      let (n', env') = freshName' n env
+      in go ns env' (acc :< n')
+
+-- This is inspired by A-normalization, look into the continuation monad
+-- There is an index on JSStmt, adopted from Stefan Hoeck's code.
+--
+-- Here we turn a Term into a statement (which may be a sequence of statements), there
+-- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns
+-- a JSStmt, wrapping recursive calls in JSnoc if necessary.
+termToJS : JSEnv -> CExp -> Cont e -> JSStmt e
+termToJS env (CBnd k) f = case getAt k env.env of
+  (Just e) => f e
+  Nothing => ?bad_bounds
+termToJS env CErased f = f JUndefined
+termToJS env (CLam nm t) f =
+  let (nm',env') = freshName' nm env -- "\{nm}$\{show $ length env}"
+  in f $ JLam [nm'] (termToJS env' t JReturn)
+termToJS env (CFun nms t) f =
+  let (nms', env') = freshNames nms env
+  in f $ JLam nms' (termToJS env' t JReturn)
+termToJS env (CRef nm) f = f $ Var nm
+termToJS env (CMeta k) f = f $ LitString "META \{show k}"
+termToJS env (CLit lit) f = f (litToJS lit)
+-- if it's a var, just use the original
+termToJS env (CLet nm (CBnd k) u) f = case getAt k env.env of
+  Just e  => termToJS (push env e) u f
+  Nothing => ?bad_bounds2
+termToJS env (CLet nm t u) f =
+  let nm' = freshName nm env
+      env' = push env (Var nm')
+  -- If it's a simple term, use const
+  in case termToJS env t (JAssign nm') of
+    (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
+    t' => JSnoc (JLet nm' t') (termToJS env' u f)
+termToJS env (CLetRec nm t u) f =
+  let nm' = freshName nm env
+      env' = push env (Var nm')
+  -- If it's a simple term, use const
+  in case termToJS env' t (JAssign nm') of
+    (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
+    t' => JSnoc (JLet nm' t') (termToJS env' u f)
+
+termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args [<] f)) --  (f (Apply t' args'))))
+  where
+    etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp
+    etaExpand env Z args tm = Apply tm (args <>> [])
+    etaExpand env (S etas) args tm =
+      let nm' = freshName "eta" env
+          env' = push env (Var nm')
+       in JLam [nm'] $ JReturn $ etaExpand (push env (Var nm')) etas (args :< Var nm') tm
+
+    argsToJS : JSExp -> List CExp -> SnocList JSExp -> (JSExp -> JSStmt e) -> JSStmt e
+    argsToJS tm [] acc k = k (etaExpand env etas acc tm)
+    -- k (acc <>> [])
+    argsToJS tm (x :: xs) acc k = termToJS env x (\ x' => argsToJS tm xs (acc :< x') k)
+
+
+termToJS env (CCase t alts) f =
+  -- need to assign the scrutinee to a variable (unless it is a var already?)
+  -- and add (Bnd -> JSExpr map)
+  -- TODO default case, let's drop the extra field.
+
+  termToJS env t $ \case
+    (Var nm) => maybeCaseStmt env nm alts
+    t' => do
+      -- TODO refactor nm to be a JSExp with Var{} or Dot{}
+      -- FIXME sc$ seemed to shadow something else, lets get this straightened out
+      -- we need freshName names that are not in env (i.e. do not play in debruijn)
+      let nm = "_sc$\{show env.depth}"
+      let env' = { depth $= S } env
+      JSnoc (JConst nm t') (maybeCaseStmt env' nm alts)
+
+  where
+    termToJSAlt : JSEnv -> String -> CAlt -> JAlt
+    termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f)
+    -- intentionally reusing scrutinee name here
+    termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS  (env) u f)
+    termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f)
+
+    maybeCaseStmt : JSEnv -> String -> List CAlt -> JSStmt e
+    -- If there is a single alt, assume it matched
+    maybeCaseStmt env nm [(CConAlt _ args u)] = (termToJS (mkEnv nm 0 env args) u f)
+    maybeCaseStmt env nm alts@(CLitAlt _ _  :: _) =
+        (JCase (Var nm) (map (termToJSAlt env nm) alts))
+    maybeCaseStmt env nm alts =
+          (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts))
+
+jsKeywords : List String
+jsKeywords = [
+  "break", "case", "catch", "continue", "debugger", "default", "delete", "do", "else",
+  "finally", "for", "function", "if", "in", "instanceof", "new", "return", "switch",
+  "this", "throw", "try", "typeof", "var", "void", "while", "with",
+  "class", "const", "enum", "export", "extends", "import", "super",
+  "implements", "interface", "let", "package", "private", "protected", "public",
+  "static", "yield",
+  "null", "true", "false",
+  -- might not be a big issue with namespaces on names now.
+  "String", "Number", "Array", "BigInt"
+]
+
+||| escape identifiers for js
+jsIdent : String -> Doc
+jsIdent id = if elem id jsKeywords then text ("$" ++ id) else text $ pack $ fix (unpack id)
+  where
+    fix : List Char -> List Char
+    fix [] = []
+    fix (x :: xs) =
+      if isAlphaNum x || x == '_' then
+        x :: fix xs
+      -- make qualified names more readable
+      else if x == '.' then '_' :: fix xs
+      else if x == '$' then
+        '$' :: '$' :: fix xs
+      else
+        '$' :: (toHex (cast x)) ++ fix xs
+
+stmtToDoc : JSStmt e -> Doc
+
+
+expToDoc : JSExp -> Doc
+expToDoc (LitArray xs) = ?expToDoc_rhs_0
+expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ text ", " <+/> e) (map entry xs) <+> text "}"
+  where
+    entry : (String, JSExp) -> Doc
+    -- TODO quote if needed
+    entry (nm, exp) = jsIdent nm ++ text ":" <+> expToDoc exp
+
+expToDoc (LitString str) = text $ quoteString str
+expToDoc (LitInt i) = text $ show i
+-- TODO add precedence
+expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")"
+expToDoc (Apply x xs) = expToDoc x ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")"
+expToDoc (Var nm) = jsIdent nm
+expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> text "(" ++ expToDoc exp ++ text ")"
+expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> bracket "{" (stmtToDoc body) "}"
+expToDoc JUndefined = text "null"
+expToDoc (Index obj ix) = expToDoc obj ++ text "[" ++ expToDoc ix ++ text "]"
+expToDoc (Dot obj nm) = expToDoc obj ++ text "." ++ jsIdent nm
+
+caseBody : JSStmt e -> Doc
+caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt)
+-- caseBody {e = Return} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt)
+caseBody {e} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt </> text "break;")
+caseBody stmt = line ++ text "{" ++ nest 2 (line ++ stmtToDoc stmt </> text "break;") </> text "}"
+
+altToDoc : JAlt -> Doc
+altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt
+altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt
+altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ text ":" ++ caseBody stmt
+
+stmtToDoc (JSnoc x y) = stmtToDoc x </> stmtToDoc y
+stmtToDoc (JPlain x) = expToDoc x ++ text ";"
+-- I might not need these split yet.
+stmtToDoc (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" </> stmtToDoc body
+stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";"
+stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";")
+stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";"
+stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");"
+stmtToDoc (JCase sc alts) =
+  text "switch (" ++ expToDoc sc ++ text ")" <+> bracket "{" (stack $ map altToDoc alts) "}"
+
+mkArgs : Nat -> List String -> List String
+mkArgs Z acc = acc
+mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc)
+
+dcon : QName -> Nat -> Doc
+dcon qn@(QN ns nm) Z = stmtToDoc $ JConst (show qn) $ LitObject [("tag", LitString nm)]
+dcon qn@(QN ns nm) arity =
+  let args := mkArgs arity []
+      obj := ("tag", LitString nm) :: map (\x => (x, Var x)) args
+  in stmtToDoc $ JConst (show qn) (JLam args (JReturn (LitObject obj)))
+
+-- use iife to turn stmts into expr
+maybeWrap : JSStmt Return -> JSExp
+maybeWrap (JReturn exp) = exp
+maybeWrap stmt = Apply (JLam [] stmt) []
+
+entryToDoc : TopEntry -> M Doc
+entryToDoc (MkEntry _ name ty (Fn tm)) = do
+  debug "compileFun \{pprint [] tm}"
+  ct <- compileFun tm
+  let exp = maybeWrap $ termToJS empty ct JReturn
+  pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";"
+entryToDoc (MkEntry _ name type Axiom) = pure $ text ""
+entryToDoc (MkEntry _ name type (TCon strs)) = pure $ dcon name (piArity type)
+entryToDoc (MkEntry _ name type (DCon arity str)) = pure $ dcon name arity
+entryToDoc (MkEntry _ name type PrimTCon) = pure $ dcon name (piArity type)
+entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent (show name) <+> text "=" <+> text src
+
+||| This version (call `reverse . snd <$> process "main" ([],[])`) will do dead
+||| code elimination, but the Prelude js primitives are reaching for
+||| stuff like True, False, MkUnit, fs which get eliminated
+process : (List QName, List Doc) -> QName -> M (List QName, List Doc)
+process (done,docs) nm = do
+  let False = nm `elem` done | _ => pure (done,docs)
+  top <- get
+  case TopContext.lookup nm top of
+    Nothing => error emptyFC "\{nm} not in scope"
+    Just entry@(MkEntry _ name ty (PrimFn src uses)) => do
+      (done,docs) <- foldlM assign (nm :: done, docs) uses
+      pure (done, !(entryToDoc entry) :: docs)
+    Just (MkEntry _ name ty (Fn tm)) => do
+                debug "compileFun \{pprint [] tm}"
+                ct <- compileFun tm
+                -- If ct has zero arity and is a compount expression, this fails..
+                let exp = maybeWrap $ termToJS empty ct JReturn
+                let doc = text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";"
+                (done,docs) <- walkTm tm (nm :: done, docs)
+                pure (done, doc :: docs)
+    Just entry => pure (nm :: done, !(entryToDoc entry) :: docs)
+  where
+    assign : (List QName, List Doc) -> String -> M (List QName, List Doc)
+    assign (done, docs) nm = case lookupRaw nm !get of
+      Nothing => pure (done, docs)
+      (Just (MkEntry fc name type def)) => do
+        let tag = QN [] nm
+        let False = tag `elem` done | _ => pure (done,docs)
+        (done,docs) <- process (done, docs) name
+        let doc = text "const" <+> jsIdent nm <+> text "=" <+> jsIdent (show name) ++ text ";"
+        pure (tag :: done, doc :: docs)
+
+    walkTm : Tm -> (List QName, List Doc) -> M (List QName, List Doc)
+    walkAlt : (List QName, List Doc) -> CaseAlt -> M (List QName, List Doc)
+    walkAlt acc (CaseDefault t) = walkTm t acc
+    walkAlt acc (CaseCons name args t) = walkTm t acc
+    walkAlt acc (CaseLit lit t) = walkTm t acc
+
+    walkTm (Ref x nm y) acc = process acc nm
+    walkTm (Lam x str _ _ t) acc = walkTm t acc
+    walkTm (App x t u) acc = walkTm t !(walkTm u acc)
+    walkTm (Pi x str icit y t u) acc = walkTm t !(walkTm u acc)
+    walkTm (Let x str t u) acc = walkTm t !(walkTm u acc)
+    walkTm (LetRec x str _ t u) acc = walkTm t !(walkTm u acc)
+    walkTm (Case x t alts) acc = foldlM walkAlt acc alts
+    walkTm _ acc = pure acc
+
+export
+compile : M (List Doc)
+compile = do
+  top <- get
+  case lookupRaw "main" top of
+    Just (MkEntry fc name type def) => do
+      tmp <- snd <$> process ([],[]) name
+      let exec = stmtToDoc $ JPlain $ Apply (Var $ show name) []
+      pure $ reverse (exec :: tmp)
+    -- If there is no main, compile everything for the benefit of the playground
+    Nothing => do
+      top <- get
+      traverse entryToDoc $ map snd $ SortedMap.toList top.defs
+

orig/Lib/CompileExp.idr

@@ -0,0 +1,159 @@
+||| First pass of compilation
+||| - work out arities and fully apply functions / constructors (currying)
+|||     currying is problemmatic because we need to insert lambdas (η-expand) and
+|||     it breaks all of the de Bruijn indices
+||| - expand metas (this is happening earlier)
+||| - erase stuff (there is another copy that essentially does the same thing)
+||| I could make names unique (e.q. on lambdas), but I might want that to vary per backend?
+module Lib.CompileExp
+
+import Data.List
+
+import Lib.Types -- Name / Tm
+import Lib.TopContext
+import Lib.Prettier
+import Lib.Util
+
+public export
+data CExp : Type
+
+public export
+data CAlt : Type where
+  CConAlt : String -> List String -> CExp -> CAlt
+  -- REVIEW keep var name?
+  CDefAlt : CExp -> CAlt
+  -- literal
+  CLitAlt : Literal -> CExp -> CAlt
+
+data CExp : Type where
+  CBnd : Nat -> CExp
+  CLam : Name -> CExp -> CExp
+  CFun : List Name -> CExp -> CExp
+  -- REVIEW This feels like a hack, but if we put CLam here, the
+  -- deBruijn gets messed up in code gen
+  CApp : CExp -> List CExp -> Nat -> CExp
+  -- TODO make DCon/TCon app separate so we can specialize
+  -- U / Pi are compiled to type constructors
+  CCase : CExp -> List CAlt -> CExp
+  CRef : Name -> CExp
+  CMeta : Nat -> CExp
+  CLit : Literal -> CExp
+  CLet : Name -> CExp -> CExp -> CExp
+  CLetRec : Name -> CExp -> CExp -> CExp
+  CErased : CExp
+
+||| I'm counting Lam in the term for arity.  This matches what I need in
+||| code gen.
+export
+lamArity : Tm -> Nat
+lamArity (Lam _ _ _ _ t) = S (lamArity t)
+lamArity _ = Z
+
+export
+piArity : Tm -> Nat
+piArity (Pi _ _ _ quant _ b) = S (piArity b)
+piArity _ = Z
+
+||| This is how much we want to curry at top level
+||| leading lambda Arity is used for function defs and metas
+||| TODO - figure out how this will work with erasure
+arityForName : FC -> QName -> M Nat
+arityForName fc nm = case lookup nm !get of
+  -- let the magic hole through for now (will generate bad JS)
+  Nothing => error fc "Name \{show nm} not in scope"
+  (Just (MkEntry _ name type Axiom)) => pure 0
+  (Just (MkEntry _ name type (TCon strs))) => pure $ piArity type
+  (Just (MkEntry _ name type (DCon k str))) => pure k
+  (Just (MkEntry _ name type (Fn t))) => pure $ lamArity t
+  (Just (MkEntry _ name type (PrimTCon))) => pure $ piArity type
+  -- Assuming a primitive can't return a function
+  (Just (MkEntry _ name type (PrimFn t uses))) => pure $ piArity type
+
+export
+compileTerm : Tm -> M CExp
+
+-- need to eta out extra args, fill in the rest of the apps
+apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp
+-- out of args, make one up (fix that last arg)
+apply t [] acc (S k) ty = pure $ CApp t (acc <>> []) (S k)
+  -- inserting Clam, index wrong?
+  -- CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty)
+apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) =  apply t xs (acc :< CErased) k b
+apply t (x :: xs) acc (S k) (Pi y str icit Many a b) =  apply t xs (acc :< x) k b
+-- see if there is anything we have to handle here
+apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}. Overapplied function that escaped type checking?"
+-- once we hit zero, we fold the rest
+apply t ts acc 0 ty = go (CApp t (acc <>> []) Z) ts
+  where
+    go : CExp -> List CExp -> M CExp
+    -- drop zero arg call
+    go (CApp t [] Z) args = go t args
+    go t [] = pure t
+    go t (arg :: args) = go (CApp t [arg] 0) args
+
+-- apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
+-- -- out of args, make one up
+-- apply t [] acc (S k) = pure $
+--   CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k)
+-- apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k
+-- apply t ts acc 0 = go (CApp t (acc <>> [])) ts
+--   where
+--     go : CExp -> List CExp -> M CExp
+--     -- drop zero arg call
+--     go (CApp t []) args = go t args
+--     go t [] = pure t
+--     go t (arg :: args) = go (CApp t [arg]) args
+
+compileTerm (Bnd _ k) = pure $ CBnd k
+-- need to eta expand to arity
+compileTerm t@(Ref fc nm _) = do
+  top <- get
+  let Just (MkEntry _ _ type _) = lookup nm top
+          | Nothing => error fc "Undefined name \{nm}"
+  apply (CRef (show nm)) [] [<] !(arityForName fc nm) type
+
+compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
+compileTerm (Lam _ nm _ _ t) = pure $ CLam nm !(compileTerm t)
+compileTerm tm@(App _ _ _) with (funArgs tm)
+  _ | (Meta _ k, args) = do
+        error (getFC tm) "Compiling an unsolved meta \{showTm tm}"
+        info (getFC tm) "Compiling an unsolved meta \{showTm tm}"
+        pure $ CApp (CRef "Meta\{show k}") [] Z
+  _ | (t@(Ref fc nm _), args) = do
+        args' <- traverse compileTerm args
+        arity <- arityForName fc nm
+        top <- get
+        let Just (MkEntry _ _ type _) = lookup nm top
+          | Nothing => error fc "Undefined name \{nm}"
+        apply (CRef (show nm)) args' [<] arity type
+  _ | (t, args) = do
+        debug "apply other \{pprint [] t}"
+        t' <- compileTerm t
+        args' <- traverse compileTerm args
+        apply t' args' [<] 0 (UU emptyFC)
+        -- error (getFC t) "Don't know how to apply \{showTm t}"
+compileTerm (UU _) = pure $ CRef "U"
+compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] Z
+compileTerm (Case _ t alts) = do
+  t' <- compileTerm t
+  alts' <- traverse (\case
+    CaseDefault tm => pure $ CDefAlt !(compileTerm tm)
+    -- we use the base name for the tag, some primitives assume this
+    CaseCons (QN ns nm) args tm => pure $ CConAlt nm args !(compileTerm tm)
+    CaseLit lit tm => pure $ CLitAlt lit !(compileTerm tm)) alts
+  pure $ CCase t' alts'
+compileTerm (Lit _ lit) = pure $ CLit lit
+compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u)
+compileTerm (LetRec _ nm _ t u) = pure $ CLetRec nm !(compileTerm t) !(compileTerm u)
+compileTerm (Erased _) = pure CErased
+
+export
+compileFun : Tm -> M CExp
+compileFun tm = go tm [<]
+  where
+    go : Tm -> SnocList String -> M CExp
+    go (Lam _ nm _ _ t) acc = go t (acc :< nm)
+    go tm [<] = compileTerm tm
+    go tm args = pure $ CFun (args <>> []) !(compileTerm tm)
+
+

orig/Lib/Erasure.idr

@@ -0,0 +1,102 @@
+module Lib.Erasure
+
+import Lib.Types
+import Data.Maybe
+import Data.SnocList
+import Lib.TopContext
+
+public export
+EEnv : Type
+EEnv = List (String, Quant, Maybe Tm)
+
+-- TODO look into removing Nothing below, can we recover all of the types?
+-- Idris does this in `chk` for linearity checking.
+
+-- check App at type
+
+getType : Tm -> M (Maybe Tm)
+getType (Ref fc nm x) = do
+  top <- get
+  case lookup nm top of
+    Nothing => error fc "\{show nm} not in scope"
+    (Just (MkEntry _ name type def)) => pure $ Just type
+getType tm = pure Nothing
+
+export
+erase : EEnv -> Tm -> List (FC, Tm) -> M Tm
+
+-- App a spine using type
+eraseSpine : EEnv -> Tm -> List (FC, Tm) -> (ty : Maybe Tm) -> M Tm
+eraseSpine env tm [] _ = pure tm
+eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Zero a b)) = do
+  let u = Erased (getFC arg)
+  eraseSpine env (App fc t u) args (Just b)
+eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Many a b)) = do
+  u <- erase env arg []
+  -- TODO this seems wrong, we need to subst u into b to get the type
+  eraseSpine env (App fc t u) args (Just b)
+-- eraseSpine env t ((fc, arg) :: args) (Just ty) = do
+--   error fc "ceci n'est pas une ∏ \{showTm ty}" -- e.g. Bnd 1
+eraseSpine env t ((fc, arg) :: args) _ = do
+  u <- erase env arg []
+  eraseSpine env (App fc t u) args Nothing
+
+doAlt : EEnv -> CaseAlt -> M CaseAlt
+-- REVIEW do we extend env?
+doAlt env (CaseDefault t) = CaseDefault <$> erase env t []
+doAlt env (CaseCons name args t) = do
+  top <- get
+  let (Just (MkEntry _ str type def)) = lookup name top
+    | _ => error emptyFC "\{show name} dcon missing from context"
+  let env' = piEnv env type args
+  CaseCons name args <$> erase env' t []
+  where
+    piEnv : EEnv -> Tm -> List String -> EEnv
+    piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg, rig, Just t) :: env) u args
+    piEnv env _ _ = env
+
+doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t []
+
+-- Check erasure and insert "Erased" value
+-- We have a solution for Erased values, so important thing here is checking.
+-- build stack, see what to do when we hit a non-app
+-- This is a little fuzzy because we don't have all of the types.
+erase env t sp = case t of
+  (App fc u v) => erase env u ((fc,v) :: sp)
+  (Ref fc nm x) => do
+    top <- get
+    case lookup nm top of
+      Nothing => error fc "\{nm} not in scope"
+      (Just (MkEntry _ name type def)) => eraseSpine env t sp (Just type)
+  (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u []
+  -- If we get here, we're looking at a runtime pi type
+  (Pi fc nm icit rig u v) => do
+    u' <- erase env u []
+    v' <- erase ((nm, Many, Just u) :: env) v []
+    eraseSpine env (Pi fc nm icit rig u' v') sp (Just $ UU emptyFC)
+  -- leaving as-is for now, we don't know the quantity of the apps
+  (Meta fc k) => pure t
+  (Case fc u alts) => do
+    -- REVIEW check if this pushes to env, and write that down or get an index on there
+    u' <- erase env u []
+    alts' <- traverse (doAlt env) alts
+    eraseSpine env (Case fc u' alts') sp Nothing
+  (Let fc nm u v) => do
+    u' <- erase env u []
+    v' <- erase ((nm, Many, Nothing) :: env) v []
+    eraseSpine env (Let fc nm u' v') sp Nothing
+  (LetRec fc nm ty u v) => do
+    u' <- erase ((nm, Many, Just ty) :: env) u []
+    v' <- erase ((nm, Many, Just ty) :: env) v []
+    eraseSpine env (LetRec fc nm ty u' v') sp Nothing
+  (Bnd fc k) => do
+    case getAt k env of
+      Nothing => error fc "bad index \{show k}"
+      -- This is working, but empty FC
+      Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)"
+      Just (nm, Many, ty) => eraseSpine env t sp ty
+  (UU fc) => eraseSpine env t sp (Just $ UU fc)
+  (Lit fc lit) => eraseSpine env t sp Nothing
+  Erased fc => error fc "erased value in relevant context" -- eraseSpine env t sp Nothing
+
+

orig/Lib/Eval.idr

@@ -0,0 +1,312 @@
+module Lib.Eval
+
+import Lib.Types
+import Lib.TopContext
+
+import Data.IORef
+import Data.Fin
+import Data.List
+import Data.SnocList
+import Data.Vect
+import Data.SortedMap
+
+export
+eval : Env -> Mode -> Tm -> M Val
+
+-- REVIEW everything is evalutated whether it's needed or not
+-- It would be nice if the environment were lazy.
+-- e.g. case is getting evaluated when passed to a function because
+-- of dependencies in pi-types, even if the dependency isn't used
+
+public export
+infixl 8 $$
+
+public export
+($$) : {auto mode : Mode} -> Closure -> Val -> M Val
+($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm
+
+export
+vapp : Val -> Val -> M Val
+vapp (VLam _ _ _ _ t) u = t $$ u
+vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u)
+vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (sp :< u)
+vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u)
+vapp t u = error' "impossible in vapp \{show t} to \{show u}\n"
+
+export
+vappSpine : Val -> SnocList Val -> M Val
+vappSpine t [<] = pure t
+vappSpine t (xs :< x) = do
+  rest <- vappSpine t xs
+  vapp rest x
+
+lookupVar : Env -> Nat -> Maybe Val
+lookupVar env k = let l = length env in
+  if k > l
+    then Nothing
+    else case getAt (lvl2ix l k) env of
+      Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v
+      Just v => Just v
+      Nothing => Nothing
+
+-- hoping to apply what we got via pattern matching
+export
+unlet : Env -> Val -> M Val
+unlet env t@(VVar fc k sp) = case lookupVar env k of
+      Just tt@(VVar fc' k' sp') => do
+        debug "lookup \{show k} is \{show tt}"
+        if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet env)
+      Just t => vappSpine t sp >>= unlet env
+      Nothing => do
+        debug "lookup \{show k} is Nothing in env \{show env}"
+        pure t
+unlet env x = pure x
+
+export
+tryEval : Env -> Val -> M (Maybe Val)
+tryEval env (VRef fc k _ sp) = do
+  top <- get
+  case lookup k top of
+      Just (MkEntry _ name ty (Fn tm)) =>
+        catchError (
+            do
+            debug "app \{show name} to \{show sp}"
+            vtm <- eval [] CBN tm
+            debug "tm is \{render 90 $ pprint [] tm}"
+            val <- vappSpine vtm sp
+            case val of
+              VCase _ _ _ => pure Nothing
+              VLetRec _ _ _ _ _ => pure Nothing
+              v => pure $ Just v)
+            (\ _ => pure Nothing)
+      _ => pure Nothing
+tryEval _ _ = pure Nothing
+
+-- Force far enough to compare types
+export
+forceType : Env -> Val -> M Val
+forceType env (VMeta fc ix sp) = do
+  meta <- lookupMeta ix
+  case meta of
+    (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
+    (Solved _ k t) => vappSpine t sp >>= forceType env
+forceType env x = do
+  Just x' <- tryEval env x
+    | _ => pure x
+  forceType env x'
+
+evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
+evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) = do
+  top <- get
+  if nm == name
+    then do
+      debug "ECase \{show nm} \{show sp} \{show nms} \{showTm t}"
+      go env (sp <>> []) nms
+    else case lookup nm top of
+      (Just (MkEntry _ str type (DCon k str1))) => evalCase env mode sc xs
+      -- bail for a stuck function
+      _ => pure Nothing
+  where
+    go : Env -> List Val -> List String -> M (Maybe Val)
+    go env (arg :: args) (nm :: nms) = go (arg :: env) args nms
+    go env args [] = do
+      t' <- eval env mode t
+      Just <$> vappSpine t' ([<] <>< args)
+    go env [] rest = pure Nothing
+-- REVIEW - this is handled in the caller already
+evalCase env mode sc@(VVar fc k sp) alts = case lookupVar env k of
+    Just tt@(VVar fc' k' sp') => do
+        debug "lookup \{show k} is \{show tt}"
+        if k' == k
+          then pure Nothing
+          else do
+            val <- vappSpine (VVar fc' k' sp') sp
+            evalCase env mode val alts
+    Just t => do
+      val <- vappSpine t sp
+      evalCase env mode val alts
+    Nothing => do
+        debug "lookup \{show k} is Nothing in env \{show env}"
+        pure Nothing
+evalCase env mode sc (CaseDefault u :: xs) = Just <$> eval (sc :: env) mode u
+evalCase env mode sc cc = do
+  debug "CASE BAIL sc \{show sc} vs \{show cc}"
+  debug "env is \{show env}"
+  pure Nothing
+
+-- TODO maybe add glueing
+
+eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
+eval env mode (App _ t u) = do
+  t' <- eval env mode t
+  u' <- eval env mode u
+  vapp t' u'
+eval env mode (UU fc) = pure (VU fc)
+eval env mode (Erased fc) = pure (VErased fc)
+eval env mode (Meta fc i) = do
+  meta <- lookupMeta i
+  case meta of
+        (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<]
+        (Solved _ k t) => pure $ t
+eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t)
+eval env mode (Pi fc x icit rig a b) = do
+  a' <- eval env mode a
+  pure $ VPi fc x icit rig a' (MkClosure env b)
+eval env mode (Let fc nm t u) = do
+  t' <- eval env mode t
+  u' <- eval (VVar fc (length env) [<] :: env) mode u
+  pure $ VLet fc nm t' u'
+eval env mode (LetRec fc nm ty t u) = do
+  ty' <- eval env mode ty
+  t' <- eval (VVar fc (length env) [<] :: env) mode t
+  u' <- eval (VVar fc (length env) [<] :: env) mode u
+  pure $ VLetRec fc nm ty' t' u'
+-- Here, we assume env has everything. We push levels onto it during type checking.
+-- I think we could pass in an l and assume everything outside env is free and
+-- translate to a level
+eval env mode (Bnd fc i) = case getAt i env of
+  Just rval => pure rval
+  Nothing => error fc "Bad deBruin index \{show i}"
+eval env mode (Lit fc lit) = pure $ VLit fc lit
+
+eval env mode tm@(Case fc sc alts) = do
+  -- TODO we need to be able to tell eval to expand aggressively here.
+  sc' <- eval env mode sc
+  sc' <- unlet env sc' -- try to expand lets from pattern matching
+  sc' <- forceType env sc'
+  vsc <- eval env mode sc
+  vcase <- evalCase env mode sc' alts
+  pure $ fromMaybe (VCase fc vsc alts) vcase
+
+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) = do
+  t' <- quoteSp lvl t xs
+  x' <- quote lvl x
+  pure $ App emptyFC t' x'
+
+quote l (VVar fc k sp) = if k < l
+  then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index
+  else error fc "Bad index in quote \{show k} depth \{show l}"
+quote l (VMeta fc i sp) = do
+  meta <- lookupMeta i
+  case meta of
+        (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp
+        (Solved _ k t) => vappSpine t sp >>= quote l
+quote l (VLam fc x icit rig t) = do
+  val <- t $$ VVar emptyFC l [<]
+  tm <- quote (S l) val
+  pure $ Lam fc x icit rig tm
+quote l (VPi fc x icit rig a b) = do
+  a' <- quote l a
+  val <- b $$ VVar emptyFC l [<]
+  tm <- quote (S l) val
+  pure $ Pi fc x icit rig a' tm
+quote l (VLet fc nm t u) = do
+  t' <- quote l t
+  u' <- quote (S l) u
+  pure $ Let fc nm t' u'
+quote l (VLetRec fc nm ty t u) = do
+  ty' <- quote l ty
+  t' <- quote (S l) t
+  u' <- quote (S l) u
+  pure $ LetRec fc nm ty' t' u'
+quote l (VU fc) = pure (UU fc)
+quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
+quote l (VCase fc sc alts) = do
+  sc' <- quote l sc
+  pure $ Case fc sc' alts
+quote l (VLit fc lit) = pure $ Lit fc lit
+quote l (VErased fc) = pure $ Erased fc
+
+-- 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 = eval env CBN t >>= quote (length env)
+
+export
+nfv : Env -> Tm -> M Tm
+nfv env t = eval env CBV t >>= quote (length env)
+
+export
+prvalCtx : {auto ctx : Context} -> Val -> M String
+prvalCtx v = do
+  tm <- quote ctx.lvl v
+  pure $ interpolate $ pprint (toList $ map fst ctx.types) tm
+
+export
+zonk : TopContext -> Nat -> Env -> Tm -> M Tm
+
+zonkBind : TopContext -> Nat -> Env -> Tm -> M Tm
+zonkBind top l env tm = zonk top (S l) (VVar (getFC tm) l [<] :: env) tm
+
+-- I don't know if app needs an FC...
+
+appSpine : Tm -> List Tm -> Tm
+appSpine t [] = t
+appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs
+
+-- REVIEW When metas are subst in, the fc point elsewhere
+-- We might want to update when it is solved and update recursively?
+-- For errors, I think we want to pretend the code has been typed in place
+tweakFC : FC -> Tm -> Tm
+tweakFC fc (Bnd fc1 k) = Bnd fc k
+tweakFC fc (Ref fc1 nm x) = Ref fc nm x
+tweakFC fc (UU fc1) = UU fc
+tweakFC fc (Meta fc1 k) = Meta fc k
+tweakFC fc (Lam fc1 nm icit rig t) = Lam fc nm icit rig t
+tweakFC fc (App fc1 t u) = App fc t u
+tweakFC fc (Pi fc1 nm icit x t u) = Pi fc nm icit x t u
+tweakFC fc (Case fc1 t xs) = Case fc t xs
+tweakFC fc (Let fc1 nm t u) = Let fc nm t u
+tweakFC fc (LetRec fc1 nm ty t u) = LetRec fc nm ty t u
+tweakFC fc (Lit fc1 lit) = Lit fc lit
+tweakFC fc (Erased fc1) = Erased fc
+
+-- TODO replace this with a variant on nf
+zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm
+zonkApp top l env (App fc t u) sp = do
+  u' <- zonk top l env u
+  zonkApp top l env t (u' :: sp)
+zonkApp top l env t@(Meta fc k) sp = do
+  meta <- lookupMeta k
+  case meta of
+    (Solved _ j v) => do
+      sp' <- traverse (eval env CBN) sp
+      debug "zonk \{show k} -> \{show v} spine \{show sp'}"
+      foo <- vappSpine v ([<] <>< sp')
+      debug "-> result is \{show foo}"
+      tweakFC fc <$> quote l foo
+    (Unsolved x j xs _ _ _) => pure $ appSpine t sp
+zonkApp top l env t sp = do
+  t' <- zonk top l env t
+  pure $ appSpine t' sp
+
+zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt
+zonkAlt top l env (CaseDefault t) = CaseDefault <$> zonkBind top l env t
+zonkAlt top l env (CaseLit lit t) = CaseLit lit <$> zonkBind top l env t
+zonkAlt top l env (CaseCons name args t) = CaseCons name args <$> go l env args t
+  where
+    go : Nat -> Env -> List String -> Tm -> M Tm
+    go l env [] tm = zonk top l env t
+    go l env (x :: xs) tm = go (S l) (VVar (getFC tm) l [<] :: env) xs tm
+
+zonk top l env t = case t of
+  (Meta fc k) => zonkApp top l env t []
+  (Lam fc nm icit rig u) => Lam fc nm icit rig <$> (zonk top (S l) (VVar fc l [<] :: env) u)
+  (App fc t u) => do
+    u' <- zonk top l env u
+    zonkApp top l env t [u']
+  (Pi fc nm icit rig a b) => Pi fc nm icit rig <$> zonk top l env a <*> zonkBind top l env b
+  (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u
+  (LetRec fc nm ty t u) => LetRec fc nm <$> zonk top l env ty <*> zonkBind top l env t <*> zonkBind top l env u
+  (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts
+  UU fc => pure $ UU fc
+  Lit fc lit => pure $ Lit fc lit
+  Bnd fc ix => pure $ Bnd fc ix
+  Ref fc ix def => pure $ Ref fc ix def
+  Erased fc => pure $ Erased fc

orig/Lib/Parser.idr

@@ -0,0 +1,616 @@
+module Lib.Parser
+
+import Data.Maybe
+import Data.String
+import Lib.Parser.Impl
+import Lib.Syntax
+import Lib.Token
+import Lib.Types
+
+ident : Parser String
+ident = token Ident <|> token MixFix
+
+uident : Parser String
+uident = token UIdent
+
+parenWrap : Parser a -> Parser a
+parenWrap pa = do
+  sym "("
+  t <- pa
+  sym ")"
+  pure t
+
+braces : Parser a -> Parser a
+braces pa = do
+  sym "{"
+  t <- pa
+  sym "}"
+  pure t
+
+dbraces : Parser a -> Parser a
+dbraces pa = do
+  sym "{{"
+  t <- pa
+  sym "}}"
+  pure t
+
+
+optional : Parser a -> Parser (Maybe a)
+optional pa = Just <$> pa <|> pure Nothing
+
+stringLit : Parser Raw
+stringLit = do
+  fc <- getPos
+  t <- token StringKind
+  pure $ RLit fc (LString (cast t))
+
+
+-- typeExpr is term with arrows.
+export
+typeExpr : Parser Raw
+export
+term : (Parser Raw)
+
+interp : Parser Raw
+interp = token StartInterp *> term <* token EndInterp
+
+
+interpString : Parser Raw
+interpString = do
+  -- fc <- getPos
+  ignore $ token StartQuote
+  part <- term
+  parts <- many (stringLit <|> interp)
+  ignore $ token EndQuote
+  pure $ foldl append part parts
+  where
+    append : Raw -> Raw -> Raw
+    append t u =
+      let fc = getFC t in
+      (RApp (getFC t) (RApp fc (RVar fc "_++_") t Explicit) u Explicit)
+
+intLit : Parser Raw
+intLit = do
+  fc <- getPos
+  t <- token Number
+  pure $ RLit fc (LInt (cast t))
+
+
+charLit : Parser Raw
+charLit = do
+  fc <- getPos
+  v <- token Character
+  pure $ RLit fc (LChar $ assert_total $ strIndex v 0)
+
+lit : Parser Raw
+lit = intLit <|> interpString <|> stringLit <|> charLit
+
+
+
+-- helpful when we've got some / many and need FC for each
+addPos : Parser a -> Parser (FC, a)
+addPos pa = (,) <$> getPos <*> pa
+
+asAtom : Parser Raw
+asAtom = do
+  fc <- getPos
+  nm <- ident
+  asPat <- optional $ keyword "@" *> parenWrap typeExpr
+  case asPat of
+    Just exp => pure $ RAs fc nm exp
+    Nothing  => pure $ RVar fc nm
+
+-- the inside of Raw
+atom : Parser Raw
+atom = RU <$> getPos <* keyword "U"
+    -- <|> RVar <$> getPos <*> ident
+    <|> asAtom
+    <|> RVar <$> getPos <*> uident
+    <|> RVar <$> getPos <*> token Projection
+    <|> lit
+    <|> RImplicit <$> getPos <* keyword "_"
+    <|> RHole <$> getPos <* keyword "?"
+    <|> parenWrap typeExpr
+
+-- Argument to a Spine
+pArg : Parser (Icit,FC,Raw)
+pArg = do
+  fc <- getPos
+  (Explicit,fc,) <$> atom
+    <|> (Implicit,fc,) <$> braces typeExpr
+    <|> (Auto,fc,) <$> dbraces typeExpr
+
+AppSpine : Type
+AppSpine = List (Icit,FC,Raw)
+
+pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
+pratt ops prec stop left spine = do
+  (left, spine) <- runPrefix stop left spine
+  let (left, spine) = projectHead left spine
+  let spine = runProject spine
+  case spine of
+    [] => pure (left, [])
+    ((Explicit, fc, tm@(RVar x nm)) :: rest) =>
+        if nm == stop then pure (left,spine) else
+        case lookup nm ops of
+          Just (MkOp name p fix False rule) => if p < prec
+            then pure (left, spine)
+            else
+              runRule p fix stop rule (RApp fc (RVar fc name) left Explicit) rest
+          Just _ => fail "expected operator"
+          Nothing =>
+            if isPrefixOf "." nm
+            then pratt ops prec stop (RApp (getFC tm) tm left Explicit) rest
+            else pratt ops prec stop (RApp (getFC left) left tm Explicit) rest
+    ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left) left tm icit) rest
+  where
+    projectHead : Raw -> AppSpine -> (Raw, AppSpine)
+    projectHead t sp@((Explicit, fc', RVar fc nm) :: rest) =
+      if isPrefixOf "." nm
+        then projectHead (RApp fc (RVar fc nm) t Explicit) rest
+        else (t,sp)
+    projectHead t sp = (t, sp)
+
+    -- we need to check left/AppSpine first
+    -- we have a case above for when the next token is a projection, but
+    -- we need this to make projection bind tighter than app
+    runProject : AppSpine -> AppSpine
+    runProject (t@(Explicit, fc', tm) :: u@(Explicit, _, RVar fc nm) :: rest) =
+      if isPrefixOf "." nm
+        then runProject ((Explicit, fc', RApp fc (RVar fc nm) tm Explicit) :: rest)
+        else (t :: u :: rest)
+    runProject tms = tms
+
+    -- left has our partially applied operator and we're picking up args
+    -- for the rest of the `_`
+    runRule : Int -> Fixity -> String -> List String -> Raw -> AppSpine -> Parser (Raw,AppSpine)
+    runRule p fix stop [] left spine = pure (left,spine)
+    runRule p fix stop [""] left spine = do
+      let pr = case fix of
+                InfixR => p
+                _ => p + 1
+      case spine of
+                ((_, fc, right) :: rest) => do
+                  (right, rest) <- pratt ops pr stop right rest
+                  pratt ops prec stop (RApp (getFC left) left right Explicit) rest
+                _ => fail "trailing operator"
+
+    runRule p fix stop (nm :: rule) left spine = do
+      let ((_,_,right)::rest) = spine | _ => fail "short"
+      (right,rest) <- pratt ops 0 nm right rest -- stop!!
+      let ((_,fc',RVar fc name) :: rest) = rest
+        | _ => fail "expected \{nm}"
+
+      if name == nm
+          then runRule p fix stop rule (RApp (getFC left) left right Explicit) rest
+          else fail "expected \{nm}"
+
+    -- run any prefix operators
+    runPrefix : String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
+    runPrefix stop (RVar fc nm) spine =
+      case lookup nm ops of
+           -- TODO False should be an error here
+         Just (MkOp name p fix True rule) => do
+            runRule p fix stop rule (RVar fc name) spine
+         _ =>
+          pure (left, spine)
+    runPrefix stop left spine = pure (left, spine)
+
+
+
+parseOp : Parser Raw
+parseOp = do
+  fc <- getPos
+  ops <- getOps
+  hd <- atom
+  rest <- many pArg
+  (res, []) <- pratt ops 0 "" hd rest
+    | _ => fail "extra stuff"
+  pure res
+
+
+-- TODO case let? We see to only have it for `do`
+-- try (keyword "let" >> sym "(")
+
+export
+letExpr : Parser Raw
+letExpr = do
+  keyword "let"
+  alts <- startBlock $ someSame $ letAssign
+  keyword' "in"
+  scope <- typeExpr
+  pure $ foldl (\ acc, (n,fc,ty,v) => RLet fc n (fromMaybe (RImplicit fc) ty) v acc) scope (reverse alts)
+  where
+    letAssign : Parser (Name,FC,Maybe Raw,Raw)
+    letAssign = do
+      fc <- getPos
+      name <- ident
+      -- TODO type assertion
+      ty <- optional (keyword ":" *> typeExpr)
+      keyword "="
+      t <- typeExpr
+      pure (name,fc,ty,t)
+
+pLamArg : Parser (Icit, String, Maybe Raw)
+pLamArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
+       <|> (Auto,,) <$> dbraces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
+       <|> (Explicit,,) <$> parenWrap (ident <|> uident) <*> optional (sym ":" >> typeExpr)
+       <|> (Explicit,,Nothing) <$> (ident <|> uident)
+       <|> (Explicit,"_",Nothing) <$ keyword "_"
+
+-- lam: λ {A} {b : A} (c : Blah) d e f. something
+export
+lamExpr : Parser Raw
+lamExpr = do
+  pos <- getPos
+  keyword "\\" <|> keyword "λ"
+  args <- some $ addPos pLamArg
+  keyword "=>"
+  scope <- typeExpr
+  pure $ foldr (\(fc, icit, name, ty), sc => RLam pos (BI fc name icit Many) sc) scope args
+
+caseAlt : Parser RCaseAlt
+caseAlt = do
+  pat <- typeExpr
+  keyword "=>"
+  t <- term
+  pure $ MkAlt pat t
+
+export
+caseExpr : Parser Raw
+caseExpr = do
+  fc <- getPos
+  keyword "case"
+  sc <- term
+  keyword "of"
+  alts <- startBlock $ someSame $ caseAlt
+  pure $ RCase fc sc alts
+
+caseLamExpr : Parser Raw
+caseLamExpr = do
+  fc <- getPos
+  try ((keyword "\\" <|> keyword "λ") *> keyword "case")
+  alts <- startBlock $ someSame $ caseAlt
+  pure $ RLam fc (BI fc "$case" Explicit Many) $ RCase fc (RVar fc "$case") alts
+
+doExpr : Parser Raw
+doStmt : Parser DoStmt
+
+caseLet : Parser Raw
+caseLet = do
+  -- look ahead so we can fall back to normal let
+  fc <- getPos
+  try (keyword "let" >> sym "(")
+  pat <- typeExpr
+  sym ")"
+  keyword "="
+  sc <- typeExpr
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  keyword "in"
+  body <- term
+  pure $ RCase fc sc (MkAlt pat body :: alts)
+
+doCaseLet : Parser DoStmt
+doCaseLet = do
+  -- look ahead so we can fall back to normal let
+  -- Maybe make it work like arrow?
+  fc <- getPos
+  try (keyword "let" >> sym "(")
+  pat <- typeExpr
+  sym ")"
+  keyword "="
+  sc <- typeExpr
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  bodyFC <- getPos
+  body <- RDo <$> getPos <*> someSame doStmt
+  pure $ DoExpr fc (RCase fc sc (MkAlt pat body :: alts))
+
+doArrow : Parser DoStmt
+doArrow = do
+  fc <- getPos
+  left <- typeExpr
+  (Just _) <- optional $ keyword "<-"
+    | _ => pure $ DoExpr fc left
+  right <- term
+  alts <- startBlock $ manySame $ sym "|" *> caseAlt
+  pure $ DoArrow fc left right alts
+
+doStmt
+  = doCaseLet
+  <|> DoLet <$> getPos <* keyword "let" <*> ident <* keyword "=" <*> term
+  <|> doArrow
+
+doExpr = RDo <$> getPos <* keyword "do" <*> (startBlock $ someSame doStmt)
+
+ifThenElse : Parser Raw
+ifThenElse = do
+  fc <- getPos
+  keyword "if"
+  a <- term
+  keyword "then"
+  b <- term
+  keyword "else"
+  c <- term
+  pure $ RIf fc a b c
+
+term' : Parser Raw
+
+term' =  caseExpr
+    <|> caseLet
+    <|> letExpr
+    <|> caseLamExpr
+    <|> lamExpr
+    <|> doExpr
+    <|> ifThenElse
+    -- Make this last for better error messages
+    <|> parseOp
+
+term = do
+  t <- term'
+  rest <- many ((,) <$> getPos <* keyword "$" <*> term')
+  pure $ apply t rest
+  where
+    apply : Raw -> List (FC,Raw) -> Raw
+    apply t [] = t
+    apply t ((fc,x) :: xs) = RApp fc t (apply x xs) Explicit
+
+varname : Parser String
+varname = (ident <|> uident <|> keyword "_" *> pure "_")
+
+quantity : Parser Quant
+quantity = fromMaybe Many <$> optional (Zero <$ keyword "0")
+
+ebind : Parser Telescope
+ebind = do
+  -- don't commit until we see the ":"
+  sym "("
+  quant <- quantity
+  names <- try (some (addPos varname) <* sym ":")
+  ty <- typeExpr
+  sym ")"
+  pure $ map (\(pos, name) => (BI pos name Explicit quant, ty)) names
+
+ibind : Parser Telescope
+ibind = do
+  -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat}
+  sym "{"
+  quant <- quantity
+  names <- (some (addPos varname))
+  ty <- optional (sym ":" *> typeExpr)
+  sym "}"
+  pure $ map (\(pos,name) => (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)) names
+
+abind : Parser Telescope
+abind = do
+  -- for this, however, it would be nice to allow {{Monad A}}
+  sym "{{"
+  name <- optional $ try (addPos varname <* sym ":")
+  ty <- typeExpr
+  sym "}}"
+  case name of
+    Just (pos,name) => pure [(BI pos name Auto Many, ty)]
+    Nothing => pure [(BI (getFC ty) "_" Auto Many, ty)]
+
+arrow : Parser Unit
+arrow = sym "->" <|> sym "→"
+
+-- Collect a bunch of binders (A : U) {y : A} -> ...
+
+forAll : Parser Raw
+forAll = do
+  keyword "forall" <|> keyword "∀"
+  all <- some (addPos varname)
+  keyword "."
+  scope <- typeExpr
+  pure $ foldr (\ (fc, n), sc => RPi fc (BI fc n Implicit Zero) (RImplicit fc) sc) scope all
+
+binders : Parser Raw
+binders = do
+  binds <- many (abind <|> ibind <|> ebind)
+  arrow
+  scope <- typeExpr
+  pure $ foldr mkBind scope (join binds)
+  where
+    mkBind : (BindInfo, Raw) -> Raw -> Raw
+    mkBind (info, ty) scope = RPi (getFC info) info ty scope
+
+typeExpr
+  = binders
+  <|> forAll
+  <|> do
+        fc <- getPos
+        exp <- term
+        scope <- optional (arrow *> typeExpr)
+        case scope of
+          Nothing      => pure exp
+          -- consider Maybe String to represent missing
+          (Just scope) => pure $ RPi fc (BI fc "_" Explicit Many) exp scope
+
+-- And top level stuff
+
+export
+parseSig : Parser Decl
+parseSig = TypeSig <$> getPos <*> try (some (ident <|> uident <|> token Projection) <* keyword ":") <*> typeExpr
+
+parseImport : Parser Import
+parseImport = do
+  fc <- getPos
+  keyword "import"
+  ident <- uident
+  rest <- many $ token Projection
+  let name = joinBy "" (ident :: rest)
+  pure $ MkImport fc name
+
+-- Do we do pattern stuff now? or just name = lambda?
+-- TODO multiple names
+parseMixfix : Parser Decl
+parseMixfix = do
+  fc <- getPos
+  fix <- InfixL <$ keyword "infixl"
+     <|> InfixR <$ keyword "infixr"
+     <|> Infix <$ keyword "infix"
+  prec <- token Number
+  ops <- some $ token MixFix
+  for_ ops $ \ op => addOp op (cast prec) fix
+  pure $ PMixFix fc ops (cast prec) fix
+
+getName : Raw -> Parser String
+getName (RVar x nm) = pure nm
+getName (RApp x t u icit) = getName t
+getName tm = fail "bad LHS"
+
+
+export
+parseDef : Parser Decl
+parseDef = do
+  fc <- getPos
+  t <- typeExpr
+  nm <- getName t
+  keyword "="
+  body <- typeExpr
+  wfc <- getPos
+  w <- optional $ do
+    keyword "where"
+    startBlock $ manySame $ (parseSig <|> parseDef)
+  let body = maybe body (\ decls => RWhere wfc decls body) w
+  -- these get collected later
+  pure $ Def fc nm [(t, body)] -- [MkClause fc [] t body]
+
+export
+parsePType : Parser Decl
+parsePType = do
+  fc <- getPos
+  keyword "ptype"
+  id <- uident
+  ty <- optional $ do
+    keyword ":"
+    typeExpr
+  pure $ PType fc id ty
+
+parsePFunc : Parser Decl
+parsePFunc = do
+  fc <- getPos
+  keyword "pfunc"
+  nm <- ident
+  uses <- optional (keyword "uses" >> parenWrap (many $ uident <|> ident <|> token MixFix))
+  keyword ":"
+  ty <- typeExpr
+  keyword ":="
+  src <- cast <$> token JSLit
+  pure $ PFunc fc nm (fromMaybe [] uses) ty src
+
+
+parseShortData : Parser Decl
+parseShortData = do
+  fc <- getPos
+  keyword "data"
+  lhs <- typeExpr
+  keyword "="
+  sigs <- sepBy (keyword "|") typeExpr
+  pure $ ShortData fc lhs sigs
+
+export
+parseData : Parser Decl
+parseData = do
+  fc <- getPos
+  -- commit when we hit ":"
+  name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":")
+  ty <- typeExpr
+  keyword "where"
+  decls <- startBlock $ manySame $ parseSig
+  pure $ Data fc name ty decls
+
+nakedBind : Parser Telescope
+nakedBind = do
+  names <- some (addPos varname)
+  pure $ map (\(pos,name) => (BI pos name Explicit Many, RImplicit pos)) names
+
+export
+parseRecord : Parser Decl
+parseRecord = do
+  fc <- getPos
+  keyword "record"
+  name <- uident
+  teles <- many $ ebind <|> nakedBind
+  keyword "where"
+  cname <- optional $ keyword "constructor" *> (uident <|> token MixFix)
+  decls <- startBlock $ manySame $ parseSig
+  pure $ Record fc name (join teles) cname decls
+
+
+export
+parseClass : Parser Decl
+parseClass = do
+  fc <- getPos
+  keyword "class"
+  name <- uident
+  teles <- many $ ebind <|> nakedBind
+  keyword "where"
+  decls <- startBlock $ manySame $ parseSig
+  pure $ Class fc name (join teles) decls
+
+export
+parseInstance : Parser Decl
+parseInstance = do
+  fc <- getPos
+  keyword "instance"
+  ty <- typeExpr
+  -- is it a forward declaration
+  (Just _) <- optional $ keyword "where"
+    | _ => pure $ Instance fc ty Nothing
+  decls <- startBlock $ manySame $ parseDef
+  pure $ Instance fc ty (Just 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 <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
+
+export
+parseDecl : Parser Decl
+parseDecl = parseMixfix <|> parsePType <|> parsePFunc
+  <|> parseNorm <|> parseData <|> parseShortData <|> parseSig <|> parseDef
+  <|> parseClass <|> parseInstance <|> parseRecord
+
+
+export
+parseModHeader : Parser (FC, String)
+parseModHeader = do
+  sameLevel (keyword "module")
+  fc <- getPos
+  name <- uident
+  rest <- many $ token Projection
+  -- FIXME use QName
+  let name = joinBy "" (name :: rest)
+  pure (fc, name)
+
+export
+parseImports : Parser (List Import)
+parseImports = manySame $ parseImport
+
+export
+parseMod : Parser Module
+parseMod = do
+  startBlock $ do
+    keyword "module"
+    name <- uident
+    rest <- many $ token Projection
+    -- FIXME use QName
+    let name = joinBy "" (name :: rest)
+    imports <- manySame $ parseImport
+    decls <- manySame $ parseDecl
+    pure $ MkModule name imports decls
+
+public export
+data ReplCmd =
+    Def Decl
+  | Norm Raw -- or just name?
+  | Check Raw
+
+
+-- Eventually I'd like immediate actions in the file, like lean, but I
+-- also want to REPL to work and we can do that first.
+export
+parseRepl : Parser ReplCmd
+parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr
+  <|> Check <$ keyword "#check" <*> typeExpr

orig/Lib/Parser/Impl.idr

@@ -0,0 +1,219 @@
+module Lib.Parser.Impl
+
+import Prelude
+import Lib.Token
+import Lib.Common
+import Data.String
+import Data.Nat
+import Data.List1
+import Data.SortedMap
+
+public export
+TokenList : Type
+TokenList = List BTok
+
+-- Result of a parse
+public export
+data Result : Type -> Type where
+  OK : a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
+  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
+
+export
+Functor Result where
+  map f (OK a toks com ops) = OK (f a) toks com ops
+  map _ (Fail fatal err toks com ops) = Fail fatal err toks com ops
+
+-- So sixty just has a newtype function here now (probably for perf).
+-- A record might be more ergonomic, but would require a record impl before
+-- self hosting.
+
+-- FC is a line and column for indents. The idea being that we check
+-- either the col < tokCol or line == tokLine, enabling sameLevel.
+
+-- We need State for operators (or postpone that to elaboration)
+-- Since I've already built out the pratt stuff, I guess I'll
+-- leave it in the parser for now
+
+-- This is a Reader in FC, a State in Operators, Commit flag, TokenList
+
+export
+data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a)
+
+export
+runP : Parser a -> TokenList -> Bool -> Operators -> FC -> Result a
+runP (P f) = f
+
+-- FIXME no filename, also half the time it is pointing at the token after the error
+error : String -> TokenList -> String -> Error
+error fn [] msg = E (MkFC fn (0,0)) msg
+error fn ((MkBounded val (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg
+
+export
+parse : String -> Parser a -> TokenList -> Either Error a
+parse fn pa toks = case runP pa toks False empty (MkFC fn (-1,-1)) of
+  Fail fatal err toks com ops => Left err
+  OK a [] _ _ => Right a
+  OK a ts _ _ => Left (error fn ts "Extra toks")
+
+||| Intended for parsing a top level declaration
+export
+partialParse : String -> Parser a -> Operators -> TokenList -> Either (Error, TokenList) (a, Operators, TokenList)
+partialParse fn pa ops toks = case runP pa toks False ops (MkFC fn (0,0)) of
+  Fail fatal err toks com ops => Left (err, toks)
+  OK a ts _ ops => Right (a,ops,ts)
+
+-- I think I want to drop the typeclasses for v1
+
+export
+try : Parser a -> Parser a
+try (P pa) = P $ \toks,com,ops,col => case pa toks com ops col of
+  (Fail x err toks com ops) => Fail x err toks False ops
+  res => res
+
+export
+fail : String -> Parser a
+fail msg = P $ \toks,com,ops,col => Fail False (error col.file toks msg) toks com ops
+
+export
+fatal : String -> Parser a
+fatal msg = P $ \toks,com,ops,col => Fail True (error col.file toks msg) toks com ops
+
+export
+getOps : Parser (Operators)
+getOps = P $ \ toks, com, ops, col => OK ops toks com ops
+
+export
+addOp : String -> Int -> Fixity -> Parser ()
+addOp nm prec fix = P $ \ toks, com, ops, col =>
+  let parts = split (=='_') nm in
+  case parts of
+    "" ::: key :: rule => OK () toks com (insert key (MkOp nm prec fix False rule) ops)
+    key ::: rule => OK () toks com (insert key (MkOp nm prec fix True rule) ops)
+
+
+
+export
+Functor Parser where
+  map f (P pa) = P $ \ toks, com, ops, col => map f (pa toks com ops col)
+
+export
+Applicative Parser where
+  pure pa = P (\ toks, com, ops, col => OK pa toks com ops)
+  P pab <*> P pa = P $ \toks,com,ops,col =>
+    case pab toks com ops col of
+      Fail fatal err toks com ops => Fail fatal err toks com ops
+      OK f toks com ops =>
+        case pa toks com ops col of
+          (OK x toks com ops) => OK (f x) toks com ops
+          (Fail fatal err toks com ops) => Fail fatal err toks com ops
+
+-- Second argument lazy so we don't have circular refs when defining parsers.
+export
+(<|>) : Parser a -> (Parser a) -> Parser a
+(P pa) <|> (P pb) = P $ \toks,com,ops,col =>
+  case pa toks False ops col of
+    OK a toks' _ ops => OK a toks' com ops
+    Fail True  err toks' com ops  => Fail True err toks' com ops
+    Fail fatal err toks' True ops => Fail fatal err toks' True ops
+    Fail fatal err toks' False ops => pb toks com ops col
+
+export
+Monad Parser where
+  P pa >>= pab = P $ \toks,com,ops,col =>
+    case pa toks com ops col of
+      (OK a toks com ops) => runP (pab a) toks com ops col
+      (Fail fatal err xs x ops) => Fail fatal err xs x ops
+
+
+satisfy : (BTok -> Bool) -> String -> Parser String
+satisfy f msg = P $ \toks,com,ops,col =>
+  case toks of
+    (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error col.file toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops
+    [] => Fail False (error col.file toks "\{msg} at EOF") toks com ops
+
+export
+commit : Parser ()
+commit = P $ \toks,com,ops,col => OK () toks True ops
+
+
+export some : Parser a -> Parser (List a)
+export many : Parser a -> Parser (List a)
+some p = (::) <$> p <*> many p
+many p = some p <|> pure []
+
+-- one or more `a` seperated by `s`
+export
+sepBy : Parser s -> Parser a -> Parser (List a)
+sepBy s a = (::) <$> a <*> many (s *> a)
+
+export
+getPos : Parser FC
+getPos = P $ \toks, com, ops, indent => case toks of
+  [] => OK emptyFC toks com ops
+  (t :: ts) => OK (MkFC indent.file (getStart t)) toks com ops
+
+||| Start an indented block and run parser in it
+export
+startBlock : Parser a -> Parser a
+startBlock (P p) = P $ \toks,com,ops,indent => case toks of
+  [] => p toks com ops indent
+  (t :: _) =>
+    -- If next token is at or before the current level, we've got an empty block
+    let (tl,tc) = getStart t in
+    let (MkFC file (line,col)) = indent in
+    p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc))
+
+||| Assert that parser starts at our current column by
+||| checking column and then updating line to match the current
+export
+sameLevel : Parser a -> Parser a
+sameLevel (P p) = P $ \toks, com, ops, indent => case toks of
+  [] => p toks com ops indent
+  (t :: _) =>
+    let (tl,tc) = getStart t in
+    let (MkFC file (line,col)) = indent in
+    if tc == col then p toks com ops (MkFC file (tl, col))
+    else if col < tc then Fail False (error file toks "unexpected indent") toks com ops
+    else Fail False (error file toks "unexpected indent") toks com ops
+
+export
+someSame : Parser a -> Parser (List a)
+someSame pa = some $ sameLevel pa
+
+export
+manySame : Parser a -> Parser (List a)
+manySame pa = many $ sameLevel pa
+
+||| check indent on next token and run parser
+export
+indented : Parser a -> Parser a
+indented (P p) = P $ \toks,com,ops,indent => case toks of
+  [] => p toks com ops indent
+  (t::_) =>
+    let (tl,tc) = getStart t
+    in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent
+    else Fail False (error (file indent) toks "unexpected outdent") toks com ops
+
+||| expect token of given kind
+export
+token' : Kind -> Parser String
+token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
+
+export
+keyword' : String -> Parser ()
+-- FIXME make this an appropriate whitelist
+keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
+
+||| expect indented token of given kind
+export
+token : Kind -> Parser String
+token = indented . token'
+
+export
+keyword : String -> Parser ()
+keyword kw = indented $ keyword' kw
+
+export
+sym : String -> Parser ()
+sym = keyword
+

orig/Lib/Prettier.idr

@@ -0,0 +1,149 @@
+||| A prettier printer, Philip Wadler
+||| https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
+module Lib.Prettier
+
+import Data.String
+import Data.Nat
+import Data.Maybe
+
+||| `Doc` is a pretty printing document.  Constructors are private, use
+||| methods below.  `Alt` in particular has some invariants on it, see paper
+||| for details. (Something along the lines of "the first line of left is not
+||| bigger than the first line of the right".)
+export
+data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
+
+||| The original paper had a List-like structure Doc (the above was DOC) which
+||| had Empty and a tail on Text and Line.
+data Item = TEXT String | LINE Nat
+
+export
+empty : Doc
+empty = Empty
+
+flatten : Doc -> Doc
+flatten Empty = Empty
+flatten (Seq x y) = Seq (flatten x) (flatten y)
+flatten (Nest i x) = flatten x
+flatten Line = Text " "
+flatten (Text str) = Text str
+flatten (Alt x y) = flatten x
+
+group : Doc -> Doc
+group x = Alt (flatten x) x
+
+-- TODO - we can accumulate snoc and cat all at once
+layout : List Item -> SnocList String -> String
+layout [] acc = fastConcat $ acc <>> []
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ')
+layout (TEXT str :: x) acc = layout x (acc :< str)
+
+||| Whether a documents first line fits.
+fits : Nat -> List Item -> Bool
+fits w ((TEXT s) :: xs) = if length s < w then fits (w `minus` length s) xs else False
+fits w _ = True
+
+-- vs Wadler, we're collecting the left side as a SnocList to prevent
+-- blowing out the stack on the Text case.  The original had DOC as
+-- a Linked-List like structure (now List Item)
+
+-- I've now added a `fit` boolean to indicate if we should cut when we hit the line length
+-- Wadler was relying on laziness to stop the first branch before LINE if necessary
+be : Bool -> SnocList Item -> Nat -> Nat -> List (Nat, Doc) -> Maybe (List Item)
+be fit acc w k [] = Just (acc <>> [])
+be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs
+be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs)
+be fit acc w k ((i, (Text s)) :: xs) =
+  if not fit || (k + length s < w)
+     then (be fit (acc :< TEXT s) w (k + length s) xs)
+     else Nothing
+be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x) :: xs)
+be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs)
+be fit acc w k ((i, (Alt x y)) :: xs) =
+  (acc <>>) <$> (be True [<] w k ((i,x) :: xs) <|> be fit [<] w k ((i,y) :: xs))
+
+best : Nat -> Nat -> Doc -> List Item
+best w k x = fromMaybe [] $ be False [<] w k [(0,x)]
+
+-- Public interface
+public export
+interface Pretty a where
+  pretty : a -> Doc
+
+export
+render : Nat -> Doc -> String
+render w x = layout (best w 0 x) [<]
+
+public export
+Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y)
+
+-- Match System.File so we don't get warnings
+public export
+infixl 5 </>
+
+export
+line : Doc
+line = Line
+
+export
+text : String -> Doc
+text = Text
+
+export
+nest : Nat -> Doc -> Doc
+nest = Nest
+
+export
+(++) : Doc -> Doc -> Doc
+x ++ y = Seq x y
+
+export
+(</>) : Doc -> Doc -> Doc
+x </> y = x ++ line ++ y
+
+||| fold, but doesn't emit extra nil
+export
+folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc
+folddoc f [] = Empty
+folddoc f [x] = x
+folddoc f (x :: xs) = f x (folddoc f xs)
+
+||| separate with space
+export
+spread : List Doc -> Doc
+spread = folddoc (<+>)
+
+||| separate with new lines
+export
+stack : List Doc -> Doc
+stack = folddoc (</>)
+
+||| bracket x with l and r, indenting contents on new line
+export
+bracket : String -> Doc -> String -> Doc
+bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
+
+export
+infixl 5 <+/>
+
+||| Either space or newline
+export
+(<+/>) : Doc -> Doc -> Doc
+x <+/> y = x ++ Alt (text " ") line ++ y
+
+||| Reformat some docs to fill. Not sure if I want this precise behavior or not.
+export
+fill : List Doc -> Doc
+fill [] = Empty
+fill [x] = x
+fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
+
+||| separate with comma
+export
+commaSep : List Doc -> Doc
+commaSep = folddoc (\a, b => a ++ text "," <+/> b)
+
+||| If we stick Doc into a String, try to avoid line-breaks via `flatten`
+public export
+Interpolation Doc where
+  interpolate = render 80 . flatten

orig/Lib/ProcessDecl.idr

@@ -0,0 +1,426 @@
+module Lib.ProcessDecl
+
+import Data.IORef
+import Data.String
+import Data.Vect
+import Data.List
+import Data.Maybe
+
+import Lib.Elab
+import Lib.Parser
+import Lib.Syntax
+import Lib.TopContext
+import Lib.Eval
+import Lib.Types
+import Lib.Util
+import Lib.Erasure
+
+dumpEnv : Context -> M String
+dumpEnv ctx =
+  unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) []
+  where
+    isVar : Nat -> Val -> Bool
+    isVar k (VVar _ k' [<]) = k == k'
+    isVar _ _ = False
+
+    go : List String -> Nat -> List (Val, String, Val) -> List String -> M (List String)
+    go _ _ [] acc = pure acc
+    go names k ((v, n, ty) :: xs) acc = if isVar k v
+      -- TODO - use Doc and add <+/> as appropriate to printing
+      then go names (S k) xs ("  \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc)
+      else go names (S k) xs ("  \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc)
+
+export
+logMetas : Nat -> M ()
+logMetas mstart = do
+  -- FIXME, now this isn't logged for Sig / Data.
+  top <- get
+  mc <- readIORef top.metaCtx
+  let mlen = length mc.metas `minus` mstart
+  for_ (reverse $ take mlen mc.metas) $ \case
+    (Solved fc k soln) => do
+      -- TODO put a flag on this, vscode is getting overwhelmed and
+      -- dropping errors
+      --info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
+      pure ()
+    (Unsolved fc k ctx ty User cons) => do
+      ty' <- quote ctx.lvl ty
+      let names = (toList $ map fst ctx.types)
+      env <- dumpEnv ctx
+      let msg = "\{env}  -----------\n  \{pprint names ty'}"
+      info fc "User Hole\n\{msg}"
+
+    (Unsolved fc k ctx ty kind cons) => do
+      tm <- quote ctx.lvl !(forceMeta ty)
+      -- Now that we're collecting errors, maybe we simply check at the end
+      -- TODO - log constraints?
+      -- FIXME in Combinatory, the val doesn't match environment?
+      let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
+      msgs <- for cons $ \ (MkMc fc env sp val) => do
+            pure "  * (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}"
+      sols <- case kind of
+        AutoSolve => do
+          x <- quote ctx.lvl ty
+          ty <- eval ctx.env CBN x
+          debug "AUTO ---> \{show ty}"
+          -- we want the context here too.
+          top <- get
+          -- matches <- case !(contextMatches ctx ty) of
+          --   [] => findMatches ctx ty $ toList top.defs
+          --   xs => pure xs
+          matches <- findMatches ctx ty $ toList top.defs
+          -- TODO try putting mc into TopContext for to see if it gives better terms
+          pure $ ["  \{show $ length matches} Solutions: \{show matches}"]
+          -- pure $ "  \{show $ length matches} Solutions:" :: map (("  " ++) . interpolate . pprint (names ctx) . fst) matches
+
+        _ => pure []
+      info fc $ unlines ([msg] ++ msgs ++ sols)
+      -- addError $ E fc $ unlines ([msg] ++ msgs ++ sols)
+
+
+-- Used for Class and Record
+getSigs : List Decl -> List (FC, String, Raw)
+getSigs [] = []
+getSigs ((TypeSig _ [] _) :: xs) = getSigs xs
+getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs
+getSigs (_ :: xs) = getSigs xs
+
+teleToPi : Telescope -> Raw -> Raw
+teleToPi [] end = end
+teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)
+
+impTele : Telescope -> Telescope
+impTele tele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele
+
+
+export
+processDecl : List String -> Decl -> M ()
+
+-- REVIEW I supposed I could have updated top here instead of the dance with the parser...
+processDecl ns  (PMixFix{})  = pure ()
+
+processDecl ns  (TypeSig fc names tm) = do
+  putStrLn "-----"
+
+  top <- get
+  mc <- readIORef top.metaCtx
+  let mstart = length mc.metas
+  for_ names $ \nm => do
+    let Nothing := lookupRaw nm top
+      | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
+    pure ()
+  ty <- check (mkCtx fc) tm (VU fc)
+  ty <- zonk top 0 [] ty
+  putStrLn "TypeSig \{unwords names} : \{pprint [] ty}"
+  for_ names $ \nm => setDef (QN ns nm) fc ty Axiom
+  -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here
+  -- logMetas mstart
+
+processDecl ns (PType fc nm ty) = do
+  top <- get
+  ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc)
+  setDef (QN ns nm) fc ty' PrimTCon
+
+processDecl ns  (PFunc fc nm uses ty src) = do
+  top <- get
+  ty <- check (mkCtx fc) ty (VU fc)
+  ty' <- nf [] ty
+  putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}"
+  -- TODO wire through fc?
+  for_ uses $ \ name => case lookupRaw name top of
+    Nothing => error fc "\{name} not in scope"
+    _ => pure ()
+  setDef (QN ns nm) fc ty' (PrimFn src uses)
+
+processDecl ns (Def fc nm clauses) = do
+  putStrLn "-----"
+  putStrLn "Def \{show nm}"
+  top <- get
+  mc <- readIORef top.metaCtx
+  let mstart = length mc.metas
+  let Just entry = lookupRaw nm top
+    | Nothing => throwError $ E fc "No declaration for \{nm}"
+  let (MkEntry fc name ty Axiom) := entry
+    | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"
+
+  putStrLn "check \{nm} at \{pprint [] ty}"
+  vty <- eval empty CBN ty
+
+  debug "\{nm} vty is \{show vty}"
+
+
+  -- I can take LHS apart syntactically or elaborate it with an infer
+  clauses' <- traverse (makeClause top) clauses
+  tm <- buildTree (mkCtx fc) (MkProb clauses' vty)
+  -- putStrLn "Ok \{pprint [] tm}"
+
+  mc <- readIORef top.metaCtx
+  let mlen = length mc.metas `minus` mstart
+  solveAutos mstart
+  -- TODO - make nf that expands all metas and drop zonk
+  -- Day1.newt is a test case
+  -- tm' <- nf [] tm
+  tm' <- zonk top 0 [] tm
+  when top.verbose $ putStrLn "NF\n\{render 80 $ pprint[] tm'}"
+  -- TODO we want to keep both versions, but this is checking in addition to erasing
+  -- currently CompileExp is also doing erasure.
+  -- TODO we need erasure info on the lambdas or to fake up an appropriate environment
+  -- and erase inside. Currently the checking is imprecise
+  tm'' <- erase [] tm' []
+  when top.verbose $ putStrLn "ERASED\n\{render 80 $ pprint[] tm'}"
+  debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
+  updateDef (QN ns nm) fc ty (Fn tm')
+  -- logMetas mstart
+
+processDecl ns (DCheck fc tm ty) = do
+  putStrLn "----- DCheck"
+  top <- get
+
+  putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}"
+  ty' <- check (mkCtx fc) ty (VU fc)
+  putStrLn "  got type \{pprint [] ty'}"
+  vty <- eval [] CBN ty'
+  res <- check (mkCtx fc) tm vty
+  putStrLn "  got \{pprint [] res}"
+  norm <- nf [] res
+  putStrLn "  NF \{pprint [] norm}"
+  norm <- nfv [] res
+  putStrLn "  NFV \{pprint [] norm}"
+
+processDecl ns (Class classFC nm tele decls) = do
+  -- REVIEW maybe we can leverage Record for this
+  -- a couple of catches, we don't want the dotted accessors and
+  -- the self argument should be an auto-implicit
+  putStrLn "-----"
+  putStrLn "Class \{nm}"
+  let fields = getSigs decls
+  -- We'll need names for the telescope
+  let dcName = "Mk\{nm}"
+  let tcType = teleToPi tele (RU classFC)
+  let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele
+  let dcType = teleToPi (impTele tele) $
+    foldr (\(fc, nm, ty), acc =>  RPi fc (BI fc nm Explicit Many) ty acc  ) tail fields
+
+  putStrLn "tcon type \{pretty tcType}"
+  putStrLn "dcon type \{pretty dcType}"
+  let decl = Data classFC nm tcType [TypeSig classFC [dcName] dcType]
+  putStrLn "Decl:"
+  putStrLn $ render 90 $ pretty decl
+  processDecl ns decl
+  for_ fields $ \ (fc,name,ty) => do
+      let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Auto Many) tail ty
+      let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields
+      let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
+      let lhs = RApp classFC lhs autoPat Auto
+      let decl = Def fc name [(lhs, (RVar fc name))]
+
+      putStrLn "\{name} : \{pretty funType}"
+      putStrLn "\{pretty decl}"
+      processDecl ns $ TypeSig fc [name] funType
+      processDecl ns decl
+
+
+processDecl ns (Instance instfc ty decls) = do
+
+  putStrLn "-----"
+  putStrLn "Instance \{pretty ty}"
+  top <- get
+  let tyFC = getFC ty
+
+  vty <- check (mkCtx instfc) ty (VU instfc)
+  -- Here `tele` holds arguments to the instance
+  let (codomain, tele) = splitTele vty
+  -- env represents the environment of those arguments
+  let env = tenv (length tele)
+  debug "codomain \{pprint [] codomain}"
+  debug "tele is \{show tele}"
+
+  -- ok so we need a name, a hack for now.
+  -- Maybe we need to ask the user (e.g. `instance someName : Monad Foo where`)
+  -- or use "Monad\{show $ length defs}"
+  let instname = interpolate $ pprint [] codomain
+  let sigDecl = TypeSig instfc [instname] ty
+  -- This needs to be declared before processing the defs, but the defs need to be
+  -- declared before this - side effect is that a duplicate def is noted at the first
+  -- member
+  case lookupRaw instname top of
+    Just _ => pure MkUnit -- TODO check that the types match
+    Nothing => processDecl ns sigDecl
+
+  let (Just decls) = collectDecl <$> decls
+    | _ => do
+      debug "Forward declaration \{show sigDecl}"
+
+  let (Ref _ tconName _, args) := funArgs codomain
+    | (tm, _) => error tyFC "\{pprint [] codomain} doesn't appear to be a TCon application"
+  let (Just (MkEntry _ name type (TCon cons))) = lookup tconName top
+    | _ => error tyFC "\{tconName} is not a type constructor"
+  let [con] = cons
+    | _ => error tyFC "\{tconName} has multiple constructors \{show cons}"
+  let (Just (MkEntry _ _ dcty (DCon _ _))) = lookup con top
+    | _ => error tyFC "can't find constructor \{show con}"
+  vdcty@(VPi _ nm icit rig a b) <- eval [] CBN dcty
+    | x => error (getFC x) "dcty not Pi"
+  debug "dcty \{pprint [] dcty}"
+  let (_,args) = funArgs codomain
+
+  debug "traverse \{show $ map showTm args}"
+  -- This is a little painful because we're reverse engineering the
+  -- individual types back out from the composite type
+  args' <- traverse (eval env CBN) args
+  debug "args' is \{show args'}"
+  conTele <- getFields !(apply vdcty args') env []
+  -- declare individual functions, collect their defs
+  defs <- for conTele $ \case
+     (MkBinder fc nm Explicit rig ty) => do
+       let ty' = foldr (\(MkBinder fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele
+       let nm' = "\{instname},\{nm}"
+       -- we're working with a Tm, so we define directly instead of processDecl
+       let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls
+          | _ => error instfc "no definition for \{nm}"
+
+       setDef (QN ns nm') fc ty' Axiom
+       let decl = (Def fc nm' xs)
+       putStrLn "***"
+       putStrLn "«\{nm'}» : \{pprint [] ty'}"
+       putStrLn $ render 80 $ pretty decl
+       pure $ Just decl
+     _ => pure Nothing
+
+  for_ (mapMaybe id defs) $ \decl => do
+    -- debug because already printed above, but nice to have it near processing
+    debug $ render 80 $ pretty decl
+    processDecl ns decl
+  let (QN _ con') = con
+  let decl = Def instfc instname [(RVar instfc instname, mkRHS instname conTele (RVar instfc con'))]
+  putStrLn "SIGDECL"
+  putStrLn "\{pretty sigDecl}"
+  putStrLn $ render 80 $ pretty decl
+  processDecl ns decl
+  where
+    -- try to extract types of individual fields from the typeclass dcon
+    -- We're assuming they don't depend on each other.
+    getFields : Val -> Env -> List Binder -> M (List Binder)
+    getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do
+      bnd <- MkBinder fc nm Explicit rig <$> quote (length env) ty
+      getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds)
+    getFields tm@(VPi fc nm _ rig ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds
+    getFields tm xs bnds = pure $ reverse bnds
+
+    tenv : Nat -> Env
+    tenv Z = []
+    tenv (S k) = (VVar emptyFC k [<] :: tenv k)
+
+    mkRHS : String -> List Binder -> Raw -> Raw
+    mkRHS instName (MkBinder fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit)
+    mkRHS instName (b :: bs) tm = mkRHS instName bs tm
+    mkRHS instName [] tm = tm
+
+    apply : Val -> List Val -> M Val
+    apply x [] = pure x
+    apply (VPi fc nm icit rig a b) (x :: xs) = apply !(b $$ x) xs
+    apply x (y :: xs) = error instfc "expected pi type \{show x}"
+
+processDecl ns (ShortData fc lhs sigs) = do
+  (nm,args) <- getArgs lhs []
+  let ty = foldr (\ (fc,n), a => (RPi fc (BI fc n Explicit Zero) (RU fc) a)) (RU fc) args
+  cons <- traverse (mkDecl args []) sigs
+  let dataDecl = Data fc nm ty cons
+  putStrLn "SHORTDATA"
+  putStrLn "\{pretty dataDecl}"
+  processDecl ns dataDecl
+  where
+    getArgs : Raw -> List (FC, String) -> M (String, List (FC, String))
+    getArgs (RVar fc1 nm) acc = pure (nm, acc)
+    getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc)
+    getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}"
+
+    mkDecl : List (FC, Name) -> List Raw -> Raw -> M Decl
+    mkDecl args acc (RVar fc' name) = do
+      let base = foldr (\ ty, acc => RPi (getFC ty) (BI (getFC ty) "_" Explicit Many) ty acc) lhs acc
+      let ty = foldr (\ (fc,nm), acc => RPi fc (BI fc nm Implicit Zero) (RU fc) acc) base args
+      pure $ TypeSig fc' [name] ty
+    mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t
+    mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}"
+
+processDecl ns (Data fc nm ty cons) = do
+  putStrLn "-----"
+  putStrLn "Data \{nm}"
+  top <- get
+  mc <- readIORef top.metaCtx
+  tyty <- check (mkCtx fc) ty (VU fc)
+  case lookupRaw nm top of
+    Just (MkEntry _ name type Axiom) => do
+      unifyCatch fc (mkCtx fc) !(eval [] CBN tyty) !(eval [] CBN type)
+    Just (MkEntry _ name type _) => error fc "\{show nm} already declared"
+    Nothing => setDef (QN ns nm) fc tyty Axiom
+  cnames <- for cons $ \x => case x of
+      (TypeSig fc names tm) => do
+          debug "check dcon \{show names} \{show tm}"
+          dty <- check (mkCtx fc) tm (VU fc)
+          debug "dty \{show names} is \{pprint [] dty}"
+
+          -- We only check that codomain uses the right type constructor
+          -- We know it's in U because it's part of a checked Pi type
+          let (codomain, tele) = splitTele dty
+          -- for printing
+          let tnames = reverse $ map (\(MkBinder _ nm _ _ _) => nm) tele
+          let (Ref _ hn _, args) := funArgs codomain
+            | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}"
+          when (hn /= QN ns nm) $
+            error (getFC codomain) "Constructor codomain is \{pprint tnames codomain} rather than \{nm}"
+
+          for_ names $ \ nm' => do
+            setDef (QN ns nm') fc dty (DCon (getArity dty) hn)
+          pure $ map (QN ns) names
+      decl => throwError $ E (getFC decl) "expected constructor declaration"
+  putStrLn "setDef \{nm}  TCon \{show $ join cnames}"
+  updateDef (QN ns nm) fc tyty (TCon (join cnames))
+  -- logMetas mstart
+  where
+    checkDeclType : Tm -> M ()
+    checkDeclType (UU _) = pure ()
+    checkDeclType (Pi _ str icit rig t u) = checkDeclType u
+    checkDeclType _ = error fc "data type doesn't return U"
+
+processDecl ns (Record recordFC nm tele cname decls) = do
+  putStrLn "-----"
+  putStrLn "Record"
+  let fields = getSigs decls
+  let dcName = fromMaybe "Mk\{nm}" cname
+  let tcType = teleToPi tele (RU recordFC)
+  -- REVIEW - I probably want to stick the telescope in front of the fields
+  let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele
+  let dcType = teleToPi (impTele tele) $
+    foldr (\(fc, nm, ty), acc =>  RPi fc (BI fc nm Explicit Many) ty acc  ) tail fields
+
+  putStrLn "tcon type \{pretty tcType}"
+  putStrLn "dcon type \{pretty dcType}"
+  let decl = Data recordFC nm tcType [TypeSig recordFC [dcName] dcType]
+  putStrLn "Decl:"
+  putStrLn $ render 90 $ pretty decl
+  processDecl ns decl
+  for_ fields $ \ (fc,name,ty) => do
+    -- TODO dependency isn't handled yet
+    -- we'll need to replace stuff like `len` with `len self`.
+    let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Explicit Many) tail ty
+    let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields
+
+    -- `fieldName` - consider dropping to keep namespace clean
+    -- let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
+    -- let lhs = RApp recordFC lhs autoPat Explicit
+    -- let decl = Def fc name [(lhs, (RVar fc name))]
+    -- putStrLn "\{name} : \{pretty funType}"
+    -- putStrLn "\{pretty decl}"
+    -- processDecl ns $ TypeSig fc [name] funType
+    -- processDecl ns decl
+
+    -- `.fieldName`
+    let pname = "." ++ name
+    let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele
+    let lhs = RApp recordFC lhs autoPat Explicit
+    let pdecl = Def fc pname [(lhs, (RVar fc name))]
+    putStrLn "\{pname} : \{pretty funType}"
+    putStrLn "\{pretty pdecl}"
+    processDecl ns $ TypeSig fc [pname] funType
+    processDecl ns pdecl

orig/Lib/Syntax.idr

@@ -0,0 +1,316 @@
+module Lib.Syntax
+
+import Data.String
+import Data.Maybe
+import Lib.Prettier
+import Lib.Types
+
+public export
+data Raw : Type
+
+public export
+data Pattern
+  = PatVar FC Icit Name
+  | PatCon FC Icit QName (List Pattern) (Maybe Name)
+  | PatWild FC Icit
+  -- Not handling this yet, but we need to be able to work with numbers and strings...
+  | PatLit FC Literal
+
+export
+getIcit : Pattern -> Icit
+getIcit (PatVar x icit str) = icit
+getIcit (PatCon x icit str xs as) = icit
+getIcit (PatWild x icit) = icit
+getIcit (PatLit fc lit) = Explicit
+
+
+export
+HasFC Pattern where
+  getFC (PatVar fc _ _) = fc
+  getFC (PatCon fc _ _ _ _) = fc
+  getFC (PatWild fc _) = fc
+  getFC (PatLit fc lit) = fc
+
+-- %runElab deriveShow `{Pattern}
+public export
+Constraint : Type
+Constraint = (String, Pattern)
+
+public export
+record Clause where
+  constructor MkClause
+  clauseFC : FC
+  -- I'm including the type of the left, so we can check pats and get the list of possibilities
+  -- But maybe rethink what happens on the left.
+  -- It's a VVar k or possibly a pattern.
+  -- a pattern either is zipped out, dropped (non-match) or is assigned to rhs
+  -- if we can do all three then we can have a VVar here.
+  cons : List Constraint
+  pats : List Pattern
+  -- We'll need some context to typecheck this
+  -- it has names from Pats, which will need types in the env
+  expr : Raw
+
+-- could be a pair, but I suspect stuff will be added?
+public export
+data RCaseAlt = MkAlt Raw Raw
+
+public export
+data DoStmt : Type where
+  DoExpr : (fc : FC) -> Raw -> DoStmt
+  DoLet : (fc : FC) -> String -> Raw -> DoStmt
+  DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
+
+data Decl : Type
+data Raw : Type where
+  RVar : (fc : FC) -> (nm : Name) -> Raw
+  RLam : (fc : FC) -> BindInfo -> (ty : Raw) -> Raw
+  RApp : (fc : FC) -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw
+  RU   : (fc : FC) -> Raw
+  RPi  : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw
+  RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
+  RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw
+  RLit : (fc : FC) -> Literal -> Raw
+  RCase : (fc : FC) -> (scrut : Raw) -> (alts : List RCaseAlt) -> Raw
+  RImplicit : (fc : FC) -> Raw
+  RHole : (fc : FC) -> Raw
+  RDo : (fc : FC) -> List DoStmt -> Raw
+  RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw
+  RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw
+  RAs : (fc : FC) -> Name -> Raw -> Raw
+
+%name Raw tm
+
+
+export
+HasFC Raw where
+  getFC (RVar fc nm) = fc
+  getFC (RLam fc _ ty) = fc
+  getFC (RApp fc t u icit) = fc
+  getFC (RU fc) = fc
+  getFC (RPi fc _ ty sc) = fc
+  getFC (RLet fc nm ty v sc) = fc
+  getFC (RAnn fc tm ty) = fc
+  getFC (RLit fc y) = fc
+  getFC (RCase fc scrut alts) = fc
+  getFC (RImplicit fc) = fc
+  getFC (RHole fc) = fc
+  getFC (RDo fc stmts) = fc
+  getFC (RIf fc _ _ _) = fc
+  getFC (RWhere fc _ _) = fc
+  getFC (RAs fc _ _) = fc
+
+
+-- derive some stuff - I'd like json, eq, show, ...
+
+
+
+public export
+data Import = MkImport FC Name
+
+
+public export
+Telescope : Type
+Telescope = List (BindInfo, Raw)
+
+public export
+data Decl
+  = TypeSig FC (List Name) Raw
+  | Def FC Name (List (Raw, Raw)) -- (List Clause)
+  | DCheck FC Raw Raw
+  | Data FC Name Raw (List Decl)
+  | ShortData FC Raw (List Raw)
+  | PType FC Name (Maybe Raw)
+  | PFunc FC Name (List String) Raw String
+  | PMixFix FC (List Name) Nat Fixity
+  | Class FC Name Telescope (List Decl)
+  | Instance FC Raw (Maybe (List Decl))
+  | Record FC Name Telescope (Maybe Name) (List Decl)
+
+public export
+HasFC Decl where
+  getFC (TypeSig x strs tm) = x
+  getFC (Def x str xs) = x
+  getFC (DCheck x tm tm1) = x
+  getFC (Data x str tm xs) = x
+  getFC (ShortData x _ _) = x
+  getFC (PType x str mtm) = x
+  getFC (PFunc x str _ tm str1) = x
+  getFC (PMixFix x strs k y) = x
+  getFC (Class x str xs ys) = x
+  getFC (Instance x tm xs) = x
+  getFC (Record x str tm str1 xs) = x
+
+public export
+record Module where
+  constructor MkModule
+  modname : Name
+  imports : List Import
+  decls : List Decl
+
+foo : List String -> String
+foo ts = "(" ++ unwords ts ++ ")"
+
+-- Show Literal where
+--   show (LString str) = foo [ "LString", show str]
+--   show (LInt i) = foo [ "LInt", show i]
+--   show (LChar c) = foo [ "LChar", show c]
+
+export
+covering
+implementation Show Raw
+
+export
+implementation Show Decl
+
+export Show Pattern
+
+export
+covering
+Show Clause where
+  show (MkClause fc cons pats expr) = show (fc, cons, pats, expr)
+
+Show Import where
+  show (MkImport _ str) = foo ["MkImport", show str]
+
+Show BindInfo where
+  show (BI _ nm icit quant) = foo ["BI", show nm, show icit, show quant]
+
+-- this is for debugging, use pretty when possible
+covering
+Show Decl where
+  show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
+  show (Def _ str clauses) = foo ["Def", show str, show clauses]
+  show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
+  show (DCheck _ x y) = foo ["DCheck", show x, show y]
+  show (PType _ name ty) = foo ["PType", name, show ty]
+  show (ShortData _ lhs sigs) = foo ["ShortData", show lhs, show sigs]
+  show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src]
+  show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
+  show (Class _ nm tele decls) = foo ["Class",  nm, "...", (show $ map show decls)]
+  show (Instance _ nm decls) = foo ["Instance",  show nm, (show $ map show decls)]
+  show (Record _ nm tele nm1 decls) = foo ["Record", show nm, show tele, show nm1, show decls]
+
+export covering
+Show Module where
+  show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
+
+export
+covering
+Show Pattern where
+  show (PatVar _ icit str) = foo ["PatVar", show icit, show str]
+  show (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, show xs, show as]
+  show (PatWild _ icit) = foo ["PatWild", show icit]
+  show (PatLit _ lit) = foo ["PatLit", show lit]
+
+covering
+Show RCaseAlt where
+  show (MkAlt x y)= foo ["MkAlt", show x, show y]
+
+covering
+Show Raw where
+  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]
+  show (RLet _ x ty v scope) = foo [ "Let", show x, " : ", show ty, " = ", show v, " in ", show scope]
+  show (RPi _ bi y z) = foo [ "Pi", show bi, show y, show z]
+  show (RApp _ x y z) = foo [ "App", show x, show y, show z]
+  show (RLam _ bi y) = foo [ "Lam", show bi, show y]
+  show (RCase _ x xs) = foo [ "Case", show x, show xs]
+  show (RDo _ stmts) = foo [ "DO", "FIXME"]
+  show (RU _) = "U"
+  show (RIf _ x y z) = foo [ "If", show x, show y, show z]
+  show (RWhere _ _ _) = foo [ "Where", "FIXME"]
+  show (RAs _ nm x) = foo [ "RAs", nm, show x]
+
+export
+Pretty Literal where
+  pretty (LString str) = text $ interpolate str
+  pretty (LInt i) = text $ show i
+  pretty (LChar c) = text $ show c
+
+export
+Pretty Pattern where
+  -- FIXME - wrap Implicit with {}
+  pretty (PatVar _ icit nm) = text nm
+  pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args)
+  pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")"
+  pretty (PatWild _ icit) = text "_"
+  pretty (PatLit _ lit) = pretty lit
+
+wrap : Icit -> Doc -> Doc
+wrap Explicit x = text "(" ++ x ++ text ")"
+wrap Implicit x = text "{" ++ x ++ text "}"
+wrap Auto x = text "{{" ++ x ++ text "}}"
+
+export
+Pretty Raw where
+  pretty = asDoc 0
+    where
+    bindDoc : BindInfo -> Doc
+    bindDoc (BI _ nm icit quant) = ?rhs_0
+
+    par : Nat -> Nat -> Doc -> Doc
+    par p p' d = if p' < p then text "(" ++ d ++ text ")" else d
+
+    asDoc : Nat -> Raw -> Doc
+    asDoc p (RVar _ str) = text str
+    asDoc p (RLam _ (BI _ nm icit q) x) = par p 0 $ text "\\" ++ wrap icit (text nm) <+> text "=>" <+> asDoc 0 x
+    -- This needs precedence and operators...
+    asDoc p (RApp _ x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y
+    asDoc p (RApp _ x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
+    asDoc p (RApp _ x y Auto) = par p 2 $ asDoc 2 x <+> text "{{" ++ asDoc 0 y ++ text "}}"
+    asDoc p (RU _) = text "U"
+    asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
+    asDoc p (RPi _ (BI _ nm icit quant) ty scope) =
+      par p 1 $ wrap icit (text (show quant ++ nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope
+    asDoc p (RLet _ x v ty scope) =
+      par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty
+          <+> text "=" <+> asDoc p v
+          <+/> text "in" <+> asDoc p scope
+    -- does this exist?
+    asDoc p (RAnn _ x y) = text "TODO - RAnn"
+    asDoc p (RLit _ lit) = pretty lit
+    asDoc p (RCase _ x xs) = text "TODO - RCase"
+    asDoc p (RImplicit _) = text "_"
+    asDoc p (RHole _) = text "?"
+    asDoc p (RDo _ stmts) = text "TODO - RDo"
+    asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z
+    asDoc p (RWhere _ dd b) = text "TODO pretty where"
+    asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")"
+
+prettyBind : (BindInfo, Raw) -> Doc
+prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)
+
+pipeSep : List Doc -> Doc
+pipeSep = folddoc (\a, b => a <+/> text "|" <+> b)
+
+export
+Pretty Decl where
+  pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
+  pretty (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> text "=" <+> pretty b) clauses
+  pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs))
+  pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y
+  pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty)
+  pretty (PFunc _ nm [] ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
+  pretty (PFunc _ nm uses ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text uses) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
+  pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
+  pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+    <+> (nest 2 $ text "where" </> stack (maybe empty (\ nm' => text "constructor" <+> text nm') cname :: map pretty decls))
+  pretty (Class _ nm tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+    <+> (nest 2 $ text "where" </> stack (map pretty decls))
+  pretty (Instance _ _ _) = text "TODO pretty Instance"
+  pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs)
+
+export
+Pretty Module where
+  pretty (MkModule name imports decls) =
+    text "module" <+> text name
+      </> stack (map doImport imports)
+      </> stack (map pretty decls)
+      where
+        doImport : Import -> Doc
+        doImport (MkImport _ nm) = text "import" <+> text nm ++ line
+

orig/Lib/Token.idr

@@ -0,0 +1,103 @@
+module Lib.Token
+
+public export
+record Bounds where
+  constructor MkBounds
+  startLine : Int
+  startCol : Int
+  endLine : Int
+  endCol : Int
+
+export
+Eq Bounds where
+  (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
+      sl == sl'
+   && sc == sc'
+   && el == el'
+   && ec == ec'
+
+public export
+record WithBounds ty where
+  constructor MkBounded
+  val : ty
+  bounds : Bounds
+
+public export
+data Kind
+  = Ident
+  | UIdent
+  | Keyword
+  | MixFix
+  | Number
+  | Character
+  | StringKind
+  | JSLit
+  | Symbol
+  | Space
+  | Comment
+  | Pragma
+  | Projection
+  -- not doing Layout.idr
+  | LBrace
+  | Semi
+  | RBrace
+  | EOI
+  | StartQuote
+  | EndQuote
+  | StartInterp
+  | EndInterp
+
+export
+Show Kind where
+  show Ident   = "Ident"
+  show UIdent   = "UIdent"
+  show Keyword = "Keyword"
+  show MixFix = "MixFix"
+  show Number  = "Number"
+  show Character  = "Character"
+  show Symbol  = "Symbol"
+  show Space  = "Space"
+  show LBrace  = "LBrace"
+  show Semi    = "Semi"
+  show RBrace  = "RBrace"
+  show Comment = "Comment"
+  show EOI     = "EOI"
+  show Pragma  = "Pragma"
+  show StringKind = "String"
+  show JSLit = "JSLit"
+  show Projection = "Projection"
+  show StartQuote = "StartQuote"
+  show EndQuote = "EndQuote"
+  show StartInterp = "StartInterp"
+  show EndInterp = "EndInterp"
+
+export
+Eq Kind where
+  a == b = show a == show b
+
+public export
+record Token where
+  constructor Tok
+  kind : Kind
+  text : String
+
+
+export
+Show Token where
+  show (Tok k v) = "<\{show k}:\{show v}>"
+
+public export
+BTok : Type
+BTok = WithBounds Token
+
+export
+value : BTok -> String
+value (MkBounded (Tok _ s) _) = s
+
+export
+kind : BTok -> Kind
+kind (MkBounded (Tok k s) _) = k
+
+export
+getStart : BTok -> (Int, Int)
+getStart (MkBounded _ (MkBounds l c _ _)) = (l,c)

orig/Lib/Tokenizer.idr

@@ -0,0 +1,161 @@
+module Lib.Tokenizer
+
+-- Working alternate tokenizer, saves about 2k, can be translated to newt
+
+-- Currently this processes a stream of characters, I may switch it to
+-- combinators for readability in the future.
+
+import Lib.Token
+import Lib.Common
+import Data.String
+
+standalone : List Char
+standalone = unpack "()\\{}[,.@]"
+
+keywords : List String
+keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
+            "ptype", "pfunc", "module", "infixl", "infixr", "infix",
+            "∀", "forall", "import", "uses",
+            "class", "instance", "record", "constructor",
+            "if", "then", "else",
+            -- it would be nice to find a way to unkeyword "." so it could be
+            -- used as an operator too
+            "$", "λ", "?", "@", ".",
+             "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]
+
+record TState where
+  constructor TS
+  trow : Int
+  tcol : Int
+  acc : SnocList BTok
+  chars : List Char
+
+-- This makes a big case tree...
+rawTokenise : TState -> Either Error TState
+
+quoteTokenise : TState -> Int -> Int -> SnocList Char -> Either Error TState
+quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of
+  '"' :: cs => Right (TS el ec (toks :< stok) chars)
+  '\\' :: '{' :: cs => do
+    let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2))
+    (TS el ec toks chars) <- rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs
+    case chars of
+      '}' :: cs =>
+        let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1))
+        in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) [<]
+      cs => Left $ E (MkFC "" (el, ec)) "Expected '{'"
+  -- TODO newline in string should be an error
+  '\n' :: cs => Left $ E (MkFC "" (el, ec)) "Newline in string"
+  '\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n')
+  '\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c)
+  c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c)
+  Nil => Left $ E (MkFC "" (el, ec)) "Expected '\"' at EOF"
+
+  where
+    stok : BTok
+    stok = MkBounded (Tok StringKind (pack $ acc <>> [])) (MkBounds startl startc el ec)
+
+
+
+rawTokenise ts@(TS sl sc toks chars) = case chars of
+  Nil => Right $ ts
+  ' ' :: cs => rawTokenise (TS sl (sc + 1) toks cs)
+  '\n' :: cs => rawTokenise (TS (sl + 1) 0 toks cs)
+
+  '"' :: cs => do
+    let tok = mktok False sl (sc + 1) StartQuote "\""
+    (TS sl sc toks chars) <- quoteTokenise (TS sl (sc + 1) (toks :< tok) cs) sl (sc + 1) [<]
+    case chars of
+      '"' :: cs => let tok = mktok False sl (sc + 1) EndQuote "\"" in
+        rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
+      cs => Left $ E (MkFC "" (sl, sc)) "Expected '\"'"
+
+  '{' :: '{' :: cs => do
+    let tok = mktok False sl (sc + 2) Keyword "{{"
+    (TS sl sc toks chars) <- rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
+    case chars of
+      '}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in
+        rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
+      cs => Left $ E (MkFC "" (sl, sc)) "Expected '}}'"
+
+  '}' :: cs => Right ts
+  '{' :: cs => do
+    let tok = mktok False sl (sc + 1) Symbol "{"
+    (TS sl sc toks chars) <- rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
+    case chars of
+      '}' :: cs => let tok = mktok False sl (sc + 1) Symbol "}" in
+        rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
+      cs => Left $ E (MkFC "" (sl, sc)) "Expected '}'"
+
+  ',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs)
+  '_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs)
+  '_' :: '.' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_._") cs)
+  '\'' :: '\\' :: c :: '\'' :: cs =>
+    let ch = ifThenElse (c == 'n') '\n' c
+    in rawTokenise (TS sl (sc + 4) (toks :< mktok False sl (sc + 4) Character (singleton ch)) cs)
+  '\'' :: c :: '\'' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) Character (singleton c)) cs)
+  '#' :: cs => doRest (TS sl (sc + 1) toks cs) Pragma isIdent (Lin :< '#')
+  '-' :: '-' :: cs => lineComment (TS sl (sc + 2) toks cs)
+  '/' :: '-' :: cs => blockComment (TS sl (sc + 2) toks cs)
+  '`' :: cs => doBacktick (TS sl (sc + 1) toks cs) [<]
+  '.' :: cs => doRest (TS sl (sc + 1) toks cs) Projection isIdent (Lin :< '.')
+  '-' :: c :: cs => if isDigit c
+    then doRest (TS sl (sc + 2) toks cs) Number isDigit (Lin :< '-' :< c)
+    else doRest (TS sl (sc + 1) toks (c :: cs)) Ident isIdent (Lin :< '-')
+
+  c :: cs => doChar c cs
+
+  where
+    isIdent : Char -> Bool
+    isIdent c = not (isSpace c || elem c standalone)
+
+    isUIdent : Char -> Bool
+    isUIdent c = isIdent c || c == '.'
+
+    doBacktick : TState -> SnocList Char -> Either Error TState
+    doBacktick (TS l c toks Nil) acc = Left $ E (MkFC "" (l,c)) "EOF in backtick string"
+    doBacktick (TS el ec toks ('`' :: cs)) acc =
+      let tok = MkBounded (Tok JSLit (pack $ acc <>> [])) (MkBounds sl sc el ec) in
+      rawTokenise (TS el (ec + 1) (toks :< tok) cs)
+    doBacktick (TS l c toks ('\n' :: cs)) acc = doBacktick (TS (l + 1) 0 toks cs) (acc :< '\n')
+    doBacktick (TS l c toks (ch :: cs)) acc = doBacktick (TS l (c + 1) toks cs) (acc :< ch)
+
+
+    -- temporary use same token as before
+    mktok : Bool -> Int -> Int -> Kind -> String -> BTok
+    mktok checkkw el ec kind text = let kind = if checkkw && elem text keywords then Keyword else kind in
+      MkBounded (Tok kind text) (MkBounds sl sc el ec)
+
+    lineComment : TState -> Either Error TState
+    lineComment (TS line col toks Nil) = rawTokenise (TS line col toks Nil)
+    lineComment (TS line col toks ('\n' :: cs)) = rawTokenise (TS (line + 1) 0 toks cs)
+    lineComment (TS line col toks (c :: cs)) = lineComment (TS line (col + 1) toks cs)
+
+    blockComment : TState -> Either Error TState
+    blockComment (TS line col toks Nil) = Left $ E (MkFC "" (line, col)) "EOF in block comment"
+    blockComment (TS line col toks ('-' :: '/' :: cs)) = rawTokenise (TS line (col + 2) toks cs)
+    blockComment (TS line col toks ('\n' :: cs)) = blockComment (TS (line + 1) 0 toks cs)
+    blockComment (TS line col toks (c :: cs)) = blockComment (TS line (col + 1) toks cs)
+
+    doRest : TState -> Kind -> (Char -> Bool) -> SnocList Char -> Either Error TState
+    doRest (TS l c toks Nil) kind pred acc = rawTokenise (TS l c (toks :< mktok True l c kind (pack $ acc <>> [])) Nil)
+    doRest (TS l c toks (ch :: cs)) kind pred acc = if pred ch
+      then doRest (TS l (c + 1) toks cs) kind pred (acc :< ch)
+      else
+        let kind = if elem '_' acc then MixFix else kind in
+        rawTokenise (TS l c (toks :< mktok True l (c - 1) kind (pack $ acc <>> [])) (ch :: cs))
+
+    doChar : Char -> List Char ->  Either Error TState
+    doChar c cs = if elem c standalone
+      then rawTokenise (TS sl (sc + 1) (toks :< mktok True sl (sc + 1) Symbol (singleton c)) cs)
+      else let kind = if isDigit c then Number else if isUpper c then UIdent else Ident in
+        doRest (TS sl sc toks (c :: cs)) kind isIdent [<]
+
+export
+tokenise : String -> String -> Either Error (List BTok)
+tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of
+  Right (TS trow tcol acc []) => Right $ acc <>> []
+  Right (TS trow tcol acc chars) => Left $ E (MkFC fn (trow, tcol)) "Extra toks"
+  Left (E (MkFC file start) str) => Left $ E (MkFC fn start) str
+  Left err => Left err
+

orig/Lib/TopContext.idr

@@ -0,0 +1,54 @@
+module Lib.TopContext
+
+import Data.IORef
+import Data.SortedMap
+import Data.String
+import Lib.Types
+
+-- 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 : QName -> TopContext -> Maybe TopEntry
+lookup nm top = lookup nm top.defs
+
+-- TODO - look at imported namespaces, and either have a map of imported names or search imported namespaces..
+export
+lookupRaw : String -> TopContext -> Maybe TopEntry
+lookupRaw raw top = go $ toList top.defs
+  where
+    go : List (QName, TopEntry) -> Maybe TopEntry
+    go Nil = Nothing
+    go (((QN ns nm), entry) :: rest) = if nm == raw then Just entry else go rest
+
+-- Maybe pretty print?
+export
+covering
+Show TopContext where
+  show (MkTop defs metas _ _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map (show . snd) $ toList defs}]"
+
+public export
+empty : HasIO m => m TopContext
+empty = pure $ MkTop empty !(newIORef (MC [] 0 CheckAll)) False !(newIORef []) [] empty
+
+public export
+setDef : QName -> FC -> Tm -> Def -> M ()
+setDef name fc ty def = do
+  top <- get
+  let Nothing = lookup name top.defs
+    | Just (MkEntry fc' nm' ty' def') => error fc "\{name} is already defined at \{show fc'}"
+  put $ { defs $= (insert name (MkEntry fc name ty def)) } top
+
+public export
+updateDef : QName -> FC -> Tm -> Def -> M ()
+updateDef name fc ty def = do
+  top <- get
+  let Just (MkEntry fc' nm' ty' def') = lookup name top.defs
+    | Nothing => error fc "\{name} not declared"
+  put $ { defs $= (insert name (MkEntry fc' name ty def)) } top
+
+public export
+addError : Error -> M ()
+addError err = do
+  top <- get
+  modifyIORef top.errors (err ::)

orig/Lib/Types.idr

@@ -0,0 +1,599 @@
+module Lib.Types
+
+-- For FC, Error
+import public Lib.Common
+import public Lib.Prettier
+
+import Data.Fin
+import Data.IORef
+import Data.List
+import Data.SnocList
+import Data.SortedMap
+import Data.String
+import Data.Vect
+
+public export
+data QName : Type where
+  QN : List String -> String -> QName
+
+public export
+Eq QName where
+  QN ns n == QN ns' n' = n == n' && ns == ns'
+
+public export
+Show QName where
+  show (QN [] n) = n
+  show (QN ns n) = joinBy "." ns ++ "." ++ n
+
+public export
+Interpolation QName where
+  interpolate = show
+
+export
+Ord QName where
+  compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
+
+
+public export
+Name : Type
+Name = String
+
+public export
+data Icit = Implicit | Explicit | Auto
+
+%name Icit icit
+
+export
+Show Icit where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+  show Auto = "Auto"
+
+public export
+data BD = Bound | Defined
+
+public export
+Eq BD where
+  Bound == Bound = True
+  Defined == Defined = True
+  _ == _ = False
+
+public export
+Show BD where
+  show Bound = "bnd"
+  show Defined = "def"
+
+public export
+data Quant = Zero | Many
+
+public export
+Show Quant where
+  show Zero = "0 "
+  show Many = ""
+
+Eq Quant where
+  Zero == Zero = True
+  Many == Many = True
+  _ == _ = False
+
+-- We could make this polymorphic and use for environment...
+public export
+data BindInfo : Type where
+  BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo
+
+%name BindInfo bi
+
+public export
+HasFC BindInfo where
+  getFC (BI fc _ _ _) = fc
+
+public export
+data Tm : Type
+
+public export
+data Literal = LString String | LInt Int | LChar Char
+
+%name Literal lit
+
+public export
+Show Literal where
+  show (LString str) = show str
+  show (LInt i) = show i
+  show (LChar c) = show c
+
+public export
+data CaseAlt : Type where
+  CaseDefault : Tm -> CaseAlt
+  CaseCons : (name : QName) -> (args : List String) -> Tm ->  CaseAlt
+  CaseLit : Literal -> Tm ->  CaseAlt
+
+data Def : Type
+
+
+public export
+Eq Literal where
+  LString x == LString y = x == y
+  LInt x == LInt y = x == y
+  LChar x == LChar y = x == y
+  _ == _ = False
+
+data Tm : Type where
+  Bnd : FC -> Nat -> Tm
+  -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
+  Ref : FC -> QName -> Def -> Tm
+  Meta : FC -> Nat -> Tm
+  -- kovacs optimization, I think we can App out meta instead
+  -- InsMeta : Nat -> List BD -> Tm
+  Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm
+  App : FC -> Tm -> Tm -> Tm
+  UU   : FC -> Tm
+  Pi  : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm
+  Case : FC -> Tm -> List CaseAlt -> Tm
+  -- need type?
+  Let : FC -> Name -> Tm -> Tm -> Tm
+  -- for desugaring where
+  LetRec : FC -> Name -> Tm -> Tm -> Tm -> Tm
+  Lit : FC -> Literal -> Tm
+  Erased : FC -> Tm
+
+%name Tm t, u, v
+
+export
+HasFC Tm where
+  getFC (Bnd fc k) = fc
+  getFC (Ref fc str x) = fc
+  getFC (Meta fc k) = fc
+  getFC (Lam fc str _ _ t) = fc
+  getFC (App fc t u) = fc
+  getFC (UU fc) = fc
+  getFC (Pi fc str icit quant t u) = fc
+  getFC (Case fc t xs) = fc
+  getFC (Lit fc _) = fc
+  getFC (Let fc _ _ _) = fc
+  getFC (LetRec fc _ _ _ _) = fc
+  getFC (Erased fc) = fc
+
+covering
+Show Tm
+
+public export
+covering
+Show CaseAlt where
+  show (CaseDefault tm) = "_ => \{show tm}"
+  show (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}"
+  show (CaseLit lit tm) = "\{show lit} => \{show tm}"
+
+public export
+covering
+Show Tm where
+  show (Bnd _ k) = "(Bnd \{show k})"
+  show (Ref _ str _) = "(Ref \{show str})"
+  show (Lam _ nm icit rig t) = "(\\ \{show rig}\{nm}  => \{show  t})"
+  show (App _ t u) = "(\{show t} \{show u})"
+  show (Meta _ i) = "(Meta \{show i})"
+  show (Lit _ l) = "(Lit \{show l})"
+  show (UU _) = "U"
+  show (Pi _ str Explicit rig t u) = "(Pi (\{show rig}\{str} : \{show t}) => \{show u})"
+  show (Pi _ str Implicit rig t u) = "(Pi {\{show rig}\{str} : \{show t}} => \{show u})"
+  show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})"
+  show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
+  show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
+  show (LetRec _ nm ty t u) = "(LetRec \{nm} : \{show ty} \{show t} \{show u})"
+  show (Erased _) = "ERASED"
+
+public export
+showTm : Tm -> String
+showTm = show
+
+-- I can't really show val because it's HOAS...
+
+-- TODO derive
+export
+Eq Icit where
+  Implicit == Implicit = True
+  Explicit == Explicit = True
+  Auto == Auto = 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 _ _ t) == Lam _ n' _ _ t' = t == t'
+  (App _ t u) == App _ t' u' = t == t' && u == u'
+  (UU _) == (UU _) = True
+  (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u'
+  _ == _ = False
+
+
+
+-- TODO App and Lam should have <+/> but we need to fix
+-- INFO pprint to `nest 2 ...`
+-- maybe return Doc and have an Interpolation..
+-- If we need to flatten, case is going to get in the way.
+
+pprint' : Nat -> List String -> Tm -> Doc
+pprintAlt : Nat -> List String -> CaseAlt -> Doc
+pprintAlt p names (CaseDefault t) = text "_" <+> text "=>" <+> pprint' p ("_" :: names) t
+pprintAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ text "=>" <+/> pprint' p (reverse args ++ names) t)
+-- `;` is not in surface syntax, but sometimes we print on one line
+pprintAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ text "=>" <+/> pprint' p names t ++ text ";")
+
+parens : Nat -> Nat -> Doc -> Doc
+parens a b doc = if a < b
+  then text "(" ++ doc ++ text ")"
+  else doc
+
+pprint' p names (Bnd _ k) = case getAt k names of
+  -- Either a bug or we're printing without names
+  Nothing => text "BND:\{show k}"
+  Just nm => text "\{nm}:\{show k}"
+pprint' p names (Ref _ str mt) = text (show str)
+pprint' p names (Meta _ k) = text "?m:\{show k}"
+pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t
+pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u
+pprint' p names (UU _) = text "U"
+pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $
+  text "{{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}}" <+> text "->" <+> pprint' 0 (nm :: names) u
+pprint' p names (Pi _ nm Implicit rig t u) = parens 0 p $
+  text "{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}" <+> text "->" <+> pprint' 0 (nm :: names) u
+pprint' p names (Pi _ "_" Explicit Many t u) =
+  parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) u
+pprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $
+  text "(" ++  text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) u
+-- FIXME - probably way wrong on the names here.  There is implicit binding going on
+pprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts)))
+pprint' p names (Lit _ lit) = text (show lit)
+pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" </> (nest 2 $ pprint' 0 (nm :: names) u)
+pprint' p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> text ":" <+> pprint' 0 names ty <+> text ":=" <+> pprint' 0 names t <+> text "in" </> (nest 2 $ pprint' 0 (nm :: names) u)
+pprint' p names (Erased _) = text "ERASED"
+
+||| Pretty printer for Tm.
+export
+pprint : List String -> Tm -> Doc
+pprint names tm = pprint' 0 names tm
+
+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 : FC -> (k : Nat) -> (sp : SnocList Val) -> Val
+  VRef : FC -> (nm : QName) -> Def -> (sp : SnocList Val) -> Val
+  -- neutral case
+  VCase : FC -> (sc : Val) -> List CaseAlt -> Val
+  -- we'll need to look this up in ctx with IO
+  VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val
+  VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
+  VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val
+  VLet : FC -> Name -> Val -> Val -> Val
+  VLetRec : FC -> Name -> Val -> Val -> Val -> Val
+  VU : FC -> Val
+  VErased : FC -> Val
+  VLit : FC -> Literal -> Val
+
+public export
+Env : Type
+Env = List Val
+
+public export
+data Mode = CBN | CBV
+
+public export
+data Closure = MkClosure Env Tm
+
+public export
+getValFC : Val -> FC
+getValFC (VVar fc _ _) = fc
+getValFC (VRef fc _ _ _) = fc
+getValFC (VCase fc _ _) = fc
+getValFC (VMeta fc _ _) = fc
+getValFC (VLam fc _ _ _ _) = fc
+getValFC (VPi fc _ _ _ a b) = fc
+getValFC (VU fc) = fc
+getValFC (VErased fc) = fc
+getValFC (VLit fc _) = fc
+getValFC (VLet fc _ _ _) = fc
+getValFC (VLetRec fc _ _ _ _) = fc
+
+
+public export
+HasFC Val where getFC = getValFC
+
+Show Closure
+
+covering
+export
+Show Val where
+  show (VVar _ k [<]) = "%var\{show k}"
+  show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> [])})"
+  show (VRef _ nm _ [<]) = show nm
+  show (VRef _ nm _ sp) = "(\{show nm} \{unwords $ map show (sp <>> [])})"
+  show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ length sp} sp])"
+  show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{show x})"
+  show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{show  y})"
+  show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{show  y})"
+  show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show  x}}}. \{show  y})"
+  show (VCase fc sc alts) = "(%case \{show sc} ...)"
+  show (VU _) = "U"
+  show (VLit _ lit) = show lit
+  show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
+  show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}"
+  show (VErased _) = "ERASED"
+
+covering
+Show Closure where
+  show (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})"
+
+record Context
+
+public export
+data MetaKind = Normal | User | AutoSolve
+
+public export
+Show MetaKind where
+  show Normal = "Normal"
+  show User = "User"
+  show AutoSolve = "Auto"
+
+public export
+Eq MetaKind where
+  a == b = show a == show b
+
+
+-- constrain meta applied to val to be a val
+public export
+data MConstraint = MkMc FC Env (SnocList Val) Val
+
+public export
+data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved FC Nat Val
+
+public export
+data MetaMode = CheckAll | CheckFirst | NoCheck
+
+public export
+record MetaContext where
+  constructor MC
+  metas : List MetaEntry
+  next : Nat
+  mcmode : MetaMode
+
+public export
+data Def = Axiom | TCon (List QName) | DCon Nat QName | Fn Tm | PrimTCon
+         | PrimFn String (List String)
+
+public export
+covering
+Show Def where
+  show Axiom = "axiom"
+  show (TCon strs) = "TCon \{show strs}"
+  show (DCon k tyname) = "DCon \{show k} \{show tyname}"
+  show (Fn t) = "Fn \{show t}"
+  show (PrimTCon) = "PrimTCon"
+  show (PrimFn src used) = "PrimFn \{show src} \{show used}"
+
+||| entry in the top level context
+public export
+record TopEntry where
+  constructor MkEntry
+  fc : FC
+  name : QName
+  type : Tm
+  def : Def
+
+-- FIXME snoc
+
+export
+covering
+Show TopEntry where
+  show (MkEntry fc 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 : SortedMap QName TopEntry
+  metaCtx : IORef MetaContext
+  verbose : Bool -- command line flag
+  errors : IORef (List Error)
+  ||| loaded modules
+  loaded : List String
+  ops : Operators
+
+-- we'll use this for typechecking, but need to keep a TopContext around too.
+public export
+record Context where
+  [noHints]
+  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 : Vect lvl BD          -- bound or defined
+
+  -- FC to use if we don't have a better option
+  ctxFC : FC
+
+%name Context ctx
+
+||| add a binding to environment
+export
+extend : Context -> String -> Val -> Context
+extend ctx name ty =
+    { lvl $= S, env $= (VVar emptyFC ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
+
+-- I guess we define things as values?
+export
+define : Context -> String -> Val -> Val -> Context
+define ctx name val ty =
+  { lvl $= S, env $= (val ::), types $= ((name,ty) ::), bds $= (Defined ::) } ctx
+
+
+export
+covering
+Show MetaEntry where
+  show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}"
+  show (Solved _ k x) = "Solved \{show k} \{show x}"
+
+export
+withPos : Context -> FC -> Context
+withPos ctx fc = { ctxFC := fc } ctx
+
+export
+names : Context -> List String
+names ctx = toList $ map fst ctx.types
+
+-- public export
+-- M : Type -> Type
+-- M = (StateT TopContext (EitherT Error IO))
+
+public export
+record M a where
+  constructor MkM
+  runM : TopContext -> IO (Either Error (TopContext, a))
+
+export
+Functor M where
+  map f (MkM run) = MkM $ \tc => do
+    result <- run tc
+    case result of
+      Left err => pure $ Left err
+      Right (tc', a) => pure $ Right (tc', f a)
+
+export
+Applicative M where
+  pure x = MkM $ \tc => pure $ Right (tc, x)
+  (MkM f) <*> (MkM x) = MkM $ \tc => do
+    resultF <- f tc
+    case resultF of
+      Left err => pure $ Left err
+      Right (tc', f') => do
+        resultX <- x tc'
+        case resultX of
+          Left err => pure $ Left err
+          Right (tc'', x') => pure $ Right (tc'', f' x')
+
+export
+Monad M where
+  (MkM x) >>= f = MkM $ \tc => do
+    resultX <- x tc
+    case resultX of
+      Left err => pure $ Left err
+      Right (tc', a) => runM (f a) tc'
+
+export
+HasIO M where
+  liftIO io = MkM $ \tc => do
+    result <- io
+    pure $ Right (tc, result)
+
+export
+throwError : Error -> M a
+throwError err = MkM $ \_ => pure $ Left err
+
+export
+catchError : M a -> (Error -> M a) -> M a
+catchError (MkM ma) handler = MkM $ \tc => do
+  result <- ma tc
+  case result of
+    Left err => runM (handler err) tc
+    Right (tc', a) => pure $ Right (tc', a)
+
+export
+tryError : M a -> M (Either Error a)
+tryError ma = catchError (map Right ma) (pure . Left)
+
+export
+get : M TopContext
+get = MkM $ \ tc => pure $ Right (tc, tc)
+
+export
+put : TopContext -> M Unit
+put tc = MkM $ \_ => pure $ Right (tc, MkUnit)
+
+export
+modify : (TopContext -> TopContext) -> M Unit
+modify f = do
+  tc <- get
+  put (f tc)
+
+||| Force argument and print if verbose is true
+export
+debug : Lazy String -> M Unit
+debug x = do
+  top <- get
+  when top.verbose $ putStrLn $ Force x
+
+export
+info : FC -> String -> M Unit
+info fc msg = putStrLn "INFO at \{show fc}: \{msg}"
+
+||| Version of debug that makes monadic computation lazy
+export
+debugM : M String -> M Unit
+debugM x = do
+  top <- get
+  when top.verbose $ do putStrLn !(x)
+
+export
+Show Context where
+  show ctx = "Context \{show $ map fst $ ctx.types}"
+
+export
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (Postpone x k str) = str
+
+export
+HasFC Error where
+  getFC (E x str) = x
+  getFC (Postpone x k str) = x
+
+export
+error : FC -> String -> M a
+error fc msg = throwError $ E fc msg
+
+export
+error' : String -> M a
+error' msg = throwError $ E emptyFC msg
+
+
+export
+lookupMeta : Nat -> M MetaEntry
+lookupMeta ix = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  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
+
+-- we need more of topcontext later - Maybe switch it up so we're not passing
+-- around top
+export
+mkCtx : FC -> Context
+mkCtx fc = MkCtx 0 [] [] [] fc

orig/Lib/Util.idr

@@ -0,0 +1,28 @@
+module Lib.Util
+
+import Lib.Types
+
+export
+funArgs : Tm -> (Tm, List Tm)
+funArgs tm = go tm []
+  where
+    go : Tm -> List Tm -> (Tm, List Tm)
+    go (App _ t u) args = go t (u :: args)
+    go t args = (t, args)
+
+public export
+data Binder : Type where
+  MkBinder : FC -> String -> Icit -> Quant -> Tm -> Binder
+
+-- I don't have a show for terms without a name list
+export
+Show Binder where
+  show (MkBinder _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]"
+
+export
+splitTele : Tm -> (Tm, List Binder)
+splitTele = go []
+  where
+    go : List Binder -> Tm -> (Tm, List Binder)
+    go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u
+    go ts tm = (tm, reverse ts)