Test.Speculate.Reason

This module is part of Speculate.

Equational reasoning for Exprs based on term rewriting.

Documentation

data Thy

Constructors

Thy

Fields

• rules :: [Rule]
• equations :: [Equation]
• canReduceTo :: Expr -> Expr -> Bool

  should be compatible with compareE

• compareE :: Expr -> Expr -> Ordering

  total order used to "sort" equations

• closureLimit :: Int
• keepE :: Expr -> Bool

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

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 infix 4

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

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

Finalize a theory by discarding redundant equations. If after finalizing you complete, redundant equations might pop-up again.

initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy

defaultKeep :: Thy -> Thy

reductions1 :: Expr -> Rule -> [Expr]

dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

(|>) :: Expr -> Expr -> Bool infix 4