From 6baa8cd0d789492e1d6a3eaaa8a1bb4ea0ad379e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 27 Nov 2018 19:17:13 -0500 Subject: Add reveal_rawexpr_equiv --- src/Experiments/NewPipeline/RewriterWf1.v | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index ac12b8585..09d5f5a29 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -786,7 +786,9 @@ Module Compilers. => rawexpr_equiv_expr f' f /\ rawexpr_equiv_expr x' x | _ => False end - | rExpr t e => e === e1 + | rExpr t e + | rValue (type.base t) e + => e === e1 | rValue t e => False end. @@ -796,6 +798,8 @@ Module Compilers. := match r1, r2 with | rExpr t e, r | r, rExpr t e + | rValue (type.base t) e, r + | r, rValue (type.base t) e => rawexpr_equiv_expr e r | rValue t1 e1, rValue t2 e2 => existT _ t1 e1 = existT _ t2 e2 @@ -926,7 +930,7 @@ Module Compilers. : @rawexpr_equiv_expr t e re -> t = type_of_rawexpr re. Proof using Type. destruct re; cbn [rawexpr_equiv_expr]; - intros; destruct_head'_and; inversion_sigma; + intros; break_innermost_match_hyps; destruct_head'_and; inversion_sigma; repeat (subst || cbn [eq_rect type_of_rawexpr] in * ); solve [ reflexivity | exfalso; assumption ]. Qed. @@ -1150,6 +1154,18 @@ Module Compilers. : @reveal_rawexpr_cps ident var e T k = k (reveal_rawexpr e). Proof. apply reveal_rawexpr_cps_gen_id. Qed. + Lemma reveal_rawexpr_equiv e + : rawexpr_equiv (reveal_rawexpr e) e. + Proof using Type. + cbv [reveal_rawexpr_cps]; induction e. + all: repeat first [ progress cbn [rawexpr_equiv reveal_rawexpr_cps_gen value'] in * + | progress cbv [id value] in * + | break_innermost_match_step + | progress expr.invert_match + | reflexivity + | apply conj ]. + Qed. + Fixpoint eval_decision_tree_cont_None_ext {T ctx d cont} (Hcont : forall x y, cont x y = None) -- cgit v1.2.3