This file has been processed with:
| ocamlorn --library stdlib.mli \ --library set.in.ml --input set.in.ml --lifting set.lif.ml \ > set.out.ml |
We consider the problem of lifting a library. We will add values to an (adapted) version of OCaml’s Set. We expect that we will only have to give a patch to explain how the values should be used.
We need to add arguments of some functions. For this, we manually edit the code to wrap these arguments in a box. Then, this box can be ornamented as needed to take a tuple instead of one argument.
| type 'a box = Box of 'a |
The encoding of arguments into boxes could be avoided (e.g. automatized) if we added support to allow ornamentation of function arguments.
We start by defining some utility functions and values for manipulating integers (that are library functions and will not be lifted):
| (mode library) type bool = True | False type 'a option = None | Some of 'a val i0 : int val i1 : int val i2 : int val gt : int -> int -> bool val gte : int -> int -> bool val plus : int -> int -> int |
We assume given a type elt of elements, and a
compare function on this type, and define the sets:
| type cmp = Eq | Lt | Gt type elt = Elt val compare: elt -> elt -> cmp (mode input) |
We now consider some functions from OCaml’s Set module rewritten in the prototype syntax:
| type t = Empty | Node of t * elt * t * int let invalid_arg = Empty let height t = match t with Empty -> i0 | Node(_, _, _, h) -> h let create l vb r = match vb with | Box v -> let hl = match l with Empty -> i0 | Node(_,_,_,h) -> h in let hr = match r with Empty -> i0 | Node(_,_,_,h) -> h in Node(l, v, r, (match gte hl hr with True -> plus hl i1 | False -> plus hr i1)) let bal l vb r = match vb with | Box v -> let hl = match l with Empty -> i0 | Node(_,_,_,h) -> h in let hr = match r with Empty -> i0 | Node(_,_,_,h) -> h in match gt hl (plus hr i2) with | True -> begin match l with Empty -> invalid_arg | Node(ll, lv, lr, _) -> match gte (height ll) (height lr) with | True -> create ll (Box lv) (create lr (Box v) r) | False -> begin match lr with Empty -> invalid_arg | Node(lrl, lrv, lrr, _)-> create (create ll (Box lv) lrl) (Box lrv) (create lrr (Box v) r) end end | False -> begin match gt hr (plus hl i2) with | True -> begin match r with Empty -> invalid_arg | Node(rl, rv, rr, _) -> match gte (height rr) (height rl) with | True -> create (create l (Box v) rl) (Box rv) rr | False -> begin match rl with Empty -> invalid_arg | Node(rll, rlv, rlr, _) -> create (create l (Box v) rll) (Box rlv) (create rlr (Box rv) rr) end end | False -> Node(l, v, r, (match gte hl hr with True -> plus hl i1 | False -> plus hr i1)) end let rec add xb t = match xb with | Box x -> match t with Empty -> Node(Empty, x, Empty, i1) | Node(l, v, r, _) -> match compare x v with | Eq -> t | Lt -> bal (add (Box x) l) (Box v) r | Gt -> bal l (Box v) (add (Box x) r) let singleton xb = match xb with | Box x -> Node(Empty, x, Empty, i1) let rec min_elt t = match t with Empty -> None | Node(Empty, v, r, _) -> Some v | Node(l, v, r, _) -> min_elt l let rec max_elt t = match t with Empty -> None | Node(l, v, Empty, _) -> Some v | Node(l, v, r, _) -> max_elt r |
Then, we define the type of maps, an ornament from sets to maps and ornaments from boxes (and options) with one element to boxes (and options) with a pair of elements.
| type 'a map = MEmpty | MNode of 'a map * elt * 'a * 'a map * int type ornament 'a setmap : t => 'a map with | Empty => MEmpty | Node(l,v,r,n) => MNode(l,v,_,r,n) when l r : 'a setmap type ornament ('a,'new) box2 : 'a box => ('a * 'new) box with | Box a => Box (a,_) type ornament ('a, 'b) option2 : 'a option => ('a * 'b) option with | None => None | Some u => Some (u, _) |
And lift the functions, specifying what happens to the values
| let minvalid_arg = lifting invalid_arg : _ setmap let mheight = lifting height : _ setmap -> _ let mcreate = lifting create : _ setmap -> _ box2 -> _ setmap -> _ setmap with | #6 <- (match vb with Box (_,x) -> x) let mbal = lifting bal : _ setmap -> _ box2 -> _ setmap -> _ setmap with ornament * <- setmap, box2 | #84, #107 <- (match l with MNode(_,_,x,_,_) -> x) | #22, #47 <- (match r with MNode(_,_,x,_,_) -> x) | #14, #31, #49, #75, #100 <- (match vb with Box(_,x) -> x) | #29 <- (match r with MNode(MNode(_,_,x,_,_),_,_,_,_) -> x) | #82 <- (match l with MNode(_,_,_,MNode(_,_,x,_,_),_) -> x) let madd = lifting add : _ box2 -> _ setmap -> _ setmap with | #5, #17, #28, #49 <- (match xb with Box(_,x) -> x) | #15, #8, #26 <- (match t with MNode(_,_,x,_,_) -> x) let msingleton = lifting singleton : _ box2 -> _ setmap with | #3 <- (match xb with Box (_,x) -> x) let mmin_binding = lifting min_elt : _ setmap -> _ option2 with | #4 <- (match t with MNode(_,_,x,_,_) -> x) let mmax_binding = lifting max_elt : _ setmap -> _ option2 with | #4 <- (match t with MNode(_,_,x,_,_) -> x) |
We obtain:
| type 'a map = | MEmpty | MNode of 'a map * elt * 'a * 'a map * int let minvalid_arg = MEmpty let mheight t = match t with | MEmpty -> i0 | MNode(_, _, _, _, h) -> h let mcreate l vb r = match vb with | Box (a, x) -> let hl = match l with | MEmpty -> i0 | MNode(_, _, _, _, n) -> n in let hr = match r with | MEmpty -> i0 | MNode(_, _, _, _, n) -> n in let x1 = gte hl hr in MNode(l, a, x, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 ) let mbal l vb r = match vb with | Box (a, x) -> let hl = match l with | MEmpty -> i0 | MNode(_, _, _, _, n) -> n in let hr = match r with | MEmpty -> i0 | MNode(_, _, _, _, n) -> n in begin match gt hl (plus hr i2) with | True -> begin match l with | MEmpty -> minvalid_arg | MNode(l, v, x1, r1, _) -> begin match gte (mheight l) (mheight r1) with | True -> mcreate l (Box (v, x1)) (mcreate r1 (Box (a, x)) r) | False -> begin match r1 with | MEmpty -> minvalid_arg | MNode(l1, v1, x2, r1, _) -> mcreate (mcreate l (Box (v, x1)) l1) (Box (v1, x2)) (mcreate r1 (Box (a, x)) r) end end end | False -> begin match gt hr (plus hl i2) with | True -> begin match r with | MEmpty -> minvalid_arg | MNode(l1, v, x1, r, _) -> begin match gte (mheight r) (mheight l1) with | True -> mcreate (mcreate l (Box (a, x)) l1) (Box (v, x1)) r | False -> begin match l1 with | MEmpty -> minvalid_arg | MNode(l1, v1, x2, r1, _) -> mcreate (mcreate l (Box (a, x)) l1) (Box (v1, x2)) (mcreate r1 (Box (v, x1)) r) end end end | False -> let x1 = gte hl hr in MNode(l, a, x, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 ) end end let rec madd xb t = match xb with | Box (a, x) -> begin match t with | MEmpty -> MNode(MEmpty, a, x, MEmpty, i1) | MNode(l, v, x1, r, _) -> begin match compare a v with | Eq -> t | Lt -> mbal (madd (Box (a, x)) l) (Box (v, x1)) r | Gt -> mbal l (Box (v, x1)) (madd (Box (a, x)) r) end end let msingleton xb = match xb with | Box (a, x) -> MNode(MEmpty, a, x, MEmpty, i1) let rec mmin_binding t = match t with | MEmpty -> None | MNode(MEmpty, u, x, _, _) -> Some (u, x) | MNode(MNode(l, v, x, r, n), _, _, _, _) -> mmin_binding (MNode(l, v, x, r, n)) let rec mmax_binding t = match t with | MEmpty -> None | MNode(_, u, x, MEmpty, _) -> Some (u, x) | MNode(_, _, _, MNode(l, v, x, r, n), _) -> mmax_binding (MNode(l, v, x, r, n)) |
See the related file map.html that specializes the obtained map module back to sets...