Test.Speculate.Reason

This module is part of Speculate.

Equational reasoning for Exprs based on term rewriting.

Documentation

data Thy

Constructors

Thy

Fields

• rules :: [Rule]
• equations :: [Equation]
• canReduceTo :: Expr -> Expr -> Bool

  should be compatible with compareE

• compareE :: Expr -> Expr -> Ordering

  total order used to "sort" equations

• closureLimit :: Int
• keepE :: Expr -> Bool
• invalid :: [Equation]

  reserved for rules and equations that were later found to be invalid through testing

Instances

Eq Thy

This instance is as efficient as it gets, but, this function will not detect equality when rules and equations are in a different order (or repeated). See |==|.

Defined in Test.Speculate.Reason

Methods

(==) :: Thy -> Thy -> Bool

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

emptyThy :: Thy

normalize :: Thy -> Expr -> Expr

normalizeE :: Thy -> Expr -> Expr

isNormal :: Thy -> Expr -> Bool

isRootNormal :: Thy -> Expr -> Bool

isRootNormalE :: Thy -> Expr -> Bool

complete :: Thy -> Thy

equivalent :: Thy -> Expr -> Expr -> Bool

equivalentInstance :: Thy -> Expr -> Expr -> Bool

insert :: Equation -> Thy -> Thy

showThy :: Thy -> String

Pretty-prints a theory into a string. (cf. printThy)

printThy :: Thy -> IO ()

Prints a Thy (theory) on the console. (cf. showThy)

keepUpToLength :: Int -> Expr -> Bool

keepMaxOf :: [Equation] -> Expr -> Bool

(|==|) :: Thy -> Thy -> Bool infix 4

theorize :: [Equation] -> Thy

theorizeBy :: (Expr -> Expr -> Bool) -> [Equation] -> Thy

finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation]

criticalPairs :: Thy -> [(Expr, Expr)]

normalizedCriticalPairs :: Thy -> [(Expr, Expr)]

append :: Thy -> [Equation] -> Thy

okThy :: Thy -> Bool

canonicalEqn :: Thy -> Equation -> Bool

canonicalRule :: Rule -> Bool

canonicalizeEqn :: Thy -> Equation -> Equation

deduce :: Thy -> Thy

simplify :: Thy -> Thy

delete :: Thy -> Thy

orient :: Thy -> Thy

compose :: Thy -> Thy

collapse :: Thy -> Thy

updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy

updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy

discardRedundantEquations :: Thy -> Thy

finalize :: Thy -> Thy

Finalize a theory by discarding redundant equations. If after finalizing you complete, redundant equations might pop-up again.

initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy

defaultKeep :: Thy -> Thy

doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy

Double-checks a resulting theory moving untrue rules and equations to the invalid list.

As a side-effect of using testing to conjecturing equations, we may get smaller equations that are obviously incorrect when we consider a bigger (harder-to-test) equation that is incorrect.

For example, given an incorrect large equation, it may follow that False=True.

This function can be used to double-check the generated theory. If any equation or rule is discarded, that means the number of tests should probably be increased.

commutativeOperators :: Thy -> [Expr]

reductions1 :: Expr -> Rule -> [Expr]

groundJoinable :: Thy -> Expr -> Expr -> Bool

dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

This is not a simplification order on funny Exprs.

(|>) :: Expr -> Expr -> Bool infix 4