Theory.Tools.EquationStore

Support for reasoning with and about disjunctions of substitutions.

Equations

newtype SplitId

Index of disjunction in equation store

Constructors

SplitId

Fields

unSplitId :: Integer

Instances

Enum SplitId

Eq SplitId

Ord SplitId

Show SplitId

Binary SplitId

NFData SplitId

Apply SplitId

HasFrees SplitId

data EqStore

Constructors

EqStore

Fields

_eqsSubst :: LNSubst

_eqsConj :: Conj (SplitId, Set LNSubstVFresh)

_eqsNextSplitId :: SplitId

Instances

Eq EqStore

Ord EqStore

Show EqStore

Binary EqStore

NFData EqStore

HasFrees EqStore

emptyEqStore :: EqStore

emptyEqStore is the empty equation store.

eqsSubst :: forall arr. Arrow arr => Lens arr EqStore LNSubst

eqsConj :: forall arr. Arrow arr => Lens arr EqStore (Conj (SplitId, Set LNSubstVFresh))

Equalitiy constraint conjunctions

falseEqConstrConj :: Conj (SplitId, Set LNSubstVFresh)

The false conjunction. It is always identified with split number -1.

Queries

eqsIsFalse :: EqStore -> Bool

True iff the EqStore is contradictory.

Adding equalities

addEqs :: MonadFresh m => MaudeHandle -> [Equal LNTerm] -> EqStore -> m (EqStore, Maybe SplitId)

Add a list of term equalities to the equation store. Returns the split identifier of the disjunction in resulting equation store.

addRuleVariants :: Disj LNSubstVFresh -> EqStore -> (EqStore, SplitId)

Add the given rule variants.

addDisj :: EqStore -> Set LNSubstVFresh -> (EqStore, SplitId)

Add a disjunction to the equation store at the beginning

Case splitting

performSplit :: EqStore -> SplitId -> Maybe [EqStore]

performSplit eqs i performs a case-split on the first disjunction with the given SplitId.

dropNameHintsBound :: EqStore -> EqStore

splits :: EqStore -> [SplitId]

Returns the list of all SplitIds valid for the given equation store sorted by the size of the disjunctions.

splitSize :: EqStore -> SplitId -> Maybe Int

Returns the number of cases for a given SplitId.

splitExists :: EqStore -> SplitId -> Bool

Returns True if the SplitId is valid.

Simplification

simp :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> EqStore -> m EqStore

simp eqStore simplifies the equation store.

simpDisjunction :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> Disj LNSubstVFresh -> m (LNSubst, Maybe [LNSubstVFresh])

Simplify given disjunction via EqStore simplification. Obtains fresh names for variables from the underlying MonadFresh.

Pretty printing

prettyEqStore :: HighlightDocument d => EqStore -> d

Pretty print an EqStore.