diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-02 11:55:46 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-02 11:58:50 -0400 |
| commit | f94f9e5b5e5deb62b5dbecab31f64b9865436955 (patch) | |
| tree | 4633c47922193966b87cf601159c7df30b1c4720 /src | |
| parent | 9458d877c381366b36275a2aa695c07fad0775bd (diff) | |
Make some typeclasses opaque
Not sure if it actually does anything in this case... The intent is to
prevent tc resolution from unfolding [reify] and [reify_internal] /
picking up one when looking for the other.
After | File Name | Before || Change
---------------------------------------------------------------------------------------
13m02.51s | Total | 13m01.90s || +0m00.60s
---------------------------------------------------------------------------------------
1m30.27s | Specific/IntegrationTestKaratsubaMul | 1m25.34s || +0m04.92s
2m50.80s | Specific/X25519/C64/ladderstep | 2m53.74s || -0m02.93s
2m21.34s | Specific/NISTP256/AMD64/femul | 2m21.37s || -0m00.03s
1m12.30s | Specific/X25519/C32/femul | 1m12.04s || +0m00.26s
1m09.50s | Specific/IntegrationTestLadderstep130 | 1m09.66s || -0m00.15s
0m41.30s | Specific/X25519/C32/fesquare | 0m41.27s || +0m00.02s
0m27.08s | Specific/IntegrationTestMontgomeryP256_128 | 0m27.13s || -0m00.05s
0m17.64s | Specific/NISTP256/AMD64/fesub | 0m18.06s || -0m00.41s
0m16.45s | Specific/IntegrationTestFreeze | 0m17.36s || -0m00.91s
0m15.94s | Specific/NISTP256/AMD64/feadd | 0m16.02s || -0m00.08s
0m14.74s | Specific/NISTP256/AMD64/feopp | 0m14.42s || +0m00.32s
0m14.33s | Specific/X25519/C64/femul | 0m13.97s || +0m00.35s
0m12.41s | Specific/IntegrationTestSub | 0m12.44s || -0m00.02s
0m11.91s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.06s || -0m00.15s
0m11.61s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.00s || -0m00.39s
0m10.95s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.82s || +0m00.12s
0m10.28s | Specific/X25519/C64/fesquare | 0m10.46s || -0m00.18s
0m09.68s | Specific/NISTP256/AMD64/fenz | 0m09.76s || -0m00.08s
0m09.28s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.30s || -0m00.02s
0m03.54s | Compilers/TestCase | 0m03.41s || +0m00.12s
0m03.04s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.20s || -0m00.16s
0m02.99s | Specific/NISTP256/FancyMachine256/Barrett | 0m02.99s || +0m00.00s
0m02.16s | Specific/NISTP256/FancyMachine256/Core | 0m02.20s || -0m00.04s
0m00.82s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || +0m00.01s
0m00.70s | Compilers/Z/Bounds/Pipeline | 0m00.66s || +0m00.03s
0m00.57s | Compilers/Z/Reify | 0m00.53s || +0m00.03s
0m00.50s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.54s || -0m00.04s
0m00.38s | Compilers/Reify | 0m00.36s || +0m00.02s
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Reify.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index 4943eca86..0ec27717a 100644 --- a/src/Compilers/Reify.v +++ b/src/Compilers/Reify.v @@ -66,6 +66,7 @@ Ltac debug_enter_reify_abs e := debug2 ltac:(fun _ => debug_enter_reify_idtac "r 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. +Typeclasses Opaque reify_internal reify. 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} _. @@ -339,6 +340,7 @@ Hint Extern 0 (reify_internal (@exprf ?base_type_code ?interp_base_type ?op ?var (** 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. +Typeclasses Opaque reify_abs_internal reify_abs. 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 let reifyf_term e := reifyf base_type_code interp_base_type op var e in |