porting WIP

done/Data/Fin.newt

@@ -0,0 +1 @@
+module Data.Fin

done/Data/IORef.newt

@@ -0,0 +1,27 @@
+module Data.IORef
+
+import Prelude
+
+-- We should test this at some point
+
+ptype IORef : U → U
+pfunc primNewIORef uses (MkIORes MkUnit) : ∀ a. a → IO (IORef a) := `(_, a) => (w) => MkIORes(undefined, [a], w)`
+pfunc primReadIORef uses (MkIORes MkUnit) : ∀ a. IORef a → IO a := `(_, ref) => (w) => MkIORes(undefined, ref[0], w)`
+pfunc primWriteIORef uses (MkIORes MkUnit) : ∀ a. IORef a → a → IO a := `(_, ref, a) => (w) => {
+  ref[0] = a
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+newIORef : ∀ io a. {{HasIO io}} → a → io (IORef a)
+newIORef a = liftIO $ primNewIORef a
+
+readIORef : ∀ io a. {{HasIO io}} → IORef a → io a
+readIORef ref = liftIO $ primReadIORef ref
+
+writeIORef : ∀ io a. {{HasIO io}} → IORef a -> a -> io Unit
+writeIORef ref a = liftIO $ writeIORef ref a
+
+-- Idris HasIO constraints to monad, we don't have those constraints yet
+modifyIORef : ∀ io a. {{Monad io}} {{HasIO io}} → IORef a -> (a -> a) -> io Unit
+modifyIORef {io} ref f =
+  bind {io} (readIORef ref) $ \a => writeIORef ref (f a)

done/Data/Int.newt

@@ -0,0 +1,12 @@
+module Data.Int
+
+import Prelude
+
+div : Int → Int → Int
+div a b = a / b
+
+instance Cast Char Int where
+  cast = ord
+
+instance Cast Int String where
+  cast = show

done/Data/List.newt

@@ -0,0 +1 @@
+module Data.List

done/Data/List1.newt

@@ -0,0 +1,10 @@
+module Data.List1
+
+import Prelude
+
+infixr 7 _:::_
+
+record List1 a where
+  constructor _:::_
+  head1 : a
+  tail1 : List a

done/Data/Maybe.newt

@@ -0,0 +1 @@
+module Data.Maybe

done/Data/Nat.newt

@@ -0,0 +1 @@
+module Data.Nat

done/Data/SnocList.newt

@@ -0,0 +1,14 @@
+module Data.SnocList
+
+import Prelude
+
+snoclen : ∀ a. SnocList a → Nat
+snoclen {a} xs = go xs Z
+  where
+    go : SnocList a → Nat → Nat
+    go Lin acc = acc
+    go (xs :< x) acc = go xs (S acc)
+
+snocelem : ∀ a. {{Eq a}} → a → SnocList a → Bool
+snocelem a Lin = False
+snocelem a (xs :< x) = if a == x then True else snocelem a xs

done/Data/SortedMap.newt

@@ -0,0 +1,202 @@
+module Data.SortedMap
+
+import Prelude
+
+-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
+
+data T23 : Nat -> U -> U -> U where
+  Leaf : ∀ k v. k -> v -> T23 Z k v
+  Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+  Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+
+lookupT23 : ∀ h k v. {{Ord k}} -> k -> T23 h k v -> Maybe (k × v)
+lookupT23 key (Leaf k v)= case compare k key of
+    EQ => Just (k,v)
+    _ => Nothing
+lookupT23 key (Node2 t1 k1 t2) =
+  if key <= k1 then lookupT23 key t1 else lookupT23 key t2
+lookupT23 key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then lookupT23 key t1
+  else if key <= k2 then lookupT23 key t2
+  else lookupT23 key t3
+
+insertT23 : ∀ h k v. {{Ord k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
+insertT23 key value (Leaf k v) = case compare key k of
+  EQ => Left (Leaf key value)
+  LT => Right (Leaf key value, key, Leaf k v)
+  GT => Right (Leaf k v, k, Leaf key value)
+insertT23 key value (Node2 t1 k1 t2) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node2 t1' k1 t2)
+      Right (a,b,c) => Left (Node3 a b c k1 t2)
+  else case insertT23 key value t2 of
+      Left t2' => Left (Node2 t1 k1 t2')
+      Right (a,b,c) => Left (Node3 t1 k1 a b c)
+insertT23 key value (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node3 t1' k1 t2 k2 t3)
+      Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
+  else if key <= k2 then
+    case insertT23 key value t2 of
+      Left t2' => Left (Node3 t1 k1 t2' k2 t3)
+      Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
+  else
+    case insertT23 key value t3 of
+      Left t3' => Left (Node3 t1 k1 t2 k2 t3')
+      Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
+
+-- This is cribbed from Idris. Deleting nodes takes a bit of code.
+Hole : Nat → U → U → U
+Hole Z k v = Unit
+Hole (S n) k v = T23 n k v
+
+Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
+
+Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
+
+Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
+
+Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
+
+merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
+merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
+merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
+merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
+merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
+
+-- height is erased in the data everywhere but the top, but needed for case
+-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
+deleteT23 : ∀ k v. {{Ord k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
+deleteT23 Z key (Leaf k v) = case compare k key of
+  EQ => Right MkUnit
+  _ => Left (Leaf k v)
+deleteT23 (S Z) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 Z key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right _ => Right t2
+  else case deleteT23 Z key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right MkUnit => Right t1
+deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right MkUnit => Left (Node2 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t2)
+deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 (S h) key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right t1 => case t2 of
+      Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
+      Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
+  else case deleteT23 _ key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right t2 => case t1 of
+      Node2 a b c => Right (Node3 a b c k1 t2)
+      Node3 a b c d e => Left (Node4 a b c d e k1 t2)
+deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t1 => Left (merge1 t1 k1 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t2 => Left (merge2 t1 k1 t2 k2 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t3 => Left (merge3 t1 k1 t2 k2 t3)
+
+treeLeft : ∀ h k v. T23 h k v → (k × v)
+treeLeft (Leaf k v) = (k, v)
+treeLeft (Node2 t1 _ _) = treeLeft t1
+treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
+
+treeRight : ∀ h k v. T23 h k v → (k × v)
+treeRight (Leaf k v) = (k, v)
+treeRight (Node2 _ _ t2) = treeRight t2
+treeRight (Node3 _ _ _ _ t3) = treeRight t3
+
+
+data SortedMap : U -> U -> U where
+  EmptyMap : ∀ k v. SortedMap k v
+  -- not erased so we know what happens in delete
+  MapOf : ∀ k v. {h : Nat} →  T23 h k v -> SortedMap k v
+
+deleteMap : ∀ k v. {{Ord k}} → k → SortedMap k v → SortedMap k v
+deleteMap key EmptyMap = EmptyMap
+-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
+deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
+  Left t => MapOf t
+  Right t => EmptyMap
+deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
+  Left t => MapOf t
+  Right t => MapOf t
+
+leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
+leftMost EmptyMap = Nothing
+leftMost (MapOf m) = Just (treeLeft m)
+
+rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
+rightMost EmptyMap = Nothing
+rightMost (MapOf m) = Just (treeRight m)
+
+-- TODO issue with metas and case if written as `do` block
+pop : ∀ k v. {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
+pop m = case leftMost m of
+    Just (k,v) => Just ((k,v), deleteMap k m)
+    Nothing => Nothing
+
+lookupMap : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe (k × v)
+lookupMap k EmptyMap = Nothing
+lookupMap k (MapOf map) = lookupT23 k map
+
+lookupMap' : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe v
+lookupMap' k EmptyMap = Nothing
+lookupMap' k (MapOf map) = snd <$> lookupT23 k map
+
+
+updateMap : ∀ k v. {{Ord k}} -> k -> v -> SortedMap k v -> SortedMap k v
+updateMap k v EmptyMap = MapOf $ Leaf k v
+updateMap k v (MapOf map) = case insertT23 k v map of
+  Left map' => MapOf map'
+  Right (a, b, c) => MapOf (Node2 a b c)
+
+toList : ∀ k v. SortedMap k v → List (k × v)
+toList {k} {v} (MapOf smap) = reverse $ go smap Nil
+  where
+    go : ∀ h. T23 h k v → List (k × v) → List (k × v)
+    go (Leaf k v) acc = (k, v) :: acc
+    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
+    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
+toList _ = Nil
+
+foldMap : ∀ a b. {{Ord a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
+foldMap f m Nil = m
+foldMap f m ((a,b) :: xs) = case lookupMap a m of
+  Nothing => foldMap f (updateMap a b m) xs
+  Just (_, b') => foldMap f (updateMap a (f b' b) m) xs

done/Data/String.newt

@@ -0,0 +1,11 @@
+module Data.String
+
+
+import Prelude
+
+class Interpolation a where
+  interpolate : a → String
+
+unwords : List String → String
+unwords stuff = joinBy " " stuff
+

done/Data/Vect.newt

@@ -0,0 +1 @@
+module Data.Vect

done/Lib/Common.newt

@@ -0,0 +1,154 @@
+module Lib.Common
+
+import Data.String
+import Data.Int
+import Data.Maybe
+import Data.SortedMap
+
+-- l is environment size, this works for both lvl2ix and ix2lvl
+
+lvl2ix : Int -> Int -> Int
+lvl2ix l k = l - k - 1
+
+hexChars : List Char
+hexChars = unpack "0123456789ABCDEF"
+
+-- export
+hexDigit : Int -> Char
+hexDigit v = fromMaybe ' ' (getAt (cast $ mod v 16) hexChars)
+
+
+toHex : Int -> List Char
+toHex 0 = Nil
+toHex v = snoc (toHex (div v 16)) (hexDigit v)
+
+
+quoteString : String -> String
+quoteString str = pack $ encode (unpack str) (Lin :<  '"')
+  where
+    encode : List Char -> SnocList Char -> List Char
+    encode Nil acc = acc <>> ('"' :: Nil)
+    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 : Int = 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)
+
+
+data Json : U where
+  JsonObj : List (String × Json) -> Json
+  JsonStr : String -> Json
+  JsonBool : Bool -> Json
+  JsonInt : Int -> Json
+  JsonArray : List Json -> Json
+
+
+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) = ite x "true" "false"
+renderJson (JsonInt i) = cast i
+renderJson (JsonArray xs) = "[" ++ joinBy "," (map renderJson xs) ++ "]"
+
+
+class ToJSON a where
+  toJson : a -> Json
+
+
+instance ToJSON String where
+  toJson = JsonStr
+
+
+instance ToJSON Int where
+  toJson = JsonInt
+
+
+record FC where
+  constructor MkFC
+  file : String
+  start : (Int × Int)
+
+
+instance ToJSON FC where
+  toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil)
+
+
+fcLine : FC -> Int
+fcLine (MkFC file (l, c)) = l
+
+
+fcCol : FC -> Int
+fcCol (MkFC file (l, c)) = c
+
+
+class HasFC a where
+  getFC : a -> FC
+
+
+
+
+emptyFC : FC
+emptyFC = MkFC "" (0,0)
+
+-- Error of a parse
+
+data Error
+  = E FC String
+  | Postpone FC Int String
+
+
+
+instance Show FC where
+  show fc = "\{fc.file}:\{show fc.start}"
+
+
+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 Nil = ""
+    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 Nil = ""
+    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
+
+
+data Fixity = InfixL | InfixR | Infix
+
+
+instance Show Fixity where
+  show InfixL = "infixl"
+  show InfixR = "infixr"
+  show Infix = "infix"
+
+
+
+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
+
+
+Operators : U
+Operators = SortedMap String OpDef

done/Lib/Erasure.newt

@@ -0,0 +1,101 @@
+module Lib.Erasure
+
+import Lib.Types
+import Data.Maybe
+import Data.SnocList
+import Lib.TopContext
+
+EEnv : U
+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
+
+
+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 Nil _ = 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 Nil
+  -- 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 Nil
+  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 Nil
+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 Nil
+  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 Nil
+
+-- 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 "\{show 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 Nil
+  -- If we get here, we're looking at a runtime pi type
+  (Pi fc nm icit rig u v) => do
+    u' <- erase env u Nil
+    v' <- erase ((nm, Many, Just u) :: env) v Nil
+    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 Nil
+    alts' <- traverse (doAlt env) alts
+    eraseSpine env (Case fc u' alts') sp Nothing
+  (Let fc nm u v) => do
+    u' <- erase env u Nil
+    v' <- erase ((nm, Many, Nothing) :: env) v Nil
+    eraseSpine env (Let fc nm u' v') sp Nothing
+  (LetRec fc nm ty u v) => do
+    u' <- erase ((nm, Many, Just ty) :: env) u Nil
+    v' <- erase ((nm, Many, Just ty) :: env) v Nil
+    eraseSpine env (LetRec fc nm ty u' v') sp Nothing
+  (Bnd fc k) => do
+    case getAt (cast 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
+
+

done/Lib/Parser/Impl.newt

@@ -0,0 +1,218 @@
+module Lib.Parser.Impl
+
+import Lib.Token
+import Lib.Common
+import Data.String
+import Data.Int
+import Data.List1
+import Data.SortedMap
+
+
+TokenList : U
+TokenList = List BTok
+
+-- Result of a parse
+
+data Result : U -> U where
+  OK : ∀ a. a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
+  Fail : ∀ a. Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
+
+
+instance 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
+
+
+data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a)
+
+
+runP : ∀ a. 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
+perror : String -> TokenList -> String -> Error
+perror fn Nil msg = E (MkFC fn (0,0)) msg
+perror fn ((MkBounded val (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg
+
+
+parse : ∀ a. String -> Parser a -> TokenList -> Either Error a
+parse fn pa toks = case runP pa toks False EmptyMap (MkFC fn (-1,-1)) of
+  Fail fatal err toks com ops => Left err
+  OK a Nil _ _ => Right a
+  OK a ts _ _ => Left (perror fn ts "Extra toks")
+
+-- Intended for parsing a top level declaration
+
+partialParse : ∀ a. 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
+
+
+try : ∀ a. 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
+
+
+fail : ∀ a. String -> Parser a
+fail msg = P $ \toks com ops col => Fail False (perror col.file toks msg) toks com ops
+
+
+fatal : ∀ a. String -> Parser a
+fatal msg = P $ \toks com ops col => Fail True (perror col.file toks msg) toks com ops
+
+
+getOps : Parser (Operators)
+getOps = P $ \ toks com ops col => OK ops toks com ops
+
+
+addOp : String -> Int -> Fixity -> Parser Unit
+addOp nm prec fix = P $ \ toks com ops col =>
+  let parts = split "_" nm in
+  case parts of
+    "" :: key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix False rule) ops)
+    key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix True rule) ops)
+    Nil => Fail True (perror col.file toks "Internal error parsing mixfix") toks com ops
+
+
+
+
+instance Functor Parser where
+  map f (P pa) = P $ \ toks com ops col => map f (pa toks com ops col)
+
+
+instance Applicative Parser where
+  return 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.
+
+instance Alternative Parser where
+  (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
+
+
+instance Monad Parser where
+  pure = return
+  bind (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 (perror col.file toks "\{msg} at \{show t.val.kind}:\{value t}") toks com ops
+    Nil => Fail False (perror col.file toks "\{msg} at EOF") toks com ops
+
+
+commit : Parser Unit
+commit = P $ \toks com ops col => OK MkUnit toks True ops
+
+
+some : ∀ a. Parser a -> Parser (List a)
+many : ∀ a. Parser a -> Parser (List a)
+some p = _::_ <$> p <*> many p
+many p = some p <|> pure Nil
+
+-- one or more `a` seperated by `s`
+
+sepBy : ∀ s a. Parser s -> Parser a -> Parser (List a)
+sepBy s a = _::_ <$> a <*> many (s *> a)
+
+
+getPos : Parser FC
+getPos = P $ \toks com ops indent => case toks of
+  Nil => 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
+
+startBlock : ∀ a. Parser a -> Parser a
+startBlock (P p) = P $ \toks com ops indent => case toks of
+  Nil => 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, ite (tc <= col) (col + 1) tc))
+
+-- Assert that parser starts at our current column by
+-- checking column and then updating line to match the current
+
+sameLevel : ∀ a. Parser a -> Parser a
+sameLevel (P p) = P $ \toks com ops indent => case toks of
+  Nil => 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 (perror file toks "unexpected indent") toks com ops
+    else Fail False (perror file toks "unexpected indent") toks com ops
+
+
+someSame : ∀ a. Parser a -> Parser (List a)
+someSame pa = some $ sameLevel pa
+
+
+manySame : ∀ a. Parser a -> Parser (List a)
+manySame pa = many $ sameLevel pa
+
+-- check indent on next token and run parser
+
+indented : ∀ a. Parser a -> Parser a
+indented (P p) = P $ \toks com ops indent => case toks of
+  Nil => 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 (perror indent.file toks "unexpected outdent") toks com ops
+
+-- expect token of given kind
+
+token' : Kind -> Parser String
+token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
+
+keyword' : String -> Parser Unit
+-- 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
+
+token : Kind -> Parser String
+token = indented ∘ token'
+
+
+keyword : String -> Parser Unit
+keyword kw = indented $ keyword' kw
+
+symbol : String -> Parser Unit
+symbol = keyword
+

done/Lib/Prettier.newt

@@ -0,0 +1,148 @@
+-- A prettier printer, Philip Wadler
+-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
+module Lib.Prettier
+
+import Data.String
+import Data.Int
+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".)
+
+data Doc = Empty | Line | Text String | Nest Int 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 Int
+
+
+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 Nil acc = fastConcat $ acc <>> Nil
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ')
+layout (TEXT str :: x) acc = layout x (acc :< str)
+
+-- Whether a documents first line fits.
+fits : Int -> List Item -> Bool
+fits w ((TEXT s) :: xs) = if slen s < w then fits (w - slen 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 -> Int -> Int -> List (Int × Doc) -> Maybe (List Item)
+be fit acc w k Nil = Just (acc <>> Nil)
+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 + slen s < w)
+     then (be fit (acc :< TEXT s) w (k + slen 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 Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i,y) :: xs))
+
+best : Int -> Int -> Doc -> List Item
+best w k x = fromMaybe Nil $ be False Lin w k ((0,x) :: Nil)
+
+-- Public class
+
+class Pretty a where
+  pretty : a -> Doc
+
+
+render : Int -> Doc -> String
+render w x = layout (best w 0 x) Lin
+
+
+instance Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y)
+
+-- Match System.File so we don't get warnings
+
+infixl 5 _</>_
+
+
+line : Doc
+line = Line
+
+
+text : String -> Doc
+text = Text
+
+
+nest : Int -> Doc -> Doc
+nest = Nest
+
+instance Concat Doc where
+  x ++ y = Seq x y
+
+
+_</>_ : Doc -> Doc -> Doc
+x </> y = x ++ line ++ y
+
+-- fold, but doesn't emit extra nil
+
+folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc
+folddoc f Nil = Empty
+folddoc f (x :: Nil) = x
+folddoc f (x :: xs) = f x (folddoc f xs)
+
+-- separate with space
+
+spread : List Doc -> Doc
+spread = folddoc _<+>_
+
+-- separate with new lines
+
+stack : List Doc -> Doc
+stack = folddoc _</>_
+
+-- bracket x with l and r, indenting contents on new line
+
+bracket : String -> Doc -> String -> Doc
+bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
+
+
+infixl 5 _<+/>_
+
+-- Either space or newline
+
+_<+/>_ : 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.
+
+fill : List Doc -> Doc
+fill Nil = Empty
+fill (x :: Nil) = x
+fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
+
+-- separate with comma
+
+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`
+
+instance Interpolation Doc where
+  interpolate = render 80 ∘ flatten

done/Lib/Syntax.newt

@@ -0,0 +1,297 @@
+module Lib.Syntax
+
+import Data.String
+import Data.Maybe
+import Lib.Parser.Impl
+import Lib.Prettier
+import Lib.Types
+
+Raw : U
+
+
+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
+
+
+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
+
+
+
+instance HasFC Pattern where
+  getFC (PatVar fc _ _) = fc
+  getFC (PatCon fc _ _ _ _) = fc
+  getFC (PatWild fc _) = fc
+  getFC (PatLit fc lit) = fc
+
+-- %runElab deriveShow `{Pattern}
+
+Constraint : U
+Constraint = (String × Pattern)
+
+
+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?
+
+data RCaseAlt = MkAlt Raw Raw
+
+
+data DoStmt : U where
+  DoExpr : (fc : FC) -> Raw -> DoStmt
+  DoLet : (fc : FC) -> String -> Raw -> DoStmt
+  DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
+
+Decl : U
+data Raw : U 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
+
+instance 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
+
+
+data Import = MkImport FC Name
+
+
+
+Telescope : U
+Telescope = List (BindInfo × Raw)
+
+
+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) Int Fixity
+  | Class FC Name Telescope (List Decl)
+  | Instance FC Raw (List Decl)
+  | Record FC Name Telescope (Maybe Name) (Maybe (List Decl))
+
+
+instance 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
+
+
+record Module where
+  constructor MkModule
+  modname : Name
+  imports : List Import
+  decls : List Decl
+
+foo : List String -> String
+foo ts = "(" ++ unwords ts ++ ")"
+
+instance Show Raw
+instance Show Pattern
+
+instance Show Clause where
+  show (MkClause fc cons pats expr) = show (fc, cons, pats, expr)
+
+instance Show Import where
+  show (MkImport _ str) = foo ("MkImport" :: show str :: Nil)
+
+instance Show BindInfo where
+  show (BI _ nm icit quant) = foo ("BI" :: show nm :: show icit :: show quant :: Nil)
+
+-- this is for debugging, use pretty when possible
+
+instance Show Decl where
+  show (TypeSig _ str x) = foo ("TypeSig" :: show str :: show x :: Nil)
+  show (Def _ str clauses) = foo ("Def" :: show str :: show clauses :: Nil)
+  show (Data _ str xs ys) = foo ("Data" :: show str :: show xs :: show ys :: Nil)
+  show (DCheck _ x y) = foo ("DCheck" :: show x :: show y :: Nil)
+  show (PType _ name ty) = foo ("PType" :: name :: show ty :: Nil)
+  show (ShortData _ lhs sigs) = foo ("ShortData" :: show lhs :: show sigs :: Nil)
+  show (PFunc _ nm used ty src) = foo ("PFunc" :: nm :: show used :: show ty :: show src :: Nil)
+  show (PMixFix _ nms prec fix) = foo ("PMixFix" :: show nms :: show prec :: show fix :: Nil)
+  show (Class _ nm tele decls) = foo ("Class" ::  nm :: "..." :: (show $ map show decls) :: Nil)
+  show (Instance _ nm decls) = foo ("Instance" ::  show nm :: (show $ map show decls) :: Nil)
+  show (Record _ nm tele nm1 decls) = foo ("Record" :: show nm :: show tele :: show nm1 :: show decls :: Nil)
+
+
+instance Show Module where
+  show (MkModule name imports decls) = foo ("MkModule" :: show name :: show imports :: show decls :: Nil)
+
+
+instance Show Pattern where
+  show (PatVar _ icit str) = foo ("PatVar" :: show icit :: show str :: Nil)
+  show (PatCon _ icit str xs as) = foo ("PatCon" :: show icit :: show str :: show xs :: show as :: Nil)
+  show (PatWild _ icit) = foo ("PatWild" :: show icit :: Nil)
+  show (PatLit _ lit) = foo ("PatLit" :: show lit :: Nil)
+
+
+instance Show RCaseAlt where
+  show (MkAlt x y)= foo ("MkAlt" :: show x :: show y :: Nil)
+
+
+instance Show Raw where
+  show (RImplicit _) = "_"
+  show (RHole _) = "?"
+  show (RVar _ name) = foo ("RVar" :: show name :: Nil)
+  show (RAnn _ t ty) = foo ( "RAnn" :: show t :: show ty :: Nil)
+  show (RLit _ x) = foo ( "RLit" :: show x :: Nil)
+  show (RLet _ x ty v scope) = foo ( "Let" :: show x :: " : " :: show ty :: " = " :: show v :: " in " :: show scope :: Nil)
+  show (RPi _ bi y z) = foo ( "Pi" :: show bi :: show y :: show z :: Nil)
+  show (RApp _ x y z) = foo ( "App" :: show x :: show y :: show z :: Nil)
+  show (RLam _ bi y) = foo ( "Lam" :: show bi :: show y :: Nil)
+  show (RCase _ x xs) = foo ( "Case" :: show x :: show xs :: Nil)
+  show (RDo _ stmts) = foo ( "DO" :: "FIXME" :: Nil)
+  show (RU _) = "U"
+  show (RIf _ x y z) = foo ( "If" :: show x :: show y :: show z :: Nil)
+  show (RWhere _ _ _) = foo ( "Where" :: "FIXME" :: Nil)
+  show (RAs _ nm x) = foo ( "RAs" :: nm :: show x :: Nil)
+
+
+instance Pretty Literal where
+  pretty (LString t) = text t
+  pretty (LInt i) = text $ show i
+  pretty (LChar c) = text $ show c
+
+
+instance Pretty Pattern where
+  -- FIXME - wrap Implicit with {}
+  pretty (PatVar _ icit str) = text str
+  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 "}}"
+
+
+instance Pretty Raw where
+  pretty = asDoc 0
+    where
+    bindDoc : BindInfo -> Doc
+    bindDoc (BI _ nm icit quant) = text "BINDDOC"
+
+    par : Int -> Int -> Doc -> Doc
+    par p p' d = if p' < p then text "(" ++ d ++ text ")" else d
+
+    asDoc : Int -> 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)
+
+
+instance Pretty Decl where
+  pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
+  pretty (Def _ nm clauses) = stack $ map prettyPair clauses
+    where
+      prettyPair : Raw × Raw → Doc
+      prettyPair (a, b) = pretty a <+> text "=" <+> pretty b
+  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 Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
+  pretty (PFunc _ nm used ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text used) <+> 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 Nothing) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+  pretty (Record _ nm tele cname (Just 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)
+
+
+instance 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
+

done/Lib/Token.newt

@@ -0,0 +1,100 @@
+module Lib.Token
+
+import Prelude
+
+record Bounds where
+  constructor MkBounds
+  startLine : Int
+  startCol : Int
+  endLine : Int
+  endCol : Int
+
+
+instance Eq Bounds where
+  (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
+      sl == sl'
+   && sc == sc'
+   && el == el'
+   && ec == ec'
+
+
+record WithBounds ty where
+  constructor MkBounded
+  val : ty
+  bounds : Bounds
+
+
+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
+
+
+instance 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"
+
+
+instance Eq Kind where
+  a == b = show a == show b
+
+
+record Token where
+  constructor Tok
+  kind : Kind
+  text : String
+
+
+
+instance Show Token where
+  show (Tok k v) = "<\{show k}:\{show v}>"
+
+
+BTok : U
+BTok = WithBounds Token
+
+
+value : BTok -> String
+value (MkBounded (Tok _ s) _) = s
+
+
+getStart : BTok -> (Int × Int)
+getStart (MkBounded _ (MkBounds l c _ _)) = (l,c)

done/Lib/Tokenizer.newt

@@ -0,0 +1,172 @@
+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.
+
+-- Newt is having a rough time dealing with do blocks for Either in here
+--
+
+import Lib.Token
+import Lib.Common
+import Data.String
+import Data.SnocList
+
+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
+            "$" :: "λ" :: "?" :: "@" :: "." ::
+             "->" :: "→" :: ":" :: "=>" :: ":=" :: "=" :: "<-" :: "\\" :: "_" :: "|" :: Nil)
+
+record TState where
+  constructor TS
+  trow : Int
+  tcol : Int
+  acc : SnocList BTok
+  chars : List Char
+
+singleton : Char → String
+singleton c = pack $ c :: Nil
+
+-- 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 =>
+    let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2)) in
+    case (rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs) of
+      Left err => Left err
+      Right (TS el ec toks chars) => 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) Lin
+        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 <>> Nil)) (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 =>
+    let tok = mktok False sl (sc + 1) StartQuote "\"" in
+    case quoteTokenise (TS sl (sc + 1) (toks :< tok) cs) sl (sc + 1) Lin of
+      Left err => Left err
+      Right (TS sl sc toks chars) => 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 =>
+    let tok = mktok False sl (sc + 2) Keyword "{{" in
+    case rawTokenise (TS sl (sc + 2) (toks :< tok) cs) of
+      Left err => Left err
+      Right (TS sl sc toks chars) => 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 =>
+    let tok = mktok False sl (sc + 1) Symbol "{" in
+    case rawTokenise (TS sl (sc + 1) (toks :< tok) cs) of
+      Left err => Left err
+      Right (TS sl sc toks chars) => 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 = ite (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) Lin
+  '.' :: 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 <>> Nil)) (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)) 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 snocelem '_' acc then MixFix else kind in
+        rawTokenise (TS l c (toks :< mktok True l (c - 1) kind (pack $ acc <>> Nil)) (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 (pack $ c :: Nil)) 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 Lin
+
+
+tokenise : String -> String -> Either Error (List BTok)
+tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of
+  Right (TS trow tcol acc Nil) => Right $ acc <>> Nil
+  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
+

done/Lib/TopContext.newt

@@ -0,0 +1,62 @@
+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.)
+
+
+lookup : QName -> TopContext -> Maybe TopEntry
+lookup nm top = lookupMap' nm top.defs
+
+-- TODO - look at imported namespaces, and either have a map of imported names or search imported namespaces..
+
+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?
+
+
+instance Show TopContext where
+  show (MkTop defs metas _ _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)"
+
+-- TODO need to get class dependencies working
+emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
+emptyTop = do
+  mcctx <- newIORef (MC Nil 0)
+  errs <- newIORef $ the (List Error) Nil
+  pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap
+
+
+setDef : QName -> FC -> Tm -> Def -> M Unit
+setDef name fc ty def = do
+  top <- get
+  let (Nothing) = lookupMap' name top.defs
+    | Just (MkEntry fc' nm' ty' def') => error fc "\{show name} is already defined at \{show fc'}"
+  modify $ \case
+    MkTop defs metaCtx verbose errors loaded ops =>
+      let defs = (updateMap name (MkEntry fc name ty def) top.defs) in
+      MkTop defs metaCtx verbose errors loaded ops
+
+
+updateDef : QName -> FC -> Tm -> Def -> M Unit
+updateDef name fc ty def = do
+  top <- get
+  let (Just (MkEntry fc' nm' ty' def')) = lookupMap' name top.defs
+    | Nothing => error fc "\{show name} not declared"
+  modify $ \case
+    MkTop defs metaCtx verbose errors loaded ops =>
+      let defs = (updateMap name (MkEntry fc' name ty def) defs) in
+      MkTop defs metaCtx verbose errors loaded ops
+
+addError : Error -> M Unit
+addError err = do
+  top <- get
+  modifyIORef top.errors (_::_ err)

done/Lib/Types.newt

@@ -0,0 +1,517 @@
+module Lib.Types
+
+-- For FC, Error
+import Lib.Common
+import Lib.Prettier
+
+import Data.Fin
+import Data.IORef
+import Data.List
+import Data.SnocList
+import Data.SortedMap
+import Data.String
+import Data.Vect
+
+data QName : U where
+  QN : List String -> String -> QName
+
+instance Eq QName where
+  QN ns n == QN ns' n' = n == n' && ns == ns'
+
+instance Show QName where
+  show (QN Nil n) = n
+  show (QN ns n) = joinBy "." ns ++ "." ++ n
+
+instance Interpolation QName where
+  interpolate = show
+
+instance Ord QName where
+  compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
+
+Name : U
+Name = String
+
+data Icit = Implicit | Explicit | Auto
+
+instance Show Icit where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+  show Auto = "Auto"
+
+data BD = Bound | Defined
+
+instance Eq BD where
+  Bound == Bound = True
+  Defined == Defined = True
+  _ == _ = False
+
+instance Show BD where
+  show Bound = "bnd"
+  show Defined = "def"
+
+data Quant = Zero | Many
+
+instance Show Quant where
+  show Zero = "0 "
+  show Many = ""
+
+instance Eq Quant where
+  Zero == Zero = True
+  Many == Many = True
+  _ == _ = False
+
+-- We could make this polymorphic and use for environment...
+
+data BindInfo : U where
+  BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo
+
+instance HasFC BindInfo where
+  getFC (BI fc _ _ _) = fc
+
+Tm : U
+
+data Literal = LString String | LInt Int | LChar Char
+
+instance Show Literal where
+  show (LString str) = show str
+  show (LInt i) = show i
+  show (LChar c) = show c
+
+data CaseAlt : U where
+  CaseDefault : Tm -> CaseAlt
+  CaseCons : (name : QName) -> (args : List String) -> Tm ->  CaseAlt
+  CaseLit : Literal -> Tm ->  CaseAlt
+
+Def : U
+
+instance Eq Literal where
+  LString x == LString y = x == y
+  LInt x == LInt y = x == y
+  LChar x == LChar y = x == y
+  _ == _ = False
+
+data Tm : U where
+  Bnd : FC -> Int -> Tm
+  -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
+  Ref : FC -> QName -> Def -> Tm
+  Meta : FC -> Int -> Tm
+  -- kovacs optimization, I think we can App out meta instead
+  -- InsMeta : Int -> 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
+
+instance 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
+
+showCaseAlt : CaseAlt → String
+
+instance 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 $ map showCaseAlt   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"
+
+
+showCaseAlt (CaseDefault tm) = "_ => \{show tm}"
+showCaseAlt (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}"
+showCaseAlt (CaseLit lit tm) = "\{show lit} => \{show tm}"
+
+
+showTm : Tm -> String
+showTm = show
+
+-- I can't really show val because it's HOAS...
+
+-- TODO derive
+
+instance 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
+
+instance 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' : Int -> List String -> Tm -> Doc
+pprintAlt : Int -> 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 : Int -> Int -> Doc -> Doc
+parens a b doc = if a < b
+  then text "(" ++ doc ++ text ")"
+  else doc
+
+pprint' p names (Bnd _ k) = case getAt (cast 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.
+
+pprint : List String -> Tm -> Doc
+pprint names tm = pprint' 0 names tm
+
+Val : U
+
+-- 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
+
+Closure : U
+
+data Val : U where
+  -- This will be local / flex with spine.
+  VVar : FC -> (k : Int) -> (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 : Int) -> (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
+
+Env : U
+Env = List Val
+
+data Mode = CBN | CBV
+
+data Closure = MkClosure Env Tm
+
+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
+
+instance HasFC Val where getFC = getValFC
+
+showClosure : Closure → String
+
+instance Show Val where
+  show (VVar _ k Lin) = "%var\{show k}"
+  show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})"
+  show (VRef _ nm _ Lin) = show nm
+  show (VRef _ nm _ sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})"
+  show (VMeta _ ix sp) = "(%meta \{show ix} (\{show $ snoclen sp} sp :: Nil))"
+  show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})"
+  show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{showClosure  y})"
+  show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{showClosure  y})"
+  show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show  x}}}. \{showClosure  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"
+
+
+showClosure (MkClosure xs t) = "(%cl (\{show $ length xs} env :: Nil) \{show t})"
+
+-- instance Show Closure where
+--   show = showClosure
+
+Context : U
+
+data MetaKind = Normal | User | AutoSolve
+
+instance Show MetaKind where
+  show Normal = "Normal"
+  show User = "User"
+  show AutoSolve = "Auto"
+
+-- constrain meta applied to val to be a val
+
+data MConstraint = MkMc FC Env (SnocList Val) Val
+
+data MetaEntry = Unsolved FC Int Context Val MetaKind (List MConstraint) | Solved FC Int Val
+
+record MetaContext where
+  constructor MC
+  metas : List MetaEntry
+  next : Int
+
+data Def = Axiom | TCon (List QName) | DCon Int QName | Fn Tm | PrimTCon
+         | PrimFn String (List String)
+
+instance 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
+
+record TopEntry where
+  constructor MkEntry
+  fc : FC
+  name : QName
+  type : Tm
+  def : Def
+
+-- FIXME snoc
+
+instance Show TopEntry where
+  show (MkEntry fc name type def) = "\{show 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?
+
+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.
+
+record Context where
+  constructor MkCtx
+  lvl : Int
+  -- shall we use lvl as an index?
+  env : Env                  -- Values in scope
+  types : List (String × Val) -- types and names in scope
+  -- so we'll try "bds" determines length of local context
+  bds : List BD          -- bound or defined
+
+  -- FC to use if we don't have a better option
+  ctxFC : FC
+
+-- add a binding to environment
+
+extend : Context -> String -> Val -> Context
+extend (MkCtx lvl env types bds ctxFC) name ty =
+  MkCtx (1 + lvl) (VVar emptyFC lvl Lin :: env) ((name,ty) :: types) (Bound :: bds) ctxFC
+
+-- I guess we define things as values?
+
+define : Context -> String -> Val -> Val -> Context
+define (MkCtx lvl env types bds ctxFC) name val ty =
+  MkCtx (1 + lvl) (val :: env) ((name,ty) :: types) (Defined :: bds) ctxFC
+
+instance 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}"
+
+withPos : Context -> FC -> Context
+withPos (MkCtx lvl env types bds ctxFC) fc = (MkCtx lvl env types bds fc)
+
+names : Context -> List String
+names ctx = map fst ctx.types
+
+-- public export
+-- M : U -> U
+-- M = (StateT TopContext (EitherT Error IO))
+
+record M a where
+  constructor MkM
+  runM : TopContext -> IO (Either Error (TopContext × a))
+
+instance Functor M where
+  map f (MkM run) = MkM $ \tc => bind {IO} (run tc) $ \case
+      Left err => pure $ Left err
+      Right (tc', a) => pure $ Right (tc', f a)
+
+instance Applicative M where
+  return x = MkM $ \tc => pure $ Right (tc, x)
+  (MkM f) <*> (MkM x) = MkM $ \tc => bind {IO} (f tc) $ \case
+      Left err => pure $ Left err
+      Right (tc', f') => bind {IO} (x tc') $ \case
+          Left err => pure $ Left err
+          Right (tc'', x') => pure $ Right (tc'', f' x')
+
+instance Monad M where
+  pure = return
+  bind (MkM x) f = MkM $ \tc => bind {IO} (x tc) $ \case
+      Left err => pure $ Left err
+      Right (tc', a) => runM (f a) tc'
+
+instance HasIO M where
+  liftIO io = MkM $ \tc => do
+    result <- io
+    pure $ Right (tc, result)
+
+throwError : ∀ a. Error -> M a
+throwError err = MkM $ \_ => pure $ Left err
+
+catchError : ∀ a. M a -> (Error -> M a) -> M a
+catchError (MkM ma) handler = MkM $ \tc => bind {IO} (ma tc) $ \case
+    Left err => runM (handler err) tc
+    Right (tc', a) => pure $ Right (tc', a)
+
+tryError : ∀ a. M a -> M (Either Error a)
+tryError ma = catchError (map Right ma) (pure ∘ Left)
+
+get : M TopContext
+get = MkM $ \ tc => pure $ Right (tc, tc)
+
+put : TopContext -> M Unit
+put tc = MkM $ \_ => pure $ Right (tc, MkUnit)
+
+modify : (TopContext -> TopContext) -> M Unit
+modify f = do
+  tc <- get
+  put (f tc)
+
+-- Force argument and print if verbose is true
+
+debug : Lazy String -> M Unit
+debug x = do
+  top <- get
+  when top.verbose $ \ _ => putStrLn $ force x
+
+info : FC -> String -> M Unit
+info fc msg = putStrLn "INFO at \{show fc}: \{msg}"
+
+-- Version of debug that makes monadic computation lazy
+
+debugM : M String -> M Unit
+debugM x = do
+  top <- get
+  when top.verbose $ \ _ => do
+    msg <- x
+    putStrLn msg
+
+instance Show Context where
+  show ctx = "Context \{show $ map fst $ ctx.types}"
+
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (Postpone x k str) = str
+
+instance HasFC Error where
+  getFC (E x str) = x
+  getFC (Postpone x k str) = x
+
+error : ∀ a. FC -> String -> M a
+error fc msg = throwError $ E fc msg
+
+error' : ∀ a. String -> M a
+error' msg = throwError $ E emptyFC msg
+
+freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
+freshMeta ctx fc ty kind = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
+  writeIORef top.metaCtx $ MC (Unsolved fc mc.next ctx ty kind Nil :: mc.metas) (1 + mc.next)
+  pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
+  where
+    -- hope I got the right order here :)
+    applyBDs : Int -> Tm -> List BD -> Tm
+    applyBDs k t Nil = t
+    -- review the order here
+    applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k)
+    applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs
+
+lookupMeta : Int -> M MetaEntry
+lookupMeta ix = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  go mc.metas
+  where
+    go : List MetaEntry -> M MetaEntry
+    go Nil = 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
+
+mkCtx : FC -> Context
+mkCtx fc = MkCtx 0 Nil Nil Nil fc

done/Lib/Util.newt

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

done/Prelude.newt

@@ -0,0 +1 @@
+../newt/Prelude.newt