Top

This has been processed with:

## Reentrance: ornamenting ornamented code

(see `tests``/``reload``.``ml`, run with `./``ocamlorn`` ``tests``/``reload``.``ml`)

This example shows that lifted code can be lifted again.

Assume we have written addition on natural numbers

 type nat = | Z | S of nat
 let rec add m n = match m with | Z -> n | S m' -> S (add m' n)

As before, we may defined append from natural numbers.

 type 'a list = | Nil | Cons of 'a * 'a list
 type ornament 'a natlist : nat => 'a list with | Z => Nil | S xs => Cons(_,xs) when xs : 'a natlist let append = lifting add : _ natlist -> _ natlist -> _ natlist with #2 <- (match m with Cons(x,_) -> x)

We get the `append` function, as expected

 let rec append m n = match m with | Nil -> n | Cons(x, m') -> Cons(x, append m' n)

We may again ornament append that has been obtained by the lifting of `add`. For example, we may defined a special version of lists with two `Cons` constructors as follows:

 type 'a list01 = | Nil01 | Cons0 of 'a list01 | Cons1 of 'a * 'a list01
 type ornament 'a boollist01 : bool list => 'a list01 with | Nil => Nil01 | Cons(False,xs) => Cons0(xs) when xs : 'a boollist01 | Cons(True,xs) => Cons1(_,xs) when xs : 'a boollist01

We may then lift `append` to these specials lists as follows:

 let append01 = lifting append : _ boollist01 -> _ boollist01 -> _ boollist01 with #2 <- (match m with Cons1(x,_) -> x)

We obtain the expected function:

 let rec append01 m n = match m with | Nil01 -> n | Cons0 m' -> Cons0 (append01 m' n) | Cons1(x, m') -> Cons1(x, append01 m' n)