Improve syntactic sugar.

Sugar makes programs nicer to write.

10 files changed, 229 insertions, 127 deletions

diff --git a/inky.ipkg b/inky.ipkg
index bbd7aaa..493dea2 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -23,6 +23,7 @@ modules
   , Inky.Term.Pretty.Error
   , Inky.Term.Recompute
   , Inky.Term.Substitution
+  , Inky.Term.Sugar
   , Inky.Type
   , Inky.Type.Pretty
   , Inky.Type.Substitution
diff --git a/program/exp.prim b/program/exp.prim
index 3c07ec1..8af7c3f 100644
--- a/program/exp.prim
+++ b/program/exp.prim
@@ -1,3 +1,3 @@
-let add (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => y; S k => ~(S k)} in
+let add (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => y; S k => suc k} in
 let mul (x : Nat) (y : Nat) : Nat = foldcase x by {Z u => 0; S k => add y k} in
 \x, y => foldcase y by {Z u => 1; S k => mul x k}
diff --git a/program/reducer.prim b/program/reducer.prim
index ead7fbc..0a0517e 100644
--- a/program/reducer.prim
+++ b/program/reducer.prim
@@ -31,7 +31,7 @@ let index (xs : List SysT) : Nat -> SysT =
     ; C p => \k => case !k of {Z u => p.H; S k => p.T k}
     }
 in
-let shift = map (\X => List X) SysT SysT (\t => rename t suc) in
+let shift = map (\X => List X) SysT SysT (\t => rename t (\x => suc x)) in
 let sub (t : SysT) : List SysT -> SysT =
   foldcase t by
     { Var n => \env => index env n
@@ -40,22 +40,23 @@ let sub (t : SysT) : List SysT -> SysT =
     ; Primrec p => \env =>
       ~(Primrec
          < Zero: p.Zero env
-         , Suc: p.Suc ~(C <H: ~(Var 0), T: shift env>)
+         , Suc: p.Suc (cons ~(Var 0) (shift env))
          , Target: p.Target env
          >)
-    ; Abs f => \env => ~(Abs (f ~(C <H: ~(Var 0), T: shift env>)))
+    ; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env))))
     ; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg env>)
     }
 in
 let app (fun : SysT) (arg : SysT) (smaller : Bool) : Stepped =
-  let default : Stepped = <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
+  let default : Stepped =
+    <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller>
   in
   case !fun of
     { Var n => default
     ; Zero u => default
     ; Suc t => default
     ; Primrec p => default
-    ; Abs t => <Term: sub t ~(C <H: arg, T: ~(N <>)>), Smaller: T <>>
+    ; Abs t => <Term: sub t [arg], Smaller: T <>>
     ; App t => default
     }
 in
@@ -67,10 +68,7 @@ let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped =
     { Var n => default
     ; Zero u => <Term: z, Smaller: T <>>
     ; Suc t =>
-      < Term:
-          sub s ~(C <H: ~(Primrec <Zero: z, Suc: s, Target: t>), T: ~(N <>)>)
-      , Smaller: T <>
-      >
+      <Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>>
     ; Primrec p => default
     ; Abs t => default
     ; App t => default
@@ -91,13 +89,13 @@ let step (t : SysT) : Stepped =
             (or t.Zero.Smaller t.Suc.Smaller)
         ; T u =>
           < Term:
-              ~(Primrec
-                 (map
-                   (\X => <Zero: X, Suc: X, Target: X>)
-                   Stepped
-                   SysT
-                   (\p => p.Term)
-                   t))
+            ~(Primrec
+               (map
+                 (\X => <Zero: X, Suc: X, Target: X>)
+                 Stepped
+                 SysT
+                 (\p => p.Term)
+                 t))
           , Smaller: T <>
           >
         }
@@ -107,8 +105,7 @@ let step (t : SysT) : Stepped =
         { F u => app t.Fun.Term t.Arg.Term t.Fun.Smaller
         ; T u =>
           < Term:
-              ~(App
-                 (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
+            ~(App (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t))
           , Smaller: T <>
           >
         }
diff --git a/src/Inky.idr b/src/Inky.idr
index 66124c6..ad3a503 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -67,14 +67,14 @@ checkType a = do
     | False `Because` bad => throw "type ill-formed"
   pure (Forget wf)
 
-checkTerm :
-  (a : Ty [<]) -> (t : Term mode m [<] [<]) ->
-  HasErr (NotChecks [<] [<] a t) es =>
-  App es (Erased $ Checks [<] [<] a t)
-checkTerm a t = do
-  let True `Because` prf = checks [<] [<] a t
-    | False `Because` contra => throw contra
-  pure (Forget prf)
+synthTerm :
+  (t : Term mode m [<] [<]) ->
+  HasErr (NotSynths [<] [<] t) es =>
+  App es (Subset (Ty [<]) (Synths [<] [<] t))
+synthTerm t = do
+  let Just a `Because` prf = synths [<] [<] t
+    | Nothing `Because` contra => throw contra
+  pure (Element a prf)
 
 printType :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
@@ -88,27 +88,25 @@ printTerm :
 printTerm a = do
   primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open
 
-printCheckError :
+printSynthError :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {a : Ty [<]} -> {t : Term mode Bounds [<] [<]} ->
-  NotChecks [<] [<] a t -> App es ()
-printCheckError contra =
+  {t : Term mode Bounds [<] [<]} ->
+  NotSynths [<] [<] t -> App es ()
+printSynthError contra =
   primIO $ renderIO $ layoutSmart opts $
   concatWith (surround hardline) $
   map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
-  prettyNotChecks contra
+  prettyNotSynths contra
 
 compileTerm :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {a : Ty [<]} ->
   {t : Term mode m [<] [<]} ->
-  (0 wf : WellFormed a) ->
-  (0 prf : Checks [<] [<] a t) ->
+  (0 prf : Synths [<] [<] t a) ->
   App es ()
-compileTerm wf prf =
+compileTerm prf =
   primIO $ renderIO $ layoutSmart opts $
   pretty "(use-modules (ice-9 match))" <+> line <+>
-  parens (hang 1 $ pretty "define main" <+> line <+> group (compileChecks [<] [<] wf prf))
+  parens (hang 1 $ pretty "define main" <+> line <+> group (compileSynths [<] [<] prf))
 
 readFile : FileIO es => File -> App es String
 readFile f = do
@@ -257,17 +255,17 @@ main = run {l = MayThrow} $ do
           toks <- handle {err = String} (lexInkyString txt) pure abortErr
           t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          a <-
-            maybe (pure (TArrow TNat TNat))
+          t <-
+            maybe (pure t)
               (\path => do
                 txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
                 toks <- handle {err = String} (lexInkyString txt) pure abortErr
                 a <- handle {err = String} (parseType toks) pure abortErr
                 handle {err = String} (checkType a) (const $ pure ()) abortErr
-                pure a)
+                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
               type
-          handle {err = NotChecks [<] [<] a t} (checkTerm a t) (const $ pure ())
-            (\contra => do printCheckError contra; primIO exitFailure)
+          handle {err = NotSynths [<] [<] t} (synthTerm t) (const $ pure ())
+            (\contra => do printSynthError contra; primIO exitFailure)
         ]
       ]
     , "compile" ::=
@@ -279,20 +277,19 @@ main = run {l = MayThrow} $ do
           toks <- handle {err = String} (lexInkyString txt) pure abortErr
           t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          Element a wf <-
-            the (App _ (Subset (Ty [<]) WellFormed)) $
-            maybe (pure (Element (TArrow TNat TNat) %search))
+          t <-
+            maybe (pure t)
               (\path => do
                 txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
                 toks <- handle {err = String} (lexInkyString txt) pure abortErr
                 a <- handle {err = String} (parseType toks) pure abortErr
-                Forget wf <- handle {err = String} (checkType a) pure abortErr
-                pure (Element a wf))
+                handle {err = String} (checkType a) (const $ pure ()) abortErr
+                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
               type
-          Forget prf <-
-            handle {err = NotChecks [<] [<] a t} (checkTerm a t) pure
-              (\contra => do printCheckError contra; primIO exitFailure)
-          compileTerm wf prf
+          Element _ prf <-
+            handle {err = NotSynths [<] [<] t} (synthTerm t) pure
+              (\contra => do printSynthError contra; primIO exitFailure)
+          compileTerm prf
         ]
       ]
     ]
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 54ac9fe..8fd15aa 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -548,40 +548,3 @@ Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where
   uninhabited (ChecksNS Case) impossible
   uninhabited (ChecksNS Roll) impossible
   uninhabited (ChecksNS Fold) impossible
-
--- Sugar -----------------------------------------------------------------------
-
-public export
-CheckLit : m -> Nat -> Term mode m tyCtx tmCtx
-CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
-CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n)
-
-public export
-Lit : m -> Nat -> Term mode m tyCtx tmCtx
-Lit meta n = Annot meta (CheckLit meta n) TNat
-
-public export
-Suc : m -> Term mode m tyCtx tmCtx
-Suc meta =
-  Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x"))))
-    (TArrow TNat TNat)
-
-export
-isCheckLit : Term mode m tyCtx tmCtx -> Maybe Nat
-isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0
-isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t
-isCheckLit _ = Nothing
-
-export
-isLit : Term mode m tyCtx tmCtx -> Maybe Nat
-isLit (Annot _ t a) =
-  if (alpha {ctx2 = [<]} a TNat).does
-  then isCheckLit t
-  else Nothing
-isLit _ = Nothing
-
-export
-isSuc : Term mode m tyCtx tmCtx -> Bool
-isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) =
-  does (alpha {ctx2 = [<]} a (TArrow TNat TNat))
-isSuc _ = False
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 402f623..829561a 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -204,6 +204,7 @@ fallbackCheck prf p a =
     (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $
   (b := p) >=> alpha b a
 
+export
 synths :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 6fd4044..1f9d983 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -18,6 +18,7 @@ import Flap.Parser
 
 import Inky.Data.Row
 import Inky.Term
+import Inky.Term.Sugar
 import Inky.Type
 
 import Text.Lexer
@@ -39,6 +40,7 @@ data InkyKind
   | Nat
   | List
   | Suc
+  | Cons
   | Map
   | ParenOpen
   | ParenClose
@@ -76,6 +78,7 @@ export
   Nat == Nat = True
   List == List = True
   Suc == Suc = True
+  Cons == Cons = True
   Map == Map = True
   ParenOpen == ParenOpen = True
   ParenClose == ParenClose = True
@@ -114,6 +117,7 @@ Interpolation InkyKind where
   interpolate Nat = "'Nat'"
   interpolate List = "'List'"
   interpolate Suc = "'suc'"
+  interpolate Cons = "'cons'"
   interpolate Map = "'map'"
   interpolate ParenOpen = "'('"
   interpolate ParenClose = "')'"
@@ -156,6 +160,7 @@ TokenKind InkyKind where
   tokValue Nat = const ()
   tokValue List = const ()
   tokValue Suc = const ()
+  tokValue Cons = const ()
   tokValue Map = const ()
   tokValue ParenOpen = const ()
   tokValue ParenClose = const ()
@@ -190,6 +195,7 @@ keywords =
   , ("Nat", Nat)
   , ("List", List)
   , ("suc", Suc)
+  , ("cons", Cons)
   , ("map", Map)
   ]
 
@@ -386,7 +392,10 @@ AtomTerm =
   OneOf
     [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
     , mkLit <$> WithBounds (match Lit)
-    , mkSuc <$> WithBounds (match Suc)
+    , mkList <$> WithBounds (
+        enclose (match BracketOpen) (match BracketClose) $
+        sepBy (match Comma) $
+        Var (%%% "openTerm"))
     , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
         RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
     , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
@@ -395,8 +404,13 @@ AtomTerm =
   mkLit : WithBounds Nat -> TermFun
   mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k.bounds k.val))
 
-  mkSuc : WithBounds () -> TermFun
-  mkSuc x = MkParseFun (\_, _ => pure (Suc x.bounds))
+  mkList : WithBounds (List TermFun) -> TermFun
+  mkList xs =
+    MkParseFun (\tyCtx, tmCtx =>
+      foldr
+        (\x, ys => pure $ Cons xs.bounds !(x.try tyCtx tmCtx) !ys)
+        (pure $ Nil xs.bounds)
+        xs.val)
 
   mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun
   mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx)
@@ -431,6 +445,15 @@ AppTerm =
       [ WithBounds (match TypeIdent)
       , weaken (S Z) SuffixTerm
       ]
+    , mkSuc <$> Seq
+      [ WithBounds (match Suc)
+      , weaken (S Z) SuffixTerm
+      ]
+    , mkCons <$> Seq
+      [ WithBounds (match Cons)
+      , weaken (S Z) SuffixTerm
+      , weaken (S Z) SuffixTerm
+      ]
     , mkApp <$> Seq
       [ OneOf
         [ WithBounds SuffixTerm
@@ -453,6 +476,14 @@ AppTerm =
   mkInj : HList [WithBounds String, TermFun] -> TermFun
   mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx)
 
+  mkSuc : HList [WithBounds _, TermFun] -> TermFun
+  mkSuc [x, t] = MkParseFun (\tyCtx, tmCtx => Suc x.bounds <$> t.try tyCtx tmCtx)
+
+  mkCons : HList [WithBounds _, TermFun, TermFun] -> TermFun
+  mkCons [x, t, u] =
+    MkParseFun (\tyCtx, tmCtx =>
+      pure $ Cons x.bounds !(t.try tyCtx tmCtx) !(u.try tyCtx tmCtx))
+
   mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun
   mkMap [m, [_, x, _, a], b, c] =
     MkParseFun (\tyCtx, tmCtx =>
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index a4bb1e1..0523362 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -5,6 +5,7 @@ import Data.String
 
 import Inky.Term
 import Inky.Type.Pretty
+import Inky.Term.Sugar
 
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
@@ -46,26 +47,53 @@ Ord TermPrec where
 export
 prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
 prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term mode m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann)
 prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
-prettyLet : Doc ann -> Doc ann -> Doc ann
+prettyLet :
+  (eqLine : Doc ann) ->
+  (doc : List String) ->
+  (bound, body : Doc ann) ->
+  Doc ann
 lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
 
 prettyTerm t d =
-  case isLit t <|> isCheckLit t of
+  case isLit t of
     Just k => pretty k
     Nothing =>
-      if isSuc t
-      then pretty "suc"
-      else lessPrettyTerm t d
+      case isSuc t of
+        Just u =>
+          group $ align $ hang 2 $ parenthesise (d < App) $
+            concatWith (surround line) [pretty "suc", prettyTerm (assert_smaller t u) Suffix]
+        Nothing => case isList t of
+          Just ts =>
+            let ts = prettyAllTerm (assert_smaller t ts) Open in
+            group $ align $ flatAlt
+              (enclose ("[" <++> neutral) (line <+> "]") $
+                concatWith (surround $ line <+> "," <++> neutral) ts)
+              (enclose "[" "]" $ concatWith (surround $ "," <++> neutral) ts)
+          Nothing => case isCons t of
+            Just (hd, tl) =>
+              group $ align $ hang 2 $ parenthesise (d < App) $
+                concatWith (surround line)
+                  [ pretty "cons"
+                  , prettyTerm (assert_smaller t hd) Suffix
+                  , prettyTerm (assert_smaller t tl) Suffix
+                  ]
+            Nothing => lessPrettyTerm t d
 
 prettyAllTerm [] d = []
 prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
 
-prettyTermCtx [<] d = [<]
-prettyTermCtx (ts :< (l :- t)) d =
-  prettyTermCtx ts d :<
-  (group $ hang 2 $ pretty l <+> ":" <+> line <+> prettyTerm t d)
+prettyTermCtx [<] = [<]
+prettyTermCtx (ts :< (l :- Abs _ (bound ** t))) =
+ prettyTermCtx ts :<
+ (group $ align $
+   pretty l <+> ":" <++>
+     "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
+   prettyTerm t Open)
+prettyTermCtx (ts :< (l :- t)) =
+  prettyTermCtx ts :<
+  (group $ align $ pretty l <+> ":" <+> line <+> prettyTerm t Open)
 
 prettyCases [<] = [<]
 prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) =
@@ -80,12 +108,21 @@ prettyCases (ts :< (l :- (x ** t))) =
     pretty l <++> pretty x <++> "=>" <+> line <+>
     prettyTerm t Open)
 
-prettyLet binding term =
+prettyLet eqLine [] bound body =
+  group $
   (group $
-    pretty "let" <++>
-    (group $ hang (-2) $ binding) <+> line <+>
+    hang 2
+      (group (pretty "let" <++> eqLine) <+> line <+>
+       group bound) <+> line <+>
     "in") <+> line <+>
-  term
+  group body
+prettyLet eqLine doc bound body  =
+  (hang 2 $
+    group (pretty "let" <++> eqLine) <+> hardline <+>
+    concatMap (enclose "--" hardline . pretty) doc <+>
+    group bound) <+> hardline <+>
+  "in" <+> line <+>
+  group body
 
 lessPrettyTerm (Annot _ t a) d =
   group $ align $ parenthesise (d < Annot) $
@@ -95,22 +132,22 @@ lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
 lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
   let (binds, cod, rest) = groupBinds bound a in
   let binds = map (\x => parens (pretty x.name <++> ":" <++> prettyType x.value Open)) binds in
-  let doc = concatMap (enclose "--" hardline . pretty) meta.doc in
   group $ align $ parenthesise (d < Open) $
   prettyLet
-    ( (group $ hang 2 $ flatAlt
+   (group $ hang 2 $ flatAlt
         ( pretty x <+> line <+>
           concatWith (surround line) binds <+> line <+>
-          ":" <++> prettyType cod Open
+          ":" <++> prettyType cod Open <++> "=" <+>
+          if null rest then neutral
+          else line <+> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>"
         )
-        (pretty x <++> concatWith (<++>) binds <++> ":" <++> prettyType cod Open)
-      ) <++> "=" <+>
-      ( if null rest
-        then neutral
-        else neutral <++> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>")
-      <+> line <+> doc <+> prettyTerm e Open
-    )
-    (prettyTerm t Open)
+        ( pretty x <++> concatWith (<++>) binds <++> ":" <++> prettyType cod Open <++> "=" <+>
+          if null rest then neutral
+          else neutral <++> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>"
+        ))
+   meta.doc
+   (prettyTerm e Open)
+   (prettyTerm t Open)
   where
   groupBinds : List String -> Ty tyCtx -> (List (Assoc $ Ty tyCtx), Ty tyCtx, List String)
   groupBinds [] a = ([], a, [])
@@ -119,24 +156,25 @@ lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
     ((x :- a) :: binds, cod, rest)
   groupBinds xs a = ([], a, xs)
 lessPrettyTerm (Let meta (Annot _ e a) (x ** t)) d =
-  let doc = concatMap (enclose "--" hardline . pretty) meta.doc in
   group $ align $ parenthesise (d < Open) $
   prettyLet
-    ( pretty x <++> ":" <++> prettyType a Open <++> "=" <+> line <+>
-      doc <+> prettyTerm e Open
-    )
+    (pretty x <+> line <+> ":" <++> prettyType a Open <++> "=")
+    meta.doc
+    (prettyTerm e Open)
     (prettyTerm t Open)
 lessPrettyTerm (Let meta e (x ** t)) d =
-  let doc = concatMap (enclose "--" hardline . pretty) meta.doc in
   group $ align $ parenthesise (d < Open) $
   prettyLet
-    (pretty x <++> "=" <+> line <+> doc <+> prettyTerm e Open)
+    (pretty x <++> "=")
+    meta.doc
+    (prettyTerm e Open)
     (prettyTerm t Open)
 lessPrettyTerm (LetTy meta a (x ** t)) d =
-  let doc = concatMap (enclose "--" hardline . pretty) meta.doc in
   group $ align $ parenthesise (d < Open) $
   prettyLet
-    (pretty x <++> "=" <+> line <+> doc <+> prettyType a Open)
+    (pretty x <++> "=")
+    meta.doc
+    (prettyType a Open)
     (prettyTerm t Open)
 lessPrettyTerm (Abs _ (bound ** t)) d =
   group $ hang 2 $ parenthesise (d < Open) $
@@ -154,7 +192,7 @@ lessPrettyTerm (App _ f ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
 lessPrettyTerm (Tup _ (MkRow ts _)) d =
-  let parts = prettyTermCtx ts Open <>> [] in
+  let parts = prettyTermCtx ts <>> [] in
   group $ align $ enclose "<" ">" $
     flatAlt
       (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
@@ -168,7 +206,7 @@ lessPrettyTerm (Inj _ l t) d =
 lessPrettyTerm (Case _ e (MkRow ts _)) d =
   let parts = prettyCases ts <>> [] in
   group $ align $ hang 2 $ parenthesise (d < Open) $
-    (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
+    (group $ "case" <++> prettyTerm e Open <++> "of") <+> line <+>
     (braces $ flatAlt
       (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
       (concatWith (surround $ ";" <++> neutral) parts))
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index a5ee2fa..d87178f 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -22,6 +22,7 @@ Pretty (ChecksOnly t) where
   pretty Roll = "rolling"
   pretty Fold = "fold"
 
+export
 prettyNotSynths :
   {tyCtx, tmCtx : SnocList String} ->
   {e : Term mode m tyCtx tmCtx} ->
@@ -99,7 +100,7 @@ prettyNotSynths (PrjNS2 prf f) =
       , pretty "cannot project non-product type" <+> line <+>
         prettyType a Open
       )]
-prettyNotSynths (PrjNS3 {l, as} prf contra) =
+prettyNotSynths (PrjNS3 {l, e, as} prf contra) =
   case synthsRecompute prf of
     Val (TProd as) =>
       [(e.meta
diff --git a/src/Inky/Term/Sugar.idr b/src/Inky/Term/Sugar.idr
new file mode 100644
index 0000000..477df5e
--- /dev/null
+++ b/src/Inky/Term/Sugar.idr
@@ -0,0 +1,73 @@
+module Inky.Term.Sugar
+
+import Flap.Decidable
+import Inky.Term
+
+-- Naturals --------------------------------------------------------------------
+
+export
+Zero : m -> Term mode m tyCtx tmCtx
+Zero meta = Roll meta (Inj meta "Z" $ Tup meta [<])
+
+export
+Suc : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+Suc meta t = Roll meta (Inj meta "S" t)
+
+export
+isZero : Term mode m tyCtx tmCtx -> Bool
+isZero (Roll _ (Inj _ "Z" $ Tup _ $ MkRow [<] _)) = True
+isZero _ = False
+
+export
+isSuc : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx)
+isSuc (Roll _ (Inj _ "S" t)) = Just t
+isSuc _ = Nothing
+
+export
+Lit : m -> Nat -> Term mode m tyCtx tmCtx
+Lit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
+Lit meta (S n) = Suc meta (Lit meta n)
+
+export
+isLit : Term mode m tyCtx tmCtx -> Maybe Nat
+isLit t =
+  if isZero t then Just 0
+  else do
+    u <- isSuc t
+    k <- isLit (assert_smaller t u)
+    pure (S k)
+
+-- Lists -----------------------------------------------------------------------
+
+export
+Nil : m -> Term mode m tyCtx tmCtx
+Nil meta = Roll meta (Inj meta "N" $ Tup meta [<])
+
+export
+Cons : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+Cons meta t ts = Roll meta (Inj meta "C" $ Tup meta [<"H" :- t, "T" :- ts])
+
+export
+fromList : m -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
+fromList meta [] = Nil meta
+fromList meta (t :: ts) = Cons meta t (fromList meta ts)
+
+export
+isNil : Term mode m tyCtx tmCtx -> Bool
+isNil (Roll _ (Inj _ "N" $ Tup _ $ MkRow [<] _)) = True
+isNil _ = False
+
+export
+isCons : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx, Term mode m tyCtx tmCtx)
+isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"H" :- t, "T" :- ts] _)) = Just (t, ts)
+isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"T" :- ts, "H" :- t] _)) = Just (t, ts)
+isCons _ = Nothing
+
+export
+isList : Term mode m tyCtx tmCtx -> Maybe (List $ Term mode m tyCtx tmCtx)
+isList t =
+  if isNil t then Just []
+  else do
+    (hd, tl) <- isCons t
+    tl <- isList (assert_smaller t tl)
+    pure (hd :: tl)