{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.CheatSheet where

import Data.Set (Set)
import Data.Set qualified as Set
import GHC.Generics
import Test.QuickCheck (Property, label)

import Constrained

-- The `constrained-generators` library allows us to write
-- constraints that give us random generators, shrinkers, and checkers
-- for data using a small embedded DSL, which defines a limited first order logic.
--
-- Every first order logic has 4 parts, as does our DSL.
-- 1) Terms :  e.g. x, 5, (member_ x set) (x ==. y)
--    Implemented as (Term fn a). We have variables like 'x', and constants like '5'.
--    'member_' and '==.' are function symbols, and build Terms from other terms.
--    By convention, a name followed by '_' or an infix operator followed by '.' are function symbols.
-- 2) Predicates (over terms). Predicates commonly used are
--        TruePred,
--        FalsePred (pure "explain"),
--        assert $ termWithTypeBool,
--    Some more unusual predicates are described below.
--    Implemented as type (Pred fn)
-- 3) Combinators (combining predicates). In general, And, Or, Not, Implies, True, False
--    But in the DSL, we are limited to
--      'And' using Block :: [Pred] -> Pred
--      'Not' using the function symbol not_ :: Term fn Bool -> Term fn Bool
--            for example:  assert $ not_ (x ==. y)
--      limited form of 'Or' using
--         chooseSpec :: (Int, Specification fn a)- > (Int, Specification fn a) -> Specification fn a
-- 4) Quantifiers (applying constraints to many things) :
--    forAll: Term fn t -> (Term fn a -> p) -> Pred fn
--    exists: ((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
--    These are explained in detail below

-- In case you are interested, here is a list of supported function symbols (note the use of the '_' and '.' convention)
-- disjoint_,  dom_,  elem_,  length_,  member_,  not_,  rng_,  singleton_,  sizeOf_,  subset_,  sum_,  (/=.),
-- (<.),  (<=.),  (==.),  (>.),  (>=.), fromList_, null_, union_
-- You may also use the methods of Num (+) (-) (*), since there is a (Num (Term fn)) instance.

-- The first order logic DSL is used to build Specifications
-- A specifcation with type (Specification fn x) has two uses
-- 1) To generate a random values of type 'x', subject to the constraints in the specifications definition.
--    This is implemented by   genFromSpec :: Specification fn x -> Gen x (Gen is the QuickCheck Gen)
-- 2) To test if a value of type 'x' meets all of the constraints given in the specifications definition.
--     This is implemented by  conformsToSpec :: HasSpec fn a => a -> Specification fn a -> Bool

-- Lets get started. We can talk about numbers:

specInt :: Specification BaseFn Int
specInt :: Specification BaseFn Int
specInt = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn Int
i ->
  [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term BaseFn Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term BaseFn Int
i
  ]

-- What's going on here? In short:
--    `constrained :: (HasSpec fn a, IsPred p fn) => (Term fn a -> p) -> Specification fn a`
--    Introduces the variable `i` over which we can write constraints of type `p` over something
--    of type `a` to produce a `Specifcation fn a` using a list of
--    `assert :: Term fn Bool -> Pred fn` with `Term fn`-level versions (function symbols) of familiar functions like
--    `(<.) :: OrdLike fn a => Term fn a -> Term fn a -> Term fn Bool`, `null_ :: Term fn [a] -> Term fn Bool`,
--    `rng_ :: (HasSpec fn k, HasSpec fn v, Ord k) => Term fn (Map k v) -> Term fn (Set k)` etc.
-- We get a generator from `genFromSpec :: Specification BaseFn a -> Gen a`:
-- λ> sample $ genFromSpec specInt
-- 1
-- 5
-- 6
-- 6
-- 8
-- 5
-- 3
-- 1
-- 1
-- 4
-- 8

-- Likewise, `shrinkWithSpec :: Specification BaseFn a -> a -> [a]` gives us
-- a shrinker:
-- λ> shrinkWithSpec specInt 10
-- [5,8,9]
-- λ> shrinkWithSpec specInt 5
-- [3,4]
-- λ> shrinkWithSpec specInt 3
-- [2]
-- λ> shrinkWithSpec specInt 1
-- []

-- And, `conformsToSpec :: a -> Specification BaseFn a -> Bool` gives us a checker:
-- λ> 10 `conformsToSpec` specInt
-- False
-- λ> 5 `conformsToSpec` specInt
-- True

-- Note that the type of `constrained` says the binding function of type `Term fn a -> p` doesn't
-- have to produce a `Pred fn` (which is the return type of `assert`), but can produce something of type `p`
-- that satisfies `IsPred p fn`. This basically just means something that can be readily turned into a
-- `Pred fn`, like e.g. `Pred fn`, `Bool`, `Term fn Bool`, `[p]` for `IsPred p fn`. Consequently, we could
-- have written `specInt` as:

specInt' :: Specification BaseFn Int
specInt' :: Specification BaseFn Int
specInt' = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn Int
i ->
  [ Term BaseFn Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term BaseFn Int
i
  ]

-- However, beware that when we start mixing `Term fn Bool` and `Pred fn` in these lists we can end
-- up getting some inscrutable error messages. So, if a call to `constrained` or another function that
-- has `IsPred` as a constraint, starts giving you strange error messages, double check that you have
-- used `assert` instead of raw `Term fn Bool` everywhere relevant.

-- We also have support for product types with functions like `fst_`, `snd_`, and `pair_`:

specProd :: Specification BaseFn (Int, Int)
specProd :: Specification BaseFn (Int, Int)
specProd = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Int, Int)
p ->
  [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term BaseFn (Int, Int)
p forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term BaseFn (Int, Int)
p forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
100
  ]

-- However, product types can also be a bit finicky:

specProd0 :: Specification BaseFn (Int, Int)
specProd0 :: Specification BaseFn (Int, Int)
specProd0 = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Int, Int)
p -> forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term BaseFn (Int, Int)
p forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term BaseFn (Int, Int)
p

-- λ> sample $ genFromSpec specProd0

-- *** Exception: Simplifying:

--   constrained $ \ v0 -> assert $ Less (Fst (ToGeneric v0)) (Snd (ToGeneric v0))
-- optimisePred => assert $ Less (Fst (ToGeneric v0)) (Snd (ToGeneric v0))
-- assert $ Less (Fst (ToGeneric v0)) (Snd (ToGeneric v0))
-- Can't build a single-hole context for variable v0 in term Less (Fst (ToGeneric v0)) (Snd (ToGeneric v0))

-- This gives us the _fundamental restriction_:
--   A variable can not appear twice in the same constraint

-- The fundamental restriction is very important to make the system compositional
-- and modular. We will get back to talking about it in detail when we discuss how to
-- extend the system. However, for now suffice to say that it's a lot easier to solve
-- constraints that look like `2 * x <. 10` than it is to solve constraints
-- like `x <. 10 - x` (i.e. ones that mention the same variable more than once).

-- To overcome the fundamental restriction we can use `match`:
-- match ::
--   forall fn p a.
--   ( HasSpec fn a
--   , IsProductType fn a
--   , IsPred p fn
--   ) =>
--   Term fn a ->
--   FunTy (MapList (Term fn) (ProductAsList a)) p ->
--   Pred fn

specProd1 :: Specification BaseFn (Int, Int)
specProd1 :: Specification BaseFn (Int, Int)
specProd1 = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Int, Int)
p ->
  forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term BaseFn (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y ->
    Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y

-- λ> sample $ genFromSpec specProd1
-- (-1,0)
-- (-4,-2)
-- (1,2)
-- (-2,1)
-- (7,8)
-- (-9,-4)
-- (-3,3)
-- (-1,12)
-- (-7,-6)
-- (-11,17)
-- (-53,-14)

-- Bringing variables into scope.
-- 'constrained' and 'match' are the ways we bring variable into scope, And they are often nested.
-- Consider writing a specification for pair of nested pairs: Specification fn ((Int,Int),(Int,Int))
-- How do we name the four different Int's ?

nested :: Specification BaseFn ((Int, Int), (Int, Int))
nested :: Specification BaseFn ((Int, Int), (Int, Int))
nested =
  forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn ((Int, Int), (Int, Int))
pp ->
    forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term BaseFn ((Int, Int), (Int, Int))
pp forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p1 Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p2 ->
      forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p1 forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x1 Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y1 ->
        forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p2 forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x2 Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y2 ->
          [Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x1 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y1, Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y1 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x2, Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x2 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y2]

-- ghci> sample $ genFromSpec nested
-- ((0,0),(0,0))
-- ((-9,-5),(-1,0))
-- ((-12,-10),(-5,-2))
-- ((-8,-4),(-3,-2))
-- ((-33,-18),(-15,-6))
-- ((-21,-12),(-1,3))
-- ((-36,-12),(1,9))
-- ((-64,-37),(-30,-4))
-- ((-53,-37),(-33,-10))
-- ((-49,-15),(-6,8))
-- ((-72,-34),(-26,-19))

-- A good rule of thumb when starting a new specification is to think about how you would
-- use 'constrained' and 'match' to bring variables, naming each of the parts that you want
-- to constrain, into scope.

-- Let's look under the hood of `match`, it introduces two auxilliary variables `v0` and `v1`
-- that circumvents the fundamental restriction by allowing us to generate values for `v1` and
-- `v0` before we generate a value for `v3`.

-- λ> simplifySpec specProd1
-- constrained $ \ v3 ->
--   let v1 = Fst (ToGeneric v3) in
--   let v0 = Snd (ToGeneric v3) in
--   assert $ Less v1 v0

-- This pattern of `constrained $ \ p -> match p $ \ x y -> ...` is very common
-- and has a shorthand in the form of `constrained'`:

specProd2 :: Specification BaseFn (Int, Int)
specProd2 :: Specification BaseFn (Int, Int)
specProd2 = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y

-- How does generation actually work when we have multiple variables? For example,
-- it is not obvious (to the computer) what the best way of generating values satisfying
-- this constraint is:

solverOrder :: Specification BaseFn (Int, Int)
solverOrder :: Specification BaseFn (Int, Int)
solverOrder = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y ->
  [ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  ]

-- For example, if you tried generating a value for `x` first chances are you'd generate
-- something larger than 10, which would make it impossible to generate a valid `y`. However,
-- when we run it we get reasonable values out:

-- sample $ genFromSpec solverOrder
-- (-1,0)
-- (0,2)
-- (-4,4)
-- (-7,-3)
-- (-7,3)
-- (-11,-3)
-- (4,8)
-- (-15,-14)
-- (-25,-10)
-- (-23,-6)
-- (-51,-20)

-- But how does the system know to generate `y` first? Unfortunately, there is nothing smart about
-- it. The system simply solves things "right to left" - variables that appear to the right in assertions
-- are solved before variables to the left. If one wants to understand the consequences of this and how it
-- affects the generator the `printPlan` function comes in handy:

-- λ> printPlan solverOrder
-- Simplified spec:
--   constrained $ \ v_3 ->
--     let v_1 = Fst (ToGeneric v_3) in
--     let v_0 = Snd (ToGeneric v_3) in
--     {assert $ Less v_0 10
--      assert $ Less v_1 v_0}
-- SolverPlan
--   Dependencies:
--     v_0 <- []
--     v_1 <- [v_0]
--     v_3 <- [v_0, v_1]
--   Linearization:
--     v_0 <- TypeSpec [..9] []
--     v_1 <- assert $ Less v_1 v_0
--     v_3 <-
--       assert $ Equal (Fst (ToGeneric v_3)) v_1
--       assert $ Equal (Snd (ToGeneric v_3)) v_0

-- There are three parts to the output:
--  - The "Simplified spec" is the input specification after it has gone through a number of optimization
--    and simplification passes to make it amenable to solving.
--  - The "Dependencies" tells us what variables depend on what other variables to be solved. In this case `v0` (y)
--    has no dependencies, `v1` (x) is solved after `v0` and `v3` (the actual pair we are generating) is solved
--    last.
--  - Finaly, the "Linearization" tells us _what constraints define what varible_. This is an important aspect of the
--    system: variables are only constrained by assertions that talk about the variable itself and variables that
--    are solved before it. In this case `v0` (y) is defined by `y <. 10`, `v1` (x) by `x <. y` and `v3` by the equalities
--    in the `Let` constructs.
--
-- As the generator executes this plan it will pick the variables in the order in which they appear in the linearization
-- and generate the corresponding values. For example, an execution trace could go like the following pseudo-trace (the details of how
-- this works are slightly more involved but the basic order of operations is accurate):
--  v0 <- pick from (-∞, 10)
--  v0 = 4
--  v1 <- pick from [4/v0](-∞, v0)
--        -> pick from (-∞, 4)
--  v1 = 2
--  v3 <- pick from [4/v0, 2/v1]{fst == v1, snd == v0}
--        -> pick from {fst == 2, snd == 4}
--  v3 = (2, 4)

-- As an aside, the frustrating thing about making sense of the output of `printPlan` is the `v0`, `v1`, etc. naming.
-- To introduce proper names we can use the `var` quasi-quoter:

solverOrder' :: Specification BaseFn (Int, Int)
solverOrder' :: Specification BaseFn (Int, Int)
solverOrder' = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|x|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|y|] ->
  [ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  ]

-- Now we get more reasonable looking oputput from `printPlan`:
-- λ> printPlan solverOrder'
-- Simplified spec:
--   constrained $ \ v_3 ->
--     let x_1 = Fst (ToGeneric v_3) in
--     let y_0 = Snd (ToGeneric v_3) in
--     {assert $ Less y_0 10
--      assert $ Less x_1 y_0}
-- SolverPlan
--   Dependencies:
--     y_0 <- []
--     x_1 <- [y_0]
--     v_3 <- [y_0, x_1]
--   Linearization:
--     y_0 <- TypeSpec [..9] []
--     x_1 <- assert $ Less x_1 y_0
--     v_3 <-
--       assert $ Equal (Fst (ToGeneric v_3)) x_1
--       assert $ Equal (Snd (ToGeneric v_3)) y_0

-- A consequence of the default dependency order approach is that it's possible
-- to write constraints that put you in a tricky situation:

tightFit0 :: Specification BaseFn (Int, Int)
tightFit0 :: Specification BaseFn (Int, Int)
tightFit0 = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y ->
  [ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y
  ]

-- λ> sample $ genFromSpec tightFit0

-- *** Exception: genFromPreds:

--   let v_1 = Fst (ToGeneric v_3) in
--   let v_0 = Snd (ToGeneric v_3) in
--   {assert $ Less v_1 v_0
--    assert $ Less 0 v_1}
-- SolverPlan
--   Dependencies:
--     v_0 <- []
--     v_1 <- [v_0]
--     v_3 <- [v_0, v_1]
--   Linearization:
--     v_0 <-
--     v_1 <-
--       TypeSpec [1..] []
--       ---
--       assert $ Less v_1 v_0
--     v_3 <-
--       assert $ Equal (Fst (ToGeneric v_3)) v_1
--       assert $ Equal (Snd (ToGeneric v_3)) v_0
-- Stepping the plan:
--   SolverPlan
--     Dependencies:
--       v_1 <- []
--       v_3 <- [v_1]
--     Linearization:
--       v_1 <- ErrorSpec [1..-1]
--       v_3 <-
--         TypeSpec (Cartesian TrueSpec (MemberSpec [0])) []
--         ---
--         assert $ Equal (Fst (ToGeneric v_3)) v_1
--   Env {unEnv = fromList [(v_0,EnvValue 0)]}
-- genFromSpecT ErrorSpec{} with explanation:
-- [1..-1]

-- The generator fails with output similar to what we saw above and a message telling us we tried to generate
-- a value from the (empty) interval [1..-1]. Inspecting the output above carefully we see that the graph and the
-- linearization tell us that `v0` (y) is completely unconstrained. The consequence of this is that when we get to the
-- point of trying to generate `v1` (x) we've already picked a value (-1) for `v0` that makes it impossible to satisfy
-- the constraints on `v1` and its constraints have specialized away to an error spec.

-- The solution to this issue is to introduce `dependsOn`, which lets us override the dependency order in constraints:

tightFit1 :: Specification BaseFn (Int, Int)
tightFit1 :: Specification BaseFn (Int, Int)
tightFit1 = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y ->
  [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x
  , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x
  ]

-- λ> printPlan tightFit1
-- Simplified spec:
--   constrained $ \ v_3 ->
--     let v_1 = Fst (ToGeneric v_3) in
--     let v_0 = Snd (ToGeneric v_3) in
--     {v_0 <- v_1
--      assert $ Less v_1 v_0
--      assert $ Less 0 v_1}
-- SolverPlan
--   Dependencies:
--     v_0 <- [v_1]
--     v_1 <- []
--     v_3 <- [v_0, v_1]
--   Linearization:
--     v_1 <- TypeSpec [1..] []
--     v_0 <- assert $ Less v_1 v_0
--     v_3 <-
--       assert $ Equal (Fst (ToGeneric v_3)) v_1
--       assert $ Equal (Snd (ToGeneric v_3)) v_0

-- This gives us more balanced constraints that solve `v1` before they solve `v0`!
-- Consequently, this constraint generates reasonable values:

-- λ> sample $ genFromSpec tightFit1
-- (1,2)
-- (2,3)
-- (9,15)
-- (4,10)
-- (12,27)
-- (15,21)
-- (10,30)
-- (23,51)
-- (7,34)
-- (21,46)
-- (28,49)

-- We also support booleans with `ifElse :: Term fn Bool -> Pred fn -> Pred fn -> Pred fn`
-- where the branches of the `ifElse` depend on the scrutinee.

booleanExample :: Specification BaseFn (Int, Int)
booleanExample :: Specification BaseFn (Int, Int)
booleanExample = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y ->
  forall (fn :: Univ) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
    (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
x)
    (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10)
    (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
y forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
20)

-- sample $ genFromSpec booleanExample
-- (0,20)
-- (2,10)
-- (4,10)
-- (1,10)
-- (-2,20)
-- (3,10)
-- (7,10)
-- (-8,20)
-- (-5,20)
-- (-2,20)
-- (-19,20)

-- We can combine `ifElse` and `dependsOn` to write a nice example saying
-- that a PVP version pair `q` can follow a pair `p`.

-- Because we will need to re-use this multiple times we start by defining a valid
-- PVP constraint as any constraint that has non-negative major and minor version number.
validPVPVersion :: Specification BaseFn (Int, Int)
validPVPVersion :: Specification BaseFn (Int, Int)
validPVPVersion = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi -> [Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma, Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi]

-- Now we are ready to define the constraints for valid PVP succession. Note here that
-- we use the `satisfies :: Term fn a -> Specification BaseFn a -> Pred fn` combinator
-- to re-use the `validPVPVersion` constraint.

canFollowExample :: Specification BaseFn ((Int, Int), (Int, Int))
canFollowExample :: Specification BaseFn ((Int, Int), (Int, Int))
canFollowExample = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q ->
  [ forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi ->
      forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma' Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi' ->
        [ forall (fn :: Univ) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
            (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma' forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma)
            (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi' forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
1)
            (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
mi' forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0)
        , -- Note how these two constraints imply a cycle:
          --  ma' <- ma <- ma'
          forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma' forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma forall a. Num a => a -> a -> a
+ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
1
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma'
        , -- We break that cycle by specifying a concrete order
          -- Another option would be to define `>=.` but that doesn't
          -- exist right now and we will get to extending the language
          -- later on!
          Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma' forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
ma
        ]
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification BaseFn (Int, Int)
validPVPVersion
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification BaseFn (Int, Int)
validPVPVersion
  ]

-- λ> sample $ genFromSpec canFollowExample
-- ((0,0),(0,1))
-- ((1,0),(1,1))
-- ((4,2),(4,3))
-- ((12,1),(12,2))
-- ((11,16),(11,17))
-- ((20,7),(21,0))
-- ((18,12),(18,13))
-- ((6,18),(7,0))
-- ((29,24),(30,0))
-- ((23,21),(23,22))
-- ((26,14),(26,15))

-- We have native support for sum types using `caseOn` and `branch`:

sumExample :: Specification BaseFn (Either Int Bool)
sumExample :: Specification BaseFn (Either Int Bool)
sumExample = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Either Int Bool)
e ->
  (forall (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term BaseFn (Either Int Bool)
e)
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0)
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b -> forall (fn :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b)

-- Furthermore, cases are solved _inside-out_ by default:

sumExampleTwo :: Specification BaseFn (Int, Either Int Bool)
sumExampleTwo :: Specification BaseFn (Int, Either Int Bool)
sumExampleTwo = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Either Int Bool)
e ->
  [ forall (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
      Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Either Int Bool)
e
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
j -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
j)
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b -> forall (fn :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b)
  , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
20 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i
  ]

-- We can work with sets with operations like `subset_`, `union_` (or `<>`), `disjoint_`, and `singleton_`:

setExample :: Specification BaseFn (Set Int, Set Int, Set Int)
setExample :: Specification BaseFn (Set Int, Set Int, Set Int)
setExample = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs ->
  [ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` (Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys forall a. Semigroup a => a -> a -> a
<> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs)
  , forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Integer
10
  ]

-- We can also quantify over things like sets with `forAll`:

forAllFollow0 :: Specification BaseFn ((Int, Int), Set (Int, Int))
forAllFollow0 :: Specification BaseFn ((Int, Int), Set (Int, Int))
forAllFollow0 = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set (Int, Int))
qs ->
  [ forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set (Int, Int))
qs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q -> forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification BaseFn ((Int, Int), (Int, Int))
canFollowExample
  ]

-- λ> sample $ genFromSpec forAllFollow0
-- ((0,0),fromList [])
-- ((1,-1),fromList [])
-- ((2,3),fromList [(2,4),(3,0)])
-- ((4,2),fromList [(4,3),(5,0)])
-- ((-2,6),fromList [])
-- ((10,-9),fromList [])
-- ((-1,-8),fromList [])
-- ((-8,-1),fromList [])
-- ((1,4),fromList [(1,5),(2,0)])
-- ((-17,-5),fromList [])
-- ((-2,12),fromList [])

-- How come the sets are so small? Note that we sometimes still generate
-- negative values for the components of `p`. But we said in the `canFollowExample`
-- that `p` needs to be a valid PVP version. However, the constraints only say that
-- it needs to be a valid PVP version _if `qs` is non-empty!_. This is easily fixed
-- by specifying that `p` is _always_ a valid PVP version!

forAllFollow :: Specification BaseFn ((Int, Int), Set (Int, Int))
forAllFollow :: Specification BaseFn ((Int, Int), Set (Int, Int))
forAllFollow = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set (Int, Int))
qs ->
  [ forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set (Int, Int))
qs forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q -> forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
q forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification BaseFn ((Int, Int), (Int, Int))
canFollowExample
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Int, Int)
p forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification BaseFn (Int, Int)
validPVPVersion
  ]

-- λ> sample $ genFromSpec forAllFollow
-- ((0,0),fromList [])
-- ((0,1),fromList [])
-- ((1,5),fromList [(1,6),(2,0)])
-- ((8,10),fromList [(8,11)])
-- ((12,15),fromList [(12,16)])
-- ((6,16),fromList [])
-- ((4,11),fromList [(4,12)])
-- ((10,21),fromList [(10,22),(11,0)])
-- ((28,2),fromList [(28,3),(29,0)])
-- ((20,3),fromList [(20,4),(21,0)])
-- ((16,29),fromList [(16,30),(17,0)])

-- We also have existential quantification in the language. The first argument to
-- `exists` tells you how to reconstruct the value from known values.

existentials :: Specification BaseFn (Set Int, Set Int)
existentials :: Specification BaseFn (Set Int, Set Int)
existentials = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys ->
  forall a p (fn :: Univ).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs) (forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
eval Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys)) forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs ->
    [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Bool
null_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
`subset_` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys
    , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
xs forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs
    , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
ys forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Set Int)
zs
    ]

-- You can work with your own types relatively easily. If they are `Generic`
-- you even get all the machinery of sum and product types for free!

data FooBarBaz = Foo Int Int | Bar Bool | Baz deriving (FooBarBaz -> FooBarBaz -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FooBarBaz -> FooBarBaz -> Bool
$c/= :: FooBarBaz -> FooBarBaz -> Bool
== :: FooBarBaz -> FooBarBaz -> Bool
$c== :: FooBarBaz -> FooBarBaz -> Bool
Eq, Int -> FooBarBaz -> ShowS
[FooBarBaz] -> ShowS
FooBarBaz -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FooBarBaz] -> ShowS
$cshowList :: [FooBarBaz] -> ShowS
show :: FooBarBaz -> String
$cshow :: FooBarBaz -> String
showsPrec :: Int -> FooBarBaz -> ShowS
$cshowsPrec :: Int -> FooBarBaz -> ShowS
Show, forall x. Rep FooBarBaz x -> FooBarBaz
forall x. FooBarBaz -> Rep FooBarBaz x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FooBarBaz x -> FooBarBaz
$cfrom :: forall x. FooBarBaz -> Rep FooBarBaz x
Generic)

-- All you need to do is introduce instances for `HasSimpleRep` and `HasSpec`:

instance HasSimpleRep FooBarBaz
instance BaseUniverse fn => HasSpec fn FooBarBaz

fooBarBaz :: Specification BaseFn FooBarBaz
fooBarBaz :: Specification BaseFn FooBarBaz
fooBarBaz = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn FooBarBaz
fbb ->
  forall (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
    Term BaseFn FooBarBaz
fbb
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
j -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
j)
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b -> forall (fn :: Univ).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Bool
b)
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  ()
_ -> Bool
False)

-- λ> sample $ genFromSpec fooBarBaz
-- Foo (-1) 0
-- Bar False
-- Foo (-9) (-3)
-- Bar False
-- Foo 1 3
-- Foo (-20) (-8)
-- Foo (-35) (-11)
-- Bar False
-- Foo (-8) 5
-- Bar False
-- Foo (-4) 7

-- Some functions don't exist on the term level. In this case we can use
-- `reifies :: (HasSpec fn a, HasSpec fn b) => Term fn b -> Term fn a -> (a -> b) -> Pred fn`
-- to introduce a one-way evaluation of a Haskell function:

reifyExample :: Specification BaseFn (Int, Int)
reifyExample :: Specification BaseFn (Int, Int)
reifyExample = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|a|] Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
[var|b|] ->
  forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn b -> Term fn a -> (a -> b) -> Pred fn
reifies Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
b Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a forall a b. (a -> b) -> a -> b
$ \Int
x -> forall a. Integral a => a -> a -> a
mod Int
x Int
10

-- Here we introduce two variables `a` and `b` without any immediate dependency and we say that
-- `b` reifies `a` via the haskell function `\x -> mod x 10`. The best way to understand what this
-- cryptic code means is to imagine there was a `mod_` function, in that case this code would be equivalent
-- to:

reifyExample' :: Specification BaseFn (Int, Int)
reifyExample' :: Specification BaseFn (Int, Int)
reifyExample' = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
b ->
  [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
b forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ). Term fn Int -> Term fn Int -> Term fn Int
mod_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
10
  , Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
b forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
a
  ]
  where
    mod_ :: Term fn Int -> Term fn Int -> Term fn Int
    mod_ :: forall (fn :: Univ). Term fn Int -> Term fn Int -> Term fn Int
mod_ = forall a. HasCallStack => String -> a
error String
"This doesn't exist"

-- When we look at the plan we get from `reifyExample` we get what we'd expect:
-- λ> printPlan reifyExample
-- Simplified spec:
--   constrained $ \ v_3 ->
--     let v_1 = Fst (ToGeneric v_3) in
--     let v_0 = Snd (ToGeneric v_3) in reifies v_0 v_1
-- SolverPlan
--   Dependencies:
--     v_0 <- [v_1]
--     v_1 <- []
--     v_3 <- [v_0, v_1]
--   Linearization:
--     v_1 <-
--     v_0 <- reifies v_0 v_1
--     v_3 <-
--       assert $ Equal (Fst (ToGeneric v_3)) v_1
--       assert $ Equal (Snd (ToGeneric v_3)) v_0

-- Sometimes it is convenient to introduce an auxilliary variable to represent the result of applying the
-- haskell-level function to the term, for this purpose we have
-- `reify :: (HasSpec fn a, HasSpec fn b, IsPred p fn) => Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn`.

-- We have tools to control the distribution of test cases and monitor those distributions. Using `branchW` we can
-- attach weights to branches in a `caseOn` and using `monitor :: ((forall. Term fn a -> a) -> Property -> Property) -> Pred fn`
-- we can use the normal QuickCheck functions for monitoring distributions of generators to see the effects of this.

monitorExample :: Specification BaseFn (Either Int Int)
monitorExample :: Specification BaseFn (Either Int Int)
monitorExample = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Either Int Int)
e ->
  forall (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
    Term BaseFn (Either Int Int)
e
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
_ -> forall (fn :: Univ).
((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn
monitor forall a b. (a -> b) -> a -> b
$ \forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
_ -> forall prop. Testable prop => String -> prop -> Property
label String
"Left")
    (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
2 forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
_ -> forall (fn :: Univ).
((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn
monitor forall a b. (a -> b) -> a -> b
$ \forall b.
Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  b
-> b
_ -> forall prop. Testable prop => String -> prop -> Property
label String
"Right")

-- The `forAllSpec :: (Testable p, HasSpec fn a) => Specification fn a -> (a -> p) -> Property` we
-- automatically get the monitoring from the spec in our property:

prop_monitoring :: Property
prop_monitoring :: Property
prop_monitoring = forall (fn :: Univ) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> p) -> Property
forAllSpec Specification BaseFn (Either Int Int)
monitorExample forall a b. (a -> b) -> a -> b
$ \Either Int Int
_ -> Bool
True

-- λ> quickCheck $ prop_monitoring
-- +++ OK, passed 100 tests:
-- 64% Right
-- 36% Left

-- Other tools for controlling distributions of specifications are available too, for example
-- `chooseSpec :: HasSpec fn a => (Int, Specification fn a) -> (Int, Specification fn a) -> Specification fn a`,
-- the definition of which constitutes a useful object of study to better understand how to use the compositional
-- nature of the system to build powerful features.

chooseSpecExample :: Specification BaseFn Int
chooseSpecExample :: Specification BaseFn Int
chooseSpecExample =
  forall (fn :: Univ) a.
HasSpec fn a =>
(Int, Specification fn a)
-> (Int, Specification fn a) -> Specification fn a
chooseSpec
    (Int
1, forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0)
    (Int
2, forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i)

prop_chooseSpec :: Property
prop_chooseSpec :: Property
prop_chooseSpec = forall (fn :: Univ) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> p) -> Property
forAllSpec Specification BaseFn Int
chooseSpecExample forall a b. (a -> b) -> a -> b
$ \Int
i ->
  forall prop. Testable prop => String -> prop -> Property
label (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
signum Int
i) Bool
True

-- λ> quickCheck prop_chooseSpec
-- +++ OK, passed 100 tests:
-- 67% 1
-- 33% -1