Documentation

Possibly negated propositions. For example, we would express t1 not equal to t2 like this: Prop { negated = True, prop = Bin Equal t1 t2 }

Constructors

Prop
Fields negated :: !Bool prop :: !p

Instances

SignPP p => PP (Prop p)

data NormProp p Source

A proposition normalized with respect to a particular variable.

Constructors

Ind (Prop PosP)	Independent of variable.
Norm (Prop p)	Depends on variable.

Instances

SignPP p => PP (NormProp p)

data RelOp Source

Basic binary relations.

Constructors

Equal
LessThan
LessThanEqual

Instances

Eq RelOp
SignPP RelOp

data PosP Source

Basic propositions.

Constructors

Bin !RelOp Term Term
Divides !Integer Term
FF

Instances

SignPP PosP

data VarP Source

Propositions specialized to say something about a particular variable.

Constructors

NBin !RelOp Term	x `op` t
NDivides !Integer Term	n \| x + t

Instances

SignPP VarP

data CVarP Source

Propositions specialized for a variable with a coefficient. For example: 4 * x = t CVarP { coeff = 4, pprop = NBin Equal t }

Constructors

CVarP
Fields coeff :: !Integer pprop :: !VarP

Instances

SignPP CVarP

norm :: Name -> Prop PosP -> NormProp CVarP Source

Rewrite a propositions as a predicate about a specific variable.

scale :: Integer -> Prop CVarP -> Prop VarP Source

Eliminate variable coefficients by scaling the properties appropriately.

neg_inf :: Term -> Prop VarP -> Prop PosP Source

Evaluate a proposition for a sufficiently small value of the variable, if possible. Otherwise, substitute the given term.

pos_inf :: Term -> Prop VarP -> Prop PosP Source

Evaluate a proposition for a sufficiently large value of the variable, if possible. Otherwise, substitute the given term.

normal :: Term -> Prop VarP -> Prop PosP Source

Evaluate a proposition with a given term for the variable.

eval_prop :: Prop PosP -> Env -> Bool Source

The meanings of atomic propositions

bin_op :: RelOp -> Integer -> Integer -> Bool Source

subst_prop :: Name -> Integer -> Prop PosP -> Prop PosP Source

Replace a variable with a constant, in a property.

simplify_prop :: Prop PosP -> Prop PosP Source

class SignPP t whereSource

Methods

pp_neg :: Bool -> t -> Doc Source

Instances

SignPP CVarP
SignPP VarP
SignPP PosP
SignPP RelOp

pp_neg_div :: Bool -> Doc Source