{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} -- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant -- cases and turning off the overlap check in newer ghc versions we disable the check for old -- versions. #if __GLASGOW_HASKELL__ < 900 {-# OPTIONS_GHC -Wno-incomplete-patterns #-} #endif module Constrained.Spec.Pairs where import Constrained.Base import Constrained.Core import Constrained.List import Constrained.Univ import qualified Data.List.NonEmpty as NE import Test.QuickCheck -- HasSpec ---------------------------------------------------------------- cartesian :: (HasSpec fn a, HasSpec fn b) => Specification fn a -> Specification fn b -> Specification fn (Prod a b) cartesian :: forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Specification fn a -> Specification fn b -> Specification fn (Prod a b) cartesian (ErrorSpec NonEmpty String es) (ErrorSpec NonEmpty String fs) = forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (NonEmpty String es forall a. Semigroup a => a -> a -> a <> NonEmpty String fs) cartesian (ErrorSpec NonEmpty String es) Specification fn b _ = forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec NonEmpty String es cartesian Specification fn a _ (ErrorSpec NonEmpty String es) = forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec NonEmpty String es cartesian (MemberSpec []) Specification fn b _ = forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [] cartesian Specification fn a _ (MemberSpec []) = forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [] 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) deriving instance (HasSpec fn a, HasSpec fn b) => Show (PairSpec fn a b) -- Functions for working on pairs ----------------------------------------- instance BaseUniverse fn => Functions (PairFn fn) fn where propagateSpecFun :: forall (as :: [*]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) => PairFn fn as b -> ListCtx Value as (HOLE a) -> Specification fn b -> Specification fn a propagateSpecFun PairFn fn as b _ ListCtx Value as (HOLE a) _ Specification fn b TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec propagateSpecFun PairFn fn as b _ ListCtx Value as (HOLE a) _ (ErrorSpec NonEmpty String err) = forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec NonEmpty String err propagateSpecFun PairFn fn as b fn ListCtx Value as (HOLE a) ctx Specification fn b spec = case PairFn fn as b fn of PairFn fn as b Fst -> -- No TypeAbstractions in ghc-8.10 case PairFn fn as b fn of (PairFn fn '[Prod b b] b _ :: PairFn fn '[Prod a b] a) | NilCtx HOLE a (Prod b b) HOLE <- ListCtx Value as (HOLE a) ctx , Evidence (Prerequisites fn (Prod b b)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Prod a b) -> forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Specification fn a -> Specification fn b -> Specification fn (Prod a b) cartesian Specification fn b spec forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec PairFn fn as b Snd -> -- No TypeAbstractions in ghc-8.10 case PairFn fn as b fn of (PairFn fn '[Prod a b] b _ :: PairFn fn '[Prod a b] b) | NilCtx HOLE a (Prod a b) HOLE <- ListCtx Value as (HOLE a) ctx , Evidence (Prerequisites fn (Prod a b)) Evidence <- forall (fn :: [*] -> * -> *) a. HasSpec fn a => Evidence (Prerequisites fn a) prerequisites @fn @(Prod a b) -> forall (fn :: [*] -> * -> *) a b. (HasSpec fn a, HasSpec fn b) => Specification fn a -> Specification fn b -> Specification fn (Prod a b) cartesian forall (fn :: [*] -> * -> *) a. Specification fn a TrueSpec Specification fn b spec PairFn fn as b _ | SuspendedSpec Var b v Pred fn ps <- Specification fn b spec , ListCtx List Value as pre HOLE a a HOLE List Value as' suf <- ListCtx Value as (HOLE a) ctx -> forall a (fn :: [*] -> * -> *) p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> Specification fn a constrained forall a b. (a -> b) -> a -> b $ \Term fn a v' -> let args :: List (Term fn) (Append as (a : as')) args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]). List f as -> List f bs -> List f (Append as bs) appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]). (forall (a :: k). f a -> g a) -> List f as -> List g as mapList (\(Value a a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit a a) List Value as pre) (Term fn a v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]). (forall (a :: k). f a -> g a) -> List f as -> List g as mapList (\(Value a a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a Lit a a) List Value as' suf) in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn Let (forall (as :: [*]) (fn :: [*] -> * -> *) a. (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a, BaseUniverse fn) => fn as a -> List (Term fn) as -> Term fn a App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn PairFn fn as b fn) List (Term fn) (Append as (a : as')) args) (Var b v forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Pred fn -> Binder fn a :-> Pred fn ps) PairFn fn as b Pair | HOLE a a HOLE :? Value a b :> List Value as1 Nil <- ListCtx Value as (HOLE a) ctx -> let sameSnd :: [Prod a a] -> [a] sameSnd [Prod a a] ps = [a a | Prod a a a b' <- [Prod a a] ps, a b forall a. Eq a => a -> a -> Bool == a b'] in case Specification fn b spec of TypeSpec (Cartesian Specification fn a sa Specification fn a sb) OrdSet b cant | a b forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn a sb -> Specification fn a sa forall a. Semigroup a => a -> a -> a <> forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a notEqualSpec ([Prod a a] -> [a] sameSnd OrdSet b cant) -- TODO: better error message | Bool otherwise -> forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall a. [a] -> NonEmpty a NE.fromList [String "propagateSpecFun (Pair a b) has conformance failure on b", forall a. Show a => a -> String show Specification fn a sb]) MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec ([Prod a a] -> [a] sameSnd OrdSet b es) | Value a a :! NilCtx HOLE a b HOLE <- ListCtx Value as (HOLE a) ctx -> let sameFst :: [Prod a a] -> [a] sameFst [Prod a a] ps = [a b | Prod a a' a b <- [Prod a a] ps, a a forall a. Eq a => a -> a -> Bool == a a'] in case Specification fn b spec of TypeSpec (Cartesian Specification fn a sa Specification fn a sb) OrdSet b cant | a a forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a -> Bool `conformsToSpec` Specification fn a sa -> Specification fn a sb forall a. Semigroup a => a -> a -> a <> forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Specification fn a notEqualSpec ([Prod a a] -> [a] sameFst OrdSet b cant) -- TODO: better error message | Bool otherwise -> forall (fn :: [*] -> * -> *) a. NonEmpty String -> Specification fn a ErrorSpec (forall a. [a] -> NonEmpty a NE.fromList [String "propagateSpecFun (Pair a b) has conformance failure on a", forall a. Show a => a -> String show Specification fn a sa]) MemberSpec OrdSet b es -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec ([Prod a a] -> [a] sameFst OrdSet b es) 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