From a86a5b99836b8455973fe7e4d4ff7e0fd72b3e75 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 25 Jul 2018 17:48:55 -0400 Subject: Add invert_LetIn --- src/Experiments/NewPipeline/Language.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index b3a7ea235..6ef9ed5d8 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -1291,6 +1291,12 @@ Module Compilers. | expr.Abs s d f => Some f | _ => None end. + Definition invert_LetIn {t} (e : expr t) + : option { s : _ & expr s * (var s -> expr t) }%type + := match e with + | expr.LetIn A B x f => Some (existT _ A (x, f)) + | _ => None + end. Definition invert_App2 {t} (e : expr t) : option { ss' : _ & expr (fst ss' -> snd ss' -> t) * expr (fst ss') * expr (snd ss') }%type := (e <- invert_App e; -- cgit v1.2.3