Copyright	(c) 2016-2024 Rudy Matela
License	3-Clause BSD (see the file LICENSE)
Maintainer	Rudy Matela <rudy@matela.com.br>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Speculate.Reason

Description

This module is part of Speculate.

Equational reasoning for Exprs based on term rewriting.

Synopsis

data Thy = Thy {
- rules :: [Rule]
- equations :: [Equation]
- canReduceTo :: Expr -> Expr -> Bool
- compareE :: Expr -> Expr -> Ordering
- closureLimit :: Int
- keepE :: Expr -> Bool
- invalid :: [Equation]
}
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
printThy :: Thy -> IO ()
keepUpToLength :: Int -> Expr -> Bool
keepMaxOf :: [Equation] -> Expr -> Bool
(|==|) :: Thy -> Thy -> Bool
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
initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy
defaultKeep :: Thy -> Thy
doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy
commutativeOperators :: Thy -> [Expr]
reductions1 :: Rule -> Expr -> [Expr]
groundJoinable :: Thy -> Expr -> Expr -> Bool
dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
(|>) :: Expr -> Expr -> Bool

Documentation

data Thy Source #

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

Instances details

Eq Thy Source #	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 `\|==\|`.
Instance details Defined in Test.Speculate.Reason Methods (==) :: Thy -> Thy -> Bool # (/=) :: Thy -> Thy -> Bool #

emptyThy :: Thy Source #

normalize :: Thy -> Expr -> Expr Source #

normalizeE :: Thy -> Expr -> Expr Source #

isNormal :: Thy -> Expr -> Bool Source #

isRootNormal :: Thy -> Expr -> Bool Source #

isRootNormalE :: Thy -> Expr -> Bool Source #

complete :: Thy -> Thy Source #

equivalent :: Thy -> Expr -> Expr -> Bool Source #

equivalentInstance :: Thy -> Expr -> Expr -> Bool Source #

insert :: Equation -> Thy -> Thy Source #

showThy :: Thy -> String Source #

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

printThy :: Thy -> IO () Source #

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

keepUpToLength :: Int -> Expr -> Bool Source #

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

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

theorize :: [Equation] -> Thy Source #

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

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

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

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

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

okThy :: Thy -> Bool Source #

canonicalEqn :: Thy -> Equation -> Bool Source #

canonicalRule :: Rule -> Bool Source #

canonicalizeEqn :: Thy -> Equation -> Equation Source #

deduce :: Thy -> Thy Source #

simplify :: Thy -> Thy Source #

delete :: Thy -> Thy Source #

orient :: Thy -> Thy Source #

compose :: Thy -> Thy Source #

collapse :: Thy -> Thy Source #

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

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

discardRedundantEquations :: Thy -> Thy Source #

finalize :: Thy -> Thy Source #

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

defaultKeep :: Thy -> Thy Source #

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

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] Source #

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

groundJoinable :: Thy -> Expr -> Expr -> Bool Source #

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

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