haskus-utils-1.5: src/lib/Haskus/Utils/Solver.hs
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
-- | Simple Constraint solver
module Haskus.Utils.Solver
(
-- * Oracle
PredState (..)
, PredOracle
, makeOracle
, oraclePredicates
, emptyOracle
, oracleUnion
, predIsSet
, predIsUnset
, predIsUndef
, predIsInvalid
, predIs
, predState
, predAdd
-- * Constraint
, Constraint (..)
, constraintOptimize
, constraintSimplify
-- * Rule
, Rule (..)
, ruleSimplify
, evalsTo
, MatchResult (..)
-- * Predicated data
, Predicated (..)
, createPredicateTable
, initP
, applyP
, resultP
)
where
import Haskus.Utils.Maybe
import Haskus.Utils.Flow
import Haskus.Utils.List
import Haskus.Utils.Map.Strict (Map)
import qualified Haskus.Utils.Map.Strict as Map
import Control.Arrow (first,second)
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (pred,length)
-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XFlexibleContexts
-- >>> :set -XTypeFamilies
-------------------------------------------------------
-- Constraint
-------------------------------------------------------
-- | Predicate state
data PredState
= SetPred -- ^ Set predicate
| UnsetPred -- ^ Unset predicate
| UndefPred -- ^ Undefined predicate
| InvalidPred -- ^ Invalid predicate (can't be used)
deriving (Show,Eq,Ord)
-- | Predicate oracle
type PredOracle p = Map p PredState
-- | Ask an oracle if a predicate is set
predIsSet :: Ord p => PredOracle p -> p -> Bool
predIsSet oracle p = predIs oracle p SetPred
-- | Ask an oracle if a predicate is unset
predIsUnset :: Ord p => PredOracle p -> p -> Bool
predIsUnset oracle p = predIs oracle p UnsetPred
-- | Ask an oracle if a predicate is undefined
predIsUndef :: Ord p => PredOracle p -> p -> Bool
predIsUndef oracle p = predIs oracle p UndefPred
-- | Ask an oracle if a predicate is invalid
predIsInvalid :: Ord p => PredOracle p -> p -> Bool
predIsInvalid oracle p = predIs oracle p InvalidPred
-- | Check the state of a predicate
predIs :: Ord p => PredOracle p -> p -> PredState -> Bool
predIs oracle p s = predState oracle p == s
-- | Get predicate state
predState :: Ord p => PredOracle p -> p -> PredState
predState oracle p = case p `Map.lookup` oracle of
Just s -> s
Nothing -> UndefPred
-- | Create an oracle from a list
makeOracle :: Ord p => [(p,PredState)] -> PredOracle p
makeOracle = Map.fromList
-- | Get a list of valid and defined predicates from an oracle
oraclePredicates :: Ord p => PredOracle p -> [(p,PredState)]
oraclePredicates = filter (\(_,s) -> s /= UndefPred) . Map.toList
-- | Combine two oracles
-- TODO: check that there is no contradiction
oracleUnion :: Ord p => PredOracle p -> PredOracle p -> PredOracle p
oracleUnion = Map.union
-- | Add predicates to an oracle
-- TODO: check that there is no contradiction
predAdd :: Ord p => [(p,PredState)] -> PredOracle p -> PredOracle p
predAdd cs = oracleUnion (makeOracle cs)
-- | Oracle that always answer Undef
emptyOracle :: PredOracle p
emptyOracle = Map.empty
-------------------------------------------------------
-- Constraint
-------------------------------------------------------
-- | A constraint is a boolean expression
--
-- `p` is the predicate type
data Constraint e p
= Predicate p -- ^ Predicate value
| IsValid p -- ^ Is the predicate valid
| Not (Constraint e p) -- ^ Logic not
| And [Constraint e p] -- ^ Logic and
| Or [Constraint e p] -- ^ Logic or
| Xor [Constraint e p] -- ^ Logic xor
| CBool Bool -- ^ Constant
| CErr (Either String e) -- ^ Error
deriving (Show,Eq,Ord)
instance Functor (Constraint e) where
fmap f (Predicate p) = Predicate (f p)
fmap f (IsValid p) = IsValid (f p)
fmap _ (CBool b) = CBool b
fmap f (Not c) = Not (fmap f c)
fmap f (And cs) = And (fmap (fmap f) cs)
fmap f (Or cs) = Or (fmap (fmap f) cs)
fmap f (Xor cs) = Xor (fmap (fmap f) cs)
fmap _ (CErr e) = CErr e
-- | Reduce a constraint
--
-- >>> data P = A | B deriving (Show,Eq,Ord)
-- >>> let c = And [IsValid A, Predicate B]
--
-- >>> let oracle = makeOracle [(A,InvalidPred),(B,SetPred)]
-- >>> constraintSimplify oracle c
-- CBool False
--
-- >>> let oracle = makeOracle [(A,SetPred),(B,SetPred)]
-- >>> constraintSimplify oracle c
-- CBool True
--
-- >>> let oracle = makeOracle [(A,SetPred),(B,UnsetPred)]
-- >>> constraintSimplify oracle c
-- CBool False
constraintSimplify :: (Ord p, Eq p, Eq e) => PredOracle p -> Constraint e p -> Constraint e p
constraintSimplify oracle c = case constraintOptimize c of
CErr e -> CErr e
IsValid p -> case predState oracle p of
UndefPred -> IsValid p
InvalidPred -> CBool False
SetPred -> CBool True
UnsetPred -> CBool True
Predicate p -> case predState oracle p of
UndefPred -> Predicate p
InvalidPred -> CErr (Left "Invalid predicate")
SetPred -> CBool True
UnsetPred -> CBool False
Not c' -> case constraintSimplify oracle c' of
CBool v -> CBool (not v)
CErr e -> CErr e
c'' -> Not c''
And cs -> case fmap (constraintSimplify oracle) cs of
[] -> CErr (Left "Empty And constraint")
cs' | all (constraintIsBool True) cs' -> CBool True
cs' | any (constraintIsBool False) cs' -> CBool False
cs' | all constraintIsError cs' -> CErr (Left "And expression only contains Error constraints")
cs' -> case filter (not . constraintIsBool True) cs' of
[c'] -> c'
cs'' -> And cs''
Or cs -> case filter (not . constraintIsError) <| fmap (constraintSimplify oracle) cs of
[] -> CErr (Left "Empty Or constraint")
cs' | all (constraintIsBool False) cs' -> CBool False
cs' | any (constraintIsBool True) cs' -> CBool True
cs' -> case filter (not . constraintIsBool False) cs' of
[c'] -> c'
cs'' -> Or cs''
Xor cs -> case fmap (constraintSimplify oracle) cs of
cs' | any constraintIsError cs' -> CErr (Left "Xor expression contains Error constraint")
[] -> CErr (Left "Empty Xor constraint")
cs' -> constraintOptimize (Xor cs')
c'@(CBool _) -> c'
-- | Check that a constraint is evaluated to a given boolean value
constraintIsBool :: Bool -> Constraint e p -> Bool
constraintIsBool v (CBool v') = v == v'
constraintIsBool _ _ = False
-- | Check that a constraint is evaluated to an error
constraintIsError :: Constraint e p -> Bool
constraintIsError (CErr _) = True
constraintIsError _ = False
-- | Get predicates used in a constraint
getConstraintPredicates :: Ord p => Constraint e p -> Set p
getConstraintPredicates = \case
CErr _ -> Set.empty
IsValid p -> Set.singleton p
Predicate p -> Set.singleton p
Not c -> getConstraintPredicates c
And cs -> Set.unions $ fmap getConstraintPredicates cs
Or cs -> Set.unions $ fmap getConstraintPredicates cs
Xor cs -> Set.unions $ fmap getConstraintPredicates cs
CBool _ -> Set.empty
-- | Get constraint terminals
getConstraintTerminals :: Constraint e p -> Set Bool
getConstraintTerminals = \case
CErr _ -> Set.empty
IsValid _ -> tf
Predicate _ -> tf
CBool v -> Set.singleton v
Not c -> Set.map not (getConstraintTerminals c)
And cs -> let cs' = fmap getConstraintTerminals cs
in if | null cs -> Set.empty
| any (False `elem`) cs' -> Set.singleton False
| all (== Set.singleton True) cs' -> Set.singleton True
| otherwise -> tf
Or cs -> let cs' = fmap getConstraintTerminals cs
in if | null cs -> Set.empty
| any (True `elem`) cs' -> Set.singleton True
| all (== Set.singleton False) cs' -> Set.singleton False
| otherwise -> tf
Xor cs -> let cs' = fmap (Set.toList . getConstraintTerminals) cs
in if | null cs -> Set.empty
| otherwise -> xo False cs'
where
tf = Set.fromList [True,False]
xo t [] = Set.singleton t
xo False ([True]:xs) = xo True xs
xo True ([True]:_) = Set.singleton False
xo False ([False]:xs) = xo False xs
xo True ([False]:xs) = xo True xs
xo _ ([]:_) = Set.empty
xo _ _ = tf
-- | Optimize/simplify a constraint
constraintOptimize :: Constraint e p -> Constraint e p
constraintOptimize x = case x of
CErr _ -> x
Not (CErr e) -> CErr e
IsValid _ -> x
Predicate _ -> x
CBool _ -> x
Not (IsValid _) -> x
Not (Predicate _) -> x
Not (CBool v) -> CBool (not v)
Not (Not c) -> constraintOptimize c
Not (Or cs) -> constraintOptimize (And (fmap Not cs))
Not (And cs) -> constraintOptimize (Or (fmap Not cs))
Not (Xor cs) -> case constraintOptimize (Xor cs) of
Xor cs' -> Not (Xor cs')
r -> constraintOptimize (Not r)
And [c] -> constraintOptimize c
Or [c] -> constraintOptimize c
Xor [c] -> let c' = constraintOptimize c
in if | constraintIsBool True c' -> CBool True
| constraintIsBool False c' -> CBool False
| otherwise -> c'
And cs -> let cs' = fmap constraintOptimize cs
in if | any (constraintIsBool False) cs' -> CBool False
| all (constraintIsBool True) cs' -> CBool True
| otherwise -> And cs'
Or cs -> let cs' = fmap constraintOptimize cs
in if | any (constraintIsBool True) cs' -> CBool True
| all (constraintIsBool False) cs' -> CBool False
| otherwise -> Or cs'
Xor cs -> let cs' = fmap constraintOptimize cs
countTrue = length (filter (constraintIsBool True) cs')
countFalse = length (filter (constraintIsBool False) cs')
countAll = length cs'
in if | countTrue > 1 -> CBool False
| countTrue == 1 && countTrue + countFalse == countAll -> CBool True
| countAll == countFalse -> CBool False
| otherwise -> Xor cs'
-------------------------------------------------------
-- Rule
-------------------------------------------------------
-- | A rule can produce some "a"s (one or more if it diverges), depending on the
-- constraints.
data Rule e p a
= Terminal a
| OrderedNonTerminal [(Constraint e p, Rule e p a)]
| NonTerminal [(Constraint e p, Rule e p a)]
| Fail e
deriving (Show,Eq,Ord)
instance Functor (Rule e p) where
fmap f (Terminal a) = Terminal (f a)
fmap f (NonTerminal xs) = NonTerminal (fmap (second (fmap f)) xs)
fmap f (OrderedNonTerminal xs) = OrderedNonTerminal (fmap (second (fmap f)) xs)
fmap _ (Fail e) = Fail e
-- | Simplify a rule given an oracle
ruleSimplify ::
( Ord p, Eq e
) => PredOracle p -> Rule e p a -> Rule e p a
ruleSimplify oracle r = case r of
Terminal a -> Terminal a
Fail e -> Fail e
OrderedNonTerminal rs -> OrderedNonTerminal (simplifyNonTerminal rs)
NonTerminal rs -> NonTerminal (concatMap foldNonTerminal (simplifyNonTerminal rs))
where
-- Simplify non-terminal rule constraints. Remove rules whose constraint is False
simplifyNonTerminal xs = xs
-- reduce constraints
|> fmap (first (constraintSimplify oracle))
-- recursively simplify nested rules
|> fmap (second (ruleSimplify oracle))
-- filter non matching rules
|> filter (not . constraintIsBool False . fst)
-- non terminal sub-rules whose constraints are True can be folded into the
-- upper non-terminal rule. We rely on this to perform rule reduction.
foldNonTerminal (c, NonTerminal rs)
| constraintIsBool True c = rs
foldNonTerminal x = [x]
-- | Reduce a rule
ruleReduce :: forall e p a.
( Ord p, Eq e, Eq p, Eq a) => PredOracle p -> Rule e p a -> MatchResult e (Rule e p a) a
ruleReduce oracle r = case ruleSimplify oracle r of
Terminal a -> Match a
Fail e -> MatchFail [e]
NonTerminal [] -> NoMatch
OrderedNonTerminal [] -> NoMatch
OrderedNonTerminal ((c,x):xs)
| constraintIsBool True c -> ruleReduce oracle x
| constraintIsBool False c -> ruleReduce oracle (OrderedNonTerminal xs)
| otherwise -> DontMatch (OrderedNonTerminal ((c,x):xs))
NonTerminal rs ->
let
(matchingRules,mayMatchRules) = partition (constraintIsBool True . fst) rs
matchingResults = nub $ fmap snd $ matchingRules
(failingResults,terminalResults,hasNonTerminalResults) = go [] [] False matchingResults
go fr tr ntr = \case
[] -> (fr,tr,ntr)
(Fail x:xs) -> go (x:fr) tr ntr xs
(Terminal x:xs) -> go fr (x:tr) ntr xs
(NonTerminal _:xs) -> go fr tr True xs
(OrderedNonTerminal _:xs) -> go fr tr True xs
divergence = case terminalResults of
-- results are already "nub"ed.
-- More than 1 results => divergence
(_:_:_) -> True
_ -> False
in
if | not (null failingResults) -> MatchFail failingResults
| divergence -> MatchDiverge (fmap Terminal terminalResults)
| hasNonTerminalResults -> DontMatch (NonTerminal rs)
| otherwise ->
case (terminalResults,mayMatchRules) of
([a], []) -> Match a
_ -> DontMatch (NonTerminal rs)
-- | Get possible resulting terminals
getRuleTerminals :: Ord a => Rule e p a -> Set a
getRuleTerminals (Fail _) = Set.empty
getRuleTerminals (Terminal a) = Set.singleton a
getRuleTerminals (NonTerminal xs) = Set.unions (fmap (getRuleTerminals . snd) xs)
getRuleTerminals (OrderedNonTerminal xs) = Set.unions (fmap (getRuleTerminals . snd) xs)
-- | Get predicates used in a rule
getRulePredicates :: (Eq p,Ord p) => Rule e p a -> Set p
getRulePredicates (Fail _) = Set.empty
getRulePredicates (Terminal _) = Set.empty
getRulePredicates (NonTerminal xs) = Set.unions $ fmap (\(x,y) -> getConstraintPredicates x `Set.union` getRulePredicates y) xs
getRulePredicates (OrderedNonTerminal xs) = Set.unions $ fmap (\(x,y) -> getConstraintPredicates x `Set.union` getRulePredicates y) xs
-- | Constraint checking that a predicated value evaluates to some terminal
evalsTo :: (Ord (Pred a), Eq a, Eq (PredTerm a), Eq (Pred a), Predicated a) => a -> PredTerm a -> Constraint e (Pred a)
evalsTo s a = case createPredicateTable s (const True) of
Left x -> CBool (x == a)
Right xs -> orConstraints <| fmap andPredicates
<| fmap oraclePredicates
<| fmap fst
<| filter ((== a) . snd)
<| xs
where
andPredicates [] = CBool True
andPredicates xs = And (concatMap makePred xs)
orConstraints [] = CBool True
orConstraints [x] = x
orConstraints xs = Or xs
makePred (p, UnsetPred) = [IsValid p, Not (Predicate p)]
makePred (p, SetPred) = [IsValid p, Predicate p]
makePred (p, InvalidPred) = [Not (IsValid p)]
makePred (_, UndefPred) = undefined -- shouldn't be possible given we use
-- get the predicates from the oracle itself
-------------------------------------------------------
-- Predicated data
-------------------------------------------------------
-- | Predicated data
--
-- @
-- data T
-- data NT
--
-- type family RuleT e p a s :: * where
-- RuleT e p a T = a
-- RuleT e p a NT = Rule e p a
--
-- data PD t = PD
-- { p1 :: RuleT () Bool Int t
-- , p2 :: RuleT () Bool String t
-- }
--
-- deriving instance Eq (PD T)
-- deriving instance Show (PD T)
-- deriving instance Ord (PD T)
-- deriving instance Eq (PD NT)
-- deriving instance Show (PD NT)
-- deriving instance Ord (PD NT)
--
--
-- instance Predicated (PD NT) where
-- type PredErr (PD NT) = ()
-- type Pred (PD NT) = Bool
-- type PredTerm (PD NT) = PD T
--
-- liftTerminal (PD a b) = PD (liftTerminal a) (liftTerminal b)
--
-- reducePredicates oracle (PD a b) =
-- initP PD PD
-- |> (`applyP` reducePredicates oracle a)
-- |> (`applyP` reducePredicates oracle b)
-- |> resultP
--
-- getTerminals (PD as bs) = [ PD a b | a <- getTerminals as
-- , b <- getTerminals bs
-- ]
--
-- getPredicates (PD a b) = concat
-- [ getPredicates a
-- , getPredicates b
-- ]
-- @
class (Ord (Pred a), Ord (PredTerm a)) => Predicated a where
-- | Error type
type PredErr a :: *
-- | Predicate type
type Pred a :: *
-- | Terminal type
type PredTerm a :: *
-- | Build a non terminal from a terminal
liftTerminal :: PredTerm a -> a
-- | Reduce predicates
reducePredicates :: PredOracle (Pred a) -> a -> MatchResult (PredErr a) a (PredTerm a)
-- | Simplify predicates
simplifyPredicates :: PredOracle (Pred a) -> a -> a
-- | Get possible resulting terminals
getTerminals :: a -> Set (PredTerm a)
-- | Get used predicates
getPredicates :: a -> Set (Pred a)
instance (Ord a, Ord p, Eq e, Eq a, Eq p) => Predicated (Rule e p a) where
type PredErr (Rule e p a) = e
type Pred (Rule e p a) = p
type PredTerm (Rule e p a) = a
reducePredicates = ruleReduce
simplifyPredicates = ruleSimplify
liftTerminal = Terminal
getTerminals = getRuleTerminals
getPredicates = getRulePredicates
instance (Ord p, Eq e, Eq p) => Predicated (Constraint e p) where
type PredErr (Constraint e p) = e
type Pred (Constraint e p) = p
type PredTerm (Constraint e p) = Bool
reducePredicates oracle c = case constraintSimplify oracle c of
CBool v -> Match v
c' -> DontMatch c'
simplifyPredicates oracle c = constraintSimplify oracle c
liftTerminal = CBool
getTerminals = getConstraintTerminals
getPredicates = getConstraintPredicates
instance forall x y.
( Predicated x
, Predicated y
, PredErr x ~ PredErr y
, Pred x ~ Pred y
) => Predicated (x,y)
where
type PredErr (x,y) = PredErr x
type Pred (x,y) = Pred x
type PredTerm (x,y) = (PredTerm x, PredTerm y)
reducePredicates oracle (x,y) =
initP (,) (,)
|> (`applyP` reducePredicates oracle x)
|> (`applyP` reducePredicates oracle y)
|> resultP
simplifyPredicates oracle (x,y) = (simplifyPredicates oracle x, simplifyPredicates oracle y)
liftTerminal (x,y) = (liftTerminal x, liftTerminal y)
getTerminals (x,y) = Set.fromList
[ (x',y') | x' <- Set.toList (getTerminals x)
, y' <- Set.toList (getTerminals y)
]
getPredicates (x,y) = Set.union (getPredicates x) (getPredicates y)
-- | Reduction result
data MatchResult e nt t
= NoMatch
| Match t
| DontMatch nt
| MatchFail [e]
| MatchDiverge [nt]
deriving (Show,Eq,Ord)
instance Functor (MatchResult e nt) where
fmap f x = case x of
NoMatch -> NoMatch
MatchDiverge xs -> MatchDiverge xs
MatchFail es -> MatchFail es
Match a -> Match (f a)
DontMatch a -> DontMatch a
-- | Compose reduction results
--
-- We reuse the MatchResult data type:
-- * a "terminal" on the left can be used to build either a terminal or a non terminal
-- * a "non terminal" on the left can only be used to build a non terminal
applyP ::
( Predicated ntb
) => MatchResult e (ntb -> nt) (ntb -> nt, PredTerm ntb -> t) -> MatchResult e ntb (PredTerm ntb) -> MatchResult e nt (nt,t)
applyP NoMatch _ = NoMatch
applyP _ NoMatch = NoMatch
applyP (MatchFail xs) (MatchFail ys) = MatchFail (xs++ys)
applyP (MatchFail xs) _ = MatchFail xs
applyP _ (MatchFail ys) = MatchFail ys
applyP (MatchDiverge fs) (MatchDiverge ys) = MatchDiverge [f y | f <- fs, y <- ys]
applyP (MatchDiverge fs) (Match b) = MatchDiverge [f (liftTerminal b) | f <- fs]
applyP (MatchDiverge fs) (DontMatch b) = MatchDiverge [f b | f <- fs]
applyP (DontMatch f) (MatchDiverge ys) = MatchDiverge [f y | y <- ys]
applyP (DontMatch f) (DontMatch b) = DontMatch (f b)
applyP (DontMatch f) (Match b) = DontMatch (f (liftTerminal b))
applyP (Match (fnt,_)) (MatchDiverge ys) = MatchDiverge [fnt y | y <- ys]
applyP (Match (fnt,_)) (DontMatch b) = DontMatch (fnt b)
applyP (Match (fnt,ft)) (Match b) = Match (fnt (liftTerminal b), ft b)
-- | Initialise a reduction result (typically with two functions/constructors)
initP :: nt -> t -> MatchResult e nt (nt,t)
initP nt t = Match (nt,t)
-- | Fixup result (see initP and applyP)
resultP :: MatchResult e nt (nt,t) -> MatchResult e nt t
resultP = fmap snd
-- | Create a table of predicates that return a terminal
createPredicateTable ::
( Ord (Pred a)
, Eq (Pred a)
, Eq a
, Predicated a
, Predicated a
, Pred a ~ Pred a
) => a -> (PredOracle (Pred a) -> Bool) -> Either (PredTerm a) [(PredOracle (Pred a),PredTerm a)]
createPredicateTable s oracleChecker =
-- we first check if the predicated value reduces to a terminal without any
-- additional oracle
case reducePredicates emptyOracle s of
Match x -> Left x
_ -> Right (mapMaybe matching oracles)
where
matching oracle = case reducePredicates oracle s of
Match x -> Just (oracle,x)
_ -> Nothing
oracles = filter oracleChecker (fmap makeOracle predSets)
preds = Set.toList (getPredicates (simplifyPredicates emptyOracle s))
predSets = makeSets preds [[]]
-- make predicate sets (each predicate is either Set, Unset or Undef)
makeSets [] os = os
makeSets (p:ps) os = let ns = [(p,SetPred),(p,UnsetPred),(p,UndefPred)]
in makeSets ps [(n:o) | o <- os, n <- ns]