Portability | GHC only |
---|---|
Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
Safe Haskell | None |
Support for reasoning with and about disjunctions of substitutions.
- newtype SplitId = SplitId {}
- data EqStore = EqStore {}
- emptyEqStore :: EqStore
- eqsSubst :: forall arr. Arrow arr => Lens arr EqStore LNSubst
- eqsConj :: forall arr. Arrow arr => Lens arr EqStore (Conj (SplitId, Set LNSubstVFresh))
- falseEqConstrConj :: Conj (SplitId, Set LNSubstVFresh)
- eqsIsFalse :: EqStore -> Bool
- addEqs :: MonadFresh m => MaudeHandle -> [Equal LNTerm] -> EqStore -> m (EqStore, Maybe SplitId)
- addRuleVariants :: Disj LNSubstVFresh -> EqStore -> (EqStore, SplitId)
- addDisj :: EqStore -> Set LNSubstVFresh -> (EqStore, SplitId)
- performSplit :: EqStore -> SplitId -> Maybe [EqStore]
- dropNameHintsBound :: EqStore -> EqStore
- splits :: EqStore -> [SplitId]
- splitSize :: EqStore -> SplitId -> Maybe Int
- splitExists :: EqStore -> SplitId -> Bool
- simp :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> EqStore -> m EqStore
- simpDisjunction :: MonadFresh m => MaudeHandle -> (LNSubst -> LNSubstVFresh -> Bool) -> Disj LNSubstVFresh -> m (LNSubst, Maybe [LNSubstVFresh])
- prettyEqStore :: HighlightDocument d => EqStore -> d
Equations
Index of disjunction in equation store
EqStore | |
|
emptyEqStore
is the empty equation store.
Equalitiy constraint conjunctions
falseEqConstrConj :: Conj (SplitId, Set LNSubstVFresh)Source
The false conjunction. It is always identified with split number -1.
Queries
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 SplitId
s valid for the given equation store
sorted by the size of the disjunctions.
Simplification
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
prettyEqStore :: HighlightDocument d => EqStore -> dSource
Pretty print an EqStore
.