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 | |
parent | be2789ada63a1a5a6710da1abc73430f9b676399 (diff) |
sed s'/RewriterProofs/RewriterAll/g'
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | README.md | 10 | ||||
-rw-r--r-- | _CoqProject | 4 | ||||
-rw-r--r-- | src/BoundsPipeline.v | 6 | ||||
-rw-r--r-- | src/CompilersTestCases.v | 4 | ||||
-rw-r--r-- | src/Rewriter/Arith.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ArithWithCasts.v | 6 | ||||
-rw-r--r-- | src/Rewriter/NBE.v | 6 | ||||
-rw-r--r-- | src/Rewriter/StripLiteralCasts.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ToFancy.v | 6 | ||||
-rw-r--r-- | src/Rewriter/ToFancyWithCasts.v | 6 | ||||
-rw-r--r-- | src/RewriterAll.v (renamed from src/RewriterProofs.v) | 0 | ||||
-rw-r--r-- | src/RewriterAllTactics.v (renamed from src/RewriterProofsTactics.v) | 0 |
13 files changed, 31 insertions, 31 deletions
@@ -51,7 +51,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/RewriterWf1.vo \ src/RewriterWf2.vo \ src/RewriterRulesGood.vo \ - src/RewriterProofs.vo + src/RewriterAll.vo NOBIGMEM_UNMADE_VOFILES := \ src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo \ @@ -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` diff --git a/_CoqProject b/_CoqProject index 2ca7a4b89..4d4b652ff 100644 --- a/_CoqProject +++ b/_CoqProject @@ -36,8 +36,8 @@ src/MiscCompilerPassesProofs.v src/PreLanguage.v src/Rewriter.v src/RewriterInterpProofs1.v -src/RewriterProofs.v -src/RewriterProofsTactics.v +src/RewriterAll.v +src/RewriterAllTactics.v src/RewriterRules.v src/RewriterRulesProofs.v src/RewriterWf1.v diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index f0c161dc2..6c21d7c64 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -29,7 +29,7 @@ Require Crypto.CStringification. Require Crypto.LanguageWf. Require Crypto.UnderLetsProofs. Require Crypto.MiscCompilerPassesProofs. -Require Crypto.RewriterProofs. +Require Crypto.RewriterAll. Require Crypto.AbstractInterpretationWf. Require Crypto.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. @@ -39,7 +39,7 @@ Import Crypto.LanguageWf Crypto.UnderLetsProofs Crypto.MiscCompilerPassesProofs - Crypto.RewriterProofs + Crypto.RewriterAll Crypto.AbstractInterpretationWf Crypto.AbstractInterpretationProofs Crypto.Language @@ -53,7 +53,7 @@ Import LanguageWf.Compilers UnderLetsProofs.Compilers MiscCompilerPassesProofs.Compilers - RewriterProofs.Compilers + RewriterAll.Compilers AbstractInterpretationWf.Compilers AbstractInterpretationProofs.Compilers Language.Compilers diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v index 2ed149cdd..91fc3af1d 100644 --- a/src/CompilersTestCases.v +++ b/src/CompilersTestCases.v @@ -5,7 +5,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.AbstractInterpretation. -Require Import Crypto.RewriterProofs. +Require Import Crypto.RewriterAll. Require Import Crypto.MiscCompilerPasses. Require Import Crypto.CStringification. Import ListNotations. Local Open Scope Z_scope. @@ -13,7 +13,7 @@ Import ListNotations. Local Open Scope Z_scope. Import Language.Compilers. Import UnderLets.Compilers. Import AbstractInterpretation.Compilers. -Import RewriterProofs.Compilers. +Import RewriterAll.Compilers. Import MiscCompilerPasses.Compilers. Import CStringification.Compilers. Local Coercion Z.of_nat : nat >-> Z. diff --git a/src/Rewriter/Arith.v b/src/Rewriter/Arith.v index cae1526d2..7b368cb16 100644 --- a/src/Rewriter/Arith.v +++ b/src/Rewriter/Arith.v @@ -1,15 +1,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ArithWithCasts.v b/src/Rewriter/ArithWithCasts.v index de17f207e..554457f1d 100644 --- a/src/Rewriter/ArithWithCasts.v +++ b/src/Rewriter/ArithWithCasts.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/NBE.v b/src/Rewriter/NBE.v index 64e38a38d..db0670179 100644 --- a/src/Rewriter/NBE.v +++ b/src/Rewriter/NBE.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/StripLiteralCasts.v b/src/Rewriter/StripLiteralCasts.v index 0f35dfed6..8c6c1799c 100644 --- a/src/Rewriter/StripLiteralCasts.v +++ b/src/Rewriter/StripLiteralCasts.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ToFancy.v b/src/Rewriter/ToFancy.v index da18848ba..da77e4f21 100644 --- a/src/Rewriter/ToFancy.v +++ b/src/Rewriter/ToFancy.v @@ -1,15 +1,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ToFancyWithCasts.v b/src/Rewriter/ToFancyWithCasts.v index 714ea071e..b8e268b1c 100644 --- a/src/Rewriter/ToFancyWithCasts.v +++ b/src/Rewriter/ToFancyWithCasts.v @@ -2,15 +2,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. Require Import Crypto.Util.ZRange. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/RewriterProofs.v b/src/RewriterAll.v index c2a891de1..c2a891de1 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterAll.v diff --git a/src/RewriterProofsTactics.v b/src/RewriterAllTactics.v index 22fd16cbb..22fd16cbb 100644 --- a/src/RewriterProofsTactics.v +++ b/src/RewriterAllTactics.v |