Make everything relevant.

Too few proofs were relevant. Now they are.

2 files changed, 307 insertions, 238 deletions

diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 6913bf8..90b4e08 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -1,14 +1,23 @@
 module Inky.Term.Parser
 
-import public Data.Fun
+import public Inky.Data.Fun
 
+import Data.Either
+import Data.Nat
 import Data.List1
 import Data.String
-import Inky.Context
+
+import Inky.Data.Context
+import Inky.Data.Context.Var
+import Inky.Data.Row
+import Inky.Data.SnocList.Var
+import Inky.Data.SnocList.Thinning
+import Inky.Decidable
+import Inky.Decidable.Maybe
 import Inky.Parser
 import Inky.Term
-import Inky.Thinning
 import Inky.Type
+
 import Text.Lexer
 
 -- Lexer -----------------------------------------------------------------------
@@ -18,7 +27,6 @@ data InkyKind
   = TermIdent
   | TypeIdent
   | Lit
-  | Suc
   | Let
   | In
   | Case
@@ -27,6 +35,10 @@ data InkyKind
   | Fold
   | By
   | Nat
+  | List
+  | Suc
+  | Map
+  | GetChildren
   | ParenOpen
   | ParenClose
   | BracketOpen
@@ -52,7 +64,6 @@ export
   TermIdent == TermIdent = True
   TypeIdent == TypeIdent = True
   Lit == Lit = True
-  Suc == Suc = True
   Let == Let = True
   In == In = True
   Case == Case = True
@@ -61,6 +72,10 @@ export
   Fold == Fold = True
   By == By = True
   Nat == Nat = True
+  List == List = True
+  Suc == Suc = True
+  Map == Map = True
+  GetChildren == GetChildren = True
   ParenOpen == ParenOpen = True
   ParenClose == ParenClose = True
   BracketOpen == BracketOpen = True
@@ -87,7 +102,6 @@ Interpolation InkyKind where
   interpolate TermIdent = "term name"
   interpolate TypeIdent = "type name"
   interpolate Lit = "number"
-  interpolate Suc = "'suc'"
   interpolate Let = "'let'"
   interpolate In = "'in'"
   interpolate Case = "'case'"
@@ -96,6 +110,10 @@ Interpolation InkyKind where
   interpolate Fold = "'fold'"
   interpolate By = "'by'"
   interpolate Nat = "'Nat'"
+  interpolate List = "'List'"
+  interpolate Suc = "'suc'"
+  interpolate Map = "'map'"
+  interpolate GetChildren = "'getChildren'"
   interpolate ParenOpen = "'('"
   interpolate ParenClose = "')'"
   interpolate BracketOpen = "'['"
@@ -125,7 +143,6 @@ TokenKind InkyKind where
   tokValue TermIdent = id
   tokValue TypeIdent = id
   tokValue Lit = stringToNatOrZ
-  tokValue Suc = const ()
   tokValue Let = const ()
   tokValue In = const ()
   tokValue Case = const ()
@@ -134,6 +151,10 @@ TokenKind InkyKind where
   tokValue Fold = const ()
   tokValue By = const ()
   tokValue Nat = const ()
+  tokValue List = const ()
+  tokValue Suc = const ()
+  tokValue Map = const ()
+  tokValue GetChildren = const ()
   tokValue ParenOpen = const ()
   tokValue ParenClose = const ()
   tokValue BracketOpen = const ()
@@ -156,8 +177,7 @@ TokenKind InkyKind where
 
 keywords : List (String, InkyKind)
 keywords =
-  [ ("suc", Suc)
-  , ("let", Let)
+  [ ("let", Let)
   , ("in", In)
   , ("case", Case)
   , ("of", Of)
@@ -165,6 +185,10 @@ keywords =
   , ("fold", Fold)
   , ("by", By)
   , ("Nat", Nat)
+  , ("List", List)
+  , ("suc", Suc)
+  , ("map", Map)
+  , ("getChildren", GetChildren)
   ]
 
 export
@@ -221,70 +245,61 @@ tokenMap =
 -- Parser ----------------------------------------------------------------------
 
 public export
-DFun : (ts : Vect n Type) -> Fun ts Type -> Type
-DFun [] r = r
-DFun (t :: ts) r = (x : t) -> DFun ts (r x)
-
-public export
-DIFun : (ts : Vect n Type) -> Fun ts Type -> Type
-DIFun [] r = r
-DIFun (t :: ts) r = {x : t} -> DIFun ts (r x)
-
-public export
 InkyParser : Bool -> Context Type -> Context Type -> (a : Type) -> Type
 InkyParser nil locked free a =
   Parser InkyKind nil
-    (map (\a => (False, a)) locked)
-    (map (\a => (False, a)) free)
+    (map (map (False,)) locked)
+    (map (map (False,)) free)
     a
 
 public export
-record ParseFun (0 tys: Vect n Type) (0 p : Fun (map Context tys) Type) where
+record ParseFun (0 n : Nat) (0 p : Fun (replicate n $ SnocList String) Type) where
   constructor MkParseFun
-  try : DFun (map Context tys) (chain {ts = map Context tys} (Either String) p)
+  try :
+    DFun (replicate n $ SnocList String)
+      (chain (lengthOfReplicate n $ SnocList String) (Either String) p)
 
-mkVar : ({ctx : Context ()} -> Var ctx () -> p ctx) -> WithBounds String -> ParseFun [()] p
+mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun 1 p
 mkVar f x =
   MkParseFun
-    (\ctx => case lookup x.val ctx of
-      Just (() ** i) => pure (f i)
+    (\ctx => case Var.lookup x.val ctx of
+      Just i => pure (f i)
       Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
 
 mkVar2 :
-  ({tyCtx, tmCtx : Context ()} -> Var tmCtx () -> p tyCtx tmCtx) ->
-  WithBounds String -> ParseFun [(), ()] p
+  ({tyCtx, tmCtx : _} -> Var tmCtx -> p tyCtx tmCtx) ->
+  WithBounds String -> ParseFun 2 p
 mkVar2 f x =
   MkParseFun
-    (\tyCtx, tmCtx => case lookup x.val tmCtx of
-      Just (() ** i) => pure (f i)
+    (\tyCtx, tmCtx => case Var.lookup x.val tmCtx of
+      Just i => pure (f i)
       Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
 
 public export
 TypeFun : Type
-TypeFun = ParseFun [()] (\ctx => Ty ctx ())
-
-public export
-SynthFun : Type
-SynthFun = ParseFun [(), ()] SynthTerm
+TypeFun = ParseFun 1 Ty
 
 public export
-CheckFun : Type
-CheckFun = ParseFun [(), ()] CheckTerm
+TermFun : Type
+TermFun = ParseFun 2 Term
 
 public export
-TypeParser : Context () -> Context () -> Type
+TypeParser : SnocList String -> SnocList String -> Type
 TypeParser locked free =
-  InkyParser False (map (const TypeFun) locked) (map (const TypeFun) free) TypeFun
+  InkyParser False (map (:- TypeFun) locked) (map (:- TypeFun) free) TypeFun
 
-RowOf : (0 free : Context Type) -> InkyParser False [<] free a -> InkyParser True [<] free (List $ WithBounds $ Assoc a)
+RowOf :
+  (0 free : Context Type) ->
+  InkyParser False [<] free a ->
+  InkyParser True [<] free (List $ WithBounds $ Assoc a)
 RowOf free p = sepBy (match Comma) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p])
   where
   mkAssoc : HList [String, (), a] -> Assoc a
   mkAssoc [x, _, v] = x :- v
 
 tryRow :
-  List (WithBounds $ Assoc (ParseFun [()] p)) ->
-  (ctx : Context ()) -> Either String (Row $ p ctx)
+  List (WithBounds $ Assoc (ParseFun 1 p)) ->
+  (ctx : _) -> Either String (Row $ p ctx)
 tryRow xs ctx =
   foldlM
     (\row, xf => do
@@ -296,8 +311,8 @@ tryRow xs ctx =
     xs
 
 tryRow2 :
-  List (WithBounds $ Assoc (ParseFun [(), ()] p)) ->
-  (tyCtx, tmCtx : Context ()) -> Either String (Row $ p tyCtx tmCtx)
+  List (WithBounds $ Assoc (ParseFun 2 p)) ->
+  (tyCtx, tmCtx : _) -> Either String (Row $ p tyCtx tmCtx)
 tryRow2 xs tyCtx tmCtx =
   foldlM
     (\row, xf => do
@@ -308,29 +323,29 @@ tryRow2 xs tyCtx tmCtx =
     [<]
     xs
 
-OpenOrFixpointType : TypeParser [<] [<"openType" :- ()]
+OpenOrFixpointType : TypeParser [<] [<"openType"]
 OpenOrFixpointType =
   OneOf
     [ mkFix <$>
-      Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%% "openType")]
-    , Var (%% "openType")
+      Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%%% "openType")]
+    , Var (%%% "openType")
     ]
   where
   mkFix : HList [(), String, (), TypeFun] -> TypeFun
-  mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ()))))
+  mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< x)))
 
-AtomType : TypeParser [<"openType" :- ()] [<]
+AtomType : TypeParser [<"openType"] [<]
 AtomType =
   OneOf
     [ mkVar TVar <$> WithBounds (match TypeIdent)
     , MkParseFun (\_ => pure TNat) <$ match Nat
-    , mkProd <$> enclose (match AngleOpen) (match AngleClose) Row
-    , mkSum <$> enclose (match BracketOpen) (match BracketClose) Row
+    , mkProd <$> enclose (match AngleOpen) (match AngleClose) row
+    , mkSum <$> enclose (match BracketOpen) (match BracketClose) row
     , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType
     ]
   where
-  Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun)
-  Row = RowOf [<"openType" :- TypeFun] $ Var (%% "openType")
+  row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun)
+  row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType")
 
   mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun
   mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx)
@@ -338,13 +353,25 @@ AtomType =
   mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun
   mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx)
 
+AppType : TypeParser [<"openType"] [<]
+AppType =
+  OneOf
+    [ AtomType
+    , match List **> mkList <$> weaken (S Z) AtomType
+    ]
+  where
+  mkList : TypeFun -> TypeFun
+  mkList x = MkParseFun (\ctx => TList <$> x.try ctx)
+
 export
 OpenType : TypeParser [<] [<]
 OpenType =
-  Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AtomType
+  Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AppType
   where
   mkArrow : List1 TypeFun -> TypeFun
-  mkArrow = foldr1 (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
+  mkArrow =
+    foldr1 {a = TypeFun}
+      (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
 
 %hint
 export
@@ -353,95 +380,122 @@ OpenTypeWf = Oh
 
 -- Terms -----------------------------------------------------------------------
 
-embed : SynthFun -> CheckFun
-embed x = MkParseFun (\tyCtx, tmCtx => Embed <$> x.try tyCtx tmCtx)
-
-unembed : WithBounds CheckFun -> SynthFun
-unembed x =
-  MkParseFun (\tyCtx, tmCtx => do
-    t <- x.val.try tyCtx tmCtx
-    case t of
-      Embed e => pure e
-      _ => Left "\{x.bounds}: cannot synthesise type")
-
-AtomCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-AtomCheck =
+AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+AtomTerm =
   OneOf
-    [ embed <$> mkVar2 Var <$> WithBounds (match TermIdent)
-    , embed <$> mkLit <$> match Lit
-    , embed <$> MkParseFun (\_, _ => pure Suc) <$ match Suc
+    [ mkVar2 Var <$> WithBounds (match TermIdent)
+    , mkLit <$> match Lit
+    , mkSuc <$ match Suc
     , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $
-        RowOf [<"openCheck" :- CheckFun] (Var (%% "openCheck")))
-    , enclose (match ParenOpen) (match ParenClose) (Var (%% "openCheck"))
+        RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
+    , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
     ]
   where
-  mkLit : Nat -> SynthFun
-  mkLit k = MkParseFun (\_, _ => pure (Lit k))
+  mkLit : Nat -> TermFun
+  mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k))
 
-  mkTup : List (WithBounds $ Assoc CheckFun) -> CheckFun
+  mkSuc : TermFun
+  mkSuc = MkParseFun (\_, _ => pure Suc)
+
+  mkTup : List (WithBounds $ Assoc TermFun) -> TermFun
   mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup <$> tryRow2 xs tyCtx tmCtx)
 
-PrefixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-PrefixCheck =
-  Fix "prefixCheck" $ OneOf
-    [ embed <$> mkExpand <$> unembed <$> (match Bang **> WithBounds (Var $ %% "prefixCheck"))
-    , mkContract <$> (match Tilde **> Var (%% "prefixCheck"))
-    , rename (Drop Id) Id AtomCheck
+PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+PrefixTerm =
+  Fix "prefixTerm" $ OneOf
+    [ match Tilde **> (mkRoll <$> Var (%%% "prefixTerm"))
+    , match Bang **> mkUnroll <$> Var (%%% "prefixTerm")
+    , rename (Drop Id) Id AtomTerm
     ]
   where
-  mkExpand : SynthFun -> SynthFun
-  mkExpand x = MkParseFun (\tyCtx, tmCtx => [| Expand (x.try tyCtx tmCtx) |])
+  mkRoll : TermFun -> TermFun
+  mkRoll x = MkParseFun (\tyCtx, tmCtx => [| Roll (x.try tyCtx tmCtx) |])
 
-  mkContract : CheckFun -> CheckFun
-  mkContract x = MkParseFun (\tyCtx, tmCtx => [| Contract (x.try tyCtx tmCtx) |])
+  mkUnroll : TermFun -> TermFun
+  mkUnroll x = MkParseFun (\tyCtx, tmCtx => [| Unroll (x.try tyCtx tmCtx) |])
 
-SuffixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-SuffixCheck = mkSuffix <$> Seq [ WithBounds PrefixCheck , star (match Dot **> match TypeIdent) ]
+SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> match TypeIdent) ]
   where
-  mkSuffix : HList [WithBounds CheckFun, List String] -> CheckFun
-  mkSuffix [t, []] = t.val
+  mkSuffix : HList [TermFun, List String] -> TermFun
+  mkSuffix [t, []] = t
   mkSuffix [t, prjs] =
-    embed $
-    MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !((unembed t).try tyCtx tmCtx) prjs)
+    MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !(t.try tyCtx tmCtx) prjs)
 
-AppCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-AppCheck =
+AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+AppTerm =
   OneOf
     [ mkInj <$> Seq
       [ match TypeIdent
-      , weaken (S Z) SuffixCheck
+      , weaken (S Z) SuffixTerm
+      ]
+    , mkApp <$> Seq
+      [ OneOf {nils = [False, False, False]}
+        [ SuffixTerm
+        , mkMap <$> Seq
+          [ match Map
+          , enclose (match ParenOpen) (match ParenClose) $ Seq
+            [ match Backslash
+            , match TypeIdent
+            , match DoubleArrow
+            , rename Id (Drop Id) OpenType
+            ]
+          , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
+          , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
+          ]
+        , mkGetChildren <$> Seq
+          [ match GetChildren
+          , enclose (match ParenOpen) (match ParenClose) $ Seq
+            [ match Backslash
+            , match TypeIdent
+            , match DoubleArrow
+            , rename Id (Drop Id) OpenType
+            ]
+          , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
+          ]
+        ]
+      , star (weaken (S Z) SuffixTerm)
       ]
-    , mkApp <$> Seq [ WithBounds SuffixCheck , star (weaken (S Z) SuffixCheck) ]
     ]
   where
-  mkInj : HList [String, CheckFun] -> CheckFun
+  mkInj : HList [String, TermFun] -> TermFun
   mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx)
 
-  mkApp : HList [WithBounds CheckFun, List CheckFun] -> CheckFun
-  mkApp [t, []] = t.val
+  mkMap : HList [_, HList [_, String, _, TypeFun], TypeFun, TypeFun] -> TermFun
+  mkMap [_, [_, x, _, a], b, c] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Map (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+
+  mkGetChildren : HList [_, HList [_, String, _, TypeFun], TypeFun] -> TermFun
+  mkGetChildren [_, [_, x, _, a], b] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ GetChildren (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
+
+  mkApp : HList [TermFun, List TermFun] -> TermFun
+  mkApp [t, []] = t
   mkApp [fun, (arg :: args)] =
     MkParseFun (\tyCtx, tmCtx =>
-      pure $ Embed $
+      pure $
       App
-        !((unembed fun).try tyCtx tmCtx)
+        !(fun.try tyCtx tmCtx)
         (  !(arg.try tyCtx tmCtx)
         :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
 
-AnnotCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-AnnotCheck =
+AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+AnnotTerm =
   mkAnnot <$> Seq
-    [ AppCheck
+    [ AppTerm
     , option (match Colon **> rename Id (Drop Id) OpenType)
     ]
   where
-  mkAnnot : HList [CheckFun, Maybe TypeFun] -> CheckFun
+  mkAnnot : HList [TermFun, Maybe TypeFun] -> TermFun
   mkAnnot [t, Nothing] = t
-  mkAnnot [t, Just a] = embed $ MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |])
+  mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |])
 
 -- Open Terms
 
-LetCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-LetCheck =
+LetTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+LetTerm =
   match Let **>
   OneOf
     [ mkLet <$> Seq
@@ -453,71 +507,72 @@ LetCheck =
           , match Colon
           , rename Id (Drop Id) OpenType
           , match Equal
-          , Var (%% "openCheck")]
-        , match Equal **> unembed <$> WithBounds (Var (%% "openCheck"))
+          , Var (%%% "openTerm")]
+        , match Equal **> Var (%%% "openTerm")
         ]
       , match In
-      , Var (%% "openCheck")
+      , Var (%%% "openTerm")
       ]
     , mkLetType <$> Seq
       [ match TypeIdent
       , match Equal
       , rename Id (Drop Id) OpenType
       , match In
-      , Var (%% "openCheck")
+      , Var (%%% "openTerm")
       ]
     ]
   where
-  mkLet : HList [String, SynthFun, (), CheckFun] -> CheckFun
-  mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let x !(e.try tyCtx tmCtx) !(t.try tyCtx (tmCtx :< (x :- ()))))
+  mkLet : HList [String, TermFun, (), TermFun] -> TermFun
+  mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let !(e.try tyCtx tmCtx) (x ** !(t.try tyCtx (tmCtx :< x))))
 
-  mkLetType : HList [String, (), TypeFun, (), CheckFun] -> CheckFun
+  mkLetType : HList [String, (), TypeFun, (), TermFun] -> TermFun
   mkLetType [x, _, a, _, t] =
-    MkParseFun (\tyCtx, tmCtx => pure $ LetTy x !(a.try tyCtx) !(t.try (tyCtx :< (x :- ())) tmCtx))
+    MkParseFun (\tyCtx, tmCtx => pure $ LetTy !(a.try tyCtx) (x ** !(t.try (tyCtx :< x) tmCtx)))
 
   mkArrow : List TypeFun -> TypeFun -> TypeFun
   mkArrow [] cod = cod
   mkArrow (arg :: args) cod =
     MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
 
-  mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), CheckFun] -> SynthFun
+  mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), TermFun] -> TermFun
   mkBound [[], _, cod, _, t] =
     MkParseFun (\tyCtx, tmCtx =>
       pure $
       Annot !(t.try tyCtx tmCtx) !(cod.try tyCtx))
   mkBound [args, _, cod, _, t] =
-    let dom = foldl (\dom, [x, _, a] => dom :< (x :- ())) [<] args in
+    let bound = map (\[x, _, a] => x) args in
+    let tys = map (\[x, _, a] => a) args in
     MkParseFun (\tyCtx, tmCtx =>
       pure $
-      Annot (Abs dom !(t.try tyCtx (tmCtx ++ dom))) !((mkArrow (map (\[x, _, a] => a) args) cod).try tyCtx))
+      Annot (Abs (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx))
 
-AbsCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-AbsCheck =
+AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+AbsTerm =
   mkAbs <$> Seq
     [ match Backslash
     , sepBy1 (match Comma) (match TermIdent)
     , match DoubleArrow
-    , Var (%% "openCheck")
+    , Var (%%% "openTerm")
     ]
   where
-  mkAbs : HList [(), List1 String, (), CheckFun] -> CheckFun
+  mkAbs : HList [(), List1 String, (), TermFun] -> TermFun
   mkAbs [_, args, _, body] =
-    let args = foldl (\args, x => args :< (x :- ())) [<] args in
-    MkParseFun (\tyCtx, tmCtx => Abs args <$> body.try tyCtx (tmCtx ++ args))
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Abs (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
 
-CaseCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-CaseCheck =
+CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+CaseTerm =
   (\[f, x] => f x) <$>
   Seq
     [ OneOf
       [ mkCase <$> Seq
         [ match Case
-        , unembed <$> WithBounds (Var $ %% "openCheck")
+        , Var (%%% "openTerm")
         , match Of
         ]
       , mkFoldCase <$> Seq
         [ match FoldCase
-        , unembed <$> WithBounds (Var $ %% "openCheck")
+        , Var (%%% "openTerm")
         , match By
         ]
       ]
@@ -528,66 +583,66 @@ CaseCheck =
           [ match TypeIdent
           , match TermIdent
           , match DoubleArrow
-          , Var (%% "openCheck")
+          , Var (%%% "openTerm")
           ])
     ]
   where
   Cases : Type
-  Cases = List (WithBounds $ HList [String, String, (), CheckFun])
+  Cases = List (WithBounds $ HList [String, String, (), TermFun])
 
   mkBranch :
-    HList [String, String, (), CheckFun] ->
-    Assoc (ParseFun [(), ()] $ \tyCtx, tmCtx => (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))))
+    HList [String, String, (), TermFun] ->
+    Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term tyCtx (tmCtx :< x)))
   mkBranch [tag, bound, _, branch] =
-    tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< (bound :- ())))))
+    tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
 
-  mkCase : HList [_, SynthFun, _] -> Cases -> CheckFun
+  mkCase : HList [_, TermFun, _] -> Cases -> TermFun
   mkCase [_, target, _] branches =
     let branches = map (map mkBranch) branches in
     MkParseFun (\tyCtx, tmCtx =>
       [| Case (target.try tyCtx tmCtx) (tryRow2 branches tyCtx tmCtx) |])
 
-  mkFoldCase : HList [_, SynthFun, _] -> Cases -> CheckFun
+  mkFoldCase : HList [_, TermFun, _] -> Cases -> TermFun
   mkFoldCase [_, target, _] branches =
     let branches = map (map mkBranch) branches in
     MkParseFun (\tyCtx, tmCtx =>
       pure $
       Fold
         !(target.try tyCtx tmCtx)
-        "__tmp"
-        (Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< ("__tmp" :- ())))))
+        ("__tmp" ** Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
 
-FoldCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun
-FoldCheck =
+FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
+FoldTerm =
   mkFold <$> Seq
     [ match Fold
-    , unembed <$> WithBounds (Var (%% "openCheck"))
+    , Var (%%% "openTerm")
     , match By
     , enclose (match ParenOpen) (match ParenClose) $
       Seq
         [ match Backslash
         , match TermIdent
         , match DoubleArrow
-        , Var (%% "openCheck")
+        , Var (%%% "openTerm")
         ]
     ]
   where
-  mkFold : HList [(), SynthFun, (), HList [(), String, (), CheckFun]] -> CheckFun
+  mkFold : HList [(), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
   mkFold [_, target, _, [_, arg, _, body]] =
-    MkParseFun (\tyCtx, tmCtx => pure $ Fold !(target.try tyCtx tmCtx) arg !(body.try tyCtx (tmCtx :< (arg :- ()))))
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Fold !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
 
 export
-OpenCheck : InkyParser False [<] [<] CheckFun
-OpenCheck =
-  Fix "openCheck" $ OneOf
-    [ LetCheck
-    , AbsCheck
-    , CaseCheck
-    , FoldCheck
-    , AnnotCheck
+OpenTerm : InkyParser False [<] [<] TermFun
+OpenTerm =
+  Fix "openTerm" $ OneOf
+    [ LetTerm
+    , AbsTerm
+    , CaseTerm
+    , FoldTerm
+    , AnnotTerm
     ]
 
 %hint
 export
-OpenCheckWf : So (wellTyped EqI [<] [<] [<] [<] OpenCheck)
-OpenCheckWf = ?d -- Oh
+OpenTermWf : So (wellTyped EqI [<] [<] [<] [<] OpenTerm)
+OpenTermWf = Oh
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 3bed88b..a9055d4 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,116 +1,130 @@
 module Inky.Term.Pretty
 
-import Inky.Context
+import Data.Singleton
+
+import Inky.Decidable.Maybe
 import Inky.Term
 import Inky.Type.Pretty
 import Text.PrettyPrint.Prettyprinter
 
-appPrec, prjPrec, expandPrec, annotPrec,
-  letPrec, absPrec, injPrec, tupPrec, casePrec, contractPrec, foldPrec : Prec
+appPrec, prjPrec, unrollPrec, annotPrec,
+  letPrec, absPrec, injPrec, tupPrec, casePrec, rollPrec, foldPrec : Prec
 appPrec = App
 prjPrec = User 9
-expandPrec = PrefixMinus
+unrollPrec = PrefixMinus
 annotPrec = Equal
 letPrec = Open
 absPrec = Open
 injPrec = App
 tupPrec = Open
 casePrec = Open
-contractPrec = PrefixMinus
+rollPrec = PrefixMinus
 foldPrec = Open
 
 export
-prettySynth :
-  {tyCtx, tmCtx : Context ()} ->
-  SynthTerm tyCtx tmCtx -> Prec -> Doc ann
-export
-prettyCheck :
-  {tyCtx, tmCtx : Context ()} ->
-  CheckTerm tyCtx tmCtx -> Prec -> Doc ann
-prettyAllCheck :
-  {tyCtx, tmCtx : Context ()} ->
-  List (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
-prettyCheckCtx :
-  {tyCtx, tmCtx : Context ()} ->
-  Row (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann)
-prettyCheckCtxBinding :
-  {tyCtx, tmCtx : Context ()} ->
-  Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann)
+prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
+prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> Prec -> List (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> Prec -> SnocList (Doc ann)
+prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
 
-prettySynth (Var i) d = pretty (unVal $ nameOf i)
-prettySynth (Lit k) d = pretty k
-prettySynth Suc d = pretty "suc"
-prettySynth (App e ts) d =
-  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
-    concatWith (surround line) (prettySynth e appPrec :: prettyAllCheck ts appPrec)
-prettySynth (Prj e x) d =
-  parenthesise (d > prjPrec) $ group $ align $ hang 2 $
-    prettySynth e prjPrec <+> line' <+> "." <+> pretty x
-prettySynth (Expand e) d =
-  "!" <+>
-  (parenthesise (d > expandPrec) $ group $ align $ hang 2 $
-    prettySynth e expandPrec)
-prettySynth (Annot t a) d =
-  parenthesise (d > annotPrec) $ group $ align $ hang 2 $
-    prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
+prettyTerm t d =
+  case isLit t <|> isCheckLit t of
+    Just k => pretty k
+    Nothing =>
+      if isSuc t
+      then pretty "suc"
+      else lessPrettyTerm t d
+
+prettyAllTerm [] d = []
+prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
 
-prettyCheck (LetTy x a t) d =
+prettyTermCtx [<] d = [<]
+prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
+
+prettyCases [<] = [<]
+prettyCases (ts :< (l :- (x ** t))) =
+  prettyCases ts :< (pretty l <++> pretty x <++> "=>" <++> prettyTerm t Open)
+
+
+lessPrettyTerm (Annot t a) d =
+  parenthesise (d > annotPrec) $ group $ align $ hang 2 $
+    prettyTerm t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
+lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
+lessPrettyTerm (Let e (x ** t)) d =
   parenthesise (d > letPrec) $ group $ align $
-    "let" <++>
     (group $ align $ hang 2 $
-      pretty x <++> "=" <+> line <+> prettyType a letPrec
+      pretty x <++> "=" <+> line <+> prettyTerm e letPrec
     ) <+> line <+>
     "in" <+> line <+>
-    prettyCheck t letPrec
-prettyCheck (Let x e t) d =
+    prettyTerm t letPrec
+lessPrettyTerm (LetTy a (x ** t)) d =
   parenthesise (d > letPrec) $ group $ align $
-    "let" <++>
     (group $ align $ hang 2 $
-      pretty x <++> "=" <+> line <+> prettySynth e letPrec
+      pretty x <++> "=" <+> line <+> prettyType a letPrec
     ) <+> line <+>
     "in" <+> line <+>
-    prettyCheck t letPrec
-prettyCheck (Abs bound t) d =
-  parenthesise (d > absPrec) $ group $ align $ hang 2 $
-    "\\" <+> concatWith (surround $ "," <+> line) (bindings bound <>> []) <++> "=>" <+> line <+>
-    prettyCheck t absPrec
-  where
-  bindings : Context () -> SnocList (Doc ann)
-  bindings [<] = [<]
-  bindings (bound :< (x :- ())) = bindings bound :< pretty x
-prettyCheck (Inj k t) d =
-  parenthesise (d > injPrec) $ group $ align $ hang 2 $
-    pretty k <+> line <+> prettyCheck t injPrec
-prettyCheck (Tup ts) d =
+    prettyTerm t letPrec
+lessPrettyTerm (Abs (bound ** t)) d =
+  parenthesise (d > absPrec) $ group $ hang 2 $
+    "\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
+    prettyTerm t absPrec
+lessPrettyTerm (App (Map (x ** a) b c) ts) d =
+  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+    concatWith (surround line)
+      (  pretty "map"
+      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
+      :: prettyType b appPrec
+      :: prettyType c appPrec
+      :: prettyAllTerm ts appPrec)
+lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
+  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+    concatWith (surround line)
+      (  pretty "getChildren"
+      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
+      :: prettyType b appPrec
+      :: prettyAllTerm ts appPrec)
+lessPrettyTerm (App f ts) d =
+  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+    concatWith (surround line) (prettyTerm f appPrec :: prettyAllTerm ts appPrec)
+lessPrettyTerm (Tup (MkRow ts _)) d =
   enclose "<" ">" $ group $ align $ hang 2 $
-    concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec)
-prettyCheck (Case e ts) d =
+    concatWith (surround $ "<" <+> line) (prettyTermCtx ts tupPrec <>> [])
+lessPrettyTerm (Prj e l) d =
+  parenthesise (d > prjPrec) $ group $ align $ hang 2 $
+    prettyTerm e prjPrec <+> line' <+> "." <+> pretty l
+lessPrettyTerm (Inj l t) d =
+  parenthesise (d >= injPrec) $ group $ align $ hang 2 $
+    pretty l <+> line <+> prettyTerm t absPrec
+lessPrettyTerm (Case e (MkRow ts _)) d =
   parenthesise (d > casePrec) $ group $ align $ hang 2 $
-    "case" <++> prettySynth e casePrec <++> "of" <+> line <+>
+    "case" <++> prettyTerm e casePrec <++> "of" <+> hardline <+>
     (braces $ group $ align $ hang 2 $
-      concatWith (surround $ ";" <+> line) $
-      prettyCheckCtxBinding ts casePrec)
-prettyCheck (Contract t) d =
-  "~" <+>
-  (parenthesise (d > contractPrec) $ group $ align $ hang 2 $
-    prettyCheck t contractPrec)
-prettyCheck (Fold e x t) d =
+      concatWith (surround $ ";" <+> hardline) $
+      prettyCases ts <>> [])
+lessPrettyTerm (Roll t) d =
+  pretty "~" <+>
+  (parenthesise (d > rollPrec) $ group $ align $ hang 2 $ prettyTerm t rollPrec)
+lessPrettyTerm (Unroll e) d =
+  pretty "!" <+>
+  (parenthesise (d > unrollPrec) $ group $ align $ hang 2 $ prettyTerm e unrollPrec)
+lessPrettyTerm (Fold e (x ** t)) d =
   parenthesise (d > foldPrec) $ group $ align $ hang 2 $
-    "fold" <++> prettySynth e foldPrec <++> "by" <+> line <+>
+    "fold" <++> prettyTerm e foldPrec <++> "by" <+> hardline <+>
     (parens $ group $ align $ hang 2 $
-      "\\" <+> pretty x <++> "=>" <+> line <+> prettyCheck t foldPrec)
-prettyCheck (Embed e) d = prettySynth e d
-
-prettyAllCheck [] d = []
-prettyAllCheck (t :: ts) d = prettyCheck t d :: prettyAllCheck ts d
-
-prettyCheckCtx [<] d = []
-prettyCheckCtx (ts :< (x :- t)) d =
-  (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyCheck t d) ::
-  prettyCheckCtx ts d
-
-prettyCheckCtxBinding [<] d = []
-prettyCheckCtxBinding (ts :< (x :- (y ** t))) d =
-  (group $ align $ hang 2 $
-    pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) ::
-  prettyCheckCtxBinding ts d
+      "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
+lessPrettyTerm (Map (x ** a) b c) d =
+  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+    concatWith (surround line)
+      [ pretty "map"
+      , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
+      , prettyType b appPrec
+      , prettyType c appPrec
+      ]
+lessPrettyTerm (GetChildren (x ** a) b) d =
+  parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+    concatWith (surround line)
+      [ pretty "getChildren"
+      , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
+      , prettyType b appPrec
+      ]