From c5da702d478710e34d7cbace3a766caf775de4f4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Mar 2019 23:13:33 -0500 Subject: Fix an issue with a proof from the previous commit Also move lam_type_of_list to Rewriter (in prep for reifying rewrite rules). --- src/Rewriter.v | 7 +++++++ src/RewriterWf1.v | 8 +------- 2 files changed, 8 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/Rewriter.v b/src/Rewriter.v index e23b65ae7..06f8d59fe 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -506,6 +506,13 @@ Module Compilers. ls f args. + Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls + := list_rect + (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls) + (fun f => f tt) + (fun T Ts rec k t => rec (fun ts => k (t, ts))) + ls. + Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope. Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope. diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 0ec6396f2..49af85a60 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -65,6 +65,7 @@ Module Compilers. Proof using Type. revert t; induction pt; repeat first [ progress cbn [pattern.base.subst pattern.base.subst_default] + | progress cbv [pattern.base.lookup_default] | progress cbv [Option.bind option_map] | progress inversion_option | progress subst @@ -895,13 +896,6 @@ Module Compilers. Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types). Local Notation unification_resultT := (@unification_resultT pident pident_arg_types). - Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls - := list_rect - (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls) - (fun f => f tt) - (fun T Ts rec k t => rec (fun ts => k (t, ts))) - ls. - Lemma app_lam_type_of_list {K ls f args} : @app_type_of_list K ls (@lam_type_of_list ls K f) args = f args. -- cgit v1.2.3