+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(*****************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Enrico Tassi <tassi@cs.unibo.it> *)
-(* 23/04/2004 *)
-(* *)
-(* This module implements the aciclic graph of universes. *)
-(* *)
-(*****************************************************************************)
-
-(* $Id$ *)
-
-(*****************************************************************************)
-(** switch implementation **)
-(*****************************************************************************)
-
-let fast_implementation = ref true ;;
-
-(*****************************************************************************)
-(** open **)
-(*****************************************************************************)
-
-open Printf
-
-(*****************************************************************************)
-(** Types and default values **)
-(*****************************************************************************)
-
-type universe = int * UriManager.uri option
-
-module UniverseType = struct
- type t = universe
- let compare = Pervasives.compare
-end
-
-module SOF = Set.Make(UniverseType)
-
-type entry = {
- eq_closure : SOF.t;
- ge_closure : SOF.t;
- gt_closure : SOF.t;
- in_gegt_of : SOF.t;
- one_s_eq : SOF.t;
- one_s_ge : SOF.t;
- one_s_gt : SOF.t;
-}
-
-module MAL = Map.Make(UniverseType)
-
-type arc_type = GE | GT | EQ
-
-type bag = entry MAL.t
-
-let empty_entry = {
- eq_closure=SOF.empty;
- ge_closure=SOF.empty;
- gt_closure=SOF.empty;
- in_gegt_of=SOF.empty;
- one_s_eq=SOF.empty;
- one_s_ge=SOF.empty;
- one_s_gt=SOF.empty;
-}
-let empty_bag = MAL.empty
-
-let are_set_eq s1 s2 =
- SOF.equal s1 s2
-
-let are_entry_eq v1 v2 =
- (are_set_eq v1.gt_closure v2.gt_closure ) &&
- (are_set_eq v1.ge_closure v2.ge_closure ) &&
- (are_set_eq v1.eq_closure v2.eq_closure ) &&
- (*(are_set_eq v1.in_gegt_of v2.in_gegt_of ) &&*)
- (are_set_eq v1.one_s_ge v2.one_s_ge ) &&
- (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
- (are_set_eq v1.one_s_eq v2.one_s_eq )
-
-let are_ugraph_eq = MAL.equal are_entry_eq
-
-(*****************************************************************************)
-(** Pretty printings **)
-(*****************************************************************************)
-
-let string_of_universe (i,u) =
- match u with
- Some u ->
- "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
- | None -> "(" ^ (string_of_int i) ^ ",None)"
-
-let string_of_universe_set l =
- SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
-
-let string_of_node n =
- "{"^
- "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^
- "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^
- "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^
- "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
-
-let string_of_arc (a,u,v) =
- (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
-
-let string_of_mal m =
- let rc = ref "" in
- MAL.iter (fun k v ->
- rc := !rc ^ sprintf "%s --> %s" (string_of_universe k)
- (string_of_node v)) m;
- !rc
-
-let string_of_bag b =
- string_of_mal b
-
-(*****************************************************************************)
-(** Benchmarking **)
-(*****************************************************************************)
-let time_spent = ref 0.0;;
-let partial = ref 0.0 ;;
-
-let reset_spent_time () = time_spent := 0.0;;
-let get_spent_time () = !time_spent ;;
-let begin_spending () =
- (*assert (!partial = 0.0);*)
- partial := Unix.gettimeofday ()
-;;
-
-let end_spending () =
- assert (!partial > 0.0);
- let interval = (Unix.gettimeofday ()) -. !partial in
- partial := 0.0;
- time_spent := !time_spent +. interval
-;;
-
-
-(*****************************************************************************)
-(** Helpers **)
-(*****************************************************************************)
-
-(* find the repr *)
-let repr u m =
- try
- MAL.find u m
- with
- Not_found -> empty_entry
-
-(* FIXME: May be faster if we make it by hand *)
-let merge_closures f nodes m =
- SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
-
-\f
-(*****************************************************************************)
-(** _fats implementation **)
-(*****************************************************************************)
-
-let rec closure_of_fast ru m =
- let eq_c = closure_eq_fast ru m in
- let ge_c = closure_ge_fast ru m in
- let gt_c = closure_gt_fast ru m in
- {
- eq_closure = eq_c;
- ge_closure = ge_c;
- gt_closure = gt_c;
- in_gegt_of = ru.in_gegt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = ru.one_s_gt
- }
-
-and closure_eq_fast ru m =
- let eq_c =
- let j = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.eq_closure) j m in
- let one_step_eq = ru.one_s_eq in
- (SOF.union one_step_eq _Uj)
- in
- eq_c
-
-and closure_ge_fast ru m =
- let ge_c =
- let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Ux = j in
- (SOF.union _Uj _Ux)
- in
- ge_c
-
-and closure_gt_fast ru m =
- let gt_c =
- let j = ru.one_s_gt in
- let k = ru.one_s_ge in
- let l = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Uk = merge_closures (fun x -> x.gt_closure) k m in
- let _Ul = merge_closures (fun x -> x.gt_closure) l m in
- let one_step_gt = ru.one_s_gt in
- (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
- in
- gt_c
-
-and print_rec_status u ru =
- print_endline ("Aggiusto " ^ (string_of_universe u) ^
- "e ottengo questa chiusura\n " ^ (string_of_node ru))
-
-and adjust_fast u m =
- let ru = repr u m in
- let gt_c = closure_gt_fast ru m in
- let ge_c = closure_ge_fast ru m in
- let eq_c = closure_eq_fast ru m in
- let changed_eq = not (are_set_eq eq_c ru.eq_closure) in
- let changed_gegt =
- (not (are_set_eq gt_c ru.gt_closure)) ||
- (not (are_set_eq ge_c ru.ge_closure))
- in
- if ((not changed_gegt) && (not changed_eq)) then
- m
- else
- begin
- let ru' = {
- eq_closure = eq_c;
- ge_closure = ge_c;
- gt_closure = gt_c;
- in_gegt_of = ru.in_gegt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = ru.one_s_gt}
- in
- let m = MAL.add u ru' m in
- let m =
- SOF.fold (fun x m -> adjust_fast x m)
- (SOF.union ru'.eq_closure ru'.in_gegt_of) m
- (* TESI:
- ru'.in_gegt_of m
- *)
- in
- m (*adjust_fast u m*)
- end
-
-and add_gt_arc_fast u v m =
- let ru = repr u m in
- let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
- let m' = MAL.add u ru' m in
- let rv = repr v m' in
- let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
- let m'' = MAL.add v rv' m' in
- adjust_fast u m''
-
-and add_ge_arc_fast u v m =
- let ru = repr u m in
- let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
- let m' = MAL.add u ru' m in
- let rv = repr v m' in
- let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
- let m'' = MAL.add v rv' m' in
- adjust_fast u m''
-
-and add_eq_arc_fast u v m =
- let ru = repr u m in
- let rv = repr v m in
- let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
- (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
- let m' = MAL.add u ru' m in
- let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
- (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
- let m'' = MAL.add v rv' m' in
- adjust_fast v (*(adjust_fast u*) m'' (* ) *)
-;;
-
-\f
-(*****************************************************************************)
-(** safe implementation **)
-(*****************************************************************************)
-
-let closure_of u m =
- let ru = repr u m in
- let eq_c =
- let j = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.eq_closure) j m in
- let one_step_eq = ru.one_s_eq in
- (SOF.union one_step_eq _Uj)
- in
- let ge_c =
- let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Ux = j in
- (SOF.union _Uj _Ux)
- in
- let gt_c =
- let j = ru.one_s_gt in
- let k = ru.one_s_ge in
- let l = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Uk = merge_closures (fun x -> x.gt_closure) k m in
- let _Ul = merge_closures (fun x -> x.gt_closure) l m in
- let one_step_gt = ru.one_s_gt in
- (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
- in
- {
- eq_closure = eq_c;
- ge_closure = ge_c;
- gt_closure = gt_c;
- in_gegt_of = ru.in_gegt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = ru.one_s_gt
- }
-
-let rec simple_adjust m =
- let m' =
- MAL.mapi (fun x _ -> closure_of x m) m
- in
- if not (are_ugraph_eq m m') then(
- simple_adjust m')
- else
- m'
-
-let add_eq_arc u v m =
- let ru = repr u m in
- let rv = repr v m in
- let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
- let m' = MAL.add u ru' m in
- let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
- let m'' = MAL.add v rv' m' in
- simple_adjust m''
-
-let add_ge_arc u v m =
- let ru = repr u m in
- let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
- let m' = MAL.add u ru' m in
- simple_adjust m'
-
-let add_gt_arc u v m =
- let ru = repr u m in
- let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
- let m' = MAL.add u ru' m in
- simple_adjust m'
-
-\f
-(*****************************************************************************)
-(** Outhern interface, that chooses between _fast and safe **)
-(*****************************************************************************)
-
-(*
- given the 2 nodes plus the current bag, adds the arc, recomputes the
- closures and returns the new map
-*)
-let add_eq fast u v b =
- if fast then
- add_eq_arc_fast u v b
- else
- add_eq_arc u v b
-
-(*
- given the 2 nodes plus the current bag, adds the arc, recomputes the
- closures and returns the new map
-*)
-let add_ge fast u v b =
- if fast then
- add_ge_arc_fast u v b
- else
- add_ge_arc u v b
-(*
- given the 2 nodes plus the current bag, adds the arc, recomputes the
- closures and returns the new map
-*)
-let add_gt fast u v b =
- if fast then
- add_gt_arc_fast u v b
- else
- add_gt_arc u v b
-
-
-(*****************************************************************************)
-(** Other real code **)
-(*****************************************************************************)
-
-exception UniverseInconsistency of string
-
-let error arc node1 closure_type node2 closure =
- let s = "\n ===== Universe Inconsistency detected =====\n\n" ^
- " Unable to add\n" ^
- "\t" ^ (string_of_arc arc) ^ "\n" ^
- " cause\n" ^
- "\t" ^ (string_of_universe node1) ^ "\n" ^
- " is in the " ^ closure_type ^ " closure\n" ^
- "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^
- " of\n" ^
- "\t" ^ (string_of_universe node2) ^ "\n\n" ^
- " ===== Universe Inconsistency detected =====\n" in
- prerr_endline s;
- raise (UniverseInconsistency s)
-
-
-let fill_empty_nodes_with_uri (g, already_contained) l uri =
- let fill_empty_universe u =
- match u with
- (i,None) -> (i,Some uri)
- | (i,Some _) as u -> u
- in
- let fill_empty_set s =
- SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
- in
- let fill_empty_entry e = {
- eq_closure = (fill_empty_set e.eq_closure) ;
- ge_closure = (fill_empty_set e.ge_closure) ;
- gt_closure = (fill_empty_set e.gt_closure) ;
- in_gegt_of = (fill_empty_set e.in_gegt_of) ;
- one_s_eq = (fill_empty_set e.one_s_eq) ;
- one_s_ge = (fill_empty_set e.one_s_ge) ;
- one_s_gt = (fill_empty_set e.one_s_gt) ;
- } in
- let m = g in
- let m' = MAL.fold (
- fun k v m ->
- MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
- in
- let l' = List.map fill_empty_universe l in
- (m', already_contained),l'
-
-
-(*****************************************************************************)
-(** World interface **)
-(*****************************************************************************)
-
-type universe_graph = bag * UriManager.UriSet.t
-(* the graph , the cache of already merged ugraphs *)
-
-let empty_ugraph = empty_bag, UriManager.UriSet.empty
-
-let current_index_anon = ref (-1)
-let current_index_named = ref (-1)
-
-let restart_numbering () = current_index_named := (-1)
-
-let fresh ?uri ?id () =
- let i =
- match uri,id with
- | None,None ->
- current_index_anon := !current_index_anon + 1;
- !current_index_anon
- | None, Some _ -> assert false
- | Some _, None ->
- current_index_named := !current_index_named + 1;
- !current_index_named
- | Some _, Some id -> id
- in
- (i,uri)
-
-let name_universe u uri =
- match u with
- | (i, None) -> (i, Some uri)
- | _ -> u
-
-let print_ugraph (g, _) =
- prerr_endline (string_of_bag g)
-
-let add_eq ?(fast=(!fast_implementation)) u v b =
- (* should we check to no add twice the same?? *)
- let m = b in
- let ru = repr u m in
- if SOF.mem v ru.gt_closure then
- error ("EQ",u,v) v "GT" u ru.gt_closure
- else
- begin
- let rv = repr v m in
- if SOF.mem u rv.gt_closure then
- error ("EQ",u,v) u "GT" v rv.gt_closure
- else
- add_eq fast u v b
- end
-
-let add_ge ?(fast=(!fast_implementation)) u v b =
- (* should we check to no add twice the same?? *)
- let m = b in
- let rv = repr v m in
- if SOF.mem u rv.gt_closure then
- error ("GE",u,v) u "GT" v rv.gt_closure
- else
- add_ge fast u v b
-
-let add_gt ?(fast=(!fast_implementation)) u v b =
- (* should we check to no add twice the same?? *)
- (*
- FIXME : check the thesis... no need to check GT and EQ closure since the
- GE is a superset of both
- *)
- let m = b in
- let rv = repr v m in
-
- if u = v then
- error ("GT",u,v) u "==" v SOF.empty
- else
-
- (*if SOF.mem u rv.gt_closure then
- error ("GT",u,v) u "GT" v rv.gt_closure
- else
- begin*)
- if SOF.mem u rv.ge_closure then
- error ("GT",u,v) u "GE" v rv.ge_closure
- else
-(* begin
- if SOF.mem u rv.eq_closure then
- error ("GT",u,v) u "EQ" v rv.eq_closure
- else*)
- add_gt fast u v b
-(* end
- end*)
-
-(*****************************************************************************)
-(** START: Decomment this for performance comparisons **)
-(*****************************************************************************)
-
-let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained) =
- (*prerr_endline "add_eq";*)
- begin_spending ();
- let rc = add_eq ~fast u v b in
- end_spending ();
- rc,already_contained
-
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) =
-(* prerr_endline "add_ge"; *)
- begin_spending ();
- let rc = add_ge ~fast u v b in
- end_spending ();
- rc,already_contained
-
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) =
-(* prerr_endline "add_gt"; *)
- begin_spending ();
- let rc = add_gt ~fast u v b in
- end_spending ();
- rc,already_contained
-
-let profiler_eq = HExtlib.profile "CicUniv.add_eq"
-let profiler_ge = HExtlib.profile "CicUniv.add_ge"
-let profiler_gt = HExtlib.profile "CicUniv.add_gt"
-let add_gt ?fast u v b =
- profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) ()
-let add_ge ?fast u v b =
- profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
-let add_eq ?fast u v b =
- profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
-
-(*****************************************************************************)
-(** END: Decomment this for performance comparisons **)
-(*****************************************************************************)
-
-let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
- let merge_brutal (u,_) v =
- let m1 = u in
- let m2 = v in
- MAL.fold (
- fun k v x ->
- (SOF.fold (
- fun u x ->
- let m = add_gt k u x in m)
- (SOF.union v.one_s_gt v.gt_closure)
- (SOF.fold (
- fun u x ->
- let m = add_ge k u x in m)
- (SOF.union v.one_s_ge v.ge_closure)
- (SOF.fold (
- fun u x ->
- let m = add_eq k u x in m)
- (SOF.union v.one_s_eq v.eq_closure) x)))
- ) m1 m2
- in
- let base, already_contained = base_ugraph in
- if MAL.is_empty base then
- increment
- else if
- MAL.is_empty (fst increment) ||
- UriManager.UriSet.mem uri_of_increment already_contained
- then
- base_ugraph
- else
- fst (merge_brutal increment base_ugraph),
- UriManager.UriSet.add uri_of_increment already_contained
-
-let profiler_merge = HExtlib.profile "CicUniv.merge_graphs"
-let merge_ugraphs ~base_ugraph ~increment =
- profiler_merge.HExtlib.profile
- (fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
-
-(*****************************************************************************)
-(** Xml sesialization and parsing **)
-(*****************************************************************************)
-
-let xml_of_universe name u =
- match u with
- | (i,Some u) ->
- Xml.xml_empty name [
- None,"id",(string_of_int i) ;
- None,"uri",(UriManager.string_of_uri u)]
- | (_,None) ->
- raise (Failure "we can serialize only universes with uri")
-
-let xml_of_set s =
- let l =
- List.map (xml_of_universe "node") (SOF.elements s)
- in
- List.fold_left (fun s x -> [< s ; x >] ) [<>] l
-
-let xml_of_entry_content e =
- let stream_of_field f name =
- let eq_c = xml_of_set f in
- if eq_c != [<>] then
- Xml.xml_nempty name [] eq_c
- else
- [<>]
- in
- [<
- (stream_of_field e.eq_closure "eq_closure");
- (stream_of_field e.gt_closure "gt_closure");
- (stream_of_field e.ge_closure "ge_closure");
- (stream_of_field e.in_gegt_of "in_gegt_of");
- (stream_of_field e.one_s_eq "one_s_eq");
- (stream_of_field e.one_s_gt "one_s_gt");
- (stream_of_field e.one_s_ge "one_s_ge")
- >]
-
-let xml_of_entry u e =
- let (i,u') = u in
- let u'' =
- match u' with
- Some x -> x
- | None ->
- raise (Failure "we can serialize only universes (entry) with uri")
- in
- let ent = Xml.xml_nempty "entry" [
- None,"id",(string_of_int i) ;
- None,"uri",(UriManager.string_of_uri u'')] in
- let content = xml_of_entry_content e in
- ent content
-
-let write_xml_of_ugraph filename (m,_) l =
- let tokens =
- [<
- Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
- Xml.xml_nempty "ugraph" []
- ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ;
- (List.fold_left
- (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>]
- in
- Xml.pp ~gzip:true tokens (Some filename)
-
-let univno = fst
-
-
-let rec clean_ugraph (m,already_contained) f =
- let m' =
- MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
- let m'' = MAL.fold (fun k v x ->
- let v' = {
- eq_closure = SOF.filter f v.eq_closure;
- ge_closure = SOF.filter f v.ge_closure;
- gt_closure = SOF.filter f v.gt_closure;
- in_gegt_of = SOF.filter f v.in_gegt_of;
- one_s_eq = SOF.filter f v.one_s_eq;
- one_s_ge = SOF.filter f v.one_s_ge;
- one_s_gt = SOF.filter f v.one_s_gt
- } in
- MAL.add k v' x ) m' MAL.empty in
- let e_l =
- MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
- begin
- k::l end else l) m'' []
- in
- if e_l != [] then
- clean_ugraph
- (m'', already_contained) (fun u -> (f u) && not (List.mem u e_l))
- else
- MAL.fold
- (fun k v x -> if v <> empty_entry then MAL.add k v x else x)
- m'' MAL.empty,
- already_contained
-
-let clean_ugraph g l =
- clean_ugraph g (fun u -> List.mem u l)
-
-let assigner_of =
- function
- "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
- | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
- | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
- | "in_gegt_of" -> (fun e u->{e with in_gegt_of =SOF.add u e.in_gegt_of})
- | "one_s_ge" -> (fun e u->{e with one_s_ge =SOF.add u e.one_s_ge})
- | "one_s_gt" -> (fun e u->{e with one_s_gt =SOF.add u e.one_s_gt})
- | "one_s_eq" -> (fun e u->{e with one_s_eq =SOF.add u e.one_s_eq})
- | s -> raise (Failure ("unsupported tag " ^ s))
-;;
-
-let cb_factory m l =
- let module XPP = XmlPushParser in
- let current_node = ref (0,None) in
- let current_entry = ref empty_entry in
- let current_assign = ref (assigner_of "in_gegt_of") in
- { XPP.default_callbacks with
- XPP.end_element = Some( fun name ->
- match name with
- | "entry" ->
- m := MAL.add !current_node !current_entry !m;
- current_entry := empty_entry
- | _ -> ()
- );
- XPP.start_element = Some( fun name attlist ->
- match name with
- | "ugraph" -> ()
- | "entry" ->
- let id = List.assoc "id" attlist in
- let uri = List.assoc "uri" attlist in
- current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
- | "node" ->
- let id = int_of_string (List.assoc "id" attlist) in
- let uri = List.assoc "uri" attlist in
- current_entry := !current_assign !current_entry
- (id,Some (UriManager.uri_of_string uri))
- | "owned_node" ->
- let id = int_of_string (List.assoc "id" attlist) in
- let uri = List.assoc "uri" attlist in
- l := (id,Some (UriManager.uri_of_string uri)) :: !l
- | s -> current_assign := assigner_of s
- )
- }
-;;
-
-let ugraph_and_univlist_of_xml filename =
- let module XPP = XmlPushParser in
- let result_map = ref MAL.empty in
- let result_list = ref [] in
- let cb = cb_factory result_map result_list in
- let xml_parser = XPP.create_parser cb in
- let xml_source = `Gzip_file filename in
- (try XPP.parse xml_parser xml_source
- with (XPP.Parse_error err) as exn -> raise exn);
- (!result_map,UriManager.UriSet.empty), !result_list
-
-\f
-(*****************************************************************************)
-(** the main, only for testing **)
-(*****************************************************************************)
-
-(*
-
-type arc = Ge | Gt | Eq ;;
-
-let randomize_actionlist n m =
- let ge_percent = 0.7 in
- let gt_percent = 0.15 in
- let random_step () =
- let node1 = Random.int m in
- let node2 = Random.int m in
- let op =
- let r = Random.float 1.0 in
- if r < ge_percent then
- Ge
- else (if r < (ge_percent +. gt_percent) then
- Gt
- else
- Eq)
- in
- op,node1,node2
- in
- let rec aux n =
- match n with
- 0 -> []
- | n -> (random_step ())::(aux (n-1))
- in
- aux n
-
-let print_action_list l =
- let string_of_step (op,node1,node2) =
- (match op with
- Ge -> "Ge"
- | Gt -> "Gt"
- | Eq -> "Eq") ^
- "," ^ (string_of_int node1) ^ "," ^ (string_of_int node2)
- in
- let rec aux l =
- match l with
- [] -> "]"
- | a::tl ->
- ";" ^ (string_of_step a) ^ (aux tl)
- in
- let body = aux l in
- let l_body = (String.length body) - 1 in
- prerr_endline ("[" ^ (String.sub body 1 l_body))
-
-let debug = false
-let d_print_endline = if debug then print_endline else ignore
-let d_print_ugraph = if debug then print_ugraph else ignore
-
-let _ =
- (if Array.length Sys.argv < 2 then
- prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
- Random.self_init ();
- let max_edges = int_of_string Sys.argv.(1) in
- let max_nodes = int_of_string Sys.argv.(2) in
- let action_listR = randomize_actionlist max_edges max_nodes in
-
- let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
- let action_list = action_listR in
-
- print_action_list action_list;
- let prform_step ?(fast=false) (t,u,v) g =
- let f,str =
- match t with
- Ge -> add_ge,">="
- | Gt -> add_gt,">"
- | Eq -> add_eq,"="
- in
- d_print_endline (
- "Aggiungo " ^
- (string_of_int u) ^
- " " ^ str ^ " " ^
- (string_of_int v));
- let g' = f ~fast (u,None) (v,None) g in
- (*print_ugraph g' ;*)
- g'
- in
- let fail = ref false in
- let time1 = Unix.gettimeofday () in
- let n_safe = ref 0 in
- let g_safe =
- try
- d_print_endline "SAFE";
- List.fold_left (
- fun g e ->
- n_safe := !n_safe + 1;
- prform_step e g
- ) empty_ugraph action_list
- with
- UniverseInconsistency s -> fail:=true;empty_bag
- in
- let time2 = Unix.gettimeofday () in
- d_print_ugraph g_safe;
- let time3 = Unix.gettimeofday () in
- let n_test = ref 0 in
- let g_test =
- try
- d_print_endline "FAST";
- List.fold_left (
- fun g e ->
- n_test := !n_test + 1;
- prform_step ~fast:true e g
- ) empty_ugraph action_list
- with
- UniverseInconsistency s -> empty_bag
- in
- let time4 = Unix.gettimeofday () in
- d_print_ugraph g_test;
- if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
- begin
- let num_eq =
- List.fold_left (
- fun s (e,_,_) ->
- if e = Eq then s+1 else s
- ) 0 action_list
- in
- let num_gt =
- List.fold_left (
- fun s (e,_,_) ->
- if e = Gt then s+1 else s
- ) 0 action_list
- in
- let num_ge = max_edges - num_gt - num_eq in
- let time_fast = (time4 -. time3) in
- let time_safe = (time2 -. time1) in
- let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
- let fail = if !fail then 1 else 0 in
- print_endline
- (sprintf
- "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d"
- fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
- exit 0
- end
- else
- begin
- print_endline "FAIL";
- print_ugraph g_safe;
- print_ugraph g_test;
- exit 1
- end
-;;
-
- *)
-
-let recons_univ u =
- match u with
- | i, None -> u
- | i, Some uri ->
- i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
-
-let recons_entry entry =
- let recons_set set =
- SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
- in
- {
- eq_closure = recons_set entry.eq_closure;
- ge_closure = recons_set entry.ge_closure;
- gt_closure = recons_set entry.gt_closure;
- in_gegt_of = recons_set entry.in_gegt_of;
- one_s_eq = recons_set entry.one_s_eq;
- one_s_ge = recons_set entry.one_s_ge;
- one_s_gt = recons_set entry.one_s_gt;
- }
-
-let recons_graph (graph,uriset) =
- MAL.fold
- (fun universe entry map ->
- MAL.add (recons_univ universe) (recons_entry entry) map)
- graph
- MAL.empty,
- UriManager.UriSet.fold
- (fun u acc ->
- UriManager.UriSet.add
- (UriManager.uri_of_string (UriManager.string_of_uri u)) acc)
- uriset UriManager.UriSet.empty
-
-let assert_univ u =
- match u with
- | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
- | _ -> ()
-
-let assert_univs_have_uri (graph,_) univlist =
- let assert_set s =
- SOF.iter (fun u -> assert_univ u) s
- in
- let assert_entry e =
- assert_set e.eq_closure;
- assert_set e.ge_closure;
- assert_set e.gt_closure;
- assert_set e.in_gegt_of;
- assert_set e.one_s_eq;
- assert_set e.one_s_ge;
- assert_set e.one_s_gt;
- in
- MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
- List.iter assert_univ univlist
-
-let eq u1 u2 =
- match u1,u2 with
- | (id1, Some uri1),(id2, Some uri2) ->
- id1 = id2 && UriManager.eq uri1 uri2
- | (id1, None),(id2, None) -> id1 = id2
- | _ -> false
-
-let compare (id1, uri1) (id2, uri2) =
- let cmp = id1 - id2 in
- if cmp = 0 then
- match uri1,uri2 with
- | None, None -> 0
- | Some _, None -> 1
- | None, Some _ -> ~-1
- | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
- else
- cmp
-
-(* EOF *)
projects / helm.git / blobdiff