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 -}