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 qualified Data.List as List
   9 import qualified Data.Map.Strict as Map
  10 import qualified Data.Set as Set
  11 import qualified Data.Text as Text
  12
  13 import Language.Symantic.Grammar
  14 import Language.Symantic.Typing.Constant
  15 import Language.Symantic.Typing.Type
  16 import Language.Symantic.Typing.Quantification
  17
  18 showTy :: forall src ctx ss cs h.
  19  Show_TyConst cs
  20  => Fixity_TyConst cs
  21  => Int -> Type src ctx ss cs h -> ShowS
  22 showTy pr typ =
  23         go Nothing
  24          (infixB L pr, L)
  25          (freeTyVar typ)
  26          (Map.empty, namesTy typ) typ
  27         where
  28         go :: forall p x.
  29             Maybe (Type src ctx ss cs p) -- parent Type, used to prettify
  30          -> (Infix, LR)    -- fixity and associativity
  31          -> Var            -- variable counter (DeBruijn)
  32          -> ( Map Var Name -- names of bound variables
  33             , Names        -- used names : bound variables', free variables' and constants'
  34             )
  35          -> Type src ctx ss cs x
  36          -> ShowS
  37         go _prev _po _v _vs (TyConst _src c) = showsPrec 11 c
  38         go _prev po v vs t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
  39          | FixityInfix op <- fixity_TyConst f =
  40                 showParen (parenInfix po op) $
  41                 go (Just t) (op, L) v vs a .
  42                 showChar ' ' .
  43                 showString (unParen $ show_TyConst f) .
  44                 showChar ' ' .
  45                 go (Just t) (op, R) v vs b
  46                 where
  47                 unParen ('(':s) | ')':s' <- reverse s = reverse s'
  48                 unParen s = s
  49         go _prev po v vs t@(TyApp _src f a) =
  50                 let op = infixR 11 in
  51                 showParen (parenInfix po op) $
  52                 go (Just t) (op, L) v vs f .
  53                 showChar ' ' .
  54                 go (Just t) (op, R) v vs a
  55         go prev po v (vs, ns) t@(TyQuant src nv kv f) =
  56                 let op  = infixR 0 in
  57                 let var = TyVar src kv v in
  58                 let n   = freshifyName ns nv in
  59                 let vs' = Map.insert v n vs in
  60                 let ns' = Set.insert n ns in
  61                 case f var of
  62                  KT x ->
  63                         showParen (parenInfix po op) $
  64                         (case prev of
  65                          Just TyQuant{} -> id
  66                          _ -> showString "forall") .
  67                         showChar ' ' .
  68                         go Nothing po v (vs', ns') var .
  69                         (case x of
  70                          TyQuant{} -> id
  71                          _ -> showString ". ") .
  72                         go (Just t) (op, R) (v + 1) (vs', ns') x
  73         go _prev _po _v (vs, _ns) (TyVar _src _kv v) =
  74                 case Map.lookup v vs of
  75                  Nothing -> showChar '#' . showsPrec 0 v
  76                  Just n  -> showString $ Text.unpack n
  77         go _prev po v vs t@(Term x _te) =
  78                 showBracket True $
  79                 go (Just t) po v vs x
  80         go _prev po v vs (TyFam _src fam args) =
  81                 let op = infixL 11 in
  82                 showParen (parenInfix po op) $
  83                 showsPrec 11 fam .
  84                 foldlTys (\h acc ->
  85                         showChar ' ' . go Nothing (op, L) v vs h . acc
  86                  ) args id
  87
  88 instance -- T
  89  ( Show_TyConst cs
  90  , Fixity_TyConst cs
  91  ) => Show (T src ctx ss cs h) where
  92         showsPrec = showTy
  93 instance -- EType
  94  ( Show_TyConst cs
  95  , Fixity_TyConst cs
  96  ) => Show (EType src ctx ss cs) where
  97         showsPrec p (EType t) = showsPrec p t
  98 instance -- KT
  99  ( Show_TyConst cs
 100  , Fixity_TyConst cs
 101  ) => Show (KT src ctx ss cs ki) where
 102         showsPrec p (KT t) = showTy p t
 103
 104 showTys
 105  :: forall src ctx ss cs hs.
 106     Show_TyConst cs
 107  => Fixity_TyConst cs
 108  => Types src ctx ss cs hs -> ShowS
 109 showTys ts = showString "[" . go ts . showString "]"
 110         where
 111         go :: forall xs. Types src ctx ss cs xs -> ShowS
 112         go TypesZ = showString ""
 113         go (TypesS h0 (TypesS h1 hs)) = showTy 10 h0 . showString ", " . showTy 10 h1 . go hs
 114         go (TypesS h hs) = showTy 10 h . go hs
 115
 116 instance
 117  ( Show_TyConst cs
 118  , Fixity_TyConst cs
 119  ) => Show (Types src ctx ss cs hs) where
 120         showsPrec _p = showTys
 121
 122 showBracket :: Bool -> ShowS -> ShowS
 123 showBracket b p =  if b then showChar '{' . p . showChar '}' else p
 124
 125 -- * Type 'Names'
 126 type Names = Set Name
 127
 128 namesTy :: Show_TyConst cs => Type src ctx ss cs h -> Names
 129 namesTy (TyConst _src c)      = Set.singleton $ Text.pack $ show_TyConst c
 130 namesTy (TyApp   _src f x)    = namesTy f `Set.union` namesTy x
 131 namesTy (TyQuant src _n kv f) = namesTy `ofKT` f (TyVar src kv (-1))
 132 namesTy (TyVar   _src _kv v)  | v < 0     = Set.empty
 133                               | otherwise = Set.singleton $ "#" <> Text.pack (show v)
 134 namesTy (Term x _te) = namesTy x
 135 namesTy (TyFam _src _f as) = foldrTys (\h acc -> Set.union (namesTy h) acc) as Set.empty
 136
 137 -- | Infinite list of unique 'Name's:
 138 -- @a, b, .., z, a1, b1 .., z1, a2, ..@
 139 poolNames :: [Name]
 140 poolNames =
 141         [ Text.singleton n     | n <- ['a'..'z'] ] <>
 142         [ Text.pack (n:show i) | n <- ['a'..'z']
 143                                , i <- [1 :: Int ..] ]
 144
 145 -- | Return given 'Name' renamed a bit to avoid
 146 -- conflicting with any given 'Names'.
 147 freshifyName :: Names -> Name -> Name
 148 freshifyName ns "" = freshName ns
 149 freshifyName ns n =
 150         let ints = [1..] :: [Int] in
 151         List.head
 152          [ fresh
 153          | suffix <- "" : (show <$> ints)
 154          , fresh <- [n <> Text.pack suffix]
 155          , fresh `Set.notMember` ns
 156          ]
 157
 158 freshName :: Names -> Name
 159 freshName ns = List.head $ poolNames List.\\ Set.toList ns