package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file hopcroft.ml

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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Partition refinement algorithm *)

module type PartitionS =
sig
  type t
  (** Type of partition structure *)

  type set
  (** Type of partitions *)

  val create : int -> t
  (** Create a partition structure of the given size *)

  val length : t -> int
  (** Number of partitions *)

  val size : set -> t -> int
  (** Number of elements of a partition *)

  val partition : int -> t -> set
  (** [partition i t] returns the index of the partition which contains [i] *)

  val iter : set -> (int -> unit) -> t -> unit
  (** Iter on elements of a partition. Don't [mark] and [split] in the loop! *)

  val fold : set -> (int -> 'a -> 'a) -> t -> 'a -> 'a
  (** Fold left to right on elements of a partition. Don't [mark] and [split] in
      the loop! *)

  val iter_all : (set -> unit) -> t -> unit
  (** Iter on partitions. Don't [mark] and [split] in the loop! *)

  val fold_all : (set -> 'a -> 'a) -> t -> 'a -> 'a
  (** Fold left to right on partitions. Don't [mark] and [split] in the loop! *)

  val mark : int -> t -> unit
  (** Mark an element for splitting *)

  val split : set -> t -> set
  (** Performs splitting and return the set of marked elements *)

  val is_marked : set -> t -> bool
  (** Returns [true] if some element of the set is marked *)

  val is_valid : set -> bool
  (** Test whether a splitting succeeded *)

  val represent : set -> int
  (** Associate a unique number to each partition. If the partition is valid, then
      the returned number is guaranteed to be between [0] and [len - 1] when
      [len] is the number of partitions of the structure. *)
end

module Partition =
struct

type set = int

type t = {
  mutable partitions : int;
  (** number of partitions *)
  mutable first : int array;
  (** index of the first element of a partition *)
  mutable last : int array;
  (** successor index of the last element of a partition *)
  mutable marked : int array;
  (** index of the last marked element of a partition *)
  index : set array;
  (** associate a partition to an element *)
  elements : int array;
  (** contain elements in a contiguous way w.r.t. partitions *)
  location : int array;
  (** keep the location of an element in [elements] *)
}

let initial_size n = max (n / 100) 7

let create n = {
  partitions = 0;
  first = Array.make (initial_size n) 0;
  last = Array.make (initial_size n) n;
  marked = Array.make (initial_size n) 0;
  index = Array.make n 0;
  elements = Array.init n (fun i -> i);
  location = Array.init n (fun i -> i);
}

let uget (t : int array) i = Array.get t i
let uset (t : int array) i x = Array.set t i x

let length t = succ t.partitions

let size s t =
  uget t.last s - uget t.first s

let partition i t = uget t.index i

let iter s f t =
  let fst = uget t.first s in
  let lst = uget t.last s in
  for i = fst to lst - 1 do
    f (uget t.elements i);
  done

let fold s f t accu =
  let fst = uget t.first s in
  let lst = uget t.last s in
  let rec fold accu i =
    if lst <= i then accu
    else fold (f (uget t.elements i) accu) (succ i)
  in
  fold accu fst

let iter_all f t =
  for i = 0 to t.partitions do f i; done

let fold_all f t accu =
  let rec fold accu i =
    if t.partitions <= i then accu
    else fold (f i accu) (succ i)
  in
  fold accu 0

let resize t =
  let len = Array.length t.first in
  if len <= t.partitions then begin
    let nlen = 2 * len + 1 in
    let pfirst = t.first in
    let plast = t.last in
    let pmarked = t.marked in
    let nfirst = Array.make nlen 0 in
    let nlast = Array.make nlen 0 in
    let nmarked = Array.make nlen 0 in
    for i = 0 to pred len do
      uset nfirst i (uget pfirst i);
      uset nlast i (uget plast i);
      uset nmarked i (uget pmarked i);
    done;
    t.first <- nfirst;
    t.last <- nlast;
    t.marked <- nmarked;
  end

let split s t =
  if uget t.marked s = uget t.last s then uset t.marked s (uget t.first s);
  if uget t.marked s = uget t.first s then -1
  (* Nothing to split *)
  else begin
    let len = succ t.partitions in
    t.partitions <- len;
    resize t;
    uset t.first len (uget t.first s);
    uset t.marked len (uget t.first s);
    uset t.last len (uget t.marked s);
    uset t.first s (uget t.marked s);
    for i = uget t.first len to pred (uget t.last len) do
      uset t.index (uget t.elements i) len;
    done;
    len
  end

let mark i t =
  let set = uget t.index i in
  let loc = uget t.location i in
  let mark = uget t.marked set in
  if mark <= loc then begin
    uset t.elements loc (uget t.elements mark);
    uset t.location (uget t.elements loc) loc;
    uset t.elements mark i;
    uset t.location i mark;
    uset t.marked set (succ mark);
  end

let is_marked s t = (uget t.marked s) <> (uget t.first s)

let is_valid s = 0 <= s

let represent s = s

end

(** Hopcroft algorithm *)

module type S =
sig
  type label
  type state
  type transition = {
    src : state;
    lbl : label;
    dst : state;
  }

  type automaton = {
    states : int;
    partitions : state list list;
    transitions : transition list;
  }

  val reduce : automaton -> state list array
end

module Make (Label : Map.OrderedType) : S
  with type label = Label.t
  and type state = int =
struct

type label = Label.t
type state = int

type transition = {
  src : state;
  lbl : label;
  dst : state;
}

module TMap = Map.Make(Label)

type automaton = {
  states : int;
  partitions : state list list;
  transitions : transition list;
}

(** Partitions of states *)
module SPartition : PartitionS = Partition

(** Partitions of transitions *)
module TPartition : PartitionS = Partition

type environment = {
  state_partition : SPartition.t;
  splitter_partition : TPartition.t;
  transition_source : int array;
}

(** Associate the list of transitions ending in a given state *)
let reverse automaton =
  let ans = Array.make automaton.states [] in
  let add (x : int) l = (* if List.mem x l then l else *) x :: l in
  let iter i trans =
    let l = Array.get ans trans.dst in
    Array.set ans trans.dst (add i l)
  in
  let () = List.iteri iter automaton.transitions in
  ans

let init automaton =
  let transitions = automaton.transitions in
  let len = List.length transitions in
  (* Sort transitions according to their label *)
  let env = {
    state_partition = SPartition.create automaton.states;
    splitter_partition = TPartition.create len;
    transition_source = Array.make len (-1);
  } in
  (* Set the source of the transitions *)
  let iteri i trans = env.transition_source.(i) <- trans.src in
  let () = List.iteri iteri transitions in
  (* Split splitters according to their label *)
  let fold i accu trans = match TMap.find_opt trans.lbl accu with
  | None -> TMap.add trans.lbl [i] accu
  | Some l -> TMap.add trans.lbl (i :: l) accu
  in
  let lblmap = CList.fold_left_i fold 0 TMap.empty transitions in
  let p = env.splitter_partition in
  let pt = TPartition.partition 0 p in
  let iter _ trs =
    let iter idx = TPartition.mark idx p in
    let () = List.iter iter trs in
    ignore (TPartition.split pt p : TPartition.set)
  in
  let () = TMap.iter iter lblmap in
  (* Push every splitter in the todo stack *)
  let fold pt todo = pt :: todo in
  let splitter_todo = TPartition.fold_all fold env.splitter_partition [] in
  env, splitter_todo, automaton.partitions

let split_partition s inv env todo =
  let p = env.state_partition in
  let r = SPartition.split s p in
  if SPartition.is_valid r then begin
    let r = if SPartition.size r p < SPartition.size s p then r else s in
    let fold state accu =
      let fold accu trans =
        let pt = TPartition.partition trans env.splitter_partition in
        let accu =
          if TPartition.is_marked pt env.splitter_partition then accu
          else pt :: accu
        in
        let () = TPartition.mark trans env.splitter_partition in
        accu
      in
      List.fold_left fold accu inv.(state)
    in
    let splitter_touched = SPartition.fold r fold p [] in
    let fold_touched todo pt =
      let npt = TPartition.split pt env.splitter_partition in
      if TPartition.is_valid npt then npt :: todo
      else todo
    in
    List.fold_left fold_touched todo splitter_touched
  end else
    todo

let reduce_aux automaton =
  let env, splitter_todo, initial = init automaton in
  let inv = reverse automaton in
  (* Mark every state in each initial partition and split *)
  let ps = SPartition.partition 0 env.state_partition in
  let splitter_todo =
    let separate todo pt =
      let iter state () = SPartition.mark state env.state_partition in
      let () = List.fold_right iter pt () in
      split_partition ps inv env todo
    in
    List.fold_left separate splitter_todo initial
  in
  (* Main loop *)
  let rec loop = function
  | [] -> ()
  | pt :: todo ->
    let fold t state_touched =
      let previous = env.transition_source.(t) in
      let equiv = SPartition.partition previous env.state_partition in
      let state_touched =
        if SPartition.is_marked equiv env.state_partition then state_touched
        else equiv :: state_touched
      in
      let () = SPartition.mark previous env.state_partition in
      state_touched
    in
    let state_touched = TPartition.fold pt fold env.splitter_partition [] in
    let fold_touched todo equiv = split_partition equiv inv env todo in
    let splitter_todo = List.fold_left fold_touched todo state_touched in
    loop splitter_todo
  in
  let () = loop splitter_todo in
  (env, inv)

let reduce automaton =
  let (ans, _) = reduce_aux automaton in
  let mapping = Array.make (SPartition.length ans.state_partition) [] in
  let iter set =
    let pi = SPartition.represent set in
    let iter i =
      let map = Array.get mapping pi in
      Array.set mapping pi (i :: map)
    in
    SPartition.iter set iter ans.state_partition
  in
  let () = SPartition.iter_all iter ans.state_partition in
  mapping

end