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

Test.Speculate.Engine

Description

This module is part of Speculate.

Main engine to process data.

Synopsis

expansions :: Instances -> Int -> Expr -> [Expr]
expansionsOfType :: Expr -> [String] -> Expr -> [Expr]
expansionsWith :: [Expr] -> Expr -> [Expr]
theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
representativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)]
consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]])
distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]
classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr]
semiTheoryFromThyAndReps :: Instances -> Int -> Int -> Thy -> [Expr] -> Shy
conditionalTheoryFromThyAndReps :: Instances -> Int -> Int -> Int -> Thy -> [Expr] -> Chy
conditionalEquivalences :: ((Expr, Expr, Expr) -> Bool) -> (Expr -> Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy
subConsequence :: Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
psortBy :: (a -> a -> Bool) -> [a] -> [(a, a)]
module Test.Speculate.Expr

Documentation

expansions :: Instances -> Int -> Expr -> [Expr] Source #

List all variable assignments for a given number of variables. It only assign variables to holes (variables with "" as its name).

> expansions preludeInstances 2 '(_ + _ + ord _)
[ (x + x) + ord c :: Int
, (x + x) + ord d :: Int
, (x + y) + ord c :: Int
, (x + y) + ord d :: Int
, (y + x) + ord c :: Int
, (y + x) + ord d :: Int
, (y + y) + ord c :: Int
, (y + y) + ord d :: Int ]

expansionsOfType :: Expr -> [String] -> Expr -> [Expr] Source #

List all variable assignments for a given type and list of variables.

expansionsWith :: [Expr] -> Expr -> [Expr] Source #

theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]]) Source #

representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]] Source #

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

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
    }

theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]]) Source #

Given atomic expressions, compute theory and representative schema expressions. (cf. theoryFromAtoms)

representativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]] Source #

theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy Source #

equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)] Source #

consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]]) Source #

distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr] Source #

classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr] Source #

classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr] Source #

semiTheoryFromThyAndReps :: Instances -> Int -> Int -> Thy -> [Expr] -> Shy Source #

conditionalTheoryFromThyAndReps :: Instances -> Int -> Int -> Int -> Thy -> [Expr] -> Chy Source #

conditionalEquivalences :: ((Expr, Expr, Expr) -> Bool) -> (Expr -> Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy Source #

subConsequence :: Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool Source #

Is the equation a consequence of substitution? > subConsequence (x == y) (x + y) (x + x) == True > subConsequence (x <= y) (x + y) (x + x) == False -- not sub > subConsequence (abs x == abs y) (abs x) (abs y) == True > subConsequence (abs x == 1) (x + abs x) (20) == False (artificial)

psortBy :: (a -> a -> Bool) -> [a] -> [(a, a)] Source #

module Test.Speculate.Expr