Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.

1 files changed, 5 insertions, 232 deletions

diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 1ff0de0..a2e6407 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,11 +1,8 @@
 module Inky.Term.Pretty
 
-import Data.List.Quantifiers
 import Data.Singleton
 import Data.String
-import Data.These
 
-import Inky.Decidable.Maybe
 import Inky.Term
 import Inky.Type.Pretty
 
@@ -47,12 +44,12 @@ Ord TermPrec where
   compare Open d2 = GT
 
 export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+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)
+prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
 prettyLet : Doc ann -> Doc ann -> Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
 
 prettyTerm t d =
   case isLit t <|> isCheckLit t of
@@ -149,13 +146,6 @@ lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
       :: prettyType b Atom
       :: prettyType c Atom
       :: prettyAllTerm ts Suffix)
-lessPrettyTerm (App _ (GetChildren _ (x ** a) b) ts) d =
-  group $ align $ hang 2 $ parenthesise (d < App) $
-    concatWith (surround line)
-      (  pretty "getChildren"
-      :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
-      :: prettyType b Atom
-      :: prettyAllTerm ts Suffix)
 lessPrettyTerm (App _ f ts) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
@@ -205,220 +195,3 @@ lessPrettyTerm (Map _ (x ** a) b c) d =
       , prettyType b Atom
       , prettyType c Atom
       ]
-lessPrettyTerm (GetChildren _ (x ** a) b) d =
-  group $ align $ hang 2 $ parenthesise (d < App) $
-    concatWith (surround line)
-      [ pretty "getChildren"
-      , group (align $ hang 2 $ parens $  "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
-      , prettyType b Atom
-      ]
-
--- Typing Errors ---------------------------------------------------------------
-
-Pretty (ChecksOnly t) where
-  pretty Abs = "abstraction"
-  pretty Inj = "injection"
-  pretty Case = "case split"
-  pretty Roll = "rolling"
-  pretty Fold = "fold"
-
-prettyNotSynths :
-  {tyCtx, tmCtx : SnocList String} ->
-  {e : Term m tyCtx tmCtx} ->
-  {tyEnv : _} -> {tmEnv : _} ->
-  NotSynths tyEnv tmEnv e ->
-  List (m, Doc ann)
-export
-prettyNotChecks :
-  {tyCtx, tmCtx : SnocList String} ->
-  {a : Ty [<]} ->
-  {t : Term m tyCtx tmCtx} ->
-  {tyEnv : _} -> {tmEnv : _} ->
-  NotChecks tyEnv tmEnv a t ->
-  List (m, Doc ann)
-prettyNotCheckSpine :
-  {tyCtx, tmCtx : SnocList String} ->
-  {a : Ty [<]} ->
-  {ts : List (Term m tyCtx tmCtx)} ->
-  {tyEnv : _} -> {tmEnv : _} ->
-  NotCheckSpine tyEnv tmEnv a ts ->
-  List (m, Doc ann)
-prettyAnyNotSynths :
-  {tyCtx, tmCtx : SnocList String} ->
-  {es : Context (Term m tyCtx tmCtx)} ->
-  {tyEnv : _} -> {tmEnv : _} ->
-  AnyNotSynths tyEnv tmEnv es ->
-  List (m, Doc ann)
-prettyAnyNotChecks :
-  {tyCtx, tmCtx : SnocList String} ->
-  {ts : Context (Term m tyCtx tmCtx)} ->
-  {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
-  (meta : m) ->
-  AnyNotChecks tyEnv tmEnv as ts ->
-  List (m, Doc ann)
-prettyAnyNotBranches :
-  {tyCtx, tmCtx : SnocList String} ->
-  {ts : Context (x ** Term m tyCtx (tmCtx :< x))} ->
-  {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
-  (meta : m) ->
-  AnyNotBranches tyEnv tmEnv as a ts ->
-  List (m, Doc ann)
-
-prettyNotSynths (ChecksNS shape) =
-  [(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
-prettyNotSynths (AnnotNS {a} (This contra)) =
-  [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
-prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
-  (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
-  prettyNotChecks contra2
-prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
-prettyNotSynths (LetNS2 prf contra) =
-  case synthsRecompute prf of
-    Val a => prettyNotSynths contra
-prettyNotSynths (LetTyNS {a} (This contra)) =
-  [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
-prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
-  (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
-  :: prettyNotSynths contra2
-prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
-prettyNotSynths (AppNS2 prf contras) =
-  case synthsRecompute prf of
-    Val a => prettyNotCheckSpine contras
-prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
-prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
-prettyNotSynths (PrjNS2 prf f) =
-  case synthsRecompute prf of
-    Val a =>
-      [(e.meta
-      , pretty "cannot project non-product type" <+> line <+>
-        prettyType a Open
-      )]
-prettyNotSynths (PrjNS3 {l, as} prf contra) =
-  case synthsRecompute prf of
-    Val (TProd as) =>
-      [(e.meta
-      , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
-        pretty "in product type" <+> line <+>
-        prettyType (TProd as) Open
-      )]
-prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
-prettyNotSynths (UnrollNS2 prf contra) =
-  case synthsRecompute prf of
-    Val a =>
-      [(e.meta
-      , pretty "cannot unroll non-inductive type" <+> line <+>
-        prettyType a Open
-      )]
-prettyNotSynths (MapNS {a} {b} {c} contras) =
-  bifoldMap
-    (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
-    (bifoldMap
-      (const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
-      (const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
-    contras
-prettyNotSynths (GetChildrenNS {a} {b}  contras) =
-  bifoldMap
-    (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
-    (const [(e.meta, pretty "ill-formed contents" <+> line <+> prettyType b Open)])
-    contras
-
-prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
-prettyNotChecks (EmbedNC2 _ prf contra) =
-  case synthsRecompute prf of
-    Val b =>
-      [(t.meta
-      , pretty "cannot unify" <+> line <+>
-        prettyType a Open <+> line <+>
-        pretty "and" <+> line <+>
-        prettyType b Open
-      )]
-prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
-prettyNotChecks (LetNC2 prf contra) =
-  case synthsRecompute prf of
-    Val _ => prettyNotChecks contra
-prettyNotChecks (LetTyNC {a} (This contra)) =
-  [(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
-prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
-prettyNotChecks (LetTyNC (Both contra1 contra2)) =
-  (t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
-  prettyNotChecks contra2
-prettyNotChecks (AbsNC1 contra) =
-  [(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (AbsNC2 prf contra) =
-  case isFunctionRecompute prf of
-    (Val _, Val _) => prettyNotChecks contra
-prettyNotChecks (TupNC1 contra) =
-  [(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
-prettyNotChecks (InjNC1 contra) =
-  [(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (InjNC2 {l} contra) =
-  [(t.meta
-  , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
-    pretty "in sum type" <+> line <+>
-    prettyType a Open
-  )]
-prettyNotChecks (InjNC3 i contra) =
-  case [| (nameOf i).value |] of
-    Val _ => prettyNotChecks contra
-prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
-prettyNotChecks (CaseNC2 prf contra) =
-  case synthsRecompute prf of
-    Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
-prettyNotChecks (CaseNC3 prf contras) =
-  case synthsRecompute prf of
-    Val _ => prettyAnyNotBranches t.meta contras
-prettyNotChecks (RollNC1 contra) =
-  [(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
-prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
-prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
-prettyNotChecks (FoldNC2 prf contra) =
-  case synthsRecompute prf of
-    Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
-prettyNotChecks (FoldNC3 prf contra) =
-  case synthsRecompute prf of
-    Val _ => prettyNotChecks contra
-
-prettyNotCheckSpine (Step1 {t} contra) =
-  [(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
-prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
-prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
-prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
-  prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
-
-prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
-prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
-prettyAnyNotSynths (Step (Both contra1 contra2)) =
-  prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
-
-prettyAnyNotChecks meta Base1 =
-  [(meta
-  , pretty "missing components" <+> line <+>
-    concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
-  )]
-prettyAnyNotChecks meta (Step1 {t, l} contra) =
-  [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
-prettyAnyNotChecks meta (Step2 i (This contra)) =
-  case [| (nameOf i).value |] of
-    Val _ => prettyNotChecks contra
-prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
-prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
-  case [| (nameOf i).value |] of
-    Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
-
-prettyAnyNotBranches meta Base1 =
-  [(meta
-  , pretty "missing cases" <+> line <+>
-    concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
-  )]
-prettyAnyNotBranches meta (Step1 {t, l} contra) =
-  [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
-prettyAnyNotBranches meta (Step2 i (This contra)) =
-  case [| (nameOf i).value |] of
-    Val _ => prettyNotChecks contra
-prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
-prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
-  case [| (nameOf i).value |] of
-    Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2