blob: 7cd185c8694a030d7a8d5c948bcb5d72a4d3ca13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
module Inky.Type.Pretty
import Data.Singleton
import Flap.Decidable
import Inky.Type
import Text.PrettyPrint.Prettyprinter
public export
data InkyPrec = Atom | Prefix | Suffix | App | Annot | Open
%name InkyPrec d
export
Eq InkyPrec where
Atom == Atom = True
Prefix == Prefix = True
Suffix == Suffix = True
App == App = True
Annot == Annot = True
Open == Open = True
_ == _ = False
export
Ord InkyPrec 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
prettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
lessPrettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> InkyPrec -> SnocList (Doc ann)
prettyType a d =
if does (alpha {ctx2 = [<]} a TNat)
then pretty "Nat"
else case isList a of
Just b =>
group $ align $ hang 2 $ parenthesise (d < App) $
pretty "List" <+> line <+>
prettyType (assert_smaller a b) Atom
Nothing => lessPrettyType a d
lessPrettyType (TVar i) d = pretty (unVal $ nameOf i)
lessPrettyType (TArrow a b) d =
group $ align $ parenthesise (d < Open) $
let parts = stripArrow b in
concatWith (surround $ neutral <++> "->" <+> line) (prettyType a App :: parts)
where
stripArrow : Ty ctx -> List (Doc ann)
stripArrow (TArrow a b) = prettyType a App :: stripArrow b
stripArrow a = [prettyType a App]
lessPrettyType (TProd (MkRow as _)) d =
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 =
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 =
group $ align $ hang 2 $ parenthesise (d < App) $
pretty "data" <++> pretty x <+> line <+> prettyType a Atom
lessPrettyTypeCtx [<] d = [<]
lessPrettyTypeCtx (as :< (x :- a)) d =
lessPrettyTypeCtx as d :<
(group $ align $ pretty x <+> ":" <+> line <+> prettyType a d)
|
