diff options
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 5 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 442 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterProofs.v | 44 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 33 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 42 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 25 |
6 files changed, 326 insertions, 265 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 5ace04e08..476612aef 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -320,6 +320,11 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ break_innermost_match; split_andb; Z.ltb_to_lt; intro H'; rewrite ?H' by lia; Z.rewrite_mod_small; reflexivity. Qed. + + Lemma cast_normalize r v : cast (ZRange.normalize r) v = cast r v. + Proof. + cbv [cast]; rewrite ZRange.normalize_idempotent; reflexivity. + Qed. End with_cast. Lemma cast_idempotent_gen {cast_outside_of_range1 cast_outside_of_range2} diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 0713ea83a..6c0572ea4 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -5,6 +5,8 @@ Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. Require Import Crypto.Experiments.NewPipeline.Language. @@ -1854,17 +1856,29 @@ Module Compilers. ; make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp e)) (* inline negation when the rewriter wouldn't already inline it *) ]. + Definition arith_with_casts_rewrite_rules : rewrite_rulesT + := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x) + ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y) + ; make_rewriteo + (#pattern.ident.Z_cast @ (#pattern.ident.Z_cast @ ??)) + (fun r1 r2 x => #(ident.Z_cast r2) @ x when ZRange.is_tighter_than_bool (ZRange.normalize r2) (ZRange.normalize r1))]. + Definition nbe_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 nbe_rewrite_rules. Definition arith_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 (arith_rewrite_rules 0%Z (* dummy val *)). + Definition arith_with_casts_dtree' + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 arith_with_casts_rewrite_rules. Definition nbe_dtree : decision_tree := Eval compute in invert_Some nbe_dtree'. Definition arith_dtree : decision_tree := Eval compute in invert_Some arith_dtree'. + Definition arith_with_casts_dtree : decision_tree + := Eval compute in invert_Some arith_with_casts_dtree'. Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules. Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)). + Definition arith_with_casts_default_fuel := Eval compute in List.length arith_with_casts_rewrite_rules. Import PrimitiveHList. (* N.B. The [combine_hlist] call MUST eta-expand @@ -1888,10 +1902,16 @@ Module Compilers. Definition arith_pr1_rewrite_rules max_const_val := Eval hnf in projT1 (arith_split_rewrite_rules max_const_val). Definition arith_pr2_rewrite_rules max_const_val := Eval hnf in projT2 (arith_split_rewrite_rules max_const_val). Definition arith_all_rewrite_rules max_const_val := combine_hlist (P:=rewrite_ruleTP) (arith_pr1_rewrite_rules max_const_val) (arith_pr2_rewrite_rules max_const_val). + Definition arith_with_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 arith_with_casts_rewrite_rules] in split_list arith_with_casts_rewrite_rules. + Definition arith_with_casts_pr1_rewrite_rules := Eval hnf in projT1 arith_with_casts_split_rewrite_rules. + Definition arith_with_casts_pr2_rewrite_rules := Eval hnf in projT2 arith_with_casts_split_rewrite_rules. + Definition arith_with_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) (arith_with_casts_pr1_rewrite_rules) arith_with_casts_pr2_rewrite_rules. Definition nbe_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters nbe_dtree nbe_all_rewrite_rules do_again t idc. Definition arith_rewrite_head0 max_const_val do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters arith_dtree (arith_all_rewrite_rules max_const_val) do_again t idc. + Definition arith_with_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t + := @assemble_identifier_rewriters arith_with_casts_dtree arith_with_casts_all_rewrite_rules do_again t idc. Section fancy. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z). @@ -2067,18 +2087,32 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) ((#pattern.ident.Z_shiftr @ ?? @ #?ℤ) * (#pattern.ident.Z_shiftr @ ?? @ #?ℤ)) (fun x offset1 y offset2 => let s := (2*offset1)%Z in #(ident.fancy_mulhh s) @ (x, y) when offset1 =? offset2) ]. + Definition fancy_with_casts_rewrite_rules : rewrite_rulesT + := []. + Definition fancy_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_rewrite_rules. Definition fancy_dtree : decision_tree := Eval compute in invert_Some fancy_dtree'. + Definition fancy_with_casts_dtree' + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_with_casts_rewrite_rules. + Definition fancy_with_casts_dtree : decision_tree + := Eval compute in invert_Some fancy_with_casts_dtree'. Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules. + Definition fancy_with_casts_default_fuel := Eval compute in List.length fancy_with_casts_rewrite_rules. Import PrimitiveHList. Definition fancy_split_rewrite_rules := Eval cbv [split_list projT1 projT2 fancy_rewrite_rules] in split_list fancy_rewrite_rules. Definition fancy_pr1_rewrite_rules := Eval hnf in projT1 fancy_split_rewrite_rules. Definition fancy_pr2_rewrite_rules := Eval hnf in projT2 fancy_split_rewrite_rules. Definition fancy_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) fancy_pr1_rewrite_rules fancy_pr2_rewrite_rules. + Definition fancy_with_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 fancy_with_casts_rewrite_rules] in split_list fancy_with_casts_rewrite_rules. + Definition fancy_with_casts_pr1_rewrite_rules := Eval hnf in projT1 fancy_with_casts_split_rewrite_rules. + Definition fancy_with_casts_pr2_rewrite_rules := Eval hnf in projT2 fancy_with_casts_split_rewrite_rules. + Definition fancy_with_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) fancy_with_casts_pr1_rewrite_rules fancy_with_casts_pr2_rewrite_rules. Definition fancy_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters fancy_dtree fancy_all_rewrite_rules do_again t idc. + Definition fancy_with_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t + := @assemble_identifier_rewriters fancy_with_casts_dtree fancy_with_casts_all_rewrite_rules do_again t idc. End fancy. End with_var. Module RewriterPrintingNotations. @@ -2103,193 +2137,150 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'type.try_make_transport_cps' t1 t2 ; '/' f ']'"). Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x <- 'base.try_make_transport_cps' t1 t2 ; '/' f ']'"). End RewriterPrintingNotations. + + Ltac make_rewrite_head1 rewrite_head0 pr2_rewrite_rules := + (eval cbv -[pr2_rewrite_rules + base.interp base.try_make_transport_cps + type.try_make_transport_cps type.try_transport_cps + pattern.type.unify_extracted_cps + Let_In Option.sequence Option.sequence_return + UnderLets.splice UnderLets.to_expr + Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule + Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps + Compile.value' + SubstVarLike.is_var_fst_snd_pair_opp + ] in rewrite_head0). + Ltac timed_make_rewrite_head1 rewrite_head0 pr2_rewrite_rules := + constr:(ltac:(time (idtac; let v := make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in exact v))). + Ltac make_rewrite_head2 rewrite_head1 pr2_rewrite_rules := + (eval cbv [id + pr2_rewrite_rules + projT1 projT2 + cpsbind cpscall cps_option_bind cpsreturn + PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd + pattern.ident.arg_types + Compile.eval_decision_tree + Compile.eval_rewrite_rules + Compile.expr_of_rawexpr + Compile.normalize_deep_rewrite_rule + Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule + (*Compile.reflect*) + (*Compile.reify*) + Compile.reveal_rawexpr_cps + Compile.reveal_rawexpr_cps_gen + Compile.rew_should_do_again + Compile.rew_with_opt + Compile.rew_under_lets + Compile.rew_replacement + Compile.rew_is_cps + Compile.rValueOrExpr + Compile.swap_list + Compile.type_of_rawexpr + Compile.value + (*Compile.value'*) + Compile.value_of_rawexpr + Compile.value_with_lets + ident.smart_Literal + type.try_transport_cps + rlist_rect rwhen rwhenl + ] in rewrite_head1). + Ltac timed_make_rewrite_head2 rewrite_head1 pr2_rewrite_rules := + constr:(ltac:(time (idtac; let v := make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in exact v))). + Ltac make_rewrite_head3 rewrite_head2 := + (eval cbn [id + cpsbind cpscall cps_option_bind cpsreturn + Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value' + Option.sequence Option.sequence_return Option.bind + UnderLets.reify_and_let_binds_base_cps + UnderLets.splice UnderLets.splice_list UnderLets.to_expr + base.interp base.base_interp + base.type.base_beq + type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps + Datatypes.fst Datatypes.snd + ] in rewrite_head2). + Ltac timed_make_rewrite_head3 rewrite_head2 := + constr:(ltac:(time (idtac; let v := make_rewrite_head3 rewrite_head2 in exact v))). + Ltac make_rewrite_head rewrite_head0 pr2_rewrite_rules := + let rewrite_head1 := make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in + let rewrite_head2 := make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in + let rewrite_head3 := make_rewrite_head3 rewrite_head2 in + rewrite_head3. + Ltac timed_make_rewrite_head rewrite_head0 pr2_rewrite_rules := + let rewrite_head1 := timed_make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in + let rewrite_head2 := timed_make_rewrite_head2 rewrite_head1 pr2_rewrite_rules in + let rewrite_head3 := timed_make_rewrite_head3 rewrite_head2 in + rewrite_head3. + Notation make_rewrite_head rewrite_head0 pr2_rewrite_rules + := (ltac:(let v := timed_make_rewrite_head rewrite_head0 pr2_rewrite_rules in + exact v)) (only parsing). + + (* For reduction *) + Local Arguments base.try_make_base_transport_cps _ !_ !_. + Local Arguments base.try_make_transport_cps _ !_ !_. + Local Arguments type.try_make_transport_cps _ _ _ !_ !_. + Local Arguments Option.sequence {A} !v1 v2. + Local Arguments Option.sequence_return {A} !v1 v2. + Local Arguments Option.bind {A B} !_ _. + Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_. + Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _. + Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. + Local Arguments base.type.base_beq !_ !_. + Local Arguments id / . + (* For printing *) + Local Arguments option {_}. + Local Arguments UnderLets.UnderLets {_ _ _}. + Local Arguments expr.expr {_ _ _}. + Local Notation ℤ := base.type.Z. + Local Notation ℕ := base.type.nat. + Local Notation bool := base.type.bool. + Local Notation unit := base.type.unit. + Local Notation list := base.type.list. + Local Notation "x" := (type.base x) (only printing, at level 9). + Section red_fancy. - Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) {var : type.type base.type -> Type} (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) - -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) {t} (idc : ident t). - Time Let rewrite_head1 - := Eval cbv -[fancy_pr2_rewrite_rules - base.interp base.try_make_transport_cps - type.try_make_transport_cps type.try_transport_cps - pattern.type.unify_extracted_cps - Let_In Option.sequence Option.sequence_return - UnderLets.splice UnderLets.to_expr - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps - Compile.value' - SubstVarLike.is_var_fst_snd_pair_opp - ] in @fancy_rewrite_head0 var invert_low invert_high do_again t idc. - (* Finished transaction in 3.395 secs (3.395u,0.s) (successful) *) - - Time Local Definition fancy_rewrite_head2 - := Eval cbv [id - rewrite_head1 fancy_pr2_rewrite_rules - projT1 projT2 - cpsbind cpscall cps_option_bind cpsreturn - PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd - pattern.ident.arg_types - Compile.eval_decision_tree - Compile.eval_rewrite_rules - Compile.expr_of_rawexpr - Compile.normalize_deep_rewrite_rule - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - (*Compile.reflect*) - (*Compile.reify*) - Compile.reveal_rawexpr_cps - Compile.reveal_rawexpr_cps_gen - Compile.rew_should_do_again - Compile.rew_with_opt - Compile.rew_under_lets - Compile.rew_replacement - Compile.rew_is_cps - Compile.rValueOrExpr - Compile.swap_list - Compile.type_of_rawexpr - Compile.value - (*Compile.value'*) - Compile.value_of_rawexpr - Compile.value_with_lets - ident.smart_Literal - type.try_transport_cps - rlist_rect rwhen rwhenl - ] in rewrite_head1. - (* Finished transaction in 10.793 secs (10.796u,0.s) (successful) *) - - Local Arguments base.try_make_base_transport_cps _ !_ !_. - Local Arguments base.try_make_transport_cps _ !_ !_. - Local Arguments type.try_make_transport_cps _ _ _ !_ !_. - Local Arguments Option.sequence {A} !v1 v2. - Local Arguments Option.sequence_return {A} !v1 v2. - Local Arguments Option.bind {A B} !_ _. - Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_. - Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _. - Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. - Local Arguments base.type.base_beq !_ !_. - Local Arguments option {_}. - Local Arguments id / . - Local Arguments fancy_rewrite_head2 / . - Local Arguments UnderLets.UnderLets {_ _ _}. - Local Arguments expr.expr {_ _ _}. - Local Notation ℤ := base.type.Z. - Local Notation ℕ := base.type.nat. - Local Notation bool := base.type.bool. - Local Notation unit := base.type.unit. - Local Notation list := base.type.list. - Local Notation "x" := (type.base x) (only printing, at level 9). Time Definition fancy_rewrite_head - := Eval cbn [id - fancy_rewrite_head2 - cpsbind cpscall cps_option_bind cpsreturn - Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value' - Option.sequence Option.sequence_return Option.bind - UnderLets.reify_and_let_binds_base_cps - UnderLets.splice UnderLets.splice_list UnderLets.to_expr - base.interp base.base_interp - base.type.base_beq - type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps - Datatypes.fst Datatypes.snd - ] in fancy_rewrite_head2. - (* Finished transaction in 1.892 secs (1.891u,0.s) (successful) *) + := make_rewrite_head (@fancy_rewrite_head0 var invert_low invert_high do_again t idc) (@fancy_pr2_rewrite_rules). + (* Tactic call ran for 0.19 secs (0.187u,0.s) (success) + Tactic call ran for 10.297 secs (10.3u,0.s) (success) + Tactic call ran for 1.746 secs (1.747u,0.s) (success) + Finished transaction in 12.402 secs (12.4u,0.s) (successful) *) Local Set Printing Depth 1000000. Local Set Printing Width 200. Import RewriterPrintingNotations. (* Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head. *) End red_fancy. + Section red_fancy_with_casts. + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + {var : type.type base.type -> Type} + (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + {t} (idc : ident t). + Time Definition fancy_with_casts_rewrite_head + := make_rewrite_head (@fancy_with_casts_rewrite_head0 var (*invert_low invert_high*) do_again t idc) (@fancy_with_casts_pr2_rewrite_rules). + Local Set Printing Depth 1000000. + Local Set Printing Width 200. + Import RewriterPrintingNotations. + (* Redirect "/tmp/fancy_with_casts_rewrite_head" Print fancy_with_casts_rewrite_head. *) + End red_fancy_with_casts. Section red_nbe. Context {var : type.type base.type -> Type} (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) - -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) {t} (idc : ident t). - - Time Let rewrite_head1 - := Eval cbv -[nbe_pr2_rewrite_rules - base.interp base.try_make_transport_cps - type.try_make_transport_cps type.try_transport_cps - pattern.type.unify_extracted_cps - Let_In Option.sequence Option.sequence_return - UnderLets.splice UnderLets.to_expr - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps - Compile.value' - SubstVarLike.is_var_fst_snd_pair_opp - ] in @nbe_rewrite_head0 var do_again t idc. - (* Finished transaction in 7.035 secs (7.036u,0.s) (successful) *) - - Time Local Definition nbe_rewrite_head2 - := Eval cbv [id - rewrite_head1 nbe_pr2_rewrite_rules - projT1 projT2 - cpsbind cpscall cps_option_bind cpsreturn - PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd - pattern.ident.arg_types - Compile.eval_decision_tree - Compile.eval_rewrite_rules - Compile.expr_of_rawexpr - Compile.normalize_deep_rewrite_rule - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - (*Compile.reflect*) - (*Compile.reify*) - Compile.reveal_rawexpr_cps - Compile.reveal_rawexpr_cps_gen - Compile.rew_should_do_again - Compile.rew_with_opt - Compile.rew_under_lets - Compile.rew_replacement - Compile.rew_is_cps - Compile.rValueOrExpr - Compile.swap_list - Compile.type_of_rawexpr - Compile.value - (*Compile.value'*) - Compile.value_of_rawexpr - Compile.value_with_lets - ident.smart_Literal - type.try_transport_cps - rlist_rect rwhen rwhenl - ] in rewrite_head1. - (* Finished transaction in 29.297 secs (29.284u,0.016s) (successful) *) - - Local Arguments base.try_make_base_transport_cps _ !_ !_. - Local Arguments base.try_make_transport_cps _ !_ !_. - Local Arguments type.try_make_transport_cps _ _ _ !_ !_. - Local Arguments Option.sequence {A} !v1 v2. - Local Arguments Option.sequence_return {A} !v1 v2. - Local Arguments Option.bind {A B} !_ _. - Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_. - Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _. - Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. - Local Arguments base.type.base_beq !_ !_. - Local Arguments option {_}. - Local Arguments id / . - Local Arguments nbe_rewrite_head2 / . - Local Arguments UnderLets.UnderLets {_ _ _}. - Local Arguments expr.expr {_ _ _}. - Local Notation ℤ := base.type.Z. - Local Notation ℕ := base.type.nat. - Local Notation bool := base.type.bool. - Local Notation unit := base.type.unit. - Local Notation list := base.type.list. - Local Notation "x" := (type.base x) (only printing, at level 9). - Time Definition nbe_rewrite_head - := Eval cbn [id - nbe_rewrite_head2 - cpsbind cpscall cps_option_bind cpsreturn - Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value' - Option.sequence Option.sequence_return Option.bind - UnderLets.reify_and_let_binds_base_cps - UnderLets.splice UnderLets.splice_list UnderLets.to_expr - base.interp base.base_interp - base.type.base_beq - type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps - PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd Datatypes.fst Datatypes.snd - ] in nbe_rewrite_head2. - (* Finished transaction in 1.998 secs (2.u,0.s) (successful) *) + := make_rewrite_head (@nbe_rewrite_head0 var do_again t idc) (@nbe_pr2_rewrite_rules). + (* Tactic call ran for 0.232 secs (0.235u,0.s) (success) + Tactic call ran for 29.061 secs (29.04u,0.004s) (success) + Tactic call ran for 1.605 secs (1.604u,0.s) (success) + Finished transaction in 31.203 secs (31.183u,0.004s) (successful) *) Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2301,93 +2292,15 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Context (max_const_val : Z) {var : type.type base.type -> Type} (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) - -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) {t} (idc : ident t). - Time Let rewrite_head1 - := Eval cbv -[arith_pr2_rewrite_rules - base.interp base.try_make_transport_cps - type.try_make_transport_cps type.try_transport_cps - pattern.type.unify_extracted_cps - Let_In Option.sequence Option.sequence_return - UnderLets.splice UnderLets.to_expr - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps - Compile.value' - SubstVarLike.is_var_fst_snd_pair_opp - ] in @arith_rewrite_head0 var max_const_val do_again t idc. - (* Finished transaction in 15.381 secs (15.379u,0.s) (successful) *) - - Time Local Definition arith_rewrite_head2 - := Eval cbv [id - rewrite_head1 arith_pr2_rewrite_rules - projT1 projT2 - cpsbind cpscall cps_option_bind cpsreturn - PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd - pattern.ident.arg_types - Compile.eval_decision_tree - Compile.eval_rewrite_rules - Compile.expr_of_rawexpr - Compile.normalize_deep_rewrite_rule - Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule - (*Compile.reflect*) - (*Compile.reify*) - Compile.reveal_rawexpr_cps - Compile.reveal_rawexpr_cps_gen - Compile.rew_should_do_again - Compile.rew_with_opt - Compile.rew_under_lets - Compile.rew_replacement - Compile.rew_is_cps - Compile.rValueOrExpr - Compile.swap_list - Compile.type_of_rawexpr - Compile.value - (*Compile.value'*) - Compile.value_of_rawexpr - Compile.value_with_lets - ident.smart_Literal - type.try_transport_cps - rlist_rect rwhen rwhenl - ] in rewrite_head1. - (* Finished transaction in 83.667 secs (83.564u,0.115s) (successful) *) - - Local Arguments base.try_make_base_transport_cps _ !_ !_. - Local Arguments base.try_make_transport_cps _ !_ !_. - Local Arguments type.try_make_transport_cps _ _ _ !_ !_. - Local Arguments Option.sequence {A} !v1 v2. - Local Arguments Option.sequence_return {A} !v1 v2. - Local Arguments Option.bind {A B} !_ _. - Local Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_. - Local Arguments base.try_make_transport_cps {P} t1 t2 {_} _. - Local Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. - Local Arguments base.type.base_beq !_ !_. - Local Arguments option {_}. - Local Arguments id / . - Local Arguments arith_rewrite_head2 / . - Local Arguments UnderLets.UnderLets {_ _ _}. - Local Arguments expr.expr {_ _ _}. - Local Notation ℤ := base.type.Z. - Local Notation ℕ := base.type.nat. - Local Notation bool := base.type.bool. - Local Notation unit := base.type.unit. - Local Notation list := base.type.list. - Local Notation "x" := (type.base x) (only printing, at level 9). - Time Definition arith_rewrite_head - := Eval cbn [id - arith_rewrite_head2 - cpsbind cpscall cps_option_bind cpsreturn - Compile.reify Compile.reify_and_let_binds_cps Compile.reflect Compile.value' - Option.sequence Option.sequence_return Option.bind - UnderLets.reify_and_let_binds_base_cps - UnderLets.splice UnderLets.splice_list UnderLets.to_expr - base.interp base.base_interp - base.type.base_beq - type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps - PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd Datatypes.fst Datatypes.snd - ] in arith_rewrite_head2. - (* Finished transaction in 3.967 secs (3.968u,0.s) (successful) *) + := make_rewrite_head (@arith_rewrite_head0 var max_const_val do_again t idc) (@arith_pr2_rewrite_rules). + (* Tactic call ran for 0.283 secs (0.284u,0.s) (success) + Tactic call ran for 79.61 secs (79.612u,0.008s) (success) + Tactic call ran for 3.574 secs (3.576u,0.s) (success) + Finished transaction in 83.677 secs (83.68u,0.008s) (successful) *) Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2395,14 +2308,35 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) (* Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head. *) End red_arith. + Section red_arith_with_casts. + Context {var : type.type base.type -> Type} + (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + {t} (idc : ident t). + + Time Definition arith_with_casts_rewrite_head + := make_rewrite_head (@arith_with_casts_rewrite_head0 var do_again t idc) (@arith_with_casts_pr2_rewrite_rules). + + Local Set Printing Depth 1000000. + Local Set Printing Width 200. + Import RewriterPrintingNotations. + (* Redirect "/tmp/arith_with_casts_rewrite_head" Print arith_with_casts_rewrite_head. *) + End red_arith_with_casts. + Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@nbe_rewrite_head) nbe_default_fuel t e. Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@arith_rewrite_head max_const_val) arith_default_fuel t e. + Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t + := @Compile.Rewrite (fun var do_again => @arith_with_casts_rewrite_head var) arith_with_casts_default_fuel t e. Definition RewriteToFancy - (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (fun var _ => @fancy_rewrite_head invert_low invert_high var) fancy_default_fuel t e. + Definition RewriteToFancyWithCasts + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t + := @Compile.Rewrite (fun var _ => @fancy_with_casts_rewrite_head (*invert_low invert_high*) var) fancy_with_casts_default_fuel t e. End RewriteRules. Import defaults. diff --git a/src/Experiments/NewPipeline/RewriterProofs.v b/src/Experiments/NewPipeline/RewriterProofs.v index eddd3585f..df51ea28d 100644 --- a/src/Experiments/NewPipeline/RewriterProofs.v +++ b/src/Experiments/NewPipeline/RewriterProofs.v @@ -77,6 +77,11 @@ Module Compilers. start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). apply arith_rewrite_rules_good. Qed. + Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e). + Proof. + start_Wf_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0). + apply arith_with_casts_rewrite_rules_good. + Qed. Lemma Wf_RewriteToFancy (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)) @@ -86,6 +91,15 @@ Module Compilers. apply fancy_rewrite_rules_good; assumption. Qed. + Lemma Wf_RewriteToFancyWithCasts (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)) + {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts invert_low invert_high t e). + Proof. + start_Wf_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0). + eapply fancy_with_casts_rewrite_rules_good; eassumption. + Qed. + Lemma Interp_gen_RewriteNBE {cast_outside_of_range t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteNBE t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. @@ -99,6 +113,13 @@ Module Compilers. start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). Admitted. + Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e. + Proof. + start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0). + Admitted. + Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (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)) @@ -109,17 +130,36 @@ Module Compilers. start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). Admitted. + Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (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)) + {t} e (Hwf : Wf e) + : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e. + Proof. + start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0). + Admitted. + Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. Proof. apply Interp_gen_RewriteNBE; assumption. Qed. Lemma Interp_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Interp (@RewriteArith max_const_val t e) == Interp e. Proof. apply Interp_gen_RewriteArith; assumption. Qed. + Lemma Interp_RewriteArithWithCasts {t} e (Hwf : Wf e) + : Interp (@RewriteArithWithCasts t e) == Interp e. + Proof. apply Interp_gen_RewriteArithWithCasts; assumption. Qed. Lemma Interp_RewriteToFancy (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)) {t} e (Hwf : Wf e) : Interp (@RewriteToFancy invert_low invert_high t e) == Interp e. Proof. apply Interp_gen_RewriteToFancy; assumption. Qed. + Lemma Interp_RewriteToFancyWithCasts (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)) + {t} e (Hwf : Wf e) + : Interp (@RewriteToFancyWithCasts invert_low invert_high t e) == Interp e. + Proof. apply Interp_gen_RewriteToFancyWithCasts; assumption. Qed. End RewriteRules. Lemma Wf_PartialEvaluate {t} e (Hwf : Wf e) : Wf (@PartialEvaluate t e). @@ -133,6 +173,6 @@ Module Compilers. : Interp (@PartialEvaluate t e) == Interp e. Proof. apply Interp_gen_PartialEvaluate; assumption. Qed. - Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy : wf. - Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy : interp. + Hint Resolve Wf_PartialEvaluate Wf_RewriteArith Wf_RewriteNBE Wf_RewriteToFancy Wf_RewriteArithWithCasts Wf_RewriteToFancyWithCasts : wf. + Hint Rewrite @Interp_gen_PartialEvaluate @Interp_gen_RewriteArith @Interp_gen_RewriteNBE @Interp_gen_RewriteToFancy @Interp_gen_RewriteArithWithCasts @Interp_gen_RewriteToFancyWithCasts @Interp_PartialEvaluate @Interp_RewriteArith @Interp_RewriteNBE @Interp_RewriteToFancy @Interp_RewriteArithWithCasts @Interp_RewriteToFancyWithCasts : interp. End Compilers. diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 978c49189..04e65dee3 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -54,6 +54,14 @@ Module Compilers. Lemma arith_rewrite_head_eq max_const_val : @arith_rewrite_head max_const_val = (fun var => @arith_rewrite_head0 var max_const_val). Proof. reflexivity. Qed. + Lemma fancy_with_casts_rewrite_head_eq (*invert_low invert_high*) + : (fun var do_again => @fancy_with_casts_rewrite_head (*invert_low invert_high*) var) + = (fun var => @fancy_with_casts_rewrite_head0 var (*invert_low invert_high*)). + Proof. reflexivity. Qed. + + Lemma arith_with_casts_rewrite_head_eq : (fun var _ => @arith_with_casts_rewrite_head var) = @arith_with_casts_rewrite_head0. + Proof. reflexivity. Qed. + Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules. Proof. reflexivity. Qed. @@ -63,6 +71,12 @@ Module Compilers. Lemma arith_all_rewrite_rules_eq : @arith_all_rewrite_rules = @arith_rewrite_rules. Proof. reflexivity. Qed. + Lemma fancy_with_casts_all_rewrite_rules_eq : @fancy_with_casts_all_rewrite_rules = @fancy_with_casts_rewrite_rules. + Proof. reflexivity. Qed. + + Lemma arith_with_casts_all_rewrite_rules_eq : @arith_with_casts_all_rewrite_rules = @arith_with_casts_rewrite_rules. + Proof. reflexivity. Qed. + Section good. Context {var1 var2 : type -> Type}. @@ -336,6 +350,13 @@ Module Compilers. Time all: repeat good_t_step. Qed. + Lemma arith_with_casts_rewrite_rules_good + : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules. + Proof using Type. + Time start_good. + Time all: repeat good_t_step. + Qed. + Lemma fancy_rewrite_rules_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)) @@ -347,6 +368,18 @@ Module Compilers. all: cbv [Option.bind]. Time all: repeat good_t_step. Qed. + + Lemma fancy_with_casts_rewrite_rules_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_goodT (fancy_with_casts_rewrite_rules (*invert_low invert_high*)) (fancy_with_casts_rewrite_rules (*invert_low invert_high*)). + Proof using Type. + Time start_good. + Time all: repeat good_t_step. + all: cbv [Option.bind]. + Time all: repeat good_t_step. + Qed. End good. End RewriteRules. End Compilers. diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index df35ffd40..3a7bef3e7 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -24,6 +24,8 @@ Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.ZUtil.MulSplit. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZRange.BasicLemmas. Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. @@ -128,6 +130,7 @@ Module Compilers. | match goal with | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand + | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence end | progress cbn [expr.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 * @@ -160,10 +163,19 @@ Module Compilers. => 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) + | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ] + => rewrite ZRange.normalize_idempotent in H + | [ |- context[ZRange.normalize (ZRange.normalize _)] ] + => rewrite ZRange.normalize_idempotent + | [ |- context[ident.cast (ZRange.normalize ?r)] ] + => rewrite ident.cast_normalize + | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ] + => rewrite ident.cast_normalize in H end | progress intros | progress subst | progress inversion_option + | progress destruct_head'_and | progress Z.ltb_to_lt | progress split_andb | match goal with @@ -279,6 +291,19 @@ Module Compilers. end | break_innermost_match_step | break_innermost_match_hyps_step + | progress destruct_head'_or + | match goal with + | [ |- context[ident.cast ?coor ?r ?v] ] + => is_var v; + pose proof (@ident.cast_always_bounded coor r v); + generalize dependent (ident.cast coor r v); clear v; intro v; intros + | [ |- context[ident.cast ?coor ?r ?v] ] + => is_var v; is_var coor; + pose proof (@ident.cast_cases coor r v); + generalize dependent (ident.cast coor r v); intros + | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ] + => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than) + end | match goal with | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ] @@ -433,6 +458,13 @@ subgoal 9 (ID 33473) is: 1-9: exact admit. Qed. + Lemma arith_with_casts_rewrite_rules_interp_good + : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. + Proof using Type. + Time start_interp_good. + Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. + Qed. + Local Ltac fancy_local_t := repeat first [ match goal with | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, @@ -524,6 +556,16 @@ subgoal 16 (ID 105431) is: *) 1-16: exact admit. Qed. + + Lemma fancy_with_casts_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_with_casts_rewrite_rules (*invert_low invert_high*)). + Proof using Type. + Time start_interp_good. + Time all: repeat interp_good_t_step. + Qed. End with_cast. End RewriteRules. End Compilers. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 74370aaea..59ce4a33e 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -713,7 +713,13 @@ Module Pipeline. let E := FromFlat e in let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in match E' with - | inl E => Success E + | inl E + => let E := RewriteRules.RewriteArithWithCasts E in + let E := match translate_to_fancy with + | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancyWithCasts invert_low invert_high E + | None => E + end in + Success E | inr (inl (b, E)) => Error (Computed_bounds_are_not_tight_enough b out_bounds E arg_bounds) | inr (inr unsupported_casts) @@ -844,15 +850,16 @@ Module Pipeline. | [ |- Wf _ ] => idtac | _ => eassumption || reflexivity end.. ]. - { subst; split; [ | assumption ]. + { subst; split; [ | solve [ wf_interp_t ] ]. split_and; simpl in *. - split; [ solve [ eauto with nocore ] | ]. - { intros; match goal with H : context[type.app_curried _ _ = _] |- _ => erewrite H; clear H end; eauto. - transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1). - { apply type.app_curried_Proper; [ | symmetry; eassumption ]. - clear dependent arg1; clear dependent arg2; clear dependent out_bounds. - wf_interp_t. } - { apply Interp_PartialEvaluateWithListInfoFromBounds; auto. } } } + split; [ solve [ wf_interp_t; eauto with nocore ] | ]. + intros; break_innermost_match; autorewrite with interp; try solve [ wf_interp_t ]; [ | ]. + all: match goal with H : context[type.app_curried _ _ = _] |- _ => erewrite H; clear H end; eauto. + all: transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1); + [ | apply Interp_PartialEvaluateWithListInfoFromBounds; auto ]. + all: apply type.app_curried_Proper; [ | symmetry; eassumption ]. + all: clear dependent arg1; clear dependent arg2; clear dependent out_bounds. + all: wf_interp_t. } { wf_interp_t. } } Qed. |