(* $Id$ *)
-(*****************************************************************************)
-(** switch implementation **)
-(*****************************************************************************)
-
-let fast_implementation = ref true ;;
-
(*****************************************************************************)
(** open **)
(*****************************************************************************)
module UniverseType = struct
type t = universe
- let compare = Pervasives.compare
+ let compare (n1,u1) (n2,u2) =
+ let ndiff = n1 - n2 in
+ if ndiff <> 0 then ndiff
+ else
+ match u1,u2 with
+ None, None -> 0
+ | Some u1, Some u2 -> UriManager.compare u1 u2
+ | None, Some _ -> 1
+ | Some _, None -> -1
end
module SOF = Set.Make(UniverseType)
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 **)
(*****************************************************************************)
print_endline ("Aggiusto " ^ (string_of_universe u) ^
"e ottengo questa chiusura\n " ^ (string_of_node ru))
-and adjust_fast u m =
+and adjust_fast_aux 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
in
let m = MAL.add u ru' m in
let m =
- SOF.fold (fun x m -> adjust_fast x m)
+ SOF.fold (fun x m -> adjust_fast_aux 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 profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
+and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
+*)
+and adjust_fast x y = adjust_fast_aux x y
and add_gt_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.gt_closure then m else
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
and add_ge_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.ge_closure then m else
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
and add_eq_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.eq_closure then m else
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 *)
;;
\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 **)
let name_universe u uri =
match u with
| (i, None) -> (i, Some uri)
- | _ -> u
+ | (i, Some ouri) when UriManager.eq ouri uri -> u
+ | (i, Some ouri) ->
+ (* inside obj living at uri 'uri' should live only
+ * universes with uri None. Call Unshare.unshare ~fresh_univs:true
+ * if you want to reuse a Type in another object *)
+ prerr_endline ("Offending universe: " ^ string_of_universe u^
+ " found inside object " ^ UriManager.string_of_uri uri);
+ assert false
+;;
let print_ugraph (g, _, o) =
if o then prerr_endline "oblivion universe" else
prerr_endline (string_of_bag g)
-let add_eq ?(fast=(!fast_implementation)) u v b =
+let add_eq 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 u rv.gt_closure then
error ("EQ",u,v) u "GT" v rv.gt_closure
else
- add_eq fast u v b
+ add_eq_arc_fast u v b
end
-let add_ge ?(fast=(!fast_implementation)) u v b =
+let add_ge 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
+ add_ge_arc_fast u v b
-let add_gt ?(fast=(!fast_implementation)) u v b =
+let add_gt 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
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
+ add_gt_arc_fast u v b
(* end
end*)
(** START: Decomment this for performance comparisons **)
(*****************************************************************************)
-let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_eq u v (b,already_contained,oblivion) =
if oblivion then (b,already_contained,oblivion) else
- (*prerr_endline "add_eq";*)
- (begin_spending ();
- let rc = add_eq ~fast u v b in
- end_spending ();
- rc,already_contained,false)
+ let rc = add_eq u v b in
+ rc,already_contained,false
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_ge u v (b,already_contained,oblivion) =
if oblivion then (b,already_contained,oblivion) else
-(* prerr_endline "add_ge"; *)
- (begin_spending ();
- let rc = add_ge ~fast u v b in
- end_spending ();
- rc,already_contained,false)
+ let rc = add_ge u v b in
+ rc,already_contained,false
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_gt u v (b,already_contained,oblivion) =
if oblivion then (b,already_contained,oblivion) else
-(* prerr_endline "add_gt"; *)
- (begin_spending ();
- let rc = add_gt ~fast u v b in
- end_spending ();
- rc,already_contained,false)
+ let rc = add_gt u v b in
+ rc,already_contained,false
-(* profiling code
+(* profiling code *)
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) ()
-*)
+let add_gt u v b =
+ profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) ()
+let add_ge u v b =
+ profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) ()
+let add_eq u v b =
+ profiler_eq.HExtlib.profile (fun _ -> add_eq u v b) ()
+
+
+(* ugly *)
+let rank = ref MAL.empty;;
+
+let do_rank (b,_,_) =
+(* print_ugraph ugraph; *)
+ let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+ let fall =
+ List.fold_left
+ (fun acc u ->
+ let rec aux k seen = function
+ | [] -> 0, seen
+ | x::tl when SOF.mem x seen -> aux k seen tl
+ | x::tl ->
+(* prerr_endline (String.make k '.' ^ string_of_universe x); *)
+ let seen = SOF.add x seen in
+ let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
+ let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in
+ let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
+ let t4, seen = aux k seen tl in
+ max (max t1 t2)
+ (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
+ seen
+ in
+ let rank, _ = aux 0 SOF.empty [u] in
+ MAL.add u rank acc)
+ MAL.empty
+ in
+ rank := fall keys;
+ MAL.iter
+ (fun k v ->
+ prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+;;
+
+let get_rank u =
+ try MAL.find u !rank
+ with Not_found -> 0
+ (* if the universe is not in the graph it means there are
+ * no contraints on it! thus it can be freely set to Type0 *)
+;;
(*****************************************************************************)
(** END: Decomment this for performance comparisons **)
(* TODO: uncomment l to gain a small speedup *)
let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
let merge_brutal (u,a,_) v =
- prerr_endline ("merging graph: "^UriManager.string_of_uri uri_of_increment);
+(* prerr_endline ("merging graph: "^UriManager.string_of_uri
+ * uri_of_increment); *)
let m1 = u in
let m2 = v in
MAL.fold (
(UriManager.UriSet.add uri_of_increment already_contained), false
(* profiling code; WARNING: the time spent during profiling can be
- greater than the profiled time
+ greater than the profiled time
let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
let merge_ugraphs ~base_ugraph ~increment =
profiler_merge.HExtlib.profile
| Some uri1, Some uri2 -> UriManager.compare uri1 uri2
else
cmp
+
+let is_anon = function (_,None) -> true | _ -> false
(* EOF *)
projects / helm.git / blobdiff