summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Inky/Term/Pretty.idr176
-rw-r--r--src/Inky/Type/Pretty.idr71
2 files changed, 153 insertions, 94 deletions
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index a9055d4..91a42b8 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,32 +1,54 @@
module Inky.Term.Pretty
import Data.Singleton
+import Data.String
import Inky.Decidable.Maybe
import Inky.Term
import Inky.Type.Pretty
import Text.PrettyPrint.Prettyprinter
-appPrec, prjPrec, unrollPrec, annotPrec,
- letPrec, absPrec, injPrec, tupPrec, casePrec, rollPrec, foldPrec : Prec
-appPrec = App
-prjPrec = User 9
-unrollPrec = PrefixMinus
-annotPrec = Equal
-letPrec = Open
-absPrec = Open
-injPrec = App
-tupPrec = Open
-casePrec = Open
-rollPrec = PrefixMinus
-foldPrec = Open
+public export
+data TermPrec = Atom | Prefix | Suffix | App | Annot | Open
+
+%name TermPrec d
+
+Eq TermPrec where
+ Atom == Atom = True
+ Prefix == Prefix = True
+ Suffix == Suffix = True
+ App == App = True
+ Annot == Annot = True
+ Open == Open = True
+ _ == _ = False
+
+Ord TermPrec where
+ compare Atom Atom = EQ
+ compare Atom d2 = LT
+ compare Prefix Atom = GT
+ compare Prefix Prefix = EQ
+ compare Prefix d2 = LT
+ compare Suffix Atom = GT
+ compare Suffix Prefix = GT
+ compare Suffix Suffix = EQ
+ compare Suffix d2 = LT
+ compare App App = EQ
+ compare App Annot = LT
+ compare App Open = LT
+ compare App d2 = GT
+ compare Annot Annot = EQ
+ compare Annot Open = LT
+ compare Annot d2 = GT
+ compare Open Open = EQ
+ compare Open d2 = GT
export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> Prec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> Prec -> SnocList (Doc ann)
+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)
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann
+prettyLet : Doc ann -> Doc ann -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
prettyTerm t d =
case isLit t <|> isCheckLit t of
@@ -43,88 +65,106 @@ 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 :<
+ (group $ align $
+ pretty l <++> pretty x <++> "=>" <++>
+ "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
+ prettyTerm t Open)
prettyCases (ts :< (l :- (x ** t))) =
- prettyCases ts :< (pretty l <++> pretty x <++> "=>" <++> prettyTerm t Open)
+ prettyCases ts :<
+ (group $ align $
+ pretty l <++> pretty x <++> "=>" <+> line <+>
+ prettyTerm t Open)
+prettyLet binding term =
+ (group $
+ pretty "let" <++>
+ (group $ hang (-2) $ binding) <+> line <+>
+ "in") <+> line <+>
+ term
lessPrettyTerm (Annot t a) d =
- parenthesise (d > annotPrec) $ group $ align $ hang 2 $
- prettyTerm t annotPrec <++> ":" <+> line <+> prettyType a annotPrec
+ 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 =
- parenthesise (d > letPrec) $ group $ align $
- (group $ align $ hang 2 $
- pretty x <++> "=" <+> line <+> prettyTerm e letPrec
- ) <+> line <+>
- "in" <+> line <+>
- prettyTerm t letPrec
+ -- 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 =
- parenthesise (d > letPrec) $ group $ align $
- (group $ align $ hang 2 $
- pretty x <++> "=" <+> line <+> prettyType a letPrec
- ) <+> line <+>
- "in" <+> line <+>
- prettyTerm t letPrec
+ group $ align $ parenthesise (d < Open) $
+ prettyLet
+ (pretty x <++> "=" <+> line <+> prettyType a Open)
+ (prettyTerm t Open)
lessPrettyTerm (Abs (bound ** t)) d =
- parenthesise (d > absPrec) $ group $ hang 2 $
+ group $ hang 2 $ parenthesise (d < Open) $
"\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
- prettyTerm t absPrec
+ prettyTerm t Open
lessPrettyTerm (App (Map (x ** a) b c) ts) d =
- parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+ group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "map"
- :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
- :: prettyType b appPrec
- :: prettyType c appPrec
- :: prettyAllTerm ts appPrec)
+ :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+ :: prettyType b Atom
+ :: prettyType c Atom
+ :: prettyAllTerm ts Suffix)
lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
- parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+ 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 appPrec
- :: prettyAllTerm ts appPrec)
+ :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+ :: prettyType b Atom
+ :: prettyAllTerm ts Suffix)
lessPrettyTerm (App f ts) d =
- parenthesise (d >= appPrec) $ group $ align $ hang 2 $
- concatWith (surround line) (prettyTerm f appPrec :: prettyAllTerm ts appPrec)
+ group $ align $ hang 2 $ parenthesise (d < App) $
+ concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
lessPrettyTerm (Tup (MkRow ts _)) d =
- enclose "<" ">" $ group $ align $ hang 2 $
- concatWith (surround $ "<" <+> line) (prettyTermCtx ts tupPrec <>> [])
+ 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 =
- parenthesise (d > prjPrec) $ group $ align $ hang 2 $
- prettyTerm e prjPrec <+> line' <+> "." <+> pretty l
+ group $ align $ hang 2 $ parenthesise (d < Suffix) $
+ prettyTerm e Suffix <+> line' <+> "." <+> pretty l
lessPrettyTerm (Inj l t) d =
- parenthesise (d >= injPrec) $ group $ align $ hang 2 $
- pretty l <+> line <+> prettyTerm t absPrec
+ group $ align $ hang 2 $ parenthesise (d < App) $
+ pretty l <+> line <+> prettyTerm t Suffix
lessPrettyTerm (Case e (MkRow ts _)) d =
- parenthesise (d > casePrec) $ group $ align $ hang 2 $
- "case" <++> prettyTerm e casePrec <++> "of" <+> hardline <+>
- (braces $ group $ align $ hang 2 $
- concatWith (surround $ ";" <+> hardline) $
- prettyCases ts <>> [])
+ let parts = prettyCases ts <>> [] in
+ group $ align $ hang 2 $ parenthesise (d < Open) $
+ (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
+ (braces $
+ flatAlt
+ (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+ (concatWith (surround $ ";" <++> neutral) parts))
lessPrettyTerm (Roll t) d =
pretty "~" <+>
- (parenthesise (d > rollPrec) $ group $ align $ hang 2 $ prettyTerm t rollPrec)
+ parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
lessPrettyTerm (Unroll e) d =
pretty "!" <+>
- (parenthesise (d > unrollPrec) $ group $ align $ hang 2 $ prettyTerm e unrollPrec)
+ parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
lessPrettyTerm (Fold e (x ** t)) d =
- parenthesise (d > foldPrec) $ group $ align $ hang 2 $
- "fold" <++> prettyTerm e foldPrec <++> "by" <+> hardline <+>
- (parens $ group $ align $ hang 2 $
+ -- 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 =
- parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+ group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "map"
- , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open)
- , prettyType b appPrec
- , prettyType c appPrec
+ , group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+ , prettyType b Atom
+ , prettyType c Atom
]
lessPrettyTerm (GetChildren (x ** a) b) d =
- parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+ 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 appPrec
+ , group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
+ , prettyType b Atom
]
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index aaef606..ae80125 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -5,51 +5,70 @@ import Inky.Decidable
import Inky.Type
import Text.PrettyPrint.Prettyprinter
-arrowPrec, prodPrec, sumPrec, fixPrec, listPrec : Prec
-arrowPrec = Open
-prodPrec = Open
-sumPrec = Open
-fixPrec = Open
-listPrec = App
+public export
+data TyPrec = Atom | App | Open
+
+%name TyPrec d
+
+Eq TyPrec where
+ Atom == Atom = True
+ App == App = True
+ Open == Open = True
+ _ == _ = False
+
+Ord TyPrec where
+ compare Atom Atom = EQ
+ compare Atom App = LT
+ compare Atom Open = LT
+ compare App Atom = GT
+ compare App App = EQ
+ compare App Open = LT
+ compare Open Atom = GT
+ compare Open App = GT
+ compare Open Open = EQ
export
-prettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann
-lessPrettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann
-lessPrettyTypeRow : {ctx : SnocList String} -> Context (Ty ctx) -> Prec -> List (Doc ann)
+prettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
+lessPrettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
+lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> TyPrec -> SnocList (Doc ann)
prettyType a d =
if does (alpha {ctx2 = [<]} a TNat)
then pretty "Nat"
else case isList a of
Just b =>
- parenthesise (d >= listPrec) $ group $ align $ hang 2 $
+ group $ align $ hang 2 $ parenthesise (d < App) $
pretty "List" <+> line <+>
- prettyType (assert_smaller a b) d
+ prettyType (assert_smaller a b) Atom
Nothing => lessPrettyType a d
lessPrettyType (TVar i) d = pretty (unVal $ nameOf i)
lessPrettyType (TArrow a b) d =
- parenthesise (d > arrowPrec) $ group $ align $ hang 2 $
+ group $ align $ parenthesise (d < Open) $
let parts = stripArrow b in
- concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts)
+ concatWith (surround $ neutral <++> "->" <+> line) (prettyType a App :: parts)
where
stripArrow : Ty ctx -> List (Doc ann)
- stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b
- stripArrow a = [prettyType a arrowPrec]
+ stripArrow (TArrow a b) = prettyType a App :: stripArrow b
+ stripArrow a = [prettyType a App]
lessPrettyType (TProd (MkRow as _)) d =
- enclose "<" ">" $ group $ align $ hang 2 $
- let parts = lessPrettyTypeRow as prodPrec in
- concatWith (surround $ "," <+> line) parts
+ let parts = lessPrettyTypeCtx as Open <>> [] in
+ group $ align $ enclose "<" ">" $
+ flatAlt
+ (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+ (concatWith (surround $ "," <++> neutral) parts)
lessPrettyType (TSum (MkRow as _)) d =
- enclose "[" "]" $ group $ align $ hang 2 $
- let parts = lessPrettyTypeRow as prodPrec in
- concatWith (surround $ "," <+> line) parts
+ let parts = lessPrettyTypeCtx as Open <>> [] in
+ group $ align $ enclose "[" "]" $
+ flatAlt
+ (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
+ (concatWith (surround $ "," <++> neutral) parts)
lessPrettyType (TFix x a) d =
- parens $ group $ align $ hang 2 $
+ group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+>
- prettyType a fixPrec
+ prettyType a Open
-lessPrettyTypeRow [<] d = []
-lessPrettyTypeRow (as :< (x :- a)) d =
+lessPrettyTypeCtx [<] d = [<]
+lessPrettyTypeCtx (as :< (x :- a)) d =
+ lessPrettyTypeCtx as d :<
(group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d)
- :: lessPrettyTypeRow as d
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:45:53 +0000