This has been processed with:
| ocamlorn --library stdlib.mli \ --library set.lib.ml --input set.out.ml --lifting map.lif.ml > map.out.ml |
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.