speculate-0.4.18: discovery of properties about Haskell functions
Copyright(c) 2016-2024 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Speculate.Reason

Description

This module is part of Speculate.

Equational reasoning for Exprs based on term rewriting.

Synopsis

Documentation

data Thy Source #

Constructors

Thy 

Fields

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 #

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)

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 #

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

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

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

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

updateEquationsBy :: ([Equation] -> [Equation]) -> 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 #

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.

reductions1 :: Expr -> Rule -> [Expr] 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 #