{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-name-shadowing #-}
module Constrained.TheKnot where
import Constrained.AbstractSyntax
import Constrained.Base
import Constrained.Conformance
import Constrained.Core
import Constrained.FunctionSymbol
import Constrained.GenT
import Constrained.Generation
import Constrained.Generic
import Constrained.List
import Constrained.NumOrd (
IntW (..),
NumLike,
NumSpec (..),
Numeric,
cardinality,
caseBoolSpec,
geqSpec,
leqSpec,
(<=.),
)
import Constrained.PrettyUtils
import Constrained.SumList
import Constrained.Syntax
import Control.Applicative
import Control.Monad
import Data.Foldable
import Data.Int
import Data.Kind
import Data.List (isPrefixOf, isSuffixOf, nub, (\\))
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import Data.String
import Data.Typeable
import Data.Word
import GHC.Natural
import GHC.Stack
import Prettyprinter hiding (cat)
import Test.QuickCheck hiding (Args, Fun, Witness, forAll, witness)
import Prelude hiding (cycle, pred)
instance Numeric a => Complete a where
simplifyA :: Specification a -> Specification a
simplifyA = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec
genFromSpecA :: forall (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecA = Specification a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT
ifElse :: (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse :: forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse Term Bool
b p
p q
q = Term Bool -> p -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
b p
p Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term Bool -> q -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (Term Bool -> Term Bool
not_ Term Bool
b) q
q
mapSpec ::
forall t a b.
AppRequires t '[a] b =>
t '[a] b ->
Specification a ->
Specification b
mapSpec :: forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t '[a] b
f (ExplainSpec [[Char]]
es SpecificationD Deps a
s) = [[Char]] -> Specification b -> Specification b
forall a. [[Char]] -> Specification a -> Specification a
explainSpecOpt [[Char]]
es (t '[a] b -> SpecificationD Deps a -> Specification b
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t '[a] b
f SpecificationD Deps a
s)
mapSpec t '[a] b
f SpecificationD Deps a
TrueSpec = t '[a] b -> TypeSpec a -> Specification b
forall a b.
(HasSpec a, HasSpec b) =>
t '[a] b -> TypeSpec a -> Specification b
forall (t :: [*] -> * -> *) a b.
(Logic t, HasSpec a, HasSpec b) =>
t '[a] b -> TypeSpec a -> Specification b
mapTypeSpec t '[a] b
f (forall a. HasSpec a => TypeSpec a
emptySpec @a)
mapSpec t '[a] b
_ (ErrorSpec NonEmpty [Char]
err) = NonEmpty [Char] -> Specification b
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec NonEmpty [Char]
err
mapSpec t '[a] b
f (MemberSpec NonEmpty a
as) = NonEmpty b -> Specification b
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (NonEmpty b -> Specification b) -> NonEmpty b -> Specification b
forall a b. (a -> b) -> a -> b
$ NonEmpty b -> NonEmpty b
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty b -> NonEmpty b) -> NonEmpty b -> NonEmpty b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> NonEmpty a -> NonEmpty b
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
f) NonEmpty a
as
mapSpec t '[a] b
f (SuspendedSpec Var a
x Pred
p) =
(Term b -> Pred) -> Specification b
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term b -> Pred) -> Specification b)
-> (Term b -> Pred) -> Specification b
forall a b. (a -> b) -> a -> b
$ \Term b
x' ->
((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (\forall b. TermD Deps b -> b
_ -> [Char] -> GE a
forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError [Char]
"mapSpec") (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ (Term b
x' Term b -> Term b -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. t '[a] b -> FunTy (MapList Term '[a]) (Term b)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm t '[a] b
f (Var a -> TermD Deps a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x)), Pred
p])
mapSpec t '[a] b
f (TypeSpec TypeSpec a
ts [a]
cant) = t '[a] b -> TypeSpec a -> Specification b
forall a b.
(HasSpec a, HasSpec b) =>
t '[a] b -> TypeSpec a -> Specification b
forall (t :: [*] -> * -> *) a b.
(Logic t, HasSpec a, HasSpec b) =>
t '[a] b -> TypeSpec a -> Specification b
mapTypeSpec t '[a] b
f TypeSpec a
ts Specification b -> Specification b -> Specification b
forall a. Semigroup a => a -> a -> a
<> [b] -> Specification b
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
f) [a]
cant)
pairView :: Term (Prod a b) -> Maybe (Term a, Term b)
pairView :: forall a b. Term (Prod a b) -> Maybe (Term a, Term b)
pairView (App (t dom (Prod a b) -> Maybe (ProdW dom (Prod a b))
forall {k1} {k2} (t :: k1 -> k2 -> *) (t' :: k1 -> k2 -> *)
(d :: k1) (r :: k2).
(Typeable t, Typeable d, Typeable r, Typeable t') =>
t d r -> Maybe (t' d r)
getWitness -> Just ProdW dom (Prod a b)
ProdW) (TermD Deps a
x :> TermD Deps a
y :> List Term as1
Nil)) = (Term a, Term b) -> Maybe (Term a, Term b)
forall a. a -> Maybe a
Just (Term a
TermD Deps a
x, Term b
TermD Deps a
y)
pairView TermD Deps (Prod a b)
_ = Maybe (Term a, Term b)
forall a. Maybe a
Nothing
cartesian ::
forall a b.
(HasSpec a, HasSpec b) =>
Specification a ->
Specification b ->
Specification (Prod a b)
cartesian :: forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian (ErrorSpec NonEmpty [Char]
es) (ErrorSpec NonEmpty [Char]
fs) = NonEmpty [Char] -> SpecificationD Deps (Prod a b)
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char]
es NonEmpty [Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. Semigroup a => a -> a -> a
<> NonEmpty [Char]
fs)
cartesian (ErrorSpec NonEmpty [Char]
es) SpecificationD Deps b
_ = NonEmpty [Char] -> SpecificationD Deps (Prod a b)
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec ([Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons [Char]
"cartesian left" NonEmpty [Char]
es)
cartesian SpecificationD Deps a
_ (ErrorSpec NonEmpty [Char]
es) = NonEmpty [Char] -> SpecificationD Deps (Prod a b)
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec ([Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons [Char]
"cartesian right" NonEmpty [Char]
es)
cartesian SpecificationD Deps a
s SpecificationD Deps b
s' = TypeSpec (Prod a b) -> SpecificationD Deps (Prod a b)
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec (Prod a b) -> SpecificationD Deps (Prod a b))
-> TypeSpec (Prod a b) -> SpecificationD Deps (Prod a b)
forall a b. (a -> b) -> a -> b
$ SpecificationD Deps a -> SpecificationD Deps b -> PairSpec a b
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian SpecificationD Deps a
s SpecificationD Deps b
s'
data PairSpec a b = Cartesian (Specification a) (Specification b)
instance (HasSpec a, HasSpec b) => HasSpec (Prod a b) where
type TypeSpec (Prod a b) = PairSpec a b
type Prerequisites (Prod a b) = (HasSpec a, HasSpec b)
emptySpec :: TypeSpec (Prod a b)
emptySpec = Specification a -> Specification b -> PairSpec a b
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian Specification a
forall a. Monoid a => a
mempty Specification b
forall a. Monoid a => a
mempty
combineSpec :: TypeSpec (Prod a b)
-> TypeSpec (Prod a b) -> Specification (Prod a b)
combineSpec (Cartesian Specification a
a Specification b
b) (Cartesian Specification a
a' Specification b
b') = Specification a -> Specification b -> Specification (Prod a b)
forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian (Specification a
a Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
a') (Specification b
b Specification b -> Specification b -> Specification b
forall a. Semigroup a => a -> a -> a
<> Specification b
b')
conformsTo :: HasCallStack => Prod a b -> TypeSpec (Prod a b) -> Bool
conformsTo (Prod a
a b
b) (Cartesian Specification a
sa Specification b
sb) = a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec a
a Specification a
sa Bool -> Bool -> Bool
&& b -> Specification b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec b
b Specification b
sb
genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Prod a b) -> GenT m (Prod a b)
genFromTypeSpec (Cartesian Specification a
sa Specification b
sb) = a -> b -> Prod a b
forall a b. a -> b -> Prod a b
Prod (a -> b -> Prod a b) -> GenT m a -> GenT m (b -> Prod a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
sa GenT m (b -> Prod a b) -> GenT m b -> GenT m (Prod a b)
forall a b. GenT m (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification b -> GenT m b
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification b
sb
shrinkWithTypeSpec :: TypeSpec (Prod a b) -> Prod a b -> [Prod a b]
shrinkWithTypeSpec (Cartesian Specification a
sa Specification b
sb) (Prod a
a b
b) =
[a -> b -> Prod a b
forall a b. a -> b -> Prod a b
Prod a
a' b
b | a
a' <- Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
sa a
a]
[Prod a b] -> [Prod a b] -> [Prod a b]
forall a. [a] -> [a] -> [a]
++ [a -> b -> Prod a b
forall a b. a -> b -> Prod a b
Prod a
a b
b' | b
b' <- Specification b -> b -> [b]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification b
sb b
b]
toPreds :: Term (Prod a b) -> TypeSpec (Prod a b) -> Pred
toPreds Term (Prod a b)
x (Cartesian Specification a
sf Specification b
ss) =
Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Prod a b) -> Term a
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ Term (Prod a b)
x) Specification a
sf
Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term b -> Specification b -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (Prod a b) -> Term b
forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_ Term (Prod a b)
x) Specification b
ss
cardinalTypeSpec :: TypeSpec (Prod a b) -> Specification Integer
cardinalTypeSpec (Cartesian Specification a
x Specification b
y) = (Specification a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
x) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Num a => a -> a -> a
+ (Specification b -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification b
y)
typeSpecHasError :: TypeSpec (Prod a b) -> Maybe (NonEmpty [Char])
typeSpecHasError (Cartesian Specification a
x Specification b
y) =
case (Specification a -> Bool
forall a. Specification a -> Bool
isErrorLike Specification a
x, Specification b -> Bool
forall a. Specification a -> Bool
isErrorLike Specification b
y) of
(Bool
False, Bool
False) -> Maybe (NonEmpty [Char])
forall a. Maybe a
Nothing
(Bool
True, Bool
False) -> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a. a -> Maybe a
Just (NonEmpty [Char] -> Maybe (NonEmpty [Char]))
-> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a b. (a -> b) -> a -> b
$ Specification a -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification a
x
(Bool
False, Bool
True) -> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a. a -> Maybe a
Just (NonEmpty [Char] -> Maybe (NonEmpty [Char]))
-> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a b. (a -> b) -> a -> b
$ Specification b -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification b
y
(Bool
True, Bool
True) -> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a. a -> Maybe a
Just (NonEmpty [Char] -> Maybe (NonEmpty [Char]))
-> NonEmpty [Char] -> Maybe (NonEmpty [Char])
forall a b. (a -> b) -> a -> b
$ (Specification a -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification a
x NonEmpty [Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. Semigroup a => a -> a -> a
<> Specification b -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification b
y)
alternateShow :: TypeSpec (Prod a b) -> BinaryShow
alternateShow (Cartesian Specification a
left right :: Specification b
right@(TypeSpec TypeSpec b
r [])) =
case forall a. HasSpec a => TypeSpec a -> BinaryShow
alternateShow @b TypeSpec b
r of
(BinaryShow [Char]
"Cartesian" [Doc a]
ps) -> [Char] -> [Doc a] -> BinaryShow
forall a. [Char] -> [Doc a] -> BinaryShow
BinaryShow [Char]
"Cartesian" (Doc a
"," Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc a
forall a ann. Show a => a -> Doc ann
viaShow Specification a
left Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: [Doc a]
ps)
(BinaryShow [Char]
"SumSpec" [Doc a]
ps) -> [Char] -> [Doc a] -> BinaryShow
forall a. [Char] -> [Doc a] -> BinaryShow
BinaryShow [Char]
"Cartesian" (Doc a
"," Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc a
forall a ann. Show a => a -> Doc ann
viaShow Specification a
left Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: [Doc a
"SumSpec" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep [Doc a]
ps])
BinaryShow
_ -> [Char] -> [Doc Any] -> BinaryShow
forall a. [Char] -> [Doc a] -> BinaryShow
BinaryShow [Char]
"Cartesian" [Doc Any
"," Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow Specification a
left, Doc Any
"," Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification b -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow Specification b
right]
alternateShow (Cartesian Specification a
left Specification b
right) = [Char] -> [Doc Any] -> BinaryShow
forall a. [Char] -> [Doc a] -> BinaryShow
BinaryShow [Char]
"Cartesian" [Doc Any
"," Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow Specification a
left, Doc Any
"," Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification b -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow Specification b
right]
instance (HasSpec a, HasSpec b) => Show (PairSpec a b) where
show :: PairSpec a b -> [Char]
show pair :: PairSpec a b
pair@(Cartesian Specification a
l Specification b
r) = case forall a. HasSpec a => TypeSpec a -> BinaryShow
alternateShow @(Prod a b) TypeSpec (Prod a b)
PairSpec a b
pair of
(BinaryShow [Char]
"Cartesian" [Doc a]
ps) -> Doc a -> [Char]
forall a. Show a => a -> [Char]
show (Doc a -> [Char]) -> Doc a -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc a -> Doc a
forall ann. Doc ann -> Doc ann
parens (Doc a
"Cartesian" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep [Doc a]
ps)
BinaryShow
_ -> [Char]
"(Cartesian " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> [Char]
forall a. Show a => a -> [Char]
show Specification a
l [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification b -> [Char]
forall a. Show a => a -> [Char]
show Specification b
r [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"))"
data ProdW :: [Type] -> Type -> Type where
ProdW :: (HasSpec a, HasSpec b) => ProdW '[a, b] (Prod a b)
ProdFstW :: (HasSpec a, HasSpec b) => ProdW '[Prod a b] a
ProdSndW :: (HasSpec a, HasSpec b) => ProdW '[Prod a b] b
deriving instance Eq (ProdW as b)
deriving instance Show (ProdW as b)
instance Syntax ProdW
instance Semantics ProdW where
semantics :: forall (d :: [*]) r. ProdW d r -> FunTy d r
semantics ProdW d r
ProdW = FunTy d r
a -> b -> Prod a b
forall a b. a -> b -> Prod a b
Prod
semantics ProdW d r
ProdFstW = FunTy d r
Prod r b -> r
forall a b. Prod a b -> a
prodFst
semantics ProdW d r
ProdSndW = FunTy d r
Prod a r -> r
forall a b. Prod a b -> b
prodSnd
instance Logic ProdW where
propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires ProdW as b, HasSpec a) =>
ProdW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec ProdW as b
ProdFstW (Unary HOLE a (Prod b b)
HOLE) TypeSpec b
ts [b]
cant = Specification b -> Specification b -> Specification (Prod b b)
forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant) Specification b
forall deps a. SpecificationD deps a
TrueSpec
propagateTypeSpec ProdW as b
ProdSndW (Unary HOLE a (Prod a b)
HOLE) TypeSpec b
ts [b]
cant =
Specification a -> Specification b -> Specification (Prod a b)
forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian Specification a
forall deps a. SpecificationD deps a
TrueSpec (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant)
propagateTypeSpec ProdW as b
ProdW (a
a :>: HOLE a b
HOLE) sc :: TypeSpec b
sc@(Cartesian Specification a
sa SpecificationD Deps a
sb) [b]
cant
| a
a a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
sa = SpecificationD Deps a
sb SpecificationD Deps a
-> SpecificationD Deps a -> SpecificationD Deps a
forall a. Semigroup a => a -> a -> a
<> (a -> SpecificationD Deps a) -> [a] -> SpecificationD Deps a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> SpecificationD Deps a
forall a. HasSpec a => a -> Specification a
notEqualSpec (a -> [Prod a a] -> [a]
forall a1 a2. Eq a1 => a1 -> [Prod a1 a2] -> [a2]
sameFst a
a [b]
[Prod a a]
cant)
| Bool
otherwise =
NonEmpty [Char] -> SpecificationD Deps a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[[Char]
"propagate (pair_ " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" HOLE) has conformance failure on a", Specification b -> [Char]
forall a. Show a => a -> [Char]
show (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
sc [b]
cant)]
)
propagateTypeSpec ProdW as b
ProdW (HOLE a a
HOLE :<: b
b) sc :: TypeSpec b
sc@(Cartesian SpecificationD Deps a
sa Specification b
sb) [b]
cant
| b
b b -> Specification b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
sb = SpecificationD Deps a
sa SpecificationD Deps a
-> SpecificationD Deps a -> SpecificationD Deps a
forall a. Semigroup a => a -> a -> a
<> (a -> SpecificationD Deps a) -> [a] -> SpecificationD Deps a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> SpecificationD Deps a
forall a. HasSpec a => a -> Specification a
notEqualSpec (b -> [Prod a b] -> [a]
forall a1 a2. Eq a1 => a1 -> [Prod a2 a1] -> [a2]
sameSnd b
b [b]
[Prod a b]
cant)
| Bool
otherwise =
NonEmpty [Char] -> SpecificationD Deps a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[[Char]
"propagate (pair_ HOLE " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> [Char]
forall a. Show a => a -> [Char]
show b
b [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") has conformance failure on b", Specification b -> [Char]
forall a. Show a => a -> [Char]
show (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
sc [b]
cant)]
)
propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires ProdW as b, HasSpec a) =>
ProdW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec ProdW as b
ProdFstW (Unary HOLE a (Prod b b)
HOLE) NonEmpty b
es = Specification b -> Specification b -> Specification (Prod b b)
forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian (NonEmpty b -> Specification b
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty b
es) Specification b
forall deps a. SpecificationD deps a
TrueSpec
propagateMemberSpec ProdW as b
ProdSndW (Unary HOLE a (Prod a b)
HOLE) NonEmpty b
es = Specification a -> Specification b -> Specification (Prod a b)
forall a b.
(HasSpec a, HasSpec b) =>
Specification a -> Specification b -> Specification (Prod a b)
cartesian Specification a
forall deps a. SpecificationD deps a
TrueSpec (NonEmpty b -> Specification b
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty b
es)
propagateMemberSpec ProdW as b
ProdW (a
a :>: HOLE a b
HOLE) NonEmpty b
es =
case ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub (a -> [Prod a a] -> [a]
forall a1 a2. Eq a1 => a1 -> [Prod a1 a2] -> [a2]
sameFst a
a (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es))) of
(a
w : [a]
ws) -> NonEmpty a -> SpecificationD Deps a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (a
w a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ws)
[] ->
NonEmpty [Char] -> SpecificationD Deps a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> SpecificationD Deps a)
-> NonEmpty [Char] -> SpecificationD Deps a
forall a b. (a -> b) -> a -> b
$
[[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"propagate (pair_ HOLE " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") on (MemberSpec " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> [Char]
forall a. Show a => a -> [Char]
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
, [Char]
"Where " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" does not appear as the fst component of anything in the MemberSpec."
]
propagateMemberSpec ProdW as b
ProdW (HOLE a a
HOLE :<: b
b) NonEmpty b
es =
case ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub (b -> [Prod a b] -> [a]
forall a1 a2. Eq a1 => a1 -> [Prod a2 a1] -> [a2]
sameSnd b
b (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es))) of
(a
w : [a]
ws) -> NonEmpty a -> SpecificationD Deps a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (a
w a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ws)
[] ->
NonEmpty [Char] -> SpecificationD Deps a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> SpecificationD Deps a)
-> NonEmpty [Char] -> SpecificationD Deps a
forall a b. (a -> b) -> a -> b
$
[[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"propagate (pair_ HOLE " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> [Char]
forall a. Show a => a -> [Char]
show b
b [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") on (MemberSpec " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> [Char]
forall a. Show a => a -> [Char]
show (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
, [Char]
"Where " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> [Char]
forall a. Show a => a -> [Char]
show b
b [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" does not appear as the snd component of anything in the MemberSpec."
]
rewriteRules :: forall (dom :: [*]) rng.
(TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
ProdW dom rng
-> List Term dom
-> Evidence (AppRequires ProdW dom rng)
-> Maybe (Term rng)
rewriteRules ProdW dom rng
ProdFstW ((Term a -> Maybe (Term rng, Term b)
Term (Prod rng b) -> Maybe (Term rng, Term b)
forall a b. Term (Prod a b) -> Maybe (Term a, Term b)
pairView -> Just (Term rng
x, Term b
_)) :> List Term as1
Nil) Evidence (AppRequires ProdW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just Term rng
x
rewriteRules ProdW dom rng
ProdSndW ((Term a -> Maybe (Term a, Term rng)
Term (Prod a rng) -> Maybe (Term a, Term rng)
forall a b. Term (Prod a b) -> Maybe (Term a, Term b)
pairView -> Just (Term a
_, Term rng
y)) :> List Term as1
Nil) Evidence (AppRequires ProdW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just Term rng
y
rewriteRules ProdW dom rng
_ List Term dom
_ Evidence (AppRequires ProdW dom rng)
_ = Maybe (Term rng)
forall a. Maybe a
Nothing
mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
ProdW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec ProdW '[a] b
ProdFstW (Cartesian Specification b
s Specification b
_) = Specification b
s
mapTypeSpec ProdW '[a] b
ProdSndW (Cartesian Specification a
_ Specification b
s) = Specification b
s
prodFst_ :: (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ :: forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term a
prodFst_ = ProdW '[Prod a b] a
-> FunTy (MapList Term '[Prod a b]) (TermD Deps a)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ProdW '[Prod a b] a
forall a t. (HasSpec a, HasSpec t) => ProdW '[Prod a t] a
ProdFstW
prodSnd_ :: (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_ :: forall a b. (HasSpec a, HasSpec b) => Term (Prod a b) -> Term b
prodSnd_ = ProdW '[Prod a b] b
-> FunTy (MapList Term '[Prod a b]) (TermD Deps b)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ProdW '[Prod a b] b
forall t b. (HasSpec t, HasSpec b) => ProdW '[Prod t b] b
ProdSndW
sameFst :: Eq a1 => a1 -> [Prod a1 a2] -> [a2]
sameFst :: forall a1 a2. Eq a1 => a1 -> [Prod a1 a2] -> [a2]
sameFst a1
a [Prod a1 a2]
ps = [a2
b | Prod a1
a' a2
b <- [Prod a1 a2]
ps, a1
a a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
a']
sameSnd :: Eq a1 => a1 -> [Prod a2 a1] -> [a2]
sameSnd :: forall a1 a2. Eq a1 => a1 -> [Prod a2 a1] -> [a2]
sameSnd a1
b [Prod a2 a1]
ps = [a2
a | Prod a2
a a1
b' <- [Prod a2 a1]
ps, a1
b a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
b']
prod_ :: (HasSpec a, HasSpec b) => Term a -> Term b -> Term (Prod a b)
prod_ :: forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> Term (Prod a b)
prod_ = ProdW '[a, b] (Prod a b)
-> FunTy (MapList Term '[a, b]) (TermD Deps (Prod a b))
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ProdW '[a, b] (Prod a b)
forall t a. (HasSpec t, HasSpec a) => ProdW '[t, a] (Prod t a)
ProdW
pattern Product ::
forall c.
() =>
forall a b.
( c ~ Prod a b
, AppRequires ProdW '[a, b] (Prod a b)
) =>
Term a ->
Term b ->
Term c
pattern $mProduct :: forall {r} {c}.
Term c
-> (forall {a} {b}.
(c ~ Prod a b, AppRequires ProdW '[a, b] (Prod a b)) =>
Term a -> Term b -> r)
-> ((# #) -> r)
-> r
Product x y <- (App (getWitness -> Just ProdW) (x :> y :> Nil))
data ElemW :: [Type] -> Type -> Type where
ElemW :: HasSpec a => ElemW '[a, [a]] Bool
deriving instance Eq (ElemW dom rng)
instance Show (ElemW dom rng) where
show :: ElemW dom rng -> [Char]
show ElemW dom rng
ElemW = [Char]
"elem_"
instance Syntax ElemW
instance Semantics ElemW where
semantics :: forall (d :: [*]) r. ElemW d r -> FunTy d r
semantics ElemW d r
ElemW = FunTy d r
a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem
instance Logic ElemW where
propagate :: forall (as :: [*]) b a.
(AppRequires ElemW as b, HasSpec a) =>
ElemW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate ElemW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [[Char]]
es SpecificationD Deps b
s) = [[Char]] -> Specification a -> Specification a
forall a. [[Char]] -> Specification a -> Specification a
explainSpec [[Char]]
es (Specification a -> Specification a)
-> Specification a -> Specification a
forall a b. (a -> b) -> a -> b
$ ElemW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires ElemW as b, HasSpec a) =>
ElemW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate ElemW as b
f ListCtx Value as (HOLE a)
ctxt SpecificationD Deps b
s
propagate ElemW as b
_ ListCtx Value as (HOLE a)
_ SpecificationD Deps b
TrueSpec = Specification a
forall deps a. SpecificationD deps a
TrueSpec
propagate ElemW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty [Char]
msgs) = NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec NonEmpty [Char]
msgs
propagate ElemW as b
ElemW (HOLE a a
HOLE :<: ([a]
x :: [w])) (SuspendedSpec Var b
v Pred
ps) =
(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
v' -> Term Bool -> BinderD Deps Bool -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (ElemW '[a, [a]] Bool -> List Term '[a, [a]] -> Term Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App ElemW '[a, [a]] Bool
forall t. HasSpec t => ElemW '[t, [t]] Bool
ElemW ((Term a
v' :: Term w) Term a -> List Term '[[a]] -> List Term '[a, [a]]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> [a] -> TermD Deps [a]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [a]
x TermD Deps [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)) (Var b
v Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
ps)
propagate ElemW as b
ElemW (a
x :>: HOLE a [a]
HOLE) (SuspendedSpec Var b
v Pred
ps) =
(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
v' -> Term Bool -> BinderD Deps Bool -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (ElemW '[a, [a]] Bool -> List Term '[a, [a]] -> Term Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App ElemW '[a, [a]] Bool
forall t. HasSpec t => ElemW '[t, [t]] Bool
ElemW (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
x TermD Deps a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
v' 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)) (Var b
v Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
ps)
propagate ElemW as b
ElemW (HOLE a a
HOLE :<: [a]
es) SpecificationD Deps b
spec =
Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case
Bool
True -> [a] -> NonEmpty [Char] -> Specification a
forall a. [a] -> NonEmpty [Char] -> Specification a
memberSpecList ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
[a]
es) ([Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"propagate on (elem_ x []), The empty list, [], has no solution")
Bool
False -> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a]
[a]
es
propagate ElemW as b
ElemW (a
e :>: HOLE a [a]
HOLE) SpecificationD Deps b
spec =
Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case
Bool
True -> TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [a
e] Specification Integer
forall a. Monoid a => a
mempty Specification a
forall a. Monoid a => a
mempty FoldSpec a
forall a. FoldSpec a
NoFold)
Bool
False -> TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [a]
forall a. Monoid a => a
mempty Specification Integer
forall a. Monoid a => a
mempty (a -> Specification a
forall a. HasSpec a => a -> Specification a
notEqualSpec a
e) FoldSpec a
forall a. FoldSpec a
NoFold)
rewriteRules :: forall (dom :: [*]) rng.
(TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
ElemW dom rng
-> List Term dom
-> Evidence (AppRequires ElemW dom rng)
-> Maybe (Term rng)
rewriteRules ElemW dom rng
ElemW (Term a
_ :> Lit [] :> List Term as1
Nil) Evidence (AppRequires ElemW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit Bool
False
rewriteRules ElemW dom rng
ElemW (Term a
t :> Lit [a
a] :> List Term as1
Nil) Evidence (AppRequires ElemW dom rng)
Evidence = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a
t Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a)
rewriteRules ElemW dom rng
_ List Term dom
_ Evidence (AppRequires ElemW dom rng)
_ = Maybe (Term rng)
forall a. Maybe a
Nothing
saturate :: forall (dom :: [*]). ElemW dom Bool -> List Term dom -> [Pred]
saturate ElemW dom Bool
ElemW ((FromGeneric (Product (Term a
x :: Term a) (Term b
y :: Term b)) :: Term c) :> Lit a
zs :> List Term as1
Nil)
| Just a :~: (a, b)
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @c @(a, b) = case a
zs of
((a, b)
w : [(a, b)]
ws) -> [Bool -> Term a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
True Term a
x (((a, b) -> a) -> NonEmpty (a, b) -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> a
forall a b. (a, b) -> a
fst ((a, b)
w (a, b) -> [(a, b)] -> NonEmpty (a, b)
forall a. a -> [a] -> NonEmpty a
:| [(a, b)]
ws))]
[] -> [NonEmpty [Char] -> Pred
forall deps. NonEmpty [Char] -> PredD deps
FalsePred ([Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> NonEmpty [Char]) -> [Char] -> NonEmpty [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"empty list, zs , in elem_ " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term a, Term b) -> [Char]
forall a. Show a => a -> [Char]
show (Term a
x, Term b
y) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" zs")]
| Bool
otherwise = []
saturate ElemW dom Bool
ElemW (Term a
x :> Lit (a
y : [a]
ys) :> List Term as1
Nil) = [Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
x (NonEmpty a -> SpecificationD Deps a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (a
y a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ys))]
saturate ElemW dom Bool
_ List Term dom
_ = []
infix 4 `elem_`
elem_ :: (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ :: forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ = ElemW '[a, [a]] Bool -> FunTy (MapList Term '[a, [a]]) (Term Bool)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ElemW '[a, [a]] Bool
forall t. HasSpec t => ElemW '[t, [t]] Bool
ElemW
elemFn :: HasSpec a => Fun '[a, [a]] Bool
elemFn :: forall a. HasSpec a => Fun '[a, [a]] Bool
elemFn = ElemW '[a, [a]] Bool -> Fun '[a, [a]] Bool
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun ElemW '[a, [a]] Bool
forall t. HasSpec t => ElemW '[t, [t]] Bool
ElemW
pattern Elem ::
forall b.
() =>
forall a.
(b ~ Bool, Eq a, HasSpec a) =>
Term a ->
Term [a] ->
Term b
pattern $mElem :: forall {r} {b}.
Term b
-> (forall {a}.
(b ~ Bool, Eq a, HasSpec a) =>
Term a -> Term [a] -> r)
-> ((# #) -> r)
-> r
Elem x y <-
( App
(getWitness -> Just ElemW)
(x :> y :> Nil)
)
data ListSpec a = ListSpec
{ forall a. ListSpec a -> Maybe Integer
listSpecHint :: Maybe Integer
, forall a. ListSpec a -> [a]
listSpecMust :: [a]
, forall a. ListSpec a -> Specification Integer
listSpecSize :: Specification Integer
, forall a. ListSpec a -> Specification a
listSpecElem :: Specification a
, forall a. ListSpec a -> FoldSpec a
listSpecFold :: FoldSpec a
}
instance HasSpec a => Show (FoldSpec a) where
showsPrec :: Int -> FoldSpec a -> ShowS
showsPrec Int
d = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS)
-> (FoldSpec a -> Doc Any) -> FoldSpec a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> FoldSpec a -> Doc Any
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
d
instance HasSpec a => Pretty (WithPrec (FoldSpec a)) where
pretty :: forall ann. WithPrec (FoldSpec a) -> Doc ann
pretty (WithPrec Int
_ FoldSpec a
NoFold) = Doc ann
"NoFold"
pretty (WithPrec Int
d (FoldSpec Fun '[a] b
fun Specification b
s)) =
Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Doc ann
"FoldSpec"
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
[ Doc ann
"fn =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Fun '[a] b -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Fun '[a] b
fun
, Doc ann
"spec =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification b -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification b -> Doc ann
pretty Specification b
s
]
instance HasSpec a => Pretty (FoldSpec a) where
pretty :: forall ann. FoldSpec a -> Doc ann
pretty = Int -> FoldSpec a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
0
instance HasSpec a => Show (ListSpec a) where
showsPrec :: Int -> ListSpec a -> ShowS
showsPrec Int
d = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS)
-> (ListSpec a -> Doc Any) -> ListSpec a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ListSpec a -> Doc Any
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
d
instance
HasSpec a =>
Pretty (WithPrec (ListSpec a))
where
pretty :: forall ann. WithPrec (ListSpec a) -> Doc ann
pretty (WithPrec Int
d ListSpec a
s) =
Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Doc ann
"ListSpec"
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
[ Doc ann
"hint =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Maybe Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (ListSpec a -> Maybe Integer
forall a. ListSpec a -> Maybe Integer
listSpecHint ListSpec a
s)
, Doc ann
"must =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [a] -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (ListSpec a -> [a]
forall a. ListSpec a -> [a]
listSpecMust ListSpec a
s)
, Doc ann
"size =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification Integer -> Doc ann
pretty (ListSpec a -> Specification Integer
forall a. ListSpec a -> Specification Integer
listSpecSize ListSpec a
s)
, Doc ann
"elem =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty (ListSpec a -> Specification a
forall a. ListSpec a -> Specification a
listSpecElem ListSpec a
s)
, Doc ann
"fold =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FoldSpec a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FoldSpec a -> Doc ann
pretty (ListSpec a -> FoldSpec a
forall a. ListSpec a -> FoldSpec a
listSpecFold ListSpec a
s)
]
instance HasSpec a => Pretty (ListSpec a) where
pretty :: forall ann. ListSpec a -> Doc ann
pretty = Int -> ListSpec a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
0
guardListSpec :: HasSpec a => [String] -> ListSpec a -> Specification [a]
guardListSpec :: forall a. HasSpec a => [[Char]] -> ListSpec a -> Specification [a]
guardListSpec [[Char]]
msg l :: ListSpec a
l@(ListSpec Maybe Integer
_hint [a]
must Specification Integer
size Specification a
elemS FoldSpec a
_fold)
| ErrorSpec NonEmpty [Char]
es <- Specification Integer
size = NonEmpty [Char] -> SpecificationD Deps [a]
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> SpecificationD Deps [a])
-> NonEmpty [Char] -> SpecificationD Deps [a]
forall a b. (a -> b) -> a -> b
$ ([[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([Char]
"Error in size of ListSpec" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
msg)) NonEmpty [Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. Semigroup a => a -> a -> a
<> NonEmpty [Char]
es
| Just Integer
u <- Specification Integer -> Maybe Integer
forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification Integer
size
, Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 =
NonEmpty [Char] -> SpecificationD Deps [a]
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> SpecificationD Deps [a])
-> NonEmpty [Char] -> SpecificationD Deps [a]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([[Char]
"Negative size in guardListSpec", Specification Integer -> [Char]
forall a. Show a => a -> [Char]
show Specification Integer
size] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
msg)
| Bool -> Bool
not ((a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) [a]
must) =
NonEmpty [Char] -> SpecificationD Deps [a]
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> SpecificationD Deps [a])
-> NonEmpty [Char] -> SpecificationD Deps [a]
forall a b. (a -> b) -> a -> b
$
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
([[Char]
"Some items in the must list do not conform to 'element' spec.", [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> [Char]
forall a. Show a => a -> [Char]
show Specification a
elemS] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
msg)
)
| Bool
otherwise = (TypeSpec [a] -> SpecificationD Deps [a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec [a]
ListSpec a
l)
instance (Sized [a], HasSpec a) => HasSpec [a] where
type TypeSpec [a] = ListSpec a
type Prerequisites [a] = HasSpec a
emptySpec :: TypeSpec [a]
emptySpec = Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [] Specification Integer
forall a. Monoid a => a
mempty Specification a
forall a. Monoid a => a
mempty FoldSpec a
forall a. FoldSpec a
NoFold
combineSpec :: TypeSpec [a] -> TypeSpec [a] -> Specification [a]
combineSpec l1 :: TypeSpec [a]
l1@(ListSpec Maybe Integer
msz [a]
must Specification Integer
size Specification a
elemS FoldSpec a
foldS) l2 :: TypeSpec [a]
l2@(ListSpec Maybe Integer
msz' [a]
must' Specification Integer
size' Specification a
elemS' FoldSpec a
foldS') =
let must'' :: [a]
must'' = [a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a]
must [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
must'
elemS'' :: Specification a
elemS'' = Specification a
elemS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> Specification a
elemS'
size'' :: Specification Integer
size'' = Specification Integer
size Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
size'
foldeither :: Either [[Char]] (FoldSpec a)
foldeither = FoldSpec a -> FoldSpec a -> Either [[Char]] (FoldSpec a)
forall a. FoldSpec a -> FoldSpec a -> Either [[Char]] (FoldSpec a)
combineFoldSpec FoldSpec a
foldS FoldSpec a
foldS'
msg :: [[Char]]
msg = [[Char]
"Error in combineSpec for ListSpec", [Char]
"1) " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeSpec [a] -> [Char]
forall a. Show a => a -> [Char]
show TypeSpec [a]
l1, [Char]
"2) " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeSpec [a] -> [Char]
forall a. Show a => a -> [Char]
show TypeSpec [a]
l2]
in case Either [[Char]] (FoldSpec a)
foldeither of
Left [[Char]]
foldmsg -> NonEmpty [Char] -> Specification [a]
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec ([[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([[Char]]
msg [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
foldmsg))
Right FoldSpec a
fold'' -> [[Char]] -> ListSpec a -> Specification [a]
forall a. HasSpec a => [[Char]] -> ListSpec a -> Specification [a]
guardListSpec [[Char]]
msg (ListSpec a -> Specification [a])
-> ListSpec a -> Specification [a]
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
msz Maybe Integer
msz') [a]
must'' Specification Integer
size'' Specification a
elemS'' FoldSpec a
fold''
genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec [a] -> GenT m [a]
genFromTypeSpec (ListSpec Maybe Integer
_ [a]
must Specification Integer
_ Specification a
elemS FoldSpec a
_)
| (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS)) [a]
must =
[Char] -> GenT m [a]
forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
genError [Char]
"genTypeSpecSpec @ListSpec: some elements of mustSet do not conform to elemS"
genFromTypeSpec (ListSpec Maybe Integer
msz [a]
must Specification Integer
TrueSpec Specification a
elemS FoldSpec a
NoFold) = do
[a]
lst <- case Maybe Integer
msz of
Maybe Integer
Nothing -> GenT GE a -> GenT m [a]
forall (m :: * -> *) a. MonadGenError m => GenT GE a -> GenT m [a]
listOfT (GenT GE a -> GenT m [a]) -> GenT GE a -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS
Just Integer
szHint -> do
Integer
sz <- Specification Integer -> GenT m Integer
forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec Integer
szHint)
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
listOfUntilLenT (Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sz) (Bool -> Int -> Bool
forall a b. a -> b -> a
const Bool
True)
Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> Gen [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle ([a]
must [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
lst)
genFromTypeSpec (ListSpec Maybe Integer
msz [a]
must Specification Integer
szSpec Specification a
elemS FoldSpec a
NoFold) = do
Integer
sz0 <- Specification Integer -> GenT m Integer
forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec (Specification Integer
szSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec ([a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
must) Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
msz)
let sz :: Int
sz = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
sz0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- [a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
must)
[a]
lst <-
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
listOfUntilLenT
(Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS)
Int
sz
((Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
szSpec) (Integer -> Bool) -> (Int -> Integer) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
must) (Integer -> Integer) -> (Int -> Integer) -> Int -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral)
Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> Gen [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle ([a]
must [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
lst)
genFromTypeSpec (ListSpec Maybe Integer
msz [a]
must Specification Integer
szSpec Specification a
elemS (FoldSpec Fun '[a] b
f Specification b
foldS)) = do
let szSpec' :: Specification Integer
szSpec' = Specification Integer
szSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Specification Integer
-> (Integer -> Specification Integer)
-> Maybe Integer
-> Specification Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Specification Integer
forall deps a. SpecificationD deps a
TrueSpec (Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (Integer -> Specification Integer)
-> (Integer -> Integer) -> Integer -> Specification Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
msz
[a]
-> Specification Integer
-> Specification a
-> Fun '[a] b
-> Specification b
-> GenT m [a]
forall (m :: * -> *) a b.
(MonadGenError m, Foldy b, HasSpec a) =>
[a]
-> Specification Integer
-> Specification a
-> Fun '[a] b
-> Specification b
-> GenT m [a]
genFromFold [a]
must Specification Integer
szSpec' Specification a
elemS Fun '[a] b
f Specification b
foldS
shrinkWithTypeSpec :: TypeSpec [a] -> [a] -> [[a]]
shrinkWithTypeSpec (ListSpec Maybe Integer
_ [a]
_ Specification Integer
_ Specification a
es FoldSpec a
_) [a]
as =
(a -> [a]) -> [a] -> [[a]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
es) [a]
as
cardinalTypeSpec :: TypeSpec [a] -> Specification Integer
cardinalTypeSpec TypeSpec [a]
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
guardTypeSpec :: [[Char]] -> TypeSpec [a] -> Specification [a]
guardTypeSpec = [[Char]] -> TypeSpec [a] -> Specification [a]
[[Char]] -> ListSpec a -> Specification [a]
forall a. HasSpec a => [[Char]] -> ListSpec a -> Specification [a]
guardListSpec
conformsTo :: HasCallStack => [a] -> TypeSpec [a] -> Bool
conformsTo [a]
xs (ListSpec Maybe Integer
_ [a]
must Specification Integer
size Specification a
elemS FoldSpec a
foldS) =
[a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
xs
Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
Bool -> Bool -> Bool
&& (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
xs) [a]
must
Bool -> Bool -> Bool
&& (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) [a]
xs
Bool -> Bool -> Bool
&& [a]
xs
[a] -> FoldSpec a -> Bool
forall a. [a] -> FoldSpec a -> Bool
`conformsToFoldSpec` FoldSpec a
foldS
toPreds :: Term [a] -> TypeSpec [a] -> Pred
toPreds Term [a]
x (ListSpec Maybe Integer
msz [a]
must Specification Integer
size Specification a
elemS FoldSpec a
foldS) =
(Term [a] -> (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 [a]
x ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x' -> Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
x' Specification a
elemS)
Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> (Term [a] -> (Term a -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll ([a] -> Term [a]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [a]
must) ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x' -> Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term a -> Term [a] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term a
x' Term [a]
x))
Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term [a] -> FoldSpec a -> Pred
forall a. HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec Term [a]
x FoldSpec a
foldS
Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term [a] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [a]
x) Specification Integer
size
Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Pred -> (Hint [a] -> Pred) -> Maybe (Hint [a]) -> Pred
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
forall deps. PredD deps
TruePred ((Hint [a] -> Term [a] -> Pred) -> Term [a] -> Hint [a] -> Pred
forall a b c. (a -> b -> c) -> b -> a -> c
flip Hint [a] -> Term [a] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Term [a]
x) Maybe Integer
Maybe (Hint [a])
msz
sizeOf_ :: (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ :: forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ = (List Term '[a] -> Term Integer)
-> FunTy (MapList Term '[a]) (Term Integer)
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
forall (f :: * -> *) r.
(List f '[a] -> r) -> FunTy (MapList f '[a]) r
curryList (SizeW '[a] Integer -> List Term '[a] -> Term Integer
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App SizeW '[a] Integer
forall t. (Sized t, HasSpec t) => SizeW '[t] Integer
SizeOfW)
genFromSizeSpec :: MonadGenError m => Specification Integer -> GenT m Integer
genFromSizeSpec :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec Specification Integer
integerSpec = Specification Integer -> GenT m Integer
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT (Specification Integer
integerSpec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec Integer
0)
instance (Sized [a], HasSpec a) => HasGenHint [a] where
type Hint [a] = Integer
giveHint :: Hint [a] -> Specification [a]
giveHint Hint [a]
szHint = TypeSpec [a] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec [a] -> Specification [a])
-> TypeSpec [a] -> Specification [a]
forall a b. (a -> b) -> a -> b
$ Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec (Hint [a] -> Maybe (Hint [a])
forall a. a -> Maybe a
Just Hint [a]
szHint) [] Specification Integer
forall a. Monoid a => a
mempty Specification a
forall a. Monoid a => a
mempty FoldSpec a
forall a. FoldSpec a
NoFold
instance Forallable [a] a where
fromForAllSpec :: (HasSpec [a], HasSpec a) => Specification a -> Specification [a]
fromForAllSpec Specification a
es = TypeSpec [a] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [] Specification Integer
forall a. Monoid a => a
mempty Specification a
es FoldSpec a
forall a. FoldSpec a
NoFold)
forAllToList :: [a] -> [a]
forAllToList = [a] -> [a]
forall a. a -> a
id
data ListW (args :: [Type]) (res :: Type) where
FoldMapW :: forall a b. (Foldy b, HasSpec a) => Fun '[a] b -> ListW '[[a]] b
SingletonListW :: HasSpec a => ListW '[a] [a]
AppendW :: (HasSpec a, Typeable a, Show a) => ListW '[[a], [a]] [a]
instance Semantics ListW where
semantics :: forall (d :: [*]) r. ListW d r -> FunTy d r
semantics = ListW d r -> FunTy d r
forall (d :: [*]) r. ListW d r -> FunTy d r
listSem
instance Syntax ListW where
prettySymbol :: forall deps (dom :: [*]) rng ann.
ListW dom rng -> List (TermD deps) dom -> Int -> Maybe (Doc ann)
prettySymbol ListW dom rng
AppendW (Lit a
n :> TermD deps a
y :> List (TermD deps) as1
Nil) Int
p = Doc ann -> Maybe (Doc ann)
forall a. a -> Maybe a
Just (Doc ann -> Maybe (Doc ann)) -> Doc ann -> Maybe (Doc ann)
forall a b. (a -> b) -> a -> b
$ Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"append_" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [a] -> Doc ann
forall a x. (Show a, Typeable a) => [a] -> Doc x
short a
[a]
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> TermD deps a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 TermD deps a
y
prettySymbol ListW dom rng
AppendW (TermD deps a
y :> Lit a
n :> List (TermD deps) as1
Nil) Int
p = Doc ann -> Maybe (Doc ann)
forall a. a -> Maybe a
Just (Doc ann -> Maybe (Doc ann)) -> Doc ann -> Maybe (Doc ann)
forall a b. (a -> b) -> a -> b
$ Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"append_" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> TermD deps a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 TermD deps a
y Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [a] -> Doc ann
forall a x. (Show a, Typeable a) => [a] -> Doc x
short a
[a]
n
prettySymbol ListW dom rng
_ List (TermD deps) dom
_ Int
_ = Maybe (Doc ann)
forall a. Maybe a
Nothing
listSem :: ListW dom rng -> FunTy dom rng
listSem :: forall (d :: [*]) r. ListW d r -> FunTy d r
listSem (FoldMapW (Fun t '[a] rng
f)) = [rng] -> rng
forall a. Foldy a => [a] -> a
adds ([rng] -> rng) -> ([a] -> [rng]) -> [a] -> rng
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> rng) -> [a] -> [rng]
forall a b. (a -> b) -> [a] -> [b]
map (t '[a] rng -> FunTy '[a] rng
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] rng
f)
listSem ListW dom rng
SingletonListW = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [])
listSem ListW dom rng
AppendW = FunTy dom rng
[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
instance Show (ListW d r) where
show :: ListW d r -> [Char]
show ListW d r
AppendW = [Char]
"append_"
show ListW d r
SingletonListW = [Char]
"singletonList_"
show (FoldMapW Fun '[a] r
n) = [Char]
"(FoldMapW " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Fun '[a] r -> [Char]
forall a. Show a => a -> [Char]
show Fun '[a] r
n [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
deriving instance (Eq (ListW d r))
instance Logic ListW where
propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires ListW as b, HasSpec a) =>
ListW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec (FoldMapW Fun '[a] b
f) (Unary HOLE a [a]
HOLE) TypeSpec b
ts [b]
cant =
TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [] Specification Integer
forall deps a. SpecificationD deps a
TrueSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec (FoldSpec a -> ListSpec a) -> FoldSpec a -> ListSpec a
forall a b. (a -> b) -> a -> b
$ Fun '[a] b -> Specification b -> FoldSpec a
forall t a.
(HasSpec a, HasSpec t, Foldy t) =>
Fun '[a] t -> Specification t -> FoldSpec a
FoldSpec Fun '[a] b
f (TypeSpec b -> [b] -> Specification b
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant))
propagateTypeSpec ListW as b
SingletonListW (Unary HOLE a a
HOLE) (ListSpec Maybe Integer
_ [a]
m Specification Integer
sz Specification a
e FoldSpec a
f) [b]
cant
| [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 =
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> Specification a)
-> NonEmpty [Char] -> Specification a
forall a b. (a -> b) -> a -> b
$
[[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"Too many required elements for SingletonListW : "
, [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> [Char]
forall a. Show a => a -> [Char]
show [a]
m
]
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Specification Integer -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
sz =
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> Specification a)
-> NonEmpty [Char] -> Specification a
forall a b. (a -> b) -> a -> b
$ [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> NonEmpty [Char]) -> [Char] -> NonEmpty [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"Size spec requires too many elements for SingletonListW : " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> [Char]
forall a. Show a => a -> [Char]
show Specification Integer
sz
| bad :: [a]
bad@(a
_ : [a]
_) <- (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e)) [a]
m =
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> Specification a)
-> NonEmpty [Char] -> Specification a
forall a b. (a -> b) -> a -> b
$
[[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"The following elements of the must spec do not conforms to the elem spec:"
, [a] -> [Char]
forall a. Show a => a -> [Char]
show [a]
bad
]
| [a
a] <- [a]
m = a -> Specification a
forall a. a -> Specification a
equalSpec a
a Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
z | [a
z] <- [b]
cant] Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> FoldSpec a -> Specification a
forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec a
f
| Bool
otherwise = Specification a
e Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
a | [a
a] <- [b]
cant] Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> FoldSpec a -> Specification a
forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec a
f
propagateTypeSpec ListW as b
AppendW ListCtx Value as (HOLE a)
ctx (ts :: TypeSpec b
ts@ListSpec {listSpecElem :: forall a. ListSpec a -> Specification a
listSpecElem = Specification a
e}) [b]
cant
| (HOLE a a
HOLE :? Value ([a]
ys :: [a]) :> List Value as1
Nil) <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a]
, (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e) [a]
ys =
TypeSpec [a] -> [[a]] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec ([a] -> ListSpec a -> ListSpec a
forall a. Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave [a]
ys TypeSpec b
ListSpec a
ts) ([a] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [[a]] -> [[a]]
suffixedBy [a]
ys [b]
[[a]]
cant)
| (Value ([a]
ys :: [a]) :! Unary HOLE a [a]
HOLE) <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a]
, (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> Specification a -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e) [a]
ys =
TypeSpec [a] -> [[a]] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec ([a] -> ListSpec a -> ListSpec a
forall a. Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave [a]
ys TypeSpec b
ListSpec a
ts) ([a] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys [b]
[[a]]
cant)
| Bool
otherwise = NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> Specification a)
-> NonEmpty [Char] -> Specification a
forall a b. (a -> b) -> a -> b
$ [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"The spec given to propagate for AppendW is inconsistent!"
propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires ListW as b, HasSpec a) =>
ListW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec (FoldMapW Fun '[a] b
f) (Unary HOLE a [a]
HOLE) NonEmpty b
es =
TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [] Specification Integer
forall deps a. SpecificationD deps a
TrueSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec (FoldSpec a -> ListSpec a) -> FoldSpec a -> ListSpec a
forall a b. (a -> b) -> a -> b
$ Fun '[a] b -> Specification b -> FoldSpec a
forall t a.
(HasSpec a, HasSpec t, Foldy t) =>
Fun '[a] t -> Specification t -> FoldSpec a
FoldSpec Fun '[a] b
f (NonEmpty b -> Specification b
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty b
es))
propagateMemberSpec ListW as b
SingletonListW (Unary HOLE a a
HOLE) NonEmpty b
xss =
case [a
a | [a
a] <- NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
xss] of
[] ->
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec (NonEmpty [Char] -> Specification a)
-> NonEmpty [Char] -> Specification a
forall a b. (a -> b) -> a -> b
$ ([Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"PropagateSpec SingletonListW with MemberSpec which has no lists of length 1")
(a
x : [a]
xs) -> NonEmpty a -> Specification a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
propagateMemberSpec ListW as b
AppendW ListCtx Value as (HOLE a)
ctx NonEmpty b
xss
| (HOLE a [a]
HOLE :<: ([a]
ys :: [a])) <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a] =
case [a] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [[a]] -> [[a]]
suffixedBy [a]
ys (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
xss) of
[] ->
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"propagateSpecFun (append HOLE ys) with (MemberSpec xss)"
, [Char]
"there are no elements in xss with suffix ys"
]
)
([a]
x : [[a]]
xs) -> NonEmpty [a] -> SpecificationD Deps [a]
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec ([a]
x [a] -> [[a]] -> NonEmpty [a]
forall a. a -> [a] -> NonEmpty a
:| [[a]]
xs)
| (([a]
ys :: [a]) :>: HOLE a [a]
HOLE) <- ListCtx Value as (HOLE a)
ctx
, Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a] =
case [a] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
xss) of
[] ->
NonEmpty [Char] -> Specification a
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"propagateSpecFun (append ys HOLE) with (MemberSpec xss)"
, [Char]
"there are no elements in xss with prefix ys"
]
)
([a]
x : [[a]]
xs) -> NonEmpty [a] -> SpecificationD Deps [a]
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec ([a]
x [a] -> [[a]] -> NonEmpty [a]
forall a. a -> [a] -> NonEmpty a
:| [[a]]
xs)
mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
ListW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec ListW '[a] b
SingletonListW TypeSpec a
ts = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [] (Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
1) (TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts) FoldSpec a
forall a. FoldSpec a
NoFold)
mapTypeSpec (FoldMapW Fun '[a] b
g) TypeSpec a
ts =
(Term b -> Pred) -> Specification b
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term b -> Pred) -> Specification b)
-> (Term b -> Pred) -> Specification b
forall a b. (a -> b) -> a -> b
$ \Term b
x ->
(Term [a] -> Pred) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term [a] -> Pred) -> Pred) -> (Term [a] -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term [a]
x' ->
Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term b
x Term b -> Term b -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Fun '[[a]] b -> Term [a] -> Term b
forall x b. Fun '[x] b -> Term x -> Term b
appFun (Fun '[a] b -> Fun '[[a]] b
forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn Fun '[a] b
g) Term [a]
x') Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term [a] -> TypeSpec [a] -> Pred
forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term [a]
x' TypeSpec a
TypeSpec [a]
ts
foldMap_ :: forall a b. (Foldy b, HasSpec a) => (Term a -> Term b) -> Term [a] -> Term b
foldMap_ :: forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term a -> Term b
f = Fun '[[a]] b -> Term [a] -> Term b
forall x b. Fun '[x] b -> Term x -> Term b
appFun (Fun '[[a]] b -> Term [a] -> Term b)
-> Fun '[[a]] b -> Term [a] -> Term b
forall a b. (a -> b) -> a -> b
$ Fun '[a] b -> Fun '[[a]] b
forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn (Fun '[a] b -> Fun '[[a]] b) -> Fun '[a] b -> Fun '[[a]] b
forall a b. (a -> b) -> a -> b
$ Term b -> Fun '[a] b
forall x. HasCallStack => Term x -> Fun '[a] x
toFn (Term b -> Fun '[a] b) -> Term b -> Fun '[a] b
forall a b. (a -> b) -> a -> b
$ Term a -> Term b
f (Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
v)
where
v :: Var a
v = Int -> [Char] -> Var a
forall a. Int -> [Char] -> Var a
Var (-Int
1) [Char]
"v" :: Var a
toFn :: forall x. HasCallStack => Term x -> Fun '[a] x
toFn :: forall x. HasCallStack => Term x -> Fun '[a] x
toFn (App t dom x
fn (V Var a
v' :> List Term as1
Nil)) | Just a :~: a
Refl <- Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a
v' = t dom x -> Fun dom x
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun t dom x
fn
toFn (App t dom x
fn (TermD Deps a
t :> List Term as1
Nil)) = Fun '[a] x -> Fun '[a] a -> Fun '[a] x
forall b c a.
(HasSpec b, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn (t dom x -> Fun dom x
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun t dom x
fn) (TermD Deps a -> Fun '[a] a
forall x. HasCallStack => Term x -> Fun '[a] x
toFn TermD Deps a
t)
toFn (V Var x
v') | Just a :~: x
Refl <- Var a -> Var x -> Maybe (a :~: x)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var x
v' = Fun '[a] a
Fun '[a] x
forall a. HasSpec a => Fun '[a] a
idFn
toFn TermD Deps x
_ = [Char] -> Fun '[a] x
forall a. HasCallStack => [Char] -> a
error [Char]
"foldMap_ has not been given a function of the form \\ x -> f (g ... (h x))"
sum_ ::
Foldy a =>
Term [a] ->
Term a
sum_ :: forall a. Foldy a => Term [a] -> Term a
sum_ = (Term a -> Term a) -> Term [a] -> Term a
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term a -> Term a
forall a. a -> a
id
singletonList_ :: (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ :: forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ = ListW '[a] [a] -> FunTy (MapList Term '[a]) (TermD Deps [a])
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ListW '[a] [a]
forall t. HasSpec t => ListW '[t] [t]
SingletonListW
append_ :: (Sized [a], HasSpec a) => Term [a] -> Term [a] -> Term [a]
append_ :: forall a.
(Sized [a], HasSpec a) =>
Term [a] -> Term [a] -> Term [a]
append_ = ListW '[[a], [a]] [a]
-> FunTy (MapList Term '[[a], [a]]) (TermD Deps [a])
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm ListW '[[a], [a]] [a]
forall t. (HasSpec t, Typeable t, Show t) => ListW '[[t], [t]] [t]
AppendW
appendFn :: forall a. (Sized [a], HasSpec a) => Fun '[[a], [a]] [a]
appendFn :: forall a. (Sized [a], HasSpec a) => Fun '[[a], [a]] [a]
appendFn = ListW '[[a], [a]] [a] -> Fun '[[a], [a]] [a]
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun ListW '[[a], [a]] [a]
forall t. (HasSpec t, Typeable t, Show t) => ListW '[[t], [t]] [t]
AppendW
singletonListFn :: forall a. HasSpec a => Fun '[a] [a]
singletonListFn :: forall a. HasSpec a => Fun '[a] [a]
singletonListFn = ListW '[a] [a] -> Fun '[a] [a]
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun ListW '[a] [a]
forall t. HasSpec t => ListW '[t] [t]
SingletonListW
foldMapFn :: forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn :: forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn Fun '[a] b
f = ListW '[[a]] b -> Fun '[[a]] b
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun (Fun '[a] b -> ListW '[[a]] b
forall t b. (Foldy b, HasSpec t) => Fun '[t] b -> ListW '[[t]] b
FoldMapW Fun '[a] b
f)
reverseFoldSpec :: FoldSpec a -> Specification a
reverseFoldSpec :: forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec a
NoFold = SpecificationD Deps a
forall deps a. SpecificationD deps a
TrueSpec
reverseFoldSpec (FoldSpec (Fun t '[a] b
fn) Specification b
spec) = t '[a] b
-> ListCtx Value '[a] (HOLE a)
-> Specification b
-> SpecificationD Deps a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t '[a] b
fn (HOLE a a
forall a. HOLE a a
HOLE HOLE a a -> List Value '[] -> ListCtx Value '[a] (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification b
spec
prefixedBy :: Eq a => [a] -> [[a]] -> [[a]]
prefixedBy :: forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys [[a]]
xss = [Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys) [a]
xs | [a]
xs <- [[a]]
xss, [a]
ys [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [a]
xs]
suffixedBy :: Eq a => [a] -> [[a]] -> [[a]]
suffixedBy :: forall a. Eq a => [a] -> [[a]] -> [[a]]
suffixedBy [a]
ys [[a]]
xss = [Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys) [a]
xs | [a]
xs <- [[a]]
xss, [a]
ys [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [a]
xs]
alreadyHave :: Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave :: forall a. Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave [a]
ys (ListSpec Maybe Integer
h [a]
m Specification Integer
sz Specification a
e FoldSpec a
f) =
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
((Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract ([a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
ys)) Maybe Integer
h)
([a]
m [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
ys)
((Term Integer -> Pred) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Pred) -> Specification Integer)
-> (Term Integer -> Pred) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
x -> (Term Integer
x Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
+ Integer -> Term Integer
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ([a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
ys)) Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
sz)
Specification a
e
([a] -> FoldSpec a -> FoldSpec a
forall a. [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold [a]
ys FoldSpec a
f)
alreadyHaveFold :: [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold :: forall a. [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold [a]
_ FoldSpec a
NoFold = FoldSpec a
forall a. FoldSpec a
NoFold
alreadyHaveFold [a]
ys (FoldSpec Fun '[a] b
fn Specification b
spec) =
Fun '[a] b -> Specification b -> FoldSpec a
forall t a.
(HasSpec a, HasSpec t, Foldy t) =>
Fun '[a] t -> Specification t -> FoldSpec a
FoldSpec
Fun '[a] b
fn
((Term b -> Pred) -> Specification b
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term b -> Pred) -> Specification b)
-> (Term b -> Pred) -> Specification b
forall a b. (a -> b) -> a -> b
$ \Term b
s -> IntW '[b, b] b -> FunTy (MapList Term '[b, b]) (Term b)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm IntW '[b, b] b
forall a. Foldy a => IntW '[a, a] a
theAddFn Term b
s ((Term a -> Term b) -> Term [a] -> Term b
forall a b.
(Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ (Fun '[a] b -> Term a -> Term b
forall x b. Fun '[x] b -> Term x -> Term b
appFun Fun '[a] b
fn) ([a] -> Term [a]
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit [a]
ys)) Term b -> Specification b -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification b
spec)
toPredsFoldSpec :: HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec :: forall a. HasSpec a => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec Term [a]
_ FoldSpec a
NoFold = Pred
forall deps. PredD deps
TruePred
toPredsFoldSpec Term [a]
x (FoldSpec Fun '[a] b
funAB Specification b
sspec) =
Term b -> Specification b -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Fun '[[a]] b -> Term [a] -> Term b
forall x b. Fun '[x] b -> Term x -> Term b
appFun (Fun '[a] b -> Fun '[[a]] b
forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn Fun '[a] b
funAB) Term [a]
x) Specification b
sspec
data FoldSpec a where
NoFold :: FoldSpec a
FoldSpec ::
forall b a.
( HasSpec a
, HasSpec b
, Foldy b
) =>
Fun '[a] b ->
Specification b ->
FoldSpec a
preMapFoldSpec :: HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec :: forall a b. HasSpec a => Fun '[a] b -> FoldSpec b -> FoldSpec a
preMapFoldSpec Fun '[a] b
_ FoldSpec b
NoFold = FoldSpec a
forall a. FoldSpec a
NoFold
preMapFoldSpec Fun '[a] b
f (FoldSpec Fun '[b] b
g Specification b
s) = Fun '[a] b -> Specification b -> FoldSpec a
forall t a.
(HasSpec a, HasSpec t, Foldy t) =>
Fun '[a] t -> Specification t -> FoldSpec a
FoldSpec (Fun '[b] b -> Fun '[a] b -> Fun '[a] b
forall b c a.
(HasSpec b, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn Fun '[b] b
g Fun '[a] b
f) Specification b
s
composeFn :: (HasSpec b, HasSpec c) => Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn :: forall b c a.
(HasSpec b, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn (Fun t '[b] c
f) (Fun t '[a] b
g) = (FunW '[a] c -> Fun '[a] c
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun (t '[b] c -> t '[a] b -> FunW '[a] c
forall t (a :: [*] -> * -> *) (b :: [*] -> * -> *) a r.
(AppRequires a '[t] r, AppRequires b '[a] t, HasSpec t) =>
a '[t] r -> b '[a] t -> FunW '[a] r
ComposeW t '[b] c
f t '[a] b
g))
idFn :: HasSpec a => Fun '[a] a
idFn :: forall a. HasSpec a => Fun '[a] a
idFn = FunW '[a] a -> Fun '[a] a
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[a] a
forall a. FunW '[a] a
IdW
combineFoldSpec :: FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec :: forall a. FoldSpec a -> FoldSpec a -> Either [[Char]] (FoldSpec a)
combineFoldSpec FoldSpec a
NoFold FoldSpec a
s = FoldSpec a -> Either [[Char]] (FoldSpec a)
forall a. a -> Either [[Char]] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec a
s
combineFoldSpec FoldSpec a
s FoldSpec a
NoFold = FoldSpec a -> Either [[Char]] (FoldSpec a)
forall a. a -> Either [[Char]] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec a
s
combineFoldSpec (FoldSpec (Fun t '[a] b
f) Specification b
s) (FoldSpec (Fun t '[a] b
g) Specification b
s') =
case t '[a] b -> t '[a] b -> Maybe (t :~: t, '[a] :~: '[a], b :~: b)
forall (t1 :: [*] -> * -> *) (d1 :: [*]) r1 (t2 :: [*] -> * -> *)
(d2 :: [*]) r2.
(Typeable t1, Typeable d1, Typeable r1, Typeable t2, Typeable d2,
Typeable r2, Eq (t1 d1 r1)) =>
t1 d1 r1 -> t2 d2 r2 -> Maybe (t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t '[a] b
f t '[a] b
g of
Just (t :~: t
_, '[a] :~: '[a]
_, b :~: b
Refl) -> FoldSpec a -> Either [[Char]] (FoldSpec a)
forall a. a -> Either [[Char]] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FoldSpec a -> Either [[Char]] (FoldSpec a))
-> FoldSpec a -> Either [[Char]] (FoldSpec a)
forall a b. (a -> b) -> a -> b
$ Fun '[a] b -> Specification b -> FoldSpec a
forall t a.
(HasSpec a, HasSpec t, Foldy t) =>
Fun '[a] t -> Specification t -> FoldSpec a
FoldSpec (t '[a] b -> Fun '[a] b
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun t '[a] b
f) (Specification b
s Specification b -> Specification b -> Specification b
forall a. Semigroup a => a -> a -> a
<> Specification b
Specification b
s')
Maybe (t :~: t, '[a] :~: '[a], b :~: b)
Nothing -> [[Char]] -> Either [[Char]] (FoldSpec a)
forall a b. a -> Either a b
Left [[Char]
"Can't combine fold specs on different functions", [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t '[a] b -> [Char]
forall a. Show a => a -> [Char]
show t '[a] b
f, [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t '[a] b -> [Char]
forall a. Show a => a -> [Char]
show t '[a] b
g]
conformsToFoldSpec :: forall a. [a] -> FoldSpec a -> Bool
conformsToFoldSpec :: forall a. [a] -> FoldSpec a -> Bool
conformsToFoldSpec [a]
_ FoldSpec a
NoFold = Bool
True
conformsToFoldSpec [a]
xs (FoldSpec (Fun t '[a] b
f) Specification b
s) = [b] -> b
forall a. Foldy a => [a] -> a
adds ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
f) [a]
xs) b -> Specification b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
s
class (HasSpec a, NumLike a, Logic IntW) => Foldy a where
genList ::
MonadGenError m => Specification a -> Specification a -> GenT m [a]
theAddFn :: IntW '[a, a] a
theAddFn = IntW '[a, a] a
forall b. NumLike b => IntW '[b, b] b
AddW
theZero :: a
theZero = a
0
genSizedList ::
MonadGenError m =>
Specification Integer ->
Specification a ->
Specification a ->
GenT m [a]
noNegativeValues :: Bool
type SizeSpec = NumSpec Integer
class Sized t where
sizeOf :: t -> Integer
default sizeOf :: (HasSimpleRep t, Sized (SimpleRep t)) => t -> Integer
sizeOf = SimpleRep t -> Integer
forall t. Sized t => t -> Integer
sizeOf (SimpleRep t -> Integer) -> (t -> SimpleRep t) -> t -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> SimpleRep t
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep
liftSizeSpec :: HasSpec t => SizeSpec -> [Integer] -> Specification t
default liftSizeSpec ::
( Sized (SimpleRep t)
, GenericRequires t
) =>
SizeSpec ->
[Integer] ->
Specification t
liftSizeSpec NumSpec Integer
sz [Integer]
cant = Specification (SimpleRep t) -> Specification t
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep t) -> Specification t)
-> Specification (SimpleRep t) -> Specification t
forall a b. (a -> b) -> a -> b
$ NumSpec Integer -> [Integer] -> Specification (SimpleRep t)
forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec NumSpec Integer
sz [Integer]
cant
liftMemberSpec :: HasSpec t => [Integer] -> Specification t
default liftMemberSpec ::
( Sized (SimpleRep t)
, GenericRequires t
) =>
[Integer] ->
Specification t
liftMemberSpec = Specification (SimpleRep t) -> Specification t
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep t) -> Specification t)
-> ([Integer] -> Specification (SimpleRep t))
-> [Integer]
-> Specification t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> Specification (SimpleRep t)
forall t. (Sized t, HasSpec t) => [Integer] -> Specification t
liftMemberSpec
sizeOfTypeSpec :: HasSpec t => TypeSpec t -> Specification Integer
default sizeOfTypeSpec ::
( HasSpec (SimpleRep t)
, Sized (SimpleRep t)
, TypeSpec t ~ TypeSpec (SimpleRep t)
) =>
TypeSpec t ->
Specification Integer
sizeOfTypeSpec = forall t.
(Sized t, HasSpec t) =>
TypeSpec t -> Specification Integer
sizeOfTypeSpec @(SimpleRep t)
adds :: Foldy a => [a] -> a
adds :: forall a. Foldy a => [a] -> a
adds = (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (IntW '[a, a] a -> FunTy '[a, a] a
forall (d :: [*]) r. IntW d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics IntW '[a, a] a
forall a. Foldy a => IntW '[a, a] a
theAddFn) a
forall a. Foldy a => a
theZero
data FunW (dom :: [Type]) (rng :: Type) where
IdW :: forall a. FunW '[a] a
ComposeW ::
forall b t1 t2 a r.
( AppRequires t1 '[b] r
, AppRequires t2 '[a] b
, HasSpec b
) =>
t1 '[b] r ->
t2 '[a] b ->
FunW '[a] r
FlipW ::
forall t a b r.
AppRequires t '[a, b] r =>
t '[a, b] r ->
FunW '[b, a] r
funSem :: FunW dom rng -> FunTy dom rng
funSem :: forall (dom :: [*]) rng. FunW dom rng -> FunTy dom rng
funSem FunW dom rng
IdW = FunTy dom rng
rng -> rng
forall a. a -> a
id
funSem (ComposeW t1 '[b] rng
f t2 '[a] b
g) = (\a
a -> t1 '[b] rng -> FunTy '[b] rng
forall (d :: [*]) r. t1 d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t1 '[b] rng
f (t2 '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t2 d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t2 '[a] b
g a
a))
funSem (FlipW (t '[a, b] rng
f :: g d r)) = (a -> b -> rng) -> b -> a -> rng
forall a b c. (a -> b -> c) -> b -> a -> c
flip (t '[a, b] rng -> FunTy '[a, b] rng
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a, b] rng
f)
instance Semantics FunW where
semantics :: forall (dom :: [*]) rng. FunW dom rng -> FunTy dom rng
semantics = FunW d r -> FunTy d r
forall (dom :: [*]) rng. FunW dom rng -> FunTy dom rng
funSem
instance Syntax FunW
instance Show (FunW dom rng) where
show :: FunW dom rng -> [Char]
show FunW dom rng
IdW = [Char]
"id_"
show (FlipW t '[a, b] rng
f) = [Char]
"(flip_ " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t '[a, b] rng -> [Char]
forall a. Show a => a -> [Char]
show t '[a, b] rng
f [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
show (ComposeW t1 '[b] rng
x t2 '[a] b
y) = [Char]
"(compose_ " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t1 '[b] rng -> [Char]
forall a. Show a => a -> [Char]
show t1 '[b] rng
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t2 '[a] b -> [Char]
forall a. Show a => a -> [Char]
show t2 '[a] b
y [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
instance Eq (FunW dom rng) where
FunW dom rng
IdW == :: FunW dom rng -> FunW dom rng -> Bool
== FunW dom rng
IdW = Bool
True
FlipW t '[a, b] rng
t1 == FlipW t '[a, b] rng
t2 = t '[a, b] rng -> t '[a, b] rng -> Bool
forall (t1 :: [*] -> * -> *) (bs1 :: [*]) r1 (t2 :: [*] -> * -> *)
(bs2 :: [*]) r2.
(AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) =>
t1 bs1 r1 -> t2 bs2 r2 -> Bool
compareWit t '[a, b] rng
t1 t '[a, b] rng
t2
ComposeW t1 '[b] rng
f t2 '[a] b
f' == ComposeW t1 '[b] rng
g t2 '[a] b
g' = t1 '[b] rng -> t1 '[b] rng -> Bool
forall (t1 :: [*] -> * -> *) (bs1 :: [*]) r1 (t2 :: [*] -> * -> *)
(bs2 :: [*]) r2.
(AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) =>
t1 bs1 r1 -> t2 bs2 r2 -> Bool
compareWit t1 '[b] rng
f t1 '[b] rng
g Bool -> Bool -> Bool
&& t2 '[a] b -> t2 '[a] b -> Bool
forall (t1 :: [*] -> * -> *) (bs1 :: [*]) r1 (t2 :: [*] -> * -> *)
(bs2 :: [*]) r2.
(AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) =>
t1 bs1 r1 -> t2 bs2 r2 -> Bool
compareWit t2 '[a] b
f' t2 '[a] b
g'
FunW dom rng
_ == FunW dom rng
_ = Bool
False
compareWit ::
forall t1 bs1 r1 t2 bs2 r2.
(AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) =>
t1 bs1 r1 ->
t2 bs2 r2 ->
Bool
compareWit :: forall (t1 :: [*] -> * -> *) (bs1 :: [*]) r1 (t2 :: [*] -> * -> *)
(bs2 :: [*]) r2.
(AppRequires t1 bs1 r1, AppRequires t2 bs2 r2) =>
t1 bs1 r1 -> t2 bs2 r2 -> Bool
compareWit t1 bs1 r1
x t2 bs2 r2
y = case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: [*] -> * -> *) (b :: [*] -> * -> *).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t1 @t2, forall (a :: [*]) (b :: [*]).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @bs1 @bs2, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @r1 @r2) of
(Just t1 :~: t2
Refl, Just bs1 :~: bs2
Refl, Just r1 :~: r2
Refl) -> t1 bs1 r1
x t1 bs1 r1 -> t1 bs1 r1 -> Bool
forall a. Eq a => a -> a -> Bool
== t1 bs1 r1
t2 bs2 r2
y
(Maybe (t1 :~: t2), Maybe (bs1 :~: bs2), Maybe (r1 :~: r2))
_ -> Bool
False
instance Logic FunW where
propagate :: forall (as :: [*]) b a.
(AppRequires FunW as b, HasSpec a) =>
FunW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate FunW as b
IdW (Unary HOLE a b
HOLE) = Specification b -> Specification b
Specification b -> SpecificationD Deps a
forall a. a -> a
id
propagate (FlipW t '[a, b] b
f) ListCtx Value as (HOLE a)
ctx = t '[a, b] b
-> ListCtx Value '[a, b] (HOLE a)
-> Specification b
-> SpecificationD Deps a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t '[a, b] b
f (ListCtx Value '[b, a] (HOLE a) -> ListCtx Value '[a, b] (HOLE a)
forall a b c.
(Typeable a, Show a, Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)
flipCtx ListCtx Value as (HOLE a)
ListCtx Value '[b, a] (HOLE a)
ctx)
propagate (ComposeW t1 '[b] b
f t2 '[a] b
g) (Unary HOLE a a
HOLE) = t2 '[a] b
-> ListCtx Value '[a] (HOLE a)
-> Specification b
-> Specification a
forall (as :: [*]) b a.
(AppRequires t2 as b, HasSpec a) =>
t2 as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t2 '[a] b
g (HOLE a a -> ListCtx Value '[a] (HOLE a)
forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
Unary HOLE a a
forall a. HOLE a a
HOLE) (Specification b -> Specification a)
-> (Specification b -> Specification b)
-> Specification b
-> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t1 '[b] b
-> ListCtx Value '[b] (HOLE b)
-> Specification b
-> Specification b
forall (as :: [*]) b a.
(AppRequires t1 as b, HasSpec a) =>
t1 as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t1 '[b] b
f (HOLE b b -> ListCtx Value '[b] (HOLE b)
forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
Unary HOLE b b
forall a. HOLE a a
HOLE)
mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
FunW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec FunW '[a] b
IdW TypeSpec a
ts = TypeSpec b -> Specification b
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
TypeSpec b
ts
mapTypeSpec (ComposeW t1 '[b] b
g t2 '[a] b
h) TypeSpec a
ts = t1 '[b] b -> Specification b -> Specification b
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t1 '[b] b
g (Specification b -> Specification b)
-> (Specification a -> Specification b)
-> Specification a
-> Specification b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t2 '[a] b -> Specification a -> Specification b
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t2 '[a] b
h (Specification a -> Specification b)
-> Specification a -> Specification b
forall a b. (a -> b) -> a -> b
$ TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
TypeSpec a
ts
rewriteRules :: forall (dom :: [*]) rng.
(TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) =>
FunW dom rng
-> List Term dom
-> Evidence (AppRequires FunW dom rng)
-> Maybe (Term rng)
rewriteRules (ComposeW t1 '[b] rng
f t2 '[a] b
g) (Term a
x :> List Term as1
Nil) Evidence (AppRequires FunW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ t1 '[b] rng -> List Term '[b] -> Term rng
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t1 '[b] rng
f (t2 '[a] b -> List Term '[a] -> TermD Deps b
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t2 '[a] b
g (Term a
x 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) TermD Deps b -> List Term '[] -> List Term '[b]
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)
rewriteRules FunW dom rng
IdW (Term a
x :> List Term as1
Nil) Evidence (AppRequires FunW dom rng)
Evidence = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
rewriteRules (FlipW t '[a, b] rng
f) (a :: Term a
a@Lit {} :> Term a
b :> List Term as1
Nil) Evidence (AppRequires FunW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ t '[a, b] rng -> List Term '[a, b] -> Term rng
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t '[a, b] rng
f (Term a
b Term a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
a 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)
rewriteRules (FlipW t '[a, b] rng
f) (Term a
a :> b :: Term a
b@Lit {} :> List Term as1
Nil) Evidence (AppRequires FunW dom rng)
Evidence = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ t '[a, b] rng -> List Term '[a, b] -> Term rng
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t '[a, b] rng
f (Term a
b Term a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
a 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)
rewriteRules (FlipW {}) List Term dom
_ Evidence (AppRequires FunW dom rng)
Evidence = Maybe (Term rng)
forall a. Maybe a
Nothing
id_ :: forall a. HasSpec a => Term a -> Term a
id_ :: forall a. HasSpec a => Term a -> Term a
id_ = FunW '[a] a -> FunTy (MapList Term '[a]) (TermD Deps a)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm FunW '[a] a
forall a. FunW '[a] a
IdW
flip_ ::
forall (t :: [Type] -> Type -> Type) a b r.
(HasSpec b, HasSpec a, AppRequires t '[a, b] r) =>
t '[a, b] r ->
Term b ->
Term a ->
Term r
flip_ :: forall (t :: [*] -> * -> *) a b r.
(HasSpec b, HasSpec a, AppRequires t '[a, b] r) =>
t '[a, b] r -> Term b -> Term a -> Term r
flip_ t '[a, b] r
x = FunW '[b, a] r -> FunTy (MapList Term '[b, a]) (TermD Deps r)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (t '[a, b] r -> FunW '[b, a] r
forall (t :: [*] -> * -> *) a b r.
AppRequires t '[a, b] r =>
t '[a, b] r -> FunW '[b, a] r
FlipW t '[a, b] r
x)
compose_ ::
forall b t1 t2 a r.
( AppRequires t1 '[b] r
, AppRequires t2 '[a] b
) =>
t1 '[b] r ->
t2 '[a] b ->
Term a ->
Term r
compose_ :: forall b (t1 :: [*] -> * -> *) (t2 :: [*] -> * -> *) a r.
(AppRequires t1 '[b] r, AppRequires t2 '[a] b) =>
t1 '[b] r -> t2 '[a] b -> Term a -> Term r
compose_ t1 '[b] r
f t2 '[a] b
g = FunW '[a] r -> FunTy (MapList Term '[a]) (TermD Deps r)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm (FunW '[a] r -> FunTy (MapList Term '[a]) (TermD Deps r))
-> FunW '[a] r -> FunTy (MapList Term '[a]) (TermD Deps r)
forall a b. (a -> b) -> a -> b
$ t1 '[b] r -> t2 '[a] b -> FunW '[a] r
forall t (a :: [*] -> * -> *) (b :: [*] -> * -> *) a r.
(AppRequires a '[t] r, AppRequires b '[a] t, HasSpec t) =>
a '[t] r -> b '[a] t -> FunW '[a] r
ComposeW t1 '[b] r
f t2 '[a] b
g
instance Foldy Integer where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> Specification Integer -> GenT m [Integer]
genList = Specification Integer -> Specification Integer -> GenT m [Integer]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Integer
-> Specification Integer
-> GenT m [Integer]
genSizedList = Specification Integer
-> Specification Integer
-> Specification Integer
-> GenT m [Integer]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Int where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Int -> Specification Int -> GenT m [Int]
genList = Specification Int -> Specification Int -> GenT m [Int]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int -> Specification Int -> GenT m [Int]
genSizedList = Specification Integer
-> Specification Int -> Specification Int -> GenT m [Int]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Int8 where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Int8 -> Specification Int8 -> GenT m [Int8]
genList = Specification Int8 -> Specification Int8 -> GenT m [Int8]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int8 -> Specification Int8 -> GenT m [Int8]
genSizedList = Specification Integer
-> Specification Int8 -> Specification Int8 -> GenT m [Int8]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Int16 where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Int16 -> Specification Int16 -> GenT m [Int16]
genList = Specification Int16 -> Specification Int16 -> GenT m [Int16]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int16 -> Specification Int16 -> GenT m [Int16]
genSizedList = Specification Integer
-> Specification Int16 -> Specification Int16 -> GenT m [Int16]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Int32 where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Int32 -> Specification Int32 -> GenT m [Int32]
genList = Specification Int32 -> Specification Int32 -> GenT m [Int32]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int32 -> Specification Int32 -> GenT m [Int32]
genSizedList = Specification Integer
-> Specification Int32 -> Specification Int32 -> GenT m [Int32]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Int64 where
noNegativeValues :: Bool
noNegativeValues = Bool
False
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Int64 -> Specification Int64 -> GenT m [Int64]
genList = Specification Int64 -> Specification Int64 -> GenT m [Int64]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int64 -> Specification Int64 -> GenT m [Int64]
genSizedList = Specification Integer
-> Specification Int64 -> Specification Int64 -> GenT m [Int64]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Natural where
noNegativeValues :: Bool
noNegativeValues = Bool
True
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Natural -> Specification Natural -> GenT m [Natural]
genList = Specification Natural -> Specification Natural -> GenT m [Natural]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Natural
-> Specification Natural
-> GenT m [Natural]
genSizedList = Specification Integer
-> Specification Natural
-> Specification Natural
-> GenT m [Natural]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Word8 where
noNegativeValues :: Bool
noNegativeValues = Bool
True
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Word8 -> Specification Word8 -> GenT m [Word8]
genList = Specification Word8 -> Specification Word8 -> GenT m [Word8]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word8 -> Specification Word8 -> GenT m [Word8]
genSizedList = Specification Integer
-> Specification Word8 -> Specification Word8 -> GenT m [Word8]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Word16 where
noNegativeValues :: Bool
noNegativeValues = Bool
True
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Word16 -> Specification Word16 -> GenT m [Word16]
genList = Specification Word16 -> Specification Word16 -> GenT m [Word16]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word16 -> Specification Word16 -> GenT m [Word16]
genSizedList = Specification Integer
-> Specification Word16 -> Specification Word16 -> GenT m [Word16]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Word32 where
noNegativeValues :: Bool
noNegativeValues = Bool
True
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Word32 -> Specification Word32 -> GenT m [Word32]
genList = Specification Word32 -> Specification Word32 -> GenT m [Word32]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word32 -> Specification Word32 -> GenT m [Word32]
genSizedList = Specification Integer
-> Specification Word32 -> Specification Word32 -> GenT m [Word32]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
instance Foldy Word64 where
noNegativeValues :: Bool
noNegativeValues = Bool
True
genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Word64 -> Specification Word64 -> GenT m [Word64]
genList = Specification Word64 -> Specification Word64 -> GenT m [Word64]
forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
TypeSpec a ~ NumSpec a, Random a, Complete a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word64 -> Specification Word64 -> GenT m [Word64]
genSizedList = Specification Integer
-> Specification Word64 -> Specification Word64 -> GenT m [Word64]
forall a (m :: * -> *).
(Complete a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
Integral a, Arbitrary a, MaybeBounded a, Complete Integer) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize
genInverse ::
( MonadGenError m
, HasSpec a
, HasSpec b
) =>
Fun '[a] b ->
Specification a ->
b ->
GenT m a
genInverse :: forall (m :: * -> *) a b.
(MonadGenError m, HasSpec a, HasSpec b) =>
Fun '[a] b -> Specification a -> b -> GenT m a
genInverse (Fun t '[a] b
f) Specification a
argS b
x =
let argSpec' :: Specification a
argSpec' = Specification a
argS Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> t '[a] b
-> ListCtx Value '[a] (HOLE a)
-> Specification b
-> Specification a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t '[a] b
f (HOLE a a
forall a. HOLE a a
HOLE HOLE a a -> List Value '[] -> ListCtx Value '[a] (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) (b -> Specification b
forall a. a -> Specification a
equalSpec b
x)
in NonEmpty [Char] -> GenT m a -> GenT m a
forall a. HasCallStack => NonEmpty [Char] -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explainNE
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"genInverse"
, [Char]
" f = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t '[a] b -> [Char]
forall a. Show a => a -> [Char]
show t '[a] b
f
, Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc Any
" argS =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
argS
, [Char]
" x = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> [Char]
forall a. Show a => a -> [Char]
show b
x
, Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc Any
" argSpec' =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
argSpec'
]
)
(GenT m a -> GenT m a) -> GenT m a -> GenT m a
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT m a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
argSpec'
genFromFold ::
forall m a b.
( MonadGenError m
, Foldy b
, HasSpec a
) =>
[a] ->
Specification Integer ->
Specification a ->
Fun '[a] b ->
Specification b ->
GenT m [a]
genFromFold :: forall (m :: * -> *) a b.
(MonadGenError m, Foldy b, HasSpec a) =>
[a]
-> Specification Integer
-> Specification a
-> Fun '[a] b
-> Specification b
-> GenT m [a]
genFromFold [a]
must (Specification Integer -> Specification Integer
forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification Integer
size) Specification a
elemS fun :: Fun '[a] b
fun@(Fun t '[a] b
fn) Specification b
foldS
| Specification Integer -> Bool
forall a. Specification a -> Bool
isErrorLike Specification Integer
size =
NonEmpty [Char] -> GenT m [a]
forall a. HasCallStack => NonEmpty [Char] -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalErrorNE ([Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons [Char]
"genFromFold has ErrorLike sizeSpec" (Specification Integer -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification Integer
size))
| Specification a -> Bool
forall a. Specification a -> Bool
isErrorLike Specification a
elemS =
NonEmpty [Char] -> GenT m [a]
forall a. HasCallStack => NonEmpty [Char] -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalErrorNE ([Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons [Char]
"genFromFold has ErrorLike elemSpec" (Specification a -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification a
elemS))
| Specification b -> Bool
forall a. Specification a -> Bool
isErrorLike Specification b
foldS =
NonEmpty [Char] -> GenT m [a]
forall a. HasCallStack => NonEmpty [Char] -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalErrorNE ([Char] -> NonEmpty [Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a -> NonEmpty a
NE.cons [Char]
"genFromFold has ErrorLike totalSpec" (Specification b -> NonEmpty [Char]
forall a. Specification a -> NonEmpty [Char]
errorLikeMessage Specification b
foldS))
| Bool
otherwise = ( NonEmpty [Char] -> GenT m [a] -> GenT m [a]
forall a. HasCallStack => NonEmpty [Char] -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explainNE
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"while calling genFromFold"
, [Char]
" must = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> [Char]
forall a. Show a => a -> [Char]
show [a]
must
, [Char]
" size = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification Integer -> [Char]
forall a. Show a => a -> [Char]
show Specification Integer
size
, [Char]
" elemS = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification a -> [Char]
forall a. Show a => a -> [Char]
show Specification a
elemS
, [Char]
" fun = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Fun '[a] b -> [Char]
forall a. Show a => a -> [Char]
show Fun '[a] b
fun
, [Char]
" foldS = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification b -> [Char]
forall a. Show a => a -> [Char]
show Specification b
foldS
]
)
)
(GenT m [a] -> GenT m [a]) -> GenT m [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ do
let elemS' :: Specification b
elemS' :: Specification b
elemS' = t '[a] b -> Specification a -> Specification b
forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t '[a] b
fn Specification a
elemS
mustVal :: b
mustVal = [b] -> b
forall a. Foldy a => [a] -> a
adds ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
fn) [a]
must)
foldS' :: Specification b
foldS' :: Specification b
foldS' = IntW '[b, b] b
-> ListCtx Value '[b, b] (HOLE b)
-> Specification b
-> Specification b
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate IntW '[b, b] b
forall a. Foldy a => IntW '[a, a] a
theAddFn (HOLE b b
forall a. HOLE a a
HOLE HOLE b b -> List Value '[b] -> ListCtx Value '[b, b] (HOLE b)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? b -> Value b
forall a. Show a => a -> Value a
Value b
mustVal Value b -> List Value '[] -> List Value '[b]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification b
foldS
sizeSpec' :: Specification Integer
sizeSpec' :: Specification Integer
sizeSpec' = IntW '[Integer, Integer] Integer
-> ListCtx Value '[Integer, Integer] (HOLE Integer)
-> Specification Integer
-> Specification Integer
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate IntW '[Integer, Integer] Integer
forall b. NumLike b => IntW '[b, b] b
AddW (HOLE Integer Integer
forall a. HOLE a a
HOLE HOLE Integer Integer
-> List Value '[Integer]
-> ListCtx Value '[Integer, Integer] (HOLE Integer)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? Integer -> Value Integer
forall a. Show a => a -> Value a
Value ([a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
must) Value Integer -> List Value '[] -> List Value '[Integer]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) Specification Integer
size
Bool -> GenT m () -> GenT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Specification Integer -> Bool
forall a. Specification a -> Bool
isErrorLike Specification Integer
sizeSpec') (GenT m () -> GenT m ()) -> GenT m () -> GenT m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> GenT m ()
forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
genError [Char]
"Inconsistent size spec"
[b]
results0 <- case Specification Integer
sizeSpec' of
Specification Integer
TrueSpec -> Specification b -> Specification b -> GenT m [b]
forall a (m :: * -> *).
(Foldy a, MonadGenError m) =>
Specification a -> Specification a -> GenT m [a]
forall (m :: * -> *).
MonadGenError m =>
Specification b -> Specification b -> GenT m [b]
genList (Specification b -> Specification b
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
elemS') (Specification b -> Specification b
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
foldS')
Specification Integer
_ -> Specification Integer
-> Specification b -> Specification b -> GenT m [b]
forall a (m :: * -> *).
(Foldy a, MonadGenError m) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification b -> Specification b -> GenT m [b]
genSizedList Specification Integer
sizeSpec' (Specification b -> Specification b
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
elemS') (Specification b -> Specification b
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
foldS')
[a]
results <-
NonEmpty [Char] -> GenT m [a] -> GenT m [a]
forall a. HasCallStack => NonEmpty [Char] -> GenT m a -> GenT m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explainNE
( [[Char]] -> NonEmpty [Char]
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
[ [Char]
"genInverse"
, [Char]
" fun = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Fun '[a] b -> [Char]
forall a. Show a => a -> [Char]
show Fun '[a] b
fun
, [Char]
" results0 = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> [Char]
forall a. Show a => a -> [Char]
show [b]
results0
, Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc Any
" elemS' =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification b -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification b -> Doc ann
pretty Specification b
elemS'
]
)
(GenT m [a] -> GenT m [a]) -> GenT m [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ (b -> GenT m a) -> [b] -> GenT m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Fun '[a] b -> Specification a -> b -> GenT m a
forall (m :: * -> *) a b.
(MonadGenError m, HasSpec a, HasSpec b) =>
Fun '[a] b -> Specification a -> b -> GenT m a
genInverse Fun '[a] b
fun Specification a
elemS) [b]
results0
Gen [a] -> GenT m [a]
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen [a] -> GenT m [a]) -> Gen [a] -> GenT m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> Gen [a]
forall a. [a] -> Gen [a]
shuffle ([a] -> Gen [a]) -> [a] -> Gen [a]
forall a b. (a -> b) -> a -> b
$ [a]
must [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
results
addFun :: NumLike n => Fun '[n, n] n
addFun :: forall n. NumLike n => Fun '[n, n] n
addFun = IntW '[n, n] n -> Fun '[n, n] n
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun IntW '[n, n] n
forall b. NumLike b => IntW '[b, b] b
AddW
instance Sized [a] where
sizeOf :: [a] -> Integer
sizeOf = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
liftSizeSpec :: HasSpec [a] => NumSpec Integer -> [Integer] -> Specification [a]
liftSizeSpec NumSpec Integer
spec [Integer]
cant = TypeSpec [a] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [a]
forall a. Monoid a => a
mempty (TypeSpec Integer -> [Integer] -> Specification Integer
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec Integer
NumSpec Integer
spec [Integer]
cant) Specification a
forall deps a. SpecificationD deps a
TrueSpec FoldSpec a
forall a. FoldSpec a
NoFold)
liftMemberSpec :: HasSpec [a] => [Integer] -> Specification [a]
liftMemberSpec [Integer]
xs = case [Integer] -> Maybe (NonEmpty Integer)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [Integer]
xs of
Maybe (NonEmpty Integer)
Nothing -> NonEmpty [Char] -> Specification [a]
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec ([Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"In liftMemberSpec for (Sized List) instance, xs is the empty list"))
Just NonEmpty Integer
zs -> TypeSpec [a] -> Specification [a]
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
forall a. Maybe a
Nothing [a]
forall a. Monoid a => a
mempty (NonEmpty Integer -> Specification Integer
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec NonEmpty Integer
zs) Specification a
forall deps a. SpecificationD deps a
TrueSpec FoldSpec a
forall a. FoldSpec a
NoFold)
sizeOfTypeSpec :: HasSpec [a] => TypeSpec [a] -> Specification Integer
sizeOfTypeSpec (ListSpec Maybe Integer
_ [a]
_ Specification Integer
_ ErrorSpec {} FoldSpec a
_) = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
0
sizeOfTypeSpec (ListSpec Maybe Integer
_ [a]
must Specification Integer
sizespec Specification a
_ FoldSpec a
_) = Specification Integer
sizespec Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
geqSpec ([a] -> Integer
forall t. Sized t => t -> Integer
sizeOf [a]
must)
data SizeW (dom :: [Type]) rng :: Type where
SizeOfW :: (Sized n, HasSpec n) => SizeW '[n] Integer
deriving instance Eq (SizeW ds r)
instance Show (SizeW d r) where
show :: SizeW d r -> [Char]
show SizeW d r
SizeOfW = [Char]
"sizeOf_"
instance Semantics SizeW where
semantics :: forall (d :: [*]) r. SizeW d r -> FunTy d r
semantics SizeW d r
SizeOfW = FunTy d r
n -> Integer
forall t. Sized t => t -> Integer
sizeOf
instance Syntax SizeW
instance Logic SizeW where
propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires SizeW as b, HasSpec a) =>
SizeW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec SizeW as b
SizeOfW (Unary HOLE a n
HOLE) TypeSpec b
ts [b]
cant = NumSpec Integer -> [Integer] -> Specification a
forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec TypeSpec b
NumSpec Integer
ts [b]
[Integer]
cant
propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires SizeW as b, HasSpec a) =>
SizeW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec SizeW as b
SizeOfW (Unary HOLE a n
HOLE) NonEmpty b
es = [Integer] -> Specification a
forall t. (Sized t, HasSpec t) => [Integer] -> Specification t
liftMemberSpec (NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
mapTypeSpec :: forall a b.
(HasSpec a, HasSpec b) =>
SizeW '[a] b -> TypeSpec a -> Specification b
mapTypeSpec (SizeW '[a] b
SizeOfW :: SizeW '[a] b) TypeSpec a
ts =
(Term b -> Pred) -> Specification b
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term b -> Pred) -> Specification b)
-> (Term b -> Pred) -> Specification b
forall a b. (a -> b) -> a -> b
$ \Term b
x ->
(Term a -> Pred) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
x' -> Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term b
x Term b -> Term b -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term a
x') Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds @a Term a
x' TypeSpec a
ts
sizeOfFn :: forall a. (HasSpec a, Sized a) => Fun '[a] Integer
sizeOfFn :: forall a. (HasSpec a, Sized a) => Fun '[a] Integer
sizeOfFn = SizeW '[a] Integer -> Fun '[a] Integer
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun SizeW '[a] Integer
forall t. (Sized t, HasSpec t) => SizeW '[t] Integer
SizeOfW
rangeSize :: Integer -> Integer -> SizeSpec
rangeSize :: Integer -> Integer -> NumSpec Integer
rangeSize Integer
a Integer
b | Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = [Char] -> NumSpec Integer
forall a. HasCallStack => [Char] -> a
error ([Char]
"Negative Int in call to rangeSize: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
b)
rangeSize Integer
a Integer
b = Maybe Integer -> Maybe Integer -> NumSpec Integer
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
a) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
b)
between :: (HasSpec a, TypeSpec a ~ NumSpec a) => a -> a -> Specification a
between :: forall a.
(HasSpec a, TypeSpec a ~ NumSpec a) =>
a -> a -> Specification a
between a
lo a
hi = TypeSpec a -> [a] -> Specification a
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
lo) (a -> Maybe a
forall a. a -> Maybe a
Just a
hi)) []
maxSpec :: Specification Integer -> Specification Integer
maxSpec :: Specification Integer -> Specification Integer
maxSpec (ExplainSpec [[Char]]
es Specification Integer
s) = [[Char]] -> Specification Integer -> Specification Integer
forall a. [[Char]] -> Specification a -> Specification a
explainSpecOpt [[Char]]
es (Specification Integer -> Specification Integer
maxSpec Specification Integer
s)
maxSpec Specification Integer
TrueSpec = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
maxSpec s :: Specification Integer
s@(SuspendedSpec Var Integer
_ Pred
_) =
(Term Integer -> Pred) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Pred) -> Specification Integer)
-> (Term Integer -> Pred) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
x -> (Term Integer -> [Pred]) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists ((Term Integer -> [Pred]) -> Pred)
-> (Term Integer -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Integer
y -> [Term Integer
y Term Integer -> Specification Integer -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
s, NonEmpty [Char] -> Pred -> Pred
forall deps. NonEmpty [Char] -> PredD deps -> PredD deps
Explain ([Char] -> NonEmpty [Char]
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"maxSpec on SuspendedSpec") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Integer
x Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
y)]
maxSpec (ErrorSpec NonEmpty [Char]
xs) = NonEmpty [Char] -> Specification Integer
forall deps a. NonEmpty [Char] -> SpecificationD deps a
ErrorSpec NonEmpty [Char]
xs
maxSpec (MemberSpec NonEmpty Integer
xs) = Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
leqSpec (NonEmpty Integer -> Integer
forall a. Ord a => NonEmpty a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty Integer
xs)
maxSpec (TypeSpec (NumSpecInterval Maybe Integer
_ Maybe Integer
hi) [Integer]
bad) = TypeSpec Integer -> [Integer] -> Specification Integer
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (Maybe Integer -> Maybe Integer -> NumSpec Integer
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
hi) [Integer]
bad
hasSize :: (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize :: forall t.
(HasSpec t, Sized t) =>
NumSpec Integer -> Specification t
hasSize NumSpec Integer
sz = NumSpec Integer -> [Integer] -> Specification t
forall t.
(Sized t, HasSpec t) =>
NumSpec Integer -> [Integer] -> Specification t
liftSizeSpec NumSpec Integer
sz []