From b60d4db95ae570fa08efcd5825d237fd8b61bc31 Mon Sep 17 00:00:00 2001 From: Eduardo Souza Date: Wed, 10 Jun 2026 01:21:54 +0000 Subject: [PATCH] Add hashcons weak-pointer/ephemeron benchmarks (bench_bdd, bench_lambda) Add backtracking's quick-and-dirty hash-consing benchmarks from ocaml-hashcons#19 to simple/hashcons/, filling a weak-pointer/ephemeron coverage gap in the suite. hashcons.ml/.mli are vendored as a local library so only the runtime varies across compiler comparisons. - bench_bdd -de-bruijn N: hash-consed BDD for a de Bruijn tautology; the workload ocaml/ocaml#13580 (mark-delay, 5.5) targets. At N=800 it shows ~1.46x speedup and ~41% lower peak heap on 5.5 vs 5.4, and is highly space_overhead-sensitive. - bench_bdd -pigeon N: pigeonhole tautology; milder hash-consing stressor. - bench_lambda N: lambda-calculus quicksort over hash-consed terms; CPU-bound short micro. Reads its term file from $QUICKSORT_TERM (the run cwd is a temp dir) with a fallback to the upstream relative default. Co-Authored-By: Claude Opus 4.8 (1M context) --- README.md | 16 + simple/hashcons/bench_bdd.build.sh | 7 + simple/hashcons/bench_bdd.ml | 306 +++++++ simple/hashcons/bench_lambda.build.sh | 10 + simple/hashcons/bench_lambda.ml | 206 +++++ simple/hashcons/dune | 19 + simple/hashcons/dune-project | 1 + simple/hashcons/hashcons.ml | 1054 +++++++++++++++++++++++++ simple/hashcons/hashcons.mli | 227 ++++++ simple/hashcons/quicksort.term | Bin 0 -> 395 bytes 10 files changed, 1846 insertions(+) create mode 100755 simple/hashcons/bench_bdd.build.sh create mode 100644 simple/hashcons/bench_bdd.ml create mode 100755 simple/hashcons/bench_lambda.build.sh create mode 100644 simple/hashcons/bench_lambda.ml create mode 100644 simple/hashcons/dune create mode 100644 simple/hashcons/dune-project create mode 100644 simple/hashcons/hashcons.ml create mode 100644 simple/hashcons/hashcons.mli create mode 100644 simple/hashcons/quicksort.term diff --git a/README.md b/README.md index a8ce7f6..fcace98 100644 --- a/README.md +++ b/README.md @@ -246,6 +246,22 @@ Macrobenchmarks are registered in `running-ng`'s `macrobenchmarks.yml`. - **Args:** _(none)_ - **Description:** Binary Decision Diagram operations (AND, OR, NOT, quantification) on propositional formulae. Pointer-heavy graph structure; exercises major GC and sharing. +### hashcons/bench_bdd + +- **Source:** `backtracking`'s quick-and-dirty hash-consing benchmarks, provided in [ocaml-hashcons#19](https://github.com/backtracking/ocaml-hashcons/issues/19). Distinct from the classic `bdd` above: this one is hash-consed and weak-pointer-backed. +- **Build:** dune; vendors `hashcons.ml`/`.mli` from `backtracking/ocaml-hashcons` as a local library (pinned so only the runtime varies across compiler comparisons). +- **Args:** `-de-bruijn ` (config: `800`) or `-pigeon ` (config: `12`). `-v` dumps hash-consing table stats. +- **Description:** Builds a BDD for a de Bruijn or pigeonhole tautology, exercising hash-consing (weak pointers / ephemerons) and the major-GC pacing that governs how fast unreachable nodes are reclaimed. +- **Note:** The `-de-bruijn` mode is the one [ocaml/ocaml#13580](https://github.com/ocaml/ocaml/pull/13580) (mark-delay, 5.5) targets — at `N=800` it shows ~1.46× speedup and ~41% lower peak heap on 5.5 vs 5.4. It is highly sensitive to `space_overhead`. `-pigeon` is a milder hash-consing stressor (barely affected by the PR). Runtime scales with `N`, and so does peak RSS. + +### hashcons/bench_lambda + +- **Source:** same archive as `hashcons/bench_bdd` ([ocaml-hashcons#19](https://github.com/backtracking/ocaml-hashcons/issues/19)). +- **Build:** dune; shares the vendored `hashcons` library. +- **Args:** `` — list length to quicksort (config: `6`). `-v` dumps heap + table stats. +- **Description:** Normalises a quicksort written in the λ-calculus (Church-encoded naturals) over a random list, with hash-consed λ-terms. CPU-bound: heap stays ~8 MB regardless of `N`; runtime grows combinatorially (N=6 ≈ 0.8 s, N=7 ≈ 60 s), so it is a short micro and cannot be tuned to macro length. +- **Adaptation:** Reads its marshalled term from `$QUICKSORT_TERM` (absolute path) when set, else the upstream relative default `quicksort.term`. The run cwd is a temp dir, so the config must set `QUICKSORT_TERM` to `…/simple/hashcons/quicksort.term`. + ### hamming - **Source:** sandmark `benchmarks/hamming/` diff --git a/simple/hashcons/bench_bdd.build.sh b/simple/hashcons/bench_bdd.build.sh new file mode 100755 index 0000000..86cc4af --- /dev/null +++ b/simple/hashcons/bench_bdd.build.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -euo pipefail +BENCH_DIR="${RUNNING_OCAML_BENCH_DIR:-$(cd "$(dirname "$0")" && pwd)}" +OUT="${RUNNING_OCAML_OUTPUT:-${BENCH_DIR}/bench_bdd-${RUNNING_OCAML_RUNTIME_NAME:-runtime}}" +dune build --root "${BENCH_DIR}" --profile release bench_bdd.exe +cp "${BENCH_DIR}/_build/default/bench_bdd.exe" "${OUT}" +chmod +x "${OUT}" diff --git a/simple/hashcons/bench_bdd.ml b/simple/hashcons/bench_bdd.ml new file mode 100644 index 0000000..56e12d2 --- /dev/null +++ b/simple/hashcons/bench_bdd.ml @@ -0,0 +1,306 @@ + +type t = + | Pvar of string + | Pnot of t + | Pand of t * t + | Por of t * t + | Pimp of t * t + | Piff of t * t + | Ptrue + | Pfalse + +let pand p1 p2 = match p1, p2 with + | Ptrue, p2 -> p2 + | p1, Ptrue -> p1 + | _ -> Pand (p1, p2) + +let pands i j f = + let rec mk k = if k > j then Ptrue else pand (f k) (mk (k+1)) in + mk i + +let piff p1 p2 = match p1, p2 with + | Ptrue, p2 -> p2 + | p1, Ptrue -> p1 + | _ -> Piff (p1, p2) + +let piffs i j f = + let rec mk k = if k > j then Ptrue else piff (f k) (mk (k+1)) in + mk i + +let por p1 p2 = match p1, p2 with + | Pfalse, _p2 -> p1 + | p1, Pfalse -> p1 + | _ -> Por (p1, p2) + +let pors i j f = + let rec mk k = if k > j then Pfalse else por (f k) (mk (k+1)) in + mk i + +(* de bruijn *) + +let var i = Pvar ("p" ^ string_of_int i) + +let iff p1 p2 = Pand (Pimp (p1, p2), Pimp (p2, p1)) + +(** +de_bruijn_p(n) == LHS(2*n+1) -> RHS(2*n+1) +de_bruijn_n(n) == LHS(2*n) -> (p0 v RHS(2*n) v ~p0) + +RHS(m) = &&_{i=1..m} p(i) +LHS(m) = &&_{i=1..m} ((p(i)<->p(i+1)) -> c(n)) +where addition is computed modulo m. +***) + +let lhs m = + pands 1 m (fun i -> Pnot (iff (var i) (var (if i=m then 1 else i+1)))) + +let de_bruijn_p n = Pnot (lhs (2*n+1)) +let de_bruijn_n n = Pnot (lhs (2*n)) + +(* pigeons + +ph_p(n) =def left(n) -> right(n) + +left(n) =def &&_{p=1..n+1} (vv_{j=1,..n} occ(i,j) ) +right(n) =def vv_{h=1..n, p1=1..{n+1}, p2={p1+1}..{n+1}} s(i1,i2,j) +s(p1,p2,h) =def occ(p1,h) & occ(p2,h) + +*) + +let occ i j = Pvar ("occ_" ^ string_of_int i ^ "_" ^ string_of_int j) + +let left n = pands 1 (n+1) (fun i -> pors 1 n (fun j -> occ i j)) +let right n = + pors 1 n (fun h -> + pors 1 (n+1) (fun p1 -> + pors (p1+1) (n+1) (fun p2 -> Pand (occ p1 h, + occ p2 h)))) + +let pigeon_p n = Pimp (left n, right n) + +let equiv_p n = + let f = ref (var n) in + for i = 1 to n-1 do f := Piff (var (n-i), !f) done; + for i = 1 to n do f := Piff (var (n+1-i), !f) done; + !f + +open Format + +let print fmt p = + let rec pr fmt = function + | Pvar s -> fprintf fmt "%s" s + | Pnot f -> fprintf fmt "(~%a)" pr f + | Pand (f1, f2) -> fprintf fmt "(%a &@ %a)" pr f1 pr f2 + | Por (f1, f2) -> fprintf fmt "(%a v@ %a)" pr f1 pr f2 + | Pimp (f1, f2) -> fprintf fmt "(%a ->@ %a)" pr f1 pr f2 + | Piff (f1, f2) -> fprintf fmt "(%a <->@ %a)" pr f1 pr f2 + | Ptrue -> fprintf fmt "true" + | Pfalse -> fprintf fmt "false" + in + fprintf fmt "@[%a@]" pr p + +(* BDD *) + +open Hashcons + +type variable = int (* 1..max_var *) + +let max_var = ref 10 +let get_max_var () = !max_var +let set_max_var n = if n <= 0 then invalid_arg "Bdd.set_max_var"; max_var := n + +type bdd = view hash_consed +and view = Zero | One | Node of variable * bdd (*low*) * bdd (*high*) + +let view b = b.node + +module HC = Hashcons.Make( + struct + type t = view + let equal x y = match x, y with + | (Zero | One), (Zero | One) -> + x == y + | Node (v1, l1, h1), Node (v2, l2, h2) -> + v1 == v2 && l1 == l2 && h1 == h2 + | _ -> + false + let hash = function + | Zero -> 0 + | One -> 1 + | Node (v, l, h) -> abs (19 * (19 * l.tag + h.tag) + v) + end) + +let htable = HC.create 251 + +let zero = HC.hashcons htable Zero +let one = HC.hashcons htable One + +let var b = match b.node with + | Zero | One -> !max_var + 1 + | Node (v, _, _) -> v + +let low b = match b.node with + | Zero | One -> invalid_arg "Bdd.low" + | Node (_, l, _) -> l + +let high b = match b.node with + | Zero | One -> invalid_arg "Bdd.low" + | Node (_, _, h) -> h + +let mk v ~low ~high = + if low == high then low else HC.hashcons htable (Node (v, low, high)) + +let mk_var v = mk v ~low:zero ~high:one + +module Bdd = struct + type t = bdd + let equal = (==) + let hash b = b.tag + let compare b1 b2 = Stdlib.compare b1.tag b2.tag +end +module H1 = Hashtbl.Make(Bdd) + +let mk_not x = + let cache = H1.create 251 in + let rec mk_not_rec x = + try + H1.find cache x + with Not_found -> + let res = match x.node with + | Zero -> one + | One -> zero + | Node (v, l, h) -> mk v ~low:(mk_not_rec l) ~high:(mk_not_rec h) + in + H1.add cache x res; + res + in + mk_not_rec x + +let bool_of = function Zero -> false | One -> true | _ -> invalid_arg "bool_of" +let of_bool b = if b then one else zero + +module H2 = Hashtbl.Make( + struct + type t = bdd * bdd + let equal (u1,v1) (u2,v2) = u1==u2 && v1==v2 + let hash (u,v) = + (*abs (19 * u.tag + v.tag)*) + let s = u.tag + v.tag in abs (s * (s+1) / 2 + u.tag) + end) + +let apply op = + let op_z_z = of_bool (op false false) in + let op_z_o = of_bool (op false true) in + let op_o_z = of_bool (op true false) in + let op_o_o = of_bool (op true true) in + fun b1 b2 -> + let cache = H2.create 251 in + let rec app ((u1,u2) as u12) = + try + H2.find cache u12 + with Not_found -> + let res = match u1.node, u2.node with + | Zero, Zero -> op_z_z + | Zero, One -> op_z_o + | One, Zero -> op_o_z + | One, One -> op_o_o + | _ -> + let v1 = var u1 in + let v2 = var u2 in + if v1 == v2 then + mk v1 ~low:(app (low u1, low u2)) ~high:(app (high u1, high u2)) + else if v1 < v2 then + mk v1 ~low:(app (low u1, u2)) ~high:(app (high u1, u2)) + else (* v1 > v2 *) + mk v2 ~low:(app (u1, low u2)) ~high:(app (u1, high u2)) + in + H2.add cache u12 res; + res + in + app (b1, b2) + + +type boolean_op = bool -> bool -> bool +let op_and = (&&) +let op_or = (||) +let op_imp b1 b2 = (not b1) || b2 + +let mk_and = apply op_and +let mk_or = apply op_or +let mk_imp = apply op_imp + +(* satisfiability *) + +let is_sat b = b.node != Zero + +let tautology b = b.node == One + +(* formula -> bdd *) + +type formula = + | Ffalse + | Ftrue + | Fvar of variable + | Fand of formula * formula + | For of formula * formula + | Fimp of formula * formula + | Fnot of formula + +let rec build = function + | Ffalse -> zero + | Ftrue -> one + | Fvar v -> mk_var v + | Fand (f1, f2) -> mk_and (build f1) (build f2) + | For (f1, f2) -> mk_or (build f1) (build f2) + | Fimp (f1, f2) -> mk_imp (build f1) (build f2) + | Fnot f -> mk_not (build f) + + +let bdd_of_formula f = + let nbvar = ref 0 in + let vars = Hashtbl.create 17 in + let rec trans = function + | Pvar s -> + Fvar (try Hashtbl.find vars s + with Not_found -> incr nbvar; Hashtbl.add vars s !nbvar; !nbvar) + | Pnot f -> Fnot (trans f) + | Pand (f1, f2) -> Fand (trans f1, trans f2) + | Por (f1, f2) -> For (trans f1, trans f2) + | Pimp (f1, f2) -> Fimp (trans f1, trans f2) + | Piff (f1, f2) -> let f1 = trans f1 and f2 = trans f2 in + Fand (Fimp (f1, f2), Fimp (f2, f1)) + | Ptrue -> Ftrue + | Pfalse -> Ffalse + in + let f = trans f in + set_max_var !nbvar; + Format.printf "nb var = %d@." !nbvar; + build f + +(* bench *) + +type bench = De_bruijn | Pigeon +let bench = ref De_bruijn +let n = ref 10 +let verbose = ref false + +let () = + Arg.parse + ["-de-bruijn", Arg.Unit (fun () -> bench := De_bruijn), ""; + "-pigeon", Arg.Unit (fun () -> bench := Pigeon), ""; + "-v", Arg.Set verbose, ""; + ] + (fun x -> n := int_of_string x) + ""; + let f = match !bench with + | De_bruijn -> de_bruijn_p !n + | Pigeon -> pigeon_p !n in + let b = bdd_of_formula f in + assert (tautology b); + if not !verbose then exit 0; + let l,n,s,b1,b2,b3 = HC.stats htable in + printf "table length: %d / nb. entries: %d / sum of bucket length: %d@." + l n s; + printf "smallest bucket: %d / median bucket: %d / biggest bucket: %d@." + b1 b2 b3 + diff --git a/simple/hashcons/bench_lambda.build.sh b/simple/hashcons/bench_lambda.build.sh new file mode 100755 index 0000000..dec1c8d --- /dev/null +++ b/simple/hashcons/bench_lambda.build.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +set -euo pipefail +BENCH_DIR="${RUNNING_OCAML_BENCH_DIR:-$(cd "$(dirname "$0")" && pwd)}" +OUT="${RUNNING_OCAML_OUTPUT:-${BENCH_DIR}/bench_lambda-${RUNNING_OCAML_RUNTIME_NAME:-runtime}}" +dune build --root "${BENCH_DIR}" --profile release bench_lambda.exe +cp "${BENCH_DIR}/_build/default/bench_lambda.exe" "${OUT}" +chmod +x "${OUT}" +# Note: bench_lambda reads its data file from $QUICKSORT_TERM (absolute path); +# the running-ng config must point it at ${BENCH_DIR}/quicksort.term since the +# run cwd is a temp dir. diff --git a/simple/hashcons/bench_lambda.ml b/simple/hashcons/bench_lambda.ml new file mode 100644 index 0000000..bba3f60 --- /dev/null +++ b/simple/hashcons/bench_lambda.ml @@ -0,0 +1,206 @@ + +(** Another example involving λ-terms. This one is from + + Constructive Computation Theory + Gérard Huet, Inria, 2011 + https://gallium.inria.fr/~huet/PUBLIC/CCT.pdf + + section 2.2 (λ-calculus as a general programming language). + + Below we run a quicksort written in λ-calculus on lists of + Church-encoded natural numbers. The quicksort term is contained in + the marshaled file "quicksort.term". +*) + +open Hashcons + +type term = term_node hash_consed +and term_node = + | Ref of int (* variables as reference depth *) + | Abs of term (* abstraction [x]t *) + | App of term * term (* application (t u) *) + +module Term = Hashcons.Make( + struct + type t = term_node + let equal t1 t2 = match t1, t2 with + | Ref i, Ref j -> i == j + | Abs u, Abs v -> u == v + | App (u1,v1), App (u2,v2) -> u1 == u2 && v1 == v2 + | _ -> false + let hash = function + | Ref i -> i + | Abs t -> (19 * t.hkey + 1) + | App (u,v) -> (19 * (19 * u.hkey + v.hkey) + 2) + end) +let ht = Term.create 10007 +let ref i = Term.hashcons ht (Ref i) +let abs t = Term.hashcons ht (Abs t) +let app (u,v) = Term.hashcons ht (App (u,v)) + +let memo f = + let h = Hashtbl.create 251 in + fun x -> + try Hashtbl.find h x.tag + with Not_found -> let y = f x in Hashtbl.add h x.tag y; y +let memo2_int_term f = + let h = Hashtbl.create 251 in + fun x y -> + try Hashtbl.find h (x, y.tag) + with Not_found -> let z = f x y in Hashtbl.add h (x, y.tag) z; z +let memo2_term_term f = + let h = Hashtbl.create 251 in + fun x y -> + try Hashtbl.find h (x.tag, y.tag) + with Not_found -> let z = f x y in Hashtbl.add h (x.tag, y.tag) z; z + +let lift n = + let rec lift_rec k = + let rec lift_k t = match t.node with + | Ref i -> + if i abs (lift_rec (k+1) t) + | App (t, u) -> app (lift_k t, lift_k u) + in + lift_k + in + lift_rec 0 + +let lift = memo2_int_term lift + +let subst_count = Stdlib.ref 0 + +let subst w = + incr subst_count; + let rec subst_w n t = match t.node with + | Ref k -> + if k=n then lift n w (* substituted variable *) + else if k abs (subst_w (n+1) t) + | App (t, u) -> app (subst_w n t, subst_w n u) + in + subst_w 0 + +let subst = memo2_term_term subst + +let rec hnf t = match t.node with + | Ref _n -> t + | Abs t -> abs (hnf t) + | App (t, u) -> match hnf t with + | {node=Abs w;_} -> hnf (subst u w) + | h -> app (h, u) + +let nhf = memo hnf + +let rec nf t = match t.node with + | Ref _n -> t + | Abs t -> abs (nf t) + | App (t, u) -> match hnf t with + | {node=Abs w;_} -> nf (subst u w) + | h -> app (nf h, nf u) + +let nf = memo nf + +type expr = Ref2 of int | Abs2 of expr | App2 of expr * expr + +let rec term_of_expr = function + | Ref2 i -> ref i + | Abs2 t -> abs (term_of_expr t) + | App2 (u,v) -> app (term_of_expr u, term_of_expr v) + +let quicksort = + (* sandmark/running-ng adaptation: run cwd is a temp dir, so the data file + path is taken from $QUICKSORT_TERM (absolute) when set, else the upstream + relative default for standalone use. *) + let path = match Sys.getenv_opt "QUICKSORT_TERM" with + | Some p -> p + | None -> "quicksort.term" in + let c = open_in path in + let e = (input_value c : expr) in + close_in c; + term_of_expr e + +let nil = (*[c,n]n*) abs (abs (ref 0)) +let cons = (*[x,l][c,n](c x (l c n))*) + abs(abs(abs(abs(app(app (ref 1, + ref 3), + app (app (ref 2, + ref 1), + ref 0)))))) + +let zero = (*[s,z]z*) abs (abs (ref 0)) +let succ = (*[n][s,z](s (n s z))*) + abs(abs(abs(app (ref 1, + app (app (ref 2, ref 1), ref 0))))) + +let rec iter f n x = if n=0 then x else iter f (n-1) (f x) + +(* Church *) +let church n = iter (fun c -> nf (app (succ, c))) n zero + +(* list : int list -> term *) +let rec list = function + | x :: l -> + let cx = church x and ll = list l in + (*[c,n](c ^Cx (^Ll c n))*) + abs(abs(app (app (ref 1, cx), + app (app (ll, ref 1), ref 0)))) + | [] -> nil + +(* and back *) + +let eval_nat iter init = function + | {node=Abs {node=Abs t;_};_} (* [s,z]t *) -> + let rec eval_rec = function + | (* z *) {node=Ref 0;_} -> init + | (* (s u) *) {node=App ({node=Ref 1;_}, u);_} -> iter (eval_rec u) + | _ -> failwith "Not a normal church natural" + in + eval_rec t + | _ -> failwith "Not a normal church natural" + +let compute_nat = eval_nat (fun n->n+1) 0 + +let normal_nat n = compute_nat (nf n) + +let eval_list_of_nats = function + | {node=Abs {node=Abs t;_};_} (* [c,n]t *) -> + let rec lrec = function + | (* n *) {node=Ref 0;_} -> [] + | (* (c x l) *) {node=App ({node=App ({node=Ref 1;_}, x);_}, l);_} -> + (compute_nat x) :: (lrec l) + | _ -> failwith "Not a normal List" + in + lrec t + | _ -> failwith "Not a normal List" + +let normal_list l = eval_list_of_nats (nf l) + +open Format + +let n = Stdlib.ref 6 +let verbose = Stdlib.ref false + +let () = Arg.parse + ["-v", Arg.Set verbose, ""; + ] + (fun x -> n := int_of_string x) + "" + +let () = + Random.init 89; + let l0 = List.init !n (fun _ -> Random.int !n) in + let l1 = List.sort Stdlib.compare l0 in + assert (normal_list (app (quicksort, list l0)) = l1); + printf "subst count: %d@." !subst_count; + if not !verbose then exit 0; + let stat = Gc.stat () in + printf "top heap words: %d (%d kb)@." stat.Gc.top_heap_words + (stat.Gc.top_heap_words / 256); + let l,n,s,b1,b2,b3 = Term.stats ht in + printf "table length: %d / nb. entries: %d / sum of bucket length: %d@." + l n s; + printf "smallest bucket: %d / median bucket: %d / biggest bucket: %d@." + b1 b2 b3 diff --git a/simple/hashcons/dune b/simple/hashcons/dune new file mode 100644 index 0000000..ae0a523 --- /dev/null +++ b/simple/hashcons/dune @@ -0,0 +1,19 @@ +; Vendored copy of backtracking/ocaml-hashcons (hashcons.ml/.mli) pinned here +; so that only the runtime varies across compiler comparisons. +(library + (name hashcons) + (modules hashcons)) + +(executable + (name bench_bdd) + (modules bench_bdd) + (libraries hashcons) + (modes native) + (ocamlopt_flags (:standard -O3))) + +(executable + (name bench_lambda) + (modules bench_lambda) + (libraries hashcons) + (modes native) + (ocamlopt_flags (:standard -O3))) diff --git a/simple/hashcons/dune-project b/simple/hashcons/dune-project new file mode 100644 index 0000000..37f995d --- /dev/null +++ b/simple/hashcons/dune-project @@ -0,0 +1 @@ +(lang dune 3.0) diff --git a/simple/hashcons/hashcons.ml b/simple/hashcons/hashcons.ml new file mode 100644 index 0000000..4f2f438 --- /dev/null +++ b/simple/hashcons/hashcons.ml @@ -0,0 +1,1054 @@ +(**************************************************************************) +(* *) +(* Copyright (C) Jean-Christophe Filliatre *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + +(*s Hash tables for hash-consing. (Some code is borrowed from the ocaml + standard library, which is copyright 1996 INRIA.) *) + +type +'a hash_consed = { + hkey : int; + tag : int; + node : 'a } + +let gentag = + let r = ref 0 in + fun () -> incr r; !r + +type 'a t = { + mutable table : 'a hash_consed Weak.t array; + mutable totsize : int; (* sum of the bucket sizes *) + mutable limit : int; (* max ratio totsize/table length *) +} + +let create sz = + let sz = if sz < 7 then 7 else sz in + let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in + let emptybucket = Weak.create 0 in + { table = Array.make sz emptybucket; + totsize = 0; + limit = 3; } + +let clear t = + let emptybucket = Weak.create 0 in + for i = 0 to Array.length t.table - 1 do t.table.(i) <- emptybucket done; + t.totsize <- 0; + t.limit <- 3 + +let iter f t = + let rec iter_bucket i b = + if i >= Weak.length b then () else + match Weak.get b i with + | Some v -> f v; iter_bucket (i+1) b + | None -> iter_bucket (i+1) b + in + Array.iter (iter_bucket 0) t.table + +let count t = + let rec count_bucket i b accu = + if i >= Weak.length b then accu else + count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0)) + in + Array.fold_right (count_bucket 0) t.table 0 + +let next_sz n = min (3*n/2 + 3) (Sys.max_array_length - 1) + +let rec resize t = + let oldlen = Array.length t.table in + let newlen = next_sz oldlen in + if newlen > oldlen then begin + let newt = create newlen in + newt.limit <- t.limit + 100; (* prevent resizing of newt *) + iter (fun d -> add newt d) t; + t.table <- newt.table; + t.totsize <- newt.totsize + end + +and add t d = + let index = d.hkey mod (Array.length t.table) in + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let i = ref 0 in + while !i < sz && Weak.check bucket !i do incr i done; + if !i < sz then + Weak.set bucket !i (Some d) + else begin + let newsz = min (3 * sz / 2 + 3) (Sys.max_array_length - 1) in + if newsz <= sz then + failwith "Hashcons.Make: hash bucket cannot grow more"; + let newbucket = Weak.create newsz in + Weak.blit bucket 0 newbucket 0 sz; + Weak.set newbucket sz (Some d); + t.table.(index) <- newbucket; + t.totsize <- t.totsize + (newsz - sz); + if t.totsize > t.limit * Array.length t.table then resize t; + end + +let hashcons t d = + let hkey = Hashtbl.hash d land max_int in + let index = hkey mod (Array.length t.table) in + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let found = ref None in + let i = ref 0 in + while !i < sz && Option.is_none !found do + match Weak.get bucket !i with + | Some v as opt when v.hkey = hkey && v.node = d -> + found := opt + | _ -> incr i + done; + match !found with + | Some v -> v + | None -> + let hnode = { hkey = hkey; tag = gentag (); node = d } in + add t hnode; + hnode + +let stats t = + let len = Array.length t.table in + let lens = Array.map Weak.length t.table in + Array.sort compare lens; + let totlen = Array.fold_left ( + ) 0 lens in + (len, count t, totlen, lens.(0), lens.(len/2), lens.(len-1)) + + +(* Functorial interface *) + +module type HashedType = + sig + type t + val equal : t -> t -> bool + val hash : t -> int + end + +module type S = + sig + type key + type t + val create : int -> t + val clear : t -> unit + val hashcons : t -> key -> key hash_consed + val iter : (key hash_consed -> unit) -> t -> unit + val stats : t -> int * int * int * int * int * int + end + +module Make(H : HashedType) : (S with type key = H.t) = struct + + type key = H.t + + type data = H.t hash_consed + + type t = { + mutable table : data Weak.t array; + mutable totsize : int; (* sum of the bucket sizes *) + mutable limit : int; (* max ratio totsize/table length *) + } + + let emptybucket = Weak.create 0 + + let create sz = + let sz = if sz < 7 then 7 else sz in + let sz = if sz > Sys.max_array_length then Sys.max_array_length else sz in + { + table = Array.make sz emptybucket; + totsize = 0; + limit = 3; + } + + let clear t = + for i = 0 to Array.length t.table - 1 do + t.table.(i) <- emptybucket + done; + t.totsize <- 0; + t.limit <- 3 + + let iter f t = + let rec iter_bucket i b = + if i >= Weak.length b then () else + match Weak.get b i with + | Some v -> f v; iter_bucket (i+1) b + | None -> iter_bucket (i+1) b + in + Array.iter (iter_bucket 0) t.table + + let count t = + let rec count_bucket i b accu = + if i >= Weak.length b then accu else + count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0)) + in + Array.fold_right (count_bucket 0) t.table 0 + + let next_sz n = min (3*n/2 + 3) (Sys.max_array_length - 1) + + let rec resize t = + let oldlen = Array.length t.table in + let newlen = next_sz oldlen in + if newlen > oldlen then begin + let newt = create newlen in + newt.limit <- t.limit + 100; (* prevent resizing of newt *) + iter (fun d -> add newt d) t; + t.table <- newt.table; + t.totsize <- newt.totsize + end + + and add t d = + let index = d.hkey mod (Array.length t.table) in + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let i = ref 0 in + while !i < sz && Weak.check bucket !i do incr i done; + if !i < sz then + Weak.set bucket !i (Some d) + else begin + let newsz = min (3 * sz / 2 + 3) (Sys.max_array_length - 1) in + if newsz <= sz then + failwith "Hashcons.Make: hash bucket cannot grow more"; + let newbucket = Weak.create newsz in + Weak.blit bucket 0 newbucket 0 sz; + Weak.set newbucket sz (Some d); + t.table.(index) <- newbucket; + t.totsize <- t.totsize + (newsz - sz); + if t.totsize > t.limit * Array.length t.table then resize t; + end + + let hashcons t d = + let hkey = H.hash d land max_int in + let index = hkey mod (Array.length t.table) in + let bucket = t.table.(index) in + let sz = Weak.length bucket in + let found = ref None in + let i = ref 0 in + while !i < sz && Option.is_none !found do + match Weak.get bucket !i with + | Some v as opt when v.hkey = hkey && H.equal v.node d -> + found := opt + | _ -> incr i + done; + match !found with + | Some v -> v + | None -> + let hnode = { hkey = hkey; tag = gentag (); node = d } in + add t hnode; + hnode + + let stats t = + let len = Array.length t.table in + let lens = Array.map Weak.length t.table in + Array.sort compare lens; + let totlen = Array.fold_left ( + ) 0 lens in + (len, count t, totlen, lens.(0), lens.(len/2), lens.(len-1)) + +end + + +(*s When comparing branching bits, one has to be careful with the sign bit *) +let unsigned_lt n m = n >= 0 && (m < 0 || n < m) + +module Hmap = struct + + type 'a key = 'a hash_consed + + type ('a, 'b) t = + | Empty + | Leaf of 'a key * 'b + | Branch of int * int * ('a, 'b) t * ('a, 'b) t + + let empty = Empty + + let is_empty = function Empty -> true | _ -> false + + let zero_bit k m = (k land m) == 0 + + let rec mem k = function + | Empty -> false + | Leaf (j,_) -> k.tag == j.tag + | Branch (_, m, l, r) -> mem k (if zero_bit k.tag m then l else r) + + let rec find k = function + | Empty -> raise Not_found + | Leaf (j,x) -> if k.tag == j.tag then x else raise Not_found + | Branch (_, m, l, r) -> find k (if zero_bit k.tag m then l else r) + + let rec find_opt k = function + | Empty -> None + | Leaf (j,x) -> if k.tag == j.tag then Some x else None + | Branch (_, m, l, r) -> find_opt k (if zero_bit k.tag m then l else r) + + let singleton k v = Leaf(k,v) + + let lowest_bit x = x land (-x) + + let branching_bit p0 p1 = lowest_bit (p0 lxor p1) + + let mask p m = p land (m-1) + + let join (p0,t0,p1,t1) = + let m = branching_bit p0 p1 in + if zero_bit p0 m then + Branch (mask p0 m, m, t0, t1) + else + Branch (mask p0 m, m, t1, t0) + + let match_prefix k p m = (mask k m) == p + + let add k x t = + let rec ins = function + | Empty -> Leaf (k,x) + | Leaf (j,_) as t -> + if j.tag == k.tag then + Leaf (k,x) + else + join (k.tag, Leaf (k,x), j.tag, t) + | Branch (p,m,t0,t1) as t -> + if match_prefix k.tag p m then + if zero_bit k.tag m then + Branch (p, m, ins t0, t1) + else + Branch (p, m, t0, ins t1) + else + join (k.tag, Leaf (k,x), p, t) + in + ins t + + let branch = function + | (_,_,Empty,t) -> t + | (_,_,t,Empty) -> t + | (p,m,t0,t1) -> Branch (p,m,t0,t1) + + let remove k t = + let rec rmv = function + | Empty -> Empty + | Leaf (j,_) as t -> if k.tag == j.tag then Empty else t + | Branch (p,m,t0,t1) as t -> + if match_prefix k.tag p m then + if zero_bit k.tag m then + branch (p, m, rmv t0, t1) + else + branch (p, m, t0, rmv t1) + else + t + in + rmv t + + let rec update k f = function + | Empty -> (match f None with Some v -> Leaf(k,v) | None -> Empty) + | Leaf (j,x) as t -> + if k.tag == j.tag then match f (Some x) with + | None -> Empty + | Some x -> Leaf(j,x) + else (match f None with + | None -> t + | Some x -> join (k.tag, Leaf (k,x), j.tag, t)) + | Branch (p, m, t0, t1) as t -> + if match_prefix k.tag p m then + if zero_bit k.tag m then + branch (p, m, update k f t0, t1) + else + branch (p, m, t0, update k f t1) + else match f None with + | None -> t + | Some x -> join (k.tag, Leaf(k,x), p, t) + + let rec iter f = function + | Empty -> () + | Leaf (k,x) -> f k x + | Branch (_,_,t0,t1) -> iter f t0; iter f t1 + + let rec cardinal = function + | Empty -> 0 + | Leaf(_,_) -> 1 + | Branch(_,_,l,r) -> cardinal l + cardinal r + + let rec map f = function + | Empty -> Empty + | Leaf (k,x) -> Leaf (k, f x) + | Branch (p,m,t0,t1) -> Branch (p, m, map f t0, map f t1) + + let rec mapi f = function + | Empty -> Empty + | Leaf (k,x) -> Leaf (k, f k x) + | Branch (p,m,t0,t1) -> Branch (p, m, mapi f t0, mapi f t1) + + let rec fold f s accu = match s with + | Empty -> accu + | Leaf (k,x) -> f k x accu + | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu) + + let rec exists f = function + | Empty -> false + | Leaf (k,v) -> f k v + | Branch(_,_,l,r) -> exists f l || exists f r + + let rec for_all f = function + | Empty -> true + | Leaf (k,v) -> f k v + | Branch(_,_,l,r) -> for_all f l && for_all f r + + let rec filter f = function + | Empty -> Empty + | Leaf(k,v) as t -> if f k v then t else Empty + | Branch(p,m,t0,t1) -> branch(p, m, filter f t0, filter f t1) + + let rec filter_map f = function + | Empty -> Empty + | Leaf(k,v) -> (match f k v with Some v' -> Leaf(k,v') | None -> Empty) + | Branch(p,m,t0,t1) -> branch(p, m, filter_map f t0, filter_map f t1) + + let split k m = + fold + (fun k' v (lt, data, gt) -> + if k.tag = k'.tag then (lt, Some v, gt) + else if k.tag < k'.tag then (lt, data, add k' v gt) + else (add k' v lt, data, gt)) + m (empty, None, empty) + + let bindings s = + let rec bindings_aux acc = function + | Empty -> acc + | Leaf (k,v) -> (k,v) :: acc + | Branch (_,_,l,r) -> bindings_aux (bindings_aux acc l) r + in + bindings_aux [] s + + let to_seq s = + let rec to_seq_aux acc = function + | Empty -> acc + | Leaf (k,v) -> Seq.cons (k,v) acc + | Branch (_,_,l,r) -> to_seq_aux (to_seq_aux acc l) r + in + to_seq_aux Seq.empty s + + let partition f m = fold (fun k v (m_true, m_false) -> + if f k v then (add k v m_true, m_false) else (m_true, add k v m_false) + ) m (Empty,Empty) + + let rec choose = function + | Empty -> raise Not_found + | Leaf (k, v) -> (k, v) + | Branch (_, _, t0, _) -> choose t0 + + let rec choose_opt = function + | Empty -> None + | Leaf (k, v) -> Some (k, v) + | Branch (_, _, t0, _) -> choose_opt t0 + + let rec equal equal_v t1 t2 = match t1, t2 with + | Empty, Empty -> true + | Leaf (k1,v1), Leaf (k2,v2) -> k1.tag == k2.tag && equal_v v1 v2 + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + p1 = p2 && m1 = m2 && equal equal_v l1 l2 && equal equal_v r1 r2 + | _ -> false + + let rec compare compare_v t1 t2 = match t1,t2 with + | Empty, Empty -> 0 + | Empty, _ -> -1 + | _, Empty -> 1 + | Leaf (k1,v1), Leaf (k2,v2) -> + let cmp = Int.compare k1.tag k2.tag in + if cmp = 0 then compare_v v1 v2 else cmp + | Leaf _, Branch _ -> -1 + | Branch _, Leaf _ -> 1 + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + let cmp = Int.compare p1 p2 in + if cmp <> 0 then cmp else + let cmp = Int.compare m1 m2 in + if cmp <> 0 then cmp else + let cmp = compare compare_v l1 l2 in + if cmp <> 0 then cmp else + compare compare_v r1 r2 + + let merge f l r = + let merge_l t = filter_map (fun k v -> f k (Some v) None) t in + let merge_r t = filter_map (fun k v -> f k None (Some v)) t in + let rec merge_aux l r = match l, r with + | Empty, t -> merge_r t + | t, Empty -> merge_l t + | Leaf (k,v1), t -> + filter_map ( + fun k' v -> f k' (if k.tag = k'.tag then (Some v1) else None) (Some v) + ) t + | t, Leaf (k,v2) -> + filter_map ( + fun k' v -> f k' (Some v) (if k.tag = k'.tag then (Some v2) else None) + ) t + | (Branch (p,m,l0,l1) as l), (Branch (q,n,r0,r1) as r) -> + if m = n && match_prefix q p m + then branch (p, m, merge_aux l0 r0, merge_aux l1 r1) + else if unsigned_lt m n && match_prefix q p m then + (* [q] contains [p]. Merge [t] with a subtree of [s]. *) + if zero_bit q m + then branch (p, m, merge_aux l0 r, merge_l l1) + else branch (p, m, merge_l l0, merge_aux l1 r) + else if unsigned_lt n m && match_prefix p q n then + (* [p] contains [q]. Merge [s] with a subtree of [t]. *) + if zero_bit p n + then branch (q, n, merge_aux l r0, merge_r r1) + else branch (q, n, merge_r r0, merge_aux l r1) + else + (* The prefixes disagree, so the trees are disjoint. *) + join (p, merge_l l, q, merge_r r) + in merge_aux l r + + let rec union f l r = match l, r with + | Empty, t + | t, Empty -> t + | Leaf (k,v1), t -> + update k (function None -> Some v1 | Some v2 -> f k v1 v2) t + | t, Leaf (k,v2) -> + update k (function None -> Some v2 | Some v1 -> f k v1 v2) t + | (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) -> + if m = n && match_prefix q p m + then branch (p, m, union f s0 t0, union f s1 t1) + else if unsigned_lt m n && match_prefix q p m then + (* [q] contains [p]. Merge [t] with a subtree of [s]. *) + if zero_bit q m + then branch (p, m, union f s0 t, s1) + else branch (p, m, s0, union f s1 t) + else if unsigned_lt n m && match_prefix p q n then + (* [p] contains [q]. Merge [s] with a subtree of [t]. *) + if zero_bit p n + then branch (q, n, union f s t0, t1) + else branch (q, n, t0, union f s t1) + else + (* The prefixes disagree. *) + join (p, s, q, t) + + let min_binding_opt m = + fold + (fun k v b -> + match b with + | None -> Some (k, v) + | Some (k', _) -> if k'.tag <= k.tag then b else Some (k, v)) + m None + + let min_binding m = match min_binding_opt m with + | Some x -> x + | None -> raise Not_found + + let max_binding_opt m = + fold + (fun k v b -> + match b with + | None -> Some (k, v) + | Some (k', _) -> if k'.tag >= k.tag then b else Some (k, v)) + m None + + let max_binding m = match max_binding_opt m with + | Some x -> x + | None -> raise Not_found + + let find_first_opt f m = + fold + (fun k v acc -> + match acc with + | None -> if f k then Some (k, v) else None + | Some (k', _) -> + if k'.tag <= k.tag then acc else + if f k then Some (k, v) else acc) + m None + + let find_first f m = match find_first_opt f m with + | Some x -> x + | None -> raise Not_found + + let find_last_opt f m = + fold + (fun k v acc -> + match acc with + | None -> if f k then Some (k, v) else None + | Some (k', _) -> + if k'.tag >= k.tag then acc else + if f k then Some (k, v) else acc) + m None + + let find_last f m = match find_last_opt f m with + | Some x -> x + | None -> raise Not_found + + let add_seq seq m = Seq.fold_left (fun m (k, v) -> add k v m) m seq + let of_seq s = add_seq s Empty + + (*s Extra functions not in [Map.S] *) + + let find_any (type a b) f (m : (a, b) t) = + let exception Found of (a key * b) in + try + iter (fun k v -> if f k v then raise (Found (k, v))) m; + raise Not_found + with Found x -> x + let find_any_opt (type a b) f (m : (a, b) t) = + let exception Found of (a key * b) in + try + iter (fun k v -> if f k v then raise (Found (k, v))) m; + None + with Found x -> Some x + + let is_singleton = function + | Leaf(k,v) -> Some (k,v) + | _ -> None +end + +module Hset = struct + (*s Sets of integers implemented as Patricia trees, following Chris + Okasaki and Andrew Gill's paper {\em Fast Mergeable Integer Maps} + ({\tt\small http://www.cs.columbia.edu/\~{}cdo/papers.html\#ml98maps}). + Patricia trees provide faster operations than standard library's + module [Set], and especially very fast [union], [subset], [inter] + and [diff] operations. *) + + (*s The idea behind Patricia trees is to build a {\em trie} on the + binary digits of the elements, and to compact the representation + by branching only one the relevant bits (i.e. the ones for which + there is at least on element in each subtree). We implement here + {\em little-endian} Patricia trees: bits are processed from + least-significant to most-significant. The trie is implemented by + the following type [t]. [Empty] stands for the empty trie, and + [Leaf k] for the singleton [k]. (Note that [k] is the actual + element.) [Branch (m,p,l,r)] represents a branching, where [p] is + the prefix (from the root of the trie) and [m] is the branching + bit (a power of 2). [l] and [r] contain the subsets for which the + branching bit is respectively 0 and 1. Invariant: the trees [l] + and [r] are not empty. *) + + (*i*) + type 'a elt = 'a hash_consed + (*i*) + + type 'a t = + | Empty + | Leaf of 'a hash_consed + | Branch of int * int * 'a t * 'a t + + (*s Example: the representation of the set $\{1,4,5\}$ is + $$\mathtt{Branch~(0,~1,~Leaf~4,~Branch~(1,~4,~Leaf~1,~Leaf~5))}$$ + The first branching bit is the bit 0 (and the corresponding prefix + is [0b0], not of use here), with $\{4\}$ on the left and $\{1,5\}$ on the + right. Then the right subtree branches on bit 2 (and so has a branching + value of $2^2 = 4$), with prefix [0b01 = 1]. *) + + (*s Empty set and singletons. *) + + let empty = Empty + + let is_empty = function Empty -> true | _ -> false + + let singleton k = Leaf k + + (*s Testing the occurrence of a value is similar to the search in a + binary search tree, where the branching bit is used to select the + appropriate subtree. *) + + let zero_bit k m = (k land m) == 0 + + let rec mem k = function + | Empty -> false + | Leaf j -> k.tag == j.tag + | Branch (_, m, l, r) -> mem k (if zero_bit k.tag m then l else r) + + let find k s = if mem k s then k else raise Not_found + let find_opt k s = if mem k s then Some k else None + + (*s The following operation [join] will be used in both insertion and + union. Given two non-empty trees [t0] and [t1] with longest common + prefixes [p0] and [p1] respectively, which are supposed to + disagree, it creates the union of [t0] and [t1]. For this, it + computes the first bit [m] where [p0] and [p1] disagree and create + a branching node on that bit. Depending on the value of that bit + in [p0], [t0] will be the left subtree and [t1] the right one, or + the converse. Computing the first branching bit of [p0] and [p1] + uses a nice property of twos-complement representation of integers. *) + + let lowest_bit x = x land (-x) + + let branching_bit p0 p1 = lowest_bit (p0 lxor p1) + + let mask p m = p land (m-1) + + let join (p0,t0,p1,t1) = + let m = branching_bit p0 p1 in + if zero_bit p0 m then + Branch (mask p0 m, m, t0, t1) + else + Branch (mask p0 m, m, t1, t0) + + (*s Then the insertion of value [k] in set [t] is easily implemented + using [join]. Insertion in a singleton is just the identity or a + call to [join], depending on the value of [k]. When inserting in + a branching tree, we first check if the value to insert [k] + matches the prefix [p]: if not, [join] will take care of creating + the above branching; if so, we just insert [k] in the appropriate + subtree, depending of the branching bit. *) + + let match_prefix k p m = (mask k m) == p + + let add k t = + let rec ins = function + | Empty -> Leaf k + | Leaf j as t -> + if j.tag == k.tag then t else join (k.tag, Leaf k, j.tag, t) + | Branch (p,m,t0,t1) as t -> + if match_prefix k.tag p m then + if zero_bit k.tag m then + Branch (p, m, ins t0, t1) + else + Branch (p, m, t0, ins t1) + else + join (k.tag, Leaf k, p, t) + in + ins t + + (*s The code to remove an element is basically similar to the code of + insertion. But since we have to maintain the invariant that both + subtrees of a [Branch] node are non-empty, we use here the + ``smart constructor'' [branch] instead of [Branch]. *) + + let branch = function + | (_,_,Empty,t) -> t + | (_,_,t,Empty) -> t + | (p,m,t0,t1) -> Branch (p,m,t0,t1) + + let remove k t = + let rec rmv = function + | Empty -> Empty + | Leaf j as t -> if k.tag == j.tag then Empty else t + | Branch (p,m,t0,t1) as t -> + if match_prefix k.tag p m then + if zero_bit k.tag m then + branch (p, m, rmv t0, t1) + else + branch (p, m, t0, rmv t1) + else + t + in + rmv t + + (*s One nice property of Patricia trees is to support a fast union + operation (and also fast subset, difference and intersection + operations). When merging two branching trees we examine the + following four cases: (1) the trees have exactly the same + prefix; (2/3) one prefix contains the other one; and (4) the + prefixes disagree. In cases (1), (2) and (3) the recursion is + immediate; in case (4) the function [join] creates the appropriate + branching. *) + + let rec merge = function + | Empty, t -> t + | t, Empty -> t + | Leaf k, t -> add k t + | t, Leaf k -> add k t + | (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) -> + if m == n && match_prefix q p m then + (* The trees have the same prefix. Merge the subtrees. *) + Branch (p, m, merge (s0,t0), merge (s1,t1)) + else if unsigned_lt m n && match_prefix q p m then + (* [q] contains [p]. Merge [t] with a subtree of [s]. *) + if zero_bit q m then + Branch (p, m, merge (s0,t), s1) + else + Branch (p, m, s0, merge (s1,t)) + else if unsigned_lt n m && match_prefix p q n then + (* [p] contains [q]. Merge [s] with a subtree of [t]. *) + if zero_bit p n then + Branch (q, n, merge (s,t0), t1) + else + Branch (q, n, t0, merge (s,t1)) + else + (* The prefixes disagree. *) + join (p, s, q, t) + + let union s t = merge (s,t) + + (*s When checking if [s1] is a subset of [s2] only two of the above + four cases are relevant: when the prefixes are the same and when the + prefix of [s1] contains the one of [s2], and then the recursion is + obvious. In the other two cases, the result is [false]. *) + + let rec subset s1 s2 = match (s1,s2) with + | Empty, _ -> true + | _, Empty -> false + | Leaf k1, _ -> mem k1 s2 + | Branch _, Leaf _ -> false + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + if m1 == m2 && p1 == p2 then + subset l1 l2 && subset r1 r2 + else if unsigned_lt m2 m1 && match_prefix p1 p2 m2 then + if zero_bit p1 m2 then + subset l1 l2 && subset r1 l2 + else + subset l1 r2 && subset r1 r2 + else + false + + (*s To compute the intersection and the difference of two sets, we + still examine the same four cases as in [merge]. The recursion is + then obvious. *) + + let rec inter s1 s2 = match (s1,s2) with + | Empty, _ -> Empty + | _, Empty -> Empty + | Leaf k1, _ -> if mem k1 s2 then s1 else Empty + | _, Leaf k2 -> if mem k2 s1 then s2 else Empty + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + if m1 == m2 && p1 == p2 then + merge (inter l1 l2, inter r1 r2) + else if unsigned_lt m1 m2 && match_prefix p2 p1 m1 then + inter (if zero_bit p2 m1 then l1 else r1) s2 + else if unsigned_lt m2 m1 && match_prefix p1 p2 m2 then + inter s1 (if zero_bit p1 m2 then l2 else r2) + else + Empty + + let rec diff s1 s2 = match (s1,s2) with + | Empty, _ -> Empty + | _, Empty -> s1 + | Leaf k1, _ -> if mem k1 s2 then Empty else s1 + | _, Leaf k2 -> remove k2 s1 + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + if m1 == m2 && p1 == p2 then + merge (diff l1 l2, diff r1 r2) + else if unsigned_lt m1 m2 && match_prefix p2 p1 m1 then + if zero_bit p2 m1 then + merge (diff l1 s2, r1) + else + merge (l1, diff r1 s2) + else if unsigned_lt m2 m1 && match_prefix p1 p2 m2 then + if zero_bit p1 m2 then diff s1 l2 else diff s1 r2 + else + s1 + + (*s All the following operations ([cardinal], [iter], [fold], [for_all], + [exists], [filter], [partition], [choose], [choose_opt], [elements], + [to_seq]) are implemented as for any other kind of binary trees. *) + + let rec cardinal = function + | Empty -> 0 + | Leaf _ -> 1 + | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1 + + let rec iter f = function + | Empty -> () + | Leaf k -> f k + | Branch (_,_,t0,t1) -> iter f t0; iter f t1 + + let rec fold f s accu = match s with + | Empty -> accu + | Leaf k -> f k accu + | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu) + + let rec for_all p = function + | Empty -> true + | Leaf k -> p k + | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1 + + let rec exists p = function + | Empty -> false + | Leaf k -> p k + | Branch (_,_,t0,t1) -> exists p t0 || exists p t1 + + let rec filter pr = function + | Empty -> Empty + | Leaf k as t -> if pr k then t else Empty + | Branch (p,m,t0,t1) -> branch (p, m, filter pr t0, filter pr t1) + + let partition p s = + let rec part (t,f as acc) = function + | Empty -> acc + | Leaf k -> if p k then (add k t, f) else (t, add k f) + | Branch (_,_,t0,t1) -> part (part acc t0) t1 + in + part (Empty, Empty) s + + let rec choose = function + | Empty -> raise Not_found + | Leaf k -> k + | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *) + + let rec choose_opt = function + | Empty -> None + | Leaf k -> Some k + | Branch (_, _,t0,_) -> choose_opt t0 (* we know that [t0] is non-empty *) + + let elements s = + let rec elements_aux acc = function + | Empty -> acc + | Leaf k -> k :: acc + | Branch (_,_,l,r) -> elements_aux (elements_aux acc l) r + in + elements_aux [] s + + let to_seq s = + let rec to_seq_aux acc = function + | Empty -> acc + | Leaf k -> Seq.cons k acc + | Branch (_,_,l,r) -> to_seq_aux (to_seq_aux acc r) l + in + to_seq_aux Seq.empty s + + let split elt s = + fold (fun elt' (lt, present, gt) -> + if elt'.tag < elt.tag then (add elt' lt, present, gt) else + if elt'.tag > elt.tag then (lt, present, add elt' gt) else + (lt, true, gt) + ) s (Empty, false, Empty) + + (*s [map] and [filter_map] are implemented via [fold] and [add] + since we can't relate the tag of [f elt] to that of [elt] *) + let map f s = fold (fun elt s -> add (f elt) s) s Empty + let filter_map f s = fold (fun elt s -> + match f elt with + | None -> s + | Some elt' -> add elt' s) + s Empty + + let add_seq seq s = Seq.fold_left (fun s elt -> add elt s) s seq + + let of_seq seq = add_seq seq Empty + + let of_list list = List.fold_left (fun s elt -> add elt s) Empty list + + (*s There is no way to give an efficient implementation of [min_elt] + and [max_elt], as with binary search trees. The following + implementation is a traversal of all elements, barely more + efficient than [fold min t (choose t)] (resp. [fold max t (choose + t)]). Note that we use the fact that there is no constructor + [Empty] under [Branch] and therefore always a minimal + (resp. maximal) element there. *) + + let rec min_elt = function + | Empty -> raise Not_found + | Leaf k -> k + | Branch (_,_,s,t) -> min (min_elt s) (min_elt t) + + let min_elt_opt = function + | Empty -> None + | x -> Some (min_elt x) + + let rec max_elt = function + | Empty -> raise Not_found + | Leaf k -> k + | Branch (_,_,s,t) -> max (max_elt s) (max_elt t) + + let max_elt_opt = function + | Empty -> None + | x -> Some (max_elt x) + + (*s [find_first], [find_last] and their opt versions are less efficient + then with binary search trees. They are linear time and can call [f] an + arbitrary number of times, and not necessarily on elements smaller/larger + than the witness. *) + let find_first_opt f s = + fold + (fun elt acc -> + match acc with + | None -> if f elt then Some elt else None + | Some witness -> + if witness.tag <= elt.tag then acc else + if f elt then Some elt else acc) + s None + + let find_first f s = + match find_first_opt f s with + | Some elt -> elt + | None -> raise Not_found + + let find_last_opt f s = + fold + (fun elt acc -> + match acc with + | None -> if f elt then Some elt else None + | Some witness -> + if witness.tag >= elt.tag then acc else + if f elt then Some elt else acc) + s None + + let find_last f s = + match find_last_opt f s with + | Some elt -> elt + | None -> raise Not_found + + (*s Another nice property of Patricia trees is to be independent of the + order of insertion. As a consequence, two Patricia trees have the + same elements if and only if they are structurally equal. + + We could use OCaml's [=] and [compare] for this, but it's faster + to reimplement them as we have a faster comparison on elements (comparing + tags), where the standard comparisons will inspect the elements in depth. + *) + + let rec equal l r = match (l, r) with + | Empty, Empty -> true + | Leaf l, Leaf r -> l.tag == r.tag + | Branch (ai, aj, al, ar), Branch (bi, bj, bl, br) -> + ai == bi && aj == bj && equal al bl && equal ar br + | _ -> false + + + let rec compare l r = match (l, r) with + | Empty, Empty -> 0 + | Empty, _ -> -1 + | _, Empty -> 1 + | Leaf l, Leaf r -> Int.compare l.tag r.tag + | Leaf _, _ -> -1 + | _, Leaf _ -> 1 + | Branch (ai, aj, al, ar), Branch (bi, bj, bl, br) -> + let cmp = Int.compare ai bi in + if cmp <> 0 then cmp else + let cmp = Int.compare aj bj in + if cmp <> 0 then cmp else + let cmp = compare al bl in + if cmp <> 0 then cmp else + compare ar br + + (*i*) + let _make l = List.fold_right add l empty + (*i*) + + (*s Additional functions w.r.t to [Set.S]. *) + + let rec intersect s1 s2 = match (s1,s2) with + | Empty, _ -> false + | _, Empty -> false + | Leaf k1, _ -> mem k1 s2 + | _, Leaf k2 -> mem k2 s1 + | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) -> + if m1 == m2 && p1 == p2 then + intersect l1 l2 || intersect r1 r2 + else if unsigned_lt m1 m2 && match_prefix p2 p1 m1 then + intersect (if zero_bit p2 m1 then l1 else r1) s2 + else if unsigned_lt m2 m1 && match_prefix p1 p2 m2 then + intersect s1 (if zero_bit p1 m2 then l2 else r2) + else + false + + let disjoint s1 s2 = not (intersect s1 s2) + + let find_any (type a) f (s : a t) = + let exception Found of a elt in + try + iter (fun elt -> if f elt then raise (Found elt)) s; + raise Not_found + with Found elt -> elt + let find_any_opt (type a) f (s : a t) = + let exception Found of a elt in + try + iter (fun elt -> if f elt then raise (Found elt)) s; + None + with Found elt -> Some elt + + let bind f s = fold (fun elt s -> union (f elt) s) s empty + + let is_singleton = function + | Leaf elt -> Some elt + | _ -> None + +end diff --git a/simple/hashcons/hashcons.mli b/simple/hashcons/hashcons.mli new file mode 100644 index 0000000..f9f6ae4 --- /dev/null +++ b/simple/hashcons/hashcons.mli @@ -0,0 +1,227 @@ +(**************************************************************************) +(* *) +(* Copyright (C) Jean-Christophe Filliatre *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + +(*s Hash tables for hash consing. + + The technique is described in this paper: + Sylvain Conchon and Jean-Christophe Filliâtre. + Type-Safe Modular Hash-Consing. + In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. + https://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf + + Note: a different, more elaborated hash-consing library + can be found in Why3 sources at http://why3.lri.fr/ + + Hash consed values are of the + following type [hash_consed]. The field [tag] contains a unique + integer (for values hash consed with the same table). The field + [hkey] contains the hash key of the value (without modulo) for + possible use in other hash tables (and internally when hash + consing tables are resized). The field [node] contains the value + itself. + + Hash consing tables are using weak pointers, so that values that are no + more referenced from anywhere else can be erased by the GC. *) + +type +'a hash_consed = private { + hkey: int; + tag : int; + node: 'a; +} + +(*s Generic part, using ocaml generic equality and hash function. *) + +type 'a t + +val create : int -> 'a t + (** [create n] creates an empty table of initial size [n]. The table + will grow as needed. *) + +val clear : 'a t -> unit + (** Removes all elements from the table. *) + +val hashcons : 'a t -> 'a -> 'a hash_consed + (** [hashcons t n] hash-cons the value [n] using table [t] i.e. returns + any existing value in [t] equal to [n], if any; otherwise, allocates + a new one hash-consed value of node [n] and returns it. + As a consequence the returned value is physically equal to + any equal value already hash-consed using table [t]. *) + +val iter : ('a hash_consed -> unit) -> 'a t -> unit + (** [iter f t] iterates [f] over all elements of [t]. *) + +val stats : 'a t -> int * int * int * int * int * int + (** Return statistics on the table. The numbers are, in order: + table length, number of entries, sum of bucket lengths, + smallest bucket length, median bucket length, biggest bucket length. *) + +(*s Functorial interface. *) + +module type HashedType = + sig + type t + val equal : t -> t -> bool + val hash : t -> int + end + +module type S = + sig + type key + type t + val create : int -> t + val clear : t -> unit + val hashcons : t -> key -> key hash_consed + val iter : (key hash_consed -> unit) -> t -> unit + val stats : t -> int * int * int * int * int * int + end + +module Make(H : HashedType) : (S with type key = H.t) + + +module Hmap : sig + type (+'a, +!'b) t + type 'a key = 'a hash_consed + + val empty : ('a, 'b) t + val is_empty : ('a, 'b) t -> bool + val singleton : 'a key -> 'b -> ('a, 'b) t + val add : 'a key -> 'b -> ('a, 'b) t -> ('a, 'b) t + val find : 'a key -> ('a, 'b) t -> 'b + val find_opt : 'a key -> ('a, 'b) t -> 'b option + val update : 'a key -> ('b option -> 'b option) -> ('a, 'b) t -> ('a, 'b) t + val cardinal : ('a, 'b) t -> int + val remove : 'a key -> ('a, 'b) t -> ('a, 'b) t + val mem : 'a key -> ('a, 'b) t -> bool + val add_seq : ('a key * 'b) Seq.t -> ('a, 'b) t -> ('a, 'b) t + val of_seq : ('a key * 'b) Seq.t -> ('a, 'b) t + val partition : ('a key -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t * ('a, 'b) t + val choose : ('a, 'b) t -> 'a key * 'b + val choose_opt : ('a, 'b) t -> ('a key * 'b) option + val split : 'a key -> ('a, 'b) t -> ('a, 'b) t * 'b option * ('a, 'b) t + val equal : ('b -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t -> bool + val compare : ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int + val merge : + ('a key -> 'b option -> 'c option -> 'd option) -> + ('a, 'b) t -> ('a, 'c) t -> ('a, 'd) t + val union : + ('a key -> 'b -> 'b -> 'b option) -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t + + (*s Warning: iterators do not iterate following key order *) + val iter : ('a key -> 'b -> unit) -> ('a, 'b) t -> unit + val map : ('b -> 'c) -> ('a, 'b) t -> ('a, 'c) t + val mapi : ('a key -> 'b -> 'c) -> ('a, 'b) t -> ('a, 'c) t + val fold : ('a key -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c + val exists : ('a key -> 'b -> bool) -> ('a, 'b) t -> bool + val for_all : ('a key -> 'b -> bool) -> ('a, 'b) t -> bool + val filter : ('a key -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t + val filter_map : ('a key -> 'b -> 'c option) -> ('a, 'b) t -> ('a, 'c) t + + (*s Warning: not sorted *) + val bindings : ('a, 'b) t -> ('a key * 'b) list + val to_seq : ('a, 'b) t -> ('a key * 'b) Seq.t + + (*s Warning: these are linear time w.r.t. the size of the map. *) + val min_binding_opt : ('a, 'b) t -> ('a key * 'b) option + val max_binding_opt : ('a, 'b) t -> ('a key * 'b) option + val min_binding : ('a, 'b) t -> 'a key * 'b + val max_binding : ('a, 'b) t -> 'a key * 'b + + (*s Warning: these are linear time w.r.t. the size of the map and can + call the function on terms greater/smaller than the witness *) + val find_first_opt : ('a key -> bool) -> ('a, 'b) t -> ('a key * 'b) option + val find_last_opt : ('a key -> bool) -> ('a, 'b) t -> ('a key * 'b) option + val find_first : ('a key -> bool) -> ('a, 'b) t -> 'a key * 'b + val find_last : ('a key -> bool) -> ('a, 'b) t -> 'a key * 'b + + (*s Extra functions not in [Map.S], a slightly faster find *) + val find_any : ('a key -> 'b -> bool) -> ('a, 'b) t -> 'a key * 'b + val find_any_opt : ('a key -> 'b -> bool) -> ('a, 'b) t -> ('a key * 'b) option + + val is_singleton : ('a, 'b) t -> ('a key * 'b) option + (** if the map is a singleton, return the unique binding, + else return [None] *) +end + +module Hset : sig + type 'a t + type 'a elt = 'a hash_consed + val empty : 'a t + val is_empty : 'a t -> bool + val mem : 'a elt -> 'a t -> bool + val add : 'a elt -> 'a t -> 'a t + val singleton : 'a elt -> 'a t + val remove : 'a elt -> 'a t -> 'a t + val union : 'a t -> 'a t -> 'a t + val subset : 'a t -> 'a t -> bool + val inter : 'a t -> 'a t -> 'a t + val diff : 'a t -> 'a t -> 'a t + val equal : 'a t -> 'a t -> bool + val compare : 'a t -> 'a t -> int + val choose : 'a t -> 'a elt + val choose_opt : 'a t -> 'a elt option + val cardinal : 'a t -> int + val for_all : ('a elt -> bool) -> 'a t -> bool + val exists : ('a elt -> bool) -> 'a t -> bool + val partition : ('a elt -> bool) -> 'a t -> 'a t * 'a t + val disjoint : 'a t -> 'a t -> bool + val find : 'a elt -> 'a t -> 'a elt + val find_opt : 'a elt -> 'a t -> 'a elt option + val add_seq : 'a elt Seq.t -> 'a t -> 'a t + val of_seq : 'a elt Seq.t -> 'a t + val of_list : 'a elt list -> 'a t + val split : 'a elt -> 'a t -> 'a t * bool * 'a t + + (*s Warning: [iter], [fold], [map], [filter] and [map_filter] do NOT iterate + over element order. Similarly, [elements] and [to_seq] are not sorted. *) + val iter : ('a elt -> unit) -> 'a t -> unit + val fold : ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b + val map : ('a elt -> 'b elt) -> 'a t -> 'b t + val filter : ('a elt -> bool) -> 'a t -> 'a t + val filter_map : ('a elt -> 'b elt option) -> 'a t -> 'b t + val elements : 'a t -> 'a elt list + val to_seq : 'a t -> 'a elt Seq.t + + (*s Warning: [min_elt], [max_elt] and the [_opt] versions are linear w.r.t. + the size of the set. In other words, [min_elt t] is barely more efficient + than [fold min t (choose t)]. *) + val min_elt : 'a t -> 'a elt + val min_elt_opt : 'a t -> 'a elt option + val max_elt : 'a t -> 'a elt + val max_elt_opt : 'a t -> 'a elt option + + (*s [find_first], [find_last] are linear time and can call [f] an arbitrary + number of times, and not necessarily on elements smaller/larger + than the witness. *) + val find_first : ('a elt -> bool) -> 'a t -> 'a elt + val find_first_opt : ('a elt -> bool) -> 'a t -> 'a elt option + val find_last : ('a elt -> bool) -> 'a t -> 'a elt + val find_last_opt : ('a elt -> bool) -> 'a t -> 'a elt option + + (*s Additional functions not appearing in the signature [Set.S] from ocaml + standard library. *) + + (* [intersect u v] determines if sets [u] and [v] have a non-empty + intersection. *) + val intersect : 'a t -> 'a t -> bool + + (* Faster finds when order doesn't matter *) + val find_any : ('a elt -> bool) -> 'a t -> 'a elt + val find_any_opt : ('a elt -> bool) -> 'a t -> 'a elt option + + val is_singleton : 'a t -> 'a elt option + (* Check if the set is a singleton, if so return unique element *) + + val bind : ('a elt -> 'b t) -> 'a t -> 'b t +end diff --git a/simple/hashcons/quicksort.term b/simple/hashcons/quicksort.term new file mode 100644 index 0000000000000000000000000000000000000000..cbcde11cc92857f0f26dc9b6e9e13f05d0ccf22e GIT binary patch literal 395 zcmZut!4bnC45OJM<3PB~)CKzP*^eyXN5<%Em25~z8#p){%aY7%+dnBio;Y(#)0@Xk z)g+rq!Oqu&H58?&dI_0g;jK!+y|4v|kpdWI9Z~Sy5V8!I92m4vGVlm9$wH<{0bsI{ zB_thjOAj+YM0D4jjy@`2%_@fKA)7fA4Ke5lcNIi`25En^#rXUZOmhf<-T9B{{GY$~ C0KmKe literal 0 HcmV?d00001