Ornaments in ML

The syntax used for ornamentation is explained in the tutorial. We recommend you start there.

Conventions for the examples

All listings with backgroup color are the input or output of automatic processing. We use color to render the processing mode.

#(mode library) (* Some library code, availaible for all other files. *)
#(mode input) (* Some input code *)
#(mode lifting) (* Type declarations for ornamented types: these are used to defined the lifting and will also be copied verbatim to the output, that's one we slighly distinguish them form the lifting declarations that come next *)
#(mode lifting) (* The lifting declarations, these will produce *)
(* This is the output code, but the type declarations, which are part of the lifting code, and that we do not repeat here. *)

Hence, to obtain the real output code one should add typing declarations of the lifting code in front of the printed output code.

For sake of completeness, for any file file.html, the library code, input code, lifting code, and output code can be found in files file.lib.ml, file.in.ml, file.lif.ml, and file.out.ml. The output code has been produced with the command

ocamlorn --library ../src/tests/stdlin.mli \ --library file.lib.ml --input $file.in.ml --lifting file.lif.ml \ > file.out.ml

While for convenience, we present examples linearly

The examples

You can look at transcripts corresponding the examples presented in the paper and some other examples that were not presented.

Some more information

Dependencies for the prototype:

To regenerate the examples, it is necessary to also install hevea (opam install hevea). Then, (re-)compile the documentation with make doc.

To use the prototype, compile it with

make ocamlorn

This will produce an executable ocamlorn in ./src. Then run examples with

.../pathto/ocamlorn input1.ml input2.ml ...

Some information on writing programs is written in the README file at the root of the project.

Ornamentation syntax

An ornament declaration is of the form:

type ornament ('a1, ..., 'an) my_ornament : from_type => to_type with | pat1 => pat1' | pat2 => pat2' when x1 x2 : ornx1x2, v3 : ornx3 | ...

where my_ornament is the name of the ornament we define, ('a1, ..., 'an) is a possibly empty list of parameters. It defines an ornament from the datatype from_type to to_type. The patterns pat1 are simple patterns (that are also expressions) and the pat1' are arbitrary patterns. Then when clauses are used to specify the ornaments to use recursively. They can be ommitted in the case of the identity ornament.


type ornament 'a listtrue_nat : bool list => nat with | Nil => () | Cons(True, xs) => S xs | Cons(False, xs) -> ~

A lifting declaration is of the form:

let new_declaration = lifting old_declaration : ornament_specification with ornament_and_patches

For example:

let append_fold = lifting add_fold : _ natlist -> _ natlist -> _ natlist with | ornament * <- onetwoopt | #2 <- (match z with Some2(x,_) -> x) | lifting * <- fold_list

The annotation ornament_specification is an optional ornament type (for example, _ natlist -> _ natlist -> _ natlist). It is unified with the result from elaboration to infer what ornaments must be used for the arguments and return types.

The ornament_and_patches part specifies a list of ornament, patches, and lifting that are used during instanciation. Each missing part has an identifier (#1, #2, ...) used to address it.

A list of positions can be given instead of a single position. Then, the ornament, patch or lifting will be applied at all these positions. One can also indicate a lifting or ornament for all positions with *. In this case, it is possible to indicate multiple liftings or ornaments. The first applicable lifting/ornament will be selected. These declarations are processed top-to-bottom, and the first applicable declaration is selected (thus, wildcard declarations should probably put at the end of the list).

Here is an example using these features:

let madd = lifting add : _ box2 -> _ setmap -> _ setmap with | ornament * <- setmap, box2, @id | #2, #11, #17 <- (match xb with Box(_,x) -> x)

Command-line flags, processing modes

The behavior of the prototype can be modified by a number of flags. They apply to all the code processed after the occurence of the flag. They can either be given on the command line (--the_flag) and apply to all the following files, or directly in the file, as #(mode the_flag).

Some flags influence the information displayed during lifting:

Flags can also be used to control what code is output, and what is added to the scope of the output code:

For example, a refactoring could be specified by: ocamlorn --library stdlib.mli --input expr.ml --lifting expr_to_expr'.oml, where stdlib.mli contains the definitions of the standard library (that need not be included in the output), expr.ml contains code using a datatype expr, and expr_to_expr'.oml defines a datatype expr', an ornament from expr to expr' and lifting declarations for all functions of expr.ml.