From ad3f1343356b2ac60da964922459105e3329af0e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Apr 2019 20:24:08 -0400 Subject: Automate more of the rewriter, and factor out rule-specific things --- src/RewriterFull.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 src/RewriterFull.v (limited to 'src/RewriterFull.v') 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. -- cgit v1.2.3