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.