{-# LANGUAGE CPP
, DataKinds
, PolyKinds
, GADTs
, TypeOperators
, TypeFamilies
, ExistentialQuantification
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.Datum
(
Datum(..), datumHint, datumType
, DatumCode(..)
, DatumStruct(..)
, DatumFun(..)
, dTrue, dFalse, dBool
, dUnit
, dPair
, dLeft, dRight
, dNil, dCons
, dNothing, dJust
, dPair_
, dLeft_, dRight_
, dNil_, dCons_
, dNothing_, dJust_
, Branch(..)
, Pattern(..)
, PDatumCode(..)
, PDatumStruct(..)
, PDatumFun(..)
, pTrue, pFalse
, pUnit
, pPair
, pLeft, pRight
, pNil, pCons
, pNothing, pJust
, GBranch(..)
) where
import qualified Data.Text as Text
import Data.Text (Text)
#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..))
import Control.Applicative
#endif
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Syntax.Variable (Variable(..))
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
#if __PARTIAL_DATUM_JMEQ__
cannotProve :: String -> a
cannotProve fun =
error $ "Language.Hakaru.Syntax.Datum." ++ fun ++ ": Cannot prove Refl because of phantomness"
#endif
data Datum :: (Hakaru -> *) -> Hakaru -> * where
Datum
:: {-# UNPACK #-} !Text
-> !(Sing (HData' t))
-> !(DatumCode (Code t) ast (HData' t))
-> Datum ast (HData' t)
datumHint :: Datum ast (HData' t) -> Text
datumHint :: Datum ast (HData' t) -> Text
datumHint (Datum Text
hint Sing (HData' t)
_ DatumCode (Code t) ast (HData' t)
_) = Text
hint
datumType :: Datum ast (HData' t) -> Sing (HData' t)
datumType :: Datum ast (HData' t) -> Sing (HData' t)
datumType (Datum Text
_ Sing (HData' t)
typ DatumCode (Code t) ast (HData' t)
_) = Sing (HData' t)
Sing (HData' t)
typ
instance Eq1 ast => JmEq1 (Datum ast) where
jmEq1 :: Datum ast i -> Datum ast j -> Maybe (TypeEq i j)
jmEq1 (Datum Text
_ Sing (HData' t)
typ1 DatumCode (Code t) ast (HData' t)
d1) (Datum Text
_ Sing (HData' t)
typ2 DatumCode (Code t) ast (HData' t)
d2) =
case Sing (HData' t)
-> Sing (HData' t) -> Maybe (TypeEq (HData' t) (HData' t))
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing (HData' t)
typ1 Sing (HData' t)
typ2 of
Just proof :: TypeEq (HData' t) (HData' t)
proof@TypeEq (HData' t) (HData' t)
Refl
| DatumCode (Code t) ast (HData' t)
-> DatumCode (Code t) ast (HData' t) -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumCode (Code t) ast (HData' t)
d1 DatumCode (Code t) ast (HData' t)
DatumCode (Code t) ast (HData' t)
d2 -> TypeEq (HData' t) (HData' t)
-> Maybe (TypeEq (HData' t) (HData' t))
forall a. a -> Maybe a
Just TypeEq (HData' t) (HData' t)
proof
Maybe (TypeEq (HData' t) (HData' t))
_ -> Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Eq1 ast => Eq1 (Datum ast) where
eq1 :: Datum ast i -> Datum ast i -> Bool
eq1 (Datum Text
_ Sing (HData' t)
_ DatumCode (Code t) ast (HData' t)
d1) (Datum Text
_ Sing (HData' t)
_ DatumCode (Code t) ast (HData' t)
d2) = DatumCode (Code t) ast (HData' t)
-> DatumCode (Code t) ast (HData' t) -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumCode (Code t) ast (HData' t)
d1 DatumCode (Code t) ast (HData' t)
DatumCode (Code t) ast (HData' t)
d2
instance Eq1 ast => Eq (Datum ast a) where
== :: Datum ast a -> Datum ast a -> Bool
(==) = Datum ast a -> Datum ast a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show1 ast => Show1 (Datum ast) where
showsPrec1 :: Int -> Datum ast i -> ShowS
showsPrec1 Int
p (Datum Text
hint Sing (HData' t)
typ DatumCode (Code t) ast (HData' t)
d) =
Int
-> String
-> Text
-> Sing (HData' t)
-> DatumCode (Code t) ast (HData' t)
-> ShowS
forall k1 k2 a (b :: k1 -> *) (c :: k2 -> *) (i :: k1) (j :: k2).
(Show a, Show1 b, Show1 c) =>
Int -> String -> a -> b i -> c j -> ShowS
showParen_011 Int
p String
"Datum" Text
hint Sing (HData' t)
typ DatumCode (Code t) ast (HData' t)
d
instance Show1 ast => Show (Datum ast a) where
showsPrec :: Int -> Datum ast a -> ShowS
showsPrec = Int -> Datum ast a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Datum ast a -> String
show = Datum ast a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor11 Datum where
fmap11 :: (forall (i :: Hakaru). a i -> b i) -> Datum a j -> Datum b j
fmap11 forall (i :: Hakaru). a i -> b i
f (Datum Text
hint Sing (HData' t)
typ DatumCode (Code t) a (HData' t)
d) = Text
-> Sing (HData' t)
-> DatumCode (Code t) b (HData' t)
-> Datum b (HData' t)
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
hint Sing (HData' t)
typ ((forall (i :: Hakaru). a i -> b i)
-> DatumCode (Code t) a (HData' t)
-> DatumCode (Code t) b (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). a i -> b i
f DatumCode (Code t) a (HData' t)
d)
instance Foldable11 Datum where
foldMap11 :: (forall (i :: Hakaru). a i -> m) -> Datum a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f (Datum Text
_ Sing (HData' t)
_ DatumCode (Code t) a (HData' t)
d) = (forall (i :: Hakaru). a i -> m)
-> DatumCode (Code t) a (HData' t) -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f DatumCode (Code t) a (HData' t)
d
instance Traversable11 Datum where
traverse11 :: (forall (i :: Hakaru). a i -> f (b i))
-> Datum a j -> f (Datum b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Datum Text
hint Sing (HData' t)
typ DatumCode (Code t) a (HData' t)
d) = Text
-> Sing (HData' t)
-> DatumCode (Code t) b (HData' t)
-> Datum b (HData' t)
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
hint Sing (HData' t)
typ (DatumCode (Code t) b (HData' t) -> Datum b j)
-> f (DatumCode (Code t) b (HData' t)) -> f (Datum b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a i -> f (b i))
-> DatumCode (Code t) a (HData' t)
-> f (DatumCode (Code t) b (HData' t))
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f DatumCode (Code t) a (HData' t)
d
infixr 7 `Et`, `PEt`
data DatumCode :: [[HakaruFun]] -> (Hakaru -> *) -> Hakaru -> * where
Inr :: !(DatumCode xss abt a) -> DatumCode (xs ': xss) abt a
Inl :: !(DatumStruct xs abt a) -> DatumCode (xs ': xss) abt a
#if __PARTIAL_DATUM_JMEQ__
instance JmEq1 ast => JmEq1 (DatumCode xss ast) where
jmEq1 (Inr c) (Inr d) = jmEq1 c d
jmEq1 (Inl c) (Inl d) = jmEq1 c d
jmEq1 _ _ = Nothing
#endif
instance Eq1 ast => Eq1 (DatumCode xss ast) where
eq1 :: DatumCode xss ast i -> DatumCode xss ast i -> Bool
eq1 (Inr DatumCode xss ast i
c) (Inr DatumCode xss ast i
d) = DatumCode xss ast i -> DatumCode xss ast i -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumCode xss ast i
c DatumCode xss ast i
DatumCode xss ast i
d
eq1 (Inl DatumStruct xs ast i
c) (Inl DatumStruct xs ast i
d) = DatumStruct xs ast i -> DatumStruct xs ast i -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumStruct xs ast i
c DatumStruct xs ast i
DatumStruct xs ast i
d
eq1 DatumCode xss ast i
_ DatumCode xss ast i
_ = Bool
False
instance Eq1 ast => Eq (DatumCode xss ast a) where
== :: DatumCode xss ast a -> DatumCode xss ast a -> Bool
(==) = DatumCode xss ast a -> DatumCode xss ast a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show1 ast => Show1 (DatumCode xss ast) where
showsPrec1 :: Int -> DatumCode xss ast i -> ShowS
showsPrec1 Int
p (Inr DatumCode xss ast i
d) = Int -> String -> DatumCode xss ast i -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Inr" DatumCode xss ast i
d
showsPrec1 Int
p (Inl DatumStruct xs ast i
d) = Int -> String -> DatumStruct xs ast i -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Inl" DatumStruct xs ast i
d
instance Show1 ast => Show (DatumCode xss ast a) where
showsPrec :: Int -> DatumCode xss ast a -> ShowS
showsPrec = Int -> DatumCode xss ast a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: DatumCode xss ast a -> String
show = DatumCode xss ast a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor11 (DatumCode xss) where
fmap11 :: (forall (i :: Hakaru). a i -> b i)
-> DatumCode xss a j -> DatumCode xss b j
fmap11 forall (i :: Hakaru). a i -> b i
f (Inr DatumCode xss a j
d) = DatumCode xss b j -> DatumCode (xs : xss) b j
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr ((forall (i :: Hakaru). a i -> b i)
-> DatumCode xss a j -> DatumCode xss b j
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). a i -> b i
f DatumCode xss a j
d)
fmap11 forall (i :: Hakaru). a i -> b i
f (Inl DatumStruct xs a j
d) = DatumStruct xs b j -> DatumCode (xs : xss) b j
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl ((forall (i :: Hakaru). a i -> b i)
-> DatumStruct xs a j -> DatumStruct xs b j
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). a i -> b i
f DatumStruct xs a j
d)
instance Foldable11 (DatumCode xss) where
foldMap11 :: (forall (i :: Hakaru). a i -> m) -> DatumCode xss a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f (Inr DatumCode xss a j
d) = (forall (i :: Hakaru). a i -> m) -> DatumCode xss a j -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f DatumCode xss a j
d
foldMap11 forall (i :: Hakaru). a i -> m
f (Inl DatumStruct xs a j
d) = (forall (i :: Hakaru). a i -> m) -> DatumStruct xs a j -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f DatumStruct xs a j
d
instance Traversable11 (DatumCode xss) where
traverse11 :: (forall (i :: Hakaru). a i -> f (b i))
-> DatumCode xss a j -> f (DatumCode xss b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Inr DatumCode xss a j
d) = DatumCode xss b j -> DatumCode (xs : xss) b j
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr (DatumCode xss b j -> DatumCode (xs : xss) b j)
-> f (DatumCode xss b j) -> f (DatumCode (xs : xss) b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a i -> f (b i))
-> DatumCode xss a j -> f (DatumCode xss b j)
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f DatumCode xss a j
d
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Inl DatumStruct xs a j
d) = DatumStruct xs b j -> DatumCode (xs : xss) b j
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct xs b j -> DatumCode (xs : xss) b j)
-> f (DatumStruct xs b j) -> f (DatumCode (xs : xss) b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a i -> f (b i))
-> DatumStruct xs a j -> f (DatumStruct xs b j)
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f DatumStruct xs a j
d
data DatumStruct :: [HakaruFun] -> (Hakaru -> *) -> Hakaru -> * where
Et :: !(DatumFun x abt a)
-> !(DatumStruct xs abt a)
-> DatumStruct (x ': xs) abt a
Done :: DatumStruct '[] abt a
#if __PARTIAL_DATUM_JMEQ__
instance JmEq1 ast => JmEq1 (DatumStruct xs ast) where
jmEq1 (Et c1 Done) (Et d1 Done) = jmEq1 c1 d1
jmEq1 (Et c1 c2) (Et d1 d2) = do
Refl <- jmEq1 c1 d1
Refl <- jmEq1 c2 d2
Just Refl
jmEq1 Done Done = Just (cannotProve "jmEq1@DatumStruct{Done}")
jmEq1 _ _ = Nothing
#endif
instance Eq1 ast => Eq1 (DatumStruct xs ast) where
eq1 :: DatumStruct xs ast i -> DatumStruct xs ast i -> Bool
eq1 (Et DatumFun x ast i
c1 DatumStruct xs ast i
c2) (Et DatumFun x ast i
d1 DatumStruct xs ast i
d2) = DatumFun x ast i -> DatumFun x ast i -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumFun x ast i
c1 DatumFun x ast i
DatumFun x ast i
d1 Bool -> Bool -> Bool
&& DatumStruct xs ast i -> DatumStruct xs ast i -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 DatumStruct xs ast i
c2 DatumStruct xs ast i
DatumStruct xs ast i
d2
eq1 DatumStruct xs ast i
Done DatumStruct xs ast i
Done = Bool
True
instance Eq1 ast => Eq (DatumStruct xs ast a) where
== :: DatumStruct xs ast a -> DatumStruct xs ast a -> Bool
(==) = DatumStruct xs ast a -> DatumStruct xs ast a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show1 ast => Show1 (DatumStruct xs ast) where
showsPrec1 :: Int -> DatumStruct xs ast i -> ShowS
showsPrec1 Int
p (Et DatumFun x ast i
d1 DatumStruct xs ast i
d2) = Int -> String -> DatumFun x ast i -> DatumStruct xs ast i -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"Et" DatumFun x ast i
d1 DatumStruct xs ast i
d2
showsPrec1 Int
_ DatumStruct xs ast i
Done = String -> ShowS
showString String
"Done"
instance Show1 ast => Show (DatumStruct xs ast a) where
showsPrec :: Int -> DatumStruct xs ast a -> ShowS
showsPrec = Int -> DatumStruct xs ast a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: DatumStruct xs ast a -> String
show = DatumStruct xs ast a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor11 (DatumStruct xs) where
fmap11 :: (forall (i :: Hakaru). a i -> b i)
-> DatumStruct xs a j -> DatumStruct xs b j
fmap11 forall (i :: Hakaru). a i -> b i
f (Et DatumFun x a j
d1 DatumStruct xs a j
d2) = DatumFun x b j -> DatumStruct xs b j -> DatumStruct (x : xs) b j
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
Et ((forall (i :: Hakaru). a i -> b i)
-> DatumFun x a j -> DatumFun x b j
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). a i -> b i
f DatumFun x a j
d1) ((forall (i :: Hakaru). a i -> b i)
-> DatumStruct xs a j -> DatumStruct xs b j
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). a i -> b i
f DatumStruct xs a j
d2)
fmap11 forall (i :: Hakaru). a i -> b i
_ DatumStruct xs a j
Done = DatumStruct xs b j
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
instance Foldable11 (DatumStruct xs) where
foldMap11 :: (forall (i :: Hakaru). a i -> m) -> DatumStruct xs a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f (Et DatumFun x a j
d1 DatumStruct xs a j
d2) = (forall (i :: Hakaru). a i -> m) -> DatumFun x a j -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f DatumFun x a j
d1 m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (forall (i :: Hakaru). a i -> m) -> DatumStruct xs a j -> m
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
(j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f DatumStruct xs a j
d2
foldMap11 forall (i :: Hakaru). a i -> m
_ DatumStruct xs a j
Done = m
forall a. Monoid a => a
mempty
instance Traversable11 (DatumStruct xs) where
traverse11 :: (forall (i :: Hakaru). a i -> f (b i))
-> DatumStruct xs a j -> f (DatumStruct xs b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Et DatumFun x a j
d1 DatumStruct xs a j
d2) = DatumFun x b j -> DatumStruct xs b j -> DatumStruct (x : xs) b j
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
Et (DatumFun x b j -> DatumStruct xs b j -> DatumStruct (x : xs) b j)
-> f (DatumFun x b j)
-> f (DatumStruct xs b j -> DatumStruct (x : xs) b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: Hakaru). a i -> f (b i))
-> DatumFun x a j -> f (DatumFun x b j)
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f DatumFun x a j
d1 f (DatumStruct xs b j -> DatumStruct (x : xs) b j)
-> f (DatumStruct xs b j) -> f (DatumStruct (x : xs) b j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (i :: Hakaru). a i -> f (b i))
-> DatumStruct xs a j -> f (DatumStruct xs b j)
forall k1 k2 (t :: (k1 -> *) -> k2 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2).
(Traversable11 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j -> f (t b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f DatumStruct xs a j
d2
traverse11 forall (i :: Hakaru). a i -> f (b i)
_ DatumStruct xs a j
Done = DatumStruct '[] b j -> f (DatumStruct '[] b j)
forall (f :: * -> *) a. Applicative f => a -> f a
pure DatumStruct '[] b j
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
data DatumFun :: HakaruFun -> (Hakaru -> *) -> Hakaru -> * where
Konst :: !(ast b) -> DatumFun ('K b) ast a
Ident :: !(ast a) -> DatumFun 'I ast a
#if __PARTIAL_DATUM_JMEQ__
instance JmEq1 ast => JmEq1 (DatumFun x ast) where
jmEq1 (Konst e) (Konst f) = do
Refl <- jmEq1 e f
Just (cannotProve "jmEq1@DatumFun{Konst}")
jmEq1 (Ident e) (Ident f) = jmEq1 e f
jmEq1 _ _ = Nothing
#endif
instance Eq1 ast => Eq1 (DatumFun x ast) where
eq1 :: DatumFun x ast i -> DatumFun x ast i -> Bool
eq1 (Konst ast b
e) (Konst ast b
f) = ast b -> ast b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 ast b
e ast b
ast b
f
eq1 (Ident ast i
e) (Ident ast i
f) = ast i -> ast i -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1 ast i
e ast i
f
instance Eq1 ast => Eq (DatumFun x ast a) where
== :: DatumFun x ast a -> DatumFun x ast a -> Bool
(==) = DatumFun x ast a -> DatumFun x ast a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show1 ast => Show1 (DatumFun x ast) where
showsPrec1 :: Int -> DatumFun x ast i -> ShowS
showsPrec1 Int
p (Konst ast b
e) = Int -> String -> ast b -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Konst" ast b
e
showsPrec1 Int
p (Ident ast i
e) = Int -> String -> ast i -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Ident" ast i
e
instance Show1 ast => Show (DatumFun x ast a) where
showsPrec :: Int -> DatumFun x ast a -> ShowS
showsPrec = Int -> DatumFun x ast a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: DatumFun x ast a -> String
show = DatumFun x ast a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor11 (DatumFun x) where
fmap11 :: (forall (i :: Hakaru). a i -> b i)
-> DatumFun x a j -> DatumFun x b j
fmap11 forall (i :: Hakaru). a i -> b i
f (Konst a b
e) = b b -> DatumFun ('K b) b j
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst (a b -> b b
forall (i :: Hakaru). a i -> b i
f a b
e)
fmap11 forall (i :: Hakaru). a i -> b i
f (Ident a j
e) = b j -> DatumFun 'I b j
forall (ast :: Hakaru -> *) (a :: Hakaru).
ast a -> DatumFun 'I ast a
Ident (a j -> b j
forall (i :: Hakaru). a i -> b i
f a j
e)
instance Foldable11 (DatumFun x) where
foldMap11 :: (forall (i :: Hakaru). a i -> m) -> DatumFun x a j -> m
foldMap11 forall (i :: Hakaru). a i -> m
f (Konst a b
e) = a b -> m
forall (i :: Hakaru). a i -> m
f a b
e
foldMap11 forall (i :: Hakaru). a i -> m
f (Ident a j
e) = a j -> m
forall (i :: Hakaru). a i -> m
f a j
e
instance Traversable11 (DatumFun x) where
traverse11 :: (forall (i :: Hakaru). a i -> f (b i))
-> DatumFun x a j -> f (DatumFun x b j)
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Konst a b
e) = b b -> DatumFun ('K b) b j
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst (b b -> DatumFun ('K b) b j) -> f (b b) -> f (DatumFun ('K b) b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a b -> f (b b)
forall (i :: Hakaru). a i -> f (b i)
f a b
e
traverse11 forall (i :: Hakaru). a i -> f (b i)
f (Ident a j
e) = b j -> DatumFun 'I b j
forall (ast :: Hakaru -> *) (a :: Hakaru).
ast a -> DatumFun 'I ast a
Ident (b j -> DatumFun 'I b j) -> f (b j) -> f (DatumFun 'I b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a j -> f (b j)
forall (i :: Hakaru). a i -> f (b i)
f a j
e
dTrue, dFalse :: Datum ast HBool
dTrue :: Datum ast HBool
dTrue = Text
-> Sing (HData' ('TyCon "Bool"))
-> DatumCode (Code ('TyCon "Bool")) ast (HData' ('TyCon "Bool"))
-> Datum ast (HData' ('TyCon "Bool"))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdTrue Sing HBool
Sing (HData' ('TyCon "Bool"))
sBool (DatumCode '[ '[], '[]] ast HBool -> Datum ast HBool)
-> (DatumStruct '[] ast HBool -> DatumCode '[ '[], '[]] ast HBool)
-> DatumStruct '[] ast HBool
-> Datum ast HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[] ast HBool -> DatumCode '[ '[], '[]] ast HBool
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[] ast HBool -> Datum ast HBool)
-> DatumStruct '[] ast HBool -> Datum ast HBool
forall a b. (a -> b) -> a -> b
$ DatumStruct '[] ast HBool
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dFalse :: Datum ast HBool
dFalse = Text
-> Sing (HData' ('TyCon "Bool"))
-> DatumCode (Code ('TyCon "Bool")) ast (HData' ('TyCon "Bool"))
-> Datum ast (HData' ('TyCon "Bool"))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdFalse Sing HBool
Sing (HData' ('TyCon "Bool"))
sBool (DatumCode '[ '[], '[]] ast HBool -> Datum ast HBool)
-> (DatumStruct '[] ast HBool -> DatumCode '[ '[], '[]] ast HBool)
-> DatumStruct '[] ast HBool
-> Datum ast HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumCode '[ '[]] ast HBool -> DatumCode '[ '[], '[]] ast HBool
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr (DatumCode '[ '[]] ast HBool -> DatumCode '[ '[], '[]] ast HBool)
-> (DatumStruct '[] ast HBool -> DatumCode '[ '[]] ast HBool)
-> DatumStruct '[] ast HBool
-> DatumCode '[ '[], '[]] ast HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[] ast HBool -> DatumCode '[ '[]] ast HBool
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[] ast HBool -> Datum ast HBool)
-> DatumStruct '[] ast HBool -> Datum ast HBool
forall a b. (a -> b) -> a -> b
$ DatumStruct '[] ast HBool
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dBool :: Bool -> Datum ast HBool
dBool :: Bool -> Datum ast HBool
dBool Bool
b = if Bool
b then Datum ast HBool
forall (ast :: Hakaru -> *). Datum ast HBool
dTrue else Datum ast HBool
forall (ast :: Hakaru -> *). Datum ast HBool
dFalse
dUnit :: Datum ast HUnit
dUnit :: Datum ast HUnit
dUnit = Text
-> Sing (HData' ('TyCon "Unit"))
-> DatumCode (Code ('TyCon "Unit")) ast (HData' ('TyCon "Unit"))
-> Datum ast (HData' ('TyCon "Unit"))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdUnit Sing HUnit
Sing (HData' ('TyCon "Unit"))
sUnit (DatumCode '[ '[]] ast HUnit -> Datum ast HUnit)
-> (DatumStruct '[] ast HUnit -> DatumCode '[ '[]] ast HUnit)
-> DatumStruct '[] ast HUnit
-> Datum ast HUnit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[] ast HUnit -> DatumCode '[ '[]] ast HUnit
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[] ast HUnit -> Datum ast HUnit)
-> DatumStruct '[] ast HUnit -> Datum ast HUnit
forall a b. (a -> b) -> a -> b
$ DatumStruct '[] ast HUnit
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dPair :: (SingI a, SingI b) => ast a -> ast b -> Datum ast (HPair a b)
dPair :: ast a -> ast b -> Datum ast (HPair a b)
dPair = Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b)
forall (a :: Hakaru) (b :: Hakaru) (ast :: Hakaru -> *).
Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b)
dPair_ Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
dPair_ :: Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b)
dPair_ :: Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b)
dPair_ Sing a
a Sing b
b ast a
x ast b
y =
Text
-> Sing (HData' (('TyCon "Pair" ':@ a) ':@ b))
-> DatumCode
(Code (('TyCon "Pair" ':@ a) ':@ b))
ast
(HData' (('TyCon "Pair" ':@ a) ':@ b))
-> Datum ast (HData' (('TyCon "Pair" ':@ a) ':@ b))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdPair (Sing a -> Sing b -> Sing (HPair a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HPair a b)
sPair Sing a
a Sing b
b) (DatumCode '[ '[ 'K a, 'K b]] ast (HPair a b)
-> Datum ast (HPair a b))
-> (DatumStruct '[ 'K a, 'K b] ast (HPair a b)
-> DatumCode '[ '[ 'K a, 'K b]] ast (HPair a b))
-> DatumStruct '[ 'K a, 'K b] ast (HPair a b)
-> Datum ast (HPair a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[ 'K a, 'K b] ast (HPair a b)
-> DatumCode '[ '[ 'K a, 'K b]] ast (HPair a b)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[ 'K a, 'K b] ast (HPair a b)
-> Datum ast (HPair a b))
-> DatumStruct '[ 'K a, 'K b] ast (HPair a b)
-> Datum ast (HPair a b)
forall a b. (a -> b) -> a -> b
$ ast a -> DatumFun ('K a) ast (HPair a b)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst ast a
x DatumFun ('K a) ast (HPair a b)
-> DatumStruct '[ 'K b] ast (HPair a b)
-> DatumStruct '[ 'K a, 'K b] ast (HPair a b)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` ast b -> DatumFun ('K b) ast (HPair a b)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst ast b
y DatumFun ('K b) ast (HPair a b)
-> DatumStruct '[] ast (HPair a b)
-> DatumStruct '[ 'K b] ast (HPair a b)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` DatumStruct '[] ast (HPair a b)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dLeft :: (SingI a, SingI b) => ast a -> Datum ast (HEither a b)
dLeft :: ast a -> Datum ast (HEither a b)
dLeft = Sing a -> Sing b -> ast a -> Datum ast (HEither a b)
forall (a :: Hakaru) (b :: Hakaru) (ast :: Hakaru -> *).
Sing a -> Sing b -> ast a -> Datum ast (HEither a b)
dLeft_ Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
dLeft_ :: Sing a -> Sing b -> ast a -> Datum ast (HEither a b)
dLeft_ :: Sing a -> Sing b -> ast a -> Datum ast (HEither a b)
dLeft_ Sing a
a Sing b
b =
Text
-> Sing (HData' (('TyCon "Either" ':@ a) ':@ b))
-> DatumCode
(Code (('TyCon "Either" ':@ a) ':@ b))
ast
(HData' (('TyCon "Either" ':@ a) ':@ b))
-> Datum ast (HData' (('TyCon "Either" ':@ a) ':@ b))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdLeft (Sing a -> Sing b -> Sing (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HEither a b)
sEither Sing a
a Sing b
b) (DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
-> Datum ast (HEither a b))
-> (ast a -> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b))
-> ast a
-> Datum ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[ 'K a] ast (HEither a b)
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[ 'K a] ast (HEither a b)
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b))
-> (ast a -> DatumStruct '[ 'K a] ast (HEither a b))
-> ast a
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatumFun ('K a) ast (HEither a b)
-> DatumStruct '[] ast (HEither a b)
-> DatumStruct '[ 'K a] ast (HEither a b)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` DatumStruct '[] ast (HEither a b)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done) (DatumFun ('K a) ast (HEither a b)
-> DatumStruct '[ 'K a] ast (HEither a b))
-> (ast a -> DatumFun ('K a) ast (HEither a b))
-> ast a
-> DatumStruct '[ 'K a] ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ast a -> DatumFun ('K a) ast (HEither a b)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst
dRight :: (SingI a, SingI b) => ast b -> Datum ast (HEither a b)
dRight :: ast b -> Datum ast (HEither a b)
dRight = Sing a -> Sing b -> ast b -> Datum ast (HEither a b)
forall (a :: Hakaru) (b :: Hakaru) (ast :: Hakaru -> *).
Sing a -> Sing b -> ast b -> Datum ast (HEither a b)
dRight_ Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
dRight_ :: Sing a -> Sing b -> ast b -> Datum ast (HEither a b)
dRight_ :: Sing a -> Sing b -> ast b -> Datum ast (HEither a b)
dRight_ Sing a
a Sing b
b =
Text
-> Sing (HData' (('TyCon "Either" ':@ a) ':@ b))
-> DatumCode
(Code (('TyCon "Either" ':@ a) ':@ b))
ast
(HData' (('TyCon "Either" ':@ a) ':@ b))
-> Datum ast (HData' (('TyCon "Either" ':@ a) ':@ b))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdRight (Sing a -> Sing b -> Sing (HEither a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (HEither a b)
sEither Sing a
a Sing b
b) (DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
-> Datum ast (HEither a b))
-> (ast b -> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b))
-> ast b
-> Datum ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumCode '[ '[ 'K b]] ast (HEither a b)
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr (DatumCode '[ '[ 'K b]] ast (HEither a b)
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b))
-> (ast b -> DatumCode '[ '[ 'K b]] ast (HEither a b))
-> ast b
-> DatumCode '[ '[ 'K a], '[ 'K b]] ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[ 'K b] ast (HEither a b)
-> DatumCode '[ '[ 'K b]] ast (HEither a b)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[ 'K b] ast (HEither a b)
-> DatumCode '[ '[ 'K b]] ast (HEither a b))
-> (ast b -> DatumStruct '[ 'K b] ast (HEither a b))
-> ast b
-> DatumCode '[ '[ 'K b]] ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatumFun ('K b) ast (HEither a b)
-> DatumStruct '[] ast (HEither a b)
-> DatumStruct '[ 'K b] ast (HEither a b)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` DatumStruct '[] ast (HEither a b)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done) (DatumFun ('K b) ast (HEither a b)
-> DatumStruct '[ 'K b] ast (HEither a b))
-> (ast b -> DatumFun ('K b) ast (HEither a b))
-> ast b
-> DatumStruct '[ 'K b] ast (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ast b -> DatumFun ('K b) ast (HEither a b)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst
dNil :: (SingI a) => Datum ast (HList a)
dNil :: Datum ast (HList a)
dNil = Sing a -> Datum ast (HList a)
forall (a :: Hakaru) (ast :: Hakaru -> *).
Sing a -> Datum ast (HList a)
dNil_ Sing a
forall k (a :: k). SingI a => Sing a
sing
dNil_ :: Sing a -> Datum ast (HList a)
dNil_ :: Sing a -> Datum ast (HList a)
dNil_ Sing a
a = Text
-> Sing (HData' ('TyCon "List" ':@ a))
-> DatumCode
(Code ('TyCon "List" ':@ a)) ast (HData' ('TyCon "List" ':@ a))
-> Datum ast (HData' ('TyCon "List" ':@ a))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdNil (Sing a -> Sing (HList a)
forall (a :: Hakaru). Sing a -> Sing (HList a)
sList Sing a
a) (DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a)
-> Datum ast (HList a))
-> (DatumStruct '[] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a))
-> DatumStruct '[] ast (HList a)
-> Datum ast (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[] ast (HList a) -> Datum ast (HList a))
-> DatumStruct '[] ast (HList a) -> Datum ast (HList a)
forall a b. (a -> b) -> a -> b
$ DatumStruct '[] ast (HList a)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dCons :: (SingI a) => ast a -> ast (HList a) -> Datum ast (HList a)
dCons :: ast a -> ast (HList a) -> Datum ast (HList a)
dCons = Sing a -> ast a -> ast (HList a) -> Datum ast (HList a)
forall (a :: Hakaru) (ast :: Hakaru -> *).
Sing a -> ast a -> ast (HList a) -> Datum ast (HList a)
dCons_ Sing a
forall k (a :: k). SingI a => Sing a
sing
dCons_ :: Sing a -> ast a -> ast (HList a) -> Datum ast (HList a)
dCons_ :: Sing a -> ast a -> ast (HList a) -> Datum ast (HList a)
dCons_ Sing a
a ast a
x ast (HList a)
xs =
Text
-> Sing (HData' ('TyCon "List" ':@ a))
-> DatumCode
(Code ('TyCon "List" ':@ a)) ast (HData' ('TyCon "List" ':@ a))
-> Datum ast (HData' ('TyCon "List" ':@ a))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdCons (Sing a -> Sing (HList a)
forall (a :: Hakaru). Sing a -> Sing (HList a)
sList Sing a
a) (DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a)
-> Datum ast (HList a))
-> (DatumStruct '[ 'K a, 'I] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a))
-> DatumStruct '[ 'K a, 'I] ast (HList a)
-> Datum ast (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumCode '[ '[ 'K a, 'I]] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a)
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr (DatumCode '[ '[ 'K a, 'I]] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a))
-> (DatumStruct '[ 'K a, 'I] ast (HList a)
-> DatumCode '[ '[ 'K a, 'I]] ast (HList a))
-> DatumStruct '[ 'K a, 'I] ast (HList a)
-> DatumCode '[ '[], '[ 'K a, 'I]] ast (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[ 'K a, 'I] ast (HList a)
-> DatumCode '[ '[ 'K a, 'I]] ast (HList a)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[ 'K a, 'I] ast (HList a) -> Datum ast (HList a))
-> DatumStruct '[ 'K a, 'I] ast (HList a) -> Datum ast (HList a)
forall a b. (a -> b) -> a -> b
$ ast a -> DatumFun ('K a) ast (HList a)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst ast a
x DatumFun ('K a) ast (HList a)
-> DatumStruct '[ 'I] ast (HList a)
-> DatumStruct '[ 'K a, 'I] ast (HList a)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` ast (HList a) -> DatumFun 'I ast (HList a)
forall (ast :: Hakaru -> *) (a :: Hakaru).
ast a -> DatumFun 'I ast a
Ident ast (HList a)
xs DatumFun 'I ast (HList a)
-> DatumStruct '[] ast (HList a)
-> DatumStruct '[ 'I] ast (HList a)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` DatumStruct '[] ast (HList a)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dNothing :: (SingI a) => Datum ast (HMaybe a)
dNothing :: Datum ast (HMaybe a)
dNothing = Sing a -> Datum ast (HMaybe a)
forall (a :: Hakaru) (ast :: Hakaru -> *).
Sing a -> Datum ast (HMaybe a)
dNothing_ Sing a
forall k (a :: k). SingI a => Sing a
sing
dNothing_ :: Sing a -> Datum ast (HMaybe a)
dNothing_ :: Sing a -> Datum ast (HMaybe a)
dNothing_ Sing a
a = Text
-> Sing (HData' ('TyCon "Maybe" ':@ a))
-> DatumCode
(Code ('TyCon "Maybe" ':@ a)) ast (HData' ('TyCon "Maybe" ':@ a))
-> Datum ast (HData' ('TyCon "Maybe" ':@ a))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdNothing (Sing a -> Sing (HMaybe a)
forall (a :: Hakaru). Sing a -> Sing (HMaybe a)
sMaybe Sing a
a) (DatumCode
(Code ('TyCon "Maybe" ':@ a)) ast (HData' ('TyCon "Maybe" ':@ a))
-> Datum ast (HData' ('TyCon "Maybe" ':@ a)))
-> DatumCode
(Code ('TyCon "Maybe" ':@ a)) ast (HData' ('TyCon "Maybe" ':@ a))
-> Datum ast (HData' ('TyCon "Maybe" ':@ a))
forall a b. (a -> b) -> a -> b
$ DatumStruct '[] ast (HMaybe a)
-> DatumCode '[ '[], '[ 'K a]] ast (HMaybe a)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl DatumStruct '[] ast (HMaybe a)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done
dJust :: (SingI a) => ast a -> Datum ast (HMaybe a)
dJust :: ast a -> Datum ast (HMaybe a)
dJust = Sing a -> ast a -> Datum ast (HMaybe a)
forall (a :: Hakaru) (ast :: Hakaru -> *).
Sing a -> ast a -> Datum ast (HMaybe a)
dJust_ Sing a
forall k (a :: k). SingI a => Sing a
sing
dJust_ :: Sing a -> ast a -> Datum ast (HMaybe a)
dJust_ :: Sing a -> ast a -> Datum ast (HMaybe a)
dJust_ Sing a
a = Text
-> Sing (HData' ('TyCon "Maybe" ':@ a))
-> DatumCode
(Code ('TyCon "Maybe" ':@ a)) ast (HData' ('TyCon "Maybe" ':@ a))
-> Datum ast (HData' ('TyCon "Maybe" ':@ a))
forall (xss :: HakaruCon) (ast :: Hakaru -> *).
Text
-> Sing (HData' xss)
-> DatumCode (Code xss) ast (HData' xss)
-> Datum ast (HData' xss)
Datum Text
tdJust (Sing a -> Sing (HMaybe a)
forall (a :: Hakaru). Sing a -> Sing (HMaybe a)
sMaybe Sing a
a) (DatumCode '[ '[], '[ 'K a]] ast (HMaybe a)
-> Datum ast (HMaybe a))
-> (ast a -> DatumCode '[ '[], '[ 'K a]] ast (HMaybe a))
-> ast a
-> Datum ast (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumCode '[ '[ 'K a]] ast (HMaybe a)
-> DatumCode '[ '[], '[ 'K a]] ast (HMaybe a)
forall (xss :: [[HakaruFun]]) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumCode xss abt a -> DatumCode (xs : xss) abt a
Inr (DatumCode '[ '[ 'K a]] ast (HMaybe a)
-> DatumCode '[ '[], '[ 'K a]] ast (HMaybe a))
-> (ast a -> DatumCode '[ '[ 'K a]] ast (HMaybe a))
-> ast a
-> DatumCode '[ '[], '[ 'K a]] ast (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatumStruct '[ 'K a] ast (HMaybe a)
-> DatumCode '[ '[ 'K a]] ast (HMaybe a)
forall (xs :: [HakaruFun]) (abt :: Hakaru -> *) (a :: Hakaru)
(xss :: [[HakaruFun]]).
DatumStruct xs abt a -> DatumCode (xs : xss) abt a
Inl (DatumStruct '[ 'K a] ast (HMaybe a)
-> DatumCode '[ '[ 'K a]] ast (HMaybe a))
-> (ast a -> DatumStruct '[ 'K a] ast (HMaybe a))
-> ast a
-> DatumCode '[ '[ 'K a]] ast (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatumFun ('K a) ast (HMaybe a)
-> DatumStruct '[] ast (HMaybe a)
-> DatumStruct '[ 'K a] ast (HMaybe a)
forall (x :: HakaruFun) (abt :: Hakaru -> *) (a :: Hakaru)
(xs :: [HakaruFun]).
DatumFun x abt a
-> DatumStruct xs abt a -> DatumStruct (x : xs) abt a
`Et` DatumStruct '[] ast (HMaybe a)
forall (abt :: Hakaru -> *) (a :: Hakaru). DatumStruct '[] abt a
Done) (DatumFun ('K a) ast (HMaybe a)
-> DatumStruct '[ 'K a] ast (HMaybe a))
-> (ast a -> DatumFun ('K a) ast (HMaybe a))
-> ast a
-> DatumStruct '[ 'K a] ast (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ast a -> DatumFun ('K a) ast (HMaybe a)
forall (ast :: Hakaru -> *) (b :: Hakaru) (a :: Hakaru).
ast b -> DatumFun ('K b) ast a
Konst
tdTrue, tdFalse, tdUnit, tdPair, tdLeft, tdRight, tdNil, tdCons, tdNothing, tdJust :: Text
tdTrue :: Text
tdTrue = String -> Text
Text.pack String
"true"
tdFalse :: Text
tdFalse = String -> Text
Text.pack String
"false"
tdUnit :: Text
tdUnit = String -> Text
Text.pack String
"unit"
tdPair :: Text
tdPair = String -> Text
Text.pack String
"pair"
tdLeft :: Text
tdLeft = String -> Text
Text.pack String
"left"
tdRight :: Text
tdRight = String -> Text
Text.pack String
"right"
tdNil :: Text
tdNil = String -> Text
Text.pack String
"nil"
tdCons :: Text
tdCons = String -> Text
Text.pack String
"cons"
tdNothing :: Text
tdNothing = String -> Text
Text.pack String
"nothing"
tdJust :: Text
tdJust = String -> Text
Text.pack String
"just"
data Pattern :: [Hakaru] -> Hakaru -> * where
PWild :: Pattern '[] a
PVar :: Pattern '[ a ] a
PDatum
:: {-# UNPACK #-} !Text
-> !(PDatumCode (Code t) vars (HData' t))
-> Pattern vars (HData' t)
#if __PARTIAL_DATUM_JMEQ__
instance JmEq2 Pattern where
jmEq2 PWild PWild = Just (Refl, cannotProve "jmEq2@Pattern{PWild}")
jmEq2 PVar PVar = Just (cannotProve "jmEq2@Pattern{PVar}", cannotProve "jmEq2@Pattern{PVar}")
jmEq2 (PDatum _ d1) (PDatum _ d2) =
jmEq2_fake d1 d2
where
jmEq2_fake
:: PDatumCode xss vars1 a1
-> PDatumCode xss' vars2 a2
-> Maybe (TypeEq vars1 vars2, TypeEq a1 a2)
jmEq2_fake =
error "jmEq2@Pattern{PDatum}: can't recurse because Code isn't injective"
jmEq2 _ _ = Nothing
instance JmEq1 (Pattern vars) where
jmEq1 p1 p2 = jmEq2 p1 p2 >>= \(_,proof) -> Just proof
#endif
instance Eq2 Pattern where
eq2 :: Pattern i j -> Pattern i j -> Bool
eq2 Pattern i j
PWild Pattern i j
PWild = Bool
True
eq2 Pattern i j
PVar Pattern i j
PVar = Bool
True
eq2 (PDatum Text
_ PDatumCode (Code t) i (HData' t)
d1) (PDatum Text
_ PDatumCode (Code t) i (HData' t)
d2) = PDatumCode (Code t) i (HData' t)
-> PDatumCode (Code t) i (HData' t) -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 PDatumCode (Code t) i (HData' t)
d1 PDatumCode (Code t) i (HData' t)
PDatumCode (Code t) i (HData' t)
d2
eq2 Pattern i j
_ Pattern i j
_ = Bool
False
instance Eq1 (Pattern vars) where
eq1 :: Pattern vars i -> Pattern vars i -> Bool
eq1 = Pattern vars i -> Pattern vars i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (Pattern vars a) where
== :: Pattern vars a -> Pattern vars a -> Bool
(==) = Pattern vars a -> Pattern vars a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show2 Pattern where
showsPrec2 :: Int -> Pattern i j -> ShowS
showsPrec2 Int
_ Pattern i j
PWild = String -> ShowS
showString String
"PWild"
showsPrec2 Int
_ Pattern i j
PVar = String -> ShowS
showString String
"PVar"
showsPrec2 Int
p (PDatum Text
hint PDatumCode (Code t) i (HData' t)
d) = Int -> String -> Text -> PDatumCode (Code t) i (HData' t) -> ShowS
forall k1 k2 b (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
(Show b, Show2 a) =>
Int -> String -> b -> a i j -> ShowS
showParen_02 Int
p String
"PDatum" Text
hint PDatumCode (Code t) i (HData' t)
d
instance Show1 (Pattern vars) where
showsPrec1 :: Int -> Pattern vars i -> ShowS
showsPrec1 = Int -> Pattern vars i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: Pattern vars i -> String
show1 = Pattern vars i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance Show (Pattern vars a) where
showsPrec :: Int -> Pattern vars a -> ShowS
showsPrec = Int -> Pattern vars a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Pattern vars a -> String
show = Pattern vars a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data PDatumCode :: [[HakaruFun]] -> [Hakaru] -> Hakaru -> * where
PInr :: !(PDatumCode xss vars a) -> PDatumCode (xs ': xss) vars a
PInl :: !(PDatumStruct xs vars a) -> PDatumCode (xs ': xss) vars a
#if __PARTIAL_DATUM_JMEQ__
instance JmEq2 (PDatumCode xss) where
jmEq2 (PInr c) (PInr d) = jmEq2 c d
jmEq2 (PInl c) (PInl d) = jmEq2 c d
jmEq2 _ _ = Nothing
instance JmEq1 (PDatumCode xss vars) where
jmEq1 (PInr c) (PInr d) = jmEq1 c d
jmEq1 (PInl c) (PInl d) = jmEq1 c d
jmEq1 _ _ = Nothing
#endif
instance Eq2 (PDatumCode xss) where
eq2 :: PDatumCode xss i j -> PDatumCode xss i j -> Bool
eq2 (PInr PDatumCode xss i j
c) (PInr PDatumCode xss i j
d) = PDatumCode xss i j -> PDatumCode xss i j -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 PDatumCode xss i j
c PDatumCode xss i j
PDatumCode xss i j
d
eq2 (PInl PDatumStruct xs i j
c) (PInl PDatumStruct xs i j
d) = PDatumStruct xs i j -> PDatumStruct xs i j -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 PDatumStruct xs i j
c PDatumStruct xs i j
PDatumStruct xs i j
d
eq2 PDatumCode xss i j
_ PDatumCode xss i j
_ = Bool
False
instance Eq1 (PDatumCode xss vars) where
eq1 :: PDatumCode xss vars i -> PDatumCode xss vars i -> Bool
eq1 = PDatumCode xss vars i -> PDatumCode xss vars i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (PDatumCode xss vars a) where
== :: PDatumCode xss vars a -> PDatumCode xss vars a -> Bool
(==) = PDatumCode xss vars a -> PDatumCode xss vars a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show2 (PDatumCode xss) where
showsPrec2 :: Int -> PDatumCode xss i j -> ShowS
showsPrec2 Int
p (PInr PDatumCode xss i j
d) = Int -> String -> PDatumCode xss i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> String -> a i j -> ShowS
showParen_2 Int
p String
"PInr" PDatumCode xss i j
d
showsPrec2 Int
p (PInl PDatumStruct xs i j
d) = Int -> String -> PDatumStruct xs i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> String -> a i j -> ShowS
showParen_2 Int
p String
"PInl" PDatumStruct xs i j
d
instance Show1 (PDatumCode xss vars) where
showsPrec1 :: Int -> PDatumCode xss vars i -> ShowS
showsPrec1 = Int -> PDatumCode xss vars i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: PDatumCode xss vars i -> String
show1 = PDatumCode xss vars i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance Show (PDatumCode xss vars a) where
showsPrec :: Int -> PDatumCode xss vars a -> ShowS
showsPrec = Int -> PDatumCode xss vars a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: PDatumCode xss vars a -> String
show = PDatumCode xss vars a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data PDatumStruct :: [HakaruFun] -> [Hakaru] -> Hakaru -> * where
PEt :: !(PDatumFun x vars1 a)
-> !(PDatumStruct xs vars2 a)
-> PDatumStruct (x ': xs) (vars1 ++ vars2) a
PDone :: PDatumStruct '[] '[] a
jmEq_P :: Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
jmEq_P :: Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
jmEq_P Pattern vs a
PWild Pattern ws a
PWild = TypeEq vs vs -> Maybe (TypeEq vs vs)
forall a. a -> Maybe a
Just TypeEq vs vs
forall k (a :: k). TypeEq a a
Refl
jmEq_P Pattern vs a
PVar Pattern ws a
PVar = TypeEq vs vs -> Maybe (TypeEq vs vs)
forall a. a -> Maybe a
Just TypeEq vs vs
forall k (a :: k). TypeEq a a
Refl
jmEq_P (PDatum Text
_ PDatumCode (Code t) vs (HData' t)
p1) (PDatum Text
_ PDatumCode (Code t) ws (HData' t)
p2) = PDatumCode (Code t) vs (HData' t)
-> PDatumCode (Code t) ws (HData' t) -> Maybe (TypeEq vs ws)
forall (xss :: [[HakaruFun]]) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumCode xss vs a -> PDatumCode xss ws a -> Maybe (TypeEq vs ws)
jmEq_PCode PDatumCode (Code t) vs (HData' t)
p1 PDatumCode (Code t) ws (HData' t)
PDatumCode (Code t) ws (HData' t)
p2
jmEq_P Pattern vs a
_ Pattern ws a
_ = Maybe (TypeEq vs ws)
forall a. Maybe a
Nothing
jmEq_PCode
:: PDatumCode xss vs a
-> PDatumCode xss ws a
-> Maybe (TypeEq vs ws)
jmEq_PCode :: PDatumCode xss vs a -> PDatumCode xss ws a -> Maybe (TypeEq vs ws)
jmEq_PCode (PInr PDatumCode xss vs a
p1) (PInr PDatumCode xss ws a
p2) = PDatumCode xss vs a -> PDatumCode xss ws a -> Maybe (TypeEq vs ws)
forall (xss :: [[HakaruFun]]) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumCode xss vs a -> PDatumCode xss ws a -> Maybe (TypeEq vs ws)
jmEq_PCode PDatumCode xss vs a
p1 PDatumCode xss ws a
PDatumCode xss ws a
p2
jmEq_PCode (PInl PDatumStruct xs vs a
p1) (PInl PDatumStruct xs ws a
p2) = PDatumStruct xs vs a
-> PDatumStruct xs ws a -> Maybe (TypeEq vs ws)
forall (xs :: [HakaruFun]) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumStruct xs vs a
-> PDatumStruct xs ws a -> Maybe (TypeEq vs ws)
jmEq_PStruct PDatumStruct xs vs a
p1 PDatumStruct xs ws a
PDatumStruct xs ws a
p2
jmEq_PCode PDatumCode xss vs a
_ PDatumCode xss ws a
_ = Maybe (TypeEq vs ws)
forall a. Maybe a
Nothing
jmEq_PStruct
:: PDatumStruct xs vs a
-> PDatumStruct xs ws a
-> Maybe (TypeEq vs ws)
jmEq_PStruct :: PDatumStruct xs vs a
-> PDatumStruct xs ws a -> Maybe (TypeEq vs ws)
jmEq_PStruct (PEt PDatumFun x vars1 a
c1 PDatumStruct xs vars2 a
c2) (PEt PDatumFun x vars1 a
d1 PDatumStruct xs vars2 a
d2) = do
TypeEq vars1 vars1
Refl <- PDatumFun x vars1 a
-> PDatumFun x vars1 a -> Maybe (TypeEq vars1 vars1)
forall (f :: HakaruFun) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumFun f vs a -> PDatumFun f ws a -> Maybe (TypeEq vs ws)
jmEq_PFun PDatumFun x vars1 a
c1 PDatumFun x vars1 a
PDatumFun x vars1 a
d1
TypeEq vars2 vars2
Refl <- PDatumStruct xs vars2 a
-> PDatumStruct xs vars2 a -> Maybe (TypeEq vars2 vars2)
forall (xs :: [HakaruFun]) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumStruct xs vs a
-> PDatumStruct xs ws a -> Maybe (TypeEq vs ws)
jmEq_PStruct PDatumStruct xs vars2 a
c2 PDatumStruct xs vars2 a
PDatumStruct xs vars2 a
d2
TypeEq vs vs -> Maybe (TypeEq vs vs)
forall a. a -> Maybe a
Just TypeEq vs vs
forall k (a :: k). TypeEq a a
Refl
jmEq_PStruct PDatumStruct xs vs a
PDone PDatumStruct xs ws a
PDone = TypeEq vs vs -> Maybe (TypeEq vs vs)
forall a. a -> Maybe a
Just TypeEq vs vs
forall k (a :: k). TypeEq a a
Refl
jmEq_PFun :: PDatumFun f vs a -> PDatumFun f ws a -> Maybe (TypeEq vs ws)
jmEq_PFun :: PDatumFun f vs a -> PDatumFun f ws a -> Maybe (TypeEq vs ws)
jmEq_PFun (PKonst Pattern vs b
p1) (PKonst Pattern ws b
p2) = Pattern vs b -> Pattern ws b -> Maybe (TypeEq vs ws)
forall (vs :: [Hakaru]) (a :: Hakaru) (ws :: [Hakaru]).
Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
jmEq_P Pattern vs b
p1 Pattern ws b
Pattern ws b
p2
jmEq_PFun (PIdent Pattern vs a
p1) (PIdent Pattern ws a
p2) = Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
forall (vs :: [Hakaru]) (a :: Hakaru) (ws :: [Hakaru]).
Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
jmEq_P Pattern vs a
p1 Pattern ws a
p2
#if __PARTIAL_DATUM_JMEQ__
instance JmEq2 (PDatumStruct xs) where
jmEq2 (PEt c1 c2) (PEt d1 d2) = do
(Refl, Refl) <- jmEq2 c1 d1
(Refl, Refl) <- jmEq2 c2 d2
Just (Refl, Refl)
jmEq2 PDone PDone = Just (Refl, cannotProve "jmEq2@PDatumStruct{PDone}")
jmEq2 _ _ = Nothing
instance JmEq1 (PDatumStruct xs vars) where
jmEq1 p1 p2 = jmEq2 p1 p2 >>= \(_,proof) -> Just proof
#endif
instance Eq2 (PDatumStruct xs) where
eq2 :: PDatumStruct xs i j -> PDatumStruct xs i j -> Bool
eq2 PDatumStruct xs i j
p1 PDatumStruct xs i j
p2 = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Maybe (TypeEq i i) -> Bool) -> Maybe (TypeEq i i) -> Bool
forall a b. (a -> b) -> a -> b
$ PDatumStruct xs i j -> PDatumStruct xs i j -> Maybe (TypeEq i i)
forall (xs :: [HakaruFun]) (vs :: [Hakaru]) (a :: Hakaru)
(ws :: [Hakaru]).
PDatumStruct xs vs a
-> PDatumStruct xs ws a -> Maybe (TypeEq vs ws)
jmEq_PStruct PDatumStruct xs i j
p1 PDatumStruct xs i j
p2
instance Eq1 (PDatumStruct xs vars) where
eq1 :: PDatumStruct xs vars i -> PDatumStruct xs vars i -> Bool
eq1 = PDatumStruct xs vars i -> PDatumStruct xs vars i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (PDatumStruct xs vars a) where
== :: PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool
(==) = PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show2 (PDatumStruct xs) where
showsPrec2 :: Int -> PDatumStruct xs i j -> ShowS
showsPrec2 Int
p (PEt PDatumFun x vars1 j
d1 PDatumStruct xs vars2 j
d2) = Int
-> String
-> PDatumFun x vars1 j
-> PDatumStruct xs vars2 j
-> ShowS
forall k4 k5 k6 k7 (a :: k4 -> k5 -> *) (b :: k6 -> k7 -> *)
(i1 :: k4) (j1 :: k5) (i2 :: k6) (j2 :: k7).
(Show2 a, Show2 b) =>
Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 Int
p String
"PEt" PDatumFun x vars1 j
d1 PDatumStruct xs vars2 j
d2
showsPrec2 Int
_ PDatumStruct xs i j
PDone = String -> ShowS
showString String
"PDone"
instance Show1 (PDatumStruct xs vars) where
showsPrec1 :: Int -> PDatumStruct xs vars i -> ShowS
showsPrec1 = Int -> PDatumStruct xs vars i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: PDatumStruct xs vars i -> String
show1 = PDatumStruct xs vars i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance Show (PDatumStruct xs vars a) where
showsPrec :: Int -> PDatumStruct xs vars a -> ShowS
showsPrec = Int -> PDatumStruct xs vars a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: PDatumStruct xs vars a -> String
show = PDatumStruct xs vars a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data PDatumFun :: HakaruFun -> [Hakaru] -> Hakaru -> * where
PKonst :: !(Pattern vars b) -> PDatumFun ('K b) vars a
PIdent :: !(Pattern vars a) -> PDatumFun 'I vars a
#if __PARTIAL_DATUM_JMEQ__
instance JmEq2 (PDatumFun x) where
jmEq2 (PKonst p1) (PKonst p2) = do
(Refl, Refl) <- jmEq2 p1 p2
Just (Refl, cannotProve "jmEq2@PDatumFun{PKonst}")
jmEq2 (PIdent p1) (PIdent p2) = jmEq2 p1 p2
jmEq2 _ _ = Nothing
instance JmEq1 (PDatumFun x vars) where
jmEq1 (PKonst e) (PKonst f) = do
Refl <- jmEq1 e f
Just (cannotProve "jmEq1@PDatumFun{PKonst}")
jmEq1 (PIdent e) (PIdent f) = jmEq1 e f
jmEq1 _ _ = Nothing
#endif
instance Eq2 (PDatumFun x) where
eq2 :: PDatumFun x i j -> PDatumFun x i j -> Bool
eq2 (PKonst Pattern i b
e) (PKonst Pattern i b
f) = Pattern i b -> Pattern i b -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 Pattern i b
e Pattern i b
Pattern i b
f
eq2 (PIdent Pattern i j
e) (PIdent Pattern i j
f) = Pattern i j -> Pattern i j -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 Pattern i j
e Pattern i j
f
instance Eq1 (PDatumFun x vars) where
eq1 :: PDatumFun x vars i -> PDatumFun x vars i -> Bool
eq1 = PDatumFun x vars i -> PDatumFun x vars i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq (PDatumFun x vars a) where
== :: PDatumFun x vars a -> PDatumFun x vars a -> Bool
(==) = PDatumFun x vars a -> PDatumFun x vars a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show2 (PDatumFun x) where
showsPrec2 :: Int -> PDatumFun x i j -> ShowS
showsPrec2 Int
p (PKonst Pattern i b
e) = Int -> String -> Pattern i b -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> String -> a i j -> ShowS
showParen_2 Int
p String
"PKonst" Pattern i b
e
showsPrec2 Int
p (PIdent Pattern i j
e) = Int -> String -> Pattern i j -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> String -> a i j -> ShowS
showParen_2 Int
p String
"PIdent" Pattern i j
e
instance Show1 (PDatumFun x vars) where
showsPrec1 :: Int -> PDatumFun x vars i -> ShowS
showsPrec1 = Int -> PDatumFun x vars i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: PDatumFun x vars i -> String
show1 = PDatumFun x vars i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance Show (PDatumFun x vars a) where
showsPrec :: Int -> PDatumFun x vars a -> ShowS
showsPrec = Int -> PDatumFun x vars a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: PDatumFun x vars a -> String
show = PDatumFun x vars a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
pTrue, pFalse :: Pattern '[] HBool
pTrue :: Pattern '[] HBool
pTrue = Text
-> PDatumCode (Code ('TyCon "Bool")) '[] (HData' ('TyCon "Bool"))
-> Pattern '[] (HData' ('TyCon "Bool"))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdTrue (PDatumCode '[ '[], '[]] '[] HBool -> Pattern '[] HBool)
-> (PDatumStruct '[] '[] HBool
-> PDatumCode '[ '[], '[]] '[] HBool)
-> PDatumStruct '[] '[] HBool
-> Pattern '[] HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[] '[] HBool -> PDatumCode '[ '[], '[]] '[] HBool
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[] '[] HBool -> Pattern '[] HBool)
-> PDatumStruct '[] '[] HBool -> Pattern '[] HBool
forall a b. (a -> b) -> a -> b
$ PDatumStruct '[] '[] HBool
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pFalse :: Pattern '[] HBool
pFalse = Text
-> PDatumCode (Code ('TyCon "Bool")) '[] (HData' ('TyCon "Bool"))
-> Pattern '[] (HData' ('TyCon "Bool"))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdFalse (PDatumCode '[ '[], '[]] '[] HBool -> Pattern '[] HBool)
-> (PDatumStruct '[] '[] HBool
-> PDatumCode '[ '[], '[]] '[] HBool)
-> PDatumStruct '[] '[] HBool
-> Pattern '[] HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumCode '[ '[]] '[] HBool -> PDatumCode '[ '[], '[]] '[] HBool
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]).
PDatumCode xss vars a -> PDatumCode (xs : xss) vars a
PInr (PDatumCode '[ '[]] '[] HBool -> PDatumCode '[ '[], '[]] '[] HBool)
-> (PDatumStruct '[] '[] HBool -> PDatumCode '[ '[]] '[] HBool)
-> PDatumStruct '[] '[] HBool
-> PDatumCode '[ '[], '[]] '[] HBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[] '[] HBool -> PDatumCode '[ '[]] '[] HBool
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[] '[] HBool -> Pattern '[] HBool)
-> PDatumStruct '[] '[] HBool -> Pattern '[] HBool
forall a b. (a -> b) -> a -> b
$ PDatumStruct '[] '[] HBool
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pUnit :: Pattern '[] HUnit
pUnit :: Pattern '[] HUnit
pUnit = Text
-> PDatumCode (Code ('TyCon "Unit")) '[] (HData' ('TyCon "Unit"))
-> Pattern '[] (HData' ('TyCon "Unit"))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdUnit (PDatumCode '[ '[]] '[] HUnit -> Pattern '[] HUnit)
-> (PDatumStruct '[] '[] HUnit -> PDatumCode '[ '[]] '[] HUnit)
-> PDatumStruct '[] '[] HUnit
-> Pattern '[] HUnit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[] '[] HUnit -> PDatumCode '[ '[]] '[] HUnit
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[] '[] HUnit -> Pattern '[] HUnit)
-> PDatumStruct '[] '[] HUnit -> Pattern '[] HUnit
forall a b. (a -> b) -> a -> b
$ PDatumStruct '[] '[] HUnit
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
varsOfPattern :: Pattern vars a -> proxy vars
varsOfPattern :: Pattern vars a -> proxy vars
varsOfPattern Pattern vars a
_ = String -> proxy vars
forall a. HasCallStack => String -> a
error String
"TODO: varsOfPattern"
pPair
:: Pattern vars1 a
-> Pattern vars2 b
-> Pattern (vars1 ++ vars2) (HPair a b)
pPair :: Pattern vars1 a
-> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b)
pPair Pattern vars1 a
x Pattern vars2 b
y =
case Any vars2 -> TypeEq vars2 (vars2 ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars2 b -> Any vars2
forall (vars :: [Hakaru]) (a :: Hakaru) (proxy :: [Hakaru] -> *).
Pattern vars a -> proxy vars
varsOfPattern Pattern vars2 b
y) of
TypeEq vars2 (vars2 ++ '[])
Refl -> Text
-> PDatumCode
(Code (('TyCon "Pair" ':@ a) ':@ b))
(vars1 ++ vars2)
(HData' (('TyCon "Pair" ':@ a) ':@ b))
-> Pattern (vars1 ++ vars2) (HData' (('TyCon "Pair" ':@ a) ':@ b))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdPair (PDatumCode '[ '[ 'K a, 'K b]] (vars1 ++ vars2) (HPair a b)
-> Pattern (vars1 ++ vars2) (HPair a b))
-> (PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
-> PDatumCode '[ '[ 'K a, 'K b]] (vars1 ++ vars2) (HPair a b))
-> PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
-> Pattern (vars1 ++ vars2) (HPair a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
-> PDatumCode '[ '[ 'K a, 'K b]] (vars1 ++ vars2) (HPair a b)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
-> Pattern (vars1 ++ vars2) (HPair a b))
-> PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
-> Pattern (vars1 ++ vars2) (HPair a b)
forall a b. (a -> b) -> a -> b
$ Pattern vars1 a -> PDatumFun ('K a) vars1 (HPair a b)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars1 a
x PDatumFun ('K a) vars1 (HPair a b)
-> PDatumStruct '[ 'K b] vars2 (HPair a b)
-> PDatumStruct '[ 'K a, 'K b] (vars1 ++ vars2) (HPair a b)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` Pattern vars2 b -> PDatumFun ('K b) vars2 (HPair a b)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars2 b
y PDatumFun ('K b) vars2 (HPair a b)
-> PDatumStruct '[] '[] (HPair a b)
-> PDatumStruct '[ 'K b] (vars2 ++ '[]) (HPair a b)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` PDatumStruct '[] '[] (HPair a b)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pLeft :: Pattern vars a -> Pattern vars (HEither a b)
pLeft :: Pattern vars a -> Pattern vars (HEither a b)
pLeft Pattern vars a
x =
case Any vars -> TypeEq vars (vars ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars a -> Any vars
forall (vars :: [Hakaru]) (a :: Hakaru) (proxy :: [Hakaru] -> *).
Pattern vars a -> proxy vars
varsOfPattern Pattern vars a
x) of
TypeEq vars (vars ++ '[])
Refl -> Text
-> PDatumCode
(Code (('TyCon "Either" ':@ a) ':@ b))
vars
(HData' (('TyCon "Either" ':@ a) ':@ b))
-> Pattern vars (HData' (('TyCon "Either" ':@ a) ':@ b))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdLeft (PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b)
-> Pattern vars (HEither a b))
-> (PDatumStruct '[ 'K a] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b))
-> PDatumStruct '[ 'K a] vars (HEither a b)
-> Pattern vars (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[ 'K a] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[ 'K a] vars (HEither a b)
-> Pattern vars (HEither a b))
-> PDatumStruct '[ 'K a] vars (HEither a b)
-> Pattern vars (HEither a b)
forall a b. (a -> b) -> a -> b
$ Pattern vars a -> PDatumFun ('K a) vars (HEither a b)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars a
x PDatumFun ('K a) vars (HEither a b)
-> PDatumStruct '[] '[] (HEither a b)
-> PDatumStruct '[ 'K a] (vars ++ '[]) (HEither a b)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` PDatumStruct '[] '[] (HEither a b)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pRight :: Pattern vars b -> Pattern vars (HEither a b)
pRight :: Pattern vars b -> Pattern vars (HEither a b)
pRight Pattern vars b
y =
case Any vars -> TypeEq vars (vars ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars b -> Any vars
forall (vars :: [Hakaru]) (a :: Hakaru) (proxy :: [Hakaru] -> *).
Pattern vars a -> proxy vars
varsOfPattern Pattern vars b
y) of
TypeEq vars (vars ++ '[])
Refl -> Text
-> PDatumCode
(Code (('TyCon "Either" ':@ a) ':@ b))
vars
(HData' (('TyCon "Either" ':@ a) ':@ b))
-> Pattern vars (HData' (('TyCon "Either" ':@ a) ':@ b))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdRight (PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b)
-> Pattern vars (HEither a b))
-> (PDatumStruct '[ 'K b] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b))
-> PDatumStruct '[ 'K b] vars (HEither a b)
-> Pattern vars (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumCode '[ '[ 'K b]] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b)
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]).
PDatumCode xss vars a -> PDatumCode (xs : xss) vars a
PInr (PDatumCode '[ '[ 'K b]] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b))
-> (PDatumStruct '[ 'K b] vars (HEither a b)
-> PDatumCode '[ '[ 'K b]] vars (HEither a b))
-> PDatumStruct '[ 'K b] vars (HEither a b)
-> PDatumCode '[ '[ 'K a], '[ 'K b]] vars (HEither a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[ 'K b] vars (HEither a b)
-> PDatumCode '[ '[ 'K b]] vars (HEither a b)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[ 'K b] vars (HEither a b)
-> Pattern vars (HEither a b))
-> PDatumStruct '[ 'K b] vars (HEither a b)
-> Pattern vars (HEither a b)
forall a b. (a -> b) -> a -> b
$ Pattern vars b -> PDatumFun ('K b) vars (HEither a b)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars b
y PDatumFun ('K b) vars (HEither a b)
-> PDatumStruct '[] '[] (HEither a b)
-> PDatumStruct '[ 'K b] (vars ++ '[]) (HEither a b)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` PDatumStruct '[] '[] (HEither a b)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pNil :: Pattern '[] (HList a)
pNil :: Pattern '[] (HList a)
pNil = Text
-> PDatumCode
(Code ('TyCon "List" ':@ a)) '[] (HData' ('TyCon "List" ':@ a))
-> Pattern '[] (HData' ('TyCon "List" ':@ a))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdNil (PDatumCode '[ '[], '[ 'K a, 'I]] '[] (HList a)
-> Pattern '[] (HList a))
-> (PDatumStruct '[] '[] (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] '[] (HList a))
-> PDatumStruct '[] '[] (HList a)
-> Pattern '[] (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[] '[] (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] '[] (HList a)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[] '[] (HList a) -> Pattern '[] (HList a))
-> PDatumStruct '[] '[] (HList a) -> Pattern '[] (HList a)
forall a b. (a -> b) -> a -> b
$ PDatumStruct '[] '[] (HList a)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pCons :: Pattern vars1 a
-> Pattern vars2 (HList a)
-> Pattern (vars1 ++ vars2) (HList a)
pCons :: Pattern vars1 a
-> Pattern vars2 (HList a) -> Pattern (vars1 ++ vars2) (HList a)
pCons Pattern vars1 a
x Pattern vars2 (HList a)
xs =
case Any vars2 -> TypeEq vars2 (vars2 ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars2 (HList a) -> Any vars2
forall (vars :: [Hakaru]) (a :: Hakaru) (proxy :: [Hakaru] -> *).
Pattern vars a -> proxy vars
varsOfPattern Pattern vars2 (HList a)
xs) of
TypeEq vars2 (vars2 ++ '[])
Refl -> Text
-> PDatumCode
(Code ('TyCon "List" ':@ a))
(vars1 ++ vars2)
(HData' ('TyCon "List" ':@ a))
-> Pattern (vars1 ++ vars2) (HData' ('TyCon "List" ':@ a))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdCons (PDatumCode '[ '[], '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
-> Pattern (vars1 ++ vars2) (HList a))
-> (PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] (vars1 ++ vars2) (HList a))
-> PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> Pattern (vars1 ++ vars2) (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumCode '[ '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]).
PDatumCode xss vars a -> PDatumCode (xs : xss) vars a
PInr (PDatumCode '[ '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] (vars1 ++ vars2) (HList a))
-> (PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[ 'K a, 'I]] (vars1 ++ vars2) (HList a))
-> PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[], '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> PDatumCode '[ '[ 'K a, 'I]] (vars1 ++ vars2) (HList a)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> Pattern (vars1 ++ vars2) (HList a))
-> PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
-> Pattern (vars1 ++ vars2) (HList a)
forall a b. (a -> b) -> a -> b
$ Pattern vars1 a -> PDatumFun ('K a) vars1 (HList a)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars1 a
x PDatumFun ('K a) vars1 (HList a)
-> PDatumStruct '[ 'I] vars2 (HList a)
-> PDatumStruct '[ 'K a, 'I] (vars1 ++ vars2) (HList a)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` Pattern vars2 (HList a) -> PDatumFun 'I vars2 (HList a)
forall (vars :: [Hakaru]) (a :: Hakaru).
Pattern vars a -> PDatumFun 'I vars a
PIdent Pattern vars2 (HList a)
xs PDatumFun 'I vars2 (HList a)
-> PDatumStruct '[] '[] (HList a)
-> PDatumStruct '[ 'I] (vars2 ++ '[]) (HList a)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` PDatumStruct '[] '[] (HList a)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pNothing :: Pattern '[] (HMaybe a)
pNothing :: Pattern '[] (HMaybe a)
pNothing = Text
-> PDatumCode
(Code ('TyCon "Maybe" ':@ a)) '[] (HData' ('TyCon "Maybe" ':@ a))
-> Pattern '[] (HData' ('TyCon "Maybe" ':@ a))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdNothing (PDatumCode '[ '[], '[ 'K a]] '[] (HMaybe a)
-> Pattern '[] (HMaybe a))
-> (PDatumStruct '[] '[] (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] '[] (HMaybe a))
-> PDatumStruct '[] '[] (HMaybe a)
-> Pattern '[] (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[] '[] (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] '[] (HMaybe a)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[] '[] (HMaybe a) -> Pattern '[] (HMaybe a))
-> PDatumStruct '[] '[] (HMaybe a) -> Pattern '[] (HMaybe a)
forall a b. (a -> b) -> a -> b
$ PDatumStruct '[] '[] (HMaybe a)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
pJust :: Pattern vars a -> Pattern vars (HMaybe a)
pJust :: Pattern vars a -> Pattern vars (HMaybe a)
pJust Pattern vars a
x =
case Any vars -> TypeEq vars (vars ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars a -> Any vars
forall (vars :: [Hakaru]) (a :: Hakaru) (proxy :: [Hakaru] -> *).
Pattern vars a -> proxy vars
varsOfPattern Pattern vars a
x) of
TypeEq vars (vars ++ '[])
Refl -> Text
-> PDatumCode
(Code ('TyCon "Maybe" ':@ a)) vars (HData' ('TyCon "Maybe" ':@ a))
-> Pattern vars (HData' ('TyCon "Maybe" ':@ a))
forall (t :: HakaruCon) (vars :: [Hakaru]).
Text
-> PDatumCode (Code t) vars (HData' t) -> Pattern vars (HData' t)
PDatum Text
tdJust (PDatumCode '[ '[], '[ 'K a]] vars (HMaybe a)
-> Pattern vars (HMaybe a))
-> (PDatumStruct '[ 'K a] vars (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] vars (HMaybe a))
-> PDatumStruct '[ 'K a] vars (HMaybe a)
-> Pattern vars (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumCode '[ '[ 'K a]] vars (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] vars (HMaybe a)
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]).
PDatumCode xss vars a -> PDatumCode (xs : xss) vars a
PInr (PDatumCode '[ '[ 'K a]] vars (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] vars (HMaybe a))
-> (PDatumStruct '[ 'K a] vars (HMaybe a)
-> PDatumCode '[ '[ 'K a]] vars (HMaybe a))
-> PDatumStruct '[ 'K a] vars (HMaybe a)
-> PDatumCode '[ '[], '[ 'K a]] vars (HMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDatumStruct '[ 'K a] vars (HMaybe a)
-> PDatumCode '[ '[ 'K a]] vars (HMaybe a)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru)
(xss :: [[HakaruFun]]).
PDatumStruct xs vars a -> PDatumCode (xs : xss) vars a
PInl (PDatumStruct '[ 'K a] vars (HMaybe a) -> Pattern vars (HMaybe a))
-> PDatumStruct '[ 'K a] vars (HMaybe a) -> Pattern vars (HMaybe a)
forall a b. (a -> b) -> a -> b
$ Pattern vars a -> PDatumFun ('K a) vars (HMaybe a)
forall (vars :: [Hakaru]) (b :: Hakaru) (a :: Hakaru).
Pattern vars b -> PDatumFun ('K b) vars a
PKonst Pattern vars a
x PDatumFun ('K a) vars (HMaybe a)
-> PDatumStruct '[] '[] (HMaybe a)
-> PDatumStruct '[ 'K a] (vars ++ '[]) (HMaybe a)
forall (x :: HakaruFun) (vars1 :: [Hakaru]) (a :: Hakaru)
(xs :: [HakaruFun]) (vars2 :: [Hakaru]).
PDatumFun x vars1 a
-> PDatumStruct xs vars2 a
-> PDatumStruct (x : xs) (vars1 ++ vars2) a
`PEt` PDatumStruct '[] '[] (HMaybe a)
forall (a :: Hakaru). PDatumStruct '[] '[] a
PDone
data Branch
(a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *)
(b :: Hakaru)
= forall xs. Branch
!(Pattern xs a)
!(abt xs b)
instance Eq2 abt => Eq1 (Branch a abt) where
eq1 :: Branch a abt i -> Branch a abt i -> Bool
eq1 (Branch Pattern xs a
p1 abt xs i
e1) (Branch Pattern xs a
p2 abt xs i
e2) =
case Pattern xs a -> Pattern xs a -> Maybe (TypeEq xs xs)
forall (vs :: [Hakaru]) (a :: Hakaru) (ws :: [Hakaru]).
Pattern vs a -> Pattern ws a -> Maybe (TypeEq vs ws)
jmEq_P Pattern xs a
p1 Pattern xs a
p2 of
Maybe (TypeEq xs xs)
Nothing -> Bool
False
Just TypeEq xs xs
Refl -> abt xs i -> abt xs i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 abt xs i
e1 abt xs i
abt xs i
e2
instance Eq2 abt => Eq (Branch a abt b) where
== :: Branch a abt b -> Branch a abt b -> Bool
(==) = Branch a abt b -> Branch a abt b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Show2 abt => Show1 (Branch a abt) where
showsPrec1 :: Int -> Branch a abt i -> ShowS
showsPrec1 Int
p (Branch Pattern xs a
pat abt xs i
e) = Int -> String -> Pattern xs a -> abt xs i -> ShowS
forall k4 k5 k6 k7 (a :: k4 -> k5 -> *) (b :: k6 -> k7 -> *)
(i1 :: k4) (j1 :: k5) (i2 :: k6) (j2 :: k7).
(Show2 a, Show2 b) =>
Int -> String -> a i1 j1 -> b i2 j2 -> ShowS
showParen_22 Int
p String
"Branch" Pattern xs a
pat abt xs i
e
instance Show2 abt => Show (Branch a abt b) where
showsPrec :: Int -> Branch a abt b -> ShowS
showsPrec = Int -> Branch a abt b -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Branch a abt b -> String
show = Branch a abt b -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Functor21 (Branch a) where
fmap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i)
-> Branch a a j -> Branch a b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f (Branch Pattern xs a
p a xs j
e) = Pattern xs a -> b xs j -> Branch a b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
(xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern xs a
p (a xs j -> b xs j
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> b h i
f a xs j
e)
instance Foldable21 (Branch a) where
foldMap21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m)
-> Branch a a j -> m
foldMap21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f (Branch Pattern xs a
_ a xs j
e) = a xs j -> m
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> m
f a xs j
e
instance Traversable21 (Branch a) where
traverse21 :: (forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i))
-> Branch a a j -> f (Branch a b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f (Branch Pattern xs a
pat a xs j
e) = Pattern xs a -> b xs j -> Branch a b j
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
(xs :: [Hakaru]).
Pattern xs a -> abt xs b -> Branch a abt b
Branch Pattern xs a
pat (b xs j -> Branch a b j) -> f (b xs j) -> f (Branch a b j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a xs j -> f (b xs j)
forall (h :: [Hakaru]) (i :: Hakaru). a h i -> f (b h i)
f a xs j
e
data GBranch (a :: Hakaru) (r :: *)
= forall xs. GBranch
!(Pattern xs a)
!(List1 Variable xs)
r
instance Functor (GBranch a) where
fmap :: (a -> b) -> GBranch a a -> GBranch a b
fmap a -> b
f (GBranch Pattern xs a
pat List1 Variable xs
vars a
x) = Pattern xs a -> List1 Variable xs -> b -> GBranch a b
forall (a :: Hakaru) r (xs :: [Hakaru]).
Pattern xs a -> List1 Variable xs -> r -> GBranch a r
GBranch Pattern xs a
pat List1 Variable xs
vars (a -> b
f a
x)
instance F.Foldable (GBranch a) where
foldMap :: (a -> m) -> GBranch a a -> m
foldMap a -> m
f (GBranch Pattern xs a
_ List1 Variable xs
_ a
x) = a -> m
f a
x
instance T.Traversable (GBranch a) where
traverse :: (a -> f b) -> GBranch a a -> f (GBranch a b)
traverse a -> f b
f (GBranch Pattern xs a
pat List1 Variable xs
vars a
x) = Pattern xs a -> List1 Variable xs -> b -> GBranch a b
forall (a :: Hakaru) r (xs :: [Hakaru]).
Pattern xs a -> List1 Variable xs -> r -> GBranch a r
GBranch Pattern xs a
pat List1 Variable xs
vars (b -> GBranch a b) -> f b -> f (GBranch a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x