blob: 7727324429ae7b14db75d8483c40e2ea1af153d8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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.
|
