{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

module Constrained.Spec.Pairs where

import Constrained.Base
import Constrained.Core
import Constrained.List
import Constrained.Univ
import Data.List (nub)
import qualified Data.List.NonEmpty as NE
import Prettyprinter
import Test.QuickCheck

-- HasSpec ----------------------------------------------------------------

cartesian ::
  (HasSpec fn a, HasSpec fn b) =>
  Specification fn a ->
  Specification fn b ->
  Specification fn (Prod a b)
cartesian :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Specification fn a
-> Specification fn b -> Specification fn (Prod a b)
cartesian (ErrorSpec NonEmpty String
es) (ErrorSpec NonEmpty String
fs) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (NonEmpty String
es forall a. Semigroup a => a -> a -> a
<> NonEmpty String
fs)
cartesian (ErrorSpec NonEmpty String
es) Specification fn b
_ = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"cartesian left" NonEmpty String
es)
cartesian Specification fn a
_ (ErrorSpec NonEmpty String
es) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"cartesian right" NonEmpty String
es)
cartesian Specification fn a
s Specification fn b
s' = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian Specification fn a
s Specification fn b
s'

data PairSpec fn a b = Cartesian (Specification fn a) (Specification fn b)

instance (Arbitrary (Specification fn a), Arbitrary (Specification fn b)) => Arbitrary (PairSpec fn a b) where
  arbitrary :: Gen (PairSpec fn a b)
arbitrary = forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
  shrink :: PairSpec fn a b -> [PairSpec fn a b]
shrink (Cartesian Specification fn a
a Specification fn b
b) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink (Specification fn a
a, Specification fn b
b)

instance (HasSpec fn a, HasSpec fn b) => HasSpec fn (Prod a b) where
  type TypeSpec fn (Prod a b) = PairSpec fn a b

  type Prerequisites fn (Prod a b) = (HasSpec fn a, HasSpec fn b)

  emptySpec :: TypeSpec fn (Prod a b)
emptySpec = forall (fn :: [*] -> * -> *) a b.
Specification fn a -> Specification fn b -> PairSpec fn a b
Cartesian forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

  combineSpec :: TypeSpec fn (Prod a b)
-> TypeSpec fn (Prod a b) -> Specification fn (Prod a b)
combineSpec (Cartesian Specification fn a
a Specification fn b
b) (Cartesian Specification fn a
a' Specification fn b
b') = forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Specification fn a
-> Specification fn b -> Specification fn (Prod a b)
cartesian (Specification fn a
a forall a. Semigroup a => a -> a -> a
<> Specification fn a
a') (Specification fn b
b forall a. Semigroup a => a -> a -> a
<> Specification fn b
b')

  conformsTo :: HasCallStack => Prod a b -> TypeSpec fn (Prod a b) -> Bool
conformsTo (Prod a
a b
b) (Cartesian Specification fn a
sa Specification fn b
sb) = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec a
a Specification fn a
sa Bool -> Bool -> Bool
&& forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec b
b Specification fn b
sb

  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec fn (Prod a b) -> GenT m (Prod a b)
genFromTypeSpec (Cartesian Specification fn a
sa Specification fn b
sb) = forall a b. a -> b -> Prod a b
Prod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
sa forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn b
sb

  shrinkWithTypeSpec :: TypeSpec fn (Prod a b) -> Prod a b -> [Prod a b]
shrinkWithTypeSpec (Cartesian Specification fn a
sa Specification fn b
sb) (Prod a
a b
b) =
    [forall a b. a -> b -> Prod a b
Prod a
a' b
b | a
a' <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
sa a
a]
      forall a. [a] -> [a] -> [a]
++ [forall a b. a -> b -> Prod a b
Prod a
a b
b' | b
b' <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn b
sb b
b]

  toPreds :: Term fn (Prod a b) -> TypeSpec fn (Prod a b) -> Pred fn
toPreds Term fn (Prod a b)
x (Cartesian Specification fn a
sf Specification fn b
ss) =
    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn Term fn (Prod a b)
x) Specification fn a
sf
      forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn Term fn (Prod a b)
x) Specification fn b
ss

  cardinalTypeSpec :: TypeSpec fn (Prod a b) -> Specification fn Integer
cardinalTypeSpec (Cartesian Specification fn a
x Specification fn b
y) = forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Specification fn Integer
-> Specification fn Integer -> Specification fn Integer
multSpecInt (forall (fn :: [*] -> * -> *) a.
(Eq a, BaseUniverse fn, HasSpec fn a) =>
Specification fn a -> Specification fn Integer
cardinality Specification fn a
x) (forall (fn :: [*] -> * -> *) a.
(Eq a, BaseUniverse fn, HasSpec fn a) =>
Specification fn a -> Specification fn Integer
cardinality Specification fn b
y)

  typeSpecHasError :: TypeSpec fn (Prod a b) -> Maybe (NonEmpty String)
typeSpecHasError (Cartesian Specification fn a
x Specification fn b
y) =
    case (forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isErrorLike Specification fn a
x, forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isErrorLike Specification fn b
y) of
      (Bool
False, Bool
False) -> forall a. Maybe a
Nothing
      (Bool
True, Bool
False) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Specification fn a -> NonEmpty String
errorLikeMessage Specification fn a
x
      (Bool
False, Bool
True) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
Specification fn a -> NonEmpty String
errorLikeMessage Specification fn b
y
      (Bool
True, Bool
True) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (forall (fn :: [*] -> * -> *) a.
Specification fn a -> NonEmpty String
errorLikeMessage Specification fn a
x forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
Specification fn a -> NonEmpty String
errorLikeMessage Specification fn b
y)

  alternateShow :: TypeSpec fn (Prod a b) -> BinaryShow
alternateShow (Cartesian Specification fn a
left right :: Specification fn b
right@(TypeSpec TypeSpec fn b
r [])) =
    case forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> BinaryShow
alternateShow @fn @b TypeSpec fn b
r of
      (BinaryShow String
"Cartesian" [Doc a]
ps) -> forall a. String -> [Doc a] -> BinaryShow
BinaryShow String
"Cartesian" (Doc a
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn a
left forall a. a -> [a] -> [a]
: [Doc a]
ps)
      (BinaryShow String
"SumSpec" [Doc a]
ps) -> forall a. String -> [Doc a] -> BinaryShow
BinaryShow String
"Cartesian" (Doc a
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn a
left forall a. a -> [a] -> [a]
: [Doc a
"SumSpec" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep [Doc a]
ps])
      BinaryShow
_ -> forall a. String -> [Doc a] -> BinaryShow
BinaryShow String
"Cartesian" [Doc Any
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn a
left, Doc Any
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn b
right]
  alternateShow (Cartesian Specification fn a
left Specification fn b
right) = forall a. String -> [Doc a] -> BinaryShow
BinaryShow String
"Cartesian" [Doc Any
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn a
left, Doc Any
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Specification fn b
right]

instance (HasSpec fn a, HasSpec fn b) => Show (PairSpec fn a b) where
  show :: PairSpec fn a b -> String
show pair :: PairSpec fn a b
pair@(Cartesian Specification fn a
l Specification fn b
r) = case forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> BinaryShow
alternateShow @fn @(Prod a b) PairSpec fn a b
pair of
    (BinaryShow String
"Cartesian" [Doc a]
ps) -> forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
parens (Doc a
"Cartesian" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep [Doc a]
ps)
    BinaryShow
_ -> String
"(Cartesian " forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification fn a
l forall a. [a] -> [a] -> [a]
++ String
") (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification fn b
r forall a. [a] -> [a] -> [a]
++ String
"))"

-- Functions for working on pairs -----------------------------------------

instance BaseUniverse fn => Functions (PairFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
PairFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun PairFn fn as b
_ ListCtx Value as (HOLE a)
_ Specification fn b
TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  propagateSpecFun PairFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [] Specification fn b
s) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun PairFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun PairFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [String]
es Specification fn b
s) = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun PairFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun PairFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun PairFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec = case PairFn fn as b
fn of
    PairFn fn as b
Fst ->
      -- No TypeAbstractions in ghc-8.10
      case PairFn fn as b
fn of
        (PairFn fn '[Prod b b] b
_ :: PairFn fn '[Prod a b] a)
          | NilCtx HOLE a (Prod b b)
HOLE <- ListCtx Value as (HOLE a)
ctx
          , Evidence (Prerequisites fn (Prod b b))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Prod a b) ->
              forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Specification fn a
-> Specification fn b -> Specification fn (Prod a b)
cartesian Specification fn b
spec forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
    PairFn fn as b
Snd ->
      -- No TypeAbstractions in ghc-8.10
      case PairFn fn as b
fn of
        (PairFn fn '[Prod a b] b
_ :: PairFn fn '[Prod a b] b)
          | NilCtx HOLE a (Prod a b)
HOLE <- ListCtx Value as (HOLE a)
ctx
          , Evidence (Prerequisites fn (Prod a b))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Prod a b) ->
              forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Specification fn a
-> Specification fn b -> Specification fn (Prod a b)
cartesian forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec Specification fn b
spec
    PairFn fn as b
_
      | SuspendedSpec Var b
v Pred fn
ps <- Specification fn b
spec
      , ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf <- ListCtx Value as (HOLE a)
ctx ->
          forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
v' ->
            let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
             in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn PairFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
    PairFn fn as b
Pair
      | HOLE a a
HOLE :? Value a
b :> List Value as1
Nil <- ListCtx Value as (HOLE a)
ctx ->
          let sameSnd :: [Prod a a] -> [a]
sameSnd [Prod a a]
ps = [a
a | Prod a
a a
b' <- [Prod a a]
ps, a
b forall a. Eq a => a -> a -> Bool
== a
b']
           in case Specification fn b
spec of
                TypeSpec (Cartesian Specification fn a
sa Specification fn a
sb) OrdSet b
cant
                  | a
b forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
sb -> Specification fn a
sa forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec ([Prod a a] -> [a]
sameSnd OrdSet b
cant)
                  -- TODO: better error message
                  | Bool
otherwise ->
                      forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"propagateSpecFun (pair_ HOLE b) has conformance failure on b", forall a. Show a => a -> String
show Specification fn a
sb])
                MemberSpec NonEmpty b
es ->
                  forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty String -> Specification fn a
memberSpecList
                    (forall a. Eq a => [a] -> [a]
nub ([Prod a a] -> [a]
sameSnd (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)))
                    (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"propagateSpecFun (pair_ HOLE b) on (MemberSpec bs) where b does not appear in bs."))
      | Value a
a :! NilCtx HOLE a b
HOLE <- ListCtx Value as (HOLE a)
ctx ->
          let sameFst :: [Prod a a] -> [a]
sameFst [Prod a a]
ps = [a
b | Prod a
a' a
b <- [Prod a a]
ps, a
a forall a. Eq a => a -> a -> Bool
== a
a']
           in case Specification fn b
spec of
                TypeSpec (Cartesian Specification fn a
sa Specification fn a
sb) OrdSet b
cant
                  | a
a forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
sa -> Specification fn a
sb forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec ([Prod a a] -> [a]
sameFst OrdSet b
cant)
                  -- TODO: better error message
                  | Bool
otherwise ->
                      forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"propagateSpecFun (pair_ a HOLE) has conformance failure on a", forall a. Show a => a -> String
show Specification fn a
sa])
                MemberSpec NonEmpty b
es ->
                  forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty String -> Specification fn a
memberSpecList
                    (forall a. Eq a => [a] -> [a]
nub ([Prod a a] -> [a]
sameFst (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)))
                    (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"propagateSpecFun (pair_ a HOLE) on (MemberSpec as) where a does not appear in as."))

  rewriteRules :: forall (as :: [*]) b.
(TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) =>
PairFn fn as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules PairFn fn as b
Fst ((forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
Term fn (Prod a b) -> Maybe (Term fn a, Term fn b)
pairView -> Just (Term fn b
x, Term fn b
_)) :> List (Term fn) as1
Nil) = forall a. a -> Maybe a
Just Term fn b
x
  rewriteRules PairFn fn as b
Snd ((forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
Term fn (Prod a b) -> Maybe (Term fn a, Term fn b)
pairView -> Just (Term fn a
_, Term fn b
y)) :> List (Term fn) as1
Nil) = forall a. a -> Maybe a
Just Term fn b
y
  rewriteRules PairFn fn as b
_ List (Term fn) as
_ = forall a. Maybe a
Nothing

  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
PairFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec PairFn fn '[a] b
f TypeSpec fn a
ts = case PairFn fn '[a] b
f of
    PairFn fn '[a] b
Fst | Cartesian Specification fn b
s Specification fn b
_ <- TypeSpec fn a
ts -> Specification fn b
s
    PairFn fn '[a] b
Snd | Cartesian Specification fn a
_ Specification fn b
s <- TypeSpec fn a
ts -> Specification fn b
s

pairView ::
  forall fn a b. Member (PairFn fn) fn => Term fn (Prod a b) -> Maybe (Term fn a, Term fn b)
pairView :: forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
Term fn (Prod a b) -> Maybe (Term fn a, Term fn b)
pairView (App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fnU as b -> Maybe (fn as b)
extractFn @(PairFn fn) @fn -> Just PairFn fn as (Prod a b)
Pair) (Term fn a
x :> Term fn a
y :> List (Term fn) as1
Nil)) = forall a. a -> Maybe a
Just (Term fn a
x, Term fn a
y)
pairView Term fn (Prod a b)
_ = forall a. Maybe a
Nothing