package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file imperative.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
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

(** {1 Nodes} *)
(** {2 Nodes without values (simple nodes)} *)

module MakeNode
    (Elt : Parameters.SIMPLE_GENERIC_ELT)
    (Relation : Parameters.GENERIC_GROUP) =
struct
  type 'a t = { mutable parent : 'a parent; payload : 'a Elt.t }
  and 'a parent =
    | Node : 'b t * ('a, 'b) Relation.t -> 'a parent
    | Root

  let polyeq a b = Elt.polyeq a.payload b.payload

  module Relation = Relation

  let get_parent x = x.parent
  let set_parent x v = x.parent <- v

  let payload x = x.payload
  let make_node payload = { payload; parent = Root }
end

module MakeNumberedNode
    (Elt : HetHashtbl.HETEROGENEOUS_HASHED_TYPE)
    (Relation : Parameters.GENERIC_GROUP)
    () =
struct
  include MakeNode(Elt)(Relation)

  module H = HetHashtbl.Make(Elt)(struct type nonrec ('a, _) t = 'a t end)

  let nodes : unit H.t = H.create 100
  let make_node payload =
    let nd = make_node payload in
    H.add nodes payload nd;
    nd

  let get_node payload = H.find_opt nodes payload

  let get_or_make_node payload = match get_node payload with
    | Some t -> t
    | None -> make_node payload
end

(** {2 Nodes with values} *)

module MakeValuedNode
    (Elt : Parameters.SIMPLE_GENERIC_ELT)
    (Relation : Parameters.GENERIC_GROUP)
    (Value : Parameters.SIMPLE_GENERIC_VALUE with type ('a,'b) relation = ('a,'b) Relation.t) =
struct
  type 'a t = { mutable parent : 'a parent; payload : 'a Elt.t }
  and 'a parent =
    | Node : 'b t * ('a, 'b) Relation.t -> 'a parent
    | Root of 'a root
  and 'a root = { mutable value : 'a Value.t; mutable size : int }

  let polyeq a b = Elt.polyeq a.payload b.payload

  module Relation = Relation
  module Value = Value

  let get_parent x = x.parent
  let set_parent x v = x.parent <- v

  let payload x = x.payload
  let make_node payload value = { payload; parent = Root { value; size = 1 } }
end

module MakeValuedNumberedNode
    (Elt : HetHashtbl.HETEROGENEOUS_HASHED_TYPE)
    (Relation : Parameters.GENERIC_GROUP)
    (Value : Parameters.SIMPLE_GENERIC_VALUE with type ('a,'b) relation = ('a,'b) Relation.t)
    () =
struct
  include MakeValuedNode(Elt)(Relation)(Value)

  module H = HetHashtbl.Make(Elt)(struct type nonrec ('a, _) t = 'a t end)

  let nodes : unit H.t = H.create 100
  let make_node payload value =
    let nd = make_node payload value in
    H.add nodes payload nd;
    nd

  let get_node payload = H.find_opt nodes payload

  let get_or_make_node payload value = match get_node payload with
    | Some t -> t
    | None -> make_node payload value
end

module HashtblSimpleNode
  (Elt: HetHashtbl.HETEROGENEOUS_HASHED_TYPE)
  (Relation: Parameters.GENERIC_GROUP)
= struct
  type 'a t = 'a Elt.t
  type 'a parent =
    | Node: 'b t * ('a, 'b) Relation.t -> 'a parent
    | Root

  let polyeq = Elt.polyeq

  module H = HetHashtbl.Make(Elt)(struct type ('a, _) t = 'a parent end)

  let table: unit H.t = H.create 125

  let get_parent x = match H.find table x with
    | x -> x
    | exception Not_found -> Root

  let set_parent x = function
    | Root -> H.remove table x
    | n -> H.replace table x n

  module Relation = Relation
end

(** {1 Union find structures} *)

module GenericRelationalValued(Node: Parameters.UF_NODE_WITH_VALUE) =
struct
  open Node
  type 'a t = 'a Node.t
  type ('a, 'b) relation = ('a, 'b) Relation.t
  type 'a value = 'a Value.t

  type 'a ret = Exists_b : 'b t * 'b root * ('a, 'b) Relation.t -> 'a ret

  let ( ** ) = Relation.compose
  let ( ~~ ) = Relation.inverse

  let rec find_repr : type a. a t -> a ret =
   fun n ->
    match get_parent n with
    | Root r -> Exists_b (n, r, Relation.identity)
    | Node (parent, rel_parent) ->
        let (Exists_b (repr, root, rel_repr)) = find_repr parent in
        let rel = rel_repr ** rel_parent in
        let () = set_parent n (Node (repr, rel)) in
        Exists_b (repr, root, rel)

  type 'a node_through_relation =
    NodeThoughRelation : 'b t * ('a, 'b) Relation.t -> 'a node_through_relation
  type 'a value_through_relation =
    ValueThroughRelation : 'b Value.t * ('a, 'b) Relation.t -> 'a value_through_relation
  type 'a node_and_value_through_relation =
    NodeValueThroughRelation : 'b t * 'b Value.t * ('a, 'b) Relation.t
        -> 'a node_and_value_through_relation

  let find_representative n =
    let (Exists_b (repr, _, rel)) = find_repr n in
    NodeThoughRelation (repr, rel)

  let find_value n =
    let (Exists_b (_, root, rel)) = find_repr n in
    ValueThroughRelation (root.value, rel)

  let find n =
    let (Exists_b (repr, root, rel)) = find_repr n in
    NodeValueThroughRelation (repr, root.value, rel)

  let check_related a b =
      let Exists_b(ra, _, rel_a) = find_repr a in
      let Exists_b(rb, _, rel_b) = find_repr b in
      match polyeq ra rb with
      | Eq -> Some(~~rel_b ** rel_a)
      | Diff -> None

  let add_value a v =
    let Exists_b(_, root, rel) = find_repr a in
    let v = Value.apply v rel in
    root.value <- Value.meet root.value v

  (** Using the following diagram:

          a --(rel)--> b
          |            |
        rel_a        rel_b
          |            |
          V            v
        repr_a       repr_b

    => repr_a --(inv rel_a; rel; rel_b)--> repr_b (where ";" is composition)
    => repr_b --(inv rel_b; inv rel; rel_a)--> repr_a
  We do need to flip the arguments, as R.compose as the opposite argument order.
  A good thing about generic types is that the typechecker ensure we generate a valid
  relation here. *)
  let union a b rel =
    let (Exists_b (repr_a, root_a, rel_a)) = find_repr a in
    let (Exists_b (repr_b, root_b, rel_b)) = find_repr b in
    match polyeq repr_a repr_b with
    | Eq ->
      let old_rel = ~~rel_b ** rel_a in
      if Relation.equal rel old_rel then Ok () else Error old_rel
    | Diff ->
        (* Favor making [a] a child of [b] over the reverse, as this avoids a
           relation flip. *)
        begin if root_b.size >= root_a.size then (
          let rel = rel_b ** rel ** ~~rel_a in
          root_b.size <- root_b.size + root_a.size;
          root_b.value <- Value.meet root_b.value (Value.apply root_a.value rel);
          set_parent repr_a (Node (repr_b, rel)))
        else
          let rel = rel_a ** ~~rel ** ~~rel_b in
          root_a.size <- root_b.size + root_a.size;
          root_a.value <- Value.meet root_a.value (Value.apply root_b.value rel);
          set_parent repr_b (Node (repr_a, rel))
        end;
        Ok ()
end

module GenericRelational (Node : Parameters.UF_NODE) =
struct
  open Node
  type 'a t = 'a Node.t
  type ('a, 'b) relation = ('a, 'b) Relation.t

  let ( ** ) = Relation.compose
  let ( ~~ ) = Relation.inverse

  type 'a node_through_relation =
  | NodeThoughRelation : 'b t * ('a, 'b) Relation.t -> 'a node_through_relation

  let rec find_representative : type a. a t -> a node_through_relation =
   fun n ->
    match get_parent n with
    | Root -> NodeThoughRelation (n, Relation.identity)
    | Node (parent, rel_parent) ->
        let (NodeThoughRelation (repr, rel_repr)) = find_representative parent in
        let rel = rel_repr ** rel_parent in
        let () = set_parent n (Node (repr, rel)) in
        NodeThoughRelation (repr, rel)

  let check_related a b =
    let NodeThoughRelation(ra, rel_a) = find_representative a in
    let NodeThoughRelation(rb, rel_b) = find_representative b in
    match polyeq ra rb with
    | Eq -> Some(~~rel_b ** rel_a)
    | Diff -> None

  (** Using the following diagram:

          a --(rel)--> b
          |            |
        rel_a        rel_b
          |            |
          V            v
        repr_a       repr_b

    => repr_a --(inv rel_a; rel; rel_b)--> repr_b (where ";" is composition)
    => repr_b --(inv rel_b; inv rel; rel_a)--> repr_a
  We do need to flip the arguments, as R.compose as the opposite argument order.
  A good thing about generic types is that the typechecker ensure we generate a valid
  relation here. *)
  let union a b rel =
    let NodeThoughRelation(repr_a, rel_a) = find_representative a in
    let NodeThoughRelation(repr_b, rel_b) = find_representative b in
    match polyeq repr_a repr_b with
       | Eq ->
          let old_rel = ~~rel_b ** rel_a in
          if Relation.equal rel old_rel then Ok () else Error old_rel
       | Diff ->
          (* Favor making [a] a child of [b] over the reverse, as this avoids a
             relation flip. *)
          (* begin *)
            let rel = rel_b ** rel ** ~~rel_a in
            (* root_b.size <- root_b.size + root_a.size; *)
            set_parent repr_a (Node (repr_b, rel));
          (* else
            let rel = rel_a ** ~~rel ** ~~rel_b in
            root_a.size <- root_b.size + root_a.size;
            set_parent repr_b (Node (repr_a, rel))
          end; *)
          Ok ()
end