diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-02 13:43:58 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-07 00:05:30 -0400 |
| commit | 76965f85cf742fb2fe9f75d7187da135fbd0eb57 (patch) | |
| tree | ce70e889b85c16ca3e00cb9311bb0fbab72117cf /src/Specific/IntegrationTestTemporaryMiscCommon.v | |
| parent | d7bc99e533f12c11e9e83ea9cec9300bf420caeb (diff) | |
Factor out parameter-specific code
After | File Name | Before || Change
------------------------------------------------------------------------------
6m08.27s | Total | 6m25.95s || -0m17.68s
------------------------------------------------------------------------------
N/A | Specific/ArithmeticSynthesisTest32 | 0m39.62s || -0m39.61s
0m38.34s | Specific/X25519/C32/ArithmeticSynthesisTest | N/A || +0m38.34s
0m20.46s | Specific/X25519/C32/ReificationTypes | N/A || +0m20.46s
2m31.97s | Specific/X25519/C64/ladderstep | 2m51.10s || -0m19.12s
N/A | Specific/ArithmeticSynthesisTest | 0m09.54s || -0m09.53s
0m09.50s | Specific/X25519/C64/ArithmeticSynthesisTest | N/A || +0m09.50s
1m03.72s | Specific/X25519/C32/femul | 1m11.22s || -0m07.50s
0m10.44s | Specific/IntegrationTestFreeze | 0m17.29s || -0m06.84s
0m34.55s | Specific/X25519/C32/fesquare | 0m40.47s || -0m05.92s
0m05.50s | Specific/X25519/C64/ReificationTypes | N/A || +0m05.50s
0m12.47s | Specific/X25519/C64/femul | 0m13.98s || -0m01.50s
0m08.93s | Specific/X25519/C64/fesquare | 0m10.67s || -0m01.74s
0m11.14s | Specific/IntegrationTestSub | 0m12.06s || -0m00.92s
0m00.50s | Specific/X25519/C32/CurveParameters | N/A || +0m00.50s
0m00.38s | Specific/CurveParameters | N/A || +0m00.38s
0m00.37s | Specific/X25519/C64/CurveParameters | N/A || +0m00.37s
Diffstat (limited to 'src/Specific/IntegrationTestTemporaryMiscCommon.v')
| -rw-r--r-- | src/Specific/IntegrationTestTemporaryMiscCommon.v | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v index 4aae7ee0a..083e82207 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -237,23 +237,18 @@ Ltac unmap_map_tuple _ := => rewrite <- (Tuple.map_map (n:=N) f g : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x)))) end. +Ltac get_feW_bounded boundedT := + lazymatch boundedT with + | and ?X ?Y => get_feW_bounded X + | ?feW_bounded _ => feW_bounded + end. Ltac subst_feW _ := let T := lazymatch goal with |- @sig ?T _ => T end in let boundedT := lazymatch goal with |- { e | ?A -> _ } => A end in - match goal with - | [ feW := _ : Type |- _ ] - => match goal with - | [ feW_bounded := _ : feW -> Prop |- _ ] - => lazymatch T with - | context[feW] => idtac - end; - lazymatch boundedT with - | context[feW_bounded _] => idtac - end; - subst feW feW_bounded - end - end; - cbv beta. + let feW_bounded := get_feW_bounded boundedT in + let feW := lazymatch type of feW_bounded with ?feW -> Prop => feW end in + cbv [feW feW_bounded]; + try clear feW feW_bounded. Ltac finish_conjoined_preglue _ := [ > match goal with | [ FINAL : _ /\ ?e |- _ ] => is_evar e; refine (proj2 FINAL) |