, module Language.Symantic.Typing.Variable
, module Language.Symantic.Typing.Type
, module Language.Symantic.Typing.Grammar
+ , module Language.Symantic.Typing.Document
, module Language.Symantic.Typing.Read
, module Language.Symantic.Typing.Show
, module Language.Symantic.Typing.Unify
import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Grammar
+import Language.Symantic.Typing.Document
import Language.Symantic.Typing.Read
import Language.Symantic.Typing.Show
import Language.Symantic.Typing.Unify
--- /dev/null
+{-# LANGUAGE PolyKinds #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Language.Symantic.Typing.Document where
+
+import Data.Function (id)
+import Data.Map.Strict (Map)
+import Data.Semigroup (Semigroup(..))
+import Data.Set (Set)
+import Data.Text (Text)
+import Data.Typeable
+import qualified Data.List as L
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+import qualified Data.Text as T
+
+import qualified Language.Symantic.Document as D
+import Language.Symantic.Grammar
+import Language.Symantic.Typing.Kind
+import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.Type
+
+-- * Type 'Config_Doc_Type'
+data Config_Doc_Type
+ = Config_Doc_Type
+ { config_Doc_Type_vars_numbering :: Bool
+ -- ^ Style of /type variables/:
+ --
+ -- * if 'True': use name and position (as in @a0@ then @a1@)
+ -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
+ --
+ -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
+ }
+
+config_doc_type :: Config_Doc_Type
+config_doc_type =
+ Config_Doc_Type
+ { config_Doc_Type_vars_numbering = True }
+
+docType ::
+ forall src vs t d.
+ Semigroup d =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ Config_Doc_Type ->
+ Precedence ->
+ Type src vs t -> d
+docType conf pr ty =
+ let (v2n, _) = var2Name conf mempty ty in
+ go v2n (infixB SideL pr, SideL) ty
+ where
+ go ::
+ forall x.
+ (Map IndexVar Name) -> -- names of variables
+ (Infix, Side) ->
+ Type src vs x -> d
+ go _v2n _po c
+ | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"
+ go _v2n _po (TyConst _src _vs c) = D.stringH $ show c
+ go v2n _po (TyVar _src _n v) =
+ let iv = indexVar v in
+ case Map.lookup iv v2n of
+ Nothing -> error "[BUG] docType: variable name missing"
+ Just n -> D.textH n
+ go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
+ | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
+ , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
+ go v2n po b
+ | Just (Fixity2 op) <- fixityOf f =
+ (if needsParenInfix po op then D.paren else id) $
+ go v2n (op, SideL) a <>
+ prettyConst f <>
+ go v2n (op, SideR) b
+ where
+ d_op = D.yellower
+ unParen ('(':s) | ')':s' <- reverse s = reverse s'
+ unParen s = s
+ prettyConst :: forall k c. Const src (c::k) -> d
+ prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
+ prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = d_op "," <> D.space
+ prettyConst c | Just HRefl <- proj_ConstKi @(K (,)) @(,) c = d_op "," <> D.space
+ prettyConst c@Const{}
+ | r <- typeRepTyCon (typeRep c)
+ , tyConName r =="#~"
+ , tyConModule r =="Language.Symantic.Typing.Type"
+ -- XXX: module name must be in sync with where (#~) is defined.
+ -- NOTE: cannot use 'proj_ConstKi' here
+ -- because (#~) has a polymorphic kind.
+ = D.space <> d_op "~" <> D.space
+ | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space
+ go v2n po (TyApp _src f a) =
+ let op = infixL 11 in
+ (if needsParenInfix po op then D.paren else id) $
+ go v2n (op, SideL) f <>
+ D.space <>
+ go v2n (op, SideR) a
+ go v2n po (TyFam _src _len fam args) =
+ let op = infixL 11 in
+ (if needsParenInfix po op then D.paren else id) $
+ D.stringH (show fam) <>
+ foldlTys (\t acc ->
+ D.space <> go v2n (op, SideL) t <> acc
+ ) args D.empty
+
+docTypes ::
+ forall src vs ts d.
+ Semigroup d =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ Config_Doc_Type ->
+ Types src vs ts -> d
+docTypes conf tys =
+ d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
+ where
+ d_op = D.yellower
+ go :: forall xs. Types src vs xs -> d
+ go TypesZ = D.empty
+ go (TypesS t0 (TypesS t1 ts)) =
+ docType conf 10 t0 <>
+ d_op (D.charH ',') <> D.space <>
+ docType conf 10 t1 <>
+ go ts
+ go (TypesS t ts) = docType conf 10 t <> go ts
+
+-- | Return a 'Map' associating a distinct 'Name'
+-- for all the variables of the given 'Type'.
+var2Name ::
+ Config_Doc_Type ->
+ (Map IndexVar Name, Names) ->
+ Type src vs t ->
+ (Map IndexVar Name, Names)
+var2Name _cfg st TyConst{} = st
+var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
+ let iv = indexVar v in
+ case Map.lookup iv v2n of
+ Just{} -> st
+ Nothing ->
+ let n' =
+ if config_Doc_Type_vars_numbering cfg && not (T.null n)
+ then n <> T.pack (show iv)
+ else freshifyName ns n in
+ let v2n' = Map.insert iv n' v2n in
+ let ns' = Set.insert n' ns in
+ (v2n', ns')
+var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
+var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
+
+-- ** Type 'Name'
+type Name = Text
+type NameHint = Name
+type Names = Set Name
+
+-- | Return given 'Name' renamed a bit to avoid
+-- conflicting with any given 'Names'.
+freshifyName :: Names -> Name -> Name
+freshifyName ns "" = freshName ns
+freshifyName ns n =
+ let ints = [1..] :: [Int] in
+ L.head
+ [ fresh
+ | suffix <- "" : (show <$> ints)
+ , fresh <- [n <> T.pack suffix]
+ , fresh `Set.notMember` ns
+ ]
+
+freshName :: Names -> Name
+freshName ns = L.head $ poolNames L.\\ Set.toList ns
+
+-- | Infinite list of unique 'Name's:
+-- @a, b, .., z, a1, b1 .., z1, a2, ..@
+poolNames :: [Name]
+poolNames =
+ [ T.singleton n | n <- ['a'..'z'] ] <>
+ [ T.pack (n:show i) | n <- ['a'..'z']
+ , i <- [1 :: Int ..] ]
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Show where
-import Data.Map.Strict (Map)
import Data.Semigroup ((<>))
-import Data.Set (Set)
-import Data.Text (Text)
-import Data.Typeable
-import qualified Data.List as List
-import qualified Data.Map.Strict as Map
-import qualified Data.Set as Set
-import qualified Data.Text as Text
+import qualified Data.Text.Lazy as TL
+import qualified Data.Text.Lazy.Builder as TLB
+import qualified Language.Symantic.Document as D
import Language.Symantic.Grammar
-import Language.Symantic.Typing.Kind
-import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.Type
+import Language.Symantic.Typing.Document
--- * Type 'Config_showType'
-data Config_showType
- = Config_showType
- { config_showType_vars_numbering :: Bool
- }
+showType :: Config_Doc_Type -> Type src vs t -> String
+showType conf ty = TL.unpack $ TLB.toLazyText $ D.plain $ docType conf 0 ty
-config_showType :: Config_showType
-config_showType =
- Config_showType
- { config_showType_vars_numbering = True }
+showTypeS :: Config_Doc_Type -> Precedence -> Type src vs t -> ShowS
+showTypeS conf pr ty s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty)
-showType :: Config_showType -> Int -> Type src vs t -> String
-showType conf pr ty = showTypeS conf pr ty ""
+showTypes :: Config_Doc_Type -> Types src vs ts -> String
+showTypes conf tys = TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)
-showTypeS :: forall src vs t. Config_showType -> Int -> Type src vs t -> ShowS
-showTypeS conf pr ty =
- let (v2n, _) = varNames conf mempty ty in
- go v2n (infixB SideL pr, SideL) ty
- where
- go ::
- forall x.
- (Map IndexVar Name) -> -- names of variables
- (Infix, Side) ->
- Type src vs x ->
- ShowS
- go _v2n _po c
- | Just HRefl <- proj_ConstKiTy @Constraint @() c = showString "()"
- go _v2n _po (TyConst _src _vs c) = showsPrec 11 c
- go v2n _po (TyVar _src _n v) =
- let iv = indexVar v in
- case Map.lookup iv v2n of
- Nothing -> error "[BUG] showsPrec @Type: variable name missing"
- Just n -> showString $ Text.unpack n
- go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
- | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
- , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
- go v2n po b
- | Just (Fixity2 op) <- fixityOf f =
- showParen (needsParenInfix po op) $
- go v2n (op, SideL) a .
- showString (prettyConst f) .
- go v2n (op, SideR) b
- where
- prettyConst :: forall k c. Const src (c::k) -> String
- prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = " => "
- prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = ", "
- prettyConst c@Const{}
- | r <- typeRepTyCon (typeRep c)
- , tyConName r =="#~"
- , tyConModule r =="Language.Symantic.Typing.Type"
- -- XXX: module name must be in sync with where (#~) is defined.
- -- NOTE: cannot use 'proj_ConstKi' here
- -- because (#~) has a polymorphic kind.
- = " ~ "
- | otherwise = ' ' : unParen (show c) ++ " "
- unParen ('(':s) | ')':s' <- reverse s = reverse s'
- unParen s = s
- go v2n po (TyApp _src f a) =
- let op = infixL 11 in
- showParen (needsParenInfix po op) $
- go v2n (op, SideL) f .
- showChar ' ' .
- go v2n (op, SideR) a
- go v2n po (TyFam _src _len fam args) =
- let op = infixL 11 in
- showParen (needsParenInfix po op) $
- showsPrec 11 fam .
- foldlTys (\t acc ->
- showChar ' ' . go v2n (op, SideL) t . acc
- ) args id
-
- -- | Return a 'Map' associating a distinct 'Name'
- -- for all the variables of the given 'Type'.
- varNames ::
- forall x.
- Config_showType ->
- (Map IndexVar Name, Names) ->
- Type src vs x ->
- (Map IndexVar Name, Names)
- varNames _cfg st TyConst{} = st
- varNames cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
- let iv = indexVar v in
- case Map.lookup iv v2n of
- Just{} -> st
- Nothing ->
- let n' = if config_showType_vars_numbering cfg
- then n <> Text.pack (show iv)
- else freshifyName ns n in
- let v2n' = Map.insert iv n' v2n in
- let ns' = Set.insert n' ns in
- (v2n', ns')
- varNames cfg st (TyApp _src f a) = varNames cfg (varNames cfg st f) a
- varNames cfg st (TyFam _src _len _fam as) = foldlTys (flip $ varNames cfg) as st
+showTypesS :: Config_Doc_Type -> Types src vs ts -> ShowS
+showTypesS conf tys s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)
instance Source src => Show (Type src vs t) where
- showsPrec = showTypeS config_showType
+ showsPrec = showTypeS config_doc_type
instance Source src => Show (TypeK src vs kt) where
showsPrec p (TypeK t) = showsPrec p t
instance Source src => Show (TypeVT src) where
instance Source src => Show (TypeT src vs) where
showsPrec p (TypeT t) = showsPrec p t
instance Source src => Show (Types src vs ts) where
- showsPrec _p tys = showString "[" . go tys . showString "]"
- where
- go :: forall xs. Types src vs xs -> ShowS
- go TypesZ = showString ""
- go (TypesS t0 (TypesS t1 ts)) = showsPrec 10 t0 . showString ", " . showsPrec 10 t1 . go ts
- go (TypesS t ts) = showsPrec 10 t . go ts
-
-showBracket :: Bool -> ShowS -> ShowS
-showBracket b p = if b then showChar '{' . p . showChar '}' else p
-
--- ** Type 'Name'
-type Name = Text
-type NameHint = Name
-type Names = Set Name
-
--- | Return given 'Name' renamed a bit to avoid
--- conflicting with any given 'Names'.
-freshifyName :: Names -> Name -> Name
-freshifyName ns "" = freshName ns
-freshifyName ns n =
- let ints = [1..] :: [Int] in
- List.head
- [ fresh
- | suffix <- "" : (show <$> ints)
- , fresh <- [n <> Text.pack suffix]
- , fresh `Set.notMember` ns
- ]
-
-freshName :: Names -> Name
-freshName ns = List.head $ poolNames List.\\ Set.toList ns
-
--- | Infinite list of unique 'Name's:
--- @a, b, .., z, a1, b1 .., z1, a2, ..@
-poolNames :: [Name]
-poolNames =
- [ Text.singleton n | n <- ['a'..'z'] ] <>
- [ Text.pack (n:show i) | n <- ['a'..'z']
- , i <- [1 :: Int ..] ]
+ showsPrec _ = showTypesS config_doc_type
- '.'
- location: '../symantic-grammar'
extra-dep: true
+- location: '../symantic-document'
+ extra-dep: true
Language.Symantic.Transforming.Beta
Language.Symantic.Transforming.Trans
Language.Symantic.Typing
+ Language.Symantic.Typing.Document
Language.Symantic.Typing.Grammar
Language.Symantic.Typing.Kind
Language.Symantic.Typing.List
, ghc-prim
, mono-traversable
, symantic-grammar
+ , symantic-document
, transformers
, text