- data Prop p = Prop {}
- data NormProp p
- data RelOp
- = Equal
- | LessThan
- | LessThanEqual
- data PosP
- data VarP
- data CVarP = CVarP {}
- norm :: Name -> Prop PosP -> NormProp CVarP
- scale :: Integer -> Prop CVarP -> Prop VarP
- neg_inf :: Term -> Prop VarP -> Prop PosP
- pos_inf :: Term -> Prop VarP -> Prop PosP
- normal :: Term -> Prop VarP -> Prop PosP
- eval_prop :: Prop PosP -> Env -> Bool
- bin_op :: RelOp -> Integer -> Integer -> Bool
- subst_prop :: Name -> Integer -> Prop PosP -> Prop PosP
- simplify_prop :: Prop PosP -> Prop PosP
- class SignPP t where
- pp_neg_div :: Bool -> Doc
Documentation
Possibly negated propositions.
For example, we would express t1 not equal to t2 like this:
Prop { negated = True, prop = Bin Equal t1 t2 }
A proposition normalized with respect to a particular variable.
Propositions specialized to say something about a particular variable.
Propositions specialized for a variable with a coefficient.
For example: 4 * x = t
CVarP { coeff = 4, pprop = NBin Equal t }
norm :: Name -> Prop PosP -> NormProp CVarPSource
Rewrite a propositions as a predicate about a specific variable.
scale :: Integer -> Prop CVarP -> Prop VarPSource
Eliminate variable coefficients by scaling the properties appropriately.
neg_inf :: Term -> Prop VarP -> Prop PosPSource
Evaluate a proposition for a sufficiently small value of the variable, if possible. Otherwise, substitute the given term.
pos_inf :: Term -> Prop VarP -> Prop PosPSource
Evaluate a proposition for a sufficiently large value of the variable, if possible. Otherwise, substitute the given term.
normal :: Term -> Prop VarP -> Prop PosPSource
Evaluate a proposition with a given term for the variable.
subst_prop :: Name -> Integer -> Prop PosP -> Prop PosPSource
Replace a variable with a constant, in a property.
pp_neg_div :: Bool -> DocSource