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.
To compile the prototype, you need the following dependencies. The easiest way to install them is to use the OPAM package manager for OCaml ().
opam update && opam switch 4.05.0
to install the latest version.
ocamlfind, pprint, and menhir (install using
opam install ocamlfind pprint menhir)
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).
The input language is a small subset of OCaml. There are a few notable absences:
function does not exist
bool are
True and False
To load and typecheck a file, type:
src/ocamlorn --library src/tests/stdlib.mli --input INPUT_FILE.ml.
As a running example, we will consider the following input, defining natural
numbers (available as doc/tutorial.in.ml) 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 |
The ornamentation is specified in a lifting file, here
doc/tutorial.lif.ml.
To apply a lifting file to an input, use the following command:
src/ocamlorn --library examples/stdlib.mli --input INPUT_FILE.in.ml --lifting LIFTING_FILE.lif.ml.
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) |
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).
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 |
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.