1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* 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 *)
|
