From 9ca306da300edd075f990ccaa3753ef5e3b59533 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Mar 2019 17:36:26 -0500 Subject: Add a couple more identifiers to support eager rec This will allow us to write rewrite rules that eagerly evaluate recursion principles on the RHS. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 35m52.89s | Total | 35m21.19s || +0m31.69s | +1.49% ----------------------------------------------------------------------------------------------------------- 1m03.44s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m52.51s || +0m10.92s | +20.81% 0m42.76s | UnderLetsProofs.vo | 0m37.59s || +0m05.16s | +13.75% 1m50.02s | RewriterRulesInterpGood.vo | 1m46.65s || +0m03.37s | +3.15% 3m14.40s | p384_32.c | 3m16.54s || -0m02.13s | -1.08% 1m53.47s | RewriterRulesGood.vo | 1m56.16s || -0m02.68s | -2.31% 0m34.80s | AbstractInterpretationZRangeProofs.vo | 0m32.33s || +0m02.46s | +7.63% 0m22.80s | ExtractionOCaml/word_by_word_montgomery | 0m20.53s || +0m02.26s | +11.05% 2m55.61s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m53.77s || +0m01.84s | +1.05% 2m37.56s | Fancy/Compiler.vo | 2m39.51s || -0m01.94s | -1.22% 1m47.71s | Fancy/Barrett256.vo | 1m46.42s || +0m01.29s | +1.21% 0m59.28s | ExtractionHaskell/word_by_word_montgomery | 0m57.33s || +0m01.95s | +3.40% 0m42.71s | LanguageInversion.vo | 0m40.75s || +0m01.96s | +4.80% 0m40.95s | ExtractionHaskell/unsaturated_solinas | 0m39.76s || +0m01.19s | +2.99% 0m32.88s | AbstractInterpretationProofs.vo | 0m31.38s || +0m01.50s | +4.78% 0m28.98s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m27.08s || +0m01.90s | +7.01% 0m17.39s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m18.95s || -0m01.55s | -8.23% 0m12.51s | GENERATEDIdentifiersWithoutTypes.vo | 0m11.11s || +0m01.40s | +12.60% 0m12.30s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.84s || -0m01.53s | -11.12% 0m07.16s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.67s || +0m01.49s | +26.27% 0m05.84s | ExtractionHaskell/saturated_solinas.hs | 0m04.84s || +0m01.00s | +20.66% 2m01.25s | RewriterWf2.vo | 2m01.06s || +0m00.18s | +0.15% 1m22.67s | Rewriter.vo | 1m22.48s || +0m00.18s | +0.23% 0m54.42s | AbstractInterpretationWf.vo | 0m55.26s || -0m00.83s | -1.52% 0m53.40s | RewriterInterpProofs1.vo | 0m52.85s || +0m00.54s | +1.04% 0m46.26s | p521_32.c | 0m46.58s || -0m00.32s | -0.68% 0m44.94s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m45.20s || -0m00.26s | -0.57% 0m40.17s | p521_64.c | 0m39.49s || +0m00.67s | +1.72% 0m37.93s | Fancy/Montgomery256.vo | 0m37.31s || +0m00.61s | +1.66% 0m36.59s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.22s || +0m00.37s | +1.02% 0m30.06s | ExtractionHaskell/saturated_solinas | 0m29.33s || +0m00.73s | +2.48% 0m29.61s | LanguageWf.vo | 0m29.48s || +0m00.12s | +0.44% 0m26.76s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.77s || -0m00.00s | -0.03% 0m26.23s | SlowPrimeSynthesisExamples.vo | 0m26.36s || -0m00.12s | -0.49% 0m25.30s | RewriterWf1.vo | 0m25.47s || -0m00.16s | -0.66% 0m20.01s | p448_solinas_64.c | 0m19.97s || +0m00.04s | +0.20% 0m19.56s | p256_32.c | 0m20.04s || -0m00.48s | -2.39% 0m19.28s | secp256k1_32.c | 0m18.86s || +0m00.42s | +2.22% 0m16.08s | CStringification.vo | 0m15.70s || +0m00.37s | +2.42% 0m16.04s | p434_64.c | 0m15.20s || +0m00.83s | +5.52% 0m13.39s | ExtractionOCaml/unsaturated_solinas | 0m13.13s || +0m00.25s | +1.98% 0m09.57s | p224_32.c | 0m08.95s || +0m00.62s | +6.92% 0m09.27s | ExtractionOCaml/saturated_solinas | 0m10.22s || -0m00.95s | -9.29% 0m08.70s | p384_64.c | 0m07.93s || +0m00.76s | +9.70% 0m08.43s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.07s || -0m00.64s | -7.05% 0m07.44s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.35s || -0m00.90s | -10.89% 0m06.97s | ExtractionOCaml/saturated_solinas.ml | 0m07.28s || -0m00.31s | -4.25% 0m06.81s | BoundsPipeline.vo | 0m06.78s || +0m00.02s | +0.44% 0m06.72s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m06.85s || -0m00.12s | -1.89% 0m05.77s | Fancy/Prod.vo | 0m06.07s || -0m00.30s | -4.94% 0m04.06s | MiscCompilerPassesProofs.vo | 0m03.84s || +0m00.21s | +5.72% 0m03.71s | PushButtonSynthesis/Primitives.vo | 0m03.34s || +0m00.37s | +11.07% 0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.26s || +0m00.08s | +2.45% 0m03.16s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.06s | -1.86% 0m03.15s | PushButtonSynthesis/BarrettReduction.vo | 0m03.29s || -0m00.14s | -4.25% 0m02.84s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.90s || -0m00.06s | -2.06% 0m02.79s | curve25519_32.c | 0m02.92s || -0m00.12s | -4.45% 0m02.12s | curve25519_64.c | 0m02.13s || -0m00.00s | -0.46% 0m01.70s | secp256k1_64.c | 0m01.55s || +0m00.14s | +9.67% 0m01.64s | p256_64.c | 0m01.23s || +0m00.40s | +33.33% 0m01.57s | p224_64.c | 0m01.68s || -0m00.10s | -6.54% 0m01.36s | Language.vo | 0m01.33s || +0m00.03s | +2.25% 0m01.33s | CLI.vo | 0m01.32s || +0m00.01s | +0.75% 0m01.26s | AbstractInterpretation.vo | 0m01.25s || +0m00.01s | +0.80% 0m01.13s | RewriterProofs.vo | 0m01.18s || -0m00.05s | -4.23% 0m01.13s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.08s | +8.65% 0m01.10s | CompilersTestCases.vo | 0m01.16s || -0m00.05s | -5.17% 0m01.04s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.13s | -11.86% 0m00.76s | MiscCompilerPasses.vo | 0m00.74s || +0m00.02s | +2.70% 0m00.60s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.66s || -0m00.06s | -9.09% 0m00.46s | UnderLets.vo | 0m00.48s || -0m00.01s | -4.16% 0m00.44s | PushButtonSynthesis/ReificationCache.vo | 0m00.52s || -0m00.08s | -15.38% --- src/AbstractInterpretation.v | 15 ++++ src/AbstractInterpretationWf.v | 1 + src/AbstractInterpretationZRangeProofs.v | 13 +++ src/CStringification.v | 16 ++++ src/GENERATEDIdentifiersWithoutTypes.v | 133 ++++++++++++++++++++++++++++++- src/Language.v | 54 +++++++++++++ src/LanguageWf.v | 2 +- 7 files changed, 232 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v index 63a7df1ed..808128025 100644 --- a/src/AbstractInterpretation.v +++ b/src/AbstractInterpretation.v @@ -509,6 +509,7 @@ Module Compilers. | None => ZRange.type.base.option.None end | ident.nat_rect _ + | ident.eager_nat_rect _ => fun O_case S_case n => match n with | Some n @@ -519,6 +520,7 @@ Module Compilers. n | None => ZRange.type.base.option.None end + | ident.eager_nat_rect_arrow _ _ | ident.nat_rect_arrow _ _ => fun O_case S_case n v => match n with @@ -531,6 +533,7 @@ Module Compilers. v | None => ZRange.type.base.option.None end + | ident.eager_list_rect _ _ | ident.list_rect _ _ => fun N C ls => match ls with @@ -542,6 +545,18 @@ Module Compilers. ls | None => ZRange.type.base.option.None end + | ident.eager_list_rect_arrow _ _ _ + => fun N C ls v + => match ls with + | Some ls + => list_rect + _ + N + (fun x xs rec => C x (Some xs) rec) + ls + v + | None => ZRange.type.base.option.None + end | ident.list_case _ _ => fun N C ls => match ls with diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v index a1e2f180e..85eef1cae 100644 --- a/src/AbstractInterpretationWf.v +++ b/src/AbstractInterpretationWf.v @@ -699,6 +699,7 @@ Module Compilers. | solve [ eauto ] | apply NatUtil.nat_rect_Proper_nondep | apply ListUtil.list_rect_Proper + | apply ListUtil.list_rect_arrow_Proper | apply ListUtil.list_case_Proper | apply ListUtil.pointwise_map | apply ListUtil.fold_right_Proper diff --git a/src/AbstractInterpretationZRangeProofs.v b/src/AbstractInterpretationZRangeProofs.v index 81483714f..2ca2ea140 100644 --- a/src/AbstractInterpretationZRangeProofs.v +++ b/src/AbstractInterpretationZRangeProofs.v @@ -354,6 +354,16 @@ Module Compilers. | specialize (IH ls'); generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ]; intros + | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls ?x) (list_rect ?P' ?N' ?C' ?ls' ?y) = true ] + => is_var ls; is_var ls'; is_var x; is_var y; + revert dependent y; try revert dependent x; + let IH := fresh "IH" in + revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *; + [ + | exfalso; discriminate | exfalso; discriminate + | specialize (IH ls'); + generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ]; + intros | [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ] => apply H; clear H @@ -362,6 +372,9 @@ Module Compilers. | [ H : context[ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true] |- ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true ] => apply H + | [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true) + |- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ] + => apply H; clear H end ]. Local Lemma mul_by_halves_bounds x y n : diff --git a/src/CStringification.v b/src/CStringification.v index 9ae80d140..3560a5f82 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -241,12 +241,20 @@ Module Compilers. | ident.bool_rect T => fun '(t, (f, ((b, br), tt))) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 200) ("if " ++ b 200%nat ++ " then " ++ maybe_wrap_cast with_casts t 200%nat ++ " else " ++ maybe_wrap_cast with_casts f 200%nat), ZRange.type.base.option.None) | ident.nat_rect P => fun args => (show_application with_casts (fun _ => "nat_rect") args, ZRange.type.base.option.None) + | ident.eager_nat_rect P + => fun args => (show_application with_casts (fun _ => "eager_nat_rect") args, ZRange.type.base.option.None) + | ident.eager_nat_rect_arrow P Q + => fun args => (show_application with_casts (fun _ => "eager_nat_rect(→)") args, ZRange.type.base.option.None) | ident.nat_rect_arrow P Q => fun args => (show_application with_casts (fun _ => "nat_rect(→)") args, ZRange.type.base.option.None) | ident.option_rect A P => fun args => (show_application with_casts (fun _ => "option_rect") args, ZRange.type.base.option.None) | ident.list_rect A P => 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.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 => fun args => (show_application with_casts (fun _ => "list_case") args, ZRange.type.base.option.None) | ident.List_length T @@ -381,8 +389,12 @@ Module Compilers. | ident.prod_rect A B T => "prod_rect" | ident.bool_rect T => "bool_rect" | ident.nat_rect P => "nat_rect" + | ident.eager_nat_rect P => "eager_nat_rect" | ident.nat_rect_arrow P Q => "nat_rect(→)" + | 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.eager_list_rect_arrow A P Q => "eager_list_rect(→)" | ident.list_case A P => "list_case" | ident.List_length T => "length" | ident.List_seq => "seq" @@ -1280,11 +1292,15 @@ Module Compilers. | ident.prod_rect _ _ _ | ident.bool_rect _ | ident.nat_rect _ + | ident.eager_nat_rect _ | ident.nat_rect_arrow _ _ + | ident.eager_nat_rect_arrow _ _ | ident.Some _ | ident.None _ | ident.option_rect _ _ | ident.list_rect _ _ + | ident.eager_list_rect _ _ + | ident.eager_list_rect_arrow _ _ _ | ident.list_case _ _ | ident.List_length _ | ident.List_seq diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index d8a8138a6..c250253e1 100644 --- a/src/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -236,6 +236,34 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (Compilers.base.type.type_base base.type.nat) -> (fun x : Compilers.base.type => type.base x) P -> (fun x : Compilers.base.type => type.base x) Q)%ptype + | eager_nat_rect : forall P : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) + ()%etype -> + (fun x : Compilers.base.type => type.base x) P) -> + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) P) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type => type.base x) P)%ptype + | eager_nat_rect_arrow : forall 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) + (Compilers.base.type.type_base base.type.nat) -> + ((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.type_base base.type.nat) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q)%ptype | list_rect : forall A P : Compilers.base.type, ident (((fun x : Compilers.base.type => type.base x) ()%etype -> @@ -248,6 +276,41 @@ 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 + | eager_list_rect : forall A P : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) + ()%etype -> + (fun x : Compilers.base.type => type.base x) P) -> + ((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) P) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.list A) -> + (fun x : Compilers.base.type => type.base x) P)%ptype + | eager_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 | list_case : forall A P : Compilers.base.type, ident (((fun x : Compilers.base.type => type.base x) ()%etype -> @@ -799,7 +862,11 @@ show_match_ident = r"""match # with | ident.bool_rect T => | ident.nat_rect P => | ident.nat_rect_arrow P Q => + | ident.eager_nat_rect P => + | ident.eager_nat_rect_arrow P Q => | ident.list_rect A P => + | ident.eager_list_rect A P => + | ident.eager_list_rect_arrow A P Q => | ident.list_case A P => | ident.List_length T => | ident.List_seq => @@ -876,7 +943,7 @@ remake = False if remake: assert(os.path.exists('/tmp/pr.out')) assert(os.path.exists('/tmp/sm.out')) - with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For.*\n', '', f.read(), flags=re.MULTILINE) + with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For [^ ]*: Argument.*', '', f.read(), flags=re.MULTILINE|re.DOTALL) with open('/tmp/sm.out', 'r') as f: show_match_ident = f.read() prefix = 'Compilers.' @@ -1405,7 +1472,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect | nat_rect | nat_rect_arrow + | eager_nat_rect + | eager_nat_rect_arrow | list_rect + | eager_list_rect + | eager_list_rect_arrow | list_case | List_length | List_seq @@ -1495,7 +1566,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect => Compilers.base.type | nat_rect => Compilers.base.type | nat_rect_arrow => Compilers.base.type * Compilers.base.type + | eager_nat_rect => Compilers.base.type + | eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type | list_rect => 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 | List_length => Compilers.base.type | List_seq => unit @@ -1586,7 +1661,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect => false | nat_rect => false | nat_rect_arrow => false + | eager_nat_rect => false + | eager_nat_rect_arrow => false | list_rect => false + | eager_list_rect => false + | eager_list_rect_arrow => false | list_case => false | List_length => false | List_seq => true @@ -1677,7 +1756,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect, Compilers.ident.bool_rect T => Datatypes.Some T | nat_rect, Compilers.ident.nat_rect P => Datatypes.Some P | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Datatypes.Some (P, Q) + | 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) + | 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) | List_length, Compilers.ident.List_length T => Datatypes.Some T | List_seq, Compilers.ident.List_seq => Datatypes.Some tt @@ -1764,7 +1847,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect, _ | nat_rect, _ | nat_rect_arrow, _ + | eager_nat_rect, _ + | eager_nat_rect_arrow, _ | list_rect, _ + | eager_list_rect, _ + | eager_list_rect_arrow, _ | list_case, _ | List_length, _ | List_seq, _ @@ -1856,7 +1943,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect => fun T => ((type.base ()%etype -> type.base T) -> (type.base ()%etype -> type.base T) -> type.base (Compilers.base.type.type_base base.type.bool) -> type.base T)%ptype | 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 | 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 + | 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 + | 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 | List_length => fun T => (type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype | List_seq => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list (Compilers.base.type.type_base base.type.nat)))%ptype @@ -1947,7 +2038,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect => fun T => @Compilers.ident.bool_rect T | nat_rect => fun P => @Compilers.ident.nat_rect P | nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of nat_rect_arrow arg') with (P, Q) => @Compilers.ident.nat_rect_arrow P Q end + | 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 + | 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 | List_length => fun T => @Compilers.ident.List_length T | List_seq => fun _ => @Compilers.ident.List_seq @@ -2045,7 +2140,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.bool_rect T => f _ (@Compilers.ident.bool_rect T) | Compilers.ident.nat_rect P => f _ (@Compilers.ident.nat_rect P) | Compilers.ident.nat_rect_arrow P Q => f _ (@Compilers.ident.nat_rect_arrow P Q) + | 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.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) | Compilers.ident.List_length T => f _ (@Compilers.ident.List_length T) | Compilers.ident.List_seq => f _ Compilers.ident.List_seq @@ -2135,7 +2234,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | bool_rect {T : base.type} : ident ((type.base ()%pbtype -> type.base T) -> (type.base ()%pbtype -> type.base T) -> type.base (base.type.type_base base.type.bool) -> type.base T)%ptype | 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 | 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 + | 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 + | 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 | List_length {T : base.type} : ident (type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat))%ptype | List_seq : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list (base.type.type_base base.type.nat)))%ptype @@ -2225,7 +2328,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @bool_rect T => Raw.ident.bool_rect | @nat_rect P => Raw.ident.nat_rect | @nat_rect_arrow P Q => Raw.ident.nat_rect_arrow + | @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 + | @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 | @List_length T => Raw.ident.List_length | @List_seq => Raw.ident.List_seq @@ -2316,7 +2423,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @bool_rect T => [] | @nat_rect P => [] | @nat_rect_arrow P Q => [] + | @eager_nat_rect P => [] + | @eager_nat_rect_arrow P Q => [] | @list_rect A P => [] + | @eager_list_rect A P => [] + | @eager_list_rect_arrow A P Q => [] | @list_case A P => [] | @List_length T => [] | @List_seq => [] @@ -2407,7 +2518,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @bool_rect T => fun _ => @Compilers.ident.bool_rect _ | @nat_rect P => fun _ => @Compilers.ident.nat_rect _ | @nat_rect_arrow P Q => fun _ => @Compilers.ident.nat_rect_arrow _ _ + | @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 _ _ + | @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 _ _ | @List_length T => fun _ => @Compilers.ident.List_length _ | @List_seq => fun _ => @Compilers.ident.List_seq @@ -2502,7 +2617,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @bool_rect T, Compilers.ident.bool_rect T' => Datatypes.Some tt | @nat_rect P, Compilers.ident.nat_rect P' => Datatypes.Some tt | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Datatypes.Some tt + | @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 + | @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 | @List_length T, Compilers.ident.List_length T' => Datatypes.Some tt | @List_seq, Compilers.ident.List_seq => Datatypes.Some tt @@ -2589,7 +2708,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @bool_rect _, _ | @nat_rect _, _ | @nat_rect_arrow _ _, _ + | @eager_nat_rect _, _ + | @eager_nat_rect_arrow _ _, _ | @list_rect _ _, _ + | @eager_list_rect _ _, _ + | @eager_list_rect_arrow _ _ _, _ | @list_case _ _, _ | @List_length _, _ | @List_seq, _ @@ -2681,7 +2804,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.bool_rect T => @bool_rect (base.relax T) | Compilers.ident.nat_rect P => @nat_rect (base.relax P) | Compilers.ident.nat_rect_arrow P Q => @nat_rect_arrow (base.relax P) (base.relax Q) + | 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.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) | Compilers.ident.List_length T => @List_length (base.relax T) | Compilers.ident.List_seq => @List_seq @@ -2772,7 +2899,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.bool_rect T => tt | Compilers.ident.nat_rect P => tt | Compilers.ident.nat_rect_arrow P Q => tt + | 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.eager_list_rect A P => tt + | Compilers.ident.eager_list_rect_arrow A P Q => tt | Compilers.ident.list_case A P => tt | Compilers.ident.List_length T => tt | Compilers.ident.List_seq => tt diff --git a/src/Language.v b/src/Language.v index 52c340d18..695073248 100644 --- a/src/Language.v +++ b/src/Language.v @@ -877,7 +877,11 @@ Module Compilers. | bool_rect {T:base.type} : ident ((unit -> T) -> (unit -> T) -> bool -> T) | nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P) | nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q) + | 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) + | 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) | List_length {T} : ident (list T -> nat) | List_seq : ident (nat -> nat -> list nat) @@ -1057,8 +1061,16 @@ Module Compilers. => 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 + | 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 + | eager_list_rect_arrow A P Q + => fun N_case C_case => Datatypes.list_rect _ N_case C_case | list_case A P => fun N_case C_case => ListUtil.list_case _ (N_case tt) C_case | List_length T => @List.length _ @@ -1149,6 +1161,7 @@ Module Compilers. Notation LiteralNat := (@Literal base.type.nat). Notation LiteralZRange := (@Literal base.type.zrange). Definition literal {T} (v : T) := v. + Definition eagerly {T} (v : T) := v. (** TODO: MOVE ME? *) Module Thunked. @@ -1291,6 +1304,25 @@ Module Compilers. | @Thunked.nat_rect ?T => let rT := base.reify T in then_tac (@ident.nat_rect rT) + | eagerly (@Datatypes.nat_rect) ?T0 ?P0 + => lazymatch (eval cbv beta in T0) with + | fun _ => _ -> _ => else_tac () + | fun _ => ?T => reify_rec (eagerly (@Thunked.nat_rect) T (fun _ : Datatypes.unit => P0)) + | T0 => else_tac () + | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T' P0) + end + | eagerly (@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.eager_nat_rect_arrow rP rQ) + | T0 => else_tac () + | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T') + end + | eagerly (@Thunked.nat_rect) ?T + => let rT := base.reify T in + 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)) @@ -1301,6 +1333,27 @@ Module Compilers. => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.list_rect rA rT) + | eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil + => lazymatch (eval cbv beta in T0) with + | fun _ => _ -> _ => else_tac () + | fun _ => ?T => reify_rec (eagerly (@Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil)) + | T0 => else_tac () + | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T' Pnil) + end + | eagerly (@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.eager_list_rect_arrow rA rP rQ) + | T0 => else_tac () + | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T') + end + | eagerly (@Thunked.list_rect) ?A ?T + => let rA := base.reify A in + let rT := base.reify T in + then_tac (@ident.eager_list_rect rA rT) | @ListUtil.list_case ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with | fun _ => ?T => reify_rec (@Thunked.list_case A T (fun _ : Datatypes.unit => Pnil)) @@ -1398,6 +1451,7 @@ Module Compilers. => let rA := base.reify A in then_tac (@ident.None rA) | ZRange.Build_zrange => then_tac ident.Build_zrange + | eagerly (?f ?x) => reify_rec (eagerly f x) | fancy.interp ?idc => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in then_tac ridc diff --git a/src/LanguageWf.v b/src/LanguageWf.v index 1119e1977..d1083e43d 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -221,7 +221,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ destruct idc; cbn [type.eqv ident.gen_interp type.interp base.interp base.base_interp]; try solve [ typeclasses eauto | cbv [respectful]; repeat intro; subst; destruct_head_hnf bool; destruct_head_hnf prod; destruct_head_hnf option; destruct_head_hnf zrange; eauto - | cbv [respectful]; repeat intro; (apply nat_rect_Proper_nondep || apply list_rect_Proper || apply list_case_Proper); repeat intro; eauto ]. + | cbv [respectful]; repeat intro; (apply nat_rect_Proper_nondep || apply list_rect_Proper || apply list_case_Proper || apply list_rect_arrow_Proper); repeat intro; eauto ]. Qed. Global Instance eqv_Reflexive_Proper {t} (idc : ident t) : Proper type.eqv (ident.interp idc) | 1. -- cgit v1.2.3