code-conjure-0.5.12: synthesize Haskell functions out of partial definitions
Copyright(c) 2021-2024 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Conjure.Reason

Description

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.

Synopsis

Documentation

data Thy #

Instances

Instances details
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 |==|.

Instance details

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)

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.

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
    }