simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-14 06:46:16 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Removed unused modules

Browse source
This commit is contained in:
Guillaume Bury 2016-07-07 14:55:48 +02:00
parent 6e6503e793
commit 599a59dda9
4 changed files with 0 additions and 375 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

97
util/hashcons.ml
View file

@ -1,97 +0,0 @@
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* 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.) *)
module type HashedType =
sig
type t
val equal : t -> t -> bool
val hash : t -> int
val tag : int -> t -> t
end
module type S =
sig
type t
val hashcons : t -> t
val iter : (t -> unit) -> unit
val stats : unit -> int * int * int * int * int * int
end
module Make(H : HashedType) : (S with type t = H.t) =
struct
type t = H.t
module WH = Weak.Make (H)
let next_tag = ref 0
let htable = WH.create 5003
let hashcons d =
let d = H.tag !next_tag d in
let o = WH.merge htable d in
if o == d then incr next_tag;
o
let iter f = WH.iter f htable
let stats () = WH.stats htable
end
let combine acc n = n * 65599 + acc
let combine2 acc n1 n2 = combine acc (combine n1 n2)
let combine3 acc n1 n2 n3 = combine acc (combine n1 (combine n2 n3))
let combine_list f = List.fold_left (fun acc x -> combine acc (f x))
let combine_option h = function None -> 0 | Some s -> (h s) + 1
let combine_pair h1 h2 (a1,a2) = combine (h1 a1) (h2 a2)
type 'a hash_consed = {
tag : int;
node : 'a }
module type HashedType_consed =
sig
type t
val equal : t -> t -> bool
val hash : t -> int
end
module type S_consed =
sig
type key
val hashcons : key -> key hash_consed
val iter : (key hash_consed -> unit) -> unit
val stats : unit -> int * int * int * int * int * int
end
module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) =
struct
module M = Make(struct
type t = H.t hash_consed
let hash x = H.hash x.node
let equal x y = H.equal x.node y.node
let tag i x = {x with tag = i}
end)
include M
type key = H.t
let hashcons x = M.hashcons {tag = -1; node = x}
end

109
util/hashcons.mli
View file

@ -1,109 +0,0 @@
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(** Hash tables for hash consing *)
(*s Hash tables for hash consing.
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. *)
module type HashedType =
sig
type t
val equal : t -> t -> bool
val hash : t -> int
val tag : int -> t -> t
end
module type S =
sig
type t
val hashcons : t -> t
(** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns
any existing value in the table equal to [n], if any;
otherwise, creates a new value with function [f], stores it
in the table and returns it. Function [f] is passed
the node [n] as first argument and the unique id as second argument.
*)
val iter : (t -> unit) -> unit
(** [iter f] iterates [f] over all elements of the table . *)
val stats : unit -> 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. *)
end
module Make(H : HashedType) : (S with type t = H.t)
(* helpers *)
val combine : int -> int -> int
val combine2 : int -> int -> int -> int
val combine3 : int -> int -> int -> int -> int
val combine_list : ('a -> int) -> int -> 'a list -> int
val combine_option : ('a -> int) -> 'a option -> int
val combine_pair : ('a -> int) -> ('b -> int) -> 'a * 'b -> int
(* For simple use *)
type 'a hash_consed = private {
tag : int;
node : 'a }
module type HashedType_consed =
sig
type t
val equal : t -> t -> bool
val hash : t -> int
end
module type S_consed =
sig
type key
val hashcons : key -> key hash_consed
(** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns
any existing value in the table equal to [n], if any;
otherwise, creates a new value with function [f], stores it
in the table and returns it. Function [f] is passed
the node [n] as first argument and the unique id as second argument.
*)
val iter : (key hash_consed -> unit) -> unit
(** [iter f] iterates [f] over all elements of the table . *)
val stats : unit -> 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. *)
end
module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t)

91
util/hstring.ml
View file

@ -1,91 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Hashcons
module S =
Hashcons.Make_consed(struct include String
let hash = Hashtbl.hash
let equal = (=) end)
module HS = struct
type t = string Hashcons.hash_consed
let make s = S.hashcons s
let view s = s.node
let equal s1 s2 = s1.tag = s2.tag
let compare s1 s2 = compare s1.tag s2.tag
let hash s = s.tag
let empty = make ""
let rec list_assoc x = function
| [] -> raise Not_found
| (y, v) :: l -> if equal x y then v else list_assoc x l
let rec list_mem_assoc x = function
| [] -> false
| (y, _) :: l -> compare x y = 0 || list_mem_assoc x l
let rec list_mem x = function
| [] -> false
| y :: l -> compare x y = 0 || list_mem x l
let compare_couple (x1,y1) (x2,y2) =
let c = compare x1 x2 in
if c <> 0 then c
else compare y1 y2
let rec compare_list l1 l2 =
match l1, l2 with
| [], [] -> 0
| [], _ -> -1
| _, [] -> 1
| x::r1, y::r2 ->
let c = compare x y in
if c <> 0 then c
else compare_list r1 r2
let rec list_mem_couple c = function
| [] -> false
| d :: l -> compare_couple c d = 0 || list_mem_couple c l
let print fmt s =
Format.fprintf fmt "%s" (view s)
end
include HS
module H = Hashtbl.Make(HS)
module HSet = Set.Make(HS)
module HMap = Map.Make(HS)
(* struct *)
(* include Hashtbl.Make(HS) *)
(* let find x h = *)
(* TimeHS.start (); *)
(* try *)
(* let r = find x h in *)
(* TimeHS.pause (); *)
(* r *)
(* with Not_found -> TimeHS.pause (); raise Not_found *)
(* end *)

78
util/hstring.mli
View file

@ -1,78 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(** {b Hash-consed strings}
Hash-consing is a technique to share values that are structurally
equal. More details on
{{:http://en.wikipedia.org/wiki/Hash_consing} Wikipedia} and
{{:http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf} here}.
This module provides an easy way to use hash-consing for strings.
*)
open Hashcons
type t = string hash_consed
(** The type of Hash-consed string *)
val make : string -> t
(** [make s] builds ans returns a hash-consed string from [s].*)
val view : t -> string
(** [view hs] returns the string corresponding to [hs].*)
val equal : t -> t -> bool
(** [equal x y] returns [true] if [x] and [y] are the same hash-consed string
(constant time).*)
val compare : t -> t -> int
(** [compares x y] returns [0] if [x] and [y] are equal, and is unspecified
otherwise but provides a total ordering on hash-consed strings.*)
val hash : t -> int
(** [hash x] returns the integer (hash) associated to [x].*)
val empty : t
(** the empty ([""]) hash-consed string.*)
val list_assoc : t -> (t * 'a) list -> 'a
(** [list_assoc x l] returns the element associated with [x] in the list of
pairs [l].
@raise Not_found if there is no value associated with [x] in the list [l].*)
val list_mem_assoc : t -> (t * 'a) list -> bool
(** Same as {! list_assoc}, but simply returns [true] if a binding exists, and
[false] if no bindings exist for the given key.*)
val list_mem : t -> t list -> bool
(** [list_mem x l] is [true] if and only if [x] is equal to an element of [l].*)
val list_mem_couple : t * t -> (t * t) list -> bool
(** [list_mem_couple (x,y) l] is [true] if and only if [(x,y)] is equal to an
element of [l].*)
val compare_list : t list -> t list -> int
(** [compare_list l1 l2] returns [0] if and only if [l1] is equal to [l2].*)
val print : Format.formatter -> t -> unit
(** Prints a list of hash-consed strings on a formatter. *)
module H : Hashtbl.S with type key = t
(** Hash-tables indexed by hash-consed strings *)
module HSet : Set.S with type elt = t
(** Sets of hash-consed strings *)
module HMap : Map.S with type key = t
(** Maps indexed by hash-consed strings *)