This has been processed with:

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

Starting with natural numbers, we define standard lists by ornamentations, but also two variants of lists: lists with a duplicated constructor and lists that may or may not contain an element at each position. Namely, here are all the datatypes we are interested in:

type nat = | Z | S of nat |

type 'a list = | Nil | Cons of 'a * 'a list type 'a bilist = | Nil0 | Cons1 of 'a * 'a bilist | Cons2 of 'a * 'a bilist type 'a maybelist = | NilM | ConsNone of 'a maybelist | ConsSome of 'a * 'a maybelist |

We define a few functions operating on integers:

let id = fun x -> x let zero = Z let rec add m n = match m with | Z -> n | S m' -> S(add m' n) |

We can then obtain the operations on standard lists by lifting those on integers: the identity function can be lifted without any patch or extra information; a value (like nil) can be lifted by simply giving the target type

type ornament 'a natlist : nat => 'a list with | Z => Nil | S n => Cons (_, n) when n : 'a natlist let id2 = lifting id let nil = lifting zero : _ natlist |

let id2 x = x let nil = Nil |

The concatenation on lists need more information. If we only specify, the expected type

let _append = lifting add : _ natlist -> _ natlist -> _ natlist |

we get this incomplete scheleton

let rec _append m n = match m with | Nil -> n | Cons(_, m') -> Cons(#2, _append m' n) |

We can then provide the missing information as a patch:

let append = lifting add : _ natlist -> _ natlist -> _ natlist with | #2 <- match m with Cons(a,_) -> a |

and we get the expected code:

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

Notice that this is exactly the code that we could have manually written, up to the choice of identifiers.

let rec append ml nl = match ml with | Nil -> nl | Cons(a,ml') -> Cons(a, append ml' nl) |

We may also lift `add`

—doing nothing, which we call the identity
lifting. This can be specified, as follows:

let add2 = lifting add with | ornament * <- @id |

The pattern `| * <- `

`@id`

means that any unspecified ornament
will default to the identity. We just get another copy of `add`

:

let rec add2 m n = match m with | Z -> n | S m' -> S (add2 m' n) |

Lists with two constructors are an ornament of lists with one
constructor, having a choice between `Cons1`

and
`Cons2`

:

type ornament 'a listbilist : 'a list => 'a bilist with | Nil => Nil0 | Cons(a,l) => (Cons1(a,l) | Cons2(a,l)) when l : 'a listbilist |

We can also lift lists at this type (here we choose to specify patching points rather than an ornament signature).

let append2 = lifting append with | ornament * <- listbilist | #2 <-match ml with Cons1(_,_) -> Left(()) | Cons2(_,_) -> Right(()) |

We get

let rec append2 ml nl = match ml with | Nil0 -> nl | Cons1(a, ml') -> Cons1(a, append2 ml' nl) | Cons2(a, ml') -> Cons2(a, append2 ml' nl) |

The unit type (represented as `()`

for syntactic reasons) is also
an ornament of `nat`

. The pattern `S`

`(`

`_`

`)`

is mapped to
the empty pattern `~`

.

type ornament natunit : nat => () with | Z => () | S(n) => ~ when n : natunit |

The type `maybelist`

is also an ornament of `nat`

type ornament 'a natmaybelist : nat => 'a maybelist with | Z => NilM | S(x) => (ConsNone(x) | ConsSome(_,x)) when x : 'a natmaybelist |

We may also lift `add`

at both of these types

let add0 = lifting add with | ornament * <- natunit let addmaybe = lifting add with | ornament * <- natmaybelist | #2 <- match m with ConsNone(_) -> Left(()) | ConsSome(a,_) -> Right(a) |

let add0 m n = match m with | () -> n let rec addmaybe m n = match m with | NilM -> n | ConsNone m' -> ConsNone (addmaybe m' n) | ConsSome(a, m') -> ConsSome(a, addmaybe m' n) |

type bool = | True | False |

let rec equal_nat m n = match (m, n) with | (Z, Z) -> True | (S m', S n') -> equal_nat m' n' | _ -> False |

let equal_length = lifting equal_nat : _ natlist -> _ natlist -> bool with | ornament * <- @id |

let rec equal_length m n = match m with | Nil -> begin match n with | Nil -> True | Cons(_, _) -> False end | Cons(_, n1) -> begin match n with | Nil -> False | Cons(_, n) -> equal_length n1 n end |