From 067d1f14b03d83dcb1c0a60808919ceff6205836 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 Apr 2019 16:43:48 -0400 Subject: Automate more of the rewriter reification, proof Now we actually make use of the rewrite-rule-specific proofs, rather than duplicating them inline. We now support reifying `ident.gets_inlined` to `SubstVarLike.is_var_fst_snd_pair_opp_cast`. We also now fix a bug where we previously incorrectly substituted context variables when reifying side conditions (needed for correct reification of split-mul things, coming up soon). Things are unfortunately a bit slow. I'm not sure what's up with my proof of `reflect_ident_iota_interp_related`; it seems more complicated than it should be (maybe partly due to funext concerns). Next up is to split out the rewrite rule generation bits into separate files and have a single tactic that builds the entire package for us (in prep for making the rewriter builder a vernacular). After that I want to more fully parameterize things over `ident`, and then also over the non-container base-types (which will require some reworking of how we handle special identifiers). Additionally, I want to make the rewrite rule definitions not depend on Language.v. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m50.18s | Total | 23m01.24s || -2m11.06s | -9.48% ----------------------------------------------------------------------------------------------- 0m27.24s | RewriterRulesGood.vo | 1m34.94s || -1m07.70s | -71.30% 0m54.89s | RewriterRulesInterpGood.vo | 1m57.72s || -1m02.82s | -53.37% 1m37.88s | RewriterWf2.vo | 1m47.69s || -0m09.81s | -9.10% 1m16.71s | Rewriter.vo | 1m12.61s || +0m04.10s | +5.64% 0m37.14s | ExtractionHaskell/unsaturated_solinas | 0m40.06s || -0m02.92s | -7.28% 0m36.10s | RewriterWf1.vo | 0m33.12s || +0m02.98s | +8.99% 0m18.31s | p256_32.c | 0m20.70s || -0m02.39s | -11.54% 1m43.31s | Fancy/Barrett256.vo | 1m42.09s || +0m01.21s | +1.19% 0m32.46s | ExtractionHaskell/saturated_solinas | 0m30.92s || +0m01.53s | +4.98% 0m23.44s | ExtractionOCaml/word_by_word_montgomery | 0m22.26s || +0m01.17s | +5.30% 0m12.17s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.58s || -0m01.41s | -10.38% 0m10.04s | p224_32.c | 0m08.20s || +0m01.83s | +22.43% 0m09.98s | ExtractionOCaml/saturated_solinas | 0m11.67s || -0m01.68s | -14.48% 0m07.80s | ExtractionOCaml/saturated_solinas.ml | 0m06.16s || +0m01.63s | +26.62% 0m06.87s | ExtractionHaskell/saturated_solinas.hs | 0m04.98s || +0m01.88s | +37.95% 3m23.11s | p384_32.c | 3m22.61s || +0m00.50s | +0.24% 0m59.32s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || +0m00.56s | +0.95% 0m46.19s | p521_32.c | 0m47.16s || -0m00.96s | -2.05% 0m45.26s | RewriterInterpProofs1.vo | 0m45.64s || -0m00.38s | -0.83% 0m39.50s | p521_64.c | 0m38.97s || +0m00.53s | +1.36% 0m36.38s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.00s || +0m00.38s | +1.05% 0m34.40s | Fancy/Montgomery256.vo | 0m34.63s || -0m00.23s | -0.66% 0m26.95s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.44s || +0m00.50s | +1.92% 0m25.62s | SlowPrimeSynthesisExamples.vo | 0m26.04s || -0m00.41s | -1.61% 0m24.39s | RewriterRulesProofs.vo | 0m24.18s || +0m00.21s | +0.86% 0m20.49s | PushButtonSynthesis/BarrettReduction.vo | 0m20.62s || -0m00.13s | -0.63% 0m18.54s | p448_solinas_64.c | 0m19.15s || -0m00.60s | -3.18% 0m17.37s | secp256k1_32.c | 0m17.70s || -0m00.32s | -1.86% 0m14.80s | p434_64.c | 0m14.16s || +0m00.64s | +4.51% 0m14.05s | ExtractionOCaml/unsaturated_solinas | 0m14.28s || -0m00.22s | -1.61% 0m09.17s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.58s || -0m00.41s | -4.27% 0m08.47s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.22s || +0m00.25s | +3.04% 0m07.69s | p384_64.c | 0m07.72s || -0m00.02s | -0.38% 0m06.80s | BoundsPipeline.vo | 0m06.65s || +0m00.14s | +2.25% 0m06.49s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.59s || +0m00.90s | +16.10% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.08s | +2.31% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.36s || -0m00.00s | -0.29% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.15s || +0m00.04s | +1.26% 0m02.79s | curve25519_32.c | 0m03.32s || -0m00.52s | -15.96% 0m02.66s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s || -0m00.06s | -2.56% 0m02.55s | RewriterRules.vo | 0m02.52s || +0m00.02s | +1.19% 0m01.98s | curve25519_64.c | 0m01.57s || +0m00.40s | +26.11% 0m01.78s | p224_64.c | 0m01.30s || +0m00.48s | +36.92% 0m01.60s | secp256k1_64.c | 0m01.74s || -0m00.13s | -8.04% 0m01.45s | p256_64.c | 0m01.55s || -0m00.10s | -6.45% 0m01.34s | RewriterProofs.vo | 0m01.16s || +0m00.18s | +15.51% 0m01.33s | CLI.vo | 0m01.40s || -0m00.06s | -4.99% 0m01.12s | StandaloneOCamlMain.vo | 0m01.09s || +0m00.03s | +2.75% 0m01.10s | CompilersTestCases.vo | 0m01.08s || +0m00.02s | +1.85% 0m01.08s | StandaloneHaskellMain.vo | 0m01.02s || +0m00.06s | +5.88% --- src/Rewriter.v | 888 +++++++++++++++++----------------- src/RewriterInterpProofs1.v | 46 -- src/RewriterProofs.v | 64 ++- src/RewriterRules.v | 3 + src/RewriterRulesGood.v | 199 ++------ src/RewriterRulesInterpGood.v | 1064 ++++++++++------------------------------- src/RewriterWf1.v | 496 +++++++++++++++++-- 7 files changed, 1221 insertions(+), 1539 deletions(-) diff --git a/src/Rewriter.v b/src/Rewriter.v index 770a7f391..05a802ddd 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -19,6 +19,8 @@ Require Import Crypto.UnderLets. Require Import Crypto.GENERATEDIdentifiersWithoutTypes. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Util.Tactics.DebugPrint. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. @@ -1240,6 +1242,7 @@ Module Compilers. end end%option. + (* only returns [None] if the fuel runs out *) Fixpoint compile_rewrites' (fuel : nat) (pattern_matrix : list (nat * list rawpattern)) : option decision_tree := match fuel with @@ -1278,6 +1281,28 @@ Module Compilers. Global Arguments rew_under_lets {_ _ _ _ _ _} _. Global Arguments rew_replacement {_ _ _ _ _ _} _. + Ltac compute_with_fuel f fuel := + lazymatch (eval compute in (f fuel)) with + | Some ?res => res + | None => compute_with_fuel f (10 + fuel * 10)%nat + | ?res => fail 0 "Invalid result of computing" f "with fuel" fuel ":" res + end. + + Ltac compile_rewrites ident var pident pident_arg_types raw_pident strip_types raw_pident_beq ps + := compute_with_fuel (fun fuel : nat => @compile_rewrites ident var pident pident_arg_types raw_pident strip_types raw_pident_beq fuel ps) 100%nat (* initial value of depth of patterns; doesn't matter too much *). + Ltac CompileRewrites ident pident pident_arg_types raw_pident strip_types raw_pident_beq ps := + let var := fresh "var" in + let res + := lazymatch constr:( + fun var : Compilers.type.type Compilers.base.type -> Type + => ltac:(let res := compile_rewrites ident var pident pident_arg_types raw_pident strip_types raw_pident_beq (ps var) in + exact res)) + with + | fun _ => ?res => res + end in + let dtree := fresh "dtree" in + cache_term res dtree. + Section full. Context {var : type.type base.type -> Type}. Local Notation expr := (@expr base.type ident). @@ -1557,15 +1582,15 @@ Module Compilers. then UnderLets.Base e else reify_expr_beta_iota e)%under_lets. - Fixpoint pair'_unification_resultT' {evm t p} - : @unification_resultT' (fun _ => positive) t p evm -> @unification_resultT' value t p evm -> PositiveMap.t { t : _ & value t } * list bool -> PositiveMap.t { t : _ & value t } * list bool - := match p return @unification_resultT' (fun _ => positive) _ p evm -> @unification_resultT' value _ p evm -> PositiveMap.t { t : _ & value t } * list bool -> PositiveMap.t { t : _ & value t } * list bool with + Fixpoint pair'_unification_resultT' {A evm t p} + : @unification_resultT' (fun _ => positive) t p evm -> @unification_resultT' value t p evm -> PositiveMap.t { t : _ & value t } * (A -> list bool) -> PositiveMap.t { t : _ & value t } * (A -> list bool) + := match p return @unification_resultT' (fun _ => positive) _ p evm -> @unification_resultT' value _ p evm -> PositiveMap.t { t : _ & value t } * (A -> list bool) -> PositiveMap.t { t : _ & value t } * (A -> list bool) with | pattern.Wildcard t => fun p v '(m, l) => (PositiveMap.add p (existT value _ v) m, l) - | pattern.Ident t idc => fun v1 v2 '(m, l) => (m, pident_type_of_list_arg_types_beq t idc v2 v1 :: l) + | pattern.Ident t idc => fun v1 v2 '(m, l) => (m, fun a => pident_type_of_list_arg_types_beq t idc v2 v1 :: l a) | pattern.App _ _ F X => fun x y '(m, l) - => let '(m, l) := @pair'_unification_resultT' _ _ F (fst x) (fst y) (m, l) in - let '(m, l) := @pair'_unification_resultT' _ _ X (snd x) (snd y) (m, l) in + => let '(m, l) := @pair'_unification_resultT' _ _ _ F (fst x) (fst y) (m, l) in + let '(m, l) := @pair'_unification_resultT' _ _ _ X (snd x) (snd y) (m, l) in (m, l) end. @@ -1592,11 +1617,32 @@ Module Compilers. (fun v => @expr_pos_to_expr_value invalid _ (f cur_i) (PositiveMap.add cur_i (existT value _ v) m) (Pos.succ cur_i)) end. + Inductive lookup_gets_inlined_error_messages := + | NO_SUCH_EXPRESSION_TO_CHECK (p : positive) (m : PositiveMap.t { t : _ & value t }) + | TYPE_IS_NOT_BASE (p : positive) (m : PositiveMap.t { t : _ & value t }) (t : type). + + Definition lookup_expr_gets_inlined + (invalid : forall A B, A -> B) + (gets_inlined : forall t, value (type.base t) -> bool) + (m : PositiveMap.t { t : _ & value t }) + (p : positive) + : bool + := Eval cbv -[value] in + match PositiveMap.find p m with + | Some (existT t e) + => match t return value t -> _ with + | type.base t => gets_inlined t + | _ => invalid _ _ (TYPE_IS_NOT_BASE p m t) + end e + | None => invalid _ _ (NO_SUCH_EXPRESSION_TO_CHECK p m) + end. + Definition expr_to_pattern_and_replacement + (gets_inlined : forall t, value (type.base t) -> bool) (should_do_again : bool) evm (invalid : forall A B, A -> B) {t} (lhs rhs : @expr.expr base.type ident (fun _ => positive) t) - (side_conditions : list bool) + (side_conditions : (positive -> bool) -> list bool) : { p : pattern (pattern.type.relax t) & @with_unif_rewrite_ruleTP_gen' _ p should_do_again true true evm } := let (p, unif_data_lhs) := @pattern_of_expr evm (fun _ => invalid _ _) t lhs in existT @@ -1610,6 +1656,7 @@ Module Compilers. (lam_unification_resultT' (fun unif_data_new => let '(value_map, side_conditions) := pair'_unification_resultT' unif_data_lhs unif_data_new (PositiveMap.empty _, side_conditions) in + let side_conditions := side_conditions (lookup_expr_gets_inlined invalid gets_inlined value_map) in let start_i := Pos.succ (PositiveMap.fold (fun k _ max => Pos.max k max) value_map 1%positive) in let replacement := expr_pos_to_expr_value (fun _ => invalid _ _) rhs value_map start_i in let replacement := expr_value_to_rewrite_rule_replacement should_do_again replacement in @@ -1618,9 +1665,9 @@ Module Compilers. else None))). - Definition expr_to_pattern_and_replacement_unfolded should_do_again evm invalid {t} lhs rhs side_conditions - := Eval cbv beta iota delta [expr_to_pattern_and_replacement pattern_of_expr lam_unification_resultT' Pos.succ pair'_unification_resultT' PositiveMap.empty PositiveMap.fold Pos.max expr_pos_to_expr_value (* expr_value_to_rewrite_rule_replacement*) fold_left List.rev List.app value PositiveMap.add PositiveMap.xfoldi Pos.compare Pos.compare_cont FMapPositive.append projT1 projT2 PositiveMap.find Base_value (*UnderLets.map reify_expr_beta_iota reflect_expr_beta_iota*) lam_type_of_list fold_right list_rect pattern.type.relax pattern.type.subst_default pattern.type.subst_default_relax pattern.type.unsubst_default_relax option_map unification_resultT' with_unification_resultT' with_unif_rewrite_ruleTP_gen'] - in @expr_to_pattern_and_replacement should_do_again evm invalid t lhs rhs side_conditions. + Definition expr_to_pattern_and_replacement_unfolded gets_inlined should_do_again evm invalid {t} lhs rhs side_conditions + := Eval cbv beta iota delta [expr_to_pattern_and_replacement lookup_expr_gets_inlined pattern_of_expr lam_unification_resultT' Pos.succ pair'_unification_resultT' PositiveMap.empty PositiveMap.fold Pos.max expr_pos_to_expr_value (* expr_value_to_rewrite_rule_replacement*) fold_left List.rev List.app value PositiveMap.add PositiveMap.xfoldi Pos.compare Pos.compare_cont FMapPositive.append projT1 projT2 PositiveMap.find Base_value (*UnderLets.map reify_expr_beta_iota reflect_expr_beta_iota*) lam_type_of_list fold_right list_rect pattern.type.relax pattern.type.subst_default pattern.type.subst_default_relax pattern.type.unsubst_default_relax option_map unification_resultT' with_unification_resultT' with_unif_rewrite_ruleTP_gen'] + in @expr_to_pattern_and_replacement gets_inlined should_do_again evm invalid t lhs rhs side_conditions. Definition partial_lam_unif_rewrite_ruleTP_gen_unfolded should_do_again {t} p := Eval cbv beta iota delta [partial_lam_unif_rewrite_ruleTP_gen pattern.collect_vars pattern.type.lam_forall_vars partial_lam_unification_resultT pattern.type.collect_vars pattern.base.collect_vars PositiveSet.union PositiveSet.add PositiveSet.empty pattern.type.lam_forall_vars_gen List.rev PositiveSet.elements PositiveSet.xelements PositiveSet.rev PositiveSet.rev_append List.app orb fold_right PositiveMap.add PositiveMap.empty] @@ -1809,31 +1856,39 @@ Module Compilers. | _ => term end. - Ltac under_binders term cont ctx := + Ltac under_binders payload term cont ctx := lazymatch term with | (fun x : ?T => ?f) => let ctx' := fresh in let f' := fresh in - constr:(fun x : T - => match f, dyncons x ctx return _ with - | f', ctx' - => ltac:(let ctx := (eval cbv delta [ctx'] in ctx') in - let f := (eval cbv delta [f'] in f') in - clear f' ctx'; - let res := under_binders f cont ctx in - exact res) - end) - | ?term => cont ctx term + let payload' := fresh in (* COQBUG(https://github.com/coq/coq/issues/7210#issuecomment-470009463) *) + constr:(match payload return _ with + | payload' + => fun x : T + => match f, dyncons x ctx return _ with + | f', ctx' + => ltac:(let ctx := (eval cbv delta [ctx'] in ctx') in + let f := (eval cbv delta [f'] in f') in + let payload := (eval cbv delta [payload'] in payload') in + clear f' ctx' payload'; + let res := under_binders payload f cont ctx in + exact res) + end + end) + | ?term => cont payload ctx term end. Ltac substitute_with term x y := lazymatch (eval pattern y in term) with | (fun z => ?term) _ => constr:(match x return _ with z => term end) end. - Ltac substitute_beq_with full_ctx term beq x := + Ltac substitute_beq_with only_eliminate_in_ctx full_ctx term beq x := let is_good y := lazymatch full_ctx with | context[dyncons y _] => fail - | _ => is_var y + | _ => is_var y; + lazymatch only_eliminate_in_ctx with + | context[y] => idtac + end end in let y := match term with | context term' [beq x ?y] @@ -1888,7 +1943,7 @@ Module Compilers. | _ => term end. - Ltac substitute_beq full_ctx ctx term := + Ltac substitute_beq only_eliminate_in_ctx full_ctx ctx term := lazymatch ctx with | dynnil => let term := (eval cbv [base.interp_beq base.base_interp_beq] in term) in @@ -1897,41 +1952,59 @@ Module Compilers. let term := adjust_if_negb term in term | dyncons ?v ?ctx - => let term := substitute_beq_with full_ctx term zrange_beq v in - let term := substitute_beq_with full_ctx term Z.eqb v in + => let term := substitute_beq_with only_eliminate_in_ctx full_ctx term zrange_beq v in + let term := substitute_beq_with only_eliminate_in_ctx full_ctx term Z.eqb v in let term := match constr:(Set) with | _ => let T := type of v in let beq := (eval cbv beta delta [Reflect.decb_rel] in (Reflect.decb_rel (@eq T))) in - substitute_beq_with full_ctx term beq v + substitute_beq_with only_eliminate_in_ctx full_ctx term beq v | _ => term end in - substitute_beq full_ctx ctx term + substitute_beq only_eliminate_in_ctx full_ctx ctx term end. - Ltac deep_substitute_beq term := + Ltac deep_substitute_beq only_eliminate_in_ctx term := lazymatch term with | context term'[@Build_rewrite_rule_data ?ident ?var ?pident ?pident_arg_types ?t ?p ?sda ?wo ?ul ?subterm] - => let subterm := under_binders subterm ltac:(fun ctx term => substitute_beq ctx ctx term) dynnil in + => let subterm := under_binders only_eliminate_in_ctx subterm ltac:(fun only_eliminate_in_ctx ctx term => substitute_beq only_eliminate_in_ctx ctx ctx term) dynnil in let term := context term'[@Build_rewrite_rule_data ident var pident pident_arg_types t p sda wo ul subterm] in term end. - Ltac clean_beq term := + Ltac clean_beq only_eliminate_in_ctx term := let term := (eval cbn [Prod.prod_beq] in term) in let term := (eval cbv [ident.literal] in term) in - let term := deep_substitute_beq term in + let term := deep_substitute_beq only_eliminate_in_ctx term in let term := (eval cbv [base.interp_beq base.base_interp_beq] in term) in let term := remove_andb_true term in term. + Ltac adjust_side_conditions_for_gets_inlined' value_ctx side_conditions lookup_gets_inlined := + lazymatch side_conditions with + | context sc[ident.gets_inlined _ ?x] + => lazymatch value_ctx with + | context[expr.var_context.cons x ?p _] + => let rep := constr:(lookup_gets_inlined p) in + let side_conditions := context sc[rep] in + adjust_side_conditions_for_gets_inlined' value_ctx side_conditions lookup_gets_inlined + | _ => constr_fail_with ltac:(fun _ => fail 1 "Could not find an expression corresponding to" x "in context" value_ctx) + end + | _ => side_conditions + end. + + Ltac adjust_side_conditions_for_gets_inlined value_ctx side_conditions := + let lookup_gets_inlined := fresh in + constr:(fun lookup_gets_inlined : positive -> bool + => ltac:(let v := adjust_side_conditions_for_gets_inlined' value_ctx side_conditions lookup_gets_inlined in + exact v)). - Ltac reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota type_ctx var should_do_again cur_i term value_ctx := + Ltac reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota type_ctx var gets_inlined should_do_again cur_i term value_ctx := let t := fresh "t" in let p := fresh "p" in - let reify_rec_gen type_ctx := reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota type_ctx var should_do_again in + let reify_rec_gen type_ctx := reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota type_ctx var gets_inlined should_do_again in let var_pos := constr:(fun _ : type base.type => positive) in let value := constr:(@value base.type ident var) in - let cexpr_to_pattern_and_replacement_unfolded := constr:(@expr_to_pattern_and_replacement_unfolded ident var pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident (reflect_ident_iota var) should_do_again type_ctx) in + let cexpr_to_pattern_and_replacement_unfolded := constr:(@expr_to_pattern_and_replacement_unfolded ident var pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident (reflect_ident_iota var) gets_inlined should_do_again type_ctx) in let cpartial_lam_unif_rewrite_ruleTP_gen := constr:(@partial_lam_unif_rewrite_ruleTP_gen_unfolded ident var pident pident_arg_types should_do_again) in let cwith_unif_rewrite_ruleTP_gen := constr:(fun t p => @with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types value t p should_do_again true true) in lazymatch term with @@ -1965,6 +2038,7 @@ Module Compilers. | (@eq ?T ?A ?B, ?side_conditions) => let rA := expr.reify_in_context base.type ident ltac:(base.reify) reify_ident var_pos A value_ctx tt in let rB := expr.reify_in_context base.type ident ltac:(base.reify) reify_ident var_pos B value_ctx tt in + let side_conditions := adjust_side_conditions_for_gets_inlined value_ctx side_conditions in let invalid := fresh "invalid" in let res := constr:(fun invalid => cexpr_to_pattern_and_replacement_unfolded invalid _ rA rB side_conditions) in let res := (eval cbv [expr_to_pattern_and_replacement_unfolded pident_arg_types pident_of_typed_ident pident_type_of_list_arg_types_beq pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in @@ -2005,29 +2079,29 @@ Module Compilers. (@rewrite_ruleTP ident var pident pident_arg_types) {| pattern.pattern_of_anypattern := projT1 res |} {| rew_replacement := projT2 res |})) in - let res := clean_beq res in + let res := clean_beq value_ctx res in res end. - Ltac reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var should_do_again lem := + Ltac reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var gets_inlined should_do_again lem := reify_under_forall_types lem ltac:( fun ty_ctx cur_i lem => let lem := equation_to_parts lem in - let res := reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota ty_ctx var should_do_again constr:(1%positive) lem (@expr.var_context.nil base.type (fun _ => positive)) in + let res := reify_to_pattern_and_replacement_in_context ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota ty_ctx var gets_inlined should_do_again constr:(1%positive) lem (@expr.var_context.nil base.type (fun _ => positive)) in res). - Ltac Reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota should_do_again lem := + Ltac Reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota gets_inlined should_do_again lem := let var := fresh "var" in constr:(fun var : Compilers.type.type Compilers.base.type -> Type - => ltac:(let res := reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var should_do_again lem in + => ltac:(let res := reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var (gets_inlined var) should_do_again lem in exact res)). (* lems is either a list of [Prop]s, or a list of [bool (* should_do_again *) * Prop] *) - Ltac reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var lems := - let reify' := reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var in - let reify_list_rec := reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var in + Ltac reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var gets_inlined lems := + let reify' := reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var gets_inlined in + let reify_list_rec := reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var gets_inlined in lazymatch (eval hnf in lems) with | (?b, ?lem) :: ?lems => let rlem := reify' b lem in @@ -2041,10 +2115,10 @@ Module Compilers. reify_list_rec lems end. - Ltac Reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota lems := + Ltac Reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota gets_inlined lems := let var := fresh "var" in constr:(fun var : Compilers.type.type Compilers.base.type -> Type - => ltac:(let res := reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var lems in + => ltac:(let res := reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var (gets_inlined var) lems in exact res)). End Reify. @@ -2292,245 +2366,293 @@ Module Compilers. := Eval cbv [interp_rewrite_rules' ident.interp ident.gen_interp ident.smart_Literal] in interp_rewrite_rules'. End make_rewrite_rules. - End Make. - Section with_var. - Import Compile. - Context {var : type.type base.type -> Type}. - Local Notation type := (type.type base.type). - Local Notation expr := (@expr.expr base.type ident var). - Local Notation value := (@value base.type ident var). - Local Notation pattern := (@pattern.pattern pattern.ident). - Local Notation UnderLets := (@UnderLets.UnderLets base.type ident var). - Local Notation ptype := (type.type pattern.base.type). - Let type_base (t : base.type) : type := type.base t. - Let ptype_base (t : pattern.base.type) : ptype := type.base t. - Let ptype_base' (t : base.type.base) : ptype := @type.base pattern.base.type t. - Coercion ptype_base' : base.type.base >-> ptype. - Coercion type_base : base.type >-> type. - Coercion ptype_base : pattern.base.type >-> ptype. - Local Notation Build_rewrite_rule_data := (@Build_rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types)). - Local Notation Build_anypattern := (@pattern.Build_anypattern pattern.ident). - Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)). - Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types)). - Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types)). + Module Import AdjustRewriteRulesForReduction. + Import PrimitiveHList. + (* N.B. The [combine_hlist] call MUST eta-expand + [pr2_rewrite_rules]. That is, it MUST NOT block reduction + of the resulting list of cons cells on the pair-structure + of [pr2_rewrite_rules]. This is required so that we can + use [cbv -] to unfold the entire decision tree + evaluation, including choosing which rewrite rule to apply + and binding its arguments, without unfolding any of the + identifiers used to define the replacement value. (The + symptom of messing this up is that the [cbv -] will run out + of memory when trying to reduce things.) We accomplish + this by making [hlist] based on a primitive [prod] type + with judgmental η, so that matching on its structure never + blocks reduction. *) + Ltac make_split_rewrite_rules rewrite_rules := + let split_rewrite_rules := fresh "split_rewrite_rules" in + let v := constr:(fun var => split_list (rewrite_rules var)) in + let h := head rewrite_rules in + let do_reduce_rules := lazymatch h with + | @cons => false + | @nil => false + | _ => true + end in + let v := lazymatch do_reduce_rules with + | true => (eval cbv [split_list projT1 projT2 h] in v) + | false => (eval cbv [split_list projT1 projT2] in v) + end in + cache_term v split_rewrite_rules. + Ltac make_pr1_rewrite_rules split_rewrite_rules := + let var := fresh "var" in + constr:(fun var => ltac:(let v := (eval hnf in (projT1 (split_rewrite_rules var))) in + exact v)). + Ltac make_pr2_rewrite_rules split_rewrite_rules := + let pr2_rewrite_rules := fresh "pr2_rewrite_rules" in + let var := fresh "var" in + let v := + constr:(fun var + => ltac:(let v := (eval hnf in (projT2 (split_rewrite_rules var))) in + exact v)) in + cache_term v pr2_rewrite_rules. + + Ltac make_all_rewrite_rules pr1_rewrite_rules pr2_rewrite_rules := + let all_rewrite_rules := fresh "all_rewrite_rules" in + let var := fresh "var" in + cache_term + (fun var + => combine_hlist (P:=@Compile.rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)) (pr1_rewrite_rules var) (pr2_rewrite_rules var)) + all_rewrite_rules. + End AdjustRewriteRulesForReduction. + + Ltac rewriter_assembly_debug_level := constr:(1%nat). + + Ltac check_debug_level_then_Set _ := + let lvl := rewriter_assembly_debug_level in + lazymatch type of lvl with + | nat => constr:(Set) + | ?T => constr_run_tac ltac:(fun _ => idtac "Error: rewriter_assembly_debug_level should have type nat but instead has type" T) + end. + Ltac debug0 tac := + constr_run_tac tac. + Ltac debug1 tac := + let lvl := rewriter_assembly_debug_level in + lazymatch lvl with + | S _ => constr_run_tac tac + | _ => check_debug_level_then_Set () + end. + + Module Export GoalType. + Record rewriter_dataT := + Build_rewriter_dataT' + { + rewrite_rules_specs : list (bool * Prop); + dummy_count : nat; + + rewrite_rules : forall var, @Compile.rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types) ; + all_rewrite_rules (* adjusted version *) : _; + all_rewrite_rules_eq : all_rewrite_rules = rewrite_rules; + + default_fuel : nat; + + rewrite_head0 : forall var (do_again : forall t, @defaults.expr (@Compile.value _ ident var) (type.base t) -> @UnderLets.UnderLets _ ident var (@defaults.expr var (type.base t))) + t (idc : ident t), @Compile.value_with_lets base.type ident var t; + rewrite_head (* adjusted version *) : _; + rewrite_head_eq : rewrite_head = rewrite_head0 + }. + End GoalType. + Definition Rewrite (data : rewriter_dataT) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t + := @Compile.Rewrite (rewrite_head data) (default_fuel data) t e. + + Ltac Reify include_interp specs := + let lems := Reify.Reify_list ident ident.reify pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_of_list_arg_types_beq) (@pattern.ident.of_typed_ident) (@pattern.ident.arg_types_of_typed_ident) (@Compile.reflect_ident_iota) (fun var t => @SubstVarLike.is_var_fst_snd_pair_opp_cast var (type.base t)) specs in + lazymatch include_interp with + | true + => let myapp := (eval cbv [List.app] in (@List.app)) in + let res := (eval cbv [interp_rewrite_rules] in + (fun var => myapp _ (@interp_rewrite_rules var) (lems var))) in + let len := lazymatch (eval compute in (fun var => List.length (@interp_rewrite_rules var))) with (fun _ => ?n) => n end in + let adjusted_specs := (eval cbv [List.app List.repeat] in + (List.app + (List.repeat (false, forall A (x : A), x = x) len))) in + constr:((len, adjusted_specs specs, res)) + | false => constr:((O, specs, lems)) + | _ => constr_fail_with ltac:(fun _ => fail 1 "Invalid value for include_interp (must be either true or false):" include_interp) + end. + Definition pident_unify_unknown := @pattern.ident.unify. Definition invert_bind_args_unknown := @pattern.Raw.ident.invert_bind_args. - Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple). - - Ltac reify lems := - Reify.reify_list ident ident.reify pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_of_list_arg_types_beq) (@pattern.ident.of_typed_ident) (@pattern.ident.arg_types_of_typed_ident) (@reflect_ident_iota) var lems. - (* Play games with [match] to get [lems] interpreted as a constr rather than an ident when it's not closed, to get better error messages *) - Local Notation reify lems - := (match lems return _ with - | _LEMS => ltac:(let LEMS := (eval cbv delta [_LEMS] in _LEMS) in let res := reify LEMS in exact res) - end) (only parsing). - - Delimit Scope rewrite_scope with rewrite. - Delimit Scope rewrite_opt_scope with rewrite_opt. - Delimit Scope rewrite_lets_scope with rewrite_lets. - Local Open Scope rewrite_opt_scope. - Local Open Scope rewrite_lets_scope. - Local Open Scope rewrite_scope. - - Notation make_rewrite_gen should_do_again with_opt under_lets p f - := (existT - rewrite_ruleTP - (@Build_anypattern _ p%pattern) - (@Build_rewrite_rule_data _ p%pattern should_do_again with_opt under_lets f)). - (* %cps%option%under_lets *) - Notation make_rewrite p f - := (make_rewrite_gen false false false p f%rewrite%expr%list%Z%bool). - Notation make_rewritel p f - := (make_rewrite_gen false false true p f%rewrite_lets%rewrite%expr%list%Z%bool%under_lets). - Notation make_rewriteo p f - := (make_rewrite_gen false true false p f%rewrite_opt%rewrite%expr%list%Z%bool). - Notation make_rewriteol p f - := (make_rewrite_gen false true true p f%rewrite_lets%rewrite_opt%rewrite%expr%list%Z%bool%under_lets). - Notation make_rewrite_step p f - := (make_rewrite_gen true false false p f%rewrite%expr%list%Z%bool). - Notation make_rewritel_step p f - := (make_rewrite_gen true false true p f%rewrite_lets%rewrite%expr%list%Z%bool%under_lets). - Notation make_rewriteo_step p f - := (make_rewrite_gen true true false p f%rewrite_opt%rewrite%expr%list%Z%bool). - Notation make_rewriteol_step p f - := (make_rewrite_gen true true true p f%rewrite_lets%rewrite_opt%rewrite%expr%list%Z%bool%under_lets). - Let UnderLetsExpr {btype bident ivar} t := @UnderLets.UnderLets base.type ident var (@expr.expr btype bident ivar t). - Let OptExpr {btype bident ivar} t := option (@expr.expr btype bident ivar t). - Let OptUnderLetsExpr {btype bident ivar} t := option (@UnderLets.UnderLets base.type ident var (@expr.expr btype bident ivar t)). - Let BaseExpr {btype ident ivar t} : @expr.expr btype ident ivar t -> @UnderLetsExpr btype ident ivar t := UnderLets.Base. - Let SomeExpr {btype ident ivar t} : @expr.expr btype ident ivar t -> @OptExpr btype ident ivar t := Some. - Let SomeUnderLetsExpr {btype ident ivar t} : @UnderLetsExpr btype ident ivar t -> @OptUnderLetsExpr btype ident ivar t := Some. - Coercion BaseExpr : expr >-> UnderLetsExpr. - Coercion SomeExpr : expr >-> OptExpr. - Coercion SomeUnderLetsExpr : UnderLetsExpr >-> OptUnderLetsExpr. - - Local Notation "x <- y ; f" := (Compile.option_bind' y%rewrite_lets%rewrite_opt%rewrite (fun x => f%rewrite_lets%rewrite_opt%rewrite : OptUnderLetsExpr _)) : rewrite_lets_scope. - Local Notation "x <- y ; f" := (Compile.option_bind' y%rewrite_opt%rewrite (fun x => f%rewrite_opt%rewrite : OptExpr _)) : rewrite_opt_scope. - Local Notation "x <-- y ; f" := (UnderLets.splice y%rewrite_lets%rewrite (fun x => (f%rewrite_lets%rewrite : UnderLetsExpr _))) : rewrite_lets_scope. - Local Notation "x <--- y ; f" := (UnderLets.splice_list y%rewrite_lets%rewrite (fun x => (f%rewrite_lets%rewrite : UnderLetsExpr _))) : rewrite_lets_scope. - Local Notation "x <---- y ; f" := (Compile.option_bind' y%rewrite_lets%rewrite_opt%rewrite (fun x => (f%rewrite_lets%rewrite : UnderLetsExpr _) : OptUnderLetsExpr _)) : rewrite_lets_scope. - Local Notation "'llet' x := y 'in' f" := (UnderLets.UnderLet y%rewrite_lets%rewrite (fun x => (f%rewrite_lets%rewrite : UnderLetsExpr _))) : rewrite_lets_scope. - - Definition rlist_rect {A P} - {ivar} - (Pnil : @UnderLetsExpr base.type ident ivar (type.base P)) - (Pcons : expr (type.base A) -> list (expr (type.base A)) -> @expr.expr base.type ident ivar (type.base P) -> @UnderLetsExpr base.type ident ivar (type.base P)) - (e : expr (type.base (base.type.list A))) - : @OptUnderLetsExpr base.type ident ivar P - := (ls <- reflect_list e; - list_rect - (fun _ => UnderLetsExpr (type.base P)) - Pnil - (fun x xs rec => rec' <-- rec; Pcons x xs rec') - ls). - - Definition rwhen {ivar t} (v : @OptExpr base.type ident ivar t) (cond : bool) - : @OptExpr base.type ident ivar t - := if cond then v else None. - Definition rwhenl {ivar t} (v : @OptUnderLetsExpr base.type ident ivar t) (cond : bool) - : @OptUnderLetsExpr base.type ident ivar t - := if cond then v else None. - - Local Notation "e 'when' cond" := (rwhen e%rewrite_opt%rewrite cond) (only parsing, at level 100) : rewrite_opt_scope. - Local Notation "e 'owhen' cond" := (rwhenl e%rewrite_lets%rewrite_opt%rewrite cond) (only parsing, at level 100) : rewrite_lets_scope. - Local Notation "e 'when' cond" := (rwhenl (e%rewrite_lets%rewrite : UnderLetsExpr _) cond) (only parsing, at level 100) : rewrite_lets_scope. - - Local Notation ℤ := base.type.Z. - Local Notation ℕ := base.type.nat. - Local Notation bool := base.type.bool. - Local Notation list := pattern.base.type.list. - Local Notation "' x" := (ident.literal x). - - Local Arguments pattern.anypattern : clear implicits. - Local Arguments Make.interp_rewrite_rules / . - Let myapp {A} := Eval cbv [List.app] in @List.app A. - Let myflatten {A} := Eval cbv in List.fold_right myapp (@nil A). - Definition nbe_rewrite_rules : rewrite_rulesT - := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in - myflatten - [Make.interp_rewrite_rules - ; reify nbe_rewrite_rulesT - ]. - - Definition arith_rewrite_rules (max_const_val : Z) : rewrite_rulesT - := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in - myflatten - [reify (arith_rewrite_rulesT max_const_val) - ; [ - make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp_cast e)) (* inline negation when the rewriter wouldn't already inline it *) - ] ]. - - Definition arith_with_casts_rewrite_rules : rewrite_rulesT - := reify arith_with_casts_rewrite_rulesT. - - Definition strip_literal_casts_rewrite_rules : rewrite_rulesT - := reify strip_literal_casts_rewrite_rulesT. - - - 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 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 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 100 arith_with_casts_rewrite_rules. - Definition strip_literal_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 100 strip_literal_casts_rewrite_rules. - Definition nbe_dtree : decision_tree - := Eval compute in Option.invert_Some nbe_dtree'. - Definition arith_dtree : decision_tree - := Eval compute in Option.invert_Some arith_dtree'. - Definition arith_with_casts_dtree : decision_tree - := Eval compute in Option.invert_Some arith_with_casts_dtree'. - Definition strip_literal_casts_dtree : decision_tree - := Eval compute in Option.invert_Some strip_literal_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. - Definition strip_literal_casts_default_fuel := Eval compute in List.length strip_literal_casts_rewrite_rules. - - Import PrimitiveHList. - (* N.B. The [combine_hlist] call MUST eta-expand - [pr2_rewrite_rules]. That is, it MUST NOT block reduction of - the resulting list of cons cells on the pair-structure of - [pr2_rewrite_rules]. This is required so that we can use - [cbv -] to unfold the entire discrimination tree evaluation, - including choosing which rewrite rule to apply and binding - its arguments, without unfolding any of the identifiers used - to define the replacement value. (The symptom of messing - this up is that the [cbv -] will run out of memory when - trying to reduce things.) We accomplish this by making - [hlist] based on a primitive [prod] type with judgmental η, - so that matching on its structure never blocks reduction. *) - Definition nbe_split_rewrite_rules := Eval cbv [split_list projT1 projT2 nbe_rewrite_rules] in split_list nbe_rewrite_rules. - Definition nbe_pr1_rewrite_rules := Eval hnf in projT1 nbe_split_rewrite_rules. - Definition nbe_pr2_rewrite_rules := Eval hnf in projT2 nbe_split_rewrite_rules. - Definition nbe_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) nbe_pr1_rewrite_rules nbe_pr2_rewrite_rules. - - Definition arith_split_rewrite_rules max_const_val := Eval cbv [split_list projT1 projT2 arith_rewrite_rules] in split_list (arith_rewrite_rules max_const_val). - 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 strip_literal_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 strip_literal_casts_rewrite_rules] in split_list strip_literal_casts_rewrite_rules. - Definition strip_literal_casts_pr1_rewrite_rules := Eval hnf in projT1 strip_literal_casts_split_rewrite_rules. - Definition strip_literal_casts_pr2_rewrite_rules := Eval hnf in projT2 strip_literal_casts_split_rewrite_rules. - Definition strip_literal_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) (strip_literal_casts_pr1_rewrite_rules) strip_literal_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. - Definition strip_literal_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t - := @assemble_identifier_rewriters strip_literal_casts_dtree strip_literal_casts_all_rewrite_rules do_again t idc. - - Section fancy. - Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) - (value_range flag_range : zrange). - Definition fancy_rewrite_rules : rewrite_rulesT - := reify fancy_rewrite_rulesT. - - Definition fancy_with_casts_rewrite_rules : rewrite_rulesT - := reify (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). - - 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 100 fancy_rewrite_rules. - Definition fancy_dtree : decision_tree - := Eval compute in Option.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 100 fancy_with_casts_rewrite_rules. - Definition fancy_with_casts_dtree : decision_tree - := Eval compute in Option.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. + + Ltac make_rewrite_head1 rewrite_head0 pr2_rewrite_rules := + let rewrite_head1 + := (eval cbv -[pr2_rewrite_rules + base.interp base.try_make_transport_cps + type.try_make_transport_cps + pattern.type.unify_extracted + Compile.option_type_type_beq + 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_cast + ] in rewrite_head0) in + let rewrite_head1 + := (eval cbn [type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps] + in rewrite_head1) in + rewrite_head1. + 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.type.subst_default pattern.base.subst_default pattern.base.lookup_default + PositiveMap.add PositiveMap.find PositiveMap.empty + PositiveSet.rev PositiveSet.rev_append + 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.rValueOrExpr + Compile.swap_list + Compile.type_of_rawexpr + Compile.option_type_type_beq + 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 option_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. + + Ltac make_rewrite_head rewrite_head0 pr2_rewrite_rules := + let rewrite_head := fresh "rewrite_head" in + let lvl := rewriter_assembly_debug_level in + let var := fresh "var" in + let do_again := fresh "do_again" in + let t := fresh "t" in + let idc := fresh "idc" in + let v := + constr:( + fun var (do_again : forall t, @defaults.expr (@Compile.value _ ident var) (type.base t) -> @UnderLets.UnderLets _ ident var (@defaults.expr var (type.base t))) + t (idc : ident t) + => ltac:( + let rewrite_head0 := constr:(rewrite_head0 var do_again t idc) in + let pr2_rewrite_rules := head pr2_rewrite_rules in + let v := lazymatch lvl with + | O => make_rewrite_head' rewrite_head0 pr2_rewrite_rules + | S _ => timed_make_rewrite_head' rewrite_head0 pr2_rewrite_rules + end in + exact v)) in + cache_term v rewrite_head. + + Ltac Build_rewriter_dataT include_interp specs := + let __ := debug1 ltac:(fun _ => idtac "Reifying...") in + let specs_lems := Reify include_interp specs in + let dummy_count := lazymatch specs_lems with (?n, ?specs, ?lems) => n end in + let specs := lazymatch specs_lems with (?n, ?specs, ?lems) => specs end in + let rewrite_rules := lazymatch specs_lems with (?n, ?specs, ?lems) => lems end in + let rewrite_rules_names := fresh "rewrite_rules" in + let rewrite_rules := cache_term rewrite_rules rewrite_rules_names in + let __ := debug1 ltac:(fun _ => idtac "Compiling decision tree...") in + let dtree := Compile.CompileRewrites ident pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq rewrite_rules in + let default_fuel := (eval compute in (List.length specs)) in + let __ := debug1 ltac:(fun _ => idtac "Splitting rewrite rules...") in + let split_rewrite_rules := make_split_rewrite_rules rewrite_rules in + let pr1_rewrite_rules := make_pr1_rewrite_rules split_rewrite_rules in + let pr2_rewrite_rules := make_pr2_rewrite_rules split_rewrite_rules in + let all_rewrite_rules := make_all_rewrite_rules pr1_rewrite_rules pr2_rewrite_rules in + let __ := debug1 ltac:(fun _ => idtac "Assembling rewrite_head...") in + let rewrite_head0 := fresh "rewrite_head0" in + let var := fresh "var" in + let rewrite_head0 + := cache_term + (fun var + => @Compile.assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple dtree (all_rewrite_rules var)) + rewrite_head0 in + let __ := debug1 ltac:(fun _ => idtac "Reducing rewrite_head...") in + let rewrite_head := make_rewrite_head rewrite_head0 pr2_rewrite_rules in + refine (@Build_rewriter_dataT' + specs dummy_count + rewrite_rules all_rewrite_rules eq_refl + default_fuel + rewrite_head0 rewrite_head eq_refl). + + Module Export Tactic. + Global Arguments base.try_make_base_transport_cps _ !_ !_. + Global Arguments base.try_make_transport_cps _ !_ !_. + Global Arguments type.try_make_transport_cps _ _ _ !_ !_. + Global Arguments Option.sequence A !v1 v2. + Global Arguments Option.sequence_return A !v1 v2. + Global Arguments Option.bind A B !_ _. + Global Arguments pattern.Raw.ident.invert_bind_args t !_ !_. + Global Arguments base.type.base_beq !_ !_. + Global Arguments id / . + + Tactic Notation "make_rewriter_data" constr(include_interp) constr(specs) := + Build_rewriter_dataT include_interp specs. + End Tactic. + End Make. + Export Make.GoalType. + Import Make.Tactic. + + Definition nbe_rewriter_data : rewriter_dataT. + Proof. make_rewriter_data true nbe_rewrite_rulesT. Defined. + + Definition arith_rewriter_data (max_const_val : Z) : rewriter_dataT. + Proof. make_rewriter_data false (arith_rewrite_rulesT max_const_val). Defined. + + Definition arith_with_casts_rewriter_data : rewriter_dataT. + Proof. make_rewriter_data false arith_with_casts_rewrite_rulesT. Defined. + + Definition strip_literal_casts_rewriter_data : rewriter_dataT. + Proof. make_rewriter_data false strip_literal_casts_rewrite_rulesT. Defined. + + Definition fancy_rewriter_data + (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + : rewriter_dataT. + Proof. make_rewriter_data false fancy_rewrite_rulesT. Defined. + + Definition fancy_with_casts_rewriter_data + (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + (value_range flag_range : zrange) + : rewriter_dataT. + Proof. make_rewriter_data false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined. + Module RewriterPrintingNotations. - Arguments base.try_make_base_transport_cps _ !_ !_. - Arguments base.try_make_transport_cps _ !_ !_. - Arguments type.try_make_transport_cps _ _ _ !_ !_. - Arguments Option.sequence {A} !v1 v2. - Arguments Option.sequence_return {A} !v1 v2. - Arguments Option.bind {A B} !_ _. - Arguments pattern.Raw.ident.invert_bind_args {t} !_ !_. Arguments base.try_make_transport_cps {P} t1 t2 {_} _. Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. Export pattern.Raw.ident. @@ -2546,104 +2668,9 @@ Module Compilers. Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Datatypes.Some x => f | Datatypes.None => Datatypes.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 := - let rewrite_head1 - := (eval cbv -[pr2_rewrite_rules - base.interp base.try_make_transport_cps - type.try_make_transport_cps - pattern.type.unify_extracted - Compile.option_type_type_beq - 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_cast - ] in rewrite_head0) in - let rewrite_head1 - := (eval cbn [type.try_make_transport_cps base.try_make_transport_cps base.try_make_base_transport_cps] - in rewrite_head1) in - rewrite_head1. - 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.type.subst_default pattern.base.subst_default pattern.base.lookup_default - PositiveMap.add PositiveMap.find PositiveMap.empty - PositiveSet.rev PositiveSet.rev_append - 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.rValueOrExpr - Compile.swap_list - Compile.type_of_rawexpr - Compile.option_type_type_beq - 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 option_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} !_ !_. + (* For printing *) 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 {_ _ _}. @@ -2655,18 +2682,10 @@ Module Compilers. Local Notation "x" := (type.base x) (only printing, at level 9). Section red_fancy. - 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_rewrite_head - := make_rewrite_head (@fancy_rewrite_head0 var 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) *) + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z). + + Local Definition fancy_rewrite_head + := Eval hnf in rewrite_head (fancy_rewriter_data invert_low invert_high). Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2675,17 +2694,10 @@ Module Compilers. End red_fancy. Section red_fancy_with_casts. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) - (value_range flag_range : zrange) - {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 value_range flag_range do_again t idc) (@fancy_with_casts_pr2_rewrite_rules). - (* Tactic call ran for 4.142 secs (4.143u,0.s) (success) - Tactic call ran for 80.563 secs (80.56u,0.s) (success) - Tactic call ran for 0.154 secs (0.156u,0.s) (success) - Finished transaction in 85.431 secs (85.427u,0.s) (successful) *) + (value_range flag_range : zrange). + + Local Definition fancy_with_casts_rewrite_head + := Eval hnf in rewrite_head (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range). Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2693,16 +2705,8 @@ Module Compilers. Redirect "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))) - {t} (idc : ident t). - Time Definition nbe_rewrite_head - := 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 Definition nbe_rewrite_head + := Eval hnf in rewrite_head nbe_rewriter_data. Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2711,18 +2715,10 @@ Module Compilers. End red_nbe. Section red_arith. - 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))) - {t} (idc : ident t). - - Time Definition arith_rewrite_head - := 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) *) + Context (max_const_val : Z). + + Local Definition arith_rewrite_head + := Eval hnf in rewrite_head (arith_rewriter_data max_const_val). Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2731,13 +2727,8 @@ Module Compilers. 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 Definition arith_with_casts_rewrite_head + := Eval hnf in rewrite_head arith_with_casts_rewriter_data. Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2746,13 +2737,8 @@ Module Compilers. End red_arith_with_casts. Section red_strip_literal_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 strip_literal_casts_rewrite_head - := make_rewrite_head (@strip_literal_casts_rewrite_head0 var do_again t idc) (@strip_literal_casts_pr2_rewrite_rules). + Local Definition strip_literal_casts_rewrite_head + := Eval hnf in rewrite_head strip_literal_casts_rewriter_data. Local Set Printing Depth 1000000. Local Set Printing Width 200. @@ -2760,23 +2746,43 @@ Module Compilers. Redirect "strip_literal_casts_rewrite_head" Print strip_literal_casts_rewrite_head. End red_strip_literal_casts. + Local Ltac unfold_Rewrite Rewrite := + let h := head Rewrite in + let Rewrite := (eval cbv [h] in Rewrite) in + let data := lazymatch Rewrite with context[@Make.Rewrite ?data] => head data end in + (eval cbv [Make.Rewrite rewrite_head default_fuel data] in Rewrite). + Local Notation unfold_Rewrite Rewrite := + (ltac:(let v := unfold_Rewrite Rewrite in + exact v)) (only parsing). + + Definition RewriteNBE_folded := @Make.Rewrite nbe_rewriter_data. Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (@nbe_rewrite_head) nbe_default_fuel t e. + := unfold_Rewrite (@RewriteNBE_folded t e). + Definition RewriteArith_folded (max_const_val : Z) := @Make.Rewrite (arith_rewriter_data max_const_val). Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (fun var do_again => @arith_rewrite_head max_const_val var) arith_default_fuel t e. + := unfold_Rewrite (@RewriteArith_folded max_const_val t e). + Definition RewriteArithWithCasts_folded := @Make.Rewrite arith_with_casts_rewriter_data. Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (@arith_with_casts_rewrite_head) arith_with_casts_default_fuel t e. + := unfold_Rewrite (@RewriteArithWithCasts_folded t e). + Definition RewriteStripLiteralCasts_folded := @Make.Rewrite strip_literal_casts_rewriter_data. Definition RewriteStripLiteralCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (fun var do_again => @strip_literal_casts_rewrite_head var) strip_literal_casts_default_fuel t e. + := unfold_Rewrite (@RewriteStripLiteralCasts_folded t e). + Definition RewriteToFancy_folded + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + := @Make.Rewrite (fancy_rewriter_data invert_low invert_high). Definition RewriteToFancy (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 var) fancy_default_fuel t e. + := unfold_Rewrite (@RewriteToFancy_folded invert_low invert_high t e). + Definition RewriteToFancyWithCasts_folded + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + (value_range flag_range : zrange) + := @Make.Rewrite (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range). Definition RewriteToFancyWithCasts (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) (value_range flag_range : zrange) {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 value_range flag_range var) fancy_with_casts_default_fuel t e. + := unfold_Rewrite (@RewriteToFancyWithCasts_folded invert_low invert_high value_range flag_range t e). End RewriteRules. Import defaults. diff --git a/src/RewriterInterpProofs1.v b/src/RewriterInterpProofs1.v index 611a6ca5b..145a3d388 100644 --- a/src/RewriterInterpProofs1.v +++ b/src/RewriterInterpProofs1.v @@ -455,52 +455,6 @@ Module Compilers. subst; reflexivity. Qed. - Lemma interp_Base_value {t v1 v2} - : value_interp_related v1 v2 - -> value_interp_related (@Base_value t v1) v2. - Proof using Type. - cbv [Base_value]; destruct t; exact id. - Qed. - - Lemma interp_splice_under_lets_with_value_of_ex {T T' t R e f v} - : (exists fv (xv : T'), - UnderLets.interp_related ident_interp R e xv - /\ (forall x1 x2, - R x1 x2 - -> value_interp_related (f x1) (fv x2)) - /\ fv xv = v) - -> value_interp_related (@splice_under_lets_with_value T t e f) v. - Proof using Type. - induction t as [|s IHs d IHd]. - all: repeat first [ progress cbn [value_interp_related splice_under_lets_with_value] in * - | progress intros - | progress destruct_head'_ex - | progress destruct_head'_and - | progress subst - | eassumption - | solve [ eauto ] - | now (eapply UnderLets.splice_interp_related_of_ex; eauto) - | match goal with - | [ H : _ |- _ ] => eapply H; clear H - | [ |- exists fv xv, _ /\ _ /\ _ ] - => do 2 eexists; repeat apply conj; [ eassumption | | ] - end ]. - Qed. - - Lemma interp_splice_value_with_lets_of_ex {t t' e f v} - : (exists fv xv, - value_interp_related e xv - /\ (forall x1 x2, - value_interp_related x1 x2 - -> value_interp_related (f x1) (fv x2)) - /\ fv xv = v) - -> value_interp_related (@splice_value_with_lets t t' e f) v. - Proof using Type. - cbv [splice_value_with_lets]; break_innermost_match. - { apply interp_splice_under_lets_with_value_of_ex. } - { intros; destruct_head'_ex; destruct_head'_and; subst; eauto. } - Qed. - Lemma interp_reify_and_let_binds {with_lets t v1 v} : value_interp_related v1 v -> UnderLets_interp_related (@reify_and_let_binds_cps with_lets t v1 _ UnderLets.Base) v. diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v index 0587aec51..6da5a9e47 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -13,6 +13,7 @@ Require Import Crypto.Rewriter. Require Import Crypto.RewriterWf1. Require Import Crypto.RewriterWf2. Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.RewriterRulesProofs. Require Import Crypto.RewriterRulesGood. Require Import Crypto.RewriterRulesInterpGood. Require Import Crypto.Util.Tactics.BreakMatch. @@ -54,14 +55,25 @@ Module Compilers. Module Import RewriteRules. - Local Ltac start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := + Local Ltac start_Wf_or_interp_proof Rewrite_folded := let Rewrite := lazymatch goal with | [ |- Wf ?e ] => head e | [ |- expr.Interp _ ?e == _ ] => head e end in - cbv [Rewrite]; rewrite rewrite_head_eq; cbv [rewrite_head0]; rewrite all_rewrite_rules_eq. - Local Ltac start_Wf_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := - start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0; + progress change Rewrite with Rewrite_folded; cbv [Rewrite_folded]; + let data := lazymatch goal with |- context[Make.Rewrite ?data] => data end in + let data_head := head data in + cbv [Make.Rewrite]; + rewrite (rewrite_head_eq data); + let lem := fresh in + pose proof (all_rewrite_rules_eq data) as lem; + cbv [data_head rewrite_head0 default_fuel all_rewrite_rules rewrite_rules]; + unfold data_head at 1 in lem; + cbv [all_rewrite_rules] in lem; + let h := lazymatch goal with |- context[Compile.Rewrite ?rewrite_head] => head rewrite_head end in + cbv [h]; rewrite lem; clear lem. + Local Ltac start_Wf_proof Rewrite_folded := + start_Wf_or_interp_proof Rewrite_folded; apply Compile.Wf_Rewrite; [ | assumption ]; let wf_do_again := fresh "wf_do_again" in (intros ? ? ? ? wf_do_again ? ?); @@ -70,8 +82,8 @@ Module Compilers. pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct with nocore; try reflexivity. - Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := - start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0; + Local Ltac start_Interp_proof Rewrite_folded := + start_Wf_or_interp_proof Rewrite_folded; eapply Compile.InterpRewrite; [ | assumption ]; intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); eauto using @@ -81,22 +93,22 @@ Module Compilers. Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). Proof. - start_Wf_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0). + start_Wf_proof RewriteNBE_folded. apply nbe_rewrite_rules_good. Qed. Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e). Proof. - start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). + start_Wf_proof RewriteArith_folded. 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). + start_Wf_proof RewriteArithWithCasts_folded. apply arith_with_casts_rewrite_rules_good. Qed. Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e). Proof. - start_Wf_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0). + start_Wf_proof RewriteStripLiteralCasts_folded. apply strip_literal_casts_rewrite_rules_good. Qed. Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) @@ -104,8 +116,8 @@ Module Compilers. (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e). Proof. - start_Wf_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). - eapply fancy_rewrite_rules_good; eassumption. + start_Wf_proof RewriteToFancy_folded. + apply fancy_rewrite_rules_good; assumption. Qed. Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) @@ -114,39 +126,39 @@ Module Compilers. (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 value_range flag_range 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. + start_Wf_proof RewriteToFancyWithCasts_folded. + apply fancy_with_casts_rewrite_rules_good; assumption. 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. Proof. - start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0). - apply nbe_rewrite_rules_interp_good. + start_Interp_proof RewriteNBE_folded. + apply nbe_rewrite_rules_interp_good, nbe_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). - apply arith_rewrite_rules_interp_good. + start_Interp_proof RewriteArith_folded. + apply arith_rewrite_rules_interp_good, arith_rewrite_rules_proofs. Qed. 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). - apply arith_with_casts_rewrite_rules_interp_good. + start_Interp_proof RewriteArithWithCasts_folded. + apply arith_with_casts_rewrite_rules_interp_good, arith_with_casts_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteStripLiteralCasts {cast_outside_of_range} {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteStripLiteralCasts t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0). - apply strip_literal_casts_rewrite_rules_interp_good. + start_Interp_proof RewriteStripLiteralCasts_folded. + apply strip_literal_casts_rewrite_rules_interp_good, strip_literal_casts_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) @@ -156,8 +168,8 @@ Module Compilers. : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy invert_low invert_high t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). - eapply fancy_rewrite_rules_interp_good; eassumption. + start_Interp_proof RewriteToFancy_folded. + apply fancy_rewrite_rules_interp_good; try assumption; apply fancy_rewrite_rules_proofs; assumption. Qed. Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) @@ -168,8 +180,8 @@ Module Compilers. : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range 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). - eapply fancy_with_casts_rewrite_rules_interp_good; eassumption. + start_Interp_proof RewriteToFancyWithCasts_folded. + apply fancy_with_casts_rewrite_rules_interp_good; try assumption; apply fancy_with_casts_rewrite_rules_proofs; assumption. Qed. Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. diff --git a/src/RewriterRules.v b/src/RewriterRules.v index 8f23c1793..08a4e8d1f 100644 --- a/src/RewriterRules.v +++ b/src/RewriterRules.v @@ -318,6 +318,9 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop) ; (forall s c y x, Z.add_with_get_carry_full s (- c) x (- y) = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) + ; (forall b x, (* inline negation when the rewriter wouldn't already inline it *) + ident.gets_inlined b x = false + -> -x = dlet v := x in -v) ] ]. diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index c4486ef67..c05bcc23e 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -44,151 +44,11 @@ Module Compilers. Module Import RewriteRules. Import Rewriter.Compilers.RewriteRules. - Lemma nbe_rewrite_head_eq : @nbe_rewrite_head = @nbe_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma fancy_rewrite_head_eq - : (fun var do_again => @fancy_rewrite_head var) - = @fancy_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma arith_rewrite_head_eq max_const_val : (fun var do_again => @arith_rewrite_head max_const_val var) = (fun var => @arith_rewrite_head0 var max_const_val). - Proof. reflexivity. Qed. - - Lemma fancy_with_casts_rewrite_head_eq invert_low invert_high value_range flag_range - : (fun var do_again => @fancy_with_casts_rewrite_head invert_low invert_high value_range flag_range var) - = (fun var => @fancy_with_casts_rewrite_head0 var invert_low invert_high value_range flag_range). - Proof. reflexivity. Qed. - - Lemma arith_with_casts_rewrite_head_eq : @arith_with_casts_rewrite_head = @arith_with_casts_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma strip_literal_casts_rewrite_head_eq : (fun var do_again => @strip_literal_casts_rewrite_head var) = @strip_literal_casts_rewrite_head0. - Proof. reflexivity. Qed. - - Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules. - Proof. reflexivity. Qed. - - Lemma fancy_all_rewrite_rules_eq : @fancy_all_rewrite_rules = @fancy_rewrite_rules. - Proof. reflexivity. Qed. - - 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. - - Lemma strip_literal_casts_all_rewrite_rules_eq : @strip_literal_casts_all_rewrite_rules = @strip_literal_casts_rewrite_rules. - Proof. reflexivity. Qed. - Section good. Context {var1 var2 : type -> Type}. Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2). - Lemma wf_rlist_rect_gen - {ivar1 ivar2 A P} - Q - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf Q G N1 N2) - (HC : forall G' x xs y ys rec1 rec2, - (exists seg, G' = (seg ++ G)%list) - -> expr.wf G x y - -> expr.wf G (reify_list xs) (reify_list ys) - -> Q G' rec1 rec2 - -> UnderLets.wf Q G' (C1 x xs rec1) (C2 y ys rec2)) - : option_eq (UnderLets.wf Q G) - (@rlist_rect var1 A P ivar1 N1 C1 ls1) - (@rlist_rect var2 A P ivar2 N2 C2 ls2). - Proof using Type. - cbv [rlist_rect]. - cbv [Compile.option_bind' Option.bind]. - break_innermost_match. - all: repeat first [ match goal with - | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] - => first [ erewrite <- expr.wf_reflect_list in H' by eassumption - | erewrite -> expr.wf_reflect_list in H' by eassumption ]; - exfalso; clear -H H'; congruence - | [ |- UnderLets.wf _ _ _ _ ] => constructor - end - | progress expr.invert_subst - | progress cbn [sequence_return option_eq] - | assumption - | reflexivity - | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G') - | progress intros ]. - lazymatch goal with - | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ] - => revert dependent l'; intro l2; revert dependent l; intro l1 - end. - revert l2; induction l1 as [|l1 ls1 IHls1], l2; cbn [list_rect]; - rewrite ?expr.reify_list_cons, ?expr.reify_list_nil; - intros; expr.inversion_wf_constr; [ assumption | ]. - all: repeat first [ match goal with - | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ] - => first [ erewrite <- expr.wf_reflect_list in H' by eassumption - | erewrite -> expr.wf_reflect_list in H' by eassumption ]; - exfalso; clear -H H'; congruence - | [ |- UnderLets.wf _ _ _ _ ] => constructor - end - | progress expr.invert_subst - | progress cbn [sequence_return option_eq] - | assumption - | reflexivity - | solve [ auto ] - | progress subst - | apply @UnderLets.wf_splice with (P:=Q) - | progress intros - | wf_safe_t_step - | progress type.inversion_type - | progress expr.inversion_wf_constr ]. - Qed. - Lemma wf_rlist_rect {A P} - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf (fun G' => expr.wf G') G N1 N2) - (HC : forall G' x xs y ys rec1 rec2, - (exists seg, G' = (seg ++ G)%list) - -> expr.wf G x y - -> expr.wf G (reify_list xs) (reify_list ys) - -> expr.wf G' rec1 rec2 - -> UnderLets.wf (fun G'' => expr.wf G'') G' (C1 x xs rec1) (C2 y ys rec2)) - : option_eq (UnderLets.wf (fun G' => expr.wf G') G) - (@rlist_rect var1 A P var1 N1 C1 ls1) - (@rlist_rect var2 A P var2 N2 C2 ls2). - Proof using Type. apply wf_rlist_rect_gen; assumption. Qed. - Lemma wf_rlist_rectv {A P} - N1 N2 C1 C2 ls1 ls2 G - (Hwf : expr.wf G ls1 ls2) - (HN : UnderLets.wf (fun G' v1 v2 - => exists G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - /\ expr.wf G'' v1 v2) G N1 N2) - (HC : forall G' x xs y ys rec1 rec2, - (exists seg, G' = (seg ++ G)%list) - -> expr.wf G x y - -> expr.wf G (reify_list xs) (reify_list ys) - -> (exists G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - /\ expr.wf G'' rec1 rec2) - -> UnderLets.wf (fun G' v1 v2 - => exists G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - /\ expr.wf G'' v1 v2) - G' (C1 x xs rec1) (C2 y ys rec2)) - : option_eq (UnderLets.wf - (fun G' v1 v2 - => exists G'', - (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2') - /\ expr.wf G'' v1 v2) - G) - (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1) - (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2). - Proof using Type. apply wf_rlist_rect_gen; assumption. Qed. - Lemma wf_list_rect {T A} G N1 N2 C1 C2 ls1 ls2 (HN : Compile.wf_value G N1 N2) @@ -222,22 +82,29 @@ Module Compilers. (nat_rect (fun _ => @Compile.value_with_lets base.type ident var2 A) O2 S2 n). Proof. induction n; cbn [nat_rect]; try eapply HS; eauto using (ex_intro _ nil). Qed. + Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps]. + Local Ltac start_good := - apply Compile.rewrite_rules_goodT_by_curried; - split; [ reflexivity | ]; - lazymatch goal with - | [ |- forall x p x' p', In (@existT ?A ?P x p, @existT ?A' ?P' x' p') ?ls -> @?Q x x' p p' ] - => apply (@forall_In_pair_existT A A' P P' Q ls); cbn [projT1 projT2 fst snd]; cbv [id] - end; - (exists eq_refl); - cbn [eq_rect]; - cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default pattern.base.lookup_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq]; - cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb]; - repeat first [ progress intros - | match goal with - | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) - end - | progress cbn [eq_rect] in * ]. + match goal with + | [ |- rewrite_rules_goodT ?rew1 ?rew2 ] + => let H := fresh in + pose proof (@Compile.rewrite_rules_goodT_by_curried _ _ _ _ _ rew1 rew2 eq_refl) as H; + let data := lazymatch rew1 with rewrite_rules ?data _ => data end in + let h := head data in + cbv [h rewrite_rules] in H; + let h' := lazymatch type of H with + | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => head rew1 + end in + let pident_arg_types + := lazymatch type of H with + | context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => pident_arg_types + end in + cbv [h' pident_arg_types Compile.rewrite_rules_goodT_curried_cps] in H; + (* make [Qed] not take forever by explicitly recording a cast node *) + let H' := fresh in + pose proof H as H'; clear H; + apply H'; clear H'; intros + end. Local Ltac fin_wf := repeat first [ progress intros @@ -286,15 +153,16 @@ Module Compilers. | progress intros | progress fin_wf ]. + Local Notation nbe_rewrite_rules := (rewrite_rules nbe_rewriter_data _). Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof using Type. Time start_good. - Time all: handle_reified_rewrite_rules; handle_extra_nbe. + Time all: abstract (handle_reified_rewrite_rules; handle_extra_nbe). Qed. Local Ltac handle_extra_arith_rules := - repeat first [ progress cbv [rwhenl option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] + repeat first [ progress cbv [option_eq SubstVarLike.is_var_fst_snd_pair_opp_cast] in * | break_innermost_match_step | match goal with | [ Hwf : Compile.wf_value _ ?x _, H : context[SubstVarLike.is_recursively_var_or_ident _ ?x] |- _ ] => erewrite SubstVarLike.wfT_is_recursively_var_or_ident in H by exact Hwf @@ -302,37 +170,42 @@ Module Compilers. | congruence | progress fin_wf ]. + Local Notation arith_rewrite_rules max_const := (rewrite_rules (arith_rewriter_data max_const) _). Lemma arith_rewrite_rules_good max_const : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const). Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules; handle_extra_arith_rules. - Qed. + Time Qed. + Local Notation arith_with_casts_rewrite_rules := (rewrite_rules arith_with_casts_rewriter_data _). 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: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation strip_literal_casts_rewrite_rules := (rewrite_rules strip_literal_casts_rewriter_data _). Lemma strip_literal_casts_rewrite_rules_good : rewrite_rules_goodT strip_literal_casts_rewrite_rules strip_literal_casts_rewrite_rules. Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation fancy_rewrite_rules invert_low invert_high := (rewrite_rules (fancy_rewriter_data invert_low invert_high) _). 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)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) - : rewrite_rules_goodT fancy_rewrite_rules fancy_rewrite_rules. + : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high). Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. + Local Notation fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range := (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _). Lemma fancy_with_casts_rewrite_rules_good (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : ZRange.zrange) @@ -342,7 +215,7 @@ Module Compilers. Proof using Type. Time start_good. Time all: handle_reified_rewrite_rules. - Qed. + Time Qed. End good. End RewriteRules. End Compilers. diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index c73867339..6ff9ef672 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -11,33 +11,11 @@ Require Import Crypto.UnderLetsProofs. Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. Require Import Crypto.Rewriter. Require Import Crypto.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.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. -Require Import Crypto.Util.ZRange.BasicLemmas. -Require Import Crypto.Util.ZRange.OperationsBounds. -Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier. +Require Import Crypto.Util.Tactics.UniquePose. 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.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Bool. Require Import Crypto.Util.ListUtil. @@ -45,7 +23,6 @@ Require Import Crypto.Util.ListUtil.Forall. 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. @@ -70,81 +47,81 @@ Module Compilers. Context {cast_outside_of_range : zrange -> Z -> Z}. Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). - - 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 Lemma unfold_is_bounded_by_bool v r - : is_bounded_by_bool v r = true -> lower r <= v <= upper r. - Proof using Type. - cbv [is_bounded_by_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. - Qed. - - Local Lemma unfold_is_tighter_than_bool r1 r2 - : is_tighter_than_bool r1 r2 = true -> lower r2 <= lower r1 /\ upper r1 <= upper r2. - Proof using Type. - cbv [is_tighter_than_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. - Qed. - Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident_interp)). - Local Ltac do_cbv0 := - cbv [id - Compile.rewrite_rules_interp_goodT_curried - Compile.rewrite_rule_data_interp_goodT_curried 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 Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement 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 pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty 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.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation 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 pattern.base.lookup_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related - Reify.expr_value_to_rewrite_rule_replacement UnderLets.flat_map Compile.reify_expr_beta_iota Compile.reflect_expr_beta_iota Compile.reflect_ident_iota Compile.reify_to_UnderLets UnderLets.of_expr Compile.Base_value]; - cbn [UnderLets.splice Compile.reflect invert_expr.invert_Literal invert_expr.ident.invert_Literal Compile.splice_under_lets_with_value]. - Local Ltac do_cbv := - do_cbv0; - cbv [List.map List.fold_right List.rev list_rect orb List.app]. - Local Ltac start_interp_good := - apply Compile.rewrite_rules_interp_goodT_by_curried; - do_cbv; + cbv [List.skipn] in *; 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); subst Q'; cbv [projT1 projT2 id] + | [ |- @Compile.rewrite_rules_interp_goodT ?ident ?pident ?pident_arg_types ?pident_to_typed ?ident_interp (rewrite_rules ?data ?var) ] + => let H := fresh in + pose proof (@Compile.rewrite_rules_interp_goodT_by_curried + _ _ _ pident_to_typed ident_interp (rewrite_rules data var) (rewrite_rules_specs data)) as H; + let h := head data in + cbv [rewrite_rules dummy_count rewrite_rules_specs h] in * |- ; + let h' := lazymatch type of H with context[Compile.rewrite_rules_interp_goodT_curried_cps _ _ _ ?v] => head v end in + unfold h' in H at 1; + cbv [Compile.rewrite_rules_interp_goodT_curried_cps pident_arg_types pident_to_typed] in H; + cbn [snd hd tl projT1 projT2] in H; + (* make [Qed] not take forever by explicitly recording a cast node *) + let H' := fresh in + pose proof H as H'; clear H; + apply H'; clear H' end; - do_cbv0; - repeat first [ progress intros - | match goal with - | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) - | [ |- True /\ _ ] => split; [ exact I | ] - | [ |- _ /\ _ ] => split; [ intros; 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.gen_interp UnderLets.interp_related UnderLets.interp_related_gen] in *. + [ try assumption; + cbn [PrimitiveHList.hlist snd]; + repeat lazymatch goal with + | [ |- PrimitiveProd.Primitive.prod _ _ ] => constructor + | [ |- forall A x, x = x ] => reflexivity + end; + try assumption + | try match goal with + | [ H : PrimitiveHList.hlist _ _ |- _ ] => clear H + end; + let H := fresh in + intro H; hnf in H; + repeat first [ progress intros + | match goal with + | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl) + | [ |- True /\ _ ] => split; [ exact I | ] + | [ |- _ /\ _ ] => split; [ intros; exact I | ] + | [ |- match (if ?b then _ else _) with Some _ => _ | None => _ end ] + => destruct b eqn:? + | [ |- True ] => exact I + end + | progress eta_expand + | progress cbn [eq_rect] in * ]; + cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp] in *; + cbn [fst snd] in *; + eta_expand; + split_andb; + repeat match goal with + | [ H : ?b = true |- _ ] => unique pose proof (@Reflect.reflect_bool _ b _ H) + | [ H : negb _ = false |- _ ] => rewrite Bool.negb_false_iff in H + | [ H : _ = false |- _ ] => rewrite <- Bool.negb_true_iff in H + end; + subst; cbv [ident.gets_inlined ident.literal] in *; + lazymatch goal with + | [ |- ?R ?v ] + => let v' := open_constr:(_) in + replace v with v'; + [ | symmetry; + unshelve eapply H; shelve_unifiable; + try eassumption; + try (repeat apply conj; assumption); + try match goal with + | [ |- ?A = ?B ] => first [ is_evar A | is_evar B ]; reflexivity + | [ |- ?T ] => is_evar T; exact I + | [ |- ?P ] (* TODO: Maybe we shouldn't simplify boolean expressions in rewriter reification, since we end up just having to undo it here in a kludgy way....... *) + => apply (proj2 (@Bool.reflect_iff P _ _)); + progress rewrite ?Bool.eqb_true_l, ?Bool.eqb_true_r, ?Bool.eqb_false_l, ?Bool.eqb_false_r; + let b := lazymatch goal with |- ?b = true => b end in + apply (proj1 (@Bool.reflect_iff _ b _)); + tauto + end ]; + clear H + end; + fold (@base.interp) in * + .. ]. Ltac recurse_interp_related_step := let do_replace v := @@ -192,767 +169,230 @@ Module Compilers. end. (* TODO: MOVE ME? *) - Local Ltac recursive_match_to_list_case term := + Local Ltac recursive_match_to_case term := + let contains_match x + := lazymatch x with + | context[match _ with nil => _ | _ => _ end] => true + | context[match _ with pair a b => _ end] => true + | context[match _ with true => _ | false => _ end] => true + | _ => false + end in lazymatch term with | context G[match ?ls with nil => ?N | cons x xs => @?C x xs end] => let T := type of N in let term := context G[list_case (fun _ => T) N C ls] in - recursive_match_to_list_case term - | context[match _ with nil => _ | _ => _ end] - => let G_f - := match term with - | context G[fun x : ?T => @?f x] - => lazymatch f with - | context[match _ with nil => _ | _ => _ end] - => let f' := fresh in - let T' := type of f in - constr:(((fun f' : T' => ltac:(let G' := context G[f'] in exact G')), - f)) - end - end in - lazymatch G_f with - | ((fun f' => ?G), (fun x : ?T => ?f)) - => let x' := fresh in - let rep := constr:(fun x' : T - => ltac:(let f := constr:(match x' with x => f end) in - let f := recursive_match_to_list_case f in - exact f)) in - let term := constr:(match rep with f' => G end) in - recursive_match_to_list_case term - end - | _ => term + recursive_match_to_case term + | context G[match ?v with pair a b => @?P a b end] + => let T := lazymatch type of P with forall a b, @?T a b => T end in + let term := context G[prod_rect (fun ab => T (fst ab) (snd ab)) P v] in + recursive_match_to_case term + | context G[match ?b with true => ?t | false => ?f end] + => let T := type of t in + let term := context G[bool_rect (fun _ => T) t f b] in + recursive_match_to_case term + | _ => let has_match := contains_match term in + match has_match with + | true + => let G_f + := match term with + | context G[fun x : ?T => @?f x] + => let has_match := contains_match f in + lazymatch has_match with + | true + => let f' := fresh in + let T' := type of f in + constr:(((fun f' : T' => ltac:(let G' := context G[f'] in exact G')), + f)) + end + end in + lazymatch G_f with + | ((fun f' => ?G), (fun x : ?T => ?f)) + => let x' := fresh in + let rep := constr:(fun x' : T + => ltac:(let f := constr:(match x' with x => f end) in + let f := recursive_match_to_case f in + exact f)) in + let term := constr:(match rep with f' => G end) in + recursive_match_to_case term + end + | false + => term + end end. - Local Ltac recursive_match_to_list_case_in_goal := + Local Ltac recursive_match_to_case_in_goal := let G := match goal with |- ?G => G end in - let G := recursive_match_to_list_case G in + let G := recursive_match_to_case G in change G. - Local Ltac interp_good_t_step_related := - first [ lazymatch goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- True ] => exact I - | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence - | [ |- ?G ] => has_evar G; reflexivity - | [ |- context[expr.interp_related_gen _ _ _ _] ] => reflexivity - | [ |- context[_ == _] ] => reflexivity - (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand - | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*) - end - | match goal with - | [ |- UnderLets.interp_related ?ii ?R (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) - | [ |- expr.interp_related_gen ?ii ?R (#ident.list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) - | [ |- expr.interp_related_gen ?ii ?R (#ident.list_case @ _ @ _ @ _)%expr (@list_case ?A (fun _ => ?P) ?N ?C ?ls) ] - => progress change (@list_case A (fun _ => P) N C ls) with (@ident.Thunked.list_case A P (fun _ => N) C ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@flat_map ?A ?B ?f ?ls) ] - => rewrite (@eq_flat_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@partition ?A ?f ?ls) ] - => rewrite (@eq_partition_list_rect A f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@List.map ?A ?B ?f ?ls) ] - => rewrite (@eq_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _ _) (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (List.repeat ?x ?n) ] - => rewrite (eq_repeat_nat_rect x n) - | [ |- ?R (nat_rect _ _ _ _ _) (@List.firstn ?A ?n ?ls) ] - => rewrite (@eq_firstn_nat_rect A n ls) - | [ |- ?R (nat_rect _ _ _ _ _) (@List.skipn ?A ?n ?ls) ] - => rewrite (@eq_skipn_nat_rect A n ls) - | [ |- ?R (list_rect _ _ _ _) (@List.rev ?A ?xs) ] - => rewrite (@eq_rev_list_rect A xs) - | [ |- ?R (list_rect _ _ _ _) (@List.length ?A ?xs) ] - => rewrite (@eq_length_list_rect A xs) - | [ |- ?R (list_rect _ _ _ _) (@List.flat_map ?A ?B ?f ?xs) ] - => rewrite (@eq_flat_map_list_rect A B f xs) - | [ |- ?R (list_rect _ _ _ _) (@List.partition ?A ?f ?xs) ] - => rewrite (@eq_partition_list_rect A f xs) - | [ |- ?R (nat_rect _ _ _ _ _) (@update_nth ?A ?n ?f ?xs) ] - => rewrite (@eq_update_nth_nat_rect A n f xs) - - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@flat_map ?A ?B ?f ?ls) ] - => rewrite (@eq_flat_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@partition ?A ?f ?ls) ] - => rewrite (@eq_partition_list_rect A f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@List.map ?A ?B ?f ?ls) ] - => rewrite (@eq_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr) (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] - => rewrite (@eq_fold_right_list_rect A B f v ls) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.firstn ?A ?n ?ls) ] - => rewrite (@eq_firstn_nat_rect A n ls) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.skipn ?A ?n ?ls) ] - => rewrite (@eq_skipn_nat_rect A n ls) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.rev ?A ?xs) ] - => rewrite (@eq_rev_list_rect A xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.length ?A ?xs) ] - => rewrite (@eq_length_list_rect A xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.flat_map ?A ?B ?f ?xs) ] - => rewrite (@eq_flat_map_list_rect A B f xs) - | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.partition ?A ?f ?xs) ] - => rewrite (@eq_partition_list_rect A f xs) - | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@update_nth ?A ?n ?f ?xs) ] - => rewrite (@eq_update_nth_nat_rect A n f xs) - | [ |- ?R (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.combine ?A ?B ?xs ?ys) ] - => rewrite (@eq_combine_list_rect A B xs ys) - - - | [ |- expr.interp_related_gen _ _ (#ident.list_rect @ _ @ _ @ _)%expr (ident.Thunked.list_rect _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (list_rect _ _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.nat_rect @ _ @ _ @ _)%expr (ident.Thunked.nat_rect _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (nat_rect _ _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | ] - | [ |- expr.interp_related_gen _ _ (#ident.list_case @ _ @ _ @ _)%expr (ident.Thunked.list_case _ _ _ _) ] - => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; - [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] - | ] - | ] - | ] - | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_list_case_in_goal - 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 bool_rect UnderLets.interp_related UnderLets.interp_related_gen type.related] in * - | progress cbv [Compile.option_bind' respectful expr.interp_related] in * - | progress fold (@type.interp _ base.interp) - | progress fold (@base.interp) - | progress change S with Nat.succ - | 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 expr.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 - | [ |- context[expr.interp_related_gen _ _ (reify_list _)] ] - => rewrite expr.reify_list_interp_related_gen_iff - | [ H : context[expr.interp_related_gen _ _ (reify_list _)] |- _ ] - => rewrite expr.reify_list_interp_related_gen_iff in H - | [ |- expr.interp_related_gen ?ident_interp _ (UnderLets.to_expr ?x) ?y ] - => change (expr.interp_related ident_interp (UnderLets.to_expr x) y); - rewrite <- UnderLets.to_expr_interp_related_iff - | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff - | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff - | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff - | [ |- context[Forall2 _ (List.rev _) (List.rev _)] ] => rewrite Forall2_rev_iff - | [ |- context[Forall2 _ ?x ?x] ] => rewrite Forall2_Forall; cbv [Proper] - | [ |- context[Forall _ (seq _ _)] ] => rewrite Forall_seq - | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.firstn ?n ?l1) (List.firstn ?n ?l2) ] - => apply Forall2_firstn, H - | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.skipn ?n ?l1) (List.skipn ?n ?l2) ] - => apply Forall2_skipn, H - | [ |- Forall2 ?R (List.combine _ _) (List.combine _ _) ] - => eapply Forall2_combine; [ | eassumption | eassumption ] - | [ H : List.Forall2 _ ?l1 ?l2, H' : ?R ?v1 ?v2 |- ?R (nth_default ?v1 ?l1 ?x) (nth_default ?v2 ?l2 ?x) ] - => apply Forall2_forall_iff''; split; assumption - | [ H : List.Forall2 _ ?x ?y |- List.length ?x = List.length ?y ] - => eapply eq_length_Forall2, H - | [ |- exists fv xv, _ /\ _ /\ fv xv = ?f ?x ] - => exists f, x; repeat apply conj; [ solve [ repeat interp_good_t_step_related ] | | reflexivity ] - | [ |- _ /\ ?x = ?x ] => split; [ | reflexivity ] - | [ |- UnderLets.interp_related - ?ident_interp ?R - (list_rect - (fun _ : list (expr ?A) => UnderLets.UnderLets _ _ _ ?B) - ?Pnil - ?Pcons - ?ls) - (list_rect - (fun _ : list _ => ?B') - ?Pnil' - ?Pcons' - ?ls') ] - => apply (@UnderLets.list_rect_interp_related _ _ _ ident_interp A B Pnil Pcons ls B' Pnil' Pcons' ls' R) - | [ |- UnderLets.interp_related - ?ident_interp ?R - (list_rect - (fun _ : list (expr ?A) => ?B -> UnderLets.UnderLets _ _ _ ?C) - ?Pnil - ?Pcons - ?ls - ?x) - (list_rect - (fun _ : list _ => ?B' -> ?C') - ?Pnil' - ?Pcons' - ?ls' - ?x') ] - => apply (@UnderLets.list_rect_arrow_interp_related _ _ _ ident_interp A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R (expr.interp_related ident_interp)) - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] - => apply UnderLets.nat_rect_interp_related - | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ] - => eapply UnderLets.nat_rect_arrow_interp_related; [ .. | eassumption ] - | [ |- UnderLets.interp_related _ _ (UnderLets.splice _ _) _ ] - => rewrite UnderLets.splice_interp_related_iff - | [ |- UnderLets.interp_related ?ident_interp _ (UnderLets.splice_list _ _) _ ] - => apply UnderLets.splice_list_interp_related_of_ex with (RA:=expr.interp_related ident_interp); exists (fun x => x); eexists; repeat apply conj; [ | | reflexivity ] - | [ H : UnderLets.interp_related _ _ ?e ?v1 |- UnderLets.interp_related _ _ ?e ?f ] - => let f := match (eval pattern v1 in f) with ?f _ => f end in - eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ e v1 f); [ | exact H ]; cbv beta - | [ H : forall x y, ?R x y -> UnderLets.interp_related _ _ (?e x) (?v1 y) |- UnderLets.interp_related _ _ (?e ?xv) ?f ] - => lazymatch f with - | context[v1 ?yv] - => let f := match (eval pattern (v1 yv) in f) with ?f _ => f end in - eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ (e xv) (v1 yv) f); [ | eapply H; assumption ] - end - | [ |- expr.interp_related_gen - _ _ - (#(ident.prod_rect) @ ?f @ ?e)%expr - match ?e' with pair a b => @?f' a b end ] - => let fh := fresh in - let eh := fresh in - set (fh := f); set (eh := e); cbn [expr.interp_related_gen]; subst fh eh; - exists (fun ev => match ev with pair a b => f' a b end), e'; - repeat apply conj; - [ | assumption | reflexivity ]; - exists (fun fv ev => match ev with pair a b => fv a b end), f'; - repeat apply conj; - [ cbn [type.interp type.related ident_interp]; cbv [respectful]; intros; subst; eta_expand; auto | | reflexivity ] - | [ |- expr.interp_related_gen - _ _ - (#(ident.bool_rect) @ ?t @ ?f @ ?b)%expr - (bool_rect ?P ?t' ?f' ?b') ] - => let th := fresh in - let fh := fresh in - let bh := fresh in - set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related_gen]; subst th fh bh; - unshelve - ((exists (bool_rect P t' f'), b'); repeat apply conj; - [ | shelve | reflexivity ]; - (exists (fun fv => bool_rect P t' (fv tt)), (fun _ => f')); repeat apply conj; - [ | shelve | reflexivity ]; - (exists (fun tv fv => bool_rect P (tv tt) (fv tt)), (fun _ => t')); repeat apply conj; - [ | shelve | reflexivity ]) - | [ |- @expr.interp_related_gen _ _ _ _ _ _ (type.base ?t) _ _ ] - => lazymatch t with - | base.type.type_base base.type.Z => idtac - | base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z) => idtac - end; - progress repeat recurse_interp_related_step - | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1), - _ /\ _ /\ fv ev = ?x ] - => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end; - lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end; - progress repeat recurse_interp_related_step - | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] - => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh - | [ H : expr.interp_related_gen _ _ ?x ?x' |- expr.interp_related_gen _ _ (?f @ ?x) (?f' ?x') ] - => let fh := fresh in - let xh := fresh in - set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; - exists f', x'; repeat apply conj; - [ | exact H | reflexivity ] - | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] => apply Forall2_update_nth - | [ H : zrange * zrange |- _ ] => destruct H - end - | progress intros - | progress subst - | assumption - | progress inversion_option - | progress destruct_head'_and - | progress destruct_head'_unit - | 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_related ] ] - | [ 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.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.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 - | progress destruct_head'_or - | progress cbn [expr.interp_related_gen] in * - | match goal with - | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] - |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ] - => apply H - | [ H : forall x1 x2, ?R1 x1 x2 -> ?R2 (?f1 x1) (?f2 x2) |- ?R2 (?f1 _) (?f2 _) ] - => apply H - | [ H : forall x1 x2, ?R1 x1 x2 -> forall y1 y2, ?R2 y1 y2 -> ?R3 (?f1 x1 y1) (?f2 x2 y2) |- ?R3 (?f1 _ _) (?f2 _ _) ] - => apply H - | [ H : forall x x', ?Rx x x' -> forall y y', _ -> forall z z', ?Rz z z' -> ?R (?f x y z) (?f' x' y' z') |- ?R (?f _ _ _) (?f' _ _ _) ] - => apply H; clear H - | [ H : forall x x', _ -> forall y y', _ -> forall z z', _ -> forall w w', _ -> ?R (?f x y z w) (?f' x' y' z' w') |- ?R (?f _ _ _ _) (?f' _ _ _ _) ] - => apply H; clear H - end - | progress cbv [Option.bind] in * - | match goal with - | [ H : expr.interp_related_gen _ _ ?e ?v |- _ ] => is_var e; clear H e - end ]. - - Local Ltac interp_good_t_step_arith := - first [ lazymatch goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- True ] => exact I - | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence - | [ H : true = false |- _ ]=> exfalso; clear -H; congruence - | [ H : false = true |- _ ]=> exfalso; clear -H; congruence - end - | progress cbv [option_beq] in * - | match goal with - | [ 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 - | [ H : ?T, H' : ?T |- _ ] => clear H' - | [ H : context[is_bounded_by_bool _ (ZRange.normalize (-_))] |- _ ] - => rewrite ZRange.is_bounded_by_bool_move_opp_normalize in H - | [ |- context[is_bounded_by_bool _ (ZRange.normalize (-_))] ] - => rewrite ZRange.is_bounded_by_bool_move_opp_normalize - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ ?r ?v] ] - => rewrite (@ident.cast_in_normalized_bounds _ r v) by exact H - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ (-?r) (-?v)] ] - => rewrite (@ident.cast_in_normalized_bounds _ (-r) (-v)); - [ | clear -H ] - | [ |- context[ident.cast _ ?r (-ident.cast _ (-?r) ?v)] ] - => rewrite (ident.cast_in_normalized_bounds r (-ident.cast _ (-r) v)) - by (rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize; apply ident.cast_always_bounded) - | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] - => rewrite (@ident.cast_idempotent _ _ r) - | [ H : is_bounded_by_bool _ ?r = true |- _] - => is_var r; unique pose proof (ZRange.is_bounded_by_normalize _ _ H) - | [ H : lower ?x = upper ?x |- _ ] => is_var x; destruct x; cbn [upper lower] in * - | [ H : is_bounded_by_bool ?x (ZRange.normalize r[?y~>?y]) = true |- _ ] - => apply ZRange.is_bounded_by_bool_normalize_constant_iff in H - | [ H : is_bounded_by_bool ?x r[?y~>?y] = true |- _ ] - => apply ZRange.is_bounded_by_bool_constant_iff in H - end + Local Ltac preprocess_step := + first [ progress cbv [expr.interp_related respectful ident.literal ident.eagerly] in * + | progress cbn [fst snd base.interp base.base_interp Compile.value'] in * | progress intros | progress subst - | assumption - | progress destruct_head'_and - | progress Z.ltb_to_lt - | progress split_andb - | match goal with - | [ |- ?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 - | break_innermost_match_step - | break_innermost_match_hyps_step - | progress destruct_head'_or - | match goal with - | [ |- context[-ident.cast _ (-?r) (-?v)] ] => rewrite (ident.cast_opp' r v) - | [ |- 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) - | [ H : is_bounded_by_bool (-?v) ?r = true, H' : (-?r <=? ?r')%zrange = true |- _ ] - => unique assert (is_bounded_by_bool v r' = true) - by (apply (@ZRange.is_bounded_by_of_is_tighter_than _ _ H'); - rewrite <- ZRange.is_bounded_by_bool_opp, ZRange.opp_involutive; exact H) - | [ H : is_bounded_by_bool ?v (-?r) = true |- _ ] - => is_var v; - unique assert (is_bounded_by_bool (-v) r = true) - by now rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize, ZRange.normalize_opp - | [ H : is_bounded_by_bool ?x r[0~>?v-1] = true |- _ ] - => progress (try unique assert (0 <= x); try unique assert (x <= v - 1)); - [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia.. - | ] - end - | progress cbn [expr.interp_related_gen] in * | match goal with - | [ |- 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 - | [ |- context[Z.land _ (Z.ones _)] ] => rewrite Z.land_ones by auto using Z.log2_nonneg - | [ |- context[- - _] ] => rewrite Z.opp_involutive - | [ 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 - | [ H : 0 <= ?x, H' : ?x <= ?r - 1 |- context[?x mod ?r] ] - => rewrite (Z.mod_small x r) by (clear -H H'; lia) - | [ H : 0 <= ?x, H' : ?x <= ?y - 1 |- context[?x / ?y] ] - => rewrite (Z.div_small x y) by (clear -H H'; lia) - | [ H : ?x = 2^Z.log2 ?x |- _ ] - => unique assert (0 <= x) by (rewrite H; auto with zarith) - | [ |- _ mod ?x = _ mod ?x ] - => progress (push_Zmod; pull_Zmod) - | [ |- ?f (_ mod ?x) = ?f (_ mod ?x) ] - => progress (push_Zmod; pull_Zmod) - | [ |- _ mod ?x = _ mod ?x ] - => apply f_equal2; (lia + nia) - | _ => rewrite !Z.shiftl_mul_pow2 in * by auto using Z.log2_nonneg - | _ => rewrite !Z.land_ones in * by auto using Z.log2_nonneg - | H : ?x mod ?b * ?y <= _ - |- context [ (?x * ?y) mod ?b ] => - rewrite (PullPush.Z.mul_mod_l x y b); - rewrite (Z.mod_small (x mod b * y) b) by omega - | [ |- context[_ - ?x + ?x] ] => rewrite !Z.sub_add - | [ |- context[_ mod (2^_) * 2^_] ] => rewrite <- !Z.mul_mod_distr_r_full - | [ |- context[Z.land _ (Z.ones _)] ] => rewrite !Z.land_ones by lia - | [ |- context[2^?a * 2^?b] ] => rewrite <- !Z.pow_add_r by lia - | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l - | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r - | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r - | [ |- context[Zpos ?p * ?x / Zpos ?p] ] - => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) - | [ H : context[Zpos ?p * ?x / Zpos ?p] |- _ ] - => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) - | [ |- ?f (?a mod ?r) = ?f (?b mod ?r) ] => apply f_equal; apply f_equal2; lia - | [ |- context[-?a - ?b + ?c] ] => replace (-a - b + c) with (c - a - b) by (clear; lia) - | [ |- context[?x - ?y + ?z] ] - => lazymatch goal with - | [ |- context[z - y + x] ] - => progress replace (z - y + x) with (x - y + z) by (clear; lia) - end - | [ |- context[?x - ?y - ?z] ] - => lazymatch goal with - | [ |- context[x - z - y] ] - => progress replace (x - z - y) with (x - y - z) by (clear; lia) - end - | [ |- context[?x + ?y] ] - => lazymatch goal with - | [ |- context[y + x] ] - => progress replace (y + x) with (x + y) by (clear; lia) - end - | [ |- context[?x + ?y + ?z] ] - => lazymatch goal with - | [ |- context[x + z + y] ] - => progress replace (x + z + y) with (x + y + z) by (clear; lia) - | [ |- context[z + x + y] ] - => progress replace (z + x + y) with (x + y + z) by (clear; lia) - | [ |- context[z + y + x] ] - => progress replace (z + y + x) with (x + y + z) by (clear; lia) - | [ |- context[y + x + z] ] - => progress replace (y + x + z) with (x + y + z) by (clear; lia) - | [ |- context[y + z + x] ] - => progress replace (y + z + x) with (x + y + z) by (clear; lia) - end - | [ |- - ident.cast _ (-?r) (- (?x / ?y)) = ident.cast _ ?r (?x' / ?y) ] - => tryif constr_eq x x' then fail else replace x with x' by lia - | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast + | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match _ with pair a b => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match _ with true => _ | false => _ end] ] => progress recursive_match_to_case_in_goal + | [ |- context[match invert_expr.reflect_list ?ls with _ => _ end] ] + => destruct (invert_expr.reflect_list ls) eqn:? + | [ |- context G[expr.interp_related_gen ?ident_interp (fun t : ?T => ?vii t ?b)] ] + => progress change (fun t : T => vii t b) with (fun t : T => @Compile.value_interp_related _ ident_interp t b) end ]. - - Local Ltac remove_casts := + Local Ltac preprocess := repeat preprocess_step. + Local Ltac handle_extra_nbe := repeat match goal with - | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] - => rewrite ident.cast_idempotent - | [ H : context[ident.cast _ ?r (ident.cast _ ?r _)] |- _ ] - => rewrite ident.cast_idempotent in H - | [ |- 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 - | [ H : 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 - | [ H : context[ZRange.constant ?v] |- _ ] => unique pose proof (ZRange.is_bounded_by_bool_normalize_constant v) - | [ H : is_tighter_than_bool (?ZRf ?r1 ?r2) (ZRange.normalize ?rs) = true, - H1 : is_bounded_by_bool ?v1 ?r1 = true, - H2 : is_bounded_by_bool ?v2 ?r2 = true - |- _ ] - => let cst := multimatch goal with - | [ |- context[ident.cast ?coor rs (?Zf v1 v2)] ] => constr:(ident.cast coor rs (Zf v1 v2)) - | [ H : context[ident.cast ?coor rs (?Zf v1 v2)] |- _ ] => constr:(ident.cast coor rs (Zf v1 v2)) - end in - lazymatch cst with - | ident.cast ?coor rs (?Zf v1 v2) - => let lem := lazymatch constr:((ZRf, Zf)%core) with - | (ZRange.shiftl, Z.shiftl)%core => constr:(@ZRange.is_bounded_by_bool_shiftl v1 r1 v2 r2 H1 H2) - | (ZRange.shiftr, Z.shiftr)%core => constr:(@ZRange.is_bounded_by_bool_shiftr v1 r1 v2 r2 H1 H2) - | (ZRange.land, Z.land)%core => constr:(@ZRange.is_bounded_by_bool_land v1 r1 v2 r2 H1 H2) - end in - try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); - clear H; - rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1 v2)) in * by assumption - end - | [ H : is_tighter_than_bool (?ZRf ?r1) (ZRange.normalize ?rs) = true, - H1 : is_bounded_by_bool ?v1 ?r1 = true - |- _ ] - => let cst := multimatch goal with - | [ |- context[ident.cast ?coor rs (?Zf v1)] ] => constr:(ident.cast coor rs (Zf v1)) - | [ H : context[ident.cast ?coor rs (?Zf v1)] |- _ ] => constr:(ident.cast coor rs (Zf v1)) - end in - lazymatch cst with - | ident.cast ?coor rs (?Zf v1) - => let lem := lazymatch constr:((ZRf, Zf)%core) with - | (ZRange.cc_m ?s, Z.cc_m ?s)%core => constr:(@ZRange.is_bounded_by_bool_cc_m s v1 r1 H1) - end in - try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); - clear H; - rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1)) in * by assumption - end - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast ?coor ?r ?v] ] - => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true, H' : context[ident.cast ?coor ?r ?v] |- _ ] - => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption - | [ H : is_bounded_by_bool ?v ?r = true, - H' : is_tighter_than_bool ?r r[0~>?x-1]%zrange = true, - H'' : Z.eqb ?x ?m = true - |- context[?v mod ?m] ] - => unique assert (is_bounded_by_bool v r[0~>x-1] = true) - by (eapply ZRange.is_bounded_by_of_is_tighter_than; eassumption) - | _ => progress Z.ltb_to_lt - | _ => progress subst + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (expr.Ident _)) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related_gen ident_interp type.related]; reflexivity + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (reify_list _)) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen]; rewrite expr.reify_list_interp_related_gen_iff + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (_, _)%expr) ?x ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen]; + recurse_interp_related_step; + [ recurse_interp_related_step + | lazymatch x with + | (_, _) => reflexivity + | _ => etransitivity; [ | symmetry; apply surjective_pairing ]; reflexivity + end ]; + [ | reflexivity ]; cbn [fst snd]; + recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | [ |- List.Forall2 _ (List.map _ _) _ ] + => rewrite Forall2_map_l_iff + | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] + | [ |- List.Forall _ _ ] => rewrite Forall_forall; intros + | [ |- expr.interp_related_gen _ _ (expr.Ident _) _ ] + => cbn [expr.interp_related_gen ident_interp type.related]; reflexivity end. + Local Ltac fin_tac := + repeat first [ assumption + | progress change S with Nat.succ + | progress cbn [base.interp base.base_interp type.interp] in * + | progress fold (@type.interp _ base.interp) + | progress fold (@base.interp) + | progress subst + | progress cbv [respectful ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.option_rect pointwise_relation] + | progress intros + | solve [ auto ] + | match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- list_rect _ _ _ _ = ident.Thunked.list_rect _ _ _ _ ] + => cbv [ident.Thunked.list_rect]; apply list_rect_Proper; cbv [pointwise_relation]; intros + | [ |- list_rect (fun _ => ?A -> ?B) _ _ _ _ = list_rect _ _ _ _ _ ] + => apply list_rect_arrow_Proper; cbv [respectful]; intros + | [ |- nat_rect _ _ _ _ = ident.Thunked.nat_rect _ _ _ _ ] + => apply nat_rect_Proper_nondep; cbv [respectful] + | [ |- nat_rect (fun _ => ?A -> ?B) _ _ _ _ = nat_rect _ _ _ _ _ ] + => apply (@nat_rect_Proper_nondep_gen (A -> B) (eq ==> eq)%signature); cbv [respectful]; intros + | [ |- list_case _ _ _ ?ls = list_case _ _ _ ?ls ] + => is_var ls; destruct ls; cbn [list_case] + | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ] + => is_var b; destruct b; cbn [bool_rect] + | [ |- _ = ident.cast2 _ _ _ ] => cbv [ident.cast2]; break_innermost_match + end ]. + Local Ltac handle_reified_rewrite_rules_interp := + repeat first [ assumption + | match goal with + | [ |- UnderLets.interp_related _ _ (Reify.expr_value_to_rewrite_rule_replacement _ ?sda _) _ ] + => apply (@Reify.expr_value_to_rewrite_rule_replacement_interp_related cast_outside_of_range _ (@Reify.reflect_ident_iota_interp_related cast_outside_of_range) sda) - Local Ltac unfold_cast_lemmas := - repeat match goal with - | [ H : context[ZRange.normalize (ZRange.constant _)] |- _ ] - => rewrite ZRange.normalize_constant in H - | [ H : is_bounded_by_bool _ (ZRange.normalize ?r) = true |- _ ] - => is_var r; generalize dependent (ZRange.normalize r); clear r; intro r; intros - | [ H : is_bounded_by_bool ?x (ZRange.constant ?x) = true |- _ ] - => clear H - | [ H : is_bounded_by_bool ?x ?r = true |- _ ] - => is_var r; apply unfold_is_bounded_by_bool in H - | [ H : is_bounded_by_bool ?x r[_~>_] = true |- _ ] - => apply unfold_is_bounded_by_bool in H - | [ H : is_tighter_than_bool r[_~>_] r[_~>_] = true |- _ ] - => apply unfold_is_tighter_than_bool in H - | _ => progress cbn [lower upper] in * - | [ H : context[lower ?r] |- _ ] - => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] - | [ H : context[upper ?r] |- _ ] - => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] - | _ => progress Z.ltb_to_lt - end. + | [ |- UnderLets.interp_related_gen ?ii ?R (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.eager_list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_case @ _ @ _ @ _)%expr (@list_case ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_case A (fun _ => P) N C ls) with (@ident.Thunked.list_case A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.nat_rect @ _ @ _ @ _)%expr (@nat_rect (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@nat_rect (fun _ => P) N C ls) with (@ident.Thunked.nat_rect P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.eager_nat_rect @ _ @ _ @ _)%expr (@nat_rect (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@nat_rect (fun _ => P) N C ls) with (@ident.Thunked.nat_rect P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.bool_rect @ _ @ _ @ _)%expr (@bool_rect (fun _ => ?P) ?T ?F ?b) ] + => progress change (@bool_rect (fun _ => P) T F b) with (@ident.Thunked.bool_rect P (fun _ => T) (fun _ => F) b) + | [ |- expr.interp_related_gen ?ii ?R (#ident.option_rect @ _ @ _ @ _)%expr (@option_rect ?A (fun _ => ?P) ?S ?N ?o) ] + => progress change (@option_rect A (fun _ => P) S N o) with (@ident.Thunked.option_rect A P S (fun _ => N) o) - Local Ltac systematically_handle_casts := - remove_casts; unfold_cast_lemmas. + | [ |- match ?x with pair _ _ => _ end = prod_rect _ _ _ ] + => cbv [prod_rect]; eta_expand + + | [ |- expr.interp_related_gen _ _ (expr.Var _) _ ] + => cbn [expr.interp_related_gen] + | [ |- expr.interp_related_gen _ _ (expr.Ident _) _ ] + => cbn [expr.interp_related_gen ident_interp type.related]; fin_tac + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh; cbv beta; intros + | [ |- expr.interp_related_gen _ _ (expr.LetIn ?v ?f) (LetIn.Let_In ?V ?F) ] + => let vh := fresh in + set (vh := v); + let fh := fresh in + set (fh := f); + cbn [expr.interp_related_gen]; subst fh vh; cbv beta; + exists F, V; repeat apply conj; intros + | [ |- expr.interp_related_gen _ _ (?f @ ?x)%expr (?F ?X) ] + => let fh := fresh in + set (fh := f); + let xh := fresh in + set (xh := x); + cbn [expr.interp_related_gen]; subst fh xh; + exists F, X; repeat apply conj; [ | | reflexivity ] + + | [ |- _ = _ ] => solve [ fin_tac ] + end ]. - Local Ltac fin_with_nia := - lazymatch goal with - | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia - | _ => reflexivity || (Z.div_mod_to_quot_rem; (lia + nia)) - end. - Lemma nbe_rewrite_rules_interp_good - : rewrite_rules_interp_goodT nbe_rewrite_rules. + Local Notation specT rewriter_data + := (PrimitiveHList.hlist (@snd bool Prop) (List.skipn (dummy_count rewriter_data) (rewrite_rules_specs rewriter_data))) + (only parsing). + + Lemma nbe_rewrite_rules_interp_good (H : specT nbe_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules nbe_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related ]. - Qed. + Time all: preprocess; handle_extra_nbe; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma arith_rewrite_rules_interp_good max_const - : rewrite_rules_interp_goodT (arith_rewrite_rules max_const). + Lemma arith_rewrite_rules_interp_good max_const (H : specT (arith_rewriter_data max_const)) + : rewrite_rules_interp_goodT (rewrite_rules (arith_rewriter_data max_const) _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith; fin_with_nia ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma arith_with_casts_rewrite_rules_interp_good - : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. + Lemma arith_with_casts_rewrite_rules_interp_good (H : specT arith_with_casts_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules arith_with_casts_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith; fin_with_nia ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. - Lemma strip_literal_casts_rewrite_rules_interp_good - : rewrite_rules_interp_goodT strip_literal_casts_rewrite_rules. + Lemma strip_literal_casts_rewrite_rules_interp_good (H : specT strip_literal_casts_rewriter_data) + : rewrite_rules_interp_goodT (rewrite_rules strip_literal_casts_rewriter_data _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related; repeat interp_good_t_step_arith ]. - Qed. - - Local Ltac fancy_local_t := - repeat match goal with - | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, - H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H' - | [ H : forall s v v', ?invert_low s v = Some v' -> v = _ |- _ ] - => clear invert_low H - end. - Local Ltac more_fancy_arith_t := repeat autorewrite with zsimplify in *. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. 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. + (H : specT (fancy_rewriter_data invert_low invert_high)) + : rewrite_rules_interp_goodT (rewrite_rules (fancy_rewriter_data invert_low invert_high) _). Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step_related ]. - Qed. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. Lemma fancy_with_casts_rewrite_rules_interp_good (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : zrange) (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 value_range flag_range). + (H : specT (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range)) + : rewrite_rules_interp_goodT (rewrite_rules (fancy_with_casts_rewriter_data invert_low invert_high value_range flag_range) _). Proof using Type. - Time start_interp_good. (* Finished transaction in 1.206 secs (1.207u,0.s) (successful) *) - Set Ltac Profiling. - Reset Ltac Profile. - Time all: repeat interp_good_t_step_related. (* Finished transaction in 13.259 secs (13.128u,0.132s) (successful) *) - Reset Ltac Profile. - Time all: fancy_local_t. (* Finished transaction in 0.051 secs (0.052u,0.s) (successful) *) - Time all: systematically_handle_casts. (* Finished transaction in 2.004 secs (1.952u,0.052s) (successful) *) - Time all: try solve [ repeat interp_good_t_step_arith ]. (* Finished transaction in 44.411 secs (44.004u,0.411s) (successful) *) - Qed. + Time start_interp_good. + Time all: preprocess; handle_reified_rewrite_rules_interp. + Time Qed. End with_cast. End RewriteRules. End Compilers. diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 420b5dc90..d3d640dc0 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -35,6 +35,7 @@ Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. +Require Crypto.Util.PrimitiveHList. Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. @@ -299,8 +300,8 @@ Module Compilers. revert v evm T k. induction t; cbn in *; intros; break_innermost_match; try reflexivity; auto. - repeat match goal with H : _ |- _ => etransitivity; rewrite H; clear H; [ | reflexivity ] end. - reflexivity. + repeat match goal with H : _ |- _ => (rewrite H; reflexivity) + (etransitivity; rewrite H; clear H; [ | reflexivity ]) end; + reflexivity. Qed. Ltac add_var_types_cps_id := @@ -386,8 +387,8 @@ Module Compilers. revert v evm T k. induction t; cbn in *; intros; break_innermost_match; try reflexivity; auto using base.add_var_types_cps_id. - repeat match goal with H : _ |- _ => etransitivity; rewrite H; clear H; [ | reflexivity ] end. - reflexivity. + repeat match goal with H : _ |- _ => (rewrite H; reflexivity) + (etransitivity; rewrite H; clear H; [ | reflexivity ]) end; + reflexivity. Qed. Ltac add_var_types_cps_id := @@ -2110,27 +2111,52 @@ Module Compilers. : Prop := wf_with_unif_rewrite_ruleTP_gen_curried G (rew_replacement r1) (rew_replacement r2). - Definition rewrite_rules_goodT_curried - (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) + Fixpoint rewrite_rules_goodT_curried_cps_folded + (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) + (H : List.map (@projT1 _ _) rew1 = List.map (@projT1 _ _) rew2) + (final : Prop) : Prop - := length rew1 = length rew2 - /\ (forall p1 r1 p2 r2, - List.In (existT _ p1 r1, existT _ p2 r2) (combine rew1 rew2) - -> { pf : p1 = p2 - | forall G, - wf_rewrite_rule_data_curried - G - (rew [fun tp => @rewrite_rule_data1 _ (pattern.pattern_of_anypattern tp)] pf in r1) - r2 }). + := match rew1, rew2 return List.map _ rew1 = List.map _ rew2 -> Prop with + | nil, nil => fun _ => final + | nil, _ | _, nil => fun _ => False -> final + | rew1 :: rew1s, rew2 :: rew2s + => fun pf : projT1 rew1 :: List.map _ rew1s = projT1 rew2 :: List.map _ rew2s + => let pfs := f_equal (@tl _) pf in + let pf := f_equal (hd (projT1 rew1)) pf in + (forall G, + wf_rewrite_rule_data_curried + G + (rew [fun tp => @rewrite_rule_data1 _ (pattern.pattern_of_anypattern tp)] pf in projT2 rew1) + (projT2 rew2)) + -> rewrite_rules_goodT_curried_cps_folded rew1s rew2s pfs final + end H. + + Definition rewrite_rules_goodT_curried_cps + := Eval cbv [id + rewrite_rules_goodT_curried_cps_folded + eq_rect f_equal hd tl List.map + wf_deep_rewrite_ruleTP_gen wf_rewrite_rule_data_curried rew_replacement rew_should_do_again rew_with_opt rew_under_lets wf_with_unif_rewrite_ruleTP_gen_curried wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern wf_maybe_under_lets_expr wf_maybe_do_again_expr wf_with_unification_resultT pattern.type.under_forall_vars_relation with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default pattern.base.lookup_default PositiveSet.rev PositiveMap.empty under_with_unification_resultT_relation_hetero under_with_unification_resultT'_relation_hetero maybe_option_eq + List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb] in + rewrite_rules_goodT_curried_cps_folded. + + Lemma rewrite_rules_goodT_curried_cps_folded_Proper_impl rews1 rews2 H + : Proper (Basics.impl ==> Basics.impl) (rewrite_rules_goodT_curried_cps_folded rews1 rews2 H). + Proof using Type. + cbv [impl]; intros P Q H'. + revert dependent rews2; induction rews1, rews2; cbn; auto. + Qed. + Lemma rewrite_rules_goodT_curried_cps_Proper_impl rews1 rews2 H + : Proper (Basics.impl ==> Basics.impl) (rewrite_rules_goodT_curried_cps rews1 rews2 H). + Proof using Type. + apply rewrite_rules_goodT_curried_cps_folded_Proper_impl. + Qed. - Lemma rewrite_rules_goodT_by_curried rew1 rew2 - : rewrite_rules_goodT_curried rew1 rew2 -> rewrite_rules_goodT rew1 rew2. + Lemma wf_rewrite_rule_data_by_curried G t p r1 r2 + : @wf_rewrite_rule_data_curried G t p r1 r2 + -> @wf_rewrite_rule_data G t p r1 r2. Proof using Type. - cbv [rewrite_rules_goodT rewrite_rules_goodT_curried wf_rewrite_rule_data_curried wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen wf_with_unif_rewrite_ruleTP_gen_curried]. - intros [Hlen H]; split; [ exact Hlen | clear Hlen ]. - repeat (let x := fresh "x" in intro x; specialize (H x)). - destruct H as [H0 H]; exists H0. - repeat (let x := fresh "x" in intro x; specialize (H x)). + cbv [wf_rewrite_rule_data_curried wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen wf_with_unif_rewrite_ruleTP_gen_curried]. + intro H. intros X Y HXY. pose proof (wf_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) ltac:(eassumption)) as H'. cps_id'_with_option app_with_unification_resultT_cps_id. @@ -2147,6 +2173,34 @@ Module Compilers. | exfalso; assumption | assumption ]. Qed. + + Lemma rewrite_rules_goodT_by_curried + (rews1 : rewrite_rulesT1) (rews2 : rewrite_rulesT2) + (H : List.map (@projT1 _ _) rews1 = List.map (@projT1 _ _) rews2) + : rewrite_rules_goodT_curried_cps rews1 rews2 H (rewrite_rules_goodT rews1 rews2). + Proof using Type. + change rewrite_rules_goodT_curried_cps with rewrite_rules_goodT_curried_cps_folded. + cbv [rewrite_rules_goodT]. + revert rews2 H; induction rews1 as [|[r p] rews1 IHrews], rews2 as [|[? ?] ?]; intro H. + all: try solve [ cbn; tauto ]. + all: cbn [rewrite_rules_goodT_curried_cps_folded List.In projT2 projT1 Datatypes.fst Datatypes.snd] in *. + all: intro H'; eapply rewrite_rules_goodT_curried_cps_folded_Proper_impl; [ | eapply IHrews ]. + all: repeat first [ progress cbv [impl] + | progress destruct_head'_or + | progress inversion_sigma + | progress subst + | progress destruct_head'_and + | progress destruct_head'_sig + | progress destruct_head'_or + | progress inversion_prod + | progress inversion_sigma + | (exists eq_refl) + | apply conj + | apply (f_equal S) + | progress cbn [eq_rect Datatypes.snd List.length List.In List.combine] in * + | solve [ eauto using wf_rewrite_rule_data_by_curried ] + | progress intros ]. + Qed. End with_var2. Section with_interp. @@ -2165,16 +2219,13 @@ Module Compilers. := (if with_lets as with_lets' return (if with_lets' then UnderLets var _ else _) -> _ then UnderLets.interp ident_interp else (fun x => x)). - Local Notation UnderLets_maybe_wf with_lets G := (if with_lets as with_lets' return (if with_lets' then UnderLets var _ else _) -> (if with_lets' then UnderLets var _ else _) -> _ then UnderLets.wf (fun G' => expr.wf G') G else expr.wf G). - Definition value'_interp {with_lets t} (v : @value' var with_lets t) : var t := expr.interp ident_interp (reify v). - Local Notation expr_interp_related := (@expr.interp_related _ ident _ ident_interp). Local Notation UnderLets_interp_related := (@UnderLets.interp_related _ ident _ ident_interp _ _ expr_interp_related). @@ -2188,7 +2239,6 @@ Module Compilers. @value_interp_related s _ x1 x2 -> @value_interp_related d _ (f1 x1) (f2 x2) end. - Fixpoint rawexpr_interp_related (r1 : rawexpr) : type.interp base.interp (type_of_rawexpr r1) -> Prop := match r1 return type.interp base.interp (type_of_rawexpr r1) -> Prop with | rExpr _ e1 @@ -2213,15 +2263,12 @@ Module Compilers. | _ => fun _ => False end end. - Definition unification_resultT'_interp_related {t p evm} : @unification_resultT' (@value var) t p evm -> @unification_resultT' var t p evm -> Prop := related_unification_resultT' (fun t => value_interp_related). - Definition unification_resultT_interp_related {t p} : @unification_resultT (@value var) t p -> @unification_resultT var t p -> Prop := related_unification_resultT (fun 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. @@ -2232,7 +2279,6 @@ Module Compilers. 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 @@ -2253,7 +2299,6 @@ Module Compilers. | apply interp_reify_reflect | solve [ auto ] ]. Qed. - Fixpoint reify_interp_related {t with_lets} v1 v2 {struct t} : @value_interp_related t with_lets v1 v2 -> expr_interp_related (reify v1) v2 @@ -2287,7 +2332,6 @@ Module Compilers. | match goal with H : _ |- _ => apply H; clear H end | progress repeat esplit ]. Qed. - Lemma expr_of_rawexpr_interp_related r v : rawexpr_interp_related r v -> expr_interp_related (expr_of_rawexpr r) v. @@ -2305,7 +2349,6 @@ Module Compilers. | solve [ eauto ] | apply reify_interp_related ]. Qed. - Lemma value_of_rawexpr_interp_related {e v} : rawexpr_interp_related e v -> value_interp_related (value_of_rawexpr e) v. Proof using Type. @@ -2323,7 +2366,6 @@ Module Compilers. | progress cbv [expr.interp_related] | solve [ eauto ] ]. Qed. - Lemma rawexpr_interp_related_Proper_rawexpr_equiv_expr {t e re v} (H : rawexpr_equiv_expr e re) : @expr_interp_related t e v @@ -2358,7 +2400,6 @@ Module Compilers. => do 4 eexists; repeat apply conj; [ eassumption | eassumption | | | reflexivity ] end ]. Qed. - Lemma rawexpr_interp_related_Proper_rawexpr_equiv_expr_no_rew {re e v} (H : rawexpr_equiv_expr e re) : @expr_interp_related _ e v @@ -2369,7 +2410,6 @@ Module Compilers. generalize (eq_type_of_rawexpr_equiv_expr H); intro; eliminate_hprop_eq. exact id. Qed. - Lemma rawexpr_interp_related_Proper_rawexpr_equiv_expr_rew_gen {t e re v} (H : rawexpr_equiv_expr e re) : forall pf, @@ -2378,7 +2418,6 @@ Module Compilers. Proof using Type. intro; subst; apply rawexpr_interp_related_Proper_rawexpr_equiv_expr_no_rew; assumption. Qed. - Lemma rawexpr_interp_related_Proper_rawexpr_equiv {re1 re2 v} (H : rawexpr_equiv re1 re2) : rawexpr_interp_related re1 v @@ -2453,6 +2492,52 @@ Module Compilers. => k (ef ex))) end. + Lemma interp_Base_value {t v1 v2} + : value_interp_related v1 v2 + -> value_interp_related (@Base_value var t v1) v2. + Proof using Type. + cbv [Base_value]; destruct t; exact id. + Qed. + + Lemma interp_splice_under_lets_with_value_of_ex {T T' t R e f v} + : (exists fv (xv : T'), + UnderLets.interp_related ident_interp R e xv + /\ (forall x1 x2, + R x1 x2 + -> value_interp_related (f x1) (fv x2)) + /\ fv xv = v) + -> value_interp_related (@splice_under_lets_with_value var T t e f) v. + Proof using Type. + induction t as [|s IHs d IHd]. + all: repeat first [ progress cbn [value_interp_related splice_under_lets_with_value] in * + | progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | eassumption + | solve [ eauto ] + | now (eapply UnderLets.splice_interp_related_of_ex; eauto) + | match goal with + | [ H : _ |- _ ] => eapply H; clear H + | [ |- exists fv xv, _ /\ _ /\ _ ] + => do 2 eexists; repeat apply conj; [ eassumption | | ] + end ]. + Qed. + + Lemma interp_splice_value_with_lets_of_ex {t t' e f v} + : (exists fv xv, + value_interp_related e xv + /\ (forall x1 x2, + value_interp_related x1 x2 + -> value_interp_related (f x1) (fv x2)) + /\ fv xv = v) + -> value_interp_related (@splice_value_with_lets var t t' e f) v. + Proof using Type. + cbv [splice_value_with_lets]; break_innermost_match. + { apply interp_splice_under_lets_with_value_of_ex. } + { intros; destruct_head'_ex; destruct_head'_and; subst; eauto. } + Qed. + Definition pattern_default_interp {t} (p : pattern t) : @with_unification_resultT var t p var (*: @with_unif_rewrite_ruleTP_gen var t p false false false*) @@ -2542,17 +2627,44 @@ Module Compilers. (rew_replacement r) (pattern_default_interp p). - Definition rewrite_rules_interp_goodT_curried - (rews : rewrite_rulesT) - : Prop - := forall p r, - List.In (existT _ p r) rews - -> rewrite_rule_data_interp_goodT_curried r. + Fixpoint rewrite_rules_interp_goodT_curried_cps_folded + (rews : rewrite_rulesT) + (specs : list (bool * Prop)) + (final : Prop) + := match rews with + | r :: rews + => (snd (hd (true, True) specs) + -> rewrite_rule_data_interp_goodT_curried (projT2 r)) + -> rewrite_rules_interp_goodT_curried_cps_folded rews (tl specs) final + | nil => final + end. + + Definition rewrite_rules_interp_goodT_curried_cps + := Eval cbv [id + rewrite_rules_interp_goodT_curried_cps_folded snd hd tl projT2 rewrite_rule_data_interp_goodT_curried + rewrite_rule_data_interp_goodT_curried under_with_unification_resultT_relation_hetero under_with_unification_resultT'_relation_hetero wf_with_unification_resultT under_type_of_list_relation_cps under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern rew_replacement rew_should_do_again rew_with_opt rew_under_lets wf_with_unification_resultT pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 deep_rewrite_ruleTP_gen with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements lam_type_of_list id pattern.ident.to_typed under_type_of_list_relation_cps deep_rewrite_ruleTP_gen_good_relation normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add option_bind' wf_value value pattern.base.subst_default pattern.base.lookup_default PositiveMap.find rewrite_ruleTP ident.smart_Literal value_interp_related + Reify.expr_value_to_rewrite_rule_replacement UnderLets.flat_map reify_expr_beta_iota reflect_expr_beta_iota reflect_ident_iota Compile.reify_to_UnderLets UnderLets.of_expr Compile.Base_value + List.map List.fold_right List.rev list_rect orb List.app + ] in + rewrite_rules_interp_goodT_curried_cps_folded. + + Lemma rewrite_rules_interp_goodT_curried_cps_folded_Proper_impl rews specs + : Proper (Basics.impl ==> Basics.impl) (rewrite_rules_interp_goodT_curried_cps_folded rews specs). + Proof using Type. + cbv [impl]; intros P Q H. + revert specs; induction rews, specs; cbn; auto. + Qed. + Lemma rewrite_rules_interp_goodT_curried_cps_Proper_impl rews specs + : Proper (Basics.impl ==> Basics.impl) (rewrite_rules_interp_goodT_curried_cps rews specs). + Proof using Type. + apply rewrite_rules_interp_goodT_curried_cps_folded_Proper_impl. + Qed. - Lemma rewrite_rules_interp_goodT_by_curried rews - : rewrite_rules_interp_goodT_curried rews -> rewrite_rules_interp_goodT rews. + Lemma rewrite_rule_data_interp_goodT_by_curried t p r + : @rewrite_rule_data_interp_goodT_curried t p r + -> @rewrite_rule_data_interp_goodT t p r. Proof using Type. - cbv [rewrite_rules_interp_goodT rewrite_rules_interp_goodT_curried rewrite_rule_data_interp_goodT rewrite_rule_data_interp_goodT_curried]. + cbv [rewrite_rule_data_interp_goodT rewrite_rule_data_interp_goodT_curried]. intro H. repeat (let x := fresh "x" in intro x; specialize (H x)). intros X Y HXY. @@ -2567,13 +2679,36 @@ Module Compilers. | exfalso; assumption | assumption ]. Qed. + + Lemma rewrite_rules_interp_goodT_by_curried rews specs + (proofs : PrimitiveHList.hlist (@snd bool Prop) specs) + : rewrite_rules_interp_goodT_curried_cps rews specs (rewrite_rules_interp_goodT rews). + Proof using Type. + change rewrite_rules_interp_goodT_curried_cps with rewrite_rules_interp_goodT_curried_cps_folded. + cbv [rewrite_rules_interp_goodT]. + revert specs proofs. + induction rews as [|[r p] rews IHrews], specs as [|[? ?] specs]; + cbn [PrimitiveHList.hlist]; + intro proofs; destruct_head' PrimitiveProd.Primitive.prod. + all: try solve [ cbn; tauto ]. + all: cbn [rewrite_rules_interp_goodT_curried_cps_folded List.In projT2 projT1 Datatypes.fst Datatypes.snd] in *. + all: intro H; eapply rewrite_rules_interp_goodT_curried_cps_folded_Proper_impl; [ | eapply IHrews ]. + all: repeat first [ progress cbv [impl] + | progress destruct_head'_or + | progress inversion_sigma + | progress subst + | progress cbn [eq_rect Datatypes.snd hd tl] in * + | solve [ eauto using rewrite_rule_data_interp_goodT_by_curried ] + | progress intros ]. + Qed. End with_interp. End with_var. End Compile. - (** Now we prove the [wf] properties about definitions used only - in reification of rewrite rules, which are used to make proving - [wf] of concrete rewrite rules easier. *) + (** Now we prove the [wf] and [interp] properties about + definitions used only in reification of rewrite rules, which + are used to make proving [wf] / [interp] of concrete rewrite + rules easier. *) Module Reify. Import Compile. Import Rewriter.Compilers.RewriteRules.Compile. @@ -2713,7 +2848,7 @@ Module Compilers. | progress handle_wf_rec ltac:(fun tac => try tac (); tac ()) ]. Ltac reify_wf_t := repeat reify_wf_t_step. - Section with_var. + Section with_var2. Context {var1 var2 : type -> Type}. Lemma wf_reflect_ident_iota G {t} (idc : ident t) @@ -2871,7 +3006,266 @@ Module Compilers. | constructor | solve [ eauto ] ]. } Qed. - End with_var. + End with_var2. + + Section with_interp. + Context (cast_outside_of_range : ZRange.zrange -> Z -> Z). + + Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). + Local Notation var := (type.interp base.interp) (only parsing). + Local Notation expr := (@expr.expr base.type ident var). + Local Notation expr_interp_related := (@expr.interp_related _ ident _ (@ident_interp)). + Local Notation UnderLets_interp_related := (@UnderLets.interp_related _ ident _ (@ident_interp) _ _ expr_interp_related). + Local Notation value_interp_related := (@value_interp_related ident (@ident_interp)). + + Local Ltac fin_t := + repeat first [ reflexivity + | progress intros + | progress subst + | progress destruct_head'_unit + | solve [ eauto ] + | match goal with + | [ |- expr.interp_related _ (reify_list _) _ ] + => rewrite expr.reify_list_interp_related_iff + end + | match goal with H : _ |- _ => apply H end ]. + + (** TODO: MOVE ME *) + Local Ltac specialize_refls H := + lazymatch type of H with + | forall x y : ?T, x = y -> _ + => let H' := fresh in + constr:(fun x : T + => match H x x eq_refl return _ with + | H' + => ltac:(let v := specialize_refls H' in + exact v) + end) + | forall x : ?T, _ + => let H' := fresh in + constr:(fun x : T + => match H x return _ with + | H' => ltac:(let v := specialize_refls H' in exact v) + end) + | _ => H + end. + + Lemma reflect_ident_iota_interp_related {t} (idc : ident t) v1 v2 + : @reflect_ident_iota var t idc = Some v1 + -> ident_interp idc == v2 + -> value_interp_related v1 v2. + Proof using Type. + destruct idc; cbv [reflect_ident_iota]; intro; inversion_option; subst. + all: repeat + repeat + first [ progress expr.invert_subst + | progress cbn [type.related type.interp base.interp base.base_interp ident_interp value_interp_related expr.interp_related expr.interp_related_gen reify reflect value'] in * + | progress cbv [respectful value] in * + | progress intros + | progress subst + | break_innermost_match_step + | match goal with + | [ H : List.Forall2 _ ?l1 ?l2, H' : ?R ?v1 ?v2 |- ?R (nth_default ?v1 ?l1 ?x) (nth_default ?v2 ?l2 ?x) ] + => apply Forall2_forall_iff''; split; assumption + | [ H : context[expr.interp_related _ (reify_list _)] |- _ ] + => rewrite expr.reify_list_interp_related_iff in H + | [ |- expr.interp_related_gen _ _ (reify_list _) _ ] + => rewrite expr.reify_list_interp_related_gen_iff + | [ |- UnderLets_interp_related (nat_rect _ _ _ _) (?f ?x ?y ?z) ] + => let v' := open_constr:(ident.Thunked.nat_rect _ x y z) in + replace (f x y z) with v'; + [ apply UnderLets.nat_rect_interp_related + | cbv [ident.Thunked.nat_rect]; solve [ fin_t ] ]; + try solve [ fin_t ]; intros + | [ |- UnderLets_interp_related (nat_rect _ _ _ _ _) (?f ?x ?y ?z ?w) ] + => let v' := open_constr:(nat_rect _ x y z w) in + replace (f x y z w) with v'; + [ eapply UnderLets.nat_rect_arrow_interp_related + | try solve [ fin_t ] ]; + try solve [ fin_t ]; intros + | [ H : context[list_rect (fun _ => ?B') _ _ _ = ?f _ _ _] + |- UnderLets.interp_related + ?ident_interp ?R + (list_rect + (fun _ : list (expr ?A) => UnderLets _ ?B) + ?Pnil + ?Pcons + ?ls) + (?f ?Pnil' ?Pcons' ?ls') ] + => erewrite <- H; + [ eapply (@UnderLets.list_rect_interp_related _ _ _ ident_interp A B Pnil Pcons ls B' (Pnil' tt) Pcons' ls' R) + | .. ]; try solve [ fin_t ]; intros + | [ H : context[list_rect (fun _ => ?B' -> ?C') _ _ _ _ = ?f _ _ _ _] + |- UnderLets.interp_related + ?ident_interp ?R + (list_rect + (fun _ : list (expr ?A) => ?B -> UnderLets _ ?C) + ?Pnil + ?Pcons + ?ls + ?x) + (?f ?Pnil' ?Pcons' ?ls' ?x') ] + => erewrite <- H; + [ eapply (@UnderLets.list_rect_arrow_interp_related _ _ _ ident_interp A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R (expr.interp_related ident_interp)) + | .. ]; try solve [ fin_t ]; intros + end + | rewrite <- UnderLets.to_expr_interp_related_gen_iff + | eapply UnderLets.splice_interp_related_of_ex; + do 2 eexists; repeat apply conj; + [ now eauto | intros | reflexivity ]; + try solve [ fin_t ] + | progress (cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related expr.interp_related_gen]; + repeat (do 2 eexists; repeat apply conj; intros)) + | solve + [ repeat + first + [ progress fin_t + | progress cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related expr.interp_related_gen type.related] + | progress cbv [respectful] + | progress repeat (do 2 eexists; repeat apply conj; intros) ] ] + | match goal with + | [ H : context[forall x y, x = y -> _] |- _ ] + => let H' := specialize_refls H in + specialize H' + | [ H : forall x y z, nth_default x y z = ?f x y z |- ?R (nth_default _ _ _) (?f _ _ _) ] + => rewrite <- H; clear f H + end + | progress fin_t ]. + all: repeat first [ progress fin_t + | match goal with + | [ H : context[forall x y, x = y -> _] |- _ ] + => let H' := specialize_refls H in + specialize H' + end ]. + all: repeat match goal with + | [ H : forall x x' Hx y y' Hy z z' Hz, UnderLets_interp_related _ (?f _ _ _) |- ?f _ _ _ = ?f _ _ _ ] + => etransitivity; [ symmetry | ]; + apply (fun x x' Hx y y' Hy z z' Hz => UnderLets.eqv_of_interp_related _ (H x x' Hx y y' Hy z z' Hz)) + | [ H : forall x x' Hx y y' Hy z z' Hz w w' Hw, UnderLets_interp_related _ (?f _ _ _ _) |- ?f _ _ _ _ = ?f _ _ _ _ ] + => etransitivity; [ symmetry | ]; + apply (fun x x' Hx y y' Hy z z' Hz w w' Hw => UnderLets.eqv_of_interp_related _ (H x x' Hx y y' Hy z z' Hz w w' Hw)) + end. + all: cbn [type.interp base.interp base.base_interp]; intros. + all: repeat first [ progress cbn [UnderLets_interp_related UnderLets.interp_related_gen type.related] in * + | progress cbv [GallinaReify.Reify_as GallinaReify.reify] + | progress subst + | match goal with + | [ |- expr_interp_related ?ev ?v ] + => is_evar ev; instantiate (1:=GallinaReify.Reify v _); + cbn [expr_interp_related expr.interp_related_gen] + | [ |- UnderLets_interp_related (?f _) (?g _) ] + => is_evar f; + instantiate (1:=fun e => UnderLets.Base (GallinaReify.Reify (g (expr.interp (@ident_interp) e)) _)) + | [ |- expr_interp_related (GallinaReify.base.reify _) _ ] + => apply expr.reify_interp_related + | [ H : forall x, ?f x = ?g x |- expr_interp_related _ (?g _) ] + => rewrite <- H + | [ H : expr_interp_related _ _ |- _ ] => apply expr.eqv_of_interp_related in H + end ]. + Qed. + + Lemma reflect_expr_beta_iota_interp_related + {reflect_ident_iota} + (Hreflect_ident_iota + : forall t idc v1 v2, + reflect_ident_iota t idc = Some v1 + -> ident_interp idc == v2 + -> value_interp_related v1 v2) + {t} e v + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : UnderLets.interp_related + (@ident_interp) value_interp_related + (@reflect_expr_beta_iota ident _ reflect_ident_iota t e) + v. + Proof using Type. + revert dependent v; induction e; cbn [reflect_expr_beta_iota]; intros. + all: repeat first [ assumption + | match goal with + | [ |- UnderLets.interp_related_gen _ _ _ (UnderLets.splice (reflect_expr_beta_iota _ _) _) _ ] + => eapply UnderLets.splice_interp_related_gen_of_ex; + do 2 eexists; repeat apply conj; + [ match goal with + | [ IH : context[UnderLets.interp_related _ _ (reflect_expr_beta_iota _ _) _] |- _ ] + => eapply IH; eassumption + end + | intros | ] + | [ |- UnderLets.interp_related_gen _ _ _ (UnderLets.UnderLet (reify _) _) _ ] + => cbn [UnderLets.interp_related_gen]; + do 2 eexists; repeat apply conj; + [ apply reify_interp_related; eassumption + | intros | reflexivity ] + | [ |- UnderLets.interp_related _ _ (UnderLets.Base _) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen] + | [ |- value_interp_related (splice_under_lets_with_value _ _) _ ] + => eapply interp_splice_under_lets_with_value_of_ex; + do 2 eexists; repeat apply conj; intros + | [ |- value_interp_related (Base_value _) _ ] + => apply interp_Base_value + | [ |- value_interp_related (reflect _) _ ] => apply reflect_interp_related + end + | break_innermost_match_step + | solve [ eauto ] + | progress cbn [value_interp_related]; intros + | progress cbn [expr.interp_related_gen] in * + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | progress cbv [UnderLets.interp_related] + | solve [ cbn [value_interp_related UnderLets.interp_related_gen] in *; eauto; repeat match goal with H : _ |- _ => eapply H end ] + | reflexivity + | match goal with H : _ |- _ => apply H end ]. + Qed. + + Lemma reify_expr_beta_iota_interp_related + {reflect_ident_iota} + (Hreflect_ident_iota + : forall t idc v1 v2, + reflect_ident_iota t idc = Some v1 + -> ident_interp idc == v2 + -> value_interp_related v1 v2) + {t} e v + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : UnderLets_interp_related + (@reify_expr_beta_iota ident _ reflect_ident_iota t e) + v. + Proof using Type. + cbv [reify_expr_beta_iota reify_to_UnderLets]. + eapply UnderLets.splice_interp_related_of_ex; do 2 eexists; repeat apply conj; + [ eapply reflect_expr_beta_iota_interp_related; eauto | | instantiate (1:=fun x => x); reflexivity ]; cbv beta. + intros; break_innermost_match; cbn [UnderLets.interp_related UnderLets.interp_related_gen value_interp_related] in *; try eassumption. + apply reify_interp_related; eauto. + Qed. + + Lemma expr_value_to_rewrite_rule_replacement_interp_related + {reflect_ident_iota} + (Hreflect_ident_iota + : forall t idc v1 v2, + reflect_ident_iota t idc = Some v1 + -> ident_interp idc == v2 + -> value_interp_related v1 v2) + (should_do_again : bool) + {t} e v + (He : expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) e v) + : UnderLets.interp_related + (@ident_interp) (if should_do_again + return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> type.interp base.interp t -> Prop + then expr.interp_related_gen (@ident_interp) (fun t => value_interp_related) + else expr_interp_related) + (@expr_value_to_rewrite_rule_replacement ident var reflect_ident_iota should_do_again t e) + v. + Proof using Type. + cbv [expr_value_to_rewrite_rule_replacement]. + apply UnderLets.splice_interp_related_of_ex + with (RA:=expr.interp_related_gen (@ident_interp) (fun t => value_interp_related)); + do 2 eexists; repeat apply conj; intros; [ | | instantiate (2:=fun x => x); reflexivity ]; cbv beta. + { apply UnderLets.flat_map_interp_related_iff with (R'':=fun t => value_interp_related); + [ intros; now apply reify_expr_beta_iota_interp_related + | intros; apply reflect_interp_related; cbn; assumption + | now rewrite UnderLets.of_expr_interp_related_gen_iff ]. } + { break_innermost_match; cbn [UnderLets.interp_related UnderLets.interp_related_gen]; + now try apply reify_expr_beta_iota_interp_related. } + Qed. + End with_interp. End Reify. End RewriteRules. End Compilers. -- cgit v1.2.3