This has been processed with:

ocamlorn --library stdlib.mli \ --library exprval.in.ml --input exprval.in.ml --lifting exprval.lif.ml \ > exprval.out.ml |

type expr = | Const of bool | Abs of (expr -> expr) | App of expr * expr |

let rec eval e = match e with | Const i -> Some (Const i) | Abs f -> Some (Abs f) | App (u, v) -> begin match eval u with | Some (Abs f) -> begin match eval v with | Some x -> eval (f x) | None -> None end | _ -> None end |

The example illustrates how the recursive structure can be changed during ornamentation.

We notice that the eval function only returns values from a limited
subset of expressions that represent values. Similarly, the functions
in abstractions are only called with values. This invariant can be
expressed using the following mutually recursive types of expressions
`expr''`

and values `value''`

:

type expr' = | Val of value | App' of expr' * expr' and value = | Const' of bool | Abs' of (value -> expr') |

We can relate this new representation to the representation
`expr'`

by the following mutually recursive ornaments: while
`oexpr'`

is able to map all expression constructors, the ornament
`oval'`

is partial and only maps the constructors that actually
correspond to values. This is an ornament, because deleting a constructor
is equivalent to asking for an information that cannot be produced (*i.e.*
a value of the empty type). We still have to match all possible constructors,
but we map them to the empty pattern, written `~`

.

type ornament oexpr : expr => expr' with | Const i => Val (Const' i) | Abs f => Val (Abs' f) when f : oval -> oexpr | App ( u , v ) => App' ( u , v ) when u v : oexpr and oval : expr => value with | Const i => Const' i | Abs f => Abs' f when f : oval -> oexpr | App (u,v) => ~ |

Note that in this case, we do not follow the recursive structure of
the `expr'`

datatype: some recursive occurences are transformed
into values while others stay expressions.

We can then re-lift `expr'`

using this ornament:

let eval' = lifting eval : oexpr -> oval option with ornament * <- @id |

We obtain the following program. No patch is asked, because we can
prove locally (*i.e.* without going through function calls) that the
restriction to values is correct. Otherwise, we would have to produce
a patch of the empty type.

let rec eval' e = match e with | Val (Const' i) -> Some (Const' i) | Val (Abs' f) -> Some (Abs' f) | App'(u, v) -> begin match eval' u with | (None |Some (Const' _)) -> None | Some (Abs' f) -> begin match eval' v with | None -> None | Some x -> eval' (f x) end end |

We should also lift the creation of values.
However, this will only succeed if we check in the creation of abstractions
that the argument is always a value form. We define the function
`cval`

for that purpose:

let cval x = match x with | App (u, v) -> fail | Const i -> Const i | Abs f -> Abs f |

We should then use it in the construction of abstractions as follows

let id = Abs (fun x -> cval x) let xx = Abs (fun x -> App (cval x, cval x)) let z = App (App (xx, id), Const True) let v _x = eval z |

let cval' = lifting cval : oval -> oexpr let id' = lifting id : oexpr let xx' = lifting xx : oexpr let z' = lifting z : oexpr let v' = lifting v : _ -> oval option |

let cval' x = match x with | Const' i -> Val (Const' i) | Abs' f -> Val (Abs' f) let id' = Val (Abs' (fun x -> cval' x)) let xx' = Val (Abs' (fun x -> App'(cval' x, cval' x))) let z' = App'(App'(xx', id'), Val (Const' True)) let v' _x = eval' z' |