diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-04-10 16:41:34 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-04-11 11:01:29 -0400 |
| commit | 60520cd8d08f63337225c0a2938827e00a2c48a3 (patch) | |
| tree | aaf3a2a7b75aabc1dee784c49da868907f4a1b54 /README.md | |
| parent | be2789ada63a1a5a6710da1abc73430f9b676399 (diff) | |
sed s'/RewriterProofs/RewriterAll/g'
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -204,7 +204,7 @@ Rewriter.v ←────────────────────── ↗ ↖ RewriterWf2.v RewriterInterpProofs1.v ↖ ↗ -RewriterRules.v RewriterProofsTactics.v +RewriterRules.v RewriterAllTactics.v ↑ ↑ RewriterRulesProofs.v │ ↑ │ @@ -218,7 +218,7 @@ RewriterRulesProofs.v │ ↑ ↑ │ └───────┬──────────────────┴───────────────────────────────────────────────────────┘ │ - RewriterProofs.v + RewriterAll.v ``` - RewriterRules.v: Defines the list of types of the rewrite rules that @@ -265,7 +265,7 @@ RewriterRulesProofs.v │ rewriter, taking in interp-goodness of rewrite rules as a hypothesis. -- RewriterProofsTactics.v: Defines the tactic +- RewriterAllTactics.v: Defines the tactic `RewriteRules.Tactic.make_rewriter` (and a similar tactic notation) which build the entire `VerifiedRewriter`. They take in the `include_interp` as in Rewriter.v tactics, as well as an hlist of @@ -274,12 +274,12 @@ RewriterRulesProofs.v │ rewriter from a list of rewrite rules. - Rewriter/{NBE, Arith, ArithWithCasts, StripLiteralCasts, ToFancy, - ToFancyWithCasts}.v: Use the tactic from RewriterProofsTactics.v + ToFancyWithCasts}.v: Use the tactic from RewriterAllTactics.v together with the proven list of rewrite rules from RewriterRulesProofs.v to reify and reduce the corresponding pass and generate a rewriter. -- RewriterProofs.v: `Definition`less file that `Export`s the rewriters +- RewriterAll.v: `Definition`less file that `Export`s the rewriters defined in `Rewriter/*.v` |