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
486
487
488
489
490
491
492
(** 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. *)
    val simpl : t -> t Stream.t  (** Simplifications of a formula. *)
  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 Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> '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] is the lazy evaluation of [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 Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> '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 Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> '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 Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) 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 Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) 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.prof "Logdag.Nval.update" (fun () -> 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 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 unget_cpt = ref 0

    let unget_chunk () = Common.prof "Logdag.unget_chunk" (fun () ->
      if (unget_cpt := !unget_cpt+1 mod Param.node_chunk; !unget_cpt = 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)

    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 Lazy.t -> 'a -> 'a * nid list) -> nid * node Lazy.t -> '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,lazy (get n)) res)
	  res0
	  nids end
      else init

    let rec first : pred_next:(bool -> nid * node Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> '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,lazy (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,lazy (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 Lazy.t -> 'a option * nid list) -> start:(nid * node Lazy.t) -> '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,lazy (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 Lazy.t -> bool) -> (nid * node Lazy.t) list -> (nid * node Lazy.t) list =
      fun ~pred -> function
	| [] -> [(top,lazy (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; (), (Lazy.force nd).inf) (nid,node) ())
	      nidnodes;
	    first
	      (fun above (nid,node) ->
		(if above & m.(nid) >= lnodes & pred (nid,node) then Some (nid,node) else None), (Lazy.force node).inf)
	      (nil, lazy {node_nil with inf = List.map fst nidnodes})

    let rec lubs : pred:(nid * node Lazy.t -> int -> 'a option) -> suppmin:int -> (nid * node Lazy.t) 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; (), (Lazy.force 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),
		(Lazy.force node).sup)
	      (if supp=l then (List.hd nidnodes) else (nil,lazy {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 (Lazy.force node)) & Log.entails feat (Lazy.force node).feat
	       then Some (nid,node), (Lazy.force node).inf
	       else None, [])
	    ~start:(top,lazy (get top)) in
	match sup with
	| [(nid,node)] when not obj & Log.entails (Lazy.force node).feat feat ->
	     (Lazy.force node).feat <- feat;  (* the old formula is replaced by the new equivalent one *)
	     nid, Lazy.force 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 (Lazy.force node).feat feat) nodes in
                 inf, List.fold_left Ext.union Ext.empty (List.map (fun (nid,node) -> (Lazy.force 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) () ->
               let nd_val = Lazy.force nd in
               nd_val.ext <- Ext.add nid nd_val.ext; (), nd_val.sup)
	    (nid,lazy 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) () ->
             let nd_val = Lazy.force nd in
             nd_val.ext <- Ext.remove nid nd_val.ext; (), nd_val.sup)
	  (nid,lazy 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), (Lazy.force nd).sup)
        (nil,lazy {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 (Lazy.force nd').inf else [])
             (n,lazy (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
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.