quickspec-0.9.6: Equational laws for free!

Safe Haskell	None

Test.QuickSpec.Reasoning.PartialEquationalReasoning

Description

Equational reasoning that deals with partial functions. Only used in HipSpec at the moment.

Documentation

data PEquation Source

Constructors

Precondition :\/: Equation

Instances

Eq PEquation
Ord PEquation
Show PEquation

type Precondition = [Symbol]Source

data Totality Source

Constructors

Partial
Total [Int]
Variable

Instances

Eq Totality
Ord Totality
Show Totality

showPEquation :: Sig -> PEquation -> String Source

data Context Source

Constructors

Context
Fields total :: Context partial :: IntMap Context vars :: IntMap Symbol

type PEQ = State Context Source

initial :: Int -> [(Symbol, Totality)] -> [Tagged Term] -> Context Source

runPEQ :: Context -> PEQ a -> (a, Context)Source

evalPEQ :: Context -> PEQ a -> aSource

execPEQ :: Context -> PEQ a -> Context Source

liftEQ :: [Int] -> (Maybe Int -> EQ a) -> PEQ [a]Source

equal :: PEquation -> PEQ Bool Source

irrelevant :: Equation -> PEQ Precondition Source

unify :: PEquation -> PEQ Bool Source

precondition :: Equation -> PEQ Precondition Source

get :: PEQ Context Source

put :: Context -> PEQ ()Source

rep :: Precondition -> Term -> PEQ [Int]Source