symantic/Language/Symantic/Typing/Document.hs

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