This file has been processed with:
| ocamlorn --library stdlib.mli \ --library expr.in.ml --input expr.in.ml --lifting expr.lif.ml \ > expr.out.ml |
We assume given a type int of integers and two functions
add and mul
(they are define abstractly in tests/stdlib.mli).
We have the following code:
| type expr = | Const of int | Add of expr * expr | Mul of expr * expr let rec eval = function | Const i -> i | Add ( u , v ) -> add (eval u) (eval v) | Mul ( u , v ) -> mul (eval u) (eval v) |
And we want to use the following representation instead:
| type binop' = | Add' | Mul' type expr' = | Const' of int | Binop' of binop' * expr' * expr' |
We define an ornament:
| type ornament oexpr : expr => expr' with | Const ( i ) => Const' ( i ) | Add ( u , v ) => Binop' ( Add' , u , v ) when u v : oexpr | Mul ( u , v ) => Binop' ( Mul' , u , v ) when u v : oexpr |
And ask for the lifting at this ornament:
| let eval' = lifting eval : oexpr -> int |
We obtain the following (complete) code:
| let rec eval' = function | Const' i -> i | Binop'(Add', u, v) -> add (eval' u) (eval' v) | Binop'(Mul', u, v) -> mul (eval' u) (eval' v) |
In fact, we need not specify the ornament relation oexpr -> int
and have instead tell to use the ornament oexpr whenever possible
and otherwise the identity ornament. That is, the following binding
| let eval' = lifting eval : _ with ornament * <- oexpr, @id |
will return exactly the same output in this case.
Notice that the reverse transformation works similarly, as the oexpr
ornament is actually an isomorphism:
| type ornament ioexpr : expr' => expr with | Const' ( i ) => Const ( i ) | Binop' ( Add' , u , v ) => Add ( u , v ) when u v : ioexpr | Binop' ( Mul' , u , v ) => Mul ( u , v ) when u v : ioexpr |
Then, we can lift eval' along this transformation
into a funtion eval'' that will happen to be equal to the function
equal we came from.
| let eval'' = lifting eval' : rev_oexpr -> int |
| let rec eval'' = function | Const x -> x | Add(x, x') -> add (eval'' x) (eval'' x') | Mul(x, x') -> mul (eval'' x) (eval'' x') |
By starting with a recursive copy function, we can
use the ornament to construct a function that transforms
expr intro expr'
| let rec copy = function | Const (i) -> Const i | Add ( u , v ) -> Add ( copy u , copy v ) | Mul ( u , v ) -> Mul ( copy u , copy v ) let expr2expr' = lifting copy : expr -> oexpr |
We obtained the expected result:
| let rec expr2expr' = function | Const i -> Const' i | Add(u, v) -> Binop'(Add', expr2expr' u, expr2expr' v) | Mul(u, v) -> Binop'(Mul', expr2expr' u, expr2expr' v) |
In this example, the goal of the ornamentation is more probably to factor out similar elements in the original data-structure, but the code is still duplicated for the two cases.
Indeed, the prototype try hard to maintain the original structure as much as possible by renesting patterns that were nested in the base code—but that are decomposed during the transformation.
However, we may always manually request otherwise, or rather redecomposed nested
pattern on demand. That is, from eval', we would obtain the
following code:
| let rec eval'_1 = function | Const' i -> i | Binop'(binop, u, v) -> match binop with | Add' -> add (eval'_1 u) (eval'_1 v) | Mul' -> mul (eval'_1 u) (eval'_1 v) |
From which, we may fact factor out both branches, leading to
| let rec eval'_2 = function | Const' i -> i | Binop'(binop, u, v) -> (match binop with Add' -> add | Mul' -> mul) (eval'_2 u) (eval'_2 v) |
Again factorization could be automated, but requesting factorization should be on demand.
This is just to emphasize that lifting is just one important tool in a chain of simple transformations that we may apply when refactoring (or modifying) code. When each transformations is a pure refactoring, which preserve the semantics, as above, so is their composition.
Some examples who relift already lifted expressions process everything in <lifting> mode, since the code lifted code must be again available as input.