1. Sébastien Ferré
  2. ocaml-lib

Source

ocaml-lib / logdag.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
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485

(** The first input signature of the functor {!Logdag.Make} specifying various paramters. *)
module type PARAM =
  sig
    val dbname : string (** File name of the Dbm database. Files {i dbname}[.dir] and {i dbname}[.pag] are created if necessary. *)
    val max_mem : float  (** Number of bytes beyond which nodes are removed from memory. *)
    val node_chunk : int  (** Number of nodes that are removed from memory when more than [max_mem] is used. *) 
    val log_file : string option  (** Optional filename for printing a log of internal messages. *)
  end

(** The second input signature of the functor {!Logdag.Make} specifying the logic. *)
module type LOG =
  sig
    type t  (** Abstract type of formulas. *)
    val top : unit -> t  (** Most general formula. *)
    val entails : t -> t -> bool  (** Entailment relation {e is more specific than} of the logic. *)
    val gen : t -> t -> t list -> t list  (** Dichotomic operator for generating new features. *)
    val parse : Syntax.t_stream -> t  (** Parsing of formulas from token streams. *)
    val print : t -> Syntax.t_list  (** Printing of formulas to token lists. *)
  end

(** The signature of implementations of logical diagrams. *)
module type T =
  sig
    module Log : LOG
    (** The logic module passed as a parameter. *)

    val some_log : bool
    (** True if a log file is open. *)

    val log_fmt : Format.formatter
    (** The formatter associated to the log file when it exists. *)

    val db : Dbm.t
    (** The database used for persistency and swapping. *)

    type nid = int
    (** Type of node ids. This type is also used for identifying objects: the id of an object is the id of its description node. *)

    val nil : nid
    (** Nil id referencing no node. *)

    val top : nid
    (** Id of the most general node. *)

    (** Module for the representation of extents (sets of objects). *)
    module Ext :
      sig
        type t  (** Abstract type of extents. *)
        val empty : t  (** The empty extent. *)
        val is_empty : t -> bool  (** [is_empty ext] tests whether [ext] is empty. *)
        val cardinal : t -> int  (** [cardinal ext] returns the size of the extent [ext]. *)
        val mem : nid -> t -> bool  (** [mem o ext] tests whether [o] belongs to [ext]. *)
        val contains : t -> t -> bool  (** [contains ext1 ext2] tests whether [ext1] contains [ext2]. *)
        val add : nid -> t -> t  (** [add o ext] returns the addition of [o] to [ext]. *)
        val remove : nid -> t -> t  (** [remove o ext] returns the removal of [o] from [ext]. *)
        val union : t -> t -> t  (** [union ext1 ext2] returns the set union of [ext1] and [ext2]. *)
        val union_r : t list -> t  (** [union_r exts] returns the union of all extents in [exts]. *)
        val inter : t -> t -> t  (** [inter ext1 ext2] returns the set intersection of [ext1] and [ext2]. *)
        val inter_r : t list -> t  (** [inter_r exts] returns the intersection of all extents in [exts].
                                       @raise Invalid_argument if [exts] is the empty list. *)
        val subtract : t -> t -> t  (** [subtract ext1 ext2] returns the set subtraction of [ext1] and [ext2]. *)
        val inter_difsym : t -> t -> t * t * t
          (** [inter_difsym ext1 ext2] returns the extent triplet [(subtract ext1 ext2, inter ext1 ext2, subtract ext2 ext1)]. *)
        val iter : (nid -> unit) -> t -> unit
          (** Iteration on the objects of an extent (see [List.iter]). Objects visited from low ids to high ids. *)
        val fold_left : ('a -> nid -> 'a) -> 'a -> t -> 'a
          (** Folding on an extent from low ids to high ids (see List.fold_left). *)
        val fold_right : (nid -> 'a -> 'a) -> t -> 'a -> 'a
          (** Folding on an extent from high ids to low ids (see List.fold_right). *)
      end

    type node
    (** Abstract type of nodes.

       {e Warning}: values of this type are relevant at the time they are
	retrieved, but are not guarenteed to remain consistent after changes are
	made. *)

    val feat : node -> Log.t
    (** [feat node] gets the formula label of [node]. *)

    val ext : node -> Ext.t
    (** [ext node] gets the extent label of [node]. *)

    val inf : node -> nid LSet.t
    (** [inf node] gets the inferior (more specific) neighbours of [node]. *)

    val sup : node -> nid LSet.t
    (** [sup node] gets the superior (more general) neighbours of [node]. *)

    val is_obj : node -> bool
    (** [is_obj node] test whether [node] is labeled by an object. *)

    val get : nid -> node
    (** [get nid] retrieves a node from its id [nid]. If the node is not yet in memory, it is loaded from the database.
        @raise Not_found when the node [nid] does not exist in the diagram. *)

    val insert : Log.t -> bool -> nid * bool
    (** [insert f obj] returns the node id whose formula label is
	logically equivalent to [f]. If such a node does not yet exist in the
	diagram, it is inserted and the second result is [true]; otherwise the second result is [false]. 
        If [obj] is true, then a new object is
	associated to this node, and extents of existing nodes are updated
	accordingly. *)

    val remove : nid -> unit
    (** [remove nid] removes the node identified by [nid] from the diagram (both in memory and the database). *)

    val fold : (nid * node -> 'a -> 'a * nid list) -> nid * node -> 'a -> 'a
    (** [fold f_next (nid,node) e] computes a result through a traversal of
	the diagram. The starting node is specified by [(nid,node)], where
	[node] must be equal to [get nid]. The application [f_next (nid,node)
	res] to the current node [(nid,node)] and the current result [res]
	returns a pair [(res',next_nids)], where [res'] is the new result, and
	[next_nids] are the ids of the next nodes to be visited. The traversal
	order is not specified, but each node is ensured to be visited at most
	once. *)

    val first : pred_next:(bool -> nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list
    (** [first ~pred_next ~start:(nid,node)] looks for the first nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. The
	first parameter can be used for optimization as, when it is false,
	[None] can be returned in all cases. *)

    val last : pred_next:(nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list
    (** [last ~pred_next ~start:(nid,node)] looks for the last nodes encountered in
	a traversal of the diagram, and satisfying some condition {e
	pred}. The traversal is defined similarly to [fold] (starting point,
	and next nodes). The first result of an application of [pred_next] is
	[None] if {e pred} is not satisfied, and [Some] {i v} otherwise, {i v}
	being the value returned as a result instead of the node itself. *)

    val glbs : pred:(nid * node -> bool) -> (nid * node) list -> (nid * node) list
    (** [glbs ~pred nodes] returns the {e glbs} (greatest lower bounds) of the nodes [nodes] among the nodes satisfying [pred]. *)

    val lubs : pred:(nid * node -> int -> 'a option) -> suppmin:int -> (nid * node) list -> 'a list
    (** [lubs ~pred ~suppmin nodes] returns the [suppmin]-approximate {e lubs}
	(least upper bounds) of the nodes [nodes] among the nodes satisfying
	[pred]. A node is a [suppmin]-approximate lub if it has at least
	[suppmin] more specific nodes in [nodes]. The second argument of
	[pred] is the support of the node (number of more specific nodes in
	[nodes]). *)

  end

module Make (Param : PARAM) (Log : LOG) : T =
  struct
    module Log = Log

    open Format

    let some_log = match Param.log_file with None -> false | Some _ -> true
    let log_fmt = match Param.log_file with None -> Format.err_formatter | Some name -> formatter_of_out_channel (open_out name)


    type nid = int

    module Ext =
      struct
        type t = int * nid LSet.t
        let empty = 0, LSet.empty ()
        let is_empty (s,_) = s=0
        let cardinal (s,_) = s
        let mem nid (_,l) = LSet.mem nid l
        let contains (_,l1) (_,l2) = LSet.contains l1 l2
        let add nid (_,l) = let l' = LSet.add nid l in LSet.cardinal l', l'
        let remove nid (_,l) = let l' = LSet.remove nid l in LSet.cardinal l', l'
        let union (_,l1) (_,l2) = let l' = LSet.union l1 l2 in LSet.cardinal l', l'
        let union_r exts = let l' = LSet.union_r (List.map snd exts) in LSet.cardinal l', l'
        let inter (_,l1) (_,l2) = let l' = LSet.inter l1 l2 in LSet.cardinal l', l'
        let inter_r exts = let l' = LSet.inter_r (List.map snd exts) in LSet.cardinal l', l'
        let subtract (_,l1) (_,l2) = let l' = LSet.subtract l1 l2 in LSet.cardinal l', l'
        let inter_difsym (_,l1) (_,l2) =
          LSet.fold
            (fun ((s1,l1), (s2,l2), (s3,l3)) (w,x) ->
               match w with
               | LSet.Infst -> (s1+1,LSet.add x l1), (s2,l2), (s3,l3)
               | LSet.Inboth -> (s1,l1), (s2+1,LSet.add x l2), (s3,l3)
               | LSet.Insnd -> (s1,l1), (s2,l2), (s3+1,LSet.add x l3))
            ((0,LSet.empty ()) , (0,LSet.empty ()), (0,LSet.empty ()))
            l1 l2
        let iter f (_,l) = List.iter f l
        let fold_left f e (_,l) = List.fold_left f e l
        let fold_right f (_,l) e = List.fold_right f l e
      end

    module Nval =
      struct
        type t = float
        let init () = Common.utime ()
        let update v = Common.utime ()
        let better v1 v2 = v1 >= v2
      end

    type node = {
	mutable feat : Log.t;  (* formula describing the node, and description of local object if some *)
	mutable ext : Ext.t;  (* object idents of the extent *)
	mutable sup : nid LSet.t;  (* list of parent nodes *)
	mutable inf : nid LSet.t;  (* list of child nodes *)
        mutable v : Nval.t  (* value w.r.t. swapping *)
      }

    let nil = 0
    let node_nil = {
        feat = Log.top ();
        ext = Ext.empty;
        inf = LSet.empty ();
        sup = LSet.empty ();
        v = Nval.init ()
      }

    let top = 1

    let db = Dbm.opendbm Param.dbname [Dbm.Dbm_create; Dbm.Dbm_rdwr] 0o664
    let _ = at_exit (fun () -> Dbm.close db)

    let db_mod : Dbm.t Cache.db_mod = {
        Cache.find = Dbm.find;
        Cache.replace = Dbm.replace;
        Cache.remove = Dbm.remove
      }

    let cache_cpt = Cache.create db_mod db "cpt" 1
    let _ =
      if not (Cache.mem cache_cpt 0)
      then Cache.add cache_cpt 0 (ref (top+1))

    let cpt () = Cache.get cache_cpt 0


    let cache_nid = Cache.create db_mod db "nid" Param.node_chunk
    let _ =
      if not (Cache.mem cache_nid top)
      then Cache.add cache_nid top node_nil

    let rec unget_chunk () =
      if Random.int Param.node_chunk = 0 & Common.heap_size () > Param.max_mem
      then begin
        if some_log then pp_print_string log_fmt "Logdag: swapping nodes on disk\n";
        let keys = get_worst_chunk () in
        List.iter (Cache.unget cache_nid) keys;
        Gc.major () end
    and get_worst_chunk () =
      let rec insert x =
        function
        | [] -> [x]
        | y::ys ->
           if Nval.better x y
           then x::y::ys
           else y::insert x ys in
      let _, worst_chunk =
        Cache.fold
          (fun nid node (n,l) ->
             let n', l' = n+1, insert (node.v,nid) l in
             if n' <= Param.node_chunk
             then n', l'
             else n, List.tl l')
          cache_nid (0,[]) in
      List.map snd worst_chunk

    let get nid = Common.prof "Logdag.get" (fun () ->
      unget_chunk ();
      let node = Cache.get cache_nid nid in
      node.v <- Nval.update node.v;
      node)

    let create node =
      unget_chunk ();
      let cpt = cpt () in
      let nid = !cpt in
      incr cpt;
      Cache.add cache_nid nid node;
      nid

    let delete nid = Cache.remove cache_nid nid


    let feat node = node.feat

    let ext node = node.ext

    let inf node = node.inf

    let sup node = node.sup

    let is_obj node = LSet.is_empty node.inf & node.ext <> Ext.empty

    let rec fold : (nid * node -> 'a -> 'a * nid list) -> nid * node -> 'a -> 'a =
      fun f_next (nid,node) init ->
        let m = Array.make !(cpt ()) `Unknown
        in fold2 m f_next (nid,node) init
    and fold2 m f_next (nid,node) init =
      if m.(nid) = `Unknown
      then begin
	m.(nid) <- `Good;
	let res0, nids = f_next (nid,node) init in
	List.fold_left
	  (fun res n -> fold2 m f_next (n,get n) res)
	  res0
	  nids end
      else init

    let rec first : pred_next:(bool -> nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list =
      fun ~pred_next ~start ->
	let m = Array.make !(cpt ()) `Unknown
	in List.map snd (
          List.fold_left
	    (fun res nid -> first2 m pred_next (nid,get nid) true res)
	    [] (snd (pred_next false start)))
    and first2 m pred_next (nid,node) above res =
	if m.(nid) = `Unknown then
	  let x, nids = pred_next above (nid,node) in
	  let good = above & (x <> None) in
	  m.(nid) <- if good then `Good else `Bad;
	  List.fold_left
	    (fun res n -> first2 m pred_next (n,get n) (above & not good) res)
	    (match x with None -> res | Some v -> if good then ((nid, v)::res) else res)
	    nids
	else if m.(nid) = `Good & not above then begin
	  m.(nid) <- `Bad;
	  List.filter (fun (n,v) -> n != nid) res end 
	else res

    let rec last : pred_next:(nid * node -> 'a option * nid list) -> start:(nid * node) -> 'a list =
      fun ~pred_next ~start ->
	let m = Array.make !(cpt ()) `Unknown in
	snd (new_last m pred_next start [])
    and new_last m pred_next (nid,node) res =
	let x, nids = pred_next (nid,node) in
	let last, res1 = List.fold_left
	    (fun (last,res) n ->
	      if m.(n) = `Good then (false,res) (* node is not a last one *)
	      else if m.(n) = `Bad then (last,res) (* node may be a last one *)
	      else (* m.(n) = `Unknown *)
		let last',res' = new_last m pred_next (n,get n) res in
		last & last', res')
	    (true,res)
	    nids in
	if not last
	then begin m.(nid) <- `Good; (false,res1) end
	else match x with
	| None -> begin m.(nid) <- `Bad; (true,res1) end
	| Some v -> begin m.(nid) <- `Good; (false,v::res1) end

    let glbs : pred:(nid * node -> bool) -> (nid * node) list -> (nid * node) list =
      fun ~pred -> function
	| [] -> [(top,get top)]
	| [nidnode] when pred nidnode -> [nidnode]
	| nidnodes ->
	    let m = Array.make !(cpt ()) 0 in
	    let lnodes = List.length nidnodes in
	    List.iter
	      (fun (nid,node) ->
		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), nd.inf) (nid,node) ())
	      nidnodes;
	    first
	      (fun above (nid,node) ->
		(if above & m.(nid) >= lnodes & pred (nid,node) then Some (nid,node) else None), node.inf)
	      (nil, {node_nil with inf = List.map fst nidnodes})

    let rec lubs : pred:(nid * node -> int -> 'a option) -> suppmin:int -> (nid * node) list -> 'a list =
      fun ~pred ~suppmin -> function
	| [] -> raise (Invalid_argument "LogDag.Make.lubs : the list is empty") 
	| nidnodes -> Common.prof "Logdag.lubs" (fun () ->
	    let m = Array.make !(cpt ()) 0 in
	    let l = List.length nidnodes in
	    let supp = min suppmin l in
	    List.iter
	      (fun (nid,node) ->
		fold (fun (n,nd) res -> m.(n) <- m.(n)+1; (), nd.sup) (nid,node) ())
	      (if supp=l then List.tl nidnodes else nidnodes);
            let smin = if supp=l then supp-1 else supp in
	    first
	      (fun _ (nid,node) ->
                let s = m.(nid) in
		(if s >= smin then pred (nid,node) s else None),
		node.sup)
	      (if supp=l then (List.hd nidnodes) else (nil,{node_nil with sup = List.map fst nidnodes})))


    let locate : Log.t -> bool -> nid * node =
      fun feat obj ->
	let sup =
	  last
	    ~pred_next:(fun (nid,node) ->
	       if not (is_obj node) & Log.entails feat node.feat
	       then Some (nid,node), node.inf
	       else None, [])
	    ~start:(top,get top) in
	match sup with
	| [(nid,node)] when not obj & Log.entails node.feat feat ->
	     node.feat <- feat;  (* the old formula is replaced by the new equivalent one *)
	     nid, node  (* the searched node already exists *)
	| nodes ->  (* the searched node must be inserted *)
	     let inf, ext =
	       if obj
               then LSet.empty (), Ext.empty
               else
                 let inf = glbs (fun (nid,node) -> Log.entails node.feat feat) nodes in
                 inf, List.fold_left Ext.union Ext.empty (List.map (fun (nid,node) -> node.ext) inf) in
	     let new_node = {
		feat = feat;
		ext = ext;
		sup = LSet.of_list (List.map fst sup);
		inf = LSet.of_list (List.map fst inf);
                v = Nval.init ()} in
	     0, new_node

    let connect : nid -> node -> bool -> unit =
      fun nid node obj ->
	List.iter
	  (fun n ->
             let nd = get n in
             nd.inf <- LSet.add nid (LSet.subtract nd.inf node.inf))
	  node.sup;
	List.iter
	  (fun n ->
             let nd = get n in
             nd.sup <- LSet.add nid (LSet.subtract nd.sup node.sup))
	  node.inf;
        if obj
        then
	  fold
	    (fun (n,nd) () -> nd.ext <- Ext.add nid nd.ext; (), nd.sup)
	    (nid,node)
	    ()

    let insert feat obj = Common.prof "Logdag.insert" (fun () ->
      let nid, node = locate feat obj in
      if nid = nil
      then begin
        let nid = create node in
        connect nid node obj;
        nid, true end
      else begin
        nid, false end)

    let rec disconnect nid =
      let node = get nid in
      if is_obj node
      then
	fold
	  (fun (n,nd) () -> nd.ext <- Ext.remove nid nd.ext; (), nd.sup)
	  (nid,node)
	  ();
      List.iter (fun n -> let nd = get n in nd.inf <- LSet.remove nid nd.inf) node.sup;
      List.iter (fun n -> let nd = get n in nd.sup <- LSet.remove nid nd.sup) node.inf;
      let mup = Array.make !(cpt ()) false in
      fold
        (fun (n,nd) () -> (mup.(n) <- true), nd.sup)
        (nil,{node_nil with sup = node.inf})
        ();
      let mdown = Array.make !(cpt ()) false in
      let tbl = Hashtbl.create (2 * LSet.cardinal node.inf) in
      List.iter (fun n -> Hashtbl.add tbl n node.sup) node.inf;
      List.iter
	(fun n ->
           let nd = get n in
           List.iter (fun n' -> mdown.(n') <- false) node.inf;
           fold
             (fun (n',nd') () -> (mdown.(n') <- true), if mup.(n') then nd'.inf else [])
             (n,get n)
             ();
           let inf_old, inf_new = List.partition (fun n' -> mdown.(n')) node.inf in
	   nd.inf <- LSet.union nd.inf inf_new;
           List.iter (fun n' -> Hashtbl.replace tbl n' (LSet.remove n (Hashtbl.find tbl n'))) inf_old)
        node.sup;
      List.iter
        (fun n ->
           let nd = get n in
           nd.sup <- LSet.union nd.sup (Hashtbl.find tbl n))
        node.inf

    let remove nid =
      if nid <> top
      then begin
        try disconnect nid with Not_found -> ();
        delete nid end

  end