{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Syntaxes.Data where
import Data.Bool (Bool)
import Data.Either (Either)
import Data.Eq qualified as Eq
import Data.Function qualified as Fun
import Data.Maybe (Maybe)
import Data.Maybe qualified as Maybe
import Data.Semigroup (Semigroup)
import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
import Symantic.Syntaxes.Classes
import Symantic.Syntaxes.Derive
data SomeData sem a
= forall able.
( Derivable (Data able sem)
, Typeable able
) =>
SomeData (Data able sem a)
type instance Derived (SomeData sem) = sem
instance Derivable (SomeData sem) where
derive :: forall a. SomeData sem a -> Derived (SomeData sem) a
derive (SomeData Data able sem a
x) = Data able sem a -> Derived (Data able sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive Data able sem a
x
data family Data (able :: Syntax) :: Semantic -> Semantic
type instance Derived (Data able sem) = sem
pattern Data :: Typeable able => Data able sem a -> SomeData sem a
pattern $mData :: forall {r} {able :: Syntax} {sem :: * -> *} {a}.
Typeable able =>
SomeData sem a -> (Data able sem a -> r) -> (Void# -> r) -> r
Data x <- (unSomeData -> Maybe.Just x)
unSomeData ::
forall able sem a.
Typeable able =>
SomeData sem a ->
Maybe (Data able sem a)
unSomeData :: forall (able :: Syntax) (sem :: * -> *) a.
Typeable able =>
SomeData sem a -> Maybe (Data able sem a)
unSomeData (SomeData (Data able sem a
c :: Data c sem a)) =
case forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: Syntax). Typeable a => TypeRep a
typeRep @able TypeRep able -> TypeRep able -> Maybe (able :~~: able)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: Syntax). Typeable a => TypeRep a
typeRep @c of
Maybe.Just able :~~: able
HRefl -> Data able sem a -> Maybe (Data able sem a)
forall a. a -> Maybe a
Maybe.Just Data able sem a
c
Maybe (able :~~: able)
Maybe.Nothing -> Maybe (Data able sem a)
forall a. Maybe a
Maybe.Nothing
data instance Data Abstractable sem a where
Lam :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
Lam1 :: (SomeData sem a -> SomeData sem b) -> Data Abstractable sem (a -> b)
Var :: sem a -> Data Abstractable sem a
instance Abstractable sem => Derivable (Data Abstractable sem) where
derive :: forall a.
Data Abstractable sem a -> Derived (Data Abstractable sem) a
derive = \case
Lam SomeData sem a -> SomeData sem b
f -> (sem a -> sem b) -> sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam (\sem a
x -> SomeData sem b -> Derived (SomeData sem) b
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive (SomeData sem a -> SomeData sem b
f (Data Abstractable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (sem a -> Data Abstractable sem a
forall (sem :: * -> *) a. sem a -> Data Abstractable sem a
Var sem a
x))))
Lam1 SomeData sem a -> SomeData sem b
f -> (sem a -> sem b) -> sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\sem a
x -> SomeData sem b -> Derived (SomeData sem) b
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive (SomeData sem a -> SomeData sem b
f (Data Abstractable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (sem a -> Data Abstractable sem a
forall (sem :: * -> *) a. sem a -> Data Abstractable sem a
Var sem a
x))))
Var sem a
x -> sem a -> sem a
forall (sem :: * -> *) a. Abstractable sem => sem a -> sem a
var sem a
x
instance Abstractable sem => Abstractable (SomeData sem) where
lam :: forall a b.
(SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
lam SomeData sem a -> SomeData sem b
f = Data Abstractable sem (a -> b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData ((SomeData sem a -> SomeData sem b)
-> Data Abstractable sem (a -> b)
forall (sem :: * -> *) a l.
(SomeData sem a -> SomeData sem l)
-> Data Abstractable sem (a -> l)
Lam SomeData sem a -> SomeData sem b
f)
lam1 :: forall a b.
(SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
lam1 SomeData sem a -> SomeData sem b
f = Data Abstractable sem (a -> b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData ((SomeData sem a -> SomeData sem b)
-> Data Abstractable sem (a -> b)
forall (sem :: * -> *) a l.
(SomeData sem a -> SomeData sem l)
-> Data Abstractable sem (a -> l)
Lam1 SomeData sem a -> SomeData sem b
f)
var :: forall a. SomeData sem a -> SomeData sem a
var = SomeData sem a -> SomeData sem a
forall a. a -> a
Fun.id
normalOrderReduction ::
forall sem a.
Abstractable sem =>
IfThenElseable sem =>
SomeData sem a ->
SomeData sem a
normalOrderReduction :: forall (sem :: * -> *) a.
(Abstractable sem, IfThenElseable sem) =>
SomeData sem a -> SomeData sem a
normalOrderReduction = SomeData sem a -> SomeData sem a
forall b. SomeData sem b -> SomeData sem b
nor
where
nor :: SomeData sem b -> SomeData sem b
nor :: forall b. SomeData sem b -> SomeData sem b
nor = \case
Data (Lam SomeData sem a -> SomeData sem b
f) -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem b -> SomeData sem b)
-> (SomeData sem a -> SomeData sem b)
-> SomeData sem a
-> SomeData sem b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData sem a -> SomeData sem b
f)
Data (Lam1 SomeData sem a -> SomeData sem b
f) -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem b -> SomeData sem b)
-> (SomeData sem a -> SomeData sem b)
-> SomeData sem a
-> SomeData sem b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData sem a -> SomeData sem b
f)
Data (SomeData sem (a -> b)
x :@ SomeData sem a
y) -> case SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
whnf SomeData sem (a -> b)
x of
Data (Lam1 SomeData sem a -> SomeData sem b
f) -> SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor (SomeData sem a -> SomeData sem b
f SomeData sem a
SomeData sem a
y)
SomeData sem (a -> b)
x' -> SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem (a -> b)
x' SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a -> SomeData sem a
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem a
y
Data (IfThenElse SomeData sem Bool
test SomeData sem b
ok SomeData sem b
ko) ->
case SomeData sem Bool -> SomeData sem Bool
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem Bool
test of
Data (Constant Bool
b :: Data (Constantable Bool) sem Bool) ->
if Bool
b then SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ok else SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ko
SomeData sem Bool
t -> SomeData sem Bool
-> SomeData sem b -> SomeData sem b -> SomeData sem b
forall (sem :: * -> *) a.
IfThenElseable sem =>
sem Bool -> sem a -> sem a -> sem a
ifThenElse (SomeData sem Bool -> SomeData sem Bool
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem Bool
t) (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ok) (SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
nor SomeData sem b
ko)
SomeData sem b
x -> SomeData sem b
x
whnf :: SomeData sem b -> SomeData sem b
whnf :: forall b. SomeData sem b -> SomeData sem b
whnf = \case
Data (SomeData sem (a -> b)
x :@ SomeData sem a
y) -> case SomeData sem (a -> b) -> SomeData sem (a -> b)
forall b. SomeData sem b -> SomeData sem b
whnf SomeData sem (a -> b)
x of
Data (Lam1 SomeData sem a -> SomeData sem b
f) -> SomeData sem b -> SomeData sem b
forall b. SomeData sem b -> SomeData sem b
whnf (SomeData sem a -> SomeData sem b
f SomeData sem a
SomeData sem a
y)
SomeData sem (a -> b)
x' -> SomeData sem (a -> b)
x' SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
y
SomeData sem b
x -> SomeData sem b
x
data instance Data Unabstractable sem a where
(:@) :: SomeData sem (a -> b) -> SomeData sem a -> Data Unabstractable sem b
instance Unabstractable sem => Derivable (Data Unabstractable sem) where
derive :: forall a.
Data Unabstractable sem a -> Derived (Data Unabstractable sem) a
derive = \case
SomeData sem (a -> a)
f :@ SomeData sem a
x -> SomeData sem (a -> a) -> Derived (SomeData sem) (a -> a)
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem (a -> a)
f sem (a -> a) -> sem a -> sem a
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
x
instance Unabstractable sem => Unabstractable (SomeData sem) where
SomeData sem (a -> b)
f .@ :: forall a b.
SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
.@ SomeData sem a
x = Data Unabstractable sem b -> SomeData sem b
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (SomeData sem (a -> b)
f SomeData sem (a -> b)
-> SomeData sem a -> Data Unabstractable sem b
forall (sem :: * -> *) a b.
SomeData sem (a -> b)
-> SomeData sem a -> Data Unabstractable sem b
:@ SomeData sem a
x)
instance
( Abstractable sem
) =>
Functionable (SomeData sem)
where
$ :: forall a b. SomeData sem ((a -> b) -> a -> b)
($) = (SomeData sem (a -> b) -> SomeData sem (a -> b))
-> SomeData sem ((a -> b) -> a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b)
f -> (SomeData sem a -> SomeData sem b) -> SomeData sem (a -> b)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem (a -> b)
f SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
x))
. :: forall b c a. SomeData sem ((b -> c) -> (a -> b) -> a -> c)
(.) = (SomeData sem (b -> c) -> SomeData sem ((a -> b) -> a -> c))
-> SomeData sem ((b -> c) -> (a -> b) -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (b -> c)
f -> (SomeData sem (a -> b) -> SomeData sem (a -> c))
-> SomeData sem ((a -> b) -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b)
g -> (SomeData sem a -> SomeData sem c) -> SomeData sem (a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem (b -> c)
f SomeData sem (b -> c) -> SomeData sem b -> SomeData sem c
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ (SomeData sem (a -> b)
g SomeData sem (a -> b) -> SomeData sem a -> SomeData sem b
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
x))))
const :: forall a b. SomeData sem (a -> b -> a)
const = (SomeData sem a -> SomeData sem (b -> a))
-> SomeData sem (a -> b -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> (SomeData sem b -> SomeData sem a) -> SomeData sem (b -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem b
_y -> SomeData sem a
x))
flip :: forall a b c. SomeData sem ((a -> b -> c) -> b -> a -> c)
flip = (SomeData sem (a -> b -> c) -> SomeData sem (b -> a -> c))
-> SomeData sem ((a -> b -> c) -> b -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem (a -> b -> c)
f -> (SomeData sem b -> SomeData sem (a -> c))
-> SomeData sem (b -> a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem b
x -> (SomeData sem a -> SomeData sem c) -> SomeData sem (a -> c)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
y -> SomeData sem (a -> b -> c)
f SomeData sem (a -> b -> c)
-> SomeData sem a -> SomeData sem (b -> c)
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem a
y SomeData sem (b -> c) -> SomeData sem b -> SomeData sem c
forall (sem :: * -> *) a b.
Unabstractable sem =>
sem (a -> b) -> sem a -> sem b
.@ SomeData sem b
x)))
id :: forall a. SomeData sem (a -> a)
id = (SomeData sem a -> SomeData sem a) -> SomeData sem (a -> a)
forall (sem :: * -> *) a b.
Abstractable sem =>
(sem a -> sem b) -> sem (a -> b)
lam1 (\SomeData sem a
x -> SomeData sem a
x)
data instance Data Anythingable sem a where
Anything :: sem a -> Data Anythingable sem a
instance
( Anythingable sem
) =>
Derivable (Data Anythingable sem)
where
derive :: forall a.
Data Anythingable sem a -> Derived (Data Anythingable sem) a
derive = \case
Anything sem a
x -> sem a -> sem a
forall (sem :: * -> *) a. Anythingable sem => sem a -> sem a
anything sem a
x
instance Anythingable (SomeData sem)
instance Anythingable (Data Anythingable sem)
data instance Data Bottomable sem a where
Bottom :: Data Bottomable sem a
instance Bottomable sem => Derivable (Data Bottomable sem) where
derive :: forall a. Data Bottomable sem a -> Derived (Data Bottomable sem) a
derive Bottom{} = Derived (Data Bottomable sem) a
forall (sem :: * -> *) a. Bottomable sem => sem a
bottom
data instance Data (Constantable c) sem a where
Constant :: c -> Data (Constantable c) sem c
instance Constantable c sem => Derivable (Data (Constantable c) sem) where
derive :: forall a.
Data (Constantable c) sem a
-> Derived (Data (Constantable c) sem) a
derive = \case
Constant c
x -> c -> sem c
forall c (sem :: * -> *). Constantable c sem => c -> sem c
constant c
x
instance
( Constantable c sem
, Typeable c
) =>
Constantable c (SomeData sem)
where
constant :: c -> SomeData sem c
constant c
c = Data (Constantable c) sem c -> SomeData sem c
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (c -> Data (Constantable c) sem c
forall c (sem :: * -> *). c -> Data (Constantable c) sem c
Constant c
c)
instance Constantable c (Data (Constantable c) sem) where
constant :: c -> Data (Constantable c) sem c
constant = c -> Data (Constantable c) sem c
forall c (sem :: * -> *). c -> Data (Constantable c) sem c
Constant
data instance Data Eitherable sem a where
Either :: Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
Left :: Data Eitherable sem (l -> Either l r)
Right :: Data Eitherable sem (r -> Either l r)
instance Eitherable sem => Derivable (Data Eitherable sem) where
derive :: forall a. Data Eitherable sem a -> Derived (Data Eitherable sem) a
derive = \case
Data Eitherable sem a
R:DataEitherablesema sem a
Either -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) l a r.
Eitherable sem =>
sem ((l -> a) -> (r -> a) -> Either l r -> a)
either
Data Eitherable sem a
R:DataEitherablesema sem a
Left -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) l r. Eitherable sem => sem (l -> Either l r)
left
Data Eitherable sem a
R:DataEitherablesema sem a
Right -> Derived (Data Eitherable sem) a
forall (sem :: * -> *) r l. Eitherable sem => sem (r -> Either l r)
right
instance Eitherable sem => Eitherable (SomeData sem) where
either :: forall l a r.
SomeData sem ((l -> a) -> (r -> a) -> Either l r -> a)
either = Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
-> SomeData sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a l r.
Data Eitherable sem ((a -> l) -> (r -> l) -> Either a r -> l)
Either
left :: forall l r. SomeData sem (l -> Either l r)
left = Data Eitherable sem (l -> Either l r)
-> SomeData sem (l -> Either l r)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem (l -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either a l)
Left
right :: forall r l. SomeData sem (r -> Either l r)
right = Data Eitherable sem (r -> Either l r)
-> SomeData sem (r -> Either l r)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Eitherable sem (r -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either l a)
Right
instance Eitherable (Data Eitherable sem) where
either :: forall l a r.
Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
either = Data Eitherable sem ((l -> a) -> (r -> a) -> Either l r -> a)
forall (sem :: * -> *) a l r.
Data Eitherable sem ((a -> l) -> (r -> l) -> Either a r -> l)
Either
left :: forall l r. Data Eitherable sem (l -> Either l r)
left = Data Eitherable sem (l -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either a l)
Left
right :: forall r l. Data Eitherable sem (r -> Either l r)
right = Data Eitherable sem (r -> Either l r)
forall (sem :: * -> *) a l. Data Eitherable sem (a -> Either l a)
Right
data instance Data Equalable sem a where
Equal :: Eq.Eq a => Data Equalable sem (a -> a -> Bool)
instance Equalable sem => Derivable (Data Equalable sem) where
derive :: forall a. Data Equalable sem a -> Derived (Data Equalable sem) a
derive = \case
Data Equalable sem a
R:DataEqualablesema sem a
Equal -> Derived (Data Equalable sem) a
forall (sem :: * -> *) a.
(Equalable sem, Eq a) =>
sem (a -> a -> Bool)
equal
instance
( Equalable sem
) =>
Equalable (SomeData sem)
where
equal :: forall a. Eq a => SomeData sem (a -> a -> Bool)
equal = Data Equalable sem (a -> a -> Bool)
-> SomeData sem (a -> a -> Bool)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Equalable sem (a -> a -> Bool)
forall a (sem :: * -> *).
Eq a =>
Data Equalable sem (a -> a -> Bool)
Equal
instance Equalable (Data Equalable sem) where
equal :: forall a. Eq a => Data Equalable sem (a -> a -> Bool)
equal = Data Equalable sem (a -> a -> Bool)
forall a (sem :: * -> *).
Eq a =>
Data Equalable sem (a -> a -> Bool)
Equal
data instance Data Emptyable sem a where
Empty :: Data Emptyable sem a
instance Emptyable sem => Derivable (Data Emptyable sem) where
derive :: forall a. Data Emptyable sem a -> Derived (Data Emptyable sem) a
derive = \case
Data Emptyable sem a
R:DataEmptyablesema sem a
Empty -> Derived (Data Emptyable sem) a
forall (sem :: * -> *) a. Emptyable sem => sem a
empty
instance
( Emptyable sem
) =>
Emptyable (SomeData sem)
where
empty :: forall a. SomeData sem a
empty = Data Emptyable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Emptyable sem a
forall (sem :: * -> *) a. Data Emptyable sem a
Empty
instance Emptyable (Data Emptyable sem) where
empty :: forall a. Data Emptyable sem a
empty = Data Emptyable sem a
forall (sem :: * -> *) a. Data Emptyable sem a
Empty
data instance Data Semigroupable sem a where
Concat :: Semigroup a => Data Semigroupable sem (a -> a -> a)
infixr 4 `Concat`
instance Semigroupable sem => Derivable (Data Semigroupable sem) where
derive :: forall a.
Data Semigroupable sem a -> Derived (Data Semigroupable sem) a
derive = \case
Data Semigroupable sem a
R:DataSemigroupablesema sem a
Concat -> Derived (Data Semigroupable sem) a
forall (sem :: * -> *) a.
(Semigroupable sem, Semigroup a) =>
sem (a -> a -> a)
concat
instance
( Semigroupable sem
) =>
Semigroupable (SomeData sem)
where
concat :: forall a. Semigroup a => SomeData sem (a -> a -> a)
concat = Data Semigroupable sem (a -> a -> a) -> SomeData sem (a -> a -> a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Semigroupable sem (a -> a -> a)
forall a (sem :: * -> *).
Semigroup a =>
Data Semigroupable sem (a -> a -> a)
Concat
instance Semigroupable (Data Semigroupable sem) where
concat :: forall a. Semigroup a => Data Semigroupable sem (a -> a -> a)
concat = Data Semigroupable sem (a -> a -> a)
forall a (sem :: * -> *).
Semigroup a =>
Data Semigroupable sem (a -> a -> a)
Concat
data instance Data IfThenElseable sem a where
IfThenElse ::
SomeData sem Bool ->
SomeData sem a ->
SomeData sem a ->
Data IfThenElseable sem a
instance IfThenElseable sem => Derivable (Data IfThenElseable sem) where
derive :: forall a.
Data IfThenElseable sem a -> Derived (Data IfThenElseable sem) a
derive = \case
IfThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko -> sem Bool -> sem a -> sem a -> sem a
forall (sem :: * -> *) a.
IfThenElseable sem =>
sem Bool -> sem a -> sem a -> sem a
ifThenElse (SomeData sem Bool -> Derived (SomeData sem) Bool
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem Bool
test) (SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
ok) (SomeData sem a -> Derived (SomeData sem) a
forall (sem :: * -> *) a. Derivable sem => sem a -> Derived sem a
derive SomeData sem a
ko)
instance
( IfThenElseable sem
) =>
IfThenElseable (SomeData sem)
where
ifThenElse :: forall a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> SomeData sem a
ifThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko = Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData (SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
forall (sem :: * -> *) a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
IfThenElse SomeData sem Bool
test SomeData sem a
ok SomeData sem a
ko)
instance IfThenElseable sem => IfThenElseable (Data IfThenElseable sem) where
ifThenElse :: forall a.
Data IfThenElseable sem Bool
-> Data IfThenElseable sem a
-> Data IfThenElseable sem a
-> Data IfThenElseable sem a
ifThenElse Data IfThenElseable sem Bool
test Data IfThenElseable sem a
ok Data IfThenElseable sem a
ko = SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
forall (sem :: * -> *) a.
SomeData sem Bool
-> SomeData sem a -> SomeData sem a -> Data IfThenElseable sem a
IfThenElse (Data IfThenElseable sem Bool -> SomeData sem Bool
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem Bool
test) (Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem a
ok) (Data IfThenElseable sem a -> SomeData sem a
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data IfThenElseable sem a
ko)
data instance Data Listable sem a where
Cons :: Data Listable sem (a -> [a] -> [a])
Nil :: Data Listable sem [a]
infixr 4 `Cons`
instance Listable sem => Derivable (Data Listable sem) where
derive :: forall a. Data Listable sem a -> Derived (Data Listable sem) a
derive = \case
Data Listable sem a
R:DataListablesema sem a
Cons -> Derived (Data Listable sem) a
forall (sem :: * -> *) a. Listable sem => sem (a -> [a] -> [a])
cons
Data Listable sem a
R:DataListablesema sem a
Nil -> Derived (Data Listable sem) a
forall (sem :: * -> *) a. Listable sem => sem [a]
nil
instance
( Listable sem
) =>
Listable (SomeData sem)
where
cons :: forall a. SomeData sem (a -> [a] -> [a])
cons = Data Listable sem (a -> [a] -> [a])
-> SomeData sem (a -> [a] -> [a])
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Listable sem (a -> [a] -> [a])
forall (sem :: * -> *) a. Data Listable sem (a -> [a] -> [a])
Cons
nil :: forall a. SomeData sem [a]
nil = Data Listable sem [a] -> SomeData sem [a]
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Listable sem [a]
forall (sem :: * -> *) a. Data Listable sem [a]
Nil
instance Listable (Data Listable sem) where
cons :: forall a. Data Listable sem (a -> [a] -> [a])
cons = Data Listable sem (a -> [a] -> [a])
forall (sem :: * -> *) a. Data Listable sem (a -> [a] -> [a])
Cons
nil :: forall a. Data Listable sem [a]
nil = Data Listable sem [a]
forall (sem :: * -> *) a. Data Listable sem [a]
Nil
data instance Data Maybeable sem a where
Nothing :: Data Maybeable sem (Maybe a)
Just :: Data Maybeable sem (a -> Maybe a)
instance Maybeable sem => Derivable (Data Maybeable sem) where
derive :: forall a. Data Maybeable sem a -> Derived (Data Maybeable sem) a
derive = \case
Data Maybeable sem a
R:DataMaybeablesema sem a
Nothing -> Derived (Data Maybeable sem) a
forall (sem :: * -> *) a. Maybeable sem => sem (Maybe a)
nothing
Data Maybeable sem a
R:DataMaybeablesema sem a
Just -> Derived (Data Maybeable sem) a
forall (sem :: * -> *) a. Maybeable sem => sem (a -> Maybe a)
just
instance
( Maybeable sem
) =>
Maybeable (SomeData sem)
where
nothing :: forall a. SomeData sem (Maybe a)
nothing = Data Maybeable sem (Maybe a) -> SomeData sem (Maybe a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Maybeable sem (Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (Maybe a)
Nothing
just :: forall a. SomeData sem (a -> Maybe a)
just = Data Maybeable sem (a -> Maybe a) -> SomeData sem (a -> Maybe a)
forall (sem :: * -> *) a (able :: Syntax).
(Derivable (Data able sem), Typeable able) =>
Data able sem a -> SomeData sem a
SomeData Data Maybeable sem (a -> Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (a -> Maybe a)
Just
instance Maybeable (Data Maybeable sem) where
nothing :: forall a. Data Maybeable sem (Maybe a)
nothing = Data Maybeable sem (Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (Maybe a)
Nothing
just :: forall a. Data Maybeable sem (a -> Maybe a)
just = Data Maybeable sem (a -> Maybe a)
forall (sem :: * -> *) a. Data Maybeable sem (a -> Maybe a)
Just