Conjure.Reason

An internal module of Conjure, a library for Conjuring function implementations from tests or partial definitions. (a.k.a.: functional inductive programming)

This module re-exports some functions from Test.Speculate along with a few additional utilities.

Documentation

data Thy

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

rules :: Thy -> [Rule]

equations :: Thy -> [Equation]

invalid :: Thy -> [Equation]

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

canReduceTo :: Thy -> Expr -> Expr -> Bool

should be compatible with compareE

printThy :: Thy -> IO ()

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

closureLimit :: Thy -> Int

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.

normalize :: Thy -> Expr -> Expr

theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy

Computes a theory from atomic expressions. Example:

> theoryFromAtoms 5 (const True) (equal preludeInstances 100)
>   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
Thy { rules = [ (x + y) + z == x + (y + z) ]
    , equations = [ y + x == x + y
                  , y + (x + z) == x + (y + z)
                  , z + (x + y) == x + (y + z)
                  , z + (y + x) == x + (y + z) ]
    , canReduceTo = (|>)
    , closureLimit = 2
    , keepE = keepUpToLength 5
    }

isRootNormalC :: Thy -> Expr -> Bool

isRootNormalE :: Thy -> Expr -> Bool

isCommutative :: Thy -> Expr -> Bool

commutativeOperators :: Thy -> [Expr]