compile-time feature PROFV to profile validation without sort inclusion

[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml

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