* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Enrico Tassi <tassi@cs.unibo.it> *)
-(* 23/04/2004 *)
-(* *)
-(* This module implements the aciclic graph of universes. *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Enrico Tassi <tassi@cs.unibo.it> *)
+(* 23/04/2004 *)
+(* *)
+(* This module implements the aciclic graph of universes. *)
+(* *)
+(*****************************************************************************)
+
+(*****************************************************************************)
+(** switch implementation **)
+(*****************************************************************************)
+
+let fast_implementation = ref false ;;
+
+(*****************************************************************************)
+(** open **)
+(*****************************************************************************)
open Printf
-(******************************************************************************)
-(** Types and default values **)
-(******************************************************************************)
-
-type universe = int
+(*****************************************************************************)
+(** 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_eq_of : SOF.t;
- in_ge_of : SOF.t;
- in_gt_of : SOF.t;
- one_s_eq : SOF.t;
- one_s_ge : SOF.t;
- one_s_gt : SOF.t;
+ 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 arc = arc_type * universe * universe
-
-type bag = entry MAL.t * (arc list)
-
+
+type bag = entry MAL.t
+
let empty_entry = {
- eq_closure=SOF.empty;
- ge_closure=SOF.empty;
- gt_closure=SOF.empty;
- in_eq_of=SOF.empty;
- in_ge_of=SOF.empty;
- in_gt_of=SOF.empty;
- one_s_eq=SOF.empty;
- one_s_ge=SOF.empty;
- one_s_gt=SOF.empty;
+ 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 empty_bag = (MAL.empty, [])
+let are_set_eq s1 s2 =
+ SOF.equal s1 s2
-let env_bag = ref empty_bag
+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 )
-(******************************************************************************)
-(** Pretty printings **)
-(******************************************************************************)
-let string_of_universe u = string_of_int u
-
-let string_of_arc_type u =
+(* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *)
+(*
+ let are_ugraph_eq308 g h =
+ MAL.equal are_entry_eq g h
+*)
+let are_ugraph_eq307 g h =
+ try
+ MAL.fold (
+ fun k v b ->
+ if not b then
+ raise (Failure "Different")
+ else
+ try
+ let k_h = MAL.find k h in
+ are_entry_eq v k_h
+ with Not_found -> true
+ ) g true
+ with
+ Failure "Different" -> false
+
+let are_ugraph_eq = are_ugraph_eq307
+
+(*****************************************************************************)
+(** Pretty printings **)
+(*****************************************************************************)
+
+let string_of_universe (i,u) =
match u with
- EQ -> "EQ"
- | GT -> "GT"
- | GE -> "EQ"
-
-let string_of_arc u =
- let atype,a,b = u in
- (string_of_arc_type atype) ^ " " ^
- (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; "
-;;
+ Some u ->
+ ((string_of_int i) ^ " " ^ (UriManager.string_of_uri u))
+ | None -> (string_of_int i)
let string_of_universe_set l =
SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
-let string_of_arc_list l =
- List.fold_left (fun s x -> s ^ (string_of_arc 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_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^
- "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^
- "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n"
+ "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 "%d --> %s" k (string_of_node v)) m;
+ 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 =
- let (m,l) = b in
- let s_m = string_of_mal m in
- let s_l = string_of_arc_list l in
- s_m ^"["^s_l^"]"
+ string_of_mal b
-(******************************************************************************)
-(** Helpers **)
-(******************************************************************************)
+(*****************************************************************************)
+(** Helpers **)
+(*****************************************************************************)
-(*
- we need to merge the 2 graphs... here the code
-*)
+(* find the repr *)
let repr u m =
try
MAL.find u m
with
- Not_found ->
- try
- let m',_ = !env_bag in
- MAL.find u m'
- with
- Not_found -> empty_entry
+ Not_found -> empty_entry
-(*
- FIXME: May be faster if we make it by hand
-*)
+(* 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
-(******************************************************************************)
-(** Real stuff GT **)
-(******************************************************************************)
+(*****************************************************************************)
+(** 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 ()
+;;
-(*
- todo is the SOF of nodes that needs to be recomputed,
- m is the MAL map, s is the already touched nodes
-*)
-let rec redo_gt_closure todo m s =
- if SOF.is_empty todo then m
- else
- begin
- (* we choose the node to recompute *)
- let u = SOF.choose todo in
- if not (SOF.mem u s) then
- let ru = repr u m in
- let ru' = {ru with gt_closure =
- (* the new gt closure is the gt-closures + ge-closures + eq-closures
- of the one step gt-connected nodes *)
- SOF.union ru.one_s_gt (merge_closures
- (fun x -> SOF.union x.eq_closure
- (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in
- let m' = MAL.add u ru' m in
- let s' = SOF.add u s in
- redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s'
+let end_spending () =
+ assert (!partial > 0.0);
+ let interval = (Unix.gettimeofday ()) -. !partial in
+ partial := 0.0;
+ time_spent := !time_spent +. interval
+;;
+
+\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
- (* if already done go next. FIXME: think if it is right
- maybe we should check if we changed something or not *)
- redo_gt_closure (SOF.remove u todo) m s
- end
+ 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''
-(*
- calculates the closures of u and adjusts the in_*_of of v, then
- starts redo_*_closure to adjust the colure of nodew thet have
- (clusure u) in theyr closures
-*)
-let add_gt_arc u v m =
+and add_eq_arc_fast u v m =
let ru = repr u m in
let rv = repr v m in
- let ru' = {
- (* new node: we add the v gt-closure and v to our gt-closure *)
- eq_closure = ru.eq_closure;
- ge_closure = ru.ge_closure;
- gt_closure = SOF.add v
- (SOF.union ru.gt_closure
- (SOF.union rv.ge_closure
- (SOF.union rv.eq_closure rv.gt_closure)));
- in_eq_of = ru.in_eq_of;
- in_ge_of = ru.in_ge_of;
- in_gt_of = ru.in_gt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = SOF.add v ru.one_s_gt;
- } in
- (* may add the sanity check *)
- let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } 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
- redo_gt_closure ru'.in_gt_of m'' SOF.empty
-
-(*
- given the 2 nodes plus the current bag, adds the arc, recomputes the
- closures and returns the new map
-*)
-let add_gt u v b =
- let m,l = b in
- let m' = add_gt_arc u v m in
- let l' = (GT,u,v)::l in
- (m',l')
+ adjust_fast v (*(adjust_fast u*) m'' (* ) *)
+;;
-(******************************************************************************)
-(** Real stuff GE **)
-(******************************************************************************)
+\f
+(*****************************************************************************)
+(** safe implementation **)
+(*****************************************************************************)
-(*
- todo is the SOF of nodes that needs to be recomputed,
- m is the MAL map, s is the already touched nodes
-*)
-let rec redo_ge_closure todo m s =
- if SOF.is_empty todo then m,s
- else
- begin
- let u = SOF.choose todo in
- if not (SOF.mem u s) then
- begin
- let ru = repr u m in
- (* the ge-closure is recomputed as the ge-closures of
- ge connected nodes plus theys eq-closure *)
- let ru' = {ru with ge_closure = merge_closures
- (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in
- let m' = MAL.add u ru' m in
- let s' = SOF.add u s in
- redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s'
- end
+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
- redo_ge_closure (SOF.remove u todo) m s
- end
+ m'
-(*
- calculates the closures of u and adjusts the in_*_of of v, then
- starts redo_*_closure to adjust the colure of nodew thet have
- (clusure u) in theyr closures
-*)
-let add_ge_arc u v m =
+let add_eq_arc u v m =
let ru = repr u m in
- let rv = repr v m in
- let ru' = {
- eq_closure = ru.eq_closure;
- ge_closure = SOF.add v
- (SOF.union ru.ge_closure
- (SOF.union rv.eq_closure rv.ge_closure));
- gt_closure = ru.gt_closure;
- in_eq_of = ru.in_eq_of;
- in_ge_of = ru.in_ge_of;
- in_gt_of = ru.in_gt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = SOF.add v ru.one_s_ge;
- one_s_gt = ru.one_s_gt;
- } in
- let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } 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
- let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
- (* closing ge may provoke aome changes in gt-closures *)
- redo_gt_closure (SOF.union ru'.in_gt_of
- (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of))
- td SOF.empty )) m''' SOF.empty
+ 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_ge u v b =
- let m,l = b in
- let m' = add_ge_arc u v m in
- let l' = (GE,u,v)::l in
- (m',l')
-
-(******************************************************************************)
-(** Real stuff EQ **)
-(******************************************************************************)
-
-let rec redo_eq_closure todo m s =
- if SOF.is_empty todo then m,s
- else begin
- let u = SOF.choose todo in
- if not (SOF.mem u s) then
- begin
- let ru = repr u m in
- let eq_closure = merge_closures
- (fun x -> x.eq_closure) ru.one_s_eq m in
- let ru' = {ru with eq_closure = eq_closure
- ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
- let m' = MAL.add u ru' m in
- let s' = SOF.add u s in
- redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
- end
- else
- redo_eq_closure (SOF.remove u todo) m s
- end
-
-(*
- calculates the closures of u and adjusts the in_*_of of v, then
- starts redo_*_closure to adjust the colure of nodew thet have
- (clusure u) in theyr closures
-*)
-let add_eq_arc u v m =
- let ru = repr u m in
- let rv = repr v m in
- (* since eq is symmetric we have to chage more *)
- let eq_closure = SOF.add u (SOF.add v
- (SOF.union ru.eq_closure rv.eq_closure)) in
- let ru' = {
- eq_closure = eq_closure;
- ge_closure = SOF.union ru.ge_closure rv.ge_closure;
- gt_closure = SOF.union ru.gt_closure rv.gt_closure;
- in_eq_of = eq_closure;
- in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
- in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
- one_s_eq = eq_closure;
- one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
- one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
- } in
- (* this is a collapse *)
- let rv' = ru' in
- let m' = MAL.add u ru' m in
- let m'' = MAL.add v rv' m' in
- let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
- (* redoing a eq may change some ge and some gt *)
- let m'''',td' = redo_ge_closure
- (SOF.union ru'.in_ge_of
- (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of))
- td SOF.empty)) m''' SOF.empty in
- redo_gt_closure (SOF.union ru'.in_gt_of
- (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of))
- td' SOF.empty)) m'''' SOF.empty
+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_eq u v b =
- let m,l = b in
- let m' = add_eq_arc u v m in
- let l' = (EQ,u,v)::l in
- (m',l')
+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
+
-(******************************************************************************)
-(** Oyther real code **)
-(******************************************************************************)
+(*****************************************************************************)
+(** Other real code **)
+(*****************************************************************************)
exception UniverseInconsistency of string
let error arc node1 closure_type node2 closure =
- let s = " ===== Universe Inconsistency detected =====\n\n" ^
- "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^
+ let s = "\n ===== Universe Inconsistency detected =====\n\n" ^
+ "\tUnable to add "^ (string_of_arc arc) ^ " cause " ^
(string_of_universe node1) ^ " is in the " ^
- (string_of_arc_type closure_type) ^ " closure {" ^
+ closure_type ^ " closure {" ^
(string_of_universe_set closure) ^ "} of " ^
(string_of_universe node2) ^ "\n\n" ^
" ===== Universe Inconsistency detected =====\n" in
prerr_endline s;
raise (UniverseInconsistency s)
-(*
- we merge the env_bag with b
-*)
-let qed b =
- let m,l = b in
- let m',l' = !env_bag in
- let m'' = ref m' in
- MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
- let l'' = l @ l' in
- env_bag := (!m'',l'')
-
-let add_eq u v b =
+
+let fill_empty_nodes_with_uri g 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
+ m'
+
+
+(*****************************************************************************)
+(** World interface **)
+(*****************************************************************************)
+
+type universe_graph = bag
+
+let empty_ugraph = empty_bag
+
+let current_index = ref (-1)
+
+let restart_numbering () = current_index := (-1)
+
+let fresh () =
+ current_index := !current_index + 1;
+ (!current_index,None)
+
+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 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
+ 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
+ error ("EQ",u,v) u "GT" v rv.gt_closure
else
- add_eq u v b
+ add_eq fast u v b
end
-let add_ge u v b =
+let add_ge ?(fast=(!fast_implementation)) u v b =
(* should we check to no add twice the same?? *)
- let m,_ = b in
+ 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
+ error ("GE",u,v) u "GT" v rv.gt_closure
else
- add_ge u v b
+ add_ge fast u v b
-let add_gt u v b =
+let add_gt ?(fast=(!fast_implementation)) u v b =
(* should we check to no add twice the same?? *)
- let m,_ = b in
+ (*
+ 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 SOF.mem u rv.gt_closure then
- error (GT,u,v) u GT v rv.gt_closure
+
+ if u = v then
+ error ("GT",u,v) u "==" v SOF.empty
else
- begin
+
+ (*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
+ error ("GT",u,v) u "GE" v rv.ge_closure
else
- begin
+(* begin
if SOF.mem u rv.eq_closure then
- error (GT,u,v) u EQ v rv.eq_closure
- else
- add_gt u v b
- end
- end
-
-
-
-(******************************************************************************)
-(** World interface **)
-(******************************************************************************)
-
-type universe_graph = bag
-
-let work_bag = ref empty_bag
-let current_index = ref (-1)
-
-let get_working () = !work_bag
-let get_global () = !env_bag
-let set_working b = work_bag := b
+ 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 =
+ begin_spending ();
+ let rc = add_eq ~fast u v b in
+ end_spending();
+ rc
+
+let add_ge ?(fast=(!fast_implementation)) u v b =
+ begin_spending ();
+ let rc = add_ge ~fast u v b in
+ end_spending();
+ rc
+
+let add_gt ?(fast=(!fast_implementation)) u v b =
+ begin_spending ();
+ let rc = add_gt ~fast u v b in
+ end_spending();
+ rc
+
+(*****************************************************************************)
+(** END: Decomment this for performance comparisons **)
+(*****************************************************************************)
+
+let merge_ugraphs u v =
+ (* this sucks *)
+ let merge_brutal u v =
+ if u = empty_bag then v
+ else if v = empty_bag then u
+ else
+ 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) v.one_s_gt
+ (SOF.fold (
+ fun u x ->
+ let m = add_ge k u x in m) v.one_s_ge
+ (SOF.fold (
+ fun u x ->
+ let m = add_eq k u x in m) v.one_s_eq x)))
+ ) m1 m2
+ in
+ merge_brutal u v
+
+
+(*****************************************************************************)
+(** Xml sesialization and parsing **)
+(*****************************************************************************)
+
+let xml_of_set s =
+ let l =
+ List.map (
+ function
+ (i,Some u) ->
+ Xml.xml_empty "node" [
+ None,"id",(string_of_int i) ;
+ None,"uri",(UriManager.string_of_uri u)]
+ | (_,None) ->
+ raise (Failure "we can serialize only universes with uri")
+ ) (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 =
+ let o = open_out filename in
+ output_string o "<?xml version=\"1.0\" encoding=\"iso-8859-1\" ?>\n";
+ Xml.pp_to_outchan (
+ Xml.xml_nempty "ugraph" [] (
+ MAL.fold (
+ fun k v s -> [< s ; (xml_of_entry k v) >])
+ m [<>])) o;
+ close_out o
+
+let rec clean_ugraph m 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 then k::l else l) m'' []
+ in
+ if e_l != [] then
+ clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
+ else
+ m''
+
+let clean_ugraph g l =
+ clean_ugraph g (fun u -> List.mem u l)
+
+open Pxp_types ;;
+
+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 fresh () =
- current_index := !current_index + 1;
- !current_index
+let cb_factory m =
+ let current_node = ref (0,None) in
+ let current_entry = ref empty_entry in
+ let current_assign = ref (assigner_of "in_ge_of") in
+ function
+ | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
+ | E_start_tag ("entry",attlist,_,_) ->
+ 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))
+ | E_start_tag ("node",attlist,_,_) ->
+ 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))
+ | E_start_tag (s,_,_,_) ->
+ current_assign := assigner_of s
+ | E_end_tag ("entry",_) ->
+ m := MAL.add !current_node !current_entry !m;
+ current_entry := empty_entry
+ | _ -> ()
+;;
+
+(* alternative implementation *)
+let mapl = [
+ ("ge_closure",0);("gt_closure",1);("eq_closure",2);
+ ("in_gegt_of", 3);
+ ("one_s_ge", 4);("one_s_gt", 5);("one_s_eq", 6)]
+;;
-let qed () =
- qed !work_bag
+let assigner_of' s = List.assoc s mapl ;;
-let print_global_graph () =
- let s = string_of_bag !env_bag in
- prerr_endline s
+let entry_of_array a = {
+ ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
+ in_gegt_of = a.(3);
+ one_s_ge = a.(4); one_s_gt = a.(5); one_s_eq = a.(6)}
+;;
-let print_working_graph () =
- let s = string_of_bag !work_bag in
- prerr_endline s
+let cb_factory' m =
+ let current_node = ref (0,None) in
+ let current_entry = Array.create 7 SOF.empty in
+ let current_assign = ref 0 in
+ function
+ | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
+ | E_start_tag ("entry",attlist,_,_) ->
+ 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))
+ | E_start_tag ("node",attlist,_,_) ->
+ let id = int_of_string (List.assoc "id" attlist) in
+ let uri = List.assoc "uri" attlist in
+ current_entry.(!current_assign) <-
+ SOF.add (id,Some (UriManager.uri_of_string uri))
+ current_entry.(!current_assign)
+ | E_start_tag (s,_,_,_) ->
+ current_assign := assigner_of' s
+ | E_end_tag ("entry",_) ->
+ m := MAL.add !current_node (entry_of_array current_entry) !m;
+ Array.fill current_entry 0 7 SOF.empty
+ | _ -> ()
+;;
-type history_ticket = int
+
+let ugraph_of_xml filename =
+ let module PX = Pxp_ev_parser in
+ let module NE = Netconversion in
+ let config = default_config in
+ let entry = `Entry_document [] in
+ let encoding = `Enc_iso88591 in
+ let source = from_file ~system_encoding:encoding filename in
+ let entity_manager =
+ PX.create_entity_manager ~is_document:true config source in
+ let result = ref MAL.empty in
+ let cb = cb_factory result in
+(*let cb = cb_factory' result in*)
+ PX.process_entity config entry entity_manager cb;
+ !result
+
+\f
+(*****************************************************************************)
+(** the main, only for testing **)
+(*****************************************************************************)
-let get_history_ticket b =
- let m,l = b in
- List.length l
+(*
-let redo_history t b b'=
- let rec get_history l n =
- if n == 0 then
- []
+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
- match l with
- [] -> failwith "erroer, lista piu' corta della history"
- | h::tl -> h::(get_history tl (n - 1))
+ print_endline "FAIL";
+ print_ugraph g_safe;
+ print_ugraph g_test;
+ exit 1
end
- in
- let rec redo_commands l b =
- match l with
- [] -> b
- | (GE,u,v)::tl -> redo_commands tl (add_ge u v b)
- | (GT,u,v)::tl -> redo_commands tl (add_gt u v b)
- | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b)
- in
- let (m,l) = b in
- let todo = List.rev (get_history l ((List.length l) - t)) in
- try
- redo_commands todo b'
- with
- UniverseInconsistency s -> failwith s
- (*| _ -> failwith "Unexpected exception"*)
-
-let add_gt u v =
- try
- work_bag := add_gt u v !work_bag; true
- with
- UniverseInconsistency s -> false
- (*| _ -> failwith "Unexpected exception"*)
-
-let add_ge u v =
- try
- work_bag := add_ge u v !work_bag;true
- with
- UniverseInconsistency s -> false
- (*| _ -> failwith "Unexpected exception"*)
-
-let add_eq u v =
- try
- work_bag := add_eq u v !work_bag;true
- with
- UniverseInconsistency s -> false
- (*| _ -> failwith "Unexpected exception"*)
+;;
-let saved_data = ref (empty_bag,0)
+ *)
-let directly_to_env_begin () =
- saved_data := (!work_bag, get_history_ticket !env_bag);
- work_bag := empty_bag
-
-let directly_to_env_end () =
- qed ();
- let (b,t) = !saved_data in
- work_bag := redo_history t !env_bag b
-
-let reset_working () = work_bag := empty_bag
-
-(******************************************************************************)
-(** Fake implementatoin **)
-(******************************************************************************)
-
-let reset_working = function _ -> ()
-let directly_to_env_end = function _ -> ()
-let directly_to_env_begin = function _ -> ()
-let add_eq = fun _ _ -> true
-let add_ge = fun _ _ -> true
-let add_gt = fun _ _ -> true
-let get_working = function a -> empty_bag
-let set_working = function a -> ()
+(* EOF *)
projects / helm.git / blobdiff