Top
This file has been processed with:
Desornamentation of lists to nat
Here is the definition of lists and a few functions that were obtained from
ornamentation of nat.
We are going to see that we can get those functions back via desornamentation, that is via ornamentation with the reversed ornaments.
| type nat = | Z
| S of nat |
| type 'a list =
| Nil
| Cons of 'a * 'a list |
| let rec append m n = match m with
| Nil -> n
| Cons(a, m') -> Cons(a, append m' n)
let rec list_length n = match n with
| Nil -> Z
| Cons(_, m) -> S (list_length m)
let rec map_list f n = match n with
| Nil -> Nil
| Cons(x, n') -> Cons(f x, map_list f n') |
We now declare an ornamentation relation which is the same as in the ornamentation of nat:
| type relation 'a natlist : nat => 'a list with
| Z => Nil
| S xs => Cons(_,xs) when xs : 'a natlist |
For every relation written, we automatically get the reversed relation. It can
be used by writing rev_ + the relation name. It is strictly
equivalent to writing another relation with the left and right patterns swapped.
Here, the reversed relation is rev_natlist and it is a disornament (because the
natlist relation is an ornament). Therefore, we can lift the functions
with this disornament to get back the original functions on nat:
| let add = lifting append: _ rev_natlist -> _ rev_natlist -> _
let copy = lifting list_length: _ rev_natlist -> nat
let map_nat = lifting map_list: _ -> _ rev_natlist -> _ rev_natlist |
| let rec add m n = match m with
| Z -> n
| S m' -> S (add m' n)
let rec copy n = match n with
| Z -> Z
| S m -> S (copy m)
let rec map_nat f n = match n with
| Z -> Z
| S n' -> S (map_nat f n') |