Top

This file has been processed with:

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

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 list2nat n = match n with | Nil -> Z | Cons(_, m) -> S (list2nat m)

We now declare an ornamentation relation which is the same as in the ornamentation of nat:

type ornament 'a natlist : nat => 'a list with | Z => Nil | S xs => Cons(_,xs) when xs : 'a natlist

We then use the reversed ornament rev_natlist to get back the original functions on nat:

let add = lifting append: _ rev_natlist -> _ rev_natlist -> _ let nat2int = lifting list_length: _ rev_natlist -> nat let copy = lifting list2nat: _ rev_natlist -> nat

And we get those functions.

let rec add m n = match m with | Z -> n | S m' -> S (add m' n) let rec nat2int n = match n with | Z -> Z | S m -> S (nat2int m) let rec copy n = match n with | Z -> Z | S m -> S (copy m)