Maintainer | Simon Meier <iridcode@gmail.com> |
---|---|

Safe Haskell | None |

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

:: (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

partialEvaluation :: EvaluationStyle -> [ProtoRuleE] -> WithMaude (Set LNFact, [ProtoRuleE])Source

Concrete partial evaluator activated with flag: --partial-evaluation