Haskus.Utils.Solver

Simple Constraint solver

Oracle

data PredState

Predicate state

Constructors

SetPred

Set predicate

UnsetPred

Unset predicate

UndefPred

Undefined predicate

InvalidPred

Invalid predicate (can't be used)

Instances

Eq PredState

Defined in Haskus.Utils.Solver

Methods

(==) :: PredState -> PredState -> Bool

(/=) :: PredState -> PredState -> Bool

Ord PredState

Defined in Haskus.Utils.Solver

Methods

compare :: PredState -> PredState -> Ordering

(<) :: PredState -> PredState -> Bool

(<=) :: PredState -> PredState -> Bool

(>) :: PredState -> PredState -> Bool

(>=) :: PredState -> PredState -> Bool

max :: PredState -> PredState -> PredState

min :: PredState -> PredState -> PredState

Show PredState

Defined in Haskus.Utils.Solver

Methods

showsPrec :: Int -> PredState -> ShowS

show :: PredState -> String

showList :: [PredState] -> ShowS

type PredOracle p = Map p PredState

Predicate oracle

makeOracle :: Ord p => [(p, PredState)] -> PredOracle p

Create an oracle from a list

oraclePredicates :: Ord p => PredOracle p -> [(p, PredState)]

Get a list of valid and defined predicates from an oracle

emptyOracle :: PredOracle p

Oracle that always answer Undef

oracleUnion :: Ord p => PredOracle p -> PredOracle p -> PredOracle p

Combine two oracles TODO: check that there is no contradiction

predIsSet :: Ord p => PredOracle p -> p -> Bool

Ask an oracle if a predicate is set

predIsUnset :: Ord p => PredOracle p -> p -> Bool

Ask an oracle if a predicate is unset

predIsUndef :: Ord p => PredOracle p -> p -> Bool

Ask an oracle if a predicate is undefined

predIsInvalid :: Ord p => PredOracle p -> p -> Bool

Ask an oracle if a predicate is invalid

predIs :: Ord p => PredOracle p -> p -> PredState -> Bool

Check the state of a predicate

predState :: Ord p => PredOracle p -> p -> PredState

Get predicate state

predAdd :: Ord p => [(p, PredState)] -> PredOracle p -> PredOracle p

Add predicates to an oracle TODO: check that there is no contradiction

Constraint

data Constraint e p

A constraint is a boolean expression

p is the predicate type

Constructors

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

Instances

Functor (Constraint e)

Defined in Haskus.Utils.Solver

Methods

fmap :: (a -> b) -> Constraint e a -> Constraint e b

(<$) :: a -> Constraint e b -> Constraint e a

(Eq p, Eq e) => Eq (Constraint e p)

Defined in Haskus.Utils.Solver

Methods

(==) :: Constraint e p -> Constraint e p -> Bool

(/=) :: Constraint e p -> Constraint e p -> Bool

(Ord p, Ord e) => Ord (Constraint e p)

Defined in Haskus.Utils.Solver

Methods

compare :: Constraint e p -> Constraint e p -> Ordering

(<) :: Constraint e p -> Constraint e p -> Bool

(<=) :: Constraint e p -> Constraint e p -> Bool

(>) :: Constraint e p -> Constraint e p -> Bool

(>=) :: Constraint e p -> Constraint e p -> Bool

max :: Constraint e p -> Constraint e p -> Constraint e p

min :: Constraint e p -> Constraint e p -> Constraint e p

(Show p, Show e) => Show (Constraint e p)

Defined in Haskus.Utils.Solver

Methods

showsPrec :: Int -> Constraint e p -> ShowS

show :: Constraint e p -> String

showList :: [Constraint e p] -> ShowS

(Ord p, Eq e, Eq p) => Predicated (Constraint e p)

Defined in Haskus.Utils.Solver

Associated Types

type PredErr (Constraint e p) :: Type

type Pred (Constraint e p) :: Type

type PredTerm (Constraint e p) :: Type

Methods

liftTerminal :: PredTerm (Constraint e p) -> Constraint e p

reducePredicates :: PredOracle (Pred (Constraint e p)) -> Constraint e p -> MatchResult (PredErr (Constraint e p)) (Constraint e p) (PredTerm (Constraint e p))

simplifyPredicates :: PredOracle (Pred (Constraint e p)) -> Constraint e p -> Constraint e p

getTerminals :: Constraint e p -> Set (PredTerm (Constraint e p))

getPredicates :: Constraint e p -> Set (Pred (Constraint e p))

type PredErr (Constraint e p)

Defined in Haskus.Utils.Solver

type PredErr (Constraint e p) = e

type Pred (Constraint e p)

Defined in Haskus.Utils.Solver

type Pred (Constraint e p) = p

type PredTerm (Constraint e p)

Defined in Haskus.Utils.Solver

type PredTerm (Constraint e p) = Bool

constraintOptimize :: Constraint e p -> Constraint e p

Optimize/simplify a constraint

constraintSimplify :: (Ord p, Eq p, Eq e) => PredOracle p -> Constraint e p -> Constraint e p

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

Rule

data Rule e p a

A rule can produce some "a"s (one or more if it diverges), depending on the constraints.

Constructors

Terminal a

OrderedNonTerminal [(Constraint e p, Rule e p a)]

NonTerminal [(Constraint e p, Rule e p a)]

Fail e

Instances

Functor (Rule e p)

Defined in Haskus.Utils.Solver

Methods

fmap :: (a -> b) -> Rule e p a -> Rule e p b

(<$) :: a -> Rule e p b -> Rule e p a

(Eq a, Eq p, Eq e) => Eq (Rule e p a)

Defined in Haskus.Utils.Solver

Methods

(==) :: Rule e p a -> Rule e p a -> Bool

(/=) :: Rule e p a -> Rule e p a -> Bool

(Ord a, Ord p, Ord e) => Ord (Rule e p a)

Defined in Haskus.Utils.Solver

Methods

compare :: Rule e p a -> Rule e p a -> Ordering

(<) :: Rule e p a -> Rule e p a -> Bool

(<=) :: Rule e p a -> Rule e p a -> Bool

(>) :: Rule e p a -> Rule e p a -> Bool

(>=) :: Rule e p a -> Rule e p a -> Bool

max :: Rule e p a -> Rule e p a -> Rule e p a

min :: Rule e p a -> Rule e p a -> Rule e p a

(Show a, Show p, Show e) => Show (Rule e p a)

Defined in Haskus.Utils.Solver

Methods

showsPrec :: Int -> Rule e p a -> ShowS

show :: Rule e p a -> String

showList :: [Rule e p a] -> ShowS

(Ord a, Ord p, Eq e, Eq a, Eq p) => Predicated (Rule e p a)

Defined in Haskus.Utils.Solver

Associated Types

type PredErr (Rule e p a) :: Type

type Pred (Rule e p a) :: Type

type PredTerm (Rule e p a) :: Type

Methods

liftTerminal :: PredTerm (Rule e p a) -> Rule e p a

reducePredicates :: PredOracle (Pred (Rule e p a)) -> Rule e p a -> MatchResult (PredErr (Rule e p a)) (Rule e p a) (PredTerm (Rule e p a))

simplifyPredicates :: PredOracle (Pred (Rule e p a)) -> Rule e p a -> Rule e p a

getTerminals :: Rule e p a -> Set (PredTerm (Rule e p a))

getPredicates :: Rule e p a -> Set (Pred (Rule e p a))

type PredErr (Rule e p a)

Defined in Haskus.Utils.Solver

type PredErr (Rule e p a) = e

type Pred (Rule e p a)

Defined in Haskus.Utils.Solver

type Pred (Rule e p a) = p

type PredTerm (Rule e p a)

Defined in Haskus.Utils.Solver

type PredTerm (Rule e p a) = a

ruleSimplify :: (Ord p, Eq e) => PredOracle p -> Rule e p a -> Rule e p a

Simplify a rule given an oracle

evalsTo :: (Ord (Pred a), Eq a, Eq (PredTerm a), Eq (Pred a), Predicated a) => a -> PredTerm a -> Constraint e (Pred a)

Constraint checking that a predicated value evaluates to some terminal

data MatchResult e nt t

Reduction result

Constructors

NoMatch

Match t

DontMatch nt

MatchFail [e]

MatchDiverge [nt]

Instances

Functor (MatchResult e nt)

Defined in Haskus.Utils.Solver

Methods

fmap :: (a -> b) -> MatchResult e nt a -> MatchResult e nt b

(<$) :: a -> MatchResult e nt b -> MatchResult e nt a

(Eq t, Eq nt, Eq e) => Eq (MatchResult e nt t)

Defined in Haskus.Utils.Solver

Methods

(==) :: MatchResult e nt t -> MatchResult e nt t -> Bool

(/=) :: MatchResult e nt t -> MatchResult e nt t -> Bool

(Ord t, Ord nt, Ord e) => Ord (MatchResult e nt t)

Defined in Haskus.Utils.Solver

Methods

compare :: MatchResult e nt t -> MatchResult e nt t -> Ordering

(<) :: MatchResult e nt t -> MatchResult e nt t -> Bool

(<=) :: MatchResult e nt t -> MatchResult e nt t -> Bool

(>) :: MatchResult e nt t -> MatchResult e nt t -> Bool

(>=) :: MatchResult e nt t -> MatchResult e nt t -> Bool

max :: MatchResult e nt t -> MatchResult e nt t -> MatchResult e nt t

min :: MatchResult e nt t -> MatchResult e nt t -> MatchResult e nt t

(Show t, Show nt, Show e) => Show (MatchResult e nt t)

Defined in Haskus.Utils.Solver

Methods

showsPrec :: Int -> MatchResult e nt t -> ShowS

show :: MatchResult e nt t -> String

showList :: [MatchResult e nt t] -> ShowS

Predicated data

class (Ord (Pred a), Ord (PredTerm a)) => Predicated a where

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
                              ]

Associated Types

type PredErr a :: *

Error type

type Pred a :: *

Predicate type

type PredTerm a :: *

Terminal type

Methods

liftTerminal :: PredTerm a -> a

Build a non terminal from a terminal

reducePredicates :: PredOracle (Pred a) -> a -> MatchResult (PredErr a) a (PredTerm a)

Reduce predicates

simplifyPredicates :: PredOracle (Pred a) -> a -> a

Simplify predicates

getTerminals :: a -> Set (PredTerm a)

Get possible resulting terminals

getPredicates :: a -> Set (Pred a)

Get used predicates

Instances

(Predicated x, Predicated y, PredErr x ~ PredErr y, Pred x ~ Pred y) => Predicated (x, y)

Defined in Haskus.Utils.Solver

Associated Types

type PredErr (x, y) :: Type

type Pred (x, y) :: Type

type PredTerm (x, y) :: Type

Methods

liftTerminal :: PredTerm (x, y) -> (x, y)

reducePredicates :: PredOracle (Pred (x, y)) -> (x, y) -> MatchResult (PredErr (x, y)) (x, y) (PredTerm (x, y))

simplifyPredicates :: PredOracle (Pred (x, y)) -> (x, y) -> (x, y)

getTerminals :: (x, y) -> Set (PredTerm (x, y))

getPredicates :: (x, y) -> Set (Pred (x, y))

(Ord p, Eq e, Eq p) => Predicated (Constraint e p)

Defined in Haskus.Utils.Solver

Associated Types

type PredErr (Constraint e p) :: Type

type Pred (Constraint e p) :: Type

type PredTerm (Constraint e p) :: Type

Methods

liftTerminal :: PredTerm (Constraint e p) -> Constraint e p

reducePredicates :: PredOracle (Pred (Constraint e p)) -> Constraint e p -> MatchResult (PredErr (Constraint e p)) (Constraint e p) (PredTerm (Constraint e p))

simplifyPredicates :: PredOracle (Pred (Constraint e p)) -> Constraint e p -> Constraint e p

getTerminals :: Constraint e p -> Set (PredTerm (Constraint e p))

getPredicates :: Constraint e p -> Set (Pred (Constraint e p))

(Ord a, Ord p, Eq e, Eq a, Eq p) => Predicated (Rule e p a)

Defined in Haskus.Utils.Solver

Associated Types

type PredErr (Rule e p a) :: Type

type Pred (Rule e p a) :: Type

type PredTerm (Rule e p a) :: Type

Methods

liftTerminal :: PredTerm (Rule e p a) -> Rule e p a

reducePredicates :: PredOracle (Pred (Rule e p a)) -> Rule e p a -> MatchResult (PredErr (Rule e p a)) (Rule e p a) (PredTerm (Rule e p a))

simplifyPredicates :: PredOracle (Pred (Rule e p a)) -> Rule e p a -> Rule e p a

getTerminals :: Rule e p a -> Set (PredTerm (Rule e p a))

getPredicates :: Rule e p a -> Set (Pred (Rule e p a))

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)]

Create a table of predicates that return a terminal

initP :: nt -> t -> MatchResult e nt (nt, t)

Initialise a reduction result (typically with two functions/constructors)

applyP :: Predicated ntb => MatchResult e (ntb -> nt) (ntb -> nt, PredTerm ntb -> t) -> MatchResult e ntb (PredTerm ntb) -> MatchResult e nt (nt, t)

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

resultP :: MatchResult e nt (nt, t) -> MatchResult e nt t

Fixup result (see initP and applyP)