This file has been processed with:
| ocamlorn --library stdlib.mli \ --library desorn_expr_loc.in.ml --input desorn_expr_loc.in.ml --lifting desorn_expr_loc.lif.ml \ > desorn_expr_loc.out.ml |
| 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 let rec eval_loc e = match e with | Abs'(_, _) -> Ok e | App'(u, v, loc) -> begin match eval_loc u with | Ok (Abs'(f, _)) -> eval_loc (f v) | Ok (App'(_, _, _)) -> Error loc | Ok (Const'(_, _)) -> Error loc | Error x -> Error x end | Const'(_, _) -> Ok e |
| type expr = | Abs of (expr -> expr) | App of expr * expr | Const of int 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 _ let eval = lifting eval_loc : rev_add_loc -> (rev_add_loc, location) rev_optres |
| type expr = | Abs of (expr -> expr) | App of expr * expr | Const of int let rec eval e = match e with | Abs _ -> Some e | App(u, v) -> begin match eval u with | ((None | Some (App(_, _))) | Some (Const _)) -> None | Some (Abs f) -> eval (f v) end | Const _ -> Some e |
| type expr' = | Abs'' of ((expr' * location) -> (expr' * location)) | App'' of (expr' * location) * (expr' * location) | Const'' of int let rec eval_loc2 e = match e with | (Abs'' _, _) -> Ok e | (App''(u, v), loc) -> begin match eval_loc2 u with | Ok (Abs'' f, _) -> eval_loc2 (f v) | Ok (App''(_, _), _) -> Error loc | Ok (Const'' _, _) -> Error loc | Error x -> Error x end | (Const'' _, _) -> Ok e |
| type ornament add_loc2 : expr => expr' * location with | Abs f => (Abs'' f, _) when f : add_loc2 -> add_loc2 | App (u, v) => (App'' (u, v), _) when u v : add_loc2 | Const (i) => (Const'' (i), _) let eval = lifting eval_loc2 : rev_add_loc2 -> (rev_add_loc2, location) rev_optres |
| let rec eval e = match e with | Abs _ -> Some e | App(u, v) -> begin match eval u with | ((None | Some (App(_, _))) | Some (Const _)) -> None | Some (Abs f) -> eval (f v) end | Const _ -> Some e |