diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-14 19:05:07 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-14 19:05:07 -0400 |
commit | b50c57557b9cb63e67a9a23c47cd318bdf067399 (patch) | |
tree | 8b9f16618a9b3b47b672482f3c337b9bddc46b70 /src/Compilers | |
parent | eb0f60f7fe94513be9c87e087d6c59c25c8b8cd0 (diff) |
Split off EliminateDeadCode
Diffstat (limited to 'src/Compilers')
-rw-r--r-- | src/Compilers/Named/DeadCodeElimination.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v index 19ccdf58f..22e823fd1 100644 --- a/src/Compilers/Named/DeadCodeElimination.v +++ b/src/Compilers/Named/DeadCodeElimination.v @@ -30,15 +30,21 @@ Section language. Local Notation nexprf := (@Named.exprf base_type_code op Name). Local Notation nexpr := (@Named.expr base_type_code op Name). + Definition EliminateDeadCode + {t} (e : @Named.expr base_type_code op _ t) (ls : list Name) + : option (nexpr t) + := Let_In (insert_dead_names (Context:=PositiveContext_nd) None e ls) (* help vm_compute by factoring this out *) + (fun names => register_reassign (InContext:=PositiveContext_nd) (ReverseContext:=Context) Pos.eqb empty empty e names). + Definition CompileAndEliminateDeadCode {t} (e : Expr t) (ls : list Name) : option (nexpr t) := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in match e with - | Some e => Let_In (insert_dead_names (Context:=PositiveContext_nd) None e ls) (* help vm_compute by factoring this out *) - (fun names => register_reassign (InContext:=PositiveContext_nd) (ReverseContext:=Context) Pos.eqb empty empty e names) + | Some e => EliminateDeadCode e ls | None => None end. End language. +Global Arguments EliminateDeadCode {_ _ _ _ t} e ls. Global Arguments CompileAndEliminateDeadCode {_ _ _ _ t} e ls. |