empty = dupI0 (Proxy @Sym_Alternative) empty
(<|>) = dupI2 (Proxy @Sym_Alternative) (<|>)
-instance Const_from Text cs => Const_from Text (Proxy Alternative ': cs) where
- const_from "Alternative" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Alternative
+ ) => Read_TypeNameR Text cs (Proxy Alternative ': rs) where
+ read_typenameR _cs "Alternative" k = k (ty @Alternative)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Alternative ': cs) where
show_const ConstZ{} = "Alternative"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Alternative))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Alternative))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Alternative
, Inj_Const (Consts_of_Ifaces is) (->)
, Proj_Con (Consts_of_Ifaces is)
pure = dupI1 (Proxy @Sym_Applicative) pure
(<*>) = dupI2 (Proxy @Sym_Applicative) (<*>)
-instance Const_from Text cs => Const_from Text (Proxy Applicative ': cs) where
- const_from "Applicative" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Applicative
+ ) => Read_TypeNameR Text cs (Proxy Applicative ': rs) where
+ read_typenameR _cs "Applicative" k = k (ty @Applicative)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
show_const ConstZ{} = "Applicative"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Applicative))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Applicative))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Applicative
, Inj_Const (Consts_of_Ifaces is) (->)
, Proj_Con (Consts_of_Ifaces is)
(||) = dupI2 (Proxy @Sym_Bool) (||)
xor = dupI2 (Proxy @Sym_Bool) xor
-instance Const_from Text cs => Const_from Text (Proxy Bool ': cs) where
- const_from "Bool" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Bool
+ ) => Read_TypeNameR Text cs (Proxy Bool ': rs) where
+ read_typenameR _cs "Bool" k = k (ty @Bool)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
show_const ConstZ{} = "Bool"
show_const (ConstS c) = show_const c
char_toUpper = dupI1 (Proxy @Sym_Char) char_toUpper
char_toLower = dupI1 (Proxy @Sym_Char) char_toLower
-instance Const_from Text cs => Const_from Text (Proxy Char ': cs) where
- const_from "Char" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Char
+ ) => Read_TypeNameR Text cs (Proxy Char ': rs) where
+ read_typenameR _cs "Char" k = k (ty @Char)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Char ': cs) where
show_const ConstZ{} = "Char"
show_const (ConstS c) = show_const c
_Right = dupI1 (Proxy @Sym_Either) _Right
either = dupI3 (Proxy @Sym_Either) either
-instance Const_from Text cs => Const_from Text (Proxy Either ': cs) where
- const_from "Either" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Either
+ ) => Read_TypeNameR Text cs (Proxy Either ': rs) where
+ read_typenameR _cs "Either" k = k (ty @Either)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Either ': cs) where
show_const ConstZ{} = "Either"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Either))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Either))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Either
, Inj_Const (Consts_of_Ifaces is) (->)
-- , Proj_Token is Token_Type
(==) = dupI2 (Proxy @Sym_Eq) (==)
(/=) = dupI2 (Proxy @Sym_Eq) (/=)
-instance Const_from Text cs => Const_from Text (Proxy Eq ': cs) where
- const_from "Eq" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Eq
+ ) => Read_TypeNameR Text cs (Proxy Eq ': rs) where
+ read_typenameR _cs "Eq" k = k (ty @Eq)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
show_const ConstZ{} = "Eq"
show_const (ConstS c) = show_const c
sequence_ = dupI1 (Proxy @Sym_Foldable) sequence_
traverse_ = dupI2 (Proxy @Sym_Foldable) traverse_
-instance Const_from Text cs => Const_from Text (Proxy Foldable ': cs) where
- const_from "Foldable" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Foldable
+ ) => Read_TypeNameR Text cs (Proxy Foldable ': rs) where
+ read_typenameR _cs "Foldable" k = k (ty @Foldable)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
show_const ConstZ{} = "Foldable"
show_const (ConstS c) = show_const c
(<$>) = fmap
infixl 4 <$>
-instance Const_from Text cs => Const_from Text (Proxy Functor ': cs) where
- const_from "Functor" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Functor
+ ) => Read_TypeNameR Text cs (Proxy Functor ': rs) where
+ read_typenameR _cs "Functor" k = k (ty @Functor)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
show_const ConstZ{} = "Functor"
show_const (ConstS c) = show_const c
io_hClose = dupI1 (Proxy @Sym_IO) io_hClose
io_openFile = dupI2 (Proxy @Sym_IO) io_openFile
-instance Const_from Text cs => Const_from Text (Proxy IO ': cs) where
- const_from "IO" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy IO.Handle ': cs) where
- const_from "IO.Handle" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy IO.IOMode ': cs) where
- const_from "IO.IOMode" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs IO
+ ) => Read_TypeNameR Text cs (Proxy IO ': rs) where
+ read_typenameR _cs "IO" k = k (ty @IO)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs IO.Handle
+ ) => Read_TypeNameR Text cs (Proxy IO.Handle ': rs) where
+ read_typenameR _cs "IO.Handle" k = k (ty @IO.Handle)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs IO.IOMode
+ ) => Read_TypeNameR Text cs (Proxy IO.IOMode ': rs) where
+ read_typenameR _cs "IO.Mode" k = k (ty @IO.IOMode)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy IO ': cs) where
show_const ConstZ{} = "IO"
instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
if_ = dupI3 (Proxy @Sym_If) if_
-instance Const_from Text cs => Const_from Text (Proxy If ': cs) where
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ ) => Read_TypeNameR Text cs (Proxy If ': rs) where
+ read_typenameR _rs = read_typenameR (Proxy @rs)
+instance Show_Const cs => Show_Const (Proxy If ': cs) where
+ show_const ConstZ{} = "If"
+ show_const (ConstS c) = show_const c
instance Proj_ConC cs (Proxy If)
data instance TokenT meta (ts::[*]) (Proxy If)
instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
int x = int x `DupI` int x
-instance Const_from Text cs => Const_from Text (Proxy Int ': cs) where
- const_from "Int" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Int
+ ) => Read_TypeNameR Text cs (Proxy Int ': rs) where
+ read_typenameR _cs "Int" k = k (ty @Int)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Int ': cs) where
show_const ConstZ{} = "Int"
show_const (ConstS c) = show_const c
instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
integer x = integer x `DupI` integer x
-instance Const_from Text cs => Const_from Text (Proxy Integer ': cs) where
- const_from "Integer" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Integer
+ ) => Read_TypeNameR Text cs (Proxy Integer ': rs) where
+ read_typenameR _cs "Integer" k = k (ty @Integer)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
show_const ConstZ{} = "Integer"
show_const (ConstS c) = show_const c
divMod = dupI2 (Proxy @Sym_Integral) divMod
toInteger = dupI1 (Proxy @Sym_Integral) toInteger
-instance Const_from Text cs => Const_from Text (Proxy Integral ': cs) where
- const_from "Integral" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Integral
+ ) => Read_TypeNameR Text cs (Proxy Integral ': rs) where
+ read_typenameR _cs "Integral" k = k (ty @Integral)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
show_const ConstZ{} = "Integral"
show_const (ConstS c) = show_const c
list l1 `DupI` list l2
zipWith = dupI3 (Proxy @Sym_List) zipWith
-instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
- const_from "[]" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs []
+ ) => Read_TypeNameR Text cs (Proxy [] ': rs) where
+ read_typenameR _cs "[]" k = k (ty @[])
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy [] ': cs) where
show_const ConstZ{} = "[]"
show_const (ConstS c) = show_const c
-instance Const_from String cs => Const_from String (Proxy String ': cs) where
- const_from "String" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy String ': cs) where
show_const ConstZ{} = "String"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) []
, Inj_Const (Consts_of_Ifaces is) (->)
, Compile is
map_difference = dupI2 (Proxy @Sym_Map) map_difference
map_foldrWithKey = dupI3 (Proxy @Sym_Map) map_foldrWithKey
-instance Const_from Text cs => Const_from Text (Proxy Map ': cs) where
- const_from "Map" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Map
+ ) => Read_TypeNameR Text cs (Proxy Map ': rs) where
+ read_typenameR _cs "Map" k = k (ty @Map)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Map ': cs) where
show_const ConstZ{} = "Map"
show_const (ConstS c) = show_const c
_Just = dupI1 (Proxy @Sym_Maybe) _Just
maybe = dupI3 (Proxy @Sym_Maybe) maybe
-instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
- const_from "Maybe" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Maybe
+ ) => Read_TypeNameR Text cs (Proxy Maybe ': rs) where
+ read_typenameR _cs "Maybe" k = k (ty @Maybe)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
show_const ConstZ{} = "Maybe"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Maybe
, Inj_Const (Consts_of_Ifaces is) (->)
, Compile is
(>>=) = dupI2 (Proxy @Sym_Monad) (>>=)
when = dupI2 (Proxy @Sym_Monad) when
-instance Const_from Text cs => Const_from Text (Proxy Monad ': cs) where
- const_from "Monad" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Monad
+ ) => Read_TypeNameR Text cs (Proxy Monad ': rs) where
+ read_typenameR _cs "Monad" k = k (ty @Monad)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
show_const ConstZ{} = "Monad"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Monad
, Inj_Const (Consts_of_Ifaces is) (->)
, Inj_Const (Consts_of_Ifaces is) ()
oany = dupI2 (Proxy @Sym_MonoFoldable) oany
otoList = dupI1 (Proxy @Sym_MonoFoldable) otoList
-instance Const_from Text cs => Const_from Text (Proxy MonoFoldable ': cs) where
- const_from "MonoFoldable" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs MonoFoldable
+ ) => Read_TypeNameR Text cs (Proxy MonoFoldable ': rs) where
+ read_typenameR _cs "MonoFoldable" k = k (ty @MonoFoldable)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
show_const ConstZ{} = "MonoFoldable"
show_const (ConstS c) = show_const c
instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
omap = dupI2 (Proxy @Sym_MonoFunctor) omap
-instance Const_from Text cs => Const_from Text (Proxy MonoFunctor ': cs) where
- const_from "MonoFunctor" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs MonoFunctor
+ ) => Read_TypeNameR Text cs (Proxy MonoFunctor ': rs) where
+ read_typenameR _cs "MonoFunctor" k = k (ty @MonoFunctor)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
show_const ConstZ{} = "MonoFunctor"
show_const (ConstS c) = show_const c
(<>) = mappend
infixr 6 <>
-instance Const_from Text cs => Const_from Text (Proxy Monoid ': cs) where
- const_from "Monoid" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Monoid
+ ) => Read_TypeNameR Text cs (Proxy Monoid ': rs) where
+ read_typenameR _cs "Monoid" k = k (ty @Monoid)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
show_const ConstZ{} = "Monoid"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Monoid
, Inj_Const (Consts_of_Ifaces is) (->)
, Proj_Con (Consts_of_Ifaces is)
init = dupI1 (Proxy @Sym_NonNull) init
nfilter = dupI2 (Proxy @Sym_NonNull) nfilter
-instance Const_from Text cs => Const_from Text (Proxy NonNull ': cs) where
- const_from "NonNull" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs NonNull
+ ) => Read_TypeNameR Text cs (Proxy NonNull ': rs) where
+ read_typenameR _cs "NonNull" k = k (ty @NonNull)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
show_const ConstZ{} = "NonNull"
show_const (ConstS c) = show_const c
(*) = dupI2 (Proxy @Sym_Num) (*)
fromInteger = dupI1 (Proxy @Sym_Num) fromInteger
-instance Const_from Text cs => Const_from Text (Proxy Num ': cs) where
- const_from "Num" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Num
+ ) => Read_TypeNameR Text cs (Proxy Num ': rs) where
+ read_typenameR _cs "Num" k = k (ty @Num)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Num ': cs) where
show_const ConstZ{} = "Num"
show_const (ConstS c) = show_const c
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Num))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Num))
instance -- CompileI
- ( Const_from Name_LamVar (Consts_of_Ifaces is)
+ ( Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Inj_Const (Consts_of_Ifaces is) Num
, Inj_Const (Consts_of_Ifaces is) (->)
, Inj_Const (Consts_of_Ifaces is) Integer
min = dupI2 (Proxy @Sym_Ord) min
max = dupI2 (Proxy @Sym_Ord) max
-instance Const_from Text cs => Const_from Text (Proxy Ord ': cs) where
- const_from "Ord" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Ord
+ ) => Read_TypeNameR Text cs (Proxy Ord ': rs) where
+ read_typenameR _cs "Ord" k = k (ty @Ord)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
show_const ConstZ{} = "Ord"
show_const (ConstS c) = show_const c
snoc = dupI2 (Proxy @Sym_SemiSequence) snoc
reverse = dupI1 (Proxy @Sym_SemiSequence) reverse
-instance Const_from Text cs => Const_from Text (Proxy SemiSequence ': cs) where
- const_from "SemiSequence" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs SemiSequence
+ ) => Read_TypeNameR Text cs (Proxy SemiSequence ': rs) where
+ read_typenameR _cs "SemiSequence" k = k (ty @SemiSequence)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
show_const ConstZ{} = "SemiSequence"
show_const (ConstS c) = show_const c
instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
filter = dupI2 (Proxy @Sym_IsSequence) filter
-instance Const_from Text cs => Const_from Text (Proxy IsSequence ': cs) where
- const_from "IsSequence" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs IsSequence
+ ) => Read_TypeNameR Text cs (Proxy IsSequence ': rs) where
+ read_typenameR _cs "IsSequence" k = k (ty @IsSequence)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
show_const ConstZ{} = "IsSequence"
show_const (ConstS c) = show_const c
show = dupI1 (Proxy @Sym_Show) show
showList = dupI1 (Proxy @Sym_Show) showList
-instance Const_from Text cs => Const_from Text (Proxy Show ': cs) where
- const_from "Show" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Show
+ ) => Read_TypeNameR Text cs (Proxy Show ': rs) where
+ read_typenameR _cs "Show" k = k (ty @Show)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Show ': cs) where
show_const ConstZ{} = "Show"
show_const (ConstS c) = show_const c
const a b = lam (lam . Fun.const) .$ a .$ b
-- | /Lambda composition/.
- (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
- (#) f g = lam $ \a -> f .$ (g .$ a)
+ (^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
+ (^) f g = lam $ \a -> f .$ (g .$ a)
flip :: term (a -> b -> c) -> term (b -> a -> c)
flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
infixl 0 .$
-infixr 9 #
+infixr 9 ^
type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
paren p p' $ "let" <> " " <> x <> " = "
<> unTextI e (Precedence 0) (succ v) <> " in "
<> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
- (#) = textI_infix "." (Precedence 9)
+ (^) = textI_infix "." (Precedence 9)
id = textI1 "id"
const = textI2 "const"
flip = textI1 "flip"
where lam_f = lam f
(.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
-instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
- const_from "(->)" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs (->)
+ ) => Read_TypeNameR Text cs (Proxy (->) ': rs) where
+ read_typenameR _cs "(->)" k = k (ty @(->))
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
show_const ConstZ{} = "(->)"
show_const (ConstS c) = show_const c
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
instance -- CompileI (->)
( Inj_Const (Consts_of_Ifaces is) (->)
- , Const_from Name_LamVar (Consts_of_Ifaces is)
+ , Read_TypeName Name_LamVar (Consts_of_Ifaces is)
, Compile is
) => CompileI is (Proxy (->)) where
compileI tok ctx k =
instance (Sym_Text r1, Sym_Text r2) => Sym_Text (DupI r1 r2) where
text x = text x `DupI` text x
-instance Const_from Text cs => Const_from Text (Proxy Text ': cs) where
- const_from "Text" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Text
+ ) => Read_TypeNameR Text cs (Proxy Text ': rs) where
+ read_typenameR _cs "Text" k = k (ty @Text)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Text ': cs) where
show_const ConstZ{} = "Text"
show_const (ConstS c) = show_const c
instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
traverse = dupI2 (Proxy @Sym_Traversable) traverse
-instance Const_from Text cs => Const_from Text (Proxy Traversable ': cs) where
- const_from "Traversable" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Traversable
+ ) => Read_TypeNameR Text cs (Proxy Traversable ': rs) where
+ read_typenameR _cs "Traversable" k = k (ty @Traversable)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
show_const ConstZ{} = "Traversable"
show_const (ConstS c) = show_const c
fst = dupI1 (Proxy @Sym_Tuple2) fst
snd = dupI1 (Proxy @Sym_Tuple2) snd
-instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where
- const_from "(,)" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs (,)
+ ) => Read_TypeNameR Text cs (Proxy (,) ': rs) where
+ read_typenameR _cs "(,)" k = k (ty @(,))
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
show_const ConstZ{} = "(,)"
show_const (ConstS c) = show_const c
instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
unit = unit `DupI` unit
-instance Const_from Text cs => Const_from Text (Proxy () ': cs) where
- const_from "()" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs ()
+ ) => Read_TypeNameR Text cs (Proxy () ': rs) where
+ read_typenameR _cs "()" k = k (ty @())
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy () ': cs) where
show_const ConstZ{} = "()"
show_const (ConstS c) = show_const c
--- /dev/null
+module Parsing.EBNF where
+
+import Data.Text.IO as Text
+import Control.Monad
+
+import Language.Symantic.Typing
+import Language.Symantic.Parsing.Grammar
+import Parsing.Grammar.Test
+import Typing.Test
+
+main :: IO ()
+main = do
+ forM_ gram_lexer render
+ forM_ gram_type render
+ where render = Text.putStrLn . renderEBNF . unCF
--- /dev/null
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+-- | This module defines symantics
+-- for regular or context-free grammars.
+module Language.Symantic.Parsing.Grammar where
+
+import Control.Applicative (Applicative(..), Alternative(..))
+import Control.Monad
+import Data.Char as Char
+import Data.Foldable hiding (any)
+import qualified Data.List as List
+import Data.Semigroup hiding (option)
+import Data.String (IsString(..))
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Prelude hiding (any)
+
+-- * Class 'Gram_Rule'
+type Id a = a -> a
+class Gram_Rule p where
+ rule :: Text -> Id (p a)
+ rule _n = id
+ rule1 :: Text -> Id (p a -> p b)
+ rule1 _n p = p
+ rule2 :: Text -> Id (p a -> p b -> p c)
+ rule2 _n p = p
+ rule3 :: Text -> Id (p a -> p b -> p c -> p d)
+ rule3 _n p = p
+ rule4 :: Text -> Id (p a -> p b -> p c -> p d -> p e)
+ rule4 _n p = p
+
+-- * Type 'Term'
+-- | Terminal grammar.
+newtype Term p a
+ = Term { unTerm :: p a }
+ deriving (Functor, Gram_Term)
+
+-- ** Class 'Gram_Term'
+-- | Symantics for terminal grammars.
+class Gram_Term p where
+ any :: p Char
+ eof :: p ()
+ char :: Char -> p Char
+ string :: String -> p String
+ unicat :: Unicat -> p Char
+ range :: (Char, Char) -> p Char
+ -- string = foldr (\c -> (<*>) ((:) <$> char c)) (pure "")
+ -- string [] = pure []
+ -- string (c:cs) = (:) <$> char c <*> string cs
+
+-- *** Type 'Unicat'
+-- | Unicode category.
+data Unicat
+ = Unicat_Letter
+ | Unicat_Mark
+ | Unicat_Number
+ | Unicat_Punctuation
+ | Unicat_Symbol
+ | Unicat Char.GeneralCategory
+ deriving (Eq, Show)
+
+unicode_categories :: Unicat -> [Char.GeneralCategory]
+unicode_categories c =
+ case c of
+ Unicat_Letter ->
+ [ UppercaseLetter
+ , LowercaseLetter
+ , TitlecaseLetter
+ , ModifierLetter
+ , OtherLetter
+ ]
+ Unicat_Mark ->
+ [ NonSpacingMark
+ , SpacingCombiningMark
+ , EnclosingMark
+ ]
+ Unicat_Number ->
+ [ DecimalNumber
+ , LetterNumber
+ , OtherNumber
+ ]
+ Unicat_Punctuation ->
+ [ ConnectorPunctuation
+ , DashPunctuation
+ , OpenPunctuation
+ , ClosePunctuation
+ , OtherPunctuation
+ ]
+ Unicat_Symbol ->
+ [ MathSymbol
+ , CurrencySymbol
+ , ModifierSymbol
+ , OtherSymbol
+ ]
+ Unicat cat -> [cat]
+
+-- * Type 'Reg'
+-- | Left or right regular grammar.
+newtype Reg (lr::LR) p a = Reg { unReg :: p a }
+ deriving (IsString, Functor, Gram_Term, Alter)
+deriving instance Gram_Rule p => Gram_Rule (Reg lr p)
+deriving instance (Functor p, Alter p, Gram_RegL p) => Gram_RegL (RegL p)
+deriving instance (Functor p, Alter p, Gram_RegR p) => Gram_RegR (RegR p)
+
+-- ** Type 'LR'
+data LR
+ = L -- ^ Left
+ | R -- ^ Right
+ deriving (Eq, Show)
+type RegL = Reg 'L
+type RegR = Reg 'R
+
+-- ** Class 'Alter'
+-- | Like 'Alternative' but without the 'Applicative' super-class,
+-- because a regular grammar is not closed under 'Applicative'.
+class Alter p where
+ nil :: p a
+ (<+>) :: p a -> p a -> p a
+ choice :: [p a] -> p a
+ default nil :: Alternative p => p a
+ default (<+>) :: Alternative p => p a -> p a -> p a
+ default choice :: Alternative p => [p a] -> p a
+ nil = empty
+ (<+>) = (<|>)
+ choice = foldr (<+>) empty
+infixl 3 <+>
+
+-- ** Class 'Gram_RegR'
+-- | Symantics for right regular grammars.
+class (Functor p, Alter p) => Gram_RegR p where
+ (.*>) :: Term p (a -> b) -> RegR p a -> RegR p b
+ manyR :: Term p a -> RegR p [a]
+ manyR p = (:) <$> p .*> manyR p <+> nil
+ someR :: Term p a -> RegR p [a]
+ someR p = (:) <$> p .*> manyR p
+infixl 4 .*>
+
+-- ** Class 'Gram_RegL'
+-- | Symantics for left regular grammars.
+class (Functor p, Alter p) => Gram_RegL p where
+ (<*.) :: RegL p (a -> b) -> Term p a -> RegL p b
+ manyL :: Term p a -> RegL p [a]
+ manyL p' = reverse <$> go p'
+ where go p = flip (:) <$> go p <*. p <+> nil
+ someL :: Term p a -> RegL p [a]
+ someL p = (\cs c -> cs ++ [c]) <$> manyL p <*. p
+infixl 4 <*.
+
+-- * Type 'CF'
+-- | Context-free grammar.
+newtype CF p a = CF { unCF :: p a }
+ deriving (IsString, Functor, Gram_Term, Applicative, App, Alternative, Alter, Alt)
+deriving instance Gram_Rule p => Gram_Rule (CF p)
+deriving instance Gram_CF p => Gram_CF (CF p)
+
+cf_of_reg :: Reg lr p a -> CF p a
+cf_of_reg (Reg p) = CF p
+
+-- ** Class 'Gram_CF'
+-- | Symantics for context-free grammars.
+class Gram_CF p where
+ -- | NOTE: CFL ∩ RL is a CFL.
+ -- See ISBN 81-7808-347-7, Theorem 7.27, p.286
+ (<&) :: CF p (a -> b) -> Reg lr p a -> CF p b
+ (&>) :: Reg lr p (a -> b) -> CF p a -> CF p b
+ -- | NOTE: CFL - RL is a CFL.
+ -- See ISBN 81-7808-347-7, Theorem 7.29, p.289
+ but :: CF p a -> Reg lr p b -> CF p a
+infixl 4 <&
+infixl 4 &>
+
+-- ** Class 'App'
+class Applicative p => App p where
+ between :: p open -> p close -> p a -> p a
+ between open close p = open *> p <* close
+
+-- ** Class 'Alt'
+class Alternative p => Alt p where
+ option :: a -> p a -> p a
+ option x p = p <|> pure x
+ skipMany :: p a -> p ()
+ skipMany = void . many
+ --manyTill :: p a -> p end -> p [a]
+ --manyTill p end = go where go = ([] <$ end) <|> ((:) <$> p <*> go)
+
+-- * Type 'EBNF'
+-- | Extended Bachus-Norm Form, following the
+-- <http://standards.iso.org/ittf/PubliclyAvailableStandards/s026153_ISO_IEC_14977_1996(E).zip ISO-IEC-14977>
+-- notations, augmented with the following notations:
+--
+-- * @("U+", code_point)@: for <http://unicode.org/versions/Unicode8.0.0/ ISO-IEC-10646> (aka. Unicode).
+-- * @(rule, "&", rule)@: for the intersection.
+-- * @(rule, "-", rule)@: for the difference.
+-- * @(rule, " ", rule)@: for rule application.
+data EBNF a = EBNF { unEBNF :: RuleMode -> (Op, LR) -> Text }
+
+runEBNF :: EBNF a -> Text
+runEBNF (EBNF p) = p RuleMode_Body (nop, L)
+
+-- | Get textual rendition of given EBNF rule.
+renderEBNF :: RuleDef a -> Text
+renderEBNF = runEBNF . unRuleDef
+
+ebnf_const :: Text -> EBNF a
+ebnf_const t = EBNF $ \_rm _op -> t
+
+-- ** Type 'RuleDef'
+newtype RuleDef a = RuleDef { unRuleDef :: EBNF a }
+ deriving (Functor, Gram_Term, Applicative, App
+ , Alternative, Alter, Alt, Gram_RegL, Gram_RegR, Gram_CF)
+deriving instance Gram_RuleDef RuleDef
+deriving instance Gram_RuleDef p => Gram_RuleDef (RegR p)
+deriving instance Gram_RuleDef p => Gram_RuleDef (RegL p)
+deriving instance Gram_RuleDef p => Gram_RuleDef (CF p)
+
+instance Gram_Rule RuleDef where
+ rule n = rule_def (ebnf_const n)
+ rule1 n p a = rule_def (ebnf_const n `ebnf_arg` unRuleDef a) (p a)
+ rule2 n p a b = rule_def (ebnf_const n `ebnf_arg` unRuleDef a `ebnf_arg` unRuleDef b) (p a b)
+ rule3 n p a b c = rule_def (ebnf_const n `ebnf_arg` unRuleDef a `ebnf_arg` unRuleDef b `ebnf_arg` unRuleDef c) (p a b c)
+ rule4 n p a b c d = rule_def (ebnf_const n `ebnf_arg` unRuleDef a `ebnf_arg` unRuleDef b `ebnf_arg` unRuleDef c `ebnf_arg` unRuleDef d) (p a b c d)
+
+-- *** Class 'Gram_RuleDef'
+class Gram_RuleDef p where
+ rule_def :: EBNF () -> p a -> RuleDef a
+ rule_arg :: Text -> p a
+
+-- | Helper for 'Gram_Rule' 'EBNF'.
+ebnf_arg :: EBNF a -> EBNF b -> EBNF ()
+ebnf_arg (EBNF a) (EBNF b) = EBNF $ \bo po -> op_paren po op $
+ a bo (op, L) <> " " <> b bo (op, R)
+ where op = Op " " 11 AssocL
+infixl 5 `ebnf_arg`
+
+instance Gram_RuleDef EBNF where
+ rule_arg = ebnf_const
+ rule_def call body =
+ RuleDef $ EBNF $ \mo po ->
+ case mo of
+ RuleMode_Ref -> unEBNF call mo po
+ RuleMode_Body ->
+ Text.intercalate " " $ concat $
+ [ [unEBNF call RuleMode_Ref (nop, L)]
+ , ["="]
+ , [unEBNF body RuleMode_Ref (nop, R)]
+ , [";"]
+ ]
+instance IsString (EBNF String) where
+ fromString = string
+instance Show (EBNF a) where
+ show = Text.unpack . runEBNF
+instance Gram_Rule EBNF where
+ rule n p = EBNF $ \rm po ->
+ case rm of
+ RuleMode_Body -> unEBNF p RuleMode_Ref po
+ RuleMode_Ref -> n
+ rule1 n p a = EBNF $ \rm po ->
+ case rm of
+ RuleMode_Body -> unEBNF (p a) RuleMode_Ref po
+ RuleMode_Ref -> unEBNF (ebnf_const n `ebnf_arg` a) RuleMode_Ref po
+ rule2 n p a b = EBNF $ \rm po ->
+ case rm of
+ RuleMode_Body -> unEBNF (p a b) RuleMode_Ref po
+ RuleMode_Ref -> unEBNF (ebnf_const n `ebnf_arg` a `ebnf_arg` b) RuleMode_Ref po
+ rule3 n p a b c = EBNF $ \rm po ->
+ case rm of
+ RuleMode_Body -> unEBNF (p a b c) RuleMode_Ref po
+ RuleMode_Ref -> unEBNF (ebnf_const n `ebnf_arg` a `ebnf_arg` b `ebnf_arg` c) RuleMode_Ref po
+ rule4 n p a b c d = EBNF $ \rm po ->
+ case rm of
+ RuleMode_Body -> unEBNF (p a b c d) RuleMode_Ref po
+ RuleMode_Ref -> unEBNF (ebnf_const n `ebnf_arg` a `ebnf_arg` b `ebnf_arg` c `ebnf_arg` d) RuleMode_Ref po
+instance Functor EBNF where
+ fmap _f (EBNF x) = EBNF x
+instance Applicative EBNF where
+ pure _ = empty
+ EBNF f <*> EBNF x = EBNF $ \bo po -> op_paren po op $
+ f bo (op, L) <> ", " <> x bo (op, R)
+ where op = Op "," 10 AssocB
+instance App EBNF
+instance Alternative EBNF where
+ empty = ebnf_const $ "\"\""
+ EBNF x <|> EBNF y = EBNF $ \bo po -> op_paren po op $
+ x bo (op, L) <> " | " <> y bo (op, R)
+ where op = Op "|" 2 AssocB
+ many (EBNF x) = EBNF $ \rm _po -> "{ " <> x rm (op, L) <> " }" where op = nop
+ some (EBNF x) = EBNF $ \rm _po -> "{ " <> x rm (op, L) <> " }-" where op = nop
+instance Alter EBNF where
+ choice [] = empty
+ choice [p] = p
+ choice l@(_:_) = EBNF $ \bo po -> op_paren po op $
+ Text.intercalate " | " $
+ (unEBNF <$> l) <*> pure bo <*> pure (op, L)
+ where op = Op "|" 2 AssocB
+instance Alt EBNF
+instance Gram_Term EBNF where
+ any = ebnf_const "_"
+ eof = ebnf_const "EOF"
+ char = ebnf_const . escape
+ where
+ escape c | Char.isPrint c && c /= '"' = Text.concat $ ["\"", Text.singleton c, "\""]
+ escape c = Text.concat ["U+", Text.pack $ show $ ord c]
+ string s =
+ case List.break (\c -> not (Char.isPrint c) || c == '"') s of
+ (ps, "") -> raw ps
+ ("", [c]) -> "" <$ char c
+ (ps, [c]) -> "" <$ raw ps <* char c
+ ("", c:rs) -> "" <$ char c <* string rs
+ (ps, c:rs) -> "" <$ raw ps <* char c <* string rs
+ where
+ raw cs = ebnf_const $ Text.concat $ ["\"", Text.pack cs, "\""]
+ unicat = ebnf_const . Text.pack . show
+ range (l, h) = ebnf_const $ Text.concat
+ [ runEBNF $ char l
+ , "…"
+ , runEBNF $ char h
+ ]
+instance Gram_RegR EBNF where
+ Term f .*> Reg x = Reg $ f <*> x
+ manyR = Reg . many . unTerm
+ someR = Reg . some . unTerm
+instance Gram_RegL EBNF where
+ Reg f <*. Term x = Reg $ f <*> x
+ manyL = Reg . many . unTerm
+ someL = Reg . some . unTerm
+instance Gram_CF EBNF where
+ CF (EBNF f) <& Reg (EBNF p) = CF $ EBNF $ \bo po -> op_paren po op $
+ f bo (op, L) <> " & " <> p bo (op, R)
+ where op = Op "&" 4 AssocL
+ Reg (EBNF f) &> CF (EBNF p) = CF $ EBNF $ \bo po -> op_paren po op $
+ f bo (op, L) <> " & " <> p bo (op, R)
+ where op = Op "&" 4 AssocL
+ CF (EBNF f) `but` Reg (EBNF p) = CF $ EBNF $ \bo po -> op_paren po op $
+ f bo (op, L) <> " - " <> p bo (op, R)
+ where op = Op "-" 6 AssocL
+
+-- ** Type 'RuleMode'
+data RuleMode
+ = RuleMode_Body -- ^ Generate the body of the rule.
+ | RuleMode_Ref -- ^ Generate a ref to the rule.
+ deriving (Eq, Show)
+
+-- ** Type 'Op'
+data Op = Op
+ { op_ident :: Text
+ , op_prece :: Precedence
+ , op_assoc :: Associativity
+ } deriving (Eq, Show)
+
+nop :: Op
+nop = Op "" 0 AssocN
+
+-- *** Type 'Precedence'
+type Precedence = Int
+
+-- *** Type 'Associativity'
+data Associativity
+ = AssocL | AssocR | AssocN | AssocB
+ deriving (Eq, Show)
+
+op_paren
+ :: (Semigroup s, IsString s)
+ => (Op, LR) -> Op -> s -> s
+op_paren (po, lr) op s =
+ if op_prece op <= op_prece po && not associate
+ then fromString "(" <> s <> fromString ")"
+ else s
+ where
+ associate =
+ op_ident po == op_ident op &&
+ case (lr, op_assoc po) of
+ (_, AssocB) -> True
+ (L, AssocL) -> True
+ (R, AssocR) -> True
+ _ -> False
+
+-- * Class 'Gram_Context'
+-- | A monadic backdoor, but limited by 'Context'.
+-- In 'CF', the context must obviously not be used to change the parser,
+-- but it can be used to change the parsed value,
+-- for instance by recording source positions into it.
+class Gram_Context p where
+ type Context p
+ type Context p = ()
+ default context :: (Context p ~ ()) => (Context p -> p a) -> p a
+ context :: (Context p -> p a) -> p a
+ context f = f ()
+instance Gram_Context p => Gram_Context (CF p) where
+ type Context (CF p) = Context p
+ context f = CF $ context (unCF . f)
+instance Gram_Context EBNF
+instance Gram_Context RuleDef
+
+-- * Class 'Gram_Lexer'
+class
+ ( Alt p
+ , Alter p
+ , Alternative p
+ , App p
+ , Gram_CF p
+ , Gram_Rule p
+ , Gram_Term p
+ ) => Gram_Lexer p where
+ commentable :: p () -> p () -> p () -> p ()
+ commentable = rule3 "commentable" $ \p line block ->
+ skipMany $ choice [p, line, block]
+ comment_line :: CF p String -> CF p String
+ comment_line prefix = rule "comment_line" $
+ prefix *> many (any `but` (void (char '\n') <+> eof))
+ comment_block :: CF p String -> Reg lr p String -> CF p String
+ comment_block start end = rule "comment_block" $
+ start *> many (any `but` void end)
+ lexeme :: CF p a -> CF p a
+ lexeme = rule1 "lexeme" $ \p -> p
+ <* commentable
+ (void $ char ' ')
+ (void $ comment_line (string "--"))
+ (void $ comment_block (string "{-") (string "-}"))
+ parens :: CF p a -> CF p a
+ parens = rule1 "parens" $
+ between
+ (lexeme $ string "(")
+ (lexeme $ string ")")
+ infixrP :: (a -> a -> a) -> CF p a -> CF p sep -> CF p a -> CF p a
+ infixrP f =
+ rule3 "infixrP" $ \next sep root ->
+ (\a -> \case Just b -> f a b; Nothing -> a)
+ <$> next <*> option Nothing (Just <$ sep <*> root)
+ inside :: (a -> b) -> CF p begin -> CF p a -> CF p end -> CF p b -> CF p b
+ inside f = rule4 "inside" $ \begin i end n ->
+ (f <$ begin <*> i <* end) <+> n
+ symbol :: String -> CF p String
+ symbol = lexeme . string
+
+deriving instance Gram_Lexer p => Gram_Lexer (CF p)
+instance Gram_Lexer EBNF
+instance Gram_Lexer RuleDef
+
+gram_lexer :: forall p . (Gram_Lexer p, Gram_RuleDef p) => [CF p ()]
+gram_lexer =
+ [ () <$ commentable (void $ rule_arg "space") (void $ rule_arg "line") (void $ rule_arg "block")
+ , () <$ comment_line (rule_arg "prefix")
+ , () <$ comment_block (rule_arg "start") (rule_arg "end" :: Reg 'L p String)
+ , () <$ lexeme (rule_arg "p")
+ , () <$ parens (rule_arg "p")
+ , () <$ inside id (rule_arg "begin") (rule_arg "i") (rule_arg "end") (rule_arg "next")
+ , () <$ infixrP const (rule_arg "next") (rule_arg "sep") (rule_arg "root")
+ ]
--- /dev/null
+{-# LANGUAGE ConstrainedClassMethods #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | This module defines symantics
+-- for regular or context-free grammars.
+-- It is intended to be imported qualified.
+module Parsing.Grammar.Test where
+
+import Control.Applicative (Applicative(..), Alternative(..))
+import Data.Maybe
+import Control.Monad
+-- import Control.Comonad
+import qualified Data.Char as Char
+import Data.Foldable hiding (any)
+import Data.Functor.Identity
+import qualified Data.List as List
+import Data.Semigroup ((<>))
+import Data.Proxy
+import Data.Text (Text)
+import Data.String (IsString(..))
+import qualified Data.Text as Text
+import qualified Data.Text.IO as Text
+import Prelude hiding (any, (^))
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Lexer as L
+
+import qualified Language.Symantic.Compiling as Sym
+import qualified Language.Symantic.Typing as Sym
+import qualified Language.Symantic.Parsing as Sym
+import Language.Symantic.Parsing.Grammar
+
+-- * Type 'ParsecT'
+type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)
+instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where
+ fromString = P.string
+instance ParsecC e s => Gram_Rule (P.ParsecT e s m) where
+ rule = P.label . Text.unpack
+instance ParsecC e s => Gram_Term (P.ParsecT e s m) where
+ any = P.anyChar
+ eof = P.eof
+ char = P.char
+ string = P.string
+ unicat cat = P.satisfy $ (`List.elem` cats) . Char.generalCategory
+ where cats = unicode_categories cat
+ range (l, h) = P.satisfy $ \c -> l <= c && c <= h
+instance ParsecC e s => Alter (P.ParsecT e s m) where
+ x <+> y = P.try x <|> y
+instance ParsecC e s => Gram_RegR (P.ParsecT e s m) where
+ Term f .*> Reg x = Reg $ f <*> x
+instance ParsecC e s => Gram_RegL (P.ParsecT e s m) where
+ Reg f <*. Term x = Reg $ f <*> x
+instance ParsecC e s => App (P.ParsecT e s m)
+instance ParsecC e s => Alt (P.ParsecT e s m)
+instance ParsecC e s => Gram_CF (P.ParsecT e s m) where
+ CF f <& Reg p = CF $ P.lookAhead f <*> p
+ Reg f &> CF p = CF $ P.lookAhead f <*> p
+ but (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f
+instance ParsecC e s => Gram_Context (P.ParsecT e s m) where
+ type Context (P.ParsecT e s m) = P.SourcePos
+ context = (P.getPosition >>=)
+instance ParsecC e s => Gram_Lexer (P.ParsecT e s m)
+instance ParsecC e s => Sym.Gram_Type (P.ParsecT e s m)
+
+runParserT :: Monad m
+ => P.ParsecT P.Dec s m a -> s
+ -> m (Either (P.ParseError (P.Token s) P.Dec) a)
+runParserT p = P.runParserT p ""
+
+runParser
+ :: P.ParsecT P.Dec s Identity a -> s
+ -> Either (P.ParseError (P.Token s) P.Dec) a
+runParser p = P.runParser p ""
+
+
+
+{-
+-- Tests
+g1 = (<>) <$> string "0" <*> string "1"
+g2 = (<>) <$> string "0" <* string "X" <*> string "1"
+g3 = (<>) <$> (string "0" <|> string "1") <*> string "2"
+g4 = string "0" <|> string "1" <|> string "2"
+g5 = choice [string "0", string "1", string "2"]
+g6 = (<>) <$> choice [(<>) <$> string "0" <*> string "1", string "2" <|> string "3", string "4"] <*> string "5"
+g7 = concat <$> many (string "0")
+g8 = (concat <$>) $ (<>) <$> many (string "0" <|> string "1") <*> some (string "2")
+g9 = (<>) <$> string "0" .*> someR (char '1')
+g10 = (<>) <$> someL (char '1') <*. string "0"
+g11 = string "0" `but` g9 `but` g10
+g12 = (<>) <$> string "0" <& g9
+g13 = string "abé\"to"
+g14 = string "\""
+g15 = string ""
+g16 = many $ unicat [Unicat_Letter]
+g17 = many $ range ('a', 'z')
+g18 = ("" <$) $ commentable (void g1) (void g2) (void g3)
+g19 = ("" <$) $ choice [g5]
+g20 = "" <$ char 'a' <* char 'b' <* char 'c'
+g21 = "" <$ comment_line "--"
+g22 = "" <$ lexeme (string "A")
+g23 = "" <$ keywords
+
+main :: IO ()
+main = do
+ putStrLn "EBNF"
+ {-
+ forM_
+ [ g1, g2, g3, g4, g5, g6, g7, g8
+ , g11, g12, g13, g14, g15, g16, g17, g18
+ , g19, g20, g21, g22, cf_of_reg g23
+ ] $ \g -> do
+ Text.putStrLn $ runEBNF RuleMode_Def $ unCF g
+ -}
+ forM_
+ [ "" <$ comment_line (rule_arg "prefix")
+ , "" <$ comment_block (rule_arg "start") (rule_arg "end" :: Reg 'L RuleDef String)
+ , "" <$ commentable (void $ rule_arg "space") (void $ rule_arg "line") (void $ rule_arg "block")
+ , "" <$ lexeme (rule_arg "p")
+ , "" <$ parens (rule_arg "p")
+ , "" <$ inside id (rule_arg "begin") (rule_arg "i") (rule_arg "end") (rule_arg "next")
+ , "" <$ infixrP const (rule_arg "next") (rule_arg "sep") (rule_arg "root")
+ {-
+ , "" <$ typeP
+ , "" <$ type_list
+ , "" <$ type_tuple2
+ , "" <$ type_fun
+ , "" <$ type_app
+ , "" <$ type_atom
+ , "" <$ type_name
+ -}
+ ] $ \g -> do
+ Text.putStrLn $ runEBNF $ unRuleDef $ unCF g
+ putStrLn ""
+ {-
+ putStrLn "Tests"
+ forM_
+ [ "Bool"
+ , "(Bool)"
+ , "((Bool))"
+ , "Bool, Int"
+ , "(Bool, Int)"
+ , "((Bool, Int), Char)"
+ , "(Bool, Int) -> Char"
+ , "(Bool -> Int)"
+ , "((Bool, Int), Char)"
+ , "String"
+ , "[Char]"
+ , "[Char] -> String"
+ , "String -> [Char]"
+ , "Maybe Bool"
+ , "Either Bool Int"
+ , "Bool -> Int"
+ , "(Bool -> Int) -> Char"
+ , "(Bool -> Int) Char"
+ , "Bool -> (Int -> Char)"
+ , "Bool -> Int -> Char"
+ ] $ \s -> do
+ putStr (show (s::Text))
+ Text.putStr " ==> "
+ print $ (compile_type <$>) $ runIdentity $ runParser (unCF (typeP <* eof)) s
+ -}
+
+-}
{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ConstrainedClassMethods #-}
+{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
Proj_ConstsR cs '[] = '[]
Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs
--- * Class 'Const_from'
--- | Try to build a 'Const' from raw data.
-class Const_from raw cs where
- const_from
- :: raw -> (forall k c. Const cs (c::k) -> Maybe ret)
- -> Maybe ret
-
-instance Const_from raw '[] where
- const_from _c _k = Nothing
-
--- TODO: move each of these to a dedicated module.
-instance Const_from Text cs => Const_from Text (Proxy Bounded ': cs) where
- const_from "Bounded" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Enum ': cs) where
- const_from "Enum" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Fractional ': cs) where
- const_from "Fractional" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-instance Const_from Text cs => Const_from Text (Proxy Real ': cs) where
- const_from "Real" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
-
-- * Class 'Show_Const'
class Show_Const cs where
show_const :: Const cs c -> String
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where
import Test.Tasty
import Test.Tasty.HUnit
+import Control.Applicative (Applicative(..), Alternative(..))
+import Control.Arrow (left)
+import qualified Data.Char as Char
+import Data.Functor.Identity
import Data.Maybe (isJust)
import Data.Proxy
+import Data.Semigroup ((<>))
import Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Data.Text.IO as Text
import GHC.Exts (Constraint)
+import Prelude hiding (exp)
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Lexer as L
+import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Parsing
+import Language.Symantic.Parsing.Grammar
import Language.Symantic.Typing
-import Language.Symantic.Compiling
+import Language.Symantic.Compiling ((~>))
import Parsing.Test
+import Parsing.Grammar.Test
-- * Tests
+type Tys = Constants ++ '[Proxy String]
+
tests :: TestTree
tests = testGroup "Typing" $
[ testGroup "compile_type" $
- let (==>) (syn::Syntax Text) expected =
- let Right (tok::EToken (Syntax Text) '[Proxy Token_Type]) = tokenize_type syn in
- testCase (Prelude.show syn) $
- (@?= EType Prelude.<$> expected) $
- (compile_type tok (Right . EType)
- :: Either (Error_Type (Syntax Text) '[Proxy Token_Type])
- (EType Constants))
- in
- [ sy @Bool ==> Right (ty @Bool)
- , sy @IO [] ==> Right (ty @IO)
- , sy @Eq [] ==> Right (ty @Eq)
- , sy @(->) [sy @Bool] ==> Right (ty @(->) :$ ty @Bool)
- , sy @Eq [sy @Bool] ==> Right (ty @Eq :$ ty @Bool)
- , sy @Monad [sy @IO []] ==> Right (ty @Monad :$ ty @IO)
- , sy @(->) [sy @IO [sy @Bool]] ==> Right (ty @(->) :$ (ty @IO :$ ty @Bool))
- , (sy @Bool .> sy @Bool) ==> Right
- (ty @Bool ~> ty @Bool)
- , ((sy @Bool .> sy @Bool) .> sy @Bool) ==> Right
- ((ty @Bool ~> ty @Bool) ~> ty @Bool)
- , ((sy @Bool .> sy @Int) .> sy @Bool) ==> Right
- ((ty @Bool ~> ty @Int) ~> ty @Bool)
- , (sy @Bool .> sy @Int .> sy @Bool) ==> Right
- (ty @Bool ~> ty @Int ~> ty @Bool)
- , ((sy @Bool .> (sy @Bool .> sy @Int)) .> sy @Bool) ==> Right
- ((ty @Bool ~> (ty @Bool ~> ty @Int)) ~> ty @Bool)
- , testGroup "Error_Type"
- [ sy @(->) [sy @IO []] ==> Left
- (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
- (At (maybeRight $ tokenize_type $ sy @(->) [sy @IO []]) $ EKind SKiType)
- (At (maybeRight $ tokenize_type $ sy @IO []) $ EKind $ SKiType `SKiArrow` SKiType))
- , sy @IO [sy @Eq [sy @Bool]] ==> Left
- (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
- (At (maybeRight $ tokenize_type $ sy @IO [sy @Eq [sy @Bool]]) $ EKind SKiType)
- (At (maybeRight $ tokenize_type $ sy @Eq [sy @Bool]) $ EKind $ SKiConstraint))
- , Syntax "Bool" [sy @Bool] ==> Left
- (Error_Type_Constraint_Kind $ Constraint_Kind_Arrow
- (At (maybeRight $ tokenize_type $ Syntax "Bool" [sy @Bool]) $ EKind SKiType))
- , Syntax ("Unknown"::Text) [] ==> Left
- (Error_Type_Constant_unknown $
- At (maybeRight $ tokenize_type $ Syntax ("Unknown"::Text) []) "Unknown")
- ]
+ let (==>) inp exp = testCase inp $ got @?= Right (Right (exp::EType Tys))
+ where got = (compile_etype <$>) $ (`runParser` inp) $ unCF $ typeP <* eof in
+ uncurry (==>) <$>
+ [ ("Bool", EType $ ty @Bool)
+ , ("[]", EType $ ty @[])
+ , ("[Char]", EType $ ty @[] :$ ty @Char)
+ , ("([])", EType $ ty @[])
+ , ("[()]", EType $ ty @[] :$ ty @())
+ , ("()", EType $ ty @())
+ , ("(())", EType $ ty @())
+ , ("(,)", EType $ ty @(,))
+ , ("((,))", EType $ ty @(,))
+ , ("(,) Int", EType $ ty @(,) :$ ty @Int)
+ , ("(Bool)", EType $ ty @Bool)
+ , ("((Bool))", EType $ ty @Bool)
+ , ("(Bool, Int)", EType $ ty @(,) :$ ty @Bool :$ ty @Int)
+ , ("((Bool, Int))", EType $ ty @(,) :$ ty @Bool :$ ty @Int)
+ , ("((Bool, Int), Char)", EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char)
+ , ("(Bool, Int) -> Char", EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char)
+ , ("(Bool -> Int)", EType $ ty @Bool ~> ty @Int)
+ , ("String", EType $ ty @[] :$ ty @Char)
+ , ("[Char] -> String", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char))
+ , ("String -> [Char]", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char))
+ , ("Maybe Bool", EType $ ty @Maybe :$ ty @Bool)
+ , ("Either Bool Int", EType $ ty @Either :$ ty @Bool :$ ty @Int)
+ , ("Bool -> Int", EType $ ty @Bool ~> ty @Int)
+ , ("(Bool -> Int) -> Char", EType $ (ty @Bool ~> ty @Int) ~> ty @Char)
+ , ("Bool -> (Int -> Char)", EType $ ty @Bool ~> (ty @Int ~> ty @Char))
+ , ("Bool -> Int -> Char", EType $ ty @Bool ~> ty @Int ~> ty @Char)
+ , ("Bool -> (Int -> Char) -> ()", EType $ ty @Bool ~> (ty @Int ~> ty @Char) ~> ty @())
+ , ("IO", EType $ ty @IO)
+ , ("Eq", EType $ ty @Eq)
+ , ("Eq Bool", EType $ ty @Eq :$ ty @Bool)
+ , ("Traversable IO", EType $ ty @Traversable :$ ty @IO)
+ , ("Monad IO", EType $ ty @Monad :$ ty @IO)
+ , ("(->) Bool", EType $ ty @(->) :$ ty @Bool)
+ , ("(->) (IO Bool)", EType $ ty @(->) :$ (ty @IO :$ ty @Bool))
+ , ("Monad IO", EType $ ty @Monad :$ ty @IO)
]
+ , testGroup "Parsing errors" $
+ let (==>) inp _exp = testCase inp $ got @?= Left ()
+ where got = left (const ()) $ (`runParser` inp) $ unCF $ typeP <* eof in
+ uncurry (==>) <$>
+ [ ("Bool, Int", ())
+ , ("(Bool -> Int) Char", ())
+ ]
+ , testGroup "Compiling errors" $
+ let (==>) inp _exp = testCase inp $ got @?= Right (Left () :: Either () (EType Tys))
+ where got = (left (const ()) . compile_etype <$>) $
+ (`runParser` inp) $ unCF $ typeP <* eof in
+ uncurry (==>) <$>
+ [ ("NonExistingType", ())
+ , ("Bool Int", ())
+ , ("[IO]", ())
+ , ("(->) IO", ())
+ , ("(->) Bool Int Char", ())
+ , ("Monad Eq", ())
+ ]
, testGroup "proj_con" $
let (==>) (typ::Type Constants (h::Constraint)) expected =
testCase (show_type typ) $
- isJust (proj_con typ) @?= expected
- in
- [ (ty @Eq :$ ty @Bool) ==> True
- , (ty @Ord :$ ty @Bool) ==> True
- , (ty @Functor :$ ty @Maybe) ==> True
- , (ty @Functor :$ ty @IO) ==> True
- , (ty @Monad :$ ty @IO) ==> True
- , (ty @Traversable :$ ty @IO) ==> False
+ isJust (proj_con typ) @?= expected in
+ [ ty @Eq :$ ty @Bool ==> True
+ , ty @Ord :$ ty @Bool ==> True
+ , ty @Functor :$ ty @Maybe ==> True
+ , ty @Functor :$ ty @IO ==> True
+ , ty @Monad :$ ty @IO ==> True
+ , ty @Traversable :$ ty @IO ==> False
]
]
+{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Type where
+import Control.Applicative (Applicative(..), Alternative(..))
+import qualified Data.Char as Char
import Data.Monoid ((<>))
import Data.Proxy
import Data.Maybe (fromMaybe, isJust)
import Data.Text (Text)
+import qualified Data.Text as Text
import Data.Type.Equality
import qualified Data.Kind as K
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant
-import Language.Symantic.Parsing.Token
+import Language.Symantic.Parsing
+import Language.Symantic.Parsing.Grammar
-- * Type 'Type'
show_type :: Show_Const cs => Type cs h -> String
show_type (TyConst c) = show c
-show_type ((:$) f@(:$){} a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
-show_type ((:$) f@(:$){} a) = "(" <> show_type f <> ") " <> show_type a
-show_type ((:$) f a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
-show_type ((:$) f a) = show_type f <> " " <> show_type a
+show_type (f@(:$){} :$ a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
+show_type (f@(:$){} :$ a) = "(" <> show_type f <> ") " <> show_type a
+show_type (f :$ a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
+show_type (f :$ a) = show_type f <> " " <> show_type a
-- show_type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
+-- | Cons a @new_c@ to @cs@.
+type_lift :: Type cs c -> Type (new_c ': cs) c
+type_lift (TyConst c) = TyConst (ConstS c)
+type_lift (f :$ a) = type_lift f :$ type_lift a
+
-- * Type 'EType'
-- | Existential for 'Type'.
data EType cs = forall h. EType (Type cs h)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))
-instance Const_from Text cs => Const_from Text (Proxy Token_Type ': cs) where
- const_from "Type" k = k (ConstZ kind)
- const_from s k = const_from s $ k . ConstS
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Token_Type
+ ) => Read_TypeNameR Text cs (Proxy Token_Type ': rs) where
+ read_typenameR _rs "Type" k = k (ty @Token_Type)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Token_Type ': cs) where
show_const ConstZ{} = "Type"
show_const (ConstS c) = show_const c
-- * Class 'Compile_Type'
--- | Try to build a 'Type' from raw data.
+-- | Try to build a 'Type' from name data.
class Compile_Type ts cs where
compile_type
:: ( MonoLift (Error_Type meta ts) err
-> (forall k h. Type cs (h::k) -> Either err ret)
-> Either err ret
+compile_etype
+ :: Read_TypeName Text cs
+ => EToken meta '[Proxy Token_Type]
+ -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
+compile_etype tok = compile_type tok (Right . EType)
+
-- ** Type 'Constraint_Kind'
data Constraint_Kind meta ts
= Constraint_Kind_Eq (At meta ts EKind) (At meta ts EKind)
deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)
+-- * Class 'Read_TypeName'
+type Read_TypeName raw cs = Read_TypeNameR raw cs cs
+
+read_typename
+ :: forall raw cs ret.
+ Read_TypeNameR raw cs cs
+ => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
+ -> Maybe ret
+read_typename = read_typenameR (Proxy @cs)
+
+-- ** Class 'Read_TypeNameR'
+class Read_TypeNameR raw cs rs where
+ read_typenameR
+ :: Proxy rs -> raw -> (forall k c. Type cs (c::k) -> Maybe ret)
+ -> Maybe ret
+
+instance Read_TypeNameR raw cs '[] where
+ read_typenameR _cs _c _k = Nothing
+
+-- TODO: move each of these to a dedicated module.
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Bounded
+ ) => Read_TypeNameR Text cs (Proxy Bounded ': rs) where
+ read_typenameR _cs "Bounded" k = k (ty @Bounded)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Enum
+ ) => Read_TypeNameR Text cs (Proxy Enum ': rs) where
+ read_typenameR _cs "Enum" k = k (ty @Enum)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Fractional
+ ) => Read_TypeNameR Text cs (Proxy Fractional ': rs) where
+ read_typenameR _cs "Fractional" k = k (ty @Fractional)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs Real
+ ) => Read_TypeNameR Text cs (Proxy Real ': rs) where
+ read_typenameR _cs "Real" k = k (ty @Real)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+instance
+ ( Read_TypeNameR Text cs rs
+ , Inj_Const cs []
+ , Inj_Const cs Char
+ ) => Read_TypeNameR Text cs (Proxy String ': rs) where
+ read_typenameR _cs "String" k = k (ty @[] :$ ty @Char)
+ read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
+
instance
- ( Const_from Text cs
+ ( Read_TypeName Text cs
, Proj_Token ts Token_Type
) => Compile_Type ts cs where
compile_type
-> Either err ret
compile_type tok@(proj_etoken -> Just (Token_Type cst args)) kk =
fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
- const_from cst $ \c -> Just $
- go args (TyConst c) kk
+ read_typename cst $ \typ -> Just $
+ go args typ kk
where
go :: [EToken meta ts]
-> Type cs h
instance
MonoLift (Constraint_Kind meta ts) (Error_Type meta ts) where
olift = olift . Error_Type_Constraint_Kind
+
+-- * Class 'Gram_Type'
+type ToType p = EToken (Context p) '[Proxy Token_Type]
+class
+ ( Alt p
+ , Alter p
+ , Alternative p
+ , App p
+ , Gram_CF p
+ , Gram_Rule p
+ , Gram_Term p
+ , Gram_Lexer p
+ , Gram_Context p
+ ) => Gram_Type p where
+ typeP :: CF p (ToType p)
+ typeP = rule "type" $ type_fun
+ type_fun :: CF p (ToType p)
+ type_fun = rule "type_fun" $
+ context $ \meta ->
+ let f a b = inj_etoken meta $ Token_Type "(->)" [a, b] in
+ infixrP f type_list (symbol "->") typeP
+ type_list :: CF p (ToType p)
+ type_list = rule "type_list" $
+ context $ \meta ->
+ let f = inj_etoken meta . Token_Type "[]" in
+ inside f (symbol "[") (option [] (pure <$> typeP)) (symbol "]") type_tuple2
+ type_tuple2 :: CF p (ToType p)
+ type_tuple2 = rule "type_tuple2" $
+ context $ \meta ->
+ let f a b = inj_etoken meta $ Token_Type "(,)" [a, b] in
+ parens (infixrP f typeP (symbol ",") typeP) <+> type_app
+ type_app :: CF p (ToType p)
+ type_app = rule "type_app" $
+ (\(EToken (TokenZ meta (Token_Type f as)):as') ->
+ (EToken (TokenZ meta (Token_Type f (as <> as')))))
+ <$> some type_atom
+ type_atom :: CF p (ToType p)
+ type_atom = rule "type_atom" $
+ parens typeP <+>
+ type_name <+>
+ type_symbol
+ type_name :: CF p (ToType p)
+ type_name = rule "type_name" $
+ context $ \meta ->
+ lexeme $
+ (\c cs -> EToken $ TokenZ meta $ Token_Type (Text.pack $ c:cs) [])
+ <$> unicat (Unicat Char.UppercaseLetter)
+ <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
+ type_symbol :: CF p (ToType p)
+ type_symbol = rule "type_symbol" $
+ context $ \meta ->
+ let f s = inj_etoken meta $ (`Token_Type` []) $
+ Text.concat ["(", Text.pack s, ")"] in
+ (f <$>) $ parens $ many $ choice (unicat <$>
+ [ Unicat_Symbol
+ , Unicat_Punctuation
+ , Unicat_Mark
+ ]) `but` char ')'
+
+deriving instance Gram_Type p => Gram_Type (CF p)
+instance Gram_Type EBNF
+instance Gram_Type RuleDef
+
+gram_type :: Gram_Type p => [CF p (ToType p)]
+gram_type =
+ [ typeP
+ , type_fun
+ , type_list
+ , type_tuple2
+ , type_app
+ , type_atom
+ , type_name
+ , type_symbol
+ ]
Language.Symantic.Lib.Data.Type.Peano
Language.Symantic.Parsing
Language.Symantic.Parsing.Token
+ Language.Symantic.Parsing.Grammar
Language.Symantic.Transforming
Language.Symantic.Transforming.Trans
Language.Symantic.Typing
TypeFamilies
TypeOperators
default-language: Haskell2010
- ghc-options: -Wall -fno-warn-tabs
+ ghc-options: -Wall -fno-warn-tabs -O0
-main-is Test
-- -fprint-explicit-kinds
hs-source-dirs: Language/Symantic
Compiling.MonoFunctor.Test
Compiling.Term.Test
Compiling.Test
+ Parsing.Grammar.Test
Parsing.Test
Typing.Test
build-depends:
base >= 4.6 && < 5
, containers
+ , megaparsec
, mono-traversable
, transformers
, tasty >= 0.11
, tasty-hunit
, text
, symantic
+
+Test-Suite ebnf
+ type: exitcode-stdio-1.0
+ default-extensions:
+ ConstraintKinds
+ DataKinds
+ EmptyDataDecls
+ FlexibleContexts
+ FlexibleInstances
+ MultiParamTypeClasses
+ NamedFieldPuns
+ OverloadedStrings
+ PatternGuards
+ PolyKinds
+ Rank2Types
+ ScopedTypeVariables
+ StandaloneDeriving
+ TupleSections
+ TypeFamilies
+ TypeApplications
+ TypeOperators
+ ghc-options: -Wall -fno-warn-tabs
+ -main-is Parsing.EBNF
+ main-is: Parsing/EBNF.hs
+ default-language: Haskell2010
+ hs-source-dirs: Language/Symantic
+ build-depends:
+ base >= 4.6 && < 5
+ , containers
+ , megaparsec
+ , transformers
+ , tasty >= 0.11
+ , tasty-hunit
+ , text
+ , symantic
sourcephile / git / haskell / symantic.git / commitdiff