{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Constrained.Examples.Tree where

import Constrained.API
import Constrained.Spec.Tree (BinTree (..), rootLabel_)
import Data.Tree

allZeroTree :: Specification (BinTree Int)
allZeroTree :: Specification (BinTree Int)
allZeroTree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
a Term (BinTree Int)
_ -> Term Int
a forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
10 Term (BinTree Int)
t
  ]

isBST :: Specification (BinTree Int)
isBST :: Specification (BinTree Int)
isBST = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
left Term Int
a Term (BinTree Int)
right ->
      -- TODO: if there was a `binTreeRoot` function on trees
      -- this wouldn't need to be quadratic as we would
      -- only check agains the head of the left and right
      -- subtrees, not _every element_
      [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
left forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
l Term (BinTree Int)
_ -> Term Int
l forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
a
      , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
right forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
h Term (BinTree Int)
_ -> Term Int
a forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
h
      ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
10 Term (BinTree Int)
t
  ]

noChildrenSameTree :: Specification (BinTree Int)
noChildrenSameTree :: Specification (BinTree Int)
noChildrenSameTree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
t forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
left Term Int
a Term (BinTree Int)
right ->
      [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
left forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
l Term (BinTree Int)
_ -> Term Int
l forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
      , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (BinTree Int)
right forall a b. (a -> b) -> a -> b
$ \Term (BinTree Int)
_ Term Int
r Term (BinTree Int)
_ -> Term Int
r forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
      ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
8 Term (BinTree Int)
t
  ]

isAllZeroTree :: Specification (Tree Int)
isAllZeroTree :: Specification (Tree Int)
isAllZeroTree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
      [ Term Int
a forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0
      , forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Tree Int]
cs forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
4
      ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
30) Term (Tree Int)
t
  ]

noSameChildrenTree :: Specification (Tree Int)
noSameChildrenTree :: Specification (Tree Int)
noSameChildrenTree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
      [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
a forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
8]
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
cs forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t' ->
          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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t' forall a b. (a -> b) -> a -> b
$ \Term Int
b Term [Tree Int]
_ ->
            Term Int
b forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
a
      ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
30) Term (Tree Int)
t
  ]

successiveChildren :: Specification (Tree Int)
successiveChildren :: Specification (Tree Int)
successiveChildren = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
cs ->
      [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
cs forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t' ->
          forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree Int)
t' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a forall a. Num a => a -> a -> a
+ Term Int
1
      ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. a -> Maybe a
Just Integer
2, Integer
10) Term (Tree Int)
t
  ]

successiveChildren8 :: Specification (Tree Int)
successiveChildren8 :: Specification (Tree Int)
successiveChildren8 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
  [ Term (Tree Int)
t forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Tree Int)
successiveChildren
  , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term Int
a Term [Tree Int]
_ -> Term Int
a forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
1 .. Int
5]
  ]

roseTreeList :: Specification [Tree Int]
roseTreeList :: Specification [Tree Int]
roseTreeList = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [Tree Int]
ts ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [Tree Int]
ts forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
  , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree Int]
ts forall a b. (a -> b) -> a -> b
$ \Term (Tree Int)
t ->
      [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Tree Int)
t forall a b. (a -> b) -> a -> b
$ \Term (Int, [Tree Int])
_ -> Bool
False
      ]
  ]

roseTreePairs :: Specification (Tree ([Int], [Int]))
roseTreePairs :: Specification (Tree ([Int], [Int]))
roseTreePairs = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree ([Int], [Int]))
t ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree ([Int], [Int]))
t forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit ([Int
1 .. Int
10], [Int
1 .. Int
10])
  , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree ([Int], [Int]))
t forall a b. (a -> b) -> a -> b
$ \Term ([Int], [Int])
p Term [Tree ([Int], [Int])]
ts ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree ([Int], [Int])]
ts forall a b. (a -> b) -> a -> b
$ \Term (Tree ([Int], [Int]))
t' ->
        forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ (forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree ([Int], [Int]))
t') forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term ([Int], [Int])
p
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. Maybe a
Nothing, Integer
10) Term (Tree ([Int], [Int]))
t
  ]

roseTreeMaybe :: Specification (Tree (Maybe (Int, Int)))
roseTreeMaybe :: Specification (Tree (Maybe (Int, Int)))
roseTreeMaybe = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree (Maybe (Int, Int)))
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Maybe (Int, Int)))
t forall a b. (a -> b) -> a -> b
$ \Term (Maybe (Int, Int))
mp Term [Tree (Maybe (Int, Int))]
ts ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Maybe (Int, Int))]
ts forall a b. (a -> b) -> a -> b
$ \Term (Tree (Maybe (Int, Int)))
t' ->
        forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust Term (Maybe (Int, Int))
mp forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
          forall a p.
(HasSpec a, IsNormalType a, IsPred p) =>
Term (Maybe a) -> (Term a -> p) -> Pred
onJust (forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (Maybe (Int, Int)))
t') forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p' ->
            forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p
  , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Maybe (Int, Int)))
t forall a b. (a -> b) -> a -> b
$ \Term (Maybe (Int, Int))
mp Term [Tree (Maybe (Int, Int))]
_ -> forall a. (HasSpec a, IsNormalType a) => Term (Maybe a) -> Pred
isJust Term (Maybe (Int, Int))
mp
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. Maybe a
Nothing, Integer
10) Term (Tree (Maybe (Int, Int)))
t
  ]

badTreeInteraction :: Specification (Tree (Either Int Int))
badTreeInteraction :: Specification (Tree (Either Int Int))
badTreeInteraction = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
t ->
  [ 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Either Int Int))
t forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
n Term [Tree (Either Int Int)]
ts' ->
      [ forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> Pred
isCon @"Right" Term (Either Int Int)
n
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Either Int Int)]
ts' forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
_ -> Bool
True
      ]
  , 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),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (Either Int Int))
t forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
n Term [Tree (Either Int Int)]
ts' ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (Either Int Int)]
ts' forall a b. (a -> b) -> a -> b
$ \Term (Tree (Either Int Int))
t' ->
        [ forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. a -> Maybe a
Just Integer
4, Integer
10) Term (Tree (Either Int Int))
t'
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (Either Int Int))
t' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Either Int Int)
n
        ]
  , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (forall a. a -> Maybe a
Just Integer
4, Integer
10) Term (Tree (Either Int Int))
t
  ]