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/RewriterWf1.v | |
parent | 7b6cc09fa0273b1eed867bd11583f7b46be5b4e2 (diff) |
Automate more of the rewriter, and factor out rule-specific things
Diffstat (limited to 'src/RewriterWf1.v')
-rw-r--r-- | src/RewriterWf1.v | 461 |
1 files changed, 461 insertions, 0 deletions
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. |