module CSPM.Evaluator.ValueSet where
import Control.Monad
import qualified Data.Set as S
import CSPM.Evaluator.Values
import qualified CSPM.Compiler.Events as CE
import qualified CSPM.Compiler.Set as CS
import Util.Exception
import Util.PrettyPrint hiding (empty)
data ValueSet =
Integers
| Processes
| ExplicitSet (S.Set Value)
| IntSetFrom Integer
| RangedSet Integer Integer
| LazySet [Value]
instance Eq ValueSet where
Integers == Integers = True
Processes == Processes = True
IntSetFrom lb1 == IntSetFrom lb2 = lb1 == lb2
RangedSet lb1 ub1 == RangedSet lb2 ub2 = lb1 == lb2 && ub1 == ub2
ExplicitSet s1 == ExplicitSet s2 = s1 == s2
ExplicitSet s == RangedSet lb ub = s == S.fromList (map VInt [lb..ub])
RangedSet lb ub == ExplicitSet s = s == S.fromList (map VInt [lb..ub])
_ == _ = panic "Cannot compare sets"
instance Ord ValueSet where
compare (ExplicitSet s1) (ExplicitSet s2) = compare s1 s2
instance PrettyPrintable ValueSet where
prettyPrint Integers = text "Integers"
prettyPrint Processes = text "Proc"
prettyPrint (IntSetFrom lb) = braces (integer lb <> text "...")
prettyPrint (RangedSet lb ub) =
braces (integer lb <> text "..." <> integer ub)
prettyPrint (ExplicitSet s) =
braces (list (map prettyPrint $ S.toList s))
prettyPrint (LazySet vs) =
braces (list (map prettyPrint vs))
instance Show ValueSet where
show = show . prettyPrint
cartesianProduct :: ([Value] -> Value) -> [ValueSet] -> ValueSet
cartesianProduct vc = fromList . map vc . sequence . map toList
powerset :: ValueSet -> ValueSet
powerset = fromList . map (VSet . fromList) .
filterM (\x -> [True, False]) . toList
allSequences :: ValueSet -> ValueSet
allSequences s = if empty s then emptySet else
let
itemsAsList :: [Value]
itemsAsList = toList s
list :: Integer -> [Value]
list 0 = [VList []]
list n = concatMap (\x -> map (app x) (list (n1))) itemsAsList
where
app :: Value -> Value -> Value
app x (VList xs) = VList $ x:xs
in LazySet (list 0)
emptySet :: ValueSet
emptySet = ExplicitSet S.empty
fromList :: [Value] -> ValueSet
fromList = ExplicitSet . S.fromList
toList :: ValueSet -> [Value]
toList (ExplicitSet s) = S.toList s
toList (RangedSet lb ub) = map VInt [lb..ub]
toList (IntSetFrom lb) = map VInt [lb..]
toList (LazySet xs) = xs
singletonValue :: ValueSet -> Maybe Value
singletonValue s = if card s == 1 then Just (head (toList s)) else Nothing
member :: Value -> ValueSet -> Bool
member v (ExplicitSet s) = S.member v s
member (VInt i) Integers = True
member (VInt i) (IntSetFrom lb) = i >= lb
member (VInt i) (RangedSet lb ub) = i >= lb && i <= ub
member v (LazySet xs) = v `elem` xs
card :: ValueSet -> Integer
card (ExplicitSet s) = toInteger (S.size s)
card (RangedSet lb ub) = ublb+1
empty :: ValueSet -> Bool
empty Processes = panic "empty(Processes) Not implemented"
empty (ExplicitSet s) = S.null s
empty (IntSetFrom lb) = False
empty (Integers) = False
empty (RangedSet lb ub) = False
empty (LazySet xs) =
case xs of
x:_ -> False
_ -> True
mapMonotonic :: (Value -> Value) -> ValueSet -> ValueSet
mapMonotonic f (ExplicitSet s) = ExplicitSet $ S.mapMonotonic f s
unions :: [ValueSet] -> ValueSet
unions vs = foldr union (ExplicitSet S.empty) vs
intersections :: [ValueSet] -> ValueSet
intersections vs = panic "Unions not implemented"
union :: ValueSet -> ValueSet -> ValueSet
union (ExplicitSet s1) (ExplicitSet s2) =
ExplicitSet (S.union s1 s2)
union (IntSetFrom lb1) (IntSetFrom lb2) =
IntSetFrom (min lb1 lb2)
union (IntSetFrom lb) Integers =Integers
union Integers (IntSetFrom lb) =Integers
union (IntSetFrom lb1) (RangedSet lb2 ub2) | lb1 <= ub2 =
IntSetFrom (min lb1 lb2)
union (RangedSet lb2 ub2) (IntSetFrom lb1) | lb1 <= ub2 =
IntSetFrom (min lb1 lb2)
union x y | x == y = x
intersection :: ValueSet -> ValueSet -> ValueSet
intersection (ExplicitSet s1) (ExplicitSet s2) =
ExplicitSet (S.intersection s1 s2)
intersection (IntSetFrom lb1) (IntSetFrom lb2) =
IntSetFrom (min lb1 lb2)
intersection (IntSetFrom lb) Integers =IntSetFrom lb
intersection Integers (IntSetFrom lb) =IntSetFrom lb
intersection (IntSetFrom lb1) (RangedSet lb2 ub2) =
if lb1 <= ub2 then RangedSet (max lb2 lb1) ub2
else ExplicitSet S.empty
intersection (RangedSet lb2 ub2) (IntSetFrom lb1) | lb1 <= ub2 =
intersection (IntSetFrom lb1) (RangedSet lb2 ub2)
inter x y | x == y = x
difference :: ValueSet -> ValueSet -> ValueSet
difference (ExplicitSet s1) (ExplicitSet s2) =
ExplicitSet (S.difference s1 s2)
difference (IntSetFrom lb1) (IntSetFrom lb2) =
if lb1 < lb2 then RangedSet lb1 (lb21)
else ExplicitSet S.empty
difference (IntSetFrom lb) Integers = ExplicitSet S.empty
difference x y | x == y = ExplicitSet S.empty
valueSetToEventSet :: ValueSet -> CE.EventSet
valueSetToEventSet = CS.fromList . map valueEventToEvent . toList