diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-05 20:24:08 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-04-11 11:01:29 -0400 |
commit | ad3f1343356b2ac60da964922459105e3329af0e (patch) | |
tree | 2cfe624931ce09ea109840bc14803542847faf28 /src/RewriterFull.v | |
parent | 7b6cc09fa0273b1eed867bd11583f7b46be5b4e2 (diff) |
Automate more of the rewriter, and factor out rule-specific things
Diffstat (limited to 'src/RewriterFull.v')
-rw-r--r-- | src/RewriterFull.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/src/RewriterFull.v b/src/RewriterFull.v new file mode 100644 index 000000000..772732442 --- /dev/null +++ b/src/RewriterFull.v @@ -0,0 +1,49 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZRange. +Require Import Crypto.RewriterRules. +Require Import Crypto.Rewriter. +Local Open Scope Z_scope. + +Import Compilers.RewriteRules.GoalType. +Import Compilers.RewriteRules.Tactic. + +Module Compilers. + Module RewriteRules. + Definition RewriterNBE : RewriterT. + Proof. make_Rewriter true nbe_rewrite_rulesT. Defined. + + Definition RewriterArith (max_const_val : Z) : RewriterT. + Proof. make_Rewriter false (arith_rewrite_rulesT max_const_val). Defined. + + Definition RewriterArithWithCasts : RewriterT. + Proof. make_Rewriter false arith_with_casts_rewrite_rulesT. Defined. + + Definition RewriterStripLiteralCasts : RewriterT. + Proof. make_Rewriter false strip_literal_casts_rewrite_rulesT. Defined. + + Definition RewriterToFancy + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + : RewriterT. + Proof. make_Rewriter false fancy_rewrite_rulesT. Defined. + + Definition RewriterToFancyWithCasts + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + (value_range flag_range : zrange) + : RewriterT. + Proof. make_Rewriter false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined. + + Definition RewriteNBE {t} := Eval hnf in @Rewrite RewriterNBE t. + Definition RewriteArith max_const_val {t} := Eval hnf in @Rewrite (RewriterArith max_const_val) t. + Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite RewriterArithWithCasts t. + Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite RewriterStripLiteralCasts t. + Definition RewriteToFancy invert_low invert_high {t} + := Eval hnf in @Rewrite (RewriterToFancy invert_low invert_high) t. + Definition RewriteToFancyWithCasts invert_low invert_high value_range flag_range {t} + := Eval hnf in @Rewrite (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) t. + End RewriteRules. + + Import Language.Compilers.defaults. + + Definition PartialEvaluate {t} (e : Expr t) : Expr t + := RewriteRules.RewriteNBE e. +End Compilers. |