1 files changed, 106 insertions, 0 deletions
diff --git a/src/lfsc/hstring.ml b/src/lfsc/hstring.ml
new file mode 100644
index 0000000..aa948e0
--- /dev/null
+++ b/src/lfsc/hstring.ml
@@ -0,0 +1,106 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+open Shashcons
+
+module S = 
+  Shashcons.Make_consed(struct include String 
+		       let hash = Hashtbl.hash 
+		       let equal = (=)     end)
+
+module HS = struct
+
+  type t = string Shashcons.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_assoc_inv x = function
+    | [] -> raise Not_found
+    | (y, v) :: l -> if equal x v then y else list_assoc_inv 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_equal l1 l2 =
+    match l1, l2 with
+      | [], [] -> true
+      | [], _ -> false
+      | _, [] -> false
+      | x::r1, y::r2 -> equal x y && list_equal 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)
+
+  let rec print_list sep fmt = function
+    | [] -> ()
+    | [s] -> print fmt s
+    | s::r -> Format.fprintf fmt "%a%s%a" print s sep (print_list sep) r
+
+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 *)