summaryrefslogtreecommitdiff
path: root/src/Inky/Term/Pretty/Error.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Term/Pretty/Error.idr')
-rw-r--r--src/Inky/Term/Pretty/Error.idr218
1 files changed, 218 insertions, 0 deletions
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
new file mode 100644
index 0000000..bb19b2f
--- /dev/null
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -0,0 +1,218 @@
+module Inky.Term.Pretty.Error
+
+import Data.List.Quantifiers
+import Data.Singleton
+import Data.String
+import Data.These
+
+import Inky.Decidable.Maybe
+import Inky.Term
+import Inky.Term.Checks
+import Inky.Type.Pretty
+
+import Text.PrettyPrint.Prettyprinter
+
+-- 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 mode m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotSynths tyEnv tmEnv e ->
+ List (m, Doc ann)
+export
+prettyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {t : Term mode m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotChecks tyEnv tmEnv a t ->
+ List (m, Doc ann)
+prettyNotCheckSpine :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {ts : List (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotCheckSpine tyEnv tmEnv a ts ->
+ List (m, Doc ann)
+prettyAnyNotSynths :
+ {tyCtx, tmCtx : SnocList String} ->
+ {es : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ AnyNotSynths tyEnv tmEnv es ->
+ List (m, Doc ann)
+prettyAnyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {ts : Context (Term mode 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 mode 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
+
+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 18:25:02 +0000