]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Document.hs
Add TyApp pattern synonyms (:$) and (:@).
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Document.hs
1 {-# LANGUAGE PolyKinds #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 module Language.Symantic.Typing.Document where
4
5 import Data.Function (id)
6 import Data.Map.Strict (Map)
7 import Data.Maybe (fromMaybe)
8 import Data.Semigroup (Semigroup(..))
9 import Data.Set (Set)
10 import Data.Typeable
11 import qualified Data.List as L
12 import qualified Data.Map.Strict as Map
13 import qualified Data.Set as Set
14 import qualified Data.Text as T
15
16 import qualified Language.Symantic.Document as D
17 import Language.Symantic.Grammar
18 import Language.Symantic.Typing.Kind
19 import Language.Symantic.Typing.Variable
20 import Language.Symantic.Typing.Module
21 import Language.Symantic.Typing.Type
22
23 -- * Type 'Config_Doc_Type'
24 data Config_Doc_Type
25 = Config_Doc_Type
26 { config_Doc_Type_vars_numbering :: Bool
27 -- ^ Style of /type variables/:
28 --
29 -- * if 'True': use name and position (as in @a0@ then @a1@)
30 -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
31 --
32 -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
33 , config_Doc_Type_imports :: Imports NameTy
34 }
35
36 config_Doc_Type :: Config_Doc_Type
37 config_Doc_Type =
38 Config_Doc_Type
39 { config_Doc_Type_vars_numbering = True
40 , config_Doc_Type_imports = mempty
41 }
42
43 -- * Document 'Type'
44 docType ::
45 forall src vs t d.
46 Semigroup d =>
47 D.Doc_Text d =>
48 D.Doc_Color d =>
49 Config_Doc_Type ->
50 Precedence ->
51 Type src vs t -> d
52 docType conf@Config_Doc_Type{config_Doc_Type_imports=imps} pr ty =
53 let (v2n, _) = var2Name conf mempty ty in
54 go v2n (infixB SideL pr, SideL) ty
55 where
56 go ::
57 forall x.
58 (Map IndexVar Name) -> -- names of variables
59 (Infix, Side) ->
60 Type src vs x -> d
61 -- Var
62 go v2n _po (TyVar _src _n v) =
63 let iv = indexVar v in
64 case Map.lookup iv v2n of
65 Nothing -> error "[BUG] docType: variable name missing"
66 Just n -> D.textH n
67 -- Const
68 go _v2n _po (TyConst _src _vs c@Const{}) =
69 (if isNameTyOp c then D.paren else id) $
70 docConst imps c
71 -- [] Const
72 go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
73 | Just HRefl <- proj_ConstKi @(K []) @[] f =
74 "[" <> go v2n (infixB SideL 0, SideL) a <> "]"
75 -- Infix Const
76 go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
77 -- () =>
78 | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
79 , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
80 go v2n po b
81 | Just (Fixity2 op) <- fixityOf f =
82 (if needsParenInfix po op then D.paren else id) $
83 go v2n (op, SideL) a <>
84 prettyConst f <>
85 go v2n (op, SideR) b
86 where
87 d_op = D.yellower
88 prettyConst :: forall k c. Const src (c::k) -> d
89 prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
90 prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = d_op "," <> D.space
91 prettyConst c | Just HRefl <- proj_ConstKi @(K (,)) @(,) c = d_op "," <> D.space
92 prettyConst c@Const{}
93 | r <- typeRepTyCon (typeRep c)
94 , tyConName r =="#~"
95 , tyConModule r =="Language.Symantic.Typing.Type"
96 -- XXX: module name must be in sync with where (#~) is defined.
97 -- NOTE: cannot use 'proj_ConstKi' here
98 -- because (#~) has a polymorphic kind.
99 = D.space <> d_op "~" <> D.space
100 | otherwise = D.space <> d_op (docConst imps c) <> D.space
101 -- TyApp
102 go v2n po (TyApp _src f a) =
103 let op = infixL 11 in
104 (if needsParenInfix po op then D.paren else id) $
105 go v2n (op, SideL) f <>
106 D.space <>
107 go v2n (op, SideR) a
108 -- TyFam
109 go v2n po (TyFam _src _len fam args) =
110 let op = infixL 11 in
111 (if needsParenInfix po op then D.paren else id) $
112 docConst imps fam <>
113 foldlTys (\t acc ->
114 D.space <> go v2n (op, SideL) t <> acc
115 ) args D.empty
116
117 -- | Return a 'Map' associating a distinct 'Name'
118 -- for all the variables of the given 'Type'.
119 var2Name ::
120 Config_Doc_Type ->
121 (Map IndexVar Name, Names) ->
122 Type src vs t ->
123 (Map IndexVar Name, Names)
124 var2Name _cfg st TyConst{} = st
125 var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
126 let iv = indexVar v in
127 case Map.lookup iv v2n of
128 Just{} -> st
129 Nothing ->
130 let n' =
131 if config_Doc_Type_vars_numbering cfg && not (T.null n)
132 then n <> T.pack (show iv)
133 else freshifyName ns n in
134 let v2n' = Map.insert iv n' v2n in
135 let ns' = Set.insert n' ns in
136 (v2n', ns')
137 var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
138 var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
139
140 -- ** Type 'Names'
141 type Names = Set Name
142
143 -- | Return given 'Name' renamed a bit to avoid
144 -- conflicting with any given 'Names'.
145 freshifyName :: Names -> Name -> Name
146 freshifyName ns "" = freshName ns
147 freshifyName ns n =
148 let ints = [1..] :: [Int] in
149 L.head
150 [ fresh
151 | suffix <- "" : (show <$> ints)
152 , fresh <- [n <> T.pack suffix]
153 , fresh `Set.notMember` ns
154 ]
155
156 freshName :: Names -> Name
157 freshName ns = L.head $ poolNames L.\\ Set.toList ns
158
159 -- | Infinite list of unique 'Name's:
160 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
161 poolNames :: [Name]
162 poolNames =
163 [ T.singleton n | n <- ['a'..'z'] ] <>
164 [ T.pack (n:show i) | n <- ['a'..'z']
165 , i <- [1 :: Int ..] ]
166
167 -- * Document 'Types'
168 docTypes ::
169 forall src vs ts d.
170 Semigroup d =>
171 D.Doc_Text d =>
172 D.Doc_Color d =>
173 Config_Doc_Type ->
174 Types src vs ts -> d
175 docTypes conf tys =
176 d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
177 where
178 d_op = D.yellower
179 go :: forall xs. Types src vs xs -> d
180 go TypesZ = D.empty
181 go (TypesS t0 (TypesS t1 ts)) =
182 docType conf 10 t0 <>
183 d_op (D.charH ',') <> D.space <>
184 docType conf 10 t1 <>
185 go ts
186 go (TypesS t ts) = docType conf 10 t <> go ts
187
188 -- * Document 'Const'
189 docConst :: D.Doc_Text d => Imports NameTy -> Const src c -> d
190 docConst imps c@Const{} =
191 docMod docNameTy $
192 maybe mn (`Mod` n) $
193 revlookupImports f (m `Mod` n) imps
194 where
195 f = fixyOfFixity $ Fixity2 infixN5 `fromMaybe` fixityOf c
196 mn@(m `Mod` n) = nameTyOf c
197
198 -- * Document 'NameTy'
199 docNameTy :: D.Doc_Text d => NameTy -> d
200 docNameTy (NameTy t) = D.textH t
201
202 -- * Document 'Mod'
203 docMod :: D.Doc_Text d => (a -> d) -> Mod a -> d
204 docMod a2d ([] `Mod` a) = a2d a
205 docMod a2d (m `Mod` a) = docPathMod m <> (D.charH '.') <> a2d a
206
207 -- * Document 'PathMod'
208 docPathMod :: D.Doc_Text d => PathMod -> d
209 docPathMod (p::PathMod) =
210 D.catH $
211 L.intersperse (D.charH '.') $
212 (\(NameMod n) -> D.textH n) <$> p
213
214
215 {-
216 docModules ::
217 Source src =>
218 D.Doc_Text d =>
219 D.Doc_Color d =>
220 D.Doc_Decoration d =>
221 ReadTe src ss =>
222 Sym.Modules src ss -> d
223 docModules (Sym.Modules mods) =
224 Map.foldrWithKey
225 (\p m doc -> docModule p m <> doc)
226 D.empty
227 mods
228
229 docModule ::
230 forall src ss d.
231 Source src =>
232 D.Doc_Text d =>
233 D.Doc_Color d =>
234 D.Doc_Decoration d =>
235 ReadTe src ss =>
236 Sym.PathMod -> Sym.Module src ss -> d
237 docModule m Sym.Module
238 { Sym.module_infix
239 , Sym.module_prefix
240 , Sym.module_postfix
241 } =
242 go docFixityInfix module_infix <>
243 go docFixityPrefix module_prefix <>
244 go docFixityPostfix module_postfix
245 where
246 go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
247 go docFixy =
248 Map.foldrWithKey
249 (\n Sym.Tokenizer
250 { Sym.token_fixity
251 , Sym.token_term = t
252 } doc ->
253 docPathTe m n <>
254 docFixy token_fixity <>
255 D.space <> D.bold (D.yellower "::") <> D.space <>
256 docTokenTerm (t Sym.noSource) <>
257 D.eol <> doc)
258 D.empty
259
260 docTokenTerm ::
261 forall src ss d.
262 Source src =>
263 D.Doc_Text d =>
264 D.Doc_Color d =>
265 ReadTe src ss =>
266 Sym.Token_Term src ss -> d
267 docTokenTerm t =
268 let n2t = name2typeInj @ss in
269 case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of
270 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
271 Right (Sym.TermVT te) ->
272 Sym.docType Sym.config_doc_type
273 { config_Doc_Type_vars_numbering = False
274 } 0 $ Sym.typeOfTerm te
275
276 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
277 docFixityInfix = \case
278 Sym.Infix Nothing 5 -> D.empty
279 Sym.Infix a p ->
280 let docAssoc = \case
281 Sym.AssocL -> "l"
282 Sym.AssocR -> "r"
283 Sym.AssocB Sym.SideL -> "l"
284 Sym.AssocB Sym.SideR -> "r" in
285 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
286 D.space <> D.bold (D.bluer (D.int p))
287 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
288 docFixityPrefix p = D.magenta $ " prefix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
289 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
290 docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
291
292 docPathTe ::
293 D.Doc_Text d =>
294 D.Doc_Color d =>
295 Sym.PathMod -> Sym.NameTe -> d
296 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
297 D.catH $
298 L.intersperse (D.charH '.') $
299 ((\(Sym.NameMod m) -> D.textH m) <$> ms) <>
300 [(if isOp n then id else D.yellower) $ D.text n]
301 where
302 isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
303 -}