aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-03 16:43:48 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-04-09 21:59:06 -0400
commit067d1f14b03d83dcb1c0a60808919ceff6205836 (patch)
treeab6612a1c1a07321a264b4c3e02d31eb7baac8ff
parentde6be31e9e0f6be7ca2f61159d6a5a0e6f3969be (diff)
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%
-rw-r--r--src/Rewriter.v888
-rw-r--r--src/RewriterInterpProofs1.v46
-rw-r--r--src/RewriterProofs.v64
-rw-r--r--src/RewriterRules.v3
-rw-r--r--src/RewriterRulesGood.v199
-rw-r--r--src/RewriterRulesInterpGood.v1064
-rw-r--r--src/RewriterWf1.v496
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.