Top

This file has been processed with:

ocamlorn --library stdlib.mli \ --library deadcode_elimination.in.ml --input deadcode_elimination.in.ml --lifting deadcode_elimination.lif.ml \ > deadcode_elimination.out.ml

Dead code elimination

During desornamentation, dead code (for instance used to compute data that is not present anymore) must be eliminated.

Lists to nat

Let us take back the disornamentation of lists to nat, and in particular the map_list function.

type nat = | Z | S of nat
type 'a list = | Nil | Cons of 'a * 'a list
type relation 'a natlist : nat => 'a list with | Z => Nil | S xs => Cons(_,xs) when xs : 'a natlist
let rec map_list f n = match n with | Nil -> Nil | Cons(x, n') -> Cons(f x, map_list f n')

When dead code elimination is disabled, as a result, the lifting of this function along the reversed relation is:

(mode keepdeadcode) let copy = lifting map_list: (_ rev_natlist -> _ rev_natlist) -> _ rev_natlist -> _ rev_natlist
let rec copy f n = match n with | Z -> Z | S n' -> let xs = copy f n' in let x = f #8 in S xs

Indeed, when this code is put in normal form, a variable is introduced to store f #7, and there is no reason for it to be removed.

This is fixed when dead code elimination is enabled:

(mode elimdeadcode) let copy = lifting map_list: (_ rev_natlist -> _ rev_natlist) -> _ rev_natlist -> _ rev_natlist
let rec copy f n = match n with | Z -> Z | S n' -> S (copy f n')

However, dead-code elimination is not enabled on code that was dead before the transformation:

let rec map_list2 f n = match n with | Nil -> Nil | Cons(x, n') -> let g = f x in Cons(f x, map_list2 f n')
let copy2 = lifting map_list2: (_ rev_natlist -> _ rev_natlist) -> _ rev_natlist -> _ rev_natlist
let rec copy2 f n = match n with | Z -> Z | S n' -> let g = f #8 in S (copy2 f n')

Balanced tree creation

Let’s take sets, implemented with balanced tree.

type t = Empty | Node of t * elt * t * int let create l vb r = match vb with | Box v -> let hl = match l with Empty -> i0 | Node(_,_,_,h) -> h in let hr = match r with Empty -> i0 | Node(_,_,_,h) -> h in Node(l, v, r, (match gte hl hr with True -> plus hl i1 | False -> plus hr i1))

We may want to see a simplified version of the code by removing the balancing information. This can be done with the following desornament.

type simplt = | SEmpty | SNode of simplt * elt * simplt
type ornament simplification: t => simplt with | Empty => SEmpty | Node(l, v, r, _) => SNode(l, v, r) when l r: simplification

Then, let’s lift the create function along this transformation.

(mode keepdeadcode) let screate = lifting create: simplification -> elt box -> simplification -> simplification
let screate l vb r = match vb with | Box v -> let hl = match l with | SEmpty -> i0 | SNode(_, _, _) -> #18 in let hr = match r with | SEmpty -> i0 | SNode(_, _, _) -> #15 in let x = match gte hl hr with | True -> plus hl i1 | False -> plus hr i1 in SNode(l, v, r)

However, hl, hr and x are not needed. Thus, dead code elimination erases them:

(mode elimdeadcode) let screate = lifting create: simplification -> elt box -> simplification -> simplification
let screate l vb r = match vb with | Box v -> SNode(l, v, r)