0 | module Idrall.Pretty
  1 |
  2 | import Data.String
  3 |
  4 | import Text.PrettyPrint.Prettyprinter
  5 | import Text.PrettyPrint.Prettyprinter.Util
  6 | import Text.PrettyPrint.Prettyprinter.Doc
  7 |
  8 | import Idrall.Expr
  9 | import Idrall.Path
 10 |
 11 | prettyDottedList : Pretty a => List a -> Doc ann
 12 | prettyDottedList [] = pretty ""
 13 | prettyDottedList (x :: []) = pretty x
 14 | prettyDottedList (x :: xs) = pretty x <+> pretty "." <+> prettyDottedList xs
 15 |
 16 | sbraces : Doc ann -> Doc ann
 17 | sbraces = enclose lbrace (space <+> rbrace)
 18 |
 19 | mutual
 20 |   prettySortedMap : Pretty x => Pretty y
 21 |                   => (Doc ann -> Doc ann)
 22 |                   -> Doc ann
 23 |                   -> (SortedMap x y)
 24 |                   -> Doc ann
 25 |   prettySortedMap wrapping sign e =
 26 |     let ls = SortedMap.toList e
 27 |         lsDoc = map (go sign) ls
 28 |     in
 29 |     wrapping $ foldl (<++>) neutral (punctuate comma lsDoc)
 30 |   where
 31 |     go : Doc ann -> (x, y) -> Doc ann
 32 |     go x (s, e) = pretty s <++> x <++> pretty e
 33 |
 34 |   prettyUnion : Pretty x => Pretty y
 35 |               => (SortedMap x (Maybe y))
 36 |               -> Doc ann
 37 |   prettyUnion e =
 38 |     let ls = SortedMap.toList e
 39 |         lsDoc = map go ls
 40 |     in
 41 |     enclose langle (space <++> rangle) $ foldl (<++>) neutral (punctuate (space <+> pipe) lsDoc)
 42 |   where
 43 |     go : (x, Maybe y) -> Doc ann
 44 |     go (s, Nothing) = pretty s
 45 |     go (s, Just e) = pretty s <++> colon <++> pretty e
 46 |
 47 |   export
 48 |   Pretty U where
 49 |     pretty CType = "Type"
 50 |     pretty Sort = "Sort"
 51 |     pretty Kind = "Kind"
 52 |
 53 |   export
 54 |   Pretty FieldName where
 55 |     pretty (MkFieldName x) = pretty x
 56 |
 57 |   export
 58 |   Pretty FilePath where
 59 |     pretty (MkFilePath path Nothing) = pretty $ prettyPrintPath path
 60 |     pretty (MkFilePath path (Just x)) =
 61 |       (pretty $ prettyPrintPath path) <+> pretty "/" <+> pretty x
 62 |
 63 |   export
 64 |   Pretty ImportStatement where
 65 |     pretty (LocalFile x) = pretty x
 66 |     pretty (EnvVar x) = pretty "env:" <+> pretty x
 67 |     pretty (Http x) = pretty x
 68 |     pretty Missing = pretty "Missing"
 69 |
 70 |   export
 71 |   Pretty a => Pretty (Import a) where
 72 |     pretty (Raw x) = pretty x
 73 |     pretty (Text x) = pretty x <++> pretty "as Text"
 74 |     pretty (Location x) = pretty x <++> pretty "as Location"
 75 |     pretty (Resolved x) = pretty "ERROR: SHOULD NOT BE"
 76 |
 77 |   export
 78 |   Pretty a => Pretty (Chunks a) where
 79 |     pretty (MkChunks [] x) = dquotes $ pretty x
 80 |     pretty (MkChunks (y :: xs) x) = dquotes $ pretty y <+> pretty xs <+> pretty x
 81 |
 82 |
 83 |   export
 84 |   Pretty a => Pretty (Expr a) where
 85 |     pretty (EConst fc x) = pretty x
 86 |     pretty (EVar fc x n) = pretty x <+> pretty "@" <+> pretty n
 87 |     pretty (EApp fc x y) = pretty x <++> parens (pretty y)
 88 |     pretty (ELam fc n x y) =
 89 |       pretty "\\" <+> parens (pretty n <++> colon <++> pretty x)
 90 |         <++> pretty "->" <++> pretty y
 91 |     pretty (EPi fc "_" x y) = pretty x <++> pretty "->" <++> pretty y
 92 |     pretty (EPi fc n x y) =
 93 |       pretty "forall" <+> parens (pretty n <++> colon <++> pretty x)
 94 |         <++> pretty "->" <++> pretty y
 95 |     pretty (ELet fc x t y z) =
 96 |       pretty "let" <++> pretty x <++> equals <++> pretty y
 97 |         <++> pretty "in" <++> pretty z
 98 |     pretty (EAnnot fc x y) = pretty x <++> colon <++> pretty y
 99 |     pretty (EBool fc) = pretty "Bool"
100 |     pretty (EBoolLit fc x) = pretty $ show x
101 |     pretty (EBoolAnd fc x y) = pretty x <++> pretty "&&" <++> pretty y
102 |     pretty (EBoolOr fc x y) = pretty x <++> pretty "||" <++> pretty y
103 |     pretty (EBoolEQ fc x y) = pretty x <++> pretty "==" <++> pretty y
104 |     pretty (EBoolNE fc x y) = pretty x <++> pretty "!=" <++> pretty y
105 |     pretty (EBoolIf fc x y z) =
106 |       pretty "if" <++> pretty x
107 |       <++> pretty "then" <++> pretty y
108 |       <++> pretty "else" <++> pretty z
109 |     pretty (ENatural fc) = pretty "Natural"
110 |     pretty (ENaturalLit fc x) = pretty x
111 |     pretty (ENaturalBuild fc) = pretty "Natural/build"
112 |     pretty (ENaturalFold fc) = pretty "Natural/fold"
113 |     pretty (ENaturalIsZero fc) = pretty "Natural/isZero"
114 |     pretty (ENaturalEven fc) = pretty "Natural/Even"
115 |     pretty (ENaturalOdd fc) = pretty "Natural/Odd"
116 |     pretty (ENaturalSubtract fc) = pretty "Natural/subtract"
117 |     pretty (ENaturalToInteger fc) = pretty "Natural/toInteger"
118 |     pretty (ENaturalShow fc) = pretty "Natural/show"
119 |     pretty (ENaturalPlus fc x y) = pretty x <++> pretty "+" <++> pretty y
120 |     pretty (ENaturalTimes fc x y) = pretty x <++> pretty "*" <++> pretty y
121 |     pretty (EInteger fc) = pretty "Integer"
122 |     pretty (EIntegerLit fc x) = pretty x
123 |     pretty (EIntegerShow fc) = pretty "Integer/show"
124 |     pretty (EIntegerNegate fc) = pretty "Integer/negate"
125 |     pretty (EIntegerClamp fc) = pretty "Integer/clamp"
126 |     pretty (EIntegerToDouble fc) = pretty "Integer/toDouble"
127 |     pretty (EDouble fc) = pretty "Double"
128 |     pretty (EDoubleLit fc x) = pretty $ show x
129 |     pretty (EDoubleShow fc) = pretty "Double/show"
130 |     pretty (EList fc) = pretty "List"
131 |     pretty (EListLit fc t []) =
132 |       pretty (the (List (Expr a)) [])
133 |         <++> colon <++> pretty "List" <++> pretty t
134 |     pretty (EListLit fc t xs) = pretty xs
135 |     pretty (EListAppend fc x y) = pretty x <++> pretty "#" <++> pretty y
136 |     pretty (EListBuild fc) = pretty "List/build"
137 |     pretty (EListFold fc) = pretty "List/fold"
138 |     pretty (EListLength fc) = pretty "List/length"
139 |     pretty (EListHead fc) = pretty "List/head"
140 |     pretty (EListLast fc) = pretty "List/last"
141 |     pretty (EListIndexed fc) = pretty "List/indexed"
142 |     pretty (EListReverse fc) = pretty "List/indexed"
143 |     pretty (EText fc) = pretty "Text"
144 |     pretty (ETextLit fc cs) = pretty cs
145 |     pretty (ETextAppend fc x y) = pretty x <++> pretty "++" <++> pretty y
146 |     pretty (ETextShow fc) = pretty "Text/show"
147 |     pretty (ETextReplace fc) = pretty "Text/replace"
148 |     pretty (EOptional fc) = pretty "Optional"
149 |     pretty (ESome fc x) = pretty "Some" <++> pretty x
150 |     pretty (ENone fc) = pretty "None"
151 |     pretty (EField fc x y) =
152 |       pretty x <+> pretty "." <+> pretty y
153 |     pretty (EWith fc x xs y) =
154 |       pretty x <++> pretty "with" <++>
155 |       prettyDottedList (forget xs) <++> equals <++> pretty y
156 |     pretty (EEquivalent fc x y) = pretty x <++> pretty "===" <++> pretty y
157 |     pretty (EAssert fc x) = pretty "assert" <++> colon <++> pretty x
158 |     pretty (ERecord fc x) = prettySortedMap sbraces colon x
159 |     pretty (ERecordLit fc x) = prettySortedMap sbraces equals x
160 |     pretty (EUnion fc x) = prettyUnion x
161 |     pretty (ECombine fc x y) = pretty x <++> pretty "/\\" <++> pretty y
162 |     pretty (ECombineTypes fc x y) = pretty x <++> pretty "//\\\\" <++> pretty y
163 |     pretty (EPrefer fc x y) = pretty x <++> pretty "//" <++> pretty y
164 |     pretty (ERecordCompletion fc x y) = pretty x <++> pretty "::" <++> pretty y
165 |     pretty (EMerge fc x y Nothing) = pretty "merge" <++> pretty x <++> pretty y
166 |     pretty (EMerge fc x y (Just z)) = pretty "merge" <++> pretty x <++> pretty y <++> pretty ":" <++> pretty z
167 |     pretty (EToMap fc x Nothing) = pretty "toMap" <++> pretty x
168 |     pretty (EProject fc x (Left y)) = pretty x <+> dot <+> braces (pretty y) -- TODO fix
169 |     pretty (EProject fc x (Right y)) = pretty x <+> dot <+> parens (pretty y)
170 |     pretty (EToMap fc x (Just y)) =
171 |       pretty "merge" <++> pretty x
172 |       <++> pretty ":" <++> pretty y
173 |     pretty (EImportAlt fc x y) = pretty x <++> pretty "?" <++> pretty y
174 |     pretty (EEmbed fc x) = pretty x
175 |