This 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' : ioexpr -> 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.