diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-08 02:33:39 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-03-31 09:36:16 -0400 |
| commit | 339ee4ec95624751f84997064a6a985478ca5645 (patch) | |
| tree | 1da8b103fa9a46a48270647dfc665f61eb3aebcb | |
| parent | a8b4394093e61b050406ca952a6d017ad1c737e4 (diff) | |
Finish reifying list lemmas
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
22m23.84s | Total | 21m34.63s || +0m49.21s | +3.80%
--------------------------------------------------------------------------------------------
1m52.62s | RewriterRulesInterpGood.vo | 1m37.14s || +0m15.48s | +15.93%
3m25.91s | p384_32.c | 3m14.24s || +0m11.66s | +6.00%
1m32.94s | RewriterRulesGood.vo | 1m42.36s || -0m09.42s | -9.20%
0m33.72s | RewriterWf1.vo | 0m24.30s || +0m09.41s | +38.76%
1m17.31s | Rewriter.vo | 1m12.10s || +0m05.21s | +7.22%
0m43.01s | ExtractionHaskell/unsaturated_solinas | 0m39.84s || +0m03.16s | +7.95%
0m45.21s | p521_32.c | 0m42.86s || +0m02.35s | +5.48%
1m46.30s | Fancy/Barrett256.vo | 1m45.08s || +0m01.21s | +1.16%
0m38.74s | p521_64.c | 0m37.49s || +0m01.25s | +3.33%
0m23.16s | ExtractionOCaml/word_by_word_montgomery | 0m21.44s || +0m01.71s | +8.02%
0m18.74s | p256_32.c | 0m16.88s || +0m01.85s | +11.01%
0m15.00s | ExtractionOCaml/unsaturated_solinas | 0m13.98s || +0m01.01s | +7.29%
0m11.92s | ExtractionOCaml/saturated_solinas | 0m10.13s || +0m01.78s | +17.67%
0m07.82s | ExtractionOCaml/saturated_solinas.ml | 0m05.98s || +0m01.83s | +30.76%
1m47.42s | RewriterWf2.vo | 1m47.81s || -0m00.39s | -0.36%
0m58.35s | ExtractionHaskell/word_by_word_montgomery | 0m57.41s || +0m00.94s | +1.63%
0m45.47s | RewriterInterpProofs1.vo | 0m45.67s || -0m00.20s | -0.43%
0m37.34s | Fancy/Montgomery256.vo | 0m37.09s || +0m00.25s | +0.67%
0m36.14s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.52s || -0m00.38s | -1.04%
0m29.91s | ExtractionHaskell/saturated_solinas | 0m29.70s || +0m00.21s | +0.70%
0m26.77s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.72s || +0m00.05s | +0.18%
0m25.87s | SlowPrimeSynthesisExamples.vo | 0m25.49s || +0m00.38s | +1.49%
0m18.72s | p448_solinas_64.c | 0m19.16s || -0m00.44s | -2.29%
0m16.94s | secp256k1_32.c | 0m17.18s || -0m00.23s | -1.39%
0m13.92s | p434_64.c | 0m13.08s || +0m00.83s | +6.42%
0m13.15s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.58s || +0m00.57s | +4.53%
0m08.97s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.95s || +0m00.02s | +0.22%
0m08.37s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s || -0m00.14s | -1.64%
0m08.35s | p224_32.c | 0m08.10s || +0m00.25s | +3.08%
0m07.77s | p384_64.c | 0m07.29s || +0m00.47s | +6.58%
0m06.92s | BoundsPipeline.vo | 0m06.85s || +0m00.07s | +1.02%
0m05.70s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.14s || -0m00.43s | -7.16%
0m05.12s | ExtractionHaskell/saturated_solinas.hs | 0m06.09s || -0m00.96s | -15.92%
0m03.53s | PushButtonSynthesis/Primitives.vo | 0m03.55s || -0m00.02s | -0.56%
0m03.38s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.04s | +1.19%
0m03.16s | PushButtonSynthesis/BarrettReduction.vo | 0m03.24s || -0m00.08s | -2.46%
0m03.06s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.23s || -0m00.16s | -5.26%
0m02.81s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.84s || -0m00.02s | -1.05%
0m02.62s | curve25519_32.c | 0m02.22s || +0m00.39s | +18.01%
0m01.88s | p224_64.c | 0m01.47s || +0m00.40s | +27.89%
0m01.68s | curve25519_64.c | 0m02.19s || -0m00.51s | -23.28%
0m01.32s | CLI.vo | 0m01.33s || -0m00.01s | -0.75%
0m01.24s | secp256k1_64.c | 0m01.30s || -0m00.06s | -4.61%
0m01.22s | p256_64.c | 0m01.47s || -0m00.25s | -17.00%
0m01.16s | RewriterProofs.vo | 0m01.16s || +0m00.00s | +0.00%
0m01.10s | StandaloneHaskellMain.vo | 0m01.00s || +0m00.10s | +10.00%
0m01.05s | CompilersTestCases.vo | 0m01.09s || -0m00.04s | -3.66%
0m01.04s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.00s | +0.00%
| -rw-r--r-- | src/Rewriter.v | 469 | ||||
| -rw-r--r-- | src/RewriterRulesGood.v | 256 | ||||
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 185 | ||||
| -rw-r--r-- | src/RewriterWf1.v | 300 | ||||
| -rw-r--r-- | src/SlowPrimeSynthesisExamples.v | 108 |
5 files changed, 1015 insertions, 303 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 2ccfb342d..f03cf69d2 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -17,6 +17,7 @@ Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.GENERATEDIdentifiersWithoutTypes. Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. @@ -495,7 +496,8 @@ Module Compilers. Let type_base (t : base.type) : type := type.base t. Coercion type_base : base.type >-> type. - Context (reify_and_let_binds_base_cps : forall (t : base.type), expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T). + Context (reify_and_let_binds_base_cps : forall (t : base.type), expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T) + (reflect_ident_iota : forall t (idc : ident t), option (value t)). Definition under_type_of_list_cps {A1 A2 ls} (F : A1 -> A2) @@ -574,30 +576,36 @@ Module Compilers. end. (** N.B. In order to preserve the (currently unstated) - invariant that ensures that the rewriter does enough - rewriting, when we reify rewrite rules, we have to perform β - on the RHS to ensure that there are no var nodes holding - values which show up in the heads of app nodes. *) - Fixpoint reflect_expr_beta {t} (e : @expr.expr base.type ident value t) + invariant that ensures that the rewriter does enough + rewriting, when we reify rewrite rules, we have to + perform β on the RHS to ensure that there are no var + nodes holding values which show up in the heads of app + nodes. Note that we also perform βιδ on "eager" + identifiers, which is what allows us to handle + [list_rect] and [nat_rect] recursion rules. *) + Fixpoint reflect_expr_beta_iota {t} (e : @expr.expr base.type ident value t) : UnderLets (value t) := match e in expr.expr t return UnderLets (value t) with | expr.Var t v => UnderLets.Base v - | expr.Abs s d f => UnderLets.Base (fun x : value s => fx <----- @reflect_expr_beta d (f x); Base_value fx) + | expr.Abs s d f => UnderLets.Base (fun x : value s => fx <----- @reflect_expr_beta_iota d (f x); Base_value fx) | expr.App s (type.base d) f x - => f <-- @reflect_expr_beta _ f; - x <-- @reflect_expr_beta _ x; + => f <-- @reflect_expr_beta_iota _ f; + x <-- @reflect_expr_beta_iota _ x; f x | expr.App s (type.arrow _ _) f x - => f <-- @reflect_expr_beta _ f; - x <-- @reflect_expr_beta _ x; + => f <-- @reflect_expr_beta_iota _ f; + x <-- @reflect_expr_beta_iota _ x; UnderLets.Base (f x) | expr.LetIn A B x f - => x <-- @reflect_expr_beta _ x; + => x <-- @reflect_expr_beta_iota _ x; UnderLets.UnderLet (reify x) - (fun xv => @reflect_expr_beta _ (f (reflect (expr.Var xv)))) - | expr.Ident t idc => UnderLets.Base (reflect (expr.Ident idc)) - end%under_lets. + (fun xv => @reflect_expr_beta_iota _ (f (reflect (expr.Var xv)))) + | expr.Ident t idc => UnderLets.Base match reflect_ident_iota t idc with + | Some ridc => ridc + | None => reflect (expr.Ident idc) + end + end%under_lets%option. Definition reify_to_UnderLets {with_lets} {t} : value' with_lets t -> UnderLets (expr t) := match t, with_lets return value' with_lets t -> UnderLets (expr t) with @@ -607,9 +615,9 @@ Module Compilers. => fun f => UnderLets.Base (reify f) end. - Definition reify_expr_beta {t} (e : @expr.expr base.type ident value t) + Definition reify_expr_beta_iota {t} (e : @expr.expr base.type ident value t) : UnderLets (@expr.expr base.type ident var t) - := e <-- @reflect_expr_beta t e; reify_to_UnderLets e. + := e <-- @reflect_expr_beta_iota t e; reify_to_UnderLets e. Definition reify_and_let_binds_cps {with_lets} {t} : value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T := match t, with_lets return value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T with @@ -1277,6 +1285,164 @@ Module Compilers. Local Notation UnderLets := (UnderLets.UnderLets base.type ident var). Local Notation reify_and_let_binds_cps := (@Compile.reify_and_let_binds_cps ident var (@UnderLets.reify_and_let_binds_base_cps var)). Local Notation reflect := (@Compile.reflect ident var). + Let type_base := @type.base base.type. + Local Coercion type_base : base.type >-> type.type. + + (* N.B. the [with_lets] argument to [reflect] doesn't matter + here because [value' true (_ → _) ≡ value' false (_ → _)] *) + Definition reflect_ident_iota {t} (idc : ident t) : option (value t) + := Eval cbv [GallinaReify.Reify_as GallinaReify.reify GallinaReify.base.reify ident.smart_Literal] in + match idc in ident.ident t return option (value t) with + | ident.eager_nat_rect P + => Some + (fun (N_case : value base.type.unit -> _) (S_case : value base.type.nat -> value P -> _) (n : expr base.type.nat) (* type annotations present for nicer fixpoint refolding *) + => match invert_Literal n with + | Some n => nat_rect + (fun _ => UnderLets (expr P)) + (N_case (GallinaReify.Reify tt _)) + (fun n' rec + => rec <-- rec; + S_case (GallinaReify.Reify n' _) rec) + n + | None => reflect (with_lets:=false) (expr.Ident (@ident.nat_rect P)) N_case S_case n + end) + | ident.eager_nat_rect_arrow P Q + => Some + (fun (N_case : value P -> _) (S_case : value base.type.nat -> (value P -> _) -> _ -> _) (n : expr base.type.nat) (v : expr P) (* type annotations present for nicer fixpoint refolding *) + => match invert_Literal n with + | Some n => nat_rect + (fun _ => expr P -> UnderLets (expr Q)) + N_case + (fun n' rec v' + => S_case (GallinaReify.Reify n' _) rec v') + n + v + | None => reflect (with_lets:=false) (expr.Ident (@ident.nat_rect_arrow P Q)) N_case S_case n v + end) + | ident.eager_list_rect A P + => Some + (fun (N_case : value base.type.unit -> _) (C_case : value A -> _ -> value P -> _) (ls : expr (base.type.list A)) (* type annotations present for nicer fixpoint refolding *) + => match reflect_list ls with + | Some ls => list_rect + (fun _ => UnderLets (expr P)) + (N_case (GallinaReify.Reify tt _)) + (fun x xs rec + => rec <-- rec; + C_case x (reify_list xs) rec) + ls + | None => reflect (with_lets:=false) (expr.Ident (@ident.list_rect A P)) N_case C_case ls + end) + | ident.eager_list_rect_arrow A P Q + => Some + (fun (N_case : value P -> _) (C_case : value A -> _ -> (value P -> _) -> value P -> _) (ls : expr (base.type.list A)) (v : value P) (* type annotations present for nicer fixpoint refolding *) + => match reflect_list ls with + | Some ls => list_rect + (fun _ => expr P -> UnderLets (expr Q)) + N_case + (fun x xs rec v + => C_case x (reify_list xs) rec v) + ls + v + | None => reflect (with_lets:=false) (expr.Ident (@ident.list_rect_arrow A P Q)) N_case C_case ls v + end) + | ident.eager_List_nth_default A + => Some + (fun default (ls : expr (base.type.list A)) (n : expr base.type.nat) + => match reflect_list ls, invert_Literal n with + | Some ls, Some n => UnderLets.Base (nth_default default ls n) + | _, _ => reflect (with_lets:=false) (expr.Ident (@ident.List_nth_default A)) default ls n + end) + | ident.Literal _ _ + | ident.Nat_succ + | ident.Nat_pred + | ident.Nat_max + | ident.Nat_mul + | ident.Nat_add + | ident.Nat_sub + | ident.Nat_eqb + | ident.nil _ + | ident.cons _ + | ident.pair _ _ + | ident.fst _ _ + | ident.snd _ _ + | ident.prod_rect _ _ _ + | ident.bool_rect _ + | ident.nat_rect _ + | ident.nat_rect_arrow _ _ + | ident.list_rect _ _ + | ident.list_rect_arrow _ _ _ + | ident.list_case _ _ + | ident.List_length _ + | ident.List_seq + | ident.List_firstn _ + | ident.List_skipn _ + | ident.List_repeat _ + | ident.List_combine _ _ + | ident.List_map _ _ + | ident.List_app _ + | ident.List_rev _ + | ident.List_flat_map _ _ + | ident.List_partition _ + | ident.List_fold_right _ _ + | ident.List_update_nth _ + | ident.List_nth_default _ + | ident.Z_add + | ident.Z_mul + | ident.Z_pow + | ident.Z_sub + | ident.Z_opp + | ident.Z_div + | ident.Z_modulo + | ident.Z_log2 + | ident.Z_log2_up + | ident.Z_eqb + | ident.Z_leb + | ident.Z_ltb + | ident.Z_geb + | ident.Z_gtb + | ident.Z_of_nat + | ident.Z_to_nat + | ident.Z_shiftr + | ident.Z_shiftl + | ident.Z_land + | ident.Z_lor + | ident.Z_min + | ident.Z_max + | ident.Z_bneg + | ident.Z_lnot_modulo + | ident.Z_mul_split + | ident.Z_add_get_carry + | ident.Z_add_with_carry + | ident.Z_add_with_get_carry + | ident.Z_sub_get_borrow + | ident.Z_sub_with_get_borrow + | ident.Z_zselect + | ident.Z_add_modulo + | ident.Z_rshi + | ident.Z_cc_m + | ident.Z_cast _ + | ident.Z_cast2 _ + | ident.option_Some _ + | ident.option_None _ + | ident.option_rect _ _ + | ident.Build_zrange + | ident.zrange_rect _ + | ident.fancy_add _ _ + | ident.fancy_addc _ _ + | ident.fancy_sub _ _ + | ident.fancy_subb _ _ + | ident.fancy_mulll _ + | ident.fancy_mullh _ + | ident.fancy_mulhl _ + | ident.fancy_mulhh _ + | ident.fancy_rshi _ _ + | ident.fancy_selc + | ident.fancy_selm _ + | ident.fancy_sell + | ident.fancy_addm + => None + end%expr%under_lets. + Section with_rewrite_head. Context (rewrite_head : forall t (idc : ident t), value_with_lets t). @@ -1335,7 +1501,8 @@ Module Compilers. (pident_arg_types : forall t, pident t -> list Type) (pident_type_of_list_arg_types_beq : forall t idc, type_of_list (pident_arg_types t idc) -> type_of_list (pident_arg_types t idc) -> bool) (pident_of_typed_ident : forall t, ident t -> pident (pattern.type.relax t)) - (pident_arg_types_of_typed_ident : forall t (idc : ident t), type_of_list (pident_arg_types _ (pident_of_typed_ident t idc))). + (pident_arg_types_of_typed_ident : forall t (idc : ident t), type_of_list (pident_arg_types _ (pident_of_typed_ident t idc))) + (reflect_ident_iota : forall t (idc : ident t), option (@value base.type ident var t)). Local Notation type := (type.type base.type). Local Notation expr := (@expr.expr base.type ident var). @@ -1344,7 +1511,7 @@ Module Compilers. Local Notation value := (@Compile.value base.type ident var). Local Notation value_with_lets := (@Compile.value_with_lets base.type ident var). Local Notation UnderLets := (UnderLets.UnderLets base.type ident var). - Local Notation reify_expr_beta := (@reify_expr_beta ident var). + Local Notation reify_expr_beta_iota := (@reify_expr_beta_iota ident var reflect_ident_iota). Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types). Local Notation with_unif_rewrite_ruleTP_gen' := (@with_unif_rewrite_ruleTP_gen' ident var pident pident_arg_types value). Local Notation lam_unification_resultT' := (@lam_unification_resultT' pident pident_arg_types). @@ -1373,10 +1540,10 @@ Module Compilers. Definition expr_value_to_rewrite_rule_replacement (should_do_again : bool) {t} (e : @expr.expr base.type ident value t) : UnderLets (expr_maybe_do_again should_do_again t) - := (e <-- UnderLets.flat_map (@reify_expr_beta) (fun t v => reflect (expr.Var v)) (UnderLets.of_expr e); + := (e <-- UnderLets.flat_map (@reify_expr_beta_iota) (fun t v => reflect (expr.Var v)) (UnderLets.of_expr e); if should_do_again return UnderLets (expr_maybe_do_again should_do_again t) then UnderLets.Base e - else reify_expr_beta e)%under_lets. + 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 @@ -1440,7 +1607,7 @@ Module Compilers. 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 reflect_expr_beta*) 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'] + := 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 partial_lam_unif_rewrite_ruleTP_gen_unfolded should_do_again {t} p @@ -1746,13 +1913,13 @@ Module Compilers. term. - 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 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 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 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 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 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) 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 @@ -1788,7 +1955,7 @@ Module Compilers. let rB := expr.reify_in_context base.type ident ltac:(base.reify) reify_ident var_pos B value_ctx tt 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] in res) 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 let res := (eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in let res := change_pattern_base_subst_default_relax res in let p := (eval cbv [projT1] in (fun invalid => projT1 (res invalid))) in @@ -1810,8 +1977,8 @@ Module Compilers. let res := replace_type_try_transport res in exact res) end) in - let res := (eval cbv [UnderLets.map UnderLets.flat_map reify_expr_beta reflect_expr_beta reify_to_UnderLets] in res) in - let res := (eval cbn [reify reflect UnderLets.of_expr UnderLets.to_expr UnderLets.splice value' Base_value] in res) in + let res := (eval cbv [UnderLets.map UnderLets.flat_map reify_expr_beta_iota reflect_expr_beta_iota reify_to_UnderLets] in res) in + let res := (eval cbn [reify reflect UnderLets.of_expr UnderLets.to_expr UnderLets.splice value' Base_value invert_Literal ident.invert_Literal splice_under_lets_with_value] in res) in let res := strip_invalid_or_fail res in (* cbv here not strictly needed *) let res := (eval cbv [partial_lam_unif_rewrite_ruleTP_gen_unfolded] in @@ -1830,25 +1997,25 @@ Module Compilers. 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 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 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 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 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 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 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 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 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 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 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 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 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 lazymatch lems with | (?b, ?lem) :: ?lems => let rlem := reify' b lem in @@ -1856,15 +2023,16 @@ Module Compilers. constr:(rlem :: rlems) | nil => constr:(@nil (@rewrite_ruleT ident var pident pident_arg_types)) | _ - => let lems := (eval cbv beta iota delta [List.map] in - (List.map (fun p : Prop => (false, p)) lems)) in + => let List_map := (eval cbv delta [List.map] in (@List.map)) in + let lems := (eval cbv beta iota in + (List_map _ _ (fun p : Prop => (false, p)) lems)) in 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 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 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 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 lems in exact res)). End Reify. @@ -2139,7 +2307,7 @@ Module Compilers. 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) var 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 @@ -2267,97 +2435,146 @@ Module Compilers. Local Notation do_again P := (true, P) (only parsing). Local Notation cstZ := (ident.cast ident.cast_outside_of_range). Local Notation cstZZ := (ident.cast2 ident.cast_outside_of_range). + (* N.B. [ident.eagerly] does not play well with [do_again] *) Definition nbe_rewrite_rules : rewrite_rulesT := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in myapp Make.interp_rewrite_rules (myflatten - [ - (reify - [(forall A B x y, @fst A B (x, y) = x) - ; (forall A B x y, @snd A B (x, y) = y) - ; (forall P t f, @ident.Thunked.bool_rect P t f true = t tt) - ; (forall P t f, @ident.Thunked.bool_rect P t f false = f tt) - ; (forall A B C f x y, @prod_rect A B (fun _ => C) f (x, y) = f x y) - ]) - ; [make_rewrite (#(@pattern.ident.List_repeat '1) @ ?? @ #?ℕ) (fun _ x n => reify_list (repeat x n)) - ; make_rewriteol (??{list '1} ++ ??{list '1}) (fun _ xs ys => rlist_rect ys (fun x _ xs_ys => x :: xs_ys) xs) - ; make_rewriteol - (#(@pattern.ident.List_firstn '1) @ #?ℕ @ ??) - (fun _ n xs => xs <- reflect_list xs; reify_list (List.firstn n xs)) - ; make_rewriteol - (#(@pattern.ident.List_skipn '1) @ #?ℕ @ ??) - (fun _ n xs => xs <- reflect_list xs; reify_list (List.skipn n xs)) - ; make_rewriteol - (#(@pattern.ident.List_rev '1) @ ??) - (fun _ xs => xs <- reflect_list xs; reify_list (List.rev xs)) - ; make_rewriteol_step - (#(@pattern.ident.List_flat_map '1 '2) @ ?? @ ??) - (fun _ _ f xs - => rlist_rect - [] - (fun x _ flat_map_tl => fx <-- f x; ($fx ++ flat_map_tl)) - xs) - ; make_rewriteol_step - (#(@pattern.ident.List_partition '1) @ ?? @ ??) - (fun _ f xs - => rlist_rect - ([], []) - (fun x tl partition_tl - => fx <-- f x; - (#ident.prod_rect - @ (λ g d, #ident.bool_rect - @ (λ _, ($x :: $g, $d)) - @ (λ _, ($g, $x :: $d)) - @ $fx) - @ partition_tl)) - xs) - ; make_rewriteol - (#(@pattern.ident.List_fold_right '1 '2) @ ?? @ ?? @ ??) - (fun _ _ f init xs => rlist_rect init (fun x _ y => f x y) xs) - ; make_rewriteol - (#(@pattern.ident.list_rect '1 '2) @ ?? @ ?? @ ??) - (fun _ _ Pnil Pcons xs - => rlist_rect (Pnil ##tt) (fun x' xs' rec => Pcons x' (reify_list xs') rec) xs) ] - - ; (reify - [(forall A P N C, @ident.Thunked.list_case A P N C nil = N tt) - ; (forall A P N C x xs, @ident.Thunked.list_case A P N C (x :: xs) = C x xs) - ]) - ; [ - make_rewriteol - (#(@pattern.ident.List_map '1 '2) @ ?? @ ??) - (fun _ _ f xs => rlist_rect [] (fun x _ fxs => fx <-- f x; fx :: fxs) xs) - ; make_rewriteo - (#(@pattern.ident.List_nth_default '1) @ ?? @ ?? @ #?ℕ) - (fun _ default ls n => ls <- reflect_list ls; nth_default default ls n) - ; make_rewritel - (#(@pattern.ident.nat_rect '1) @ ?? @ ?? @ #?ℕ) - (fun _ O_case S_case n - => nat_rect _ (O_case ##tt) (fun n' rec => rec <-- rec; S_case ##n' rec) n) - ; make_rewritel - (#(@pattern.ident.nat_rect_arrow '1 '2) @ ?? @ ?? @ #?ℕ @ ??) - (fun _ _ O_case S_case n v - => nat_rect _ O_case (fun n' rec v => S_case ##n' rec v) n v) - ; make_rewriteo - (#(@pattern.ident.List_length '1) @ ??) - (fun _ xs => xs <- reflect_list xs; ##(List.length xs)) - ; make_rewriteo - (#(@pattern.ident.List_combine '1 '2) @ ?? @ ??) - (fun _ _ xs ys - => xs <- reflect_list xs; - ys <- reflect_list ys; - reify_list (List.map (fun '((x, y)%core) => (x, y)) (List.combine xs ys))) - ; make_rewriteol - (#(@pattern.ident.List_update_nth '1) @ #?ℕ @ ?? @ ??) - (fun _ n f ls - => ls <---- reflect_list ls; - retv <--- (update_nth - n - (fun x => x <-- x; f x) - (List.map UnderLets.Base ls)); - reify_list retv) - ] ]). + [reify + [(forall A B x y, @fst A B (x, y) = x) + ; (forall A B x y, @snd A B (x, y) = y) + ; (forall P t f, @ident.Thunked.bool_rect P t f true = t tt) + ; (forall P t f, @ident.Thunked.bool_rect P t f false = f tt) + ; (forall A B C f x y, @prod_rect A B (fun _ => C) f (x, y) = f x y) + + ; (forall A x n, + @List.repeat A x ('n) + = ident.eagerly (@nat_rect) _ nil (fun k repeat_k => x :: repeat_k) ('n)) + ; (forall A xs ys, + xs ++ ys + = ident.eagerly (@list_rect) A _ ys (fun x xs app_xs_ys => x :: app_xs_ys) xs) + ; (forall A B f a ls, + @fold_right A B f a ls + = (ident.eagerly (@list_rect) _ _) + a + (fun x xs fold_right_xs => f x fold_right_xs) + ls) + ; (forall A P N C ls, + @ident.Thunked.list_rect A P N C ls + = ident.eagerly (@ident.Thunked.list_rect) A P N C ls) + ; (forall A P Q N C ls v, + @list_rect A (fun _ => P -> Q) N C ls v + = ident.eagerly (@list_rect) A (fun _ => P -> Q) N C ls v) + ; (forall A P N C, @ident.Thunked.list_case A P N C nil = N tt) + ; (forall A P N C x xs, @ident.Thunked.list_case A P N C (x :: xs) = C x xs) + ; (forall A B f ls, + @List.map A B f ls + = (ident.eagerly (@list_rect) _ _) + nil + (fun x xs map_f_xs => f x :: map_f_xs) + ls) + ; (forall P O_case S_case n, + @ident.Thunked.nat_rect P O_case S_case ('n) + = (ident.eagerly (@ident.Thunked.nat_rect) _) + O_case + S_case + ('n)) + ; (forall P Q O_case S_case n v, + @nat_rect (fun _ => P -> Q) O_case S_case ('n) v + = (ident.eagerly (@nat_rect) _) + O_case + S_case + ('n) + v) + ; (forall A default ls n, + @List.nth_default A default ls ('n) + = ident.eagerly (@List.nth_default) _ default ls ('n)) + ] + ; reify + [do_again + (forall A B xs ys, + @List.combine A B xs ys + = (list_rect _) + (fun _ => nil) + (fun x xs combine_xs ys + => match ys with + | nil => nil + | y :: ys => (x, y) :: combine_xs ys + end) + xs + ys) + ; do_again + (forall A n ls, + @List.firstn A ('n) ls + = (nat_rect _) + (fun _ => nil) + (fun n' firstn_n' ls + => match ls with + | nil => nil + | cons x xs => x :: firstn_n' xs + end) + ('n) + ls) + ; do_again + (forall A n ls, + @List.skipn A ('n) ls + = (nat_rect _) + (fun ls => ls) + (fun n' skipn_n' ls + => match ls with + | nil => nil + | cons x xs => skipn_n' xs + end) + ('n) + ls) + ; do_again + (forall A xs, + @List.length A xs + = (list_rect _) + 0%nat + (fun _ xs length_xs => S length_xs) + xs) + ; do_again + (forall A xs, + @List.rev A xs + = (list_rect _) + nil + (fun x xs rev_xs => rev_xs ++ [x]) + xs) + ; do_again + (forall A B f xs, + @List.flat_map A B f xs + = (list_rect _) + nil + (fun x _ flat_map_tl => f x ++ flat_map_tl) + xs) + ; do_again + (forall A f xs, + @List.partition A f xs + = (list_rect _) + ([], []) + (fun x tl partition_tl + => let '(g, d) := partition_tl in + if f x then (x :: g, d) else (g, x :: d)) + xs) + ; do_again + (forall A n f xs, + @update_nth A ('n) f xs + = (nat_rect _) + (fun xs => match xs with + | nil => nil + | x' :: xs' => f x' :: xs' + end) + (fun n' update_nth_n' xs + => match xs with + | nil => nil + | x' :: xs' => x' :: update_nth_n' xs' + end) + ('n) + xs) + ] + ]). Definition arith_rewrite_rules (max_const_val : Z) : rewrite_rulesT := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index c9c41a392..935a32474 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -189,28 +189,38 @@ Module Compilers. (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2). Proof using Type. apply wf_rlist_rect_gen; assumption. Qed. - Lemma wf_nat_rect {A} - G O1 O2 S1 S2 n - (HO : UnderLets.wf (fun G' => expr.wf G') G O1 O2) - (HS : forall n rec1 rec2, - UnderLets.wf (fun G' => expr.wf G') G rec1 rec2 - -> UnderLets.wf (fun G' => expr.wf G') G (S1 n rec1) (S2 n rec2)) - : UnderLets.wf (fun G' => expr.wf G') G - (nat_rect (fun _ => UnderLets.UnderLets base.type ident var1 (expr (type.base A))) O1 S1 n) - (nat_rect (fun _ => UnderLets.UnderLets base.type ident var2 (expr (type.base A))) O2 S2 n). - Proof. induction n; cbn [nat_rect]; auto. Qed. + Lemma wf_list_rect {T A} + G N1 N2 C1 C2 ls1 ls2 + (HN : Compile.wf_value G N1 N2) + (HC : forall G' x1 x2 xs1 xs2 rec1 rec2, + (exists seg, G' = (seg ++ G)%list) + -> Compile.wf_value G x1 x2 + -> List.Forall2 (Compile.wf_value G) xs1 xs2 + -> Compile.wf_value G' rec1 rec2 + -> Compile.wf_value G' (C1 x1 xs1 rec1) (C2 x2 xs2 rec2)) + (Hls : List.Forall2 (Compile.wf_value G) ls1 ls2) + : Compile.wf_value + G + (list_rect (fun _ : list (@Compile.value base.type ident var1 (type.base T)) + => @Compile.value base.type ident var1 A) + N1 C1 ls1) + (list_rect (fun _ : list (@Compile.value base.type ident var2 (type.base T)) + => @Compile.value base.type ident var2 A) + N2 C2 ls2). + Proof. induction Hls; cbn [list_rect]; try eapply HC; eauto using (ex_intro _ nil). Qed. - Lemma wf_nat_rect_arrow {A B} + Lemma wf_nat_rect {A} G O1 O2 S1 S2 n - (HO : Compile.wf_value G O1 O2) - (HS : forall n rec1 rec2, - Compile.wf_value G rec1 rec2 - -> Compile.wf_value G (S1 n rec1) (S2 n rec2)) - : Compile.wf_value + (HO : Compile.wf_value_with_lets G O1 O2) + (HS : forall G' n rec1 rec2, + (exists seg, G' = (seg ++ G)%list) + -> Compile.wf_value_with_lets G' rec1 rec2 + -> Compile.wf_value_with_lets G' (S1 n rec1) (S2 n rec2)) + : Compile.wf_value_with_lets G - (nat_rect (fun _ => @Compile.value base.type ident var1 (type.base A -> type.base B)) O1 S1 n) - (nat_rect (fun _ => @Compile.value base.type ident var2 (type.base A -> type.base B)) O2 S2 n). - Proof. induction n; cbn [nat_rect]; auto. Qed. + (nat_rect (fun _ => @Compile.value_with_lets base.type ident var1 A) O1 S1 n) + (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. Local Ltac start_good := apply Compile.rewrite_rules_goodT_by_curried; @@ -229,170 +239,88 @@ Module Compilers. end | progress cbn [eq_rect] in * ]. - Local Ltac good_t_step := - first [ progress subst - | progress cbn [eq_rect Compile.value' option_eq projT1 projT2 fst snd base.interp In combine Option.bind Option.sequence Option.sequence_return UnderLets.splice] in * - | progress destruct_head'_unit - | progress destruct_head'_sigT - | progress destruct_head'_prod - | progress eliminate_hprop_eq - | progress destruct_head'_and - | progress destruct_head'_sig - | progress inversion_option - | progress destruct_head'_ex - | progress cbn [pattern.ident.arg_types] in * - | progress cbn [fst snd projT1 projT2] in * - | progress intros - | progress cbv [id pattern.ident.arg_types Compile.value cpsbind cpscall cpsreturn cps_option_bind type_base ident.smart_Literal rwhen rwhenl nth_default SubstVarLike.is_var_fst_snd_pair_opp_cast] in * - | progress cbv [Compile.option_bind'] in * - | progress type_beq_to_eq - | progress type.inversion_type - | progress rewrite_type_transport_correct - | progress specialize_by exact eq_refl - | match goal with - | [ |- context[invert_expr.reflect_list ?v] ] => destruct (invert_expr.reflect_list v) eqn:? - end - | break_innermost_match_step - | wf_safe_t_step - | rewrite !expr.reflect_list_cps_id - | congruence - | match goal with - | [ H : nth_error ?l1 ?n = Some _, H' : nth_error ?l2 ?n = None |- _ ] - => let H0 := fresh in - assert (H0 : length l1 = length l2) by congruence; - apply nth_error_error_length in H'; - apply nth_error_value_length in H; - exfalso; clear -H0 H H'; lia - | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list - | [ |- option_eq _ (rlist_rect _ _ _) (rlist_rect _ _ _) ] - => first [ apply wf_rlist_rect | apply wf_rlist_rectv ] - | [ |- context[length ?ls] ] => tryif is_var ls then fail else (progress autorewrite with distr_length) - | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H) - | [ |- @ex (_ = _) _ ] => (exists eq_refl) - | [ |- ex _ ] => eexists - | [ |- UnderLets.wf _ _ _ _ ] => constructor - | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] - => eapply UnderLets.wf_splice; [ eapply UnderLets.wf_Proper_list; [ | | solve [ repeat good_t_step ] ] | ] - | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice - | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ] - => apply @UnderLets.wf_splice_list_no_order with (P:=fun G' => expr.wf G') - | [ |- ?x = ?x /\ _ ] => split; [ reflexivity | ] - | [ 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 - | [ H : Compile.wf_value _ (reify_list _) (reify_list _) |- _ ] - => hnf in H; rewrite expr.wf_reify_list in H - | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] - | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff - | [ |- List.Forall2 _ (List.repeat _ _) (List.repeat _ _) ] - => rewrite Forall2_repeat_iff - | [ |- List.Forall2 _ (List.rev _) (List.rev _) ] - => rewrite Forall2_rev_iff - | [ |- List.Forall _ (seq _ _) ] => rewrite Forall_seq - | [ |- List.Forall2 _ (firstn _ _) (firstn _ _) ] - => now apply Forall2_firstn - | [ |- List.Forall2 _ (skipn _ _) (skipn _ _) ] - => now apply Forall2_skipn - | [ |- List.Forall2 _ (List.combine _ _) (List.combine _ _) ] - => eapply Forall2_combine; [ intros | eassumption | eassumption ] - | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] - => apply Forall2_update_nth; intros - | [ H : List.Forall2 _ ?x ?y |- context[@List.length ?T ?y] ] - => rewrite <- (@eq_length_Forall2 _ T _ x y H) - | [ H : Forall2 (expr.wf ?G) ?xs ?ys |- Forall2 (fun a b => UnderLets.wf (fun G' => expr.wf G') ?G _ _) ?xs ?ys ] - => eapply Forall2_Proper_impl; [ .. | exact H ]; try reflexivity; repeat intro - | [ H : Forall2 ?P ?xs ?ys, Hx : nth_error ?xs ?n = _, Hy : nth_error ?ys ?n = _ |- _ ] - => let H' := fresh in - pose proof H as H'; - rewrite Forall2_forall_iff_nth_error in H'; specialize (H' n); rewrite Hx, Hy in H'; clear n Hx Hy - | [ H : length ?l = length ?l' |- context[length ?l] ] => rewrite H - | [ H : context[combine (firstn ?n _) (firstn ?n _)] |- _ ] => rewrite <- firstn_combine in H - | [ H : context[combine (skipn ?n _) (skipn ?n _)] |- _ ] => rewrite <- skipn_combine in H - | [ H : context[In _ (firstn _ _)] |- _ ] => solve [ eauto using In_firstn ] - | [ H : context[In _ (skipn _ _)] |- _ ] => solve [ eauto using In_skipn ] - | [ H : context[combine (repeat _ _) (repeat _ _)] |- _ ] => rewrite combine_repeat in H - | [ H : context[combine (Lists.List.repeat _ _) (Lists.List.repeat _ _)] |- _ ] => rewrite combine_repeat in H - | [ H : In _ (repeat _ _) |- _ ] => apply repeat_spec in H - | [ H : In _ (Lists.List.repeat _ _) |- _ ] => apply repeat_spec in H - | [ H : context[combine (rev ?l1) (rev ?l2)] |- _ ] => rewrite (@combine_rev_rev_samelength _ _ l1 l2) in H by congruence - | [ H : In _ (rev _) |- _ ] => rewrite <- in_rev in H - | [ H : forall e1' e2', In (e1', e2') (combine ?l1 ?l2) -> _, H1 : nth_error ?l1 ?n = Some ?e1, H2 : nth_error ?l2 ?n = Some ?e2 |- _ ] - => specialize (fun pf => H e1 e2 (@nth_error_In _ _ n _ pf)) - | [ H : context[nth_error (combine _ _) _] |- _ ] => rewrite nth_error_combine in H - | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : context[combine (map _ _) (map _ _)] |- _ ] => rewrite combine_map_map in H - | [ H : context[nth_error (update_nth _ _ _) _] |- _ ] => rewrite nth_update_nth in H - | [ H : nth_error (map _ _) _ = Some _ |- _ ] => apply nth_error_map in H - | [ H : In _ (map _ _) |- _ ] => rewrite in_map_iff in H - | [ H : In _ (combine _ _) |- _ ] => apply In_nth_error_value in H - | [ |- expr.wf ?G (fold_right _ _ (map _ (seq ?a ?b))) (fold_right _ _ (map _ (seq ?a ?b))) ] - => induction (seq a b); cbn [fold_right map] - | [ 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 - | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] => apply wf_nat_rect - | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply wf_nat_rect_arrow; [ | | reflexivity | ]; cycle 1 ]; revgoals; hnf - | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _) (?e2 _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | ] ]; revgoals - | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _ _) (?e2 _ _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals - | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _ _ _) (?e2 _ _ _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | | reflexivity | ]; cycle 1 ]; revgoals - | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _) (?e2 _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | ] ]; revgoals - | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _ _) (?e2 _ _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals - | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _ _ _) (?e2 _ _ _) ] - => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | | reflexivity | ]; cycle 1 ]; revgoals - | [ |- Compile.wf_value _ (fun _ => _) (fun _ => _) ] => hnf - | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _) (?g _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ] - | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _ _) (?g _ _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ] - | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _ _ _) (?g _ _ _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ] - | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _) (?e2 _) ] => eapply (H nil) - | [ H : ?R ?G ?a ?b |- expr.wf ?G ?a ?b ] - => is_evar R; revert H; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] - | [ H : expr.wf ?G ?a ?b |- ?R ?G ?a ?b ] - => is_evar R; instantiate (1:=fun G' => expr.wf G'); solve [ auto ] - | [ |- (forall t v1 v2, In _ _ -> _) /\ expr.wf _ _ _ ] => apply conj; revgoals - | [ H : expr.wf _ ?x ?y |- Compile.wf_value _ ?x ?y ] => hnf - | [ |- Compile.wf_value _ ?x ?y ] => eapply Compile.wf_value'_Proper_list; [ | solve [ cbv [Compile.wf_value] in *; eauto ] ]; solve [ wf_t ] - | [ |- In ?x ?ls ] => is_evar ls; refine (or_introl eq_refl : In x (x :: _)); shelve - | [ |- or (_ = _) ?G ] => first [ left; reflexivity | has_evar G; right ] - | [ H : @In ?A _ ?ls |- _ ] => is_evar ls; unify ls (@nil A); cbn [In] in H - end - | progress expr.invert_subst - | solve [ wf_t ] - | break_match_hyps_step ltac:(fun v => let h := head v in constr_eq h (@nth_error)) - | break_match_hyps_step ltac:(fun v => match v with Nat.eq_dec _ _ => idtac end) - | progress cbv [option_map] in * ]. + Local Ltac fin_wf := + repeat first [ progress intros + | match goal with + | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor + | [ |- expr.wf _ (#_) (#_) ] => constructor + | [ |- expr.wf _ ($_) ($_) ] => constructor + | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros + | [ H : @List.In ?T _ ?ls |- _ ] => is_evar ls; unify ls (@nil T); cbn [List.In] in H + | [ |- List.In ?v ?ls ] => is_evar ls; instantiate (1:=cons v _) + end + | progress subst + | progress destruct_head'_or + | progress destruct_head'_False + | progress inversion_sigma + | progress inversion_prod + | assumption + | esplit; revgoals; solve [ fin_wf ] + | econstructor; solve [ fin_wf ] + | progress cbn [List.In fst snd eq_rect] in * ]. + + Local Ltac handle_reified_rewrite_rules := + repeat + first [ match goal with + | [ |- option_eq _ ?x ?y ] + => lazymatch x with Some _ => idtac | None => idtac end; + lazymatch y with Some _ => idtac | None => idtac end; + progress cbn [option_eq] + | [ |- UnderLets.wf _ _ (Reify.expr_value_to_rewrite_rule_replacement ?rii1 ?sda _) (Reify.expr_value_to_rewrite_rule_replacement ?rii2 ?sda _) ] + => apply (fun H => @Reify.wf_expr_value_to_rewrite_rule_replacement _ _ _ rii1 rii2 H sda); intros + | [ |- option_eq _ (Compile.reflect_ident_iota _) (Compile.reflect_ident_iota _) ] + => apply Reify.wf_reflect_ident_iota + | [ |- ?x = ?x ] => reflexivity + end + | break_innermost_match_step + | progress cbv [Compile.wf_maybe_do_again_expr] in * + | progress fin_wf ]. + + Local Ltac handle_extra_nbe := + repeat first [ match goal with + | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list + | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper] + | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff + | [ |- List.Forall _ (seq _ _) ] => rewrite Forall_seq + end + | progress intros + | progress fin_wf ]. Lemma nbe_rewrite_rules_good : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules. Proof using Type. Time start_good. - Time all: repeat repeat good_t_step. + Time all: 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] + | 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 + end + | congruence + | progress fin_wf ]. + 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: repeat good_t_step. + Time all: handle_reified_rewrite_rules; handle_extra_arith_rules. Qed. Lemma arith_with_casts_rewrite_rules_good : rewrite_rules_goodT arith_with_casts_rewrite_rules arith_with_casts_rewrite_rules. Proof using Type. Time start_good. - Time all: repeat good_t_step. + Time all: handle_reified_rewrite_rules. Qed. 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: repeat good_t_step. + Time all: handle_reified_rewrite_rules. Qed. Lemma fancy_rewrite_rules_good @@ -402,9 +330,7 @@ Module Compilers. : rewrite_rules_goodT fancy_rewrite_rules fancy_rewrite_rules. Proof using Type. Time start_good. - Time all: repeat good_t_step. - all: cbv [Option.bind]. - Time all: repeat good_t_step. + Time all: handle_reified_rewrite_rules. Qed. Lemma fancy_with_casts_rewrite_rules_good @@ -415,9 +341,7 @@ Module Compilers. : rewrite_rules_goodT (fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range) (fancy_with_casts_rewrite_rules invert_low invert_high value_range flag_range). Proof using Type. Time start_good. - Time all: repeat good_t_step. - all: cbv [Option.bind]. - Time all: repeat good_t_step. + Time all: handle_reified_rewrite_rules. Qed. End good. End RewriteRules. diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 954340fa4..d30366220 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -119,7 +119,9 @@ Module Compilers. 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]. + 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]. @@ -183,11 +185,48 @@ Module Compilers. end; progress cbn [ident_interp fst snd] | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else (progress subst) + | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else reflexivity | [ |- ?x = ?x ] => tryif has_evar x then fail else reflexivity | [ |- ?ev = _ ] => is_evar ev; reflexivity | [ |- _ = ?ev ] => is_evar ev; reflexivity end. + (* TODO: MOVE ME? *) + Local Ltac recursive_match_to_list_case term := + 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 + end. + Local Ltac recursive_match_to_list_case_in_goal := + let G := match goal with |- ?G => G end in + let G := recursive_match_to_list_case G in + change G. + Local Ltac interp_good_t_step_related := first [ lazymatch goal with | [ |- ?x = ?x ] => reflexivity @@ -199,10 +238,123 @@ Module Compilers. (*| [ |- 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 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 @@ -220,20 +372,13 @@ Module Compilers. | [ |- 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 - | [ |- 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 _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] - => rewrite (@eq_fold_right_list_rect A B f v ls) | [ |- 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 @@ -266,6 +411,21 @@ Module Compilers. ?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 _ _ _ _ _) ] @@ -338,6 +498,7 @@ Module Compilers. | 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 @@ -464,6 +625,8 @@ Module Compilers. => 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 diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 49af85a60..411287bcc 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -27,6 +27,7 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Sigma.Related. Require Import Crypto.Util.ListUtil.SetoidList. +Require Import Crypto.Util.ListUtil.Forall. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Option. Require Import Crypto.Util.Logic.ExistsEqAnd. @@ -2569,5 +2570,304 @@ Module Compilers. End with_interp. End with_var. End Compile. + + Module Reify. + Import Compile. + Import Rewriter.Compilers.RewriteRules.Compile. + Import Rewriter.Compilers.RewriteRules.Reify. + + Local Notation type := (type.type base.type). + Local Notation expr := (@expr.expr base.type ident). + Local Notation value := (@value base.type ident). + Local Notation UnderLets := (@UnderLets.UnderLets base.type ident). + + Ltac wf_ctors := + repeat first [ match goal with + | [ |- UnderLets.wf _ _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor + | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor + | [ |- expr.wf ?seg (#_) (#_) ] + => (tryif is_evar seg then instantiate (1:=nil) else idtac); + constructor + | [ |- expr.wf _ ($_) ($_) ] => constructor + | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros + | [ |- expr.wf _ (UnderLets.to_expr _) (UnderLets.to_expr _) ] => apply UnderLets.wf_to_expr + | [ H : expr.wf ?G ?x ?y |- expr.wf ?seg ?x ?y ] => first [ is_evar seg | constr_eq G seg ]; exact H + | [ H : List.Forall2 (expr.wf _) ?x ?y |- List.Forall2 (expr.wf _) ?x ?y ] + => eapply Forall2_Proper_impl; [ | reflexivity | reflexivity | exact H ]; repeat intro + | [ H : List.Forall2 (expr.wf ?G) ?x ?y |- List.Forall2 (expr.wf ?seg) ?x ?y ] + => first [ is_evar seg | constr_eq seg G ]; exact H + | [ H : List.Forall2 ?P ?x ?y |- List.Forall2 ?Pe ?x ?y ] + => first [ is_evar Pe | constr_eq Pe P ]; exact H + | [ H : forall x y, List.In (x, y) ?G -> expr.wf ?G' x y, H' : List.In (?v1, ?v2) ?G |- expr.wf ?seg ?v1 ?v2 ] + => first [ is_evar seg | constr_eq seg G' ]; exact (H _ _ H') + | [ |- expr.wf _ (reify_list _) (reify_list _) ] + => rewrite expr.wf_reify_list + | [ H : expr.wf _ (reify_list ?xs) (reify_list ?ys) |- List.Forall2 _ ?xs ?xy ] + => rewrite expr.wf_reify_list in H + | [ |- ?G ] => tryif has_evar G then fail else solve [ destruct_head'_ex; subst; wf_t ] + end ]. + Ltac handle_wf_rec do_try := + let tac _ + := solve + [ repeat + first + [ progress wf_ctors + | handle_wf_rec do_try + | match goal with + | [ |- List.In ?v ?seg ] => is_evar seg; unify seg (cons v nil) + | [ |- List.In ?v (?seg1 ++ ?seg2) ] + => rewrite in_app_iff; + first [ is_evar seg1; left + | is_evar seg2; right ] + (*| [ |- ?x ++ ?y = ?x ++ ?z ] => apply f_equal2*) + | [ |- ?x = ?y ] + => is_evar x; tryif has_evar y then fail else reflexivity + | [ |- forall t v1 v2, List.In (existT _ t (v1, v2)) (?x ++ ?G1) -> List.In (existT _ t (v1, v2)) (?x ++ ?G2) ] + => is_evar G2; + tryif first [ has_evar x | has_evar G1 ] then fail else (do 3 intro; exact id) + end ] ] in + match goal with + | [ H : expr.wf ?segv ?x1 ?x2 + |- UnderLets.wf _ ?Gv (nat_rect _ _ _ _ ?x1) (nat_rect _ _ _ _ ?x2) ] + => unshelve + (eapply UnderLets.wf_Proper_list; + [ | | eapply @UnderLets.wf_nat_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ]; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + | [ H : expr.wf ?segv ?x1 ?x2 + |- UnderLets.wf _ ?Gv (list_rect _ _ _ _ ?x1) (list_rect _ _ _ _ ?x2) ] + => unshelve + (eapply UnderLets.wf_Proper_list; + [ | | eapply @UnderLets.wf_list_rect_arrow with (R' := fun G' => expr.wf G') (seg:=segv) (G:=Gv); intros ]; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + | [ |- UnderLets.wf _ _ ?x ?y ] + => let f := head x in + let g := head y in + is_var f; is_var g; + unshelve + (lazymatch goal with + | [ H : context[UnderLets.wf _ _ (f _) (g _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _) (g _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _ _) (g _ _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + | [ H : context[UnderLets.wf _ _ (f _ _ _ _) (g _ _ _ _)] |- _ ] + => eapply UnderLets.wf_Proper_list; [ | | eapply H ] + end; + [ try (intros; subst; match goal with |- expr.wf _ _ _ => shelve end).. ]; + [ try (intros; subst; match goal with |- UnderLets.wf _ _ _ _ => shelve end).. ]; + [ try match goal with |- _ = _ => shelve end.. ]); + shelve_unifiable; + do_try tac + end. + + Ltac reify_wf_t_step := + first [ progress subst + | 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 + end + | progress inversion_option + | progress destruct_head'_False + | progress intros + | progress cbn [invert_expr.invert_Literal invert_expr.ident.invert_Literal value' type.interp base.interp base.base_interp] in * + | match goal with + | [ H : ident.Literal _ = ident.Literal _ |- _ ] + => pose proof (f_equal invert_expr.ident.invert_Literal H); clear H + end + | progress expr.inversion_wf_constr + | break_innermost_match_hyps_step + | progress expr.inversion_wf_one_constr + | progress expr.invert_subst + | progress expr.inversion_expr + | progress expr.invert_match + | progress wf_ctors + | match goal with + | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] + => apply UnderLets.wf_nat_rect; intros + | [ |- UnderLets.wf _ ?G (list_rect _ _ _ _) (list_rect _ _ _ _) ] + => apply @UnderLets.wf_list_rect with (RA := expr.wf G) + | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] + => apply @UnderLets.wf_splice with (P := fun G => expr.wf G); intros; subst + | [ H : expr.wf _ (reify_list ?l1) (reify_list ?l2) + |- expr.wf ?G (nth_default ?d1 ?l1 ?n) (nth_default ?d2 ?l2 ?n) ] + => cut (List.Forall2 (expr.wf G) l1 l2 /\ expr.wf G d1 d2); + [ rewrite Forall2_forall_iff''; + let H := fresh in intro H; apply H + | split ] + | [ |- ?x = ?x ] => reflexivity + end + | progress handle_wf_rec ltac:(fun tac => try tac (); tac ()) ]. + Ltac reify_wf_t := repeat reify_wf_t_step. + + Section with_var. + Context {var1 var2 : type -> Type}. + + Lemma wf_reflect_ident_iota G {t} (idc : ident t) + : option_eq + (wf_value G) + (@reflect_ident_iota var1 t idc) + (@reflect_ident_iota var2 t idc). + Proof using Type. + destruct idc; cbv [reflect_ident_iota option_eq]; try reflexivity. + all: cbv [wf_value wf_value']; intros; subst; break_innermost_match; cbn [reify reflect] in *; + lazymatch 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 + | _ => idtac + end; + expr.invert_subst; subst. + all: reify_wf_t. + Qed. + + Lemma wf_reflect_expr_beta_iota + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + G G' + (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2) + {t} e1 e2 + (Hwf : expr.wf G' e1 e2) + : UnderLets.wf + (fun G'' => wf_value G'') + G + (@reflect_expr_beta_iota ident var1 reflect_ident_iota1 t e1) + (@reflect_expr_beta_iota ident var2 reflect_ident_iota2 t e2). + Proof using Type. + revert G HG'; induction Hwf; cbn [reflect_expr_beta_iota]; intros. + all: repeat first [ match goal with + | [ |- UnderLets.wf _ _ _ _ ] => constructor + | [ |- expr.wf _ _ _ ] => constructor + | [ |- wf_value' _ (UnderLets.Base _) (UnderLets.Base _) ] => constructor + | [ Hwf_reflect_ident_iota : forall G t' idc', option_eq (wf_value G) (?reflect_ident_iota1 t' idc') (?reflect_ident_iota2 t' idc'), + H1 : ?reflect_ident_iota1 ?t ?idc = _, H2 : ?reflect_ident_iota2 ?t ?idc = _ |- _ ] + => let H' := fresh in + pose proof (fun G => Hwf_reflect_ident_iota G t idc) as H'; + rewrite H1, H2 in H'; clear H1 H2; cbv [option_eq] in H' + | [ H : list _ -> ?T |- _ ] => specialize (H nil) + | [ |- UnderLets.wf ?Pv ?Gv (UnderLets.splice _ _) (UnderLets.splice _ _) ] + => apply @UnderLets.wf_splice with (P:=fun G => wf_value G); intros; subst + | [ H : context[reflect_expr_beta_iota] |- UnderLets.wf _ _ (reflect_expr_beta_iota _ _) (reflect_expr_beta_iota _ _) ] + => apply H; intros + | [ |- wf_value _ (fun x => _) (fun y => _) ] => hnf; intros; subst + | [ |- wf_value' _ (splice_under_lets_with_value _ _) (splice_under_lets_with_value _ _) ] + => apply wf_splice_under_lets_with_value + | [ |- UnderLets.wf (fun G a1 a2 => wf_value_with_lets G (Base_value a1) (Base_value a2)) ?G' ?x ?y ] + => cut (UnderLets.wf (fun G => wf_value G) G' x y); + [ apply UnderLets.wf_Proper_list_impl; cbv [wf_value_with_lets Base_value] + | ] + end + | progress destruct_head'_False + | progress inversion_option + | solve [ auto ] + | break_innermost_match_step + | apply wf_reflect + | apply wf_reify + | progress intros + | progress cbn [List.In eq_rect fst snd] in * + | progress destruct_head'_or + | progress inversion_sigma + | progress subst + | progress inversion_prod + | cbn [wf_value wf_value'] in *; + handle_wf_rec ltac:(fun tac => try tac (); try eassumption; tac ()) + | eapply wf_value'_Proper_list; [ | match goal with H : _ |- _ => now eapply H end ]; solve [ destruct_head'_ex; subst; wf_t ] + | match goal with + | [ H : wf_value _ ?f ?g |- wf_value _ (?f _) (?g _) ] + => eapply wf_value'_Proper_list; revgoals; [ hnf in H; eapply H; revgoals | ]; try eassumption; try reflexivity; now destruct_head'_ex; subst; wf_t + end ]. + Qed. + + Lemma wf_reify_expr_beta_iota + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + G G' + (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> wf_value G v1 v2) + {t} e1 e2 + (Hwf : expr.wf G' e1 e2) + : UnderLets.wf + (fun G'' => expr.wf G'') + G + (@reify_expr_beta_iota ident var1 reflect_ident_iota1 t e1) + (@reify_expr_beta_iota ident var2 reflect_ident_iota2 t e2). + Proof using Type. + cbv [reify_expr_beta_iota reify_to_UnderLets]. + eapply @UnderLets.wf_splice with (P := fun G => wf_value G); + intros; destruct_head'_ex; subst. + all: repeat first [ break_innermost_match_step + | progress cbn [reflect reify] in * + | progress fold (@reflect ident var1) (@reflect ident var2) + | progress fold (@reify ident var1) (@reify ident var2) + | progress intros + | assumption + | apply wf_reify + | apply wf_reflect + | eapply wf_reflect_expr_beta_iota + | match goal with + | [ |- List.In ?x ?seg ] => is_evar seg; unify seg (cons x nil); left + end + | constructor + | match goal with H : _ |- _ => eapply H; revgoals; clear H end ]. + Qed. + + Lemma wf_expr_value_to_rewrite_rule_replacement + {ident} + {reflect_ident_iota1 reflect_ident_iota2} + (Hwf_reflect_ident_iota + : forall G {t} (idc : ident t), + option_eq + (@wf_value _ ident var1 var2 G _) + (@reflect_ident_iota1 t idc) + (@reflect_ident_iota2 t idc)) + (should_do_again : bool) + G {t} e1 e2 + (Hwf : @wf_maybe_do_again_expr ident var1 var2 t true true G e1 e2) + : UnderLets.wf + (fun G' => @wf_maybe_do_again_expr ident var1 var2 t should_do_again should_do_again G') + G + (@expr_value_to_rewrite_rule_replacement ident var1 reflect_ident_iota1 should_do_again t e1) + (@expr_value_to_rewrite_rule_replacement ident var2 reflect_ident_iota2 should_do_again t e2). + Proof using Type. + cbv [expr_value_to_rewrite_rule_replacement]. + eapply @UnderLets.wf_splice with (P := @wf_maybe_do_again_expr ident var1 var2 _ true true); intros; destruct_head'_ex; subst. + { destruct Hwf as [G' [HG' Hwf] ]. + eapply UnderLets.wf_flat_map; + cbv [wf_value] in *; + eauto using wf_value'_Proper_list, UnderLets.wf_of_expr, wf_reify_expr_beta_iota. + { intros; eapply wf_reflect; now repeat constructor. } } + { repeat first [ progress cbv [wf_maybe_do_again_expr] in * + | break_innermost_match_step + | progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | eapply wf_reify_expr_beta_iota; try eassumption + | constructor + | solve [ eauto ] ]. } + Qed. + End with_var. + End Reify. End RewriteRules. End Compilers. diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index 9bac61295..eb02d9ad6 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -25,6 +25,114 @@ Local Coercion Z.of_nat : nat >-> Z. Local Coercion QArith_base.inject_Z : Z >-> Q. Local Coercion Z.pos : positive >-> Z. +Module debugging_rewriting. + Section __. + Context (n : nat := 2%nat) + (s : Z := 2^127) + (c : list (Z * Z) := [(1,1)]) + (machine_wordsize : Z := 64). + + Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. + Let idxs := (List.seq 0 n ++ [0; 1])%list%nat. + + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + + + Let prime_upperbound_list : list Z + := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1). + Let tight_upperbounds : list Z + := List.map + (fun v : Z => Qceiling (11/10 * v)) + prime_upperbound_list. + Definition tight_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. + Definition loose_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. + + + Let limbwidth_num := Eval vm_compute in Qnum limbwidth. + Let limbwidth_den := Eval vm_compute in QDen limbwidth. + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => ( (addmod limbwidth_num limbwidth_den n f g) + )) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => ( (add (weight limbwidth_num limbwidth_den) n f g) + )) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f g + => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in + let b_a := to_associational (weight limbwidth_num limbwidth_den) n g in from_associational (weight limbwidth_num limbwidth_den) n (a_a ++ b_a) + ) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f (g : list Z) + => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in + a_a) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun (f g : list Z) + => let a_a := combine (map (weight limbwidth_num limbwidth_den) (seq 0 n)) f in + a_a) in + exact r) + (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt)) + ZRange.type.base.option.None). + + Definition foo := (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (combine [1; 2] [1; 2]) in + exact r) + tt + ZRange.type.base.option.None). + + (* + Goal True. + pose foo as X; cbv [foo] in X. + clear -X. + cbv [Pipeline.BoundsPipeline LetIn.Let_In] in X. + set (Y := (PartialEvaluateWithListInfoFromBounds _ _)) in (value of X). + vm_compute in Y. + subst Y; set (Y := (Rewriter.Compilers.PartialEvaluate _)) in (value of X). + cbv [Rewriter.Compilers.PartialEvaluate Rewriter.Compilers.RewriteRules.RewriteNBE Rewriter.Compilers.RewriteRules.Compile.Rewrite Rewriter.Compilers.RewriteRules.Compile.rewrite] in Y. + clear -Y. + change (Rewriter.Compilers.RewriteRules.nbe_default_fuel) with (S (pred Rewriter.Compilers.RewriteRules.nbe_default_fuel)) in (value of Y). + cbn [Rewriter.Compilers.RewriteRules.Compile.repeat_rewrite] in Y. + cbv [Rewriter.Compilers.RewriteRules.Compile.rewrite_bottomup] in Y. + Print Rewriter.Compilers.RewriteRules.nbe_rewrite_head. + Abort. + *) + End __. +End debugging_rewriting. + Section debugging_p448. Context (n : nat := 8%nat) (s : Z := 2^448) |