This tutorial intends to give an overview of the usage of our prototype ornamentation tools. The concepts introduced here are explored in more details in the examples.

1  Getting started

To compile the prototype, you need the following dependencies. The easiest way to install them is to use the OPAM package manager for OCaml ().

In the root directory of the archive, type

    make ocamlorn

The prototype is then compiled as src/ocamlorn.

To process all the examples in the ./doc/ directory, but without generating the html files, type

    make examples

If you wish to reproduce the html files as well, you need hevea install, which you can do with opam:

    opam install hevea

Then, type

    make doc 

This will regenerate all files in ./doc/html/ (including this one).

2  The input language

The input language is a small subset of OCaml. There are a few notable absences:

To load and typecheck a file, type: src/ocamlorn --library src/tests/stdlib.mli --input

As a running example, we will consider the following input, defining natural numbers (available as doc/ and a few functions:

type nat = | Z | S of nat let zero = Z let one = S (Z) let two = S (S Z) let three = S (S (S Z)) let rec add m n = match m with | Z -> n | S m' -> S (add m' n) let double n = add n n

3  Defining ornaments and lifting functions

The ornamentation is specified in a lifting file, here doc/ To apply a lifting file to an input, use the following command: src/ocamlorn --library examples/stdlib.mli --input --lifting The result of the lifting commands is printed on the standard output.

Before defining an ornament from one type to another, we have to define the ornamented type:

type 'a list = | Nil | Cons of 'a * 'a list

Once we have defined some types, we can define ornaments. Ornaments are introduced by the type ornament keywords. They can take some type parameters, and always relate a datatype (or tuples) to a type. the ornament 'a natlist taking natural numbers to lists:

type ornament 'a natlist : nat => 'a list with | Z => Nil | S(xs) => Cons(_,xs) when xs : 'a natlist

We introduce a list of ornamentation clauses with the keyword with (as with pattern matching). Ornamentation clauses are indicated with =>. When part of a type must be ornamented recursively, this is indicated with a when clause after the corresponding ornamentation clause. To help the name generation algorithm, the names given in the ornament should be name that make sense for the destination type rather than the source type. More details on ornament definitions are given in the next sections.

We can then ask for a lifting for a lifting append of add using the following notation:

let _append = lifting add : 'a natlist -> 'a natlist -> 'a natlist

The signature 'a natlist -> 'a natlist -> 'a natlist indicates at which ornaments the arguments and result must be lifted.

We get the following output:

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

The lifting is incomplete, the lifting has a hole noted #2: we must insert a corresponding patch in the definition. We have used the name _append to tell the ornamentation tool that this is expected. Otherwise, the tool would have quit with an error, after printing the incomplete lifting.

When writing the patch, we have in scope all the variables that were in scope in the original term at this point in the program: thus, to obtain the head of m, we need to pattern-match on it again. We ask for a lifting again, giving the patch after the keyword with:

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

We get the following output:

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

Notice that the extra pattern matching has been simplified away, revealing that it was in fact complete.

We can also copy the definition of add by asking for its lifting at the identity ornament. The identity ornament is noted the same as the base type it ornaments:

let add = lifting add : nat -> nat -> nat

In this case, we do not need a patch, because there is no information added:

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

4  More on patches and incomplete definitions

Let us ask for a lifting of add without any additional information.

let _add = lifting add

We obtain the following output:

let rec _add m n = match (orn-match #4) m with | Z_skel -> n | S_skel m' -> (orn-cons #1) (S_skel (_add m' n)) #2

The lifting has the structure of add but is missing a lot of information: the hole corresponding to the patch #2 is still present, but there are two new holes #1 and #3. They both correspond to ornaments: (orn-match #3) indicates that we need to specify an ornament #3 of nat to translate the pattern matching, and #1 indicates taht we need to specify an ornament #1 to build the return value. These ornaments can be specified using the ornament keyword instead of a signature:

let append2 = lifting add with | ornament #1, #4 <- natlist | #2 <- (match m with Cons(x,_) -> x)
let rec append2 m n = match m with | Nil -> n | Cons(x, m') -> Cons(x, append2 m' n)

Let us now consider the double function, and lift it without any indications.

let _double = lifting double

We obtain the following output:

let _double n = (lifting #3 of add) n n

The ambiguity in this case comes from the fact that there are multiple liftings of add that can be used (add, append, append2). We can specify which lifting to use with the keyword lifting:

let double_list = lifting double with | lifting #3 <- append
let double_list n = append n n

Or with an appropriate specification:

let double = lifting double : nat -> nat
let double n = add n n

One can specify multiple ornaments or lifting at once using the syntaxes ornament * <- (list) and lifting * <- (list). Then, at each hole, the first possible ornament or lifting in the list is used (if it would not conflict with another defintion).

5  Advanced ornaments

In a ornament definitions, the patterns on the left-hand side must form a partition of the base type, and the patterns on the right-hand side a partition of the ornamented type. If they are incomplete, or overlap, an error message is produced.

There is a second condition on variables: the same variables must appear on the left-hand side and the right-hand side of the pattern. If a when clause is given, they have, on the left-hand side, the base type of the ornament given for them, and the ornamented type on the right-hand side. Otherwise, the identity ornament is used and the types are the same. Thus, all these clauses are incorrect:

| S xs => Cons(_, xs) (* xs must be both a nat and a list *) | S xs => Cons(x, xs) (* x is not present on the left *) | S xs => Cons(xs, xs) (* xs is present twice on the right *)

The pattern on the left must be simple: they can only have variables and constructors. On the right, one can use wildcards _ for new data, or-patterns to denote multiple possible liftings, and the empty pattern noted ~.

For example, this ornament lifts the Z case to two possible constructors True and False, while the S case has no lifting.

type bool = | False | True
type ornament natbool : nat => bool with | Z => (True | False) | S xs => ~

Then, we try to lift zero:

let _zero_bool = lifting zero : natbool

We are presented with a program with a hole #2:

let _zero_bool = match #2 with | Left _ -> True | Right _ -> False

If we put Left () in the hole, we obtain True, while if we put Right () we obtain false. In both case, the code would be simplified accordingly:

let true = lifting zero : natbool with | #2 <- Left ()
let true = True

Let us try to lift another number:

let _one_bool = lifting one : natbool
let _one_bool = <absurd>

The lifting is rejected: the S constructor has no possible liftings, but the branch indicated by <absurd> cannot be proved unreachable.

It is possible to write ornaments that match more than one level of constructor of the base datatype:

type nattwo = | Z01 | S0 of nattwo | S1 of nattwo
type ornament list_nattwo : bool list => nattwo with | Nil => Z01 | Cons(False, xs) => S0(xs) when xs : list_nattwo | Cons(True, xs) => S1(xs) when xs : list_nattwo

6  Non-regular ornaments

We can write ornaments that do not correspond to the recursive structure of the base datatype. For example, this ornament “divides by two”: the first ornament copies on successor and passes the tail to the second ornament, the second ornament skips one successor and passes the tail to the first.

type ornament natdiv_even : nat => nat with | Z => Z | S xs => S xs when xs : natdiv_odd and natdiv_odd : nat => nat with | Z => ~ | S xs => xs when xs : natdiv_even let one' = lifting two : natdiv_even
let one' = S Z

On the other hand, we cannot write a version of add that would double its first argument as we would hope:

let _add_twice = lifting add : natdiv_even -> nat -> nat

While the error message we get is unhelpful, the error is simple: add expects its first argument to be lifted with a single ornament, and here we must produce two mutually recursive versions that use different ornaments. The problem can be solved by unfolding add first:

let rec add_unfolded m n = match m with | Z -> n | S m' -> begin match m' with | Z -> S n | S m'' -> S (S (add_unfolded m'' n)) end
let add_twice = lifting add_unfolded : natdiv_even -> nat -> nat

We get the following result:

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

This can be done automatically by enabling both unfolding and autolifting, see for exampe unfolding for lists and unfolding for generic programming.