diff options
author | 2012-01-12 16:02:20 +0100 | |
---|---|---|
committer | 2012-01-12 16:02:20 +0100 | |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /lib/tlm.ml | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'lib/tlm.ml')
-rw-r--r-- | lib/tlm.ml | 63 |
1 files changed, 0 insertions, 63 deletions
diff --git a/lib/tlm.ml b/lib/tlm.ml deleted file mode 100644 index 17d337c8..00000000 --- a/lib/tlm.ml +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* 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 |