Haskus.Utils.Solver

Simple Constraint solver

Oracle

data PredState

Predicate state

Constructors

SetPred

Set predicate

UnsetPred

Unset predicate

UndefPred

Undefined predicate

Instances

Eq PredState

Methods

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

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

Ord PredState

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

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 predicates from an oracle

emptyOracle :: PredOracle p

Oracle that always answer Undef

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

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

Check the state of a predicate

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

Get predicate state

Constraint

data Constraint e p

Constructors

Predicate p

Not (Constraint e p)

And [Constraint e p]

Or [Constraint e p]

Xor [Constraint e p]

CBool Bool

Instances

Functor (Constraint e)

Methods

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

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

Eq p => Eq (Constraint e p)

Methods

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

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

Ord p => Ord (Constraint e p)

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 (Constraint e p)

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)

Associated Types

type PredErr (Constraint e p) :: *

type Pred (Constraint e p) :: *

type PredTerm (Constraint e p) :: *

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

getTerminals :: Constraint e p -> [PredTerm (Constraint e p)]

getPredicates :: Constraint e p -> [Pred (Constraint e p)]

type PredErr (Constraint e p)

type PredErr (Constraint e p) = e

type Pred (Constraint e p)

type Pred (Constraint e p) = p

type PredTerm (Constraint e p)

type PredTerm (Constraint e p) = Bool

simplifyConstraint :: Constraint e p -> Constraint e p

Simplify a constraint

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

Reduce a constraint

Rule

data Rule e p a

Constructors

Terminal a

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

Fail e

Instances

Functor (Rule e p)

Methods

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

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

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

Methods

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

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

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

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 e, Show p, Show a) => Show (Rule e p a)

Methods

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

show :: Rule e p a -> String

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

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

Associated Types

type PredErr (Rule e p a) :: *

type Pred (Rule e p a) :: *

type PredTerm (Rule e p a) :: *

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

getTerminals :: Rule e p a -> [PredTerm (Rule e p a)]

getPredicates :: Rule e p a -> [Pred (Rule e p a)]

type PredErr (Rule e p a)

type PredErr (Rule e p a) = e

type Pred (Rule e p a)

type Pred (Rule e p a) = p

type PredTerm (Rule e p a)

type PredTerm (Rule e p a) = a

orderedNonTerminal :: [(Constraint e p, Rule e p a)] -> Rule e p a

NonTerminal whose constraints are evaluated in order

Earlier constraints must be proven false for the next ones to be considered

mergeRules :: Rule e p a -> Rule e p b -> Rule e p (a, b)

Merge two rules together

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)

Methods

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

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

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

Methods

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

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

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

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 e, Show nt, Show t) => Show (MatchResult e nt t)

Methods

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

show :: MatchResult e nt t -> String

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

Predicated data

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

Minimal complete definition

liftTerminal, reducePredicates, getTerminals, getPredicates

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

getTerminals :: a -> [PredTerm a]

Get possible resulting terminals

getPredicates :: a -> [Pred a]

Get used predicates

Instances

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

Associated Types

type PredErr (Constraint e p) :: *

type Pred (Constraint e p) :: *

type PredTerm (Constraint e p) :: *

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

getTerminals :: Constraint e p -> [PredTerm (Constraint e p)]

getPredicates :: Constraint e p -> [Pred (Constraint e p)]

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

Associated Types

type PredErr (Rule e p a) :: *

type Pred (Rule e p a) :: *

type PredTerm (Rule e p a) :: *

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

getTerminals :: Rule e p a -> [PredTerm (Rule e p a)]

getPredicates :: Rule e p a -> [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) -> 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)