{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
module Test.IOTasks.Internal.ValueSet (
  ValueSet(..),
  empty, complete, singleton, fromList,
  lessThan, greaterThan,
  union, intersection,
  (\\), with, without,
  complement,
  unique, notInVar,
  embed, embedFromList,
  isEmpty,
  containsValue, initiallyContainsValue,
  showValueSet,
  valueOf,
  Size(..),
  ints, nats, bools, str,
  z3ValueSetConstraint,
  ) where

import Data.Set (Set)
import qualified Data.Set as Set (union,intersection,filter,toList,fromAscList, empty, fromList)
import Type.Reflection

import Test.QuickCheck

import Z3.Monad
import Test.IOTasks.ValueMap (ValueMap, lookupInteger, emptyValueMap, lookupBool, lookupString)
import Test.IOTasks.Var (Var (..), SomeVar (..), someVar, intVar, Embedded (Embedded), Embeddable (..), Varname, varname)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.List (nub)

data ValueSet a where
  Union :: ValueSet a -> ValueSet a -> ValueSet a
  Intersection :: ValueSet a -> ValueSet a -> ValueSet a
  GreaterThan :: Integer -> ValueSet Integer
  LessThan :: Integer -> ValueSet Integer
  Eq :: Integer -> ValueSet Integer
  CurrentlyIn :: VarRef a -> ValueSet a
  CurrentlyNotIn :: VarRef a -> ValueSet a

  Every :: ValueSet a
  None :: ValueSet a
  Embed :: Embeddable a => ValueSet Integer -> ValueSet (Embedded a)

deriving instance Eq (ValueSet a)
deriving instance Ord (ValueSet a)

data VarRef a = Self | Other (Var a)
  deriving (VarRef a -> VarRef a -> Bool
(VarRef a -> VarRef a -> Bool)
-> (VarRef a -> VarRef a -> Bool) -> Eq (VarRef a)
forall a. VarRef a -> VarRef a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. VarRef a -> VarRef a -> Bool
== :: VarRef a -> VarRef a -> Bool
$c/= :: forall a. VarRef a -> VarRef a -> Bool
/= :: VarRef a -> VarRef a -> Bool
Eq,Eq (VarRef a)
Eq (VarRef a) =>
(VarRef a -> VarRef a -> Ordering)
-> (VarRef a -> VarRef a -> Bool)
-> (VarRef a -> VarRef a -> Bool)
-> (VarRef a -> VarRef a -> Bool)
-> (VarRef a -> VarRef a -> Bool)
-> (VarRef a -> VarRef a -> VarRef a)
-> (VarRef a -> VarRef a -> VarRef a)
-> Ord (VarRef a)
VarRef a -> VarRef a -> Bool
VarRef a -> VarRef a -> Ordering
VarRef a -> VarRef a -> VarRef a
forall a. Eq (VarRef a)
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
forall a. VarRef a -> VarRef a -> Bool
forall a. VarRef a -> VarRef a -> Ordering
forall a. VarRef a -> VarRef a -> VarRef a
$ccompare :: forall a. VarRef a -> VarRef a -> Ordering
compare :: VarRef a -> VarRef a -> Ordering
$c< :: forall a. VarRef a -> VarRef a -> Bool
< :: VarRef a -> VarRef a -> Bool
$c<= :: forall a. VarRef a -> VarRef a -> Bool
<= :: VarRef a -> VarRef a -> Bool
$c> :: forall a. VarRef a -> VarRef a -> Bool
> :: VarRef a -> VarRef a -> Bool
$c>= :: forall a. VarRef a -> VarRef a -> Bool
>= :: VarRef a -> VarRef a -> Bool
$cmax :: forall a. VarRef a -> VarRef a -> VarRef a
max :: VarRef a -> VarRef a -> VarRef a
$cmin :: forall a. VarRef a -> VarRef a -> VarRef a
min :: VarRef a -> VarRef a -> VarRef a
Ord)

hasVarRefs :: ValueSet a -> Bool
hasVarRefs :: forall a. ValueSet a -> Bool
hasVarRefs ValueSet a
Every = Bool
False
hasVarRefs ValueSet a
None = Bool
False
hasVarRefs GreaterThan{} = Bool
False
hasVarRefs LessThan{} = Bool
False
hasVarRefs Eq{} = Bool
False
hasVarRefs (Embed ValueSet Integer
vs) = ValueSet Integer -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet Integer
vs
hasVarRefs CurrentlyIn{} = Bool
True
hasVarRefs CurrentlyNotIn{} = Bool
True
hasVarRefs (Union ValueSet a
x ValueSet a
y) = ValueSet a -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet a
x Bool -> Bool -> Bool
|| ValueSet a -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet a
y
hasVarRefs (Intersection ValueSet a
x ValueSet a
y) = ValueSet a -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet a
x Bool -> Bool -> Bool
|| ValueSet a -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet a
y

data Size = Size { Size -> Integer
intAbs :: Integer, Size -> Int
strLen :: Int }

empty :: ValueSet a
empty :: forall a. ValueSet a
empty = ValueSet a
forall a. ValueSet a
None

complete :: ValueSet a
complete :: forall a. ValueSet a
complete = ValueSet a
forall a. ValueSet a
Every

singleton :: Integer -> ValueSet Integer
singleton :: Integer -> ValueSet Integer
singleton = Integer -> ValueSet Integer
Eq

fromList :: [Integer] -> ValueSet Integer
fromList :: [Integer] -> ValueSet Integer
fromList = (Integer -> ValueSet Integer -> ValueSet Integer)
-> ValueSet Integer -> [Integer] -> ValueSet Integer
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ValueSet Integer -> ValueSet Integer -> ValueSet Integer
forall a. ValueSet a -> ValueSet a -> ValueSet a
union (ValueSet Integer -> ValueSet Integer -> ValueSet Integer)
-> (Integer -> ValueSet Integer)
-> Integer
-> ValueSet Integer
-> ValueSet Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ValueSet Integer
singleton) ValueSet Integer
forall a. ValueSet a
empty

unique :: ValueSet a -> ValueSet a
unique :: forall a. ValueSet a -> ValueSet a
unique ValueSet a
vs = VarRef a -> ValueSet a
forall a. VarRef a -> ValueSet a
CurrentlyNotIn VarRef a
forall a. VarRef a
Self ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
`intersection` ValueSet a
vs

notInVar :: ValueSet a -> Var a -> ValueSet a
notInVar :: forall a. ValueSet a -> Var a -> ValueSet a
notInVar ValueSet a
vs Var a
y = VarRef a -> ValueSet a
forall a. VarRef a -> ValueSet a
CurrentlyNotIn (Var a -> VarRef a
forall a. Var a -> VarRef a
Other Var a
y) ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
`intersection` ValueSet a
vs

greaterThan :: Integer -> ValueSet Integer
greaterThan :: Integer -> ValueSet Integer
greaterThan = Integer -> ValueSet Integer
GreaterThan

lessThan :: Integer -> ValueSet Integer
lessThan :: Integer -> ValueSet Integer
lessThan = Integer -> ValueSet Integer
LessThan

union :: ValueSet a -> ValueSet a -> ValueSet a
union :: forall a. ValueSet a -> ValueSet a -> ValueSet a
union = ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
Union

intersection :: ValueSet a -> ValueSet a -> ValueSet a
intersection :: forall a. ValueSet a -> ValueSet a -> ValueSet a
intersection = ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
Intersection

-- | The '(\\)' operator computes set difference.
-- It returns a 'ValueSet' containing all integers of the first set that are not present in the second set.
(\\) :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer
\\ :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer
(\\) ValueSet Integer
xs = (ValueSet Integer
xs `intersection`) (ValueSet Integer -> ValueSet Integer)
-> (ValueSet Integer -> ValueSet Integer)
-> ValueSet Integer
-> ValueSet Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueSet Integer -> ValueSet Integer
forall a. ValueSet a -> ValueSet a
complement

without :: ValueSet Integer -> Integer -> ValueSet Integer
without :: ValueSet Integer -> Integer -> ValueSet Integer
without ValueSet Integer
vs = (ValueSet Integer
vs \\) (ValueSet Integer -> ValueSet Integer)
-> (Integer -> ValueSet Integer) -> Integer -> ValueSet Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ValueSet Integer
singleton

with :: ValueSet Integer -> Integer -> ValueSet Integer
with :: ValueSet Integer -> Integer -> ValueSet Integer
with ValueSet Integer
vs = (ValueSet Integer
vs `union`) (ValueSet Integer -> ValueSet Integer)
-> (Integer -> ValueSet Integer) -> Integer -> ValueSet Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ValueSet Integer
singleton

embed ::  Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
embed :: forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
embed ValueSet Integer
vs
  | ValueSet Integer -> Bool
forall a. ValueSet a -> Bool
hasVarRefs ValueSet Integer
vs = String -> ValueSet (Embedded a)
forall a. HasCallStack => String -> a
error String
"embed: cannot embed value sets with references to variables"
  | Bool
otherwise = ValueSet Integer -> ValueSet (Embedded a)
forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
Embed ValueSet Integer
vs

embedFromList :: Embeddable a => [a] -> ValueSet (Embedded a)
embedFromList :: forall a. Embeddable a => [a] -> ValueSet (Embedded a)
embedFromList = ValueSet Integer -> ValueSet (Embedded a)
forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
embed (ValueSet Integer -> ValueSet (Embedded a))
-> ([a] -> ValueSet Integer) -> [a] -> ValueSet (Embedded a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> ValueSet Integer
fromList ([Integer] -> ValueSet Integer)
-> ([a] -> [Integer]) -> [a] -> ValueSet Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Integer) -> [a] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map a -> Integer
forall a. Embeddable a => a -> Integer
asInteger

complement :: ValueSet a -> ValueSet a
complement :: forall a. ValueSet a -> ValueSet a
complement (GreaterThan Integer
n) = Integer -> ValueSet Integer
LessThan Integer
n ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
`union` Integer -> ValueSet Integer
Eq Integer
n
complement (LessThan Integer
n) =  Integer -> ValueSet Integer
GreaterThan Integer
n ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
`union` Integer -> ValueSet Integer
Eq Integer
n
complement (Intersection ValueSet a
va ValueSet a
vb) = ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
Union (ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a
complement ValueSet a
va) (ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a
complement ValueSet a
vb)
complement (Union ValueSet a
va ValueSet a
vb) = ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
Intersection (ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a
complement ValueSet a
va) (ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a
complement ValueSet a
vb)
complement (Eq Integer
n) = Integer -> ValueSet Integer
GreaterThan Integer
n ValueSet a -> ValueSet a -> ValueSet a
forall a. ValueSet a -> ValueSet a -> ValueSet a
`union` Integer -> ValueSet Integer
LessThan Integer
n
complement (CurrentlyIn VarRef a
x) = VarRef a -> ValueSet a
forall a. VarRef a -> ValueSet a
CurrentlyNotIn VarRef a
x
complement (CurrentlyNotIn VarRef a
x) = VarRef a -> ValueSet a
forall a. VarRef a -> ValueSet a
CurrentlyIn VarRef a
x
complement ValueSet a
Every = ValueSet a
forall a. ValueSet a
None
complement ValueSet a
None = ValueSet a
forall a. ValueSet a
Every
complement (Embed ValueSet Integer
vs) = ValueSet (Embedded a) -> ValueSet (Embedded a)
forall a.
Embeddable a =>
ValueSet (Embedded a) -> ValueSet (Embedded a)
embedComplement (ValueSet Integer -> ValueSet (Embedded a)
forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
Embed ValueSet Integer
vs)
  where
    embedComplement :: forall a. Embeddable a => ValueSet (Embedded a) -> ValueSet (Embedded a)
    embedComplement :: forall a.
Embeddable a =>
ValueSet (Embedded a) -> ValueSet (Embedded a)
embedComplement (Embed ValueSet Integer
vs) = ValueSet Integer -> ValueSet (Embedded a)
forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
Embed ([Integer] -> ValueSet Integer
fromList (forall a. Embeddable a => [Integer]
embeddingRange @a) ValueSet Integer -> ValueSet Integer -> ValueSet Integer
\\ ValueSet Integer
vs)
    embedComplement ValueSet (Embedded a)
x = ValueSet (Embedded a) -> ValueSet (Embedded a)
forall a. ValueSet a -> ValueSet a
complement ValueSet (Embedded a)
x

containsValue :: Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue :: forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
m (Union ValueSet a
vs1 ValueSet a
vs2) a
n = Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
m ValueSet a
vs1  a
n Bool -> Bool -> Bool
|| Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
m ValueSet a
vs2 a
n
containsValue Var a
x ValueMap
m (Intersection ValueSet a
vs1 ValueSet a
vs2) a
n = Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
m ValueSet a
vs1 a
n Bool -> Bool -> Bool
&& Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
m ValueSet a
vs2 a
n
containsValue Var a
_ ValueMap
_ (GreaterThan Integer
i) a
n = a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
Integer
i
containsValue Var a
_ ValueMap
_ (LessThan Integer
i) a
n = a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
Integer
i
containsValue Var a
_ ValueMap
_ (Eq Integer
i) a
n = Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== a
Integer
n
containsValue Var a
x ValueMap
m (CurrentlyIn VarRef a
Self) a
n = Var a -> (Eq a => Bool) -> Bool
forall a r. Var a -> (Eq a => r) -> r
withVarEq Var a
x ((Eq a => Bool) -> Bool) -> (Eq a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ a
n a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn Var a
x ValueMap
m
containsValue Var a
_ ValueMap
m (CurrentlyIn (Other Var a
y)) a
n = Var a -> (Eq a => Bool) -> Bool
forall a r. Var a -> (Eq a => r) -> r
withVarEq Var a
y ((Eq a => Bool) -> Bool) -> (Eq a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ a
n a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn Var a
y ValueMap
m
containsValue Var a
x ValueMap
m (CurrentlyNotIn VarRef a
Self) a
n = Var a -> (Eq a => Bool) -> Bool
forall a r. Var a -> (Eq a => r) -> r
withVarEq Var a
x ((Eq a => Bool) -> Bool) -> (Eq a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ a
n a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn Var a
x ValueMap
m
containsValue Var a
_ ValueMap
m (CurrentlyNotIn (Other Var a
y)) a
n = Var a -> (Eq a => Bool) -> Bool
forall a r. Var a -> (Eq a => r) -> r
withVarEq Var a
y ((Eq a => Bool) -> Bool) -> (Eq a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ a
n a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn Var a
y ValueMap
m
containsValue Var a
_ ValueMap
_ ValueSet a
Every a
_ = Bool
True
containsValue Var a
_ ValueMap
_ ValueSet a
None a
_ = Bool
False
containsValue Var a
_ ValueMap
_ (Embed ValueSet Integer
vs) a
v = ValueSet Integer -> Embedded a -> Bool
forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
vs a
Embedded a
v

withVarEq :: Var a -> (Eq a => r) -> r
withVarEq :: forall a r. Var a -> (Eq a => r) -> r
withVarEq IntVar{} Eq a => r
x = r
Eq a => r
x
withVarEq BoolVar{} Eq a => r
x = r
Eq a => r
x
withVarEq StringVar{} Eq a => r
x = r
Eq a => r
x
withVarEq EmbeddedVar{} Eq a => r
x = r
Eq a => r
x

containsEmbeddedValue :: ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue :: forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
Every Embedded a
_ = Bool
True
containsEmbeddedValue ValueSet Integer
None Embedded a
_ = Bool
False
containsEmbeddedValue (Union ValueSet Integer
a ValueSet Integer
b) Embedded a
v = ValueSet Integer -> Embedded a -> Bool
forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
a Embedded a
v Bool -> Bool -> Bool
|| ValueSet Integer -> Embedded a -> Bool
forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
b Embedded a
v
containsEmbeddedValue (Intersection ValueSet Integer
a ValueSet Integer
b) Embedded a
v = ValueSet Integer -> Embedded a -> Bool
forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
a Embedded a
v Bool -> Bool -> Bool
&& ValueSet Integer -> Embedded a -> Bool
forall a. ValueSet Integer -> Embedded a -> Bool
containsEmbeddedValue ValueSet Integer
b Embedded a
v
containsEmbeddedValue (GreaterThan Integer
i) (Embedded Integer
n) = Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n
containsEmbeddedValue (LessThan Integer
i) (Embedded Integer
n) = Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n
containsEmbeddedValue (Eq Integer
i) (Embedded Integer
n) = Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n
containsEmbeddedValue CurrentlyIn{} Embedded a
_ = String -> Bool
forall a. HasCallStack => String -> a
error String
"not allowed"
containsEmbeddedValue CurrentlyNotIn{} Embedded a
_ = String -> Bool
forall a. HasCallStack => String -> a
error String
"not allowed"

valuesIn :: Var a -> ValueMap -> [a]
valuesIn :: forall a. Var a -> ValueMap -> [a]
valuesIn x :: Var a
x@IntVar{} ValueMap
env =
  case SomeVar -> ValueMap -> Maybe [(Integer, Int)]
lookupInteger (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
env of
    Just [(Integer, Int)]
values -> ((a, Int) -> a) -> [(a, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Int) -> a
forall a b. (a, b) -> a
fst [(a, Int)]
[(Integer, Int)]
values
    Maybe [(Integer, Int)]
Nothing -> String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot find values for variable", Var a -> String
forall a. Show a => a -> String
show Var a
x , String
"in", ValueMap -> String
forall a. Show a => a -> String
show ValueMap
env, String
"(perhaps you misspelled a variable name)"]
valuesIn x :: Var a
x@(EmbeddedVar (TypeRep a1
ty :: TypeRep x) String
_) ValueMap
env =
  case SomeVar -> ValueMap -> Maybe [(Integer, Int)]
lookupInteger (TypeRep a1 -> (Typeable a1 => SomeVar) -> SomeVar
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep a1
ty ((Typeable a1 => SomeVar) -> SomeVar)
-> (Typeable a1 => SomeVar) -> SomeVar
forall a b. (a -> b) -> a -> b
$ Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
env of
    Just [(Integer, Int)]
values -> ((Integer, Int) -> a) -> [(Integer, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> a
Integer -> Embedded a1
forall a. (Show a, Embeddable a) => Integer -> Embedded a
Embedded (Integer -> a)
-> ((Integer, Int) -> Integer) -> (Integer, Int) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Int) -> Integer
forall a b. (a, b) -> a
fst) [(Integer, Int)]
values
    Maybe [(Integer, Int)]
Nothing -> String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot find values for variable", Var a -> String
forall a. Show a => a -> String
show Var a
x , String
"in", ValueMap -> String
forall a. Show a => a -> String
show ValueMap
env, String
"(perhaps you misspelled a variable name)"]
valuesIn x :: Var a
x@BoolVar{} ValueMap
env =
  case SomeVar -> ValueMap -> Maybe [(Bool, Int)]
lookupBool (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
env of
    Just [(Bool, Int)]
values -> ((a, Int) -> a) -> [(a, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Int) -> a
forall a b. (a, b) -> a
fst [(a, Int)]
[(Bool, Int)]
values
    Maybe [(Bool, Int)]
Nothing -> String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot find values for variable", Var a -> String
forall a. Show a => a -> String
show Var a
x , String
"in", ValueMap -> String
forall a. Show a => a -> String
show ValueMap
env, String
"(perhaps you misspelled a variable name)"]
valuesIn x :: Var a
x@StringVar{} ValueMap
env =
  case SomeVar -> ValueMap -> Maybe [(String, Int)]
lookupString (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
env of
    Just [(String, Int)]
values -> ((a, Int) -> a) -> [(a, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Int) -> a
forall a b. (a, b) -> a
fst [(a, Int)]
[(String, Int)]
values
    Maybe [(String, Int)]
Nothing -> String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot find values for variable", Var a -> String
forall a. Show a => a -> String
show Var a
x , String
"in", ValueMap -> String
forall a. Show a => a -> String
show ValueMap
env, String
"(perhaps you misspelled a variable name)"]


initiallyContainsValue ::  ValueSet Integer -> Integer -> Bool
initiallyContainsValue :: ValueSet Integer -> Integer -> Bool
initiallyContainsValue = Var Integer -> ValueMap -> ValueSet Integer -> Integer -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue (String -> Var Integer
intVar String
"x") (ValueMap -> ValueSet Integer -> Integer -> Bool)
-> ValueMap -> ValueSet Integer -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ [SomeVar] -> ValueMap
emptyValueMap [Var Integer -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar (Var Integer -> SomeVar) -> Var Integer -> SomeVar
forall a b. (a -> b) -> a -> b
$ String -> Var Integer
intVar String
"x"]

valueOf :: Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf :: forall a. Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf Var a
_ ValueMap
_ ValueSet a
None = String -> Size -> Gen a
forall a. HasCallStack => String -> a
error String
"valueOf: cannot draw value from empty value set"
valueOf x :: Var a
x@IntVar{} ValueMap
m ValueSet a
vs = Var Integer -> ValueMap -> ValueSet Integer -> Size -> Gen Integer
valueOfInt Var a
Var Integer
x ValueMap
m ValueSet a
ValueSet Integer
vs
valueOf x :: Var a
x@BoolVar{} ValueMap
m ValueSet a
vs = Gen Bool -> Size -> Gen Bool
forall a b. a -> b -> a
const (Gen Bool -> Size -> Gen Bool) -> Gen Bool -> Size -> Gen Bool
forall a b. (a -> b) -> a -> b
$ Var Bool -> ValueMap -> ValueSet Bool -> Gen Bool
valueOfBool Var a
Var Bool
x ValueMap
m ValueSet a
ValueSet Bool
vs
valueOf x :: Var a
x@StringVar{} ValueMap
m ValueSet a
vs = Var String -> ValueMap -> ValueSet String -> Size -> Gen String
valueOfString Var a
Var String
x ValueMap
m ValueSet a
ValueSet String
vs
valueOf x :: Var a
x@EmbeddedVar{} ValueMap
m ValueSet a
vs = Var (Embedded a1)
-> ValueMap -> ValueSet (Embedded a1) -> Size -> Gen (Embedded a1)
forall a.
Var (Embedded a)
-> ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a)
valueOfEmbedded Var a
Var (Embedded a1)
x ValueMap
m ValueSet a
ValueSet (Embedded a1)
vs

valueOfInt :: Var Integer -> ValueMap -> ValueSet Integer -> Size -> Gen Integer
valueOfInt :: Var Integer -> ValueMap -> ValueSet Integer -> Size -> Gen Integer
valueOfInt (IntVar String
x) = (Integer -> Integer)
-> (String -> Var Integer)
-> (Size -> [Integer])
-> String
-> ValueMap
-> ValueSet Integer
-> Size
-> Gen Integer
forall a.
(Typeable a, Eq a) =>
(Integer -> a)
-> (String -> Var a)
-> (Size -> [Integer])
-> String
-> ValueMap
-> ValueSet a
-> Size
-> Gen a
valueOfIntOrEmbedded Integer -> Integer
forall a. a -> a
id String -> Var Integer
IntVar (\(Size Integer
sz Int
_) -> [-Integer
sz..Integer
sz]) String
x

valueOfEmbedded :: Var (Embedded a) -> ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a)
valueOfEmbedded :: forall a.
Var (Embedded a)
-> ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a)
valueOfEmbedded (EmbeddedVar (TypeRep a1
ty :: TypeRep x) String
x) = TypeRep a1
-> (Typeable a1 =>
    ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a))
-> ValueMap
-> ValueSet (Embedded a)
-> Size
-> Gen (Embedded a)
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep a1
ty ((Typeable a1 =>
  ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a))
 -> ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a))
-> (Typeable a1 =>
    ValueMap -> ValueSet (Embedded a) -> Size -> Gen (Embedded a))
-> ValueMap
-> ValueSet (Embedded a)
-> Size
-> Gen (Embedded a)
forall a b. (a -> b) -> a -> b
$ (Integer -> Embedded a)
-> (String -> Var (Embedded a))
-> (Size -> [Integer])
-> String
-> ValueMap
-> ValueSet (Embedded a)
-> Size
-> Gen (Embedded a)
forall a.
(Typeable a, Eq a) =>
(Integer -> a)
-> (String -> Var a)
-> (Size -> [Integer])
-> String
-> ValueMap
-> ValueSet a
-> Size
-> Gen a
valueOfIntOrEmbedded Integer -> Embedded a
forall a. (Show a, Embeddable a) => Integer -> Embedded a
Embedded (TypeRep a -> String -> Var (Embedded a)
forall a1.
(Embeddable a1, Show a1, Read a1) =>
TypeRep a1 -> String -> Var (Embedded a1)
EmbeddedVar TypeRep a
TypeRep a1
ty) ([Integer] -> Size -> [Integer]
forall a b. a -> b -> a
const ([Integer] -> Size -> [Integer]) -> [Integer] -> Size -> [Integer]
forall a b. (a -> b) -> a -> b
$ forall a. Embeddable a => [Integer]
embeddingRange @x) String
x

valueOfIntOrEmbedded :: (Typeable a, Eq a) => (Integer -> a) -> (Varname -> Var a) -> (Size -> [Integer]) -> Varname -> ValueMap -> ValueSet a -> Size -> Gen a
valueOfIntOrEmbedded :: forall a.
(Typeable a, Eq a) =>
(Integer -> a)
-> (String -> Var a)
-> (Size -> [Integer])
-> String
-> ValueMap
-> ValueSet a
-> Size
-> Gen a
valueOfIntOrEmbedded Integer -> a
f String -> Var a
g Size -> [Integer]
h String
x ValueMap
m ValueSet a
vs Size
sz =
  case Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList (Set Integer -> [Integer]) -> Set Integer -> [Integer]
forall a b. (a -> b) -> a -> b
$ ValueSet a -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet a
vs (Set Integer -> Set Integer) -> Set Integer -> Set Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Set Integer
forall a. Eq a => [a] -> Set a
Set.fromAscList (Size -> [Integer]
h Size
sz) of
    [] -> String -> Gen a
forall a. HasCallStack => String -> a
error (String -> Gen a) -> String -> Gen a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"valueOf: no values within size limits for",ValueSet a -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet a
vs]
    [Integer]
xs -> Integer -> a
f (Integer -> a) -> Gen Integer -> Gen a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer] -> Gen Integer
forall a. [a] -> Gen a
elements [Integer]
xs
  where
    range :: ValueSet a -> Set Integer -> Set Integer
    range :: forall a. ValueSet a -> Set Integer -> Set Integer
range (Union ValueSet a
x ValueSet a
y) Set Integer
r = ValueSet a -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet a
x Set Integer
r Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ValueSet a -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet a
y Set Integer
r
    range (Intersection ValueSet a
x ValueSet a
y) Set Integer
r = ValueSet a -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet a
x Set Integer
r Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` ValueSet a -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet a
y Set Integer
r
    range (GreaterThan Integer
n) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
n) Set Integer
r
    range (LessThan Integer
n) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<Integer
n) Set Integer
r
    range (Eq Integer
n) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
n) Set Integer
r
    range (CurrentlyIn VarRef a
Self) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
v -> Integer -> a
f Integer
v a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn (String -> Var a
g String
x) ValueMap
m) Set Integer
r
    range (CurrentlyIn (Other Var a
y)) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
v -> Integer -> a
f Integer
v a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn (String -> Var a
g (String -> Var a) -> String -> Var a
forall a b. (a -> b) -> a -> b
$ Var a -> String
forall a. Var a -> String
varname Var a
y) ValueMap
m) Set Integer
r
    range (CurrentlyNotIn VarRef a
Self) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
v -> Integer -> a
f Integer
v a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn (String -> Var a
g String
x) ValueMap
m) Set Integer
r
    range (CurrentlyNotIn (Other Var a
y)) Set Integer
r = (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
v -> Integer -> a
f Integer
v a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var a -> ValueMap -> [a]
forall a. Var a -> ValueMap -> [a]
valuesIn (String -> Var a
g (String -> Var a) -> String -> Var a
forall a b. (a -> b) -> a -> b
$ Var a -> String
forall a. Var a -> String
varname Var a
y) ValueMap
m) Set Integer
r
    range ValueSet a
Every Set Integer
r = Set Integer
r
    range ValueSet a
None Set Integer
_ = Set Integer
forall a. Set a
Set.empty
    range (Embed ValueSet Integer
vs) Set Integer
r = ValueSet Integer -> Set Integer -> Set Integer
forall a. ValueSet a -> Set Integer -> Set Integer
range ValueSet Integer
vs Set Integer
r

valueOfBool :: Var Bool -> ValueMap -> ValueSet Bool -> Gen Bool
valueOfBool :: Var Bool -> ValueMap -> ValueSet Bool -> Gen Bool
valueOfBool Var Bool
x ValueMap
m ValueSet Bool
vs =
  case Set Bool -> [Bool]
forall a. Set a -> [a]
Set.toList (Set Bool -> [Bool]) -> Set Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ ValueSet Bool -> Set Bool -> Set Bool
range ValueSet Bool
vs (Set Bool -> Set Bool) -> Set Bool -> Set Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Set Bool
forall a. Ord a => [a] -> Set a
Set.fromList [Bool
True,Bool
False] of
    [] -> String -> Gen Bool
forall a. HasCallStack => String -> a
error (String -> Gen Bool) -> String -> Gen Bool
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"valueOf: no boolean values between for",ValueSet Bool -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet Bool
vs]
    [Bool]
xs -> [Bool] -> Gen Bool
forall a. [a] -> Gen a
elements [Bool]
xs
  where
    range :: ValueSet Bool -> Set Bool -> Set Bool
    range :: ValueSet Bool -> Set Bool -> Set Bool
range (Union ValueSet Bool
x ValueSet Bool
y) Set Bool
r = ValueSet Bool -> Set Bool -> Set Bool
range ValueSet Bool
x Set Bool
r Set Bool -> Set Bool -> Set Bool
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ValueSet Bool -> Set Bool -> Set Bool
range ValueSet Bool
y Set Bool
r
    range (Intersection ValueSet Bool
x ValueSet Bool
y) Set Bool
r = ValueSet Bool -> Set Bool -> Set Bool
range ValueSet Bool
x Set Bool
r Set Bool -> Set Bool -> Set Bool
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` ValueSet Bool -> Set Bool -> Set Bool
range ValueSet Bool
y Set Bool
r
    range (CurrentlyIn VarRef Bool
Self) Set Bool
r = (Bool -> Bool) -> Set Bool -> Set Bool
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Bool
v -> Bool
v Bool -> [Bool] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var Bool -> ValueMap -> [Bool]
forall a. Var a -> ValueMap -> [a]
valuesIn Var Bool
x ValueMap
m) Set Bool
r
    range (CurrentlyIn (Other Var Bool
y)) Set Bool
r = (Bool -> Bool) -> Set Bool -> Set Bool
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Bool
v -> Bool
v Bool -> [Bool] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Var Bool -> ValueMap -> [Bool]
forall a. Var a -> ValueMap -> [a]
valuesIn Var Bool
y ValueMap
m) Set Bool
r
    range (CurrentlyNotIn VarRef Bool
Self) Set Bool
r = (Bool -> Bool) -> Set Bool -> Set Bool
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Bool
v -> Bool
v Bool -> [Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var Bool -> ValueMap -> [Bool]
forall a. Var a -> ValueMap -> [a]
valuesIn Var Bool
x ValueMap
m) Set Bool
r
    range (CurrentlyNotIn (Other Var Bool
y)) Set Bool
r = (Bool -> Bool) -> Set Bool -> Set Bool
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Bool
v -> Bool
v Bool -> [Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Var Bool -> ValueMap -> [Bool]
forall a. Var a -> ValueMap -> [a]
valuesIn Var Bool
y ValueMap
m) Set Bool
r
    range ValueSet Bool
Every Set Bool
r = Set Bool
r
    range ValueSet Bool
None Set Bool
_ = Set Bool
forall a. Set a
Set.empty

valueOfString :: Var String -> ValueMap -> ValueSet String -> Size -> Gen String
valueOfString :: Var String -> ValueMap -> ValueSet String -> Size -> Gen String
valueOfString Var String
x ValueMap
m ValueSet String
vs (Size Integer
_ Int
len) =
  case Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
x ValueMap
m ValueSet String
vs of
    FromThese [] -> String -> Gen String
forall a. HasCallStack => String -> a
error (String -> Gen String) -> String -> Gen String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"valueOf: no string values for", ValueSet String -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet String
vs]
    FromThese [String]
xs -> [String] -> Gen String
forall a. [a] -> Gen a
elements ([String] -> Gen String) -> [String] -> Gen String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String]
xs
    NotThese [String]
xs -> Int -> Gen String -> Gen String
forall a. Int -> Gen a -> Gen a
resize Int
len (Gen Char -> Gen String
forall a. Gen a -> Gen [a]
listOf (Gen Char -> Gen String) -> Gen Char -> Gen String
forall a b. (a -> b) -> a -> b
$ String -> Gen Char
forall a. [a] -> Gen a
elements [Char
'a'..Char
'z']) Gen String -> (String -> Bool) -> Gen String
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
xs)

data Str = FromThese [String] | NotThese [String]

reduceStringSet :: Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet :: Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
_ ValueMap
_ ValueSet String
Every = [String] -> Str
NotThese []
reduceStringSet Var String
_ ValueMap
_ ValueSet String
None = [String] -> Str
FromThese []
reduceStringSet Var String
x ValueMap
m (CurrentlyIn VarRef String
Self) = [String] -> Str
FromThese (Var String -> ValueMap -> [String]
forall a. Var a -> ValueMap -> [a]
valuesIn Var String
x ValueMap
m)
reduceStringSet Var String
_ ValueMap
m (CurrentlyIn (Other Var String
y)) = [String] -> Str
FromThese (Var String -> ValueMap -> [String]
forall a. Var a -> ValueMap -> [a]
valuesIn Var String
y ValueMap
m)
reduceStringSet Var String
x ValueMap
m (CurrentlyNotIn VarRef String
Self) = [String] -> Str
NotThese (Var String -> ValueMap -> [String]
forall a. Var a -> ValueMap -> [a]
valuesIn Var String
x ValueMap
m)
reduceStringSet Var String
_ ValueMap
m (CurrentlyNotIn (Other Var String
y)) = [String] -> Str
NotThese (Var String -> ValueMap -> [String]
forall a. Var a -> ValueMap -> [a]
valuesIn Var String
y ValueMap
m)
reduceStringSet Var String
x ValueMap
m (Union ValueSet String
a ValueSet String
b) = case (Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
x ValueMap
m ValueSet String
a, Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
x ValueMap
m ValueSet String
b) of
  (FromThese [String]
xs, FromThese [String]
ys) -> [String] -> Str
FromThese ([String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ys)
  (FromThese [String]
xs, NotThese [String]
ys) -> [String] -> Str
NotThese [ String
y | String
y <- [String]
ys, String
y String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
xs ]
  (NotThese [String]
xs, FromThese [String]
ys) -> [String] -> Str
NotThese [ String
x | String
x <- [String]
xs, String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
ys ]
  (NotThese [String]
xs, NotThese [String]
ys) -> [String] -> Str
NotThese [ String
x | String
x <- [String]
xs, String
x String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
ys ]
reduceStringSet Var String
x ValueMap
m (Intersection ValueSet String
a ValueSet String
b) = case (Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
x ValueMap
m ValueSet String
a, Var String -> ValueMap -> ValueSet String -> Str
reduceStringSet Var String
x ValueMap
m ValueSet String
b) of
  (FromThese [String]
xs, FromThese [String]
ys) -> [String] -> Str
FromThese [ String
x | String
x <- [String]
xs, String
x String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
ys]
  (FromThese [String]
xs, NotThese [String]
ys) -> [String] -> Str
FromThese  [ String
x | String
x <- [String]
xs, String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
ys ]
  (NotThese [String]
xs, FromThese [String]
ys) -> [String] -> Str
FromThese [ String
y | String
y <- [String]
ys, String
y String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
xs ]
  (NotThese [String]
xs, NotThese [String]
ys) -> [String] -> Str
NotThese ([String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ys)

showValueSet :: Typeable a => ValueSet a -> String
showValueSet :: forall a. Typeable a => ValueSet a -> String
showValueSet = ValueSet a -> String
forall a. Typeable a => ValueSet a -> String
go where
  go :: forall a. Typeable a => ValueSet a -> String
  go :: forall a. Typeable a => ValueSet a -> String
go ValueSet a
vs = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"{ v : ",TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a), String
" | ", ValueSet a -> String
forall a. ValueSet a -> String
showValueSet' ValueSet a
vs ,String
"}"]

  showValueSet' :: ValueSet a -> String
  showValueSet' :: forall a. ValueSet a -> String
showValueSet' (Union ValueSet a
vs1 ValueSet a
vs2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(",ValueSet a -> String
forall a. ValueSet a -> String
showValueSet' ValueSet a
vs1,String
") \\/ (", ValueSet a -> String
forall a. ValueSet a -> String
showValueSet' ValueSet a
vs2,String
")"]
  showValueSet' (Intersection ValueSet a
vs1 ValueSet a
vs2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(",ValueSet a -> String
forall a. ValueSet a -> String
showValueSet' ValueSet a
vs1,String
") /\\ (", ValueSet a -> String
forall a. ValueSet a -> String
showValueSet' ValueSet a
vs2,String
")"]
  showValueSet' (GreaterThan Integer
n) = String
"v > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
  showValueSet' (LessThan Integer
n) = String
"v < " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
  showValueSet' (Eq Integer
n) = String
"v == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
  showValueSet' (CurrentlyIn VarRef a
ref) = String
"currentlyIn " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarRef a -> String
forall {a}. VarRef a -> String
showVarRef VarRef a
ref
  showValueSet' (CurrentlyNotIn VarRef a
ref) = String
"currentlyNotIn " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarRef a -> String
forall {a}. VarRef a -> String
showVarRef VarRef a
ref
  showValueSet' ValueSet a
Every = String
"true"
  showValueSet' ValueSet a
None = String
"false"
  showValueSet' (Embed ValueSet Integer
vs) = String
"Embed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ValueSet Integer -> String
forall a. ValueSet a -> String
showValueSet' ValueSet Integer
vs

  showVarRef :: VarRef a -> String
showVarRef VarRef a
Self = String
"self"
  showVarRef (Other Var a
y) = Var a -> String
forall a. Show a => a -> String
show Var a
y

-- basic ValueSets
ints, nats :: ValueSet Integer
ints :: ValueSet Integer
ints = ValueSet Integer
forall a. ValueSet a
Every
nats :: ValueSet Integer
nats = Integer -> ValueSet Integer
Eq Integer
0 ValueSet Integer -> ValueSet Integer -> ValueSet Integer
forall a. ValueSet a -> ValueSet a -> ValueSet a
`Union` Integer -> ValueSet Integer
GreaterThan Integer
0

bools :: ValueSet Bool
bools :: ValueSet Bool
bools = ValueSet Bool
forall a. ValueSet a
complete

str :: ValueSet String
str :: ValueSet String
str = ValueSet String
forall a. ValueSet a
Every

--
-- | Check if a given 'ValueSet' of integers is empty.
--
-- This function uses an external SMT solver to check the constraints defined by the 'ValueSet'.
isEmpty :: Var Integer -> Map SomeVar [AST] -> ValueSet Integer -> IO Bool
isEmpty :: Var Integer -> Map SomeVar [AST] -> ValueSet Integer -> IO Bool
isEmpty Var Integer
var Map SomeVar [AST]
m ValueSet Integer
vs = Z3 Bool -> IO Bool
forall a. Z3 a -> IO a
evalZ3 (Z3 Bool -> IO Bool) -> Z3 Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
  AST
x <- Symbol -> Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Symbol -> z3 AST
mkIntVar (Symbol -> Z3 AST) -> Z3 Symbol -> Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> Z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol String
"x"
  AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 ()
assert (AST -> Z3 ()) -> Z3 AST -> Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Var Integer
-> Map SomeVar [AST] -> ValueSet Integer -> AST -> Z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var Integer
var Map SomeVar [AST]
m ValueSet Integer
vs AST
x
  Result
res <- Z3 Result
forall (z3 :: * -> *). MonadZ3 z3 => z3 Result
check
  Bool -> Z3 Bool
forall a. a -> Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Z3 Bool) -> Bool -> Z3 Bool
forall a b. (a -> b) -> a -> b
$ case Result
res of
    Result
Sat -> Bool
False
    Result
Unsat -> Bool
True
    Result
Undef -> String -> Bool
forall a. HasCallStack => String -> a
error String
"isEmpty: could not solve SMT constraints"

z3ValueSetConstraint :: MonadZ3 z3 => Typeable a => Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint :: forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m (Union ValueSet a
x ValueSet a
y) AST
xVar = do
  AST
cx <- Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m ValueSet a
x AST
xVar
  AST
cy <- Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m ValueSet a
y AST
xVar
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr [AST
cx,AST
cy]
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m (Intersection ValueSet a
x ValueSet a
y) AST
xVar = do
  AST
cx <- Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m ValueSet a
x AST
xVar
  AST
cy <- Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m ValueSet a
y AST
xVar
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd [AST
cx,AST
cy]
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
_ (GreaterThan Integer
n) AST
xVar = Integer -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Integer
n z3 AST -> (AST -> z3 AST) -> z3 AST
forall a b. z3 a -> (a -> z3 b) -> z3 b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkGt AST
xVar
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
_ (LessThan Integer
n) AST
xVar = Integer -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Integer
n z3 AST -> (AST -> z3 AST) -> z3 AST
forall a b. z3 a -> (a -> z3 b) -> z3 b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkLt AST
xVar
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
_ (Eq Integer
n) AST
xVar = Integer -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Integer
n z3 AST -> (AST -> z3 AST) -> z3 AST
forall a b. z3 a -> (a -> z3 b) -> z3 b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xVar
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m (CurrentlyIn VarRef a
Self) AST
xVar = do
  let xs :: [AST]
xs = [AST] -> Maybe [AST] -> [AST]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [AST] -> [AST]) -> Maybe [AST] -> [AST]
forall a b. (a -> b) -> a -> b
$ SomeVar -> Map SomeVar [AST] -> Maybe [AST]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
var) Map SomeVar [AST]
m
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr ([AST] -> z3 AST) -> z3 [AST] -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [z3 AST] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xVar AST
x | AST
x <- [AST]
xs, AST
x AST -> AST -> Bool
forall a. Eq a => a -> a -> Bool
/= AST
xVar]
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
m (CurrentlyIn (Other Var a
y)) AST
xVar = do
  let xs :: [AST]
xs = [AST] -> Maybe [AST] -> [AST]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [AST] -> [AST]) -> Maybe [AST] -> [AST]
forall a b. (a -> b) -> a -> b
$ SomeVar -> Map SomeVar [AST] -> Maybe [AST]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
y) Map SomeVar [AST]
m
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr ([AST] -> z3 AST) -> z3 [AST] -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [z3 AST] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xVar AST
x | AST
x <- [AST]
xs, AST
x AST -> AST -> Bool
forall a. Eq a => a -> a -> Bool
/= AST
xVar]
z3ValueSetConstraint Var a
var Map SomeVar [AST]
m (CurrentlyNotIn VarRef a
Self) AST
xVar = do
  let xs :: [AST]
xs = [AST] -> Maybe [AST] -> [AST]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [AST] -> [AST]) -> Maybe [AST] -> [AST]
forall a b. (a -> b) -> a -> b
$ SomeVar -> Map SomeVar [AST] -> Maybe [AST]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
var) Map SomeVar [AST]
m
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd ([AST] -> z3 AST) -> z3 [AST] -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [z3 AST] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkNot (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xVar AST
x | AST
x <- [AST]
xs, AST
x AST -> AST -> Bool
forall a. Eq a => a -> a -> Bool
/= AST
xVar]
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
m (CurrentlyNotIn (Other Var a
y)) AST
xVar = do
  let xs :: [AST]
xs = [AST] -> Maybe [AST] -> [AST]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [AST] -> [AST]) -> Maybe [AST] -> [AST]
forall a b. (a -> b) -> a -> b
$ SomeVar -> Map SomeVar [AST] -> Maybe [AST]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
y) Map SomeVar [AST]
m
  [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd ([AST] -> z3 AST) -> z3 [AST] -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [z3 AST] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkNot (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xVar AST
x | AST
x <- [AST]
xs, AST
x AST -> AST -> Bool
forall a. Eq a => a -> a -> Bool
/= AST
xVar]
z3ValueSetConstraint x :: Var a
x@(EmbeddedVar (TypeRep a1
_ :: TypeRep x) String
_) Map SomeVar [AST]
m ValueSet a
Every AST
xVar = Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var a
x Map SomeVar [AST]
m (ValueSet Integer -> ValueSet (Embedded a1)
forall a. Embeddable a => ValueSet Integer -> ValueSet (Embedded a)
Embed (ValueSet Integer -> ValueSet (Embedded a1))
-> ValueSet Integer -> ValueSet (Embedded a1)
forall a b. (a -> b) -> a -> b
$ [Integer] -> ValueSet Integer
fromList (forall a. Embeddable a => [Integer]
embeddingRange @x)) AST
xVar
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
_ ValueSet a
Every AST
_ = z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkTrue
z3ValueSetConstraint Var a
_ Map SomeVar [AST]
_ ValueSet a
None AST
_ = z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse
z3ValueSetConstraint (EmbeddedVar TypeRep a1
_ String
x) Map SomeVar [AST]
m (Embed ValueSet Integer
vs) AST
xVar = Var Integer
-> Map SomeVar [AST] -> ValueSet Integer -> AST -> z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint (String -> Var Integer
intVar String
x) Map SomeVar [AST]
m ValueSet Integer
vs AST
xVar