{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
-- HasSpec instances for known types such as (a,b,c), (a,b,c,d) i.e. tuples.
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Minimal.Tuple where

import Constrained.GenT
import Constrained.List hiding (ListCtx)
import Data.Kind
import qualified Data.List.NonEmpty as NE
import Data.Set (Set)
import Test.Minimal.Base
import Test.Minimal.Model
import Test.Minimal.Syntax

-- import Data.Coerce
-- import Data.Typeable

-- =======================================================
-- Experiment to see if we can build tuples, using only the binary tuple
-- as the base case.  The only compilcated part is the `combineSpec` which
-- uses `guardTypeSpec` to merge the simple sub cases on smaller tuples.

instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (a, b, c) where
  type TypeSpec (a, b, c) = (Spec a, Spec (b, c))

  anySpec :: TypeSpec (a, b, c)
anySpec = (forall a. Monoid a => a
mempty @(Spec a), forall a. Monoid a => a
mempty @(Spec (b, c)))

  combineSpec :: TypeSpec (a, b, c) -> TypeSpec (a, b, c) -> Spec (a, b, c)
combineSpec (Spec a
a, Spec (b, c)
b) (Spec a
a', Spec (b, c)
b') = TypeSpec (a, b, c) -> Spec (a, b, c)
forall a. HasSpec a => TypeSpec a -> Spec a
guardTypeSpec (Spec a
a Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
a', Spec (b, c)
b Spec (b, c) -> Spec (b, c) -> Spec (b, c)
forall a. Semigroup a => a -> a -> a
<> Spec (b, c)
b')

  conformsTo :: HasCallStack => (a, b, c) -> TypeSpec (a, b, c) -> Bool
conformsTo (a
a, b
b, c
c) (Spec a
sa, Spec (b, c)
sbc) = a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
a Spec a
sa Bool -> Bool -> Bool
&& (b, c) -> Spec (b, c) -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec (b
b, c
c) Spec (b, c)
sbc

  guardTypeSpec :: TypeSpec (a, b, c) -> Spec (a, b, c)
guardTypeSpec (Spec a
a, Spec (b, c)
bc) =
    Spec a
-> Spec (b, c)
-> (Spec a -> Spec (b, c) -> Spec (a, b, c))
-> Spec (a, b, c)
forall a b c.
Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c
handleErrors
      Spec a
a
      Spec (b, c)
bc
      ( \Spec a
x Spec (b, c)
y -> case (Spec a
x :: Spec a, Spec (b, c)
y :: Spec (b, c)) of
          (MemberSpec NonEmpty a
xs, MemberSpec NonEmpty (b, c)
ys) ->
            -- Given two MemberSpec, build one MemberSpec, by joining all combinations
            NonEmpty (a, b, c) -> Spec (a, b, c)
forall a. NonEmpty a -> Spec a
MemberSpec
              ( [(a, b, c)] -> NonEmpty (a, b, c)
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                  [ (a
a', b
b', c
c')
                  | a
a' <- NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs
                  , (b
b', c
c') <- NonEmpty (b, c) -> [(b, c)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (b, c)
ys
                  ]
              )
          (Spec a
specA, Spec (b, c)
specBC) -> (Term (a, b, c) -> Pred) -> Spec (a, b, c)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (a, b, c) -> Pred) -> Spec (a, b, c))
-> (Term (a, b, c) -> Pred) -> Spec (a, b, c)
forall a b. (a -> b) -> a -> b
$ \Term (a, b, c)
p -> [Pred] -> Pred
And [Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c) -> Term a
forall a b c. All HasSpec '[a, b, c] => Term (a, b, c) -> Term a
head3_ Term (a, b, c)
p) Spec a
specA, Term (b, c) -> Spec (b, c) -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c) -> Term (b, c)
forall a b c.
All HasSpec '[a, b, c] =>
Term (a, b, c) -> Term (b, c)
tail3_ Term (a, b, c)
p) Spec (b, c)
specBC]
      )

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (a, b, c) -> GenT m (a, b, c)
genFromTypeSpec (Spec a
a, Spec (b, c)
bc) = a -> (b, c) -> (a, b, c)
forall {a} {b} {c}. a -> (b, c) -> (a, b, c)
f (a -> (b, c) -> (a, b, c))
-> GenT m a -> GenT m ((b, c) -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
a GenT m ((b, c) -> (a, b, c)) -> GenT m (b, c) -> GenT m (a, b, c)
forall a b. GenT m (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Spec (b, c) -> GenT m (b, c)
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec (b, c)
bc
    where
      f :: a -> (b, c) -> (a, b, c)
f a
a' (b
b', c
c') = (a
a', b
b', c
c')

  toPreds :: Term (a, b, c) -> TypeSpec (a, b, c) -> Pred
toPreds Term (a, b, c)
x (Spec a
a, Spec (b, c)
bc) = Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c) -> Term a
forall a b c. All HasSpec '[a, b, c] => Term (a, b, c) -> Term a
head3_ Term (a, b, c)
x) Spec a
a Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term (b, c) -> Spec (b, c) -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c) -> Term (b, c)
forall a b c.
All HasSpec '[a, b, c] =>
Term (a, b, c) -> Term (b, c)
tail3_ Term (a, b, c)
x) Spec (b, c)
bc

head3_ :: All HasSpec '[a, b, c] => Term (a, b, c) -> Term a
head3_ :: forall a b c. All HasSpec '[a, b, c] => Term (a, b, c) -> Term a
head3_ Term (a, b, c)
x = TupleSym '[(a, b, c)] a -> List Term '[(a, b, c)] -> Term a
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App TupleSym '[(a, b, c)] a
forall a a b. All HasSpec '[a, a, b] => TupleSym '[(a, a, b)] a
Head3W (Term (a, b, c)
x Term (a, b, c) -> List Term '[] -> List Term '[(a, b, c)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

tail3_ :: All HasSpec '[a, b, c] => Term (a, b, c) -> Term (b, c)
tail3_ :: forall a b c.
All HasSpec '[a, b, c] =>
Term (a, b, c) -> Term (b, c)
tail3_ Term (a, b, c)
x = TupleSym '[(a, b, c)] (b, c)
-> List Term '[(a, b, c)] -> Term (b, c)
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App TupleSym '[(a, b, c)] (b, c)
forall a b c.
All HasSpec '[a, b, c] =>
TupleSym '[(a, b, c)] (b, c)
Tail3W (Term (a, b, c)
x Term (a, b, c) -> List Term '[] -> List Term '[(a, b, c)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- =======================================================

instance (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => HasSpec (a, b, c, d) where
  type TypeSpec (a, b, c, d) = (Spec a, Spec (b, c, d))

  anySpec :: TypeSpec (a, b, c, d)
anySpec = (forall a. Monoid a => a
mempty @(Spec a), forall a. Monoid a => a
mempty @(Spec (b, c, d)))

  combineSpec :: TypeSpec (a, b, c, d) -> TypeSpec (a, b, c, d) -> Spec (a, b, c, d)
combineSpec (Spec a
a, Spec (b, c, d)
bcd) (Spec a
a', Spec (b, c, d)
bcd') = TypeSpec (a, b, c, d) -> Spec (a, b, c, d)
forall a. HasSpec a => TypeSpec a -> Spec a
guardTypeSpec (Spec a
a Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
a', Spec (b, c, d)
bcd Spec (b, c, d) -> Spec (b, c, d) -> Spec (b, c, d)
forall a. Semigroup a => a -> a -> a
<> Spec (b, c, d)
bcd')

  conformsTo :: HasCallStack => (a, b, c, d) -> TypeSpec (a, b, c, d) -> Bool
conformsTo (a
a, b
b, c
c, d
d) (Spec a
sA, Spec (b, c, d)
sBCD) = a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
a Spec a
sA Bool -> Bool -> Bool
&& (b, c, d) -> Spec (b, c, d) -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec (b
b, c
c, d
d) Spec (b, c, d)
sBCD

  guardTypeSpec :: TypeSpec (a, b, c, d) -> Spec (a, b, c, d)
guardTypeSpec (Spec a
a, Spec (b, c, d)
bcd) =
    Spec a
-> Spec (b, c, d)
-> (Spec a -> Spec (b, c, d) -> Spec (a, b, c, d))
-> Spec (a, b, c, d)
forall a b c.
Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c
handleErrors
      Spec a
a
      Spec (b, c, d)
bcd
      ( \Spec a
x Spec (b, c, d)
y -> case (Spec a
x, Spec (b, c, d)
y) of
          (MemberSpec NonEmpty a
xs, MemberSpec NonEmpty (b, c, d)
ys) ->
            NonEmpty (a, b, c, d) -> Spec (a, b, c, d)
forall a. NonEmpty a -> Spec a
MemberSpec
              ( [(a, b, c, d)] -> NonEmpty (a, b, c, d)
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                  [ (a
s, b
b, c
c, d
d)
                  | a
s <- NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs
                  , (b
b, c
c, d
d) <- NonEmpty (b, c, d) -> [(b, c, d)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (b, c, d)
ys
                  ]
              )
          (Spec a
specA, Spec (b, c, d)
specBCD) -> (Term (a, b, c, d) -> Pred) -> Spec (a, b, c, d)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (a, b, c, d) -> Pred) -> Spec (a, b, c, d))
-> (Term (a, b, c, d) -> Pred) -> Spec (a, b, c, d)
forall a b. (a -> b) -> a -> b
$ \Term (a, b, c, d)
ps -> [Pred] -> Pred
And [Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c, d) -> Term a
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term a
head4_ Term (a, b, c, d)
ps) Spec a
specA, Term (b, c, d) -> Spec (b, c, d) -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c, d) -> Term (b, c, d)
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term (b, c, d)
tail4_ Term (a, b, c, d)
ps) Spec (b, c, d)
specBCD]
      )

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (a, b, c, d) -> GenT m (a, b, c, d)
genFromTypeSpec (Spec a
a, Spec (b, c, d)
bcd) = a -> (b, c, d) -> (a, b, c, d)
forall {a} {b} {c} {d}. a -> (b, c, d) -> (a, b, c, d)
f (a -> (b, c, d) -> (a, b, c, d))
-> GenT m a -> GenT m ((b, c, d) -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
a GenT m ((b, c, d) -> (a, b, c, d))
-> GenT m (b, c, d) -> GenT m (a, b, c, d)
forall a b. GenT m (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Spec (b, c, d) -> GenT m (b, c, d)
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec (b, c, d)
bcd
    where
      f :: a -> (b, c, d) -> (a, b, c, d)
f a
a' (b
b, c
c, d
d) = (a
a', b
b, c
c, d
d)

  toPreds :: Term (a, b, c, d) -> TypeSpec (a, b, c, d) -> Pred
toPreds Term (a, b, c, d)
x (Spec a
a, Spec (b, c, d)
bcd) = Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c, d) -> Term a
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term a
head4_ Term (a, b, c, d)
x) Spec a
a Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term (b, c, d) -> Spec (b, c, d) -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (a, b, c, d) -> Term (b, c, d)
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term (b, c, d)
tail4_ Term (a, b, c, d)
x) Spec (b, c, d)
bcd

head4_ :: All HasSpec '[a, b, c, d] => Term (a, b, c, d) -> Term a
head4_ :: forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term a
head4_ Term (a, b, c, d)
x = TupleSym '[(a, b, c, d)] a -> List Term '[(a, b, c, d)] -> Term a
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App TupleSym '[(a, b, c, d)] a
forall a a b c.
All HasSpec '[a, a, b, c] =>
TupleSym '[(a, a, b, c)] a
Head4W (Term (a, b, c, d)
x Term (a, b, c, d) -> List Term '[] -> List Term '[(a, b, c, d)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

tail4_ :: All HasSpec '[a, b, c, d] => Term (a, b, c, d) -> Term (b, c, d)
tail4_ :: forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term (b, c, d)
tail4_ Term (a, b, c, d)
x = TupleSym '[(a, b, c, d)] (b, c, d)
-> List Term '[(a, b, c, d)] -> Term (b, c, d)
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App TupleSym '[(a, b, c, d)] (b, c, d)
forall a b c d.
All HasSpec '[a, b, c, d] =>
TupleSym '[(a, b, c, d)] (b, c, d)
Tail4W (Term (a, b, c, d)
x Term (a, b, c, d) -> List Term '[] -> List Term '[(a, b, c, d)]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

-- ======================================================================
-- We need some function symbols, to break Bigger tuples into sub-tuples

data TupleSym (ds :: [Type]) r where
  Head3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] a
  Tail3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] (b, c)
  Head4W :: All HasSpec '[a, b, c, d] => TupleSym '[(a, b, c, d)] a
  Tail4W :: All HasSpec '[a, b, c, d] => TupleSym '[(a, b, c, d)] (b, c, d)

deriving instance Eq (TupleSym ds r)

instance Show (TupleSym ds r) where show :: TupleSym ds r -> String
show = TupleSym ds r -> String
forall (ds :: [*]) r. TupleSym ds r -> String
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> String
name

instance Syntax TupleSym where
  inFix :: forall (dom :: [*]) rng. TupleSym dom rng -> Bool
inFix TupleSym dom rng
_ = Bool
False
  name :: forall (ds :: [*]) r. TupleSym ds r -> String
name TupleSym dom rng
Head3W = String
"head3_"
  name TupleSym dom rng
Tail3W = String
"tail3_"
  name TupleSym dom rng
Head4W = String
"head4_"
  name TupleSym dom rng
Tail4W = String
"tail4_"

instance Semantics TupleSym where
  semantics :: forall (d :: [*]) r. TupleSym d r -> FunTy d r
semantics TupleSym d r
Head3W = \(r
a, b
_b, c
_c) -> r
a
  semantics TupleSym d r
Tail3W = \(a
_a, b
b, c
c) -> (b
b, c
c)
  semantics TupleSym d r
Head4W = \(r
a, b
_b, c
_c, d
_d) -> r
a
  semantics TupleSym d r
Tail4W = \(a
_a, b
b, c
c, d
d) -> (b
b, c
c, d
d)

instance Logic TupleSym where
  propagate :: forall (as :: [*]) b a.
(AppRequires TupleSym as b, HasSpec a) =>
TupleSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate TupleSym as b
_ ListCtx as (HOLE a)
_ Spec b
TrueSpec = Spec a
forall a. Spec a
TrueSpec
  propagate TupleSym as b
_ ListCtx as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
msgs
  propagate TupleSym as b
symW (Unary HOLE a a
HOLE) (SuspendedSpec Var b
v Pred
ps) =
    (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> Term b -> Binder b -> Pred
forall a. Term a -> Binder a -> Pred
Let (TupleSym as b -> List Term as -> Term b
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App TupleSym as b
symW (Term a
v' Term a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
v Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate TupleSym as b
Head3W (Unary HOLE a a
HOLE) Spec b
specA = Spec b -> Spec (b, b, c)
forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec a -> Spec (a, b, c)
anyTail3 Spec b
specA
  propagate TupleSym as b
Tail3W (Unary HOLE a a
HOLE) Spec b
specBC = Spec (b, c) -> Spec (a, b, c)
forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec (b, c) -> Spec (a, b, c)
anyHead3 Spec b
Spec (b, c)
specBC
  propagate TupleSym as b
Head4W (Unary HOLE a a
HOLE) Spec b
specA = Spec b -> Spec (b, b, c, d)
forall a b c d.
(HasSpec a, HasSpec b, HasSpec c, HasSpec d) =>
Spec a -> Spec (a, b, c, d)
anyTail4 Spec b
specA
  propagate TupleSym as b
Tail4W (Unary HOLE a a
HOLE) Spec b
specBCD = Spec (b, c, d) -> Spec (a, b, c, d)
forall a b c d.
(HasSpec a, HasSpec b, HasSpec c, HasSpec d) =>
Spec (b, c, d) -> Spec (a, b, c, d)
anyHead4 Spec b
Spec (b, c, d)
specBCD

anyHead3 :: forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec (b, c) -> Spec (a, b, c)
anyHead3 :: forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec (b, c) -> Spec (a, b, c)
anyHead3 Spec (b, c)
specBC = forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec @(a, b, c) (forall a. Monoid a => a
mempty @(Spec a), Spec (b, c)
specBC)

anyTail3 :: forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec a -> Spec (a, b, c)
anyTail3 :: forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec a -> Spec (a, b, c)
anyTail3 Spec a
specA = TypeSpec (a, b, c) -> Spec (a, b, c)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Spec a
specA, forall a. Monoid a => a
mempty @(Spec (b, c)))

anyHead4 ::
  forall a b c d. (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => Spec (b, c, d) -> Spec (a, b, c, d)
anyHead4 :: forall a b c d.
(HasSpec a, HasSpec b, HasSpec c, HasSpec d) =>
Spec (b, c, d) -> Spec (a, b, c, d)
anyHead4 Spec (b, c, d)
specBCD = TypeSpec (a, b, c, d) -> Spec (a, b, c, d)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (forall a. Monoid a => a
mempty @(Spec a), Spec (b, c, d)
specBCD)

anyTail4 ::
  forall a b c d. (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => Spec a -> Spec (a, b, c, d)
anyTail4 :: forall a b c d.
(HasSpec a, HasSpec b, HasSpec c, HasSpec d) =>
Spec a -> Spec (a, b, c, d)
anyTail4 Spec a
specA = TypeSpec (a, b, c, d) -> Spec (a, b, c, d)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (Spec a
specA, forall a. Monoid a => a
mempty @(Spec (b, c, d)))

-- ======================================================================
-- The Match class, with function `match` makes using all tuples uniform
-- For any n-tuple, supply `match` with an n-ary function to bring into
-- scope 'n' variables with type Term, which can be used to make Pred
-- Note how the binary case is the inductive step, and the others just
-- call the `match` with one less item in the tuple.

class Match t (ts :: [Type]) | t -> ts where
  match :: All HasSpec ts => Term t -> FunTy (MapList Term ts) Pred -> Pred

-- Base case where binary tuple.
instance Match (a, b) '[a, b] where
  match :: All HasSpec '[a, b] =>
Term (a, b) -> FunTy (MapList Term '[a, b]) Pred -> Pred
match Term (a, b)
ab FunTy (MapList Term '[a, b]) Pred
f =
    Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let
      (Term (a, b) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term a
fst_ Term (a, b)
ab)
      ( (Term a -> Pred) -> Binder a
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term a -> Pred) -> Binder a) -> (Term a -> Pred) -> Binder a
forall a b. (a -> b) -> a -> b
$ \Term a
ft ->
          Term b -> Binder b -> Pred
forall a. Term a -> Binder a -> Pred
Let (Term (a, b) -> Term b
forall a b. (HasSpec a, HasSpec b) => Term (a, b) -> Term b
snd_ Term (a, b)
ab) ((Term b -> Pred) -> Binder b
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term b -> Pred) -> Binder b) -> (Term b -> Pred) -> Binder b
forall a b. (a -> b) -> a -> b
$ \Term b
st -> FunTy (MapList Term '[a, b]) Pred
Term a -> Term b -> Pred
f Term a
ft Term b
st)
      )

-- Inductive case for ternary tuple, calls 'match' for binary tuple.
instance Match (a, b, c) '[a, b, c] where
  match :: All HasSpec '[a, b, c] =>
Term (a, b, c) -> FunTy (MapList Term '[a, b, c]) Pred -> Pred
match Term (a, b, c)
abc FunTy (MapList Term '[a, b, c]) Pred
f =
    Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let
      (Term (a, b, c) -> Term a
forall a b c. All HasSpec '[a, b, c] => Term (a, b, c) -> Term a
head3_ Term (a, b, c)
abc)
      ( (Term a -> Pred) -> Binder a
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term a -> Pred) -> Binder a) -> (Term a -> Pred) -> Binder a
forall a b. (a -> b) -> a -> b
$ \Term a
a ->
          Term (b, c) -> Binder (b, c) -> Pred
forall a. Term a -> Binder a -> Pred
Let
            (Term (a, b, c) -> Term (b, c)
forall a b c.
All HasSpec '[a, b, c] =>
Term (a, b, c) -> Term (b, c)
tail3_ Term (a, b, c)
abc)
            ((Term (b, c) -> Pred) -> Binder (b, c)
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term (b, c) -> Pred) -> Binder (b, c))
-> (Term (b, c) -> Pred) -> Binder (b, c)
forall a b. (a -> b) -> a -> b
$ \Term (b, c)
bc -> forall t (ts :: [*]).
(Match t ts, All HasSpec ts) =>
Term t -> FunTy (MapList Term ts) Pred -> Pred
match @(b, c) Term (b, c)
bc (FunTy (MapList Term '[a, b, c]) Pred
Term a -> Term b -> Term c -> Pred
f Term a
a))
      )

-- Inductive case for quadary tuple, calls 'match' for ternary tuple.
instance Match (a, b, c, d) '[a, b, c, d] where
  match :: All HasSpec '[a, b, c, d] =>
Term (a, b, c, d)
-> FunTy (MapList Term '[a, b, c, d]) Pred -> Pred
match Term (a, b, c, d)
abcd FunTy (MapList Term '[a, b, c, d]) Pred
f =
    Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let
      (Term (a, b, c, d) -> Term a
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term a
head4_ Term (a, b, c, d)
abcd)
      ( (Term a -> Pred) -> Binder a
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term a -> Pred) -> Binder a) -> (Term a -> Pred) -> Binder a
forall a b. (a -> b) -> a -> b
$ \Term a
a ->
          Term (b, c, d) -> Binder (b, c, d) -> Pred
forall a. Term a -> Binder a -> Pred
Let
            (Term (a, b, c, d) -> Term (b, c, d)
forall a b c d.
All HasSpec '[a, b, c, d] =>
Term (a, b, c, d) -> Term (b, c, d)
tail4_ Term (a, b, c, d)
abcd)
            ((Term (b, c, d) -> Pred) -> Binder (b, c, d)
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind ((Term (b, c, d) -> Pred) -> Binder (b, c, d))
-> (Term (b, c, d) -> Pred) -> Binder (b, c, d)
forall a b. (a -> b) -> a -> b
$ \Term (b, c, d)
bcd -> forall t (ts :: [*]).
(Match t ts, All HasSpec ts) =>
Term t -> FunTy (MapList Term ts) Pred -> Pred
match @(b, c, d) Term (b, c, d)
bcd (FunTy (MapList Term '[a, b, c, d]) Pred
Term a -> Term b -> Term c -> Term d -> Pred
f Term a
a))
      )

-- =========================================================
-- Here are some examples, Notice how the arity of the function
-- passed to `match` changes as the width of the tuples changes.

spec2 :: Spec (Integer, Integer)
spec2 :: Spec (Integer, Integer)
spec2 = (Term (Integer, Integer) -> Pred) -> Spec (Integer, Integer)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (Integer, Integer) -> Pred) -> Spec (Integer, Integer))
-> (Term (Integer, Integer) -> Pred) -> Spec (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Term (Integer, Integer)
x ->
  Term (Integer, Integer)
-> FunTy (MapList Term '[Integer, Integer]) Pred -> Pred
forall t (ts :: [*]).
(Match t ts, All HasSpec ts) =>
Term t -> FunTy (MapList Term ts) Pred -> Pred
match Term (Integer, Integer)
x (FunTy (MapList Term '[Integer, Integer]) Pred -> Pred)
-> FunTy (MapList Term '[Integer, Integer]) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Integer
a Term Integer
b -> Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
a Term Integer -> Term Integer -> Term Bool
<=. Term Integer
b

spec3 :: Spec (Integer, Integer, Integer)
spec3 :: Spec (Integer, Integer, Integer)
spec3 = (Term (Integer, Integer, Integer) -> Pred)
-> Spec (Integer, Integer, Integer)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (Integer, Integer, Integer) -> Pred)
 -> Spec (Integer, Integer, Integer))
-> (Term (Integer, Integer, Integer) -> Pred)
-> Spec (Integer, Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Term (Integer, Integer, Integer)
v4 ->
  Term (Integer, Integer, Integer)
-> FunTy (MapList Term '[Integer, Integer, Integer]) Pred -> Pred
forall t (ts :: [*]).
(Match t ts, All HasSpec ts) =>
Term t -> FunTy (MapList Term ts) Pred -> Pred
match Term (Integer, Integer, Integer)
v4 (FunTy (MapList Term '[Integer, Integer, Integer]) Pred -> Pred)
-> FunTy (MapList Term '[Integer, Integer, Integer]) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Integer
v3 Term Integer
v1 Term Integer
v0 -> [Pred] -> Pred
And [Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
v3 Term Integer -> Term Integer -> Term Bool
<=. Term Integer
v1, Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
v1 Term Integer -> Term Integer -> Term Bool
<=. Term Integer
v0]

spec4 :: Spec (Integer, Integer, Integer, Integer)
spec4 :: Spec (Integer, Integer, Integer, Integer)
spec4 = (Term (Integer, Integer, Integer, Integer) -> Pred)
-> Spec (Integer, Integer, Integer, Integer)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (Integer, Integer, Integer, Integer) -> Pred)
 -> Spec (Integer, Integer, Integer, Integer))
-> (Term (Integer, Integer, Integer, Integer) -> Pred)
-> Spec (Integer, Integer, Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Term (Integer, Integer, Integer, Integer)
x ->
  Term (Integer, Integer, Integer, Integer)
-> FunTy (MapList Term '[Integer, Integer, Integer, Integer]) Pred
-> Pred
forall t (ts :: [*]).
(Match t ts, All HasSpec ts) =>
Term t -> FunTy (MapList Term ts) Pred -> Pred
match Term (Integer, Integer, Integer, Integer)
x (FunTy (MapList Term '[Integer, Integer, Integer, Integer]) Pred
 -> Pred)
-> FunTy (MapList Term '[Integer, Integer, Integer, Integer]) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Integer
a Term Integer
b Term Integer
c Term Integer
d -> [Pred] -> Pred
And [Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
a Term Integer -> Term Integer -> Term Bool
<=. Term Integer
b, Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
b Term Integer -> Term Integer -> Term Bool
<=. Term Integer
c, Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Integer
c Term Integer -> Term Integer -> Term Bool
<=. Term Integer
d]

-- ========================================================

{-
class TypeList ts where
  uncurryList :: FunTy (MapList f ts) r -> List f ts -> r
  uncurryList_ :: (forall a. f a -> a)
                  -> FunTy ts r -> List f ts -> r
  curryList :: (List f ts -> r) -> FunTy (MapList f ts) r
  curryList_ :: (forall a. a -> f a)
                -> (List f ts -> r) -> FunTy ts r
  unfoldList :: (forall a (as :: [*]). List f as -> f a) -> List f ts
-}

-- | Fold over a (List Term ts) with 'getTermsize' which consumes a Term component for each element of the list
ex1 :: Maybe Int
ex1 :: Maybe Int
ex1 = FunTy (MapList Term '[Int, Bool, String]) (Maybe Int)
-> List Term '[Int, Bool, String] -> Maybe Int
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
FunTy (MapList f ts) r -> List f ts -> r
forall (f :: * -> *) r.
FunTy (MapList f '[Int, Bool, String]) r
-> List f '[Int, Bool, String] -> r
uncurryList FunTy (MapList Term '[Int, Bool, String]) (Maybe Int)
Term Int -> Term Bool -> Term String -> Maybe Int
getTermsize1 List Term '[Int, Bool, String]
args1
  where
    args1 :: List Term '[Int, Bool, String]
    args1 :: List Term '[Int, Bool, String]
args1 = Int -> Term Int
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Int
5 Term Int
-> List Term '[Bool, String] -> List Term '[Int, Bool, String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Bool -> Term Bool
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
True Term Bool -> List Term '[String] -> List Term '[Bool, String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> String -> Term String
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit String
"abc" Term String -> List Term '[] -> List Term '[String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil
    getTermsize1 :: Term Int -> Term Bool -> Term String -> Maybe Int
    getTermsize1 :: Term Int -> Term Bool -> Term String -> Maybe Int
getTermsize1 (Lit Int
n) (Lit Bool
b) (Lit String
s) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ if Bool
b then Int
n else String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
    getTermsize1 Term Int
_ Term Bool
_ Term String
_ = Maybe Int
forall a. Maybe a
Nothing

-- Fold over a list with two parts 'unLit' and 'getSize'
ex2 :: Int
ex2 :: Int
ex2 = (forall a. Term a -> a)
-> FunTy '[Int, Bool, String] Int
-> List Term '[Int, Bool, String]
-> Int
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a)
-> FunTy '[Int, Bool, String] r -> List f '[Int, Bool, String] -> r
uncurryList_ Term a -> a
forall a. Term a -> a
unLit FunTy '[Int, Bool, String] Int
Int -> Bool -> String -> Int
getsize2 List Term '[Int, Bool, String]
args2
  where
    unLit :: forall a. Term a -> a
    unLit :: forall a. Term a -> a
unLit (Lit a
n) = a
n
    unLit Term a
_ = String -> a
forall a. HasCallStack => String -> a
error String
"unLit on non literal"
    getsize2 :: Int -> Bool -> String -> Int
    getsize2 :: Int -> Bool -> String -> Int
getsize2 Int
n Bool
b String
s = if Bool
b then Int
n else String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
    args2 :: List Term '[Int, Bool, String]
    args2 :: List Term '[Int, Bool, String]
args2 = Int -> Term Int
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Int
5 Term Int
-> List Term '[Bool, String] -> List Term '[Int, Bool, String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Bool -> Term Bool
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Bool
True Term Bool -> List Term '[String] -> List Term '[Bool, String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> String -> Term String
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit String
"abc" Term String -> List Term '[] -> List Term '[String]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil

-- Construct a function from a List and function on that list.
ex3 :: Term a -> Term b -> Term c -> String
ex3 :: forall a b c. Term a -> Term b -> Term c -> String
ex3 = (List Term '[a, b, c] -> String)
-> FunTy (MapList Term '[a, b, c]) String
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
forall (f :: * -> *) r.
(List f '[a, b, c] -> r) -> FunTy (MapList f '[a, b, c]) r
curryList List Term '[a, b, c] -> String
forall a b c. List Term '[a, b, c] -> String
crush
  where
    crush :: (List Term '[a, b, c] -> String)
    crush :: forall a b c. List Term '[a, b, c] -> String
crush (Term a
a :> Term a
b :> Term a
c :> List Term as1
Nil) = Term a -> String
forall a. Show a => a -> String
show Term a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
c

-- Construct a function over from a
ex4 :: Int -> Bool -> String -> Int
ex4 :: Int -> Bool -> String -> Int
ex4 = (forall a. a -> [a])
-> (List [] '[Int, Bool, String] -> Int)
-> FunTy '[Int, Bool, String] Int
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. a -> f a) -> (List f ts -> r) -> FunTy ts r
forall (f :: * -> *) r.
(forall a. a -> f a)
-> (List f '[Int, Bool, String] -> r)
-> FunTy '[Int, Bool, String] r
curryList_ a -> [a]
forall a. a -> [a]
one List [] '[Int, Bool, String] -> Int
totalLength
  where
    totalLength :: List [] '[Int, Bool, String] -> Int
    totalLength :: List [] '[Int, Bool, String] -> Int
totalLength ([a]
n :> [a]
b :> [a]
s :> List [] as1
Nil) = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
s
    one :: a -> [a]
    one :: forall a. a -> [a]
one a
x = [a
x]

ex5 :: Spec (Set Integer)
ex5 :: Spec (Set Integer)
ex5 = (Term (Set Integer) -> Pred) -> Spec (Set Integer)
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term (Set Integer) -> Pred) -> Spec (Set Integer))
-> (Term (Set Integer) -> Pred) -> Spec (Set Integer)
forall a b. (a -> b) -> a -> b
$ \Term (Set Integer)
s -> Term Bool -> Pred
Assert (Term (Set Integer) -> Term Integer
forall s. (HasSpec s, Ord s) => Term (Set s) -> Term Integer
size_ Term (Set Integer)
s Term Integer -> Term Integer -> Term Bool
forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit Integer
104)

-- ==========================================================================

data Sum3 a b c where
  Inj3_1 :: a -> Sum3 a b c
  Inj3_2 :: b -> Sum3 a b c
  Inj3_3 :: c -> Sum3 a b c

deriving instance (Show a, Show b, Show c) => Show (Sum3 a b c)

deriving instance (Eq a, Eq b, Eq c) => Eq (Sum3 a b c)

foo_ :: Term (Sum3 a b c) -> Term a
foo_ :: forall a b c. Term (Sum3 a b c) -> Term a
foo_ = Term (Sum3 a b c) -> Term a
forall a. HasCallStack => a
undefined

bar_ :: forall a b c. Term (Sum3 a b c) -> Term (Either b c)
bar_ = Term (Sum3 a b c) -> Term (Either b c)
forall a. HasCallStack => a
undefined

bar_ :: Term (Sum3 a b c) -> Term (Either b c)
guardSum3 ::
  forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec a -> Spec (Either b c) -> Spec (Sum3 a b c)
guardSum3 :: forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec a -> Spec (Either b c) -> Spec (Sum3 a b c)
guardSum3 (ErrorSpec NonEmpty String
es) (ErrorSpec NonEmpty String
fs) = NonEmpty String -> Spec (Sum3 a b c)
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String
es NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
fs)
guardSum3 (ErrorSpec NonEmpty String
es) Spec (Either b c)
_ = NonEmpty String -> Spec (Sum3 a b c)
forall a. NonEmpty String -> Spec a
ErrorSpec (String -> NonEmpty String -> NonEmpty String
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"Sum3 error on left" NonEmpty String
es)
guardSum3 Spec a
_ (ErrorSpec NonEmpty String
es) = NonEmpty String -> Spec (Sum3 a b c)
forall a. NonEmpty String -> Spec a
ErrorSpec (String -> NonEmpty String -> NonEmpty String
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"Sum3 error on right" NonEmpty String
es)
guardSum3 Spec a
s Spec (Either b c)
s' = TypeSpec (Sum3 a b c) -> Spec (Sum3 a b c)
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec (TypeSpec (Sum3 a b c) -> Spec (Sum3 a b c))
-> TypeSpec (Sum3 a b c) -> Spec (Sum3 a b c)
forall a b. (a -> b) -> a -> b
$ Spec a -> Spec (Either b c) -> SumSpec (Spec a) (Spec (Either b c))
forall a b. a -> b -> SumSpec a b
SumSpec Spec a
s Spec (Either b c)
s'

instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (Sum3 a b c) where
  type TypeSpec (Sum3 a b c) = SumSpec (Spec a) (Spec (Either b c))

  anySpec :: TypeSpec (Sum3 a b c)
anySpec = Spec a -> Spec (Either b c) -> SumSpec (Spec a) (Spec (Either b c))
forall a b. a -> b -> SumSpec a b
SumSpec Spec a
forall a. Spec a
TrueSpec Spec (Either b c)
forall a. Spec a
TrueSpec

  combineSpec :: TypeSpec (Sum3 a b c) -> TypeSpec (Sum3 a b c) -> Spec (Sum3 a b c)
combineSpec (SumSpec Spec a
x Spec (Either b c)
y) (SumSpec Spec a
a Spec (Either b c)
b) = Spec a -> Spec (Either b c) -> Spec (Sum3 a b c)
forall a b c.
(HasSpec a, HasSpec b, HasSpec c) =>
Spec a -> Spec (Either b c) -> Spec (Sum3 a b c)
guardSum3 (Spec a
x Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> Spec a
a) (Spec (Either b c)
y Spec (Either b c) -> Spec (Either b c) -> Spec (Either b c)
forall a. Semigroup a => a -> a -> a
<> Spec (Either b c)
b)

  conformsTo :: HasCallStack => Sum3 a b c -> TypeSpec (Sum3 a b c) -> Bool
conformsTo (Inj3_1 a
a) (SumSpec Spec a
as Spec (Either b c)
_) = a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
a Spec a
as
  conformsTo (Inj3_2 b
b) (SumSpec Spec a
_ Spec (Either b c)
es) = Either b c -> Spec (Either b c) -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec (b -> Either b c
forall a b. a -> Either a b
Left b
b) Spec (Either b c)
es
  conformsTo (Inj3_3 c
c) (SumSpec Spec a
_ Spec (Either b c)
es) = Either b c -> Spec (Either b c) -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec (c -> Either b c
forall a b. b -> Either a b
Right c
c) Spec (Either b c)
es

  toPreds :: Term (Sum3 a b c) -> TypeSpec (Sum3 a b c) -> Pred
toPreds Term (Sum3 a b c)
x (SumSpec Spec a
a Spec (Either b c)
es) = Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (Sum3 a b c) -> Term a
forall a b c. Term (Sum3 a b c) -> Term a
foo_ Term (Sum3 a b c)
x) Spec a
a Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term (Either b c) -> Spec (Either b c) -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Term (Sum3 a b c) -> Term (Either b c)
forall a b c. Term (Sum3 a b c) -> Term (Either b c)
bar_ Term (Sum3 a b c)
x) Spec (Either b c)
es

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Sum3 a b c) -> GenT m (Sum3 a b c)
genFromTypeSpec (SumSpec (Spec a -> Spec a
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec a
sa) (Spec (Either b c) -> Spec (Either b c)
forall a. HasSpec a => Spec a -> Spec a
simplifySpec -> Spec (Either b c)
sb))
    | Bool
emptyA, Bool
emptyB = String -> GenT m (Sum3 a b c)
forall (m :: * -> *) a. MonadGenError m => String -> m a
genError String
"genFromTypeSpec @SumSpec: empty"
    | Bool
emptyA = a -> Sum3 a b c
forall a b c. a -> Sum3 a b c
Inj3_1 (a -> Sum3 a b c) -> GenT m a -> GenT m (Sum3 a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
sa
    | Bool
emptyB = Either b c -> Sum3 a b c
select (Either b c -> Sum3 a b c)
-> GenT m (Either b c) -> GenT m (Sum3 a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec (Either b c) -> GenT m (Either b c)
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec (Either b c)
sb
    | Bool
otherwise = [GenT GE (Sum3 a b c)] -> GenT m (Sum3 a b c)
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT [a -> Sum3 a b c
forall a b c. a -> Sum3 a b c
Inj3_1 (a -> Sum3 a b c) -> GenT GE a -> GenT GE (Sum3 a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec a
sa, Either b c -> Sum3 a b c
select (Either b c -> Sum3 a b c)
-> GenT GE (Either b c) -> GenT GE (Sum3 a b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec (Either b c) -> GenT GE (Either b c)
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Spec a -> GenT m a
genFromSpecT Spec (Either b c)
sb]
    where
      emptyA :: Bool
emptyA = Spec a -> Bool
forall a. Spec a -> Bool
isErrorLike Spec a
sa
      emptyB :: Bool
emptyB = Spec (Either b c) -> Bool
forall a. Spec a -> Bool
isErrorLike Spec (Either b c)
sb
      select :: Either b c -> Sum3 a b c
      select :: Either b c -> Sum3 a b c
select (Left b
x) = b -> Sum3 a b c
forall b a c. b -> Sum3 a b c
Inj3_2 b
x
      select (Right c
x) = c -> Sum3 a b c
forall c a b. c -> Sum3 a b c
Inj3_3 c
x

-- ====================================================

coerce_ :: Term (E3 a b c) -> Term (Either a (Either b c))
coerce_ :: forall a b c. Term (E3 a b c) -> Term (Either a (Either b c))
coerce_ = Term (E3 a b c) -> Term (Either a (Either b c))
forall a. HasCallStack => a
undefined

newtype E3 a b c = E3 (Either a (Either b c))
  deriving (E3 a b c -> E3 a b c -> Bool
(E3 a b c -> E3 a b c -> Bool)
-> (E3 a b c -> E3 a b c -> Bool) -> Eq (E3 a b c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b c. (Eq a, Eq b, Eq c) => E3 a b c -> E3 a b c -> Bool
$c== :: forall a b c. (Eq a, Eq b, Eq c) => E3 a b c -> E3 a b c -> Bool
== :: E3 a b c -> E3 a b c -> Bool
$c/= :: forall a b c. (Eq a, Eq b, Eq c) => E3 a b c -> E3 a b c -> Bool
/= :: E3 a b c -> E3 a b c -> Bool
Eq, Int -> E3 a b c -> ShowS
[E3 a b c] -> ShowS
E3 a b c -> String
(Int -> E3 a b c -> ShowS)
-> (E3 a b c -> String) -> ([E3 a b c] -> ShowS) -> Show (E3 a b c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b c. (Show a, Show b, Show c) => Int -> E3 a b c -> ShowS
forall a b c. (Show a, Show b, Show c) => [E3 a b c] -> ShowS
forall a b c. (Show a, Show b, Show c) => E3 a b c -> String
$cshowsPrec :: forall a b c. (Show a, Show b, Show c) => Int -> E3 a b c -> ShowS
showsPrec :: Int -> E3 a b c -> ShowS
$cshow :: forall a b c. (Show a, Show b, Show c) => E3 a b c -> String
show :: E3 a b c -> String
$cshowList :: forall a b c. (Show a, Show b, Show c) => [E3 a b c] -> ShowS
showList :: [E3 a b c] -> ShowS
Show) via Either a (Either b c)

{-
instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (E3 a b c) where
   type TypeSpec (E3 a b c) = TypeSpec (Either a (Either b c))

   anySpec = SumSpec TrueSpec TrueSpec

   combineSpec (SumSpec x y) (SumSpec a b) = typeSpec (SumSpec (x <> a) (y <> b))

   conformsTo (E3 (Left x)) (SumSpec a b) = conformsToSpec x a
   conformsTo (E3 (Right x)) (SumSpec a b) = conformsToSpec x b

   toPreds x (SumSpec a b) = Case (coerce_ x)
                                  (bind $ \y -> satisfies y a)
                                  (bind $ \y -> satisfies y b)

flipp :: (Eq b, Typeable b, Show b, HasSpec b, Coercible a b) => Term a -> Term b
flipp (Lit x) = Lit (coerce x)
flipp (V x) = V (coerce x)
-- flipp (App c xs) = App (coerce c) xs
-}