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
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
You can look at transcripts corresponding the examples presented in the paper and some other examples that were not presented.
Dependencies for the prototype:
opam
install
ocamlfind
)
opam
install
pprint
)
opam
install
menhir
)
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.
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.
Example:
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.
ornament
#
xx
<-
ornament_name
specifies that the ornament ornament_name
should 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 @id
.
lifting
#
xx
<-
var
specifies that var
should be used as the lifting of the function appearing at #
xx
.
#
xx
<-
an_expression
specifies that the patch an_expression
should be used at #
xx
.
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) |
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:
--noisy
: when active, output the representation of the skeleton and the encoding and decoding functions.
--nonoisy
: disables noisy mode (default).
--info
, --debug
: displays some useful information during the ornamentation process. The debug flags also preserves internal exceptions and backtraces (but is very verbose).
--noinfo
, --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
, and expr_to_expr'.oml
defines
a datatype expr'
, an ornament from expr
to expr'
and
lifting declarations for all functions of expr.ml
.