This section has been processed with:
ocamlorn --library stdlib.mli \ --library disorn_aexpr.in.ml --input disorn_aexpr.in.ml --lifting disorn_aexpr.lif.ml \ > disorn_aexpr.out.ml |
We start with a small language of expressions and its evaluator:
type expr = | Const of int | Add of expr * expr let rec eval e = match e with | Const i -> i | Add(u, v) -> add (eval u) (eval v) |
We wish to add a new independent case to expressions. The new type will be as follows:
type expr' = | Const' of int | Add' of expr' * expr' | Mul' of expr' * expr' |
The two types can be put in relation. We can adapt the code of ornaments
type ornament aexpr : expr => expr' with | Const ( i ) => Const' ( i ) | Add ( u , v ) => Add' ( u , v ) when u v : aexpr | ~ => Mul' ( u , v ) when u v : aexpr |
Then the skeleton of the new version of eval can be obtained by lifting the old one:
let _eval' = lifting eval : aexpr -> _ |
which returns an incomplete definition:
let rec _eval' e = match e with | Const' i -> i | Add'(u, v) -> add (_eval' u) (_eval' v) | Mul'(_, _) -> #1 |
Notice that the user is ask to fill in all the code for the new branch, and
does not try to deduce it from the Add
branch—the two cases are
unrelated. We can fill in the expected code as follows:
let eval' = lifting eval : aexpr -> _ with patch match __ with Mul' (u, v) -> #[mul (eval' u) (eval' v)] |
Which returns the expected code:
let rec eval' e = match e with | Const' i -> i | Add'(u, v) -> add (eval' u) (eval' v) | Mul'(x, x1) -> mul (eval' x) (eval' x1) |
This section has been processed with:
ocamlorn --library stdlib.mli \ --library disorn_aexpr.in.ml --input disorn_aexpr.in.ml --lifting disorn_aexpr.lif.ml \ > disorn_aexpr.out.ml |
We start with a small more structured definition of expressions:
type binop = | Add type expr = | Const of int | Binop of binop * expr * expr |
and proceed as before:
type binop' = | Add' | Mul' type expr' = | Const' of int | Binop' of binop' * expr' * expr' |
The ornament and the ~
appears in a deep pattern matching on the
left:
type ornament aexpr : expr => expr' with | Const ( i ) => Const' ( i ) | Binop (Add, u , v ) => Binop' (Add', u , v ) when u v : aexpr | ~ => Binop' (Mul', _ , _) |
The eval function
let rec eval e = match e with | Const i -> i | Binop(Add, u, v) -> add (eval u) (eval v) |
is lifted eval
into eval'
as before:
let eval' = lifting eval : aexpr -> _ with (match _e with Binop' (Mul', u, v) -> #a) => #a <- mul (eval' u) (eval' v) |
with the expected output:
let rec eval' e = match e with | Const' i -> i | Binop'(Add', u, v) -> add (eval' u) (eval' v) | Binop'(Mul', u, v) -> mul (eval' u) (eval' v) |
We may require Binop
to always be lifted to Binop'
then using an auxiliary ornament for op
:
type ornament aexpr' : expr => expr' with | Const ( i ) => Const' ( i ) | Binop (op, u , v ) => Binop' (op, u , v ) when op : aop, u v : aexpr' and aop : binop => binop' with | Add => Add' | ~ => Mul' |
However, if we do not change the definition of eval
the lifting is
unable to take advantage of this definition:
let eval' = lifting eval : aexpr' -> _ |
This leads to the same result as above:
let rec eval' e = match e with | Const' i -> i | Binop'(Add', u, v) -> add (eval' u) (eval' v) | Binop'(Mul', _, _) -> #1 |
Then we have to patch altogether as previously:
let eval' = lifting eval : aexpr' -> _ with (match _e with Binop' (Mul', u, v) -> #a) => #a <- mul (eval' u) (eval' v) |
and get the same result:
let rec eval' e = match e with | Const' i -> i | Binop'(Add', u, v) -> add (eval' u) (eval' v) | Binop'(Mul', u, v) -> mul (eval' u) (eval' v) |
To alllow writing a smaller patch, we need to use shallow pattern matching:
let rec evalop e = match e with | Const i -> i | Binop(op, u, v) -> (match op with Add -> add) (evalop u) (evalop v) |
We can then just write:
let evalop' = lifting evalop : aexpr' -> _ |
Which returns the expected code:
let rec evalop' e = match e with | Const' i -> i | Binop'(op, u, v) -> begin match op with | Add' -> add | Mul' -> #1 end (evalop' u) (evalop' v) |
We may then fill the code as desired:
let evalop' = lifting evalop : aexpr' -> _ with (match _op with Mul' -> #a) => #a <- mul |
This returns the expected code:
let rec evalop' e = match e with | Const' i -> i | Binop'(op, u, v) -> begin match op with | Add' -> add | Mul' -> mul end (evalop' u) (evalop' v) |
At first glance, one may wonder why the user must do the rewriting of
eval
into evalop
manually, since the two codes are
observationally equivalent.
However, lifting is syntactic and the differences between
| Binop (Add, u, v) -> add (evalop u) (evalop v)
and
| Binop (Add, u, v) -> (match op with Add -> add) (evalop u) (evalop v)
is still signifant. To see this, assume that we had two constructors
Add
and Sub
:
| Binop (Add, u, v) -> add (evalop u) (evalop v) | Binop (Sub, u, v) -> sub (evalop u) (evalop v)
and
| Binop (op, u, v) -> (match op with Add -> add | Sub -> sub) (evalop u) (evalop v)
In the second pattern, we learn that the two recursive calls
evalop u
and evalop v
is idependent of the op
value.
| Binop (op, u, v) -> ??? (evalop u) (evalop v)
Still, in this case (with two constructors) this transformation could be semi-automated, i.e. performed automatically but under an explicit user request of maximally sharing the two branches.