Top
This file has been processed with:
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.
- guard: an expression pattern that selects holes. It can contain
the program variables or metavariables (prefixed with a wildcard
“_”) which corresponds to any subterm. The hole must be written
#name.
- hole: #name where name is the name used
in the guard. (At this moment, we can only bind a unique hole, but should
allow more flexibility in the future.)
- patch content: an expression that uses any program variables or
metavariables (defined in the guard) in scope.
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 |