Top

1  Extending a language of expressions

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)

Top

2  Variant with a more structured definition

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'

2.1  Plain adaption of the previous version

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)

2.2  A more precise ornament

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)

2.3  Exploiting the refinement

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)

2.4  Pre-processing?

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.