The syntax used for ornamentation is explained in the tutorial. We recommend you start there.
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
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
You can look at transcripts corresponding the examples presented in the paper and some other examples that were not presented.
Dependencies for the prototype:
To regenerate the examples, it is necessary to also install hevea (
opam install hevea).
Then, (re-)compile the documentation with
To use the prototype, compile it with
This will produce an executable
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.
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 | ...|
my_ornament is the name of the ornament we define,
, ..., '
) is a possibly empty list of
parameters. It defines an ornament from the datatype
to_type. The patterns
pat1 are simple patterns (that are also expressions) and
' are arbitrary patterns. Then
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|
|let append_fold = lifting add_fold : _ natlist -> _ natlist -> _ natlist with | ornament * <- onetwoopt | #2 <- (match z with Some2(x,_) -> x) | lifting * <- fold_list|
ornament_specification is an optional ornament type (for example,
natlist). It is unified with the result from elaboration
to infer what ornaments must be used for the arguments and return types.
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.
ornament_namespecifies that the ornament
ornament_nameshould be used for
xx. The type parameters of the ornament are not specified. The identity ornament can be either written with the name of the type, or with the special identifier
varshould be used as the lifting of the function appearing at
an_expressionspecifies that the patch
an_expressionshould be used at
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
*. 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)|
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
Some flags influence the information displayed during lifting:
--noisy: when active, output the representation of the skeleton and the encoding and decoding functions.
--nonoisy: disables noisy mode (default).
--debug: displays some useful information during the ornamentation process. The debug flags also preserves internal exceptions and backtraces (but is very verbose).
--nodebug: disable information, debug (default).
Flags can also be used to control what code is output, and what is added to the scope of the output code:
--copy: all (type and value) definitions are copied to the output, along with the result of lifting declarations.
--lifting(default): type definitions are copied to the output, value definitions can be used in the output code but are not copied, the result of lifting declaration is added to the output.
--library: all (type and value) definitions and the result of liftings can be used in the output, but they are not printed.
--input: the definitions can be ornamented, but can not be referenced in 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', an ornament from
lifting declarations for all functions of