| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.Speculate.Engine
- vassignments :: Expr -> [Expr]
- expansions :: Instances -> Int -> Expr -> [Expr]
- mostGeneral :: Expr -> Expr
- mostSpecific :: Expr -> Expr
- theoryAndRepresentativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> (Thy, [Expr])
- theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy
- equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)]
- consider :: (Expr -> Expr -> Bool) -> Expr -> (Thy, [Expr]) -> (Thy, [Expr])
- distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]
- classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
- semiTheoryFromThyAndReps :: Instances -> Int -> Int -> Thy -> [Expr] -> Shy
- conditionalTheoryFromThyAndReps :: Instances -> (Expr -> Expr -> Ordering) -> Int -> Int -> Int -> Thy -> [Expr] -> Chy
- conditionalEquivalences :: (Expr -> Expr -> Ordering) -> ((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
vassignments :: Expr -> [Expr] Source #
List all relevant variable assignments in an expresssion. In pseudo-Haskell:
vassignments (0 + x) == [0 + x] vassignments (0 + 0) == [0 + 0] vassignments (0 + _) == [0 + x] vassignments (_ + _) == [x + x, x + y] vassignments (_ + (_ + ord _)) == [x + (x + ord c), x + (y + ord c)]
You should not use this on expression with already assinged variables (undefined, but currently defined behavior):
vassignments (ii -+- i_) == [ii -+- ii]
mostGeneral :: Expr -> Expr Source #
List the most general assignment of holes in an expression
mostSpecific :: Expr -> Expr Source #
List the most specific assignment of holes in an expression
theoryAndRepresentativesFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> (Thy, [Expr]) Source #
Given atomic expressions, compute theory and representative schema expressions.
theoryFromAtoms :: Int -> (Expr -> Expr -> Ordering) -> (Expr -> Bool) -> (Expr -> Expr -> Bool) -> [Expr] -> Thy Source #
Computes a theory from atomic expressions. Example:
> theoryFromAtoms 5 compare (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
}conditionalTheoryFromThyAndReps :: Instances -> (Expr -> Expr -> Ordering) -> Int -> Int -> Int -> Thy -> [Expr] -> Chy Source #
conditionalEquivalences :: (Expr -> Expr -> Ordering) -> ((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)
module Test.Speculate.Expr