diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-02 11:33:25 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-02 11:33:25 -0400 |
commit | 9458d877c381366b36275a2aa695c07fad0775bd (patch) | |
tree | 69ef551ff09bf7112057728a15616c30424a78c5 /src | |
parent | 63da3166914ea3c7de954f1015fea3df305bf5b6 (diff) |
Speed up reification a little bit
This helps a lot more in C32 ladderstep; we eliminate useless typeclass
unification against hypotheses by separating out the typeclass used for
external overloading and posing hypotheses, and the typeclass used for
recursion under binders.
After | File Name | Before || Change
---------------------------------------------------------------------------------------
12m49.58s | Total | 13m04.75s || -0m15.16s
---------------------------------------------------------------------------------------
2m48.67s | Specific/X25519/C64/ladderstep | 2m58.05s || -0m09.37s
2m21.65s | Specific/NISTP256/AMD64/femul | 2m16.64s || +0m05.01s
1m25.60s | Specific/IntegrationTestKaratsubaMul | 1m30.00s || -0m04.40s
1m08.01s | Specific/X25519/C32/femul | 1m12.17s || -0m04.15s
1m08.25s | Specific/IntegrationTestLadderstep130 | 1m11.61s || -0m03.35s
0m39.67s | Specific/X25519/C32/fesquare | 0m39.16s || +0m00.51s
0m27.09s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.02s || +0m00.07s
0m17.74s | Specific/NISTP256/AMD64/fesub | 0m18.34s || -0m00.60s
0m17.21s | Specific/IntegrationTestFreeze | 0m16.37s || +0m00.83s
0m15.89s | Specific/NISTP256/AMD64/feadd | 0m15.31s || +0m00.58s
0m14.78s | Specific/NISTP256/AMD64/feopp | 0m14.73s || +0m00.04s
0m14.47s | Specific/X25519/C64/femul | 0m14.39s || +0m00.08s
0m12.07s | Specific/IntegrationTestSub | 0m11.76s || +0m00.31s
0m12.07s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.93s || +0m00.14s
0m11.79s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.21s
0m10.84s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.90s || -0m00.06s
0m10.08s | Specific/X25519/C64/fesquare | 0m10.61s || -0m00.52s
0m09.66s | Specific/NISTP256/AMD64/fenz | 0m09.68s || -0m00.01s
0m09.27s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.28s || -0m00.00s
0m03.51s | Compilers/TestCase | 0m03.49s || +0m00.01s
0m03.08s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.23s || -0m00.14s
0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m03.00s || -0m00.00s
0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.15s || +0m00.01s
0m00.86s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.84s || +0m00.02s
0m00.68s | Compilers/Z/Bounds/Pipeline | 0m00.61s || +0m00.07s
0m00.56s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || +0m00.02s
0m00.54s | Compilers/Z/Reify | 0m00.54s || +0m00.00s
0m00.40s | Compilers/Reify | 0m00.41s || -0m00.00s
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Reify.v | 49 |
1 files changed, 41 insertions, 8 deletions
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index b986722f8..4943eca86 100644 --- a/src/Compilers/Reify.v +++ b/src/Compilers/Reify.v @@ -64,6 +64,7 @@ Tactic Notation "debug_reifyf_case" string(case) := debug3 ltac:(fun _ => idtac "reifyf:" case). Ltac debug_enter_reify_abs e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reify_abs:" e). +Class reify_internal {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_internal : T. Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. Arguments reify_var_for_in_is _ {T} _ _ {eT} _. @@ -172,7 +173,13 @@ Ltac reifyf base_type_code interp_base_type op var e := let reify_pretag := constr:(@exprf base_type_code interp_base_type op) in let reify_tag := constr:(reify_pretag var) in let dummy := debug_enter_reifyf e in - match constr:(Set) with + match goal with + | [ re := ?rev : reify reify_tag e |- _ ] => + (* fast path *) + let dummy := debug_reifyf_case "hyp" in + let ret := rev in + let dummy := debug_leave_reifyf_success e ret in + ret | _ => let ret := lazymatch e with @@ -202,7 +209,7 @@ Ltac reifyf base_type_code interp_base_type op var e := let not_x := fresh x in let C' := match constr:(Set) with | _ => constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => - (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) + (_ : reify_internal reify_tag C)) (* [C] here is an open term that references "x" by name *) | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to reify by typeclasses:" e) end in match constr:(Set) with @@ -313,11 +320,24 @@ Ltac reifyf base_type_code interp_base_type op var e := | _ => debug_leave_reifyf_failure e end. +Ltac do_reifyf_goal _ := + debug_enter_reify_rec; + let e := lazymatch goal with + | [ |- reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ] + => reifyf base_type_code interp_base_type op var e + | [ |- reify_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ] + => reifyf base_type_code interp_base_type op var e + end in + debug_leave_reify_rec e; + eexact e. + Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) - : typeclass_instances. +=> do_reifyf_goal () : typeclass_instances. +Hint Extern 0 (reify_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> do_reifyf_goal () : typeclass_instances. (** For reification including [Abs] *) +Class reify_abs_internal {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs_internal : T. Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. Ltac reify_abs base_type_code interp_base_type op var e := let reify_rec e := reify_abs base_type_code interp_base_type op var e in @@ -347,7 +367,7 @@ Ltac reify_abs base_type_code interp_base_type op var e := let not_x := fresh x in let C' := match constr:(Set) with | _ => constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => - (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) + (_ : reify_abs_internal reify_tag C)) (* [C] here is an open term that references "x" by name *) | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to reify by typeclasses:" e) end in let C := match constr:(Set) with @@ -362,11 +382,24 @@ Ltac reify_abs base_type_code interp_base_type op var e := end end. +Ltac do_reify_abs_goal _ := + debug_enter_reify_rec; + let e := lazymatch goal with + | [ |- reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ] + => reify_abs base_type_code interp_base_type op var e + | [ |- reify_abs_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ] + => reify_abs base_type_code interp_base_type op var e + end in + debug_leave_reify_rec e; + eexact e. + Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. +=> do_reify_abs_goal () : typeclass_instances. +Hint Extern 0 (reify_abs_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> do_reify_abs_goal () : typeclass_instances. Ltac Reify' base_type_code interp_base_type op e := - lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with + lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs_internal (@exprf base_type_code interp_base_type op var) e)) with (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *) end. Ltac Reify base_type_code interp_base_type op make_const e := @@ -463,7 +496,7 @@ Ltac unique_reify_context_variable base_type_code interp_base_type op F Fbody rT => let maybe_x := fresh x in let not_x := fresh maybe_x in let rF := lazymatch constr:(fun var' (x : X) (not_x : var' src) (_ : reify_var_for_in_is base_type_code x src not_x) - => (_ : reify (reify_pretag var') Fbody')) + => (_ : reify_internal (reify_pretag var') Fbody')) with | fun (var' : ?VAR) (x : ?X) (v : ?V) _ => ?C => constr:(fun (var' : VAR) (v : V) => C) |