let y = attrs_for_decl yw in
UH.add henv (uri_of_qid qid) (y, lenv);
let t = add_proj yw lenv ww in
-(*
- print_newline (); CrgOutput.pp_term print_string t;
-*)
let na = E.node_attrs ~apix:lst.line () in
let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
IFDEF TRACE THEN
| A.Def (name, w, trans, v) ->
let f lenv =
let f qid =
- let f _ ww =
+ let f yw ww =
let f yv vv =
UH.add henv (uri_of_qid qid) (yv, lenv);
let t = add_proj yv lenv (D.TCast (ww, vv)) in
(*
- print_newline (); CrgOutput.pp_term print_string t;
+ let lenv0 = D.set_layer C.start N.one lenv in
+ let t = D.TCast (add_proj yw lenv0 ww, add_proj yv lenv vv) in
*)
let na = E.node_attrs ~apix:lst.line () in
let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
let output_entity och st (_, na, u, b) =
out_comment och (KP.sprintf "constant %u" na.E.n_apix);
match b with
- | E.Abbr v ->
+(*
+ | E.Abbr (B.Cast (w, v)) ->
+ KP.fprintf och "Definition %a : %a.\n%!" out_uri u (out_term st false B.empty) w;
+ KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v;
+ KP.fprintf och "Time Defined.\n\n%!";
+*)
+ | E.Abbr V ->
KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
(* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
| E.Abst w ->
module U = NUri
module L = Log
+module Y = Time
+module G = Options
module E = Entity
module B = Brg
module BE = BrgEnvironment
END
let validate err f st e =
+IFDEF PROFV THEN
+ Y.utime_lap ""
+ELSE () END;
let uri, t = match e with
| _, _, uri, E.Abst t -> uri, t
| _, _, uri, E.Abbr t -> uri, t
| _, _, _, E.Void -> assert false
in
let err msg = err (L.Uri uri :: msg) in
- let f () = let _ = BE.set_entity e in f () in
+ let f () =
+ let _ = BE.set_entity e in
+IFDEF PROFV THEN
+ if !G.si then () else Y.utime_lap "validated"
+ELSE () END;
+ f ()
+ in
BV.validate err f st BR.empty_rtm t
let level = 1
-let utime_stamp =
- let old = ref 0.0 in
- fun msg ->
- let times = Unix.times () in
- let stamp = times.Unix.tms_utime in
- let lap = stamp -. !old in
- let str = KP.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in
- L.warn level str;
- old := stamp
+let old = [|0.0; 0.0|]
+
+let stamp_ix = 0
+
+let lap_ix = 1
let gmtime msg =
let gmt = Unix.gmtime (Unix.time ()) in
let m = gmt.Unix.tm_min in
let s = gmt.Unix.tm_sec in
let str = KP.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s in
+ L.warn level str
+
+let utime_stamp msg =
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime in
+ let lap = stamp -. old.(stamp_ix) in
+ let str = KP.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in
L.warn level str;
+ old.(stamp_ix) <- stamp
+
+IFDEF PROFV THEN
+
+let utime_lap msg =
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime in
+ if msg <> "" then begin
+ let lap = stamp -. old.(lap_ix) in
+ let str = KP.sprintf "USR TIME LAP (%s): %f" msg lap in
+ L.warn level str
+ end;
+ old.(lap_ix) <- stamp
+
+END
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+val gmtime: string -> unit
+
+val utime_stamp: string -> unit
+
+IFDEF PROFV THEN
+
+val utime_lap: string -> unit
+
+END
(IFDEF QUOTE THEN "QUOTE" ELSE "" END);
(IFDEF STAGE THEN "STAGE" ELSE "" END);
(IFDEF TYPE THEN "TYPE" ELSE "" END);
+(IFDEF PROFV THEN "PROFV" ELSE "" END);
] in
let map s = s <> "" in
let features_string = KT.concat " " (KL.filter map features) in