{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Data where
import Data.Bool (Bool)
import Data.Either (Either)
import Data.Kind (Constraint)
import Data.Maybe (Maybe)
import Type.Reflection (Typeable, (:~~:)(..), eqTypeRep, typeRep)
import qualified Data.Eq as Eq
import qualified Data.Maybe as Maybe
import qualified Data.Function as Fun
import Symantic.Lang
import Symantic.Derive
data SomeData repr a =
forall able.
( Derivable (Data able repr)
, Typeable able
) => SomeData (Data able repr a)
type instance Derived (SomeData repr) = repr
instance Derivable (SomeData repr) where
derive :: SomeData repr a -> Derived (SomeData repr) a
derive (SomeData Data able repr a
x) = Data able repr a -> Derived (Data able repr) a
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive Data able repr a
x
data family Data
(able :: ReprKind -> Constraint)
:: ReprKind -> ReprKind
type instance Derived (Data able repr) = repr
pattern Data :: Typeable able => Data able repr a -> SomeData repr a
pattern $mData :: forall r (able :: (* -> *) -> Constraint) (repr :: * -> *) a.
Typeable able =>
SomeData repr a -> (Data able repr a -> r) -> (Void# -> r) -> r
Data x <- (unSomeData -> Maybe.Just x)
unSomeData ::
forall able repr a.
Typeable able =>
SomeData repr a -> Maybe (Data able repr a)
unSomeData :: SomeData repr a -> Maybe (Data able repr a)
unSomeData (SomeData (Data able repr a
c::Data c repr a)) =
case Typeable able => TypeRep able
forall k (a :: k). 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` Typeable able => TypeRep able
forall k (a :: k). Typeable a => TypeRep a
typeRep @c of
Maybe.Just able :~~: able
HRefl -> Data able repr a -> Maybe (Data able repr a)
forall a. a -> Maybe a
Maybe.Just Data able repr a
c
Maybe (able :~~: able)
Maybe.Nothing -> Maybe (Data able repr a)
forall a. Maybe a
Maybe.Nothing
data instance Data Abstractable repr a where
(:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
Var :: repr a -> Data Abstractable repr a
instance
( Abstractable repr
) => Derivable (Data Abstractable repr) where
derive :: Data Abstractable repr a -> Derived (Data Abstractable repr) a
derive = \case
f :@ x -> SomeData repr (a -> a) -> Derived (SomeData repr) (a -> a)
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive SomeData repr (a -> a)
f repr (a -> a) -> repr a -> repr a
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a -> Derived (SomeData repr) a
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive SomeData repr a
x
Lam f -> (repr a -> repr b) -> repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (\repr a
x -> SomeData repr b -> Derived (SomeData repr) b
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive (SomeData repr a -> SomeData repr b
f (Data Abstractable repr a -> SomeData repr a
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData (repr a -> Data Abstractable repr a
forall (repr :: * -> *) a. repr a -> Data Abstractable repr a
Var repr a
x))))
Lam1 f -> (repr a -> repr b) -> repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\repr a
x -> SomeData repr b -> Derived (SomeData repr) b
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive (SomeData repr a -> SomeData repr b
f (Data Abstractable repr a -> SomeData repr a
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData (repr a -> Data Abstractable repr a
forall (repr :: * -> *) a. repr a -> Data Abstractable repr a
Var repr a
x))))
Var x -> repr a -> repr a
forall (repr :: * -> *) a. Abstractable repr => repr a -> repr a
var repr a
x
instance
( Abstractable repr
) => Abstractable (SomeData repr) where
SomeData repr (a -> b)
f .@ :: SomeData repr (a -> b) -> SomeData repr a -> SomeData repr b
.@ SomeData repr a
x = Data Abstractable repr b -> SomeData repr b
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData (SomeData repr (a -> b)
f SomeData repr (a -> b)
-> SomeData repr a -> Data Abstractable repr b
forall (repr :: * -> *) a b.
SomeData repr (a -> b)
-> SomeData repr a -> Data Abstractable repr b
:@ SomeData repr a
x)
lam :: (SomeData repr a -> SomeData repr b) -> SomeData repr (a -> b)
lam SomeData repr a -> SomeData repr b
f = Data Abstractable repr (a -> b) -> SomeData repr (a -> b)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData ((SomeData repr a -> SomeData repr b)
-> Data Abstractable repr (a -> b)
forall (repr :: * -> *) a b.
(SomeData repr a -> SomeData repr b)
-> Data Abstractable repr (a -> b)
Lam SomeData repr a -> SomeData repr b
f)
lam1 :: (SomeData repr a -> SomeData repr b) -> SomeData repr (a -> b)
lam1 SomeData repr a -> SomeData repr b
f = Data Abstractable repr (a -> b) -> SomeData repr (a -> b)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData ((SomeData repr a -> SomeData repr b)
-> Data Abstractable repr (a -> b)
forall (repr :: * -> *) a b.
(SomeData repr a -> SomeData repr b)
-> Data Abstractable repr (a -> b)
Lam1 SomeData repr a -> SomeData repr b
f)
var :: SomeData repr a -> SomeData repr a
var = SomeData repr a -> SomeData repr a
forall a. a -> a
Fun.id
$ :: SomeData repr ((a -> b) -> a -> b)
($) = (SomeData repr (a -> b) -> SomeData repr (a -> b))
-> SomeData repr ((a -> b) -> a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr (a -> b)
f -> (SomeData repr a -> SomeData repr b) -> SomeData repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr a
x -> SomeData repr (a -> b)
f SomeData repr (a -> b) -> SomeData repr a -> SomeData repr b
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a
x))
. :: SomeData repr ((b -> c) -> (a -> b) -> a -> c)
(.) = (SomeData repr (b -> c) -> SomeData repr ((a -> b) -> a -> c))
-> SomeData repr ((b -> c) -> (a -> b) -> a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr (b -> c)
f -> (SomeData repr (a -> b) -> SomeData repr (a -> c))
-> SomeData repr ((a -> b) -> a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr (a -> b)
g -> (SomeData repr a -> SomeData repr c) -> SomeData repr (a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr a
x -> SomeData repr (b -> c)
f SomeData repr (b -> c) -> SomeData repr b -> SomeData repr c
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ (SomeData repr (a -> b)
g SomeData repr (a -> b) -> SomeData repr a -> SomeData repr b
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a
x))))
const :: SomeData repr (a -> b -> a)
const = (SomeData repr a -> SomeData repr (b -> a))
-> SomeData repr (a -> b -> a)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr a
x -> (SomeData repr b -> SomeData repr a) -> SomeData repr (b -> a)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr b
_y -> SomeData repr a
x))
flip :: SomeData repr ((a -> b -> c) -> b -> a -> c)
flip = (SomeData repr (a -> b -> c) -> SomeData repr (b -> a -> c))
-> SomeData repr ((a -> b -> c) -> b -> a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr (a -> b -> c)
f -> (SomeData repr b -> SomeData repr (a -> c))
-> SomeData repr (b -> a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr b
x -> (SomeData repr a -> SomeData repr c) -> SomeData repr (a -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr a
y -> SomeData repr (a -> b -> c)
f SomeData repr (a -> b -> c)
-> SomeData repr a -> SomeData repr (b -> c)
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a
y SomeData repr (b -> c) -> SomeData repr b -> SomeData repr c
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr b
x)))
id :: SomeData repr (a -> a)
id = (SomeData repr a -> SomeData repr a) -> SomeData repr (a -> a)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (\SomeData repr a
x -> SomeData repr a
x)
data instance Data Anythingable repr a where
Anything :: repr a -> Data Anythingable repr a
instance
( Anythingable repr
) =>
Derivable (Data Anythingable repr) where
derive :: Data Anythingable repr a -> Derived (Data Anythingable repr) a
derive = \case
Anything x -> repr a -> repr a
forall (repr :: * -> *) a. Anythingable repr => repr a -> repr a
anything repr a
x
instance Anythingable (SomeData repr)
instance Anythingable (Data Anythingable repr)
data instance Data Bottomable repr a where
Bottom :: Data Bottomable repr a
instance Bottomable repr => Derivable (Data Bottomable repr) where
derive :: Data Bottomable repr a -> Derived (Data Bottomable repr) a
derive Bottom{} = Derived (Data Bottomable repr) a
forall (repr :: * -> *) a. Bottomable repr => repr a
bottom
data instance Data (Constantable c) repr a where
Constant :: c -> Data (Constantable c) repr c
instance Constantable c repr => Derivable (Data (Constantable c) repr) where
derive :: Data (Constantable c) repr a
-> Derived (Data (Constantable c) repr) a
derive = \case
Constant x -> c -> repr c
forall c (repr :: * -> *). Constantable c repr => c -> repr c
constant c
x
instance
( Constantable c repr
, Typeable c
) => Constantable c (SomeData repr) where
constant :: c -> SomeData repr c
constant c
c = Data (Constantable c) repr c -> SomeData repr c
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData (c -> Data (Constantable c) repr c
forall c (repr :: * -> *). c -> Data (Constantable c) repr c
Constant c
c)
instance Constantable c (Data (Constantable c) repr) where
constant :: c -> Data (Constantable c) repr c
constant = c -> Data (Constantable c) repr c
forall c (repr :: * -> *). c -> Data (Constantable c) repr c
Constant
data instance Data Eitherable repr a where
Left :: Data Eitherable repr (l -> Either l r)
Right :: Data Eitherable repr (r -> Either l r)
instance Eitherable repr => Derivable (Data Eitherable repr) where
derive :: Data Eitherable repr a -> Derived (Data Eitherable repr) a
derive = \case
Data Eitherable repr a
Left -> Derived (Data Eitherable repr) a
forall (repr :: * -> *) l r.
Eitherable repr =>
repr (l -> Either l r)
left
Data Eitherable repr a
Right -> Derived (Data Eitherable repr) a
forall (repr :: * -> *) r l.
Eitherable repr =>
repr (r -> Either l r)
right
instance
( Eitherable repr
) => Eitherable (SomeData repr) where
left :: SomeData repr (l -> Either l r)
left = Data Eitherable repr (l -> Either l r)
-> SomeData repr (l -> Either l r)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Eitherable repr (l -> Either l r)
forall (repr :: * -> *) l r. Data Eitherable repr (l -> Either l r)
Left
right :: SomeData repr (r -> Either l r)
right = Data Eitherable repr (r -> Either l r)
-> SomeData repr (r -> Either l r)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Eitherable repr (r -> Either l r)
forall (repr :: * -> *) r l. Data Eitherable repr (r -> Either l r)
Right
instance Eitherable (Data Eitherable repr) where
left :: Data Eitherable repr (l -> Either l r)
left = Data Eitherable repr (l -> Either l r)
forall (repr :: * -> *) l r. Data Eitherable repr (l -> Either l r)
Left
right :: Data Eitherable repr (r -> Either l r)
right = Data Eitherable repr (r -> Either l r)
forall (repr :: * -> *) r l. Data Eitherable repr (r -> Either l r)
Right
data instance Data Equalable repr a where
Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
instance Equalable repr => Derivable (Data Equalable repr) where
derive :: Data Equalable repr a -> Derived (Data Equalable repr) a
derive = \case
Data Equalable repr a
Equal -> Derived (Data Equalable repr) a
forall (repr :: * -> *) a.
(Equalable repr, Eq a) =>
repr (a -> a -> Bool)
equal
instance
( Equalable repr
) => Equalable (SomeData repr) where
equal :: SomeData repr (a -> a -> Bool)
equal = Data Equalable repr (a -> a -> Bool)
-> SomeData repr (a -> a -> Bool)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Equalable repr (a -> a -> Bool)
forall a (repr :: * -> *).
Eq a =>
Data Equalable repr (a -> a -> Bool)
Equal
instance Equalable (Data Equalable repr) where
equal :: Data Equalable repr (a -> a -> Bool)
equal = Data Equalable repr (a -> a -> Bool)
forall a (repr :: * -> *).
Eq a =>
Data Equalable repr (a -> a -> Bool)
Equal
data instance Data IfThenElseable repr a where
IfThenElse ::
SomeData repr Bool ->
SomeData repr a ->
SomeData repr a ->
Data IfThenElseable repr a
instance IfThenElseable repr => Derivable (Data IfThenElseable repr) where
derive :: Data IfThenElseable repr a -> Derived (Data IfThenElseable repr) a
derive = \case
IfThenElse test ok ko -> repr Bool -> repr a -> repr a -> repr a
forall (repr :: * -> *) a.
IfThenElseable repr =>
repr Bool -> repr a -> repr a -> repr a
ifThenElse (SomeData repr Bool -> Derived (SomeData repr) Bool
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive SomeData repr Bool
test) (SomeData repr a -> Derived (SomeData repr) a
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive SomeData repr a
ok) (SomeData repr a -> Derived (SomeData repr) a
forall (repr :: * -> *) a.
Derivable repr =>
repr a -> Derived repr a
derive SomeData repr a
ko)
instance
( IfThenElseable repr
) => IfThenElseable (SomeData repr) where
ifThenElse :: SomeData repr Bool
-> SomeData repr a -> SomeData repr a -> SomeData repr a
ifThenElse SomeData repr Bool
test SomeData repr a
ok SomeData repr a
ko = Data IfThenElseable repr a -> SomeData repr a
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData (SomeData repr Bool
-> SomeData repr a -> SomeData repr a -> Data IfThenElseable repr a
forall (repr :: * -> *) a.
SomeData repr Bool
-> SomeData repr a -> SomeData repr a -> Data IfThenElseable repr a
IfThenElse SomeData repr Bool
test SomeData repr a
ok SomeData repr a
ko)
instance IfThenElseable repr => IfThenElseable (Data IfThenElseable repr) where
ifThenElse :: Data IfThenElseable repr Bool
-> Data IfThenElseable repr a
-> Data IfThenElseable repr a
-> Data IfThenElseable repr a
ifThenElse Data IfThenElseable repr Bool
test Data IfThenElseable repr a
ok Data IfThenElseable repr a
ko = SomeData repr Bool
-> SomeData repr a -> SomeData repr a -> Data IfThenElseable repr a
forall (repr :: * -> *) a.
SomeData repr Bool
-> SomeData repr a -> SomeData repr a -> Data IfThenElseable repr a
IfThenElse (Data IfThenElseable repr Bool -> SomeData repr Bool
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data IfThenElseable repr Bool
test) (Data IfThenElseable repr a -> SomeData repr a
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data IfThenElseable repr a
ok) (Data IfThenElseable repr a -> SomeData repr a
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data IfThenElseable repr a
ko)
data instance Data Listable repr a where
Cons :: Data Listable repr (a -> [a] -> [a])
Nil :: Data Listable repr [a]
infixr 4 `Cons`
instance Listable repr => Derivable (Data Listable repr) where
derive :: Data Listable repr a -> Derived (Data Listable repr) a
derive = \case
Data Listable repr a
Cons -> Derived (Data Listable repr) a
forall (repr :: * -> *) a. Listable repr => repr (a -> [a] -> [a])
cons
Data Listable repr a
Nil -> Derived (Data Listable repr) a
forall (repr :: * -> *) a. Listable repr => repr [a]
nil
instance
( Listable repr
) => Listable (SomeData repr) where
cons :: SomeData repr (a -> [a] -> [a])
cons = Data Listable repr (a -> [a] -> [a])
-> SomeData repr (a -> [a] -> [a])
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Listable repr (a -> [a] -> [a])
forall (repr :: * -> *) a. Data Listable repr (a -> [a] -> [a])
Cons
nil :: SomeData repr [a]
nil = Data Listable repr [a] -> SomeData repr [a]
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Listable repr [a]
forall (repr :: * -> *) a. Data Listable repr [a]
Nil
instance Listable (Data Listable repr) where
cons :: Data Listable repr (a -> [a] -> [a])
cons = Data Listable repr (a -> [a] -> [a])
forall (repr :: * -> *) a. Data Listable repr (a -> [a] -> [a])
Cons
nil :: Data Listable repr [a]
nil = Data Listable repr [a]
forall (repr :: * -> *) a. Data Listable repr [a]
Nil
data instance Data Maybeable repr a where
Nothing :: Data Maybeable repr (Maybe a)
Just :: Data Maybeable repr (a -> Maybe a)
instance Maybeable repr => Derivable (Data Maybeable repr) where
derive :: Data Maybeable repr a -> Derived (Data Maybeable repr) a
derive = \case
Data Maybeable repr a
Nothing -> Derived (Data Maybeable repr) a
forall (repr :: * -> *) a. Maybeable repr => repr (Maybe a)
nothing
Data Maybeable repr a
Just -> Derived (Data Maybeable repr) a
forall (repr :: * -> *) a. Maybeable repr => repr (a -> Maybe a)
just
instance
( Maybeable repr
) => Maybeable (SomeData repr) where
nothing :: SomeData repr (Maybe a)
nothing = Data Maybeable repr (Maybe a) -> SomeData repr (Maybe a)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Maybeable repr (Maybe a)
forall (repr :: * -> *) a. Data Maybeable repr (Maybe a)
Nothing
just :: SomeData repr (a -> Maybe a)
just = Data Maybeable repr (a -> Maybe a) -> SomeData repr (a -> Maybe a)
forall (repr :: * -> *) a (able :: (* -> *) -> Constraint).
(Derivable (Data able repr), Typeable able) =>
Data able repr a -> SomeData repr a
SomeData Data Maybeable repr (a -> Maybe a)
forall (repr :: * -> *) a. Data Maybeable repr (a -> Maybe a)
Just
instance Maybeable (Data Maybeable repr) where
nothing :: Data Maybeable repr (Maybe a)
nothing = Data Maybeable repr (Maybe a)
forall (repr :: * -> *) a. Data Maybeable repr (Maybe a)
Nothing
just :: Data Maybeable repr (a -> Maybe a)
just = Data Maybeable repr (a -> Maybe a)
forall (repr :: * -> *) a. Data Maybeable repr (a -> Maybe a)
Just