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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
type 'a key = 'a Types.key
external key : int -> 'a key = "%identity"
type data
and proc = data -> data -> data option
external make : int -> int -> 'a array = "caml_obj_block"
external get : data array -> 'a key -> 'a = "%obj_field"
external set : data array -> 'a key -> 'a -> unit = "%obj_set_field"
external handler : ('a -> 'a -> 'a option) -> proc = "%identity"
module type S = sig
type t
val id : t -> int
val get : 'a key -> t -> 'a
val set : 'a key -> 'a -> t -> unit
val register_key : ?merge:('a -> 'a -> 'a option) -> 'a -> 'a key
val register_at_fork : (t -> t -> unit) -> unit
val register_at_end : (t -> Types.status -> unit) -> unit
end
module Make () : sig
include S
val empty : unit -> t
val fork : t -> t
val merge : t -> t -> t option
val terminate : t -> Types.status -> unit
end = struct
type t = data array
let id : int key = key 0
let merger : (data -> data -> data option) array ref = ref (make 0 16)
let matrice : data array ref = ref (make 0 16)
let n = ref 0
and s = ref 1
let at_fork_callbacks = Queue.create ()
let register_at_fork f = Queue.add f at_fork_callbacks
let at_end_callbacks = Queue.create ()
let register_at_end f = Queue.add f at_end_callbacks
let default_merge x y = if x == y then Some x else None
let register_key : ?merge:('a -> 'a -> 'a option) -> 'a -> 'a key =
fun ?merge default ->
if !n > 0 then
Options.Logger.fatal
"data registration should happen before the start of exploration";
let l = Array.length !matrice in
let k = key !s in
if !s >= l then (
let merger' = Array.make (2 * l) (Array.get !merger 0) in
Array.blit !merger 0 merger' 0 l;
merger := merger';
let matrice' = Array.make (2 * l) (Array.get !matrice 0) in
Array.blit !matrice 0 matrice' 0 l;
matrice := matrice');
let merge = Option.fold ~none:default_merge ~some:handler merge in
Array.set !merger !s merge;
set !matrice k default;
incr s;
k
let empty () =
let t = Array.sub !matrice 0 !s in
incr n;
set t id !n;
t
let fork t =
let t' = Array.copy t in
incr n;
set t' id !n;
Queue.iter (fun f -> f t t') at_fork_callbacks;
t'
let rec merge t'' t t' i =
if i = !s then Some t''
else
match (Array.get !merger i) (Array.get t i) (Array.get t' i) with
| None -> None
| Some data ->
Array.set t'' i data;
merge t'' t t' (i + 1)
let merge t t' =
let t'' = Array.copy t in
merge t'' t t' 1
let terminate t status = Queue.iter (fun f -> f t status) at_end_callbacks
let id t = get t id
let get k t = get t k
let set k v t = set t k v
end