| Maintainer | Simon Meier <iridcode@gmail.com> |
|---|---|
| Safe Haskell | None |
Theory.Tools.AbstractInterpretation
Description
Abstract intepretation for partial evaluation of multiset rewriting systems.
- interpretAbstractly :: (Eq s, HasFrees i, Apply i, Show i) => ([Equal LNFact] -> [LNSubstVFresh]) -> s -> (LNFact -> s -> s) -> (s -> [LNFact]) -> [Rule i] -> [(s, [Rule i])]
- data EvaluationStyle
- partialEvaluation :: EvaluationStyle -> [ProtoRuleE] -> WithMaude (Set LNFact, [ProtoRuleE])
Combinator to define abstract interpretations
Arguments
| :: (Eq s, HasFrees i, Apply i, Show i) | |
| => ([Equal LNFact] -> [LNSubstVFresh]) | Unification of equalities over facts. We assume that facts with different tags are never unified. |
| -> s | Initial abstract state. |
| -> (LNFact -> s -> s) | Add a fact to the abstract state |
| -> (s -> [LNFact]) | Facts of a state. |
| -> [Rule i] | Multiset rewriting rules to apply abstractly. |
| -> [(s, [Rule i])] | Sequence of abstract states and refined versions of all given multiset rewriting rules. |
Higher-order combinator to construct abstract interpreters.
Actual interpretations
data EvaluationStyle Source
How to report on performing a partial evaluation.
partialEvaluation :: EvaluationStyle -> [ProtoRuleE] -> WithMaude (Set LNFact, [ProtoRuleE])Source
Concrete partial evaluator activated with flag: --partial-evaluation