From fe1979bf47951352ce32a6709cb5138fd26f311d Mon Sep 17 00:00:00 2001 From: soubiran Date: Wed, 21 Oct 2009 15:12:52 +0000 Subject: This big commit addresses two problems: 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/lib.mllib | 1 + lib/tries.ml | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/tries.mli | 34 ++++++++++++++++++++++++++ 3 files changed, 113 insertions(+) create mode 100644 lib/tries.ml create mode 100644 lib/tries.mli (limited to 'lib') diff --git a/lib/lib.mllib b/lib/lib.mllib index 2321abd1b0..56fe32cbd5 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -13,6 +13,7 @@ Edit Gset Gmap Tlm +tries Gmapl Profile Explore diff --git a/lib/tries.ml b/lib/tries.ml new file mode 100644 index 0000000000..1159ea2331 --- /dev/null +++ b/lib/tries.ml @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + functor (Y : Map.OrderedType) -> +struct + module T_dom = Set.Make(X) + module T_codom = Map.Make(Y) + + type t = Node of T_dom.t * t T_codom.t + + let codom_to_list m = T_codom.fold (fun x y l -> (x,y)::l) m [] + + let codom_rng m = T_codom.fold (fun _ y acc -> y::acc) m [] + + let codom_dom m = T_codom.fold (fun x _ acc -> x::acc) m [] + + let empty = Node (T_dom.empty, T_codom.empty) + + let map (Node (_,m)) lbl = T_codom.find lbl m + + let xtract (Node (hereset,_)) = T_dom.elements hereset + + let dom (Node (_,m)) = codom_dom m + + let in_dom (Node (_,m)) lbl = T_codom.mem lbl m + + let is_empty_node (Node(a,b)) = (T_dom.elements a = []) & (codom_to_list b = []) + +let assure_arc m lbl = + if T_codom.mem lbl m then + m + else + T_codom.add lbl (Node (T_dom.empty,T_codom.empty)) m + +let cleanse_arcs (Node (hereset,m)) = + let l = codom_rng m in + Node(hereset, if List.for_all is_empty_node l then T_codom.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, + T_codom.add h (at_path f (T_codom.find h m) t) m)) + +let add tm (path,v) = + at_path (fun hereset -> T_dom.add v hereset) tm path + +let rmv tm (path,v) = + at_path (fun hereset -> T_dom.remove v hereset) tm path + +let app f tlm = + let rec apprec pfx (Node(hereset,m)) = + let path = List.rev pfx in + T_dom.iter (fun v -> f(path,v)) hereset; + T_codom.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)) (T_dom.elements hereset)):: + (List.map (fun (l,tm) -> torec (l::pfx) tm) (codom_to_list m))) + in + torec [] tlm + +end diff --git a/lib/tries.mli b/lib/tries.mli new file mode 100644 index 0000000000..342c81ecdc --- /dev/null +++ b/lib/tries.mli @@ -0,0 +1,34 @@ + + + + + +module Make : + functor (X : Set.OrderedType) -> + functor (Y : Map.OrderedType) -> +sig + + type t + + val empty : t + + (* Work on labels, not on paths. *) + + val map : t -> Y.t -> t + + val xtract : t -> X.t list + + val dom : t -> Y.t list + + val in_dom : t -> Y.t -> bool + + (* Work on paths, not on labels. *) + + val add : t -> Y.t list * X.t -> t + + val rmv : t -> Y.t list * X.t -> t + + val app : ((Y.t list * X.t) -> unit) -> t -> unit + + val to_list : t -> (Y.t list * X.t) list +end -- cgit v1.2.3