Test.Speculate.CondReason

This module is part o Speculate.

Conditional equational reasoning.

Documentation

data Chy

Constructors

Chy

Fields

• cequations :: [(Expr, Expr, Expr)]
• cimplications :: Digraph Expr
• cclasses :: [(Expr, [Expr])]
• unThy :: Thy

emptyChy :: Chy

updateCEquationsBy :: ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]) -> Chy -> Chy

listImplied :: Chy -> Expr -> [Expr]

listImplies :: Chy -> Expr -> [Expr]

listEquivalent :: Chy -> Expr -> [Expr]

reduceRootWith :: Binds -> Expr -> (Expr, Expr) -> Maybe Expr

reductions1With :: Binds -> Expr -> (Expr, Expr) -> [Expr]

creductions1 :: Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]

cnormalize :: Chy -> Expr -> Expr -> Expr

cequivalent :: Chy -> Expr -> Expr -> Expr -> Bool

cIsInstanceOf :: Chy -> (Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Bool

cinsert :: (Expr, Expr, Expr) -> Chy -> Chy

cfilter :: ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy

cdiscard :: ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy

cdelete :: Chy -> Chy

cfinalize :: Chy -> Chy

canonicalizeCEqn :: (Expr -> Expr -> Ordering) -> (Expr, Expr, Expr) -> (Expr, Expr, Expr)

canonicalizeCEqnWith :: (Expr -> Expr -> Ordering) -> Instances -> (Expr, Expr, Expr) -> (Expr, Expr, Expr)

canonicalCEqnBy :: (Expr -> Expr -> Ordering) -> Instances -> (Expr, Expr, Expr) -> Bool

canonicalCEqn :: (Expr -> Expr -> Ordering) -> (Expr, Expr, Expr) -> Bool

finalCondEquations :: ((Expr, Expr, Expr) -> Bool) -> Chy -> [(Expr, Expr, Expr)]