aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-08 02:41:01 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-03-08 03:09:22 -0500
commitac184af76e778cbc9e9655bc96b90fc76f6161a5 (patch)
tree9641b234ecb6be48bbbf2404a68b314561bf5d7a
parentb91315237cc35aa061b2549d31fb908416019b7e (diff)
Add eager_nth_default
After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 36m12.92s | Total | 35m47.30s || +0m25.61s | +1.19% ----------------------------------------------------------------------------------------------------------- 3m17.05s | p384_32.c | 3m13.40s || +0m03.65s | +1.88% 0m35.31s | AbstractInterpretationZRangeProofs.vo | 0m32.23s || +0m03.08s | +9.55% 2m54.44s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m51.77s || +0m02.66s | +1.55% 1m49.48s | RewriterRulesInterpGood.vo | 1m47.32s || +0m02.15s | +2.01% 1m08.68s | GENERATEDIdentifiersWithoutTypesProofs.vo | 1m06.34s || +0m02.34s | +3.52% 0m43.79s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m45.80s || -0m02.00s | -4.38% 0m42.94s | UnderLetsProofs.vo | 0m40.56s || +0m02.37s | +5.86% 0m24.06s | ExtractionOCaml/word_by_word_montgomery | 0m21.22s || +0m02.83s | +13.38% 2m40.36s | Fancy/Compiler.vo | 2m38.94s || +0m01.42s | +0.89% 2m01.11s | RewriterWf2.vo | 1m59.26s || +0m01.85s | +1.55% 1m55.19s | RewriterRulesGood.vo | 1m56.66s || -0m01.46s | -1.26% 1m47.22s | Fancy/Barrett256.vo | 1m45.62s || +0m01.59s | +1.51% 0m58.84s | ExtractionHaskell/word_by_word_montgomery | 0m57.60s || +0m01.24s | +2.15% 0m31.40s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m29.80s || +0m01.59s | +5.36% 0m29.65s | ExtractionHaskell/saturated_solinas | 0m31.01s || -0m01.36s | -4.38% 0m25.82s | SlowPrimeSynthesisExamples.vo | 0m24.58s || +0m01.24s | +5.04% 0m18.46s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m16.98s || +0m01.48s | +8.71% 0m14.02s | ExtractionOCaml/unsaturated_solinas | 0m12.74s || +0m01.27s | +10.04% 0m07.66s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.32s || +0m01.33s | +21.20% 1m21.57s | Rewriter.vo | 1m22.53s || -0m00.96s | -1.16% 0m55.21s | RewriterInterpProofs1.vo | 0m56.14s || -0m00.92s | -1.65% 0m54.08s | AbstractInterpretationWf.vo | 0m54.37s || -0m00.28s | -0.53% 0m46.95s | p521_32.c | 0m46.27s || +0m00.67s | +1.46% 0m44.37s | LanguageInversion.vo | 0m43.42s || +0m00.94s | +2.18% 0m41.31s | ExtractionHaskell/unsaturated_solinas | 0m41.46s || -0m00.14s | -0.36% 0m40.51s | p521_64.c | 0m40.38s || +0m00.12s | +0.32% 0m37.50s | Fancy/Montgomery256.vo | 0m37.46s || +0m00.03s | +0.10% 0m36.28s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.34s || -0m00.06s | -0.16% 0m33.28s | AbstractInterpretationProofs.vo | 0m33.19s || +0m00.09s | +0.27% 0m29.56s | LanguageWf.vo | 0m29.64s || -0m00.08s | -0.26% 0m26.86s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.96s || -0m00.10s | -0.37% 0m25.33s | RewriterWf1.vo | 0m25.65s || -0m00.32s | -1.24% 0m19.81s | p256_32.c | 0m20.11s || -0m00.30s | -1.49% 0m18.70s | secp256k1_32.c | 0m19.18s || -0m00.48s | -2.50% 0m18.62s | p448_solinas_64.c | 0m19.51s || -0m00.89s | -4.56% 0m16.73s | CStringification.vo | 0m16.25s || +0m00.48s | +2.95% 0m15.03s | p434_64.c | 0m15.84s || -0m00.81s | -5.11% 0m13.45s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.80s || -0m00.35s | -2.53% 0m13.44s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.30s || +0m00.13s | +1.05% 0m10.74s | ExtractionOCaml/saturated_solinas | 0m10.38s || +0m00.35s | +3.46% 0m09.11s | p224_32.c | 0m08.93s || +0m00.17s | +2.01% 0m08.78s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.92s || +0m00.85s | +10.85% 0m08.74s | p384_64.c | 0m08.50s || +0m00.24s | +2.82% 0m08.66s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.47s || -0m00.81s | -8.55% 0m07.90s | ExtractionOCaml/saturated_solinas.ml | 0m06.93s || +0m00.97s | +13.99% 0m06.80s | BoundsPipeline.vo | 0m06.73s || +0m00.06s | +1.04% 0m06.57s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.78s || -0m00.20s | -3.09% 0m05.68s | Fancy/Prod.vo | 0m05.78s || -0m00.10s | -1.73% 0m05.36s | ExtractionHaskell/saturated_solinas.hs | 0m05.40s || -0m00.04s | -0.74% 0m03.86s | MiscCompilerPassesProofs.vo | 0m04.20s || -0m00.34s | -8.09% 0m03.37s | PushButtonSynthesis/Primitives.vo | 0m03.41s || -0m00.04s | -1.17% 0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.22s || +0m00.13s | +4.34% 0m03.20s | PushButtonSynthesis/BarrettReduction.vo | 0m03.16s || +0m00.04s | +1.26% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.12s || +0m00.06s | +2.24% 0m03.00s | curve25519_32.c | 0m02.62s || +0m00.37s | +14.50% 0m02.83s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.82s || +0m00.01s | +0.35% 0m02.02s | curve25519_64.c | 0m02.12s || -0m00.10s | -4.71% 0m01.61s | p224_64.c | 0m01.48s || +0m00.13s | +8.78% 0m01.60s | secp256k1_64.c | 0m01.70s || -0m00.09s | -5.88% 0m01.48s | p256_64.c | 0m01.28s || +0m00.19s | +15.62% 0m01.34s | CompilersTestCases.vo | 0m01.24s || +0m00.10s | +8.06% 0m01.30s | CLI.vo | 0m01.35s || -0m00.05s | -3.70% 0m01.30s | Language.vo | 0m01.33s || -0m00.03s | -2.25% 0m01.28s | AbstractInterpretation.vo | 0m01.28s || +0m00.00s | +0.00% 0m01.24s | RewriterProofs.vo | 0m01.16s || +0m00.08s | +6.89% 0m01.07s | StandaloneHaskellMain.vo | 0m01.26s || -0m00.18s | -15.07% 0m01.04s | StandaloneOCamlMain.vo | 0m01.27s || -0m00.23s | -18.11% 0m00.76s | MiscCompilerPasses.vo | 0m00.82s || -0m00.05s | -7.31% 0m00.61s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.66s || -0m00.05s | -7.57% 0m00.57s | PushButtonSynthesis/ReificationCache.vo | 0m00.52s || +0m00.04s | +9.61% 0m00.48s | UnderLets.vo | 0m00.51s || -0m00.03s | -5.88%
Diffstat
-rw-r--r--src/AbstractInterpretation.v1
-rw-r--r--src/CStringification.v4
-rw-r--r--src/GENERATEDIdentifiersWithoutTypes.v28
-rw-r--r--src/Language.v5
4 files changed, 38 insertions, 0 deletions
diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index ca0cb68bd..e74582ae6 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -576,6 +576,7 @@ Module Compilers.
=> fold_right f v ls
| None => ZRange.type.base.option.None
end
+ | ident.eager_List_nth_default _
| ident.List_nth_default _
=> fun d ls n
=> match ls, n with
diff --git a/src/CStringification.v b/src/CStringification.v
index ff455130b..0862aec64 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -285,6 +285,8 @@ Module Compilers.
=> fun args => (show_application with_casts (fun _ => "fold_right") args, ZRange.type.base.option.None)
| ident.List_update_nth T
=> fun args => (show_application with_casts (fun _ => "update_nth") args, ZRange.type.base.option.None)
+ | ident.eager_List_nth_default T
+ => fun '((d, dr), ((ls, lsr), ((i, ir), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) (ls 10%nat ++ "[[" ++ i 200%nat ++ "]]"), ZRange.type.base.option.None)
| ident.List_nth_default T
=> fun '((d, dr), ((ls, lsr), ((i, ir), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 10) (ls 10%nat ++ "[" ++ i 200%nat ++ "]"), ZRange.type.base.option.None)
| ident.Z_mul => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " * " ++ y 39%nat), ZRange.type.base.option.None)
@@ -413,6 +415,7 @@ Module Compilers.
| ident.List_fold_right A B => "fold_right"
| ident.List_update_nth T => "update_nth"
| ident.List_nth_default T => "nth"
+ | ident.eager_List_nth_default T => "eager_nth"
| ident.Some _ => "Some"
| ident.None _ => "None"
| ident.option_rect _ _ => "option_rect"
@@ -1320,6 +1323,7 @@ Module Compilers.
| ident.List_fold_right _ _
| ident.List_update_nth _
| ident.List_nth_default _
+ | ident.eager_List_nth_default _
| ident.Z_pow
| ident.Z_div
| ident.Z_modulo
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index db84a33a3..c84540ba1 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -450,6 +450,17 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
(fun x : Compilers.base.type => type.base x)
(Compilers.base.type.type_base base.type.nat) ->
(fun x : Compilers.base.type => type.base x) T)%ptype
+ | eager_List_nth_default : forall T : Compilers.base.type,
+ ident
+ ((fun x : Compilers.base.type => type.base x)
+ T ->
+ (fun x : Compilers.base.type => type.base x)
+ (Compilers.base.type.list T) ->
+ (fun x : Compilers.base.type => type.base x)
+ (Compilers.base.type.type_base
+ base.type.nat) ->
+ (fun x : Compilers.base.type => type.base x)
+ T)%ptype
| Z_add : ident
((fun x : Compilers.base.type => type.base x)
(Compilers.base.type.type_base base.type.Z) ->
@@ -898,6 +909,7 @@ show_match_ident = r"""match # with
| ident.List_fold_right A B =>
| ident.List_update_nth T =>
| ident.List_nth_default T =>
+ | ident.eager_List_nth_default T =>
| ident.Z_add =>
| ident.Z_mul =>
| ident.Z_pow =>
@@ -1509,6 +1521,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right
| List_update_nth
| List_nth_default
+ | eager_List_nth_default
| Z_add
| Z_mul
| Z_pow
@@ -1604,6 +1617,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right => Compilers.base.type * Compilers.base.type
| List_update_nth => Compilers.base.type
| List_nth_default => Compilers.base.type
+ | eager_List_nth_default => Compilers.base.type
| Z_add => unit
| Z_mul => unit
| Z_pow => unit
@@ -1700,6 +1714,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right => false
| List_update_nth => false
| List_nth_default => false
+ | eager_List_nth_default => false
| Z_add => true
| Z_mul => true
| Z_pow => true
@@ -1796,6 +1811,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right, Compilers.ident.List_fold_right A B => Datatypes.Some (A, B)
| List_update_nth, Compilers.ident.List_update_nth T => Datatypes.Some T
| List_nth_default, Compilers.ident.List_nth_default T => Datatypes.Some T
+ | eager_List_nth_default, Compilers.ident.eager_List_nth_default T => Datatypes.Some T
| Z_add, Compilers.ident.Z_add => Datatypes.Some tt
| Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
| Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
@@ -1888,6 +1904,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right, _
| List_update_nth, _
| List_nth_default, _
+ | eager_List_nth_default, _
| Z_add, _
| Z_mul, _
| Z_pow, _
@@ -1985,6 +2002,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right => fun arg => let '(A, B) := eta2 arg in ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (Compilers.base.type.list B) -> type.base A)%ptype
| List_update_nth => fun T => (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.list T))%ptype
| List_nth_default => fun T => (type.base T -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base T)%ptype
+ | eager_List_nth_default => fun T => (type.base T -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base T)%ptype
| Z_add => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
| Z_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
| Z_pow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
@@ -2081,6 +2099,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_fold_right arg') with (A, B) => @Compilers.ident.List_fold_right A B end
| List_update_nth => fun T => @Compilers.ident.List_update_nth T
| List_nth_default => fun T => @Compilers.ident.List_nth_default T
+ | eager_List_nth_default => fun T => @Compilers.ident.eager_List_nth_default T
| Z_add => fun _ => @Compilers.ident.Z_add
| Z_mul => fun _ => @Compilers.ident.Z_mul
| Z_pow => fun _ => @Compilers.ident.Z_pow
@@ -2184,6 +2203,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.List_fold_right A B => f _ (@Compilers.ident.List_fold_right A B)
| Compilers.ident.List_update_nth T => f _ (@Compilers.ident.List_update_nth T)
| Compilers.ident.List_nth_default T => f _ (@Compilers.ident.List_nth_default T)
+ | Compilers.ident.eager_List_nth_default T => f _ (@Compilers.ident.eager_List_nth_default T)
| Compilers.ident.Z_add => f _ Compilers.ident.Z_add
| Compilers.ident.Z_mul => f _ Compilers.ident.Z_mul
| Compilers.ident.Z_pow => f _ Compilers.ident.Z_pow
@@ -2279,6 +2299,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| List_fold_right {A : base.type} {B : base.type} : ident ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (base.type.list B) -> type.base A)%ptype
| List_update_nth {T : base.type} : ident (type.base (base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (base.type.list T) -> type.base (base.type.list T))%ptype
| List_nth_default {T : base.type} : ident (type.base T -> type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat) -> type.base T)%ptype
+ | eager_List_nth_default {T : base.type} : ident (type.base T -> type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat) -> type.base T)%ptype
| Z_add : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
| Z_mul : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
| Z_pow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
@@ -2374,6 +2395,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @List_fold_right A B => Raw.ident.List_fold_right
| @List_update_nth T => Raw.ident.List_update_nth
| @List_nth_default T => Raw.ident.List_nth_default
+ | @eager_List_nth_default T => Raw.ident.eager_List_nth_default
| @Z_add => Raw.ident.Z_add
| @Z_mul => Raw.ident.Z_mul
| @Z_pow => Raw.ident.Z_pow
@@ -2470,6 +2492,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @List_fold_right A B => []
| @List_update_nth T => []
| @List_nth_default T => []
+ | @eager_List_nth_default T => []
| @Z_add => []
| @Z_mul => []
| @Z_pow => []
@@ -2566,6 +2589,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @List_fold_right A B => fun _ => @Compilers.ident.List_fold_right _ _
| @List_update_nth T => fun _ => @Compilers.ident.List_update_nth _
| @List_nth_default T => fun _ => @Compilers.ident.List_nth_default _
+ | @eager_List_nth_default T => fun _ => @Compilers.ident.eager_List_nth_default _
| @Z_add => fun _ => @Compilers.ident.Z_add
| @Z_mul => fun _ => @Compilers.ident.Z_mul
| @Z_pow => fun _ => @Compilers.ident.Z_pow
@@ -2666,6 +2690,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Datatypes.Some tt
| @List_update_nth T, Compilers.ident.List_update_nth T' => Datatypes.Some tt
| @List_nth_default T, Compilers.ident.List_nth_default T' => Datatypes.Some tt
+ | @eager_List_nth_default T, Compilers.ident.eager_List_nth_default T' => Datatypes.Some tt
| @Z_add, Compilers.ident.Z_add => Datatypes.Some tt
| @Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
| @Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
@@ -2758,6 +2783,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @List_fold_right _ _, _
| @List_update_nth _, _
| @List_nth_default _, _
+ | @eager_List_nth_default _, _
| @Z_add, _
| @Z_mul, _
| @Z_pow, _
@@ -2855,6 +2881,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.List_fold_right A B => @List_fold_right (base.relax A) (base.relax B)
| Compilers.ident.List_update_nth T => @List_update_nth (base.relax T)
| Compilers.ident.List_nth_default T => @List_nth_default (base.relax T)
+ | Compilers.ident.eager_List_nth_default T => @eager_List_nth_default (base.relax T)
| Compilers.ident.Z_add => @Z_add
| Compilers.ident.Z_mul => @Z_mul
| Compilers.ident.Z_pow => @Z_pow
@@ -2951,6 +2978,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.List_fold_right A B => tt
| Compilers.ident.List_update_nth T => tt
| Compilers.ident.List_nth_default T => tt
+ | Compilers.ident.eager_List_nth_default T => tt
| Compilers.ident.Z_add => tt
| Compilers.ident.Z_mul => tt
| Compilers.ident.Z_pow => tt
diff --git a/src/Language.v b/src/Language.v
index 703449eca..81ca370db 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -898,6 +898,7 @@ Module Compilers.
| List_fold_right {A B:base.type} : ident ((B -> A -> A) -> A -> list B -> A)
| List_update_nth {T:base.type} : ident (nat -> (T -> T) -> list T -> list T)
| List_nth_default {T:base.type} : ident (T -> list T -> nat -> T)
+ | eager_List_nth_default {T:base.type} : ident (T -> list T -> nat -> T)
| Z_add : ident (Z -> Z -> Z)
| Z_mul : ident (Z -> Z -> Z)
| Z_pow : ident (Z -> Z -> Z)
@@ -1086,6 +1087,7 @@ Module Compilers.
| List_fold_right A B => @List.fold_right _ _
| List_update_nth T => update_nth
| List_nth_default T => @nth_default _
+ | eager_List_nth_default T => @nth_default _
| Z_add => Z.add
| Z_mul => Z.mul
| Z_pow => Z.pow
@@ -1422,6 +1424,9 @@ Module Compilers.
| @List.nth_default ?T
=> let rT := base.reify T in
then_tac (@ident.List_nth_default rT)
+ | ident.eagerly (@List.nth_default) ?T
+ => let rT := base.reify T in
+ then_tac (@ident.eager_List_nth_default rT)
| Z.add => then_tac ident.Z_add
| Z.mul => then_tac ident.Z_mul
| Z.pow => then_tac ident.Z_pow
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 22:41:18 +0000