diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-23 01:38:50 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-04-24 09:39:45 -0400 |
commit | 8a4d828e05bca153f12370d08d3b4ad404fbbee2 (patch) | |
tree | cd0b847c4d39cdd440d1c2a6833ae54ab5149067 /.dir-locals.el | |
parent | ecdfd03c636ab63e167fbe4fc4d7ab0ed5d9db74 (diff) |
Do less reduction in GENERATEDIdentifiersWithoutTypes
Since more of the definitions are now done in Gallina, hopefully these
should be easier to factor out / parameterize over the type of
identifiers, now.
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------
21m28.78s | Total | 21m49.80s || -0m21.01s | -1.60%
-----------------------------------------------------------------------------------------------
0m22.98s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m49.53s || -0m26.55s | -53.60%
0m47.26s | p521_32.c | 0m44.08s || +0m03.17s | +7.21%
0m36.30s | ExtractionHaskell/saturated_solinas | 0m32.96s || +0m03.33s | +10.13%
1m00.34s | ExtractionHaskell/word_by_word_montgomery | 1m02.45s || -0m02.10s | -3.37%
0m26.90s | SlowPrimeSynthesisExamples.vo | 0m24.35s || +0m02.54s | +10.47%
0m16.06s | GENERATEDIdentifiersWithoutTypes.vo | 0m19.05s || -0m02.99s | -15.69%
0m14.89s | ExtractionOCaml/unsaturated_solinas | 0m12.83s || +0m02.06s | +16.05%
0m43.92s | ExtractionHaskell/unsaturated_solinas | 0m42.40s || +0m01.52s | +3.58%
0m20.11s | ExtractionOCaml/word_by_word_montgomery | 0m21.19s || -0m01.08s | -5.09%
0m20.06s | p256_32.c | 0m21.81s || -0m01.75s | -8.02%
0m17.96s | secp256k1_32.c | 0m19.45s || -0m01.48s | -7.66%
0m13.58s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.89s || -0m01.31s | -8.79%
0m07.27s | ExtractionOCaml/saturated_solinas.ml | 0m05.75s || +0m01.51s | +26.43%
3m23.62s | p384_32.c | 3m23.29s || +0m00.33s | +0.16%
1m42.18s | Fancy/Barrett256.vo | 1m41.69s || +0m00.49s | +0.48%
1m33.94s | RewriterWf2.vo | 1m34.43s || -0m00.49s | -0.51%
0m55.14s | Rewriter/ToFancyWithCasts.vo | 0m55.92s || -0m00.78s | -1.39%
0m46.15s | Rewriter/NBE.vo | 0m46.06s || +0m00.08s | +0.19%
0m44.70s | Rewriter/ArithWithCasts.vo | 0m44.55s || +0m00.15s | +0.33%
0m43.96s | RewriterInterpProofs1.vo | 0m44.18s || -0m00.21s | -0.49%
0m39.78s | p521_64.c | 0m38.84s || +0m00.93s | +2.42%
0m36.72s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.54s || +0m00.17s | +0.49%
0m35.92s | RewriterWf1.vo | 0m36.26s || -0m00.33s | -0.93%
0m34.57s | Fancy/Montgomery256.vo | 0m34.64s || -0m00.07s | -0.20%
0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.17s || +0m00.11s | +0.44%
0m23.67s | Rewriter/Arith.vo | 0m24.59s || -0m00.91s | -3.74%
0m20.78s | PushButtonSynthesis/BarrettReduction.vo | 0m20.69s || +0m00.08s | +0.43%
0m18.97s | p448_solinas_64.c | 0m18.10s || +0m00.86s | +4.80%
0m14.02s | p434_64.c | 0m13.37s || +0m00.65s | +4.86%
0m11.26s | ExtractionOCaml/unsaturated_solinas.ml | 0m10.61s || +0m00.65s | +6.12%
0m10.76s | ExtractionOCaml/saturated_solinas | 0m11.65s || -0m00.89s | -7.63%
0m08.76s | p224_32.c | 0m09.58s || -0m00.82s | -8.55%
0m08.07s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.96s || +0m00.11s | +1.38%
0m07.88s | p384_64.c | 0m08.81s || -0m00.93s | -10.55%
0m06.98s | BoundsPipeline.vo | 0m06.97s || +0m00.01s | +0.14%
0m06.41s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || +0m00.89s | +16.12%
0m05.21s | ExtractionHaskell/saturated_solinas.hs | 0m04.48s || +0m00.72s | +16.29%
0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.61s || -0m00.06s | -1.93%
0m03.33s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.04s | -1.47%
0m03.20s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.02s | -0.62%
0m03.05s | curve25519_32.c | 0m02.76s || +0m00.29s | +10.50%
0m02.63s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.70s || -0m00.07s | -2.59%
0m02.53s | Rewriter.vo | 0m02.04s || +0m00.48s | +24.01%
0m02.10s | curve25519_64.c | 0m01.80s || +0m00.30s | +16.66%
0m01.94s | p224_64.c | 0m01.52s || +0m00.41s | +27.63%
0m01.85s | secp256k1_64.c | 0m01.55s || +0m00.30s | +19.35%
0m01.40s | CLI.vo | 0m01.33s || +0m00.06s | +5.26%
0m01.36s | p256_64.c | 0m01.84s || -0m00.48s | -26.08%
0m01.33s | Rewriter/StripLiteralCasts.vo | 0m01.22s || +0m00.11s | +9.01%
0m01.23s | CompilersTestCases.vo | 0m01.14s || +0m00.09s | +7.89%
0m01.15s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.03s | +3.60%
0m01.13s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.04s | -3.41%
0m01.11s | Rewriter/ToFancy.vo | 0m01.07s || +0m00.04s | +3.73%
0m00.80s | RewriterAll.vo | 0m00.80s || +0m00.00s | +0.00%
0m00.74s | RewriterAllTactics.vo | 0m00.91s || -0m00.17s | -18.68%
The diff in the .ml files is quite small, and is effectively just
variable renaming:
```diff
diff --git a/src/ExtractionOCaml/saturated_solinas.ml b/src/ExtractionOCaml/saturated_solinas.ml
index fd8a9d3..e9afa49 100644
--- a/src/ExtractionOCaml/saturated_solinas.ml
+++ b/src/ExtractionOCaml/saturated_solinas.ml
@@ -39856,7 +39856,7 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Literal (t1, v) ->
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
@@ -39962,7 +39962,7 @@ module Coq2_Compilers =
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
@@ -40068,7 +40068,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
@@ -40174,7 +40174,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
| Compilers.Coq_ident.Nat_succ -> None
@@ -40280,7 +40280,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange ->
- (fun v0 -> Some (Obj.magic (v0, ())))) v
+ (fun x -> Some (Obj.magic (x, ())))) v
| Compilers.Coq_ident.Nat_succ -> None
| Compilers.Coq_ident.Nat_pred -> None
| Compilers.Coq_ident.Nat_max -> None
@@ -49466,8 +49466,8 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Coq_fancy_mullh _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhl _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhh _ -> None
- | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) ->
- Some (Obj.magic (log2wordmax, (z0, ())))
+ | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) ->
+ Some (Obj.magic (log2wordmax, (x, ())))
| Compilers.Coq_ident.Coq_fancy_selc -> None
| Compilers.Coq_ident.Coq_fancy_selm _ -> None
| Compilers.Coq_ident.Coq_fancy_sell -> None
diff --git a/src/ExtractionOCaml/unsaturated_solinas.ml b/src/ExtractionOCaml/unsaturated_solinas.ml
index 473992c..4d4d604 100644
--- a/src/ExtractionOCaml/unsaturated_solinas.ml
+++ b/src/ExtractionOCaml/unsaturated_solinas.ml
@@ -40045,7 +40045,7 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Literal (t1, v) ->
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
@@ -40151,7 +40151,7 @@ module Coq2_Compilers =
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
@@ -40257,7 +40257,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
@@ -40363,7 +40363,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
| Compilers.Coq_ident.Nat_succ -> None
@@ -40469,7 +40469,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange ->
- (fun v0 -> Some (Obj.magic (v0, ())))) v
+ (fun x -> Some (Obj.magic (x, ())))) v
| Compilers.Coq_ident.Nat_succ -> None
| Compilers.Coq_ident.Nat_pred -> None
| Compilers.Coq_ident.Nat_max -> None
@@ -49655,8 +49655,8 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Coq_fancy_mullh _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhl _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhh _ -> None
- | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) ->
- Some (Obj.magic (log2wordmax, (z0, ())))
+ | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) ->
+ Some (Obj.magic (log2wordmax, (x, ())))
| Compilers.Coq_ident.Coq_fancy_selc -> None
| Compilers.Coq_ident.Coq_fancy_selm _ -> None
| Compilers.Coq_ident.Coq_fancy_sell -> None
diff --git a/src/ExtractionOCaml/word_by_word_montgomery.ml b/src/ExtractionOCaml/word_by_word_montgomery.ml
index f955bc6..a672b5d 100644
--- a/src/ExtractionOCaml/word_by_word_montgomery.ml
+++ b/src/ExtractionOCaml/word_by_word_montgomery.ml
@@ -39944,7 +39944,7 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Literal (t1, v) ->
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
@@ -40050,7 +40050,7 @@ module Coq2_Compilers =
(match t1 with
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
@@ -40156,7 +40156,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
@@ -40262,7 +40262,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Z -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat ->
- (fun v0 -> Some (Obj.magic (v0, ())))
+ (fun x -> Some (Obj.magic (x, ())))
| Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None))
v
| Compilers.Coq_ident.Nat_succ -> None
@@ -40368,7 +40368,7 @@ module Coq2_Compilers =
| Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None)
| Compilers.Coq_base.Coq_type.Coq_zrange ->
- (fun v0 -> Some (Obj.magic (v0, ())))) v
+ (fun x -> Some (Obj.magic (x, ())))) v
| Compilers.Coq_ident.Nat_succ -> None
| Compilers.Coq_ident.Nat_pred -> None
| Compilers.Coq_ident.Nat_max -> None
@@ -49554,8 +49554,8 @@ module Coq2_Compilers =
| Compilers.Coq_ident.Coq_fancy_mullh _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhl _ -> None
| Compilers.Coq_ident.Coq_fancy_mulhh _ -> None
- | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) ->
- Some (Obj.magic (log2wordmax, (z0, ())))
+ | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) ->
+ Some (Obj.magic (log2wordmax, (x, ())))
| Compilers.Coq_ident.Coq_fancy_selc -> None
| Compilers.Coq_ident.Coq_fancy_selm _ -> None
| Compilers.Coq_ident.Coq_fancy_sell -> None
```
Diffstat (limited to '.dir-locals.el')
0 files changed, 0 insertions, 0 deletions