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