1 {-# LANGUAGE PolyKinds #-}
2 {-# LANGUAGE TypeInType #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 module Language.Symantic.Typing.Document where
6 import Data.Function (id)
7 import Data.Map.Strict (Map)
8 import Data.Maybe (fromMaybe)
9 import Data.Monoid (Monoid(..))
10 import Data.Semigroup (Semigroup(..))
12 import Data.Text (Text)
14 import Symantic.Document (DocFrom(..))
15 import qualified Data.List as L
16 import qualified Data.Map.Strict as Map
17 import qualified Data.Set as Set
18 import qualified Data.Text as T
19 import qualified Symantic.Document as Doc
21 import Language.Symantic.Grammar
22 import Language.Symantic.Typing.Kind
23 import Language.Symantic.Typing.Variable
24 import Language.Symantic.Typing.Module
25 import Language.Symantic.Typing.Type
27 -- * Type 'Config_Doc_Type'
30 { config_Doc_Type_vars_numbering :: Bool
31 -- ^ Style of /type variables/:
33 -- * if 'True': use name and position (as in @a0@ then @a1@)
34 -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
36 -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
37 , config_Doc_Type_imports :: Imports NameTy
40 config_Doc_Type :: Config_Doc_Type
43 { config_Doc_Type_vars_numbering = True
44 , config_Doc_Type_imports = mempty
51 DocFrom (Doc.Word Char) d =>
52 DocFrom (Doc.Word Text) d =>
58 docType conf@Config_Doc_Type{config_Doc_Type_imports=imps} pr ty =
59 let (v2n, _) = var2Name conf mempty ty in
60 go v2n (infixB SideL pr, SideL) ty
64 Map IndexVar Name -> -- names of variables
68 go v2n _po (TyVar _src _n v) =
69 let iv = indexVar v in
70 case Map.lookup iv v2n of
71 Nothing -> error "[BUG] docType: variable name missing"
72 Just n -> docFrom (Doc.Word n)
74 go _v2n _po (TyConst _src _vs c@Const{}) =
75 (if isNameTyOp c then docParen else id) $
78 go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
79 | Just HRefl <- proj_ConstKi @(K []) @[] f =
80 Doc.between (docFrom (Doc.Word '[')) (docFrom (Doc.Word ']')) $
81 go v2n (infixB SideL 0, SideL) a
83 go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
85 | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
86 , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
88 | Just (Fixity2 op) <- fixityOf f =
89 (if isPairNeeded po op then docParen else id) $
90 go v2n (op, SideL) a <>
95 d_op = Doc.yellower . docFrom . Doc.Word
96 prettyConst :: forall k c. Const src (c::k) -> d
97 prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = Doc.space <> d_op "=>" <> Doc.space
98 prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = d_op "," <> Doc.space
99 prettyConst c | Just HRefl <- proj_ConstKi @(K (,)) @(,) c = d_op "," <> Doc.space
100 prettyConst c@Const{}
101 | r <- typeRepTyCon (typeRep c)
103 , tyConModule r =="Language.Symantic.Typing.Type"
104 -- XXX: module name must be in sync with where (#~) is defined.
105 -- NOTE: cannot use 'proj_ConstKi' here
106 -- because (#~) has a polymorphic kind.
107 = Doc.space <> d_op "~" <> Doc.space
108 | otherwise = Doc.space <> d_op (docConst imps c) <> Doc.space
110 go v2n po (TyApp _src f a) =
111 let op = infixL 11 in
112 (if isPairNeeded po op then docParen else id) $
113 go v2n (op, SideL) f <>
117 go v2n po (TyFam _src _len fam args) =
118 let op = infixL 11 in
119 (if isPairNeeded po op then docParen else id) $
122 Doc.space <> go v2n (op, SideL) t <> acc
125 -- | Return a 'Map' associating a distinct 'Name'
126 -- for all the variables of the given 'Type'.
129 (Map IndexVar Name, Names) ->
131 (Map IndexVar Name, Names)
132 var2Name _cfg st TyConst{} = st
133 var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
134 let iv = indexVar v in
135 case Map.lookup iv v2n of
139 if config_Doc_Type_vars_numbering cfg && not (T.null n)
140 then n <> T.pack (show iv)
141 else freshifyName ns n in
142 let v2n' = Map.insert iv n' v2n in
143 let ns' = Set.insert n' ns in
145 var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
146 var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
149 type Names = Set Name
151 -- | Return given 'Name' renamed a bit to avoid
152 -- conflicting with any given 'Names'.
153 freshifyName :: Names -> Name -> Name
154 freshifyName ns "" = freshName ns
156 let ints = [1..] :: [Int] in
159 | suffix <- "" : (show <$> ints)
160 , fresh <- [n <> T.pack suffix]
161 , fresh `Set.notMember` ns
164 freshName :: Names -> Name
165 freshName ns = L.head $ poolNames L.\\ Set.toList ns
167 -- | Infinite list of unique 'Name's:
168 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
171 [ T.singleton n | n <- ['a'..'z'] ] <>
172 [ T.pack (n:show i) | n <- ['a'..'z']
173 , i <- [1 :: Int ..] ]
175 -- * Document 'Types'
179 DocFrom (Doc.Word Char) d =>
180 DocFrom (Doc.Word Text) d =>
186 d_op (docFrom (Doc.Word '[')) <> go tys <> d_op (docFrom (Doc.Word ']'))
189 go :: forall xs. Types src vs xs -> d
191 go (TypesS t0 (TypesS t1 ts)) =
192 docType conf 10 t0 <>
193 d_op (docFrom (Doc.Word ',')) <> Doc.space <>
194 docType conf 10 t1 <>
196 go (TypesS t ts) = docType conf 10 t <> go ts
198 -- * Document 'Const'
201 DocFrom (Doc.Word Char) d =>
202 DocFrom (Doc.Word Text) d =>
203 Imports NameTy -> Const src c -> d
204 docConst imps c@Const{} =
207 revlookupImports f (m `Mod` n) imps
209 f = fixyOfFixity $ Fixity2 infixN5 `fromMaybe` fixityOf c
210 mn@(m `Mod` n) = nameTyOf c
212 -- * Document 'NameTy'
213 docNameTy :: DocFrom (Doc.Word Text) d => NameTy -> d
214 docNameTy (NameTy t) = docFrom (Doc.Word t)
219 DocFrom (Doc.Word Char) d =>
220 DocFrom (Doc.Word Text) d =>
221 (a -> d) -> Mod a -> d
222 docMod a2d ([] `Mod` a) = a2d a
223 docMod a2d (m `Mod` a) = docPathMod m <> (docFrom (Doc.Word '.')) <> a2d a
225 -- * Document 'PathMod'
228 DocFrom (Doc.Word Char) d =>
229 DocFrom (Doc.Word Text) d =>
231 docPathMod (p::PathMod) =
233 L.intersperse (docFrom (Doc.Word '.')) $
234 (\(NameMod n) -> docFrom (Doc.Word n)) <$> p
236 docParen :: Doc.Spaceable d => DocFrom (Doc.Word Char) d => d -> d
237 docParen = Doc.between (docFrom (Doc.Word '(')) (docFrom (Doc.Word ')'))
244 Doc.Decorationable d =>
246 Sym.Modules src ss -> d
247 docModules (Sym.Modules mods) =
249 (\p m doc -> docModule p m <> doc)
258 Doc.Decorationable d =>
260 Sym.PathMod -> Sym.Module src ss -> d
261 docModule m Sym.Module
266 go docFixityInfix module_infix <>
267 go docFixityPrefix module_prefix <>
268 go docFixityPostfix module_postfix
270 go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
278 docFixy token_fixity <>
279 Doc.space <> Doc.bold (Doc.yellower "::") <> Doc.space <>
280 docTokenTerm (t Sym.noSource) <>
290 Sym.Token_Term src ss -> d
292 let n2t = name2typeInj @ss in
293 case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of
294 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
295 Right (Sym.TermVT te) ->
296 Sym.docType Sym.config_doc_type
297 { config_Doc_Type_vars_numbering = False
298 } 0 $ Sym.typeOfTerm te
300 docFixityInfix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Infix -> t
301 docFixityInfix = \case
302 Sym.Infix Nothing 5 -> mempty
307 Sym.AssocB Sym.SideL -> "l"
308 Sym.AssocB Sym.SideR -> "r" in
309 Doc.magenta $ " infix" <> maybe mempty docAssoc a <>
310 Doc.space <> Doc.bold (Doc.bluer (Doc.int p))
311 docFixityPrefix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Unifix -> t
312 docFixityPrefix p = Doc.magenta $ " prefix " <> Doc.bold (Doc.bluer (Doc.int $ Sym.unifix_prece p))
313 docFixityPostfix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Unifix -> t
314 docFixityPostfix p = Doc.magenta $ " postfix " <> Doc.bold (Doc.bluer (Doc.int $ Sym.unifix_prece p))
319 Sym.PathMod -> Sym.NameTe -> d
320 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
322 L.intersperse (Doc.charH '.') $
323 ((\(Sym.NameMod m) -> Doc.textH m) <$> ms) <>
324 [(if isOp n then id else Doc.yellower) $ Doc.text n]
326 isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c