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