From 8256bfbdc7dedffe64db2049f25756b453b14130 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Oct 2022 22:32:39 +0530 Subject: [PATCH] Use to_expr_App instead of to_expr so that reduction works correctly (#79) --- src/Rewriter/Language/UnderLets.v | 8 +++++++- src/Rewriter/Language/UnderLetsCacheProofs.v | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Rewriter/Language/UnderLets.v b/src/Rewriter/Language/UnderLets.v index 0419c80ef..8dd7f8f89 100644 --- a/src/Rewriter/Language/UnderLets.v +++ b/src/Rewriter/Language/UnderLets.v @@ -107,6 +107,12 @@ Module Compilers. | UnderLet A x f => expr.LetIn x (fun v => @to_expr _ (f v)) end. + Fixpoint to_expr_App {t} (x : @UnderLets (expr t)) : expr t + := match x with + | Base v => v + | UnderLet A x f + => expr.App (expr.Abs (fun v => @to_expr_App _ (f v))) x + end. Fixpoint of_expr {t} (x : expr t) : @UnderLets (expr t) := match x in expr.expr t return @UnderLets (expr t) with | expr.LetIn A B x f @@ -263,5 +269,5 @@ Module Compilers. End reify. End UnderLets. Export UnderLets.Notations. - Global Strategy -1000 [UnderLets.to_expr]. + Global Strategy -1000 [UnderLets.to_expr UnderLets.to_expr_App]. End Compilers. diff --git a/src/Rewriter/Language/UnderLetsCacheProofs.v b/src/Rewriter/Language/UnderLetsCacheProofs.v index 717d30185..efb7d9b7c 100644 --- a/src/Rewriter/Language/UnderLetsCacheProofs.v +++ b/src/Rewriter/Language/UnderLetsCacheProofs.v @@ -43,7 +43,7 @@ Module Compilers. (fun t e v => expr.interp ident_interp e = v) (fun e v => expr.interp ident_interp e = v) v - (expr.interp ident_interp (UnderLets.to_expr e) = v) + (expr.interp ident_interp (UnderLets.to_expr_App e) = v) e. Lemma cached_interp_related_impl {t} e v