Top
This file 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 three holes at the points where we have to generate
errors. Since they come from the same original program location, they have
the same number.
| let rec _eval e = match e with
| App'(u, v, _) ->
begin match _eval u with
| Ok (Abs'(f, _)) -> _eval (f v)
| Ok (App'(_, _, _)) -> Error #10
| Ok (Const'(_, _)) -> Error #8
| Error _ -> Error #6
end
| _ -> Ok e |
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
| (match _a with Ok (_) -> Error (#a)) => #a <- (match e with App'(_, _, loc) -> loc)
| (match _a with Error b -> Error (#a)) => #a <- b
(*)| #4 <-
begin match _2 with
| Ok _ -> (match e with App'(_, _, loc) -> loc)
| Error x -> x
end*) |
We obtain an evaluator that propagates locations:
| let rec eval_loc e = match e with
| 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
| _ -> Ok e |
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
| (App'(u, v), _) ->
begin match _eval u with
| Ok (Abs' f, _) -> _eval (f v)
| Ok (App'(_, _), _) -> Error #10
| Ok (Const' _, _) -> Error #8
| Error _ -> Error #6
end
| _ -> Ok e |
Which we can patch similarly:
| let eval_loc = lifting eval : add_loc -> (add_loc, location) optres with
| (match _a with Ok (_, b) -> Error (#a)) => #a <- (match e with (_, loc) -> loc)
| (match _a with Error b -> Error (#a)) => #a <- b |
| let rec eval_loc e = match e with
| (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
| _ -> Ok e |