Copyright | (c) 2016-2017 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | None |
Language | Haskell2010 |
Test.Speculate.Reason
Description
This module is part of Speculate.
Equational reasoning for Expr
s based on term rewriting.
- data Thy = Thy {}
- emptyThy :: Thy
- normalize :: Thy -> Expr -> Expr
- normalizeE :: Thy -> Expr -> Expr
- isNormal :: Thy -> Expr -> Bool
- complete :: Thy -> Thy
- equivalent :: Thy -> Expr -> Expr -> Bool
- equivalentInstance :: Thy -> Expr -> Expr -> Bool
- insert :: Equation -> Thy -> Thy
- showThy :: Thy -> String
- printThy :: Thy -> IO ()
- keepUpToLength :: Int -> Expr -> Bool
- keepMaxOf :: [Equation] -> Expr -> Bool
- (|==|) :: Thy -> Thy -> Bool
- theorize :: [Equation] -> Thy
- theorizeBy :: (Expr -> Expr -> Bool) -> [Equation] -> Thy
- finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation]
- criticalPairs :: Thy -> [(Expr, Expr)]
- normalizedCriticalPairs :: Thy -> [(Expr, Expr)]
- append :: Thy -> [Equation] -> Thy
- difference :: Thy -> Thy -> Thy
- okThy :: Thy -> Bool
- canonicalEqn :: Thy -> Equation -> Bool
- canonicalRule :: Rule -> Bool
- canonicalizeEqn :: Thy -> Equation -> Equation
- deduce :: Thy -> Thy
- simplify :: Thy -> Thy
- delete :: Thy -> Thy
- orient :: Thy -> Thy
- compose :: Thy -> Thy
- collapse :: Thy -> Thy
- updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy
- updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy
- discardRedundantEquations :: Thy -> Thy
- finalize :: Thy -> Thy
- initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy
- defaultKeep :: Thy -> Thy
- reductions1 :: Expr -> Rule -> [Expr]
- dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
- (|>) :: Expr -> Expr -> Bool
Documentation
Constructors
Thy | |
normalizeE :: Thy -> Expr -> Expr #
keepUpToLength :: Int -> Expr -> Bool #
finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation] #
criticalPairs :: Thy -> [(Expr, Expr)] #
normalizedCriticalPairs :: Thy -> [(Expr, Expr)] #
difference :: Thy -> Thy -> Thy #
canonicalEqn :: Thy -> Equation -> Bool #
canonicalRule :: Rule -> Bool #
canonicalizeEqn :: Thy -> Equation -> Equation #
updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy #
updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy #
discardRedundantEquations :: Thy -> Thy #
Finalize a theory by discarding redundant equations. If after finalizing
you complete
, redundant equations might pop-up again.
defaultKeep :: Thy -> Thy #
reductions1 :: Expr -> Rule -> [Expr] #