From f0b19b99805aae0ec66da6650e0f3572716d7529 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 25 Jan 2015 20:07:29 +0100 Subject: [PATCH] remove a lot of stuff from containers.misc (see _oasis for details) --- _oasis | 18 +- benchs/bench_conv.ml | 94 ------ benchs/run_benchs.ml | 93 ------ src/misc/AVL.ml | 407 ----------------------- src/misc/AVL.mli | 106 ------ src/misc/bTree.ml | 382 --------------------- src/misc/bTree.mli | 90 ----- src/misc/bidir.ml | 135 -------- src/misc/bidir.mli | 86 ----- src/misc/cC.ml | 494 ---------------------------- src/misc/cC.mli | 105 ------ src/misc/cause.ml | 168 ---------- src/misc/cause.mli | 125 ------- src/misc/circList.ml | 135 -------- src/misc/circList.mli | 82 ----- src/misc/conv.ml | 621 ----------------------------------- src/misc/conv.mli | 260 --------------- src/misc/fHashtbl.ml | 503 ---------------------------- src/misc/fHashtbl.mli | 96 ------ src/misc/flatHashtbl.ml | 264 --------------- src/misc/flatHashtbl.mli | 97 ------ src/misc/hGraph.ml | 374 --------------------- src/misc/hGraph.mli | 127 ------- src/misc/hashset.ml | 75 ----- src/misc/hashset.mli | 64 ---- src/misc/heap.ml | 130 -------- src/misc/heap.mli | 58 ---- src/misc/iteratee.ml | 73 ---- src/misc/iteratee.mli | 44 --- src/misc/json.ml | 172 ---------- src/misc/json.mli | 62 ---- src/misc/parseReact.ml | 237 ------------- src/misc/parseReact.mli | 113 ------- src/misc/persistentGraph.ml | 372 --------------------- src/misc/persistentGraph.mli | 161 --------- src/misc/piCalculus.ml | 287 ---------------- src/misc/piCalculus.mli | 74 ----- src/misc/skipList.ml | 198 ----------- src/misc/skipList.mli | 60 ---- src/misc/splayMap.ml | 416 ----------------------- src/misc/splayMap.mli | 129 -------- src/misc/splayTree.ml | 140 -------- src/misc/splayTree.mli | 73 ---- src/misc/tTree.ml | 161 --------- src/misc/tTree.mli | 65 ---- src/misc/ty.ml | 175 ---------- src/misc/ty.mli | 84 ----- tests/run_tests.ml | 9 - tests/test_PiCalculus.ml | 35 -- tests/test_cc.ml | 93 ------ tests/test_fHashtbl.ml | 124 ------- tests/test_flatHashtbl.ml | 93 ------ tests/test_graph.ml | 88 ----- tests/test_heap.ml | 42 --- tests/test_splayMap.ml | 44 --- 55 files changed, 3 insertions(+), 8810 deletions(-) delete mode 100644 benchs/bench_conv.ml delete mode 100644 src/misc/AVL.ml delete mode 100644 src/misc/AVL.mli delete mode 100644 src/misc/bTree.ml delete mode 100644 src/misc/bTree.mli delete mode 100644 src/misc/bidir.ml delete mode 100644 src/misc/bidir.mli delete mode 100644 src/misc/cC.ml delete mode 100644 src/misc/cC.mli delete mode 100644 src/misc/cause.ml delete mode 100644 src/misc/cause.mli delete mode 100644 src/misc/circList.ml delete mode 100644 src/misc/circList.mli delete mode 100644 src/misc/conv.ml delete mode 100644 src/misc/conv.mli delete mode 100644 src/misc/fHashtbl.ml delete mode 100644 src/misc/fHashtbl.mli delete mode 100644 src/misc/flatHashtbl.ml delete mode 100644 src/misc/flatHashtbl.mli delete mode 100644 src/misc/hGraph.ml delete mode 100644 src/misc/hGraph.mli delete mode 100644 src/misc/hashset.ml delete mode 100644 src/misc/hashset.mli delete mode 100644 src/misc/heap.ml delete mode 100644 src/misc/heap.mli delete mode 100644 src/misc/iteratee.ml delete mode 100644 src/misc/iteratee.mli delete mode 100644 src/misc/json.ml delete mode 100644 src/misc/json.mli delete mode 100644 src/misc/parseReact.ml delete mode 100644 src/misc/parseReact.mli delete mode 100644 src/misc/persistentGraph.ml delete mode 100644 src/misc/persistentGraph.mli delete mode 100644 src/misc/piCalculus.ml delete mode 100644 src/misc/piCalculus.mli delete mode 100644 src/misc/skipList.ml delete mode 100644 src/misc/skipList.mli delete mode 100644 src/misc/splayMap.ml delete mode 100644 src/misc/splayMap.mli delete mode 100644 src/misc/splayTree.ml delete mode 100644 src/misc/splayTree.mli delete mode 100644 src/misc/tTree.ml delete mode 100644 src/misc/tTree.mli delete mode 100644 src/misc/ty.ml delete mode 100644 src/misc/ty.mli delete mode 100644 tests/test_PiCalculus.ml delete mode 100644 tests/test_cc.ml delete mode 100644 tests/test_fHashtbl.ml delete mode 100644 tests/test_flatHashtbl.ml delete mode 100644 tests/test_graph.ml delete mode 100644 tests/test_heap.ml delete mode 100644 tests/test_splayMap.ml diff --git a/_oasis b/_oasis index d3cd0174..15078c4f 100644 --- a/_oasis +++ b/_oasis @@ -22,7 +22,7 @@ Description: library full of experimental ideas (not stable, not necessarily usable). Flag "misc" - Description: Build the misc library, containing everything from the rotating kitchen sink to automatic banana distributors + Description: Build the misc library, with experimental modules still susceptible to change Default: true Flag "lwt" @@ -113,12 +113,8 @@ Library "containers_pervasives" Library "containers_misc" Path: src/misc Pack: true - Modules: FHashtbl, FlatHashtbl, Hashset, - Heap, LazyGraph, PersistentGraph, - PHashtbl, SkipList, SplayTree, SplayMap, Univ, - Bij, PiCalculus, RAL, UnionFind, SmallSet, AbsSet, CSM, - TTree, PrintBox, HGraph, Automaton, Conv, Bidir, Iteratee, - BTree, Ty, Cause, AVL, ParseReact + Modules: AbsSet, Automaton, Bij, CSM, LazyGraph, PHashtbl, + PrintBox, RAL, SmallSet, UnionFind, Univ BuildDepends: containers, containers.data FindlibName: misc FindlibParent: containers @@ -176,14 +172,6 @@ Executable bench_hash MainIs: bench_hash.ml BuildDepends: containers, containers.misc -Executable bench_conv - Path: benchs/ - Install: false - CompiledObject: native - Build$: flag(bench) - MainIs: bench_conv.ml - BuildDepends: containers, benchmark, gen - Executable test_levenshtein Path: tests/ Install: false diff --git a/benchs/bench_conv.ml b/benchs/bench_conv.ml deleted file mode 100644 index 7e958f36..00000000 --- a/benchs/bench_conv.ml +++ /dev/null @@ -1,94 +0,0 @@ -let conv_json = - let src = Conv.Source.(list_ (pair int_ int_)) in - fun x -> Conv.into src Conv.Json.sink x - -let manual_json = - fun l -> - `List (List.map (fun (a,b) -> `List [`Int a; `Int b]) l) - -let bench_list x = - let res = Benchmark.throughputN 5 - [ "conv", conv_json, x - ; "manual", manual_json, x - ] in - Benchmark.tabulate res - -(** benchmark points *) -module Point = Conv.Point - -let rec point_to_json_manual p = - let module P = Point in - `Assoc - [ "x", `Int p.P.x - ; "y", `Int p.P.y - ; "color", `String p.P.color - ; "prev", (match p.P.prev with - | None -> `String "none" - | Some p' -> point_to_json_manual p') - ] - -let list_point_to_json_manual l = - `List (List.map point_to_json_manual l) - -let conv_list_point_to_json l = - Conv.into (Conv.Source.list_ Point.source) Conv.Json.sink l - -let bench_point_list x = - let res = Benchmark.throughputN 5 - [ "conv", conv_list_point_to_json, x - ; "manual", list_point_to_json_manual, x - ] in - Benchmark.tabulate res - -(* conversion back from json *) -let rec point_of_json_manual (j:Conv.Json.t) = - let module P = Point in - match j with - | `Assoc l -> - let x = List.assoc "x" l in - let y = List.assoc "y" l in - let color = List.assoc "color" l in - let prev = List.assoc "prev" l in - let prev = match prev with - | `String "none" -> None - | `List [`String "some"; p'] -> Some (point_of_json_manual p') - | _ -> failwith "expected point" - in - begin match x, y, color with - | `Int x, `Int y, `String color -> P.({x;y;color;prev;}) - | _ -> failwith "expected point" - end - | _ -> failwith "expected point" - -let points_of_json_manual = function - | `List l -> List.map point_of_json_manual l - | _ -> failwith "expected list of points" - -let points_of_json_conv = - Conv.from Conv.Json.source (Conv.Sink.list_ Point.sink) - -let bench_point_list_back l = - let res = Benchmark.throughputN 5 - [ "conv", points_of_json_conv, l - ; "manual", points_of_json_manual, l - ] in - Benchmark.tabulate res - -let () = - Printf.printf "list of 5 elements...\n"; - bench_list [1,2; 3,4; 5,6; 7,8; 9,10]; - - let open CCFun in - let l = Gen.(1 -- 100 |> map (fun x->x,x) |> to_rev_list) in - Printf.printf "list of %d elements...\n" (List.length l); - bench_list l; - - let l = Gen.(repeat Point.p |> take 10 |> to_rev_list) in - Printf.printf "list of %d points...\n" (List.length l); - bench_point_list l; - - (* convert back from json *) - let l' = conv_list_point_to_json l in - Printf.printf "from JSON...\n"; - bench_point_list_back l'; - () diff --git a/benchs/run_benchs.ml b/benchs/run_benchs.ml index 01753b76..3c2e5e22 100644 --- a/benchs/run_benchs.ml +++ b/benchs/run_benchs.ml @@ -182,18 +182,6 @@ module Tbl = struct let hash i = i end) - module IFlatHashtbl = FlatHashtbl.Make(struct - type t = int - let equal i j = i = j - let hash i = i - end) - - module IFHashtbl = FHashtbl.Tree(struct - type t = int - let equal i j = i = j - let hash i = i - end) - module IPersistentHashtbl = CCPersistentHashtbl.Make(struct type t = int let equal i j = i = j @@ -232,27 +220,6 @@ module Tbl = struct done; h - let iflathashtbl_add n = - let h = IFlatHashtbl.create 50 in - for i = n downto 0 do - IFlatHashtbl.replace h i i; - done; - h - - let ifhashtbl_add n = - let h = ref (IFHashtbl.empty 32) in - for i = n downto 0 do - h := IFHashtbl.replace !h i i; - done; - !h - - let skiplist_add n = - let l = SkipList.create compare in - for i = n downto 0 do - SkipList.add l i i; - done; - l - let ipersistenthashtbl_add n = let h = ref (IPersistentHashtbl.create 32) in for i = n downto 0 do @@ -279,10 +246,7 @@ module Tbl = struct ["phashtbl_add", (fun n -> ignore (phashtbl_add n)), n; "hashtbl_add", (fun n -> ignore (hashtbl_add n)), n; "ihashtbl_add", (fun n -> ignore (ihashtbl_add n)), n; - "iflathashtbl_add", (fun n -> ignore (iflathashtbl_add n)), n; - "ifhashtbl_add", (fun n -> ignore (ifhashtbl_add n)), n; "ipersistenthashtbl_add", (fun n -> ignore (ipersistenthashtbl_add n)), n; - "skiplist_add", (fun n -> ignore (skiplist_add n)), n; "imap_add", (fun n -> ignore (imap_add n)), n; "ccflathashtbl_add", (fun n -> ignore (icchashtbl_add n)), n; ] @@ -317,26 +281,6 @@ module Tbl = struct done; h - let iflathashtbl_replace n = - let h = IFlatHashtbl.create 50 in - for i = 0 to n do - IFlatHashtbl.replace h i i; - done; - for i = n downto 0 do - IFlatHashtbl.replace h i i; - done; - h - - let ifhashtbl_replace n = - let h = ref (IFHashtbl.empty 32) in - for i = 0 to n do - h := IFHashtbl.replace !h i i; - done; - for i = n downto 0 do - h := IFHashtbl.replace !h i i; - done; - !h - let ipersistenthashtbl_replace n = let h = ref (IPersistentHashtbl.create 32) in for i = 0 to n do @@ -347,16 +291,6 @@ module Tbl = struct done; !h - let skiplist_replace n = - let l = SkipList.create compare in - for i = 0 to n do - SkipList.add l i i; - done; - for i = n downto 0 do - SkipList.add l i i; - done; - l - let imap_replace n = let h = ref IMap.empty in for i = 0 to n do @@ -382,10 +316,7 @@ module Tbl = struct ["phashtbl_replace", (fun n -> ignore (phashtbl_replace n)), n; "hashtbl_replace", (fun n -> ignore (hashtbl_replace n)), n; "ihashtbl_replace", (fun n -> ignore (ihashtbl_replace n)), n; - "iflathashtbl_replace", (fun n -> ignore (iflathashtbl_replace n)), n; - "ifhashtbl_replace", (fun n -> ignore (ifhashtbl_replace n)), n; "ipersistenthashtbl_replace", (fun n -> ignore (ipersistenthashtbl_replace n)), n; - "skiplist_replace", (fun n -> ignore (skiplist_replace n)), n; "imap_replace", (fun n -> ignore (imap_replace n)), n; "ccflathashtbl_replace", (fun n -> ignore (icchashtbl_replace n)), n; ] @@ -410,30 +341,12 @@ module Tbl = struct ignore (IHashtbl.find h i); done - let iflathashtbl_find h = - fun n -> - for i = 0 to n-1 do - ignore (IFlatHashtbl.find h i); - done - - let ifhashtbl_find h = - fun n -> - for i = 0 to n-1 do - ignore (IFHashtbl.find h i); - done - let ipersistenthashtbl_find h = fun n -> for i = 0 to n-1 do ignore (IPersistentHashtbl.find h i); done - let skiplist_find l = - fun n -> - for i = 0 to n-1 do - ignore (SkipList.find l i); - done - let array_find a = fun n -> for i = 0 to n-1 do @@ -456,10 +369,7 @@ module Tbl = struct let h = phashtbl_add n in let h' = hashtbl_add n in let h'' = ihashtbl_add n in - let h''' = iflathashtbl_add n in - let h'''' = ifhashtbl_add n in let h''''' = ipersistenthashtbl_add n in - let l = skiplist_add n in let a = Array.init n (fun i -> string_of_int i) in let m = imap_add n in let h'''''' = icchashtbl_add n in @@ -467,10 +377,7 @@ module Tbl = struct "phashtbl_find", (fun () -> phashtbl_find h n), (); "hashtbl_find", (fun () -> hashtbl_find h' n), (); "ihashtbl_find", (fun () -> ihashtbl_find h'' n), (); - "iflathashtbl_find", (fun () -> iflathashtbl_find h''' n), (); - "ifhashtbl_find", (fun () -> ifhashtbl_find h'''' n), (); "ipersistenthashtbl_find", (fun () -> ipersistenthashtbl_find h''''' n), (); - "skiplist_find", (fun () -> skiplist_find l n), (); "array_find", (fun () -> array_find a n), (); "imap_find", (fun () -> imap_find m n), (); "cchashtbl_find", (fun () -> icchashtbl_find h'''''' n), (); diff --git a/src/misc/AVL.ml b/src/misc/AVL.ml deleted file mode 100644 index b28a4b8f..00000000 --- a/src/misc/AVL.ml +++ /dev/null @@ -1,407 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 AVL trees} - -See https://en.wikipedia.org/wiki/AVL_tree *) - -type 'a comparator = 'a -> 'a -> int - -type ('a,'b) tree = - | Empty - | Node of ('a,'b) tree * 'a * 'b * ('a,'b) tree * int - -type ('a,'b) t = { - cmp: 'a comparator; - t: ('a,'b) tree -} - -let empty ~cmp = { cmp; t=Empty } - -let _height = function - | Empty -> 0 - | Node (_, _, _, _, h) -> h - -let _balance l r = _height l - _height r - -(* build the tree *) -let _make l x y r = - Node (l, x, y, r, 1 + max (_height l) (_height r)) - -let _singleton k v = _make Empty k v Empty -let singleton ~cmp k v = { cmp; t = _singleton k v } - -(* balance tree [t] *) -let _rebalance t = match t with - | Empty -> t - | Node (l, k1, v1, r, _) -> - let b = _balance l r in - if b = 2 - then (* left cases: left tree is too deep *) - match l with - | Empty -> assert false - | Node (ll, k2, v2, lr, _) -> - if _balance ll lr = -1 - then (* left-right *) - match lr with - | Empty -> assert false - | Node (lrl, k3, v3, lrr, _) -> - _make - (_make ll k2 v2 lrl) - k3 v3 - (_make lrr k1 v1 r) - else (* left-left *) - _make - ll k2 v2 - (_make lr k1 v1 r) - else if b = -2 (* right cases: symetric *) - then match r with - | Empty -> assert false - | Node (rl, k2, v2, rr, _) -> - if _balance rl rr = 1 - then (* right-left *) - match rl with - | Empty -> assert false - | Node (rll, k3, v3, rlr, _) -> - _make - (_make l k1 v1 rll) - k3 v3 - (_make rll k2 v2 rlr) - else (* right-right *) - _make - (_make l k1 v1 rl) - k2 v2 rr - else t - -let _make_balance l k v r = - _rebalance (_make l k v r) - -let rec _fold f acc t = match t with - | Empty -> acc - | Node (l, x, y, r, _) -> - let acc = _fold f acc l in - let acc = f acc x y in - _fold f acc r - -let fold f acc {t; _} = _fold f acc t - -let rec _for_all p t = match t with - | Empty -> true - | Node (l, x, y, r, _) -> - p x y && _for_all p l && _for_all p r - -let for_all p {t; _} = _for_all p t - -let rec _exists p t = match t with - | Empty -> false - | Node (l, x, y, r, _) -> - p x y || _exists p l || _exists p r - -let exists p {t; _} = _exists p t - -let rec _insert ~cmp t k v = match t with - | Empty -> _make Empty k v Empty - | Node (l, k1, v1, r, _) -> - let c = cmp k k1 in - if c < 0 - then _make_balance (_insert ~cmp l k v) k1 v1 r - else if c = 0 - then _make l k v r - else _make_balance l k1 v1 (_insert ~cmp r k v) - -let insert {cmp; t} k v = {cmp; t=_insert ~cmp t k v} - -(* remove the maximal value in the given tree (the only which only has a left - child), and return its key/value pair *) -let rec _remove_max t = match t with - | Empty -> assert false - | Node (l, k, v, Empty, _) -> - l, k, v - | Node (l, k, v, r, _) -> - let r', k', v' = _remove_max r in - _make_balance l k v r', k', v' - -exception NoSuchElement - -let _remove ~cmp t key = - let rec _remove t = match t with - | Empty -> raise NoSuchElement - | Node (l, k, v, r, _) -> - let c = cmp key k in - if c < 0 - then _make_balance (_remove l) k v r - else if c > 0 - then _make_balance l k v (_remove r) - else - (* interesting case: the node to remove is this one. We need - to find a replacing node, unless [l] is empty *) - match l with - | Empty -> r - | Node _ -> - let l', k', v' = _remove_max l in - _make_balance l' k' v' r - in - try _remove t - with NoSuchElement -> t (* element not found *) - -let remove {cmp; t} k = {cmp; t=_remove ~cmp t k} - -let _update ~cmp t key f = failwith "update: not implemented" -let update {cmp; t} = _update ~cmp t - -let rec _find_exn ~cmp t key = match t with - | Empty -> raise Not_found - | Node (l, k, v, r, _) -> - let c = cmp key k in - if c < 0 then _find_exn ~cmp l key - else if c > 0 then _find_exn ~cmp r key - else v -let find_exn {cmp; t} = _find_exn ~cmp t - -let find t key = - try Some (find_exn t key) - with Not_found -> None - -(* add k,v as strictly maximal element to t. [t] must not contain - any key >= k *) -let rec _add_max k v t = match t with - | Empty -> _singleton k v - | Node (l, k', v', r, _) -> - _make_balance l k' v' (_add_max k v r) - -(* same for minimal value *) -let rec _add_min k v t = match t with - | Empty -> _singleton k v - | Node (l, k', v', r, _) -> - _make_balance (_add_min k v l) k' v' r - -(* same as [_make] but doesn't assume anything about balance *) -let rec _join l k v r = - match l, r with - | Empty, _ -> _add_min k v r - | _, Empty -> _add_max k v l - | Node (ll, k1, v1, lr, h1), Node (rl, k2, v2, rr, h2) -> - if h1 + 1 < h2 - then (* r is much bigger. join l with rl *) - _make_balance (_join l k v rl) k2 v2 rr - else if h1 > h2 + 1 - then - _make_balance ll k1 v1 (_join lr k v r) - else (* balance uneeded *) - _make l k v r - -(* concat t1 and t2, where all keys of [t1] are smaller than - those of [t2] *) -let _concat t1 t2 = match t1, t2 with - | Empty, t - | t, Empty -> t - | _ -> - let t1', k, v = _remove_max t1 in - _join t1' k v t2 - -let rec _split ~cmp t key = match t with - | Empty -> Empty, None, Empty - | Node (l, k, v, r, _) -> - let c = cmp key k in - if c < 0 - then - let ll, result, lr = _split ~cmp l key in - ll, result, _join lr k v r - else if c > 0 - then - let rl, result, rr = _split ~cmp r key in - _join l k v rl, result, rr - else - l, Some v, r - -let split {cmp; t} k = - let (t,b,t') = _split ~cmp t k in - {cmp; t}, b, {cmp; t=t'} - -(* if k = Some v, join l k v r, else concat l v *) -let _concat_or_join l k result r = match result with - | None -> _concat l r - | Some v -> _join l k v r - -let rec _merge ~cmp f t1 t2 = match t1, t2 with - | Empty, Empty -> Empty - | Node (l1, k1, v1, r1, h1), _ when h1 >= _height t2 -> - let l2, result2, r2 = _split ~cmp t2 k1 in - let result = f k1 (Some v1) result2 in - let l = _merge ~cmp f l1 l2 in - let r = _merge ~cmp f r1 r2 in - _concat_or_join l k1 result r - | _, Node (l2, k2, v2, r2, _) -> - let l1, result1, r1 = _split ~cmp t1 k2 in - let result = f k2 result1 (Some v2) in - let l = _merge ~cmp f l1 l2 in - let r = _merge ~cmp f r1 r2 in - _concat_or_join l k2 result r - | _, Empty -> assert false (* h1 < heigth h2?? *) - -let merge f {cmp; t} {cmp=cmp'; t=t'} = - if(cmp != cmp') then invalid_arg "AVL.merge: trees wit different - comparison function"; - {cmp; t = _merge ~cmp f t t'} - -(* invariant: balanced *) -let rec invariant_balance t = match t with - | Empty -> true - | Node (l, _, _, r, _) -> - abs (_balance l r) < 2 - && invariant_balance l && invariant_balance r - -(* invariant: search tree *) -let rec invariant_search ~cmp t = match t with - | Empty -> true - | Node (l, x, _, r, _) -> - invariant_search ~cmp l && - invariant_search ~cmp r && - _for_all (fun x' _ -> cmp x' x < 0) l && - _for_all (fun x' _ -> cmp x' x > 0) r - -let of_list ~cmp l = - {cmp; t = List.fold_left (fun acc (x,y) -> _insert ~cmp acc x y) Empty l} - -let to_list {t; _} = - let rec aux acc t = match t with - | Empty -> acc - | Node (l, k, v, r, _) -> - let acc = aux acc r in - let acc = (k,v)::acc in - aux acc l - in aux [] t - -(** {2 Iterators} *) - -module type ITERATOR = sig - type 'a iter - - val after : ('a,'b) t -> 'a -> ('a * 'b) iter - val before : ('a,'b) t -> 'a -> ('a * 'b) iter - val iter : ('a,'b) t -> ('a * 'b) iter - val add : ('a,'b) t -> ('a * 'b) iter -> ('a,'b) t -end - -type ('a,'b) explore = - | Yield of 'a * 'b - | Explore of ('a, 'b) tree - -exception EndOfIter - -(* push the tree [t] on the stack [s] *) -let _push t s = match t with - | Empty -> s - | Node _ -> Explore t :: s - -(* push [t] on [s] with swapped children *) -let _push_swap t s = match t with - | Empty -> s - | Node (l, k, v, r,h) -> - Explore (Node(r,k,v,l,h)) :: s - -let _yield k v l = Yield (k,v) :: l - -let _has_next = function - | [] -> false - | _::_ -> true - -(* next key,value to yield *) -let rec _pop l = match l with - | [] -> raise EndOfIter - | (Yield (k,v))::l' -> k, v, l' - | (Explore Empty) :: _ -> assert false - | (Explore Node(l, k, v, r, _)::l') -> - _pop (_push l (_yield k v (_push r l'))) - -(* return the initial stack of trees to explore, that - are all "after" key (included) *) -let rec _after ~cmp stack t key = match t with - | Empty -> stack - | Node (l, k, v, r, _) -> - let c = cmp key k in - if c = 0 then _yield k v stack - else if c < 0 then _yield k v (_push r stack) - else _after ~cmp stack r key - -(* same as [_after] but for the range before *) -let rec _before~cmp stack t key = match t with - | Empty -> stack - | Node (l, k, v, r, _) -> - let c = cmp key k in - if c = 0 then _yield k v stack - else if c < 0 then _before ~cmp stack l key - else _yield k v (_push_swap l stack) - -module KList = struct - type 'a t = unit -> [ `Nil | `Cons of 'a * 'a t ] - - let rec _next (l:('a,'b) explore list) () = match l with - | [] -> `Nil - | _::_ -> - let k, v, l' = _pop l in - `Cons ((k,v), _next l') - - let iter {t; _} = _next (_push t []) - - let rec _add ~cmp t (l:'a t) = match l () with - | `Nil -> t - | `Cons ((k,v), l') -> - _add ~cmp (_insert ~cmp t k v) l' - - let add {cmp; t} l = {cmp; t=_add ~cmp t l} - - let after {cmp; t} key = _next (_after ~cmp [] t key) - - let before {cmp; t} key = _next (_before ~cmp [] t key) -end - -module Gen = struct - type 'a t = unit -> 'a option - - let _gen stack = - let stack = ref stack in - let next () = - match !stack with - | [] -> None - | l -> - let k, v, stack' = _pop l in - stack := stack'; - Some (k, v) - in next - - let iter {t; _} = _gen (_push t []) - - let rec _add ~cmp t gen = - match gen() with - | None -> t - | Some (k,v) -> _add ~cmp (_insert ~cmp t k v) gen - - let add {cmp; t} l = {cmp; t=_add ~cmp t l} - - let after {cmp; t} key = _gen (_after ~cmp [] t key) - let before {cmp; t} key = _gen (_before ~cmp [] t key) -end diff --git a/src/misc/AVL.mli b/src/misc/AVL.mli deleted file mode 100644 index 094ace1e..00000000 --- a/src/misc/AVL.mli +++ /dev/null @@ -1,106 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 AVL trees} *) - -type 'a comparator = 'a -> 'a -> int - -type ('a,'b) tree = private - | Empty - | Node of ('a,'b) tree * 'a * 'b * ('a,'b) tree * int - -type ('a,'b) t = private { - cmp: 'a comparator; - t: ('a,'b) tree -} - -val empty : cmp:'a comparator -> ('a,'b) t -(** Empty tree *) - -val singleton : cmp:'a comparator -> 'a -> 'b -> ('a,'b) t -(** Tree with a single node *) - -val fold : ('c -> 'a -> 'b -> 'c) -> 'c -> ('a,'b) t -> 'c -(** Fold on all key/value pairs in the tree *) - -val for_all : ('a -> 'b -> bool) -> ('a,'b) t -> bool -val exists : ('a -> 'b -> bool) -> ('a,'b) t -> bool - -val find : ('a,'b) t -> 'a -> 'b option -(** Find the value associated to the key, if any *) - -val find_exn : ('a,'b) t -> 'a -> 'b -(** @raise Not_found if the key is not present *) - -val insert : ('a,'b) t -> 'a -> 'b -> ('a,'b) t -(** Insertion in the tree *) - -val remove : ('a,'b) t -> 'a -> ('a,'b) t -(** Removal from the tree *) - -val update : ('a,'b) t -> 'a -> - ('b option -> ('a * 'b) option) -> ('a,'b) t -(** Update of the given key binding (subsumes [insert] and [remove]) *) - -val split : ('a,'b) t -> 'a -> - ('a,'b) t * 'b option * ('a,'b) t -(** [split ~cmp t k] splits [t] into a left part that - is smaller than [k], the possible binding of [k], - and a part bigger than [k]. *) - -val merge : - ('a -> 'b option -> 'c option -> 'd option) -> - ('a,'b) t -> ('a,'c) t -> ('a,'d) t -(** Merge two trees together, with the given function *) - -val of_list : cmp:'a comparator -> ('a * 'b) list -> ('a,'b) t -(** Add a list of bindings *) - -val to_list : ('a,'b) t -> ('a * 'b) list -(** List of bindings, in infix order *) - -(** {2 Iterators} *) - -module type ITERATOR = sig - type 'a iter - - val after : ('a,'b) t -> 'a -> ('a * 'b) iter - val before : ('a,'b) t -> 'a -> ('a * 'b) iter - val iter : ('a,'b) t -> ('a * 'b) iter - val add : ('a,'b) t -> ('a * 'b) iter -> ('a,'b) t -end - -module KList : sig - type 'a t = unit -> [ `Nil | `Cons of 'a * 'a t ] - - include ITERATOR with type 'a iter := 'a t -end - -module Gen : sig - type 'a t = unit -> 'a option - - include ITERATOR with type 'a iter := 'a t -end diff --git a/src/misc/bTree.ml b/src/misc/bTree.ml deleted file mode 100644 index 3ae1a43f..00000000 --- a/src/misc/bTree.ml +++ /dev/null @@ -1,382 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 B-Trees} *) - -type 'a sequence = ('a -> unit) -> unit -type 'a ktree = unit -> [`Nil | `Node of 'a * 'a ktree list] - -(** {2 signature} *) - -module type S = sig - type key - type 'a t - - val create : unit -> 'a t - (** Empty map *) - - val size : _ t -> int - (** Number of bindings *) - - val add : key -> 'a -> 'a t -> unit - (** Add a binding to the tree. Erases the old binding, if any *) - - val remove : key -> 'a t -> unit - (** Remove the given key, or does nothing if the key isn't present *) - - val get : key -> 'a t -> 'a option - (** Key lookup *) - - val get_exn : key -> 'a t -> 'a - (** Unsafe version of {!get}. - @raise Not_found if the key is not present *) - - val fold : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b - (** Fold on bindings *) - - val of_list : (key * 'a) list -> 'a t - val to_list : 'a t -> (key * 'a) list - val to_tree : 'a t -> (key * 'a) list ktree -end - -(** {2 Functor} *) - -module type ORDERED = sig - type t - val compare : t -> t -> int -end - -module Make(X : ORDERED) = struct - type key = X.t - - let _len_node = 1 lsl 6 - let _min_len = _len_node / 2 - - (* B-tree *) - type 'a tree = - | E - | N of 'a node - | L of 'a node - - (* an internal node, with children separated by keys/value pairs. - the [i]-th key of [n.keys] separates the subtrees [n.children.(i)] and - [n.children.(i+1)] *) - and 'a node = { - keys : key array; - values : 'a array; - children : 'a tree array; (* with one more slot *) - mutable size : int; (* number of bindings in the [key] *) - } - - type 'a t = { - mutable root : 'a tree; - mutable cardinal : int; - } - - let is_empty = function - | E -> true - | N _ - | L _ -> false - - let create () = { - root=E; - cardinal=0; - } - - (* build a new leaf with the given binding *) - let _make_singleton k v = { - keys = Array.make _len_node k; - values = Array.make _len_node v; - children = Array.make (_len_node+1) E; - size = 1; - } - - (* slice of [l] starting at indices [i], of length [len]. Only - copies inner children (between two keys in the range). *) - let _make_slice l i len = - assert (len>0); - assert (i+len<=l.size); - let k = l.keys.(i) and v = l.values.(i) in - let l' = { - keys = Array.make _len_node k; - values = Array.make _len_node v; - children = Array.make (_len_node+1) E; - size = len; - } in - Array.blit l.keys i l'.keys 0 len; - Array.blit l.values i l'.values 0 len; - Array.blit l.children (i+1) l'.children 1 (len-1); - l' - - let _full_node n = n.size = _len_node - let _empty_node n = n.size = 0 - - let size t = t.cardinal - - let rec _fold f acc t = match t with - | E -> () - | L n -> - for i=0 to n.size-1 do - assert (n.children.(i) = E); - acc := f !acc n.keys.(i) n.values.(i) - done - | N n -> - for i=0 to n.size-1 do - _fold f acc n.children.(i); - acc := f !acc n.keys.(i) n.values.(i); - done; - _fold f acc n.children.(n.size) - - let fold f acc t = - let acc = ref acc in - _fold f acc t.root; - !acc - - type lookup_result = - | At of int - | After of int - - (* lookup in a node. *) - let rec _lookup_rec l k i = - if i = l.size then After (i-1) - else match X.compare k l.keys.(i) with - | 0 -> At i - | n when n<0 -> After (i-1) - | _ -> _lookup_rec l k (i+1) - - let _lookup l k = - if l.size = 0 then After ~-1 - else _lookup_rec l k 0 - - (* recursive lookup in a tree *) - let rec _get_exn k t = match t with - | E -> raise Not_found - | L l -> - begin match _lookup l k with - | At i -> l.values.(i) - | After _ -> raise Not_found - end - | N n -> - assert (n.size > 0); - match _lookup n k with - | At i -> n.values.(i) - | After i -> _get_exn k n.children.(i+1) - - let get_exn k t = _get_exn k t.root - - let get k t = - try Some (_get_exn k t.root) - with Not_found -> None - - (* sorted insertion into a leaf that has room and doesn't contain the key *) - let _insert_sorted l k v i = - assert (not (_full_node l)); - (* make room by shifting to the right *) - let len = l.size - i in - assert (i+len<=l.size); - assert (len>=0); - Array.blit l.keys i l.keys (i+1) len; - Array.blit l.values i l.values (i+1) len; - l.keys.(i) <- k; - l.values.(i) <- v; - l.size <- l.size + 1; - - (* what happens when we insert a value *) - type 'a add_result = - | NewTree of 'a tree - | Add - | Replace - | Split of 'a tree * key * 'a * 'a tree - - let _add_leaf k v t l = - match _lookup l k with - | At i -> - l.values.(i) <- v; - Replace - | After i -> - if _full_node l - then ( - (* split. [k'] and [v']: separator for split *) - let j = _len_node/2 in - let left = _make_slice l 0 j in - let right = _make_slice l (j+1) (_len_node-j-1) in - (* insert in proper sub-leaf *) - (if i+1=0); - Array.blit n.keys i n.keys (i+1) len; - Array.blit n.values i n.values (i+1) len; - Array.blit n.children (i+1) n.children (i+2) len; - n.keys.(i) <- k; - n.values.(i) <- v; - (* erase subtree with sub1,sub2 *) - n.children.(i) <- sub1; - n.children.(i+1) <- sub2; - n.size <- n.size + 1; - () - - (* return a boolean indicating whether the key was already - present, and a new tree. *) - let rec _add k v t = match t with - | E -> NewTree (L (_make_singleton k v)) - | L l -> _add_leaf k v t l - | N n -> - match _lookup n k with - | At i -> - n.values.(i) <- v; - Replace - | After i -> - assert (X.compare n.keys.(i) k < 0); - let sub = n.children.(i+1) in - match _add k v sub with - | NewTree t' -> - n.children.(i+1) <- t'; - Add - | Add -> Add - | Replace -> Replace - | Split (sub1, k', v', sub2) -> - assert (X.compare n.keys.(i) k' < 0); - if _full_node n - then ( - (* split this node too! *) - let j = _len_node/2 in - let left = _make_slice n 0 j in - let right = _make_slice n (j+1) (_len_node-j-1) in - left.children.(0) <- n.children.(0); - right.children.(_len_node-j) <- n.children.(_len_node); - (* insert k' and subtrees in the correct tree *) - (if i - t.cardinal <- t.cardinal + 1; - t.root <- t' - | Replace -> () - | Add -> t.cardinal <- t.cardinal + 1 - | Split (sub1, k, v, sub2) -> - (* make a new root with one child *) - let n = _make_singleton k v in - n.children.(0) <- sub1; - n.children.(1) <- sub2; - t.cardinal <- t.cardinal + 1; - t.root <- N n - - let of_list l = - let t = create() in - List.iter (fun (k, v) -> add k v t) l; - t - - let to_list t = - List.rev (fold (fun acc k v -> (k,v)::acc) [] t) - - let rec _to_tree t () = match t with - | E -> `Nil - | L n - | N n -> - let l = ref [] and children = ref [] in - for i=0 to n.size-1 do - l := (n.keys.(i),n.values.(i)) :: !l; - children := n.children.(i) :: !children - done; - children := n.children.(n.size) :: !children; - children := List.filter (function E -> false | _ -> true) !children; - `Node (List.rev !l, List.rev_map _to_tree !children) - - let to_tree t = _to_tree t.root - - (*$T - let module T = Make(CCInt) in \ - let t = T.of_list (CCList.(1--1000) |> List.map (fun x->x, string_of_int x)) in \ - T.get 1 t = Some "1" - let module T = Make(CCInt) in \ - let t = T.of_list (CCList.(1--1000) |> List.map (fun x->x, string_of_int x)) in \ - T.get 3 t = Some "3" - let module T = Make(CCInt) in \ - let t = T.of_list (CCList.(1--100) |> List.map (fun x->x, string_of_int x)) in \ - T.get 400 t = None - *) - - (* remove the key if present. TODO - let rec _remove k t = match t with - | E -> false, E - | N n -> - assert (n.size > 0); - if X.compare k (_min_key n) < 0 - then ( - let removed, left' = _remove k n.left in - n.left <- left'; - n.depth <- 1+max (_depth n.left) (_depth n.right); - removed, _balance t - ) else if X.compare k (_max_key n) > 0 - then ( - let removed, right' = _remove k n.right in - n.right <- right'; - n.depth <- 1+max (_depth n.left) (_depth n.right); - removed, _balance t - ) - else try - let i = _lookup n k 0 in - if n.size = 1 (* TODO: actually minimal threshold should be higher *) - then true, E - else ( - let len = n.size - i in - Array.blit n.keys (i+1) n.keys i len; - Array.blit n.values (i+1) n.values i len; - true, t - ) - with Not_found -> - false, t (* not to be removed *) - *) - - let remove k t = assert false (* TODO *) -end diff --git a/src/misc/bTree.mli b/src/misc/bTree.mli deleted file mode 100644 index 0d068d9c..00000000 --- a/src/misc/bTree.mli +++ /dev/null @@ -1,90 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 B-Trees} - -Shallow, cache-friendly associative data structure. -See {{: https://en.wikipedia.org/wiki/B-tree} wikipedia}. - -Not thread-safe. *) - -type 'a sequence = ('a -> unit) -> unit -type 'a ktree = unit -> [`Nil | `Node of 'a * 'a ktree list] - -(** {2 signature} *) - -module type S = sig - type key - type 'a t - - val create : unit -> 'a t - (** Empty map *) - - val size : _ t -> int - (** Number of bindings *) - - val add : key -> 'a -> 'a t -> unit - (** Add a binding to the tree. Erases the old binding, if any *) - - val remove : key -> 'a t -> unit - (** Remove the given key, or does nothing if the key isn't present *) - - val get : key -> 'a t -> 'a option - (** Key lookup *) - - val get_exn : key -> 'a t -> 'a - (** Unsafe version of {!get}. - @raise Not_found if the key is not present *) - - val fold : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b - (** Fold on bindings *) - - val of_list : (key * 'a) list -> 'a t - val to_list : 'a t -> (key * 'a) list - val to_tree : 'a t -> (key * 'a) list ktree -end - -(** {2 Functor that builds trees for comparable keys} *) - -module type ORDERED = sig - type t - val compare : t -> t -> int -end - -module Make(X : ORDERED) : S with type key = X.t - -(* note: to print a B-tree in dot: -{[ -let t = some_btree in -let t' = CCKTree.map - (fun t -> - [`Shape "square"; - `Label (CCPrint.to_string (CCList.pp (CCPair.pp CCInt.pp CCString.pp)) t)] - ) (T.to_tree t);; -CCPrint.to_file "/tmp/some_file.dot" "%a\n" (CCKTree.Dot.pp_single "btree") t'; -]} -*) - diff --git a/src/misc/bidir.ml b/src/misc/bidir.ml deleted file mode 100644 index 3ba5d687..00000000 --- a/src/misc/bidir.ml +++ /dev/null @@ -1,135 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Bidirectional Iterators} - -Iterators that can be traversed in both directions *) - -type 'a t = - | Nil - | Cons of (unit -> 'a t) * 'a * (unit -> 'a t) - -let nil = Nil - -let ret_nil () = Nil - -let insert_before x = function - | Nil -> Cons (ret_nil, x, ret_nil) - | Cons (l, y, r) -> - let rec cur() = - Cons (l, x, (fun () -> Cons (cur, y, r))) - in cur() - -let insert_after x = function - | Nil -> Cons (ret_nil, x, ret_nil) - | Cons (l, y, r) -> - let rec cur() = - Cons (l, y, (fun () -> Cons (cur, x, r))) - in cur() - -let left = function - | Nil -> Nil - | Cons (l, _, _) -> l() - -let right = function - | Nil -> Nil - | Cons (_, _, r) -> r() - -let graft_before ~inner outer = - match outer with - | Nil -> inner - | Cons (l_out, x_out, r_out) -> - let rec right ret_left inner () = match inner () with - | Nil -> Cons(ret_left, x_out, r_out) (* yield x_out *) - | Cons (_, x_in, r_in) -> - let rec cur() = - Cons (ret_left, x_in, right cur r_in) - in cur() - and left ret_right inner () = match inner () with - | Nil -> l_out() (* yield same as l_out *) - | Cons (l_in, x_in, _) -> - let rec cur() = - Cons (left cur l_in, x_in, ret_right) - in cur() - and start() = match inner with - | Nil -> outer - | Cons (l, x, r) -> Cons (left start l, x, right start r) - in - start() - -let graft_after ~inner outer = - graft_before ~inner (right outer) - -let rev = function - | Nil -> Nil - | Cons (l, x, r) -> - Cons (r, x, l) - -(** {2 Right-iteration} *) - -let rec fold f acc = function - | Nil -> acc - | Cons (_, x, l) -> - let acc = f acc x in - fold f acc (l ()) - -let to_rev_list l = - fold (fun acc x -> x::acc) [] l - -let to_list l = - List.rev (to_rev_list l) - -let rec __of_list prev l () = match l with - | [] -> Nil - | x::l -> - let rec cur() = - Cons (prev, x, __of_list cur l) - in cur() - -let of_list l = __of_list ret_nil l () - -(** {2 Full constructor} *) - -let of_lists l x r = - let rec cur() = - Cons (__of_list cur l, x, __of_list cur r) - in cur() - -(** {2 Moves} *) - -let left_n n b = - let rec traverse acc n b = match n, b with - | 0, _ - | _, Nil -> acc, b - | _, Cons (l, x, _) -> traverse (x::acc) (n-1) (l()) - in traverse [] n b - -let right_n n b = - let rec traverse acc n b = match n, b with - | 0, _ - | _, Nil -> acc, b - | _, Cons (_, x, r) -> traverse (x::acc) (n-1) (r()) - in traverse [] n b diff --git a/src/misc/bidir.mli b/src/misc/bidir.mli deleted file mode 100644 index dee7b0e9..00000000 --- a/src/misc/bidir.mli +++ /dev/null @@ -1,86 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Bidirectional Iterators} - -Iterators that can be traversed in both directions *) - -type 'a t = - | Nil - | Cons of (unit -> 'a t) * 'a * (unit -> 'a t) - -val nil : 'a t - (** Empty iterator *) - -val insert_before : 'a -> 'a t -> 'a t - (** Insert the given element before the current slot in the - * given iterator *) - -val insert_after : 'a -> 'a t -> 'a t - (** Insert the element right after the current one *) - -val left : 'a t -> 'a t - (** Go left once. Doesn't do anything on empty iterator. *) - -val right : 'a t -> 'a t - (** Go right once. Doesn't do anything on empty iterator. *) - -val graft_before : inner:'a t -> 'a t -> 'a t - (** [insert ~inner outer] grafts [inner] just before the current element of - [outer]. *) - -val graft_after : inner:'a t -> 'a t -> 'a t - -val rev : 'a t -> 'a t - (** Reverse the order of iteration *) - -(** {2 Right-iteration} -traverse the right part of the iterator. traversing the left is -easily done with {!rev}. *) - -val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a - (** Fold on elements starting from the current one, to the right end *) - -val to_rev_list : 'a t -> 'a list - (** To reverse list *) - -val to_list : 'a t -> 'a list - (** Conversion to list. Only traverse the right part. *) - -val of_list : 'a list -> 'a t - (** Iterate on the list *) - -(** {2 Full constructor} *) - -val of_lists : 'a list -> 'a -> 'a list -> 'a t - -(** {2 Moves} *) - -val left_n : int -> 'a t -> 'a list * 'a t - (** Move left n times, and return the n elements traversed (at most), - from left-most one to right_most one.*) - -val right_n : int -> 'a t -> 'a list * 'a t diff --git a/src/misc/cC.ml b/src/misc/cC.ml deleted file mode 100644 index c1273eef..00000000 --- a/src/misc/cC.ml +++ /dev/null @@ -1,494 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Congruence Closure} *) - -(** This implementation follows more or less the paper - "fast congruence closure and extensions" by Nieuwenhuis & Oliveras. - It uses semi-persistent data structures but still thrives for efficiency. *) - -(** {2 Curryfied terms} *) - -module type CurryfiedTerm = sig - type symbol - type t = private { - shape : shape; (** Which kind of term is it? *) - tag : int; (** Unique ID *) - } (** A curryfied term *) - and shape = private - | Const of symbol (** Constant *) - | Apply of t * t (** Curryfied application *) - - val mk_const : symbol -> t - val mk_app : t -> t -> t - val get_id : t -> int - val eq : t -> t -> bool - val pp_skel : out_channel -> t -> unit (* print tags recursively *) -end - -module Curryfy(X : Hashtbl.HashedType) = struct - type symbol = X.t - type t = { - shape : shape; (** Which kind of term is it? *) - tag : int; (** Unique ID *) - } - and shape = - | Const of symbol (** Constant *) - | Apply of t * t (** Curryfied application *) - - type term = t - - module WE = Weak.Make(struct - type t = term - let equal a b = match a.shape, b.shape with - | Const ia, Const ib -> X.equal ia ib - | Apply (a1,a2), Apply (b1,b2) -> a1 == b1 && a2 == b2 - | _ -> false - let hash a = match a.shape with - | Const i -> X.hash i - | Apply (a, b) -> a.tag * 65599 + b.tag - end) - - let __table = WE.create 10001 - let count = ref 0 - - let hashcons t = - let t' = WE.merge __table t in - (if t == t' then incr count); - t' - - let mk_const i = - let t = {shape=Const i; tag= !count; } in - hashcons t - - let mk_app a b = - let t = {shape=Apply (a, b); tag= !count; } in - hashcons t - - let get_id t = t.tag - - let eq t1 t2 = t1 == t2 - - let rec pp_skel oc t = match t.shape with - | Const _ -> Printf.fprintf oc "%d" t.tag - | Apply (t1, t2) -> - Printf.fprintf oc "(%a %a):%d" pp_skel t1 pp_skel t2 t.tag -end - -(** {2 Congruence Closure} *) - -module type S = sig - module CT : CurryfiedTerm - - type t - (** Congruence Closure instance *) - - exception Inconsistent of t * CT.t * CT.t * CT.t * CT.t - (** Exception raised when equality and inequality constraints are - inconsistent. [Inconsistent (a, b, a', b')] means that [a=b, a=a', b=b'] in - the congruence closure, but [a' != b'] was asserted before. *) - - val create : int -> t - (** Create an empty CC of given size *) - - val eq : t -> CT.t -> CT.t -> bool - (** Check whether the two terms are equal *) - - val merge : t -> CT.t -> CT.t -> t - (** Assert that the two terms are equal (may raise Inconsistent) *) - - val distinct : t -> CT.t -> CT.t -> t - (** Assert that the two given terms are distinct (may raise Inconsistent) *) - - type action = - | Merge of CT.t * CT.t - | Distinct of CT.t * CT.t - (** Action that can be performed on the CC *) - - val do_action : t -> action -> t - (** Perform the given action (may raise Inconsistent) *) - - val can_eq : t -> CT.t -> CT.t -> bool - (** Check whether the two terms can be equal *) - - val iter_equiv_class : t -> CT.t -> (CT.t -> unit) -> unit - (** Iterate on terms that are congruent to the given term *) - - type explanation = - | ByCongruence of CT.t * CT.t (* direct congruence of terms *) - | ByMerge of CT.t * CT.t (* user merge of terms *) - - val explain : t -> CT.t -> CT.t -> explanation list - (** Explain why those two terms are equal (assuming they are, - otherwise raises Invalid_argument) by returning a list - of merges. *) -end - -module Make(T : CurryfiedTerm) = struct - module CT = T - module BV = Puf.PBitVector - module Puf = Puf.Make(CT) - - module HashedCT = struct - type t = CT.t - let equal t1 t2 = t1.CT.tag = t2.CT.tag - let hash t = t.CT.tag - end - - (* Persistent Hashtable on curryfied terms *) - module THashtbl = CCPersistentHashtbl.Make(HashedCT) - - (* Persistent Hashtable on pairs of curryfied terms *) - module T2Hashtbl = CCPersistentHashtbl.Make(struct - type t = CT.t * CT.t - let equal (t1,t1') (t2,t2') = t1.CT.tag = t2.CT.tag && t1'.CT.tag = t2'.CT.tag - let hash (t,t') = t.CT.tag * 65599 + t'.CT.tag - end) - - type t = { - uf : pending_eqn Puf.t; (* representatives for terms *) - defined : BV.t; (* is the term defined? *) - use : eqn list THashtbl.t; (* for all repr a, a -> all a@b=c and b@a=c *) - lookup : eqn T2Hashtbl.t; (* for all reprs a,b, some a@b=c (if any) *) - inconsistent : (CT.t * CT.t) option; - } (** Congruence Closure data structure *) - and eqn = - | EqnSimple of CT.t * CT.t (* t1 = t2 *) - | EqnApply of CT.t * CT.t * CT.t (* (t1 @ t2) = t3 *) - (** Equation between two terms *) - and pending_eqn = - | PendingSimple of eqn - | PendingDouble of eqn * eqn - - exception Inconsistent of t * CT.t * CT.t * CT.t * CT.t - (** Exception raised when equality and inequality constraints are - inconsistent. [Inconsistent (a, b, a', b')] means that [a=b, a=a', b=b'] in - the congruence closure, but [a' != b'] was asserted before. *) - - (** Create an empty CC of given size *) - let create size = - { uf = Puf.create size; - defined = BV.make 3; - use = THashtbl.create size; - lookup = T2Hashtbl.create size; - inconsistent = None; - } - - let mem cc t = - BV.get cc.defined t.CT.tag - - let is_const t = match t.CT.shape with - | CT.Const _ -> true - | CT.Apply _ -> false - - (** Merge equations in the congruence closure structure. [q] is a list - of [eqn], processed in FIFO order. May raise Inconsistent. *) - let rec merge cc eqn = match eqn with - | EqnSimple (a, b) -> - (* a=b, just propagate *) - propagate cc [PendingSimple eqn] - | EqnApply (a1, a2, a) -> - (* (a1 @ a2) = a *) - let a1' = Puf.find cc.uf a1 in - let a2' = Puf.find cc.uf a2 in - begin try - (* eqn' is (b1 @ b2) = b for some b1=a1', b2=a2' *) - let eqn' = T2Hashtbl.find cc.lookup (a1', a2') in - (* merge a and b because of eqn and eqn' *) - propagate cc [PendingDouble (eqn, eqn')] - with Not_found -> - (* remember that a1' @ a2' = a *) - let lookup = T2Hashtbl.replace cc.lookup (a1', a2') eqn in - let use_a1' = try THashtbl.find cc.use a1' with Not_found -> [] in - let use_a2' = try THashtbl.find cc.use a2' with Not_found -> [] in - let use = THashtbl.replace cc.use a1' (eqn::use_a1') in - let use = THashtbl.replace use a2' (eqn::use_a2') in - { cc with use; lookup; } - end - (* propagate: merge pending equations *) - and propagate cc eqns = - let pending = ref eqns in - let uf = ref cc.uf in - let use = ref cc.use in - let lookup = ref cc.lookup in - (* process each pending equation *) - while !pending <> [] do - let eqn = List.hd !pending in - pending := List.tl !pending; - (* extract the two merged terms *) - let a, b = match eqn with - | PendingSimple (EqnSimple (a, b)) -> a, b - | PendingDouble (EqnApply (a1,a2,a), EqnApply (b1,b2,b)) -> a, b - | _ -> assert false - in - let a' = Puf.find !uf a in - let b' = Puf.find !uf b in - if not (CT.eq a' b') then begin - let use_a' = try THashtbl.find !use a' with Not_found -> [] in - let use_b' = try THashtbl.find !use b' with Not_found -> [] in - (* merge a and b's equivalence classes *) - (* Format.printf "merge %d %d@." a.CT.tag b.CT.tag; *) - uf := Puf.union !uf a b eqn; - (* check which of [a'] and [b'] is the new representative. [repr] is - the new representative, and [other] is the former representative *) - let repr = Puf.find !uf a' in - let use_repr = ref (if CT.eq repr a' then use_a' else use_b') in - let use_other = if CT.eq repr a' then use_b' else use_a' in - (* consider all c1@c2=c in use(a') *) - List.iter - (fun eqn -> match eqn with - | EqnSimple _ -> () - | EqnApply (c1, c2, c) -> - let c1' = Puf.find !uf c1 in - let c2' = Puf.find !uf c2 in - begin try - let eqn' = T2Hashtbl.find !lookup (c1', c2') in - (* merge eqn with eqn', by congruence *) - pending := (PendingDouble (eqn,eqn')) :: !pending - with Not_found -> - lookup := T2Hashtbl.replace !lookup (c1', c2') eqn; - use_repr := eqn :: !use_repr; - end) - use_other; - (* update use list of [repr] *) - use := THashtbl.replace !use repr !use_repr; - (* check for inconsistencies *) - match Puf.inconsistent !uf with - | None -> () (* consistent *) - | Some (t1, t2, t1', t2') -> - (* inconsistent *) - let cc = { cc with use= !use; lookup= !lookup; uf= !uf; } in - raise (Inconsistent (cc, t1, t2, t1', t2')) - end - done; - let cc = { cc with use= !use; lookup= !lookup; uf= !uf; } in - cc - - (** Add the given term to the CC *) - let rec add cc t = - match t.CT.shape with - | CT.Const _ -> - cc (* always trivially defined *) - | CT.Apply (t1, t2) -> - if BV.get cc.defined t.CT.tag - then cc (* already defined *) - else begin - (* note that [t] is defined, add it to the UF to avoid GC *) - let defined = BV.set_true cc.defined t.CT.tag in - let cc = {cc with defined; } in - (* recursive add. invariant: if a term is added, then its subterms - also are (hence the base case of constants or already added terms). *) - let cc = add cc t1 in - let cc = add cc t2 in - let cc = merge cc (EqnApply (t1, t2, t)) in - cc - end - - (** Check whether the two terms are equal *) - let eq cc t1 t2 = - let cc = add (add cc t1) t2 in - let t1' = Puf.find cc.uf t1 in - let t2' = Puf.find cc.uf t2 in - CT.eq t1' t2' - - (** Assert that the two terms are equal (may raise Inconsistent) *) - let merge cc t1 t2 = - let cc = add (add cc t1) t2 in - merge cc (EqnSimple (t1, t2)) - - (** Assert that the two given terms are distinct (may raise Inconsistent) *) - let distinct cc t1 t2 = - let cc = add (add cc t1) t2 in - let t1' = Puf.find cc.uf t1 in - let t2' = Puf.find cc.uf t2 in - if CT.eq t1' t2' - then raise (Inconsistent (cc, t1', t2', t1, t2)) (* they are equal, fail *) - else - (* remember that they should not become equal *) - let uf = Puf.distinct cc.uf t1 t2 in - { cc with uf; } - - type action = - | Merge of CT.t * CT.t - | Distinct of CT.t * CT.t - (** Action that can be performed on the CC *) - - let do_action cc action = match action with - | Merge (t1, t2) -> merge cc t1 t2 - | Distinct (t1, t2) -> distinct cc t1 t2 - - (** Check whether the two terms can be equal *) - let can_eq cc t1 t2 = - let cc = add (add cc t1) t2 in - not (Puf.must_be_distinct cc.uf t1 t2) - - (** Iterate on terms that are congruent to the given term *) - let iter_equiv_class cc t f = - Puf.iter_equiv_class cc.uf t f - - (** {3 Auxilliary Union-find for explanations} *) - - module SparseUF = struct - module H = Hashtbl.Make(HashedCT) - - type t = uf_ref H.t - and uf_ref = { - term : CT.t; - mutable parent : CT.t; - mutable highest_node : CT.t; - } (** Union-find reference *) - - let create size = H.create size - - let get_ref uf t = - try H.find uf t - with Not_found -> - let r_t = { term=t; parent=t; highest_node=t; } in - H.add uf t r_t; - r_t - - let rec find_ref uf r_t = - if CT.eq r_t.parent r_t.term - then r_t (* fixpoint *) - else - let r_t' = get_ref uf r_t.parent in - find_ref uf r_t' (* recurse (no path compression) *) - - let find uf t = - try - let r_t = H.find uf t in - (find_ref uf r_t).term - with Not_found -> - t - - let eq uf t1 t2 = - CT.eq (find uf t1) (find uf t2) - - let highest_node uf t = - try - let r_t = H.find uf t in - (find_ref uf r_t).highest_node - with Not_found -> - t - - (* oriented union (t1 -> t2), assuming t2 is "higher" than t1 *) - let union uf t1 t2 = - let r_t1' = find_ref uf (get_ref uf t1) in - let r_t2' = find_ref uf (get_ref uf t2) in - r_t1'.parent <- r_t2'.term - end - - (** {3 Producing explanations} *) - - type explanation = - | ByCongruence of CT.t * CT.t (* direct congruence of terms *) - | ByMerge of CT.t * CT.t (* user merge of terms *) - - (** Explain why those two terms are equal (they must be) *) - let explain cc t1 t2 = - assert (eq cc t1 t2); - (* keeps track of which equalities are already explained *) - let explained = SparseUF.create 5 in - let explanations = ref [] in - (* equations waiting to be explained *) - let pending = Queue.create () in - Queue.push (t1,t2) pending; - (* explain why a=c, where c is the root of the proof forest a belongs to *) - let rec explain_along a c = - let a' = SparseUF.highest_node explained a in - if CT.eq a' c then () - else match Puf.explain_step cc.uf a' with - | None -> assert (CT.eq a' c) - | Some (b, e) -> - (* a->b on the path from a to c *) - begin match e with - | PendingSimple (EqnSimple (a',b')) -> - explanations := ByMerge (a', b') :: !explanations - | PendingDouble (EqnApply (a1, a2, a'), EqnApply (b1, b2, b')) -> - explanations := ByCongruence (a', b') :: !explanations; - Queue.push (a1, b1) pending; - Queue.push (a2, b2) pending; - | _ -> assert false - end; - (* now a' = b is justified *) - SparseUF.union explained a' b; - (* recurse *) - let new_a = SparseUF.highest_node explained b in - explain_along new_a c - in - (* process pending equations *) - while not (Queue.is_empty pending) do - let a, b = Queue.pop pending in - if SparseUF.eq explained a b - then () - else begin - let c = Puf.common_ancestor cc.uf a b in - explain_along a c; - explain_along b c; - end - done; - !explanations -end - -module StrTerm = Curryfy(struct - type t = string - let equal s1 s2 = s1 = s2 - let hash s = Hashtbl.hash s -end) - -module StrCC = Make(StrTerm) - -let lex str = - let lexer = Genlex.make_lexer ["("; ")"] in - lexer (Stream.of_string str) - -let parse str = - let stream = lex str in - let rec parse_term () = - match Stream.peek stream with - | Some (Genlex.Kwd "(") -> - Stream.junk stream; - let t1 = parse_term () in - let t2 = parse_term () in - begin match Stream.peek stream with - | Some (Genlex.Kwd ")") -> - Stream.junk stream; - StrTerm.mk_app t1 t2 (* end apply *) - | _ -> raise (Stream.Error "expected )") - end - | Some (Genlex.Ident s) -> - Stream.junk stream; - StrTerm.mk_const s - | _ -> raise (Stream.Error "expected term") - in - parse_term () - -let rec pp fmt t = - match t.StrTerm.shape with - | StrTerm.Const s -> - Format.fprintf fmt "%s:%d" s t.StrTerm.tag - | StrTerm.Apply (t1, t2) -> - Format.fprintf fmt "(%a %a):%d" pp t1 pp t2 t.StrTerm.tag - diff --git a/src/misc/cC.mli b/src/misc/cC.mli deleted file mode 100644 index 89a1b031..00000000 --- a/src/misc/cC.mli +++ /dev/null @@ -1,105 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Congruence Closure} *) - -(** {2 Curryfied terms} *) - -module type CurryfiedTerm = sig - type symbol - type t = private { - shape : shape; (** Which kind of term is it? *) - tag : int; (** Unique ID *) - } (** A curryfied term *) - and shape = private - | Const of symbol (** Constant *) - | Apply of t * t (** Curryfied application *) - - val mk_const : symbol -> t - val mk_app : t -> t -> t - val get_id : t -> int - val eq : t -> t -> bool - val pp_skel : out_channel -> t -> unit (* print tags recursively *) -end - -module Curryfy(X : Hashtbl.HashedType) : CurryfiedTerm with type symbol = X.t - -(** {2 Congruence Closure} *) - -module type S = sig - module CT : CurryfiedTerm - - type t - (** Congruence Closure instance *) - - exception Inconsistent of t * CT.t * CT.t * CT.t * CT.t - (** Exception raised when equality and inequality constraints are - inconsistent. [Inconsistent (a, b, a', b')] means that [a=b, a=a', b=b'] in - the congruence closure, but [a' != b'] was asserted before. *) - - val create : int -> t - (** Create an empty CC of given size *) - - val eq : t -> CT.t -> CT.t -> bool - (** Check whether the two terms are equal *) - - val merge : t -> CT.t -> CT.t -> t - (** Assert that the two terms are equal (may raise Inconsistent) *) - - val distinct : t -> CT.t -> CT.t -> t - (** Assert that the two given terms are distinct (may raise Inconsistent) *) - - type action = - | Merge of CT.t * CT.t - | Distinct of CT.t * CT.t - (** Action that can be performed on the CC *) - - val do_action : t -> action -> t - (** Perform the given action (may raise Inconsistent) *) - - val can_eq : t -> CT.t -> CT.t -> bool - (** Check whether the two terms can be equal *) - - val iter_equiv_class : t -> CT.t -> (CT.t -> unit) -> unit - (** Iterate on terms that are congruent to the given term *) - - type explanation = - | ByCongruence of CT.t * CT.t (* direct congruence of terms *) - | ByMerge of CT.t * CT.t (* user merge of terms *) - - val explain : t -> CT.t -> CT.t -> explanation list - (** Explain why those two terms are equal (assuming they are, - otherwise raises Invalid_argument) by returning a list - of merges. *) -end - -module Make(T : CurryfiedTerm) : S with module CT = T - -module StrTerm : CurryfiedTerm with type symbol = string - -module StrCC : S with module CT = StrTerm - -val parse : string -> StrTerm.t -val pp : Format.formatter -> StrTerm.t -> unit diff --git a/src/misc/cause.ml b/src/misc/cause.ml deleted file mode 100644 index 6452f766..00000000 --- a/src/misc/cause.ml +++ /dev/null @@ -1,168 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Causal Graph} for Debugging *) - -(** {2 Basic Causal Description} *) - -type t = { - id : int; - descr : string; - attrs : string list; - mutable within : t list; - mutable after : t list; -} - -type cause = t - -let _count = ref 0 - -let make ?(attrs=[]) ?(within=[]) ?(after=[]) descr = - let id = !_count in - incr _count; - { id; descr; attrs; within; after; } - -let root = make ~within:[] ~after:[] "root cause" - -let make_b ?attrs ?within ?after fmt = - let buf = Buffer.create 24 in - Printf.kbprintf - (fun buf -> make ?attrs ?within ?after (Buffer.contents buf)) - buf fmt - -let add_within a b = a.within <- b :: a.within -let add_after a b = a.after <- b :: a.after - -let id c = c.id - -let level c = assert false (* TODO *) - -let pp buf c = - let rec pp_id_list buf l = match l with - | [] -> () - | [x] -> Printf.bprintf buf "%d" x.id - | x::l' -> Printf.bprintf buf "%d, " x.id; pp_id_list buf l' - in - Printf.bprintf buf "cause_%d{%s, within{%a}, after{%a}}" c.id - c.descr pp_id_list c.within pp_id_list c.after - -let fmt fmt c = - let buf = Buffer.create 15 in - pp buf c; - Format.pp_print_string fmt (Buffer.contents buf) - -(** {2 Encoding to/from B-Encode} *) - -type 'a sequence = ('a -> unit) -> unit - -module Bencode = struct - type token = - [ `I of int - | `S of string - | `BeginDict - | `BeginList - | `End - ] - - let to_seq c k = - k `BeginDict; - k (`S "after"); - k `BeginList; - List.iter (fun c' -> k (`I c'.id)) c.after; - k `End; - k (`S "attrs"); - k `BeginList; - List.iter (fun s -> k (`S s)) c.attrs; - k `End; - k (`S "descr"); - k (`S c.descr); - k (`S "id"); - k (`I c.id); - k (`S "within"); - k `BeginList; - List.iter (fun c' -> k (`I c'.id)) c.within; - k `End; - k `End - - module ITbl = Hashtbl.Make(struct - type t = int - let equal i j = i=j - let hash i = i land max_int - end) - - module Sink = struct - type t = { - send : token -> unit; - ids : unit ITbl.t; (* printed IDs *) - } - - let make send = { send; ids = ITbl.create 32; } - - let mem sink id = ITbl.mem sink.ids id - - let print sink c = - let s = Stack.create () in - Stack.push (`Enter c) s; - (* DFS in postfix order *) - while not (Stack.is_empty s) do - match Stack.pop s with - | `Enter c when mem sink c.id -> () (* already done *) - | `Enter c -> - ITbl.add sink.ids c.id (); - (* explore sub-causes *) - List.iter (fun c' -> Stack.push (`Enter c') s) c.within; - List.iter (fun c' -> Stack.push (`Enter c') s) c.after; - Stack.push (`Exit c) s; - | `Exit c -> - (* print the cause *) - to_seq c sink.send - done - end - - module Source = struct - type t = { - tbl : cause ITbl.t; - mutable roots : cause list; - } - - let make seq = - let tbl = ITbl.create 128 in - let _roots = ref [] in - seq - (function - | _ -> assert false (* TODO parse back *) - ); - { tbl; roots= !_roots; } - - let roots src k = List.iter k src.roots - - let by_id_exn src id = ITbl.find src.tbl id - - let by_id src id = - try Some (by_id_exn src id) - with Not_found -> None - end -end diff --git a/src/misc/cause.mli b/src/misc/cause.mli deleted file mode 100644 index ced3d9a1..00000000 --- a/src/misc/cause.mli +++ /dev/null @@ -1,125 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Causal Graph} for Debugging -As often, for unique name generation reasons, this module is not thread -safe (several causes may have the same name otherwise, which can break -serialization). - -Causal loops should be avoided. *) - -(** {2 Basic Causal Description} *) - -type t -type cause = t - -val root : t - (** Root cause (the start of the program?) *) - -val make : ?attrs:string list -> ?within:t list -> ?after:t list -> - string -> t - (** New cause for some object, that depends on an informal description - (the string parameter), some previous objects (the [after] list), - and some more global context (ongoing task? see [within]). - - @param attrs attributes that describe the cause further. *) - -val make_b : ?attrs:string list -> ?within:t list -> ?after:t list -> - ('a, Buffer.t, unit, t) format4 -> 'a - (** Same as {!make}, but allows to use Buffer printers to build the - description. *) - -val add_within : t -> t -> unit - (** [within a b] specifies that [a] occurs within the more general context - of [b]. *) - -val add_after : t -> t -> unit - (** [after a b] specifies that [a] is (partially) caused by [b], and occurs - afterwards. *) - -val id : t -> int - (** Unique ID of the cause. Can be used for equality, hashing, etc. *) - -val level : t -> int - (** Depth-level of the cause. It is determined from the [within] and - [after] relations of the cause with other causes. *) - -val pp : Buffer.t -> t -> unit - (** print a single step *) - -val fmt : Format.formatter -> t -> unit - -(** {2 Encoding to/from B-Encode} -This can be used for serializing a cause (set) and re-examine them -later. It assumes a streaming API because cause graphs can become -huge quickly. *) - -type 'a sequence = ('a -> unit) -> unit - -module Bencode : sig - type token = - [ `I of int - | `S of string - | `BeginDict - | `BeginList - | `End - ] - - val to_seq : cause -> token sequence - (** token representation of a single cause *) - - module Sink : sig - type t - - val make : (token -> unit) -> t - (** Build a sink from some way of printing B-encode values out *) - - val mem : t -> int -> bool - (** Is the given [id] already printed into the sink? *) - - val print : t -> cause -> unit - (** Print the given cause (if not already printed). *) - end - - module Source : sig - type t - - val make : token sequence -> t - (** Build a source of causal graph from some sequence of B-encode - values. The whole graph will be read immediately, but the sequence - is iterated on only once. *) - - val roots : t -> cause sequence - (** Causes that have no parent (no [within] field) *) - - val by_id : t -> int -> cause option - (** Retrieve a cause by its unique ID, if present *) - - val by_id_exn : t -> int -> cause - (** Same as {!by_id}, but unsafe. - @raise Not_found if the ID is not present. *) - end -end diff --git a/src/misc/circList.ml b/src/misc/circList.ml deleted file mode 100644 index 0b0670be..00000000 --- a/src/misc/circList.ml +++ /dev/null @@ -1,135 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Circular List} - -Those are infinite lists that are built from a finite list of -elements, and cycles through them. *) - -type 'a t = { - front : 'a list; - f_len : int; - rear : 'a list; - r_len : int; -} -(* invariant: if front=[] then rear=[] *) - -let make f f_len r r_len = match f with - | [] -> - assert (f_len = 0); - { front=List.rev r; f_len=r_len; rear=[]; r_len=0; } - | _::_ -> {front=f; f_len; rear=r; r_len; } - -let singleton x = make [x] 1 [] 0 - -let of_list l = - if l = [] then raise (Invalid_argument "empty list"); - make l (List.length l) [] 0 - -let length l = l.f_len + l.r_len - -(*$Q - (Q.list Q.small_int) (fun l -> \ - l = [] || \ - let q = of_list l in \ - let _, q = next q in \ - length q = List.length l) -*) - -let cons x l = make (x::l.front) (l.f_len+1) l.rear l.r_len - -let snoc l x = make l.front l.f_len (x::l.rear) (l.r_len+1) - -let next l = match l.front with - | [] -> assert false - | x::l' -> - x, make l' (l.f_len-1) (x::l.rear) (l.r_len+1) - -let rev l = make l.rear l.r_len l.front l.f_len - -let find p l = - let rec _find p i l = - if i = 0 then None - else - let x, l' = next l in - if p x then Some x else _find p (i-1) l' - in - _find p (length l) l - -let mem ?(eq=fun x y -> x=y) x l = - match find (eq x) l with - | None -> false - | Some _ -> true - -let exists p l = match find p l with - | None -> false - | Some _ -> true - -(*$T - exists (fun x-> x mod 2 = 0) (of_list [1;3;5;7;8]) - not (exists (fun x-> x mod 2 = 0) (of_list [1;3;5;7;9])) - *) - -let for_all p l = - let rec _check i l = - i = 0 || - ( let x, l' = next l in - p x && _check (i-1) l') - in - _check (length l) l - -let fold f acc l = - let rec _fold acc i l = - if i=0 then acc - else - let x, l' = next l in - let acc = f acc x in - _fold acc (i-1) l' - in - _fold acc (length l) l - -type 'a gen = unit -> 'a option -type 'a sequence = ('a -> unit) -> unit - -let gen l = - let l = ref l in - fun () -> - let x, l' = next !l in - l := l'; - Some x - -(*$Q - (Q.list Q.small_int) (fun l -> \ - l = [] || let q = of_list l in \ - gen q |> Gen.take (List.length l) |> Gen.to_list = l) - *) - -let seq l k = - let r' = lazy (List.rev l.rear) in - while true do - List.iter k l.front; - List.iter k (Lazy.force r') - done diff --git a/src/misc/circList.mli b/src/misc/circList.mli deleted file mode 100644 index 5c982a5b..00000000 --- a/src/misc/circList.mli +++ /dev/null @@ -1,82 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Circular List} - -Those are infinite lists that are built from a finite list of -elements, and cycles through them. -Unless specified otherwise, operations have an amortized cost in O(1). *) - -type +'a t - -val singleton : 'a -> 'a t -(** list that cycles on one element *) - -val of_list : 'a list -> 'a t -(** build a circular list from a list. Linear in the length - of the list. - @raise Invalid_argument if the list is empty *) - -val length : 'a t -> int -(** length of the cycle. *) - -val cons : 'a -> 'a t -> 'a t -(** [cons x l] adds [x] at the beginning of [l] *) - -val snoc : 'a t -> 'a -> 'a t -(** [snoc l x] adds [x] at the end of [l] *) - -val next : 'a t -> 'a * 'a t -(** obtain the next element, and the list rotated by one. *) - -val rev : 'a t -> 'a t -(** reverse the traversal (goes right-to-left from now). *) - -val find : ('a -> bool) -> 'a t -> 'a option -(** [find p l] returns [Some x] where [p x] is [true] - and [x] belongs to [l], or [None] if no such - element exists *) - -val mem : ?eq:('a -> 'a -> bool) -> 'a -> 'a t -> bool -(** does the element belong to the infinite list? *) - -val exists : ('a -> bool) -> 'a t -> bool - -val for_all : ('a -> bool) -> 'a t -> bool - -val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b -(** fold through each element of the list exactly once. *) - -(** {2 Iterators} *) - -type 'a gen = unit -> 'a option -type 'a sequence = ('a -> unit) -> unit - -val gen : 'a t -> 'a gen -(** CCGenerator on elements of the list *) - -val seq : 'a t -> 'a sequence -(** CCSequence of elements of the list *) diff --git a/src/misc/conv.ml b/src/misc/conv.ml deleted file mode 100644 index 373088b4..00000000 --- a/src/misc/conv.ml +++ /dev/null @@ -1,621 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Bidirectional Conversion} *) - -exception ConversionFailure of string - -(* error-raising function *) -let __error msg = - let b = Buffer.create 15 in - Printf.bprintf b "conversion error: "; - Printf.kbprintf - (fun b -> raise (ConversionFailure (Buffer.contents b))) - b msg - -(* function to look up the given name in an association list *) -let _get_field l name = - try List.assoc name l - with Not_found -> - __error "record field %s not found in source" name - -(** Universal sink, such as a serialization format *) -module UniversalSink = struct - type 'a t = { - unit_ : 'a; - bool_ : bool -> 'a; - float_ : float -> 'a; - int_ : int -> 'a; - string_ : string -> 'a; - list_ : 'a list -> 'a; - record : (string*'a) list -> 'a; - tuple : 'a list -> 'a; - sum : string -> 'a list -> 'a; - } -end - -module Source = struct - module US = UniversalSink - - type 'a t = { - convert : 'b. 'b US.t -> 'a -> 'b; - } - - type 'r record_src = - | RecordField : string * ('r -> 'a) * 'a t * 'r record_src -> 'r record_src - | RecordStop : 'r record_src - - type hlist = - | HNil : hlist - | HCons : 'a t * 'a * hlist -> hlist - - let hnil = HNil - let hcons src x tl = HCons(src,x,tl) - - let unit_ = { convert = (fun sink () -> sink.US.unit_); } - let bool_ = { convert = (fun sink b -> sink.US.bool_ b); } - let float_ = { convert = (fun sink f -> sink.US.float_ f); } - let int_ = { convert = (fun sink i -> sink.US.int_ i); } - let string_ = { convert = (fun sink s -> sink.US.string_ s); } - let list_ e = - let convert sink l = - let l' = List.map (e.convert sink) l in - sink.US.list_ l' - in {convert;} - - let map f src = - { convert=(fun sink x -> src.convert sink (f x)); } - let array_ src = map Array.to_list (list_ src) - - let field name get src' cont = - RecordField (name,get,src',cont) - let record_stop = RecordStop - - let record (r:'a record_src) = - (* fold over record description *) - let rec conv_fields - : type b. b US.t -> (string*b)list -> 'a record_src -> 'a -> (string*b)list - = fun sink acc r x -> match r with - | RecordStop -> acc - | RecordField (name,get,src',r') -> - let acc = (name, src'.convert sink (get x)) :: acc in - conv_fields sink acc r' x - in - let convert sink x = sink.US.record (conv_fields sink [] r x) in - { convert; } - - let record_fix f = - let rec convert: type b. b US.t -> 'r -> b - = fun sink x -> - (* evaluate src, and use it to convert x *) - (Lazy.force src).convert sink x - and src = lazy (record (f {convert})) in - Lazy.force src - - (* fold over hlist *) - let rec conv_hlist : type b. b US.t -> b list -> hlist -> b list - = fun sink acc t -> match t with - | HNil -> List.rev acc - | HCons (src',x,t') -> - let acc = src'.convert sink x :: acc in - conv_hlist sink acc t' - - let tuple t = - let convert sink x = - let hlist = t x in - sink.US.tuple (conv_hlist sink [] hlist) in - { convert; } - - let pair a b = - { convert=(fun sink (x,y) -> - sink.US.tuple [a.convert sink x; b.convert sink y]); - } - - let triple a b c = - { convert=(fun sink (x,y,z) -> - sink.US.tuple [a.convert sink x; b.convert sink y; c.convert sink z]); - } - - let quad a b c d = - { convert=(fun sink (x,y,z,w) -> - sink.US.tuple [a.convert sink x; b.convert sink y; - c.convert sink z; d.convert sink w]); - } - - let sum f = - let convert sink x = - let name, l = f x in - sink.US.sum name (conv_hlist sink [] l) in - { convert; } - - let sum0 f = - {convert=(fun sink x -> sink.US.sum (f x) []); } - - let sum_fix f = - let rec convert : type b. b US.t -> 'r -> b - = fun sink x -> - (* evaluate src, and use it to convert x *) - (Lazy.force src).convert sink x - and src = lazy (sum (f {convert})) in - Lazy.force src - - let opt src = sum (function - | Some x -> "some", hcons src x hnil - | None -> "none", hnil) -end - -let into src sink x = src.Source.convert sink x - -module Sink = struct - (** A specific sink that requires a given shape to produce - a value of type 'a *) - type 'a t = - | Unit : unit t - | Bool : bool t - | Float : float t - | Int : int t - | String : string t - | List : (('b t -> 'b list) -> 'a) -> 'a t - | Record : 'a record_sink -> 'a t - | Tuple : 'a hlist -> 'a t - | Sum : (string -> 'a hlist) -> 'a t - | Map : 'a t * ('a -> 'b) -> 'b t - | Fix : ('a t -> 'a t) -> 'a t - - and 'r record_sink = - | RecordField : string * 'a t * ('a -> 'r record_sink) -> 'r record_sink - | RecordStop : 'r -> 'r record_sink - - and 't hlist = - | HCons : 'a t * ('a -> 't hlist) -> 't hlist - | HNil : 't -> 't hlist - - let rec __expected : type a. a t -> string = function - | Unit -> "unit" - | Bool -> "bool" - | Float -> "float" - | Int -> "int" - | String -> "string" - | List _ -> "list" - | Record _ -> "record" - | Tuple _ -> "tuple" - | Sum _ -> "sum" - | Map (sink', _) -> __expected sink' - | (Fix f) as sink -> __expected (f sink) - - let unit_ = Unit - let bool_ = Bool - let float_ = Float - let int_ = Int - let string_ = String - let list_ e = - List (fun k -> let l = k e in l) - - let map f sink = Map (sink, f) - let array_ sink = - map Array.of_list (list_ sink) - - let field name sink cont = RecordField (name, sink, cont) - let yield_record r = RecordStop r - let record r = Record r - let record_fix f = - let rec r = lazy (Fix (fun _ -> Record (f (Lazy.force r)))) in - Lazy.force r - - let (|+|) sink cont = HCons (sink, cont) - let yield t = HNil t - - let tuple t = Tuple t - - let pair a b = - tuple ( - a |+| fun x -> - b |+| fun y -> - yield (x,y) - ) - - let triple a b c = - tuple ( - a |+| fun x -> - b |+| fun y -> - c |+| fun z -> - yield (x,y,z) - ) - - let quad a b c d = - tuple ( - a |+| fun x -> - b |+| fun y -> - c |+| fun z -> - d |+| fun w -> - yield (x,y,z,w) - ) - - let sum f = Sum f - let sum_fix f = - Fix (fun s -> Sum (f s)) - - let opt sink = sum (fun name -> - match name with - | "some" -> sink |+| fun x -> yield (Some x) - | "none" -> yield None - | _ -> __error "unexpected variant %s" name) - - (** What is expected by the sink? *) - type expected = - | ExpectInt - | ExpectBool - | ExpectUnit - | ExpectFloat - | ExpectString - | ExpectRecord - | ExpectTuple - | ExpectList - | ExpectSum - - let rec expected : type a. a t -> expected = function - | Unit -> ExpectUnit - | Bool -> ExpectBool - | Int -> ExpectInt - | Float -> ExpectFloat - | String -> ExpectString - | Record _ -> ExpectRecord - | Tuple _ -> ExpectTuple - | Sum _ -> ExpectSum - | List _ -> ExpectList - | (Fix f) as sink -> expected (f sink) - | Map (sink', _) -> expected sink' -end - -module UniversalSource = struct - type 'a t = { - visit : 'b. 'b Sink.t -> 'a -> 'b; - } - - let rec unit_ : type b. b Sink.t -> b - = fun sink -> match sink with - | Sink.Unit -> () - | Sink.Int -> 0 - | Sink.Map (sink', f) -> f (unit_ sink') - | Sink.Fix f -> unit_ (f sink) - | _ -> __error "get Unit, but expected %s" (Sink.__expected sink) - - let rec bool_ : type b. b Sink.t -> bool -> b - = fun sink b -> match sink with - | Sink.Bool -> b - | Sink.Int -> if b then 1 else 0 - | Sink.String -> string_of_bool b - | Sink.Map (sink', f) -> f (bool_ sink' b) - | Sink.Fix f -> bool_ (f sink) b - | _ -> __error "get Bool, but expected %s" (Sink.__expected sink) - - let rec float_ : type b. b Sink.t -> float -> b - = fun sink x -> match sink with - | Sink.Float -> x - | Sink.String -> string_of_float x - | Sink.Map (sink', f) -> f (float_ sink' x) - | Sink.Fix f -> float_ (f sink) x - | _ -> __error "get Float, but expected %s" (Sink.__expected sink) - - let rec int_ : type b. b Sink.t -> int -> b - = fun sink i -> match sink with - | Sink.Int -> i - | Sink.Bool -> i <> 0 - | Sink.String -> string_of_int i - | Sink.Map (sink', f) -> f (int_ sink' i) - | Sink.Fix f -> int_ (f sink) i - | _ -> __error "get Int, but expected %s" (Sink.__expected sink) - - let rec string_ : type b. b Sink.t -> string -> b - = fun sink s -> match sink with - | Sink.String -> s - | Sink.Int -> - begin try int_of_string s - with Invalid_argument _ -> __error "get String, but expected Int" - end - | Sink.Bool -> - begin try bool_of_string s - with Invalid_argument _ -> __error "get String, but expected Bool" - end - | Sink.Float -> - begin try float_of_string s - with Invalid_argument _ -> __error "get String, but expected Float" - end - | Sink.Map (sink', f) -> f (string_ sink' s) - | Sink.Fix f -> string_ (f sink) s - | _ -> __error "get String, but expected %s" (Sink.__expected sink) - - let rec list_ : type b. src:'a t -> b Sink.t -> 'a list -> b - = fun ~src sink l -> match sink with - | Sink.List f -> - f (fun sink' -> List.map (src.visit sink') l) - | Sink.Tuple _ -> tuple ~src sink l - | Sink.Map (sink', f) -> f (list_ ~src sink' l) - | Sink.Fix f -> list_ ~src (f sink) l - | _ -> __error "get List, but expected %s" (Sink.__expected sink) - - and record : type b. src:'a t -> b Sink.t -> (string*'a) list -> b - = fun ~src sink l -> match sink with - | Sink.Record r -> - (* fold over the expected record fields *) - let rec build_record - = function - | Sink.RecordStop x -> x - | Sink.RecordField (name, sink', cont) -> - let src_field = _get_field l name in - let sink_field = src.visit sink' src_field in - build_record (cont sink_field) - in build_record r - | Sink.Map (sink', f) -> f (record ~src sink' l) - | Sink.Fix f -> record ~src (f sink) l - | _ -> __error "get Record, but expected %s" (Sink.__expected sink) - - and build_hlist : 't. src:'a t -> 'a list -> 't Sink.hlist -> 't - = fun ~src l t_sink -> match l, t_sink with - | [], Sink.HNil t -> t - | [], _ -> - __error "not enough tuple components" - | _::_, Sink.HNil _ -> - __error "too many tuple components (%d too many)" (List.length l) - | x::l', Sink.HCons (sink', cont) -> - let y = src.visit sink' x in - build_hlist ~src l' (cont y) - - and tuple : type b. src:'a t -> b Sink.t -> 'a list -> b - = fun ~src sink l -> match sink with - | Sink.Tuple t_sink -> - (* fold over the expected tuple component *) - build_hlist ~src l t_sink - | Sink.List _ -> list_ ~src sink l (* adapt *) - | Sink.Map (sink', f) -> f (tuple ~src sink' l) - | Sink.Fix f -> tuple ~src (f sink) l - | _ -> __error "get Tuple, but expected %s" (Sink.__expected sink) - - and sum : type b. src:'a t -> b Sink.t -> string -> 'a list -> b - = fun ~src sink name s -> match sink with - | Sink.Sum f -> - let l_sink = f name in - build_hlist ~src s l_sink - | Sink.Map (sink', f) -> f (sum ~src sink' name s) - | Sink.Fix f -> sum ~src (f sink) name s - | _ -> __error "get Sum(%s), but expected %s" name (Sink.__expected sink) -end - -let from (src:'a UniversalSource.t) (sink:'b Sink.t) (x:'a) : 'b = - src.UniversalSource.visit sink x - -(** {6 Exemples} *) - -module Json = struct - type t = [ - | `Int of int - | `Float of float - | `Bool of bool - | `Null - | `String of string - | `List of t list - | `Assoc of (string * t) list - ] - - let source = - let module U = UniversalSource in - let rec visit : type b. b Sink.t -> t -> b = - fun sink x -> match x with - | `Int i -> U.int_ sink i - | `Float f -> U.float_ sink f - | `Bool b -> U.bool_ sink b - | `Null -> U.unit_ sink - | `String s -> - begin match Sink.expected sink with - | Sink.ExpectSum -> U.sum ~src sink s [] - | _ -> U.string_ sink s - end - | `List ((`String name :: l) as l') -> - begin match Sink.expected sink with - | Sink.ExpectSum -> U.sum ~src sink name l - | _ -> U.list_ ~src sink l' - end - | `List l -> U.list_ ~src sink l - | `Assoc l -> U.record ~src sink l - and src = { U.visit=visit; } in - src - - let sink : t UniversalSink.t = - let open UniversalSink in - { unit_ = `Null; - bool_ = (fun b -> `Bool b); - float_ = (fun f -> `Float f); - int_ = (fun i -> `Int i); - string_ = (fun s -> `String s); - list_ = (fun l -> `List l); - record = (fun l -> `Assoc l); - tuple = (fun l -> `List l); - sum = (fun name l -> match l with - | [] -> `String name - | _::_ -> `List (`String name :: l)); - } -end - -module Sexp = struct - type t = - | Atom of string - | List of t list - - let source = - let module U = UniversalSource in - let rec visit : type b. b Sink.t -> t -> b = - fun sink x -> match x, Sink.expected sink with - | Atom s, Sink.ExpectSum -> U.sum ~src sink s [] - | List (Atom name :: l), Sink.ExpectSum -> U.sum ~src sink name l - | List l, Sink.ExpectRecord -> - let l' = List.map (function - | List [Atom name; x] -> name, x - | _ -> __error "get List, but expected Record") l - in U.record ~src sink l' - | Atom s, _ -> U.string_ sink s - | List [], Sink.ExpectUnit -> U.unit_ sink - | List l, _ -> U.list_ ~src sink l - and src = { U.visit=visit; } in - src - - let sink = - let open UniversalSink in - { unit_ = List []; - bool_ = (fun b -> Atom (string_of_bool b)); - float_ = (fun f -> Atom (string_of_float f)); - int_ = (fun i -> Atom (string_of_int i)); - string_ = (fun s -> Atom (String.escaped s)); - list_ = (fun l -> List l); - record = (fun l -> List (List.map (fun (a,b) -> List [Atom a; b]) l)); - tuple = (fun l -> List l); - sum = (fun name l -> match l with - | [] -> Atom name - | _::_ -> List (Atom name :: l)); - } - - let rec fmt out = function - | Atom s -> Format.pp_print_string out s - | List l -> - Format.pp_print_char out '('; - List.iteri (fun i s -> - if i > 0 then Format.pp_print_char out ' '; - fmt out s) l; - Format.pp_print_char out ')' -end - -module Bencode = struct - type t = - | Int of int - | String of string - | List of t list - | Assoc of (string * t) list - - let source = - let module U = UniversalSource in - let rec visit : type b. b Sink.t -> t -> b = - fun sink x -> match x, Sink.expected sink with - | String s, Sink.ExpectSum -> U.sum ~src sink s [] - | List (String name :: l), Sink.ExpectSum -> U.sum ~src sink name l - | Assoc l, _ -> U.record ~src sink l - | String s, _ -> U.string_ sink s - | List [], Sink.ExpectUnit -> U.unit_ sink - | List l, _ -> U.list_ ~src sink l - | Int 0, Sink.ExpectUnit -> U.unit_ sink - | Int i, _ -> U.int_ sink i - and src = { U.visit=visit; } in - src - - let sink = - let open UniversalSink in - { unit_ = Int 0; - bool_ = (fun b -> Int (if b then 1 else 0)); - float_ = (fun f -> String (string_of_float f)); - int_ = (fun i -> Int i); - string_ = (fun s -> String s); - list_ = (fun l -> List l); - record = (fun l -> Assoc l); - tuple = (fun l -> List l); - sum = (fun name l -> match l with - | [] -> String name - | _::_ -> List (String name :: l)); - } -end - -(* tests *) - -let (@@) f x = f x - -module Point = struct - type t = { - x : int; - y : int; - color : string; - prev : t option; (* previous position, say *) - } - - let sink = - Sink.(record_fix - (fun self -> - field "x" int_ @@ fun x -> - field "y" int_ @@ fun y -> - field "color" string_ @@ fun color -> - field "prev" (opt self) @@ fun prev -> - yield_record {x;y;color;prev} - )) - - let source = - Source.(record_fix - (fun self -> - field "x" (fun p -> p.x) int_ @@ - field "y" (fun p -> p.y) int_ @@ - field "color" (fun p -> p.color) string_ @@ - field "prev" (fun p -> p.prev) (opt self) @@ - record_stop - )) - - let p = {x=1; y=42; color="yellow"; - prev = Some {x=1; y=41; color="red"; prev=None};} - - let p2 = into source Json.sink p - - let p3 = from Json.source sink p2 - - let p4 = into source Json.sink p3 - - let p2_sexp = into source Sexp.sink p - - let p3_sexp = from Sexp.source sink p2_sexp - - let p4_sexp = into source Sexp.sink p3_sexp -end - -module Lambda = struct - type t = - | Var of string - | App of t * t - | Lambda of string * t - - let source = Source.(sum_fix - (fun self t -> match t with - | Var s -> "var", hcons string_ s @@ hnil - | App (t1, t2) -> "app", hcons self t1 @@ hcons self t2 @@ hnil - | Lambda (s, t) -> "lam", hcons string_ s @@ hcons self t @@ hnil - )) - - let sink = Sink.(sum_fix - (fun self str -> match str with - | "var" -> string_ |+| fun s -> yield (Var s) - | "app" -> self |+| fun t1 -> self |+| fun t2 -> yield (App (t1, t2)) - | "lam" -> string_ |+| fun s -> self |+| fun t -> yield (Lambda (s, t)) - | _ -> __error "expected lambda term" - )) - - let t1 = Lambda ("x", App (Lambda ("y", App (Var "y", Var "x")), Var "x")) - - let t1_json = into source Json.sink t1 - let t1_bencode = into source Bencode.sink t1 - let t1_sexp = into source Sexp.sink t1 -end diff --git a/src/misc/conv.mli b/src/misc/conv.mli deleted file mode 100644 index 25b8f977..00000000 --- a/src/misc/conv.mli +++ /dev/null @@ -1,260 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Bidirectional Conversion} *) - -exception ConversionFailure of string - -(** {6 Universal sink} - -Some type any valye can be traducted into, such as a serialization format -like JSON or B-encode. *) -module UniversalSink : sig - type 'a t = { - unit_ : 'a; - bool_ : bool -> 'a; - float_ : float -> 'a; - int_ : int -> 'a; - string_ : string -> 'a; - list_ : 'a list -> 'a; - record : (string*'a) list -> 'a; - tuple : 'a list -> 'a; - sum : string -> 'a list -> 'a; - } -end - -(** {6 Sources} -A 'a source is used to build values of some type 'b, given a 'b sink -description of how to build values of type 'b. *) -module Source : sig - type 'a t = { - convert : 'b. 'b UniversalSink.t -> 'a -> 'b; - } - - type 'r record_src - - type hlist = - | HNil : hlist - | HCons : 'a t * 'a * hlist -> hlist - - val hnil : hlist - val hcons : 'a t -> 'a -> hlist -> hlist - - val unit_ : unit t - val bool_ : bool t - val float_ : float t - val int_ : int t - val string_ : string t - val list_ : 'a t -> 'a list t - - val map : ('a -> 'b) -> 'b t -> 'a t - val array_ : 'a t -> 'a array t - - val field : string -> ('r -> 'a) -> 'a t -> 'r record_src -> 'r record_src - val record_stop : 'r record_src - val record : 'r record_src -> 'r t - val record_fix : ('r t -> 'r record_src) -> 'r t - - val tuple : ('a -> hlist) -> 'a t - - val pair : 'a t -> 'b t -> ('a * 'b) t - val triple : 'a t -> 'b t -> 'c t -> ('a * 'b * 'c) t - val quad : 'a t -> 'b t -> 'c t -> 'd t -> ('a * 'b * 'c * 'd) t - - val sum : ('a -> string * hlist) -> 'a t - val sum0 : ('a -> string) -> 'a t - val sum_fix : ('a t -> 'a -> string * hlist) -> 'a t - - val opt : 'a t -> 'a option t -end - -(** {6 Sinks} -A sink is used to produce values of type 'a from a universal source. *) -module Sink : sig - type 'a t (** How to produce values of type 'a *) - - and 'r record_sink = - | RecordField : string * 'a t * ('a -> 'r record_sink) -> 'r record_sink - | RecordStop : 'r -> 'r record_sink - - and 't hlist = - | HCons : 'a t * ('a -> 't hlist) -> 't hlist - | HNil : 't -> 't hlist - - val unit_ : unit t - val bool_ : bool t - val float_ : float t - val int_ : int t - val string_ : string t - val list_ : 'a t -> 'a list t - - val map : ('a -> 'b) -> 'a t -> 'b t - val array_ : 'a t -> 'a array t - - val field : string -> 'a t -> ('a -> 'r record_sink) -> 'r record_sink - val yield_record : 'r -> 'r record_sink - val record : 'r record_sink -> 'r t - val record_fix : ('r t -> 'r record_sink) -> 'r t - - val (|+|) : 'a t -> ('a -> 't hlist) -> 't hlist - val yield : 'a -> 'a hlist - - val tuple : 't hlist -> 't t - - val pair : 'a t -> 'b t -> ('a * 'b) t - val triple : 'a t -> 'b t -> 'c t -> ('a * 'b * 'c) t - val quad : 'a t -> 'b t -> 'c t -> 'd t -> ('a * 'b * 'c * 'd) t - - val sum : (string -> 'a hlist) -> 'a t - val sum_fix : ('a t -> string -> 'a hlist) -> 'a t - - val opt : 'a t -> 'a option t - - (** What is expected by the sink? *) - type expected = - | ExpectInt - | ExpectBool - | ExpectUnit - | ExpectFloat - | ExpectString - | ExpectRecord - | ExpectTuple - | ExpectList - | ExpectSum - - val expected : _ t -> expected - (** To be used by sources that have ambiguities to know what is expected. - maps and fixpoints are unrolled. *) -end - -(** {6 Universal source} - -source from type 'a, where 'a is typically a serialization -format. This is used to translate from 'a to some other type. -A universal format should use the provided combinators to -interface with {!Sink.t} values *) -module UniversalSource : sig - type 'a t = { - visit : 'b. 'b Sink.t -> 'a -> 'b; - } - - val unit_ : 'b Sink.t -> 'b - val bool_ : 'b Sink.t -> bool -> 'b - val float_ : 'b Sink.t -> float -> 'b - val int_ : 'b Sink.t -> int -> 'b - val string_ : 'b Sink.t -> string -> 'b - val list_ : src:'a t -> 'b Sink.t -> 'a list -> 'b - val record : src:'a t -> 'b Sink.t -> (string*'a) list -> 'b - val tuple : src:'a t -> 'b Sink.t -> 'a list -> 'b - val sum : src:'a t -> 'b Sink.t -> string -> 'a list -> 'b -end - -(** {6 Conversion Functions} *) - -val into : 'a Source.t -> 'b UniversalSink.t -> 'a -> 'b - (** Conversion to universal sink *) - -val from : 'a UniversalSource.t -> 'b Sink.t -> 'a -> 'b - (** Conversion from universal source *) - -(* TODO for format conversion -val between : 'a Source.universal -> 'b Sink.universal -> 'a -> 'b -*) - -(** {6 Exemples} *) - -module Json : sig - type t = [ - | `Int of int - | `Float of float - | `Bool of bool - | `Null - | `String of string - | `List of t list - | `Assoc of (string * t) list - ] - - val source : t UniversalSource.t - val sink : t UniversalSink.t -end - -module Sexp : sig - type t = - | Atom of string - | List of t list - - val source : t UniversalSource.t - val sink : t UniversalSink.t - val fmt : Format.formatter -> t -> unit (* for debug *) -end - -module Bencode : sig - type t = - | Int of int - | String of string - | List of t list - | Assoc of (string * t) list - - val source : t UniversalSource.t - val sink : t UniversalSink.t -end - -(** Tests *) - -module Point : sig - type t = { - x : int; - y : int; - color : string; - prev : t option; (* previous position, say *) - } - - val source : t Source.t - val sink : t Sink.t - - val p : t - val p2 : Json.t - val p4 : Json.t - - val p2_sexp : Sexp.t - val p4_sexp : Sexp.t -end - -module Lambda : sig - type t = - | Var of string - | App of t * t - | Lambda of string * t - - val source : t Source.t - val sink : t Sink.t - - val t1 : t - - val t1_json : Json.t - val t1_bencode : Bencode.t - val t1_sexp : Sexp.t -end diff --git a/src/misc/fHashtbl.ml b/src/misc/fHashtbl.ml deleted file mode 100644 index a72dd203..00000000 --- a/src/misc/fHashtbl.ml +++ /dev/null @@ -1,503 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional (persistent) hashtable} *) - -type 'a sequence = ('a -> unit) -> unit - -(** {2 Signatures} *) - -module type HASH = sig - type t - val equal : t -> t -> bool - val hash : t -> int -end - -(** The signature for such a functional hashtable *) -module type S = sig - type 'a t - type key - - val empty : int -> 'a t - (** The empty hashtable (with sub-hashtables of given size) *) - - val is_empty : _ t -> bool - - val find : 'a t -> key -> 'a - (** Find the binding for this key, or raise Not_found *) - - val mem : 'a t -> key -> bool - (** Check whether the key is bound in this hashtable *) - - val replace : 'a t -> key -> 'a -> 'a t - (** [replace t key val] returns a copy of [t] where [key] binds to [val] *) - - val remove : 'a t -> key -> 'a t - (** Remove the bindings for the given key *) - - val fold : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b - (** Fold on bindings *) - - val iter : (key -> 'a -> unit) -> 'a t -> unit - (** Iterate on bindings *) - - val size : 'a t -> int - (** Number of bindings *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : ?size:int -> (key * 'a) sequence -> 'a t -end - -(** {2 Persistent array} *) - -module PArray = struct - type 'a t = 'a zipper ref - and 'a zipper = - | Array of 'a array - | Diff of int * 'a * 'a zipper ref - - (* XXX maybe having a snapshot of the array from point to point may help? *) - - let make size elt = - let a = Array.make size elt in - ref (Array a) - - (** Recover the given version of the shared array. Returns the array - itself. *) - let rec reroot t = - match !t with - | Array a -> a - | Diff (i, v, t') -> - begin - let a = reroot t' in - let v' = a.(i) in - t' := Diff (i, v', t); - a.(i) <- v; - t := Array a; - a - end - - let get t i = - match !t with - | Array a -> a.(i) - | Diff _ -> - let a = reroot t in - a.(i) - - let set t i v = - let a = - match !t with - | Array a -> a - | Diff _ -> reroot t in - let v' = a.(i) in - if v == v' - then t (* no change *) - else begin - let t' = ref (Array a) in - a.(i) <- v; - t := Diff (i, v', t'); - t' (* create new array *) - end - - let fold_left f acc t = - let a = reroot t in - Array.fold_left f acc a - - let rec length t = - match !t with - | Array a -> Array.length a - | Diff (_, _, t') -> length t' -end - -(** {2 Tree-like hashtable} *) - -module Tree(X : HASH) = struct - (** The hashtable is a binary tree, with persistent arrays as leaves. - Nodes at depth n of the tree are split on the n-th digit of the hash - (starting with the least significant bit as 0). - - The left child is for bit=0, the right one for bit=1. *) - - type key = X.t - - type 'a t = - | Split of 'a t * 'a t (** Split on the last digit of the hash *) - | Table of 'a buckets (** Hashtable as a persistent array *) - (** The hashtable, as a tree of persistent open addressing hashtables *) - and 'a buckets = 'a bucket PArray.t - (** A persistent array of buckets *) - and 'a bucket = - | Empty - | Deleted - | Used of key * 'a - (** One buckets stores one key->value binding *) - - let empty_buckets size = - PArray.make size Empty - - (** Empty hashtable *) - let empty size = - let size = max size 4 in (* size >= 4 *) - Table (empty_buckets size) - - let rec is_empty_array a i = - if i = Array.length a then true - else (a.(i) = Empty || a.(i) = Deleted) && is_empty_array a (i+1) - - let rec is_empty t = - match t with - | Split (l, r) -> is_empty l && is_empty r - | Table a -> is_empty_array (PArray.reroot a) 0 - - (** The address in a bucket array, after probing [i] times *) - let addr n h i = ((h land max_int) + i) mod n - - (** Find the bucket that contains the given [key]. [h] is - not necessarily the hash of the key, because it can have been - shifted to right several times. *) - let rec probe_find buckets n h key i = - if i = n then raise Not_found else begin - let j = addr n h i in - match PArray.get buckets j with - | Empty -> raise Not_found - | Used (key', value) when X.equal key key' -> - value (* found *) - | Used _ | Deleted -> - probe_find buckets n h key (i+1) (* go further *) - end - - (** Find the value bound to the given [key] *) - let find t key = - let h = X.hash key in - (* find the appropriate leaf *) - let rec find h t = - match t with - | Split (l, r) -> - if h land 0x1 = 0 - then find (h lsr 1) l (* bit=0, goto left *) - else find (h lsr 1) r (* bit=1, goto right *) - | Table buckets -> - probe_find buckets (PArray.length buckets) h key 0 - in - find h t - - (** Check whether the key is bound in this hashtable *) - let mem t key = - try ignore (find t key); true - with Not_found -> false - - (** Maximal depth of the tree (number of bits of the hash) *) - let max_depth = Sys.word_size - 1 - - (** [i] is the length of the current probe. [n] is the size of - the buckets array. This decides whether the probe, looking - for a free bucket to insert a binding in, is too long. *) - let probe_too_long n i = - i / 5 > n / 8 (* i/n > 5/8 *) - - (** Insert [key] -> [value] in the buckets. *) - let rec probe_insert buckets ~depth h key value = - let n = PArray.length buckets in - let rec probe i = - if n = i then (assert (depth = max_depth); failwith "FHashtbl is full") - else if (depth < max_depth && probe_too_long n i) - (* We are not too deep, and the table starts being full, we - split it into two sub-tables *) - then - let depth' = depth + 1 in - (* increase size of sub-arrays by 1.5 *) - let sub_size = min (n + (n lsr 1)) Sys.max_array_length in - let l, r = PArray.fold_left - (fun (l,r) bucket -> match bucket with - | Empty | Deleted -> (l,r) - | Used (key',value') -> - let h' = (X.hash key') lsr depth in - if h' land 0x1 = 0 - then - let l' = insert l ~depth:depth' (h' lsr 1) key' value' in - l', r - else - let r' = insert r ~depth:depth' (h' lsr 1) key' value' in - l, r') - (empty sub_size, empty sub_size) buckets in - (* the split of those two sub-hashtables *) - let new_table = Split (l, r) in - (* insert in this new hashtable *) - insert new_table ~depth h key value - else (* look for an empty slot to insert the bucket *) - let j = addr n h i in - match PArray.get buckets j with - | Empty | Deleted -> - (* insert here *) - let buckets' = PArray.set buckets j (Used (key, value)) in - Table buckets' - | Used (key', _) when X.equal key key' -> - (* replace *) - let buckets' = PArray.set buckets j (Used (key, value)) in - Table buckets' - | Used _ -> probe (i+1) (* probe failed, go further *) - in - probe 0 - (** Insert [key] -> [value] in the sub-hashtable *) - and insert t ~depth h key value = - match t with - | Split (l, r) -> - if h land 0x1 = 0 - then (* bit=0, goto left *) - let l' = insert l ~depth:(depth+1) (h lsr 1) key value in - Split (l', r) - else (* bit=1, goto right *) - let r' = insert r ~depth:(depth+1) (h lsr 1) key value in - Split (l, r') - | Table buckets -> - (* insert in the flat hashtable *) - probe_insert buckets ~depth h key value - - (** [replace t key val] returns a copy of [t] where [key] binds to [val] *) - let replace t key value = - let h = X.hash key in - insert t ~depth:0 h key value - - (** Recursive removal function *) - let rec rec_remove t h key = - match t with - | Split (l, r) -> - if h land 0x1 = 0 - then (* bit=0, goto left *) - let l' = rec_remove l (h lsr 1) key in - if l == l' then t else Split (l', r) - else (* bit=1, goto right *) - let r' = rec_remove r (h lsr 1) key in - if r == r' then t else Split (l, r') - | Table buckets -> - (* remove from the flat hashtable *) - probe_remove t buckets h key - (* remove key from the buckets *) - and probe_remove old_table buckets h key = - let n = PArray.length buckets in - let rec probe i = - if i = n - then old_table (* not present *) - else - let j = addr n h i in - match PArray.get buckets j with - | Empty -> old_table (* not present *) - | Deleted -> probe (i+1) - | Used (key', _) -> - if X.equal key key' - then Table (PArray.set buckets j Deleted) - else probe (i+1) - in - probe 0 - - - (** Remove the bindings for the given key *) - let remove t key = - let h = X.hash key in - rec_remove t h key - - (** Fold on bindings *) - let rec fold f acc t = - match t with - | Split (l, r) -> - let acc' = fold f acc l in - fold f acc' r - | Table buckets -> - PArray.fold_left - (fun acc bucket -> match bucket with - | Empty | Deleted -> acc - | Used (key, value) -> f acc key value) - acc buckets - - let iter f t = - fold (fun () k v -> f k v) () t - - let size t = - fold (fun n _ _ -> n + 1) 0 t - - let to_seq t k = - iter (fun key value -> k (key, value)) t - - let of_seq ?(size=32) seq = - let cur = ref (empty size) in - seq (fun (k,v) -> cur := replace !cur k v); - !cur -end - -(** {2 Flat hashtable} *) - -module Flat(X : HASH) = struct - type key = X.t - - (** A hashtable is a persistent array of (key, value) buckets *) - type 'a t = { - buckets : 'a bucket PArray.t; - size : int; - } - and 'a bucket = - | Deleted - | Empty - | Used of key * 'a - - let max_load = 0.8 - - (** Empty table. Size will be >= 2 *) - let empty size = - let size = max 2 size in - { buckets = PArray.make size Empty; - size = 0; - } - - let rec is_empty_array a i = - if i = Array.length a then true - else (a.(i) = Empty || a.(i) = Deleted) && is_empty_array a (i+1) - - let is_empty t = is_empty_array (PArray.reroot t.buckets) 0 - - (** Index of slot, for i-th probing starting from hash [h] in - a table of length [n] *) - let addr h n i = ((h land max_int) + i) mod n - - (** Insert (key -> value) in buckets, starting with the hash. *) - let insert buckets h key value = - let n = PArray.length buckets in - (* lookup an empty slot to insert the key->value in. *) - let rec lookup h n i = - let j = addr h n i in - match PArray.get buckets j with - | Empty -> - PArray.set buckets j (Used (key, value)) - | Used (key', _) when X.equal key key' -> - PArray.set buckets j (Used (key, value)) - | _ -> lookup h n (i+1) - in - lookup h n 0 - - (** Resize the array, by inserting its content into twice as large an array *) - let resize buckets = - let new_size = min (PArray.length buckets * 2) Sys.max_array_length in - let buckets' = PArray.make new_size Empty in - (* loop to transfer values from buckets to buckets' *) - let rec tranfer buckets' i = - if i = PArray.length buckets then buckets' - else match PArray.get buckets i with - | Used (key, value) -> - (* insert key -> value into new array *) - let buckets' = insert buckets' (X.hash key) key value in - tranfer buckets' (i+1) - | _ -> - tranfer buckets' (i+1) - in tranfer buckets' 0 - - (** Lookup [key] in the table *) - let find t key = - let buckets = t.buckets in - let n = PArray.length buckets in - let h = X.hash key in - let rec probe h n i num = - if num = n then raise Not_found - else let j = addr h n i in - match PArray.get buckets j with - | Used (key', value) when X.equal key key' -> - value (* found value for this key *) - | Deleted | Used _ -> - probe h n (i+1) (num + 1) (* try next bucket *) - | Empty -> raise Not_found - in - probe h n 0 0 - - (** put [key] -> [value] in the hashtable *) - let replace t key value = - let load = float_of_int t.size /. float_of_int (PArray.length t.buckets) in - let t = - if load > max_load then { t with buckets = resize t.buckets } else t in - let n = PArray.length t.buckets in - let h = X.hash key in - let buckets = t.buckets in - let rec probe h n i = - let j = addr h n i in - match PArray.get buckets j with - | Used (key', _) when X.equal key key' -> - let buckets' = PArray.set buckets j (Used (key, value)) in - { t with buckets = buckets' } (* replace binding *) - | Deleted | Empty -> - let buckets' = PArray.set buckets j (Used (key, value)) in - { buckets = buckets'; size = t.size + 1; } (* add binding *) - | Used _ -> - probe h n (i+1) (* go further *) - in - probe h n 0 - - (** Remove the key from the table *) - let remove t key = - let n = PArray.length t.buckets in - let h = X.hash key in - let buckets = t.buckets in - let rec probe h n i = - let j = addr h n i in - match PArray.get buckets j with - | Used (key', _) when X.equal key key' -> - (* remove slot *) - let buckets' = PArray.set buckets j Deleted in - { buckets = buckets'; size = t.size - 1; } - | Deleted | Used _ -> - probe h n (i+1) (* search further *) - | Empty -> t (* not present *) - in - probe h n 0 - - (** size of the table *) - let size t = t.size - - (** Is the key member of the table? *) - let mem t key = - try ignore (find t key); true - with Not_found -> false - - (** Iterate on key -> value pairs *) - let iter k t = - let buckets = t.buckets in - for i = 0 to PArray.length buckets - 1 do - match PArray.get buckets i with - | Used (key, value) -> k key value - | _ -> () - done - - (** Fold on key -> value pairs *) - let fold f acc t = - PArray.fold_left - (fun acc bucket -> match bucket with - | Used (key, value) -> f acc key value - | _ -> acc) - acc t.buckets - - let to_seq t k = iter (fun key value -> k (key, value)) t - - let of_seq ?(size=32) seq = - let t = ref (empty size) in - seq (fun (k,v) -> t := replace !t k v); - !t -end diff --git a/src/misc/fHashtbl.mli b/src/misc/fHashtbl.mli deleted file mode 100644 index 27866813..00000000 --- a/src/misc/fHashtbl.mli +++ /dev/null @@ -1,96 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional (persistent) hashtable} *) - -type 'a sequence = ('a -> unit) -> unit - -(** {2 Signatures} *) - -module type HASH = sig - type t - val equal : t -> t -> bool - val hash : t -> int -end - -(** The signature for such a functional hashtable *) -module type S = sig - type 'a t - type key - - val empty : int -> 'a t - (** The empty hashtable (with sub-hashtables of given size) *) - - val is_empty : _ t -> bool - - val find : 'a t -> key -> 'a - (** Find the binding for this key, or raise Not_found *) - - val mem : 'a t -> key -> bool - (** Check whether the key is bound in this hashtable *) - - val replace : 'a t -> key -> 'a -> 'a t - (** [replace t key val] returns a copy of [t] where [key] binds to [val] *) - - val remove : 'a t -> key -> 'a t - (** Remove the bindings for the given key *) - - val fold : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b - (** Fold on bindings *) - - val iter : (key -> 'a -> unit) -> 'a t -> unit - (** Iterate on bindings *) - - val size : 'a t -> int - (** Number of bindings *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : ?size:int -> (key * 'a) sequence -> 'a t -end - -(** {2 Persistent array} *) - -module PArray : sig - type 'a t - - val make : int -> 'a -> 'a t - - val get : 'a t -> int -> 'a - - val set : 'a t -> int -> 'a -> 'a t - - val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b - - val length : 'a t -> int -end - -(** {2 Tree-like hashtable} *) - -module Tree(X : HASH) : S with type key = X.t - -(** {2 Flat hashtable} *) - -module Flat(X : HASH) : S with type key = X.t diff --git a/src/misc/flatHashtbl.ml b/src/misc/flatHashtbl.ml deleted file mode 100644 index 1ff59a21..00000000 --- a/src/misc/flatHashtbl.ml +++ /dev/null @@ -1,264 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** Open addressing hashtable, with linear probing. *) - -type 'a sequence = ('a -> unit) -> unit - -module type S = - sig - type key - - type 'a t - - val create : ?max_load:float -> int -> 'a t - (** Create a hashtable. [max_load] is (number of items / size of table). - Must be in ]0, 1[ *) - - val copy : 'a t -> 'a t - - val clear : 'a t -> unit - (** Clear the content of the hashtable *) - - val find : 'a t -> key -> 'a - (** Find the value for this key, or raise Not_found *) - - val replace : 'a t -> key -> 'a -> unit - (** Add/replace the binding for this key. O(1) amortized. *) - - val remove : 'a t -> key -> unit - (** Remove the binding for this key, if any *) - - val length : 'a t -> int - (** Number of bindings in the table *) - - val mem : 'a t -> key -> bool - (** Is the key present in the hashtable? *) - - val iter : (key -> 'a -> unit) -> 'a t -> unit - (** Iterate on bindings *) - - val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - (** Fold on bindings *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : 'a t -> (key * 'a) sequence -> unit - - val stats : 'a t -> int * int * int * int * int * int - (** Cf Weak.S *) - end - -module Make(H : Hashtbl.HashedType) = - struct - type key = H.t - - (** A hashtable is an array of (key, value) buckets that have a state, plus the - size of the table *) - type 'a t = { - mutable buckets : 'a bucket array; - mutable size : int; - max_load : float; - } - and 'a bucket = - | Deleted - | Empty - | Used of key * 'a - - (** Create a table. Size will be >= 2 *) - let create ?(max_load=0.8) size = - let size = max 2 size in - { buckets = Array.make size Empty; - size = 0; - max_load; } - - let copy t = - { buckets = Array.copy t.buckets; - size = t.size; - max_load = t.max_load; - } - - (** clear the table, by resetting all states to Empty *) - let clear t = - Array.fill t.buckets 0 (Array.length t.buckets) Empty; - t.size <- 0 - - (** Index of slot, for i-th probing starting from hash [h] in - a table of length [n] *) - let addr h n i = (h + i) mod n - - (** Insert (key -> value) in buckets, starting with the hash. *) - let insert buckets h key value = - let n = Array.length buckets in - (* lookup an empty slot to insert the key->value in. *) - let rec lookup h n i = - let j = addr h n i in - match buckets.(j) with - | Empty -> - buckets.(j) <- Used (key, value) - | Used (key', _) when H.equal key key' -> - buckets.(j) <- Used (key, value) - | _ -> lookup h n (i+1) - in - lookup h n 0 - - (** Resize the array, by inserting its content into twice as large an array *) - let resize buckets = - let new_size = min (Array.length buckets * 2) Sys.max_array_length in - let buckets' = Array.make new_size Empty in - for i = 0 to Array.length buckets - 1 do - match buckets.(i) with - | Used (key, value) -> - (* insert key -> value into new array *) - insert buckets' (H.hash key) key value - | _ -> () - done; - buckets' - - (** Lookup [key] in the table *) - let find t key = - let n = Array.length t.buckets in - let h = H.hash key in - let buckets = t.buckets in - let rec probe h n i num = - if num = n then raise Not_found - else - let j = addr h n i in - match buckets.(j) with - | Used (key', value) when H.equal key key' -> - value (* found value for this key *) - | Deleted | Used _ -> - probe h n (i+1) (num + 1) (* try next bucket *) - | Empty -> raise Not_found - in - probe h n 0 0 - - (** put [key] -> [value] in the hashtable *) - let replace t key value = - let load = float_of_int t.size /. float_of_int (Array.length t.buckets) in - (if load > t.max_load then t.buckets <- resize t.buckets); - let n = Array.length t.buckets in - let h = H.hash key in - let buckets = t.buckets in - let rec probe h n i = - let j = addr h n i in - match buckets.(j) with - | Used (key', _) when H.equal key key' -> - buckets.(j) <- Used (key, value) (* replace value *) - | Deleted | Empty -> - buckets.(j) <- Used (key, value); - t.size <- t.size + 1 (* insert and increment size *) - | Used _ -> - probe h n (i+1) (* go further *) - in - probe h n 0 - - (** Remove the key from the table *) - let remove t key = - let n = Array.length t.buckets in - let h = H.hash key in - let buckets = t.buckets in - let rec probe h n i = - let j = addr h n i in - match buckets.(j) with - | Used (key', _) when H.equal key key' -> - buckets.(j) <- Deleted; - t.size <- t.size - 1 (* remove slot *) - | Deleted | Used _ -> - probe h n (i+1) (* search further *) - | Empty -> () (* not present *) - in - probe h n 0 - - (** size of the table *) - let length t = t.size - - (** Is the key member of the table? *) - let mem t key = - try ignore (find t key); true - with Not_found -> false - - (** Iterate on key -> value pairs *) - let iter k t = - let buckets = t.buckets in - for i = 0 to Array.length buckets - 1 do - match buckets.(i) with - | Used (key, value) -> k key value - | _ -> () - done - - (** Fold on key -> value pairs *) - let fold f t acc = - let buckets = t.buckets in - let rec fold acc i = - if i = Array.length buckets - then acc - else match buckets.(i) with - | Used (key, value) -> fold (f key value acc) (i+1) - | _ -> fold acc (i+1) - in fold acc 0 - - let to_seq t k = - iter (fun key value -> k (key, value)) t - - let of_seq t seq = - seq (fun (k,v) -> replace t k v) - - (** Statistics on the table *) - let stats t = (Array.length t.buckets, t.size, t.size, 0, 0, 1) - end - -(** Hashconsed type *) -module type HashconsedType = - sig - include Hashtbl.HashedType - val tag : int -> t -> t - end - -(** Create a hashconsing module *) -module Hashcons(H : HashconsedType) = - struct - module Table = Make(H) - - type t = H.t - - let table = Table.create 5003 - - let count = ref 0 - - let hashcons x = - try Table.find table x - with Not_found -> - let x' = H.tag !count x in - incr count; - Table.replace table x' x'; - x' - - let iter k = - Table.iter (fun _ x -> k x) table - - let stats () = - Table.stats table - end diff --git a/src/misc/flatHashtbl.mli b/src/misc/flatHashtbl.mli deleted file mode 100644 index 55b462a7..00000000 --- a/src/misc/flatHashtbl.mli +++ /dev/null @@ -1,97 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** Open addressing hashtable, with linear probing. *) - -type 'a sequence = ('a -> unit) -> unit - -module type S = - sig - type key - - type 'a t - - val create : ?max_load:float -> int -> 'a t - (** Create a hashtable. [max_load] is (number of items / size of table). - Must be in {v ]0, 1[ v} *) - - val copy : 'a t -> 'a t - - val clear : 'a t -> unit - (** Clear the content of the hashtable *) - - val find : 'a t -> key -> 'a - (** Find the value for this key, or raise Not_found *) - - val replace : 'a t -> key -> 'a -> unit - (** Add/replace the binding for this key. O(1) amortized. *) - - val remove : 'a t -> key -> unit - (** Remove the binding for this key, if any *) - - val length : 'a t -> int - (** Number of bindings in the table *) - - val mem : 'a t -> key -> bool - (** Is the key present in the hashtable? *) - - val iter : (key -> 'a -> unit) -> 'a t -> unit - (** Iterate on bindings *) - - val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - (** Fold on bindings *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : 'a t -> (key * 'a) sequence -> unit - - val stats : 'a t -> int * int * int * int * int * int - (** Cf Weak.S *) - end - -(** Create a hashtable *) -module Make(H : Hashtbl.HashedType) : S with type key = H.t - -(** The hashconsing part has the very bad property that it may introduce - memory leak, because the hashtable is not weak. Be warned. *) - -(** Hashconsed type *) -module type HashconsedType = - sig - include Hashtbl.HashedType - val tag : int -> t -> t - end - -(** Create a hashconsing module *) -module Hashcons(H : HashconsedType) : - sig - type t = H.t - - val hashcons : t -> t - - val iter : (t -> unit) -> unit - - val stats : unit -> int * int * int * int * int * int - end diff --git a/src/misc/hGraph.ml b/src/misc/hGraph.ml deleted file mode 100644 index 9abfaab3..00000000 --- a/src/misc/hGraph.ml +++ /dev/null @@ -1,374 +0,0 @@ - -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {2 Hypergraph Representation} - -CCGeneralized Hypergraphs. Objects are either constants, or hyperedges that -connect [n] other objets together (a [n]-tuple). Each hyperedge can contain -additional data. -*) - -module type S = sig - type const - (** Constants. Those are what can annotate hyperedges or make single, - leaf, nodes. *) - - type t - (** An hypergraph. It stores a set of edges, and possibly inherits from - another graph. *) - - type edge - (** A single edge of the hypergraph. *) - - val self : t -> edge - (** The edge that represents (reifies) the hypergraph itself *) - - val eq : edge -> edge -> bool - (** Equality of the two edges. *) - - val arity : edge -> int - (** Number of sub-elements of the edge (how many other edges it connects - together) *) - - val nth : edge -> int -> edge - (** [nth x i] accesses the [i]-th sub-node of [x]. - @raise Invalid_argument if [i >= arity x]. *) - - val make_graph : ?parent:t -> unit -> t - (** New graph, possibly inheriting from another graph. *) - - val make_edge : t -> edge array -> edge - (** Create a new hyperedge from an ordered tuple of sub-edges. - The edge belongs to the given graph. - The array must not be used afterwards and must not be empty. - @raise Invalid_argument if the array is empty *) - - val make_const : t -> const -> edge - (** Constant edge, without sub-edges *) - - val fresh : t -> edge - (** Fresh edge, without constant. It is equal to no other edge. *) - - module EdgeTbl : Hashtbl.S with type key = edge - - val pp : ?printed:unit EdgeTbl.t -> - Buffer.t -> edge -> unit - (** Print the edge on the buffer. @param printed: sub-edges already - printed. *) - - val fmt : Format.formatter -> edge -> unit - val to_string : edge -> string -end - -module type PARAM = sig - type const - - val eq : const -> const -> bool - val hash : const -> int - val to_string : const -> string (* for printing *) -end - -module Make(P : PARAM) = struct - type const = P.const - - type edge = - | Fresh of int - | Const of const - | Edge of edge array - - let rec eq e1 e2 = match e1, e2 with - | Fresh _, Fresh _ -> e1 == e2 - | Const c1, Const c2 -> P.eq c1 c2 - | Edge a1, Edge a2 -> - Array.length a1 = Array.length a2 && - begin try - for i = 0 to Array.length a1 - 1 do - if not (eq (Array.unsafe_get a1 i) (Array.unsafe_get a2 i)) - then raise Exit; - done; true - with Exit -> false - end - | _ -> false - - let rec hash e = match e with - | Fresh i -> i - | Const c -> P.hash c - | Edge a -> - let h = ref 0 in - for i = 0 to Array.length a - 1 do - h := max_int land (!h * 65599 + (hash (Array.unsafe_get a i))) - done; - !h - - (* hashtable on edges *) - module EdgeTbl = Hashtbl.Make(struct - type t = edge - let equal = eq - let hash = hash - end) - - (* hashtable on edges * int *) - module BackTbl = Hashtbl.Make(struct - type t = edge * int - let equal (e1, i1) (e2, i2) = i1 = i2 && eq e1 e2 - let hash (e, i) = i * 65599 + hash e - end) - - (** Hypergraph: set of edges. We map each edge to other edges that point - to it (knowing which ones it points to is trivial) *) - type t = { - edges : unit EdgeTbl.t; - backref : edge BackTbl.t; - parent : t option; - mutable count : int; (* used for Fresh nodes *) - self : edge; - } - - let arity e = match e with - | Fresh _ - | Const _ -> 0 - | Edge a -> Array.length a - - let nth e i = match e with - | Fresh _ - | Const _ -> raise (Invalid_argument"HGraph.nth") - | Edge a -> a.(i) - - let self g = g.self - - let make_graph ?parent () = - let g = { - parent; - edges = EdgeTbl.create 15; - backref = BackTbl.create 15; - count = 1; - self = Fresh 0; - } in - g - - (* add a backref from [e]'s sub-edges to [e] *) - let _add_backrefs g e = match e with - | Fresh _ - | Const _ -> assert false - | Edge a -> - for i = 0 to Array.length a - 1 do - BackTbl.add g.backref (Array.unsafe_get a i, i) e - done - - let make_edge g sub = - if Array.length sub = 0 then raise (Invalid_argument "HGraph.make_edge"); - let e = Edge sub in - (* add edge if not already present *) - if not (EdgeTbl.mem g.edges e) then begin - EdgeTbl.add g.edges e (); - _add_backrefs g e - end; - e - - let make_const g c = - let e = Const c in - if not (EdgeTbl.mem g.edges e) then - EdgeTbl.add g.edges e (); - e - - let fresh g = - let e = Fresh g.count in - g.count <- g.count + 1; - (* always new! *) - EdgeTbl.add g.edges e (); - e - - let pp ?(printed=EdgeTbl.create 7) buf e = - let rec pp buf e = match e with - | Fresh i -> Printf.bprintf buf "_e%d" i - | Const c -> Buffer.add_string buf (P.to_string c) - | Edge a -> - if not (EdgeTbl.mem printed e) then begin - EdgeTbl.add printed e (); - Buffer.add_char buf '['; - for i = 0 to Array.length a - 1 do - if i > 0 then Buffer.add_char buf ' '; - pp buf a.(i) - done; - Buffer.add_char buf ']' - end - in - pp buf e - - let to_string e = - let buf = Buffer.create 15 in - pp buf e; - Buffer.contents buf - - let fmt fmt e = - Format.pp_print_string fmt (to_string e) -end - -(** {2 Useful default} *) - -module DefaultParam = struct - type const = - | S of string - | I of int - - type data = unit - - let eq c1 c2 = match c1, c2 with - | S s1, S s2 -> s1 = s2 - | I i1, I i2 -> i1 = i2 - | _ -> false - - let hash = function - | S s -> Hashtbl.hash s - | I i -> i - - let to_string = function - | S s -> s - | I i -> string_of_int i - - let i i = I i - let s s = S s -end - -module Default = struct - include Make(DefaultParam) - - exception EOI - exception Error of string - - module Lexbuf = struct - type t = { - mutable s : string; - mutable i : int; - get : (unit -> string option); - } - - let of_string s = { s; i=0; get = (fun () -> None); } - - let of_fun get = { s=""; i = 0; get; } - - let of_chan c = - let s = String.make 64 ' ' in - let get () = - try - let n = input c s 0 64 in - Some (String.sub s 0 n) - with End_of_file -> None - in - { s = ""; i = 0; get; } - end - - let rec _get_rec lb = - if lb.Lexbuf.i >= String.length lb.Lexbuf.s - then match lb.Lexbuf.get () with - | None -> raise EOI - | Some s' -> - lb.Lexbuf.s <- s'; - lb.Lexbuf.i <- 0; - _get_rec lb - else lb.Lexbuf.s.[lb.Lexbuf.i] - - let _get lb = - if lb.Lexbuf.i >= String.length lb.Lexbuf.s - then _get_rec lb - else lb.Lexbuf.s.[lb.Lexbuf.i] - - let _skip lb = lb.Lexbuf.i <- lb.Lexbuf.i + 1 - - (* skip whitespace *) - let rec _white lb = - match _get lb with - | ' ' | '\t' | '\n' -> _skip lb; _white lb - | _ -> () - - (* read lb, expecting the given char *) - let _expect lb c = - if _get lb = c - then _skip lb - else raise (Error (Printf.sprintf "expected %c" c)) - - let rec __parse_edge g lb = - _white lb; - match _get lb with - | '[' -> - _skip lb; - let sub = __parse_edges g [] lb in - let sub = match sub with - | [] -> raise (Error "parsed an empty list of sub-edges") - | _ -> Array.of_list sub - in - _white lb; - _expect lb ']'; - make_edge g sub - | '0' .. '9' -> - let i = _parse_int 0 lb in - make_const g (DefaultParam.I i) - | '_' -> - _skip lb; - fresh g - | _ -> - let s = _parse_str (Buffer.create 15) lb in - make_const g (DefaultParam.S s) - - and __parse_edges g acc lb = - _white lb; - match _get lb with - | ']' -> List.rev acc (* done *) - | _ -> - let e = __parse_edge g lb in - __parse_edges g (e::acc) lb - - and _parse_int i lb = - match _get lb with - | ('0' .. '9') as c -> - let n = Char.code c - Char.code '0' in - _skip lb; - _parse_int ((i * 10) + n) lb - | _ -> i - - and _parse_str buf lb = - match _get lb with - | ' ' | '\t' | '\n' | ']' -> Buffer.contents buf (* done *) - | '\\' -> - (* must read next char *) - _skip lb; - Buffer.add_char buf (_get lb); - _skip lb; - _parse_str buf lb - | c -> - Buffer.add_char buf c; - _skip lb; - _parse_str buf lb - - (* parse one edge *) - let parse_edge g lb = - try `Ok (__parse_edge g lb) - with - | EOI -> `Error "unexpected end of input" - | Error e -> `Error e - - let edge_of_string g s = parse_edge g (Lexbuf.of_string s) -end diff --git a/src/misc/hGraph.mli b/src/misc/hGraph.mli deleted file mode 100644 index a182a93d..00000000 --- a/src/misc/hGraph.mli +++ /dev/null @@ -1,127 +0,0 @@ - -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {2 Hypergraph Representation} - -CCGeneralized Hypergraphs. Objects are either constants, or hyperedges that -connect [n] other objets together (a [n]-tuple). - -Hashconsing is used to ensure that structural equality implies physical -equality. This makes this module non thread safe. -*) - -module type S = sig - type const - (** Constants. Those are what can annotate hyperedges or make single, - leaf, nodes. *) - - type t - (** An hypergraph. It stores a set of edges, and possibly inherits from - another graph. *) - - type edge - (** A single edge of the hypergraph. *) - - val self : t -> edge - (** The edge that represents (reifies) the hypergraph itself *) - - val eq : edge -> edge -> bool - (** Equality of the two edges. *) - - val arity : edge -> int - (** Number of sub-elements of the edge (how many other edges it connects - together) *) - - val nth : edge -> int -> edge - (** [nth x i] accesses the [i]-th sub-node of [x]. - @raise Invalid_argument if [i >= arity x]. *) - - val make_graph : ?parent:t -> unit -> t - (** New graph, possibly inheriting from another graph. *) - - val make_edge : t -> edge array -> edge - (** Create a new hyperedge from an ordered tuple of sub-edges. - The edge belongs to the given graph. - The array must not be used afterwards and must not be empty. - @raise Invalid_argument if the array is empty *) - - val make_const : t -> const -> edge - (** Constant edge, without sub-edges *) - - val fresh : t -> edge - (** Fresh edge, without constant. It is equal to no other edge. *) - - module EdgeTbl : Hashtbl.S with type key = edge - - val pp : ?printed:unit EdgeTbl.t -> - Buffer.t -> edge -> unit - (** Print the edge on the buffer. @param printed: sub-edges already - printed. *) - - val fmt : Format.formatter -> edge -> unit - val to_string : edge -> string -end - -module type PARAM = sig - type const - - val eq : const -> const -> bool - val hash : const -> int - val to_string : const -> string (* for printing *) -end - -module Make(P : PARAM) : S with type const = P.const - -(** {2 Useful default} *) - -module DefaultParam : sig - type const = - | S of string - | I of int - - include PARAM with type const := const - - val i : int -> const - val s : string -> const -end - -module Default : sig - include S with type const = DefaultParam.const - - module Lexbuf : sig - type t - - val of_string : string -> t - - val of_fun : (unit -> string option) -> t - - val of_chan : in_channel -> t - end - - val parse_edge : t -> Lexbuf.t -> [ `Ok of edge | `Error of string ] - - val edge_of_string : t -> string -> [ `Ok of edge | `Error of string ] -end diff --git a/src/misc/hashset.ml b/src/misc/hashset.ml deleted file mode 100644 index 110e4994..00000000 --- a/src/misc/hashset.ml +++ /dev/null @@ -1,75 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Mutable polymorphic hash-set} *) - -type 'a sequence = ('a -> unit) -> unit - -type 'a t = ('a, unit) PHashtbl.t - (** A set is a hashtable, with trivial values *) - -let empty ?max_load ?eq ?hash size = - PHashtbl.create ?max_load ?eq ?hash size - -let copy set = PHashtbl.copy set - -let clear set = PHashtbl.clear set - -let cardinal set = PHashtbl.length set - -let mem set x = PHashtbl.mem set x - -let add set x = PHashtbl.add set x () - -let remove set x = PHashtbl.remove set x - -let iter f set = PHashtbl.iter (fun x () -> f x) set - -let fold f acc set = PHashtbl.fold (fun acc x () -> f acc x) acc set - -let filter p set = PHashtbl.filter (fun x () -> p x) set - -let to_seq set k = iter k set - -let of_seq set seq = - seq (fun x -> add set x) - -let union ?into (s1 : 'a t) (s2 : 'a t) = - let into = match into with - | Some s -> of_seq s (to_seq s1); s - | None -> copy s1 in - of_seq into (to_seq s2); - into - -let seq_filter p seq k = - seq (fun x -> if p x then k x) - -let inter ?into (s1 : 'a t) (s2 : 'a t) = - let into = match into with - | Some s -> s - | None -> empty ~eq:s1.PHashtbl.eq ~hash:s1.PHashtbl.hash (cardinal s1) in - (* add to [into] elements of [s1] that also belong to [s2] *) - of_seq into (seq_filter (fun x -> mem s2 x) (to_seq s1)); - into diff --git a/src/misc/hashset.mli b/src/misc/hashset.mli deleted file mode 100644 index f421c557..00000000 --- a/src/misc/hashset.mli +++ /dev/null @@ -1,64 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Mutable polymorphic hash-set} *) - -type 'a sequence = ('a -> unit) -> unit - -type 'a t = ('a, unit) PHashtbl.t - (** A set is a hashtable, with trivial values *) - -val empty : ?max_load:float -> ?eq:('a -> 'a -> bool) -> - ?hash:('a -> int) -> int -> 'a t - (** See {!PHashtbl.create} *) - -val copy : 'a t -> 'a t - -val clear : 'a t -> unit - -val cardinal : 'a t -> int - -val mem : 'a t -> 'a -> bool - -val add : 'a t -> 'a -> unit - -val remove : 'a t -> 'a -> unit - -val iter : ('a -> unit) -> 'a t -> unit - -val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b - -val filter : ('a -> bool) -> 'a t -> unit - (** destructive filter (remove elements that do not satisfy the predicate) *) - -val to_seq : 'a t -> 'a sequence - -val of_seq : 'a t -> 'a sequence -> unit - -val union : ?into:'a t -> 'a t -> 'a t -> 'a t - (** Set union. The result is stored in [into] *) - -val inter : ?into:'a t -> 'a t -> 'a t -> 'a t - (** Set intersection. The result is stored in [into] *) diff --git a/src/misc/heap.ml b/src/misc/heap.ml deleted file mode 100644 index 7b402d51..00000000 --- a/src/misc/heap.ml +++ /dev/null @@ -1,130 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Imperative priority queue} *) - -type 'a sequence = ('a -> unit) -> unit - -type 'a t = { - mutable tree : 'a tree; - cmp : 'a -> 'a -> int; -} (** A splay tree heap with the given comparison function *) -and 'a tree = - | Empty - | Node of ('a tree * 'a * 'a tree) - (** A splay tree containing values of type 'a *) - -let empty ~cmp = { - tree = Empty; - cmp; -} - -let is_empty h = - match h.tree with - | Empty -> true - | Node _ -> false - -(** Partition the tree into (elements <= pivot, elements > pivot) *) -let rec partition ~cmp pivot tree = - match tree with - | Empty -> Empty, Empty - | Node (a, x, b) -> - if cmp x pivot <= 0 - then begin - match b with - | Empty -> (tree, Empty) - | Node (b1, y, b2) -> - if cmp y pivot <= 0 - then - let small, big = partition ~cmp pivot b2 in - Node (Node (a, x, b1), y, small), big - else - let small, big = partition ~cmp pivot b1 in - Node (a, x, small), Node (big, y, b2) - end else begin - match a with - | Empty -> (Empty, tree) - | Node (a1, y, a2) -> - if cmp y pivot <= 0 - then - let small, big = partition ~cmp pivot a2 in - Node (a1, y, small), Node (big, x, b) - else - let small, big = partition ~cmp pivot a1 in - small, Node (big, y, Node (a2, x, b)) - end - -(** Insert the element in the tree *) -let insert h x = - let small, big = partition ~cmp:h.cmp x h.tree in - let tree' = Node (small, x, big) in - h.tree <- tree' - -(** Access minimum value *) -let min h = - let rec min tree = - match tree with - | Empty -> raise Not_found - | Node (Empty, x, _) -> x - | Node (l, _, _) -> min l - in min h.tree - -(** Get minimum value and remove it from the tree *) -let pop h = - let rec delete_min tree = match tree with - | Empty -> raise Not_found - | Node (Empty, x, b) -> x, b - | Node (Node (Empty, x, b), y, c) -> - x, Node (b, y, c) (* rebalance *) - | Node (Node (a, x, b), y, c) -> - let m, a' = delete_min a in - m, Node (a', x, Node (b, y, c)) - in - let m, tree' = delete_min h.tree in - h.tree <- tree'; - m - -let junk h = - ignore (pop h) - -(** Iterate on elements *) -let iter h f = - let rec iter tree = - match tree with - | Empty -> () - | Node (a, x, b) -> - iter a; f x; iter b - in iter h.tree - -let size h = - let r = ref 0 in - iter h (fun _ -> incr r); - !r - -let to_seq h = - fun k -> iter h k - -let of_seq h seq = - seq (fun elt -> insert h elt) diff --git a/src/misc/heap.mli b/src/misc/heap.mli deleted file mode 100644 index e9adee7c..00000000 --- a/src/misc/heap.mli +++ /dev/null @@ -1,58 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Imperative priority queue} *) - -type 'a sequence = ('a -> unit) -> unit - -type 'a t - (** A heap containing values of type 'a *) - -val empty : cmp:('a -> 'a -> int) -> 'a t - (** Create an empty heap *) - -val insert : 'a t -> 'a -> unit - (** Insert a value in the heap *) - -val is_empty : 'a t -> bool - (** Check whether the heap is empty *) - -val min : 'a t -> 'a - (** Access the minimal value of the heap, or raises Invalid_argument *) - -val junk : 'a t -> unit - (** Discard the minimal element *) - -val pop : 'a t -> 'a - (** Remove and return the mininal value (or raise Invalid_argument) *) - -val iter : 'a t -> ('a -> unit) -> unit - (** Iterate on the elements, in an unspecified order *) - -val size : _ t -> int - -val to_seq : 'a t -> 'a sequence - -val of_seq : 'a t -> 'a sequence -> unit diff --git a/src/misc/iteratee.ml b/src/misc/iteratee.ml deleted file mode 100644 index 25fb383d..00000000 --- a/src/misc/iteratee.ml +++ /dev/null @@ -1,73 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -type 'a t = { - fold: 'b. ('b -> 'a -> [`Continue | `Stop] * 'b) -> 'b -> 'b -} - -exception StopNow - -let of_iter i = { - fold = (fun f acc -> - let r = ref acc in - begin try i (fun x -> - let cont, acc' = f !r x in - r := acc'; - match cont with - | `Stop -> raise StopNow - | `Continue -> ()); - with StopNow -> () - end; - !r - ); -} - -let fold f acc i = - i.fold (fun acc x -> `Continue, f acc x) acc - -let iter f i = - i.fold (fun () x -> f x; `Continue, ()) () - -let map f i = { - fold=(fun g acc -> - i.fold (fun acc x -> g acc (f x)) acc - ) -} - -let of_list l = - let rec next f acc l = match l with - | [] -> acc - | x::l' -> - match f acc x with - | `Continue, acc' -> next f acc' l' - | `Stop, res -> res - in - {fold=(fun f acc -> next f acc l) } - -let to_rev_list i = - i.fold (fun acc x -> `Continue, x::acc) [] - -let to_list i = List.rev (to_rev_list i) diff --git a/src/misc/iteratee.mli b/src/misc/iteratee.mli deleted file mode 100644 index f21843c5..00000000 --- a/src/misc/iteratee.mli +++ /dev/null @@ -1,44 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Stoppable Folds} *) - -type 'a t = { - fold: 'b. ('b -> 'a -> [`Continue | `Stop] * 'b) -> 'b -> 'b -} - -val of_iter : (('a -> unit) -> unit) -> 'a t - -val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b - -val iter : ('a -> unit) -> 'a t -> unit - -val map : ('a -> 'b) -> 'a t -> 'b t - -val of_list : 'a list -> 'a t - -val to_rev_list : 'a t -> 'a list -val to_list : 'a t -> 'a list diff --git a/src/misc/json.ml b/src/misc/json.ml deleted file mode 100644 index 051434ff..00000000 --- a/src/misc/json.ml +++ /dev/null @@ -1,172 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Very simple JSON parser/printer} *) - -type t = - | Int of int - | Float of float - | String of string - | Null - | Bool of bool - | List of t list - | Object of (string * t) list - -(** {2 Print/parse} *) - -let lex = - Genlex.make_lexer ["{"; "}"; ":"; ","; "["; "]"; "true"; "false"; "null"] - -exception EOF - -let parse chars = - let tokens = lex chars in - let open Stream in - let rec next () = - match peek tokens with - | None -> raise EOF (* end stream *) - | Some (Genlex.Kwd "{") -> - junk tokens; - let args = read_pairs [] in - (match peek tokens with - | Some (Genlex.Kwd "}") -> - junk tokens; Object args - | _ -> raise (Stream.Error "expected '}'")) - | Some (Genlex.Kwd "[") -> - junk tokens; - let args = read_list [] in - (match peek tokens with - | Some (Genlex.Kwd "]") -> - junk tokens; List args - | _ -> raise (Stream.Error "expected ']'")) - | Some (Genlex.Int i) -> junk tokens; Int i - | Some (Genlex.Float f) -> junk tokens; Float f - | Some (Genlex.Kwd "true") -> junk tokens; Bool true - | Some (Genlex.Kwd "false") -> junk tokens; Bool false - | Some (Genlex.Kwd "null") -> junk tokens; Null - | Some (Genlex.String s) -> junk tokens; String s - | _ -> raise (Stream.Error "expected JSON value") - and read_list acc = - match peek tokens with - | Some (Genlex.Kwd "]") -> List.rev acc (* yield *) - | _ -> - let t = next () in - (match peek tokens with - | Some (Genlex.Kwd ",") -> - junk tokens; - read_list (t::acc) (* next *) - | Some (Genlex.Kwd "]") -> - read_list (t::acc) (* next *) - | _ -> raise (Stream.Error "expected ','")) - and read_pairs acc = - match peek tokens with - | Some (Genlex.Kwd "}") -> List.rev acc (* yield *) - | _ -> - let k, v = pair () in - (match peek tokens with - | Some (Genlex.Kwd ",") -> - junk tokens; - read_pairs ((k,v)::acc) (* next *) - | Some (Genlex.Kwd "}") -> - read_pairs ((k,v)::acc) (* next *) - | _ -> raise (Stream.Error "expected ','")) - and pair () = - match Stream.npeek 2 tokens with - | [Genlex.String k; Genlex.Kwd ":"] -> - junk tokens; junk tokens; - let v = next () in - k, v - | _ -> raise (Stream.Error "expected pair") - in - Stream.from - (fun _ -> - try Some (next ()) - with EOF -> None) - -let parse_one chars = - Stream.peek (parse chars) - -let rec output oc t = - match t with - | Null -> output_string oc "null" - | Bool true -> output_string oc "true" - | Bool false -> output_string oc "false" - | Int i -> Printf.fprintf oc "%d" i - | Float f -> Printf.fprintf oc "%f" f - | String s -> Printf.fprintf oc "\"%s\"" (String.escaped s) - | List l -> - output_string oc "["; - List.iteri - (fun i t -> - (if i > 0 then output_string oc ", "); - output oc t) - l; - output_string oc "]" - | Object pairs -> - output_string oc "{"; - List.iteri - (fun i (k,v) -> - (if i > 0 then output_string oc ", "); - Printf.fprintf oc "\"%s\": " k; - output oc v) - pairs; - output_string oc "}" - -let rec pp fmt t = - match t with - | Null -> Format.pp_print_string fmt "null" - | Bool true -> Format.pp_print_string fmt "true" - | Bool false -> Format.pp_print_string fmt "false" - | Int i -> Format.fprintf fmt "%d" i - | Float f -> Format.fprintf fmt "%f" f - | String s -> Format.fprintf fmt "\"%s\"" (String.escaped s) - | List l -> - Format.pp_print_string fmt "["; - List.iteri - (fun i t -> - (if i > 0 then Format.pp_print_string fmt ", "); - pp fmt t) - l; - Format.pp_print_string fmt "]" - | Object pairs -> - Format.pp_print_string fmt "{"; - List.iteri - (fun i (k,v) -> - (if i > 0 then Format.pp_print_string fmt ", "); - Format.fprintf fmt "\"%s\": " k; - pp fmt v) - pairs; - Format.pp_print_string fmt "}" - -let to_string t = - let buf = Buffer.create 16 in - let fmt = Format.formatter_of_buffer buf in - Format.fprintf fmt "%a@?" pp t; - Buffer.contents buf - -(** {2 Utils *) - -exception TypeError of string * t - diff --git a/src/misc/json.mli b/src/misc/json.mli deleted file mode 100644 index 3c112d77..00000000 --- a/src/misc/json.mli +++ /dev/null @@ -1,62 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Very simple JSON parser/printer} *) - -type t = - | Int of int - | Float of float - | String of string - | Null - | Bool of bool - | List of t list - | Object of (string * t) list - -(** {2 Print/parse} *) - -val parse : char Stream.t -> t Stream.t - -val parse_one : char Stream.t -> t option - -val output : out_channel -> t -> unit - -val pp : Format.formatter -> t -> unit - -val to_string : t -> string - -(** {2 Utils *) - -exception TypeError of string * t - -(* -val to_int : t -> int -val to_float : t -> float -val to_string : t -> string -val to_bool : t -> bool -val to_null : t -> unit -val to_list : t -> t list -val to_object : t -> (string * t) list - -*) diff --git a/src/misc/parseReact.ml b/src/misc/parseReact.ml deleted file mode 100644 index 99b7c12e..00000000 --- a/src/misc/parseReact.ml +++ /dev/null @@ -1,237 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Parser combinators driven by the input} *) - -type ('a, 'b) t = - | Return : 'b -> ('a,'b) t - | Delay : (unit -> ('a, 'b) t) -> ('a, 'b) t - | One : ('a, 'a) t - | Stop : ('a, unit) t - | Bind : ('a, 'b) t * ('b -> ('a, 'c) t) -> ('a, 'c) t - | Choice : ('a, 'b) t * ('a, 'b) t -> ('a, 'b) t - | Map : ('a, 'b) t * ('b -> 'c) -> ('a, 'c) t - | Guard : ('a, 'b) t * ('b -> bool) -> ('a, 'b) t - | Skip : ('a, unit) t - | IfThenElse: ('a -> bool) * ('a, 'b) t * ('a, 'b) t -> ('a, 'b) t - | Fail : ('a, 'b) t - -let stop = Stop - -let return x = Return x - -let delay f = Delay f - -let return' f = Delay (fun () -> return (f ())) - -let fail = Fail - -let one = One - -let skip = Skip - -let bind f p = Bind (p, f) - -let (>>=) p f = bind f p - -let exact ?(eq=(=)) x = - one - >>= fun y -> - if eq x y then Return () else Fail - -let guard f p = Guard (p, f) - -let (>>) p1 p2 = p1 >>= fun _ -> p2 - -let map f p = Map (p, f) - -let (>>|) p f = Map (p, f) - -let (<|>) p1 p2 = Choice (p1, p2) - -let pair p1 p2 = - p1 >>= fun x1 -> - p2 >>= fun x2 -> - return (x1, x2) - -let triple p1 p2 p3 = - p1 >>= fun x1 -> - p2 >>= fun x2 -> - p3 >>= fun x3 -> - return (x1, x2, x3) - -let if_then_else p a b = IfThenElse (p, a, b) - -(** {6 Utils} *) - -let take_while pred = - let rec next acc = - if_then_else pred - (one >>= fun x -> next (x::acc)) - (return' (fun () -> List.rev acc)) - in - next [] - -let take_n n = - let rec next acc n = - if n = 0 - then return (List.rev acc) - else one >>= fun x -> next (x::acc) (n-1) - in - next [] n - -let skip_spaces = - let rec next () = - if_then_else - (fun c -> c = ' ' || c = '\t' || c = '\n') - (skip >> delay next) - (return ()) - in next () - -let ident = - let accept = function - | c when Char.code c >= Char.code 'a' && Char.code c <= Char.code 'z' -> true - | c when Char.code c >= Char.code 'A' && Char.code c <= Char.code 'Z' -> true - | c when Char.code c >= Char.code '0' && Char.code c <= Char.code '9' -> true - | _ -> false - in - let rec aggregate buf = - if_then_else - accept - (one >>= fun c -> Buffer.add_char buf c; aggregate buf) - (return (Buffer.contents buf)) - in - (* create buffer on demand, to avoid sharing it *) - delay (fun () -> aggregate (Buffer.create 32)) - -let many ~sep p = - let rec next acc = - (return (List.rev acc)) - <|> (p >>= fun x -> sep >> next (x::acc)) - in - next [] - -let many1 ~sep p = - let rec next acc = - p >>= fun x -> - let acc = x :: acc in - (return (List.rev acc)) - <|> (sep >> next acc) - in - next [] - -(** {6 Run} *) - -type 'a sequence = ('a -> unit) -> unit - -let _fold_seq f acc seq = - let acc = ref acc in - seq (fun x -> acc := f !acc x); - !acc - -(** Partial state during parsing: a tree of continuations *) -type (_, _) state = - | STBottom : 'b -> ('a, 'b) state - | STPush : ('a, 'c) t * ('c -> ('a, 'b) state list) -> ('a, 'b) state - -let (>>>) p cont = STPush (p, cont) - -let run p seq = - (* normalize the stack (do not let a "return" on top) *) - let rec reduce : type a b. (a,b)state -> (a,b) state list - = fun stack -> match stack with - | STPush (Return x, cont) -> CCList.flat_map reduce (cont x) - | STPush (Delay f, cont) -> reduce (f () >>> cont) - | STPush (Bind (p, f), cont) -> - let stack' = p >>> fun x -> [f x >>> cont] in - reduce stack' - | STPush (Choice (a, b), cont) -> - (* fork into sub-stacks *) - CCList.append (reduce (a >>> cont)) (reduce (b >>> cont)) - | STPush (Map (p, f), cont) -> - let stack' = p >>> fun x -> cont (f x) in - reduce stack' - | STPush (Guard (p, f), cont) -> - let stack' = p >>> fun x -> if f x then cont x else [] in - reduce stack' - | _ -> [stack] - in - (* consume one input token *) - let rec consume_one : type a b. (a,b) state -> a -> (a,b) state list - = fun stack x -> match stack with - | STBottom _ -> [] (* fail *) - | STPush (Stop, _) -> [] (* fail *) - | STPush (Fail, _) -> [] (* fail *) - | STPush (One, cont) -> CCList.flat_map reduce (cont x) - | STPush (Skip, cont) -> CCList.flat_map reduce (cont ()) - | STPush (IfThenElse (p, yay, nay), cont) -> - let l = if p x - then reduce (yay >>> cont) - else reduce (nay >>> cont) - in - CCList.flat_map (fun stack -> consume_one stack x) l - | STPush (Return _, _) -> assert false - | STPush (Delay _, _) -> assert false - | STPush (Bind _, _) -> assert false - | STPush (Choice _, _) -> assert false - | STPush (Map _, _) -> assert false - | STPush (Guard _, _) -> assert false - in - (* to be called at the end of input *) - let finish : type a b. (a,b) state -> (a,b) state list - = fun stack -> match stack with - | STPush (Stop, cont) -> CCList.flat_map reduce (cont ()) - | STPush (Fail, _) -> [] - | _ -> [stack] - in - (* how to parse the input: step by step, starting with [p] as initial parser *) - let step l x = CCList.flat_map (fun p -> consume_one p x) l in - let initial_state = p >>> fun x -> [STBottom x] in - let res = _fold_seq step (reduce initial_state) seq in - (* signal "end of input" *) - let res = CCList.flat_map finish res in - (* recover results *) - CCList.filter_map - (function - | STBottom x -> Some x - | _ -> None - ) res - - -(*$R - let module S = struct type t = Atom of string | List of t list end in - let open S in - let (%) f g x = f (g x) in - let atom i = Atom i in - let list_ i = List i in - let rec p () = - (skip_spaces >> ident >>= (return % atom)) - <|> (skip_spaces >> exact '(' >> many1 ~sep:(exact ' ') (delay p) >>= fun l -> - skip_spaces >> exact ')' >> return (list_ l)) - in - let res = run (p ()) (Sequence.of_str "(a b (c d))") in - assert_equal res [list_ [atom "a"; atom "b"; list_ [atom "c"; atom "d"]]] -*) diff --git a/src/misc/parseReact.mli b/src/misc/parseReact.mli deleted file mode 100644 index da823495..00000000 --- a/src/misc/parseReact.mli +++ /dev/null @@ -1,113 +0,0 @@ - -(* -copyright (c) 2013-2014, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Parser combinators driven by the input} *) - -type ('input, 'result) t -(** parser that takes some type as input and outputs a value of type 'result -when it's done *) - -(** {6 Basic Building Blocs} *) - -val stop : ('a, unit) t -(** Succeed exactly at the end of input *) - -val return : 'b -> ('a, 'b) t -(** Return a value *) - -val return' : (unit -> 'b) -> ('a, 'b) t -(** Suspended version of {!return}, does not evaluate yet *) - -val delay : (unit -> ('a, 'b) t) -> ('a, 'b) t -(** Delay evaluation of the parser *) - -val fail : ('a, 'b) t -(** Failure *) - -val one : ('a, 'a) t -(** Parse one value exactly *) - -val skip : ('a, unit) t -(** Ignore the next value *) - -val exact : ?eq:('a -> 'a -> bool) -> 'a -> ('a, unit) t -(** Accept one value as input exactly *) - -val guard : ('b -> bool) -> ('a, 'b) t -> ('a, 'b) t -(** Ensure the return value of the given parser satisfies the predicate. - [guard f p] will be the same as [p] if [p] returns - some [x] with [f x = true]. If [not (f x)], then [guard f p] fails. *) - -val bind : ('b -> ('a, 'c) t) -> ('a, 'b) t -> ('a, 'c) t - -val (>>=) : ('a, 'b) t -> ('b -> ('a, 'c) t) -> ('a, 'c) t - -val (>>) : ('a, 'b) t -> ('a, 'c) t -> ('a, 'c) t -(** Wait for the first parser to succeed, then switch to the second one *) - -val map : ('b -> 'c) -> ('a, 'b) t -> ('a, 'c) t -(** Map outputs *) - -val (>>|) : ('a, 'b) t -> ('b -> 'c) -> ('a, 'c) t -(** Infix version of {!map} *) - -val (<|>) : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t -(** Non-deterministic choice. Both branches are evaluated in parallel *) - -val pair : ('a,'b) t -> ('a, 'c) t -> ('a, ('b * 'c)) t -val triple : ('a,'b) t -> ('a, 'c) t -> ('a, 'd) t -> ('a, ('b * 'c * 'd)) t - -val if_then_else : ('a -> bool) -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t -(** Test the next input, and choose the parser based on it. Does not consume - the input token for the test *) - -(** {6 Utils} *) - -val take_while : ('a -> bool) -> ('a, 'a list) t -(** Take input while it satisfies the given predicate *) - -val take_n : int -> ('a, 'a list) t -(** Take n input elements *) - -val skip_spaces : (char, unit) t -(** Skip whitespace (space,tab,newline) *) - -val ident : (char, string) t -(** Parse identifiers (stops on whitespaces) *) - -val many : sep:('a,_) t -> ('a, 'b) t -> ('a, 'b list) t -(** [many ~sep p] parses as many [p] as possible, separated by [sep]. *) - -val many1 : sep:('a,_) t -> ('a, 'b) t -> ('a, 'b list) t - -(** {6 Run} *) - -type 'a sequence = ('a -> unit) -> unit - -val run : ('a,'b) t -> 'a sequence -> 'b list -(** List of results. Each element of the list comes from a successful - series of choices [<|>]. If no choice operator was used, the list - contains 0 or 1 elements *) diff --git a/src/misc/persistentGraph.ml b/src/misc/persistentGraph.ml deleted file mode 100644 index fb42ea08..00000000 --- a/src/misc/persistentGraph.ml +++ /dev/null @@ -1,372 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 A simple polymorphic directed graph.} *) - -type 'a sequence = ('a -> unit) -> unit - -type ('v, 'e) t = ('v, ('v, 'e) node) PHashtbl.t - (** Graph parametrized by a type for vertices, and one for edges *) -and ('v, 'e) node = { - n_vertex : 'v; - mutable n_next : ('e * 'v) list; - mutable n_prev : ('e * 'v) list; -} (** A node of the graph *) - -(** Create an empty graph. The int argument specifies the initial size *) -let empty ?hash ?eq size = - PHashtbl.create ?hash ?eq size - -let mk_v_set ?(size=10) graph = - let open PHashtbl in - empty ~hash:graph.hash ~eq:graph.eq size - -let mk_v_table ?(size=10) graph = - let open PHashtbl in - create ~hash:graph.hash ~eq:graph.eq size - -let is_empty graph = - PHashtbl.length graph = 0 - -let length graph = - PHashtbl.length graph - -(** Create an empty node for this vertex *) -let empty_node v = { - n_vertex = v; - n_next = []; - n_prev = []; -} - -(** Copy of the graph *) -let copy graph = - PHashtbl.map - (fun v node -> - let node' = empty_node v in - node'.n_prev <- node.n_prev; - node'.n_next <- node.n_next; - node') - graph - -let get_node t v = - try PHashtbl.find t v - with Not_found -> - let n = empty_node v in - PHashtbl.replace t v n; - n - -let add t v1 e v2 = - let n1 = get_node t v1 - and n2 = get_node t v2 in - n1.n_next <- (e,v2) :: n1.n_next; - n2.n_prev <- (e,v1) :: n2.n_prev; - () - -let add_seq t seq = - seq (fun (v1,e,v2) -> add t v1 e v2) - -let next t v k = - List.iter k (PHashtbl.find t v).n_next - -let prev t v k = - List.iter k (PHashtbl.find t v).n_prev - -let seq_map f seq k = seq (fun x -> k (f x)) -let seq_filter p seq k = seq (fun x -> if p x then k x) - -let between t v1 v2 = - let edges k = List.iter k (PHashtbl.find t v1).n_next in - let edges = seq_filter (fun (e, v2') -> (PHashtbl.get_eq t) v2 v2') edges in - seq_map fst edges - -(** Call [k] on every vertex *) -let iter_vertices t k = - PHashtbl.iter (fun v _ -> k v) t - -let vertices t = iter_vertices t - -(** Call [k] on every edge *) -let iter t k = - PHashtbl.iter - (fun v1 node -> List.iter (fun (e, v2) -> k (v1, e, v2)) node.n_next) - t - -let to_seq t = iter t - -(** {2 Global operations} *) - -exception ExitIsEmpty -let seq_is_empty seq = - try seq (fun _ -> raise ExitIsEmpty); true - with ExitIsEmpty -> false - -(** Roots, ie vertices with no incoming edges *) -let roots g = - let vertices = vertices g in - seq_filter (fun v -> seq_is_empty (prev g v)) vertices - -(** Leaves, ie vertices with no outgoing edges *) -let leaves g = - let vertices = vertices g in - seq_filter (fun v -> seq_is_empty (next g v)) vertices - -exception ExitHead -let seq_head seq = - let r = ref None in - try - seq (fun x -> r := Some x; raise ExitHead); None - with ExitHead -> !r - -(** Pick a vertex, or raise Not_found *) -let choose g = - match seq_head (vertices g) with - | Some x -> x - | None -> raise Not_found - -let rev_edge (v,e,v') = (v',e,v) - -(** Reverse all edges in the graph, in place *) -let rev g = - PHashtbl.iter - (fun _ node -> (* reverse the incoming and outgoing edges *) - let next = node.n_next in - node.n_next <- node.n_prev; - node.n_prev <- next) - g - -(** {2 Traversals} *) - -(** Breadth-first search *) -let bfs graph first k = - let q = Queue.create () - and explored = mk_v_set graph in - Hashset.add explored first; - Queue.push first q; - while not (Queue.is_empty q) do - let v = Queue.pop q in - (* yield current node *) - k v; - (* explore children *) - next graph v - (fun (e, v') -> if not (Hashset.mem explored v') - then (Hashset.add explored v'; Queue.push v' q)) - done - -let bfs_seq graph first k = bfs graph first k - -(** DFS, with callbacks called on each encountered node and edge *) -let dfs_full graph ?(labels=mk_v_table graph) -?(enter=fun _ -> ()) ?(exit=fun _ -> ()) -?(tree_edge=fun _ -> ()) ?(fwd_edge=fun _ -> ()) ?(back_edge=fun _ -> ()) -first -= - (* next free number for traversal *) - let count = ref (-1) in - PHashtbl.iter (fun _ i -> count := max i !count) labels; - (* explore the vertex. trail is the reverse path from v to first *) - let rec explore trail v = - if PHashtbl.mem labels v then () else begin - (* first time we explore this node! give it an index, put it in trail *) - let n = (incr count; !count) in - PHashtbl.replace labels v n; - let trail' = (v, n) :: trail in - (* enter the node *) - enter trail'; - (* explore edges *) - next graph v - (fun (e, v') -> - try let n' = PHashtbl.find labels v' in - if n' < n && List.exists (fun (_,n'') -> n' = n'') trail' - then back_edge (v,e,v') (* back edge, cycle *) - else - fwd_edge (v,e,v') (* forward or cross edge *) - with Not_found -> - tree_edge (v,e,v'); (* tree edge *) - explore trail' v' (* explore the subnode *) - ); - (* exit the node *) - exit trail' - end - in - explore [] first - -(** Depth-first search, from given vertex. Each vertex is labelled - with its index in the traversal order. *) -let dfs graph first k = - (* callback upon entering node *) - let enter = function - | [] -> assert false - | (v,n)::_ -> k (v,n) - in - dfs_full graph ~enter first - -(** Is the graph acyclic? *) -let is_dag g = - if is_empty g then true - else try - let labels = mk_v_table g in - (* do a DFS from each root; any back edge indicates a cycle *) - vertices g - (fun v -> - dfs_full g ~labels ~back_edge:(fun _ -> raise Exit) v - ); - true (* complete traversal without back edge *) - with Exit -> - false (* back edge detected! *) - -(** {2 Path operations} *) - -type ('v, 'e) path = ('v * 'e * 'v) list - -(** Reverse the path *) -let rev_path p = - let rec rev acc p = match p with - | [] -> acc - | (v,e,v')::p' -> rev ((v',e,v)::acc) p' - in rev [] p - -exception ExitBfs - -(** Find the minimal path, from the given [vertex], that does not contain - any vertex satisfying [ignore], and that reaches a vertex - that satisfies [goal]. It raises Not_found if no reachable node - satisfies [goal]. *) -let min_path_full (type v) (type e) graph -?(cost=fun _ _ _ -> 1) ?(ignore=fun _ -> false) ~goal v = - (* priority queue *) - let cmp (_,i,_) (_,j,_) = i - j in - let q = Heap.empty ~cmp in - let explored = mk_v_set graph in - Heap.insert q (v, 0, []); - let best_path = ref (v,0,[]) in - try - while not (Heap.is_empty q) do - let (v, cost_v, path) = Heap.pop q in - if Hashset.mem explored v then () (* a shorter path is known *) - else if ignore v then () (* ignore the node. *) - else if goal v path (* shortest path to goal node! *) - then (best_path := v, cost_v, path; raise ExitBfs) - else begin - Hashset.add explored v; - (* explore successors *) - next graph v - (fun (e, v') -> - if Hashset.mem explored v' || ignore v' then () - else - let cost_v' = (cost v e v') + cost_v in - let path' = (v',e,v) :: path in - Heap.insert q (v', cost_v', path')) - end - done; - (* if a satisfying path was found, Exit would have been raised *) - raise Not_found - with ExitBfs -> (* found shortest satisfying path *) - !best_path - -(** Minimal path from first vertex to second, given the cost function *) -let min_path graph ~cost v1 v2 = - let cost _ e _ = cost e in - let goal v' _ = (PHashtbl.get_eq graph) v' v2 in - let _,_,path = min_path_full graph ~cost ~goal v1 in - path - -(** Maximal distance between the given vertex, and any other vertex - in the graph that is reachable from it. *) -let diameter graph v = - let diameter = ref 0 in - (* no path is a goal, but we can use its length to update diameter *) - let goal _ path = - diameter := max !diameter (List.length path); - false - in - try ignore (min_path_full graph ~goal v); assert false - with Not_found -> - !diameter (* explored every shortest path *) - -(** {2 Print to DOT} *) - -type attribute = [ -| `Color of string -| `Shape of string -| `Weight of int -| `Style of string -| `Label of string -| `Other of string * string -] (** Dot attribute *) - -(** Pretty print the graph in DOT, on given formatter. Using a sequence - allows to easily select which edges are important, - or to combine several graphs with [seq_append]. *) -let pp ~name ?vertices -~(print_edge : 'v -> 'e -> 'v -> attribute list) -~(print_vertex : 'v -> attribute list) formatter (graph : ('v, 'e) t) = - (* map vertex -> unique int *) - let vertices = match vertices with - | Some v -> v - | None -> mk_v_table graph in - (* map from vertices to integers *) - let get_id = - let count = ref 0 in - fun vertex -> - try PHashtbl.find vertices vertex - with Not_found -> - let n = !count in - incr count; - PHashtbl.replace vertices vertex n; - n - (* print an attribute *) - and print_attribute formatter attr = - match attr with - | `Color c -> Format.fprintf formatter "color=%s" c - | `Shape s -> Format.fprintf formatter "shape=%s" s - | `Weight w -> Format.fprintf formatter "weight=%d" w - | `Style s -> Format.fprintf formatter "style=%s" s - | `Label l -> Format.fprintf formatter "label=\"%s\"" l - | `Other (name, value) -> Format.fprintf formatter "%s=\"%s\"" name value - in - (* the unique name of a vertex *) - let pp_vertex formatter v = - Format.fprintf formatter "vertex_%d" (get_id v) in - (* print preamble *) - Format.fprintf formatter "@[digraph %s {@;" name; - (* print edges *) - to_seq graph - (fun (v1, e, v2) -> - let attributes = print_edge v1 e v2 in - Format.fprintf formatter " @[%a -> %a [%a];@]@." - pp_vertex v1 pp_vertex v2 - (CCList.print ~sep:"," print_attribute) - attributes - ); - (* print vertices *) - PHashtbl.iter - (fun v _ -> - let attributes = print_vertex v in - Format.fprintf formatter " @[%a [%a];@]@." pp_vertex v - (CCList.print ~sep:"," print_attribute) attributes) - vertices; - (* close *) - Format.fprintf formatter "}@]@;"; - () diff --git a/src/misc/persistentGraph.mli b/src/misc/persistentGraph.mli deleted file mode 100644 index 8ec044cc..00000000 --- a/src/misc/persistentGraph.mli +++ /dev/null @@ -1,161 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 A simple polymorphic directed graph.} *) - -type 'a sequence = ('a -> unit) -> unit - -(** {2 Basics} *) - -type ('v, 'e) t - (** Graph parametrized by a type for vertices, and a type for edges *) - -val empty : ?hash:('v -> int) -> ?eq:('v -> 'v -> bool) -> int -> ('v, 'e) t - (** Create an empty graph. The int argument specifies the initial size *) - -val mk_v_set : ?size:int -> ('v, _) t -> 'v Hashset.t - (** Create an empty set of vertices *) - -val mk_v_table : ?size:int -> ('v, _) t -> ('v, 'a) PHashtbl.t - (** Create an empty hashtable of vertices *) - -val copy : ('v, 'e) t -> ('v, 'e) t - (** Copy the graph *) - -val is_empty : (_, _) t -> bool - (** Is the graph empty? *) - -val length : (_, _) t -> int - (** Number of vertices *) - -val add : ('v,'e) t -> 'v -> 'e -> 'v -> unit - (** Add an edge between two vertices *) - -val add_seq : ('v,'e) t -> ('v * 'e * 'v) sequence -> unit - (** Add the vertices to the graph *) - -val next : ('v, 'e) t -> 'v -> ('e * 'v) sequence - (** Outgoing edges *) - -val prev : ('v, 'e) t -> 'v -> ('e * 'v) sequence - (** Incoming edges *) - -val between : ('v, 'e) t -> 'v -> 'v -> 'e sequence - -val iter_vertices : ('v, 'e) t -> ('v -> unit) -> unit -val vertices : ('v, 'e) t -> 'v sequence - (** Iterate on vertices *) - -val iter : ('v, 'e) t -> ('v * 'e * 'v -> unit) -> unit -val to_seq : ('v, 'e) t -> ('v * 'e * 'v) sequence - (** Dump the graph as a sequence of vertices *) - -(** {2 Global operations} *) - -val roots : ('v, 'e) t -> 'v sequence - (** Roots, ie vertices with no incoming edges *) - -val leaves : ('v, 'e) t -> 'v sequence - (** Leaves, ie vertices with no outgoing edges *) - -val choose : ('v, 'e) t -> 'v - (** Pick a 'v, or raise Not_found *) - -val rev_edge : ('v * 'e * 'v) -> ('v * 'e * 'v) - (** Reverse one edge *) - -val rev : ('v, 'e) t -> unit - (** Reverse all edges in the graph, in place *) - -(** {2 Traversals} *) - -val bfs : ('v, 'e) t -> 'v -> ('v -> unit) -> unit - (** Breadth-first search, from given 'v *) - -val bfs_seq : ('v, 'e) t -> 'v -> 'v sequence - (** Sequence of vertices traversed during breadth-first search *) - -val dfs_full : ('v, 'e) t -> - ?labels:('v, int) PHashtbl.t -> - ?enter:(('v * int) list -> unit) -> - ?exit:(('v * int) list -> unit) -> - ?tree_edge:(('v * 'e * 'v) -> unit) -> - ?fwd_edge:(('v * 'e * 'v) -> unit) -> - ?back_edge:(('v * 'e * 'v) -> unit) -> - 'v -> - unit - (** DFS, with callbacks called on each encountered node and edge *) - -val dfs : ('v, 'e) t -> 'v -> (('v * int) -> unit) -> unit - (** Depth-first search, from given 'v. Each 'v is labelled - with its index in the traversal order. *) - -val is_dag : ('v, 'e) t -> bool - (** Is the graph acyclic? *) - -(** {2 Path operations} *) - -type ('v, 'e) path = ('v * 'e * 'v) list - (** A path is a list of edges connected by vertices. *) - -val rev_path : ('v, 'e) path -> ('v, 'e) path - (** Reverse the path *) - -val min_path_full : ('v, 'e) t -> - ?cost:('v -> 'e -> 'v -> int) -> - ?ignore:('v -> bool) -> - goal:('v -> ('v, 'e) path -> bool) -> - 'v -> - 'v * int * ('v, 'e) path - (** Find the minimal path, from the given ['v], that does not contain - any 'v satisfying [ignore], and that reaches a 'v - that satisfies [goal]. It raises Not_found if no reachable node - satisfies [goal]. The path is reversed. *) - -val min_path : ('v, 'e) t -> cost:('e -> int) -> 'v -> 'v -> ('v,'e) path - (** Minimal path from first 'v to second, given the cost function, - or raises Not_found. The path is reversed. *) - -val diameter : ('v, 'e) t -> 'v -> int - (** Maximal distance between the given 'v, and any other 'v - in the graph that is reachable from it. *) - -(** {2 Print to DOT} *) - -type attribute = [ -| `Color of string -| `Shape of string -| `Weight of int -| `Style of string -| `Label of string -| `Other of string * string -] (** Dot attribute *) - -val pp : name:string -> ?vertices:('v,int) PHashtbl.t -> - print_edge:('v -> 'e -> 'v -> attribute list) -> - print_vertex:('v -> attribute list) -> - Format.formatter -> - ('v, 'e) t -> unit - (** Pretty print the graph in DOT, on given formatter. *) diff --git a/src/misc/piCalculus.ml b/src/misc/piCalculus.ml deleted file mode 100644 index 62e70b1b..00000000 --- a/src/misc/piCalculus.ml +++ /dev/null @@ -1,287 +0,0 @@ -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -this software is provided by the copyright holders and contributors "as is" and -any express or implied warranties, including, but not limited to, the implied -warranties of merchantability and fitness for a particular purpose are -disclaimed. in no event shall the copyright holder or contributors be liable -for any direct, indirect, incidental, special, exemplary, or consequential -damages (including, but not limited to, procurement of substitute goods or -services; loss of use, data, or profits; or business interruption) however -caused and on any theory of liability, whether in contract, strict liability, -or tort (including negligence or otherwise) arising in any way out of the use -of this software, even if advised of the possibility of such damage. -*) - -(** {1 Pi-calculus model of concurrency} *) - -module DList = struct - type 'a t = { - value : 'a wrapper; - mutable prev : 'a t; - mutable next : 'a t; - } - and 'a wrapper = - | First (* first element of the list *) - | Element of 'a - - (** New empty list *) - let create () = - let rec node = { - value = First; - prev = node; - next = node; - } in - node - - let is_empty l = - let ans = l.prev == l in - (if ans then (assert (l.next == l && l.value == First))); - ans - - (** Add element at the end *) - let append l x = - let node = { - value = Element x; - prev = l.prev; - next = l; - } in - l.prev.next <- node; - l.prev <- node; - node - - (** Add element at the beginning *) - let prepend l x = - let node = { - value = Element x; - prev = l; - next = l.next; - } in - l.next.prev <- node; - l.next <- node; - node - - (* remove the given element *) - let remove x = - assert (not (x.prev == x || x.next == x)); - x.prev.next <- x.next; - x.next.prev <- x.prev; - () - - (** Pop the first element *) - let pop l = - match l.next.value with - | First -> failwith "DList.pop: empty list" - | Element x -> - remove l.next; - x - - let rec remove_list l = match l with - | [] -> () - | x::l' -> remove x; remove_list l' - - (** Iterate on all elements *) - let iter l f = - let rec iter l = match l.value with - | First -> () - | Element x -> - f x; - iter l.next - in - iter l.next -end - -type 'a chan = { - receivers : 'a transition_node DList.t; - senders : 'a transition_node DList.t; -} (** Channel conveying values of type 'a. Invariant: receivers = None || senders = None *) -and 'a transition_node = { - tn_transition : 'a __transition; - mutable tn_hook : unit -> unit; (* hook to call after transition *) - tn_to_replicate : to_replicate ref; (* do we have to replicate a process *) -} (** List of transitions for a channel *) -and to_replicate = - | ReplicateNothing - | ReplicateThis of process - (** Do we have to replicate a process? *) -and process = - | Parallel : process list -> process (** Spawn several processes *) - | Sum : transition list -> process (** Choice point *) - | Replicate : process -> process (** Replication of a process *) - | New : ('a chan -> process) -> process (** New local name *) - | Escape : (unit -> process) -> process (** Run a user function *) - | Stop : process (** Stop this process *) - (** A process of the Pi-calculus *) -and _ __transition = - | Receive : 'a chan * ('a -> process) -> 'a __transition - | Send : 'a chan * 'a * process -> 'a __transition - (** Transition: send or receive a message *) -and transition = - | Transition : 'a __transition -> transition - -let parallel l = (assert (l <> []); Parallel l) -let sum l = (assert (l <> []); Sum l) -let replicate p = Replicate p -let new_ f = New f -let escape f = Escape f -let stop = Stop - -let send ch x p = Transition (Send (ch, x, p)) -let receive ch f = Transition (Receive (ch, f)) - -let send_one ch x p = sum [send ch x p] -let receive_one ch f = sum [receive ch f] - -let (>>) f p = - escape (fun () -> f (); p) - -let (|||) a b = parallel [a; b] - -let (++) a b = sum [a; b] - -(** New channel (name) *) -let mk_chan () = - let ch = { - receivers = DList.create (); - senders = DList.create (); - } in - ch - -type run_env = { - tasks : (process * to_replicate ref) Queue.t; -} (** Environment for running processes *) - -let mk_env () = - { tasks = Queue.create (); } - -(** Push the process in the queue of processes to eval *) -let push_process ~env p to_restart = - Queue.push (p, to_restart) env.tasks - -(** Check whether there is a process to replicate now *) -let check_replicate ~env to_replicate = - match !to_replicate with - | ReplicateNothing -> () - | ReplicateThis p' -> - (* replicate p' now; it will be useless from now on to replicate it again *) - push_process ~env p' (ref ReplicateNothing); - to_replicate := ReplicateNothing - -(** Make a new transition node (linked to nothing) *) -let mk_transition_node transition to_replicate = - let node = { - tn_transition = transition; - tn_hook = (fun () -> ()); - tn_to_replicate = to_replicate; - } in - node - -(** Perform the given transition (one send, one receive). *) -let perform_transition -: type a. env:run_env -> a transition_node -> a transition_node -> unit = -fun ~env sender receiver -> - (* cleanup alternatives, replicate some processes if needed *) - sender.tn_hook (); - receiver.tn_hook (); - check_replicate ~env sender.tn_to_replicate; - check_replicate ~env receiver.tn_to_replicate; - match sender.tn_transition, receiver.tn_transition with - | Send (ch, x, send_p), Receive (ch', receive_p) -> - assert (ch == ch'); - (* receiving channel gets the sent value *) - let receive_p = receive_p x in - (* push the two new processes (with no process to replicate) *) - push_process ~env send_p (ref ReplicateNothing); - push_process ~env receive_p (ref ReplicateNothing); - () - | _ -> assert false - -(** Check whether any transition in the list can be performed; otherwise, - register all of them to their respective channels; Returns the - list of corresponding [transition_node] (empty if some - transition fired immediately). *) -let try_transitions ~env transitions to_replicate = - try - let set_hooks, hook = List.fold_left - (fun (set_hooks, hook) transition -> match transition with - | Transition (Receive (ch, _) as transition) -> - let receiver = mk_transition_node transition to_replicate in - if DList.is_empty ch.senders - then (* wait *) - let dlist = DList.append ch.receivers receiver in - (fun hook -> receiver.tn_hook <- hook) :: set_hooks, - (fun () -> DList.remove dlist; hook ()) - else begin (* fire *) - let sender = DList.pop ch.senders in - perform_transition ~env sender receiver; - hook (); (* cancel previous sum cases *) - raise Exit - end - | Transition (Send (ch, _, _) as transition) -> - let sender = mk_transition_node transition to_replicate in - if DList.is_empty ch.receivers - then (* wait *) - let dlist = DList.append ch.senders sender in - (fun hook -> sender.tn_hook <- hook) :: set_hooks, - (fun () -> DList.remove dlist; hook ()) - else begin (* fire *) - let receiver = DList.pop ch.receivers in - perform_transition ~env sender receiver; - hook (); (* cancel previous sum cases *) - raise Exit - end) - ([], fun () -> ()) transitions - in - (* we have a list of transition nodes; save it for when a transition fires *) - List.iter (fun set_hook -> set_hook hook) set_hooks - with Exit -> (* some transition fired immediately *) - () - -(** Run the simulation until all processes are stuck, or stopped. *) -let run p = - (* run tasks one by one until none remains *) - let rec run : env:run_env -> unit = fun ~env -> - if not (Queue.is_empty env.tasks) then begin - (* eval next process *) - let p, to_replicate = Queue.pop env.tasks in - eval_process ~env p to_replicate; - run ~env - end - (* evaluate this process *) - and eval_process : env:run_env -> process -> to_replicate ref -> unit - = fun ~env p to_replicate -> - match p with - | Stop -> (* stop, but maybe there is a process to replicate *) - check_replicate ~env to_replicate - | New f -> - (* apply [f] to a new chan *) - let c = mk_chan () in - let p' = f c in - eval_process ~env p' to_replicate - | Parallel l -> - (* evaluate each process *) - List.iter (fun p -> push_process ~env p to_replicate) l - | Replicate p' -> - (* run [p'] within an env where [p] is to be replicated *) - let to_replicate' = ref (ReplicateThis p) in - eval_process ~env p' to_replicate' - | Escape f -> - let p' = f () in - push_process ~env p' to_replicate (* yield before processing the result *) - | Sum transitions -> - try_transitions ~env transitions to_replicate - in - (* initial env *) - let env = mk_env () in - push_process ~env p (ref ReplicateNothing); - run ~env diff --git a/src/misc/piCalculus.mli b/src/misc/piCalculus.mli deleted file mode 100644 index dc14c9d7..00000000 --- a/src/misc/piCalculus.mli +++ /dev/null @@ -1,74 +0,0 @@ -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -this software is provided by the copyright holders and contributors "as is" and -any express or implied warranties, including, but not limited to, the implied -warranties of merchantability and fitness for a particular purpose are -disclaimed. in no event shall the copyright holder or contributors be liable -for any direct, indirect, incidental, special, exemplary, or consequential -damages (including, but not limited to, procurement of substitute goods or -services; loss of use, data, or profits; or business interruption) however -caused and on any theory of liability, whether in contract, strict liability, -or tort (including negligence or otherwise) arising in any way out of the use -of this software, even if advised of the possibility of such damage. -*) - -(** {1 Pi-calculus model of concurrency} *) - -type 'a chan - (** Channel conveying values of type 'a *) - -type process = private - | Parallel : process list -> process (** Spawn several processes *) - | Sum : transition list -> process (** Choice point *) - | Replicate : process -> process (** Replication of a process *) - | New : ('a chan -> process) -> process (** New local name *) - | Escape : (unit -> process) -> process (** Run a user function *) - | Stop : process (** Stop this process *) -and 'a __transition = - | Receive : 'a chan * ('a -> process) -> 'a __transition - | Send : 'a chan * 'a * process -> 'a __transition -and transition = - | Transition : 'a __transition -> transition - -val parallel : process list -> process -val sum : transition list -> process -val replicate : process -> process -val new_ : ('a chan -> process) -> process -val escape : (unit -> process) -> process -val stop : process - -val send : 'a chan -> 'a -> process -> transition -val receive : 'a chan -> ('a -> process) -> transition - -(** Be careful: there must be at least one send/receive between a replicate - and a stop, otherwise {! run} will get stuck in a loop, replicating the - process forever. *) - -val send_one : 'a chan -> 'a -> process -> process - (** Send a value, with no alternative *) - -val receive_one : 'a chan -> ('a -> process) -> process - (** Receive a value, with no alternative *) - -val (>>) : (unit -> unit) -> process -> process - (** Perform the action, then proceed to the following process *) - -val (|||) : process -> process -> process - (** Infix version of {! parallel} for two processes *) - -val (++) : transition -> transition -> process - (** Infix version of {! sum} for two processes *) - -val run : process -> unit - (** Run the simulation until all processes are stuck, or stopped. *) diff --git a/src/misc/skipList.ml b/src/misc/skipList.ml deleted file mode 100644 index c9af6a63..00000000 --- a/src/misc/skipList.ml +++ /dev/null @@ -1,198 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Imperative skip-list} *) - -type 'a gen = unit -> 'a option - -(** Most functions are inspired from - "A skip list cookbook", William Pugh, 1989. *) - -type ('a, 'b) t = { - mutable data : ('a, 'b) bucket; - cmp : ('a -> 'a -> int); (* comparison function *) - mutable size : int; -} (** A skip list that maps elements of type 'a to elements of type 'b *) -and ('a, 'b) bucket = - | Init of int * ('a, 'b) bucket array (* level + first array *) - | Node of 'a * 'b ref * ('a, 'b) bucket array - | Nil - -(* give a random level between 0 and [maxLevel] *) -let random_level maxLevel = - let rec iter level = - if level = maxLevel then level - else if Random.bool () then iter (level+1) - else level - in iter 1 - -let create ?(maxLevel=4) cmp = - { data = Init (1, Array.make maxLevel Nil); - cmp; - size = 0; - } - -(* level of the list node *) -let level node = match node with - | Init (n, _) -> n - | Node (_, _, a) -> Array.length a - | _ -> assert false - -(* check whether the element is lower than k *) -let lower ~cmp node k = match node with - | Init _ -> assert false - | Node (k', _, _) -> cmp k' k < 0 - | Nil -> false - -let eq ~cmp node k = match node with - | Init _ -> assert false - | Node (k', _, _) -> cmp k' k = 0 - | Nil -> false - -(** Is the list empty? *) -let is_empty l = - l.size = 0 - -let maxLevel l = - match l.data with - | Init (_, a) -> Array.length a - | _ -> assert false - -let array_of node = - match node with - | Init (_, a) | Node (_, _, a) -> a - | Nil -> assert false - -let clear l = - l.size <- 0; - let a = array_of l.data in - Array.fill a 0 (Array.length a) Nil; - l.data <- Init (1, a) - -(* next element of node, at level [n] *) -let next node n = - (array_of node).(n) - -(** Find given key in the list, or Not_found *) -let find l k = - let cmp = l.cmp in - let rec search x n = - if n < 0 then peek_last x - else - let x' = next x n in - match x' with - | Nil -> search x (n-1) - | Node (k', v, _) -> - let c = cmp k' k in - if c = 0 then !v - else if c < 0 then search x' n - else search x (n-1) - | Init _ -> assert false - and peek_last x = - match next x 0 with - | Node (k', v, _) when cmp k k' = 0 -> !v - | _ -> raise Not_found - in - search l.data (level l.data - 1) - -let mem l k = - try ignore (find l k); true - with Not_found -> false - -(** Add [k -> v] to the list [l] *) -let add l k v = - let cmp = l.cmp in - let x = ref l.data in - let update = Array.make (maxLevel l) (array_of l.data) in - (* find which pointers to update *) - for i = level l.data - 1 downto 0 do - while lower ~cmp (next !x i) k do x := next !x i done; - update.(i) <- array_of !x; - done; - x := next !x 0; - match !x with - | Node (k', v', _) when cmp k k' = 0 -> - v' := v (* replace mapping of [k] *) - | _ -> - let new_level = random_level (maxLevel l) in - l.size <- l.size + 1; - (* update level of the list *) - (if new_level > level l.data then - begin - for i = level l.data to new_level - 1 do - update.(i) <- array_of l.data - done; - l.data <- Init (new_level, array_of l.data) - end); - (* create node and insert it *) - let a = Array.make new_level Nil in - x := Node (k, ref v, a); - for i = 0 to new_level - 1 do - a.(i) <- update.(i).(i); - update.(i).(i) <- !x - done - -(** Removal of the given key *) -let remove l k = - let cmp = l.cmp in - let x = ref l.data in - let update = Array.make (maxLevel l) (array_of l.data) in - (* find which pointers to update *) - for i = level l.data - 1 downto 0 do - while lower ~cmp (next !x i) k do x := next !x i done; - update.(i) <- array_of !x; - done; - x := next !x 0; - if eq ~cmp !x k then begin - (* found the node containing [k] *) - for i = 0 to level l.data - 1 do - if update.(i).(i) == !x then update.(i).(i) <- next !x i - done; - (* update level of list *) - l.size <- l.size - 1; - while level l.data > 1 && next l.data (level l.data - 1) = Nil - do l.data <- Init (level l.data - 1, array_of l.data) done - end - -let length l = l.size - -(** Iterator on the skip list *) -let gen l = - let x = ref (next l.data 0) in - fun () -> - match !x with - | Nil -> None - | Init _ -> assert false - | Node (k, v, a) -> - x := a.(0); - Some (k, !v) - -let rec gen_iter f g = match g() with - | None -> () - | Some x -> f x; gen_iter f g - -(** Add content of the iterator to the list *) -let of_gen l gen = - gen_iter (fun (k,v) -> add l k v) gen diff --git a/src/misc/skipList.mli b/src/misc/skipList.mli deleted file mode 100644 index d701e4b9..00000000 --- a/src/misc/skipList.mli +++ /dev/null @@ -1,60 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Imperative skip-list} *) - -type 'a gen = unit -> 'a option - -type ('a, 'b) t - (** A skip list that maps elements of type 'a to elements of type 'b *) - -val create : ?maxLevel:int -> ('a -> 'a -> int) -> ('a, 'b) t - (** Create an empty list (comparison function required). The optional - argument indicates how many layer the skiplist has. *) - -val clear : (_, _) t -> unit - (** Clear content *) - -val is_empty : (_, _) t -> bool - (** Are there any bindings in the list? *) - -val find : ('a, 'b) t -> 'a -> 'b - (** Find mapping for 'a *) - -val mem : ('a, _) t -> 'a -> bool - (** Does the key have a binding in the list? *) - -val add : ('a, 'b) t -> 'a -> 'b -> unit - (** Add the mapping *) - -val remove : ('a, 'b) t -> 'a -> unit - (** Remove binding of the key *) - -val length : (_, _) t -> int - (** Number of elements *) - -val gen : ('a, 'b) t -> ('a * 'b) gen - -val of_gen : ('a, 'b) t -> ('a * 'b) gen -> unit diff --git a/src/misc/splayMap.ml b/src/misc/splayMap.ml deleted file mode 100644 index 4a9de67d..00000000 --- a/src/misc/splayMap.ml +++ /dev/null @@ -1,416 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Maps} *) - -(* We use splay trees, following -http://www.cs.cornell.edu/Courses/cs3110/2009fa/recitations/rec-splay.html -*) - -type 'a sequence = ('a -> unit) -> unit - -(** {2 Polymorphic Maps} *) - -type ('a, 'b) t = { - cmp : 'a -> 'a -> int; - mutable tree : ('a, 'b) tree; (* for lookups *) -} (** Tree with keys of type 'a, and values of type 'b *) -and ('a, 'b) tree = - | Empty - | Node of ('a * 'b * ('a, 'b) tree * ('a, 'b) tree) - -let empty_with ~cmp = - { cmp; - tree = Empty; - } - -let empty () = - { cmp = Pervasives.compare; - tree = Empty; - } - -let is_empty t = - match t.tree with - | Empty -> true - | Node _ -> false - -(** Pivot the tree so that the node that has key [key], or close to [key], is - the root node. *) -let rec splay ~cmp (k, v, l, r) key = - let c = cmp key k in - if c = 0 - then (k, v, l, r) (* found *) - else if c < 0 - then match l with - | Empty -> (k, v, l, r) (* not found *) - | Node (lk, lv, ll, lr) -> - let lc = cmp key lk in - if lc = 0 - then (lk, lv, ll, Node (k, v, lr, r)) (* zig *) - else if lc < 0 - then match ll with - | Empty -> (lk, lv, Empty, Node (k, v, lr, r)) (* not found *) - | Node n -> (* zig zig *) - let (llk, llv, lll, llr) = splay ~cmp n key in - (llk, llv, lll, Node (lk, lv, llr, Node (k, v, lr, r))) - else - match lr with - | Empty -> (lk, lv, ll, Node (k, v, Empty, r)) - | Node n -> (* zig zag *) - let (lrk, lrv, lrl, lrr) = splay ~cmp n key in - (lrk, lrv, Node (lk, lv, ll, lrl), Node (k, v, lrr, r)) - else match r with - | Empty -> (k, v, l, r) (* not found *) - | Node (rk, rv, rl, rr) -> - let rc = cmp key rk in - if rc = 0 - then (rk, rv, Node (k, v, l, rl), rr) (* zag *) - else if rc > 0 - then match rr with - | Empty -> (rk, rv, Node (k, v, l, rl), Empty) (* not found *) - | Node n -> (* zag zag *) - let (rrk, rrv, rrl, rrr) = splay ~cmp n key in - (rrk, rrv, Node (rk, rv, Node (k, v, l, rl), rrl), rrr) - else match rl with - | Empty -> (rk, rv, Node (k, v, l, Empty), rr) (* zag zig *) - | Node n -> (* zag zig *) - let (rlk, rlv, rll, rlr) = splay ~cmp n key in - (rlk, rlv, Node (k, v, l, rll), Node (rk, rv, rlr, rr)) - -let find t key = - match t.tree with - | Empty -> raise Not_found - | Node (k, v, l, r) -> - let (k, v, l, r) = splay ~cmp:t.cmp (k, v, l, r) key in - t.tree <- Node (k, v, l, r); (* save balanced tree *) - if t.cmp key k = 0 - then v - else raise Not_found - -let mem t key = - match t.tree with - | Empty -> false - | Node (k, v, l, r) -> - let (k, v, l, r) = splay ~cmp:t.cmp (k, v, l, r) key in - t.tree <- Node (k, v, l, r); (* save balanced tree *) - if t.cmp key k = 0 - then true - else false - -(** Recursive insertion of key->value in the tree *) -let rec insert ~cmp tree key value = - match tree with - | Empty -> Node (key, value, Empty, Empty) - | Node (k, v, l, r) -> - let c = cmp key k in - if c = 0 - then Node (key, value, l, r) (* replace *) - else if c < 0 - then Node (k, v, insert ~cmp l key value, r) - else Node (k, v, l, insert ~cmp r key value) - -let add t key value = - let tree = - match t.tree with - | Empty -> Node (key, value, Empty, Empty) - | Node (k, v, l, r) -> - let (k, v, l, r) = splay ~cmp:t.cmp (k, v, l, r) key in - let tree = Node (k, v, l, r) in - t.tree <- tree; (* save balanced tree *) - (* insertion in this tree *) - insert ~cmp:t.cmp tree key value - in - { t with tree; } - -let singleton ~cmp key value = - add (empty_with ~cmp) key value - -(** Merge of trees, where a < b *) -let rec left_merge a b = - match a, b with - | Empty, Empty -> Empty - | Node (k, v, l, r), b -> Node (k, v, l, left_merge r b) - | Empty, b -> b - -let remove t key = - match t.tree with - | Empty -> t - | Node (k, v, l, r) -> - let (k, v, l, r) = splay ~cmp:t.cmp (k, v, l, r) key in - t.tree <- Node (k, v, l, r); - if t.cmp key k = 0 - then (* remove the node, by merging the subnodes *) - let tree = left_merge l r in - { t with tree; } - else (* not present, same tree *) - t - -let iter t f = - let rec iter t = match t with - | Empty -> () - | Node (k, v, l, r) -> - iter l; - f k v; - iter r - in iter t.tree - -let fold t acc f = - let rec fold acc t = match t with - | Empty -> acc - | Node (k, v, l, r) -> - let acc = fold acc l in - let acc = f acc k v in - fold acc r - in - fold acc t.tree - -let size t = fold t 0 (fun acc _ _ -> acc+1) - -let choose t = - match t.tree with - | Empty -> raise Not_found - | Node (k, v, _, _) -> k, v - -let to_seq t = - fun kont -> iter t (fun k v -> kont (k, v)) - -let of_seq t seq = - let t = ref t in - seq (fun (k, v) -> t := add !t k v); - !t - -(** {2 Functorial interface} *) - -module type S = sig - type key - type 'a t - (** Tree with keys of type [key] and values of type 'a *) - - val empty : unit -> 'a t - (** Empty tree *) - - val is_empty : _ t -> bool - (** Is the tree empty? *) - - val find : 'a t -> key -> 'a - (** Find the element for this key, or raises Not_found *) - - val mem : _ t -> key -> bool - (** Is the key member of the tree? *) - - val add : 'a t -> key -> 'a -> 'a t - (** Add the binding to the tree *) - - val singleton : key -> 'a -> 'a t - (** Singleton map *) - - val remove : 'a t -> key -> 'a t - (** Remove the binding for this key *) - - val iter : 'a t -> (key -> 'a -> unit) -> unit - (** Iterate on bindings *) - - val fold : 'a t -> 'c -> ('c -> key -> 'a -> 'c) -> 'c - (** Fold on bindings *) - - val size : _ t -> int - (** Number of bindings (linear) *) - - val choose : 'a t -> (key * 'a) - (** Some binding, or raises Not_found *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : 'a t -> (key * 'a) sequence -> 'a t -end - -module type ORDERED = sig - type t - val compare : t -> t -> int -end - -module Make(X : ORDERED) = struct - - type key = X.t - type 'a t = { - mutable tree : 'a tree; (* for lookups *) - } (** Tree with keys of type key, and values of type 'a *) - and 'a tree = - | Empty - | Node of (key * 'a * 'a tree * 'a tree) - - let empty () = - { tree = Empty; } - - let is_empty t = - match t.tree with - | Empty -> true - | Node _ -> false - - (** Pivot the tree so that the node that has key [key], or close to [key], is - the root node. *) - let rec splay (k, v, l, r) key = - let c = X.compare key k in - if c = 0 - then (k, v, l, r) (* found *) - else if c < 0 - then match l with - | Empty -> (k, v, l, r) (* not found *) - | Node (lk, lv, ll, lr) -> - let lc = X.compare key lk in - if lc = 0 - then (lk, lv, ll, Node (k, v, lr, r)) (* zig *) - else if lc < 0 - then match ll with - | Empty -> (lk, lv, Empty, Node (k, v, lr, r)) (* not found *) - | Node n -> (* zig zig *) - let (llk, llv, lll, llr) = splay n key in - (llk, llv, lll, Node (lk, lv, llr, Node (k, v, lr, r))) - else - match lr with - | Empty -> (lk, lv, ll, Node (k, v, Empty, r)) - | Node n -> (* zig zag *) - let (lrk, lrv, lrl, lrr) = splay n key in - (lrk, lrv, Node (lk, lv, ll, lrl), Node (k, v, lrr, r)) - else match r with - | Empty -> (k, v, l, r) (* not found *) - | Node (rk, rv, rl, rr) -> - let rc = X.compare key rk in - if rc = 0 - then (rk, rv, Node (k, v, l, rl), rr) (* zag *) - else if rc > 0 - then match rr with - | Empty -> (rk, rv, Node (k, v, l, rl), Empty) (* not found *) - | Node n -> (* zag zag *) - let (rrk, rrv, rrl, rrr) = splay n key in - (rrk, rrv, Node (rk, rv, Node (k, v, l, rl), rrl), rrr) - else match rl with - | Empty -> (rk, rv, Node (k, v, l, Empty), rr) (* zag zig *) - | Node n -> (* zag zig *) - let (rlk, rlv, rll, rlr) = splay n key in - (rlk, rlv, Node (k, v, l, rll), Node (rk, rv, rlr, rr)) - - let find t key = - match t.tree with - | Empty -> raise Not_found - | Node (k, v, l, r) -> - let (k, v, l, r) = splay (k, v, l, r) key in - t.tree <- Node (k, v, l, r); (* save balanced tree *) - if X.compare key k = 0 - then v - else raise Not_found - - let mem t key = - match t.tree with - | Empty -> false - | Node (k, v, l, r) -> - let (k, v, l, r) = splay (k, v, l, r) key in - t.tree <- Node (k, v, l, r); (* save balanced tree *) - if X.compare key k = 0 - then true - else false - - (** Recursive insertion of key->value in the tree *) - let rec insert tree key value = - match tree with - | Empty -> Node (key, value, Empty, Empty) - | Node (k, v, l, r) -> - let c = X.compare key k in - if c = 0 - then Node (key, value, l, r) (* replace *) - else if c < 0 - then Node (k, v, insert l key value, r) - else Node (k, v, l, insert r key value) - - let add t key value = - let tree = - match t.tree with - | Empty -> Node (key, value, Empty, Empty) - | Node (k, v, l, r) -> - let (k, v, l, r) = splay (k, v, l, r) key in - let tree = Node (k, v, l, r) in - t.tree <- tree; (* save balanced tree *) - (* insertion in this tree *) - insert tree key value - in - { tree; } - - let singleton key value = - add (empty ()) key value - - (** Merge of trees, where a < b *) - let rec left_merge a b = - match a, b with - | Empty, Empty -> Empty - | Node (k, v, l, r), b -> Node (k, v, l, left_merge r b) - | Empty, b -> b - - let remove t key = - match t.tree with - | Empty -> t - | Node (k, v, l, r) -> - let (k, v, l, r) = splay (k, v, l, r) key in - t.tree <- Node (k, v, l, r); - if X.compare key k = 0 - then (* remove the node, by merging the subnodes *) - let tree = left_merge l r in - { tree; } - else (* not present, same tree *) - t - - let iter t f = - let rec iter t = match t with - | Empty -> () - | Node (k, v, l, r) -> - iter l; - f k v; - iter r - in iter t.tree - - let fold t acc f = - let rec fold acc t = match t with - | Empty -> acc - | Node (k, v, l, r) -> - let acc = fold acc l in - let acc = f acc k v in - fold acc r - in - fold acc t.tree - - let size t = fold t 0 (fun acc _ _ -> acc+1) - - let choose t = - match t.tree with - | Empty -> raise Not_found - | Node (k, v, _, _) -> k, v - - let to_seq t = - fun kont -> iter t (fun k v -> kont (k, v)) - - let of_seq t seq = - let t = ref t in - seq (fun (k, v) -> t := add !t k v); - !t -end diff --git a/src/misc/splayMap.mli b/src/misc/splayMap.mli deleted file mode 100644 index 6733f506..00000000 --- a/src/misc/splayMap.mli +++ /dev/null @@ -1,129 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Functional Maps} *) - -(* TODO: map-wide operations: merge, compare, equal, for_all, exists, - batch (sorted) add, partition, split, max_elt, min_elt, map... *) - -type 'a sequence = ('a -> unit) -> unit - - -(** {2 Polymorphic Maps} *) - -type ('a, 'b) t - (** Tree with keys of type 'a, and values of type 'b *) - -val empty_with : cmp:('a -> 'a -> int) -> ('a, 'b) t - (** Empty tree *) - -val empty : unit -> ('a, 'b) t - (** Empty tree using Pervasives.compare *) - -val is_empty : (_, _) t -> bool - (** Is the tree empty? *) - -val find : ('a, 'b) t -> 'a -> 'b - (** Find the element for this key, or raises Not_found *) - -val mem : ('a, _) t -> 'a -> bool - (** Is the key member of the tree? *) - -val add : ('a, 'b) t -> 'a -> 'b -> ('a, 'b) t - (** Add the binding to the tree *) - -val singleton : cmp:('a -> 'a -> int) -> 'a -> 'b -> ('a, 'b) t - (** Singleton map *) - -val remove : ('a, 'b) t -> 'a -> ('a, 'b) t - (** Remove the binding for this key *) - -val iter : ('a, 'b) t -> ('a -> 'b -> unit) -> unit - (** Iterate on bindings *) - -val fold : ('a, 'b) t -> 'c -> ('c -> 'a -> 'b -> 'c) -> 'c - (** Fold on bindings *) - -val size : (_, _) t -> int - (** Number of bindings (linear) *) - -val choose : ('a, 'b) t -> ('a * 'b) - (** Some binding, or raises Not_found *) - -val to_seq : ('a, 'b) t -> ('a * 'b) sequence - -val of_seq : ('a, 'b) t -> ('a * 'b) sequence -> ('a, 'b) t - -(** {2 Functorial interface} *) - -module type S = sig - type key - type 'a t - (** Tree with keys of type [key] and values of type 'a *) - - val empty : unit -> 'a t - (** Empty tree *) - - val is_empty : _ t -> bool - (** Is the tree empty? *) - - val find : 'a t -> key -> 'a - (** Find the element for this key, or raises Not_found *) - - val mem : _ t -> key -> bool - (** Is the key member of the tree? *) - - val add : 'a t -> key -> 'a -> 'a t - (** Add the binding to the tree *) - - val singleton : key -> 'a -> 'a t - (** Singleton map *) - - val remove : 'a t -> key -> 'a t - (** Remove the binding for this key *) - - val iter : 'a t -> (key -> 'a -> unit) -> unit - (** Iterate on bindings *) - - val fold : 'a t -> 'c -> ('c -> key -> 'a -> 'c) -> 'c - (** Fold on bindings *) - - val size : _ t -> int - (** Number of bindings (linear) *) - - val choose : 'a t -> (key * 'a) - (** Some binding, or raises Not_found *) - - val to_seq : 'a t -> (key * 'a) sequence - - val of_seq : 'a t -> (key * 'a) sequence -> 'a t -end - -module type ORDERED = sig - type t - val compare : t -> t -> int -end - -module Make(X : ORDERED) : S with type key = X.t diff --git a/src/misc/splayTree.ml b/src/misc/splayTree.ml deleted file mode 100644 index f520e56a..00000000 --- a/src/misc/splayTree.ml +++ /dev/null @@ -1,140 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Splay trees} *) - -(** See http://en.wikipedia.org/wiki/Splay_tree and - Okasaki's "purely functional data structures" p46 *) - -type ('a, 'b) t = (('a, 'b) tree * ('a -> 'a -> int)) - (** A splay tree with the given comparison function *) -and ('a, 'b) tree = - | Empty - | Node of (('a,'b) tree * 'a * 'b * ('a,'b) tree) - (** A splay tree containing values of type 'a *) - -let empty ~cmp = - (Empty, cmp) - -let is_empty (tree, _) = - match tree with - | Empty -> true - | Node _ -> false - -(** Partition the tree into (elements <= pivot, elements > pivot) *) -let rec partition ~cmp pivot tree = - match tree with - | Empty -> Empty, Empty - | Node (a, x, x_val, b) -> - if cmp x pivot <= 0 - then begin - match b with - | Empty -> (tree, Empty) - | Node (b1, y, y_val, b2) -> - if cmp y pivot <= 0 - then - let small, big = partition ~cmp pivot b2 in - Node (Node (a, x, x_val, b1), y, y_val, small), big - else - let small, big = partition ~cmp pivot b1 in - Node (a, x, x_val, small), Node (big, y, y_val, b2) - end else begin - match a with - | Empty -> (Empty, tree) - | Node (a1, y, y_val, a2) -> - if cmp y pivot <= 0 - then - let small, big = partition ~cmp pivot a2 in - Node (a1, y, y_val, small), Node (big, x, x_val, b) - else - let small, big = partition ~cmp pivot a1 in - small, Node (big, y, y_val, Node (a2, x, x_val, b)) - end - -(** Insert the pair (key -> value) in the tree *) -let insert (tree, cmp) k v = - let small, big = partition ~cmp k tree in - let tree' = Node (small, k, v, big) in - tree', cmp - -let remove (tree, cmp) k = failwith "not implemented" - -let replace (tree, cmp) k = failwith "not implemented" - -(** Returns the top value, or raise Not_found is empty *) -let top (tree, _) = - match tree with - | Empty -> raise Not_found - | Node (_, k, v, _) -> k, v - -(** Access minimum value *) -let min (tree, _) = - let rec min tree = - match tree with - | Empty -> raise Not_found - | Node (Empty, k, v, _) -> k, v - | Node (l, _, _, _) -> min l - in min tree - -(** Get minimum value and remove it from the tree *) -let delete_min (tree, cmp) = - let rec delete_min tree = match tree with - | Empty -> raise Not_found - | Node (Empty, x, x_val, b) -> x, x_val, b - | Node (Node (Empty, x, x_val, b), y, y_val, c) -> - x, x_val, Node (b, y, y_val, c) (* rebalance *) - | Node (Node (a, x, x_val, b), y, y_val, c) -> - let m, m_val, a' = delete_min a in - m, m_val, Node (a', x, x_val, Node (b, y, y_val, c)) - in - let m, m_val, tree' = delete_min tree in - m, m_val, (tree', cmp) - -(** Find the value for the given key (or raise Not_found). - It also returns the splayed tree *) -let find (tree, cmp) k = - failwith "not implemented" - -let find_fold (tree, cmp) k f acc = - acc (* TODO *) - -(** Iterate on elements *) -let iter (tree, _) f = - let rec iter tree = - match tree with - | Empty -> () - | Node (a, x, x_val, b) -> - iter a; - f x x_val; - iter b - in iter tree - -(** Number of elements (linear) *) -let size t = - let r = ref 0 in - iter t (fun _ _ -> incr r); - !r - -let get_cmp (_, cmp) = cmp diff --git a/src/misc/splayTree.mli b/src/misc/splayTree.mli deleted file mode 100644 index dab3b18e..00000000 --- a/src/misc/splayTree.mli +++ /dev/null @@ -1,73 +0,0 @@ -(* -Copyright (c) 2013, Simon Cruanes -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -Redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. Redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Splay trees} *) - -(** See http://en.wikipedia.org/wiki/Splay_tree and - Okasaki's "purely functional data structures" p46 *) - -type ('a, 'b) t - (** A functional splay tree *) - -val empty : cmp:('a -> 'a -> int) -> ('a, 'b) t - (** Empty splay tree using the given comparison function *) - -val is_empty : (_, _) t -> bool - (** Check whether the tree is empty *) - -val insert : ('a, 'b) t -> 'a -> 'b -> ('a, 'b) t - (** Insert the pair (key -> value) in the tree *) - -val remove : ('a, 'b) t -> 'a -> ('a, 'b) t - (** Remove an element by its key, returns the splayed tree *) - -val replace : ('a, 'b) t -> 'a -> 'b -> ('a, 'b) t - (** Insert the pair (key -> value) into the tree, replacing - the previous binding (if any). It replaces at most one - binding. *) - -val top : ('a, 'b) t -> 'a * 'b - (** Returns the top value, or raise Not_found is empty *) - -val min : ('a, 'b) t -> 'a * 'b - (** Access minimum value *) - -val delete_min : ('a, 'b) t -> 'a * 'b * ('a, 'b) t - (** Get minimum value and remove it from the tree *) - -val find : ('a, 'b) t -> 'a -> 'b * ('a, 'b) t - (** Find the value for the given key (or raise Not_found). - It also returns the splayed tree *) - -val find_fold : ('a, 'b) t -> 'a -> ('c -> 'b -> 'c) -> 'c -> 'c - (** Fold on all values associated with the given key *) - -val iter : ('a, 'b) t -> ('a -> 'b -> unit) -> unit - (** Iterate on elements *) - -val size : (_, _) t -> int - (** Number of elements (linear) *) - -val get_cmp : ('a, _) t -> ('a -> 'a -> int) diff --git a/src/misc/tTree.ml b/src/misc/tTree.ml deleted file mode 100644 index 034f91d9..00000000 --- a/src/misc/tTree.ml +++ /dev/null @@ -1,161 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 T-Trees} *) - -(** {2 Persistent array} - -The nodes of the tree are arrays, but to expose a persistent interface we -use persistent arrays. *) - -module PArray = struct - type 'a t = 'a zipper ref - and 'a zipper = - | Array of 'a array - | Diff of int * 'a * 'a zipper ref - - (* XXX maybe having a snapshot of the array from point to point may help? *) - - let make size elt = - let a = Array.make size elt in - ref (Array a) - - (** Recover the given version of the shared array. Returns the array - itself. *) - let rec reroot t = - match !t with - | Array a -> a - | Diff (i, v, t') -> - begin - let a = reroot t' in - let v' = a.(i) in - t' := Diff (i, v', t); - a.(i) <- v; - t := Array a; - a - end - - let get t i = - match !t with - | Array a -> a.(i) - | Diff _ -> - let a = reroot t in - a.(i) - - let set t i v = - let a = - match !t with - | Array a -> a - | Diff _ -> reroot t in - let v' = a.(i) in - if v == v' - then t (* no change *) - else begin - let t' = ref (Array a) in - a.(i) <- v; - t := Diff (i, v', t'); - t' (* create new array *) - end - - let fold_left f acc t = - let a = reroot t in - Array.fold_left f acc a - - let rec length t = - match !t with - | Array a -> Array.length a - | Diff (_, _, t') -> length t' -end - -(** {2 signature} *) - -module type S = sig - type key - - type 'a t - - val empty : 'a t - (** Empty tree *) - - val add : 'a t -> key -> 'a -> 'a t - (** Add a binding key/value. If the key already was bound to some - value, the old binding is erased. *) - - val remove : 'a t -> key -> 'a t - (** Remove the key *) - - val find : 'a t -> key -> 'a - (** Find the element associated with this key. - @raise Not_found if the key is not present *) - - val length : 'a t -> int - (** Number of bindings *) - - val fold : 'a t -> 'b -> ('b -> key -> 'a -> 'b) -> 'b - (** Fold on bindings *) -end - -(** {2 Functor} *) - -module Make(X : Set.OrderedType) = struct - type key = X.t - - (* bucket that maps a key to a value *) - type 'a bucket = - | B_none - | B_some of key * 'a - - (* recursive tree type *) - type 'a node = { - left : 'a node option; - right : 'a node option; - depth : int; - buckets : 'a bucket PArray.t; - } - - (* to avoid the value restriction, we need to make a special case for - the empty tree *) - type 'a t = - | E - | N of 'a node - - let empty = E - - let add tree k v = assert false - - let remove tree k = assert false - - let find tree k = - let rec find node k = assert false (* TODO *) - in - match tree with - | E -> raise Not_found - | N node -> find node k - - let length tree = assert false - - let fold tree acc f = assert false -end diff --git a/src/misc/tTree.mli b/src/misc/tTree.mli deleted file mode 100644 index 2357c5be..00000000 --- a/src/misc/tTree.mli +++ /dev/null @@ -1,65 +0,0 @@ - -(* -copyright (c) 2013, simon cruanes -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 T-Trees} - -Shallow, cache-friendly associative data structure. -See {{:http://en.wikipedia.org/wiki/T-tree} wikipedia}. - -Not thread-safe. -*) - -(** {2 signature} *) - -module type S = sig - type key - - type 'a t - - val empty : 'a t - (** Empty tree *) - - val add : 'a t -> key -> 'a -> 'a t - (** Add a binding key/value. If the key already was bound to some - value, the old binding is erased. *) - - val remove : 'a t -> key -> 'a t - (** Remove the key *) - - val find : 'a t -> key -> 'a - (** Find the element associated with this key. - @raise Not_found if the key is not present *) - - val length : 'a t -> int - (** Number of bindings *) - - val fold : 'a t -> 'b -> ('b -> key -> 'a -> 'b) -> 'b - (** Fold on bindings *) -end - -(** {2 Functor that builds T trees for comparable keys} *) - -module Make(X : Set.OrderedType) : S with type key = X.t diff --git a/src/misc/ty.ml b/src/misc/ty.ml deleted file mode 100644 index 66d097d9..00000000 --- a/src/misc/ty.ml +++ /dev/null @@ -1,175 +0,0 @@ - -(* -copyright (c) 2014, Simon Cruanes, Gabriel Scherer -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Dynamic Type Representation} *) - -type 'a ty = - | Int: int ty - | String: string ty - | List: 'a ty -> 'a list ty - | Pair: ('a ty * 'b ty) -> ('a * 'b) ty - | Record: ('builder, 'r) record * 'builder -> 'r ty - | Sum: 's sum_cps -> 's ty - | Fix : ('a ty -> 'a ty) -> 'a ty - -and (_, _) record = - | RecField : string * 'a ty * ('r -> 'a) * ('builder, 'r) record - -> ('a -> 'builder, 'r) record - | RecYield : ('r , 'r) record - -(* yeah, this is a bit hard to swallow: we need to quantify - universally over the return type of the pattern-matching, and then - existentially on the type of the partial matching function -*) -and 's sum_cps = { cases : 't . ('s, 't) sum_ex } -and ('s, 't) sum_ex = Match : ('matcher, 't, 's) sum * 'matcher -> ('s, 't) sum_ex - -and (_, _, _) sum = - | SumCase: string * 'a ty * ('a -> 's) * ('matcher, 't, 's) sum - -> (('a -> 't) -> 'matcher, 't, 's) sum - | SumYield : (('s -> 't), 't, 's) sum - -let record_fix f = - let rec r = lazy (Fix (fun _ -> - let descr, builder = f (Lazy.force r) in - Record (descr, builder))) - in Lazy.force r - -let sum_fix f = - let rec s = lazy (Fix (fun _ -> Sum (f (Lazy.force s)))) in - Lazy.force s - -(* TODO -let rec_field name ty get cont = - RecField (name, ty, get, cont) - -let rec_yield = RecYield - -let sum_case name ty matcher cont = - SumCase (name, ty, matcher, cont) - -let sum_yield = SumYield -*) - -(** {2 Some Functions} *) - -let rec identity : type a . a ty -> a -> a = function - | Int -> (fun n -> n+0) - | String -> (fun s -> s^"") - | List t -> List.map (identity t) - | Pair (ta, tb) -> (fun (a, b) -> identity ta a, identity tb b) - | Record (recty, builder) -> fun record -> - let rec fid : type b . b -> (b, a) record -> a = fun builder -> function - | RecYield -> builder - | RecField (_name, ty, read, rest) -> - let field = identity ty (read record) in - fid (builder field) rest - in fid builder recty - | Sum { cases = Match (sumty, matcher) } -> fun sum -> - let rec sid : type m . m -> (m, a, a) sum -> a = fun matcher -> function - | SumYield -> matcher sum - | SumCase (_name, ty, constr, rest) -> - let case = fun param -> constr (identity ty param) in - sid (matcher case) rest - in sid matcher sumty - | (Fix f) as ty -> (fun x -> identity (f ty) x) - - -(** Attempt to print a type. Will terminate on cyclic types, but only - * after printing a lot of unreadable stuff *) -let pp fmt ty = - let rec pp : type a. int -> Format.formatter -> a ty -> unit = fun depth fmt ty -> - if depth > 10 then Format.pp_print_string fmt "..." - else match ty with - | Int -> Format.pp_print_string fmt "int" - | String -> Format.pp_print_string fmt "string" - | List ty' -> - Format.fprintf fmt "@[<>%a@] list" (pp (depth+1)) ty' - | Pair (tya, tyb) -> - Format.fprintf fmt "@[(%a * %a)@]" (pp (depth+1)) tya (pp (depth+1)) tyb - | Record (descr, _) -> - let first = ref true in - let rec pp_rec : type b. Format.formatter -> (b, a) record -> unit = - fun fmt ty -> match ty with - | RecYield -> () - | RecField (name, ty', _get, cont) -> - if !first then first:=false else Format.pp_print_string fmt ", "; - Format.fprintf fmt "@[%s: %a@]" name (pp (depth+1)) ty'; - pp_rec fmt cont - in - Format.fprintf fmt "{@[%a@]}" pp_rec descr - | Sum {cases = Match(sumty, _)} -> - let rec pp_sum : type m. Format.formatter -> (m, unit, a) sum -> unit = - fun fmt case -> match case with - | SumYield -> () - | SumCase(name, ty', _, cont) -> - Format.fprintf fmt "@[| %s -> %a@]" name (pp (depth+1)) ty'; - pp_sum fmt cont - in - Format.fprintf fmt "@[case %a@]" pp_sum sumty - | Fix f -> pp depth fmt (f ty) - in pp 0 fmt ty - -(** {2 Tests} *) - -type my_record = - { - a: int; - b: string list; - } - -let my_record = - Record( - RecField ("a", Int, (fun {a} -> a), - RecField ("b", List String, (fun {b} -> b), - RecYield)), fun a b -> {a;b}) - -type my_sum = -| A of int -| B of string list - -let my_sum = - Sum{ cases = Match( - SumCase ("a", Int, (fun a -> A a), - SumCase ("b", List String, (fun b -> B b), - SumYield)), fun pa pb -> function A a -> pa a | B b -> pb b) } - -type lambda = - | Var of string - | App of lambda * lambda - | Lambda of string * lambda - -let lambda = - sum_fix (fun lambda -> {cases=Match( - SumCase("var", String, (fun s -> Var s), - SumCase("app", Pair(lambda,lambda), (fun (t1,t2) -> App(t1,t2)), - SumCase("lambda", Pair(String,lambda), (fun (x,t') -> Lambda(x,t')), - SumYield))), - fun pvar papp plambda -> function - | Var s -> pvar s - | App (t1,t2) -> papp (t1, t2) - | Lambda (x, t') -> plambda (x, t'))}) - diff --git a/src/misc/ty.mli b/src/misc/ty.mli deleted file mode 100644 index 0b794df5..00000000 --- a/src/misc/ty.mli +++ /dev/null @@ -1,84 +0,0 @@ - -(* -copyright (c) 2014, Simon Cruanes, Gabriel Scherer -all rights reserved. - -redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -redistributions of source code must retain the above copyright notice, this -list of conditions and the following disclaimer. redistributions in binary -form must reproduce the above copyright notice, this list of conditions and the -following disclaimer in the documentation and/or other materials provided with -the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -(** {1 Dynamic Type Representation} *) - -type 'a ty = - | Int: int ty - | String: string ty - | List: 'a ty -> 'a list ty - | Pair: ('a ty * 'b ty) -> ('a * 'b) ty - | Record: ('builder, 'r) record * 'builder -> 'r ty - | Sum: 's sum_cps -> 's ty - | Fix : ('a ty -> 'a ty) -> 'a ty - -and (_, _) record = - | RecField : string * 'a ty * ('r -> 'a) * ('builder, 'r) record - -> ('a -> 'builder, 'r) record - | RecYield : ('r , 'r) record - -(* yeah, this is a bit hard to swallow: we need to quantify - universally over the return type of the pattern-matching, and then - existentially on the type of the partial matching function -*) -and 's sum_cps = { cases : 't . ('s, 't) sum_ex } -and ('s, 't) sum_ex = Match : ('matcher, 't, 's) sum * 'matcher -> ('s, 't) sum_ex - -and (_, _, _) sum = - | SumCase: string * 'a ty * ('a -> 's) * ('matcher, 't, 's) sum - -> (('a -> 't) -> 'matcher, 't, 's) sum - | SumYield : (('s -> 't), 't, 's) sum - -val record_fix : ('a ty -> ('b, 'a) record * 'b) -> 'a ty - -val sum_fix : ('a ty -> 'a sum_cps) -> 'a ty - -val identity : 'a ty -> 'a -> 'a - -val pp : Format.formatter -> _ ty -> unit - -(** {2 Tests} *) - -type my_record = - { - a: int; - b: string list; - } - -val my_record : my_record ty - -type my_sum = -| A of int -| B of string list - -val my_sum : my_sum ty - -type lambda = - | Var of string - | App of lambda * lambda - | Lambda of string * lambda - -val lambda : lambda ty diff --git a/tests/run_tests.ml b/tests/run_tests.ml index 2641584d..6fd66b5d 100644 --- a/tests/run_tests.ml +++ b/tests/run_tests.ml @@ -1,24 +1,15 @@ open OUnit -(* TODO more tests *) - let suite = "all_tests" >::: [ Test_pHashtbl.suite; Test_PersistentHashtbl.suite; Test_bv.suite; - Test_PiCalculus.suite; - Test_splayMap.suite; Test_CCHeap.suite; - Test_cc.suite; Test_puf.suite; Test_vector.suite; Test_deque.suite; - Test_fHashtbl.suite; Test_fQueue.suite; - Test_flatHashtbl.suite; - Test_heap.suite; - Test_graph.suite; Test_univ.suite; Test_mixtbl.suite; ] diff --git a/tests/test_PiCalculus.ml b/tests/test_PiCalculus.ml deleted file mode 100644 index 1a2a1243..00000000 --- a/tests/test_PiCalculus.ml +++ /dev/null @@ -1,35 +0,0 @@ - -open OUnit - -open Containers_misc -open PiCalculus -module Pi = PiCalculus - -let test_message () = - let r = ref 0 in - let p1 = new_ - (fun c -> - send_one c 1 stop ||| - receive_one c (fun x -> r := x; stop)) - in - Pi.run p1; - OUnit.assert_equal ~printer:string_of_int 1 !r; - () - -let test_replicate () = - let a = ref 0 in - let b = ref 0 in - let p1 = new_ - (fun c -> - replicate (escape (fun () -> incr a; send_one c !a stop)) ||| - receive_one c (fun _ -> receive_one c (fun x -> b := x; stop))) - in - run p1; - OUnit.assert_equal ~printer:string_of_int 2 !b; - () - -let suite = - "test_PiCalculus" >::: - [ "test_message" >:: test_message; - "test_replicate" >:: test_replicate; - ] diff --git a/tests/test_cc.ml b/tests/test_cc.ml deleted file mode 100644 index 97b40b7a..00000000 --- a/tests/test_cc.ml +++ /dev/null @@ -1,93 +0,0 @@ -(** Tests for congruence closure *) - -open OUnit - -let parse = CC.parse -let pp = CC.pp - -module CT = CC.StrTerm -module CC = CC.StrCC - -let test_add () = - let cc = CC.create 5 in - let t = parse "((a (b c)) d)" in - OUnit.assert_equal ~cmp:CT.eq t t; - let t2 = parse "(f (g (h x)))" in - OUnit.assert_bool "not eq" (not (CC.eq cc t t2)); - () - -let test_merge () = - let t1 = parse "((f (a b)) c)" in - let t2 = parse "((f (a b2)) c2)" in - (* Format.printf "t1=%a, t2=%a@." pp t1 pp t2; *) - let cc = CC.create 5 in - (* merge b and b2 *) - let cc = CC.merge cc (parse "b") (parse "b2") in - OUnit.assert_bool "not eq" (not (CC.eq cc t1 t2)); - OUnit.assert_bool "eq_sub" (CC.eq cc (parse "b") (parse "b2")); - (* merge c and c2 *) - let cc = CC.merge cc (parse "c") (parse "c2") in - OUnit.assert_bool "eq_sub" (CC.eq cc (parse "c") (parse "c2")); - (* Format.printf "t1=%a, t2=%a@." pp (CC.normalize cc t1) pp (CC.normalize cc t2); *) - OUnit.assert_bool "eq" (CC.eq cc t1 t2); - () - -let test_merge2 () = - let cc = CC.create 5 in - let cc = CC.distinct cc (parse "a") (parse "b") in - let cc = CC.merge cc (parse "(f c)") (parse "a") in - let cc = CC.merge cc (parse "(f d)") (parse "b") in - OUnit.assert_bool "not_eq" (not (CC.can_eq cc (parse "a") (parse "b"))); - OUnit.assert_bool "inconsistent" - (try ignore (CC.merge cc (parse "c") (parse "d")); false - with CC.Inconsistent _ -> true); - () - -let test_merge3 () = - let cc = CC.create 5 in - (* f^3(a) = a *) - let cc = CC.merge cc (parse "a") (parse "(f (f (f a)))") in - OUnit.assert_equal ~cmp:CT.eq (parse "(f (f a))") (parse "(f (f a))"); - (* f^4(a) = a *) - let cc = CC.merge cc (parse "(f (f (f (f (f a)))))") (parse "a") in - (* CC.iter_equiv_class cc (parse "a") (fun t -> Format.printf "a = %a@." pp t); *) - (* hence, f^5(a) = f^2(f^3(a)) = f^2(a), and f^3(a) = f(f^2(a)) = f(a) = a *) - OUnit.assert_bool "eq" (CC.eq cc (parse "a") (parse "(f a)")); - () - -let test_merge4 () = - let cc = CC.create 5 in - let cc = CC.merge cc (parse "true") (parse "(p (f (f (f (f (f (f a)))))))") in - let cc = CC.merge cc (parse "a") (parse "(f b)") in - let cc = CC.merge cc (parse "(f a)") (parse "b") in - OUnit.assert_bool "eq" (CC.eq cc (parse "a") (parse "(f (f (f (f (f (f a))))))")); - () - -let test_explain () = - let cc = CC.create 5 in - (* f^3(a) = a *) - let cc = CC.merge cc (parse "a") (parse "(f (f (f a)))") in - (* f^4(a) = a *) - let cc = CC.merge cc (parse "(f (f (f (f (f a)))))") (parse "a") in - (* Format.printf "t: %a@." pp (parse "(f (f (f (f (f a)))))"); *) - (* hence, f^5(a) = f^2(f^3(a)) = f^2(a), and f^3(a) = f(f^2(a)) = f(a) = a *) - let l = CC.explain cc (parse "a") (parse "(f (f a))") in - (* - List.iter - (function - | CC.ByMerge (a,b) -> Format.printf "merge %a %a@." pp a pp b - | CC.ByCongruence (a,b) -> Format.printf "congruence %a %a@." pp a pp b) - l; - *) - OUnit.assert_equal 4 (List.length l); - () - -let suite = - "test_cc" >::: - [ "test_add" >:: test_add; - "test_merge" >:: test_merge; - "test_merge2" >:: test_merge2; - "test_merge3" >:: test_merge3; - "test_merge4" >:: test_merge4; - "test_explain" >:: test_explain; - ] diff --git a/tests/test_fHashtbl.ml b/tests/test_fHashtbl.ml deleted file mode 100644 index d77d7b13..00000000 --- a/tests/test_fHashtbl.ml +++ /dev/null @@ -1,124 +0,0 @@ - -open OUnit -open Containers_misc - - - -module Test(SomeHashtbl : FHashtbl.S with type key = int) = struct - let test_add () = - let h = SomeHashtbl.empty 32 in - let h = SomeHashtbl.replace h 42 "foo" in - OUnit.assert_equal (SomeHashtbl.find h 42) "foo" - - let my_list = - [ 1, "a"; - 2, "b"; - 3, "c"; - 4, "d"; - ] - - let my_seq = Sequence.of_list my_list - - let test_of_seq () = - let h = SomeHashtbl.of_seq my_seq in - OUnit.assert_equal "b" (SomeHashtbl.find h 2); - OUnit.assert_equal "a" (SomeHashtbl.find h 1); - OUnit.assert_raises Not_found (fun () -> SomeHashtbl.find h 42); - () - - let test_to_seq () = - let h = SomeHashtbl.of_seq my_seq in - let l = Sequence.to_list (SomeHashtbl.to_seq h) in - OUnit.assert_equal my_list (List.sort compare l) - - let test_resize () = - let h = SomeHashtbl.of_seq - (Sequence.map (fun i -> i, string_of_int i) - (Sequence.int_range ~start:0 ~stop:200)) in - OUnit.assert_equal 201 (SomeHashtbl.size h); - () - - let test_persistent () = - let h = SomeHashtbl.of_seq my_seq in - OUnit.assert_equal "a" (SomeHashtbl.find h 1); - OUnit.assert_raises Not_found (fun () -> SomeHashtbl.find h 5); - let h' = SomeHashtbl.replace h 5 "e" in - OUnit.assert_equal "a" (SomeHashtbl.find h' 1); - OUnit.assert_equal "e" (SomeHashtbl.find h' 5); - OUnit.assert_equal "a" (SomeHashtbl.find h 1); - OUnit.assert_raises Not_found (fun () -> SomeHashtbl.find h 5); - () - - let test_big () = - let n = 10000 in - let seq = Sequence.map (fun i -> i, string_of_int i) - (Sequence.int_range ~start:0 ~stop:n) in - let h = SomeHashtbl.of_seq seq in - (* - Format.printf "@[table:%a@]@." (Sequence.pp_seq - (fun formatter (k,v) -> Format.fprintf formatter "%d -> \"%s\"" k v)) - (SomeHashtbl.to_seq h); - *) - Sequence.iter - (fun (k,v) -> - (* - Format.printf "lookup %d@." k; - *) - OUnit.assert_equal ~printer:(fun x -> x) v (SomeHashtbl.find h k)) - seq; - OUnit.assert_raises Not_found (fun () -> SomeHashtbl.find h (n+1)); - () - - let test_remove () = - let h = SomeHashtbl.of_seq my_seq in - OUnit.assert_equal (SomeHashtbl.find h 2) "b"; - OUnit.assert_equal (SomeHashtbl.find h 3) "c"; - OUnit.assert_equal (SomeHashtbl.find h 4) "d"; - OUnit.assert_equal (SomeHashtbl.size h) 4; - let h = SomeHashtbl.remove h 2 in - OUnit.assert_equal (SomeHashtbl.find h 3) "c"; - OUnit.assert_equal (SomeHashtbl.size h) 3; - (* test that 2 has been removed *) - OUnit.assert_raises Not_found (fun () -> SomeHashtbl.find h 2) - - let test_size () = - let open Sequence.Infix in - let n = 10000 in - let seq = Sequence.map (fun i -> i, string_of_int i) (0 -- n) in - let h = SomeHashtbl.of_seq seq in - OUnit.assert_equal (n+1) (SomeHashtbl.size h); - let h = Sequence.fold (fun h i -> SomeHashtbl.remove h i) h (0 -- 500) in - OUnit.assert_equal (n-500) (SomeHashtbl.size h); - OUnit.assert_bool "is_empty" (SomeHashtbl.is_empty (SomeHashtbl.empty 16)); - () - - let suite = - "test_FHashtbl" >::: - [ "test_add" >:: test_add; - "test_of_seq" >:: test_of_seq; - "test_to_seq" >:: test_to_seq; - "test_resize" >:: test_resize; - "test_persistent" >:: test_persistent; - "test_big" >:: test_big; - "test_remove" >:: test_remove; - "test_size" >:: test_size; - ] -end - -module ITreeHashtbl = FHashtbl.Tree(struct - type t = int - let equal i j = i = j - let hash i = i -end) - -module IFlatHashtbl = FHashtbl.Flat(struct - type t = int - let equal i j = i = j - let hash i = i -end) - -module TestTree = Test(ITreeHashtbl) -module TestFlat = Test(IFlatHashtbl) - -let suite = - OUnit.TestList ["tree" >: TestTree.suite; "flat" >: TestFlat.suite] diff --git a/tests/test_flatHashtbl.ml b/tests/test_flatHashtbl.ml deleted file mode 100644 index d0cde3a9..00000000 --- a/tests/test_flatHashtbl.ml +++ /dev/null @@ -1,93 +0,0 @@ - -open OUnit -open Containers_misc - - - -module IHashtbl = FlatHashtbl.Make(struct - type t = int - let equal i j = i = j - let hash i = i -end) - -let test_add () = - let h = IHashtbl.create 5 in - IHashtbl.replace h 42 "foo"; - OUnit.assert_equal (IHashtbl.find h 42) "foo" - -let my_list = - [ 1, "a"; - 2, "b"; - 3, "c"; - 4, "d"; - ] - -let my_seq = Sequence.of_list my_list - -let test_of_seq () = - let h = IHashtbl.create 5 in - IHashtbl.of_seq h my_seq; - OUnit.assert_equal (IHashtbl.find h 2) "b"; - OUnit.assert_equal (IHashtbl.find h 1) "a"; - OUnit.assert_raises Not_found (fun () -> IHashtbl.find h 42); - () - -let test_to_seq () = - let h = IHashtbl.create 5 in - IHashtbl.of_seq h my_seq; - let l = Sequence.to_list (IHashtbl.to_seq h) in - OUnit.assert_equal my_list (List.sort compare l) - -let test_resize () = - let h = IHashtbl.create 5 in - for i = 0 to 10 do - IHashtbl.replace h i (string_of_int i); - done; - OUnit.assert_bool "must have been resized" (IHashtbl.length h > 5); - () - -let test_eq () = - let h = IHashtbl.create 3 in - IHashtbl.replace h 1 "odd"; - IHashtbl.replace h 2 "even"; - OUnit.assert_equal (IHashtbl.find h 1) "odd"; - OUnit.assert_equal (IHashtbl.find h 2) "even"; - () - -let test_copy () = - let h = IHashtbl.create 2 in - IHashtbl.replace h 1 "one"; - OUnit.assert_equal (IHashtbl.find h 1) "one"; - OUnit.assert_raises Not_found (fun () -> IHashtbl.find h 2); - let h' = IHashtbl.copy h in - IHashtbl.replace h' 2 "two"; - OUnit.assert_equal (IHashtbl.find h' 1) "one"; - OUnit.assert_equal (IHashtbl.find h' 2) "two"; - OUnit.assert_equal (IHashtbl.find h 1) "one"; - OUnit.assert_raises Not_found (fun () -> IHashtbl.find h 2); - () - -let test_remove () = - let h = IHashtbl.create 3 in - IHashtbl.of_seq h my_seq; - OUnit.assert_equal (IHashtbl.find h 2) "b"; - OUnit.assert_equal (IHashtbl.find h 3) "c"; - OUnit.assert_equal (IHashtbl.find h 4) "d"; - OUnit.assert_equal (IHashtbl.length h) 4; - IHashtbl.remove h 2; - OUnit.assert_equal (IHashtbl.find h 3) "c"; - OUnit.assert_equal (IHashtbl.length h) 3; - (* test that 2 has been removed *) - OUnit.assert_raises Not_found (fun () -> IHashtbl.find h 2) - -let suite = - "test_flatHashtbl" >::: - [ "test_add" >:: test_add; - "test_of_seq" >:: test_of_seq; - "test_to_seq" >:: test_to_seq; - "test_resize" >:: test_resize; - "test_eq" >:: test_eq; - "test_copy" >:: test_copy; - "test_remove" >:: test_remove; - ] - diff --git a/tests/test_graph.ml b/tests/test_graph.ml deleted file mode 100644 index 70e126d3..00000000 --- a/tests/test_graph.ml +++ /dev/null @@ -1,88 +0,0 @@ - -(** Tests on graphs *) - -open OUnit -open Helpers -open Containers_misc - - -module G = PersistentGraph - -(* build a graph from a list of pairs of ints *) -let mk_graph l = - let g = G.empty 5 in - G.add_seq g - (Sequence.map (fun (x,y) -> x,1,y) - (Sequence.of_list l)); - g - -let test_copy () = - let g = mk_graph [0,1; 1,2; 2,3; 3,0] in - let g' = G.copy g in - G.add g 1 1 3; - G.add g 1 2 3; - OUnit.assert_equal ~printer:print_int_list - [1;2] (List.sort compare (Sequence.to_list (G.between g 1 3))); - OUnit.assert_bool "copy" (Sequence.is_empty (G.between g' 1 3)); - () - -let test_roots () = - let g = mk_graph [0,1; 1,2; 2,3; 4,1; 5,1; 6,5; 3,5] in - let roots = Sequence.to_list (G.roots g) in - OUnit.assert_equal (List.sort compare roots) [0;4;6] - -let test_leaves () = - let g = mk_graph [0,1; 1,2; 2,3; 4,1; 6,5; 3,5; 3,7] in - let leaves = Sequence.to_list (G.leaves g) in - OUnit.assert_equal (List.sort compare leaves) [5;7] - -let test_dfs () = - let g = mk_graph [0,1; 1,2; 2,3; 3,0; 1,4; 1,5; 5,6; 4,6; 6,0] in - let l = ref [] in - G.dfs g 0 (fun (v,i) -> l := (v,i) :: !l); - (* get index of vertex [v] in DFS traversal *) - let get_idx v = List.assoc v !l in - OUnit.assert_bool "order" (get_idx 0 < get_idx 1); - OUnit.assert_bool "order" (get_idx 1 < get_idx 2); - OUnit.assert_bool "order" (get_idx 2 < get_idx 3); - OUnit.assert_bool "order" (get_idx 1 < get_idx 4); - OUnit.assert_bool "order" (get_idx 1 < get_idx 5); - OUnit.assert_bool "order" (get_idx 4 < get_idx 6 || get_idx 5 < get_idx 6); - () - -let test_bfs () = - let g = mk_graph [0,1; 1,2; 2,3; 2,4; 3,0; 1,4; 1,5; 5,6; 4,6; 6,0] in - let l = Sequence.to_list - (Sequence.mapi (fun i v -> (v,i)) (G.bfs_seq g 0)) in - (* get index of vertex [v] in DFS traversal *) - let get_idx v = List.assoc v l in - OUnit.assert_bool "order" (get_idx 0 < get_idx 1); - OUnit.assert_bool "order" (get_idx 0 < get_idx 2); - OUnit.assert_bool "order" (get_idx 0 < get_idx 4); - OUnit.assert_bool "order" (get_idx 1 < get_idx 3); - OUnit.assert_bool "order" (get_idx 2 < get_idx 3); - OUnit.assert_bool "order" (get_idx 4 < get_idx 6); - OUnit.assert_bool "order" (get_idx 5 < get_idx 6); - () - -let rec pp_path p = - CCPrint.to_string (CCList.pp ~sep:"; " pp_edge) p -and pp_edge b (v1,e,v2) = - Printf.bprintf b "%d -> %d" v1 v2 - -let test_dijkstra () = - let g = mk_graph [0,1; 1,2; 2,3; 3,4; 3,0; 4,5; 1,5; 5,6; 4,6; 6,0] in - let path = G.min_path g ~cost:(fun x -> x) 0 6 in - let path = G.rev_path path in - OUnit.assert_equal ~printer:pp_path [0,1,1; 1,1,5; 5,1,6] path; - () - -let suite = - "test_graph" >::: - [ "test_copy" >:: test_copy; - "test_leaves" >:: test_leaves; - "test_roots" >:: test_roots; - "test_dfs" >:: test_dfs; - "test_bfs" >:: test_bfs; - "test_dijkstra" >:: test_dijkstra; - ] diff --git a/tests/test_heap.ml b/tests/test_heap.ml deleted file mode 100644 index 62b62586..00000000 --- a/tests/test_heap.ml +++ /dev/null @@ -1,42 +0,0 @@ -(** Test heaps *) - -open OUnit -open Helpers -open Containers_misc - - -let test_empty () = - let h = Heap.empty ~cmp:(fun x y -> x - y) in - OUnit.assert_bool "is_empty empty" (Heap.is_empty h); - Heap.insert h 42; - OUnit.assert_bool "not empty" (not (Heap.is_empty h)); - () - -let test_sort () = - let h = Heap.empty ~cmp:(fun x y -> x - y) in - (* Heap sort *) - let l = [3;4;2;1;6;5;0;7;10;9;8] in - Heap.of_seq h (Sequence.of_list l); - OUnit.assert_equal ~printer:string_of_int 11 (Heap.size h); - let l' = Sequence.to_list (Heap.to_seq h) in - OUnit.assert_equal ~printer:print_int_list [0;1;2;3;4;5;6;7;8;9;10] l' - -let test_remove () = - let h = Heap.empty ~cmp:(fun x y -> x - y) in - let l = [3;4;2;1;6;5;0;7;10;9;8] in - Heap.of_seq h (Sequence.of_list l); - (* check pop *) - OUnit.assert_equal 0 (Heap.pop h); - OUnit.assert_equal 1 (Heap.pop h); - OUnit.assert_equal 2 (Heap.pop h); - OUnit.assert_equal 3 (Heap.pop h); - (* check that elements have been removed *) - let l' = Sequence.to_list (Heap.to_seq h) in - OUnit.assert_equal ~printer:print_int_list [4;5;6;7;8;9;10] l' - -let suite = - "test_heaps" >::: - [ "test_empty" >:: test_empty; - "test_sort" >:: test_sort; - "test_remove" >:: test_remove; - ] diff --git a/tests/test_splayMap.ml b/tests/test_splayMap.ml deleted file mode 100644 index fb1d85b8..00000000 --- a/tests/test_splayMap.ml +++ /dev/null @@ -1,44 +0,0 @@ - -open OUnit -open Containers_misc - - - -let test1 () = - let empty = SplayMap.empty () in - let m = SplayMap.of_seq empty (Sequence.of_list [1, "1"; 2, "2"; 3, "3"]) in - OUnit.assert_equal ~printer:(fun s -> s) "2" (SplayMap.find m 2); - OUnit.assert_equal ~printer:(fun s -> s) "2" (SplayMap.find m 2); - OUnit.assert_equal ~printer:(fun s -> s) "3" (SplayMap.find m 3); - OUnit.assert_equal ~printer:(fun s -> s) "1" (SplayMap.find m 1); - OUnit.assert_raises Not_found (fun () -> SplayMap.find m 4); - () - -let test_remove () = - let n = 100 in - let m = SplayMap.of_seq (SplayMap.empty ()) - (Sequence.zip (Sequence.zip_i (Sequence.int_range ~start:0 ~stop:n))) in - for i = 0 to n do - OUnit.assert_equal ~printer:string_of_int i (SplayMap.find m i); - done; - let m = SplayMap.remove m (n/2) in - OUnit.assert_equal ~printer:string_of_int n (SplayMap.find m n); - OUnit.assert_raises Not_found (fun () -> SplayMap.find m (n/2)); - () - -let test_big () = - let n = 100_000 in - let m = SplayMap.of_seq (SplayMap.empty ()) - (Sequence.zip (Sequence.zip_i (Sequence.int_range ~start:0 ~stop:n))) in - for i = 0 to n do - OUnit.assert_equal ~printer:string_of_int i (SplayMap.find m i); - done; - OUnit.assert_equal ~printer:string_of_int (n+1) (SplayMap.size m); - () - -let suite = - "test_splayMap" >::: - [ "test1" >:: test1; - "test_remove" >:: test_remove; - "test_big" >:: test_big; - ]