Top
This file has been processed with:
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) |