{-# LANGUAGE CPP
           , DataKinds
           , PolyKinds
           , GADTs
           , TypeOperators
           , TypeFamilies
           , ExistentialQuantification
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.05.24
-- |
-- Module      :  Language.Hakaru.Syntax.Datum
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Haskell types and helpers for Hakaru's user-defined data types.
-- At present we only support regular-recursive polynomial data
-- types. Reduction of case analysis on data types is in
-- "Language.Hakaru.Syntax.Datum".
--
-- /Developers note:/ many of the 'JmEq1' instances in this file
-- don't actually work because of problems with matching existentially
-- quantified types in the basis cases. For now I've left the
-- partially-defined code in place, but turned it off with the
-- @__PARTIAL_DATUM_JMEQ__@ CPP macro. In the future we should
-- either (a) remove this unused code, or (b) if the instances are
-- truly necessary then we should add the 'Sing' arguments everywhere
-- to make things work :(
----------------------------------------------------------------
module Language.Hakaru.Syntax.Datum
    (
    -- * Data constructors
      Datum(..), datumHint, datumType
    , DatumCode(..)
    , DatumStruct(..)
    , DatumFun(..)
    -- ** Some smart constructors for the \"built-in\" datatypes
    , dTrue, dFalse, dBool
    , dUnit
    , dPair
    , dLeft, dRight
    , dNil, dCons
    , dNothing, dJust
    -- *** Variants which allow explicit type passing.
    , dPair_
    , dLeft_, dRight_
    , dNil_, dCons_
    , dNothing_, dJust_

    -- * Pattern constructors
    , Branch(..)
    , Pattern(..)
    , PDatumCode(..)
    , PDatumStruct(..)
    , PDatumFun(..)
    -- ** Some smart constructors for the \"built-in\" datatypes
    , pTrue, pFalse
    , pUnit
    , pPair
    , pLeft, pRight
    , pNil, pCons
    , pNothing, pJust
    -- ** Generalized branches
    , 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(..))
-- TODO: make things polykinded so we can make our ABT implementation
-- independent of Hakaru's type system.
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


-- TODO: change the kind to @(Hakaru -> *) -> HakaruCon -> *@ so
-- we can avoid the use of GADTs? Would that allow us to actually
-- UNPACK?
--
-- | A fully saturated data constructor, which recurses as @ast@.
-- We define this type as separate from 'DatumCode' for two reasons.
-- First is to capture the fact that the datum is \"complete\"
-- (i.e., is a well-formed constructor). The second is to have a
-- type which is indexed by its 'Hakaru' type, whereas 'DatumCode'
-- involves non-Hakaru types.
--
-- The first component is a hint for what the data constructor
-- should be called when pretty-printing, giving error messages,
-- etc. Like the hints for variable names, its value is not actually
-- used to decide which constructor is meant or which pattern
-- matches.
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

-- N.B., This doesn't require jmEq on 'DatumCode' nor on @ast@. The
-- jmEq on the singleton is sufficient.
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

-- TODO: instance Read (Datum ast a)

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`

-- | The intermediate components of a data constructor. The intuition
-- behind the two indices is that the @[[HakaruFun]]@ is a functor
-- applied to the Hakaru type. Initially the @[[HakaruFun]]@ functor
-- will be the 'Code' associated with the Hakaru type; hence it's
-- the one-step unrolling of the fixed point for our recursive
-- datatypes. But as we go along, we'll be doing induction on the
-- @[[HakaruFun]]@ functor.
data DatumCode :: [[HakaruFun]] -> (Hakaru -> *) -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- Skip rightwards along the sum.
    Inr :: !(DatumCode  xss abt a) -> DatumCode (xs ': xss) abt a
    -- Inject into the sum.
    Inl :: !(DatumStruct xs abt a) -> DatumCode (xs ': xss) abt a


-- N.B., these \"Foo1\" instances rely on polymorphic recursion,
-- since the @code@ changes at each constructor. However, we don't
-- actually need to abstract over @code@ in order to define these
-- functions, because (1) we never existentially close over any
-- codes, and (2) the code is always getting smaller; so we have
-- a good enough inductive hypothesis from polymorphism alone.

#if __PARTIAL_DATUM_JMEQ__
-- This instance works, but recurses into non-working instances.
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

-- TODO: instance Read (DatumCode xss abt a)

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
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- Combine components of the product. (\"et\" means \"and\" in Latin)
    Et  :: !(DatumFun    x         abt a)
        -> !(DatumStruct xs        abt a)
        ->   DatumStruct (x ': xs) abt a

    -- Close off the product.
    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 -- HACK: to handle 'Done' in the cases where we can.
    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

-- TODO: instance Read (DatumStruct xs abt a)

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


----------------------------------------------------------------
-- TODO: do we like those constructor names? Should we change them?
data DatumFun :: HakaruFun -> (Hakaru -> *) -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- Hit a leaf which isn't a recursive component of the datatype.
    Konst :: !(ast b) -> DatumFun ('K b) ast a
    -- Hit a leaf which is a recursive component of the datatype.
    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 -- This 'Refl' should be free because @x@ is fixed
        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

-- TODO: instance Read (DatumFun x abt a)

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


----------------------------------------------------------------
-- In GHC 7.8 we can make the monomorphic smart constructors into
-- pattern synonyms, but 7.8 can't handle anything polymorphic (but
-- GHC 7.10 can). For libraries (e.g., "Language.Hakaru.Syntax.Prelude")
-- we can use functions to construct our Case_ statements, so library
-- designers don't need pattern synonyms. Whereas, for the internal
-- aspects of the compiler, we need to handle all possible Datum
-- values, so the pattern synonyms wouldn't even be helpful.

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"


----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: negative patterns? (to facilitate reordering of case branches)
-- TODO: disjunctive patterns, a~la ML?
-- TODO: equality patterns for Nat\/Int? (what about Prob\/Real??)
-- TODO: exhaustiveness, non-overlap, dead-branch checking
--
-- | We index patterns by the type they scrutinize. This requires
-- the parser to be smart enough to build these patterns up, but
-- then it guarantees that we can't have 'Case_' of patterns which
-- can't possibly match according to our type system. In addition,
-- we also index patterns by the type of what variables they bind,
-- so that we can ensure that 'Branch' will never \"go wrong\".
-- Alas, this latter indexing means we can't use 'DatumCode',
-- 'DatumStruct', and 'DatumFun' but rather must define our own @P@
-- variants for pattern matching.
data Pattern :: [Hakaru] -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- The \"don't care\" wildcard pattern.
    PWild :: Pattern '[]    a

    -- A pattern variable.
    PVar  :: Pattern '[ a ] a

    -- A data type constructor pattern. As with the 'Datum'
    -- constructor, the first component is a hint.
    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" -- so @xss@ and @xss'@ aren't guaranteed to be the same
    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

-- TODO: instance Read (Pattern vars a)

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

-- TODO: as necessary Functor22, Foldable22, Traversable22


----------------------------------------------------------------
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

-- This instance works, but recurses into non-working instances.
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

-- TODO: instance Read (PDatumCode xss vars a)

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

-- TODO: as necessary Functor22, Foldable22, Traversable22

----------------------------------------------------------------
data PDatumStruct :: [HakaruFun] -> [Hakaru] -> Hakaru -> * where
    PEt :: !(PDatumFun    x         vars1 a)
        -> !(PDatumStruct xs        vars2 a)
        ->   PDatumStruct (x ': xs) (vars1 ++ vars2) a

    PDone :: PDatumStruct '[] '[] a


-- This block of recursive functions are analogous to 'JmEq2' except
-- we only return the equality proof for the penultimate index
-- rather than both the penultimate and ultimate index. (Because
-- we /can/ return proofs for the penultimate index, but not for
-- the ultimate.) This is necessary for defining the @Eq1 (PDatumStruct
-- xs vars)@ and @Eq1 (Branch a abt)@ instances, since we need to
-- make sure the existential @vars@ match up.

-- N.B., that we can use 'Refl' in the 'PVar' case relies on the
-- fact that the @a@ parameter is fixed to be the same in both
-- patterns.
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

-- TODO: instance Read (PDatumStruct xs vars a)

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

-- TODO: as necessary Functor22, Foldable22, Traversable22


----------------------------------------------------------------
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

-- TODO: instance Read (PDatumFun x vars a)

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

-- TODO: as necessary Functor22, Foldable22, Traversable22


----------------------------------------------------------------
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

-- HACK: using undefined like that isn't going to help if we use
-- the variant of eqAppendIdentity that actually needs the Sing...
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

----------------------------------------------------------------
-- TODO: a pretty infix syntax, like (:=>) or something?
--
-- TODO: this datatype is helpful for capturing the existential;
-- but other than that, it should be replaced\/augmented with a
-- type for pattern automata, so we can optimize case analysis.
--
-- TODO: if we used the argument order @Branch abt a b@ then we
-- could give @Foo2@ instances instead of just @Foo1@ instances.
-- Also would possibly let us talk about branches as profunctors
-- mapping @a@ to @b@. Would either of these actually be helpful
-- in practice for us?
data Branch
    (a   :: Hakaru)                  -- The type of the scrutinee.
    (abt :: [Hakaru] -> Hakaru -> *) -- The 'ABT' of the body.
    (b   :: Hakaru)                  -- The type of the body.
    = 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

-- TODO: instance Read (Branch abt a b)

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

----------------------------------------------------------------
-- | A generalization of the 'Branch' type to allow a \"body\" of
-- any Haskell type.
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

----------------------------------------------------------------
----------------------------------------------------------- fin.