Top

This has been processed with:

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

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)