{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
-- Natural
{-# OPTIONS_GHC -Wno-unused-imports #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

-- | Code for the Foldy class, the FunW witness (compose_,id_,flip_) and
--   HasSpec instance for List. These things are all mutually recursive.
module Constrained.Spec.ListFoldy where

import Constrained.Base
import Constrained.Conformance (conformsToSpec, satisfies)
import Constrained.Core (Evidence (..), NonEmpty ((:|)), Var (..), eqVar, unionWithMaybe)
import Constrained.GenT
import Constrained.List
import Constrained.NumSpec
import Constrained.Spec.Num ()
import Constrained.Spec.Size (Sized (..), genFromSizeSpec, sizeOf_)
import Constrained.SumList (Cost (..), Solution (No, Yes), pickAll)
import Constrained.Syntax (forAll, genHint, unsafeExists)
import Constrained.TheKnot (
  caseBoolSpec,
  genFromSpecT,
  mapSpec,
  shrinkWithSpec,
  simplifySpec,
  (==.),
 )
import Control.Applicative ((<|>))
import Control.Monad (guard, when)
import Data.Int
import Data.Kind
import Data.List (isPrefixOf, isSuffixOf, nub, (\\))
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import qualified Data.Set as Set
import Data.Typeable
import Data.Word
import GHC.Natural (Natural)
import GHC.Stack
import GHC.TypeLits
import Prettyprinter hiding (cat)
import System.Random (Random)
import Test.QuickCheck (Arbitrary (..), oneof, shrinkList, shuffle)

-- =============================================================
-- All Foldy class instances are over Numbers (so far).
-- So that's why the Foldy class is in the NumberSpec module.
-- Foldy class requires higher order functions, so here they are.
-- Note this is a new witness type, different from BaseW
-- but serving the same purpose. Note it can take Witnesses from
-- other classes as inputs. See FlipW amd ComposeW
-- ==============================================================

-- We need Arbitrary Specification to do this
instance {-# OVERLAPPABLE #-} (Arbitrary (Specification a {- Arbitrary (TypeSpec a), -}), Foldy a) => Arbitrary (FoldSpec a) where
  arbitrary :: Gen (FoldSpec a)
arbitrary = forall a. HasCallStack => [Gen a] -> Gen a
oneof [forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a. FunW "id_" '[a] a
IdW) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. FoldSpec a
NoFold]
  shrink :: FoldSpec a -> [FoldSpec a]
shrink FoldSpec a
NoFold = []
  shrink (FoldSpec (Fun t s '[a] b
wit) Specification b
spec)
    | Just (FunW "id_" '[a] a
idW, "id_" :~: s
Refl, FunW :~: t
Refl, '[a] :~: '[a]
Refl, a :~: b
Refl) <- forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (d1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (d2 :: [*]) r2.
(Logic s1 t1 d1 r1, Logic s2 t2 d2 r2) =>
t1 s1 d1 r1
-> t2 s2 d2 r2
-> Maybe (t1 s1 d1 r1, s1 :~: s2, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym (forall a. FunW "id_" '[a] a
IdW @a) t s '[a] b
wit = forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun FunW "id_" '[a] a
idW) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink Specification b
spec
  shrink FoldSpec {} = [forall a. FoldSpec a
NoFold]

data FunW (sym :: Symbol) (dom :: [Type]) (rng :: Type) where
  IdW :: forall a. FunW "id_" '[a] a
  ComposeW ::
    forall b s1 s2 t1 t2 a r.
    ( Logic s1 t1 '[b] r
    , Logic s2 t2 '[a] b
    , HasSpec b
    ) =>
    t1 s1 '[b] r -> t2 s2 '[a] b -> FunW "composeFn" '[a] r
  FlipW ::
    forall sym t a b r.
    Logic sym t '[a, b] r =>
    t sym '[a, b] r -> FunW "flip_" '[b, a] r

funSem :: FunW sym dom rng -> FunTy dom rng
funSem :: forall (sym :: Symbol) (dom :: [*]) rng.
FunW sym dom rng -> FunTy dom rng
funSem FunW sym dom rng
IdW = forall a. a -> a
id
funSem (ComposeW t1 s1 '[b] rng
f t2 s2 '[a] b
g) = (\a
a -> forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t1 s1 '[b] rng
f (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t2 s2 '[a] b
g a
a))
funSem (FlipW (t sym '[a, b] rng
f :: g s d r)) = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t sym '[a, b] rng
f)

instance Semantics FunW where
  semantics :: forall (sym :: Symbol) (dom :: [*]) rng.
FunW sym dom rng -> FunTy dom rng
semantics = forall (sym :: Symbol) (dom :: [*]) rng.
FunW sym dom rng -> FunTy dom rng
funSem

instance Syntax FunW

instance KnownSymbol s => Show (FunW s dom rng) where
  show :: FunW s dom rng -> String
show FunW s dom rng
IdW = String
"id_"
  show (FlipW t sym '[a, b] rng
f) = String
"(flip_ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t sym '[a, b] rng
f forall a. [a] -> [a] -> [a]
++ String
")"
  show (ComposeW t1 s1 '[b] rng
x t2 s2 '[a] b
y) = String
"(compose_ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t1 s1 '[b] rng
x forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t2 s2 '[a] b
y forall a. [a] -> [a] -> [a]
++ String
")"

instance Eq (FunW s dom rng) where
  FunW s dom rng
IdW == :: FunW s dom rng -> FunW s dom rng -> Bool
== FunW s dom rng
IdW = Bool
True
  FlipW t sym '[a, b] rng
t1 == FlipW t sym '[a, b] rng
t2 = forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (bs1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (bs2 :: [*]) r2.
(Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) =>
t1 s1 bs1 r1 -> t2 s2 bs2 r2 -> Bool
compareWit t sym '[a, b] rng
t1 t sym '[a, b] rng
t2
  ComposeW t1 s1 '[b] rng
f t2 s2 '[a] b
f' == ComposeW t1 s1 '[b] rng
g t2 s2 '[a] b
g' = forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (bs1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (bs2 :: [*]) r2.
(Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) =>
t1 s1 bs1 r1 -> t2 s2 bs2 r2 -> Bool
compareWit t1 s1 '[b] rng
f t1 s1 '[b] rng
g Bool -> Bool -> Bool
&& forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (bs1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (bs2 :: [*]) r2.
(Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) =>
t1 s1 bs1 r1 -> t2 s2 bs2 r2 -> Bool
compareWit t2 s2 '[a] b
f' t2 s2 '[a] b
g'

compareWit ::
  forall s1 t1 bs1 r1 s2 t2 bs2 r2.
  (Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) =>
  t1 s1 bs1 r1 -> t2 s2 bs2 r2 -> Bool
compareWit :: forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (bs1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (bs2 :: [*]) r2.
(Logic s1 t1 bs1 r1, Logic s2 t2 bs2 r2) =>
t1 s1 bs1 r1 -> t2 s2 bs2 r2 -> Bool
compareWit t1 s1 bs1 r1
x t2 s2 bs2 r2
y = case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @t1 @t2, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @s1 @s2, 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)
eqT @r1 @r2) of
  (Just t1 :~: t2
Refl, Just s1 :~: s2
Refl, Just bs1 :~: bs2
Refl, Just r1 :~: r2
Refl) -> t1 s1 bs1 r1
x forall a. Eq a => a -> a -> Bool
== t2 s2 bs2 r2
y
  (Maybe (t1 :~: t2), Maybe (s1 :~: s2), Maybe (bs1 :~: bs2),
 Maybe (r1 :~: r2))
_ -> Bool
False

-- ===================================
-- Logic instances for IdW, FlipW and ComposeW
-- Also their Haskell implementations id_ flip_ composeFn

instance HasSpec a => Logic "id_" FunW '[a] a where
  propagate :: forall hole.
Context "id_" FunW '[a] a hole
-> Specification a -> Specification hole
propagate Context "id_" FunW '[a] a hole
ctxt (ExplainSpec [] Specification a
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "id_" FunW '[a] a hole
ctxt Specification a
s
  propagate Context "id_" FunW '[a] a hole
ctxt (ExplainSpec [String]
es Specification a
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "id_" FunW '[a] a hole
ctxt Specification a
s
  propagate Context "id_" FunW '[a] a hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context FunW "id_" '[a] a
IdW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) Specification a
spec = Specification a
spec
  propagate Context "id_" FunW '[a] a hole
ctxt Specification a
_ = forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"IdW (id_)", String
"Unreachable context, too many args", forall a. Show a => a -> String
show Context "id_" FunW '[a] a hole
ctxt])

  mapTypeSpec :: forall a b.
('[a] ~ '[a], a ~ b, HasSpec a, HasSpec b) =>
FunW "id_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec FunW "id_" '[a] b
IdW TypeSpec a
ts = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts
  rewriteRules :: (TypeList '[a], Typeable '[a], HasSpec a, All HasSpec '[a]) =>
FunW "id_" '[a] a
-> List Term '[a]
-> Evidence (AppRequires "id_" FunW '[a] a)
-> Maybe (Term a)
rewriteRules FunW "id_" '[a] a
IdW (Term a
x :> List Term as1
Nil) Evidence (AppRequires "id_" FunW '[a] a)
Evidence = forall a. a -> Maybe a
Just Term a
x

id_ :: forall a. HasSpec a => Term a -> Term a
id_ :: forall a. HasSpec a => Term a -> Term a
id_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. FunW "id_" '[a] a
IdW

instance
  (forall sym t. Logic sym t '[a, b] r, All Typeable [a, b, r]) =>
  Logic "flip_" FunW '[b, a] r
  where
  propagate :: forall hole.
Context "flip_" FunW '[b, a] r hole
-> Specification r -> Specification hole
propagate Context "flip_" FunW '[b, a] r hole
ctxt (ExplainSpec [] Specification r
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "flip_" FunW '[b, a] r hole
ctxt Specification r
s
  propagate Context "flip_" FunW '[b, a] r hole
ctxt (ExplainSpec [String]
es Specification r
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "flip_" FunW '[b, a] r hole
ctxt Specification r
s
  propagate Context "flip_" FunW '[b, a] r hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context (FlipW t sym '[a, b] r
f) (Ctx hole y
HOLE :<> a
v :<| CList 'Post as1 Any Any
End)) Specification r
spec = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t sym '[a, b] r
f (a
v forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Pre as1 hole y -> CList 'Pre (a : as1) hole y
:|> forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) Specification r
spec
  propagate (Context (FlipW t sym '[a, b] r
f) (a
v :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) Specification r
spec = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t sym '[a, b] r
f (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> a
v forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Post as1 hole y -> CList 'Post (a : as1) hole y
:<| forall hole y. CList 'Post '[] hole y
End)) Specification r
spec
  propagate ctxt :: Context "flip_" FunW '[b, a] r hole
ctxt@(Context FunW "flip_" '[b, a] r
_ CList 'Pre '[b, a] hole y
_) Specification r
_ = forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"FlipW (flip_)", String
"Unreachable context, too many args", forall a. Show a => a -> String
show Context "flip_" FunW '[b, a] r hole
ctxt])

  -- Note we need Evidence to apply App to f
  rewriteRules :: (TypeList '[b, a], Typeable '[b, a], HasSpec r,
 All HasSpec '[b, a]) =>
FunW "flip_" '[b, a] r
-> List Term '[b, a]
-> Evidence (AppRequires "flip_" FunW '[b, a] r)
-> Maybe (Term r)
rewriteRules (FlipW t sym '[a, b] r
f) (a :: Term a
a@Lit {} :> Term a
b :> List Term as1
Nil) Evidence (AppRequires "flip_" FunW '[b, a] r)
Evidence = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App t sym '[a, b] r
f (Term a
b forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)
  rewriteRules (FlipW t sym '[a, b] r
f) (Term a
a :> b :: Term a
b@Lit {} :> List Term as1
Nil) Evidence (AppRequires "flip_" FunW '[b, a] r)
Evidence = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App t sym '[a, b] r
f (Term a
b forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)
  rewriteRules (FlipW {}) List Term '[b, a]
_ Evidence (AppRequires "flip_" FunW '[b, a] r)
Evidence = forall a. Maybe a
Nothing

flip_ ::
  forall (t :: FSType) (sym :: Symbol) a b r.
  (HasSpec b, HasSpec a, HasSpec r, forall sym1 t1. Logic sym1 t1 '[a, b] r) =>
  t sym '[a, b] r -> Term b -> Term a -> Term r
flip_ :: forall (t :: Symbol -> [*] -> * -> *) (sym :: Symbol) a b r.
(HasSpec b, HasSpec a, HasSpec r,
 forall (sym1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *).
 Logic sym1 t1 '[a, b] r) =>
t sym '[a, b] r -> Term b -> Term a -> Term r
flip_ t sym '[a, b] r
x = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm (forall (a :: Symbol) (s1 :: Symbol -> [*] -> * -> *) s2 t1 r.
Logic a s1 '[s2, t1] r =>
s1 a '[s2, t1] r -> FunW "flip_" '[t1, s2] r
FlipW t sym '[a, b] r
x)

instance
  ( All Typeable [a, r]
  , HasSpec r
  ) =>
  Logic "composeFn" FunW '[a] r
  where
  propagate :: forall hole.
Context "composeFn" FunW '[a] r hole
-> Specification r -> Specification hole
propagate Context "composeFn" FunW '[a] r hole
ctxt (ExplainSpec [] Specification r
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "composeFn" FunW '[a] r hole
ctxt Specification r
s
  propagate Context "composeFn" FunW '[a] r hole
ctxt (ExplainSpec [String]
es Specification r
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "composeFn" FunW '[a] r hole
ctxt Specification r
s
  propagate Context "composeFn" FunW '[a] r hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context (ComposeW (t1 s1 '[b] r
f :: t1' s1' '[b'] r') (t2 s2 '[a] b
g :: t2' s2' '[a'] b'')) (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) Specification r
spec =
    forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate @s2' @t2' @'[a'] @b' (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t2 s2 '[a] b
g (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) forall a b. (a -> b) -> a -> b
$
      forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate @s1' @t1' @'[b'] @r' (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t1 s1 '[b] r
f (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) Specification r
spec
  propagate ctxt :: Context "composeFn" FunW '[a] r hole
ctxt@(Context FunW "composeFn" '[a] r
_ CList 'Pre '[a] hole y
_) Specification r
_ = forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"ComposeW (composeFn)", String
"Unreachable context, too many args", forall a. Show a => a -> String
show Context "composeFn" FunW '[a] r hole
ctxt])

  mapTypeSpec :: forall a b.
('[a] ~ '[a], r ~ b, HasSpec a, HasSpec b) =>
FunW "composeFn" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec (ComposeW t1 s1 '[b] b
g t2 s2 '[a] b
h) TypeSpec a
ts = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) a b.
(Logic s t '[a] b, HasSpec a, HasSpec b) =>
t s '[a] b -> Specification a -> Specification b
mapSpec t1 s1 '[b] b
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) a b.
(Logic s t '[a] b, HasSpec a, HasSpec b) =>
t s '[a] b -> Specification a -> Specification b
mapSpec t2 s2 '[a] b
h forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts

  -- Note we need the Evidence to apply App to f, and to apply App to g
  rewriteRules :: (TypeList '[a], Typeable '[a], HasSpec r, All HasSpec '[a]) =>
FunW "composeFn" '[a] r
-> List Term '[a]
-> Evidence (AppRequires "composeFn" FunW '[a] r)
-> Maybe (Term r)
rewriteRules (ComposeW t1 s1 '[b] r
f t2 s2 '[a] b
g) (Term a
x :> List Term as1
Nil) Evidence (AppRequires "composeFn" FunW '[a] r)
Evidence = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App t1 s1 '[b] r
f (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App t2 s2 '[a] b
g (Term a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)

compose_ ::
  forall b s1 s2 t1 t2 a r.
  ( AppRequires s1 t1 '[b] r
  , AppRequires s2 t2 '[a] b
  ) =>
  t1 s1 '[b] r -> t2 s2 '[a] b -> Term a -> Term r
compose_ :: forall b (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       r.
(AppRequires s1 t1 '[b] r, AppRequires s2 t2 '[a] b) =>
t1 s1 '[b] r -> t2 s2 '[a] b -> Term a -> Term r
compose_ t1 s1 '[b] r
f t2 s2 '[a] b
g = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a b. (a -> b) -> a -> b
$ forall a (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       r.
(Logic s1 t1 '[a] r, Logic s2 t2 '[a] a, HasSpec a) =>
t1 s1 '[a] r -> t2 s2 '[a] a -> FunW "composeFn" '[a] r
ComposeW t1 s1 '[b] r
f t2 s2 '[a] b
g -- @b @c1 @c2 @s1 @s2 @t1 @t2 @a @r f g

-- =============================================================

composeFn :: (HasSpec b, HasSpec a, HasSpec c) => Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn :: forall b a c.
(HasSpec b, HasSpec a, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn (Fun t s '[b] c
f) (Fun t s '[a] b
g) = (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun (forall a (s1 :: Symbol) (s2 :: Symbol)
       (t1 :: Symbol -> [*] -> * -> *) (t2 :: Symbol -> [*] -> * -> *) a
       r.
(Logic s1 t1 '[a] r, Logic s2 t2 '[a] a, HasSpec a) =>
t1 s1 '[a] r -> t2 s2 '[a] a -> FunW "composeFn" '[a] r
ComposeW t s '[b] c
f t s '[a] b
g))

idFn :: HasSpec a => Fun '[a] a
idFn :: forall a. HasSpec a => Fun '[a] a
idFn = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a. FunW "id_" '[a] a
IdW

-- =======================================================
-- All the Foldy class instances are intimately tied to
-- Numbers. But that is not required, but this is a
-- convenient place to put the code.
-- =======================================================

class (HasSpec a, NumLike a, Logic "addFn" IntW '[a, a] a) => Foldy a where
  genList ::
    MonadGenError m => Specification a -> Specification a -> GenT m [a]
  theAddFn :: IntW "addFn" '[a, a] a
  theAddFn = forall b. NumLike b => IntW "addFn" '[b, b] b
AddW
  theZero :: a
  theZero = a
0
  genSizedList ::
    MonadGenError m =>
    Specification Integer -> Specification a -> Specification a -> GenT m [a]
  noNegativeValues :: Bool

instance Foldy Integer where
  noNegativeValues :: Bool
noNegativeValues = Bool
False
  genList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> Specification Integer -> GenT m [Integer]
genList = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Integer
-> Specification Integer
-> GenT m [Integer]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int -> Specification Int -> GenT m [Int]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int8 -> Specification Int8 -> GenT m [Int8]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int16 -> Specification Int16 -> GenT m [Int16]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int32 -> Specification Int32 -> GenT m [Int32]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Int64 -> Specification Int64 -> GenT m [Int64]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Natural
-> Specification Natural
-> GenT m [Natural]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word8 -> Specification Word8 -> GenT m [Word8]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word16 -> Specification Word16 -> GenT m [Word16]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word32 -> Specification Word32 -> GenT m [Word32]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 = forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList
  genSizedList :: forall (m :: * -> *).
MonadGenError m =>
Specification Integer
-> Specification Word64 -> Specification Word64 -> GenT m [Word64]
genSizedList = forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
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 s '[a] b
f) Specification a
argS b
x =
  let argSpec' :: Specification a
argSpec' = Specification a
argS forall a. Semigroup a => a -> a -> a
<> forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t s '[a] b
f (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) (forall a. a -> Specification a
equalSpec b
x)
   in forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"genInverse"
            , String
"  f = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t s '[a] b
f
            , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  argS =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
argS
            , String
"  x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
x
            , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  argSpec' =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
argSpec'
            ]
        )
        forall a b. (a -> b) -> a -> b
$ 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 (forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification Integer
size) Specification a
elemS fun :: Fun '[a] b
fun@(Fun t s '[a] b
fn) Specification b
foldS
  | forall a. Specification a -> Bool
isErrorLike Specification Integer
size =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"genFromFold has ErrorLike sizeSpec" (forall a. Specification a -> NonEmpty String
errorLikeMessage Specification Integer
size))
  | forall a. Specification a -> Bool
isErrorLike Specification a
elemS =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"genFromFold has ErrorLike elemSpec" (forall a. Specification a -> NonEmpty String
errorLikeMessage Specification a
elemS))
  | forall a. Specification a -> Bool
isErrorLike Specification b
foldS =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons String
"genFromFold has ErrorLike totalSpec" (forall a. Specification a -> NonEmpty String
errorLikeMessage Specification b
foldS))
  | Bool
otherwise = ( forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
                    ( forall a. [a] -> NonEmpty a
NE.fromList
                        [ String
"while calling genFromFold"
                        , String
"  must  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
must
                        , String
"  size  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
size
                        , String
"  elemS = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS
                        , String
"  fun   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Fun '[a] b
fun
                        , String
"  foldS = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification b
foldS
                        ]
                    )
                )
      forall a b. (a -> b) -> a -> b
$ do
        let elemS' :: Specification b
            elemS' :: Specification b
elemS' = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) a b.
(Logic s t '[a] b, HasSpec a, HasSpec b) =>
t s '[a] b -> Specification a -> Specification b
mapSpec t s '[a] b
fn Specification a
elemS
            mustVal :: b
mustVal = forall a. Foldy a => [a] -> a
adds (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t s '[a] b
fn) [a]
must)
            foldS' :: Specification b
            foldS' :: Specification b
foldS' = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context forall a. Foldy a => IntW "addFn" '[a, a] a
theAddFn (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> b
mustVal forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Post as1 hole y -> CList 'Post (a : as1) hole y
:<| forall hole y. CList 'Post '[] hole y
End)) Specification b
foldS
            sizeSpec' :: Specification Integer
            sizeSpec' :: Specification Integer
sizeSpec' = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context forall b. NumLike b => IntW "addFn" '[b, b] b
AddW (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> (forall t. Sized t => t -> Integer
sizeOf [a]
must) forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Post as1 hole y -> CList 'Post (a : as1) hole y
:<| forall hole y. CList 'Post '[] hole y
End)) Specification Integer
size
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Specification a -> Bool
isErrorLike Specification Integer
sizeSpec') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadGenError m => String -> m a
genError1 String
"Inconsistent size spec"
        [b]
results0 <- case Specification Integer
sizeSpec' of
          Specification Integer
TrueSpec -> forall a (m :: * -> *).
(Foldy a, MonadGenError m) =>
Specification a -> Specification a -> GenT m [a]
genList (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
elemS') (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
foldS')
          Specification Integer
_ -> forall a (m :: * -> *).
(Foldy a, MonadGenError m) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genSizedList Specification Integer
sizeSpec' (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
elemS') (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification b
foldS')
        [a]
results <-
          forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
            ( forall a. [a] -> NonEmpty a
NE.fromList
                [ String
"genInverse"
                , String
"  fun = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Fun '[a] b
fun
                , String
"  results0 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [b]
results0
                , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  elemS' =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification b
elemS'
                ]
            )
            forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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
        forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Gen [a]
shuffle forall a b. (a -> b) -> a -> b
$ [a]
must forall a. [a] -> [a] -> [a]
++ [a]
results

adds :: Foldy a => [a] -> a
adds :: forall a. Foldy a => [a] -> a
adds = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics forall a. Foldy a => IntW "addFn" '[a, a] a
theAddFn) forall a. Foldy a => a
theZero

addFun :: NumLike n => Fun '[n, n] n
addFun :: forall n. NumLike n => Fun '[n, n] n
addFun = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall b. NumLike b => IntW "addFn" '[b, b] b
AddW

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 = forall a. FoldSpec a
NoFold
preMapFoldSpec Fun '[a] b
f (FoldSpec Fun '[b] b
g Specification b
s) = forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec (forall b a c.
(HasSpec b, HasSpec a, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn Fun '[b] b
g Fun '[a] b
f) Specification b
s

combineFoldSpec :: FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec :: forall a. FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec FoldSpec a
NoFold FoldSpec a
s = forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec a
s
combineFoldSpec FoldSpec a
s FoldSpec a
NoFold = forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec a
s
combineFoldSpec (FoldSpec (Fun t s '[a] b
f) Specification b
s) (FoldSpec (Fun t s '[a] b
g) Specification b
s') =
  case forall (s1 :: Symbol) (t1 :: Symbol -> [*] -> * -> *) (d1 :: [*])
       r1 (s2 :: Symbol) (t2 :: Symbol -> [*] -> * -> *) (d2 :: [*]) r2.
(Logic s1 t1 d1 r1, Logic s2 t2 d2 r2) =>
t1 s1 d1 r1
-> t2 s2 d2 r2
-> Maybe (t1 s1 d1 r1, s1 :~: s2, t1 :~: t2, d1 :~: d2, r1 :~: r2)
sameFunSym t s '[a] b
f t s '[a] b
g of
    Just (t s '[a] b
_h, s :~: s
Refl, t :~: t
Refl, '[a] :~: '[a]
Refl, b :~: b
Refl) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun t s '[a] b
f) (Specification b
s forall a. Semigroup a => a -> a -> a
<> Specification b
s')
    Maybe (t s '[a] b, s :~: s, t :~: t, '[a] :~: '[a], b :~: b)
Nothing -> forall a b. a -> Either a b
Left [String
"Can't combine fold specs on different functions", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t s '[a] b
f, String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t s '[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 s '[a] b
f) Specification b
s) = forall a. Foldy a => [a] -> a
adds (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t s '[a] b
f) [a]
xs) forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification b
s

-- =============================================================================
-- Lists and Foldy are mutually recursive
-- Here are HasSpec instance for List and the Logic instances for List operators

data ListW (s :: Symbol) (args :: [Type]) (res :: Type) where
  FoldMapW :: forall a b. (Foldy b, HasSpec a) => Fun '[a] b -> ListW "foldMap_" '[[a]] b
  SingletonListW :: ListW "singeltonList_" '[a] [a]
  AppendW :: (Typeable a, Show a) => ListW "append_" '[[a], [a]] [a]

-- ====================== Semantics for ListW

instance Semantics ListW where
  semantics :: forall (s :: Symbol) (d :: [*]) r. ListW s d r -> FunTy d r
semantics = forall (s :: Symbol) (d :: [*]) r. ListW s d r -> FunTy d r
listSem

instance Syntax ListW where
  prettyWit :: forall (s :: Symbol) (dom :: [*]) rng ann.
(All HasSpec dom, HasSpec rng) =>
ListW s dom rng -> List Term dom -> Int -> Maybe (Doc ann)
prettyWit ListW s dom rng
AppendW (Lit a
n :> Term a
y :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"append_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short a
n forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y
  prettyWit ListW s dom rng
AppendW (Term a
y :> Lit a
n :> List Term as1
Nil) Int
p = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ Doc ann
"append_" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
y forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a x. (Show a, Typeable a) => [a] -> Doc x
short a
n
  prettyWit ListW s dom rng
_ List Term dom
_ Int
_ = forall a. Maybe a
Nothing

listSem :: ListW s dom rng -> FunTy dom rng
listSem :: forall (s :: Symbol) (d :: [*]) r. ListW s d r -> FunTy d r
listSem (FoldMapW (Fun t s '[a] rng
f)) = forall a. Foldy a => [a] -> a
adds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: Symbol -> [*] -> * -> *) (s :: Symbol) (d :: [*]) r.
Semantics t =>
t s d r -> FunTy d r
semantics t s '[a] rng
f)
listSem ListW s dom rng
SingletonListW = (forall a. a -> [a] -> [a]
: [])
listSem ListW s dom rng
AppendW = forall a. [a] -> [a] -> [a]
(++)

instance Show (ListW s d r) where
  show :: ListW s d r -> String
show ListW s d r
AppendW = String
"append_"
  show ListW s d r
SingletonListW = String
"singletonList_"
  show (FoldMapW Fun '[a] r
n) = String
"(FoldMapW  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Fun '[a] r
n forall a. [a] -> [a] -> [a]
++ String
")"

deriving instance (Eq (ListW s d r))

-- ============= Logicbol for FoldMapW

instance (Typeable a, Foldy b) => Logic "foldMap_" ListW '[[a]] b where
  propagate :: forall hole.
Context "foldMap_" ListW '[[a]] b hole
-> Specification b -> Specification hole
propagate Context "foldMap_" ListW '[[a]] b hole
ctxt (ExplainSpec [] Specification b
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "foldMap_" ListW '[[a]] b hole
ctxt Specification b
s
  propagate Context "foldMap_" ListW '[[a]] b hole
ctxt (ExplainSpec [String]
es Specification b
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "foldMap_" ListW '[[a]] b hole
ctxt Specification b
s
  propagate Context "foldMap_" ListW '[[a]] b hole
_ Specification b
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "foldMap_" ListW '[[a]] b hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context (FoldMapW Fun '[a] b
f) (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var b
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App (forall a b.
(Foldy b, HasSpec a) =>
Fun '[a] b -> ListW "foldMap_" '[[a]] b
FoldMapW Fun '[a] b
f) (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context (FoldMapW Fun '[a] b
f) (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec TypeSpec b
ts [b]
cant) =
    forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [] forall a. Specification a
TrueSpec forall a. Specification a
TrueSpec forall a b. (a -> b) -> a -> b
$ forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec Fun '[a] b
f (forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec TypeSpec b
ts [b]
cant))
  propagate (Context (FoldMapW Fun '[a] b
f) (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty b
es) =
    forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [] forall a. Specification a
TrueSpec forall a. Specification a
TrueSpec forall a b. (a -> b) -> a -> b
$ forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec Fun '[a] b
f (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty b
es))
  propagate Context "foldMap_" ListW '[[a]] b hole
ctx Specification b
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for FoldMapW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "foldMap_" ListW '[[a]] b hole
ctx)

  mapTypeSpec :: forall a b.
('[[a]] ~ '[a], b ~ b, HasSpec a, HasSpec b) =>
ListW "foldMap_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec (FoldMapW Fun '[a] b
g) TypeSpec a
ts =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term b
x ->
      forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists forall a b. (a -> b) -> a -> b
$ \Term [a]
x' ->
        Term Bool -> Pred
Assert (Term b
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall x b.
(HasSpec x, HasSpec b) =>
Fun '[x] b -> Term x -> Term b
appFun (forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn Fun '[a] b
g) Term [a]
x') forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term [a]
x' TypeSpec a
ts

foldMap_ :: forall a b. (Sized [a], Foldy b, HasSpec a) => (Term a -> Term b) -> Term [a] -> Term b
foldMap_ :: forall a b.
(Sized [a], Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ Term a -> Term b
f = forall x b.
(HasSpec x, HasSpec b) =>
Fun '[x] b -> Term x -> Term b
appFun forall a b. (a -> b) -> a -> b
$ forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn forall a b. (a -> b) -> a -> b
$ forall x. HasCallStack => Term x -> Fun '[a] x
toFn forall a b. (a -> b) -> a -> b
$ Term a -> Term b
f (forall a. HasSpec a => Var a -> Term a
V Var a
v)
  where
    v :: Var a
v = forall a. Int -> String -> Var a
Var (-Int
1) String
"v" :: Var a
    -- Turn `f (V v) = fn (gn (hn v))` into `composeFn fn (composeFn gn hn)`
    -- Note: composeFn :: HasSpec b => Fun '[b] c -> Fun '[a] b -> Fun '[a] c
    toFn :: forall x. HasCallStack => Term x -> Fun '[a] x
    toFn :: forall x. HasCallStack => Term x -> Fun '[a] x
toFn (App t sym dom x
fn (V Var a
v' :> List Term as1
Nil)) | Just a :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a
v' = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun t sym dom x
fn
    toFn (App t sym dom x
fn (Term a
t :> List Term as1
Nil)) = forall b a c.
(HasSpec b, HasSpec a, HasSpec c) =>
Fun '[b] c -> Fun '[a] b -> Fun '[a] c
composeFn (forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun t sym dom x
fn) (forall x. HasCallStack => Term x -> Fun '[a] x
toFn Term a
t)
    toFn (V Var x
v') | Just a :~: x
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var x
v' = forall a. HasSpec a => Fun '[a] a
idFn
    toFn Term x
_ = forall a. HasCallStack => String -> a
error String
"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_ = forall a b.
(Sized [a], Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ forall a. a -> a
id

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 = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun (forall a b.
(Foldy b, HasSpec a) =>
Fun '[a] b -> ListW "foldMap_" '[[a]] b
FoldMapW Fun '[a] b
f)

-- | Used in the HasSpec [a] instance
toPredsFoldSpec :: (HasSpec a, HasSpec [a]) => Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec :: forall a.
(HasSpec a, HasSpec [a]) =>
Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec Term [a]
_ FoldSpec a
NoFold = Pred
TruePred
toPredsFoldSpec Term [a]
x (FoldSpec Fun '[a] b
funAB Specification b
sspec) =
  forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall x b.
(HasSpec x, HasSpec b) =>
Fun '[x] b -> Term x -> Term b
appFun (forall a b. (HasSpec a, Foldy b) => Fun '[a] b -> Fun '[[a]] b
foldMapFn Fun '[a] b
funAB) Term [a]
x) Specification b
sspec

-- ============ Logicbol for ElemW

instance HasSpec a => Logic "elem_" BaseW '[a, [a]] Bool where
  propagate :: forall hole.
Context "elem_" BaseW '[a, [a]] Bool hole
-> Specification Bool -> Specification hole
propagate Context "elem_" BaseW '[a, [a]] Bool hole
ctxt (ExplainSpec [] Specification Bool
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "elem_" BaseW '[a, [a]] Bool hole
ctxt Specification Bool
s
  propagate Context "elem_" BaseW '[a, [a]] Bool hole
ctxt (ExplainSpec [String]
es Specification Bool
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "elem_" BaseW '[a, [a]] Bool hole
ctxt Specification Bool
s
  propagate Context "elem_" BaseW '[a, [a]] Bool hole
_ Specification Bool
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "elem_" BaseW '[a, [a]] Bool hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context BaseW "elem_" '[a, [a]] Bool
ElemW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. Eq a => BaseW "elem_" '[a, [a]] Bool
ElemW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "elem_" '[a, [a]] Bool
ElemW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var Bool
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. Eq a => BaseW "elem_" '[a, [a]] Bool
ElemW (forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var Bool
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context BaseW "elem_" '[a, [a]] Bool
ElemW (Ctx hole y
HOLE :<> a
es :<| CList 'Post as1 Any Any
End)) Specification Bool
spec =
    forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification Bool
spec forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> forall a. [a] -> NonEmpty String -> Specification a
memberSpecList (forall a. Eq a => [a] -> [a]
nub a
es) (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"propagate on (elem_ x []), The empty list, [], has no solution")
      Bool
False -> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec a
es
  propagate (Context BaseW "elem_" '[a, [a]] Bool
ElemW (a
e :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) Specification Bool
spec =
    forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification Bool
spec forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [a
e] forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. FoldSpec a
NoFold)
      Bool
False -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty (forall a. HasSpec a => a -> Specification a
notEqualSpec a
e) forall a. FoldSpec a
NoFold)
  propagate Context "elem_" BaseW '[a, [a]] Bool hole
ctx Specification Bool
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for ElemW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "elem_" BaseW '[a, [a]] Bool hole
ctx)

  rewriteRules :: (TypeList '[a, [a]], Typeable '[a, [a]], HasSpec Bool,
 All HasSpec '[a, [a]]) =>
BaseW "elem_" '[a, [a]] Bool
-> List Term '[a, [a]]
-> Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool)
-> Maybe (Term Bool)
rewriteRules BaseW "elem_" '[a, [a]] Bool
ElemW (Term a
_ :> Lit [] :> List Term as1
Nil) Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool)
Evidence = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Literal a => a -> Term a
Lit Bool
False
  rewriteRules BaseW "elem_" '[a, [a]] Bool
ElemW (Term a
t :> Lit [a
a] :> List Term as1
Nil) Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool)
Evidence = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term a
t forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (forall a. Literal a => a -> Term a
Lit a
a)
  rewriteRules BaseW "elem_" '[a, [a]] Bool
_ List Term '[a, [a]]
_ Evidence (AppRequires "elem_" BaseW '[a, [a]] Bool)
_ = forall a. Maybe a
Nothing

  saturate :: BaseW "elem_" '[a, [a]] Bool -> List Term '[a, [a]] -> [Pred]
saturate BaseW "elem_" '[a, [a]] Bool
ElemW (FromGeneric (Product (Term a
x :: Term m) (Term b
y :: Term n)) :> 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)
eqT @a @(m, n) = case a
zs of
        ((a, b)
w : [(a, b)]
ws) -> [forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
True Term a
x (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst ((a, b)
w forall a. a -> [a] -> NonEmpty a
:| [(a, b)]
ws))]
        [] -> [NonEmpty String -> Pred
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String
"empty list, zs , in elem_ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term a
x, Term b
y) forall a. [a] -> [a] -> [a]
++ String
" zs")]
  saturate BaseW "elem_" '[a, [a]] Bool
ElemW (Term a
x :> Lit (a
y : [a]
ys) :> List Term as1
Nil) = [forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
x (forall a. NonEmpty a -> Specification a
MemberSpec (a
y forall a. a -> [a] -> NonEmpty a
:| [a]
ys))]
  saturate BaseW "elem_" '[a, [a]] Bool
_ List Term '[a, [a]]
_ = []

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_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. Eq a => BaseW "elem_" '[a, [a]] Bool
ElemW

elemFn :: HasSpec a => Fun '[a, [a]] Bool
elemFn :: forall a. HasSpec a => Fun '[a, [a]] Bool
elemFn = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a. Eq a => BaseW "elem_" '[a, [a]] Bool
ElemW

-- ============= Logicbol for SingletonListW

instance HasSpec a => Logic "singeltonList_" ListW '[a] [a] where
  propagate :: forall hole.
Context "singeltonList_" ListW '[a] [a] hole
-> Specification [a] -> Specification hole
propagate Context "singeltonList_" ListW '[a] [a] hole
ctxt (ExplainSpec [] Specification [a]
s) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "singeltonList_" ListW '[a] [a] hole
ctxt Specification [a]
s
  propagate Context "singeltonList_" ListW '[a] [a] hole
ctxt (ExplainSpec [String]
es Specification [a]
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "singeltonList_" ListW '[a] [a] hole
ctxt Specification [a]
s
  propagate Context "singeltonList_" ListW '[a] [a] hole
_ Specification [a]
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "singeltonList_" ListW '[a] [a] hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context ListW "singeltonList_" '[a] [a]
SingletonListW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var [a]
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. ListW "singeltonList_" '[a] [a]
SingletonListW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var [a]
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context ListW "singeltonList_" '[a] [a]
SingletonListW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (TypeSpec (ListSpec Maybe Integer
_ [hole]
m Specification Integer
sz Specification hole
e FoldSpec hole
f) [[a]]
cant)
    | forall (t :: * -> *) a. Foldable t => t a -> Int
length [hole]
m forall a. Ord a => a -> a -> Bool
> Int
1 =
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"Too many required elements for SingletonListW : "
            , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [hole]
m
            ]
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Integer
1 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
sz =
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String
"Size spec requires too many elements for SingletonListW : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
sz
    | bad :: [hole]
bad@(hole
_ : [hole]
_) <- forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification hole
e)) [hole]
m =
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"The following elements of the must spec do not conforms to the elem spec:"
            , forall a. Show a => a -> String
show [hole]
bad
            ]
    -- There is precisely one required element in the final list, so the argument to singletonList_ has to
    -- be that element and we have to respect the cant and fold specs
    | [hole
a] <- [hole]
m = forall a. a -> Specification a
equalSpec hole
a forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
z | [a
z] <- [[a]]
cant] forall a. Semigroup a => a -> a -> a
<> forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec hole
f
    -- We have to respect the elem-spec, the can't spec, and the fold spec.
    | Bool
otherwise = Specification hole
e forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [a
a | [a
a] <- [[a]]
cant] forall a. Semigroup a => a -> a -> a
<> forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec hole
f
  propagate (Context ListW "singeltonList_" '[a] [a]
SingletonListW (Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (MemberSpec NonEmpty [a]
xss) =
    case [a
a | [a
a] <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty [a]
xss] of
      [] ->
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"PropagateSpec SingletonListW  with MemberSpec which has no lists of length 1")
      (a
x : [a]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec (a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
  propagate Context "singeltonList_" ListW '[a] [a] hole
ctx Specification [a]
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for SingletonListW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "singeltonList_" ListW '[a] [a] hole
ctx)

  -- NOTE: this function over-approximates and returns a liberal spec.
  mapTypeSpec :: forall a b.
('[a] ~ '[a], [a] ~ b, HasSpec a, HasSpec b) =>
ListW "singeltonList_" '[a] b -> TypeSpec a -> Specification b
mapTypeSpec ListW "singeltonList_" '[a] b
SingletonListW TypeSpec a
ts = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [] (forall a. a -> Specification a
equalSpec Integer
1) (forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec a
ts) forall a. FoldSpec a
NoFold)

reverseFoldSpec :: FoldSpec a -> Specification a
reverseFoldSpec :: forall a. FoldSpec a -> Specification a
reverseFoldSpec FoldSpec a
NoFold = forall a. Specification a
TrueSpec
-- The single element list has to sum to something that obeys spec, i.e. `conformsToSpec (f a) spec`
reverseFoldSpec (FoldSpec (Fun t s '[a] b
fn) Specification b
spec) = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context t s '[a] b
fn (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> forall hole y. CList 'Post '[] hole y
End)) Specification b
spec

singletonList_ :: (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ :: forall a. (Sized [a], HasSpec a) => Term a -> Term [a]
singletonList_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. ListW "singeltonList_" '[a] [a]
SingletonListW

singletonListFn :: forall a. HasSpec a => Fun '[a] [a]
singletonListFn :: forall a. HasSpec a => Fun '[a] [a]
singletonListFn = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a. ListW "singeltonList_" '[a] [a]
SingletonListW

-- ============== Logicbol for AppendW

instance (Sized [a], HasSpec a) => Logic "append_" ListW '[[a], [a]] [a] where
  propagate :: forall hole.
Context "append_" ListW '[[a], [a]] [a] hole
-> Specification [a] -> Specification hole
propagate Context "append_" ListW '[[a], [a]] [a] hole
ctxt (ExplainSpec [String]
es Specification [a]
s) = forall a. [String] -> Specification a -> Specification a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate Context "append_" ListW '[[a], [a]] [a] hole
ctxt Specification [a]
s
  propagate Context "append_" ListW '[[a], [a]] [a] hole
_ Specification [a]
TrueSpec = forall a. Specification a
TrueSpec
  propagate Context "append_" ListW '[[a], [a]] [a] hole
_ (ErrorSpec NonEmpty String
msgs) = forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
msgs
  propagate (Context ListW "append_" '[[a], [a]] [a]
AppendW (Ctx hole y
HOLE :<> a
x :<| CList 'Post as1 Any Any
End)) (SuspendedSpec Var [a]
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Typeable a, Show a) => ListW "append_" '[[a], [a]] [a]
AppendW (Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var [a]
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context ListW "append_" '[[a], [a]] [a]
AppendW (a
x :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End)) (SuspendedSpec Var [a]
v Pred
ps) =
    forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term hole
v' -> forall a. Term a -> Binder a -> Pred
Let (forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       a.
AppRequires sym t dom a =>
t sym dom a -> List Term dom -> Term a
App forall a. (Typeable a, Show a) => ListW "append_" '[[a], [a]] [a]
AppendW (forall a. Literal a => a -> Term a
Lit a
x forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term hole
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)) (Var [a]
v forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate (Context ListW "append_" '[[a], [a]] [a]
AppendW CList 'Pre '[[a], [a]] hole y
ctx) (TypeSpec (ts :: TypeSpec [a]
ts@ListSpec {listSpecElem :: forall a. ListSpec a -> Specification a
listSpecElem = Specification a
e}) [[a]]
cant)
    | (Ctx hole y
HOLE :<> ([a]
ys :: [a]) :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[[a], [a]] hole y
ctx
    , Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a]
    , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e) [a]
ys =
        forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall a. Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave [a]
ys TypeSpec [a]
ts) (forall a. Eq a => [a] -> [[a]] -> [[a]]
suffixedBy [a]
ys [[a]]
cant)
    | (([a]
ys :: [a]) :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[[a], [a]] hole y
ctx
    , Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a]
    , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
e) [a]
ys =
        forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall a. Eq a => [a] -> ListSpec a -> ListSpec a
alreadyHave [a]
ys TypeSpec [a]
ts) (forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys [[a]]
cant)
    | Bool
otherwise = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"The spec given to propagate for AppendW is inconsistent!"
  propagate (Context ListW "append_" '[[a], [a]] [a]
AppendW CList 'Pre '[[a], [a]] hole y
ctx) (MemberSpec NonEmpty [a]
xss)
    | (Ctx hole y
HOLE :<> ([a]
ys :: [a]) :<| CList 'Post as1 Any Any
End) <- CList 'Pre '[[a], [a]] hole y
ctx
    , Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a] =
        -- Only keep the prefixes of the elements of xss that can
        -- give you the correct resulting list
        case forall a. Eq a => [a] -> [[a]] -> [[a]]
suffixedBy [a]
ys (forall a. NonEmpty a -> [a]
NE.toList NonEmpty [a]
xss) of
          [] ->
            forall a. NonEmpty String -> Specification a
ErrorSpec
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  [ String
"propagateSpecFun (append HOLE ys) with (MemberSpec xss)"
                  , String
"there are no elements in xss with suffix ys"
                  ]
              )
          ([a]
x : [[a]]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec ([a]
x forall a. a -> [a] -> NonEmpty a
:| [[a]]
xs)
    | (([a]
ys :: [a]) :|> Ctx hole y
HOLE :<> CList 'Post as1 Any Any
forall i j. CList 'Post as1 i j
End) <- CList 'Pre '[[a], [a]] hole y
ctx
    , Evidence (Prerequisites [a])
Evidence <- forall a. HasSpec a => Evidence (Prerequisites a)
prerequisites @[a] =
        -- Only keep the suffixes of the elements of xss that can
        -- give you the correct resulting list
        case forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys (forall a. NonEmpty a -> [a]
NE.toList NonEmpty [a]
xss) of
          [] ->
            forall a. NonEmpty String -> Specification a
ErrorSpec
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  [ String
"propagateSpecFun (append ys HOLE) with (MemberSpec xss)"
                  , String
"there are no elements in xss with prefix ys"
                  ]
              )
          ([a]
x : [[a]]
xs) -> forall a. NonEmpty a -> Specification a
MemberSpec ([a]
x forall a. a -> [a] -> NonEmpty a
:| [[a]]
xs)
  propagate Context "append_" ListW '[[a], [a]] [a] hole
ctx Specification [a]
_ =
    forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Logic instance for AppendW with wrong number of arguments. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Context "append_" ListW '[[a], [a]] [a] hole
ctx)

prefixedBy :: Eq a => [a] -> [[a]] -> [[a]]
prefixedBy :: forall a. Eq a => [a] -> [[a]] -> [[a]]
prefixedBy [a]
ys [[a]]
xss = [forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys) [a]
xs | [a]
xs <- [[a]]
xss, [a]
ys 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 = [forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys) [a]
xs | [a]
xs <- [[a]]
xss, [a]
ys forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [a]
xs]

alreadyHave {- (Eq a, Typeable a, Show a) -} :: 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) =
  forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec
    -- Reduce the hint
    (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Num a => a -> a -> a
subtract (forall t. Sized t => t -> Integer
sizeOf [a]
ys)) Maybe Integer
h)
    -- The things in `ys` have already been added to the list, no need to
    -- require them too
    ([a]
m forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
ys)
    -- Reduce the required size
    (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
x -> (Term Integer
x forall a. Num a => a -> a -> a
+ forall a. Literal a => a -> Term a
Lit (forall t. Sized t => t -> Integer
sizeOf [a]
ys)) forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification Integer
sz)
    -- Nothing changes about what's a correct element
    Specification a
e
    -- we have fewer things to sum now
    (forall a. [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold [a]
ys FoldSpec a
f)

alreadyHaveFold {- (Typeable a, Show a) => -} :: [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold :: forall a. [a] -> FoldSpec a -> FoldSpec a
alreadyHaveFold [a]
_ FoldSpec a
NoFold = forall a. FoldSpec a
NoFold
alreadyHaveFold [a]
ys (FoldSpec Fun '[a] b
fn Specification b
spec) =
  forall a a.
(HasSpec a, HasSpec a, Foldy a) =>
Fun '[a] a -> Specification a -> FoldSpec a
FoldSpec
    Fun '[a] b
fn
    (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term b
s -> forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. Foldy a => IntW "addFn" '[a, a] a
theAddFn Term b
s (forall a b.
(Sized [a], Foldy b, HasSpec a) =>
(Term a -> Term b) -> Term [a] -> Term b
foldMap_ (forall x b.
(HasSpec x, HasSpec b) =>
Fun '[x] b -> Term x -> Term b
appFun Fun '[a] b
fn) (forall a. Literal a => a -> Term a
Lit [a]
ys)) forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification b
spec)

appendFn :: forall a. (Sized [a], HasSpec a) => Fun '[[a], [a]] [a]
appendFn :: forall a. (Sized [a], HasSpec a) => Fun '[[a], [a]] [a]
appendFn = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng.
Logic s t dom rng =>
t s dom rng -> Fun dom rng
Fun forall a. (Typeable a, Show a) => ListW "append_" '[[a], [a]] [a]
AppendW

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_ = forall (sym :: Symbol) (t :: Symbol -> [*] -> * -> *) (ds :: [*])
       r.
AppRequires sym t ds r =>
t sym ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. (Typeable a, Show a) => ListW "append_" '[[a], [a]] [a]
AppendW

-- ================================================
-- Sized instance for Lists

instance Sized [a] where
  sizeOf :: [a] -> Integer
sizeOf = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length
  liftSizeSpec :: HasSpec [a] => NumSpec Integer -> [Integer] -> Specification [a]
liftSizeSpec NumSpec Integer
spec [Integer]
cant = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing forall a. Monoid a => a
mempty (forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec NumSpec Integer
spec [Integer]
cant) forall a. Specification a
TrueSpec forall a. FoldSpec a
NoFold)
  liftMemberSpec :: HasSpec [a] => [Integer] -> Specification [a]
liftMemberSpec [Integer]
xs = case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [Integer]
xs of
    Maybe (NonEmpty Integer)
Nothing -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In liftMemberSpec for (Sized List) instance, xs is the empty list"))
    Just NonEmpty Integer
zs -> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing forall a. Monoid a => a
mempty (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty Integer
zs) forall a. Specification a
TrueSpec forall a. FoldSpec a
NoFold)
  sizeOfTypeSpec :: HasSpec [a] => TypeSpec [a] -> Specification Integer
sizeOfTypeSpec (ListSpec Maybe Integer
_ [a]
_ Specification Integer
_ ErrorSpec {} FoldSpec a
_) = forall a. a -> Specification a
equalSpec Integer
0
  sizeOfTypeSpec (ListSpec Maybe Integer
_ [a]
must Specification Integer
sizespec Specification a
_ FoldSpec a
_) = Specification Integer
sizespec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf [a]
must)

-- ================================================================
-- The TypeSpec for List. Used in the HasSpec instance for Lists
-- ================================================================

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
  ( Arbitrary a
  , Arbitrary (FoldSpec a)
  , Arbitrary (TypeSpec a)
  , HasSpec a
  ) =>
  Arbitrary (ListSpec a)
  where
  arbitrary :: Gen (ListSpec a)
arbitrary = forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
  shrink :: ListSpec a -> [ListSpec a]
shrink (ListSpec Maybe Integer
a [a]
b Specification Integer
c Specification a
d FoldSpec a
e) = [forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
a' [a]
b' Specification Integer
c' Specification a
d' FoldSpec a
e' | (Maybe Integer
a', [a]
b', Specification Integer
c', Specification a
d', FoldSpec a
e') <- forall a. Arbitrary a => a -> [a]
shrink (Maybe Integer
a, [a]
b, Specification Integer
c, Specification a
d, FoldSpec a
e)]

instance HasSpec a => Show (FoldSpec a) where
  showsPrec :: Int -> FoldSpec a -> ShowS
showsPrec Int
d = forall a. Show a => a -> ShowS
shows forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)) =
    forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      Doc ann
"FoldSpec"
        forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
          [ Doc ann
"fn   =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Fun '[a] b
fun
          , Doc ann
"spec =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification b
s
          ]

instance HasSpec a => Pretty (FoldSpec a) where
  pretty :: forall ann. FoldSpec a -> Doc ann
pretty = 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 = forall a. Show a => a -> ShowS
shows forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
    forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      Doc ann
"ListSpec"
        forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
          [ Doc ann
"hint =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall a. ListSpec a -> Maybe Integer
listSpecHint ListSpec a
s)
          , Doc ann
"must =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow (forall a. ListSpec a -> [a]
listSpecMust ListSpec a
s)
          , Doc ann
"size =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. ListSpec a -> Specification Integer
listSpecSize ListSpec a
s)
          , Doc ann
"elem =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. ListSpec a -> Specification a
listSpecElem ListSpec a
s)
          , Doc ann
"fold =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (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 = 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 => [String] -> ListSpec a -> Specification [a]
guardListSpec [String]
msg l :: ListSpec a
l@(ListSpec Maybe Integer
_hint [a]
must Specification Integer
size Specification a
elemS FoldSpec a
_fold)
  | ErrorSpec NonEmpty String
es <- Specification Integer
size = forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ (forall a. [a] -> NonEmpty a
NE.fromList (String
"Error in size of ListSpec" forall a. a -> [a] -> [a]
: [String]
msg)) forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es
  | Just Integer
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification Integer
size
  , Integer
u forall a. Ord a => a -> a -> Bool
< Integer
0 =
      forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList ([String
"Negative size in guardListSpec", forall a. Show a => a -> String
show Specification Integer
size] forall a. [a] -> [a] -> [a]
++ [String]
msg)
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) [a]
must) =
      forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
        ( forall a. [a] -> NonEmpty a
NE.fromList
            ([String
"Some items in the must list do not conform to 'element' spec.", String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS] forall a. [a] -> [a] -> [a]
++ [String]
msg)
        )
  | Bool
otherwise = (forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec 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 = forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [] forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty 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'' = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [a]
must forall a. Semigroup a => a -> a -> a
<> [a]
must'
        elemS'' :: Specification a
elemS'' = Specification a
elemS forall a. Semigroup a => a -> a -> a
<> Specification a
elemS'
        size'' :: Specification Integer
size'' = Specification Integer
size forall a. Semigroup a => a -> a -> a
<> Specification Integer
size'
        foldeither :: Either [String] (FoldSpec a)
foldeither = forall a. FoldSpec a -> FoldSpec a -> Either [String] (FoldSpec a)
combineFoldSpec FoldSpec a
foldS FoldSpec a
foldS'
        msg :: [String]
msg = [String
"Error in combineSpec for ListSpec", String
"1) " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec [a]
l1, String
"2) " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec [a]
l2]
     in case Either [String] (FoldSpec a)
foldeither of
          Left [String]
foldmsg -> forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList ([String]
msg forall a. [a] -> [a] -> [a]
++ [String]
foldmsg))
          Right FoldSpec a
fold'' -> forall a. HasSpec a => [String] -> ListSpec a -> Specification [a]
guardListSpec [String]
msg forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe 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
_)
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS)) [a]
must =
        forall (m :: * -> *) a. MonadGenError m => String -> m a
genError1 String
"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 -> forall (m :: * -> *) a. MonadGenError m => GenT GE a -> GenT m [a]
listOfT forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS
      Just Integer
szHint -> do
        Integer
sz <- forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec (forall a. OrdLike a => a -> Specification a
leqSpec Integer
szHint)
        forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
listOfUntilLenT (forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sz) (forall a b. a -> b -> a
const Bool
True)
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Gen [a]
shuffle ([a]
must 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 <- forall (m :: * -> *).
MonadGenError m =>
Specification Integer -> GenT m Integer
genFromSizeSpec (Specification Integer
szSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec (forall t. Sized t => t -> Integer
sizeOf [a]
must) forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Specification a
TrueSpec (forall a. OrdLike a => a -> Specification a
leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
msz)
    let sz :: Int
sz = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
sz0 forall a. Num a => a -> a -> a
- forall t. Sized t => t -> Integer
sizeOf [a]
must)
    [a]
lst <-
      forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT GE a -> Int -> (Int -> Bool) -> GenT m [a]
listOfUntilLenT
        (forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS)
        Int
sz
        ((forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
szSpec) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+ forall t. Sized t => t -> Integer
sizeOf [a]
must) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral)
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Gen [a]
shuffle ([a]
must 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 forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Specification a
TrueSpec (forall a. OrdLike a => a -> Specification a
leqSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Integer
0) Maybe Integer
msz
    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 =
    forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
es) [a]
as

  cardinalTypeSpec :: TypeSpec [a] -> Specification Integer
cardinalTypeSpec TypeSpec [a]
_ = forall a. Specification a
TrueSpec

  guardTypeSpec :: [String] -> TypeSpec [a] -> Specification [a]
guardTypeSpec = forall a. HasSpec a => [String] -> 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) =
    forall t. Sized t => t -> Integer
sizeOf [a]
xs forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification Integer
size
      Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
xs) [a]
must
      Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS) [a]
xs
      Bool -> Bool -> Bool
&& [a]
xs 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) =
    (forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [a]
x forall a b. (a -> b) -> a -> b
$ \Term a
x' -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
x' Specification a
elemS)
      forall a. Semigroup a => a -> a -> a
<> (forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall a. Literal a => a -> Term a
Lit [a]
must) forall a b. (a -> b) -> a -> b
$ \Term a
x' -> Term Bool -> Pred
Assert (forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term a
x' Term [a]
x))
      forall a. Semigroup a => a -> a -> a
<> forall a.
(HasSpec a, HasSpec [a]) =>
Term [a] -> FoldSpec a -> Pred
toPredsFoldSpec Term [a]
x FoldSpec a
foldS
      forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ Term [a]
x) Specification Integer
size
      forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pred
TruePred (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Term [a]
x) Maybe Integer
msz

instance (Sized [a], HasSpec a) => HasGenHint [a] where
  type Hint [a] = Integer
  giveHint :: Hint [a] -> Specification [a]
giveHint Hint [a]
szHint = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec (forall a. a -> Maybe a
Just Hint [a]
szHint) [] forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. FoldSpec a
NoFold

instance Forallable [a] a where
  fromForAllSpec :: (HasSpec [a], HasSpec a) => Specification a -> Specification [a]
fromForAllSpec Specification a
es = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec forall a. Maybe a
Nothing [] forall a. Monoid a => a
mempty Specification a
es forall a. FoldSpec a
NoFold)
  forAllToList :: [a] -> [a]
forAllToList = forall a. a -> a
id

-- ==========================================================
-- helpers

knownUpperBound ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
  Specification a ->
  Maybe a
knownUpperBound :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound (ExplainSpec [String]
_ Specification a
s) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
s
knownUpperBound Specification a
TrueSpec = forall a. MaybeBounded a => Maybe a
upperBound
knownUpperBound (MemberSpec NonEmpty a
as) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty a
as
knownUpperBound ErrorSpec {} = forall a. Maybe a
Nothing
knownUpperBound SuspendedSpec {} = forall a. MaybeBounded a => Maybe a
upperBound
knownUpperBound (TypeSpec (NumSpecInterval Maybe a
lo Maybe a
hi) [a]
cant) = Maybe a -> Maybe a -> Maybe a
upper (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound)
  where
    upper :: Maybe a -> Maybe a -> Maybe a
upper Maybe a
_ Maybe a
Nothing = forall a. Maybe a
Nothing
    upper Maybe a
Nothing (Just a
b) = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
b, a
b forall a. Num a => a -> a -> a
- a
1 ..] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
    upper (Just a
a) (Just a
b)
      | a
a forall a. Eq a => a -> a -> Bool
== a
b = a
a forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
      | Bool
otherwise = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
b, a
b forall a. Num a => a -> a -> a
- a
1 .. a
a] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

knownLowerBound ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
  Specification a ->
  Maybe a
knownLowerBound :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound (ExplainSpec [String]
_ Specification a
s) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
s
knownLowerBound Specification a
TrueSpec = forall a. MaybeBounded a => Maybe a
lowerBound
knownLowerBound (MemberSpec NonEmpty a
as) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum NonEmpty a
as
knownLowerBound ErrorSpec {} = forall a. Maybe a
Nothing
knownLowerBound SuspendedSpec {} = forall a. MaybeBounded a => Maybe a
lowerBound
knownLowerBound (TypeSpec (NumSpecInterval Maybe a
lo Maybe a
hi) [a]
cant) =
  Maybe a -> Maybe a -> Maybe a
lower (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound)
  where
    lower :: Maybe a -> Maybe a -> Maybe a
lower Maybe a
Nothing Maybe a
_ = forall a. Maybe a
Nothing
    lower (Just a
a) Maybe a
Nothing = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
a, a
a forall a. Num a => a -> a -> a
+ a
1 ..] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant
    lower (Just a
a) (Just a
b)
      | a
a forall a. Eq a => a -> a -> Bool
== a
b = a
a forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
cant)
      | Bool
otherwise = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ [a
a, a
a forall a. Num a => a -> a -> a
+ a
1 .. a
b] forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

isEmptyNumSpec ::
  (TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Specification a -> Bool
isEmptyNumSpec :: forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec = \case
  ExplainSpec [String]
_ Specification a
s -> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
s
  ErrorSpec {} -> Bool
True
  Specification a
TrueSpec -> Bool
False
  MemberSpec NonEmpty a
_ -> Bool
False -- MemberSpec always has at least one element (NE.NonEmpty)
  SuspendedSpec {} -> Bool
False
  TypeSpec TypeSpec a
i [a]
cant -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval TypeSpec a
i forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
cant

-- | Note: potentially infinite list
enumerateInterval :: (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval :: forall a. (Enum a, Num a, MaybeBounded a) => NumSpec a -> [a]
enumerateInterval (NumSpecInterval Maybe a
lo Maybe a
hi) =
  case (Maybe a
lo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound, Maybe a
hi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound) of
    (Maybe a
Nothing, Maybe a
Nothing) -> forall a. [a] -> [a] -> [a]
interleave [a
0 ..] [-a
1, -a
2 ..]
    (Maybe a
Nothing, Just a
b) -> [a
b, a
b forall a. Num a => a -> a -> a
- a
1 ..]
    (Just a
a, Maybe a
Nothing) -> [a
a ..]
    (Just a
a, Just a
b) -> [a
a .. a
b]
  where
    interleave :: [a] -> [a] -> [a]
interleave [] [a]
ys = [a]
ys
    interleave (a
x : [a]
xs) [a]
ys = a
x forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
interleave [a]
ys [a]
xs

-- ========================================================================
-- Operations to complete the Foldy instances genNumList, genListWithSize

genNumList ::
  forall a m.
  ( MonadGenError m
  , Arbitrary a
  , Integral a
  , MaybeBounded a
  , TypeSpec a ~ NumSpec a
  , Foldy a
  , Random a
  ) =>
  Specification a ->
  Specification a ->
  GenT m [a]
genNumList :: forall a (m :: * -> *).
(MonadGenError m, Arbitrary a, Integral a, MaybeBounded a,
 TypeSpec a ~ NumSpec a, Foldy a, Random a) =>
Specification a -> Specification a -> GenT m [a]
genNumList Specification a
elemSIn Specification a
foldSIn = do
  let extraElemConstraints :: Specification a
extraElemConstraints
        | Just a
l <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemSIn
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
l
        , Just a
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldSIn =
            forall a. OrdLike a => a -> Specification a
leqSpec a
u
        | Bool
otherwise = forall a. Specification a
TrueSpec
      elemSIn' :: Specification a
elemSIn' = Specification a
elemSIn forall a. Semigroup a => a -> a -> a
<> Specification a
extraElemConstraints
  Specification a
normElemS <- forall {a} {m :: * -> *}.
(TypeSpec a ~ NumSpec a, HasSpec a, MaybeBounded a, Num a,
 MonadGenError m, Ord a) =>
Specification a -> GenT m (Specification a)
normalize Specification a
elemSIn'
  Specification a
normFoldS <- forall {a} {m :: * -> *}.
(TypeSpec a ~ NumSpec a, HasSpec a, MaybeBounded a, Num a,
 MonadGenError m, Ord a) =>
Specification a -> GenT m (Specification a)
normalize Specification a
foldSIn
  let narrowedSpecs :: (Specification a, Specification a)
narrowedSpecs = forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a
normElemS, Specification a
normFoldS)
  forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
    ( forall a. [a] -> NonEmpty a
NE.fromList
        [ String
"Can't generate list of ints with fold constraint"
        , String
"  elemSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemSIn
        , String
"  normElemSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
normElemS
        , String
"  foldSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldSIn
        ]
    )
    forall a b. (a -> b) -> a -> b
$ forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
narrowedSpecs Int
50 [] forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Gen [a]
shuffle
  where
    normalize :: Specification a -> GenT m (Specification a)
normalize (ExplainSpec [String]
es Specification a
x) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> GenT m (Specification a)
normalize Specification a
x
    normalize spec :: Specification a
spec@SuspendedSpec {} = do
      Int
sz <- forall (m :: * -> *). Monad m => GenT m Int
sizeT
      Specification a
spec' <- forall {t} {m :: * -> *} {a}.
(Num t, MonadGenError m, HasSpec a, Ord a, Eq t) =>
Int -> t -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec Int
sz (Int
100 :: Int) forall a. Monoid a => a
mempty Specification a
spec
      Specification a -> GenT m (Specification a)
normalize forall a b. (a -> b) -> a -> b
$ Specification a
spec'
    normalize Specification a
spec =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. OrdLike a => a -> Specification a
geqSpec forall a. MaybeBounded a => Maybe a
lowerBound
          forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. OrdLike a => a -> Specification a
leqSpec forall a. MaybeBounded a => Maybe a
upperBound
          forall a. Semigroup a => a -> a -> a
<> Specification a
spec

    buildMemberSpec :: Int -> t -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec Int
_ t
0 Set a
es Specification a
_ =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
            (forall a. Set a -> [a]
Set.toList Set a
es)
            (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"In genNumList, in buildMemberSpec 'es' is the empty list, can't make a MemberSpec from that")
        )
    buildMemberSpec Int
sz t
fuel Set a
es Specification a
spec = do
      Maybe a
me <- forall (m :: * -> *) a. (Int -> Int) -> GenT m a -> GenT m a
scaleT (forall a b. a -> b -> a
const Int
sz) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadGenError m =>
GenT GE a -> GenT m (Maybe a)
tryGenT (forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
spec)
      let sz' :: Int
sz'
            | Int
sz forall a. Ord a => a -> a -> Bool
> Int
100 = Int
sz
            | forall a. Maybe a -> Bool
isNothing Maybe a
me = Int
2 forall a. Num a => a -> a -> a
* Int
sz forall a. Num a => a -> a -> a
+ Int
1
            | Just a
e <- Maybe a
me, forall a. Ord a => a -> Set a -> Bool
Set.member a
e Set a
es = Int
2 forall a. Num a => a -> a -> a
* Int
sz forall a. Num a => a -> a -> a
+ Int
1
            | Bool
otherwise = Int
sz
      Int -> t -> Set a -> Specification a -> GenT m (Specification a)
buildMemberSpec
        Int
sz'
        (t
fuel forall a. Num a => a -> a -> a
- t
1)
        (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
es (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Set a -> Set a
Set.insert Set a
es) Maybe a
me)
        Specification a
spec

    gen ::
      forall m'. MonadGenError m' => (Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
    gen :: forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a
elemS, Specification a
foldS) Int
fuel [a]
lst
      | Int
fuel forall a. Ord a => a -> a -> Bool
<= Int
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
          forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genError forall a b. (a -> b) -> a -> b
$
            forall a. [a] -> NonEmpty a
NE.fromList
              [ String
"Ran out of fuel in genNumList"
              , String
"  elemSpec =" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemSIn
              , String
"  foldSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldSIn
              , String
"  lst = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse [a]
lst)
              ]
      | ErrorSpec NonEmpty String
err <- Specification a
foldS = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
genError NonEmpty String
err
      | ErrorSpec {} <- Specification a
elemS = forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst -- At this point we know that foldS admits 0 (also this should be redundant)
      | a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS = forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
[GenT GE a] -> GenT m a
oneofT [forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
lst, forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList @GE] -- TODO: distribution
      | Bool
otherwise = forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList
      where
        isUnsat :: (Specification a, Specification a) -> Bool
isUnsat (Specification a
elemSpec, Specification a
foldSpec) = forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
foldSpec Bool -> Bool -> Bool
|| Bool -> Bool
not (a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldSpec) Bool -> Bool -> Bool
&& forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
elemSpec
        nonemptyList :: forall m''. MonadGenError m'' => GenT m'' [a]
        nonemptyList :: forall (m'' :: * -> *). MonadGenError m'' => GenT m'' [a]
nonemptyList = do
          (a
x, (Specification a, Specification a)
specs') <-
            forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explain
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  [ String
"Generating an element:"
                  , String
"  elemS = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
elemS
                  , String
"  foldS = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification a
foldS
                  , String
"  fuel  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
fuel
                  , String
"  lst   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse [a]
lst)
                  ]
              )
              forall a b. (a -> b) -> a -> b
$ do
                Int
sz <- forall (m :: * -> *). Monad m => GenT m Int
sizeT
                a
x <- forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
elemS
                let foldS' :: Specification a
foldS' = forall (s :: Symbol) (t :: Symbol -> [*] -> * -> *) (dom :: [*])
       rng hole.
Logic s t dom rng =>
Context s t dom rng hole -> Specification rng -> Specification hole
propagate (forall (dom :: [*]) rng (t :: Symbol -> [*] -> * -> *)
       (s :: Symbol) hole y.
(All HasSpec dom, HasSpec rng) =>
t s dom rng -> CList 'Pre dom hole y -> Context s t dom rng hole
Context forall a. Foldy a => IntW "addFn" '[a, a] a
theAddFn (forall hole. HasSpec hole => Ctx hole hole
HOLE forall y hole (as1 :: [*]).
HasSpec y =>
Ctx hole y
-> (forall i j. CList 'Post as1 i j) -> CList 'Pre (y : as1) hole y
:<> a
x forall a (as1 :: [*]) hole y.
Literal a =>
a -> CList 'Post as1 hole y -> CList 'Post (a : as1) hole y
:<| forall hole y. CList 'Post '[] hole y
End)) Specification a
foldS
                    specs' :: (Specification a, Specification a)
specs' = forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
a
-> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
narrowByFuelAndSize (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int
fuel forall a. Num a => a -> a -> a
- Int
1) Int
sz (Specification a
elemS, Specification a
foldS')
                forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, (Specification a, Specification a)
specs')
                forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
GenT m a -> (a -> Bool) -> GenT m a
`suchThatT` Bool -> Bool
not
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a}.
(TypeSpec a ~ NumSpec a, TypeSpec a ~ NumSpec a, HasSpec a, Ord a,
 Ord a, Enum a, Enum a, Num a, Num a, MaybeBounded a,
 MaybeBounded a) =>
(Specification a, Specification a) -> Bool
isUnsat
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
          forall (m' :: * -> *).
MonadGenError m' =>
(Specification a, Specification a) -> Int -> [a] -> GenT m' [a]
gen (Specification a, Specification a)
specs' (Int
fuel forall a. Num a => a -> a -> a
- Int
1) (a
x forall a. a -> [a] -> [a]
: [a]
lst)

narrowByFuelAndSize ::
  forall a.
  ( TypeSpec a ~ NumSpec a
  , HasSpec a
  , Arbitrary a
  , Integral a
  , Random a
  , MaybeBounded a
  ) =>
  -- | Fuel
  a ->
  -- | Integer
  Int ->
  (Specification a, Specification a) ->
  (Specification a, Specification a)
narrowByFuelAndSize :: forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
a
-> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
narrowByFuelAndSize a
fuel Int
size (Specification a, Specification a)
specpair =
  Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop (Int
100 :: Int) ((Specification a, Specification a)
-> (Specification a, Specification a)
onlyOnceTransformations forall a b. (a -> b) -> a -> b
$ forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specpair)
  where
    loop :: Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop Int
0 (Specification a, Specification a)
specs =
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        [String] -> String
unlines
          [ String
"narrowByFuelAndSize loops:"
          , String
"  fuel = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
fuel
          , String
"  size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
          , String
"  specs = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Specification a, Specification a)
specs
          , String
"  narrowFoldSpecs spec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs)
          , String
"  go (narrowFoldSpecs specs) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ((Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs))
          ]
    loop Int
n (Specification a, Specification a)
specs = case (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (Specification a, Specification a)
specs of
      Maybe (Specification a, Specification a)
Nothing -> (Specification a, Specification a)
specs
      Just (Specification a, Specification a)
specs' -> Int
-> (Specification a, Specification a)
-> (Specification a, Specification a)
loop (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs')

    -- Transformations only applied once. It's annoying to check if you're
    -- going to change the spec with these so easier to just make sure you only apply
    -- these once
    onlyOnceTransformations :: (Specification a, Specification a)
-> (Specification a, Specification a)
onlyOnceTransformations (Specification a
elemS, Specification a
foldS)
      | a
fuel forall a. Eq a => a -> a -> Bool
== a
1 = (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> Specification a
foldS, Specification a
foldS)
      | Bool
otherwise = (Specification a
elemS, Specification a
foldS)

    canReach :: t -> t -> t -> Bool
canReach t
_ t
0 t
s = t
s forall a. Eq a => a -> a -> Bool
== t
0
    canReach t
e t
currentfuel t
s
      -- You can reach it in one step
      | t
s forall a. Ord a => a -> a -> Bool
<= t
e = t
0 forall a. Ord a => a -> a -> Bool
< t
currentfuel
      | Bool
otherwise = t -> t -> t -> Bool
canReach t
e (t
currentfuel forall a. Num a => a -> a -> a
- t
1) (t
s forall a. Num a => a -> a -> a
- t
e)

    -- Precondition:
    --   a is negative
    --   the type has more negative numbers than positive ones
    safeNegate :: a -> a
safeNegate a
a
      | Just a
u <- forall a. MaybeBounded a => Maybe a
upperBound
      , a
a forall a. Ord a => a -> a -> Bool
< forall a. Num a => a -> a
negate a
u =
          a
u
      | Bool
otherwise = forall a. Num a => a -> a
negate a
a

    divCeil :: a -> a -> a
divCeil a
a a
b
      | a
b forall a. Num a => a -> a -> a
* a
d forall a. Ord a => a -> a -> Bool
< a
a = a
d forall a. Num a => a -> a -> a
+ a
1
      | Bool
otherwise = a
d
      where
        d :: a
d = a
a forall a. Integral a => a -> a -> a
`div` a
b

    go :: (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification a
elemS, forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification a
foldS)
      -- There is nothing we can do
      | a
fuel forall a. Eq a => a -> a -> Bool
== a
0 = forall a. Maybe a
Nothing
      | ErrorSpec {} <- Specification a
elemS = forall a. Maybe a
Nothing
      | ErrorSpec {} <- Specification a
foldS = forall a. Maybe a
Nothing
      -- Give up as early as possible
      | Just a
0 <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , Just a
0 <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS =
          forall a. a -> Maybe a
Just (forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"only 0 left"]), Specification a
foldS)
      -- Make sure we try to generate the smallest possible list
      -- that gives you the right result - don't put a bunch of zeroes in
      -- a _small_ (size 0) list.
      | Int
size forall a. Eq a => a -> a -> Bool
== Int
0
      , a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
elemS =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => a -> Specification a
notEqualSpec a
0, Specification a
foldS)
      -- Member specs with non-zero elements, TODO: explain
      | MemberSpec NonEmpty a
ys <- Specification a
elemS
      , let xs :: [a]
xs = forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys
      , Just a
u <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
0 forall a. Ord a => a -> a -> Bool
<=) [a]
xs
      , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a
0 forall a. Ord a => a -> a -> Bool
<) [a]
xs
      , let xMinP :: a
xMinP = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (a
0 forall a. Ord a => a -> a -> Bool
<) [a]
xs
            possible :: a -> Bool
possible a
x = a
x forall a. Eq a => a -> a -> Bool
== a
u Bool -> Bool -> Bool
|| a
xMinP forall a. Ord a => a -> a -> Bool
<= a
u forall a. Num a => a -> a -> a
- a
x
            xs' :: [a]
xs' = forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
possible [a]
xs
      , [a]
xs' forall a. Eq a => a -> a -> Bool
/= [a]
xs =
          forall a. a -> Maybe a
Just (forall a. [a] -> NonEmpty String -> Specification a
memberSpecList (forall a. Ord a => [a] -> [a]
nubOrd [a]
xs') (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"None of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
xs forall a. [a] -> [a] -> [a]
++ String
" are possible")), Specification a
foldS)
      -- The lower bound on the number of elements is too low
      | Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
> a
0
      , Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
> a
0
      , let c :: a
c = forall a. Integral a => a -> a -> a
divCeil a
s a
fuel
      , a
e forall a. Ord a => a -> a -> Bool
< a
c =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec a
c, Specification a
foldS)
      -- The upper bound on the number of elements is too high
      | Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
< a
0
      , Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
< a
0
      , let c :: a
c = forall a. Integral a => a -> a -> a
divCeil (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s) a
fuel
      , forall a. Num a => a -> a
negate a
c forall a. Ord a => a -> a -> Bool
< a
e
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
c forall a. Ord a => a -> a -> Bool
<) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
leqSpec a
c, Specification a
foldS)
      -- It's time to stop generating negative numbers
      | Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
> a
0
      , Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
> a
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach a
e (a
fuel forall a. Integral a => a -> a -> a
`div` a
2 forall a. Num a => a -> a -> a
+ a
1) a
s
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Ord a => a -> a -> Bool
<= a
0) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec a
0, Specification a
foldS)
      -- It's time to stop generating positive numbers
      | Just a
s <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
      , a
s forall a. Ord a => a -> a -> Bool
< a
0
      , Just a
e <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
      , a
e forall a. Ord a => a -> a -> Bool
< a
0
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {t} {t}. (Num t, Num t, Ord t, Ord t) => t -> t -> t -> Bool
canReach (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
e) (a
fuel forall a. Integral a => a -> a -> a
`div` a
2 forall a. Num a => a -> a -> a
+ a
1) (forall {a}. (MaybeBounded a, Ord a, Num a) => a -> a
safeNegate a
s)
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (a
0 forall a. Ord a => a -> a -> Bool
<=) (forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) =
          forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
ltSpec a
0, Specification a
foldS)
      -- There is nothing we need to do
      | Bool
otherwise = forall a. Maybe a
Nothing

narrowFoldSpecs ::
  forall a.
  ( TypeSpec a ~ NumSpec a
  , HasSpec a
  , Arbitrary a
  , Integral a
  , Random a
  , MaybeBounded a
  ) =>
  (Specification a, Specification a) ->
  (Specification a, Specification a)
narrowFoldSpecs :: forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (Specification a, Specification a)
specs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Specification a, Specification a)
specs forall a.
(TypeSpec a ~ NumSpec a, HasSpec a, Arbitrary a, Integral a,
 Random a, MaybeBounded a) =>
(Specification a, Specification a)
-> (Specification a, Specification a)
narrowFoldSpecs (forall {a}.
(TypeSpec a ~ NumSpec a, HasSpec a, Ord a, Enum a, Num a,
 MaybeBounded a) =>
(Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (Specification a, Specification a)
specs)
  where
    -- Note: make sure there is some progress when returning Just or this will loop forever
    go :: (Specification a, Specification a)
-> Maybe (Specification a, Specification a)
go (forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification a
elemS, forall a. HasSpec a => Specification a -> Specification a
simplifySpec -> Specification a
foldS) = case (Specification a
elemS, Specification a
foldS) of
      -- Empty foldSpec
      (Specification a
_, ErrorSpec {}) -> forall a. Maybe a
Nothing
      (Specification a, Specification a)
_ | forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Bool
isEmptyNumSpec Specification a
foldS -> forall a. a -> Maybe a
Just (Specification a
elemS, forall a. NonEmpty String -> Specification a
ErrorSpec (forall a. [a] -> NonEmpty a
NE.fromList [String
"Empty foldSpec:", forall a. Show a => a -> String
show Specification a
foldS]))
      -- Empty elemSpec
      (ErrorSpec {}, MemberSpec NonEmpty a
ys) | forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys forall a. Eq a => a -> a -> Bool
== [a
0] -> forall a. Maybe a
Nothing
      (ErrorSpec {}, Specification a
_)
        | a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS -> forall a. a -> Maybe a
Just (Specification a
elemS, forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
0))
        | Bool
otherwise ->
            forall a. a -> Maybe a
Just
              ( Specification a
elemS
              , forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
                  forall a. [a] -> NonEmpty a
NE.fromList
                    [ String
"Empty elemSpec and non-zero foldSpec"
                    , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Int -> Doc ann -> Doc ann
indent Int
2 forall a b. (a -> b) -> a -> b
$ Doc Any
"elemSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
elemS
                    , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall ann. Int -> Doc ann -> Doc ann
indent Int
2 forall a b. (a -> b) -> a -> b
$ Doc Any
"foldSpec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification a
foldS
                    ]
              )
      -- We can reduce the size of the `elemS` interval when it is
      -- `[l, u]` or `[l, ∞)` given that `0 <= l` and we have
      -- an upper bound on the sum - we can't pick things bigger than the
      -- upper bound.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
lo
        , Just a
hi <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
        , -- Check that we will actually be making the set smaller
          forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
hi forall a. Ord a => a -> a -> Bool
<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS) ->
            forall a. a -> Maybe a
Just (Specification a
elemS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
lo) (forall a. a -> Maybe a
Just a
hi)), Specification a
foldS)
      -- We can reduce the size of the foldS set by bumping the lower bound when
      -- there is a positive lower bound on the elemS, we can't generate things smaller
      -- than the lower bound on `elemS`.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , a
0 forall a. Ord a => a -> a -> Bool
<= a
lo
        , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ a
0 forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
foldS
        , -- Check that we will actually be making the set smaller
          forall a. a -> Maybe a -> a
fromMaybe Bool
True ((a
lo forall a. Ord a => a -> a -> Bool
>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS) ->
            forall a. a -> Maybe a
Just (Specification a
elemS, Specification a
foldS forall a. Semigroup a => a -> a -> a
<> forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
lo) forall a. Maybe a
Nothing))
      -- NOTE: this is far from sufficient, but it's good enough of an approximation
      -- to avoid the worst failures.
      (Specification a, Specification a)
_
        | Just a
lo <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
elemS
        , Just a
loS <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownLowerBound Specification a
foldS
        , Just a
hi <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
elemS
        , Just a
hiS <- forall a.
(TypeSpec a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) =>
Specification a -> Maybe a
knownUpperBound Specification a
foldS
        , a
hi forall a. Ord a => a -> a -> Bool
< a
loS
        , a
lo forall a. Ord a => a -> a -> Bool
> a
hiS forall a. Num a => a -> a -> a
- a
lo ->
            forall a. a -> Maybe a
Just
              ( forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
              , forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$ forall a. [a] -> NonEmpty a
NE.fromList [String
"Can't solve diophantine equation"]
              )
      (Specification a, Specification a)
_ -> forall a. Maybe a
Nothing

-- =====================================================================================
-- Like genList, but generate a list whose size conforms to s SizeSpec
-- =====================================================================================

-- | Generate a list with 'sizeSpec' elements, that add up to a total that conforms
--   to 'foldSpec'. Every element in the list should conform to 'elemSpec'
genListWithSize ::
  forall a m.
  (Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a, Integral a) =>
  Specification Integer -> Specification a -> Specification a -> GenT m [a]
genListWithSize :: forall a (m :: * -> *).
(Foldy a, TypeSpec a ~ NumSpec a, MonadGenError m, Random a,
 Integral a) =>
Specification Integer
-> Specification a -> Specification a -> GenT m [a]
genListWithSize Specification Integer
sizeSpec Specification a
elemSpec Specification a
foldSpec
  | Specification Integer
TrueSpec <- Specification Integer
sizeSpec = forall a (m :: * -> *).
(Foldy a, MonadGenError m) =>
Specification a -> Specification a -> GenT m [a]
genList Specification a
elemSpec Specification a
foldSpec
  | ErrorSpec NonEmpty String
_ <- Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
geqSpec Integer
0 =
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"genListWithSize called with possible negative size"
            , String
"  sizeSpec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
            , String
"  elemSpec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
            , String
"  foldSpec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
foldSpec
            ]
        )
  | Bool
otherwise = do
      a
total <- forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
foldSpec
      -- The compatible sizes for the list, for a given choice of total
      let sizeAdjusted :: Specification Integer
sizeAdjusted =
            if a
total forall a. Eq a => a -> a -> Bool
/= a
0
              then Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec Integer
0 -- if total is not zero, we better not pick a 0 size
              else
                if forall a. Foldy a => Bool
noNegativeValues @a
                  then Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. a -> Specification a
equalSpec Integer
0 -- if it is zero, and negative numbers not allowed, then only possible size is 0
                  else Specification Integer
sizeSpec forall a. Semigroup a => a -> a -> a
<> forall a. OrdLike a => a -> Specification a
gtSpec Integer
0
          message :: [String]
message =
            [ String
"\nGenSizedList fails"
            , String
"sizespec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification Integer
sizeSpec
            , String
"elemSpec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
elemSpec
            , String
"foldSpec = " forall a. [a] -> [a] -> [a]
++ forall a. HasSpec a => Specification a -> String
specName Specification a
foldSpec
            , String
"total choosen from foldSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
total
            , String
"size adjusted for total = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification Integer
sizeAdjusted
            ]
      forall (m :: * -> *) a. MonadGenError m => [String] -> m a -> m a
push [String]
message forall a b. (a -> b) -> a -> b
$ do
        Integer
count <- forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification Integer
sizeAdjusted
        case forall a. Ord a => a -> a -> Ordering
compare a
total a
0 of
          Ordering
EQ ->
            if Integer
count forall a. Eq a => a -> a -> Bool
== Integer
0
              then forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              else forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Foldy t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification a
elemSpec a
total Integer
count
          Ordering
GT -> forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Foldy t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification a
elemSpec a
total Integer
count
          Ordering
LT -> forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 HasSpec t) =>
Specification t -> t -> Integer -> GenT m [t]
pickNegative Specification a
elemSpec a
total Integer
count

pickPositive ::
  forall t m.
  (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, Foldy t) =>
  Specification t -> t -> Integer -> GenT m [t]
pickPositive :: forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 Foldy t) =>
Specification t -> t -> Integer -> GenT m [t]
pickPositive Specification t
elemspec t
total Integer
count = do
  (Cost, Solution t)
sol <-
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$
      forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
        (forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec t
0 Specification t
elemspec) -- Search from [0..total] unless elemspec says otherwise
        (forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec t
total Specification t
elemspec)
        (forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
        t
total
        (forall a. Num a => Integer -> a
fromInteger Integer
count)
        (Int -> Cost
Cost Int
0)
  case forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
    No [String]
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall a. [a] -> NonEmpty a
NE.fromList [String]
msgs)
    Yes ([t]
x :| [[t]]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [t]
x

pickNegative ::
  forall t m.
  (Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t, HasSpec t) =>
  Specification t -> t -> Integer -> GenT m [t]

-- | total can be either negative, or 0. If it is 0, we want count numbers that add to zero
pickNegative :: forall t (m :: * -> *).
(Integral t, Random t, MonadGenError m, TypeSpec t ~ NumSpec t,
 HasSpec t) =>
Specification t -> t -> Integer -> GenT m [t]
pickNegative Specification t
elemspec t
total Integer
count = do
  (Cost, Solution t)
sol <-
    forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall a b. (a -> b) -> a -> b
$
      forall t.
(Show t, Integral t, Random t) =>
t
-> t
-> (String, t -> Bool)
-> t
-> Int
-> Cost
-> Gen (Cost, Solution t)
pickAll
        -- Recall 'total' is negative here.
        -- Here is a graphic of the range we search in (smallest .. largest)
        -- [(total+n) .. total .. 0 .. (0-n)],  where n = (total `div` 4) which is negative.
        (forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec (t
total forall a. Num a => a -> a -> a
+ (t
total forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
        (forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec (t
0 forall a. Num a => a -> a -> a
- (t
total forall a. Integral a => a -> a -> a
`div` t
4)) Specification t
elemspec)
        (forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification t
elemspec)
        t
total
        (forall a. Num a => Integer -> a
fromInteger Integer
count)
        (Int -> Cost
Cost Int
0)
  case forall a b. (a, b) -> b
snd (Cost, Solution t)
sol of
    No [String]
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalError (forall a. [a] -> NonEmpty a
NE.fromList [String]
msgs)
    Yes ([t]
x :| [[t]]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [t]
x

specName :: forall a. HasSpec a => Specification a -> String
specName :: forall a. HasSpec a => Specification a -> String
specName (ExplainSpec [String
x] Specification a
_) = String
x
specName Specification a
x = forall a. Show a => a -> String
show Specification a
x

predSpecPair :: forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair :: forall a. HasSpec a => Specification a -> (String, a -> Bool)
predSpecPair Specification a
spec = (forall a. HasSpec a => Specification a -> String
specName Specification a
spec, (forall a. HasSpec a => a -> Specification a -> Bool
`conformsToSpec` Specification a
spec))

-- | The smallest number admitted by the spec, if we can find one.
--   if not return the defaultValue 'dv'
minFromSpec ::
  forall n.
  (Ord n, TypeSpec n ~ NumSpec n) =>
  n -> Specification n -> n
minFromSpec :: forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec n
dv (ExplainSpec [String]
_ Specification n
spec) = forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv Specification n
spec
minFromSpec n
dv Specification n
TrueSpec = n
dv
minFromSpec n
dv s :: Specification n
s@(SuspendedSpec Var n
_ Pred
_) =
  case forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification n
s of
    SuspendedSpec {} -> n
dv
    Specification n
x -> forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
minFromSpec @n n
dv Specification n
x
minFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
minFromSpec n
_ (MemberSpec NonEmpty n
xs) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum NonEmpty n
xs
minFromSpec n
dv (TypeSpec (NumSpecInterval Maybe n
lo Maybe n
_) [n]
_) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv forall a. a -> a
id Maybe n
lo

-- | The largest number admitted by the spec, if we can find one.
--   if not return the defaultValue 'dv'
maxFromSpec ::
  forall n.
  (Ord n, TypeSpec n ~ NumSpec n) =>
  n -> Specification n -> n
maxFromSpec :: forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec n
dv (ExplainSpec [String]
_ Specification n
spec) = forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv Specification n
spec
maxFromSpec n
dv Specification n
TrueSpec = n
dv
maxFromSpec n
dv s :: Specification n
s@(SuspendedSpec Var n
_ Pred
_) =
  case forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification n
s of
    SuspendedSpec {} -> n
dv
    Specification n
x -> forall n.
(Ord n, TypeSpec n ~ NumSpec n) =>
n -> Specification n -> n
maxFromSpec @n n
dv Specification n
x
maxFromSpec n
dv (ErrorSpec NonEmpty String
_) = n
dv
maxFromSpec n
_ (MemberSpec NonEmpty n
xs) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum NonEmpty n
xs
maxFromSpec n
dv (TypeSpec (NumSpecInterval Maybe n
_ Maybe n
hi) [n]
_) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
dv forall a. a -> a
id Maybe n
hi