Top

This has been processed with:

ocamlorn --library stdlib.mli \ --library set.lib.ml --input set.out.ml --lifting map.lif.ml > map.out.ml

Specializing a library: maps to sets

We consider the problem of specializing a library. For exemple, maps with unit values can be used to implement maps.

We reused the library of sets that have been obtained by lifting maps! That is the source file map.in.ml of this example is the same of the target file set.out.ml of the set example.

The library map.lib.ml is also the library set.lib.ml, so we only produce the lifting input:

type set = | Empty | Node of set * elt * set * int type ornament mapset : unit map => set with | MNode (l,k,(),r,i) => Node (l,k,r,i) when l r : mapset | MEmpty => Empty

This would be sufficient, but dummy unit arguments will be carry arround by auxiliary functions. To remove then, we need the following ornaments.

type ornament 'a debox2 : ('a * unit) box => 'a box with | Box (a,()) => Box a type ornament 'a deoption2 : ('a * unit) option => 'a option with | None => None | Some (u, ()) => Some u

We still need to list all functions that we wish to lift with their types...

let invalid_arg = lifting minvalid_arg : mapset let height = lifting mheight : mapset -> _ let create = lifting mcreate : mapset -> _ debox2 -> mapset -> mapset

Notice here the ornament specification _ debox2 to remove the useless unit argument.

If we had simply defined:

let create2 = lifting mcreate : mapset -> _ -> mapset -> mapset with ornament * <-@id

We instead need to tell that missing ornament are the identity,

let create2 l vb r = match vb with | Box (k, x) -> let hl = match l with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let hr = match r with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let x1 = gte hl hr in let i = match x1 with | True -> plus hl i1 | False -> plus hr i1 in match x with | () -> SNode(l, k, r, i)

instead of:

let create l vb r = match vb with | Box k -> let hl = match l with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let hr = match r with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let x1 = gte hl hr in SNode(l, k, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 )

We may still recover the correct code a posteriori

let create3 = lifting create2 : _ -> _ debox2 -> _ -> _ with ornament * <-@id

We get:

let create l vb r = match vb with | Box k -> let hl = match l with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let hr = match r with | SEmpty -> i0 | SNode(l, k, r, i) -> i in let x1 = gte hl hr in let i = match x1 with | True -> plus hl i1 | False -> plus hr i1 in SNode(l, k, r, i)

Which is exquivalent to create, but the auxiliary let binding.

We continue with the “deboxing” ornaments:

let bal = lifting mbal : mapset -> _ debox2 -> mapset -> mapset let add = lifting madd : _ debox2 -> mapset -> mapset let singleton = lifting msingleton : _ debox2 -> mapset let min_elt = lifting mmin_binding : mapset -> _ deoption2 let max_elt = lifting mmax_binding : mapset -> _ deoption2

That’ it! just read the output from map.out.ml. It only differs from set.in.ml by typesetting, choice of variables (more often omitted in the original file), and some auxiliary let bindings.