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 _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
  65          | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
  66          , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
  67                 go v2n po b
  68          | Just (Fixity2 op) <- fixityOf f =
  69                 (if needsParenInfix po op then D.paren else id) $
  70                 go v2n (op, SideL) a <>
  71                 prettyConst f <>
  72                 go v2n (op, SideR) b
  73                 where
  74                 d_op = D.yellower
  75                 unParen ('(':s) | ')':s' <- reverse s = reverse s'
  76                 unParen s = s
  77                 prettyConst :: forall k c. Const src (c::k) -> d
  78                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
  79                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> D.space
  80                 prettyConst c | Just HRefl <- proj_ConstKi @(K (,))  @(,)  c = d_op "," <> D.space
  81                 prettyConst c@Const{}
  82                  | r <- typeRepTyCon (typeRep c)
  83                  , tyConName   r =="#~"
  84                  , tyConModule r =="Language.Symantic.Typing.Type"
  85                  -- XXX: module name must be in sync with where (#~) is defined.
  86                  -- NOTE: cannot use 'proj_ConstKi' here
  87                  -- because (#~) has a polymorphic kind.
  88                  = D.space <> d_op "~" <> D.space
  89                  | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space
  90         go v2n po (TyApp _src f a) =
  91                 let op = infixL 11 in
  92                 (if needsParenInfix po op then D.paren else id) $
  93                 go v2n (op, SideL) f <>
  94                 D.space <>
  95                 go v2n (op, SideR) a
  96         go v2n po (TyFam _src _len fam args) =
  97                 let op = infixL 11 in
  98                 (if needsParenInfix po op then D.paren else id) $
  99                 D.stringH (show fam) <>
 100                 foldlTys (\t acc ->
 101                         D.space <> go v2n (op, SideL) t <> acc
 102                  ) args D.empty
 103
 104 docTypes ::
 105  forall src vs ts d.
 106  Semigroup d =>
 107  D.Doc_Text d =>
 108  D.Doc_Color d =>
 109  Config_Doc_Type ->
 110  Types src vs ts -> d
 111 docTypes conf tys =
 112         d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
 113         where
 114         d_op = D.yellower
 115         go :: forall xs. Types src vs xs -> d
 116         go TypesZ = D.empty
 117         go (TypesS t0 (TypesS t1 ts)) =
 118                 docType conf 10 t0 <>
 119                 d_op (D.charH ',') <> D.space <>
 120                 docType conf 10 t1 <>
 121                 go ts
 122         go (TypesS t ts) = docType conf 10 t <> go ts
 123
 124 -- | Return a 'Map' associating a distinct 'Name'
 125 -- for all the variables of the given 'Type'.
 126 var2Name ::
 127  Config_Doc_Type ->
 128  (Map IndexVar Name, Names) ->
 129  Type src vs t ->
 130  (Map IndexVar Name, Names)
 131 var2Name _cfg st TyConst{} = st
 132 var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
 133         let iv = indexVar v in
 134         case Map.lookup iv v2n of
 135          Just{} -> st
 136          Nothing ->
 137                 let n' =
 138                         if config_Doc_Type_vars_numbering cfg && not (T.null n)
 139                         then n <> T.pack (show iv)
 140                         else freshifyName ns n in
 141                 let v2n' = Map.insert iv n' v2n in
 142                 let ns'  = Set.insert n' ns in
 143                 (v2n', ns')
 144 var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
 145 var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
 146
 147 -- ** Type 'Name'
 148 type Name     = Text
 149 type NameHint = Name
 150 type Names    = Set Name
 151
 152 -- | Return given 'Name' renamed a bit to avoid
 153 -- conflicting with any given 'Names'.
 154 freshifyName :: Names -> Name -> Name
 155 freshifyName ns "" = freshName ns
 156 freshifyName ns n =
 157         let ints = [1..] :: [Int] in
 158         L.head
 159          [ fresh
 160          | suffix <- "" : (show <$> ints)
 161          , fresh <- [n <> T.pack suffix]
 162          , fresh `Set.notMember` ns
 163          ]
 164
 165 freshName :: Names -> Name
 166 freshName ns = L.head $ poolNames L.\\ Set.toList ns
 167
 168 -- | Infinite list of unique 'Name's:
 169 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 170 poolNames :: [Name]
 171 poolNames =
 172         [ T.singleton n     | n <- ['a'..'z'] ] <>
 173         [ T.pack (n:show i) | n <- ['a'..'z']
 174                             , i <- [1 :: Int ..] ]