quickspec-0.9: Equational laws for free

Safe HaskellNone

Test.QuickSpec.Reasoning.NaiveEquationalReasoning

Description

Equational reasoning built on top of congruence closure.

Documentation

data Context Source

Constructors

Context 

Fields

rel :: S
 
universe :: Map TypeRep Universe
 
maxDepth :: Int
 

type Universe = IntMap [Int]Source

type EQ = ReaderT (Map TypeRep Universe, Int) CCSource

initial :: Int -> [Tagged Term] -> ContextSource

createUniverse :: [Term] -> CC UniverseSource

runEQ :: Context -> EQ a -> (a, Context)Source

evalEQ :: Context -> EQ a -> aSource

execEQ :: Context -> EQ a -> ContextSource

liftCC :: CC a -> EQ aSource

(=?=) :: Term -> Term -> EQ BoolSource

unifiable :: Equation -> EQ BoolSource

(=:=) :: Term -> Term -> EQ BoolSource

unify :: Equation -> EQ BoolSource

type Subst = Symbol -> IntSource

substs :: Term -> Map TypeRep Universe -> Int -> [Subst]Source

subst :: Subst -> Term -> CC IntSource

flatten :: Term -> CC IntSource

get :: EQ SSource

put :: S -> EQ ()Source

rep :: Term -> EQ IntSource