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) |