diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-14 20:10:21 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-04-17 14:16:02 -0400 |
commit | 655ead456c31c4bba2a31c8ae4c33c107814648d (patch) | |
tree | 07b96a0ffa9e8c06abccdedb04b7d4181bb916e6 | |
parent | 69646d18cf155b5099c87a796ad47b54a59d1d60 (diff) |
Inline a24_sig in ladderstep
Update the pipeline to be powerful enough to take advantage of this
change by doing more simplification.
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 4 | ||||
-rw-r--r-- | src/Specific/IntegrationTestLadderstep.v | 30 | ||||
-rw-r--r-- | src/Specific/IntegrationTestLadderstep130.v | 32 |
3 files changed, 34 insertions, 32 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 53296cc13..e9355e5ee 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -76,7 +76,9 @@ Definition PostWfPipeline : option (@ProcessedReflectivePackage round_up) := Build_ProcessedReflectivePackage_from_option_sigma e input_bounds - (let e := ANormal e in + (let e := InlineConst e in + let e := SimplifyArith e in + let e := ANormal e in let e := InlineConst e in let e := MapCast _ e input_bounds in option_map diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v index d810c8078..3e944b7c6 100644 --- a/src/Specific/IntegrationTestLadderstep.v +++ b/src/Specific/IntegrationTestLadderstep.v @@ -67,27 +67,27 @@ Section BoundedField25p5. (* TODO : change this to field once field isomorphism happens *) Definition xzladderstep : - { xzladderstep : feW -> feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) - | forall a24 x1 Q Q', - let xz := xzladderstep a24 x1 Q Q' in - feW_bounded a24 - -> feW_bounded x1 + { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) + | forall x1 Q Q', + let xz := xzladderstep x1 Q Q' in + let eval := B.Positional.Fdecode wt in + feW_bounded x1 -> feW_bounded (fst Q) /\ feW_bounded (snd Q) -> feW_bounded (fst Q') /\ feW_bounded (snd Q') -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz))) /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) - /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. + /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. lazymatch goal with - | [ |- { op | forall (a:?A) (b:?B) (c:?C) (d:?D), - let v := op a b c d in - @?P a b c d v } ] - => refine (@lift4_sig A B C D _ P _) + | [ |- { op | forall (a:?A) (b:?B) (c:?C), + let v := op a b c in + @?P a b c v } ] + => refine (@lift3_sig A B C _ P _) end. - intros a b c d; cbv beta iota zeta. + intros a b c; cbv beta iota zeta. lazymatch goal with - | [ |- { e | ?A -> ?B -> ?C -> ?D -> @?E e } ] - => refine (proj2_sig_map (P:=fun e => A -> B -> C -> D -> (_:Prop)) _ _) + | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] + => refine (proj2_sig_map (P:=fun e => A -> B -> C -> (_:Prop)) _ _) end. { intros ? FINAL. repeat let H := fresh in intro H; specialize (FINAL H). @@ -101,8 +101,8 @@ Section BoundedField25p5. rewrite <- (proj2_sig Mxzladderstep_sig). apply f_equal. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. - context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _). - cbv [M.xzladderstep]. + context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). + cbv [M.xzladderstep a24_sig]. do 4 lazymatch goal with | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] => context_to_dlet_in_rhs (@proj1_sig a b f_sig) diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index 74b2ce674..c8e3ba2b8 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -66,27 +66,27 @@ Section BoundedField25p5. (* TODO : change this to field once field isomorphism happens *) Definition xzladderstep : - { xzladderstep : feW -> feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) - | forall a24 x1 Q Q', - let xz := xzladderstep a24 x1 Q Q' in - feW_bounded a24 - -> feW_bounded x1 + { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) + | forall x1 Q Q', + let xz := xzladderstep x1 Q Q' in + let eval := B.Positional.Fdecode wt in + feW_bounded x1 -> feW_bounded (fst Q) /\ feW_bounded (snd Q) -> feW_bounded (fst Q') /\ feW_bounded (snd Q') -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz))) /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) - /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. + /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. lazymatch goal with - | [ |- { op | forall (a:?A) (b:?B) (c:?C) (d:?D), - let v := op a b c d in - @?P a b c d v } ] - => refine (@lift4_sig A B C D _ P _) + | [ |- { op | forall (a:?A) (b:?B) (c:?C), + let v := op a b c in + @?P a b c v } ] + => refine (@lift3_sig A B C _ P _) end. - intros a b c d; cbv beta iota zeta. + intros a b c; cbv beta iota zeta. lazymatch goal with - | [ |- { e | ?A -> ?B -> ?C -> ?D -> @?E e } ] - => refine (proj2_sig_map (P:=fun e => A -> B -> C -> D -> (_:Prop)) _ _) + | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] + => refine (proj2_sig_map (P:=fun e => A -> B -> C -> (_:Prop)) _ _) end. { intros ? FINAL. repeat let H := fresh in intro H; specialize (FINAL H). @@ -100,8 +100,8 @@ Section BoundedField25p5. rewrite <- (proj2_sig Mxzladderstep_sig). apply f_equal. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. - context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _). - cbv [M.xzladderstep]. + context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). + cbv [M.xzladderstep a24_sig]. do 4 lazymatch goal with | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] => context_to_dlet_in_rhs (@proj1_sig a b f_sig) @@ -110,8 +110,8 @@ Section BoundedField25p5. refine (proj2 FINAL). } subst feW feW_bounded; cbv beta. (* jgross start here! *) - (* Set Ltac Profiling. + (* Time Glue.refine_to_reflective_glue (128::256::nil)%nat%list. Time ReflectiveTactics.refine_with_pipeline_correct. { Time ReflectiveTactics.do_reify. } |