Merge branch 'improve-dead-elim' into 'dev'

Improve purity test for dead code elimination

See merge request ligolang/ligo!193
This commit is contained in:
Gabriel Alfour 2019-11-14 14:31:29 +00:00
commit 533cbaa1b5
2 changed files with 57 additions and 10 deletions

View File

@ -1,14 +1,62 @@
open Mini_c open Mini_c
open Trace open Trace
(* Overly conservative for now: ok to treat pure things as impure, (* Overly conservative purity test: ok to treat pure things as impure,
must not treat impure things as pure. *) must not treat impure things as pure. *)
let is_pure : expression -> bool = fun e ->
match e.content with (* true if the name names a pure constant -- i.e. if uses will be pure
| E_closure _ -> true assuming arguments are pure *)
let is_pure_constant : string -> bool =
function
| "CAR"
| "CDR"
| "PAIR"
-> true
(* TODO... *)
| _ -> false | _ -> false
let rec elim_dead_lambdas : expression -> expression result = fun e -> let rec is_pure : expression -> bool = fun e ->
match e.content with
| E_literal _
| E_closure _
| E_skip
| E_variable _
| E_make_empty_map _
| E_make_empty_list _
| E_make_empty_set _
| E_make_none _
-> true
| E_if_bool (cond, bt, bf)
| E_if_none (cond, bt, (_, bf))
| E_if_cons (cond, bt, (_, bf))
| E_if_left (cond, (_, bt), (_, bf))
-> List.for_all is_pure [ cond ; bt ; bf ]
| E_let_in (_, e1, e2)
| E_sequence (e1, e2)
-> List.for_all is_pure [ e1 ; e2 ]
| E_constant (c, args)
-> is_pure_constant c && List.for_all is_pure args
(* I'm not sure about these. Maybe can be tested better? *)
| E_application _
| E_iterator _
| E_fold _
-> false
(* Could be pure, but, divergence is an effect, so halting problem
is near... *)
| E_while _ -> false
(* definitely not pure *)
| E_assignment _ -> false
(* Eliminate dead `let` with pure rhs *)
let rec elim_dead_code : expression -> expression result = fun e ->
let changed = ref false in (* ugh *) let changed = ref false in (* ugh *)
let mapper : Helpers.mapper = fun e -> let mapper : Helpers.mapper = fun e ->
match e.content with match e.content with
@ -22,8 +70,8 @@ let rec elim_dead_lambdas : expression -> expression result = fun e ->
| _ -> ok e in | _ -> ok e in
let%bind e = Helpers.map_expression mapper e in let%bind e = Helpers.map_expression mapper e in
if !changed if !changed
then elim_dead_lambdas e then elim_dead_code e
else ok e else ok e
let all_expression : expression -> expression result = let all_expression : expression -> expression result =
elim_dead_lambdas elim_dead_code

View File

@ -75,9 +75,8 @@ module Free_variables = struct
expression (union (singleton v) b) body ; expression (union (singleton v) b) body ;
] ]
| E_sequence (x, y) -> union (self x) (self y) | E_sequence (x, y) -> union (self x) (self y)
(* we do not consider the assigned variable free... seems strange, (* NB different from ast_typed... *)
but, matches ast_typed, and does not cause any troubles? *) | E_assignment (v, _, e) -> unions [ var_name b v ; self e ]
| E_assignment (_, _, e) -> self e
| E_while (cond , body) -> union (self cond) (self body) | E_while (cond , body) -> union (self cond) (self body)
and var_name : bindings -> var_name -> bindings = fun b n -> and var_name : bindings -> var_name -> bindings = fun b n ->