{-# 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 #-}
#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
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
"))"
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
_ 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 ->
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 ->
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)
| 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)
| 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