module HEL = HExtlib
module DTI = DoubleTypeInference
module NU = CicNotationUtil
+module L = Librarian
module Cl = ProceduralClassify
module T = ProceduralTypes
case: int list
}
-let debug = false
+let debug = ref false
(* helpers ******************************************************************)
let e = Cn.hole "" in
let csty, cety = H.cic sty, H.cic ety in
let script =
- if debug then
+ if !debug then
let sname = match name with None -> "" | Some (id, _) -> id in
let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
note sname (Pp.ppterm csty) (Pp.ppterm cety)
let convert st ?name v =
match get_inner_types st v with
| None ->
- if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
+ if !debug then [T.Note "NORMAL: NO INNER TYPES"] else []
| Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
let convert_elim st ?name t v pattern =
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
- let ty = get_type "TC2" st hd in
+ let ty = match get_inner_types st hd with
+ | Some (ity, _) -> H.cic ity
+ | None -> get_type "TC2" st hd
+ in
let classes, rc = Cl.classify st.context ty in
let goal_arity, goal = match get_inner_types st what with
| None -> 0, None
context = [];
case = []
} in
- H.print_times "LEVEL 2";
+ L.time_stamp "P : LEVEL 2 ";
HLog.debug "Procedural: level 2 transformation";
let steps = proc_obj st ?flavour anobj in
- H.print_times "RENDERING";
+ L.time_stamp "P : RENDERING";
HLog.debug "Procedural: grafite rendering";
let r = List.rev (T.render_steps [] steps) in
- H.print_times "DONE "; r
+ L.time_stamp "P : DONE "; r
let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
prefix context annterm =
* http://helm.cs.unibo.it/
*)
-let debug = false;;
-
-let timestamp msg =
- if debug then
- let times = Unix.times () in
- let utime = times.Unix.tms_utime in
- let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg utime in
- prerr_endline msg
+let debug = ref true
+
+let time_stamp =
+ let old = ref 0.0 in
+ fun msg ->
+ if !debug then begin
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in
+ let lap = stamp -. !old in
+ Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr;
+ old := stamp
+ end
exception NoRootFor of string
type status = Done of bool
| Ready of bool
- let say s = if debug then prerr_endline ("make: "^s);;
+ let say s = if !debug then prerr_endline ("make: "^s);;
let unopt_or_call x f y = match x with Some _ -> x | None -> f y;;
let fst4 = function (x,_,_,_) -> x;;
let modified_before_s_t (_,cs, ct, _, _) a b =
+ prerr_endline ("L s_t: a " ^ F.string_of_source_object a);
+ prerr_endline ("L s_t: b " ^ F.string_of_target_object b);
let a = try Hashtbl.find cs a with Not_found -> assert false in
let b =
try
| x -> x
with Not_found -> assert false
in
- match a, b with
- | Some a, Some b -> a < b
- | _ -> false
- ;;
+ let r = match a, b with
+ | Some a, Some b -> a <= b
+ | _ -> false
+ in
+ prerr_endline ("L s_t: " ^ string_of_bool r); r
let modified_before_t_t (_,_,ct, _, _) a b =
- let a =
+(*
+ prerr_endline ("L t_t: a " ^ F.string_of_target_object a);
+ prerr_endline ("L t_t: b " ^ F.string_of_target_object b);
+*) let a =
try
match Hashtbl.find ct a with
| Some _ as x -> x
| None ->
- match F.mtime_of_target_object a with
+ match F.mtime_of_target_object a with
| Some t as x ->
- Hashtbl.remove ct a;
+ Hashtbl.remove ct a;
Hashtbl.add ct a x; x
| x -> x
with Not_found -> assert false
| None ->
match F.mtime_of_target_object b with
| Some t as x ->
- Hashtbl.remove ct b;
+ Hashtbl.remove ct b;
Hashtbl.add ct b x; x
| x -> x
with Not_found -> assert false
in
- match a, b with
- | Some a, Some b -> a < b
+ let r = match a, b with
+ | Some a, Some b ->
+(*
+ prerr_endline ("tt: a " ^ string_of_float a);
+ prerr_endline ("tt: b " ^ string_of_float b);
+*)
+ a <= b
| _ -> false
- ;;
+ in
+ prerr_endline ("L t_t: " ^ string_of_bool r); r
let rec purge_unwanted_roots wanted deps =
let roots, rest =
aux [] [] l
let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps =
- timestamp "filter get_status: begin";
+ time_stamp "filter get_status: begin";
let map what = match get_status opts what with
| Done _ -> None
| Ready b -> Some b
in
let todo, deps = list_partition_filter_rev map deps in
- timestamp "filter get_status: end";
+ time_stamp "filter get_status: end";
let todo =
let local, remote =
List.partition (fun (_,_,froot,_) -> froot = Some root) todo
| Some froot when froot = root ->
Hashtbl.remove ct tgt;
Hashtbl.add ct tgt None;
- timestamp "building";
+ time_stamp "building";
let r = F.build lo file in
- timestamp "done"; r
+ time_stamp "done"; r
| Some froot -> make froot [file]
| None ->
HLog.error ("No root for: "^F.string_of_source_object file);
and make_one root opts ok what =
let lo, _, ct, cc, cd = opts in
let t, deps, froot, tgt = what in
+ let str = F.string_of_source_object t 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
+ let r = make_one root opts okd whatd in
+ r, okt && modified_before_t_t opts tgtd tgt
in
- try ok && Hashtbl.find cc t
+ prerr_endline ("L : processing " ^ str);
+ try
+ let r = Hashtbl.find cc t in
+ prerr_endline ("L : " ^ string_of_bool r ^ " " ^ str);
+ ok && r
(* 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";
+ time_stamp ("L : BUILDING " ^ str);
let res = F.build lo t in
- timestamp "done"; res
+ time_stamp ("L : DONE " ^ str); res
end else begin
HLog.warn("Read only baseuri for: "^ str); false
end
HLog.error ("No root for: " ^ str); false
else false
in
+ prerr_endline ("L : " ^ string_of_bool res ^ " " ^ str);
Hashtbl.add cc t res; ok && res
(****************************************************************************)
and make root targets =
- timestamp "entering";
+ time_stamp "L : ENTERING";
HLog.debug ("Entering directory '"^root^"'");
let old_root = Sys.getcwd () in
Sys.chdir root;
in
HLog.debug ("Leaving directory '"^root^"'");
Sys.chdir old_root;
- timestamp "leaving";
+ time_stamp "L : LEAVING";
ok
;;
projects / helm.git / commitdiff