Top

This file has been processed with:

ocamlorn --library stdlib.mli \ --library desorn_set.in.ml --input desorn_set.in.ml --lifting desorn_set.lif.ml \ > desorn_set.out.ml

Desornamentation of maps to sets

In another chapter, sets are ornamented to maps. Then, they are specialized back to sets via an ornamentation from the unit map type. Now, let’s see how we can also recover functions about sets from the maps ones with the reversed ornamentation.

type 'a box = Box of 'a 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 type cmp = Eq | Lt | Gt type elt = Elt val compare: elt -> elt -> cmp
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 = (* _2 *) 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 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 = (* _4 *) gte hl hr in MNode(l, a, x, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 ) 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))
type t = Empty | Node of t * elt * t * 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, _) let invalid_arg = lifting minvalid_arg : _ rev_setmap let height = lifting mheight : _ rev_setmap -> _ let create = lifting mcreate : _ rev_setmap -> _ rev_box2 -> _ rev_setmap -> _ rev_setmap let bal = lifting mbal : _ rev_setmap -> _ rev_box2 -> _ rev_setmap -> _ rev_setmap let add = lifting madd : _ rev_box2 -> _ rev_setmap -> _ rev_setmap let singleton = lifting msingleton : _ rev_box2 -> _ rev_setmap let min_binding = lifting mmin_binding : _ rev_setmap -> _ rev_option2 let max_binding = lifting mmax_binding : _ rev_setmap -> _ rev_option2
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(_, _, _, n) -> n in let hr = match r with | Empty -> i0 | Node(_, _, _, n) -> n in let x1 = gte hl hr in Node(l, v, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 ) let bal l vb r = match vb with | Box a -> let hl = match l with | Empty -> i0 | Node(_, _, _, n) -> n in let hr = match r with | Empty -> i0 | Node(_, _, _, n) -> n in begin match gt hl (plus hr i2) with | True -> begin match l with | Empty -> invalid_arg | Node(l, v, r1, _) -> begin match gte (height l) (height r1) with | True -> create l (Box v) (create r1 (Box a) r) | False -> begin match r1 with | Empty -> invalid_arg | Node(l1, v1, r1, _) -> create (create l (Box v) l1) (Box v1) (create r1 (Box a) r) end end end | False -> begin match gt hr (plus hl i2) with | True -> begin match r with | Empty -> invalid_arg | Node(l1, v, r, _) -> begin match gte (height r) (height l1) with | True -> create (create l (Box a) l1) (Box v) r | False -> begin match l1 with | Empty -> invalid_arg | Node(l1, v1, r1, _) -> create (create l (Box a) l1) (Box v1) (create r1 (Box v) r) end end end | False -> let x1 = gte hl hr in Node(l, a, r, match x1 with | True -> plus hl i1 | False -> plus hr i1 ) end end let rec add xb t = match xb with | Box a -> begin match t with | Empty -> Node(Empty, a, Empty, i1) | Node(l, v, r, _) -> begin match compare a v with | Eq -> t | Lt -> bal (add (Box a) l) (Box v) r | Gt -> bal l (Box v) (add (Box a) r) end end let singleton xb = match xb with | Box v -> Node(Empty, v, Empty, i1) let rec min_binding t = match t with | Empty -> None | Node(Empty, u, _, _) -> Some u | Node(Node(l, v, r, n), _, _, _) -> min_binding (Node(l, v, r, n)) let rec max_binding t = match t with | Empty -> None | Node(_, u, Empty, _) -> Some u | Node(_, _, Node(l, v, r, n), _) -> max_binding (Node(l, v, r, n))