{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.ManualExamples where

import Constrained.API
import Constrained.Properties (forAllSpec)
import Data.Set (Set)
import GHC.Generics
import GHC.Natural
import Test.QuickCheck hiding (forAll)
import qualified Test.QuickCheck as QuickCheck

{- Generating from Specifications, and checking against Specifications -}

prop1 :: Gen Property
prop1 :: Gen Property
prop1 = do
  (Int
w, Int
x, Int
y, Int
z) <- Gen (Int, Int, Int, Int)
forall a. Arbitrary a => Gen a
arbitrary :: Gen (Int, Int, Int, Int)
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y Bool -> Bool -> Bool
&& Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Property
forall prop. Testable prop => prop -> Property
property (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z)

spec1 :: Specification (Int, Int, Int, Int)
spec1 :: Specification (Int, Int, Int, Int)
spec1 = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Int, Int)))) [Term Bool]
-> Specification (Int, Int, Int, Int)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int, Int)))) [Term Bool]
 -> Specification (Int, Int, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int, Int)))) [Term Bool]
-> Specification (Int, Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
w Term Int
x Term Int
y Term Int
z -> [Term Int
w Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x, Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y, Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
z]

prop2 :: Gen Property
prop2 :: Gen Property
prop2 = do
  (Int
w, Int
x, Int
y, Int
z) <- Specification (Int, Int, Int, Int) -> Gen (Int, Int, Int, Int)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (Int, Int, Int, Int)
spec1
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y Bool -> Bool -> Bool
&& Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool -> Property
forall prop. Testable prop => prop -> Property
property (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z)

prop3 :: Gen Property
prop3 :: Gen Property
prop3 = do
  (Int
w, Int
x, Int
y, Int
z) <- [(Int, Gen (Int, Int, Int, Int))] -> Gen (Int, Int, Int, Int)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
9, Specification (Int, Int, Int, Int) -> Gen (Int, Int, Int, Int)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (Int, Int, Int, Int)
spec1), (Int
1, Gen (Int, Int, Int, Int)
forall a. Arbitrary a => Gen a
arbitrary)]
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    if (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y Bool -> Bool -> Bool
&& Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z)
      then Bool -> Property
forall prop. Testable prop => prop -> Property
property (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z)
      else Property -> Property
forall prop. Testable prop => prop -> Property
expectFailure (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property (Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
z)

leqPair :: Specification (Int, Int)
leqPair :: Specification (Int, Int)
leqPair = (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> Pred) -> Specification (Int, Int))
-> (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
    Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. (Term Int
y Term Int -> Term Int -> Term Int
forall a. NumLike a => Term a -> Term a -> Term a
+. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
2))

sumPair :: Specification (Int, Int)
sumPair :: Specification (Int, Int)
sumPair = (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> Pred) -> Specification (Int, Int))
-> (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
    [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Term Int
20
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
25
      ]

ex1 :: Specification Int
ex1 :: Specification Int
ex1 = (Term Int -> Bool) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Bool) -> Specification Int)
-> (Term Int -> Bool) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_x -> Bool
True

ex2 :: Specification Int
ex2 :: Specification Int
ex2 = (Term Int -> Term Bool) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Term Bool) -> Specification Int)
-> (Term Int -> Term Bool) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
3

ex3 :: Specification Int
ex3 :: Specification Int
ex3 = (Term Int -> [Term Bool]) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> [Term Bool]) -> Specification Int)
-> (Term Int -> [Term Bool]) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> [Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
2, Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0]

ex4 :: Specification Int
ex4 :: Specification Int
ex4 = (Term Int -> Pred) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Pred) -> Specification Int)
-> (Term Int -> Pred) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
9

{- From Term to Pred
1.   `assert`
-}

-- assert :: IsPred p => p -> Pred
ex5 :: Specification [Int]
ex5 :: Specification [Int]
ex5 = (Term [Int] -> Pred) -> Specification [Int]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [Int] -> Pred) -> Specification [Int])
-> (Term [Int] -> Pred) -> Specification [Int]
forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term Int
7 Term [Int]
xs

{-  For all elements in a container type (List, Set, Map)
1.  `forAll`
-}

-- forAll :: (Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
--           Term t -> (Term a -> p) -> Pred
-- class Forallable t e | t -> e where
-- instance Ord k => Forallable (Map k v) (k, v)
-- instance Ord a => Forallable (Set a) a
-- instance Forallable [a] a

ex6 :: Specification [Int]
ex6 :: Specification [Int]
ex6 = (Term [Int] -> Pred) -> Specification [Int]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [Int] -> Pred) -> Specification [Int])
-> (Term [Int] -> Pred) -> Specification [Int]
forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs ->
  Term [Int] -> (Term Int -> [Term Bool]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs ((Term Int -> [Term Bool]) -> Pred)
-> (Term Int -> [Term Bool]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> [Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10, Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
1]

{-  Reification
1.  `reifies`
2.  `reify`
3.  `assertRefified`
-}

-- reifies :: (HasSpec a, HasSpec b) => Term b -> Term a -> (a -> b) -> Pred
ex7 :: Specification (Int, [Int])
ex7 :: Specification (Int, [Int])
ex7 = (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, [Int]) -> Pred) -> Specification (Int, [Int]))
-> (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a b. (a -> b) -> a -> b
$ \Term (Int, [Int])
pair ->
  Term (Int, [Int])
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [Int])
pair (FunTy (MapList Term (ProductAsList (Int, [Int]))) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
n Term [Int]
xs ->
    Term Int -> Term [Int] -> ([Int] -> Int) -> Pred
forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term Int
n Term [Int]
xs [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum

-- reify :: (HasSpec a, HasSpec b, IsPred p) => Term a -> (a -> b) -> (Term b -> p) -> Pred
ex8 :: Specification ([Int], [Int])
ex8 :: Specification ([Int], [Int])
ex8 = (Term ([Int], [Int]) -> Pred) -> Specification ([Int], [Int])
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term ([Int], [Int]) -> Pred) -> Specification ([Int], [Int]))
-> (Term ([Int], [Int]) -> Pred) -> Specification ([Int], [Int])
forall a b. (a -> b) -> a -> b
$ \Term ([Int], [Int])
pair ->
  Term ([Int], [Int])
-> FunTy (MapList Term (ProductAsList ([Int], [Int]))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ([Int], [Int])
pair (FunTy (MapList Term (ProductAsList ([Int], [Int]))) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList ([Int], [Int]))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs1 Term [Int]
xs2 ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Int] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
xs1 Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
5
    , Term [Int] -> (Term Int -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
xs1 ((Term Int -> Term Bool) -> Pred)
-> (Term Int -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
    , Term [Int] -> ([Int] -> [Int]) -> (Term [Int] -> Term Bool) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term [Int]
xs1 [Int] -> [Int]
forall a. [a] -> [a]
reverse ((Term [Int] -> Term Bool) -> Pred)
-> (Term [Int] -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term [Int]
t -> Term [Int]
xs2 Term [Int] -> Term [Int] -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Int]
t
    ]

-- assertReified :: (HasSpec Bool, HasSpec a) => Term a -> (a -> Bool) -> Pred
ex9 :: Specification Int
ex9 :: Specification Int
ex9 = (Term Int -> [Pred]) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> [Pred]) -> Specification Int)
-> (Term Int -> [Pred]) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
  , Term Int -> (Int -> Bool) -> Pred
forall a. HasSpec a => Term a -> (a -> Bool) -> Pred
assertReified Term Int
x (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
10)
  ]

{- Disjunction, choosing between multiple things with the same type
1.  `CaseOn`, `branch`, `branchW`
2.  `chooseSpec`
-}

{-
caseOn
  :: (HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
      TypeSpec a ~ TypeSpec (SimpleRep a),
      SimpleRep a
      ~ Constrained.Generic.SumOver
          (Constrained.Spec.SumProd.Cases (SimpleRep a)),
      TypeList (Constrained.Spec.SumProd.Cases (SimpleRep a))) =>
     Term a
     -> FunTy
          (MapList
             (Weighted Binder) (Constrained.Spec.SumProd.Cases (SimpleRep a)))
          Pred
-}

data Three = One Int | Two Bool | Three Int deriving (Eq Three
Eq Three =>
(Three -> Three -> Ordering)
-> (Three -> Three -> Bool)
-> (Three -> Three -> Bool)
-> (Three -> Three -> Bool)
-> (Three -> Three -> Bool)
-> (Three -> Three -> Three)
-> (Three -> Three -> Three)
-> Ord Three
Three -> Three -> Bool
Three -> Three -> Ordering
Three -> Three -> Three
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Three -> Three -> Ordering
compare :: Three -> Three -> Ordering
$c< :: Three -> Three -> Bool
< :: Three -> Three -> Bool
$c<= :: Three -> Three -> Bool
<= :: Three -> Three -> Bool
$c> :: Three -> Three -> Bool
> :: Three -> Three -> Bool
$c>= :: Three -> Three -> Bool
>= :: Three -> Three -> Bool
$cmax :: Three -> Three -> Three
max :: Three -> Three -> Three
$cmin :: Three -> Three -> Three
min :: Three -> Three -> Three
Ord, Three -> Three -> Bool
(Three -> Three -> Bool) -> (Three -> Three -> Bool) -> Eq Three
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Three -> Three -> Bool
== :: Three -> Three -> Bool
$c/= :: Three -> Three -> Bool
/= :: Three -> Three -> Bool
Eq, Int -> Three -> ShowS
[Three] -> ShowS
Three -> String
(Int -> Three -> ShowS)
-> (Three -> String) -> ([Three] -> ShowS) -> Show Three
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Three -> ShowS
showsPrec :: Int -> Three -> ShowS
$cshow :: Three -> String
show :: Three -> String
$cshowList :: [Three] -> ShowS
showList :: [Three] -> ShowS
Show, (forall x. Three -> Rep Three x)
-> (forall x. Rep Three x -> Three) -> Generic Three
forall x. Rep Three x -> Three
forall x. Three -> Rep Three x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Three -> Rep Three x
from :: forall x. Three -> Rep Three x
$cto :: forall x. Rep Three x -> Three
to :: forall x. Rep Three x -> Three
Generic)

instance HasSimpleRep Three

instance HasSpec Three

ex10 :: Specification Three
ex10 :: Specification Three
ex10 = (Term Three -> Pred) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> Pred) -> Specification Three)
-> (Term Three -> Pred) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three ->
  Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn
    Term Three
three
    (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1) -- One
    (FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
b -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Term Bool
not_ Term Bool
b)) -- Two
    (FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
j -> Term Int
j Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
3) -- Three

ex11 :: Specification Three
ex11 :: Specification Three
ex11 = (Term Three -> Pred) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> Pred) -> Specification Three)
-> (Term Three -> Pred) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three ->
  Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn
    Term Three
three
    (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0) -- One, weight 1
    (Int
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
b -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert Term Bool
b) -- Two, weight 2
    (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
j -> Term Int
j Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
0) -- Three, weight 3

-- chooseSpec:: HasSpec a => (Int, Specification a) -> (Int, Specification a) -> Specification a

ex12 :: Specification (Int, [Int])
ex12 :: Specification (Int, [Int])
ex12 =
  (Int, Specification (Int, [Int]))
-> (Int, Specification (Int, [Int])) -> Specification (Int, [Int])
forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec
    ( Int
5
    , (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, [Int]) -> Pred) -> Specification (Int, [Int]))
-> (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a b. (a -> b) -> a -> b
$ \Term (Int, [Int])
pair ->
        Term (Int, [Int])
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [Int])
pair (FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
tot Term [Int]
xs -> [Term Int
tot Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
10, Term [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
xs Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
tot, Term [Int] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
xs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
3]
    )
    ( Int
3
    , (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, [Int]) -> Pred) -> Specification (Int, [Int]))
-> (Term (Int, [Int]) -> Pred) -> Specification (Int, [Int])
forall a b. (a -> b) -> a -> b
$ \Term (Int, [Int])
pair ->
        Term (Int, [Int])
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [Int])
pair (FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Int, [Int]))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
tot Term [Int]
xs -> [Term Int
tot Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
10, Term [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Int]
xs Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
tot, Term [Int] -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
xs Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
6]
    )

{- Primed library functions which are compositions with match

1.  `forAll'`
2.  `constrained'`
3.  `reify'`
-}

ex13a :: Specification [(Int, Int)]
ex13a :: Specification [(Int, Int)]
ex13a = (Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)])
-> (Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ \Term [(Int, Int)]
xs ->
  Term [(Int, Int)] -> (Term (Int, Int) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [(Int, Int)]
xs ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
x -> Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
x (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b -> Term Int
a Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int -> Term Int
forall a. Num a => a -> a
negate Term Int
b

ex13b :: Specification [(Int, Int)]
ex13b :: Specification [(Int, Int)]
ex13b = (Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)]
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)])
-> (Term [(Int, Int)] -> Pred) -> Specification [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ \Term [(Int, Int)]
xs ->
  Term [(Int, Int)]
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term [(Int, Int)]
xs (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b -> Term Int
a Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int -> Term Int
forall a. Num a => a -> a
negate Term Int
b

ex14a :: Specification (Int, Int, Int)
ex14a :: Specification (Int, Int, Int)
ex14a = (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int))
-> (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int, Int)
triple ->
  Term (Int, Int, Int)
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int, Int)
triple (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b Term Int
c -> [Term Int
b Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1, Term Int
c Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
b Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1]

ex14b :: Specification (Int, Int, Int)
ex14b :: Specification (Int, Int, Int)
ex14b = FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
-> Specification (Int, Int, Int)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
 -> Specification (Int, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) [Term Bool]
-> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b Term Int
c -> [Term Int
b Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1, Term Int
c Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
b Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1]

ex15a :: Specification (Int, Int, Int)
ex15a :: Specification (Int, Int, Int)
ex15a = (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int))
-> (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int, Int)
triple ->
  Term (Int, Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int, Int)
triple (FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x1 Term Int
x2 Term Int
x3 ->
    Term Int
-> (Int -> (Int, Int)) -> (Term (Int, Int) -> Pred) -> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term Int
x1 (\Int
a -> (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)) ((Term (Int, Int) -> Pred) -> Pred)
-> (Term (Int, Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
t ->
      Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
t (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
b Term Int
c -> [Term Int
x2 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
b, Term Int
x3 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
c]

ex15b :: Specification (Int, Int, Int)
ex15b :: Specification (Int, Int, Int)
ex15b = (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int))
-> (Term (Int, Int, Int) -> Pred) -> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int, Int)
triple ->
  Term (Int, Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int, Int)
triple (FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x1 Term Int
x2 Term Int
x3 ->
    Term Int
-> (Int -> (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b),
 HasSimpleRep b, All HasSpec (Args (SimpleRep b)),
 IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b,
 IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) =>
Term a
-> (a -> b) -> FunTy (MapList Term (Args (SimpleRep b))) p -> Pred
reify' Term Int
x1 (\Int
a -> (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)) (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
b Term Int
c -> [Term Int
x2 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
b, Term Int
x3 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
c]

ex15c :: Specification (Int, Int, Int)
ex15c :: Specification (Int, Int, Int)
ex15c = FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Specification (Int, Int, Int)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
 -> Specification (Int, Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int, Int)))) Pred
-> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x1 Term Int
x2 Term Int
x3 ->
  Term Int
-> (Int -> (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec b ~ TypeSpec (SimpleRep b), HasSpec (SimpleRep b),
 HasSimpleRep b, All HasSpec (Args (SimpleRep b)),
 IsProd (SimpleRep b), HasSpec a, HasSpec b, IsProductType b,
 IsProd a, IsPred p, GenericRequires b, ProdAsListComputes b) =>
Term a
-> (a -> b) -> FunTy (MapList Term (Args (SimpleRep b))) p -> Pred
reify' Term Int
x1 (\Int
a -> (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)) (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
b Term Int
c -> [Term Int
x2 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
b, Term Int
x3 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
c]

{-  Construtors and Selectors
1.  `onCon`
2.  `sel`
4.  `isJust`
-}

ex16 :: Specification Three
ex16 :: Specification Three
ex16 = (Term Three -> Pred) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> Pred) -> Specification Three)
-> (Term Three -> Pred) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three ->
  Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn
    Term Three
three
    (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1) -- One, weight 1
    (Int
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
b -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Term Bool
not_ Term Bool
b)) -- Two, weight 2
    (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
j -> Term Int
j Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
3) -- Three, weight 3

ex17 :: Specification Three
ex17 :: Specification Three
ex17 = (Term Three -> [Pred]) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> [Pred]) -> Specification Three)
-> (Term Three -> [Pred]) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three ->
  [ forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"One" Term Three
three (\Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1)
  , forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Two" Term Three
three (\Term Bool
x -> Term Bool -> Term Bool
not_ Term Bool
x)
  , forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Three" Term Three
three (\Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
3)
  ]

ex18 :: Specification Three
ex18 :: Specification Three
ex18 = (Term Three -> Pred) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> Pred) -> Specification Three)
-> (Term Three -> Pred) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three -> forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Three" Term Three
three (\Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
3)

ex19 :: Specification (Maybe Bool)
ex19 :: Specification (Maybe Bool)
ex19 = (Term (Maybe Bool) -> Pred) -> Specification (Maybe Bool)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Maybe Bool) -> Pred) -> Specification (Maybe Bool))
-> (Term (Maybe Bool) -> Pred) -> Specification (Maybe Bool)
forall a b. (a -> b) -> a -> b
$ \Term (Maybe Bool)
mb -> forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 GenericRequires a, SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"Just" Term (Maybe Bool)
mb (\Term Bool
x -> Term Bool
x Term Bool -> Term Bool -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Bool -> Term Bool
forall a. HasSpec a => a -> Term a
lit Bool
False)

data Dimensions where
  Dimensions ::
    { Dimensions -> Int
length :: Int
    , Dimensions -> Int
width :: Int
    , Dimensions -> Int
depth :: Int
    } ->
    Dimensions
  deriving (Eq Dimensions
Eq Dimensions =>
(Dimensions -> Dimensions -> Ordering)
-> (Dimensions -> Dimensions -> Bool)
-> (Dimensions -> Dimensions -> Bool)
-> (Dimensions -> Dimensions -> Bool)
-> (Dimensions -> Dimensions -> Bool)
-> (Dimensions -> Dimensions -> Dimensions)
-> (Dimensions -> Dimensions -> Dimensions)
-> Ord Dimensions
Dimensions -> Dimensions -> Bool
Dimensions -> Dimensions -> Ordering
Dimensions -> Dimensions -> Dimensions
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Dimensions -> Dimensions -> Ordering
compare :: Dimensions -> Dimensions -> Ordering
$c< :: Dimensions -> Dimensions -> Bool
< :: Dimensions -> Dimensions -> Bool
$c<= :: Dimensions -> Dimensions -> Bool
<= :: Dimensions -> Dimensions -> Bool
$c> :: Dimensions -> Dimensions -> Bool
> :: Dimensions -> Dimensions -> Bool
$c>= :: Dimensions -> Dimensions -> Bool
>= :: Dimensions -> Dimensions -> Bool
$cmax :: Dimensions -> Dimensions -> Dimensions
max :: Dimensions -> Dimensions -> Dimensions
$cmin :: Dimensions -> Dimensions -> Dimensions
min :: Dimensions -> Dimensions -> Dimensions
Ord, Dimensions -> Dimensions -> Bool
(Dimensions -> Dimensions -> Bool)
-> (Dimensions -> Dimensions -> Bool) -> Eq Dimensions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Dimensions -> Dimensions -> Bool
== :: Dimensions -> Dimensions -> Bool
$c/= :: Dimensions -> Dimensions -> Bool
/= :: Dimensions -> Dimensions -> Bool
Eq, Int -> Dimensions -> ShowS
[Dimensions] -> ShowS
Dimensions -> String
(Int -> Dimensions -> ShowS)
-> (Dimensions -> String)
-> ([Dimensions] -> ShowS)
-> Show Dimensions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Dimensions -> ShowS
showsPrec :: Int -> Dimensions -> ShowS
$cshow :: Dimensions -> String
show :: Dimensions -> String
$cshowList :: [Dimensions] -> ShowS
showList :: [Dimensions] -> ShowS
Show, (forall x. Dimensions -> Rep Dimensions x)
-> (forall x. Rep Dimensions x -> Dimensions) -> Generic Dimensions
forall x. Rep Dimensions x -> Dimensions
forall x. Dimensions -> Rep Dimensions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Dimensions -> Rep Dimensions x
from :: forall x. Dimensions -> Rep Dimensions x
$cto :: forall x. Rep Dimensions x -> Dimensions
to :: forall x. Rep Dimensions x -> Dimensions
Generic)

instance HasSimpleRep Dimensions

instance HasSpec Dimensions

ex20a :: Specification Dimensions
ex20a :: Specification Dimensions
ex20a = (Term Dimensions -> Pred) -> Specification Dimensions
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Dimensions -> Pred) -> Specification Dimensions)
-> (Term Dimensions -> Pred) -> Specification Dimensions
forall a b. (a -> b) -> a -> b
$ \Term Dimensions
d ->
  Term Dimensions
-> FunTy (MapList Term (ProductAsList Dimensions)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Dimensions
d (FunTy (MapList Term (ProductAsList Dimensions)) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList Dimensions)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
l Term Int
w Term Int
dp -> [Term Int
l Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
10, Term Int
w Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5, Term Int
dp Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
20]

ex20b :: Specification Dimensions
ex20b :: Specification Dimensions
ex20b = (Term Dimensions -> [Term Bool]) -> Specification Dimensions
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Dimensions -> [Term Bool]) -> Specification Dimensions)
-> (Term Dimensions -> [Term Bool]) -> Specification Dimensions
forall a b. (a -> b) -> a -> b
$ \Term Dimensions
d ->
  [ forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @0 Term Dimensions
d Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
10
  , forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term Dimensions
d Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5
  , forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @2 Term Dimensions
d Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
20
  ]

width_ :: Term Dimensions -> Term Int
width_ :: Term Dimensions -> Term Int
width_ Term Dimensions
d = forall (n :: Natural) a (c :: Symbol) (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec a ~ TypeSpec (ProdOver as), Select n as, HasSpec a,
 HasSpec (ProdOver as), HasSimpleRep a, GenericRequires a) =>
Term a -> Term (At n as)
sel @1 Term Dimensions
d

ex21 :: Specification Dimensions
ex21 :: Specification Dimensions
ex21 = (Term Dimensions -> Term Bool) -> Specification Dimensions
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Dimensions -> Term Bool) -> Specification Dimensions)
-> (Term Dimensions -> Term Bool) -> Specification Dimensions
forall a b. (a -> b) -> a -> b
$ \Term Dimensions
d -> Term Dimensions -> Term Int
width_ Term Dimensions
d Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1

{- Naming introduced lambda bound Term variables
1.  [var|name|]
-}

ex22a :: Specification (Int, Int)
ex22a :: Specification (Int, Int)
ex22a = (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> Pred) -> Specification (Int, Int))
-> (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
pair ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
pair (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
left Term Int
right -> [Term Int
left Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
right, Term Int
left Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
right Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1]

ex22b :: Specification (Int, Int)
ex22b :: Specification (Int, Int)
ex22b = (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> Pred) -> Specification (Int, Int))
-> (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \ Term (Int, Int)
[var|pair|] ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
pair (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|left|] Term Int
[var|right|] -> [Term Int
left Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
right, Term Int
left Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
right Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
1]

{-  Existential quantifiers
1.  `exists`
2.  `unsafeExists`
-}

ex24 :: Specification Int
ex24 :: Specification Int
ex24 = (Term Int -> Pred) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Pred) -> Specification Int)
-> (Term Int -> Pred) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|oddx|] ->
  (Term Int -> [Pred]) -> Pred
forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists
    (\ Term Int
[var|y|] -> [Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
oddx Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1])

ex25 :: Specification Int
ex25 :: Specification Int
ex25 = [String] -> Specification Int -> Specification Int
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"odd via (y+y+1)"] (Specification Int -> Specification Int)
-> Specification Int -> Specification Int
forall a b. (a -> b) -> a -> b
$
  (Term Int -> Pred) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> Pred) -> Specification Int)
-> (Term Int -> Pred) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|oddx|] ->
    ((forall b. Term b -> b) -> GE Int) -> (Term Int -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
      (\forall b. Term b -> b
eval -> Int -> GE Int
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Int
forall a. Integral a => a -> a -> a
div (Term Int -> Int
forall b. Term b -> b
eval Term Int
oddx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
2))
      (\ Term Int
[var|y|] -> [Term Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
oddx Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1])

{-  Conditionals
1.  `whenTrue`
2.  `ifElse`
-}

data Rectangle = Rectangle {Rectangle -> Int
wid :: Int, Rectangle -> Int
len :: Int, Rectangle -> Bool
square :: Bool}
  deriving (Int -> Rectangle -> ShowS
[Rectangle] -> ShowS
Rectangle -> String
(Int -> Rectangle -> ShowS)
-> (Rectangle -> String)
-> ([Rectangle] -> ShowS)
-> Show Rectangle
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Rectangle -> ShowS
showsPrec :: Int -> Rectangle -> ShowS
$cshow :: Rectangle -> String
show :: Rectangle -> String
$cshowList :: [Rectangle] -> ShowS
showList :: [Rectangle] -> ShowS
Show, Rectangle -> Rectangle -> Bool
(Rectangle -> Rectangle -> Bool)
-> (Rectangle -> Rectangle -> Bool) -> Eq Rectangle
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rectangle -> Rectangle -> Bool
== :: Rectangle -> Rectangle -> Bool
$c/= :: Rectangle -> Rectangle -> Bool
/= :: Rectangle -> Rectangle -> Bool
Eq, (forall x. Rectangle -> Rep Rectangle x)
-> (forall x. Rep Rectangle x -> Rectangle) -> Generic Rectangle
forall x. Rep Rectangle x -> Rectangle
forall x. Rectangle -> Rep Rectangle x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Rectangle -> Rep Rectangle x
from :: forall x. Rectangle -> Rep Rectangle x
$cto :: forall x. Rep Rectangle x -> Rectangle
to :: forall x. Rep Rectangle x -> Rectangle
Generic)

instance HasSimpleRep Rectangle

instance HasSpec Rectangle

ex26 :: Specification Rectangle
ex26 :: Specification Rectangle
ex26 = FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred]
-> Specification Rectangle
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred]
 -> Specification Rectangle)
-> FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred]
-> Specification Rectangle
forall a b. (a -> b) -> a -> b
$ \Term Int
w Term Int
l Term Bool
sq ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
w Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
l Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
  , Term Bool -> Pred -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
sq (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
w Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
l)
  ]

ex27 :: Specification Rectangle
ex27 :: Specification Rectangle
ex27 = FunTy (MapList Term (Args (SimpleRep Rectangle))) Pred
-> Specification Rectangle
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep Rectangle))) Pred
 -> Specification Rectangle)
-> FunTy (MapList Term (Args (SimpleRep Rectangle))) Pred
-> Specification Rectangle
forall a b. (a -> b) -> a -> b
$ \Term Int
w Term Int
l Term Bool
sq ->
  Term Bool -> Pred -> [Pred] -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
    Term Bool
sq
    (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
w Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
l)
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
w Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
l Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
    ]

{-  `Explanantions`
1.  `assertExplain`
2.  `explanation`
3.  `ExplainSpec`
-}

ex28a :: Specification (Set Int)
ex28a :: Specification (Set Int)
ex28a = (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> [Pred]) -> Specification (Set Int))
-> (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5) Term (Set Int)
s
  , Term (Set Int) -> (Term Int -> [Term Bool]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s ((Term Int -> [Term Bool]) -> Pred)
-> (Term Int -> [Term Bool]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> [Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
6, Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
20]
  ]

ex28b :: Specification (Set Int)
ex28b :: Specification (Set Int)
ex28b = [String] -> Specification (Set Int) -> Specification (Set Int)
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"5 must be in the set"] (Specification (Set Int) -> Specification (Set Int))
-> Specification (Set Int) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$
  (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set Int) -> [Pred]) -> Specification (Set Int))
-> (Term (Set Int) -> [Pred]) -> Specification (Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
s ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ (Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5) Term (Set Int)
s
    , Term (Set Int) -> (Term Int -> [Term Bool]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set Int)
s ((Term Int -> [Term Bool]) -> Pred)
-> (Term Int -> [Term Bool]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Int
x -> [Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
6, Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
20]
    ]

{-  Operations to define and use Specifications
1.  `satisfies`
2.  `equalSpec`
3.  `notEqualSpec`
4.  `notMemberSpec`
5.  `leqSpec`
6.  `ltSpec`
7.  `geqSpec`
8.  `gtSpec`
5.  `cardinality`
-}

ex29 :: Specification Int
ex29 :: Specification Int
ex29 = (Term Int -> [Pred]) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> [Pred]) -> Specification Int)
-> (Term Int -> [Pred]) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
0
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Int -> Term Int
forall a. HasSpec a => a -> Term a
lit Int
5
  , Term Int -> Specification Int -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term Int
x ([Int] -> Specification Int
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec [Int
2, Int
3])
  ]

{-  Utility functions
1.  `simplifyTerm`
2.  `simplifySpec`
3.  `genFromSpecT`
4.  `genFromSpec`
5.  `genFromSpecWithSeed`
6.  `debugSpec`
-}

{-  Escape Hatch to QuickCheck Gen monad
1.  `monitor`
-}

ex30 :: Specification (Int, Int)
ex30 :: Specification (Int, Int)
ex30 = (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> Pred) -> Specification (Int, Int))
-> (Term (Int, Int) -> Pred) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \ Term (Int, Int)
[var|p|] ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Pred] -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|x|] Term Int
[var|y|] ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
0
    , -- You can use `monitor` to add QuickCheck property modifiers for
      -- monitoring distribution, like classify, label, and cover, to your
      -- specification
      ((forall b. Term b -> b) -> Property -> Property) -> Pred
monitor (((forall b. Term b -> b) -> Property -> Property) -> Pred)
-> ((forall b. Term b -> b) -> Property -> Property) -> Pred
forall a b. (a -> b) -> a -> b
$ \forall b. Term b -> b
eval ->
        Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QuickCheck.classify (Term Int -> Int
forall b. Term b -> b
eval Term Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive y"
          (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QuickCheck.classify (Term Int -> Int
forall b. Term b -> b
eval Term Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive x"
    ]

prop31 :: QuickCheck.Property
prop31 :: Property
prop31 = Specification (Int, Int) -> ((Int, Int) -> Bool) -> Property
forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> p) -> Property
forAllSpec Specification (Int, Int)
ex30 (((Int, Int) -> Bool) -> Property)
-> ((Int, Int) -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Int, Int)
_ -> Bool
True

ex32 :: IO ()
ex32 :: IO ()
ex32 = Property -> IO ()
forall prop. Testable prop => prop -> IO ()
QuickCheck.quickCheck (Property -> IO ()) -> Property -> IO ()
forall a b. (a -> b) -> a -> b
$ Property
prop31

ex11m :: Specification Three
ex11m :: Specification Three
ex11m = (Term Three -> [Pred]) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> [Pred]) -> Specification Three)
-> (Term Three -> [Pred]) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
three ->
  [ Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn
      Term Three
three
      (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0) -- One, weight 1
      (Int
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
b -> Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert Term Bool
b) -- Two, weight 2
      (Int
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args Int)) (Term Bool)
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) (Term Bool)
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
j -> Term Int
j Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
0) -- Three, weight 3
  , ((forall b. Term b -> b) -> Property -> Property) -> Pred
monitor (((forall b. Term b -> b) -> Property -> Property) -> Pred)
-> ((forall b. Term b -> b) -> Property -> Property) -> Pred
forall a b. (a -> b) -> a -> b
$ \forall b. Term b -> b
eval ->
      case (Term Three -> Three
forall b. Term b -> b
eval Term Three
three) of
        One Int
_ -> Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QuickCheck.classify Bool
True String
"One should be about 1/6"
        Two Bool
_ -> Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QuickCheck.classify Bool
True String
"Two should be about 2/6"
        Three Int
_ -> Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QuickCheck.classify Bool
True String
"Three should be about 3/6"
  ]

propex11 :: QuickCheck.Property
propex11 :: Property
propex11 = Specification Three -> (Three -> Bool) -> Property
forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> p) -> Property
forAllSpec Specification Three
ex11m ((Three -> Bool) -> Property) -> (Three -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \Three
_ -> Bool
True

ex33 :: IO ()
ex33 :: IO ()
ex33 = Property -> IO ()
forall prop. Testable prop => prop -> IO ()
QuickCheck.quickCheck (Property -> IO ()) -> Property -> IO ()
forall a b. (a -> b) -> a -> b
$ Property
propex11

{-  Strategy for constraining a large type with many nested sub-components -}

data Nested = Nested Three Rectangle [Int]
  deriving (Int -> Nested -> ShowS
[Nested] -> ShowS
Nested -> String
(Int -> Nested -> ShowS)
-> (Nested -> String) -> ([Nested] -> ShowS) -> Show Nested
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Nested -> ShowS
showsPrec :: Int -> Nested -> ShowS
$cshow :: Nested -> String
show :: Nested -> String
$cshowList :: [Nested] -> ShowS
showList :: [Nested] -> ShowS
Show, Nested -> Nested -> Bool
(Nested -> Nested -> Bool)
-> (Nested -> Nested -> Bool) -> Eq Nested
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nested -> Nested -> Bool
== :: Nested -> Nested -> Bool
$c/= :: Nested -> Nested -> Bool
/= :: Nested -> Nested -> Bool
Eq, (forall x. Nested -> Rep Nested x)
-> (forall x. Rep Nested x -> Nested) -> Generic Nested
forall x. Rep Nested x -> Nested
forall x. Nested -> Rep Nested x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Nested -> Rep Nested x
from :: forall x. Nested -> Rep Nested x
$cto :: forall x. Rep Nested x -> Nested
to :: forall x. Rep Nested x -> Nested
Generic)

instance HasSimpleRep Nested

instance HasSpec Nested

{-
Problem using TruePred, not monomorphic enough
skeleton1 :: Specification Nested
skeleton1 = constrained $ \ [var|nest|] ->
  match nest $ \ [var|three|] [var|rect|] [var|line|] ->
    [ (caseOn (three :: Term Three))
        (branch $ \ _i -> TruePred) -- One,
        (branch $ \ _k -> TruePred) -- Two,
        (branch $ \ _j -> TruePred) -- Three,
    , match rect $ \ [var|_wid|] [var|_len|] [var|_square|] -> TruePred
    , forAll line $ \ [var|_point|] -> TruePred
    ]
-}

-- By type applying match, branch, and forAll to @Pred , makes it monomorphic
--  Note    type Pred = PredD Deps , so it fixes the type argument of PredD
skeleton2 :: Specification Nested
skeleton2 :: Specification Nested
skeleton2 = (Term Nested -> Pred) -> Specification Nested
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Nested -> Pred) -> Specification Nested)
-> (Term Nested -> Pred) -> Specification Nested
forall a b. (a -> b) -> a -> b
$ \ Term Nested
[var|nest|] ->
  Term Nested
-> FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Nested
nest (FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Three
[var|three|] Term Rectangle
[var|rect|] Term [Int]
[var|line|] ->
    [ (Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn (Term Three
three :: Term Three))
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch @Pred (FunTy (MapList Term (Args Int)) Pred
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Pred
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_i -> Pred
forall deps. PredD deps
TruePred) -- One,
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch @Pred (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
_k -> Pred
forall deps. PredD deps
TruePred) -- Two,
        (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch @Pred (FunTy (MapList Term (Args Int)) Pred
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Pred
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_j -> Pred
forall deps. PredD deps
TruePred) -- Three,
    , forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match @Pred Term Rectangle
rect (FunTy (MapList Term (Args (SimpleRep Rectangle))) Pred -> Pred)
-> FunTy (MapList Term (Args (SimpleRep Rectangle))) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|_wid|] Term Int
[var|_len|] Term Bool
[var|_square|] -> Pred
forall deps. PredD deps
TruePred
    , forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll @Pred Term [Int]
line ((Term Int -> Pred) -> Pred) -> (Term Int -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|_point|] -> Pred
forall deps. PredD deps
TruePred
    ]

-- We can do a similar thing by introducing `truePred` with the monomorphic type.
truePred :: Pred
truePred :: Pred
truePred = Pred
forall deps. PredD deps
TruePred

skeleton :: Specification Nested
skeleton :: Specification Nested
skeleton = (Term Nested -> Pred) -> Specification Nested
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Nested -> Pred) -> Specification Nested)
-> (Term Nested -> Pred) -> Specification Nested
forall a b. (a -> b) -> a -> b
$ \ Term Nested
[var|nest|] ->
  Term Nested
-> FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Nested
nest (FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList Nested)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Three
[var|three|] Term Rectangle
[var|rect|] Term [Int]
[var|line|] ->
    [ (Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three))) Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn (Term Three
three :: Term Three))
        (FunTy (MapList Term (Args Int)) Pred -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Pred
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Pred
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_i -> Pred
truePred) -- One,
        (FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Bool)) Pred
 -> Weighted (BinderD Deps) Bool)
-> FunTy (MapList Term (Args Bool)) Pred
-> Weighted (BinderD Deps) Bool
forall a b. (a -> b) -> a -> b
$ \Term Bool
_k -> Pred
truePred) -- Two,
        (FunTy (MapList Term (Args Int)) Pred -> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) Pred
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) Pred
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
_j -> Pred
truePred) -- Three,
    , Term Rectangle
-> FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Rectangle
rect (FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred] -> Pred)
-> FunTy (MapList Term (Args (SimpleRep Rectangle))) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|_wid|] Term Int
[var|_len|] Term Bool
[var|_square|] -> [Pred
truePred]
    , Term [Int] -> (Term Int -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
line ((Term Int -> Pred) -> Pred) -> (Term Int -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|_point|] -> Pred
truePred
    ]

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

newtype Coin = Coin {Coin -> Integer
unCoin :: Integer} deriving (Coin -> Coin -> Bool
(Coin -> Coin -> Bool) -> (Coin -> Coin -> Bool) -> Eq Coin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Coin -> Coin -> Bool
== :: Coin -> Coin -> Bool
$c/= :: Coin -> Coin -> Bool
/= :: Coin -> Coin -> Bool
Eq, Int -> Coin -> ShowS
[Coin] -> ShowS
Coin -> String
(Int -> Coin -> ShowS)
-> (Coin -> String) -> ([Coin] -> ShowS) -> Show Coin
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Coin -> ShowS
showsPrec :: Int -> Coin -> ShowS
$cshow :: Coin -> String
show :: Coin -> String
$cshowList :: [Coin] -> ShowS
showList :: [Coin] -> ShowS
Show)

instance HasSimpleRep Coin where
  type SimpleRep Coin = Natural
  toSimpleRep :: Coin -> SimpleRep Coin
toSimpleRep (Coin Integer
i) = case Integer -> Maybe Natural
integerToNatural Integer
i of
    Maybe Natural
Nothing -> String -> SimpleRep Coin
forall a. HasCallStack => String -> a
error (String -> SimpleRep Coin) -> String -> SimpleRep Coin
forall a b. (a -> b) -> a -> b
$ String
"The impossible happened in toSimpleRep for (Coin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    Just Natural
w -> Natural
SimpleRep Coin
w
  fromSimpleRep :: SimpleRep Coin -> Coin
fromSimpleRep = Natural -> Coin
SimpleRep Coin -> Coin
naturalToCoin

instance HasSpec Coin

integerToNatural :: Integer -> Maybe Natural
integerToNatural :: Integer -> Maybe Natural
integerToNatural Integer
c
  | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Maybe Natural
forall a. Maybe a
Nothing
  | Bool
otherwise = Natural -> Maybe Natural
forall a. a -> Maybe a
Just (Natural -> Maybe Natural) -> Natural -> Maybe Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
c

naturalToCoin :: Natural -> Coin
naturalToCoin :: Natural -> Coin
naturalToCoin = Integer -> Coin
Coin (Integer -> Coin) -> (Natural -> Integer) -> Natural -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral

ex34 :: Specification Coin
ex34 :: Specification Coin
ex34 = (Term Coin -> Pred) -> Specification Coin
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Coin -> Pred) -> Specification Coin)
-> (Term Coin -> Pred) -> Specification Coin
forall a b. (a -> b) -> a -> b
$ \Term Coin
coin ->
  Term Coin
-> FunTy (MapList Term (ProductAsList Coin)) [Term Bool] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term Coin
coin (FunTy (MapList Term (ProductAsList Coin)) [Term Bool] -> Pred)
-> FunTy (MapList Term (ProductAsList Coin)) [Term Bool] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Natural
nat -> [Term Natural
nat Term Natural -> Term Natural -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Natural -> Term Natural
forall a. HasSpec a => a -> Term a
lit Natural
100, Term Natural
nat Term Natural -> Term Natural -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Natural -> Term Natural
forall a. HasSpec a => a -> Term a
lit Natural
200]