{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Constrained.Spec.SumProd (
IsNormalType,
ProdAsListComputes,
IsProductType,
caseOn,
branch,
branchW,
forAll',
constrained',
reify',
con,
onCon,
isCon,
sel,
match,
onJust,
isJust,
chooseSpec,
left_,
right_,
cJust_,
cNothing_,
fst_,
snd_,
fstW,
sndW,
pair_,
injLeft_,
injRight_,
prodFst_,
prodSnd_,
prod_,
PairSpec (..),
SumW (..),
) where
import Constrained.AbstractSyntax
import Constrained.Base (
BaseW (..),
Binder,
Forallable (..),
Fun (..),
GenericRequires,
HasSpec (..),
IsPred (..),
Pred,
Specification,
Term,
appTerm,
bind,
constrained,
fromGeneric_,
toGeneric_,
)
import Constrained.Conformance (
conformsToSpec,
satisfies,
)
import Constrained.Core (
Evidence (..),
)
import Constrained.Generation
import Constrained.Generic (
ConstrOf,
HasSimpleRep (..),
Prod,
ProdOver,
SOP,
SimpleRep,
Sum,
SumOver,
TheSop,
(:::),
)
import Constrained.List (
All,
FunTy,
List (..),
MapList,
TypeList,
curryList,
listShape,
mapListC,
)
import Constrained.Syntax (
exists,
forAll,
letBind,
mkCase,
reify,
)
import Constrained.TheKnot (
FoldSpec (..),
FunW (..),
PairSpec (..),
ProdW (..),
preMapFoldSpec,
prodFst_,
prodSnd_,
prod_,
)
import Constrained.TypeErrors
import Data.Typeable (Typeable)
import GHC.Generics
import GHC.TypeLits (Symbol)
import GHC.TypeNats
import Test.QuickCheck (Arbitrary (..), oneof)
instance (Typeable a, Typeable b) => HasSimpleRep (a, b)
instance (Typeable a, Typeable b, Typeable c) => HasSimpleRep (a, b, c)
instance (Typeable a, Typeable b, Typeable c, Typeable d) => HasSimpleRep (a, b, c, d)
instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => HasSimpleRep (a, b, c, d, e)
instance
(Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g) =>
HasSimpleRep (a, b, c, d, e, g)
instance
(Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable g, Typeable h) =>
HasSimpleRep (a, b, c, d, e, g, h)
instance Typeable a => HasSimpleRep (Maybe a)
instance (Typeable a, Typeable b) => HasSimpleRep (Either a b)
instance
( HasSpec a
, HasSpec b
) =>
HasSpec (a, b)
instance
( HasSpec a
, HasSpec b
, HasSpec c
) =>
HasSpec (a, b, c)
instance
( HasSpec a
, HasSpec b
, HasSpec c
, HasSpec d
) =>
HasSpec (a, b, c, d)
instance
( HasSpec a
, HasSpec b
, HasSpec c
, HasSpec d
, HasSpec e
) =>
HasSpec (a, b, c, d, e)
instance
( HasSpec a
, HasSpec b
, HasSpec c
, HasSpec d
, HasSpec e
, HasSpec g
) =>
HasSpec (a, b, c, d, e, g)
instance
( HasSpec a
, HasSpec b
, HasSpec c
, HasSpec d
, HasSpec e
, HasSpec g
, HasSpec h
) =>
HasSpec (a, b, c, d, e, g, h)
instance
(IsNormalType a, HasSpec a) =>
HasSpec (Maybe a)
instance
( HasSpec a
, IsNormalType a
, HasSpec b
, IsNormalType b
) =>
HasSpec (Either a b)
class IsProd p where
toArgs ::
HasSpec p => Term p -> List Term (Args p)
instance {-# OVERLAPPABLE #-} Args a ~ '[a] => IsProd a where
toArgs :: HasSpec a => Term a -> List Term (Args a)
toArgs = (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)
instance IsProd b => IsProd (Prod a b) where
toArgs :: HasSpec (Prod a b) =>
Term (Prod a b) -> List Term (Args (Prod a b))
toArgs (Term (Prod a b)
p :: Term (Prod a b))
| Evidence (Prerequisites (Prod a b))
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @(Prod a b) = Term (Prod a b) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ Term (Prod a b)
p Term a -> List Term (Args b) -> List Term (a : Args b)
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term b -> List Term (Args b)
forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs (Term (Prod a b) -> Term b
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_ Term (Prod a b)
p)
type family Args t where
Args (Prod a b) = a : Args b
Args a = '[a]
type family ResultType t where
ResultType (a -> b) = ResultType b
ResultType a = a
type IsNormalType a =
( AssertComputes
(Cases a)
( Text "Failed to compute Cases in a use of IsNormalType for "
:$$: ShowType a
:<>: Text ", are you missing an IsNormalType constraint?"
)
, Cases a ~ '[a]
, AssertComputes
(Args a)
( Text "Failed to compute Args in a use of IsNormalType for "
:<>: ShowType a
:<>: Text ", are you missing an IsNormalType constraint?"
)
, Args a ~ '[a]
, IsProd a
, CountCases a ~ 1
)
type family Cases t where
Cases (Sum a b) = a : Cases b
Cases a = '[a]
type IsProductType a =
( HasSimpleRep a
, AssertComputes
(Cases (SimpleRep a))
( Text "Failed to compute Cases in a use of IsProductType for "
:$$: ShowType a
:<>: Text ", are you missing an IsProductType constraint?"
)
, Cases (SimpleRep a) ~ '[SimpleRep a]
, SimpleRep a ~ SumOver (Cases (SimpleRep a))
, IsProd (SimpleRep a)
, HasSpec (SimpleRep a)
, TypeSpec a ~ TypeSpec (SimpleRep a)
, All HasSpec (Args (SimpleRep a))
)
type ProductAsList a = Args (SimpleRep a)
class HasSpec (SOP sop) => SOPTerm c sop where
inj_ :: Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)
instance HasSpec (ProdOver constr) => SOPTerm c (c ::: constr : '[]) where
inj_ :: Term (ProdOver (ConstrOf c '[c ::: constr]))
-> Term (SOP '[c ::: constr])
inj_ = Term (ProdOver constr) -> Term (ProdOver constr)
Term (ProdOver (ConstrOf c '[c ::: constr]))
-> Term (SOP '[c ::: constr])
forall a. a -> a
id
instance
( HasSpec (SOP (con : sop))
, HasSpec (ProdOver constr)
, KnownNat (CountCases (SOP (con : sop)))
) =>
SOPTerm c (c ::: constr : con : sop)
where
inj_ :: Term (ProdOver (ConstrOf c ((c ::: constr) : con : sop)))
-> Term (SOP ((c ::: constr) : con : sop))
inj_ = Term (ProdOver constr)
-> Term (Sum (ProdOver constr) (SOP (con : sop)))
Term (ProdOver (ConstrOf c ((c ::: constr) : con : sop)))
-> Term (SOP ((c ::: constr) : con : sop))
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term a -> Term (Sum a b)
injLeft_
instance
{-# OVERLAPPABLE #-}
( HasSpec (ProdOver con)
, SOPTerm c (con' : sop)
, ConstrOf c (con' : sop) ~ ConstrOf c ((c' ::: con) : con' : sop)
, KnownNat (CountCases (SOP (con' : sop)))
) =>
SOPTerm c ((c' ::: con) : con' : sop)
where
inj_ :: Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term (SOP ((c' ::: con) : con' : sop))
inj_ = Term (SOP (con' : sop))
-> Term (Sum (ProdOver con) (SOP (con' : sop)))
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_ (Term (SOP (con' : sop))
-> Term (Sum (ProdOver con) (SOP (con' : sop))))
-> (Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term (SOP (con' : sop)))
-> Term (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term (Sum (ProdOver con) (SOP (con' : sop)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (sop :: [*]).
SOPTerm c sop =>
Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)
inj_ @c @(con' : sop)
class HasSpec (ProdOver constr) => ConstrTerm constr where
prodOver_ :: List Term constr -> Term (ProdOver constr)
instance HasSpec a => ConstrTerm '[a] where
prodOver_ :: List Term '[a] -> Term (ProdOver '[a])
prodOver_ (Term a
a :> List Term as1
Nil) = Term a
Term (ProdOver '[a])
a
type family At n as where
At 0 (a : as) = a
At n (a : as) = At (n - 1) as
class Select n as where
select_ :: Term (ProdOver as) -> Term (At n as)
instance Select 0 (a : '[]) where
select_ :: Term (ProdOver '[a]) -> Term (At 0 '[a])
select_ = Term a -> Term a
Term (ProdOver '[a]) -> Term (At 0 '[a])
forall a. a -> a
id
instance (HasSpec a, HasSpec (ProdOver (a' : as))) => Select 0 (a : a' : as) where
select_ :: Term (ProdOver (a : a' : as)) -> Term (At 0 (a : a' : as))
select_ = Term (ProdOver (a : a' : as)) -> Term (At 0 (a : a' : as))
Term (Prod a (ProdOver (a' : as))) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_
instance
{-# OVERLAPPABLE #-}
( HasSpec a
, HasSpec (ProdOver (a' : as))
, At (n - 1) (a' : as) ~ At n (a : a' : as)
, Select (n - 1) (a' : as)
) =>
Select n (a : a' : as)
where
select_ :: Term (ProdOver (a : a' : as)) -> Term (At n (a : a' : as))
select_ = forall (n :: Natural) (as :: [*]).
Select n as =>
Term (ProdOver as) -> Term (At n as)
select_ @(n - 1) @(a' : as) (Term (ProdOver (a' : as)) -> Term (At n (a : a' : as)))
-> (Term (Prod a (ProdOver (a' : as)))
-> Term (ProdOver (a' : as)))
-> Term (Prod a (ProdOver (a' : as)))
-> Term (At n (a : a' : as))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Prod a (ProdOver (a' : as))) -> Term (ProdOver (a' : as))
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_
class IsConstrOf (c :: Symbol) b sop where
mkCases ::
(HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred) ->
(Term b -> Pred) ->
List (Weighted Binder) (Cases (SOP sop))
instance
( b ~ ProdOver as
, TypeList (Cases (SOP (con : sop)))
) =>
IsConstrOf c b ((c ::: as) : con : sop)
where
mkCases :: (HasSpec b, All HasSpec (Cases (SOP ((c ::: as) : con : sop)))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP ((c ::: as) : con : sop)))
mkCases forall a. Term a -> Pred
r (Term b -> Pred
k :: Term b -> Pred) =
Maybe Int -> Binder b -> Weighted Binder b
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term b -> Pred) -> Binder b
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k)
Weighted Binder b
-> List (Weighted Binder) (Cases (SOP (con : sop)))
-> List (Weighted Binder) (b : Cases (SOP (con : sop)))
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
(g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
(g :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> List f as -> List g as
mapListC @HasSpec (\Const () a
_ -> Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> Pred
forall a. Term a -> Pred
r)) (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @(Cases (SOP (con : sop))))
instance
( b ~ ProdOver as
, IsNormalType b
) =>
IsConstrOf c b '[c ::: as]
where
mkCases :: (HasSpec b, All HasSpec (Cases (SOP '[c ::: as]))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP '[c ::: as]))
mkCases forall a. Term a -> Pred
_ (Term b -> Pred
k :: Term b -> Pred) = Maybe Int -> Binder b -> Weighted Binder b
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term b -> Pred) -> Binder b
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term b -> Pred
k) Weighted Binder b
-> List (Weighted Binder) '[] -> List (Weighted Binder) '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List (Weighted Binder) '[]
forall {k} (f :: k -> *). List f '[]
Nil
instance
{-# OVERLAPPABLE #-}
( Cases (SOP ((c' ::: as) : cs)) ~ (ProdOver as : Cases (SOP cs))
, IsConstrOf c b cs
) =>
IsConstrOf c b ((c' ::: as) : cs)
where
mkCases :: (HasSpec b, All HasSpec (Cases (SOP ((c' ::: as) : cs)))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred)
-> List (Weighted Binder) (Cases (SOP ((c' ::: as) : cs)))
mkCases forall a. Term a -> Pred
r Term b -> Pred
k = Maybe Int -> Binder (ProdOver as) -> Weighted Binder (ProdOver as)
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term (ProdOver as) -> Pred) -> Binder (ProdOver as)
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall a. Term a -> Pred
r @(ProdOver as))) Weighted Binder (ProdOver as)
-> List (Weighted Binder) (Cases (SOP cs))
-> List (Weighted Binder) (ProdOver as : Cases (SOP cs))
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @_ @cs Term a -> Pred
forall a. Term a -> Pred
r Term b -> Pred
k
fst_ :: (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ :: forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ = FunW '[(x, y)] x -> FunTy (MapList Term '[(x, y)]) (TermD Deps x)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (ProdW '[Prod x y] x
-> BaseW '[(x, y)] (Prod x y) -> FunW '[(x, y)] x
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod x y] x
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW BaseW '[(x, y)] (SimpleRep (x, y))
BaseW '[(x, y)] (Prod x y)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW)
snd_ :: (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ :: forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ = FunW '[(x, y)] y -> FunTy (MapList Term '[(x, y)]) (TermD Deps y)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (ProdW '[Prod x y] y
-> BaseW '[(x, y)] (Prod x y) -> FunW '[(x, y)] y
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod x y] y
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW BaseW '[(x, y)] (SimpleRep (x, y))
BaseW '[(x, y)] (Prod x y)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW)
fstW :: (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW :: forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW = ProdW '[Prod a b] a
-> BaseW '[(a, b)] (Prod a b) -> FunW '[(a, b)] a
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod a b] a
forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW BaseW '[(a, b)] (SimpleRep (a, b))
BaseW '[(a, b)] (Prod a b)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW
sndW :: (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW :: forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW = ProdW '[Prod a b] b
-> BaseW '[(a, b)] (Prod a b) -> FunW '[(a, b)] b
forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a rng.
(AppRequires t1 '[b] rng, AppRequires t2 '[a] b, HasSpec b) =>
t1 '[b] rng -> t2 '[a] b -> FunW '[a] rng
ComposeW ProdW '[Prod a b] b
forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW BaseW '[(a, b)] (SimpleRep (a, b))
BaseW '[(a, b)] (Prod a b)
forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW
instance
(HasSpec a, HasSpec b, Arbitrary (FoldSpec a), Arbitrary (FoldSpec b)) =>
Arbitrary (FoldSpec (a, b))
where
arbitrary :: Gen (FoldSpec (a, b))
arbitrary =
[Gen (FoldSpec (a, b))] -> Gen (FoldSpec (a, b))
forall a. HasCallStack => [Gen a] -> Gen a
oneof
[ Fun '[(a, b)] a -> FoldSpec a -> FoldSpec (a, b)
forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (FunW '[(a, b)] a -> Fun '[(a, b)] a
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[(a, b)] a
forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] a
fstW) (FoldSpec a -> FoldSpec (a, b))
-> Gen (FoldSpec a) -> Gen (FoldSpec (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (FoldSpec a)
forall a. Arbitrary a => Gen a
arbitrary
, Fun '[(a, b)] b -> FoldSpec b -> FoldSpec (a, b)
forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec (FunW '[(a, b)] b -> Fun '[(a, b)] b
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[(a, b)] b
forall a b. (HasSpec a, HasSpec b) => FunW '[(a, b)] b
sndW) (FoldSpec b -> FoldSpec (a, b))
-> Gen (FoldSpec b) -> Gen (FoldSpec (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (FoldSpec b)
forall a. Arbitrary a => Gen a
arbitrary
, FoldSpec (a, b) -> Gen (FoldSpec (a, b))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (a, b)
forall a. FoldSpec a
NoFold
]
shrink :: FoldSpec (a, b) -> [FoldSpec (a, b)]
shrink FoldSpec (a, b)
NoFold = []
shrink FoldSpec {} = [FoldSpec (a, b)
forall a. FoldSpec a
NoFold]
pair_ ::
( HasSpec a
, HasSpec b
, IsNormalType a
, IsNormalType b
) =>
Term a ->
Term b ->
Term (a, b)
pair_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term a
x Term b
y = Term (SimpleRep (a, b)) -> Term (a, b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (Term (SimpleRep (a, b)) -> Term (a, b))
-> Term (SimpleRep (a, b)) -> Term (a, b)
forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term (Prod a b)
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ Term a
x Term b
y
left_ ::
( HasSpec a
, HasSpec b
, IsNormalType a
, IsNormalType b
) =>
Term a ->
Term (Either a b)
left_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term (Either a b)
left_ = Term (SimpleRep (Either a b)) -> Term (Either a b)
TermD Deps (Sum a b) -> Term (Either a b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (TermD Deps (Sum a b) -> Term (Either a b))
-> (Term a -> TermD Deps (Sum a b)) -> Term a -> Term (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> TermD Deps (Sum a b)
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term a -> Term (Sum a b)
injLeft_
right_ ::
( HasSpec a
, HasSpec b
, IsNormalType a
, IsNormalType b
) =>
Term b ->
Term (Either a b)
right_ :: forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term b -> Term (Either a b)
right_ = Term (SimpleRep (Either a b)) -> Term (Either a b)
TermD Deps (Sum a b) -> Term (Either a b)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (TermD Deps (Sum a b) -> Term (Either a b))
-> (Term b -> TermD Deps (Sum a b)) -> Term b -> Term (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term b -> TermD Deps (Sum a b)
forall a b.
(HasSpec a, HasSpec b, KnownNat (CountCases b)) =>
Term b -> Term (Sum a b)
injRight_
caseOn ::
forall a.
( GenericRequires a
, SimpleRep a ~ SumOver (Cases (SimpleRep a))
, TypeList (Cases (SimpleRep a))
) =>
Term a ->
FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn :: forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term a
tm = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(Cases (SimpleRep a)) (Term (SumOver (Cases (SimpleRep a)))
-> List (Weighted Binder) (Cases (SimpleRep a)) -> Pred
forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase (Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm))
buildBranch ::
forall p as.
( All HasSpec as
, IsPred p
) =>
FunTy (MapList Term as) p ->
List Term as ->
Pred
buildBranch :: forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch FunTy (MapList Term as) p
bd List Term as
Nil = p -> Pred
forall p. IsPred p => p -> Pred
toPred p
FunTy (MapList Term as) p
bd
buildBranch FunTy (MapList Term as) p
bd (Term a
t :> List Term as1
args) =
Term a -> (Term a -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind Term a
t ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p (FunTy (MapList Term as) p
Term a -> FunTy (MapList Term as1) p
bd Term a
x) List Term as1
args
branch ::
forall p a.
( HasSpec a
, All HasSpec (Args a)
, IsPred p
, IsProd a
) =>
FunTy (MapList Term (Args a)) p ->
Weighted Binder a
branch :: forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch FunTy (MapList Term (Args a)) p
body =
Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
forall a. Maybe a
Nothing ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (Args a)) p
body (List Term (Args a) -> Pred)
-> (Term a -> List Term (Args a)) -> Term a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs @a))
branchW ::
forall p a.
( HasSpec a
, All HasSpec (Args a)
, IsPred p
, IsProd a
) =>
Int ->
FunTy (MapList Term (Args a)) p ->
Weighted Binder a
branchW :: forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w FunTy (MapList Term (Args a)) p
body =
Maybe Int -> Binder a -> Weighted Binder a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
w) ((Term a -> Pred) -> Binder a
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind (forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (Args a)) p
body (List Term (Args a) -> Pred)
-> (Term a -> List Term (Args a)) -> Term a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs @a))
type ProdAsListComputes a =
AssertSpineComputes
(Text "Have you considered adding an IsNormalType or ProdAsListComputes constraint?")
(ProductAsList a)
match ::
forall p a.
( IsProductType a
, IsPred p
, GenericRequires a
, ProdAsListComputes a
) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match :: forall p a.
(IsProductType a, IsPred p, GenericRequires a,
ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term a
p FunTy (MapList Term (Args (SimpleRep a))) p
m = Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term a
p (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch @p FunTy (MapList Term (Args (SimpleRep a))) p
m)
con ::
forall c a r.
( SimpleRep a ~ SOP (TheSop a)
, TypeSpec a ~ TypeSpec (SOP (TheSop a))
, TypeList (ConstrOf c (TheSop a))
, r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a)
, ResultType r ~ Term a
, SOPTerm c (TheSop a)
, ConstrTerm (ConstrOf c (TheSop a))
, GenericRequires a
) =>
r
con :: forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
TypeSpec a ~ TypeSpec (SOP (TheSop a)),
TypeList (ConstrOf c (TheSop a)),
r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
ResultType r ~ Term a, SOPTerm c (TheSop a),
ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con =
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(ConstrOf c (TheSop a)) @Term
(forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ @a (TermD Deps (SOP (TheSop a)) -> Term a)
-> (List Term (ConstrOf c (TheSop a))
-> TermD Deps (SOP (TheSop a)))
-> List Term (ConstrOf c (TheSop a))
-> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (sop :: [*]).
SOPTerm c sop =>
Term (ProdOver (ConstrOf c sop)) -> Term (SOP sop)
inj_ @c @(TheSop a) (Term (ProdOver (ConstrOf c (TheSop a)))
-> TermD Deps (SOP (TheSop a)))
-> (List Term (ConstrOf c (TheSop a))
-> Term (ProdOver (ConstrOf c (TheSop a))))
-> List Term (ConstrOf c (TheSop a))
-> TermD Deps (SOP (TheSop a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List Term (ConstrOf c (TheSop a))
-> Term (ProdOver (ConstrOf c (TheSop a)))
forall (constr :: [*]).
ConstrTerm constr =>
List Term constr -> Term (ProdOver constr)
prodOver_)
cJust_ :: (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ :: forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ = forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
TypeSpec a ~ TypeSpec (SOP (TheSop a)),
TypeList (ConstrOf c (TheSop a)),
r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
ResultType r ~ Term a, SOPTerm c (TheSop a),
ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con @"Just"
cNothing_ :: (HasSpec a, IsNormalType a) => Term (Maybe a)
cNothing_ :: forall a. (HasSpec a, IsNormalType a) => Term (Maybe a)
cNothing_ = forall (c :: Symbol) a r.
(SimpleRep a ~ SOP (TheSop a),
TypeSpec a ~ TypeSpec (SOP (TheSop a)),
TypeList (ConstrOf c (TheSop a)),
r ~ FunTy (MapList Term (ConstrOf c (TheSop a))) (Term a),
ResultType r ~ Term a, SOPTerm c (TheSop a),
ConstrTerm (ConstrOf c (TheSop a)), GenericRequires a) =>
r
con @"Nothing" (() -> TermD Deps ()
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ())
sel ::
forall n a c as.
( SimpleRep a ~ ProdOver as
,
TheSop a ~ '[c ::: as]
, TypeSpec a ~ TypeSpec (ProdOver as)
, Select n as
, HasSpec a
, HasSpec (ProdOver as)
, HasSimpleRep a
, GenericRequires a
) =>
Term a ->
Term (At n as)
sel :: forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel = forall (n :: Natural) (as :: [*]).
Select n as =>
Term (ProdOver as) -> Term (At n as)
select_ @n @as (Term (ProdOver as) -> Term (At n as))
-> (Term a -> Term (ProdOver as)) -> Term a -> Term (At n as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> Term (SimpleRep a)
Term a -> Term (ProdOver as)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_
forAll' ::
forall t a p.
( Forallable t a
, Cases (SimpleRep a) ~ '[SimpleRep a]
, TypeSpec a ~ TypeSpec (SimpleRep a)
, HasSpec t
, HasSpec (SimpleRep a)
, HasSimpleRep a
, All HasSpec (Args (SimpleRep a))
, IsPred p
, IsProd (SimpleRep a)
, IsProductType a
, HasSpec a
, GenericRequires a
, ProdAsListComputes a
) =>
Term t ->
FunTy (MapList Term (ProductAsList a)) p ->
Pred
forAll' :: forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
IsProductType a, HasSpec a, GenericRequires a,
ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term t
xs FunTy (MapList Term (Args (SimpleRep a))) p
f = Term t -> (Term a -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term t
xs ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term a
x FunTy (MapList Term (Args (SimpleRep a))) p
f
constrained' ::
forall a p.
( Cases (SimpleRep a) ~ '[SimpleRep a]
, TypeSpec a ~ TypeSpec (SimpleRep a)
, HasSpec (SimpleRep a)
, HasSimpleRep a
, All HasSpec (Args (SimpleRep a))
, IsProd (SimpleRep a)
, HasSpec a
, IsProductType a
, IsPred p
, GenericRequires a
, ProdAsListComputes a
) =>
FunTy (MapList Term (ProductAsList a)) p ->
Specification a
constrained' :: forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' FunTy (MapList Term (Args (SimpleRep a))) p
f = (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term a
x FunTy (MapList Term (Args (SimpleRep a))) p
f
reify' ::
forall a b p.
( Cases (SimpleRep b) ~ '[SimpleRep b]
, TypeSpec b ~ TypeSpec (SimpleRep b)
, HasSpec (SimpleRep b)
, HasSimpleRep b
, All HasSpec (Args (SimpleRep b))
, IsProd (SimpleRep b)
, HasSpec a
, HasSpec b
, IsProductType b
, IsProd a
, IsPred p
, GenericRequires b
, ProdAsListComputes b
) =>
Term a ->
(a -> b) ->
FunTy (MapList Term (ProductAsList b)) p ->
Pred
reify' :: forall a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b),
HasSimpleRep b, All HasSpec (Args (SimpleRep b)),
IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b,
IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) =>
Term a
-> (a -> b) -> FunTy (MapList Term (Args (SimpleRep b))) p -> Pred
reify' Term a
a a -> b
r FunTy (MapList Term (Args (SimpleRep b))) p
f = Term a -> (a -> b) -> (Term b -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
a a -> b
r ((Term b -> Pred) -> Pred) -> (Term b -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term b
x -> forall p a.
(IsProductType a, IsPred p, GenericRequires a,
ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @p Term b
x FunTy (MapList Term (Args (SimpleRep b))) p
f
instance
( HasSpec a
, HasSpec (ProdOver (a : b : as))
, ConstrTerm (b : as)
) =>
ConstrTerm (a : b : as)
where
prodOver_ :: List Term (a : b : as) -> Term (ProdOver (a : b : as))
prodOver_ (Term a
a :> List Term as1
as) = Term a
-> Term (ProdOver (b : as)) -> Term (Prod a (ProdOver (b : as)))
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ Term a
a (List Term as1 -> Term (ProdOver as1)
forall (constr :: [*]).
ConstrTerm constr =>
List Term constr -> Term (ProdOver constr)
prodOver_ List Term as1
as)
onCon ::
forall c a p.
( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
, GenericRequires a
, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
, All HasSpec (Cases (SOP (TheSop a)))
, HasSpec (ProdOver (ConstrOf c (TheSop a)))
, IsPred p
, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a)
, All HasSpec (ConstrOf c (TheSop a))
, IsProd (ProdOver (ConstrOf c (TheSop a)))
) =>
Term a ->
FunTy (MapList Term (ConstrOf c (TheSop a))) p ->
Pred
onCon :: forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
All HasSpec (Cases (SOP (TheSop a))),
HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
All HasSpec (ConstrOf c (TheSop a)),
IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon Term a
tm FunTy (MapList Term (ConstrOf c (TheSop a))) p
p =
TermD Deps (SumOver (Cases (SOP (TheSop a))))
-> List (Weighted Binder) (Cases (SOP (TheSop a))) -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case
(Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm)
( forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
(Pred -> Term a -> Pred
forall a b. a -> b -> a
const (Pred -> Term a -> Pred) -> Pred -> Term a -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
True))
(forall p (as :: [*]).
(All HasSpec as, IsPred p) =>
FunTy (MapList Term as) p -> List Term as -> Pred
buildBranch @p FunTy (MapList Term (ConstrOf c (TheSop a))) p
p (List Term (ConstrOf c (TheSop a)) -> Pred)
-> (Term (ProdOver (ConstrOf c (TheSop a)))
-> List Term (ConstrOf c (TheSop a)))
-> Term (ProdOver (ConstrOf c (TheSop a)))
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (ProdOver (ConstrOf c (TheSop a)))
-> List Term (ConstrOf c (TheSop a))
Term (ProdOver (ConstrOf c (TheSop a)))
-> List Term (Args (ProdOver (ConstrOf c (TheSop a))))
forall p. (IsProd p, HasSpec p) => Term p -> List Term (Args p)
toArgs)
)
isCon ::
forall c a.
( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
, All HasSpec (Cases (SOP (TheSop a)))
, HasSpec (ProdOver (ConstrOf c (TheSop a)))
, GenericRequires a
) =>
Term a ->
Pred
isCon :: forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
All HasSpec (Cases (SOP (TheSop a))),
HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon Term a
tm =
TermD Deps (SumOver (Cases (SOP (TheSop a))))
-> List (Weighted Binder) (Cases (SOP (TheSop a))) -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case
(Term a -> Term (SimpleRep a)
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term a
tm)
( forall (c :: Symbol) b (sop :: [*]).
(IsConstrOf c b sop, HasSpec b, All HasSpec (Cases (SOP sop))) =>
(forall a. Term a -> Pred)
-> (Term b -> Pred) -> List (Weighted Binder) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
(Pred -> Term a -> Pred
forall a b. a -> b -> a
const (Pred -> Term a -> Pred) -> Pred -> Term a -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
False))
(Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred
forall a b. a -> b -> a
const (Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred)
-> Pred -> Term (ProdOver (ConstrOf c (TheSop a))) -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Bool -> TermD Deps Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
True))
)
onJust ::
forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) ->
(Term a -> p) ->
Pred
onJust :: forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust = forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
All HasSpec (Cases (SOP (TheSop a))),
HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
All HasSpec (ConstrOf c (TheSop a)),
IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Just"
isJust ::
forall a.
(HasSpec a, IsNormalType a) =>
Term (Maybe a) ->
Pred
isJust :: forall a. (HasSpec a, IsNormalType a) => Term (Maybe a) -> Pred
isJust = forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
All HasSpec (Cases (SOP (TheSop a))),
HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"Just"
chooseSpec ::
HasSpec a =>
(Int, Specification a) ->
(Int, Specification a) ->
Specification a
chooseSpec :: forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec (Int
w, Specification a
s) (Int
w', Specification a
s') =
(Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x ->
((forall b. Term b -> b) -> GE Picky)
-> (Term Picky -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> Picky -> GE Picky
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Picky -> GE Picky) -> Picky -> GE Picky
forall a b. (a -> b) -> a -> b
$ if Term a -> a
forall b. Term b -> b
eval Term a
x a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
s then Picky
PickFirst else Picky
PickSecond) ((Term Picky -> Pred) -> Pred) -> (Term Picky -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Picky
p ->
Term Picky
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep Picky))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
Term Picky
p
(Int -> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w' (FunTy (MapList Term (Args ())) Pred -> Weighted Binder ())
-> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s))
(Int -> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
w (FunTy (MapList Term (Args ())) Pred -> Weighted Binder ())
-> FunTy (MapList Term (Args ())) Pred -> Weighted Binder ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
s'))
data Picky = PickFirst | PickSecond deriving (Eq Picky
Eq Picky =>
(Picky -> Picky -> Ordering)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Bool)
-> (Picky -> Picky -> Picky)
-> (Picky -> Picky -> Picky)
-> Ord Picky
Picky -> Picky -> Bool
Picky -> Picky -> Ordering
Picky -> Picky -> Picky
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Picky -> Picky -> Ordering
compare :: Picky -> Picky -> Ordering
$c< :: Picky -> Picky -> Bool
< :: Picky -> Picky -> Bool
$c<= :: Picky -> Picky -> Bool
<= :: Picky -> Picky -> Bool
$c> :: Picky -> Picky -> Bool
> :: Picky -> Picky -> Bool
$c>= :: Picky -> Picky -> Bool
>= :: Picky -> Picky -> Bool
$cmax :: Picky -> Picky -> Picky
max :: Picky -> Picky -> Picky
$cmin :: Picky -> Picky -> Picky
min :: Picky -> Picky -> Picky
Ord, Picky -> Picky -> Bool
(Picky -> Picky -> Bool) -> (Picky -> Picky -> Bool) -> Eq Picky
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Picky -> Picky -> Bool
== :: Picky -> Picky -> Bool
$c/= :: Picky -> Picky -> Bool
/= :: Picky -> Picky -> Bool
Eq, Int -> Picky -> ShowS
[Picky] -> ShowS
Picky -> String
(Int -> Picky -> ShowS)
-> (Picky -> String) -> ([Picky] -> ShowS) -> Show Picky
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Picky -> ShowS
showsPrec :: Int -> Picky -> ShowS
$cshow :: Picky -> String
show :: Picky -> String
$cshowList :: [Picky] -> ShowS
showList :: [Picky] -> ShowS
Show, (forall x. Picky -> Rep Picky x)
-> (forall x. Rep Picky x -> Picky) -> Generic Picky
forall x. Rep Picky x -> Picky
forall x. Picky -> Rep Picky x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Picky -> Rep Picky x
from :: forall x. Picky -> Rep Picky x
$cto :: forall x. Rep Picky x -> Picky
to :: forall x. Rep Picky x -> Picky
Generic)
instance HasSimpleRep Picky
instance HasSpec Picky