implement simple dependent value sets

src/Test/IOTasks.hs

@@ -10,6 +10,7 @@ module Test.IOTasks (
   union, intersection,
   (\\), with, without,
   complement,
+  unique, notInVar,
   isEmpty,
   ints, nats, str,
   OutputPattern,

src/Test/IOTasks/Constraints.hs

@@ -12,6 +12,7 @@ module Test.IOTasks.Constraints (
   partitionPath, pathDepth,
   numberOfPaths,
   showPath, showConstraint, showSomeConstraint,
+  ix
   ) where
 
 import Test.IOTasks.ValueSet
@@ -30,7 +31,7 @@ import Data.Tuple.Extra (fst3)
 import Data.Typeable
 
 data Constraint (t :: ConstraintType) where
-  InputConstraint :: Typeable v => (Var v, Int) -> ValueSet v -> Constraint 'Input
+  InputConstraint :: Typeable v => (Var v, Int) -> ValueSet v -> Map SomeVar (Int, [Int]) -> Constraint 'Input
   ConditionConstraint :: Term 'Transparent Bool -> Map SomeVar (Int, [Int]) -> Constraint 'Condition
   OverflowConstraints :: [Term 'Transparent Integer] -> Map SomeVar (Int, [Int]) -> Constraint 'Overflow
 
@@ -51,8 +52,8 @@ constraintTree negMax =
     (\(n,e,k) x vs mode ->
       let
         e' = inc (someVar x) k e
-        p = (InputConstraint(x, ix (someVar x) e') vs
-            ,InputConstraint(x, ix (someVar x) e') (complement vs)
+        p = (InputConstraint(x, ix (someVar x) e') vs e'
+            ,InputConstraint(x, ix (someVar x) e') (complement vs) e'
             , mode == ElseAbort && n < negMax)
       in case mode of
           AssumeValid -> RecSub p id (n,e',k+1)
@@ -120,7 +121,7 @@ showSomeConstraint :: SomeConstraint -> String
 showSomeConstraint (SomeConstraint c) = showConstraint c
 
 showConstraint :: Constraint t -> String
-showConstraint (InputConstraint (x,i) vs) = concat [varname x,"_",show i," : ",showValueSet vs]
+showConstraint (InputConstraint (x,i) vs _) = concat [varname x,"_",show i," : ",showValueSet vs]
 showConstraint (ConditionConstraint t m) = showIndexedTerm t m
 showConstraint (OverflowConstraints _ _) = "**some overflow checks**"
 

src/Test/IOTasks/Internal/Specification.hs

@@ -259,7 +259,7 @@ runSpecification' addLinebreaks spec inputs =
       case ins of
         [] -> NoRec (outOfInputs,NoOverflow)
         (i:is)
-          | vs `containsValue` readValue i -> RecSub i id (insertValue (wrapValue $ readValue @v i) (someVar x) e,is)
+          | containsValue x e vs (readValue i) -> RecSub i id (insertValue (wrapValue $ readValue @v i) (someVar x) e,is)
           | otherwise -> case mode of
               AssumeValid -> error $ "invalid value: " ++ i ++ " is not an element of " ++ showValueSet vs
               UntilValid ->  RecSame i (first (progWrite Optional (Set.singleton Wildcard) <>)) (e,is)
@@ -356,18 +356,18 @@ accept s_ t_ = accept' s_ k_I t_ d_I
   where
     accept' :: Specification -> (Action -> Trace -> ValueMap -> Bool) -> Trace -> ValueMap -> Bool
     accept' (ReadInput x (ty :: ValueSet a) AssumeValid s') k t d = case t of
-      ProgReadString v t' | ty `containsValue` val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
+      ProgReadString v t' | containsValue x d ty val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
                           where val = readValue @a v
       _ -> False
     accept' (ReadInput x (ty :: ValueSet a) ElseAbort s') k t d = case t of
-      ProgReadString v t'| ty `containsValue` val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
+      ProgReadString v t'| containsValue x d ty val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
                          where val = readValue @a v
-      ProgReadString v Terminate | not (ty `containsValue` readValue v) -> True
+      ProgReadString v Terminate | not (containsValue x d ty (readValue v)) -> True
       _ -> False
     accept' s@(ReadInput x (ty :: ValueSet a) UntilValid s') k t d = case t of
       ProgReadString v t'
-        | ty `containsValue` val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
-        | not (ty `containsValue` val) -> accept' s k t d
+        | containsValue x d ty val -> accept' s' k t' (insertValue (wrapValue val) (someVar x) d)
+        | not (containsValue x d ty val) -> accept' s k t d
         where val = readValue @a v
       _ -> False
     accept' (WriteOutput Optional os s') k t d = accept' (WriteOutput Mandatory os s') k t d || accept' s' k t d

src/Test/IOTasks/Internal/ValueSet.hs

@@ -9,8 +9,9 @@ module Test.IOTasks.Internal.ValueSet (
   union, intersection,
   (\\), with, without,
   complement,
+  unique, notInVar,
   isEmpty,
-  containsValue,
+  containsValue, initiallyContainsValue,
   showValueSet,
   valueOf,
   Size(..),
@@ -25,19 +26,29 @@ import Data.Typeable
 import Test.QuickCheck
 
 import Z3.Monad
+import Test.IOTasks.ValueMap (ValueMap, lookupInteger, emptyValueMap)
+import Test.IOTasks.Var (Var, someVar, SomeVar, intVar)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (fromMaybe)
 
 data ValueSet a where
   Union :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer
   Intersection :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer
   GreaterThan :: Integer -> ValueSet Integer
   LessThan :: Integer -> ValueSet Integer
   Eq :: Integer -> ValueSet Integer
+  CurrentlyIn :: VarRef -> ValueSet Integer
+  CurrentlyNotIn :: VarRef -> ValueSet Integer
   Every :: ValueSet a
   None :: ValueSet a
 
 deriving instance Eq (ValueSet a)
 deriving instance Ord (ValueSet a)
 
+data VarRef = Self | Other (Var Integer)
+  deriving (Eq,Ord)
+
 data Size = Size { intAbs :: Integer, strLen :: Int }
 
 empty :: ValueSet a
@@ -52,6 +63,12 @@ singleton = Eq
 fromList :: [Integer] -> ValueSet Integer
 fromList = foldr (union . singleton) empty
 
+unique :: ValueSet Integer -> ValueSet Integer
+unique vs = CurrentlyNotIn Self `intersection` vs
+
+notInVar :: ValueSet Integer -> Var Integer -> ValueSet Integer
+notInVar vs y = CurrentlyNotIn (Other y) `intersection` vs
+
 greaterThan :: Integer -> ValueSet Integer
 greaterThan = GreaterThan
 
@@ -76,35 +93,50 @@ with :: ValueSet Integer -> Integer -> ValueSet Integer
 with vs = (vs `union`) . singleton
 
 complement :: ValueSet a -> ValueSet a
-complement (GreaterThan n) = LessThan n `Union` Eq n
-complement (LessThan n) =  GreaterThan n `Union` Eq n
+complement (GreaterThan n) = LessThan n `union` Eq n
+complement (LessThan n) =  GreaterThan n `union` Eq n
 complement (Intersection va vb) = Union (complement va) (complement vb)
 complement (Union va vb) = Intersection (complement va) (complement vb)
-complement (Eq n) = GreaterThan n `Union` LessThan n
+complement (Eq n) = GreaterThan n `union` LessThan n
+complement (CurrentlyIn x) = CurrentlyNotIn x
+complement (CurrentlyNotIn x) = CurrentlyIn x
 complement Every = None
 complement None = Every
 
-containsValue :: ValueSet a -> a -> Bool
-containsValue (Union vs1 vs2) n = vs1 `containsValue` n || vs2 `containsValue` n
-containsValue (Intersection vs1 vs2) n = vs1 `containsValue` n && vs2 `containsValue` n
-containsValue (GreaterThan i) n = n > i
-containsValue (LessThan i) n = n < i
-containsValue (Eq i) n = i == n
-containsValue Every _ = True
-containsValue None _ = False
-
-valueOf :: Typeable a => ValueSet a -> Size -> Gen a
+containsValue :: Var a -> ValueMap -> ValueSet a -> a -> Bool
+containsValue x m (Union vs1 vs2) n = containsValue x m vs1  n || containsValue x m vs2 n
+containsValue x m (Intersection vs1 vs2) n = containsValue x m vs1 n && containsValue x m vs2 n
+containsValue _ _ (GreaterThan i) n = n > i
+containsValue _ _ (LessThan i) n = n < i
+containsValue _ _ (Eq i) n = i == n
+containsValue x m (CurrentlyIn Self) n = n `elem` valuesIn x m
+containsValue _ m (CurrentlyIn (Other y)) n = n `elem` valuesIn y m
+containsValue x m (CurrentlyNotIn Self) n = n `notElem` valuesIn x m
+containsValue _ m (CurrentlyNotIn (Other y)) n = n `notElem` valuesIn y m
+containsValue _ _ Every _ = True
+containsValue _ _ None _ = False
+
+valuesIn :: Var Integer -> ValueMap -> [Integer]
+valuesIn x env =
+  case lookupInteger (someVar x) env of
+    Just values -> map fst values
+    Nothing -> error $ unwords ["cannot find values for variable", show x , "in", show env, "(perhaps you misspelled a variable name)"]
+
+initiallyContainsValue ::  ValueSet Integer -> Integer -> Bool
+initiallyContainsValue = containsValue (intVar "x") $ emptyValueMap [someVar $ intVar "x"]
+
+valueOf :: Typeable a => Var a -> ValueMap -> ValueSet a -> Size -> Gen a
 valueOf = valueOf' where
-  valueOf' :: forall a. Typeable a => ValueSet a -> Size -> Gen a
-  valueOf' =
+  valueOf' :: forall a. Typeable a => Var a -> ValueMap -> ValueSet a -> Size -> Gen a
+  valueOf' x m =
     case eqT @a @Integer of
-      Just Refl -> valueOfInt
+      Just Refl -> valueOfInt x m
       Nothing -> case eqT @a @String of
         Just Refl -> valueOfString
         Nothing -> error $ "unsupported ValueSet type: " ++ show (typeRep $ Proxy @a)
 
-valueOfInt :: ValueSet Integer -> Size -> Gen Integer
-valueOfInt vs (Size sz _) =
+valueOfInt :: Var Integer -> ValueMap -> ValueSet Integer -> Size -> Gen Integer
+valueOfInt x m vs (Size sz _) =
   case Set.toList $ range vs $ Set.fromAscList [-sz..sz] of
     [] -> error $ unwords ["valueOf: no values between",show (-sz),"and",show sz,"within size bound for",showValueSet vs]
     xs -> elements xs
@@ -115,6 +147,10 @@ valueOfInt vs (Size sz _) =
     range (GreaterThan n) r = Set.filter (>n) r
     range (LessThan n) r = Set.filter (<n) r
     range (Eq n) r = Set.filter (==n) r
+    range (CurrentlyIn Self) r = Set.filter (\v -> v `elem` valuesIn x m) r
+    range (CurrentlyIn (Other y)) r = Set.filter (\v -> v `elem` valuesIn y m) r
+    range (CurrentlyNotIn Self) r = Set.filter (\v -> v `notElem` valuesIn x m) r
+    range (CurrentlyNotIn (Other y)) r = Set.filter (\v -> v `notElem` valuesIn y m) r
     range Every r = r
     range None _ = Set.empty
 
@@ -131,8 +167,12 @@ showValueSet = go where
     showValueSet' (GreaterThan n) = "v > " ++ show n
     showValueSet' (LessThan n) = "v < " ++ show n
     showValueSet' (Eq n) = "v == " ++ show n
+    showValueSet' (CurrentlyIn ref) = "currentlyIn " ++ showVarRef ref
+    showValueSet' (CurrentlyNotIn ref) = "currentlyNotIn " ++ showVarRef ref
     showValueSet' Every = "true"
     showValueSet' None = "false"
+    showVarRef Self = "self"
+    showVarRef (Other y) = show y
 
 -- basic ValueSets
 ints, nats :: ValueSet Integer
@@ -146,27 +186,39 @@ str = 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 :: ValueSet Integer -> IO Bool
-isEmpty vs = evalZ3 $ do
+isEmpty :: Var Integer -> Map SomeVar [AST] -> ValueSet Integer -> IO Bool
+isEmpty var m vs = evalZ3 $ do
   x <- mkIntVar =<< mkStringSymbol "x"
-  assert =<< z3ValueSetConstraint vs x
+  assert =<< z3ValueSetConstraint var m vs x
   res <- check
   pure $ case res of
     Sat -> False
     Unsat -> True
     Undef -> error "isEmpty: could not solve SMT constraints"
 
-z3ValueSetConstraint :: MonadZ3 z3 => ValueSet a -> AST -> z3 AST
-z3ValueSetConstraint (Union x y) xVar = do
-  cx <- z3ValueSetConstraint x xVar
-  cy <- z3ValueSetConstraint y xVar
+z3ValueSetConstraint :: MonadZ3 z3 => Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
+z3ValueSetConstraint var m (Union x y) xVar = do
+  cx <- z3ValueSetConstraint var m x xVar
+  cy <- z3ValueSetConstraint var m y xVar
   mkOr [cx,cy]
-z3ValueSetConstraint (Intersection x y) xVar = do
-  cx <- z3ValueSetConstraint x xVar
-  cy <- z3ValueSetConstraint y xVar
+z3ValueSetConstraint var m (Intersection x y) xVar = do
+  cx <- z3ValueSetConstraint var m x xVar
+  cy <- z3ValueSetConstraint var m y xVar
   mkAnd [cx,cy]
-z3ValueSetConstraint (GreaterThan n) xVar = mkIntNum n >>= mkGt xVar
-z3ValueSetConstraint (LessThan n) xVar = mkIntNum n >>= mkLt xVar
-z3ValueSetConstraint (Eq n) xVar = mkIntNum n >>= mkEq xVar
-z3ValueSetConstraint Every _ = mkTrue
-z3ValueSetConstraint None _ = mkFalse
+z3ValueSetConstraint _ _ (GreaterThan n) xVar = mkIntNum n >>= mkGt xVar
+z3ValueSetConstraint _ _ (LessThan n) xVar = mkIntNum n >>= mkLt xVar
+z3ValueSetConstraint _ _ (Eq n) xVar = mkIntNum n >>= mkEq xVar
+z3ValueSetConstraint var m (CurrentlyIn Self) xVar = do
+  let xs = fromMaybe [] $ Map.lookup (someVar var) m
+  mkOr =<< sequence [ mkEq xVar x | x <- xs, x /= xVar]
+z3ValueSetConstraint _ m (CurrentlyIn (Other y)) xVar = do
+  let xs = fromMaybe [] $ Map.lookup (someVar y) m
+  mkOr =<< sequence [ mkEq xVar x | x <- xs, x /= xVar]
+z3ValueSetConstraint var m (CurrentlyNotIn Self) xVar = do
+  let xs = fromMaybe [] $ Map.lookup (someVar var) m
+  mkAnd =<< sequence [ mkNot =<< mkEq xVar x | x <- xs, x /= xVar]
+z3ValueSetConstraint _ m (CurrentlyNotIn (Other y)) xVar = do
+  let xs = fromMaybe [] $ Map.lookup (someVar y) m
+  mkAnd =<< sequence [ mkNot =<< mkEq xVar x | x <- xs, x /= xVar]
+z3ValueSetConstraint _ _ Every _ = mkTrue
+z3ValueSetConstraint _ _ None _ = mkFalse

src/Test/IOTasks/Interpreter.hs

@@ -29,23 +29,26 @@ interpret s = do
   collapsed <- collapseChoice s
   pure $ flip evalStateT (emptyValueMap [] :: ValueMap) $
     sem
-      (\() x (vs :: ValueSet v) m -> RecSub (someVar x,wrapValue . readValue @v ,containsValue vs . unwrapValue,m) id ())
+      -- (\() x (vs :: ValueSet v) m -> RecSub (someVar x,wrapValue . readValue @v, \var m -> (containsValue var m vs . unwrapValue),m) id ())
+      (\() x (vs :: ValueSet v) m -> RecSub (someVar x,wrapValue . readValue @v, \vMap -> containsValue x vMap vs . unwrapValue,m) id ())
       (\case
         RecSub (x,readF,_,AssumeValid) () p' -> do
           v <- lift (readF <$> MTT.getLine)
           modify $ insertValue v x
           p'
         RecSub (x,readF,vsContains,ElseAbort) () p' -> do
           v <- lift (readF <$> MTT.getLine)
-          if vsContains v
+          vMap <- get
+          if vsContains vMap v
             then do
               modify $ insertValue v x
               p'
             else lift $ MTT.putStrLn "abort: invalid input value"
         RecSub (x,readF,vsContains,UntilValid) () p' -> do
           let readLoop = do
                 v <- lift (readF <$> MTT.getLine)
-                if vsContains v then pure v else lift (putStrLn "invalid value, try again") >> readLoop
+                vMap <- get
+                if vsContains vMap v then pure v else lift (putStrLn "invalid value, try again") >> readLoop
           v <- readLoop
           modify $ insertValue v x
           p'

src/Test/IOTasks/Random.hs

@@ -10,6 +10,7 @@ module Test.IOTasks.Random (
   union, intersection,
   (\\), with, without,
   complement,
+  unique, notInVar,
   isEmpty,
   ints, nats, str,
   OutputPattern,

src/Test/IOTasks/Random/Testing.hs

@@ -112,9 +112,9 @@ genTrace spec depth sz maxNeg =
       (if maybe False (d >) depth then pure $ NoRec OutOfInputs
       else do
         frequency $
-            (5, valueOf vs sz >>= (\i -> pure $ RecSub (wrapValue i) id (insertValue (wrapValue i) (someVar x) e,d+1,n)))
-          : [(1, valueOf (complement vs) sz >>= (\i -> pure $ RecSame (wrapValue i) id (e,d+1,n+1))) | mode == UntilValid && n < maxNeg]
-          ++ [(1, valueOf (complement vs) sz >>= (\i -> pure $ NoRec $ foldr ProgRead Terminate (show i ++ "\n"))) | mode == ElseAbort && n < maxNeg]
+            (5, valueOf x e vs sz >>= (\i -> pure $ RecSub (wrapValue i) id (insertValue (wrapValue i) (someVar x) e,d+1,n)))
+          : [(1, valueOf x e (complement vs) sz >>= (\i -> pure $ RecSame (wrapValue i) id (e,d+1,n+1))) | mode == UntilValid && n < maxNeg]
+          ++ [(1, valueOf x e (complement vs) sz >>= (\i -> pure $ NoRec $ foldr ProgRead Terminate (show i ++ "\n"))) | mode == ElseAbort && n < maxNeg]
     ))
     (pure . \case
       NoRec r -> r

src/Test/IOTasks/ValueSet.hs

@@ -5,8 +5,9 @@ module Test.IOTasks.ValueSet (
   lessThan, greaterThan,
   (\\), with, without,
   complement,
+  unique, notInVar,
   isEmpty,
-  containsValue,
+  containsValue, initiallyContainsValue,
   showValueSet,
   -- | = random value generation
   valueOf,