diff options
| -rw-r--r-- | src/Rewriter.v | 4 | ||||
| -rw-r--r-- | src/RewriterInterpProofs1.v | 10 |
2 files changed, 6 insertions, 8 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index b9b57ff43..5f10869b2 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -948,7 +948,7 @@ Module Compilers. Local Notation maybe_do_again := (maybe_do_again do_again). - Definition rewrite_with_rule {t} (defaulte : expr t) e' (pf : rewrite_ruleT) + Definition rewrite_with_rule {t} e' (pf : rewrite_ruleT) : option (UnderLets (expr t)) := let 'existT p f := pf in let should_do_again := rew_should_do_again f in @@ -980,7 +980,7 @@ Module Compilers. (fun k ctx => match ctx return option (UnderLets (expr (type_of_rawexpr e))) with | e'::nil - => (pf <- nth_error rews k; rewrite_with_rule defaulte e' pf)%option + => (pf <- nth_error rews k; rewrite_with_rule e' pf)%option | _ => None end);;; (UnderLets.Base defaulte))%option. diff --git a/src/RewriterInterpProofs1.v b/src/RewriterInterpProofs1.v index e59591f0c..611a6ca5b 100644 --- a/src/RewriterInterpProofs1.v +++ b/src/RewriterInterpProofs1.v @@ -326,7 +326,7 @@ Module Compilers. \/ exists n pf e', nth_error rew_rules n = Some pf /\ Some res - = rewrite_with_rule do_again (expr_of_rawexpr e) e' pf + = rewrite_with_rule do_again e' pf /\ rawexpr_equiv e e'. Proof using raw_pident_to_typed_invert_bind_args invert_bind_args_unknown_correct. subst res; cbv [eval_rewrite_rules]. @@ -1017,11 +1017,10 @@ Module Compilers. -> UnderLets_interp_related (do_again t e) v) (rewr : rewrite_ruleT) (Hrewr : rewrite_rule_data_interp_goodT (projT2 rewr)) - t e re v1 v2 + t re v1 v2 (Ht : t = type_of_rawexpr re) (Ht' : rawexpr_types_ok re (type_of_rawexpr re)) - (He : expr_interp_related e v2) - : @rewrite_with_rule do_again t e re rewr = Some v1 + : @rewrite_with_rule do_again t re rewr = Some v1 -> rawexpr_interp_related re (rew Ht in v2) -> UnderLets_interp_related v1 v2. Proof using pident_unify_to_typed pident_unify_unknown_correct. @@ -1123,11 +1122,10 @@ Module Compilers. | [ |- ?R (Option.sequence_return ?x ?y) _ ] => destruct x eqn:Hinterp end; cbn [Option.sequence_return UnderLets.interp]; [ | now apply expr_of_rawexpr_interp_related ]. - unshelve (eapply interp_rewrite_with_rule; [ | | | | eassumption | ]; try eassumption). + unshelve (eapply interp_rewrite_with_rule; [ | | | eassumption | ]; try eassumption). { apply eq_type_of_rawexpr_equiv; assumption. } { eapply Hrew_rules, nth_error_In; rewrite <- sigT_eta; eassumption. } { erewrite <- rawexpr_types_ok_iff_of_rawexpr_equiv, <- eq_type_of_rawexpr_equiv by eassumption; assumption. } - { apply expr_of_rawexpr_interp_related; assumption. } { apply rawexpr_interp_related_Proper_rawexpr_equiv; assumption. } Qed. |