natlist_extended

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

More complex ornaments

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

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