From: Ferruccio Guidi Date: Wed, 10 Sep 2008 19:03:21 +0000 (+0000) Subject: cicDischarge, Procedural: we improved debugging and added some time stamps X-Git-Tag: make_still_working~4791 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ea5357bace160aaf57750d9dcfb3077fe5a1b38;p=helm.git cicDischarge, Procedural: we improved debugging and added some time stamps librarian.ml: new algorithm for sorting sources according to compilation order --- diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index deb3088f2..ce6316de1 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -489,10 +489,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth context = []; case = [] } in + H.print_times "LEVEL 2"; HLog.debug "Procedural: level 2 transformation"; let steps = proc_obj st ?flavour anobj in + H.print_times "RENDERING"; HLog.debug "Procedural: grafite rendering"; - List.rev (T.render_steps [] steps) + let r = List.rev (T.render_steps [] steps) in + H.print_times "DONE "; r let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix context annterm = diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 91f7016cd..54b115aa2 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -35,6 +35,17 @@ module D = Deannotate module PER = ProofEngineReduction module Ut = CicUtil +(* time stamping ************************************************************) + +let print_times = + let old = ref 0.0 in + fun msg -> + let times = Unix.times () in + let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in + let lap = stamp -. !old in + Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout; + old := stamp + (* raw cic prettyprinter ****************************************************) let xiter out so ss sc map l = diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 770534af6..239c789c2 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -23,14 +23,16 @@ * http://cs.unibo.it/helm/. *) +val print_times: + string -> unit val pp_term: (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit val mk_fresh_name: Cic.context -> Cic.name -> Cic.name val list_map_cps: - ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b + ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b val identity: - 'a -> 'a + 'a -> 'a val compose: ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b val fst3: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 20e04d322..c5958575a 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -38,6 +38,10 @@ module Un = CicUniv module H = ProceduralHelpers module Cl = ProceduralClassify +(* debugging ****************************************************************) + +let debug = ref false + (* term preprocessing: optomization 1 ***************************************) let defined_premise = "DEFINED" @@ -54,7 +58,7 @@ let clear_absts m = | C.Lambda (_, _, t) when n > 0 -> aux 0 (pred n) (S.lift (-1) t) | t when n > 0 -> - Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t); + Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t); assert false | t -> t in @@ -275,15 +279,20 @@ let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in let g bo = - Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" - (Pp.ppterm bo) (I.count_nodes 0 bo); - prerr_string "H.pp_term : "; - H.pp_term prerr_string [] [] bo; prerr_newline (); + if !debug then begin + Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" + (Pp.ppterm bo) (I.count_nodes 0 bo); + prerr_string "H.pp_term : "; + H.pp_term prerr_string [] [] bo; prerr_newline () + end; let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in + H.print_times ("OPTIMIZED: " ^ name); C.Constant (name, Some bo, ty, pars, attrs) in - Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" - name (I.count_nodes 0 bo); + H.print_times ("BEGIN : " ^ name); + if !debug then + Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" + name (I.count_nodes 0 bo); begin try opt1_term g (* (opt2_term g []) *) true [] bo with | E.Object_not_found uri -> let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.mli b/helm/software/components/acic_procedural/proceduralOptimizer.mli index 45505d72c..3e2eebf00 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.mli +++ b/helm/software/components/acic_procedural/proceduralOptimizer.mli @@ -24,3 +24,5 @@ *) val optimize_obj: Cic.obj -> Cic.obj + +val debug: bool ref diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index f8ad074fb..52b841952 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.ml +++ b/helm/software/components/cic_proof_checking/cicDischarge.ml @@ -33,6 +33,8 @@ let hashtbl_size = 11 let not_implemented = "discharge of current proofs is not implemented yet" +let debug = ref false + (* helper functions *********************************************************) let list_pos found l = @@ -108,11 +110,10 @@ let rec discharge_term st t = match t with let s = List.map (mk_arg s) args in C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s) | C.Var (u, s) -> -(* FG: We do not discharge the nsubst here ?? *) - let args = get_args st u in - if args = [] then C.Rel (discharge st u) else - let s = List.map (mk_arg s) args in - (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *) +(* We do not discharge the nsubst because variables are not closed *) +(* thus only the identity nsubst should be allowed *) + if s <> [] then assert false else + C.Rel (discharge st u) | C.Meta (i, s) -> let s' = list_map_sh (discharge_usubst st) s in if s' == s then t else C.Meta (i, s') @@ -232,9 +233,9 @@ let rec discharge_object dn du obj = and discharge_uri dn du uri = let obj, _ = E.get_obj Un.default_ugraph uri in - prerr_endline ("Plain : " ^ CicPp.ppobj obj); + if !debug then prerr_endline ("Plain : " ^ CicPp.ppobj obj); let obj' = discharge_object dn du obj in - prerr_endline ("Discharged: " ^ CicPp.ppobj obj'); + if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj'); obj', obj' == obj and discharge_vars dn du vars = diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli index a6b097db2..7d6f630f4 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.mli +++ b/helm/software/components/cic_proof_checking/cicDischarge.mli @@ -35,3 +35,6 @@ val discharge_object: val discharge_uri: (string -> string) -> (UriManager.uri -> UriManager.uri) -> UriManager.uri -> Cic.obj * bool + +(* if activated prints the received object before and after discharging *) +val debug: bool ref diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index f56ba5840..990e74813 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -204,7 +204,7 @@ module Make = functor (F:Format) -> struct let fst4 = function (x,_,_,_) -> x;; - let younger_s_t (_,cs, ct, _, _) a b = + let modified_before_s_t (_,cs, ct, _, _) a b = let a = try Hashtbl.find cs a with Not_found -> assert false in let b = try @@ -223,7 +223,7 @@ module Make = functor (F:Format) -> struct | _ -> false ;; - let younger_t_t (_,_,ct, _, _) a b = + let modified_before_t_t (_,_,ct, _, _) a b = let a = try match Hashtbl.find ct a with @@ -272,7 +272,8 @@ module Make = functor (F:Format) -> struct | Some root -> not (F.is_readonly_buri_of opts f) | None -> assert false ;; - +(* FG: Old sorting algorithm ************************************************) +(* let rec get_status opts what = let _, _, _, cc, cd = opts in let t, dependencies, root, tgt = what in @@ -288,7 +289,7 @@ module Make = functor (F:Format) -> struct begin match st, get_status opts whatd with | _, Done false -> Hashtbl.add cc t false; Done false | Done true, Done true -> - if younger_t_t opts tgt tgtd then Ready true else Done true + if modified_before_t_t opts tgt tgtd then Ready true else Done true (* say (F.string_of_source_object t^" depends on "^F.string_of_target_object unsat^" and "^F.string_of_source_object t^".o is younger than "^ F.string_of_target_object unsat^", thus needs to be built") *) | Done true, Ready _ -> Ready false | Ready true, Ready _ -> Ready false @@ -297,7 +298,7 @@ module Make = functor (F:Format) -> struct | _ -> st end in - let st = if younger_s_t opts t tgt then Done true else Ready true in + let st = if modified_before_s_t opts t tgt then Done true else Ready true in match List.fold_left map st dependencies with | Done true -> Hashtbl.add cc t true; Done true (* say(F.string_of_source_object t^" is built" *) @@ -340,7 +341,7 @@ module Make = functor (F:Format) -> struct let rc = match froot with | Some froot when froot = root -> - Hashtbl.remove ct tgt; + Hashtbl.remove ct tgt; Hashtbl.add ct tgt None; timestamp "building"; let r = F.build lo file in @@ -359,8 +360,48 @@ module Make = functor (F:Format) -> struct end else ok +*) +(* FG: new sorting algorithm ************************************************) + + let rec make_aux root opts ok deps = + List.fold_left (make_one root opts) ok deps + + and make_one root opts ok what = + let lo, _, ct, cc, cd = opts in + let t, deps, froot, tgt = what in + let map (okd, okt) d = + let (_, _, _, tgtd) as whatd = (Hashtbl.find cd d) in + make_one root opts okd whatd, okt && modified_before_t_t opts tgtd tgt + in + try ok && Hashtbl.find cc t +(* say "already built" *) + with Not_found -> + let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in + let res = + if okd then + if okt then true else + let str = F.string_of_source_object t in + match froot with + | Some froot when froot = root -> + if is_not_ro opts what then begin + Hashtbl.remove ct tgt; + Hashtbl.add ct tgt None; + timestamp "building"; + let res = F.build lo t in + timestamp "done"; res + end else begin + HLog.warn("Read only baseuri for: "^ str); false + end + | Some froot -> make froot [t] + | None -> + HLog.error ("No root for: " ^ str); false + else false + in + Hashtbl.add cc t res; ok && res + +(****************************************************************************) - and make root targets = + and make root targets = timestamp "entering"; HLog.debug ("Entering directory '"^root^"'"); let old_root = Sys.getcwd () in