diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 532 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 215 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf2.v | 2 |
4 files changed, 728 insertions, 22 deletions
diff --git a/_CoqProject b/_CoqProject index 70fca8fd2..0b4816189 100644 --- a/_CoqProject +++ b/_CoqProject @@ -264,6 +264,7 @@ src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/RewriterRulesGood.v +src/Experiments/NewPipeline/RewriterRulesInterpGood.v src/Experiments/NewPipeline/RewriterWf1.v src/Experiments/NewPipeline/RewriterWf2.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v new file mode 100644 index 000000000..7647b1f06 --- /dev/null +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -0,0 +1,532 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Coq.Classes.Morphisms. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.FSets.FMapPositive. +Require Import Crypto.Experiments.NewPipeline.Language. +Require Import Crypto.Experiments.NewPipeline.LanguageInversion. +Require Import Crypto.Experiments.NewPipeline.LanguageWf. +Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. +Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Experiments.NewPipeline.Rewriter. +Require Import Crypto.Experiments.NewPipeline.RewriterWf1. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.ZSimplify. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.AddGetCarry. +Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.ForallIn. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Decidable. +Import ListNotations. Local Open Scope list_scope. +Local Open Scope Z_scope. + +Import EqNotations. +Module Compilers. + Import Language.Compilers. + Import LanguageInversion.Compilers. + Import LanguageWf.Compilers. + Import UnderLetsProofs.Compilers. + Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. + Import Rewriter.Compilers. + Import RewriterWf1.Compilers. + Import expr.Notations. + Import RewriterWf1.Compilers.RewriteRules. + Import defaults. + + Module Import RewriteRules. + Import Rewriter.Compilers.RewriteRules. + + Local Lemma rlist_rect_eq {var A P ivar} Pnil Pcons ls + : @rlist_rect var A P ivar Pnil Pcons ls + = match invert_expr.reflect_list ls with + | Some ls + => Some (list_rect + (fun _ => _) + Pnil + (fun x xs rec => rec' <-- rec; Pcons x xs rec') + ls)%under_lets + | None => None + end. + Proof. cbv [rlist_rect Compile.option_bind' Option.bind]; reflexivity. Qed. + + Local Lemma UnderLets_interp_list_rect {A P} Pnil Pcons ls + : UnderLets.interp + (@ident.interp) + (list_rect + (fun _ : list A => UnderLets.UnderLets base.type ident _ P) + Pnil + (fun x xs rec => rec' <-- rec; Pcons x xs rec') + ls)%under_lets + = list_rect + (fun _ => P) + (UnderLets.interp (@ident.interp) Pnil) + (fun x xs rec => UnderLets.interp (@ident.interp) (Pcons x xs rec)) + ls. + Proof. + induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ]. + rewrite UnderLets.interp_splice, IHxs; reflexivity. + Qed. + + Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident.interp)). + + Local Ltac do_cbv0 := + cbv [id + Compile.rewrite_rules_interp_goodT + Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related]. + Local Ltac do_cbv := + do_cbv0; + cbv [List.map List.fold_right List.rev list_rect orb List.app]. + + Local Ltac start_interp_good := + do_cbv; + lazymatch goal with + | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ] + => let Q' := fresh in + pose Q as Q'; + change (forall x p, In (@existT A P x p) ls -> Q' x p); + apply (@forall_In_existT A P Q' ls); cbn [projT1 projT2]; cbv [id]; + subst Q'; cbn [projT1 projT2] + end; + do_cbv0; + repeat first [ progress intros + | match goal with + | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) + | [ |- True /\ _ ] => split; [ exact I | ] + end + | progress cbn [eq_rect] in * ]; + cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.interp ident.gen_interp] in *. + + Local Ltac interp_good_t_step := + first [ reflexivity + | match goal with + | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand + | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand + end + | progress cbn [expr.interp ident.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr] in * + | progress cbv [Compile.option_bind' respectful] in * + | progress fold (@type.interp _ base.interp) + | progress fold (@base.interp) + | match goal with + | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat + | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map + | [ |- context[List.map (fun x => x) _] ] => rewrite map_id + | [ |- context[List.map _ (List.rev _)] ] => rewrite map_rev + | [ |- context[List.map _ (firstn _ _)] ] => rewrite <- firstn_map + | [ |- context[List.map _ (skipn _ _)] ] => rewrite <- skipn_map + | [ |- context[List.length (List.map _ _)] ] => rewrite map_length + | [ |- context[List.combine (List.map _ _) _] ] => rewrite combine_map_l + | [ |- context[List.combine _ (List.map _ _)] ] => rewrite combine_map_r + | [ |- context[expr.interp _ (reify_list _)] ] => rewrite interp_reify_list + | [ |- context[expr.interp _ (UnderLets.to_expr ?e)] ] => rewrite UnderLets.interp_to_expr + | [ |- context[UnderLets.interp _ (UnderLets.splice_list _ _)] ] => rewrite UnderLets.interp_splice_list + | [ |- context[rlist_rect] ] => rewrite rlist_rect_eq + | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect + | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice + | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map + | [ |- list_rect _ _ _ _ = List.app ?ls1 ?ls2 ] + => rewrite (eq_app_list_rect ls1 ls2) + | [ |- list_rect _ _ _ _ = @flat_map ?A ?B ?f ?ls ] + => rewrite (@eq_flat_map_list_rect A B f ls) + | [ |- list_rect _ _ _ _ = @partition ?A ?f ?ls ] + => rewrite (@eq_partition_list_rect A f ls) + | [ |- list_rect _ _ _ _ = @List.map ?A ?B ?f ?ls ] + => rewrite (@eq_map_list_rect A B f ls) + | [ |- _ = @fold_right ?A ?B ?f ?v ?ls ] + => rewrite (@eq_fold_right_list_rect A B f v ls) + end + | progress intros + | progress subst + | progress inversion_option + | progress Z.ltb_to_lt + | progress split_andb + | match goal with + | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2 + | [ |- firstn _ _ = firstn _ _ ] => apply f_equal2 + | [ |- skipn _ _ = skipn _ _ ] => apply f_equal2 + | [ |- rev _ = rev _ ] => apply f_equal + | [ |- List.app ?l1 ?l2 = List.app ?l1' ?l2 ] => apply f_equal2 + | [ |- List.app ?l1 ?l2 = List.app ?l1 ?l2' ] => apply f_equal2 + | [ |- cons _ _ = cons _ _ ] => apply f_equal2 + | [ |- list_rect _ ?Pnil ?Pcons ?ls = list_rect _ ?Pnil ?Pcons' ?ls ] + => apply list_rect_Proper; [ reflexivity | repeat intro | reflexivity ] + | [ |- bool_rect _ ?x ?y ?b = bool_rect _ ?x ?y ?b' ] + => apply f_equal3; [ reflexivity | reflexivity | solve [ repeat interp_good_t_step ] ] + | [ H : expr.wf _ ?v1 ?v2 |- expr.interp _ ?v1 = expr.interp _ ?v2 ] + => apply (expr.wf_interp_Proper _ _ _ H ltac:(assumption)) + | [ |- ?R (?f (?g (if ?b then ?x else ?y))) (bool_rect ?A ?B ?C ?D) ] + => rewrite <- (@Bool.pull_bool_if _ _ g b), <- (@Bool.pull_bool_if _ _ f b); + change (R (bool_rect _ (f (g x)) (f (g y)) b) (bool_rect A B C D)) + | [ |- context[invert_expr.reflect_list ?ls] ] + => destruct (invert_expr.reflect_list ls) eqn:?; expr.invert_subst + | [ |- ?f (nth_default _ _ _) = _ ] + => rewrite <- (@map_nth_default_always _ _ f) + | [ |- map ?f ?ls = map ?g ?ls ] => apply map_ext_in + | [ |- List.map _ (update_nth _ _ _) = update_nth _ _ _ ] => apply map_update_nth_ext + | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) + | [ H : forall v : unit, _ |- _ ] => specialize (H tt) + | [ H : _ = expr.interp ?ii ?v |- _ ] => is_var v; generalize dependent (expr.interp ii v); clear v + | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ] + => is_var b; destruct b; cbv [bool_rect] + | [ H : (forall x y, _ -> expr.interp _ (UnderLets.interp _ (?f1 x)) = expr.interp _ (UnderLets.interp _ (?f2 y))) + |- expr.interp _ (UnderLets.interp _ (?f1 ?x1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2)) ] + => apply H + | [ H : (forall x y, _ -> forall x' y', _ -> expr.interp _ (UnderLets.interp _ (?f1 x x')) = expr.interp _ (UnderLets.interp _ (?f2 y y'))) + |- expr.interp _ (UnderLets.interp _ (?f1 ?x1 ?y1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2 ?y2)) ] + => apply H + | [ |- context G[rwhen ?v ?b] ] + => let c := constr:(rwhen v b) in + let c := (eval cbv [rwhen] in c) in + let G' := context G[c] in + change G'; + destruct b eqn:? + | [ |- context G[rwhenl ?v ?b] ] + => let c := constr:(rwhenl v b) in + let c := (eval cbv [rwhenl] in c) in + let G' := context G[c] in + change G'; + destruct b eqn:? + | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H + | [ |- context[expr.interp ?ii ?v] ] + => is_var v; generalize dependent (expr.interp ii v); clear v; intro v + | [ |- context[Z.mul_split ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod + | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct + | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod + | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ] + => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod + | [ |- context[Z.add_get_carry_full ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod + | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ] + => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod + | [ |- pair _ _ = pair _ _ ] => apply f_equal2 + | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia + | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia + | [ |- Z.opp _ = Z.opp _ ] => apply f_equal + end + | match goal with + | [ |- context[?f (list_rect _ _ _ _)] ] + => match f with + | expr.interp _ => idtac + | Compile.reify_expr => idtac + end; + erewrite (@push_f_list_rect _ _ f) + by (intros; + repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr] + | rewrite UnderLets.interp_splice ]; + match goal with + | [ |- ?LHS = ?Pcons' ?x ?xs ?rec ] + => let LHS' := match (eval pattern x, xs, rec in LHS) with ?f _ _ _ => f end in + unify Pcons' LHS'; reflexivity + end) + | [ |- context[?f (nat_rect _ _ _ _)] ] + => match f with + | expr.interp _ => idtac + | UnderLets.interp _ => idtac + | Compile.reify_expr => idtac + end; + erewrite (@push_f_nat_rect _ _ f) + by (intros; + repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr] + | rewrite UnderLets.interp_splice ]; + match goal with + | [ |- ?LHS = ?PS' ?x ?rec ] + => let LHS' := match (eval pattern x, rec in LHS) with ?f _ _ => f end in + unify PS' LHS'; reflexivity + end) + | [ |- ?f (list_rect _ _ _ _) = list_rect _ _ _ _ ] + => match f with + | expr.interp _ => idtac + | Compile.reify_expr => idtac + end; + erewrite (@push_f_list_rect _ _ f); + [ apply list_rect_Proper; repeat intro; try reflexivity | ] + | [ |- ?f (nat_rect _ _ _ _) = nat_rect _ _ _ _ ] + => match f with + | expr.interp _ => idtac + | UnderLets.interp _ => idtac + | Compile.reify_expr => idtac + end; + erewrite (@push_f_nat_rect _ _ f); + [ apply nat_rect_Proper_nondep; repeat intro; try reflexivity | ] + end + | break_innermost_match_step + | break_innermost_match_hyps_step + | match goal with + | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] + |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ] + => apply H + | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith + | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith + | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r + | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H + | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] + => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith + | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm + | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H + | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H + | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ] + => rewrite <- H in H' + | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const + | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ] + => revert v; is_var n; induction n; intro v; cbn [nat_rect] + | [ |- _ mod ?x = _ mod ?x ] + => progress (push_Zmod; pull_Zmod) + | [ |- _ mod ?x = _ mod ?x ] + => apply f_equal2; (lia + nia) + | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast + end ]. + + Lemma nbe_rewrite_rules_interp_good + : rewrite_rules_interp_goodT nbe_rewrite_rules. + Proof using Type. + Time start_interp_good. + Time all: repeat interp_good_t_step. + Qed. + + Axiom proof_admitted : False. + Local Notation admit := (match proof_admitted with end). + + Lemma arith_rewrite_rules_interp_good max_const + : rewrite_rules_interp_goodT (arith_rewrite_rules max_const). + Proof using Type. + Time start_interp_good. + Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. + (* This is mainly for display *) + all: repeat first [ progress cbn [Compile.value' Compile.reify] in * + | progress subst + | match goal with + | [ H : context[expr.interp ?ii ?v] |- _ ] + => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros + | [ |- context[expr.interp ?ii ?v] ] + => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros + end ]. + (* 9 subgoals (ID 30397) + + max_const, x, x0 : Z + v1 : expr (type.base base.type.Z) + ============================ + match + (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1); + Some (UnderLets.Base x1))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.mul_split x x0 (expr.interp (@ident.interp) v1) + | None => True + end + +subgoal 2 (ID 30445) is: + match + (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1); + Some (UnderLets.Base x1))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.mul_split x (expr.interp (@ident.interp) v1) x0 + | None => True + end +subgoal 3 (ID 30493) is: + match + (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1); + Some (UnderLets.Base x1))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.mul_split x x0 (expr.interp (@ident.interp) v1) + | None => True + end +subgoal 4 (ID 30541) is: + match + (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1); + Some (UnderLets.Base x1))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.mul_split x (expr.interp (@ident.interp) v1) x0 + | None => True + end +subgoal 5 (ID 30631) is: + match + (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0); + Some (UnderLets.Base x0))%option + with + | Some v1 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) = + Z.add_get_carry_full v2 x (expr.interp (@ident.interp) v0) + | None => True + end +subgoal 6 (ID 30721) is: + match + (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0); + Some (UnderLets.Base x0))%option + with + | Some v1 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) = + Z.add_get_carry_full v2 (expr.interp (@ident.interp) v0) x + | None => True + end +subgoal 7 (ID 30772) is: + match + (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0)); + Some (UnderLets.Base x2))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.add_with_get_carry_full x x0 x1 (expr.interp (@ident.interp) v1) + | None => True + end +subgoal 8 (ID 30824) is: + match + (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0)); + Some (UnderLets.Base x2))%option + with + | Some v0 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) = + Z.add_with_get_carry_full x x0 (expr.interp (@ident.interp) v1) x1 + | None => True + end +subgoal 9 (ID 30915) is: + match + rwhenl + (Some + (UnderLets.UnderLet + (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @ + (##x0)%expr)%expr_pat + (fun vc : Z * Z => + UnderLets.Base (#(ident.fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat))) + ((x =? 0) && (x0 =? 0)) + with + | Some v2 => + expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v2) = + Z.add_with_get_carry_full (expr.interp (@ident.interp) v1) + (expr.interp (@ident.interp) v0) x x0 + | None => True + end +*) + 1-9: exact admit. + Qed. + + Local Ltac fancy_local_t := + repeat first [ match goal with + | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, + H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H' + end + | progress autorewrite with zsimplify in * ]. + + Lemma fancy_rewrite_rules_interp_good + (invert_low invert_high : Z -> Z -> option Z) + (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) + : rewrite_rules_interp_goodT (fancy_rewrite_rules invert_low invert_high). + Proof using Type. + Time start_interp_good. + Time all: try solve [ + repeat interp_good_t_step; + cbv [Option.bind] in *; + repeat interp_good_t_step; + fancy_local_t; + repeat interp_good_t_step ]. + Time all: repeat interp_good_t_step. + Time all: cbv [Option.bind] in *. + Time all: repeat interp_good_t_step. + Time all: fancy_local_t. + Time all: repeat interp_good_t_step. + all: repeat first [ progress cbn [Compile.value' Compile.reify] in * + | progress subst + | match goal with + | [ H : context[expr.interp ?ii ?v] |- _ ] + => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros + | [ |- context[expr.interp ?ii ?v] ] + => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros + end ]. + all: repeat match goal with + | [ H : _ = _ :> BinInt.Z |- _ ] => revert H + | [ v : BinInt.Z |- _ ] => clear v || revert v + end. + (* 16 subgoals (ID 100240) + + invert_low, invert_high : Z -> Z -> option Z + Hlow : forall s v v' : Z, + invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1) + Hhigh : forall s v v' : Z, invert_high s v = Some v' -> v = Z.shiftr v' (s / 2) + ============================ + forall x x0 v1 v0 : Z, + x = 2 ^ Z.log2 x -> (v1 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0) / x + +subgoal 2 (ID 100250) is: + forall x x0 v0 v1 : Z, + x = 2 ^ Z.log2 x -> (v0 + Z.shiftl v1 x0 mod x) / x = (Z.shiftl v1 x0 + v0) / x +subgoal 3 (ID 100260) is: + forall x x0 v1 v0 : Z, + x = 2 ^ Z.log2 x -> (v1 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0) / x +subgoal 4 (ID 100270) is: + forall x x0 v0 v1 : Z, + x = 2 ^ Z.log2 x -> (v0 + Z.shiftr v1 x0 mod x) / x = (Z.shiftr v1 x0 + v0) / x +subgoal 5 (ID 100278) is: + forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 mod x) / x = (v1 + v0) / x +subgoal 6 (ID 100290) is: + forall x x0 v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> + (v1 + v0 + Z.shiftl v4 x0 mod x) / x = (v1 + v0 + Z.shiftl v4 x0) / x +subgoal 7 (ID 100302) is: + forall x x0 v1 v4 v0 : Z, + x = 2 ^ Z.log2 x -> + (v1 + v4 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0 + v4) / x +subgoal 8 (ID 100314) is: + forall x x0 v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> + (v1 + v0 + Z.shiftr v4 x0 mod x) / x = (v1 + v0 + Z.shiftr v4 x0) / x +subgoal 9 (ID 100326) is: + forall x x0 v1 v4 v0 : Z, + x = 2 ^ Z.log2 x -> + (v1 + v4 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0 + v4) / x +subgoal 10 (ID 100336) is: + forall x v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> (v1 + v0 + v4 mod x) / x = (v1 + v0 + v4) / x +subgoal 11 (ID 100346) is: + forall x x0 v1 v0 : Z, + x = 2 ^ Z.log2 x -> (v1 - Z.shiftl v0 x0 mod x) / x = (v1 - Z.shiftl v0 x0) / x +subgoal 12 (ID 100356) is: + forall x x0 v1 v0 : Z, + x = 2 ^ Z.log2 x -> (v1 - Z.shiftr v0 x0 mod x) / x = (v1 - Z.shiftr v0 x0) / x +subgoal 13 (ID 100364) is: + forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 - v0 mod x) / x = (v1 - v0) / x +subgoal 14 (ID 100376) is: + forall x x0 v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> + (v0 - Z.shiftl v4 x0 mod x - v1) / x = (v0 - Z.shiftl v4 x0 - v1) / x +subgoal 15 (ID 100388) is: + forall x x0 v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> + (v0 - Z.shiftr v4 x0 mod x - v1) / x = (v0 - Z.shiftr v4 x0 - v1) / x +subgoal 16 (ID 100398) is: + forall x v1 v0 v4 : Z, + x = 2 ^ Z.log2 x -> (v0 - v4 mod x - v1) / x = (v0 - v4 - v1) / x +*) + all: exact admit. + Qed. + End RewriteRules. +End Compilers. diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 37e192f07..4f2017cbf 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -204,6 +204,9 @@ Module Compilers. (full_types : raw_pident -> Type) (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) + (pident_to_typed + : forall t (idc : pident t) (evm : EvarMap), + type_of_list (pident_arg_types t idc) -> ident (pattern.type.subst_default t evm)) (type_of_raw_pident : forall (pidc : raw_pident), full_types pidc -> type.type base.type) (raw_pident_to_typed : forall (pidc : raw_pident) (args : full_types pidc), ident (type_of_raw_pident pidc args)) (raw_pident_is_simple : raw_pident -> bool) @@ -236,15 +239,24 @@ Module Compilers. Local Notation to_raw_pattern := (@pattern.to_raw pident raw_pident (@strip_types)). Local Notation reify := (@reify ident). Local Notation reflect := (@reflect ident). + Local Notation reify_expr := (@reify_expr ident). Local Notation rawexpr := (@rawexpr ident). Local Notation eval_decision_tree var := (@eval_decision_tree ident var pident full_types invert_bind_args type_of_raw_pident raw_pident_to_typed). Local Notation reveal_rawexpr e := (@reveal_rawexpr_cps ident _ e _ id). Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown). Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown type_vars_of_pident). + Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls + := list_rect + (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls) + (fun f => f tt) + (fun T Ts rec k t => rec (fun ts => k (t, ts))) + ls. + Section with_var1. Context {var : type -> Type}. Local Notation expr := (@expr.expr base.type ident var). + Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var). Local Notation "e1 === e2" := (existT expr _ e1 = existT expr _ e2) : type_scope. @@ -572,27 +584,37 @@ Module Compilers. | break_match_step ltac:(fun _ => idtac) ]. Qed. - Lemma normalize_deep_rewrite_rule_cps_id - {should_do_again with_opt under_lets is_cps t v T k} - (Hk : k None = None) - (Hv : (match is_cps, with_opt return @deep_rewrite_ruleTP_gen ident var should_do_again with_opt under_lets is_cps t -> Prop - with - | true, true => fun v => forall T k, v T k = k (v _ id) - | true, false => fun v => forall T k, v T k = (v' <- v _ (@Some _); k v')%option - | false, _ => fun _ => True - end) - v) - : @normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v T k = k (@normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v _ id). - Proof using Type. - clear -Hv Hk; cbn in *. - repeat first [ progress cbn in * - | progress destruct_head'_bool - | reflexivity - | progress cbv [id Option.bind] in * - | solve [ auto ] - | break_innermost_match_step - | rewrite Hv; (solve [ auto ] + break_innermost_match_step) ]. - Qed. + Section normalize_deep_rewrite_rule_cps_id. + Context {should_do_again with_opt under_lets is_cps : bool} + {t} + {v : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t} + {T} + {k : option (UnderLets var (@expr.expr base.type ident (if should_do_again then @value var else var) t)) -> option T}. + + Definition normalize_deep_rewrite_rule_cps_id_hypsT + := ((match is_cps, with_opt return @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t -> Prop + with + | true, true => fun v => forall T k, v T k = k (v _ id) + | true, false => fun v => forall T k, v T k = (v' <- v _ (@Some _); k v')%option + | false, _ => fun _ => True + end) + v). + + Lemma normalize_deep_rewrite_rule_cps_id + (Hk : k None = None) + (Hv : normalize_deep_rewrite_rule_cps_id_hypsT) + : @normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v T k = k (@normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v _ id). + Proof using Type. + clear -Hk Hv; cbv [normalize_deep_rewrite_rule_cps_id_hypsT] in *; cbn in *. + repeat first [ progress cbn in * + | progress destruct_head'_bool + | reflexivity + | progress cbv [id Option.bind] in * + | solve [ auto ] + | break_innermost_match_step + | rewrite Hv; (solve [ auto ] + break_innermost_match_step) ]. + Qed. + End normalize_deep_rewrite_rule_cps_id. End with_var1. Section with_var2. @@ -671,6 +693,26 @@ Module Compilers. eapply wf_reify; auto. } Qed. + Lemma wf_reify_expr G G' {t} + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @wf_value G' t v1 v2) + e1 e2 + (Hwf : expr.wf G e1 e2) + : expr.wf G' (@reify_expr var1 t e1) (@reify_expr var2 t e2). + Proof using Type. + cbv [wf_value] in *; revert dependent G'; induction Hwf; intros; cbn [reify_expr]; + first [ constructor | apply wf_reify ]; eauto; intros. + all: match goal with H : _ |- _ => apply H end. + all: repeat first [ progress cbn [In eq_rect] in * + | progress intros + | progress destruct_head'_or + | progress subst + | progress inversion_sigma + | progress inversion_prod + | apply wf_reflect + | solve [ eapply wf_value'_Proper_list; [ | solve [ eauto ] ]; wf_safe_t ] + | constructor ]. + Qed. + Inductive wf_rawexpr : list { t : type & var1 t * var2 t }%type -> forall {t}, @rawexpr var1 -> @expr var1 t -> @rawexpr var2 -> @expr var2 t -> Prop := | Wf_rIdent {t} G known (idc : ident t) : wf_rawexpr G (rIdent known idc (expr.Ident idc)) (expr.Ident idc) (rIdent known idc (expr.Ident idc)) (expr.Ident idc) | Wf_rApp {s d} G @@ -994,6 +1036,137 @@ Module Compilers. (rew [fun tp => @rewrite_rule_data1 _ (pattern.pattern_of_anypattern tp)] pf in r1) r2 }). End with_var2. + + Section with_interp. + Context (ident_interp : forall t, ident t -> type.interp base.interp t) + {ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (ident_interp t)}. + Local Notation var := (type.interp base.interp) (only parsing). + Local Notation expr := (@expr.expr base.type ident var). + Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types type_vars_of_pident). + Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types type_vars_of_pident). + Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types type_vars_of_pident). + Local Notation with_unification_resultT' := (@with_unification_resultT' ident var pident pident_arg_types). + Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var). + Local Notation under_with_unification_resultT_relation := (@under_with_unification_resultT_relation ident var pident pident_arg_types type_vars_of_pident). + Local Notation under_with_unification_resultT_relation_hetero := (@under_with_unification_resultT_relation_hetero ident var pident pident_arg_types type_vars_of_pident). + Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var). + + Local Notation UnderLets_maybe_interp with_lets + := (if with_lets as with_lets' return (if with_lets' then UnderLets var _ else _) -> _ + then UnderLets.interp ident_interp + else (fun x => x)). + + Fixpoint value'_interp_related + {with_lets1 with_lets2 t} + : @value' var with_lets1 t + -> @value' var with_lets2 t + -> Prop + := match t return value' _ t -> value' _ t -> Prop with + | type.base t + => fun v1 v2 + => expr.interp ident_interp (UnderLets_maybe_interp with_lets1 v1) + == expr.interp ident_interp (UnderLets_maybe_interp with_lets2 v2) + | type.arrow s d + => fun (f1 f2 : value' _ s -> value' _ d) + => forall x1 x2, + @value'_interp_related _ _ s x1 x2 + -> @value'_interp_related _ _ d (f1 x1) (f2 x2) + end. + + Definition value_interp_related {t} : relation (@value var t) + := value'_interp_related. + + Lemma interp_reify_reflect {with_lets t} e v + : expr.interp ident_interp e == v -> expr.interp ident_interp (@reify _ with_lets t (reflect e)) == v. + Proof using Type. + revert with_lets; induction t as [|s IHs d IHd]; intro; + cbn [type.related reflect reify]; + fold (@reify var) (@reflect var); cbv [respectful]; break_innermost_match; + cbn [expr.interp UnderLets.to_expr]; auto; []. + intros Hf ? ? Hx. + apply IHd; cbn [expr.interp]; auto. + Qed. + + Lemma interp_of_wf_reify_expr G {t} + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp ident_interp (reify v1) == v2) + e1 e2 + (Hwf : expr.wf G e1 e2) + : expr.interp ident_interp (@reify_expr _ t e1) == expr.interp ident_interp e2. + Proof using ident_interp_Proper. + induction Hwf; cbn [expr.interp reify_expr]; cbv [LetIn.Let_In]; + try solve [ auto + | apply ident_interp_Proper; reflexivity ]. + all: cbn [type.related] in *; cbv [respectful]; intros. + all: match goal with H : _ |- _ => apply H; clear H end. + all: repeat first [ progress cbn [In eq_rect fst snd] in * + | progress intros + | progress destruct_head'_or + | progress subst + | progress inversion_sigma + | progress inversion_prod + | apply interp_reify_reflect + | solve [ auto ] ]. + Qed. + + Fixpoint pattern_default_interp' {K t} (p : pattern t) evm {struct p} : (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K + := match p in pattern.pattern t return (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K with + | pattern.Wildcard t => fun k v => k (reify v) + | pattern.Ident t idc + => fun k + => lam_type_of_list (fun args => k (expr.Ident (pident_to_typed _ idc _ args))) + | pattern.App s d f x + => fun k + => @pattern_default_interp' + _ _ f evm + (fun ef + => @pattern_default_interp' + _ _ x evm + (fun ex + => k (expr.App ef ex))) + end. + + Definition pattern_default_interp {t} (p : pattern t) : @with_unif_rewrite_ruleTP_gen t p false false false false + := pattern.type.lam_forall_vars + (fun evm + => pattern_default_interp' p evm id). + + Definition deep_rewrite_ruleTP_gen_good_relation + {should_do_again with_opt under_lets is_cps : bool} {t} + (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t) + (v2 : expr t) + : Prop + := @normalize_deep_rewrite_rule_cps_id_hypsT var _ _ _ _ _ v1 + /\ (let v1 := normalize_deep_rewrite_rule v1 _ id in + match v1 with + | None => True + | Some v1 => let v1 := UnderLets.interp ident_interp v1 in + (if should_do_again + return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> Prop + then + (fun v1 + => expr.interp ident_interp (reify_expr v1) == expr.interp ident_interp v2) + else + (fun v1 => expr.interp ident_interp v1 == expr.interp ident_interp v2)) + v1 + end). + + Definition rewrite_rule_data_interp_goodT + {t} {p : pattern t} (r : @rewrite_rule_data t p) + : Prop + := @under_with_unification_resultT_relation_hetero + _ _ _ _ + (fun _ => value_interp_related) + (fun evm => deep_rewrite_ruleTP_gen_good_relation) + (rew_replacement _ _ r) + (pattern_default_interp p). + + Definition rewrite_rules_interp_goodT + (rews : rewrite_rulesT) + : Prop + := forall p r, + List.In (existT _ p r) rews + -> rewrite_rule_data_interp_goodT r. + End with_interp. End with_var. End Compile. End RewriteRules. diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index 6b2d92971..de17f2896 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -799,7 +799,7 @@ Module Compilers. => rewrite ap_transport_Base | [ |- True ] => exact I end - | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind'] in * + | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind' normalize_deep_rewrite_rule_cps_id_hypsT] in * | lazymatch goal with | [ |- (@unify_pattern1 ?t ?re1 ?p ?K1 ?v1 ?T1 ?cont1 = None <-> @unify_pattern2 ?t ?re2 ?p ?K2 ?v2 ?T2 ?cont2 = None) |