{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-} -- 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.Generics ( GenericsFn, IsNormalType, fst_, snd_, pair_, left_, right_, cJust_, cNothing_, caseOn, branch, branchW, forAll', constrained', reify', con, onCon, isCon, sel, match, onJust, isJust, ifElse, chooseSpec, ) where import Data.Typeable import GHC.TypeLits (Symbol) import GHC.TypeNats import Test.QuickCheck (Arbitrary (..), oneof) import Constrained.Base import Constrained.Core import Constrained.List import Constrained.Spec.Pairs () import Constrained.Univ ------------------------------------------------------------------------ -- Generics ------------------------------------------------------------------------ instance FunctionLike (GenericsFn fn) where sem :: forall (as :: [*]) b. GenericsFn fn as b -> FunTy as b sem = \case GenericsFn fn as b ToGeneric -> forall a. HasSimpleRep a => a -> SimpleRep a toSimpleRep GenericsFn fn as b FromGeneric -> forall a. HasSimpleRep a => SimpleRep a -> a fromSimpleRep instance BaseUniverse fn => Functions (GenericsFn fn) fn where propagateSpecFun :: forall (as :: [*]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) => GenericsFn fn as b -> ListCtx Value as (HOLE a) -> Specification fn b -> Specification fn a propagateSpecFun GenericsFn fn as b _ ListCtx Value as (HOLE a) _ Specification fn b TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec propagateSpecFun GenericsFn 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 GenericsFn fn as b fn ListCtx Value as (HOLE a) ctx Specification fn b spec = case GenericsFn fn as b fn of GenericsFn 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 GenericsFn 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) GenericsFn fn as b ToGeneric | NilCtx HOLE a a HOLE <- ListCtx Value as (HOLE a) ctx -> case Specification fn b spec of TypeSpec TypeSpec fn b s OrdSet b cant -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> OrdSet a -> Specification fn a TypeSpec TypeSpec fn b s (forall a. HasSimpleRep a => SimpleRep a -> a fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> OrdSet b cant) MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec (forall a. HasSimpleRep a => SimpleRep a -> a fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> OrdSet b es) GenericsFn fn as b FromGeneric | NilCtx HOLE a (SimpleRep b) HOLE <- ListCtx Value as (HOLE a) ctx -> case Specification fn b spec of TypeSpec TypeSpec fn b s OrdSet b cant -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> OrdSet a -> Specification fn a TypeSpec TypeSpec fn b s (forall a. HasSimpleRep a => a -> SimpleRep a toSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> OrdSet b cant) MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec (forall a. HasSimpleRep a => a -> SimpleRep a toSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> OrdSet b es) rewriteRules :: forall (as :: [*]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) => GenericsFn fn as b -> List (Term fn) as -> Maybe (Term fn b) rewriteRules GenericsFn fn as b FromGeneric (App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fnU as b -> Maybe (fn as b) extractFn @(GenericsFn fn) @fn -> Just GenericsFn fn as a ToGeneric) (Term fn a x :> List (Term fn) as1 Nil) :> List (Term fn) as1 _) = forall a b. (Typeable a, Typeable b) => a -> Maybe b cast Term fn a x rewriteRules GenericsFn fn as b ToGeneric (App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fnU as b -> Maybe (fn as b) extractFn @(GenericsFn fn) @fn -> Just GenericsFn fn as a FromGeneric) (Term fn a x :> List (Term fn) as1 Nil) :> List (Term fn) as1 _) = forall a. a -> Maybe a Just Term fn a x rewriteRules GenericsFn fn as b _ List (Term fn) as _ = forall a. Maybe a Nothing mapTypeSpec :: forall a b. (HasSpec fn a, HasSpec fn b) => GenericsFn fn '[a] b -> TypeSpec fn a -> Specification fn b mapTypeSpec GenericsFn fn '[a] b f TypeSpec fn a ts = case GenericsFn fn '[a] b f of GenericsFn fn '[a] b ToGeneric -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec TypeSpec fn a ts GenericsFn fn '[a] b FromGeneric -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec TypeSpec fn a ts -- HasSpec for various generic types -------------------------------------- instance HasSimpleRep (a, b) instance HasSimpleRep (a, b, c) instance HasSimpleRep (a, b, c, d) instance HasSimpleRep (a, b, c, d, e) instance HasSimpleRep (a, b, c, d, e, g) instance HasSimpleRep (a, b, c, d, e, g, h) instance HasSimpleRep (Maybe a) instance HasSimpleRep (Either a b) instance ( HasSpec fn a , HasSpec fn b ) => HasSpec fn (a, b) instance ( HasSpec fn a , HasSpec fn b , HasSpec fn c ) => HasSpec fn (a, b, c) instance ( HasSpec fn a , HasSpec fn b , HasSpec fn c , HasSpec fn d ) => HasSpec fn (a, b, c, d) instance ( HasSpec fn a , HasSpec fn b , HasSpec fn c , HasSpec fn d , HasSpec fn e ) => HasSpec fn (a, b, c, d, e) instance ( HasSpec fn a , HasSpec fn b , HasSpec fn c , HasSpec fn d , HasSpec fn e , HasSpec fn g ) => HasSpec fn (a, b, c, d, e, g) instance ( HasSpec fn a , HasSpec fn b , HasSpec fn c , HasSpec fn d , HasSpec fn e , HasSpec fn g , HasSpec fn h ) => HasSpec fn (a, b, c, d, e, g, h) instance (IsNormalType a, HasSpec fn a) => HasSpec fn (Maybe a) instance ( HasSpec fn a , IsNormalType a , HasSpec fn b , IsNormalType b ) => HasSpec fn (Either a b) ------------------------------------------------------------------------ -- Sums ------------------------------------------------------------------------ instance BaseUniverse fn => Functions (SumFn fn) fn where propagateSpecFun :: forall (as :: [*]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) => SumFn fn as b -> ListCtx Value as (HOLE a) -> Specification fn b -> Specification fn a propagateSpecFun SumFn fn as b _ ListCtx Value as (HOLE a) _ Specification fn b TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec propagateSpecFun SumFn 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 SumFn fn as b fn ListCtx Value as (HOLE a) ctx Specification fn b spec = case SumFn fn as b fn of SumFn 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 SumFn 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) SumFn fn as b InjLeft | NilCtx HOLE a a HOLE <- ListCtx Value as (HOLE a) ctx -> case Specification fn b spec of TypeSpec (SumSpec Maybe (Int, Int) _ Specification fn a sl Specification fn b _) OrdSet b cant -> Specification fn a sl 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 [a a | SumLeft a a <- OrdSet b cant] MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [a a | SumLeft a a <- OrdSet b es] SumFn fn as b InjRight | NilCtx HOLE a b HOLE <- ListCtx Value as (HOLE a) ctx -> case Specification fn b spec of TypeSpec (SumSpec Maybe (Int, Int) _ Specification fn a _ Specification fn a sr) OrdSet b cant -> Specification fn a sr 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 [a a | SumRight a a <- OrdSet b cant] MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [a a | SumRight a a <- OrdSet b es] -- NOTE: this function over-approximates and returns a liberal spec. mapTypeSpec :: forall a b. (HasSpec fn a, HasSpec fn b) => SumFn fn '[a] b -> TypeSpec fn a -> Specification fn b mapTypeSpec SumFn fn '[a] b f TypeSpec fn a ts = case SumFn fn '[a] b f of -- TODO possibly not the right counts?? SumFn fn '[a] b InjLeft -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a b. Maybe (Int, Int) -> Specification fn a -> Specification fn b -> SumSpec fn a b SumSpec forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec TypeSpec fn a ts) (forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a pure String "mapTypeSpec InjLeft")) SumFn fn '[a] b InjRight -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a b. Maybe (Int, Int) -> Specification fn a -> Specification fn b -> SumSpec fn a b SumSpec forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a pure String "mapTypeSpec InjRight")) (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec TypeSpec fn a ts) ------------------------------------------------------------------------ -- Syntax ------------------------------------------------------------------------ fst_ :: forall fn a b. ( HasSpec fn a , HasSpec fn b ) => Term fn (a, b) -> Term fn a fst_ :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn a fst_ = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol) (as :: [*]). (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) => Term fn a -> Term fn (At n as) sel @0 snd_ :: forall fn a b. ( HasSpec fn a , HasSpec fn b ) => Term fn (a, b) -> Term fn b snd_ :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn (a, b) -> Term fn b snd_ = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol) (as :: [*]). (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) => Term fn a -> Term fn (At n as) sel @1 pair_ :: forall fn a b. ( HasSpec fn a , HasSpec fn b ) => Term fn a -> Term fn b -> Term fn (a, b) pair_ :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Term fn a -> Term fn b -> Term fn (a, b) pair_ Term fn a a Term fn b b = forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn (SimpleRep a) -> Term fn a fromGeneric_ forall a b. (a -> b) -> a -> b $ 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 '[a, b] (Prod a b) pairFn Term fn a a Term fn b b left_ :: ( HasSpec fn a , HasSpec fn b , IsNormalType a , IsNormalType b ) => Term fn a -> Term fn (Either a b) left_ :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) => Term fn a -> Term fn (Either a b) left_ = forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn (SimpleRep a) -> Term fn a fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c . 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 (SumFn fn) fn => fn '[a] (Sum a b) injLeftFn right_ :: ( HasSpec fn a , HasSpec fn b , IsNormalType a , IsNormalType b ) => Term fn b -> Term fn (Either a b) right_ :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) => Term fn b -> Term fn (Either a b) right_ = forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn (SimpleRep a) -> Term fn a fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c . 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 (SumFn fn) fn => fn '[b] (Sum a b) injRightFn caseOn :: forall fn a. ( HasSpec fn a , HasSpec fn (SimpleRep a) , HasSimpleRep a , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , SimpleRep a ~ SumOver (Cases (SimpleRep a)) , TypeList (Cases (SimpleRep a)) ) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn :: forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term fn a tm = forall (ts :: [*]) (f :: * -> *) r. TypeList ts => (List f ts -> r) -> FunTy (MapList f ts) r curryList @(Cases (SimpleRep a)) (forall (fn :: [*] -> * -> *) (as :: [*]). HasSpec fn (SumOver as) => Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn mkCase (forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn a -> Term fn (SimpleRep a) toGeneric_ Term fn a tm)) branch :: forall fn p a. ( HasSpec fn a , All (HasSpec fn) (Args a) , IsPred p fn , IsProd a ) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch :: forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch FunTy (MapList (Term fn) (Args a)) p body = -- NOTE: It's not sufficient to simply apply `body` to all the arguments -- with `uncurryList` because that will mean that `var` is repeated in the -- body. For example, consider `branch $ \ i j -> i <=. j`. If we don't -- build the lets this will boil down to `p :-> fst p <=. snd p` which -- will blow up at generation time. If we instead do: `p :-> Let x (fst p) (Let y (snd p) (x <=. y))` -- the solver will solve `x` and `y` separately (`y` before `x` in this case) and things -- will work just fine. forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind (forall p (fn :: [*] -> * -> *) (as :: [*]). (All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch @p @fn FunTy (MapList (Term fn) (Args a)) p body forall b c a. (b -> c) -> (a -> b) -> a -> c . forall p (fn :: [*] -> * -> *). (IsProd p, HasSpec fn p, BaseUniverse fn) => Term fn p -> List (Term fn) (Args p) toArgs @a @fn)) branchW :: forall fn p a. ( HasSpec fn a , All (HasSpec fn) (Args a) , IsPred p fn , IsProd a ) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW :: forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int w FunTy (MapList (Term fn) (Args a)) p body = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted (forall a. a -> Maybe a Just Int w) (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind (forall p (fn :: [*] -> * -> *) (as :: [*]). (All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch @p @fn FunTy (MapList (Term fn) (Args a)) p body forall b c a. (b -> c) -> (a -> b) -> a -> c . forall p (fn :: [*] -> * -> *). (IsProd p, HasSpec fn p, BaseUniverse fn) => Term fn p -> List (Term fn) (Args p) toArgs @a @fn)) type IsProductType fn a = ( HasSimpleRep a , Cases (SimpleRep a) ~ '[SimpleRep a] , SimpleRep a ~ SumOver (Cases (SimpleRep a)) , IsProd (SimpleRep a) , HasSpec fn (SimpleRep a) , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , All (HasSpec fn) (ProductAsList a) ) type ProductAsList a = Args (SimpleRep a) match :: forall fn p a. ( HasSpec fn a , IsProductType fn a , IsPred p fn ) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match :: forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match Term fn a p FunTy (MapList (Term fn) (Args (SimpleRep a))) p m = forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term fn a p (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branch @fn @p FunTy (MapList (Term fn) (Args (SimpleRep a))) p m) buildBranch :: forall p fn as. ( All (HasSpec fn) as , IsPred p fn , BaseUniverse fn ) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch :: forall p (fn :: [*] -> * -> *) (as :: [*]). (All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch FunTy (MapList (Term fn) as) p bd List (Term fn) as Nil = forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, PredLike p, UnivConstr p fn) => p -> Pred fn toPred FunTy (MapList (Term fn) as) p bd buildBranch FunTy (MapList (Term fn) as) p bd (Term fn a t :> List (Term fn) as1 args) = forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => Term fn a -> (Term fn a -> p) -> Pred fn letBind Term fn a t forall a b. (a -> b) -> a -> b $ \Term fn a x -> forall p (fn :: [*] -> * -> *) (as :: [*]). (All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch @p @fn (FunTy (MapList (Term fn) as) p bd Term fn a x) List (Term fn) as1 args type family Args t where Args (Prod a b) = a : Args b Args a = '[a] class IsProd p where toArgs :: ( HasSpec fn p , BaseUniverse fn ) => Term fn p -> List (Term fn) (Args p) instance {-# OVERLAPPABLE #-} Args a ~ '[a] => IsProd a where toArgs :: forall (fn :: [*] -> * -> *). (HasSpec fn a, BaseUniverse fn) => Term fn a -> List (Term fn) (Args a) toArgs = (forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall {k} (f :: k -> *). List f '[] Nil) instance IsProd b => IsProd (Prod a b) where toArgs :: forall (fn :: [*] -> * -> *). (HasSpec fn (Prod a b), BaseUniverse fn) => Term fn (Prod a b) -> List (Term fn) (Args (Prod a b)) toArgs (Term fn (Prod a b) p :: Term fn (Prod a b)) | Evidence (Prerequisites fn (Prod a b)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Prod a b) = (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) p) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall p (fn :: [*] -> * -> *). (IsProd p, HasSpec fn p, BaseUniverse fn) => Term fn p -> List (Term fn) (Args p) toArgs (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) p) type family ResultType t where ResultType (a -> b) = ResultType b ResultType a = a -- NOTE: `ResultType r ~ Term fn a` is NOT a redundant constraint, -- removing it causes type inference to break elsewhere con :: forall c a r fn. ( SimpleRep a ~ SOP (TheSop a) , TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)) , TypeList (ConstrOf c (TheSop a)) , HasSpec fn a , HasSimpleRep a , r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a) , ResultType r ~ Term fn a , SOPTerm c fn (TheSop a) , ConstrTerm fn (ConstrOf c (TheSop a)) ) => r con :: forall (c :: Symbol) a r (fn :: [*] -> * -> *). (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) => r con = forall (ts :: [*]) (f :: * -> *) r. TypeList ts => (List f ts -> r) -> FunTy (MapList f ts) r curryList @(ConstrOf c (TheSop a)) @(Term fn) (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. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[SimpleRep a] a fromGenericFn @_ @a) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (c :: Symbol) (fn :: [*] -> * -> *) (sop :: [*]). SOPTerm c fn sop => Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop) inj_ @c @fn @(TheSop a) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (fn :: [*] -> * -> *) (constr :: [*]). ConstrTerm fn constr => List (Term fn) constr -> Term fn (ProdOver constr) prod_) cJust_ :: (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (Maybe a) cJust_ :: forall (fn :: [*] -> * -> *) a. (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (Maybe a) cJust_ = forall (c :: Symbol) a r (fn :: [*] -> * -> *). (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) => r con @"Just" cNothing_ :: (HasSpec fn a, IsNormalType a) => Term fn (Maybe a) cNothing_ :: forall (fn :: [*] -> * -> *) a. (HasSpec fn a, IsNormalType a) => Term fn (Maybe a) cNothing_ = forall (c :: Symbol) a r (fn :: [*] -> * -> *). (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) => r con @"Nothing" (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a lit ()) sel :: forall n fn a c as. ( SimpleRep a ~ ProdOver as , TheSop a ~ '[c ::: as] , TypeSpec fn a ~ TypeSpec fn (ProdOver as) , Select fn n as , HasSpec fn a , HasSpec fn (ProdOver as) , HasSimpleRep a ) => Term fn a -> Term fn (At n as) sel :: forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol) (as :: [*]). (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) => Term fn a -> Term fn (At n as) sel = forall (fn :: [*] -> * -> *) (n :: Natural) (as :: [*]). Select fn n as => Term fn (ProdOver as) -> Term fn (At n as) select_ @fn @n @as forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn a -> Term fn (SimpleRep a) toGeneric_ type family Cases t where Cases (Sum a b) = a : Cases b Cases a = '[a] -- | Like `forAll` but pattern matches on the `Term fn a` forAll' :: forall fn t a p. ( Forallable t a , Cases (SimpleRep a) ~ '[SimpleRep a] , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSpec fn t , HasSpec fn (SimpleRep a) , HasSimpleRep a , All (HasSpec fn) (Args (SimpleRep a)) , IsPred p fn , IsProd (SimpleRep a) , HasSpec fn a ) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' :: forall (fn :: [*] -> * -> *) t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) => Term fn t -> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn forAll' Term fn t xs FunTy (MapList (Term fn) (Args (SimpleRep a))) p f = forall t a (fn :: [*] -> * -> *) p. (Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) => Term fn t -> (Term fn a -> p) -> Pred fn forAll Term fn t xs forall a b. (a -> b) -> a -> b $ \Term fn a x -> forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match @fn @p Term fn a x FunTy (MapList (Term fn) (Args (SimpleRep a))) p f -- | Like `constrained` but pattern matches on the bound `Term fn a` constrained' :: forall a fn p. ( Cases (SimpleRep a) ~ '[SimpleRep a] , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSpec fn (SimpleRep a) , HasSimpleRep a , All (HasSpec fn) (Args (SimpleRep a)) , IsProd (SimpleRep a) , HasSpec fn a , IsPred p fn ) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' :: forall a (fn :: [*] -> * -> *) p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Specification fn a constrained' FunTy (MapList (Term fn) (Args (SimpleRep a))) p f = 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 x -> forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match @fn @p Term fn a x FunTy (MapList (Term fn) (Args (SimpleRep a))) p f -- | Like `reify` but pattern matches on the bound `Term fn b` reify' :: forall fn a b p. ( Cases (SimpleRep b) ~ '[SimpleRep b] , TypeSpec fn b ~ TypeSpec fn (SimpleRep b) , HasSpec fn (SimpleRep b) , HasSimpleRep b , All (HasSpec fn) (Args (SimpleRep b)) , IsProd (SimpleRep b) , HasSpec fn a , HasSpec fn b , IsPred p fn ) => Term fn a -> (a -> b) -> FunTy (MapList (Term fn) (Args (SimpleRep b))) p -> Pred fn reify' :: forall (fn :: [*] -> * -> *) a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> FunTy (MapList (Term fn) (Args (SimpleRep b))) p -> Pred fn reify' Term fn a a a -> b r FunTy (MapList (Term fn) (Args (SimpleRep b))) p f = forall (fn :: [*] -> * -> *) a b p. (HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn reify Term fn a a a -> b r forall a b. (a -> b) -> a -> b $ \Term fn b x -> forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) => Term fn a -> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn match @fn @p Term fn b x FunTy (MapList (Term fn) (Args (SimpleRep b))) p f class (BaseUniverse fn, HasSpec fn (SOP sop)) => SOPTerm c fn sop where inj_ :: Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop) instance HasSpec fn (ProdOver constr) => SOPTerm c fn (c ::: constr : '[]) where inj_ :: Term fn (ProdOver (ConstrOf c '[c ::: constr])) -> Term fn (SOP '[c ::: constr]) inj_ = forall a. a -> a id instance ( HasSpec fn (SOP (con : sop)) , HasSpec fn (ProdOver constr) , KnownNat (CountCases (SOP (con : sop))) ) => SOPTerm c fn (c ::: constr : con : sop) where inj_ :: Term fn (ProdOver (ConstrOf c ((c ::: constr) : con : sop))) -> Term fn (SOP ((c ::: constr) : con : sop)) inj_ = 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 (SumFn fn) fn => fn '[a] (Sum a b) injLeftFn instance {-# OVERLAPPABLE #-} ( HasSpec fn (ProdOver con) , SOPTerm c fn (con' : sop) , ConstrOf c (con' : sop) ~ ConstrOf c ((c' ::: con) : con' : sop) , KnownNat (CountCases (SOP (con' : sop))) ) => SOPTerm c fn ((c' ::: con) : con' : sop) where inj_ :: Term fn (ProdOver (ConstrOf c ((c' ::: con) : con' : sop))) -> Term fn (SOP ((c' ::: con) : con' : sop)) inj_ = 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 (SumFn fn) fn => fn '[b] (Sum a b) injRightFn forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (c :: Symbol) (fn :: [*] -> * -> *) (sop :: [*]). SOPTerm c fn sop => Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop) inj_ @c @fn @(con' : sop) class (BaseUniverse fn, HasSpec fn (ProdOver constr)) => ConstrTerm fn constr where prod_ :: List (Term fn) constr -> Term fn (ProdOver constr) instance HasSpec fn a => ConstrTerm fn '[a] where prod_ :: List (Term fn) '[a] -> Term fn (ProdOver '[a]) prod_ (Term fn a a :> List (Term fn) as1 Nil) = Term fn a a instance ( HasSpec fn a , HasSpec fn (ProdOver (a : b : as)) , ConstrTerm fn (b : as) ) => ConstrTerm fn (a : b : as) where prod_ :: List (Term fn) (a : b : as) -> Term fn (ProdOver (a : b : as)) prod_ (Term fn a a :> List (Term fn) as1 as) = 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 '[a, b] (Prod a b) pairFn Term fn a a (forall (fn :: [*] -> * -> *) (constr :: [*]). ConstrTerm fn constr => List (Term fn) constr -> Term fn (ProdOver constr) prod_ List (Term fn) as1 as) type family At n as where At 0 (a : as) = a At n (a : as) = At (n - 1) as class Select fn n as where select_ :: Term fn (ProdOver as) -> Term fn (At n as) instance Select fn 0 (a : '[]) where select_ :: Term fn (ProdOver '[a]) -> Term fn (At 0 '[a]) select_ = forall a. a -> a id instance (HasSpec fn a, HasSpec fn (ProdOver (a' : as))) => Select fn 0 (a : a' : as) where select_ :: Term fn (ProdOver (a : a' : as)) -> Term fn (At 0 (a : a' : as)) select_ = 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 instance {-# OVERLAPPABLE #-} ( HasSpec fn a , HasSpec fn (ProdOver (a' : as)) , At (n - 1) (a' : as) ~ At n (a : a' : as) , Select fn (n - 1) (a' : as) ) => Select fn n (a : a' : as) where select_ :: Term fn (ProdOver (a : a' : as)) -> Term fn (At n (a : a' : as)) select_ = forall (fn :: [*] -> * -> *) (n :: Natural) (as :: [*]). Select fn n as => Term fn (ProdOver as) -> Term fn (At n as) select_ @fn @(n - 1) @(a' : as) forall b c a. (b -> c) -> (a -> b) -> a -> c . 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 class IsConstrOf (c :: Symbol) b sop where mkCases :: (HasSpec fn b, All (HasSpec fn) (Cases (SOP sop))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP sop)) instance ( b ~ ProdOver as , TypeList (Cases (SOP (con : sop))) ) => IsConstrOf c b ((c ::: as) : con : sop) where mkCases :: forall (fn :: [*] -> * -> *). (HasSpec fn b, All (HasSpec fn) (Cases (SOP ((c ::: as) : con : sop)))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP ((c ::: as) : con : sop))) mkCases forall a. Term fn a -> Pred fn r (Term fn b -> Pred fn k :: Term fn b -> Pred fn) = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind Term fn b -> Pred fn k) 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 mapListC @(HasSpec fn) (\Const () a _ -> forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind forall a. Term fn a -> Pred fn 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 :: forall (fn :: [*] -> * -> *). (HasSpec fn b, All (HasSpec fn) (Cases (SOP '[c ::: as]))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP '[c ::: as])) mkCases forall a. Term fn a -> Pred fn _ (Term fn b -> Pred fn k :: Term fn b -> Pred fn) = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind Term fn b -> Pred fn k) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> 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 :: forall (fn :: [*] -> * -> *). (HasSpec fn b, All (HasSpec fn) (Cases (SOP ((c' ::: as) : cs)))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP ((c' ::: as) : cs))) mkCases forall a. Term fn a -> Pred fn r Term fn b -> Pred fn k = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a Weighted forall a. Maybe a Nothing (forall (fn :: [*] -> * -> *) a p. (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Binder fn a bind (forall a. Term fn a -> Pred fn r @(ProdOver as))) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *). (IsConstrOf c b sop, HasSpec fn b, All (HasSpec fn) (Cases (SOP sop))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP sop)) mkCases @c @_ @cs forall a. Term fn a -> Pred fn r Term fn b -> Pred fn k -- TODO: the constraints around this are horrible!! We should figure out a way to make these things nicer. onCon :: forall c a fn p. ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a) , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , HasSpec fn a , HasSpec fn (SimpleRep a) , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a , All (HasSpec fn) (Cases (SOP (TheSop a))) , HasSpec fn (ProdOver (ConstrOf c (TheSop a))) , IsPred p fn , Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a) , All (HasSpec fn) (ConstrOf c (TheSop a)) , IsProd (ProdOver (ConstrOf c (TheSop a))) ) => Term fn a -> FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p -> Pred fn onCon :: forall (c :: Symbol) a (fn :: [*] -> * -> *) p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) => Term fn a -> FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p -> Pred fn onCon Term fn a tm FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p p = forall (fn :: [*] -> * -> *) (as :: [*]). HasSpec fn (SumOver as) => Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn Case (forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn a -> Term fn (SimpleRep a) toGeneric_ Term fn a tm) ( forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *). (IsConstrOf c b sop, HasSpec fn b, All (HasSpec fn) (Cases (SOP sop))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP sop)) mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a) (forall a b. a -> b -> a const forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert Bool True) (forall p (fn :: [*] -> * -> *) (as :: [*]). (All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) => FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn buildBranch @p FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p p forall b c a. (b -> c) -> (a -> b) -> a -> c . forall p (fn :: [*] -> * -> *). (IsProd p, HasSpec fn p, BaseUniverse fn) => Term fn p -> List (Term fn) (Args p) toArgs) ) isCon :: forall c a fn. ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a) , TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , HasSpec fn a , HasSpec fn (SimpleRep a) , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a , All (HasSpec fn) (Cases (SOP (TheSop a))) , HasSpec fn (ProdOver (ConstrOf c (TheSop a))) ) => Term fn a -> Pred fn isCon :: forall (c :: Symbol) a (fn :: [*] -> * -> *). (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) => Term fn a -> Pred fn isCon Term fn a tm = forall (fn :: [*] -> * -> *) (as :: [*]). HasSpec fn (SumOver as) => Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn Case (forall a (fn :: [*] -> * -> *). (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => Term fn a -> Term fn (SimpleRep a) toGeneric_ Term fn a tm) ( forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *). (IsConstrOf c b sop, HasSpec fn b, All (HasSpec fn) (Cases (SOP sop))) => (forall a. Term fn a -> Pred fn) -> (Term fn b -> Pred fn) -> List (Weighted (Binder fn)) (Cases (SOP sop)) mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a) (forall a b. a -> b -> a const forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert Bool False) (forall a b. a -> b -> a const forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) p. (BaseUniverse fn, IsPred p fn) => p -> Pred fn assert Bool True) ) type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1) onJust :: forall fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) => Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn onJust :: forall (fn :: [*] -> * -> *) a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) => Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn onJust = forall (c :: Symbol) a (fn :: [*] -> * -> *) p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) => Term fn a -> FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p -> Pred fn onCon @"Just" isJust :: forall fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) => Term fn (Maybe a) -> Pred fn isJust :: forall (fn :: [*] -> * -> *) a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) => Term fn (Maybe a) -> Pred fn isJust = forall (c :: Symbol) a (fn :: [*] -> * -> *). (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) => Term fn a -> Pred fn isCon @"Just" chooseSpec :: HasSpec fn a => (Int, Specification fn a) -> (Int, Specification fn a) -> Specification fn a chooseSpec :: forall (fn :: [*] -> * -> *) a. HasSpec fn a => (Int, Specification fn a) -> (Int, Specification fn a) -> Specification fn a chooseSpec (Int w, Specification fn a s) (Int w', Specification fn a s') = 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 x -> forall a p (fn :: [*] -> * -> *). (HasSpec fn a, IsPred p fn) => ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn exists (\forall b. Term fn b -> b eval -> forall (f :: * -> *) a. Applicative f => a -> f a pure forall a b. (a -> b) -> a -> b $ forall b. Term fn b -> b eval Term fn a x forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn a s) forall a b. (a -> b) -> a -> b $ \Term fn Bool b -> [ forall (fn :: [*] -> * -> *) p q. (BaseUniverse fn, IsPred p fn, IsPred q fn) => Term fn Bool -> p -> q -> Pred fn ifElse Term fn Bool b (Term fn a x forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification fn a s) (Term fn a x forall (fn :: [*] -> * -> *) a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn `satisfies` Specification fn a s') , forall (fn :: [*] -> * -> *) a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term fn a -> FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) caseOn Term fn Bool b (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int w' forall a b. (a -> b) -> a -> b $ \Term fn () _ -> Bool True) (forall (fn :: [*] -> * -> *) p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) => Int -> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a branchW Int w forall a b. (a -> b) -> a -> b $ \Term fn () _ -> Bool True) ] -- Arbitrary instances ---------------------------------------------------- instance (HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) => Arbitrary (FoldSpec fn (a, b)) where arbitrary :: Gen (FoldSpec fn (a, b)) arbitrary = forall a. [Gen a] -> Gen a oneof [ forall (fn :: [*] -> * -> *) a b. HasSpec fn a => fn '[a] b -> FoldSpec fn b -> FoldSpec fn a preMapFoldSpec (forall (fn :: [*] -> * -> *) b a c. (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) => fn '[b] c -> fn '[a] b -> fn '[a] c composeFn forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall a. Arbitrary a => Gen a arbitrary , forall (fn :: [*] -> * -> *) a b. HasSpec fn a => fn '[a] b -> FoldSpec fn b -> FoldSpec fn a preMapFoldSpec (forall (fn :: [*] -> * -> *) b a c. (Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b), Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) => fn '[b] c -> fn '[a] b -> fn '[a] c composeFn forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] b sndFn forall (fn :: [*] -> * -> *) a. (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) => fn '[a] (SimpleRep a) toGenericFn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall a. Arbitrary a => Gen a arbitrary , forall (f :: * -> *) a. Applicative f => a -> f a pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold ] shrink :: FoldSpec fn (a, b) -> [FoldSpec fn (a, b)] shrink FoldSpec fn (a, b) NoFold = [] shrink FoldSpec {} = [forall (fn :: [*] -> * -> *) a. FoldSpec fn a NoFold]