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

module Constrained.Examples.Map where

import Constrained.API
import Constrained.Examples.Basic
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Word

mapElemSpec :: Specification (Map Int (Bool, Int))
mapElemSpec :: Specification (Map Int (Bool, Int))
mapElemSpec = (Term (Map Int (Bool, Int)) -> [Pred])
-> Specification (Map Int (Bool, Int))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int (Bool, Int)) -> [Pred])
 -> Specification (Map Int (Bool, Int)))
-> (Term (Map Int (Bool, Int)) -> [Pred])
-> Specification (Map Int (Bool, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Map Int (Bool, Int))
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map Int (Bool, Int))
m Term (Map Int (Bool, Int))
-> Term (Map Int (Bool, Int)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Map Int (Bool, Int) -> Term (Map Int (Bool, Int))
forall a. HasSpec a => a -> Term a
lit Map Int (Bool, Int)
forall a. Monoid a => a
mempty
  , Term [(Bool, Int)]
-> FunTy (MapList Term (Args (SimpleRep (Bool, 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 (Map Int (Bool, Int)) -> Term [(Bool, Int)]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int (Bool, Int))
m) (FunTy (MapList Term (Args (SimpleRep (Bool, Int)))) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Bool, Int)))) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
_ Term Int
b ->
      [Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
b, Term Int
b Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10]
  ]

mapPairSpec :: Specification (Map Int Int, Set Int)
mapPairSpec :: Specification (Map Int Int, Set Int)
mapPairSpec = FunTy
  (MapList Term (Args (SimpleRep (Map Int Int, Set Int))))
  (Term Bool)
-> Specification (Map Int Int, Set 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 (Map Int Int, Set Int))))
   (Term Bool)
 -> Specification (Map Int Int, Set Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Map Int Int, Set Int))))
     (Term Bool)
-> Specification (Map Int Int, Set Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m Term (Set Int)
s ->
  Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map Int Int) -> Term (Set Int)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Int Int)
m) Term (Set Int)
s

mapEmptyDomainSpec :: Specification (Map Int Int)
mapEmptyDomainSpec :: Specification (Map Int Int)
mapEmptyDomainSpec = (Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int))
-> (Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map Int Int) -> Term (Set Int)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Int Int)
m) Term (Set Int)
forall a. Monoid a => a
mempty -- mempty in the Monoid instance (Term fn (Set a))

mapSubSize :: Specification (Map Int Int)
mapSubSize :: Specification (Map Int Int)
mapSubSize = (Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int))
-> (Term (Map Int Int) -> Term Bool) -> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
s ->
  Term Integer
2 Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
- (Term (Map Int Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
s)

knownDomainMap :: Specification (Map Int Int)
knownDomainMap :: Specification (Map Int Int)
knownDomainMap = (Term (Map Int Int) -> [Term Bool]) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> [Term Bool])
 -> Specification (Map Int Int))
-> (Term (Map Int Int) -> [Term Bool])
-> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ Term (Map Int Int) -> Term (Set Int)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Int Int)
m Term (Set Int) -> Term (Set Int) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
1, Int
2])
  , Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term Int
0 Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term (Map Int Int) -> Term [Int]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m
  ]

mapSizeConstrained :: Specification (Map Three Int)
mapSizeConstrained :: Specification (Map Three Int)
mapSizeConstrained = (Term (Map Three Int) -> Term Bool)
-> Specification (Map Three Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Three Int) -> Term Bool)
 -> Specification (Map Three Int))
-> (Term (Map Three Int) -> Term Bool)
-> Specification (Map Three Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Three Int)
m -> Term (Set Three) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map Three Int) -> Term (Set Three)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Three Int)
m) Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
3

sumRange :: Specification (Map Word64 Word64)
sumRange :: Specification (Map Word64 Word64)
sumRange = (Term (Map Word64 Word64) -> Term Bool)
-> Specification (Map Word64 Word64)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Word64 Word64) -> Term Bool)
 -> Specification (Map Word64 Word64))
-> (Term (Map Word64 Word64) -> Term Bool)
-> Specification (Map Word64 Word64)
forall a b. (a -> b) -> a -> b
$ \Term (Map Word64 Word64)
m -> Term [Word64] -> Term Word64
forall a. Foldy a => Term [a] -> Term a
sum_ (Term (Map Word64 Word64) -> Term [Word64]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Word64 Word64)
m) Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Word64 -> Term Word64
forall a. HasSpec a => a -> Term a
lit Word64
10

fixedRange :: Specification (Map Int Int)
fixedRange :: Specification (Map Int Int)
fixedRange = (Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int))
-> (Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ Term [Int] -> (Term Int -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map Int Int) -> Term [Int]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m) (\Term Int
x -> Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
5)
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ (Term (Map Int Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
m) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
1
  ]

rangeHint :: Specification (Map Int Int)
rangeHint :: Specification (Map Int Int)
rangeHint = (Term (Map Int Int) -> Pred) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> Pred) -> Specification (Map Int Int))
-> (Term (Map Int Int) -> Pred) -> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  Hint [Int] -> Term [Int] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [Int]
10 (Term (Map Int Int) -> Term [Int]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m)

rangeSumSize :: Specification (Map Int Int)
rangeSumSize :: Specification (Map Int Int)
rangeSumSize = (Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int))
-> (Term (Map Int Int) -> [Pred]) -> Specification (Map Int Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Int Int)
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map Int Int) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map Int Int)
m Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
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] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ (Term (Map Int Int) -> Term [Int]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m) Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term 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
1) Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term [Int] -> Term Int
forall a. Foldy a => Term [a] -> Term a
sum_ (Term (Map Int Int) -> Term [Int]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map Int Int)
m)
  , Term (Map 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 (Map Int Int)
m (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
k Term Int
v ->
      [ Term Int
k Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (-Term Int
1)
      , Term Int
v Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1
      ]
  ]

elemSpec :: Specification (Int, Int, Map Int Int)
elemSpec :: Specification (Int, Int, Map Int Int)
elemSpec = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Map Int Int)))) [Pred]
-> Specification (Int, Int, Map 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, Map Int Int)))) [Pred]
 -> Specification (Int, Int, Map Int Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Map Int Int)))) [Pred]
-> Specification (Int, Int, Map Int Int)
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|key|] Term Int
[var|val|] Term (Map Int Int)
[var|mapp|] ->
  [ 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
key Term Int -> Term (Set Int) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Map Int Int) -> Term (Set Int)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Int Int)
mapp
  , Term (Map Int Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) Pred -> 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 (Map Int Int)
mapp (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|k'|] Term Int
[var|v'|] ->
      Term Bool -> Term Bool -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue (Term Int
k' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
key) (Term Int
v' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
val)
  , Term (Map Int Int)
mapp Term (Map Int Int) -> Term Int -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
key
  ]

lookupSpecific :: Specification (Int, Int, Map Int Int)
lookupSpecific :: Specification (Int, Int, Map Int Int)
lookupSpecific = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Map Int Int)))) [Pred]
-> Specification (Int, Int, Map 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, Map Int Int)))) [Pred]
 -> Specification (Int, Int, Map Int Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Map Int Int)))) [Pred]
-> Specification (Int, Int, Map Int Int)
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var|k|] Term Int
[var|v|] Term (Map Int Int)
[var|m|] ->
  [ Term (Map Int Int)
m Term (Map Int Int) -> Term Int -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
k
  , 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 (Map Int Int) -> Term (Maybe Int)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term Int
k Term (Map Int Int)
m Term (Maybe Int) -> Term (Maybe Int) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int -> Term (Maybe Int)
forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ Term Int
v
  ]

mapRestrictedValues :: Specification (Map (Either Int ()) Int)
mapRestrictedValues :: Specification (Map (Either Int ()) Int)
mapRestrictedValues = (Term (Map (Either Int ()) Int) -> [Pred])
-> Specification (Map (Either Int ()) Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Either Int ()) Int) -> [Pred])
 -> Specification (Map (Either Int ()) Int))
-> (Term (Map (Either Int ()) Int) -> [Pred])
-> Specification (Map (Either Int ()) Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map (Either Int ()) Int)
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Either Int ())) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map (Either Int ()) Int) -> Term (Set (Either Int ()))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Either Int ()) Int)
m) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
6
  , Term (Map (Either Int ()) Int)
-> FunTy
     (MapList Term (Args (SimpleRep (Either Int (), Int)))) [Pred]
-> 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 (Map (Either Int ()) Int)
m (FunTy
   (MapList Term (Args (SimpleRep (Either Int (), Int)))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (Either Int (), Int)))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Either Int ())
k Term Int
v ->
      [ Term (Either Int ())
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int ()))))
     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 (Either Int ())
k
          (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
_ -> Term Int
20 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)
          (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      , Term Int
v Term Int -> Term (Either Int ()) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Either Int ())
k
      ]
  ]

-- NOTE: this fails if you pick the values of the map first - you're unlikely to generate
-- three values such that two of them are <= -100 and >= 100 respectively even though
-- you take satisfiability of the whole elem constraint into account. This can't be fixed
-- with a `dependsOn v k` because the issue is that we've generated a bunch of values
-- before we ever go to generate the keys.
mapRestrictedValuesThree :: Specification (Map Three Int)
mapRestrictedValuesThree :: Specification (Map Three Int)
mapRestrictedValuesThree = (Term (Map Three Int) -> [Pred]) -> Specification (Map Three Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Three Int) -> [Pred]) -> Specification (Map Three Int))
-> (Term (Map Three Int) -> [Pred])
-> Specification (Map Three Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Three Int)
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set Three) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map Three Int) -> Term (Set Three)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Three Int)
m) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
3
  , Term (Map Three Int)
-> FunTy (MapList Term (Args (SimpleRep (Three, Int)))) [Pred]
-> 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 (Map Three Int)
m (FunTy (MapList Term (Args (SimpleRep (Three, Int)))) [Pred]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Three, Int)))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Three
k Term Int
v ->
      [ 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
k
          (FunTy (MapList Term (Args ())) (Term Bool)
-> Weighted (BinderD Deps) ()
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 ())) (Term Bool)
 -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) (Term Bool)
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term Int
v Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. (-Term Int
100))
          (FunTy (MapList Term (Args ())) (Term Bool)
-> Weighted (BinderD Deps) ()
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 ())) (Term Bool)
 -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) (Term Bool)
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term Int
100 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)
          (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      , -- This is important to demonstrate the point that keys sometimes need to be solved before
        -- values
        Term Int
v Term Int -> Term Three -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Three
k
      ]
  ]

mapRestrictedValuesBool :: Specification (Map Bool Int)
mapRestrictedValuesBool :: Specification (Map Bool Int)
mapRestrictedValuesBool = (Term (Map Bool Int) -> [Pred]) -> Specification (Map Bool Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map Bool Int) -> [Pred]) -> Specification (Map Bool Int))
-> (Term (Map Bool Int) -> [Pred]) -> Specification (Map Bool Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map Bool Int)
m ->
  [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set Bool) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ (Term (Map Bool Int) -> Term (Set Bool)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Bool Int)
m) Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
2
  , Term (Map Bool Int)
-> FunTy (MapList Term (Args (SimpleRep (Bool, Int)))) [Pred]
-> 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 (Map Bool Int)
m (FunTy (MapList Term (Args (SimpleRep (Bool, Int)))) [Pred]
 -> Pred)
-> FunTy (MapList Term (Args (SimpleRep (Bool, Int)))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
k Term Int
v -> [Term Int
v Term Int -> Term Bool -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Bool
k, Term Bool -> Term Bool -> Pred
forall p. IsPred p => Term Bool -> p -> Pred
whenTrue Term Bool
k (Term Int
100 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
v)]
  ]

mapSetSmall :: Specification (Map (Set Int) Int)
mapSetSmall :: Specification (Map (Set Int) Int)
mapSetSmall = (Term (Map (Set Int) Int) -> Pred)
-> Specification (Map (Set Int) Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (Set Int) Int) -> Pred)
 -> Specification (Map (Set Int) Int))
-> (Term (Map (Set Int) Int) -> Pred)
-> Specification (Map (Set Int) Int)
forall a b. (a -> b) -> a -> b
$ \Term (Map (Set Int) Int)
x ->
  Term (Set (Set Int)) -> (Term (Set Int) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Set Int) Int) -> Term (Set (Set Int))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Set Int) Int)
x) ((Term (Set Int) -> Pred) -> Pred)
-> (Term (Set Int) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
d ->
    Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set Int) -> Term (Set Int) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set Int)
d (Term (Set Int) -> Term Bool) -> Term (Set Int) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Set Int -> Term (Set Int)
forall a. HasSpec a => a -> Term a
lit ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
3 .. Int
4])

-- | this tests the function saturatePred
mapIsJust :: Specification (Int, Int)
mapIsJust :: Specification (Int, Int)
mapIsJust = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Specification (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)))) (Term Bool)
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] Term Int
[var| y |] ->
  Term Int -> Term (Maybe Int)
forall a. (HasSpec a, IsNormalType a) => Term a -> Term (Maybe a)
cJust_ Term Int
x Term (Maybe Int) -> Term (Maybe Int) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int -> Term (Map Int Int) -> Term (Maybe Int)
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term (Maybe v)
lookup_ Term Int
y (Map Int Int -> Term (Map Int Int)
forall a. HasSpec a => a -> Term a
lit (Map Int Int -> Term (Map Int Int))
-> Map Int Int -> Term (Map Int Int)
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
z, Int
z) | Int
z <- [Int
100 .. Int
102]])