diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-04-05 20:24:08 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-04-11 11:01:29 -0400 |
| commit | ad3f1343356b2ac60da964922459105e3329af0e (patch) | |
| tree | 2cfe624931ce09ea109840bc14803542847faf28 /src | |
| parent | 7b6cc09fa0273b1eed867bd11583f7b46be5b4e2 (diff) | |
Automate more of the rewriter, and factor out rule-specific things
Diffstat (limited to 'src')
| -rw-r--r-- | src/BoundsPipeline.v | 3 | ||||
| -rw-r--r-- | src/CompilersTestCases.v | 4 | ||||
| -rw-r--r-- | src/Language.v | 100 | ||||
| -rw-r--r-- | src/PreLanguage.v | 54 | ||||
| -rw-r--r-- | src/Rewriter.v | 386 | ||||
| -rw-r--r-- | src/RewriterFull.v | 49 | ||||
| -rw-r--r-- | src/RewriterProofs.v | 178 | ||||
| -rw-r--r-- | src/RewriterRules.v | 15 | ||||
| -rw-r--r-- | src/RewriterRulesGood.v | 227 | ||||
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 425 | ||||
| -rw-r--r-- | src/RewriterWf1.v | 461 |
11 files changed, 865 insertions, 1037 deletions
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index f0c161dc2..af25f223e 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -24,6 +24,7 @@ Require Crypto.Language. Require Crypto.UnderLets. Require Crypto.AbstractInterpretation. Require Crypto.Rewriter. +Require Crypto.RewriterFull. Require Crypto.MiscCompilerPasses. Require Crypto.CStringification. Require Crypto.LanguageWf. @@ -46,6 +47,7 @@ Import Crypto.UnderLets Crypto.AbstractInterpretation Crypto.Rewriter + Crypto.RewriterFull Crypto.MiscCompilerPasses Crypto.CStringification. @@ -60,6 +62,7 @@ Import UnderLets.Compilers AbstractInterpretation.Compilers Rewriter.Compilers + RewriterFull.Compilers MiscCompilerPasses.Compilers CStringification.Compilers. diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v index d5c8b2579..19fcf1588 100644 --- a/src/CompilersTestCases.v +++ b/src/CompilersTestCases.v @@ -5,7 +5,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.AbstractInterpretation. -Require Import Crypto.Rewriter. +Require Import Crypto.RewriterFull. Require Import Crypto.MiscCompilerPasses. Require Import Crypto.CStringification. Import ListNotations. Local Open Scope Z_scope. @@ -13,7 +13,7 @@ Import ListNotations. Local Open Scope Z_scope. Import Language.Compilers. Import UnderLets.Compilers. Import AbstractInterpretation.Compilers. -Import Rewriter.Compilers. +Import RewriterFull.Compilers. Import MiscCompilerPasses.Compilers. Import CStringification.Compilers. Local Coercion Z.of_nat : nat >-> Z. diff --git a/src/Language.v b/src/Language.v index 966cd3118..eb64e0f2e 100644 --- a/src/Language.v +++ b/src/Language.v @@ -3,6 +3,7 @@ Require Import Coq.FSets.FMapPositive. Require Import Coq.Bool.Bool. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. +Require Import Crypto.PreLanguage. Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. Require Import Crypto.Util.Option. @@ -18,8 +19,10 @@ Require Import Crypto.Util.Tactics.RunTacticAsConstr. Require Import Crypto.Util.Tactics.DebugPrint. Require Import Crypto.Util.Tactics.ConstrFail. Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. +Export PreLanguage. Module Compilers. + Export PreLanguage. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. Module Reify. @@ -1012,27 +1015,9 @@ Module Compilers. Section gen. Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z). - Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool - := ((Z.abs (lower r) <? Z.abs (upper r)) (* if more of the range is above 0 than below 0 *) - || ((lower r =? upper r) && (0 <=? lower r)) - || ((Z.abs (lower r) =? Z.abs (upper r)) && (0 <=? v))). - - (** We ensure that [ident.cast] is symmetric under [Z.opp], as - this makes some rewrite rules much, much easier to - prove. *) - Let cast_outside_of_range' (r : zrange) (v : BinInt.Z) : BinInt.Z - := ((cast_outside_of_range r v - lower r) mod (upper r - lower r + 1)) + lower r. - - Definition cast (r : zrange) (x : BinInt.Z) - := let r := ZRange.normalize r in - if (lower r <=? x) && (x <=? upper r) - then x - else if is_more_pos_than_neg r x - then cast_outside_of_range' r x - else -cast_outside_of_range' (-r) (-x). - Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z) - := (cast (Datatypes.fst r) (Datatypes.fst x), - cast (Datatypes.snd r) (Datatypes.snd x)). + Local Notation is_more_pos_than_neg := ident.is_more_pos_than_neg. + Local Notation cast := (ident.cast cast_outside_of_range). + Local Notation cast2 := (ident.cast2 cast_outside_of_range). Local Notation wordmax log2wordmax := (2 ^ log2wordmax). Local Notation half_bits log2wordmax := (log2wordmax / 2). @@ -1153,39 +1138,20 @@ Module Compilers. => fancy.interp (invert_Some (to_fancy idc)) end. End gen. - - Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z. - Proof. exact v. Qed. End with_base. Notation Some := option_Some. Notation None := option_None. (** Interpret identifiers where [Z_cast] is an opaque identity function when the value is not inside the range *) - Notation interp := (@gen_interp cast_outside_of_range). + Notation interp := (@gen_interp ident.cast_outside_of_range). Notation LiteralUnit := (@Literal base.type.unit). Notation LiteralZ := (@Literal base.type.Z). Notation LiteralBool := (@Literal base.type.bool). Notation LiteralNat := (@Literal base.type.nat). Notation LiteralZRange := (@Literal base.type.zrange). - Definition literal {T} (v : T) := v. - Definition eagerly {T} (v : T) := v. - Definition gets_inlined (real_val : bool) {T} (v : T) : bool := real_val. (** TODO: MOVE ME? *) - Module Thunked. - Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P - := Datatypes.bool_rect (fun _ => P) (t tt) (f tt) b. - Definition list_rect {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P -> P) (ls : list A) : P - := Datatypes.list_rect (fun _ => P) (N tt) C ls. - Definition list_case {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P) (ls : list A) : P - := ListUtil.list_case (fun _ => P) (N tt) C ls. - Definition nat_rect P (O_case : unit -> P) (S_case : nat -> P -> P) (n : nat) : P - := Datatypes.nat_rect (fun _ => P) (O_case tt) S_case n. - Definition option_rect {A} P (S_case : A -> P) (N_case : unit -> P) (o : option A) : P - := Datatypes.option_rect (fun _ => P) S_case (N_case tt) o. - End Thunked. - Ltac require_primitive_const term := lazymatch term with | S ?n => require_primitive_const n @@ -1203,7 +1169,7 @@ Module Compilers. | Datatypes.None => idtac | ZRange.Build_zrange ?x ?y => require_primitive_const x; require_primitive_const y - | literal ?x => idtac + | ident.literal ?x => idtac | ?term => fail 0 "Not a known const:" term end. Ltac is_primitive_const term := @@ -1259,20 +1225,20 @@ Module Compilers. then_tac (@ident.pair rA rB) | @Datatypes.bool_rect ?T0 ?Ptrue ?Pfalse => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.bool_rect T (fun _ : Datatypes.unit => Ptrue) (fun _ : Datatypes.unit => Pfalse)) + | fun _ => ?T => reify_rec (@ident.Thunked.bool_rect T (fun _ : Datatypes.unit => Ptrue) (fun _ : Datatypes.unit => Pfalse)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.bool_rect T' Ptrue Pfalse) end - | @Thunked.bool_rect ?T + | @ident.Thunked.bool_rect ?T => let rT := base.reify T in then_tac (@ident.bool_rect rT) | @Datatypes.option_rect ?A ?T0 ?PSome ?PNone => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.option_rect A T PSome (fun _ : Datatypes.unit => PNone)) + | fun _ => ?T => reify_rec (@ident.Thunked.option_rect A T PSome (fun _ : Datatypes.unit => PNone)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.option_rect A T' PSome PNone) end - | @Thunked.option_rect ?A ?T + | @ident.Thunked.option_rect ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.option_rect rA rT) @@ -1297,7 +1263,7 @@ Module Compilers. | @Datatypes.nat_rect ?T0 ?P0 => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (@Thunked.nat_rect T (fun _ : Datatypes.unit => P0)) + | fun _ => ?T => reify_rec (@ident.Thunked.nat_rect T (fun _ : Datatypes.unit => P0)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.nat_rect T' P0) end @@ -1310,32 +1276,32 @@ Module Compilers. | T0 => else_tac () | ?T' => reify_rec (@Datatypes.nat_rect T') end - | @Thunked.nat_rect ?T + | @ident.Thunked.nat_rect ?T => let rT := base.reify T in then_tac (@ident.nat_rect rT) - | eagerly (@Datatypes.nat_rect) ?T0 ?P0 + | ident.eagerly (@Datatypes.nat_rect) ?T0 ?P0 => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (eagerly (@Thunked.nat_rect) T (fun _ : Datatypes.unit => P0)) + | fun _ => ?T => reify_rec (ident.eagerly (@ident.Thunked.nat_rect) T (fun _ : Datatypes.unit => P0)) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T' P0) + | ?T' => reify_rec (ident.eagerly (@Datatypes.nat_rect) T' P0) end - | eagerly (@Datatypes.nat_rect) ?T0 + | ident.eagerly (@Datatypes.nat_rect) ?T0 => lazymatch (eval cbv beta in T0) with | (fun _ => ?P -> ?Q) => let rP := base.reify P in let rQ := base.reify Q in then_tac (@ident.eager_nat_rect_arrow rP rQ) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.nat_rect) T') + | ?T' => reify_rec (ident.eagerly (@Datatypes.nat_rect) T') end - | eagerly (@Thunked.nat_rect) ?T + | ident.eagerly (@ident.Thunked.nat_rect) ?T => let rT := base.reify T in then_tac (@ident.eager_nat_rect rT) | @Datatypes.list_rect ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (@ident.Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil) end @@ -1349,18 +1315,18 @@ Module Compilers. | T0 => else_tac () | ?T' => reify_rec (@Datatypes.list_rect A T') end - | @Thunked.list_rect ?A ?T + | @ident.Thunked.list_rect ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.list_rect rA rT) - | eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil + | ident.eagerly (@Datatypes.list_rect) ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with | fun _ => _ -> _ => else_tac () - | fun _ => ?T => reify_rec (eagerly (@Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (ident.eagerly (@ident.Thunked.list_rect) A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T' Pnil) + | ?T' => reify_rec (ident.eagerly (@Datatypes.list_rect) A T' Pnil) end - | eagerly (@Datatypes.list_rect) ?A ?T0 + | ident.eagerly (@Datatypes.list_rect) ?A ?T0 => lazymatch (eval cbv beta in T0) with | (fun _ => ?P -> ?Q) => let rA := base.reify A in @@ -1368,19 +1334,19 @@ Module Compilers. let rQ := base.reify Q in then_tac (@ident.eager_list_rect_arrow rA rP rQ) | T0 => else_tac () - | ?T' => reify_rec (eagerly (@Datatypes.list_rect) A T') + | ?T' => reify_rec (ident.eagerly (@Datatypes.list_rect) A T') end - | eagerly (@Thunked.list_rect) ?A ?T + | ident.eagerly (@ident.Thunked.list_rect) ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.eager_list_rect rA rT) | @ListUtil.list_case ?A ?T0 ?Pnil => lazymatch (eval cbv beta in T0) with - | fun _ => ?T => reify_rec (@Thunked.list_case A T (fun _ : Datatypes.unit => Pnil)) + | fun _ => ?T => reify_rec (@ident.Thunked.list_case A T (fun _ : Datatypes.unit => Pnil)) | T0 => else_tac () | ?T' => reify_rec (@ListUtil.list_case A T' Pnil) end - | @Thunked.list_case ?A ?T + | @ident.Thunked.list_case ?A ?T => let rA := base.reify A in let rT := base.reify T in then_tac (@ident.list_case rA rT) @@ -1479,9 +1445,9 @@ Module Compilers. => let rA := base.reify A in then_tac (@ident.None rA) | ZRange.Build_zrange => then_tac ident.Build_zrange - | eagerly (?f ?x) => reify_rec (eagerly f x) + | ident.eagerly (?f ?x) => reify_rec (ident.eagerly f x) | fancy.interp ?idc - => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in + => let ridc := (eval cbv [of_fancy] in (of_fancy idc)) in then_tac ridc | @gen_interp _ _ ?idc => then_tac idc | _ => else_tac () @@ -2047,4 +2013,4 @@ Module Compilers. := FromFlat (to_flat e). End GeneralizeVar. End Compilers. -Global Opaque Compilers.ident.cast. (* This should never be unfolded except in [LanguageWf] *) +Global Opaque ident.cast. (* This should never be unfolded except in [LanguageWf] *) diff --git a/src/PreLanguage.v b/src/PreLanguage.v new file mode 100644 index 000000000..04146dddb --- /dev/null +++ b/src/PreLanguage.v @@ -0,0 +1,54 @@ +(** Definitions for use in pre-reified rewriter rules *) +Require Import Coq.ZArith.BinInt. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Local Open Scope bool_scope. +Local Open Scope Z_scope. + +Module ident. + Definition literal {T} (v : T) := v. + Definition eagerly {T} (v : T) := v. + Definition gets_inlined (real_val : bool) {T} (v : T) : bool := real_val. + + Section cast. + Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z). + + Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool + := ((Z.abs (lower r) <? Z.abs (upper r)) (* if more of the range is above 0 than below 0 *) + || ((lower r =? upper r) && (0 <=? lower r)) + || ((Z.abs (lower r) =? Z.abs (upper r)) && (0 <=? v))). + + (** We ensure that [ident.cast] is symmetric under [Z.opp], as + this makes some rewrite rules much, much easier to + prove. *) + Let cast_outside_of_range' (r : zrange) (v : BinInt.Z) : BinInt.Z + := ((cast_outside_of_range r v - lower r) mod (upper r - lower r + 1)) + lower r. + + Definition cast (r : zrange) (x : BinInt.Z) + := let r := ZRange.normalize r in + if (lower r <=? x) && (x <=? upper r) + then x + else if is_more_pos_than_neg r x + then cast_outside_of_range' r x + else -cast_outside_of_range' (-r) (-x). + Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z) + := (cast (Datatypes.fst r) (Datatypes.fst x), + cast (Datatypes.snd r) (Datatypes.snd x)). + End cast. + + Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z. + Proof. exact v. Qed. + + Module Thunked. + Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P + := Datatypes.bool_rect (fun _ => P) (t tt) (f tt) b. + Definition list_rect {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P -> P) (ls : list A) : P + := Datatypes.list_rect (fun _ => P) (N tt) C ls. + Definition list_case {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P) (ls : list A) : P + := ListUtil.list_case (fun _ => P) (N tt) C ls. + Definition nat_rect P (O_case : unit -> P) (S_case : nat -> P -> P) (n : nat) : P + := Datatypes.nat_rect (fun _ => P) (O_case tt) S_case n. + Definition option_rect {A} P (S_case : A -> P) (N_case : unit -> P) (o : option A) : P + := Datatypes.option_rect (fun _ => P) S_case (N_case tt) o. + End Thunked. +End ident. diff --git a/src/Rewriter.v b/src/Rewriter.v index 05a802ddd..34107b2c2 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -13,7 +13,6 @@ Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.Tactics.ConstrFail. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. -Require Import Crypto.RewriterRules. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.GENERATEDIdentifiersWithoutTypes. @@ -1716,7 +1715,11 @@ Module Compilers. Ltac equation_to_parts' lem side_conditions := lazymatch lem with | ?H -> ?P - => let H := prop_to_bool H in + => let __ := lazymatch type of H with + | Prop => constr:(I) + | ?T => constr_fail_with ltac:(fun _ => fail 1 "Invalid non-Prop non-dependent hypothesis of type" H ":" T "when reifying a lemma of type" lem) + end in + let H := prop_to_bool H in let side_conditions := push_side_conditions H side_conditions in equation_to_parts' P side_conditions | forall x : ?T, ?P @@ -2435,12 +2438,16 @@ Module Compilers. | _ => check_debug_level_then_Set () end. + Definition pident_unify_unknown := @pattern.ident.unify. + Definition invert_bind_args_unknown := @pattern.Raw.ident.invert_bind_args. + Module Export GoalType. Record rewriter_dataT := Build_rewriter_dataT' { rewrite_rules_specs : list (bool * Prop); dummy_count : nat; + dtree : @Compile.decision_tree pattern.Raw.ident; rewrite_rules : forall var, @Compile.rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types) ; all_rewrite_rules (* adjusted version *) : _; @@ -2448,9 +2455,11 @@ Module Compilers. 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))) + rewrite_head0 + := (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_head (* adjusted version *) : 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. @@ -2473,94 +2482,95 @@ Module Compilers. | _ => 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. + Ltac time_if_debug1 := + let lvl := rewriter_assembly_debug_level in + lazymatch lvl with + | O => ltac:(fun tac => tac ()) + | S _ => ltac:(fun tac => time tac ()) + | ?v => ltac:(fun tac => fail 0 "Invalid non-nat rewriter_assembly_debug_level" v) + end. + Ltac time_tac_in_constr_if_debug1 tac := + constr:(ltac:(time_if_debug1 ltac:(fun _ => idtac; let v := tac () in exact v))). 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))). + time_tac_in_constr_if_debug1 + ltac:(fun _ + => 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 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))). + time_tac_in_constr_if_debug1 + ltac:(fun _ + => (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 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))). + time_tac_in_constr_if_debug1 + ltac:(fun _ + => (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 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 @@ -2572,10 +2582,7 @@ Module Compilers. => 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 + let v := make_rewrite_head' rewrite_head0 pr2_rewrite_rules in exact v)) in cache_term v rewrite_head. @@ -2605,187 +2612,56 @@ Module Compilers. 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 + constr:(@Build_rewriter_dataT' + specs dummy_count dtree rewrite_rules all_rewrite_rules eq_refl default_fuel - rewrite_head0 rewrite_head eq_refl). + (*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 / . + Module Export Settings. + 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 / . + End Settings. Tactic Notation "make_rewriter_data" constr(include_interp) constr(specs) := - Build_rewriter_dataT include_interp specs. + let res := Build_rewriter_dataT include_interp specs in refine res. 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_transport_cps {P} t1 t2 {_} _. - Arguments type.try_make_transport_cps {base_type _ P} t1 t2 {_} _. - Export pattern.Raw.ident. - Export GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw. - Export GENERATEDIdentifiersWithoutTypes.Compilers.pattern. - Export UnderLets. - Export Compilers.ident. - Export Language.Compilers. - Export Language.Compilers.defaults. - Export PrimitiveSigma.Primitive. - Notation "'llet' x := v 'in' f" := (Let_In v (fun x => f)). - Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.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 <- 'type.try_make_transport_cps' t1 t2 ; '/' f ']'"). - Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with 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. - - (* 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 option {_}. - Local Arguments UnderLets.UnderLets {_ _ _}. - Local Arguments expr.expr {_ _ _}. - Local Notation ℤ := base.type.Z. - Local Notation ℕ := base.type.nat. - Local Notation bool := base.type.bool. - Local Notation unit := base.type.unit. - Local Notation list := base.type.list. - Local Notation "x" := (type.base x) (only printing, at level 9). - - Section red_fancy. - Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z). - - 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. - Import RewriterPrintingNotations. - Redirect "fancy_rewrite_head" Print fancy_rewrite_head. - End red_fancy. - Section red_fancy_with_casts. - Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) - (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. - Import RewriterPrintingNotations. - Redirect "fancy_with_casts_rewrite_head" Print fancy_with_casts_rewrite_head. - End red_fancy_with_casts. - Section red_nbe. - Local Definition nbe_rewrite_head - := Eval hnf in rewrite_head nbe_rewriter_data. - - Local Set Printing Depth 1000000. - Local Set Printing Width 200. - Import RewriterPrintingNotations. - Redirect "nbe_rewrite_head" Print nbe_rewrite_head. - End red_nbe. - - Section red_arith. - 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. - Import RewriterPrintingNotations. - Redirect "arith_rewrite_head" Print arith_rewrite_head. - End red_arith. - - Section red_arith_with_casts. - 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. - Import RewriterPrintingNotations. - Redirect "arith_with_casts_rewrite_head" Print arith_with_casts_rewrite_head. - End red_arith_with_casts. - - Section red_strip_literal_casts. - 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. - Import RewriterPrintingNotations. - 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 - := 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 - := 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 - := 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 - := 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 - := 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 - := unfold_Rewrite (@RewriteToFancyWithCasts_folded invert_low invert_high value_range flag_range t e). + Module Export GoalType. + Record RewriterT := + { + Rewriter_data : rewriter_dataT; + Rewrite : forall {t} (e : expr.Expr (ident:=ident) t), expr.Expr (ident:=ident) t; + Rewrite_eq : @Rewrite = @Make.Rewrite Rewriter_data + }. + End GoalType. + + Ltac Build_RewriterT include_interp specs := + let rewriter_data := fresh "rewriter_data" in + let data := Make.Build_rewriter_dataT include_interp specs in + let Rewrite_name := fresh "Rewriter" in + let Rewrite := (eval cbv [Make.Rewrite rewrite_head default_fuel] in (@Make.Rewrite data)) in + let Rewrite := cache_term Rewrite Rewrite_name in + constr:(@Build_RewriterT data Rewrite eq_refl). + + Module Export Tactic. + Module Export Settings. + Export Make.Tactic.Settings. + End Settings. + + Tactic Notation "make_Rewriter" constr(include_interp) constr(specs) := + let res := Build_RewriterT include_interp specs in refine res. + End Tactic. End RewriteRules. - - Import defaults. - - Definition PartialEvaluate {t} (e : Expr t) : Expr t := RewriteRules.RewriteNBE e. End Compilers. diff --git a/src/RewriterFull.v b/src/RewriterFull.v new file mode 100644 index 000000000..772732442 --- /dev/null +++ b/src/RewriterFull.v @@ -0,0 +1,49 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZRange. +Require Import Crypto.RewriterRules. +Require Import Crypto.Rewriter. +Local Open Scope Z_scope. + +Import Compilers.RewriteRules.GoalType. +Import Compilers.RewriteRules.Tactic. + +Module Compilers. + Module RewriteRules. + Definition RewriterNBE : RewriterT. + Proof. make_Rewriter true nbe_rewrite_rulesT. Defined. + + Definition RewriterArith (max_const_val : Z) : RewriterT. + Proof. make_Rewriter false (arith_rewrite_rulesT max_const_val). Defined. + + Definition RewriterArithWithCasts : RewriterT. + Proof. make_Rewriter false arith_with_casts_rewrite_rulesT. Defined. + + Definition RewriterStripLiteralCasts : RewriterT. + Proof. make_Rewriter false strip_literal_casts_rewrite_rulesT. Defined. + + Definition RewriterToFancy + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + : RewriterT. + Proof. make_Rewriter false fancy_rewrite_rulesT. Defined. + + Definition RewriterToFancyWithCasts + (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) + (value_range flag_range : zrange) + : RewriterT. + Proof. make_Rewriter false (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Defined. + + Definition RewriteNBE {t} := Eval hnf in @Rewrite RewriterNBE t. + Definition RewriteArith max_const_val {t} := Eval hnf in @Rewrite (RewriterArith max_const_val) t. + Definition RewriteArithWithCasts {t} := Eval hnf in @Rewrite RewriterArithWithCasts t. + Definition RewriteStripLiteralCasts {t} := Eval hnf in @Rewrite RewriterStripLiteralCasts t. + Definition RewriteToFancy invert_low invert_high {t} + := Eval hnf in @Rewrite (RewriterToFancy invert_low invert_high) t. + Definition RewriteToFancyWithCasts invert_low invert_high value_range flag_range {t} + := Eval hnf in @Rewrite (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) t. + End RewriteRules. + + Import Language.Compilers.defaults. + + Definition PartialEvaluate {t} (e : Expr t) : Expr t + := RewriteRules.RewriteNBE e. +End Compilers. diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v index 6da5a9e47..2d45a6271 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -1,33 +1,17 @@ Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.FSets.FMapPositive. Require Import Crypto.Language. Require Import Crypto.LanguageInversion. Require Import Crypto.LanguageWf. Require Import Crypto.UnderLetsProofs. Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. Require Import Crypto.Rewriter. +Require Import Crypto.RewriterFull. 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. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Decidable. Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. @@ -39,6 +23,7 @@ Module Compilers. Import UnderLetsProofs.Compilers. Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. Import Rewriter.Compilers. + Import RewriterFull.Compilers. Import RewriterWf1.Compilers. Import RewriterWf2.Compilers. Import RewriterInterpProofs1.Compilers. @@ -47,131 +32,117 @@ Module Compilers. Import expr.Notations. Import defaults. Import Rewriter.Compilers.RewriteRules. + Import RewriterFull.Compilers.RewriteRules. Import RewriterWf1.Compilers.RewriteRules. Import RewriterWf2.Compilers.RewriteRules. Import RewriterInterpProofs1.Compilers.RewriteRules. Import RewriterRulesGood.Compilers.RewriteRules. Import RewriterRulesInterpGood.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. Module Import RewriteRules. + Module Export Tactics. + Definition VerifiedRewriter_of_Rewriter + (R : RewriterT) + (RWf : Wf_GoalT R) + (RInterp : Interp_GoalT R) + (RProofs : PrimitiveHList.hlist + (@snd bool Prop) + (List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R)))) + : VerifiedRewriter. + Proof. + simple refine + (let HWf := _ in + let HInterp_gen := _ in + @Build_VerifiedRewriter R RWf RInterp HWf HInterp_gen (HInterp_gen _)); + [ | clear HWf ]; intros. + all: abstract ( + rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq; + first [ apply Compile.Wf_Rewrite; [ | assumption ]; + let wf_do_again := fresh "wf_do_again" in + (intros ? ? ? ? wf_do_again ? ?); + eapply @Compile.wf_assemble_identifier_rewriters; + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct + with nocore; + try reflexivity + | eapply Compile.InterpRewrite; [ | assumption ]; + intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, + @ident.gen_interp_Proper, eq_refl + with nocore ]). + Defined. + End Tactics. - 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 - 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 ? ?); - eapply @Compile.wf_assemble_identifier_rewriters; - eauto using - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct - with nocore; - try reflexivity. - 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 - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, - @ident.gen_interp_Proper, eq_refl - with nocore. + Definition VerifiedRewriterNBE : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter RewriterNBE RewriterRulesNBEWf RewriterRulesNBEInterp nbe_rewrite_rules_proofs. + Definition VerifiedRewriterArith (max_const_val : Z) : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter (RewriterArith max_const_val) (RewriterRulesArithWf max_const_val) (RewriterRulesArithInterp max_const_val) (arith_rewrite_rules_proofs max_const_val). + Definition VerifiedRewriterArithWithCasts : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter RewriterArithWithCasts RewriterRulesArithWithCastsWf RewriterRulesArithWithCastsInterp arith_with_casts_rewrite_rules_proofs. + Definition VerifiedRewriterStripLiteralCasts : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter RewriterStripLiteralCasts RewriterRulesStripLiteralCastsWf RewriterRulesStripLiteralCastsInterp strip_literal_casts_rewrite_rules_proofs. + Definition VerifiedRewriterToFancy (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)) + : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter (RewriterToFancy invert_low invert_high) (RewriterRulesToFancyWf invert_low invert_high Hlow Hhigh) (RewriterRulesToFancyInterp invert_low invert_high Hlow Hhigh) fancy_rewrite_rules_proofs. + Definition VerifiedRewriterToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) + (value_range flag_range : ZRange.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)) + : VerifiedRewriter + := @VerifiedRewriter_of_Rewriter (RewriterToFancyWithCasts invert_low invert_high value_range flag_range) (RewriterRulesToFancyWithCastsWf invert_low invert_high value_range flag_range Hlow Hhigh) (RewriterRulesToFancyWithCastsInterp invert_low invert_high value_range flag_range Hlow Hhigh) (fancy_with_casts_rewrite_rules_proofs invert_low invert_high value_range flag_range Hlow Hhigh). Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). - Proof. - start_Wf_proof RewriteNBE_folded. - apply nbe_rewrite_rules_good. - Qed. + Proof. now apply VerifiedRewriterNBE. Qed. Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e). - Proof. - start_Wf_proof RewriteArith_folded. - apply arith_rewrite_rules_good. - Qed. + Proof. now apply VerifiedRewriterArith. Qed. Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e). - Proof. - start_Wf_proof RewriteArithWithCasts_folded. - apply arith_with_casts_rewrite_rules_good. - Qed. + Proof. now apply VerifiedRewriterArithWithCasts. Qed. Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e). - Proof. - start_Wf_proof RewriteStripLiteralCasts_folded. - apply strip_literal_casts_rewrite_rules_good. - Qed. + Proof. now apply VerifiedRewriterStripLiteralCasts. Qed. Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e). - Proof. - start_Wf_proof RewriteToFancy_folded. - apply fancy_rewrite_rules_good; assumption. - Qed. - + Proof. unshelve eapply VerifiedRewriterToFancy; multimatch goal with H : _ |- _ => refine H end. Qed. Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : ZRange.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)) {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e). - Proof. - start_Wf_proof RewriteToFancyWithCasts_folded. - apply fancy_with_casts_rewrite_rules_good; assumption. - Qed. + Proof. now unshelve eapply VerifiedRewriterToFancyWithCasts. 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 RewriteNBE_folded. - apply nbe_rewrite_rules_interp_good, nbe_rewrite_rules_proofs. - Qed. + Proof. now apply VerifiedRewriterNBE. 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 RewriteArith_folded. - apply arith_rewrite_rules_interp_good, arith_rewrite_rules_proofs. - Qed. - + Proof. now apply VerifiedRewriterArith. 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 RewriteArithWithCasts_folded. - apply arith_with_casts_rewrite_rules_interp_good, arith_with_casts_rewrite_rules_proofs. - Qed. - + Proof. now apply VerifiedRewriterArithWithCasts. 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 RewriteStripLiteralCasts_folded. - apply strip_literal_casts_rewrite_rules_interp_good, strip_literal_casts_rewrite_rules_proofs. - Qed. - + Proof. now apply VerifiedRewriterStripLiteralCasts. Qed. Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) {t} e (Hwf : Wf e) : 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 RewriteToFancy_folded. - apply fancy_rewrite_rules_interp_good; try assumption; apply fancy_rewrite_rules_proofs; assumption. - Qed. - + Proof. unshelve eapply VerifiedRewriterToFancy; multimatch goal with H : _ |- _ => refine H end. Qed. Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) (value_range flag_range : ZRange.zrange) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) @@ -179,10 +150,7 @@ Module Compilers. {t} e (Hwf : Wf e) : 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 RewriteToFancyWithCasts_folded. - apply fancy_with_casts_rewrite_rules_interp_good; try assumption; apply fancy_with_casts_rewrite_rules_proofs; assumption. - Qed. + Proof. now unshelve eapply VerifiedRewriterToFancyWithCasts. Qed. Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. Proof. apply Interp_gen_RewriteNBE; assumption. Qed. diff --git a/src/RewriterRules.v b/src/RewriterRules.v index 08a4e8d1f..f7bc63bfa 100644 --- a/src/RewriterRules.v +++ b/src/RewriterRules.v @@ -6,7 +6,7 @@ Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. -Require Import Crypto.Language. +Require Import Crypto.PreLanguage. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. @@ -17,8 +17,6 @@ Local Definition myflatten {A} := Eval cbv in List.fold_right myapp (@nil A). Local Notation dont_do_again := (pair false) (only parsing). Local Notation do_again := (pair true) (only parsing). -Import Language.Compilers. - Local Notation "' x" := (ident.literal x). Local Notation cstZ := (ident.cast ident.cast_outside_of_range). Local Notation cstZZ := (ident.cast2 ident.cast_outside_of_range). @@ -76,7 +74,10 @@ Local Ltac generalize_cast' force_progress term := | _ => default () end end. -Local Ltac generalize_cast term := generalize_cast' false term. +Local Ltac early_unfold_in term := term. +Local Ltac generalize_cast term := + let term := early_unfold_in term in + generalize_cast' false term. (* Play tricks/games with [match] to get [term] interpreted as a constr rather than an ident when it's not closed, to get better error messages *) Local Notation generalize_cast term @@ -486,6 +487,12 @@ Definition arith_with_casts_rewrite_rulesT : list (bool * Prop) Definition strip_literal_casts_rewrite_rulesT : list (bool * Prop) := generalize_cast [dont_do_again (forall rx x, x ∈ rx -> cstZ rx ('x) = 'x)]%Z%zrange. +(** FIXME Don't use [ident.interp] for the fancy identifier rewrite rules *) +Require Import Crypto.Language. +Import Compilers. + +Ltac early_unfold_in term ::= (eval cbv [ident.interp ident.to_fancy Option.invert_Some] in term). + Section fancy. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) (value_range flag_range : zrange). diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index c05bcc23e..2d3ed96e2 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -1,221 +1,42 @@ Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Language. -Require Import Crypto.LanguageInversion. -Require Import Crypto.LanguageWf. -Require Import Crypto.UnderLetsProofs. -Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Rewriter. +Require Import Crypto.RewriterFull. Require Import Crypto.RewriterWf1. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SpecializeAllWays. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.ListUtil.ForallIn. -Require Import Crypto.Util.ListUtil.Forall. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Decidable. -Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. -Import EqNotations. Module Compilers. - Import Language.Compilers. - Import LanguageInversion.Compilers. - Import LanguageWf.Compilers. - Import UnderLetsProofs.Compilers. - Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. - Import Rewriter.Compilers. + Import RewriterFull.Compilers. Import RewriterWf1.Compilers. - Import expr.Notations. - Import RewriterWf1.Compilers.RewriteRules. - Import defaults. Module Import RewriteRules. - Import Rewriter.Compilers.RewriteRules. + Import RewriterFull.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. - Section good. - Context {var1 var2 : type -> Type}. + Lemma RewriterRulesNBEWf : Wf_GoalT RewriterNBE. + Proof. prove_good (). Qed. - Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2). + Lemma RewriterRulesArithWf max_const : Wf_GoalT (RewriterArith max_const). + Proof. prove_good (). 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 RewriterRulesArithWithCastsWf : Wf_GoalT RewriterArithWithCasts. + Proof. prove_good (). Qed. - Lemma wf_nat_rect {A} - G O1 O2 S1 S2 n - (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_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. + Lemma RewriterRulesStripLiteralCastsWf : Wf_GoalT RewriterStripLiteralCasts. + Proof. prove_good (). Qed. - Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps]. - - Local Ltac start_good := - 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 - | 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 ]. - - 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: abstract (handle_reified_rewrite_rules; handle_extra_nbe). - Qed. - - Local Ltac handle_extra_arith_rules := - 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 - end - | 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. - 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. - 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. - 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 invert_low invert_high) (fancy_rewrite_rules invert_low invert_high). - Proof using Type. - Time start_good. - Time all: handle_reified_rewrite_rules. - 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 + Lemma RewriterRulesToFancyWf (invert_low invert_high : Z -> Z -> option Z) - (value_range flag_range : ZRange.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_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: handle_reified_rewrite_rules. - Time Qed. - End good. + : Wf_GoalT (RewriterToFancy invert_low invert_high). + Proof. prove_good (). Qed. + + Lemma RewriterRulesToFancyWithCastsWf + (invert_low invert_high : Z -> Z -> option Z) + (value_range flag_range : ZRange.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)) + : Wf_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range). + Proof. prove_good (). Qed. End RewriteRules. End Compilers. diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 4b3c1d664..095719421 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -1,419 +1,42 @@ Require Import Coq.ZArith.ZArith. -Require Import Coq.micromega.Lia. -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.FSets.FMapPositive. -Require Import Crypto.Language. -Require Import Crypto.LanguageInversion. -Require Import Crypto.LanguageWf. -Require Import Crypto.UnderLetsProofs. -Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Rewriter. +Require Import Crypto.RewriterFull. Require Import Crypto.RewriterWf1. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.ListUtil.Forall. -Require Import Crypto.Util.ListUtil.ForallIn. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.HProp. -Require Import Crypto.Util.Decidable. -Import ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. -Import EqNotations. Module Compilers. - Import Language.Compilers. - Import LanguageInversion.Compilers. - Import LanguageWf.Compilers. - Import UnderLetsProofs.Compilers. - Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. - Import Rewriter.Compilers. + Import RewriterFull.Compilers. Import RewriterWf1.Compilers. - Import expr.Notations. - Import RewriterWf1.Compilers.RewriteRules. - Import defaults. Module Import RewriteRules. - Import Rewriter.Compilers.RewriteRules. - Section with_cast. - Context {cast_outside_of_range : zrange -> Z -> Z}. + Import RewriterFull.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. - Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range). - Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident_interp)). + Lemma RewriterRulesNBEInterp : Interp_GoalT RewriterNBE. + Proof. prove_interp_good (). Qed. - (** Coq >= 8.9 is much better at [eapply] than Coq <= Coq 8.8 *) - Local Ltac cbv_type_for_Coq88 T := - lazymatch eval hnf in T with - | @eq ?T ?A ?B => let A' := (eval cbv [ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.list_rect ident.Thunked.nat_rect ident.Thunked.option_rect] in A) in - constr:(@eq T A' B) - | forall x : ?A, ?P - => let P' := fresh in - constr:(forall x : A, - match P return Prop with - | P' - => ltac:(let v := cbv_type_for_Coq88 P' in - exact v) - end) - end. - Local Ltac cbv_for_Coq88_in H := - cbv [ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.list_rect ident.Thunked.nat_rect ident.Thunked.option_rect]; - let T := type of H in - let T := cbv_type_for_Coq88 T in - change T in H. + Lemma RewriterRulesArithInterp max_const : Interp_GoalT (RewriterArith max_const). + Proof. prove_interp_good (). Qed. - Local Ltac start_interp_good := - cbv [List.skipn] in *; - lazymatch goal with - | [ |- @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; - [ 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; - cbv_for_Coq88_in H; - 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 * - .. ]. + Lemma RewriterRulesArithWithCastsInterp : Interp_GoalT RewriterArithWithCasts. + Proof. prove_interp_good (). Qed. - Ltac recurse_interp_related_step := - let do_replace v := - ((tryif is_evar v then fail else idtac); - let v' := open_constr:(_) in - let v'' := fresh in - cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in - match goal with - | _ => progress cbv [expr.interp_related] in * - | _ => progress cbn [Compile.reify_expr] - | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand - | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand - | [ |- expr.interp_related_gen ?ident_interp ?R ?f ?v ] - => do_replace v - | [ |- 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; - first [ do_replace x - | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ] - | _ => progress intros - | [ |- expr.interp_related_gen _ _ _ ?ev ] => is_evar ev; eassumption - | [ |- expr.interp_related_gen _ _ (?f @ ?x) ?ev ] - => is_evar ev; - let fh := fresh in - let xh := fresh in - set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; - do 2 eexists; repeat apply conj; [ | | reflexivity ] - | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] - => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh - | [ |- expr.interp_related_gen _ _ (expr.Ident ?idc) ?ev ] - => is_evar ev; - cbn [expr.interp_related_gen]; apply ident.gen_interp_Proper; reflexivity - | [ |- _ = _ :> ?T ] - => lazymatch T with - | BinInt.Z => idtac - | (BinInt.Z * BinInt.Z)%type => idtac - 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. + Lemma RewriterRulesStripLiteralCastsInterp : Interp_GoalT RewriterStripLiteralCasts. + Proof. prove_interp_good (). Qed. - (* TODO: MOVE ME? *) - 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_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_case_in_goal := - let G := match goal with |- ?G => G end in - let G := recursive_match_to_case G in - change G. - - 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 - | match goal with - | [ |- 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 preprocess := repeat preprocess_step. - Local Ltac handle_extra_nbe := - repeat match goal with - | [ |- 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) - - | [ |- 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) - - | [ |- 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 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: preprocess; handle_extra_nbe; handle_reified_rewrite_rules_interp. - Time Qed. - - 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: preprocess; handle_reified_rewrite_rules_interp. - Time Qed. - - 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: preprocess; handle_reified_rewrite_rules_interp. - Time Qed. - - 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: 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)) - (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: preprocess; handle_reified_rewrite_rules_interp. - Time Qed. - - Lemma fancy_with_casts_rewrite_rules_interp_good + Lemma RewriterRulesToFancyInterp (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)) - (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. - Time all: preprocess; handle_reified_rewrite_rules_interp. - Time Qed. - End with_cast. + : Interp_GoalT (RewriterToFancy invert_low invert_high). + Proof. prove_interp_good (). Qed. + + Lemma RewriterRulesToFancyWithCastsInterp + (invert_low invert_high : Z -> Z -> option Z) + (value_range flag_range : ZRange.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)) + : Interp_GoalT (RewriterToFancyWithCasts invert_low invert_high value_range flag_range). + Proof. prove_interp_good (). Qed. End RewriteRules. End Compilers. diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index d3d640dc0..d9e1f6293 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -35,6 +35,8 @@ Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.NatUtil. Require Crypto.Util.PrimitiveHList. Import Coq.Lists.List ListNotations. Local Open Scope list_scope. Local Open Scope Z_scope. @@ -3267,5 +3269,464 @@ Module Compilers. Qed. End with_interp. End Reify. + + Module Import WfTactics. + Module Export Settings. + Global Strategy -100 [rewrite_rules Compile.rewrite_rules_goodT_curried_cps]. + End Settings. + + Module Export GoalType. + Definition Wf_GoalT (Rewriter : RewriterT) : Prop + := forall var1 var2, + @Compile.rewrite_rules_goodT + ident pattern.ident (@pattern.ident.arg_types) var1 var2 + (Make.GoalType.rewrite_rules (Rewriter_data Rewriter) _) + (Make.GoalType.rewrite_rules (Rewriter_data Rewriter) _). + End GoalType. + + Ltac start_good _ := + cbv [Wf_GoalT]; intros; + match goal with + | [ |- @Compile.rewrite_rules_goodT ?ident ?pident ?pident_arg_types ?var1 ?var2 ?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 Make.GoalType.rewrite_rules ?data _ => data end in + let data' := (eval hnf in data) in + change data with data' in H; + cbv [Make.GoalType.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 + 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. + + 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 * ]. + + 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 ]. + + 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 ]. + + Ltac handle_extra_arith_rules := + 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 + end + | congruence + | progress fin_wf ]. + + + Module Export Tactic. + Export Settings. + + Ltac prove_good _ := + let do_time := Make.time_if_debug1 in (* eval the level early *) + do_time start_good; + do_time ltac:(fun _ => handle_reified_rewrite_rules; handle_extra_nbe; handle_extra_arith_rules). + End Tactic. + End WfTactics. + + Module InterpTactics. + Import Crypto.Util.ZRange. + + Module Export GoalType. + Local Notation specT rewriter_data + := (PrimitiveHList.hlist (@snd bool Prop) (List.skipn (dummy_count rewriter_data) (rewrite_rules_specs rewriter_data))) + (only parsing). + + Local Notation rewrite_rules_interp_goodT cast_outside_of_range + := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident.gen_interp cast_outside_of_range)). + + Local Notation "'plet' x := y 'in' z" + := (match y return _ with x => z end). + + Definition Interp_GoalT (Rewriter : RewriterT) : Prop + := forall (cast_outside_of_range : zrange -> Z -> Z), + plet data := Rewriter_data Rewriter in + specT data + -> rewrite_rules_interp_goodT cast_outside_of_range (Make.GoalType.rewrite_rules data _). + End GoalType. + + (** Coq >= 8.9 is much better at [eapply] than Coq <= Coq 8.8 *) + Ltac cbv_type_for_Coq88 T := + lazymatch eval hnf in T with + | @eq ?T ?A ?B => let A' := (eval cbv [ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.list_rect ident.Thunked.nat_rect ident.Thunked.option_rect] in A) in + constr:(@eq T A' B) + | forall x : ?A, ?P + => let P' := fresh in + constr:(forall x : A, + match P return Prop with + | P' + => ltac:(let v := cbv_type_for_Coq88 P' in + exact v) + end) + end. + Ltac cbv_for_Coq88_in H := + cbv [ident.Thunked.bool_rect ident.Thunked.list_case ident.Thunked.list_rect ident.Thunked.nat_rect ident.Thunked.option_rect]; + let T := type of H in + let T := cbv_type_for_Coq88 T in + change T in H. + + Ltac start_interp_good _ := + cbv [List.skipn Interp_GoalT] in *; intros; + lazymatch goal with + | [ |- @Compile.rewrite_rules_interp_goodT ?ident ?pident ?pident_arg_types ?pident_to_typed ?ident_interp (Make.GoalType.rewrite_rules ?data ?var) ] + => let H := fresh in + pose proof (@Compile.rewrite_rules_interp_goodT_by_curried + _ _ _ pident_to_typed ident_interp (Make.GoalType.rewrite_rules data var) (rewrite_rules_specs data)) as H; + let data' := (eval hnf in data) in + change data with data' in * |- ; + cbv [Make.GoalType.rewrite_rules dummy_count rewrite_rules_specs] 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; + [ 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; + cbv_for_Coq88_in H; + 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 := + ((tryif is_evar v then fail else idtac); + let v' := open_constr:(_) in + let v'' := fresh in + cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in + match goal with + | _ => progress cbv [expr.interp_related] in * + | _ => progress cbn [Compile.reify_expr] + | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand + | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand + | [ |- expr.interp_related_gen ?ident_interp ?R ?f ?v ] + => do_replace v + | [ |- 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; + first [ do_replace x + | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ] + | _ => progress intros + | [ |- expr.interp_related_gen _ _ _ ?ev ] => is_evar ev; eassumption + | [ |- expr.interp_related_gen _ _ (?f @ ?x) ?ev ] + => is_evar ev; + let fh := fresh in + let xh := fresh in + set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh; + do 2 eexists; repeat apply conj; [ | | reflexivity ] + | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ] + => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh + | [ |- expr.interp_related_gen _ _ (expr.Ident ?idc) ?ev ] + => is_evar ev; + cbn [expr.interp_related_gen]; apply ident.gen_interp_Proper; reflexivity + | [ |- _ = _ :> ?T ] + => lazymatch T with + | BinInt.Z => idtac + | (BinInt.Z * BinInt.Z)%type => idtac + end; + progress cbn [ident.gen_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? *) + 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_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. + Ltac recursive_match_to_case_in_goal := + let G := match goal with |- ?G => G end in + let G := recursive_match_to_case G in + change G. + + 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 + | match goal with + | [ |- 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 ]. + Ltac preprocess := repeat preprocess_step. + Ltac handle_extra_nbe := + repeat match goal with + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (expr.Ident _)) _ ] + => cbn [UnderLets.interp_related UnderLets.interp_related_gen expr.interp_related_gen ident.gen_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.gen_interp type.related]; reflexivity + end. + 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 ]. + Ltac handle_reified_rewrite_rules_interp := + repeat first [ assumption + | match goal with + | [ cast_outside_of_range : zrange -> Z -> Z |- 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) + + | [ |- 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) + + | [ |- 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.gen_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 ] + | [ |- type.eqv _ _ ] => cbn [ident.gen_interp type.related]; cbv [respectful]; intros; subst + end + | progress repeat (do 2 eexists; repeat apply conj; [ | | reflexivity ]) ]. + + Module Export Tactic. + Ltac prove_interp_good _ := + let do_time := Make.time_if_debug1 in (* eval the level early *) + do_time start_interp_good; + do_time ltac:(fun _ => preprocess; handle_extra_nbe; handle_reified_rewrite_rules_interp). + End Tactic. + End InterpTactics. + + Module GoalType. + Record VerifiedRewriter := + { + Rewriter : RewriterT; + RewriterRulesWf : WfTactics.GoalType.Wf_GoalT Rewriter; + RewriterRulesInterp : InterpTactics.GoalType.Interp_GoalT Rewriter; + Wf_Rewrite : forall {t} e (Hwf : Wf e), Wf (@Rewrite Rewriter t e); + Interp_gen_Rewrite + : forall {cast_outside_of_range t} e (Hwf : Wf e), + expr.Interp (@ident.gen_interp cast_outside_of_range) (@Rewrite Rewriter t e) + == expr.Interp (@ident.gen_interp cast_outside_of_range) e; + Interp_Rewrite + : forall {t} e (Hwf : Wf e), Interp (@Rewrite Rewriter t e) == Interp e + }. + End GoalType. End RewriteRules. End Compilers. |