Top
This has been processed with:
Hiding administrative data
(code in tests/expr_loc.ml, run with
./ocamlorn tests/stdlib.mli tests/expr_loc.ml)
Let us start with the code for a simple interpreter:
| type 'a option =
| Some of 'a
| None
type expr =
| Abs of (expr -> expr)
| App of expr * expr
| Const of int |
| let rec eval e = match e with
| App (u, v) ->
begin match eval u with Some (Abs f) -> eval (f v) | _ -> None end
| _ -> Some(e) |
We want to add a more precise error reporting, pointing out the location of
an error. We need a type extended with locations, and a result
type to return either a value or the location of the error.
| type location = Location of string * int * int
type expr_loc =
| Abs' of (expr_loc -> expr_loc) * location
| App' of expr_loc * expr_loc * location
| Const' of int * location
type ('a,'err) result =
| Ok of 'a
| Error of 'err |
The type expr_loc is an ornament of expr, and
result of option
| type ornament add_loc : expr => expr_loc 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 ask for an incomplete lifting:
| let _eval = lifting eval : add_loc -> (add_loc, location) optres |
The resulting term has one hole at the point where we have to generate an error.
| let rec _eval e = match e with
| (Abs'(_, _) | Const'(_, _)) -> Ok e
| App'(u, v, _) ->
begin match _eval u with
| Ok (Abs'(f, _)) -> _eval (f v)
| ((Ok (App'(_, _, _)) | Ok (Const'(_, _)))
| Error _) -> Error #4
end |
We re-match on the result of the preivous pattern matchin to check in which of these cases we are.
The result has been automatically named _2: since it is the result of an expression, we
do not want to compute it a second time.
In the case of an error, we propagate the error, while in other
cases we need to return the location of the application.
| let eval_loc = lifting eval : add_loc -> (add_loc, location) optres with
| #4 <-
begin match _2 with
| Ok _ -> (match e with App'(_, _, loc) -> loc)
| Error x -> x
end |
We obtain an evaluator that propagates locations. Note that the patterns that were previously grouped
in the error case have been separated:
| let rec eval_loc e = match e with
| (Abs'(_, _) | Const'(_, _)) -> Ok e
| App'(u, v, loc) ->
begin match eval_loc u with
| Ok (Abs'(f, _)) -> eval_loc (f v)
| (Ok (App'(_, _, _)) | Ok (Const'(_, _))) ->
Error loc
| Error x -> Error x
end |
Alternative representation of locations
Remark that instead of attaching locations directly to the constructor, one
would rather systematically lift expressions to a pair of expressions
and a location:
| type expr_loc = expr' * location
and expr' =
| Abs' of (expr_loc -> expr_loc)
| App' of expr_loc * expr_loc
| Const' of int |
However, our prototype does not implement type abbraviation yet. Hence to
fit with these syntactic restriction, we may equivalently defined:
| type expr' =
| Abs' of ((expr' * location) -> (expr' * location))
| App' of (expr' * location) * (expr' * location)
| Const' of int |
and use expr' loc instead of expr_loc:
| 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), _)
let _eval = lifting eval : add_loc -> (add_loc, location) optres |
We get the following program:
| let rec _eval e = match e with
| ((Abs' _, _) | (Const' _, _)) -> Ok e
| (App'(u, v), _) ->
begin match _eval u with
| Ok (Abs' f, _) -> _eval (f v)
| ((Ok (App'(_, _), _) | Ok (Const' _, _)) | Error _) ->
Error #4
end |
Which we can patch similarly:
| let eval_loc = lifting eval : add_loc -> (add_loc, location) optres with
| #4 <-
begin match _2 with
| Ok _ -> (match e with (_,loc) -> loc)
| Error x -> x
end |
| let rec eval_loc e = match e with
| ((Abs' _, _) | (Const' _, _)) -> Ok e
| (App'(u, v), loc) ->
begin match eval_loc u with
| Ok (Abs' f, _) -> eval_loc (f v)
| (Ok (App'(_, _), _) | Ok (Const' _, _)) ->
Error loc
| Error x -> Error x
end |