From: Enrico Tassi Date: Tue, 22 Apr 2008 13:44:27 +0000 (+0000) Subject: slow_implementation and some dead code removed X-Git-Tag: make_still_working~5297 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5cd2efd21063b304c30a9486a562bdff7852957b;p=helm.git slow_implementation and some dead code removed --- diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index 2bfbc92a3..7aac62cff 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -36,12 +36,6 @@ (* $Id$ *) -(*****************************************************************************) -(** switch implementation **) -(*****************************************************************************) - -let fast_implementation = ref true ;; - (*****************************************************************************) (** open **) (*****************************************************************************) @@ -135,29 +129,6 @@ let string_of_mal m = 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 **) (*****************************************************************************) @@ -301,108 +272,6 @@ and add_eq_arc_fast u v m = ;; -(*****************************************************************************) -(** 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' - - -(*****************************************************************************) -(** 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 **) @@ -500,7 +369,7 @@ 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 @@ -512,19 +381,19 @@ let add_eq ?(fast=(!fast_implementation)) u v b = 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 @@ -548,7 +417,7 @@ let add_gt ?(fast=(!fast_implementation)) u v b = 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*) @@ -556,46 +425,37 @@ let add_gt ?(fast=(!fast_implementation)) u v b = (** 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,_,_ as ugraph) = +let do_rank (b,_,_) = (* print_ugraph ugraph; *) let keys = MAL.fold (fun k _ acc -> k::acc) b [] in let fall = diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli index fd501df8c..7b422583f 100644 --- a/helm/software/components/cic/cicUniv.mli +++ b/helm/software/components/cic/cicUniv.mli @@ -66,11 +66,11 @@ val oblivion_ugraph: universe_graph UniverseInconsistency *) val add_eq: - ?fast:bool -> universe -> universe -> universe_graph -> universe_graph + universe -> universe -> universe_graph -> universe_graph val add_ge: - ?fast:bool -> universe -> universe -> universe_graph -> universe_graph + universe -> universe -> universe_graph -> universe_graph val add_gt: - ?fast:bool -> universe -> universe -> universe_graph -> universe_graph + universe -> universe -> universe_graph -> universe_graph val do_rank: universe_graph -> unit val get_rank: universe -> int @@ -152,10 +152,4 @@ val assert_univ: universe -> unit val compare: universe -> universe -> int val eq: universe -> universe -> bool -(* - Benchmarking stuff -*) -val get_spent_time: unit -> float -val reset_spent_time: unit -> unit - val is_anon: universe -> bool