Add dead code elimination

2 files changed, 85 insertions, 9 deletions

diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v
index b6b4f7b3c..e37815597 100644
--- a/src/Reflection/Named/Compile.v
+++ b/src/Reflection/Named/Compile.v
@@ -25,36 +25,41 @@ Section language.
   Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name).
   Local Notation nexpr := (@Named.expr base_type_code interp_base_type op Name).
 
-  Fixpoint compilef {t} (e : exprf t) (ls : list Name) {struct e}
+  Fixpoint ocompilef {t} (e : exprf t) (ls : list (option Name)) {struct e}
     : option (nexprf t)
     := match e in @Syntax.exprf _ _ _ _ t return option (nexprf t) with
        | Const _ x => Some (Named.Const x)
        | Var _ x => Some (Named.Var x)
-       | Op _ _ op args => option_map (Named.Op op) (@compilef _ args ls)
+       | Op _ _ op args => option_map (Named.Op op) (@ocompilef _ args ls)
        | LetIn tx ex _ eC
-         => match @compilef _ ex nil, split_names tx ls with
+         => match @ocompilef _ ex nil, split_onames tx ls with
             | Some x, (Some n, ls')%core
-              => option_map (fun C => Named.LetIn tx n x C) (@compilef _ (eC n) ls')
+              => option_map (fun C => Named.LetIn tx n x C) (@ocompilef _ (eC n) ls')
             | _, _ => None
             end
-       | Pair _ ex _ ey => match @compilef _ ex nil, @compilef _ ey nil with
+       | Pair _ ex _ ey => match @ocompilef _ ex nil, @ocompilef _ ey nil with
                            | Some x, Some y => Some (Named.Pair x y)
                            | _, _ => None
                            end
        end.
 
-  Fixpoint compile {t} (e : expr t) (ls : list Name) {struct e}
+  Fixpoint ocompile {t} (e : expr t) (ls : list (option Name)) {struct e}
     : option (nexpr t)
     := match e in @Syntax.expr _ _ _ _ t return option (nexpr t) with
-       | Return _ x => option_map Named.Return (compilef x ls)
+       | Return _ x => option_map Named.Return (ocompilef x ls)
        | Abs _ _ f
          => match ls with
-            | cons n ls'
-              => option_map (Named.Abs n) (@compile _ (f n) ls')
+            | cons (Some n) ls'
+              => option_map (Named.Abs n) (@ocompile _ (f n) ls')
             | _ => None
             end
        end.
+
+  Definition compilef {t} (e : exprf t) (ls : list Name) := @ocompilef t e (List.map (@Some _) ls).
+  Definition compile {t} (e : expr t) (ls : list Name) := @ocompile t e (List.map (@Some _) ls).
 End language.
 
+Global Arguments ocompilef {_ _ _ _ _} e ls.
+Global Arguments ocompile {_ _ _ _ _} e ls.
 Global Arguments compilef {_ _ _ _ _} e ls.
 Global Arguments compile {_ _ _ _ _} e ls.
diff --git a/src/Reflection/Named/DeadCodeElimination.v b/src/Reflection/Named/DeadCodeElimination.v
new file mode 100644
index 000000000..f7bbed46b
--- /dev/null
+++ b/src/Reflection/Named/DeadCodeElimination.v
@@ -0,0 +1,71 @@
+(** * PHOAS → Named Representation of Gallina *)
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.Compile.
+Require Import Crypto.Reflection.FilterLive.
+Require Import Crypto.Reflection.Syntax.
+
+Local Notation eta x := (fst x, snd x).
+
+Local Open Scope ctype_scope.
+Local Open Scope nexpr_scope.
+Local Open Scope expr_scope.
+Section language.
+  Context (base_type_code : Type)
+          (interp_base_type : base_type_code -> Type)
+          (op : flat_type base_type_code -> flat_type base_type_code -> Type)
+          (Name : Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Local Notation interp_type := (interp_type interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation exprf := (@exprf base_type_code interp_base_type op (fun _ => Name)).
+  Local Notation expr := (@expr base_type_code interp_base_type op (fun _ => Name)).
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+  Local Notation lexprf := (@Syntax.exprf base_type_code interp_base_type op (fun _ => list (option Name))).
+  Local Notation lexpr := (@Syntax.expr base_type_code interp_base_type op (fun _ => list (option Name))).
+  Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name).
+  Local Notation nexpr := (@Named.expr base_type_code interp_base_type op Name).
+
+  Definition get_live_namesf (names : list Name) {t} (e : lexprf t) : list (option Name)
+    := filter_live_namesf
+         base_type_code interp_base_type op
+         (option Name) None
+         (fun x y => match x, y with
+                     | Some x, _ => Some x
+                     | _, Some y => Some y
+                     | None, None => None
+                     end)
+         nil (List.map (@Some _) names) e.
+  Definition get_live_names (names : list Name) {t} (e : lexpr t) : list (option Name)
+    := filter_live_names
+         base_type_code interp_base_type op
+         (option Name) None
+         (fun x y => match x, y with
+                     | Some x, _ => Some x
+                     | _, Some y => Some y
+                     | None, None => None
+                     end)
+         nil (List.map (@Some _) names) e.
+
+  Definition compile_and_eliminate_dead_codef
+             {t} (e : exprf t) (e' : lexprf t) (ls : list Name)
+    : option (nexprf t)
+    := ocompilef e (get_live_namesf ls e').
+
+  Definition compile_and_eliminate_dead_code
+             {t} (e : expr t) (e' : lexpr t) (ls : list Name)
+    : option (nexpr t)
+    := ocompile e (get_live_names ls e').
+
+  Definition CompileAndEliminateDeadCode
+             {t} (e : Expr t) (ls : list Name)
+    : option (nexpr t)
+    := compile_and_eliminate_dead_code (e _) (e _) ls.
+End language.
+
+Global Arguments compile_and_eliminate_dead_codef {_ _ _ _ t} _ _ ls.
+Global Arguments compile_and_eliminate_dead_code {_ _ _ _ t} _ _ ls.
+Global Arguments CompileAndEliminateDeadCode {_ _ _ _ t} _ ls.