Haskus.Utils.Solver

Simple Constraint solver

Oracle

data PredState

Predicate state

Constructors

SetPred

Set predicate

UnsetPred

Unset predicate

UndefPred

Undefined predicate

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

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

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

getPredicates :: Constraint e p -> [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

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)

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

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)

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

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)

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

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)

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

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)

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

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)