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 5a726ca9703b732041fe5a0f0f09ef5536de5890..f597f6cf1db3fb8e306d8e1112543990b6e9074a 100644 (file)
--- 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 bc65fe0752244f0c89c737f76c62f325baa57db1..100b7c4df79afd7b392a5ab7b6f745a4e2d33ab2 100644 (file)
--- 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 a6ab35ea94420b3d2f03ffd619512a53afcc4321..0806a3d3255b2e857f20792decdea52b9d06f580 100644 (file)
--- 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 2ca44689fbdbc91a46f58ae83960e75bd5b345ae..a9e542664f6f79134a2ae233b5bc6ca70087029b 100644 (file)
--- 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 (file)
index 0000000..e70c3b9
--- /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 c80bff4f85dc06fc82bc2c06ff5a279de9149e32..b7c6fc1355c056329c416075b81d83953f4ea732 100644 (file)
--- 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