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.Semigroup (Semigroup(..))
   8 import Data.Set (Set)
   9 import Data.Text (Text)
  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.Type
  21
  22 -- * Type 'Config_Doc_Type'
  23 data Config_Doc_Type
  24  =   Config_Doc_Type
  25  {   config_Doc_Type_vars_numbering :: Bool
  26      -- ^ Style of /type variables/:
  27      --
  28      -- * if 'True': use name and position (as in @a0@ then @a1@)
  29      -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
  30      --
  31      -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
  32  }
  33
  34 config_doc_type :: Config_Doc_Type
  35 config_doc_type =
  36         Config_Doc_Type
  37          { config_Doc_Type_vars_numbering = True }
  38
  39 docType ::
  40  forall src vs t d.
  41  Semigroup d =>
  42  D.Doc_Text d =>
  43  D.Doc_Color d =>
  44  Config_Doc_Type ->
  45  Precedence ->
  46  Type src vs t -> d
  47 docType conf pr ty =
  48         let (v2n, _) = var2Name conf mempty ty in
  49         go v2n (infixB SideL pr, SideL) ty
  50         where
  51         go ::
  52          forall x.
  53          (Map IndexVar Name) -> -- names of variables
  54          (Infix, Side) ->
  55          Type src vs x -> d
  56         go _v2n _po c
  57          | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"
  58         go _v2n _po (TyConst _src _vs c) = D.stringH $ show c
  59         go v2n _po (TyVar _src _n v) =
  60                 let iv = indexVar v in
  61                 case Map.lookup iv v2n of
  62                  Nothing -> error "[BUG] docType: variable name missing"
  63                  Just n -> D.textH n
  64         go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
  65          | Just HRefl <- proj_ConstKi @(K []) @[] f =
  66                 "[" <> go v2n (infixB SideL 0, SideL) a <> "]"
  67         go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
  68          | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
  69          , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
  70                 go v2n po b
  71          | Just (Fixity2 op) <- fixityOf f =
  72                 (if needsParenInfix po op then D.paren else id) $
  73                 go v2n (op, SideL) a <>
  74                 prettyConst f <>
  75                 go v2n (op, SideR) b
  76                 where
  77                 d_op = D.yellower
  78                 unParen ('(':s) | ')':s' <- reverse s = reverse s'
  79                 unParen s = s
  80                 prettyConst :: forall k c. Const src (c::k) -> d
  81                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
  82                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> D.space
  83                 prettyConst c | Just HRefl <- proj_ConstKi @(K (,))  @(,)  c = d_op "," <> D.space
  84                 prettyConst c@Const{}
  85                  | r <- typeRepTyCon (typeRep c)
  86                  , tyConName   r =="#~"
  87                  , tyConModule r =="Language.Symantic.Typing.Type"
  88                  -- XXX: module name must be in sync with where (#~) is defined.
  89                  -- NOTE: cannot use 'proj_ConstKi' here
  90                  -- because (#~) has a polymorphic kind.
  91                  = D.space <> d_op "~" <> D.space
  92                  | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space
  93         go v2n po (TyApp _src f a) =
  94                 let op = infixL 11 in
  95                 (if needsParenInfix po op then D.paren else id) $
  96                 go v2n (op, SideL) f <>
  97                 D.space <>
  98                 go v2n (op, SideR) a
  99         go v2n po (TyFam _src _len fam args) =
 100                 let op = infixL 11 in
 101                 (if needsParenInfix po op then D.paren else id) $
 102                 D.stringH (show fam) <>
 103                 foldlTys (\t acc ->
 104                         D.space <> go v2n (op, SideL) t <> acc
 105                  ) args D.empty
 106
 107 docTypes ::
 108  forall src vs ts d.
 109  Semigroup d =>
 110  D.Doc_Text d =>
 111  D.Doc_Color d =>
 112  Config_Doc_Type ->
 113  Types src vs ts -> d
 114 docTypes conf tys =
 115         d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
 116         where
 117         d_op = D.yellower
 118         go :: forall xs. Types src vs xs -> d
 119         go TypesZ = D.empty
 120         go (TypesS t0 (TypesS t1 ts)) =
 121                 docType conf 10 t0 <>
 122                 d_op (D.charH ',') <> D.space <>
 123                 docType conf 10 t1 <>
 124                 go ts
 125         go (TypesS t ts) = docType conf 10 t <> go ts
 126
 127 -- | Return a 'Map' associating a distinct 'Name'
 128 -- for all the variables of the given 'Type'.
 129 var2Name ::
 130  Config_Doc_Type ->
 131  (Map IndexVar Name, Names) ->
 132  Type src vs t ->
 133  (Map IndexVar Name, Names)
 134 var2Name _cfg st TyConst{} = st
 135 var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
 136         let iv = indexVar v in
 137         case Map.lookup iv v2n of
 138          Just{} -> st
 139          Nothing ->
 140                 let n' =
 141                         if config_Doc_Type_vars_numbering cfg && not (T.null n)
 142                         then n <> T.pack (show iv)
 143                         else freshifyName ns n in
 144                 let v2n' = Map.insert iv n' v2n in
 145                 let ns'  = Set.insert n' ns in
 146                 (v2n', ns')
 147 var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
 148 var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
 149
 150 -- ** Type 'Name'
 151 type Name     = Text
 152 type NameHint = Name
 153 type Names    = Set Name
 154
 155 -- | Return given 'Name' renamed a bit to avoid
 156 -- conflicting with any given 'Names'.
 157 freshifyName :: Names -> Name -> Name
 158 freshifyName ns "" = freshName ns
 159 freshifyName ns n =
 160         let ints = [1..] :: [Int] in
 161         L.head
 162          [ fresh
 163          | suffix <- "" : (show <$> ints)
 164          , fresh <- [n <> T.pack suffix]
 165          , fresh `Set.notMember` ns
 166          ]
 167
 168 freshName :: Names -> Name
 169 freshName ns = L.head $ poolNames L.\\ Set.toList ns
 170
 171 -- | Infinite list of unique 'Name's:
 172 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 173 poolNames :: [Name]
 174 poolNames =
 175         [ T.singleton n     | n <- ['a'..'z'] ] <>
 176         [ T.pack (n:show i) | n <- ['a'..'z']
 177                             , i <- [1 :: Int ..] ]