From: Ferruccio Guidi Date: Tue, 7 Jul 2015 19:57:05 +0000 (+0000) Subject: compile-time feature PROFV to profile validation without sort inclusion X-Git-Tag: make_still_working~706 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd453d40e15929d6faef02f7b01a17f0cd6fc5b7;p=helm.git compile-time feature PROFV to profile validation without sort inclusion --- diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 5a726ca97..f597f6cf1 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -207,9 +207,6 @@ let xlate_entity err f st lst = function 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 @@ -226,12 +223,13 @@ ELSE () END; | 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 diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml index bc65fe075..100b7c4df 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgGallina.ml @@ -118,7 +118,13 @@ let close_out och () = close_out och 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 -> diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index a6ab35ea9..0806a3d32 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -11,6 +11,8 @@ module U = NUri module L = Log +module Y = Time +module G = Options module E = Entity module B = Brg module BE = BrgEnvironment @@ -45,11 +47,20 @@ let type_check err f st = function 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 diff --git a/helm/software/helena/src/lib/time.ml b/helm/software/helena/src/lib/time.ml index 2ca44689f..a9e542664 100644 --- a/helm/software/helena/src/lib/time.ml +++ b/helm/software/helena/src/lib/time.ml @@ -15,15 +15,11 @@ module L = Log 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 @@ -34,4 +30,26 @@ let gmtime msg = 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 diff --git a/helm/software/helena/src/lib/time.mli b/helm/software/helena/src/lib/time.mli new file mode 100644 index 000000000..e70c3b955 --- /dev/null +++ b/helm/software/helena/src/lib/time.mli @@ -0,0 +1,20 @@ +(* + ||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 diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index c80bff4f8..b7c6fc135 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -439,6 +439,7 @@ let main = (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