From 8a2f95d13c792b236fdb962895be76b7c757eff6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Mar 2019 19:22:00 -0500 Subject: Add list_rect_arrow After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 36m06.27s | Total | 35m50.70s || +0m15.57s | +0.72% ----------------------------------------------------------------------------------------------------------- 2m45.00s | Fancy/Compiler.vo | 2m40.67s || +0m04.32s | +2.69% 1m05.90s | GENERATEDIdentifiersWithoutTypesProofs.vo | 1m02.06s || +0m03.84s | +6.18% 0m19.29s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m16.24s || +0m03.05s | +18.78% 2m55.24s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m57.84s || -0m02.59s | -1.46% 1m56.35s | RewriterRulesGood.vo | 1m54.16s || +0m02.18s | +1.91% 0m41.32s | ExtractionHaskell/unsaturated_solinas | 0m39.10s || +0m02.21s | +5.67% 0m34.84s | AbstractInterpretationProofs.vo | 0m32.77s || +0m02.07s | +6.31% 0m17.77s | p448_solinas_64.c | 0m20.12s || -0m02.35s | -11.67% 2m01.09s | RewriterWf2.vo | 1m59.61s || +0m01.48s | +1.23% 1m48.15s | RewriterRulesInterpGood.vo | 1m49.56s || -0m01.40s | -1.28% 1m21.56s | Rewriter.vo | 1m22.98s || -0m01.42s | -1.71% 0m57.30s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || -0m01.46s | -2.48% 0m47.94s | p521_32.c | 0m46.84s || +0m01.09s | +2.34% 0m38.63s | Fancy/Montgomery256.vo | 0m37.28s || +0m01.35s | +3.62% 0m26.01s | SlowPrimeSynthesisExamples.vo | 0m24.90s || +0m01.11s | +4.45% 0m13.56s | ExtractionOCaml/unsaturated_solinas | 0m12.32s || +0m01.24s | +10.06% 0m09.90s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.70s || +0m01.20s | +13.79% 3m16.06s | p384_32.c | 3m15.80s || +0m00.25s | +0.13% 1m46.10s | Fancy/Barrett256.vo | 1m47.02s || -0m00.92s | -0.85% 0m56.15s | RewriterInterpProofs1.vo | 0m56.60s || -0m00.45s | -0.79% 0m54.38s | AbstractInterpretationWf.vo | 0m53.72s || +0m00.66s | +1.22% 0m44.40s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m44.48s || -0m00.07s | -0.17% 0m43.51s | LanguageInversion.vo | 0m42.77s || +0m00.73s | +1.73% 0m41.61s | UnderLetsProofs.vo | 0m41.02s || +0m00.58s | +1.43% 0m39.63s | p521_64.c | 0m39.86s || -0m00.22s | -0.57% 0m36.21s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.25s || -0m00.03s | -0.11% 0m32.80s | AbstractInterpretationZRangeProofs.vo | 0m33.19s || -0m00.39s | -1.17% 0m30.94s | ExtractionHaskell/saturated_solinas | 0m30.24s || +0m00.70s | +2.31% 0m29.79s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m30.53s || -0m00.74s | -2.42% 0m29.47s | LanguageWf.vo | 0m29.89s || -0m00.42s | -1.40% 0m26.82s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.79s || +0m00.03s | +0.11% 0m25.66s | RewriterWf1.vo | 0m25.60s || +0m00.05s | +0.23% 0m22.53s | ExtractionOCaml/word_by_word_montgomery | 0m22.10s || +0m00.42s | +1.94% 0m19.93s | secp256k1_32.c | 0m19.65s || +0m00.28s | +1.42% 0m19.36s | p256_32.c | 0m19.96s || -0m00.60s | -3.00% 0m16.44s | CStringification.vo | 0m16.20s || +0m00.24s | +1.48% 0m16.13s | p434_64.c | 0m15.73s || +0m00.39s | +2.54% 0m13.93s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.21s || +0m00.71s | +5.45% 0m12.76s | GENERATEDIdentifiersWithoutTypes.vo | 0m12.35s || +0m00.41s | +3.31% 0m09.96s | ExtractionOCaml/saturated_solinas | 0m10.05s || -0m00.08s | -0.89% 0m09.08s | p224_32.c | 0m08.38s || +0m00.69s | +8.35% 0m08.38s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.55s || -0m00.16s | -1.98% 0m07.65s | p384_64.c | 0m08.54s || -0m00.88s | -10.42% 0m06.72s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.69s || +0m00.02s | +0.44% 0m06.64s | BoundsPipeline.vo | 0m06.58s || +0m00.05s | +0.91% 0m06.58s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.48s || +0m00.09s | +1.54% 0m06.50s | ExtractionOCaml/saturated_solinas.ml | 0m07.02s || -0m00.51s | -7.40% 0m05.84s | Fancy/Prod.vo | 0m05.75s || +0m00.08s | +1.56% 0m04.96s | ExtractionHaskell/saturated_solinas.hs | 0m05.78s || -0m00.82s | -14.18% 0m03.50s | PushButtonSynthesis/Primitives.vo | 0m03.35s || +0m00.14s | +4.47% 0m03.41s | PushButtonSynthesis/SmallExamples.vo | 0m03.29s || +0m00.12s | +3.64% 0m03.19s | PushButtonSynthesis/BarrettReduction.vo | 0m03.26s || -0m00.06s | -2.14% 0m03.18s | curve25519_32.c | 0m02.47s || +0m00.71s | +28.74% 0m03.14s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.25s || -0m00.10s | -3.38% 0m02.86s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.73s || +0m00.12s | +4.76% 0m02.85s | MiscCompilerPassesProofs.vo | 0m03.76s || -0m00.90s | -24.20% 0m02.15s | curve25519_64.c | 0m02.16s || -0m00.01s | -0.46% 0m01.59s | secp256k1_64.c | 0m01.68s || -0m00.08s | -5.35% 0m01.36s | Language.vo | 0m01.25s || +0m00.11s | +8.80% 0m01.35s | CLI.vo | 0m01.35s || +0m00.00s | +0.00% 0m01.29s | p224_64.c | 0m01.59s || -0m00.30s | -18.86% 0m01.29s | p256_64.c | 0m01.33s || -0m00.04s | -3.00% 0m01.25s | CompilersTestCases.vo | 0m01.55s || -0m00.30s | -19.35% 0m01.22s | AbstractInterpretation.vo | 0m01.28s || -0m00.06s | -4.68% 0m01.12s | StandaloneHaskellMain.vo | 0m01.14s || -0m00.01s | -1.75% 0m01.12s | StandaloneOCamlMain.vo | 0m01.10s || +0m00.02s | +1.81% 0m01.01s | RewriterProofs.vo | 0m01.14s || -0m00.12s | -11.40% 0m00.74s | MiscCompilerPasses.vo | 0m00.68s || +0m00.05s | +8.82% 0m00.70s | PushButtonSynthesis/ReificationCache.vo | 0m00.50s || +0m00.19s | +39.99% 0m00.69s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.64s || +0m00.04s | +7.81% 0m00.49s | UnderLets.vo | 0m00.51s || -0m00.02s | -3.92% --- src/AbstractInterpretation.v | 5 +++-- src/CStringification.v | 4 ++++ src/GENERATEDIdentifiersWithoutTypes.v | 32 ++++++++++++++++++++++++++++++ src/Language.v | 36 ++++++++++++++++++++++------------ 4 files changed, 62 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v index 808128025..ca0cb68bd 100644 --- a/src/AbstractInterpretation.v +++ b/src/AbstractInterpretation.v @@ -520,8 +520,8 @@ Module Compilers. n | None => ZRange.type.base.option.None end - | ident.eager_nat_rect_arrow _ _ | ident.nat_rect_arrow _ _ + | ident.eager_nat_rect_arrow _ _ => fun O_case S_case n v => match n with | Some n @@ -533,8 +533,8 @@ Module Compilers. v | None => ZRange.type.base.option.None end - | ident.eager_list_rect _ _ | ident.list_rect _ _ + | ident.eager_list_rect _ _ => fun N C ls => match ls with | Some ls @@ -545,6 +545,7 @@ Module Compilers. ls | None => ZRange.type.base.option.None end + | ident.list_rect_arrow _ _ _ | ident.eager_list_rect_arrow _ _ _ => fun N C ls v => match ls with diff --git a/src/CStringification.v b/src/CStringification.v index 3560a5f82..ff455130b 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -253,6 +253,8 @@ Module Compilers. => fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None) | ident.eager_list_rect A P => fun args => (show_application with_casts (fun _ => "eager_list_rect") args, ZRange.type.base.option.None) + | ident.list_rect_arrow A P Q + => fun args => (show_application with_casts (fun _ => "list_rect(→)") args, ZRange.type.base.option.None) | ident.eager_list_rect_arrow A P Q => fun args => (show_application with_casts (fun _ => "eager_list_rect(→)") args, ZRange.type.base.option.None) | ident.list_case A P @@ -394,6 +396,7 @@ Module Compilers. | ident.eager_nat_rect_arrow P Q => "eager_nat_rect(→)" | ident.list_rect A P => "list_rect" | ident.eager_list_rect A P => "eager_list_rect" + | ident.list_rect_arrow A P Q => "list_rect(→)" | ident.eager_list_rect_arrow A P Q => "eager_list_rect(→)" | ident.list_case A P => "list_case" | ident.List_length T => "length" @@ -1300,6 +1303,7 @@ Module Compilers. | ident.option_rect _ _ | ident.list_rect _ _ | ident.eager_list_rect _ _ + | ident.list_rect_arrow _ _ _ | ident.eager_list_rect_arrow _ _ _ | ident.list_case _ _ | ident.List_length _ diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index c250253e1..db84a33a3 100644 --- a/src/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -276,6 +276,21 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (fun x : Compilers.base.type => type.base x) (Compilers.base.type.list A) -> (fun x : Compilers.base.type => type.base x) P)%ptype + | list_rect_arrow : forall A P Q : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + ((fun x : Compilers.base.type => type.base x) A -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.list A) -> + ((fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.list A) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q)%ptype | eager_list_rect : forall A P : Compilers.base.type, ident (((fun x : Compilers.base.type => type.base x) @@ -865,6 +880,7 @@ show_match_ident = r"""match # with | ident.eager_nat_rect P => | ident.eager_nat_rect_arrow P Q => | ident.list_rect A P => + | ident.list_rect_arrow A P Q => | ident.eager_list_rect A P => | ident.eager_list_rect_arrow A P Q => | ident.list_case A P => @@ -1475,6 +1491,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect | eager_nat_rect_arrow | list_rect + | list_rect_arrow | eager_list_rect | eager_list_rect_arrow | list_case @@ -1569,6 +1586,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => Compilers.base.type | eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type | list_rect => Compilers.base.type * Compilers.base.type + | list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type | eager_list_rect => Compilers.base.type * Compilers.base.type | eager_list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type | list_case => Compilers.base.type * Compilers.base.type @@ -1664,6 +1682,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => false | eager_nat_rect_arrow => false | list_rect => false + | list_rect_arrow => false | eager_list_rect => false | eager_list_rect_arrow => false | list_case => false @@ -1759,6 +1778,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect, Compilers.ident.eager_nat_rect P => Datatypes.Some P | eager_nat_rect_arrow, Compilers.ident.eager_nat_rect_arrow P Q => Datatypes.Some (P, Q) | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P) + | list_rect_arrow, Compilers.ident.list_rect_arrow A P Q => Datatypes.Some (A, P, Q) | eager_list_rect, Compilers.ident.eager_list_rect A P => Datatypes.Some (A, P) | eager_list_rect_arrow, Compilers.ident.eager_list_rect_arrow A P Q => Datatypes.Some (A, P, Q) | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P) @@ -1850,6 +1870,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect, _ | eager_nat_rect_arrow, _ | list_rect, _ + | list_rect_arrow, _ | eager_list_rect, _ | eager_list_rect_arrow, _ | list_case, _ @@ -1946,6 +1967,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype | eager_nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype | list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype + | list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype | eager_list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype | eager_list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype | list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype @@ -2041,6 +2063,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => fun P => @Compilers.ident.eager_nat_rect P | eager_nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_nat_rect_arrow arg') with (P, Q) => @Compilers.ident.eager_nat_rect_arrow P Q end | list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end + | list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.list_rect_arrow A P Q end | eager_list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_list_rect arg') with (A, P) => @Compilers.ident.eager_list_rect A P end | eager_list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of eager_list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.eager_list_rect_arrow A P Q end | list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end @@ -2143,6 +2166,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => f _ (@Compilers.ident.eager_nat_rect P) | Compilers.ident.eager_nat_rect_arrow P Q => f _ (@Compilers.ident.eager_nat_rect_arrow P Q) | Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P) + | Compilers.ident.list_rect_arrow A P Q => f _ (@Compilers.ident.list_rect_arrow A P Q) | Compilers.ident.eager_list_rect A P => f _ (@Compilers.ident.eager_list_rect A P) | Compilers.ident.eager_list_rect_arrow A P Q => f _ (@Compilers.ident.eager_list_rect_arrow A P Q) | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P) @@ -2237,6 +2261,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype | eager_nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype | list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype + | list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype | eager_list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype | eager_list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype | list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype @@ -2331,6 +2356,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => Raw.ident.eager_nat_rect | @eager_nat_rect_arrow P Q => Raw.ident.eager_nat_rect_arrow | @list_rect A P => Raw.ident.list_rect + | @list_rect_arrow A P Q => Raw.ident.list_rect_arrow | @eager_list_rect A P => Raw.ident.eager_list_rect | @eager_list_rect_arrow A P Q => Raw.ident.eager_list_rect_arrow | @list_case A P => Raw.ident.list_case @@ -2426,6 +2452,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => [] | @eager_nat_rect_arrow P Q => [] | @list_rect A P => [] + | @list_rect_arrow A P Q => [] | @eager_list_rect A P => [] | @eager_list_rect_arrow A P Q => [] | @list_case A P => [] @@ -2521,6 +2548,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => fun _ => @Compilers.ident.eager_nat_rect _ | @eager_nat_rect_arrow P Q => fun _ => @Compilers.ident.eager_nat_rect_arrow _ _ | @list_rect A P => fun _ => @Compilers.ident.list_rect _ _ + | @list_rect_arrow A P Q => fun _ => @Compilers.ident.list_rect_arrow _ _ _ | @eager_list_rect A P => fun _ => @Compilers.ident.eager_list_rect _ _ | @eager_list_rect_arrow A P Q => fun _ => @Compilers.ident.eager_list_rect_arrow _ _ _ | @list_case A P => fun _ => @Compilers.ident.list_case _ _ @@ -2620,6 +2648,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P, Compilers.ident.eager_nat_rect P' => Datatypes.Some tt | @eager_nat_rect_arrow P Q, Compilers.ident.eager_nat_rect_arrow P' Q' => Datatypes.Some tt | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt + | @list_rect_arrow A P Q, Compilers.ident.list_rect_arrow A' P' Q' => Datatypes.Some tt | @eager_list_rect A P, Compilers.ident.eager_list_rect A' P' => Datatypes.Some tt | @eager_list_rect_arrow A P Q, Compilers.ident.eager_list_rect_arrow A' P' Q' => Datatypes.Some tt | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt @@ -2711,6 +2740,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect _, _ | @eager_nat_rect_arrow _ _, _ | @list_rect _ _, _ + | @list_rect_arrow _ _ _, _ | @eager_list_rect _ _, _ | @eager_list_rect_arrow _ _ _, _ | @list_case _ _, _ @@ -2807,6 +2837,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => @eager_nat_rect (base.relax P) | Compilers.ident.eager_nat_rect_arrow P Q => @eager_nat_rect_arrow (base.relax P) (base.relax Q) | Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P) + | Compilers.ident.list_rect_arrow A P Q => @list_rect_arrow (base.relax A) (base.relax P) (base.relax Q) | Compilers.ident.eager_list_rect A P => @eager_list_rect (base.relax A) (base.relax P) | Compilers.ident.eager_list_rect_arrow A P Q => @eager_list_rect_arrow (base.relax A) (base.relax P) (base.relax Q) | Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P) @@ -2902,6 +2933,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => tt | Compilers.ident.eager_nat_rect_arrow P Q => tt | Compilers.ident.list_rect A P => tt + | Compilers.ident.list_rect_arrow A P Q => tt | Compilers.ident.eager_list_rect A P => tt | Compilers.ident.eager_list_rect_arrow A P Q => tt | Compilers.ident.list_case A P => tt diff --git a/src/Language.v b/src/Language.v index 695073248..74c34b2f2 100644 --- a/src/Language.v +++ b/src/Language.v @@ -880,6 +880,7 @@ Module Compilers. | eager_nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P) | eager_nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q) | list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P) + | list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q) | eager_list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P) | eager_list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q) | list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P) @@ -1058,17 +1059,15 @@ Module Compilers. | bool_rect T => fun t f => Datatypes.bool_rect _ (t tt) (f tt) | nat_rect P - => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case - | nat_rect_arrow P Q - => fun O_case S_case => Datatypes.nat_rect _ O_case S_case | eager_nat_rect P => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case + | nat_rect_arrow P Q | eager_nat_rect_arrow P Q => fun O_case S_case => Datatypes.nat_rect _ O_case S_case | list_rect A P - => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case | eager_list_rect A P => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case + | list_rect_arrow A P Q | eager_list_rect_arrow A P Q => fun N_case C_case => Datatypes.list_rect _ N_case C_case | list_case A P @@ -1294,13 +1293,13 @@ Module Compilers. end | @Datatypes.nat_rect ?T0 => lazymatch (eval cbv beta in T0) with - | (fun _ => ?P -> ?Q) - => let rP := base.reify P in - let rQ := base.reify Q in - then_tac (@ident.nat_rect_arrow rP rQ) + | (fun _ => ?P -> ?Q) + => let rP := base.reify P in + let rQ := base.reify Q in + then_tac (@ident.nat_rect_arrow rP rQ) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.nat_rect T') - end + end | @Thunked.nat_rect ?T => let rT := base.reify T in then_tac (@ident.nat_rect rT) @@ -1325,10 +1324,21 @@ Module Compilers. then_tac (@ident.eager_nat_rect rT) | @Datatypes.list_rect ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) - | T0 => else_tac () - | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil) - end + | fun _ => _ -> _ => else_tac () + | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) + | T0 => else_tac () + | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil) + end + | @Datatypes.list_rect ?A ?T0 + => lazymatch (eval cbv beta in T0) with + | (fun _ => ?P -> ?Q) + => let rA := base.reify A in + let rP := base.reify P in + let rQ := base.reify Q in + then_tac (@ident.list_rect_arrow rA rP rQ) + | T0 => else_tac () + | ?T' => reify_rec (@Datatypes.list_rect A T') + end | @Thunked.list_rect ?A ?T => let rA := base.reify A in let rT := base.reify T in -- cgit v1.2.3