diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-19 13:59:02 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-19 13:59:02 -0400 |
commit | f02a19f5e98a0c202165179bf0752b8339da8706 (patch) | |
tree | e11e1830e7b80898db72af4c88bd8a3e9242a4bd /src | |
parent | 9d16ae4ecb6f24ae7eefabd056902b00bf2fe001 (diff) |
Move tactics around in src/Arithmetic/CoreUnfolder.v
Also unfold some cps things
Diffstat (limited to 'src')
-rw-r--r-- | src/Arithmetic/CoreUnfolder.v | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v index 039232684..df005e630 100644 --- a/src/Arithmetic/CoreUnfolder.v +++ b/src/Arithmetic/CoreUnfolder.v @@ -1,4 +1,5 @@ Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Util.IdfunWithAlt. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Util.Tactics.VM. @@ -10,7 +11,9 @@ Ltac make_parameterized_sig t := CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 Decidable.dec Decidable.dec_eq_Z id_tuple_with_alt id_tuple'_with_alt - Z.add_get_carry_full Z.mul_split]; + Z.add_get_carry_full Z.mul_split + Z.add_get_carry_full_cps Z.mul_split_cps + Z.add_get_carry_cps]; repeat autorewrite with pattern_runtime; reflexivity. @@ -29,6 +32,16 @@ Ltac make_parameterized_eq t t_sig := Notation parameterize_eq t t_sig := ltac:(let v := t in let v_sig := t_sig in make_parameterized_eq v v_sig) (only parsing). +Ltac basesystem_partial_evaluation_RHS_fast := + repeat autorewrite with pattern_runtime; + let t := match goal with |- _ _ ?t => t end in + let t := pattern_strip t in + let t1 := fresh "t1" in + pose t as t1; + let t1' := apply_patterned t1 in + transitivity t1'; + [replace_with_vm_compute t1; clear t1|reflexivity]. + Module B. Module Associational. (** @@ -296,13 +309,3 @@ Definition div_sig := parameterize_sig (@Core.div). Definition div := parameterize_from_sig div_sig. Definition div_eq := parameterize_eq div div_sig. Hint Rewrite <- div_eq : pattern_runtime. - -Ltac basesystem_partial_evaluation_RHS_fast := - repeat autorewrite with pattern_runtime; - let t := match goal with |- _ _ ?t => t end in - let t := pattern_strip t in - let t1 := fresh "t1" in - pose t as t1; - let t1' := apply_patterned t1 in - transitivity t1'; - [replace_with_vm_compute t1; clear t1|reflexivity]. |