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 |