Top

This file has been processed with:

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

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