tamarin-prover-theory- Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone




Support for reasoning with and about disjunctions of substitutions.



newtype SplitId Source

Index of disjunction in equation store




unSplitId :: Integer

emptyEqStore :: EqStoreSource

emptyEqStore is the empty equation store.

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

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

Equalitiy constraint conjunctions

falseEqConstrConj :: Conj (SplitId, Set LNSubstVFresh)Source

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


eqsIsFalse :: EqStore -> BoolSource

True iff the EqStore is contradictory.

Adding equalities

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

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)Source

Add the given rule variants.

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

Add a disjunction to the equation store at the beginning

Case splitting

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

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

splits :: EqStore -> [SplitId]Source

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

splitSize :: EqStore -> SplitId -> Maybe IntSource

Returns the number of cases for a given SplitId.

splitExists :: EqStore -> SplitId -> BoolSource

Returns True if the SplitId is valid.


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

simp eqStore simplifies the equation store.

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

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

Pretty printing