summaryrefslogtreecommitdiff
path: root/src/Inky/Term/Pretty.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Term/Pretty.idr')
-rw-r--r--src/Inky/Term/Pretty.idr260
1 files changed, 237 insertions, 23 deletions
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 91a42b8..79e8f6c 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,11 +1,15 @@
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
+
+import Text.Bounded
import Text.PrettyPrint.Prettyprinter
public export
@@ -43,12 +47,12 @@ Ord TermPrec where
compare Open d2 = GT
export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+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)
prettyLet : Doc ann -> Doc ann -> Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
prettyTerm t d =
case isLit t <|> isCheckLit t of
@@ -65,7 +69,7 @@ prettyTermCtx [<] d = [<]
prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
prettyCases [<] = [<]
-prettyCases (ts :< (l :- (x ** Abs (bound ** t)))) =
+prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) =
prettyCases ts :<
(group $ align $
pretty l <++> pretty x <++> "=>" <++>
@@ -84,26 +88,26 @@ prettyLet binding term =
"in") <+> line <+>
term
-lessPrettyTerm (Annot t a) d =
+lessPrettyTerm (Annot _ t a) d =
group $ align $ hang 2 $ parenthesise (d < Annot) $
prettyTerm t App <++> ":" <+> line <+> prettyType a Open
-lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
-lessPrettyTerm (Let e (x ** t)) d =
+lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+lessPrettyTerm (Let _ e (x ** t)) d =
-- TODO: pretty print annotated abstraction
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyTerm e Open)
(prettyTerm t Open)
-lessPrettyTerm (LetTy a (x ** t)) d =
+lessPrettyTerm (LetTy _ a (x ** t)) d =
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyType a Open)
(prettyTerm t Open)
-lessPrettyTerm (Abs (bound ** t)) d =
+lessPrettyTerm (Abs _ (bound ** t)) d =
group $ hang 2 $ parenthesise (d < Open) $
"\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open
-lessPrettyTerm (App (Map (x ** a) b c) ts) d =
+lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "map"
@@ -111,29 +115,29 @@ 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 =
+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 =
+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 =
+lessPrettyTerm (Tup _ (MkRow ts _)) d =
let parts = prettyTermCtx ts Open <>> [] in
group $ align $ enclose "<" ">" $
flatAlt
(neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
(concatWith (surround $ "," <++> neutral) parts)
-lessPrettyTerm (Prj e l) d =
+lessPrettyTerm (Prj _ e l) d =
group $ align $ hang 2 $ parenthesise (d < Suffix) $
prettyTerm e Suffix <+> line' <+> "." <+> pretty l
-lessPrettyTerm (Inj l t) d =
+lessPrettyTerm (Inj _ l t) d =
group $ align $ hang 2 $ parenthesise (d < App) $
pretty l <+> line <+> prettyTerm t Suffix
-lessPrettyTerm (Case e (MkRow ts _)) 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 <+>
@@ -141,19 +145,19 @@ lessPrettyTerm (Case e (MkRow ts _)) d =
flatAlt
(neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
(concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Roll t) d =
+lessPrettyTerm (Roll _ t) d =
pretty "~" <+>
parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
-lessPrettyTerm (Unroll e) d =
+lessPrettyTerm (Unroll _ e) d =
pretty "!" <+>
parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
-lessPrettyTerm (Fold e (x ** t)) d =
+lessPrettyTerm (Fold _ e (x ** t)) d =
-- TODO: foldcase
group $ align $ hang 2 $ parenthesise (d < Open) $
"fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
(group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
-lessPrettyTerm (Map (x ** a) b c) d =
+lessPrettyTerm (Map _ (x ** a) b c) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "map"
@@ -161,10 +165,220 @@ lessPrettyTerm (Map (x ** a) b c) d =
, prettyType b Atom
, prettyType c Atom
]
-lessPrettyTerm (GetChildren (x ** a) b) d =
+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
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:55:29 +0000