Test.Speculate.SemiReason

This module is part o Speculate.

Inequational (or semi-equational) reasoning.

Documentation

type Equation = (Expr, Expr)

data Shy

Constructors

Shy

Fields

• sequations :: [Equation]
• sthy :: Thy

emptyShy :: Shy

updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy

mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy

scompareE :: Shy -> Expr -> Expr -> Ordering

lesser :: Shy -> Expr -> [Expr]

greater :: Shy -> Expr -> [Expr]

simplerThan :: Equation -> Shy -> Shy

given a semi-equation (inequality), simplerThan restricts the Shy (SemiTheory) into only equations simpler than the given semi-equation or that are instances of simpler equations.

half-baked example:

x + 1 is simpler than x + y and it is returned. (1 + 1) + 1 is more complex than x + y but it is returned as well as it is an instance of x + 1.

transConsequence :: Shy -> Equation -> Bool

updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy

stheorize :: Thy -> [Equation] -> Shy

sides :: Shy -> [Expr]

finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]

canonicalizeShyWith :: Instances -> Shy -> Shy

canonicalizeSemiEquationWith :: Instances -> Equation -> Equation