Add negative labels

bin/rtree-c/Main.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 import Control.RTree
+import Data.Valuation qualified as Val
 
 import ReduceC
 
@@ -15,7 +16,6 @@ import Control.Monad
 import Control.Monad.Trans
 import Data.Foldable
 import Data.Functor
-import Data.Map.Strict qualified as Map
 import Data.Text qualified as Text
 import GHC.Stack
 import Language.C qualified as C
@@ -106,7 +106,7 @@ run = do
         check' f val c = do
           logInfo "Checking predictate"
           when debug do
-            pPrint [(void k, v) | (k, v) <- Map.toList val]
+            pPrint [(void k, v) | (k, v) <- Val.toPairs val]
             pPrint (void c)
           when pedandic do
             liftIO $ copyFile file (file <.> "last")
@@ -163,7 +163,7 @@ run = do
       l <-
         (if expmode then ireduceExp else ireduce)
           (check' file)
-          (Map.singleton (C.internalIdent "main") True)
+          (Val.singleton (Val.is $ C.internalIdent "main"))
           (ReduceC.reduceC c)
 
       output file l

bin/rtree-c/ReduceC.hs

@@ -9,6 +9,8 @@ module ReduceC where
 
 import Control.Monad.Reduce
 
+import qualified Data.Valuation as Val
+
 import Control.Applicative
 import Control.Monad.Trans
 import Control.Monad.Trans.Maybe
@@ -102,7 +104,7 @@ cCTypeSpecifier = \case
   -- C.CUInt128Type a -> pure ()
   C.CFloatNType{} -> pure ()
   C.CTypeDef i _ -> do
-    givenThat i
+    givenThat (Val.is i)
     pure ()
   (C.CTypeOfExpr e _) -> cCExpression e
   (C.CTypeOfType t _) -> cCDeclaration t
@@ -140,7 +142,7 @@ mrCFunctionDef (C.CFunDef spc dec cdecls smt ni) = do
 cCDeclr :: (MonadReduce Lab m) => C.CDeclarator C.NodeInfo -> MaybeT m ()
 cCDeclr (C.CDeclr x dd _ _ _) = do
   mapM_ cCDerivedDeclarator dd
-  givenWith x
+  givenWith (Val.is <$> x)
  where
   cCDerivedDeclarator = \case
     C.CPtrDeclr ts _ -> mapM_ cCTypeQualifier ts
@@ -153,13 +155,13 @@ cCDeclr (C.CDeclr x dd _ _ _) = do
       mapM_ cCAttr attr
       cCFunParams f
   cCFunParams = \case
-    C.CFunParamsOld o -> mapM_ givenThat o
+    C.CFunParamsOld o -> mapM_ (givenThat . Val.is) o
     C.CFunParamsNew o _ -> mapM_ cCDeclaration o
 
 cCAttr :: (MonadReduce Lab m) => C.CAttribute C.NodeInfo -> MaybeT m ()
 cCAttr (C.CAttr i e _) = do
   mapM_ cCExpression e
-  givenThat i
+  givenThat (Val.is i)
 
 rCStatement :: (MonadReduce Lab m) => C.CStatement C.NodeInfo -> m (C.CStatement C.NodeInfo)
 rCStatement = \case
@@ -197,12 +199,12 @@ rCStatement = \case
   C.CCont ni -> pure (C.CCont ni)
   C.CLabel i s [] ni ->
     -- todo fix attrs
-    splitOn i (rCStatement s) do
+    splitOn (Val.is i) (rCStatement s) do
       s' <- rCStatement s
       pure $ C.CLabel i s' [] ni
   C.CGoto i ni ->
     -- todo fix attrs
-    splitOn i (pure $ C.CExpr Nothing ni) do
+    splitOn (Val.is i) (pure $ C.CExpr Nothing ni) do
       pure $ C.CGoto i ni
   C.CWhile e s dow ni -> do
     e' <- zrCExpression e
@@ -231,7 +233,7 @@ zrCExpression e = orZero <$> runMaybeT (mrCExpression e)
 mrCExpression :: (MonadReduce Lab m) => C.CExpression C.NodeInfo -> MaybeT m (C.CExpression C.NodeInfo)
 mrCExpression = \case
   C.CVar i ni -> do
-    givenThat i
+    givenThat (Val.is i)
     pure $ C.CVar i ni
   C.CCall e es ni -> do
     e' <- mrCExpression e
@@ -260,7 +262,7 @@ mrCExpression = \case
   C.CIndex e1 e2 ni -> onBothExpr e1 e2 \e1' e2' ->
     pure $ C.CIndex e1' e2' ni
   C.CMember e i b ni -> do
-    givenThat i
+    givenThat (Val.is i)
     e' <- mrCExpression e
     pure $ C.CMember e' i b ni
   C.CComma items ni -> do

src/Control/Monad/Reduce.hs

@@ -49,6 +49,8 @@ import Control.Monad.Trans.Maybe
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe
 
+import Data.Valuation (Truth (..))
+
 -- {- | A reducer should extract itself
 -- @
 --  extract . red = id
@@ -63,7 +65,7 @@ class (Monad m) => MonadReduce l m | m -> l where
 
   -- | Split the world into the a reduced world (left) without an element and a world
   -- with that element (right). Optionally, labeled with l.
-  splitWith :: Maybe l -> m i -> m i -> m i
+  splitWith :: Maybe (Truth l) -> m i -> m i -> m i
   splitWith l r1 r2 =
     checkWith l >>= \case
       False -> r1
@@ -71,8 +73,8 @@ class (Monad m) => MonadReduce l m | m -> l where
   {-# INLINE splitWith #-}
 
   -- | Check with returns a boolean, that can be used to split the input into a world where
-  -- an optional label is true and where it is false.
-  checkWith :: Maybe l -> m Bool
+  -- the optional truth assignement is satisfiable and where it is not.
+  checkWith :: Maybe (Truth l) -> m Bool
   checkWith l = splitWith l (pure False) (pure True)
   {-# INLINE checkWith #-}
 
@@ -96,7 +98,7 @@ r1 |> r2 = r2 <| r1
 infixl 3 |>
 
 -- | Split on a label.
-splitOn :: (MonadReduce l m) => l -> m i -> m i -> m i
+splitOn :: (MonadReduce l m) => Truth l -> m i -> m i -> m i
 splitOn l = splitWith (Just l)
 {-# INLINE splitOn #-}
 
@@ -106,7 +108,7 @@ check = checkWith Nothing
 {-# INLINE check #-}
 
 -- | Split the world on a labeled fact. False it does not happen, and True it does happen.
-checkThat :: (MonadReduce l m) => l -> m Bool
+checkThat :: (MonadReduce l m) => Truth l -> m Bool
 checkThat l = checkWith (Just l)
 {-# INLINE checkThat #-}
 
@@ -116,12 +118,12 @@ given = givenWith Nothing
 {-# INLINE given #-}
 
 -- | Continues if the labeled fact is true.
-givenWith :: (MonadReduce l m, MonadPlus m) => Maybe l -> m ()
+givenWith :: (MonadReduce l m, MonadPlus m) => Maybe (Truth l) -> m ()
 givenWith l = splitWith l mzero (pure ())
 {-# INLINE givenWith #-}
 
 -- | Continues if the labeled fact is true.
-givenThat :: (MonadReduce l m, MonadPlus m) => l -> m ()
+givenThat :: (MonadReduce l m, MonadPlus m) => Truth l -> m ()
 givenThat l = givenWith (Just l)
 {-# INLINE givenThat #-}
 

src/Control/RTree.hs

@@ -42,17 +42,18 @@ import Control.Monad.Reduce
 import qualified Data.Valuation as Val
 
 type Valuation = Val.Valuation
+type Truth = Val.Truth
 
 data RTree l i
-  = SplitWith (Maybe l) (RTree l i) !(RTree l i)
+  = SplitWith (Maybe (Truth l)) (RTree l i) !(RTree l i)
   | Done i
   deriving (Functor)
 
 extract :: (Ord l) => Valuation l -> RTree l i -> i
 extract v = \case
-  SplitWith ml lhs rhs -> case ml >>= Val.truthValue v of
-    Just False -> extract v lhs
-    _ -> extract v rhs
+  SplitWith ml lhs rhs -> case ml >>= Val.condition v of
+    Just v' -> extract v' rhs
+    _ -> extract v lhs
   Done i -> i
 
 instance Applicative (RTree l) where
@@ -79,10 +80,11 @@ reduce p = checkgo
   checkgo v r = p (extract v r) *> go v r
   go v = \case
     Done i -> pure i
-    SplitWith (Just l) lhs rhs -> case Val.truthValue v l of
-      Just True -> checkgo v rhs
-      Just False -> checkgo v lhs
-      Nothing -> checkgo (Val.setTruthValue v l False) lhs <|> go (Val.setTruthValue v l True) rhs
+    SplitWith (Just l) lhs rhs -> case Val.truthValue v (Val.label l) of
+      Just t
+        | t == Val.truth l -> checkgo v rhs
+        | otherwise -> checkgo v lhs
+      Nothing -> checkgo (Val.withTruth v $ Val.not l) lhs <|> go (Val.withTruth v l) rhs
     SplitWith Nothing lhs rhs -> (checkgo v lhs <|> go v rhs)
 {-# INLINE reduce #-}
 
@@ -104,10 +106,10 @@ instance (Monad m, Ord l) => MonadReduce l (IRTreeT l m) where
         ReState (uncons -> (a, as)) v ->
           pure (a, ReState as v)
       Just l -> \case
-        ReState as v@((`Val.truthValue` l) -> Just x) ->
+        ReState as v@((`Val.truthValue` Val.label l) -> Just x) ->
           pure (x, ReState as v)
         ReState (uncons -> (a, as)) v ->
-          pure (a, ReState as (Val.setTruthValue v l a))
+          pure (a, ReState as (Val.withTruth v (if a then l else Val.not l)))
    where
     uncons [] = (True, [])
     uncons (a : as) = (a, as)

src/Data/Valuation.hs

@@ -14,10 +14,16 @@ module Data.Valuation (
   toPairs,
 
   -- * Access
-  setTruthValue,
+  withTruth,
   truthValue,
   condition,
 
+  -- * Truth
+  Truth (..),
+  not,
+  is,
+  isNot,
+
   -- * Helpers
   viaMap,
   viaMapF,
@@ -26,34 +32,61 @@ module Data.Valuation (
 import Data.Functor.Identity
 import qualified Data.Map.Strict as Map
 
+import Prelude hiding (not)
+import qualified Prelude
+
+-- | A Single truth assignment
+data Truth l = Truth
+  { label :: !l
+  , truth :: !Bool
+  }
+
+is :: l -> Truth l
+is l = Truth{label = l, truth = True}
+{-# INLINE is #-}
+
+isNot :: l -> Truth l
+isNot l = Truth{label = l, truth = False}
+{-# INLINE isNot #-}
+
+not :: Truth l -> Truth l
+not (Truth l t) = Truth l (Prelude.not t)
+
 newtype Valuation l = Valuation {toMap :: Map.Map l Bool}
 
-singleton :: (Ord l) => l -> Bool -> Valuation l
-singleton l t = fromMap $ Map.singleton l t
+singleton :: (Ord l) => Truth l -> Valuation l
+singleton (Truth l t) = fromMap $ Map.singleton l t
+{-# INLINE singleton #-}
 
 viaMap :: (Map.Map l Bool -> Map.Map l Bool) -> Valuation l -> Valuation l
 viaMap fn = runIdentity . viaMapF (Identity . fn)
+{-# INLINE viaMap #-}
 
 viaMapF :: (Functor f) => (Map.Map l Bool -> f (Map.Map l Bool)) -> Valuation l -> f (Valuation l)
 viaMapF fn = fmap fromMap . fn . toMap
+{-# INLINE viaMapF #-}
 
 fromMap :: Map.Map l Bool -> Valuation l
 fromMap = Valuation
+{-# INLINE fromMap #-}
 
 fromPairs :: (Ord l) => [(l, Bool)] -> Valuation l
 fromPairs = Valuation . Map.fromList
+{-# INLINE fromPairs #-}
 
 toPairs :: Valuation l -> [(l, Bool)]
 toPairs = Map.toList . toMap
+{-# INLINE toPairs #-}
 
 truthValue :: (Ord l) => Valuation l -> l -> Maybe Bool
 truthValue (Valuation m) = (`Map.lookup` m)
+{-# INLINE truthValue #-}
 
 {- | Conditions a valuation with key value pair, if it conficts with the valuation,
 it returns Nothing
 -}
-condition :: (Ord l) => Valuation l -> l -> Bool -> Maybe (Valuation l)
-condition v l t =
+condition :: (Ord l) => Valuation l -> Truth l -> Maybe (Valuation l)
+condition v (Truth l t) =
   viaMapF
     ( Map.alterF
         \case
@@ -62,6 +95,8 @@ condition v l t =
         l
     )
     v
+{-# INLINE condition #-}
 
-setTruthValue :: (Ord l) => Valuation l -> l -> Bool -> Valuation l
-setTruthValue v l t = viaMap (Map.insert l t) v
+withTruth :: (Ord l) => Valuation l -> Truth l -> Valuation l
+withTruth v (Truth l t) = viaMap (Map.insert l t) v
+{-# INLINE withTruth #-}