From cd99d56d2e5dbf8d11d8f4836653f966d6d7a907 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 18 Sep 2016 23:38:33 -0400 Subject: Add dead code elimination --- src/Reflection/Named/Compile.v | 23 ++++++---- src/Reflection/Named/DeadCodeElimination.v | 71 ++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+), 9 deletions(-) create mode 100644 src/Reflection/Named/DeadCodeElimination.v (limited to 'src') 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. -- cgit v1.2.3