Improve syntactic sugar.

Sugar makes programs nicer to write.

5 files changed, 183 insertions, 39 deletions

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)