diff --git a/experiment/configuration/BasePredicate.hs b/experiment/configuration/BasePredicate.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1736c96422368c29d0fca7c72b29b73d23f855e3
--- /dev/null
+++ b/experiment/configuration/BasePredicate.hs
@@ -0,0 +1,112 @@
+module BasePredicate (
+
+ BasePredicate(..),
+ eval,
+ applyOS,
+ applyArch,
+ applyCompiler,
+ applyFlagAssignment,
+
+ applySystemParams,
+
+ --TODO: move elsewhere:
+ SystemParams(..)
+
+ ) where
+
+import PartialValuation
+
+import Distribution.Version
+ ( VersionRange(..), withinRange )
+import Distribution.System
+ ( OS(..), Arch(..) )
+import Distribution.Compiler
+ ( CompilerFlavor, CompilerId(..) )
+
+import Distribution.PackageDescription
+ ( FlagName, FlagAssignment )
+
+import Data.Monoid
+ ( Monoid(..) )
+
+data SystemParams = SystemParams OS Arch CompilerId
+
+data BasePredicate
+ = OSPredicate OS
+ | ArchPredicate Arch
+ | CompilerPredicate CompilerFlavor VersionRange
+ | FlagPredicate FlagName
+ deriving (Eq, Show)
+
+-- | Evaluate a 'BasePredicate'. It will return 'Nothing' if and only if the
+-- 'FlagAssignment' is not total.
+--
+-- You can use this along with 'PredicateExpr.eval'' to give a valuation on a
+-- whole 'PredicateExpr':
+--
+-- > PredicateExpr.eval' (eval sysParms flags)
+-- > :: PredicateExpr BasePredicate -> Maybe Bool
+--
+eval :: SystemParams
+ -> FlagAssignment
+ -> PartialValuation BasePredicate
+eval (SystemParams os arch (CompilerId comp ver)) flagAssignment =
+ PartialValuation peval
+ where
+ peval (OSPredicate os') = Just $! os == os'
+ peval (ArchPredicate arch') = Just $! arch == arch'
+ peval (CompilerPredicate comp' range) = Just $! comp == comp'
+ && ver `withinRange` range
+ peval (FlagPredicate flag) = lookup flag flagAssignment
+
+applyOS :: OS -> PartialValuation BasePredicate
+applyOS os = PartialValuation peval
+ where
+ peval (OSPredicate os') = Just $! os == os'
+ peval _ = Nothing
+
+applyArch :: Arch -> PartialValuation BasePredicate
+applyArch arch = PartialValuation peval
+ where
+ peval (ArchPredicate arch') = Just $! arch == arch'
+ peval _ = Nothing
+
+applyCompiler :: CompilerId -> PartialValuation BasePredicate
+applyCompiler (CompilerId comp ver) = PartialValuation peval
+ where
+ peval (CompilerPredicate comp' range) = Just $! comp == comp'
+ && ver `withinRange` range
+ peval _ = Nothing
+
+-- | A 'PartialValuation' on a 'BasePredicate' obtained by applying a
+-- 'FlagAssignment'. It gives a value in the case that the 'BasePredicate' is a
+-- 'FlagPredicate' that is given a value by the 'FlagAssignment'.
+--
+-- This can be used to simplify a compound 'PredicateExpr' using:
+--
+-- > PredicateExpr.simplify (applyFlagAssignment flagAssignment)
+-- > :: PredicateExpr BasePredicate -> PredicateExpr BasePredicate
+--
+applyFlagAssignment :: FlagAssignment -> PartialValuation BasePredicate
+applyFlagAssignment flagAssignment = PartialValuation peval
+ where
+ peval (FlagPredicate flag) = lookup flag flagAssignment
+ peval other = Nothing
+
+--applyCompilerFlavor :: CompilerFlavor -> PartialValuation BasePredicate
+
+--applyCompilerIds :: [CompilerId] -> PartialValuation BasePredicate
+
+
+-- | Partially evaluate a 'BasePredicate' by supplying values for the
+-- all the 'SystemParams', leaving only the flags.
+--
+applySystemParams :: SystemParams
+ -> (BasePredicate -> Either Bool FlagName)
+applySystemParams (SystemParams os arch (CompilerId comp ver)) = peval
+ where
+ peval (OSPredicate os') = Left $ os == os'
+ peval (ArchPredicate arch') = Left $ arch == arch'
+ peval (CompilerPredicate comp' range) = Left $ comp == comp'
+ && ver `withinRange` range
+ peval (FlagPredicate flag) = Right flag
diff --git a/experiment/configuration/ConditionTree.hs b/experiment/configuration/ConditionTree.hs
new file mode 100644
index 0000000000000000000000000000000000000000..eed6845d0ee12efb8d9ed6b9b5c86a3abc3ad206
--- /dev/null
+++ b/experiment/configuration/ConditionTree.hs
@@ -0,0 +1,215 @@
+module ConditionTree (
+ ConditionTree(..),
+ ConditionNode(..),
+
+ flatten,
+ leaves,
+ unconditional,
+ resolve,
+ resolve',
+ simplify,
+ mapCondition,
+ paths,
+ ) where
+
+import PartialValuation
+ ( PartialValuation(..), TotalValuation )
+
+import Data.Monoid
+ ( Monoid(..) )
+import qualified Data.Foldable as Foldable
+ ( Foldable(..), toList )
+import Data.Foldable
+ ( Foldable )
+
+-- | A condition tree is a tree of values guarded by condition expressions.
+-- Each level of the tree has a list of nodes.
+--
+newtype ConditionTree condition body
+ = ConditionTree [ConditionNode condition body]
+ deriving (Eq, Show)
+
+-- An individual condition tree node is either a body value or a conditional
+-- with a further tree below. Conditionals can have an else part.
+--
+data ConditionNode condition body
+ = Body body
+ | IfThen condition (ConditionTree condition body)
+ | IfElse condition (ConditionTree condition body)
+ (ConditionTree condition body)
+ deriving (Eq, Show)
+
+
+instance Functor (ConditionTree condition) where
+ fmap f (ConditionTree ns) = ConditionTree (map (fmap f) ns)
+
+instance Functor (ConditionNode condition) where
+ fmap f (Body x) = Body (f x)
+ fmap f (IfThen c e) = IfThen c (fmap f e)
+ fmap f (IfElse c e1 e2) = IfElse c (fmap f e1) (fmap f e2)
+
+instance Foldable (ConditionTree condition) where
+ foldr f z (ConditionTree ns) = foldr (flip (Foldable.foldr f)) z ns
+
+instance Foldable (ConditionNode condition) where
+ foldr f z (Body b) = f b z
+ foldr f z (IfThen _ e) = Foldable.foldr f z e
+ foldr f z (IfElse _ e1 e2) = Foldable.foldr f (Foldable.foldr f z e2) e1
+
+-- | Take all the leaves and flatten them into one value using the monoid
+-- operation.
+--
+flatten :: Monoid body
+ => ConditionTree condition body -> body
+flatten = Foldable.fold
+
+-- | Get a list of all the leaves of the tree.
+--
+leaves :: ConditionTree condition body -> [body]
+leaves = Foldable.toList
+
+-- | Get a list of all the body nodes that are unconditional
+--
+unconditional :: ConditionTree condition body -> [body]
+unconditional (ConditionTree nodes) = [ b | Body b <- nodes ]
+
+{-
+-- | Within each level of the tree, merge all body nodes using the monoid
+-- operation.
+--
+-- Note that this is only valid for commutative monoids
+--
+reorder :: ConditionTree condition body -> ConditionTree condition body
+reorder (ConditionTree nodes) =
+ ConditionTree (body:conditions)
+ where
+ body = mappend [ b | Body b <- nodes ]
+ conditions =
+ -}
+
+
+-- | Resolve a condition tree by evaluating all the conditionals and merging
+-- together all those bodies for which the guard conditions are true.
+--
+-- This gives us the semantics of a 'PredicateExpr' so is crucial in the
+-- definition of other properties.
+--
+resolve :: Monoid body
+ => TotalValuation condition
+ -> ConditionTree condition body -> body
+resolve eval = flip evalTree mempty
+ where
+ evalTree (ConditionTree ns) accum = foldr evalNode accum ns
+
+ evalNode (Body body) accum = body `mappend` accum
+
+ evalNode (IfThen condition thenPart) accum
+ | eval condition = evalTree thenPart accum
+ | otherwise = accum
+
+ evalNode (IfElse condition thenPart elsePart) accum
+ | eval condition = evalTree thenPart accum
+ | otherwise = evalTree elsePart accum
+
+-- property: in all contexts,
+-- IfThen c t === IfThenElse c t mempty
+
+-- property: in all contexts,
+-- [IfThenElse c t e] === [IfThen c t, IfThen (Not c) e]
+
+-- property:
+-- n === IfThen True [n]
+-- IfThen False ns === mempty
+
+resolve' :: Monoid body
+ => PartialValuation condition
+ -> ConditionTree condition body -> Maybe body
+resolve' peval = flip evalTree mempty
+ where
+ evalTree (ConditionTree ns) accum = foldr evalNode accum ns
+
+ evalNode (Body body) accum = fmap (body `mappend`) accum
+
+ evalNode (IfThen condition thenPart) accum =
+ case applyPartialValuation peval condition of
+ Just True -> evalTree thenPart accum
+ Just False -> accum
+ Nothing -> Nothing
+
+ evalNode (IfElse condition thenPart elsePart) accum =
+ case applyPartialValuation peval condition of
+ Just True -> evalTree thenPart accum
+ Just False -> evalTree elsePart accum
+ Nothing -> Nothing
+
+-- | Simplify a condition tree by trying to evaluate or simplify all the
+-- conditional expressions. Whenever a conditional expression can be fully
+-- evaluated then we resolve the conditonal. Otherwise the conditional
+-- expression is just simplified and the conditional left unresolved.
+--
+-- * Property, simplify is an identity if no expressions are changed
+--
+-- > simplify Right = id
+--
+-- * Property, for all condition valuations v
+--
+-- > flatten . simplify (Left . v) = resolve v
+--
+simplify :: (condition -> Either Bool condition')
+ -> ConditionTree condition body
+ -> ConditionTree condition' body
+simplify simplifyCondition = simplifyTree
+ where
+ simplifyTree ns = ConditionTree (simplifyTree' ns [])
+ simplifyTree' (ConditionTree ns) ns' = foldr simplifyNode ns' ns
+
+ simplifyNode (Body body) ns = Body body : ns
+
+ simplifyNode (IfThen condition thenPart) ns =
+ case simplifyCondition condition of
+ Left True -> simplifyTree' thenPart ns
+ Left False -> ns
+ Right condition' -> IfThen condition' (simplifyTree thenPart) : ns
+
+ simplifyNode (IfElse condition thenPart elsePart) ns =
+ case simplifyCondition condition of
+ Left True -> simplifyTree' thenPart ns
+ Left False -> simplifyTree' elsePart ns
+ Right condition' -> IfElse condition' (simplifyTree thenPart)
+ (simplifyTree elsePart) : ns
+
+-- property: simplify (Left . f) == ConditionTree [ns] where all ns isbody
+-- that is, if we simplify every conditional we should end up with a (possibly
+-- empty) list of bodies (no conditionals).
+
+-- property: simplify Right = id
+
+mapCondition :: (condition -> condition')
+ -> ConditionTree condition body
+ -> ConditionTree condition' body
+mapCondition f = simplify (Right . f)
+
+-- property: canonical t => mapCondition id t = t
+
+-- | All the leaves of the condition tree along with the conditions along the
+-- path to that leaf.
+--
+-- Effectively this gives an alternative representation of the tree but without
+-- any of the sharing of conditions that we get from the tree structure.
+--
+paths :: (condition -> condition)
+ -> ConditionTree condition body
+ -> [([condition], body)]
+paths cnot = leaves . pathsTree []
+ where
+ pathsTree path (ConditionTree ns) = ConditionTree (map (pathsNode path) ns)
+
+ pathsNode path (Body body) =
+ Body (path, body)
+
+ pathsNode path (IfThen condition thenPart) =
+ IfThen condition (pathsTree (condition:path) thenPart)
+
+ pathsNode path (IfElse condition thenPart elsePart) =
+ IfElse condition (pathsTree ( condition:path) thenPart)
+ (pathsTree (cnot condition:path) elsePart)
diff --git a/experiment/configuration/Configuration.hs b/experiment/configuration/Configuration.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2e0e5dd2294c9c751a1f4c076fb443e31bd39408
--- /dev/null
+++ b/experiment/configuration/Configuration.hs
@@ -0,0 +1,214 @@
+module Configuration where
+
+import qualified Predicate
+import Predicate (Predicate)
+
+import qualified ConditionTree
+import qualified PredicateExpr
+import PredicateExpr (PredicateExpr)
+import ConditionTree (ConditionTree)
+import qualified BasePredicate
+import BasePredicate (BasePredicate, SystemParams)
+import PartialValuation (PartialValuation, TotalValuation)
+
+import Distribution.Package
+ ( Dependency(..), PackageName )
+import Distribution.Version
+ ( VersionRange )
+
+import Distribution.PackageDescription
+ ( FlagName, FlagAssignment )
+
+import Data.Monoid
+ ( Monoid(..) )
+import Data.Foldable
+ ( Foldable(fold) )
+import Data.List
+ ( partition )
+import Data.Maybe
+ ( isNothing )
+import qualified Data.Map as Map
+import Data.Map (Map)
+
+
+flatten :: GenericPackageDescription -> PackageDescription
+flatten = PackageDescription . ConditionTree.flatten . pkgCondTree
+
+-- | Finalise a generic package description by resolving all the conditonals.
+-- It requires a full flag assignment. Use 'search' if you do not know the
+-- flags or only have a partial flag assignment.
+--
+-- It returns Nothing if and only if the flag assignment is does not to cover
+-- all flags used in conditions. (CHECK this! does short-cut evaluation mean
+-- some flags may not be needed?)
+--
+finalise :: SystemParams -> FlagAssignment
+ -> GenericPackageDescription -> Maybe PackageDescription
+finalise sysParams flagAssignment =
+ fmap PackageDescription
+ . ConditionTree.resolve' (Predicate.eval sysParams flagAssignment)
+ . pkgCondTree
+
+--apply partial flag assignment
+-- :: FlagAssignment
+-- -> GenericPackageDescription -> GenericPackageDescription
+simplify :: PartialValuation BasePredicate
+ -> GenericPackageDescription -> GenericPackageDescription
+simplify v pkg =
+ pkg {
+ pkgCondTree = ConditionTree.simplify evalOrSimplify (pkgCondTree pkg)
+ }
+ where
+ evalOrSimplify :: Predicate -> Either Bool Predicate
+ evalOrSimplify cond = case PredicateExpr.simplify v cond of
+ PredicateExpr.PredExprLit b -> Left b
+ other -> Right other
+
+type ResolveError = ()
+
+resolve :: FlagAssignment
+ -> (Constraint -> Bool)
+ -> SystemParams
+ -> [Constraint]
+ -> GenericPackageDescription
+ -> Either ResolveError FlagAssignment
+resolve initialFlags satisfyDep sysParams extraConstraints pkg =
+ search
+ satisfiable
+ flagDoms
+ (simplifyTree (pkgCondTree pkg))
+
+ where
+ mkConstraints :: BuildInfo -> Constraints
+ mkConstraints = undefined
+
+ satisfiable :: Constraints -> Maybe ResolveError
+ satisfiable SatisfiableConstraints = Nothing
+ satisfiable UnsatisfiableConstraints = Just ()
+
+ flagDoms :: [FlagDomain]
+ flagDoms = undefined
+
+ --TODO: apply the initial flag assignment, and manual flags
+ -- extract the remaining used flags after simplifying
+ -- construct all test flag assignments
+
+ --TODO: merge constraints on the same level
+
+ simplifyTree :: ConditionTree (PredicateExpr BasePredicate) BuildInfo
+ -> ConditionTree (PredicateExpr FlagName) Constraints
+ simplifyTree = fmap mkConstraints
+ . ConditionTree.simplify (literal . simplifyExpr)
+ where
+ literal (PredicateExpr.PredExprLit b) = Left b
+ literal e = Right e
+
+ simplifyExpr :: PredicateExpr BasePredicate
+ -> PredicateExpr FlagName
+ simplifyExpr =
+ PredicateExpr.simplify' (BasePredicate.applySystemParams sysParams)
+
+
+search :: forall constraints error
+ . Monoid constraints
+ => (constraints -> Maybe error)
+ -> [FlagDomain]
+ -> ConditionTree (PredicateExpr FlagName) constraints
+ -> Either error FlagAssignment
+search satisfiable flagDoms tree =
+ case satisfiable (mconcat (ConditionTree.unconditional tree)) of
+ Just err -> Left err
+ Nothing -> tryAllAssignments Nothing assignments
+
+ where
+ -- Find the first assignment that works,
+ -- though if all fail then return the first failure
+ tryAllAssignments (Just err) [] = Left err
+ tryAllAssignments Nothing [] = error "impossible"
+ tryAllAssignments merr (a:as) =
+ case checkAssignment a tree of
+ Just err' | isNothing merr -> tryAllAssignments (Just err') as
+ | otherwise -> tryAllAssignments merr as
+ Nothing -> Right a
+
+ assignments = allAssignments (reorderFlagDomains flagDoms)
+
+ checkAssignment :: FlagAssignment
+ -> ConditionTree (PredicateExpr FlagName) constraints
+ -> Maybe error
+ checkAssignment flagAssignment =
+ satisfiable
+ . ConditionTree.resolve (PredicateExpr.eval (evalFlags flagAssignment))
+
+ evalFlags :: FlagAssignment -> TotalValuation FlagName
+ evalFlags flagAssignment flag =
+ case lookup flag flagAssignment of
+ Just val -> val
+ Nothing -> error "missing flag"
+
+ -- | Generate all possible flag assignements given the domain of each flag
+ allAssignments :: [FlagDomain] -> [FlagAssignment]
+ allAssignments [] = [ [] ]
+ allAssignments ((flag, dom):doms) = [ (flag, val):flags
+ | val <- dom
+ , flags <- allAssignments doms ]
+
+ -- | If flags can only take one possible value then put them first
+ reorderFlagDomains :: [FlagDomain] -> [FlagDomain]
+ reorderFlagDomains doms =
+ let (singles, rest) = partition ((==1) . length . snd) doms
+ in singles ++ rest
+
+
+type FlagDomain = (FlagName, [Bool])
+
+
+data GenericPackageDescription = GenericPackageDescription {
+ flags :: [Flag],
+ pkgCondTree :: ConditionTree Predicate BuildInfo
+}
+
+data Flag = Flag {
+ flagName :: FlagName,
+ flagDefault :: Bool,
+ flagManual :: Bool
+ }
+ deriving (Show, Eq)
+
+data PackageDescription = PackageDescription {
+ buildInfo :: BuildInfo
+ }
+
+data BuildInfo = BuildInfo {
+ buildDepends :: [Dependency],
+ pkgconfigDepends :: [Dependency],
+ extralibs :: [String]
+ }
+
+instance Monoid BuildInfo where
+ mempty = BuildInfo {
+ buildDepends = [],
+ pkgconfigDepends = [],
+ extralibs = []
+ }
+ mappend a b = BuildInfo {
+ buildDepends = combine buildDepends,
+ pkgconfigDepends = combine pkgconfigDepends,
+ extralibs = combine extralibs
+ }
+ where combine f = f a `mappend` f b
+
+data Constraint = HaskellLibPackage PackageName VersionRange
+ | PkgConfigPackage PackageName VersionRange
+ | CLib String
+ | BuildTool String
+
+data Constraints
+ = SatisfiableConstraints {
+ hsLibVersions :: Map PackageName VersionRange,
+ pkgConfigVersions :: Map PackageName VersionRange
+
+ }
+ | UnsatisfiableConstraints
+
+instance Monoid Constraints where
diff --git a/experiment/configuration/PartialValuation.hs b/experiment/configuration/PartialValuation.hs
new file mode 100644
index 0000000000000000000000000000000000000000..53b09bf1cfcd83a0c3f698dd532b7389d9468531
--- /dev/null
+++ b/experiment/configuration/PartialValuation.hs
@@ -0,0 +1,62 @@
+module PartialValuation where
+
+import Data.Monoid
+ ( Monoid(..) )
+import Control.Monad
+ ( liftM, liftM2 )
+import qualified Data.Foldable as Foldable
+ ( Foldable(foldMap, foldr), toList )
+
+import Prelude hiding (null)
+
+-- | A valuation on some base predicate type.
+--
+type TotalValuation base = (base -> Bool)
+
+-- | A partial valuation on some base predicate. This is useful when we have
+-- only partial information but still wish to simplify an expression using the
+-- predicates.
+--
+-- In particular, a partial valuation is a 'Monoid' via 'null' and 'extend'.
+--
+newtype PartialValuation base
+ = PartialValuation { applyPartialValuation :: base -> Maybe Bool }
+
+-- | A null valuation. It gives no value for all predicates.
+--
+null :: PartialValuation base
+null = PartialValuation (const Nothing)
+
+-- | Extend one partial valuation with another.
+--
+-- In the valuation @v' `extend` v@, the valuation @v@ is being extended by the
+-- valuation @v'@. That means values returned by the first take precedence over
+-- those returned by the second.
+--
+extend :: PartialValuation base
+ -> PartialValuation base
+ -> PartialValuation base
+extend (PartialValuation v) (PartialValuation v') =
+ PartialValuation $ \x -> v x `override` v' x
+ where
+ override a@(Just _) _ = a
+ override _ b = b
+
+instance Monoid (PartialValuation base) where
+ mempty = null
+ mappend = extend
+
+
+-- | Extend one a total valuation with a partial valuation to give a total
+-- valuation.
+--
+-- Values from the partial valuation take precedence.
+--
+extend' :: PartialValuation base
+ -> TotalValuation base
+ -> TotalValuation base
+extend' (PartialValuation v) v' =
+ \x -> v x `override` v' x
+ where
+ override (Just a) _ = a
+ override _ b = b
diff --git a/experiment/configuration/Predicate.hs b/experiment/configuration/Predicate.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a4829a320c9779dd03417f92c16f900557d9abb6
--- /dev/null
+++ b/experiment/configuration/Predicate.hs
@@ -0,0 +1,38 @@
+module Predicate (
+
+ Predicate,
+ eval,
+ applySystemParams,
+ applyFlagAssignment,
+
+ ) where
+
+import qualified BasePredicate
+import BasePredicate (BasePredicate, SystemParams)
+
+import qualified PredicateExpr
+import PredicateExpr (PredicateExpr)
+
+import PartialValuation
+ ( PartialValuation )
+
+import Distribution.PackageDescription
+ ( FlagName, FlagAssignment )
+
+type Predicate = PredicateExpr BasePredicate
+
+eval :: SystemParams
+ -> FlagAssignment
+ -> PartialValuation Predicate
+eval sysParams flagAssignment =
+ PredicateExpr.eval' (BasePredicate.eval sysParams flagAssignment)
+
+applySystemParams :: SystemParams
+ -> Predicate -> PredicateExpr FlagName
+applySystemParams sysParams =
+ PredicateExpr.simplify' (BasePredicate.applySystemParams sysParams)
+
+applyFlagAssignment :: FlagAssignment
+ -> Predicate -> Predicate
+applyFlagAssignment flagAssignment =
+ PredicateExpr.simplify (BasePredicate.applyFlagAssignment flagAssignment)
diff --git a/experiment/configuration/PredicateExpr.hs b/experiment/configuration/PredicateExpr.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b9ca2924910117d7fdc1aa2d0e14d01e922f21ad
--- /dev/null
+++ b/experiment/configuration/PredicateExpr.hs
@@ -0,0 +1,192 @@
+module PredicateExpr (
+
+ PredicateExpr(..),
+ fold,
+
+ eval, eval',
+ simplify, simplify',
+
+ basePredicates,
+
+
+ PartialValuation(..),
+ ) where
+
+import PartialValuation
+
+import Data.Monoid
+ ( Monoid(..) )
+import Control.Monad
+ ( liftM, liftM2 )
+import qualified Data.Foldable as Foldable
+ ( Foldable(foldMap, foldr), toList )
+
+-- | A predicate expression. It is parameterised over the type of the base
+-- predicate.
+--
+data PredicateExpr base
+ = PredExprBase base
+ | PredExprLit Bool
+ | PredExprNot (PredicateExpr base)
+ | PredExprAnd (PredicateExpr base) (PredicateExpr base)
+ | PredExprOr (PredicateExpr base) (PredicateExpr base)
+ deriving (Eq, Show)
+
+-- | The natural fold on the 'PredicateExpr' type.
+--
+-- For example, an evaluation function is just:
+--
+-- > eval :: PredicateExpr BasePredicate -> Bool
+-- > eval = fold BasePredicate.eval id not (&&) (||)
+--
+fold :: (base -> a) -> (Bool -> a)
+ -> (a -> a) -> (a -> a -> a) -> (a -> a -> a)
+ -> PredicateExpr base -> a
+fold fbase flit fnot fand for = fold'
+ where
+ fold' (PredExprBase base) = fbase base
+ fold' (PredExprLit lit) = flit lit
+ fold' (PredExprNot a) = fnot (fold' a)
+ fold' (PredExprAnd a b) = fand (fold' a) (fold' b)
+ fold' (PredExprOr a b) = for (fold' a) (fold' b)
+{-# INLINE fold #-}
+
+instance Functor PredicateExpr where
+ fmap f = fold (PredExprBase . f)
+ PredExprLit PredExprNot PredExprAnd PredExprOr
+
+instance Foldable.Foldable PredicateExpr where
+ foldMap f = fold f (const mempty) id mappend mappend
+
+ foldr f z (PredExprBase b) = f b z
+ foldr f z (PredExprLit _) = z
+ foldr f z (PredExprNot a) = Foldable.foldr f z a
+ foldr f z (PredExprAnd a b) = Foldable.foldr f (Foldable.foldr f z b) a
+ foldr f z (PredExprOr a b) = Foldable.foldr f (Foldable.foldr f z b) a
+
+-- | List all the base predicates occuring in the expression.
+--
+basePredicates :: PredicateExpr base -> [base]
+basePredicates = Foldable.toList
+
+-- | Given a valuation on the base predicate, extend it to a valuation on the
+-- whole 'PredicateExpr'. This gives the semantics of a 'PredicateExpr'
+--
+eval :: TotalValuation base
+ -> TotalValuation (PredicateExpr base)
+eval evalBase = fold evalBase id not (&&) (||)
+
+-- | Given a partial valuation on the base predicate, extend it to a partial
+-- valuation on the whole 'PredicateExpr'.
+--
+-- * Property: with a total valuation for the base predicate, 'eval'' is the
+-- same as 'eval':
+--
+-- > eval' (Just . v) = Just . eval v
+--
+-- * Property: the evaluation is 'Nothing' if and only if the valuation is
+-- 'Nothing' on any value in the expression
+--
+-- > eval' v e == Nothing
+-- > = any (\e' -> v e' == Nothing) (basePredicates e)
+--
+eval' :: PartialValuation base
+ -> PartialValuation (PredicateExpr base)
+eval' (PartialValuation evalBase) = PartialValuation $
+ fold evalBase return (liftM not) (liftM2 (&&)) (liftM2 (||))
+
+-- | Simplify a 'PredicateExpr', given a function to evaluate or simplify
+-- base predicates. It can do some simple algebraic simplification even if no
+-- base predicates are evaluated.
+--
+-- * Property: simplify is the syntactic equivalent of evaluation. For any
+-- partial valuation, using that to syntacticly simplify gives an expression
+-- with the same set of valuations as the original expression with the partial
+-- valuation extend to a full valuation.
+--
+-- > eval v (simplify (toEither v') e) = eval (extend v' v) e
+-- > where
+-- > extend f' f = \x -> f' x `override` f x
+-- > override = flip fromMaybe
+-- >
+-- > toEither f = \x -> maybe (Right x) Left (f x)
+-- > toEither :: (b -> Maybe a )
+-- > -> (b -> Either a b)
+--
+-- * Property: when doing no evaluation of the base predicate, simplify does
+-- not change the valuations of the expression. Or to put it another way,
+-- @simplify Right@ is an identify function on the semantics of expressions.
+-- Note this property is a simple consequence of the first property. If we pick
+-- @v' x = Nothing@ then we can derive this property.
+--
+-- > eval v (simplify Right e) = eval v e
+--
+-- * Property: when doing full evaluation of the base predicate, simplify does
+-- sufficient simplification to be equivalent to full evaluation using 'eval'.
+--
+-- > simplify (Left . v) e == PredExprLit (eval v e)
+--
+-- * Property: when doing no evaluation of the base predicate, simplify
+-- eliminates all True and False literals occuring as subexpressions.
+--
+-- > not (literalAsSubExpr (simplify Right e))
+-- > where
+-- > literalAsSubExpr (PredExprLit _) = False
+-- > literalAsSubExpr e = PredicateExpr.fold (const False) (const True)
+-- > id (||) (||) e
+--
+-- The first property tells us simplify does correct simplification though
+-- not necessarily that it does any evaluation at all. The third and fourth
+-- properties tell us that it's doing enough simplification. Note that due to
+-- the symmetry of '&&' and '||', the second property is not enough to tell us
+-- we're doing full simplification. Full evaluation only needs to reduce on one
+-- side of '&&' and '||', not on both. The third property shows we're
+-- simplifying on both sides.
+--
+-- * Property: idempotentcy, at least for a partial valuation that keeps the
+-- old expression when it gives it no value. In other words 'simplify' does
+-- all it's work in one go.
+--
+-- > simplify v' . simplify v' = simplify v'
+-- > where
+-- > v' = toEither v
+-- > toEither f x = maybe (Right x) Left (f x)
+-- > toEither :: (b -> Maybe a )
+-- > -> (b -> Either a b)
+--
+simplify :: PartialValuation base
+ -> PredicateExpr base
+ -> PredicateExpr base
+simplify v = simplify' v'
+ where
+ v' x = maybe (Right x) Left (applyPartialValuation v x)
+
+simplify' :: (base -> Either Bool base')
+ -> PredicateExpr base
+ -> PredicateExpr base'
+simplify' valuation =
+ fold simplifyBase simplifyLit
+ simplifyNot simplifyAnd simplifyOr
+ where
+ simplifyBase predicate =
+ case valuation predicate of
+ Left bool -> PredExprLit bool
+ Right predicate' -> PredExprBase predicate'
+
+ simplifyLit lit = PredExprLit lit
+
+ simplifyNot (PredExprLit lit) = PredExprLit (not lit)
+ simplifyNot (PredExprNot e) = e
+ simplifyNot e = PredExprNot e
+
+ simplifyAnd (PredExprLit True) e2 = e2
+ simplifyAnd (PredExprLit False) _ = PredExprLit False
+ simplifyAnd e1 (PredExprLit True) = e1
+ simplifyAnd _ (PredExprLit False) = PredExprLit False
+ simplifyAnd e1 e2 = PredExprAnd e1 e2
+
+ simplifyOr (PredExprLit True) _ = PredExprLit True
+ simplifyOr (PredExprLit False) e2 = e2
+ simplifyOr _ (PredExprLit True) = PredExprLit True
+ simplifyOr e1 (PredExprLit False) = e1
+ simplifyOr e1 e2 = PredExprOr e1 e2
diff --git a/experiment/configuration/Test/BasePredicate.hs b/experiment/configuration/Test/BasePredicate.hs
new file mode 100644
index 0000000000000000000000000000000000000000..11b4603e53875784fc377c4d6813c0a2450d1ae9
--- /dev/null
+++ b/experiment/configuration/Test/BasePredicate.hs
@@ -0,0 +1,44 @@
+module Test.BasePredicate where
+
+import BasePredicate
+import PartialValuation
+
+import Test.QuickCheck
+
+import Control.Monad (liftM, liftM2, liftM3)
+import Data.Monoid
+ ( Monoid(..) )
+
+instance Arbitrary SystemParams where
+ arbitrary = liftM3 SystemParams arbitrary arbitrary arbitrary
+ shrink (SystemParams os arch compid) =
+ [ SystemParams os' arch compid | os' <- shrink os ]
+ ++ [ SystemParams os arch' compid | arch' <- shrink arch ]
+ ++ [ SystemParams os arch compid' | compid' <- shrink compid ]
+
+instance Arbitrary BasePredicate where
+ arbitrary = frequency
+ [ (1, liftM OSPredicate arbitrary)
+ , (1, liftM ArchPredicate arbitrary)
+ , (1, liftM2 CompilerPredicate arbitrary arbitrary)
+ , (2, liftM FlagPredicate arbitrary)
+ ]
+ shrink (OSPredicate os ) = [ OSPredicate os' | os' <- shrink os ]
+ shrink (ArchPredicate arch) = [ ArchPredicate arch' | arch' <- shrink arch ]
+ shrink (CompilerPredicate comp range) =
+ [ CompilerPredicate comp' range | comp' <- shrink comp ]
+ ++ [ CompilerPredicate comp range' | range' <- shrink range ]
+ shrink (FlagPredicate flag) = [ FlagPredicate flag' | flag' <- shrink flag ]
+
+
+v === v' = forAll arbitrary $ \e -> applyPartialValuation v e
+ == applyPartialValuation v' e
+
+prop_eval sysParams flags = eval sysParams flags
+ === eval' sysParams flags
+ where
+ eval' (SystemParams os arch comp) flagAssignment =
+ applyOS os
+ `mappend` applyArch arch
+ `mappend` applyCompiler comp
+ `mappend` applyFlagAssignment flagAssignment
diff --git a/experiment/configuration/Test/ConditionTree.hs b/experiment/configuration/Test/ConditionTree.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a3335b65720bce07a792095f9feeb912eca6a2e1
--- /dev/null
+++ b/experiment/configuration/Test/ConditionTree.hs
@@ -0,0 +1,78 @@
+module Test.ConditionTree where
+
+import ConditionTree
+import Test.QuickCheck
+import qualified Test.Laws as Laws
+import Test.Poly (A, B, C, M)
+
+import Control.Monad (liftM, liftM2, liftM3)
+
+import qualified Data.Foldable as Foldable
+import Data.Monoid (Sum(..))
+
+instance (Arbitrary condition, Arbitrary body)
+ => Arbitrary (ConditionTree condition body) where
+ arbitrary = sized $ \n -> do
+ k <- choose (0,n)
+ liftM ConditionTree $
+ sequence [ resize (n `div` k) arbitrary | _ <- [1..k] ]
+
+ shrink (ConditionTree ns) = [ ConditionTree ns' | ns' <- shrink ns ]
+
+instance (Arbitrary condition, Arbitrary body)
+ => Arbitrary (ConditionNode condition body) where
+ arbitrary = sized arbNode
+ where
+ arbNode n = frequency $
+ [ (2, liftM Body arbitrary)
+ ] ++ concat
+ [ [ (1, liftM2 IfThen arbitrary arbTree1)
+ , (1, liftM3 IfElse arbitrary arbTree2 arbTree2)
+ ]
+ | n > 0
+ ]
+ where
+ arbTree1 = resize (n `div` 2) arbitrary
+ arbTree2 = resize (n `div` 2) arbitrary
+
+ shrink (Body b) = [ Body b' | b' <- shrink b ]
+ shrink (IfThen c e1) = (case e1 of ConditionTree x -> x)
+ ++ [ IfThen c' e1 | c' <- shrink c ]
+ ++ [ IfThen c e1' | e1' <- shrink e1 ]
+ shrink (IfElse c e1 e2) = (case e1 of ConditionTree x -> x)
+ ++ (case e2 of ConditionTree x -> x)
+ ++ [ IfElse c' e1 e2 | c' <- shrink c ]
+ ++ [ IfElse c e1' e2 | e1' <- shrink e1 ]
+ ++ [ IfElse c e1 e2' | e2' <- shrink e2 ]
+
+prop_tree_fmap_1 :: ConditionTree C M -> Bool
+prop_tree_fmap_1 = Laws.fmap_1
+
+prop_tree_fmap_2 :: (A -> B) -> (M -> A) -> ConditionTree C M -> Bool
+prop_tree_fmap_2 = Laws.fmap_2
+
+prop_node_fmap_1 :: ConditionNode C M -> Bool
+prop_node_fmap_1 = Laws.fmap_1
+
+prop_node_fmap_2 :: (A -> B) -> (M -> A) -> ConditionNode C M -> Bool
+prop_node_fmap_2 = Laws.fmap_2
+
+prop_tree_foldable_1 :: ConditionTree C M -> Bool
+prop_tree_foldable_1 = Laws.foldable_1
+
+prop_tree_foldable_2 :: (A -> B -> B) -> B -> ConditionTree C A -> Bool
+prop_tree_foldable_2 = Laws.foldable_2
+
+prop_node_foldable_1 :: ConditionNode C M -> Bool
+prop_node_foldable_1 = Laws.foldable_1
+
+prop_node_foldable_2 :: (A -> B -> B) -> B -> ConditionNode C A -> Bool
+prop_node_foldable_2 = Laws.foldable_2
+
+prop_resolve_1 :: (C -> Bool) -> ConditionTree.ConditionTree C M -> Bool
+prop_resolve_1 v t = resolve v t == flatten (simplify (Left . v) t)
+
+prop_simplify_1 t = simplify Right t == t
+
+size :: ConditionNode a b -> Int
+size = length . Foldable.toList
diff --git a/experiment/configuration/Test/Configuration.hs b/experiment/configuration/Test/Configuration.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a361242a820695ee8760fc7d594e63488ed0b528
--- /dev/null
+++ b/experiment/configuration/Test/Configuration.hs
@@ -0,0 +1,63 @@
+module Test.Configuration where
+
+import qualified Predicate
+import Predicate (Predicate)
+
+import BasePredicate (SystemParams)
+
+import Distribution.Package
+ ( Dependency(..) )
+
+import Distribution.PackageDescription
+ ( FlagAssignment )
+
+import Data.Monoid
+ ( Monoid(..) )
+import Data.Foldable
+ ( Foldable(fold) )
+
+flatten :: GenericPackageDescription -> PackageDescription
+flatten = PackageDescription . flattenConditionTree
+
+finalise :: FlagAssignment -> SystemParams
+ -> GenericPackageDescription -> PackageDescription
+finalise = error "TODO: finalise"
+
+--apply partial flag assignment
+-- :: FlagAssignment
+-- -> GenericPackageDescription -> GenericPackageDescription
+
+type DepInfo = ()
+
+search :: SystemParams -> DepInfo
+ -> GenericPackageDescription -> Maybe FlagAssignment
+search = error "TODO: search"
+
+
+
+type GenericPackageDescription
+ = ConditionTree Predicate BuildInfo
+
+
+data PackageDescription = PackageDescription {
+ buildInfo :: BuildInfo
+}
+
+data BuildInfo = BuildInfo {
+ buildDepends :: [Dependency],
+ pkgconfigDepends :: [Dependency],
+ extralibs :: [String]
+}
+
+instance Monoid BuildInfo where
+ mempty = BuildInfo {
+ buildDepends = [],
+ pkgconfigDepends = [],
+ extralibs = []
+ }
+ mappend a b = BuildInfo {
+ buildDepends = combine buildDepends,
+ pkgconfigDepends = combine pkgconfigDepends,
+ extralibs = combine extralibs
+ }
+ where combine f = f a `mappend` f b
diff --git a/experiment/configuration/Test/Laws.hs b/experiment/configuration/Test/Laws.hs
new file mode 100644
index 0000000000000000000000000000000000000000..62450dbe725428bbeef2c8ff6148dc969515cbcb
--- /dev/null
+++ b/experiment/configuration/Test/Laws.hs
@@ -0,0 +1,64 @@
+module Test.Laws where
+
+import Prelude
+import Prelude (Functor(..))
+import Data.Monoid (Monoid(..), Endo(..))
+import qualified Data.Foldable as Foldable
+
+-- | The first 'fmap' law
+--
+-- > fmap id == id
+--
+fmap_1 :: (Eq (f a), Functor f) => f a -> Bool
+fmap_1 x = fmap id x == x
+
+-- | The second 'fmap' law
+--
+-- > fmap (f . g) == fmap f . fmap g
+--
+fmap_2 :: (Eq (f c), Functor f) => (b -> c) -> (a -> b) -> f a -> Bool
+fmap_2 f g x = fmap (f . g) x == (fmap f . fmap g) x
+
+
+-- | The monoid identity law, 'mempty' is a left and right identity of
+-- 'mappend':
+--
+-- > mempty `mappend` x = x
+-- > x `mappend` mempty = x
+--
+monoid_1 :: (Eq a, Data.Monoid.Monoid a) => a -> Bool
+monoid_1 x = mempty `mappend` x == x
+ && x `mappend` mempty == x
+
+-- | The monoid associativity law, 'mappend' must be associative.
+--
+-- > (x `mappend` y) `mappend` z = x `mappend` (y `mappend` z)
+--
+monoid_2 :: (Eq a, Data.Monoid.Monoid a) => a -> a -> a -> Bool
+monoid_2 x y z = (x `mappend` y) `mappend` z
+ == x `mappend` (y `mappend` z)
+
+-- | The 'mconcat' definition. It can be overidden for the sake of effeciency
+-- but it must still satisfy the property given by the default definition:
+--
+-- > mconcat = foldr mappend mempty
+--
+monoid_3 :: (Eq a, Data.Monoid.Monoid a) => [a] -> Bool
+monoid_3 xs = mconcat xs == foldr mappend mempty xs
+
+
+-- | First 'Foldable' law
+--
+-- > Foldable.fold = Foldable.foldr mappend mempty
+--
+foldable_1 :: (Foldable.Foldable t, Monoid m, Eq m) => t m -> Bool
+foldable_1 x = Foldable.fold x == Foldable.foldr mappend mempty x
+
+-- | Second 'Foldable' law
+--
+-- > foldr f z t = appEndo (foldMap (Endo . f) t) z
+--
+foldable_2 :: (Foldable.Foldable t, Eq b)
+ => (a -> b -> b) -> b -> t a -> Bool
+foldable_2 f z t = Foldable.foldr f z t
+ == appEndo (Foldable.foldMap (Endo . f) t) z
diff --git a/experiment/configuration/Test/PartialValuation.hs b/experiment/configuration/Test/PartialValuation.hs
new file mode 100644
index 0000000000000000000000000000000000000000..47b1f0e2a0c778b4bb6717cc59b075ba3b0c2200
--- /dev/null
+++ b/experiment/configuration/Test/PartialValuation.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE StandaloneDeriving #-}
+module Test.PartialValuation where
+
+import BasePredicate
+import PartialValuation
+
+import Test.QuickCheck
+import Test.Poly (A)
+
+import Data.Monoid
+ ( Monoid(..) )
+
+
+instance CoArbitrary a => Arbitrary (PartialValuation a) where
+ arbitrary = fmap PartialValuation arbitrary
+
+deriving instance Show (PartialValuation a)
+
+infix 4 ===
+
+(===) :: (Arbitrary a, Show a) => PartialValuation a -> PartialValuation a -> Property
+v === v' = forAll arbitrary $ \e ->
+ applyPartialValuation v e
+ == applyPartialValuation v' e
+
+prop_monoid_1 :: PartialValuation A -> Property
+prop_monoid_1 v = mempty `mappend` v === v
+
+prop_monoid_2 :: PartialValuation A -> Property
+prop_monoid_2 v = v `mappend` mempty === v
+
+prop_monoid_3 :: PartialValuation A -> PartialValuation A -> PartialValuation A -> Property
+prop_monoid_3 x y z = (x `mappend` y) `mappend` z
+ === x `mappend` (y `mappend` z)
diff --git a/experiment/configuration/Test/Poly.hs b/experiment/configuration/Test/Poly.hs
new file mode 100644
index 0000000000000000000000000000000000000000..975e453932b1a248ac15df08e518d06c963770cd
--- /dev/null
+++ b/experiment/configuration/Test/Poly.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Test.Poly where
+
+import Data.Monoid (Monoid)
+
+import Test.QuickCheck (Arbitrary, CoArbitrary)
+import Text.Show.Functions
+
+newtype A = A Int deriving (Eq, Show, Arbitrary, CoArbitrary)
+newtype B = B Int deriving (Eq, Show, Arbitrary, CoArbitrary)
+newtype C = C Int deriving (Eq, Show, Arbitrary, CoArbitrary)
+
+newtype M = M [Int] deriving (Eq, Show, Arbitrary, CoArbitrary, Monoid)
diff --git a/experiment/configuration/Test/Predicate.hs b/experiment/configuration/Test/Predicate.hs
new file mode 100644
index 0000000000000000000000000000000000000000..88ac786aa279c5c64c577aeac07a4cec061b4902
--- /dev/null
+++ b/experiment/configuration/Test/Predicate.hs
@@ -0,0 +1,35 @@
+module Test.Predicate (
+
+ Predicate,
+ eval,
+ applySystemParams,
+ applyFlagAssignment,
+
+ ) where
+
+import qualified BasePredicate
+import BasePredicate (BasePredicate, SystemParams)
+
+import qualified PredicateExpr
+import PredicateExpr (PredicateExpr)
+
+import Distribution.PackageDescription
+ ( FlagName, FlagAssignment )
+
+type Predicate = PredicateExpr BasePredicate
+
+eval :: SystemParams
+ -> FlagAssignment
+ -> Predicate -> Maybe Bool
+eval sysParams flagAssignment =
+ PredicateExpr.eval' (BasePredicate.eval sysParams flagAssignment)
+
+applySystemParams :: SystemParams
+ -> Predicate -> PredicateExpr FlagName
+applySystemParams sysParams =
+ PredicateExpr.simplify (BasePredicate.applySystemParams sysParams)
+
+applyFlagAssignment :: FlagAssignment
+ -> Predicate -> Predicate
+applyFlagAssignment flagAssignment =
+ PredicateExpr.simplify (BasePredicate.applyFlagAssignment flagAssignment)
diff --git a/experiment/configuration/Test/PredicateExpr.hs b/experiment/configuration/Test/PredicateExpr.hs
new file mode 100644
index 0000000000000000000000000000000000000000..25ff0a371f809fe6d75c7bc6506a41bdc5aa090c
--- /dev/null
+++ b/experiment/configuration/Test/PredicateExpr.hs
@@ -0,0 +1,109 @@
+module Test.PredicateExpr where
+
+import PredicateExpr
+import qualified PartialValuation
+import PartialValuation (PartialValuation, TotalValuation)
+
+import Test.PartialValuation
+
+import Test.QuickCheck
+import qualified Test.Laws as Laws
+import Test.Poly (A, B, C, M)
+
+import Text.Show.Functions
+
+import Control.Monad (MonadPlus(..), liftM, liftM2)
+import qualified Data.Foldable as Foldable
+import Data.Maybe (fromMaybe)
+import Data.Monoid (Monoid(mempty))
+
+instance Arbitrary base => Arbitrary (PredicateExpr base) where
+ arbitrary = sized arbExp
+ where
+ arbExp n = frequency $
+ [ (2, liftM PredExprBase arbitrary)
+ , (1, liftM PredExprLit arbitrary)
+ ] ++ concat
+ [ [ (2, liftM PredExprNot arbExp1)
+ , (2, liftM2 PredExprAnd arbExp2 arbExp2)
+ , (2, liftM2 PredExprOr arbExp2 arbExp2)
+ ]
+ | n > 0
+ ]
+ where
+ arbExp1 = arbExp (n-1)
+ arbExp2 = arbExp (n `div` 2)
+
+ shrink (PredExprBase base) = [ PredExprBase base' | base' <- shrink base ]
+ shrink (PredExprLit lit) = []
+ shrink (PredExprNot e ) = e
+ : [ PredExprNot e' | e' <- shrink e ]
+ shrink (PredExprAnd e1 e2) = [e1, e2]
+ ++ [ PredExprAnd e1' e2 | e1' <- shrink e1 ]
+ ++ [ PredExprAnd e1 e2' | e2' <- shrink e2 ]
+ shrink (PredExprOr e1 e2) = [e1, e2]
+ ++ [ PredExprOr e1' e2 | e1' <- shrink e1 ]
+ ++ [ PredExprOr e1 e2' | e2' <- shrink e2 ]
+
+-- fold is an identity, given suitable constructors as args
+prop_fold_id :: PredicateExpr A -> Bool
+prop_fold_id x = predId x == x
+ where predId = PredicateExpr.fold PredExprBase PredExprLit
+ PredExprNot PredExprAnd PredExprOr
+
+-- Check basePredicates against an oracle that's obviously(!) right.
+prop_basePredicates_1 :: PredicateExpr A -> Bool
+prop_basePredicates_1 x = basePredicates x == basePredicates' x
+ where
+ basePredicates' = PredicateExpr.fold (\x -> [x]) (const []) id (++) (++)
+
+-- PredicateExpr is in Functor, check the functor laws
+prop_fmap_1 :: PredicateExpr A -> Bool
+prop_fmap_1 = Laws.fmap_1
+
+prop_fmap_2 :: (B -> C) -> (A -> B) -> PredicateExpr A -> Bool
+prop_fmap_2 = Laws.fmap_2
+
+-- PredicateExpr is in Foldable, check the laws
+prop_foldable_1 :: PredicateExpr M -> Bool
+prop_foldable_1 = Laws.foldable_1
+
+prop_foldable_2 :: (A -> B -> B) -> B -> PredicateExpr A -> Bool
+prop_foldable_2 = Laws.foldable_2
+
+-- with a total valuation for the base predicate, eval' is the same as eval
+prop_eval'_1 :: TotalValuation A -> PredicateExpr A -> Bool
+prop_eval'_1 v e = eval' (Just . v) e == Just (eval v e)
+
+-- the overall evaluation of the expression is Nothing if and only if the
+-- base valuation is Nothing on any base value in the expression
+prop_eval'_2 :: (A -> Maybe Bool) -> PredicateExpr A -> Bool
+prop_eval'_2 v e = (eval' v e == Nothing)
+ == any (\e' -> v e' == Nothing) (basePredicates e)
+
+prop_simplify_1 :: PartialValuation A -> TotalValuation A -> PredicateExpr A -> Bool
+prop_simplify_1 v' v e = eval (PartialValuation.extend' v' v) e
+ == eval v (simplify v' e)
+ where
+ extend f' f = \x -> applyPartialValuation f' x `override` f x
+ override = flip fromMaybe
+
+prop_simplify_2 :: TotalValuation A -> PredicateExpr A -> Bool
+prop_simplify_2 v e = eval v (simplify mempty e) == eval v e
+
+prop_simplify_3 :: TotalValuation A -> PredicateExpr A -> Bool
+prop_simplify_3 v e = simplify v' e == PredExprLit (eval v e)
+ where
+ v' = PartialValuation.liftTotal v
+
+prop_simplify_4 :: PredicateExpr A -> Bool
+prop_simplify_4 e = not (literalAsSubExpr (simplify PartialValuation.null e))
+ where
+ literalAsSubExpr (PredExprLit _) = False
+ literalAsSubExpr e = PredicateExpr.fold (const False) (const True)
+ id (||) (||) e
+-- idempotentcy, at least for a partial valuation that keeps the old expression
+-- when it gives it no value. In other words simplify does all it's work in one
+-- go.
+prop_simplify_5 :: PartialValuation A -> PredicateExpr A -> Bool
+prop_simplify_5 v e = simplify v (simplify v e) == simplify v e