Tests and documentation for normalization of boolean values

what4/CHANGES.md

@@ -1,3 +1,10 @@
+# next
+
+* The `BoolMap` parameter of `ConjPred` is now a `ConjMap`. This is a `newtype`
+  wrapper around `BoolMap` that makes clear that the `BoolMap` in question
+  represents a conjunction (as `BoolMap`s may also represent disjunctions).
+  See the Haddocks on `ConjMap` for more details.
+
 # 1.6.2 (Sep 2024)
 
 * Allow building with GHC 9.10.

what4/src/What4/Expr/App.hs

@@ -80,7 +80,7 @@ import           What4.ProgramLoc
 import qualified What4.SemiRing as SR
 import qualified What4.SpecialFunctions as SFn
 import qualified What4.Expr.ArrayUpdateMap as AUM
-import           What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..), Wrap(..))
+import           What4.Expr.BoolMap (BoolMap, Polarity(..), Wrap(..))
 import qualified What4.Expr.BoolMap as BM
 import           What4.Expr.MATLAB
 import           What4.Expr.WeightedSum (WeightedSum, SemiRingProduct)
@@ -191,10 +191,10 @@ data App (e :: BaseType -> Type) (tp :: BaseType) where
   -- Invariant: The argument to a NotPred must not be another NotPred.
   NotPred :: !(e BaseBoolType) -> App e BaseBoolType
 
-  -- Invariant: The BoolMap must contain at least two elements. No
-  -- element may be a NotPred; negated elements must be represented
-  -- with Negative element polarity.
-  ConjPred :: !(BoolMap e) -> App e BaseBoolType
+  -- Invariant: The 'BM.ConjMap' must contain at least two elements. No element
+  -- may be a NotPred; negated elements must be represented with Negative
+  -- element polarity. See also 'isNormal' in @test/Bool.hs@.
+  ConjPred :: !(BM.ConjMap e) -> App e BaseBoolType
 
   ------------------------------------------------------------------------
   -- Semiring operations
@@ -814,6 +814,9 @@ traverseApp =
     , ( ConType [t|BoolMap|] `TypeApp` AnyType
       , [| BM.traverseVars |]
       )
+    , ( ConType [t|BM.ConjMap|] `TypeApp` AnyType
+      , [| \f cm -> BM.ConjMap <$> BM.traverseVars f (BM.getConjMap cm) |]
+      )
     , ( ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType
       , [| traverseFC |]
       )
@@ -1158,20 +1161,20 @@ asWeightedSum sr x
 asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
 asConjunction (BoolExpr True _) = []
 asConjunction (asApp -> Just (ConjPred xs)) =
- case BM.viewBoolMap xs of
-   BoolMapUnit     -> []
-   BoolMapDualUnit -> [(BoolExpr False initializationLoc, Positive)]
-   BoolMapTerms (tm:|tms) -> tm:tms
+ case BM.viewConjMap xs of
+   BM.ConjTrue -> []
+   BM.ConjFalse -> [(BoolExpr False initializationLoc, Positive)]
+   BM.Conjuncts (tm:|tms) -> tm:tms
 asConjunction x = [(x,Positive)]
 
 
 asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
 asDisjunction (BoolExpr False _) = []
 asDisjunction (asApp -> Just (NotPred (asApp -> Just (ConjPred xs)))) =
- case BM.viewBoolMap xs of
-   BoolMapUnit     -> []
-   BoolMapDualUnit -> [(BoolExpr True initializationLoc, Positive)]
-   BoolMapTerms (tm:|tms) -> map (over _2 BM.negatePolarity) (tm:tms)
+ case BM.viewConjMap xs of
+   BM.ConjTrue -> []
+   BM.ConjFalse -> [(BoolExpr True initializationLoc, Positive)]
+   BM.Conjuncts (tm:|tms) -> map (over _2 BM.negatePolarity) (tm:tms)
 asDisjunction x = [(x,Positive)]
 
 asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
@@ -2086,11 +2089,11 @@ reduceApp sym unary a0 = do
     BaseEq _ x y -> isEq sym x y
 
     NotPred x -> notPred sym x
-    ConjPred bm ->
-      case BM.viewBoolMap bm of
-        BoolMapDualUnit -> return $ falsePred sym
-        BoolMapUnit     -> return $ truePred sym
-        BoolMapTerms tms ->
+    ConjPred cm ->
+      case BM.viewConjMap cm of
+        BM.ConjFalse -> return $ falsePred sym
+        BM.ConjTrue -> return $ truePred sym
+        BM.Conjuncts tms ->
           do let pol (p, Positive) = return p
                  pol (p, Negative) = notPred sym p
              x:|xs <- mapM pol tms
@@ -2337,14 +2340,14 @@ ppApp' a0 = do
 
     NotPred x -> ppSExpr "not" [x]
 
-    ConjPred xs ->
+    ConjPred cm ->
       let pol (x,Positive) = exprPrettyArg x
           pol (x,Negative) = PrettyFunc "not" [ exprPrettyArg x ]
        in
-       case BM.viewBoolMap xs of
-         BoolMapUnit      -> prettyApp "true" []
-         BoolMapDualUnit  -> prettyApp "false" []
-         BoolMapTerms tms -> prettyApp "and" (map pol (toList tms))
+       case BM.viewConjMap cm of
+         BM.ConjTrue -> prettyApp "true" []
+         BM.ConjFalse-> prettyApp "false" []
+         BM.Conjuncts tms -> prettyApp "and" (map pol (toList tms))
 
     RealIsInteger x -> ppSExpr "isInteger" [x]
     BVTestBit i x   -> prettyApp "testBit"  [exprPrettyArg x, showPrettyArg i]

what4/src/What4/Expr/BoolMap.hs

@@ -11,8 +11,12 @@ laws like commutativity, associativity and resolution.
 -}
 
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
 module What4.Expr.BoolMap
   ( BoolMap
   , var
@@ -26,18 +30,30 @@ module What4.Expr.BoolMap
   , isNull
   , BoolMapView(..)
   , viewBoolMap
+  , foldMapVars
   , traverseVars
   , reversePolarities
   , removeVar
   , Wrap(..)
+    -- * 'ConjMap'
+  , ConjMap(..)
+  , ConjMapView
+  , pattern ConjTrue
+  , pattern ConjFalse
+  , pattern Conjuncts
+  , viewConjMap
+  , addConjunct
+  , evalConj
   ) where
 
 import           Control.Lens (_1, over)
+import           Data.Coerce (coerce)
 import           Data.Hashable
 import qualified Data.List as List (foldl')
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Kind (Type)
 import           Data.Parameterized.Classes
+import           Data.Parameterized.TraversableF
 
 import           What4.BaseTypes
 import qualified What4.Utils.AnnotatedMap as AM
@@ -66,18 +82,20 @@ instance OrdF f => Ord (Wrap f x) where
 instance (HashableF f, TestEquality f) => Hashable (Wrap f x) where
   hashWithSalt s (Wrap a) = hashWithSaltF s a
 
--- | This data structure keeps track of a collection of expressions
---   together with their polarities. Such a collection might represent
---   either a conjunction or a disjunction of expressions.  The
---   implementation uses a map from expression values to their
---   polarities, and thus automatically implements the associative,
---   commutative and idempotency laws common to both conjunctions and
---   disjunctions.  Moreover, if the same expression occurs in the
---   collection with opposite polarities, the entire collection
---   collapses via a resolution step to an \"inconsistent\" map.  For
---   conjunctions this corresponds to a contradiction and
---   represents false; for disjunction, this corresponds to the law of
---   the excluded middle and represents true.
+-- | A representation of a conjunction or a disjunction.
+--
+--   This data structure keeps track of a collection of expressions together
+--   with their polarities.  The implementation uses a map from expression
+--   values to their polarities, and thus automatically implements the
+--   associative, commutative and idempotency laws common to both conjunctions
+--   and disjunctions.  Moreover, if the same expression occurs in the
+--   collection with opposite polarities, the entire collection collapses
+--   via a resolution step to an \"inconsistent\" map.  For conjunctions this
+--   corresponds to a contradiction and represents false; for disjunction, this
+--   corresponds to the law of the excluded middle and represents true.
+--
+--   The annotation on the 'AM.AnnotatedMap' is an incremental hash ('IncrHash')
+--   of the map, used to support a fast 'Hashable' instance.
 
 data BoolMap (f :: BaseType -> Type)
   = InconsistentMap
@@ -88,6 +106,16 @@ instance OrdF f => Eq (BoolMap f) where
   BoolMap m1 == BoolMap m2 = AM.eqBy (==) m1 m2
   _ == _ = False
 
+instance OrdF f => Semigroup (BoolMap f) where
+  (<>) = combine
+
+-- | Specialized version of 'foldMapVars'
+instance FoldableF BoolMap where
+  foldMapF f = foldMapVars f
+
+foldMapVars :: Monoid m => (f BaseBoolType -> m) -> BoolMap f -> m
+foldMapVars _ InconsistentMap = mempty
+foldMapVars f (BoolMap am) = foldMap (f . unWrap . fst) (AM.toList am)
 
 -- | Traverse the expressions in a bool map, and rebuild the map.
 traverseVars :: (Applicative m, HashableF g, OrdF g) =>
@@ -107,7 +135,10 @@ instance (OrdF f, HashableF f) => Hashable (BoolMap f) where
       Nothing -> hashWithSalt s (1::Int)
       Just h  -> hashWithSalt (hashWithSalt s (1::Int)) h
 
--- | Represents the state of a bool map
+-- | Represents the state of a 'BoolMap' (either a conjunction or disjunction).
+--
+-- If you know you are dealing with a 'BoolMap' that represents a conjunction,
+-- consider using 'ConjMap' and 'viewConjMap' for the sake of clarity.
 data BoolMapView f
   = BoolMapUnit
        -- ^ A bool map with no expressions, represents the unit of the corresponding operation
@@ -179,3 +210,66 @@ reversePolarities (BoolMap m) = BoolMap $! fmap negatePolarity m
 removeVar :: OrdF f => BoolMap f -> f BaseBoolType -> BoolMap f
 removeVar InconsistentMap _ = InconsistentMap
 removeVar (BoolMap m) x = BoolMap (AM.delete (Wrap x) m)
+
+--------------------------------------------------------------------------------
+-- ConjMap
+
+-- | A 'BoolMap' representing a conjunction.
+newtype ConjMap f = ConjMap { getConjMap :: BoolMap f }
+  deriving (Eq, FoldableF, Hashable, Semigroup)
+
+-- | Represents the state of a 'ConjMap'. See 'viewConjMap'.
+--
+-- Like 'BoolMapView', but with more specific patterns for readability.
+newtype ConjMapView f = ConjMapView (BoolMapView f)
+
+pattern ConjTrue :: ConjMapView f
+pattern ConjTrue = ConjMapView BoolMapUnit
+
+pattern ConjFalse :: ConjMapView f
+pattern ConjFalse = ConjMapView BoolMapDualUnit
+
+pattern Conjuncts :: NonEmpty (f BaseBoolType, Polarity) -> ConjMapView f
+pattern Conjuncts ts = ConjMapView (BoolMapTerms ts)
+
+{-# COMPLETE ConjTrue, ConjFalse, Conjuncts #-}
+
+-- | Deconstruct the given 'ConjMap' for later processing
+viewConjMap :: forall f. ConjMap f -> ConjMapView f
+viewConjMap =
+  -- The explicit type annotations on `coerce` are likely necessary because of
+  -- https://gitlab.haskell.org/ghc/ghc/-/issues/21003
+  coerce @(BoolMap f -> BoolMapView f) @(ConjMap f -> ConjMapView f) viewBoolMap
+{-# INLINE viewConjMap #-}
+
+-- | Add a conjunct to a 'ConjMap'.
+--
+-- Wrapper around 'addVar'.
+addConjunct ::
+  forall f.
+  (HashableF f, OrdF f) =>
+  f BaseBoolType ->
+  Polarity ->
+  ConjMap f ->
+  ConjMap f
+addConjunct =
+  -- The explicit type annotations on `coerce` are likely necessary because of
+  -- https://gitlab.haskell.org/ghc/ghc/-/issues/21003
+  coerce
+    @(f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f)
+    @(f BaseBoolType -> Polarity -> ConjMap f -> ConjMap f)
+    addVar
+{-# INLINE addConjunct #-}
+
+-- | Given the means to evaluate the conjuncts of a 'ConjMap' to a concrete
+-- 'Bool', evaluate the whole conjunction to a 'Bool'.
+evalConj :: Applicative m => (f BaseBoolType -> m Bool) -> ConjMap f -> m Bool
+evalConj f cm =
+  let pol (x, Positive) = f x
+      pol (x, Negative) = not <$> f x
+  in
+  case viewConjMap cm of
+    ConjTrue -> pure True
+    ConjFalse -> pure False
+    Conjuncts (t:|ts) ->
+      List.foldl' (&&) <$> pol t <*> traverse pol ts