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