Top

This file has been processed with:

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

First, we explain how to use the robust patch language in the case of the ornementation of a small interpreter with bare expressions to localized expressions. Then, we extend this small interpreter by adding an addition primitive using a type relation: the patches written previously were sufficiently robust and we can do the lifting again without additional specifications. At last, we add let constructs to the ornamented code, and we show that we can go back to a simpler version via disornamentation.

Some definitions useful throughout this example:

let eq a b = True type 'a list = Nil | Cons of 'a * 'a list let rec assoc n l = match l with | Nil -> None | Cons((a, b), q) -> match eq a n with | True -> Some b | False -> assoc n q

From bare expressions to localized expressions

Let’s take an interpreter of a small language, without location information.

type expr = | Abs of (expr -> expr) | App of expr * expr | Const of int let rec eval env e = match e with | App (u, v) -> let res_u = eval env u in begin match res_u with | Some (Abs f) -> eval env (f v) | _ -> None end | _ -> Some(e)

We define the type of localized expressions:

type location = Location of string * int * int type ('a, 'err) result = | Ok of 'a | Error of 'err
type expr' = | Abs' of ((expr' * location) -> (expr' * location)) | App' of (expr' * location) * (expr' * location) | Const' of int

The goal is to lift the eval function to a function that evaluates localized expressions and returns a localized error when it does not succeed.

Let us define two ornaments, one for the expressions and the other one for the error types.

type ornament add_loc : expr => expr' * location with | Abs f => (Abs' f, _) when f : add_loc -> add_loc | App (u, v) => (App' (u, v), _) when u v : add_loc | Const (i) => (Const' (i), _) type ornament ('a, 'err) optres : 'a option => ('a, 'err) result with | Some a => Ok a | None => Error _

We are ready to lift eval:

let _eval_incomplete = lifting eval : _ list -> add_loc -> (add_loc, location) optres
let rec _eval_incomplete env e = match e with | (App'(u, v), _) -> let res_u = _eval_incomplete env u in begin match res_u with | Ok (Abs' f, _) -> _eval_incomplete env (f v) | Ok (App'(_, _), _) -> Error #8 | Ok (Const' _, _) -> Error #6 | Error _ -> Error #13 end | _ -> Ok e

There are some holes that are identified with a number, such as #8. We need to specify patches for every hole. They must be supplied after the with keyword. They can be filled using their numbered identifiers (that was the only way to do it prior to our work):

let eval' = lifting eval: _ list -> add_loc -> (_, _) optres with | #6, #8 <- (match e with (_, loc) -> loc) | #13 <- (match res_u with Error x -> x)
let rec eval' env e = match e with | (App'(u, v), loc) -> let res_u = eval' env u in begin match res_u with | Ok (Abs' f, _) -> eval' env (f v) | (Ok (App'(_, _), _) | Ok (Const' _, _)) -> Error loc | Error x -> Error x end | _ -> Ok e

However, these identifiers may change when the code is edited. Instead of this, we can use an expression pattern to select the holes that we want to fill. Thus, if the code is slightly changed or extended, the patches may still apply.

let eval' = lifting eval: _ list -> add_loc -> (_, _) optres with | (match _a with Error x -> Error (#a)) => #a <- x | (match _a with Ok _ -> Error (#a)) => #a <- (match e with (_, loc) -> loc)
let rec eval' env e = match e with | (App'(u, v), loc) -> let res_u = eval' env u in begin match res_u with | Ok (Abs' f, _) -> eval' env (f v) | (Ok (App'(_, _), _) | Ok (Const' _, _)) -> Error loc | Error x -> Error x end | _ -> Ok e

Every patch is specified with the following syntax: guard => hole <- patch content.

Add the add primitive

We now add a new construct to our small language in a new datatype expr2 and define the relation between expr and expr2:

type expr2 = | Abs2 of (expr2 -> expr2) | App2 of expr2 * expr2 | Const2 of int | Add2 of expr2 * expr2
type relation add_add: expr => expr2 with | Abs f => Abs2 f when f: add_add -> add_add | App(a, b) => App2(a, b) when a b: add_add | Const(i) => Const2(i) | ~ => Add2(a, b) when a b: add_add

The pattern ~ stands for the empty pattern. This relation is not considered to be an ornament but it is still supported by the generalized framework.

We use this relation to lift the eval function:

let eval2 = lifting eval: _ -> add_add -> _ option
let rec eval2 env e = match e with | App2(u, v) -> let res_u = eval2 env u in begin match res_u with | Some (Abs2 f) -> eval2 env (f v) | ((None | Some (App2(_, _))) | Some (Const2 _)) -> None | Some (Add2(_, _)) -> #1 end | (Abs2 _ | Const2 _) -> Some e | Add2(_, _) -> #2

This needs contains two holes, indeed. We fill them with the following two patches:

let eval2 = lifting eval: _ -> add_add -> _ option with | (match _a with Some(Add2(_, _)) -> #a) => #a <- None | (match e with Add2(u, v) -> #a) => #a <- (let u' = eval2 env u in let v' = eval2 env v in match u' with | Some (Const2 i) -> begin match v' with | Some (Const2 j) -> Some (Const2 (plus i j)) | _ -> None end | _ -> None)
let rec eval2 env e = match e with | App2(u, v) -> let res_u = eval2 env u in begin match res_u with | Some (Abs2 f) -> eval2 env (f v) | _ -> None end | (Abs2 _ | Const2 _) -> Some e | Add2(x, x1) -> let u' = eval2 env x in let v' = eval2 env x1 in begin match u' with | Some (Const2 i) -> begin match v' with | Some (Const2 j) -> Some (Const2 (plus i j)) | (((None | Some (Abs2 _)) | Some (App2(_, _))) | Some (Add2(_, _))) -> None end | (((None | Some (Abs2 _)) | Some (App2(_, _))) | Some (Add2(_, _))) -> None end

Branches of pattern matching are not correctly compressed. This could be addressed in future work.

Lifting again

Now, let’s try to re-lift the eval function with this new construct. We write the ornament again:

type expr2' = | Abs2' of ((expr2' * location) -> (expr2' * location)) | App2' of (expr2' * location) * (expr2' * location) | Add2' of (expr2' * location) * (expr2' * location) | Const2' of int
type ornament add_loc : expr2 => expr2' * location with | Abs2 f => (Abs2' f, _) when f : add_loc -> add_loc | App2 (u, v) => (App2' (u, v), _) when u v : add_loc | Add2 (u, v) => (Add2' (u, v), _) when u v : add_loc | App2 (u, v) => (App2' (u, v), _) when u v : add_loc | Const2 (i) => (Const2' (i), _)

And we do the lifting again, first without any patch:

let eval2' = lifting eval2: _ list -> add_loc -> (_, _) optres
let rec eval2' env e = match e with | (App2'(u, v), _) -> let res_u = eval2' env u in begin match res_u with | Ok (Abs2' f, _) -> eval2' env (f v) | Ok (App2'(_, _), _) -> Error #43 | Ok (Add2'(_, _), _) -> Error #39 | Ok (Const2' _, _) -> Error #41 | Error _ -> Error #48 end | ((Abs2' _, _) | (Const2' _, _)) -> Ok e | (Add2'(u, v), _) -> let u' = eval2' env u in let v' = eval2' env v in begin match u' with | Ok (Const2' i, _) -> begin match v' with | Ok (Const2' i1, _) -> Ok (Const2' (plus i i1), #12) | Ok (Abs2' _, _) -> Error #17 | Ok (App2'(_, _), _) -> Error #15 | Ok (Add2'(_, _), _) -> Error #8 | Error _ -> Error #21 end | Ok (Abs2' _, _) -> Error #27 | Ok (App2'(_, _), _) -> Error #25 | Ok (Add2'(_, _), _) -> Error #6 | Error _ -> Error #31 end

Then, with the same patches as before:

let eval2' = lifting eval2: _ list -> add_loc -> (_, _) optres with | (match _a with Error x -> Error (#a)) => #a <- x | (match _a with Ok _ -> Error (#a)) => #a <- (match e with (_, loc) -> loc)
let rec eval2' env e = match e with | (App2'(u, v), loc) -> let res_u = eval2' env u in begin match res_u with | Ok (Abs2' f, _) -> eval2' env (f v) | ((Ok (App2'(_, _), _) | Ok (Add2'(_, _), _)) | Ok (Const2' _, _)) -> Error loc | Error x -> Error x end | ((Abs2' _, _) | (Const2' _, _)) -> Ok e | (Add2'(u, v), loc) -> let u' = eval2' env u in let v' = eval2' env v in begin match u' with | Ok (Const2' i, _) -> begin match v' with | Ok (Const2' i1, _) -> Ok (Const2' (plus i i1), #12) | ((Ok (Abs2' _, _) | Ok (App2'(_, _), _)) | Ok (Add2'(_, _), _)) -> Error loc | Error x -> Error x end | ((Ok (Abs2' _, _) | Ok (App2'(_, _), _)) | Ok (Add2'(_, _), _)) -> Error loc | Error x -> Error x end

With the same set of patches, holes that were filled are still filled, some new holes are also directly filled (as they match the expression pattern) and only one hole remains. We only have to add a single patch:

let eval2' = lifting eval2: _ list -> add_loc -> (_, _) optres with | (match _a with Error x -> Error (#a)) => #a <- x | (match _a with Ok _ -> Error (#a)) => #a <- (match e with (_, loc) -> loc) | (Ok (Const2' (plus _a _b), #a)) => #a <- (match e with (Add2'(_, _), loc) -> loc)
let rec eval2' env e = match e with | (App2'(u, v), loc) -> let res_u = eval2' env u in begin match res_u with | Ok (Abs2' f, _) -> eval2' env (f v) | ((Ok (App2'(_, _), _) | Ok (Add2'(_, _), _)) | Ok (Const2' _, _)) -> Error loc | Error x -> Error x end | ((Abs2' _, _) | (Const2' _, _)) -> Ok e | (Add2'(u, v), loc) -> let u' = eval2' env u in let v' = eval2' env v in begin match u' with | Ok (Const2' i, _) -> begin match v' with | Ok (Const2' i1, _) -> Ok (Const2' (plus i i1), loc) | ((Ok (Abs2' _, _) | Ok (App2'(_, _), _)) | Ok (Add2'(_, _), _)) -> Error loc | Error x -> Error x end | ((Ok (Abs2' _, _) | Ok (App2'(_, _), _)) | Ok (Add2'(_, _), _)) -> Error loc | Error x -> Error x end

There are two interesting points: first, holes that were patched before we add the add constructor are still patched, even if the term has changed. Second, new holes that were similar to the previous ones were also automatically filled. That may be dangerous: the user has to give a guard strong enough so that holes are not incorrectly filled.

let construct and disornamentation

Now, let us assume that we modified our types and ornaments to add two new constructs to our little language, namely let bindings and variables:

type expr_big = | Absb of (expr_big -> expr_big) | Appb of expr_big * expr_big | Letb of string * expr_big * expr_big | Constb of int | Varb of string | Addb of expr_big * expr_big
type expr_big' = | Absb' of ((expr_big' * location) -> (expr_big' * location)) | Appb' of (expr_big' * location) * (expr_big' * location) | Constb' of int | Varb' of string | Letb' of string * (expr_big' * location) * (expr_big' * location) | Addb' of (expr_big' * location) * (expr_big' * location)
type ornament add_loc' : expr_big => expr_big' * location with | Absb f => (Absb' f, _) when f : add_loc' -> add_loc' | Appb (u, v) => (Appb' (u, v), _) when u v : add_loc' | Addb (u, v) => (Addb' (u, v), _) when u v : add_loc' | Constb (i) => (Constb' (i), _) | Varb i => (Varb' i, _) | Letb (s, u, v) => (Letb' (s, u, v), _) when u v : add_loc'

This time, let us complete the evaluator in the localized version:

let rec eval_big env e = match e with | (Absb' _, _) -> Ok e | (Appb'(u, v), loc) -> let res_u = eval_big env u in begin match res_u with | Ok (Absb' f, _) -> eval_big env (f v) | Ok _ -> Error loc | Error x -> Error x end | (Addb' (u, v), loc) -> let u' = eval_big env u in let v' = eval_big env v in begin match u' with | Ok (Constb' i, _) -> begin match v' with | Ok (Constb' i1, _) -> Ok (Constb' (plus i i1), loc) | Error x -> Error x | Ok (_, _) -> Error loc end | Ok (_, _) -> Error loc | Error x -> Error x end | (Constb' _, _) -> Ok e | (Varb' i, loc) -> begin match assoc i env with | Some a -> Ok a | None -> Error loc end | (Letb'(s, u, v), _) -> begin match eval_big env u with | Ok a -> eval_big (Cons((s, a), env)) v | Error x -> Error x end

We may still want to go back to the original datatype because the code is more readable there. We can use disornamentation for that purpose. The prefix rev_ added to add_loc' designate the type relation add_loc' taken in the reverse direction, as if we had defined:

type ornament rev_add_loc' : expr_big' * location => expr_big with | (Absb' f, _) => Absb f when f : rev_add_loc' -> rev_add_loc' | (Appb' (u, v), _) => Appb (u, v) when u v : rev_add_loc' | (Addb' (u, v), _) => Addb (u, v) when u v : rev_add_loc' | (Constb' (i), _) => Constb (i) | (Varb' i, _) => Varb i | (Letb' (s, u, v), _) => Letb (s, u, v) when u v : rev_add_loc'

but we need not make this definition.

let eval_desorn = lifting eval_big: _ -> rev_add_loc' -> _ rev_optres

We get:

let rec eval_desorn env e = match e with | (Absb _ | Constb _) -> Some e | Appb(u, v) -> let res_u = eval_desorn env u in begin match res_u with | Some (Absb f) -> eval_desorn env (f v) | (((((None | Some (Appb(_, _))) | Some (Letb(_, _, _))) | Some (Constb _)) | Some (Varb _)) | Some (Addb(_, _))) -> None end | Addb(u, v) -> let u' = eval_desorn env u in let v' = eval_desorn env v in begin match u' with | Some (Constb i) -> begin match v' with | Some (Constb i1) -> Some (Constb (plus i i1)) | (((((None | Some (Absb _)) | Some (Appb(_, _))) | Some (Letb(_, _, _))) | Some (Varb _)) | Some (Addb(_, _))) -> None end | (((((None | Some (Absb _)) | Some (Appb(_, _))) | Some (Letb(_, _, _))) | Some (Varb _)) | Some (Addb(_, _))) -> None end | Varb i -> begin match assoc i env with | Some a -> Some a | None -> None end | Letb(s, u, v) -> begin match eval_desorn env u with | Some a -> eval_desorn (Cons((s, a), env)) v | None -> None end

And ornamentation again

Then, this code can be ornamented again. We can use the same set of patches, but there is one hole that needs an extra patch. There is ongoing work to generate patches at desornamentation time.

let eval_desorn_orn = lifting eval_desorn: _ list -> add_loc' -> (_, _) optres with | (match _a with Error x -> Error (#a)) => #a <- x | (match _a with Ok _ -> Error (#a)) => #a <- (match e with (_, loc) -> loc) | (Ok (Constb' (plus _a _b), #a)) => #a <- (match e with (Addb'(_, _), loc) -> loc)
let rec eval_desorn_orn env e = match e with | ((Absb' _, _) | (Constb' _, _)) -> Ok e | (Appb'(u, v), loc) -> let res_u = eval_desorn_orn env u in begin match res_u with | Ok (Absb' f, _) -> eval_desorn_orn env (f v) | ((((Ok (Appb'(_, _), _) | Ok (Constb' _, _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | (Addb'(u, v), loc) -> let u' = eval_desorn_orn env u in let v' = eval_desorn_orn env v in begin match u' with | Ok (Constb' i, _) -> begin match v' with | Ok (Constb' i1, _) -> Ok (Constb' (plus i i1), loc) | ((((Ok (Absb' _, _) | Ok (Appb'(_, _), _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | ((((Ok (Absb' _, _) | Ok (Appb'(_, _), _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | (Varb' i, _) -> begin match assoc i env with | Some a -> Ok a | None -> Error #49 end | (Letb'(s, u, v), _) -> begin match eval_desorn_orn env u with | Ok a -> eval_desorn_orn (Cons((s, a), env)) v | Error x -> Error x end

With the extra patch:

let eval_desorn_orn = lifting eval_desorn: _ list -> add_loc' -> (_, _) optres with | (match _a with Error x -> Error (#a)) => #a <- x | (match _a with Ok _ -> Error (#a)) => #a <- (match e with (_, loc) -> loc) | (Ok (Constb' (plus _a _b), #a)) => #a <- (match e with (Addb'(_, _), loc) -> loc) | (match _a with None -> Error (#a)) => #a <- (match e with (_, loc) -> loc)
let rec eval_desorn_orn env e = match e with | ((Absb' _, _) | (Constb' _, _)) -> Ok e | (Appb'(u, v), loc) -> let res_u = eval_desorn_orn env u in begin match res_u with | Ok (Absb' f, _) -> eval_desorn_orn env (f v) | ((((Ok (Appb'(_, _), _) | Ok (Constb' _, _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | (Addb'(u, v), loc) -> let u' = eval_desorn_orn env u in let v' = eval_desorn_orn env v in begin match u' with | Ok (Constb' i, _) -> begin match v' with | Ok (Constb' i1, _) -> Ok (Constb' (plus i i1), loc) | ((((Ok (Absb' _, _) | Ok (Appb'(_, _), _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | ((((Ok (Absb' _, _) | Ok (Appb'(_, _), _)) | Ok (Varb' _, _)) | Ok (Letb'(_, _, _), _)) | Ok (Addb'(_, _), _)) -> Error loc | Error x -> Error x end | (Varb' i, loc) -> begin match assoc i env with | Some a -> Ok a | None -> Error loc end | (Letb'(s, u, v), _) -> begin match eval_desorn_orn env u with | Ok a -> eval_desorn_orn (Cons((s, a), env)) v | Error x -> Error x end