Predicate state

Predicate oracle

Create an oracle from a list

Get a list of valid and defined predicates from an oracle

Oracle that always answer Undef

Combine two oracles TODO: check that there is no contradiction

Ask an oracle if a predicate is set

Ask an oracle if a predicate is unset

Ask an oracle if a predicate is undefined

Ask an oracle if a predicate is invalid

Check the state of a predicate

Get predicate state

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

A constraint is a boolean expression

p is the predicate type

Optimize/simplify a constraint

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

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

Simplify a rule given an oracle

Constraint checking that a predicated value evaluates to some terminal

Reduction result

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
                              ]

Create a table of predicates that return a terminal

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

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

Fixup result (see initP and applyP)