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