summaryrefslogtreecommitdiff
path: root/lib/tlm.ml
blob: 17d337c887467386550c9423826cde48e30a03ee (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: tlm.ml 14641 2011-11-06 11:59:10Z herbelin $ *)

type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t

let empty = Node (Gset.empty, Gmap.empty)

let map (Node (_,m)) lbl = Gmap.find lbl m

let xtract (Node (hereset,_)) = Gset.elements hereset

let dom (Node (_,m)) = Gmap.dom m

let in_dom (Node (_,m)) lbl = Gmap.mem lbl m

let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = [])

let assure_arc m lbl =
  if Gmap.mem lbl m then
    m
  else
    Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m

let cleanse_arcs (Node (hereset,m)) =
  let l = Gmap.rng m in
  Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m)

let rec at_path f (Node (hereset,m)) = function
  | [] ->
      cleanse_arcs (Node(f hereset,m))
  | h::t ->
      let m = assure_arc m h in
      cleanse_arcs (Node(hereset,
                         Gmap.add h (at_path f (Gmap.find h m) t) m))

let add tm (path,v) =
  at_path (fun hereset -> Gset.add v hereset) tm path

let rmv tm (path,v) =
  at_path (fun hereset -> Gset.remove v hereset) tm path

let app f tlm =
  let rec apprec pfx (Node(hereset,m)) =
    let path = List.rev pfx in
    Gset.iter (fun v -> f(path,v)) hereset;
    Gmap.iter (fun l tm -> apprec (l::pfx) tm) m
  in
  apprec [] tlm

let to_list tlm =
  let rec torec pfx (Node(hereset,m)) =
    let path = List.rev pfx in
    List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset))::
		 (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
  in
  torec [] tlm