symantic/Language/Symantic/Typing/Show.hs

   1 {-# LANGUAGE PolyKinds #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 module Language.Symantic.Typing.Show where
   4
   5 import Data.Map.Strict (Map)
   6 import Data.Semigroup ((<>))
   7 import Data.Set (Set)
   8 import Data.Text (Text)
   9 import Data.Typeable
  10 import qualified Data.List as List
  11 import qualified Data.Map.Strict as Map
  12 import qualified Data.Set as Set
  13 import qualified Data.Text as Text
  14
  15 import Language.Symantic.Grammar
  16 import Language.Symantic.Typing.Kind
  17 import Language.Symantic.Typing.Variable
  18 import Language.Symantic.Typing.Type
  19
  20 -- * Type 'Config_showType'
  21 data Config_showType
  22  =   Config_showType
  23  {   config_showType_vars_numbering :: Bool
  24  }
  25
  26 config_showType :: Config_showType
  27 config_showType =
  28         Config_showType
  29          { config_showType_vars_numbering = True }
  30
  31 showType :: Config_showType -> Int -> Type src vs t -> String
  32 showType conf pr ty = showTypeS conf pr ty ""
  33
  34 showTypeS :: forall src vs t. Config_showType -> Int -> Type src vs t -> ShowS
  35 showTypeS conf pr ty =
  36         let (v2n, _) = varNames conf mempty ty in
  37         go v2n (infixB SideL pr, SideL) ty
  38         where
  39         go ::
  40          forall x.
  41          (Map IndexVar Name) -> -- names of variables
  42          (Infix, Side) ->
  43          Type src vs x ->
  44          ShowS
  45         go _v2n _po c
  46          | Just HRefl <- proj_ConstKiTy @Constraint @() c = showString "()"
  47         go _v2n _po (TyConst _src _vs c) = showsPrec 11 c
  48         go v2n _po (TyVar _src _n v) =
  49                 let iv = indexVar v in
  50                 case Map.lookup iv v2n of
  51                  Nothing -> error "[BUG] showsPrec @Type: variable name missing"
  52                  Just n -> showString $ Text.unpack n
  53         go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
  54          | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
  55          , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
  56                 go v2n po b
  57          | Fixity2 op <- fixityOf f =
  58                 showParen (needsParenInfix po op) $
  59                 go v2n (op, SideL) a .
  60                 showString (prettyConst f) .
  61                 go v2n (op, SideR) b
  62                 where
  63                 prettyConst :: forall k c. Const src (c::k) -> String
  64                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = " => "
  65                 prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = ", "
  66                 prettyConst c@Const{}
  67                  | r <- typeRepTyCon (typeRep c)
  68                  , tyConName   r =="#~"
  69                  , tyConModule r =="Language.Symantic.Typing.Type"
  70                  -- XXX: module name must be in sync with where (#~) is defined.
  71                  -- NOTE: cannot use 'proj_ConstKi' here
  72                  -- because (#~) has a polymorphic kind.
  73                  = " ~ "
  74                  | otherwise = ' ' : unParen (show c) ++ " "
  75                 unParen ('(':s) | ')':s' <- reverse s = reverse s'
  76                 unParen s = s
  77         go v2n po (TyApp _src f a) =
  78                 let op = infixR 11 in
  79                 showParen (needsParenInfix po op) $
  80                 go v2n (op, SideL) f .
  81                 showChar ' ' .
  82                 go v2n (op, SideR) a
  83         go v2n po (TyFam _src _len fam args) =
  84                 let op = infixL 11 in
  85                 showParen (needsParenInfix po op) $
  86                 showsPrec 11 fam .
  87                 foldlTys (\t acc ->
  88                         showChar ' ' . go v2n (op, SideL) t . acc
  89                  ) args id
  90
  91         -- | Return a 'Map' associating a distinct 'Name'
  92         -- for all the variables of the given 'Type'.
  93         varNames ::
  94          forall x.
  95          Config_showType ->
  96          (Map IndexVar Name, Names) ->
  97          Type src vs x ->
  98          (Map IndexVar Name, Names)
  99         varNames _cfg st TyConst{} = st
 100         varNames cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
 101                 let iv = indexVar v in
 102                 case Map.lookup iv v2n of
 103                  Just{} -> st
 104                  Nothing ->
 105                         let n' = if config_showType_vars_numbering cfg
 106                                 then n <> Text.pack (show iv)
 107                                 else freshifyName ns n in
 108                         let v2n' = Map.insert iv n' v2n in
 109                         let ns'  = Set.insert n' ns in
 110                         (v2n', ns')
 111         varNames cfg st (TyApp _src f a) = varNames cfg (varNames cfg st f) a
 112         varNames cfg st (TyFam _src _len _fam as) = foldlTys (flip $ varNames cfg) as st
 113
 114 instance Source src => Show (Type src vs t) where
 115         showsPrec = showTypeS config_showType
 116 instance Source src => Show (TypeK src vs kt) where
 117         showsPrec p (TypeK t) = showsPrec p t
 118 instance Source src => Show (TypeVT src) where
 119         showsPrec p (TypeVT t) = showsPrec p t
 120 instance Source src => Show (TypeT src vs) where
 121         showsPrec p (TypeT t) = showsPrec p t
 122 instance Source src => Show (Types src vs ts) where
 123         showsPrec _p tys = showString "[" . go tys . showString "]"
 124                 where
 125                 go :: forall xs. Types src vs xs -> ShowS
 126                 go TypesZ = showString ""
 127                 go (TypesS t0 (TypesS t1 ts)) = showsPrec 10 t0 . showString ", " . showsPrec 10 t1 . go ts
 128                 go (TypesS t ts) = showsPrec 10 t . go ts
 129
 130 showBracket :: Bool -> ShowS -> ShowS
 131 showBracket b p =  if b then showChar '{' . p . showChar '}' else p
 132
 133 -- ** Type 'Name'
 134 type Name     = Text
 135 type NameHint = Name
 136 type Names    = Set Name
 137
 138 -- | Return given 'Name' renamed a bit to avoid
 139 -- conflicting with any given 'Names'.
 140 freshifyName :: Names -> Name -> Name
 141 freshifyName ns "" = freshName ns
 142 freshifyName ns n =
 143         let ints = [1..] :: [Int] in
 144         List.head
 145          [ fresh
 146          | suffix <- "" : (show <$> ints)
 147          , fresh <- [n <> Text.pack suffix]
 148          , fresh `Set.notMember` ns
 149          ]
 150
 151 freshName :: Names -> Name
 152 freshName ns = List.head $ poolNames List.\\ Set.toList ns
 153
 154 -- | Infinite list of unique 'Name's:
 155 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 156 poolNames :: [Name]
 157 poolNames =
 158         [ Text.singleton n     | n <- ['a'..'z'] ] <>
 159         [ Text.pack (n:show i) | n <- ['a'..'z']
 160                                , i <- [1 :: Int ..] ]