This 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 |

(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 |

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 |