X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgUntrusted.ml;h=b1cd52523d794f36db670f5636e6c0e810fba4b3;hb=150f931929c8333dbcfff8dbe77fb2e177f44c56;hp=8425774d2a6bc890cb4cd439b67fec74ee9ab24c;hpb=30eb28f8c35d7667b3a0052c30d2750a492fa464;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml
index 8425774d2..b1cd52523 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
@@ -20,32 +22,45 @@ module BV = BrgValidity
 
 (* Interface functions ******************************************************)
 
+IFDEF TYPE THEN
+
 (* to share *)
 let type_check err f st = function
-   | ra, na, uri, E.Abst t ->
+   | ra, na, uri, E.Abst (a, t) ->
       let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
-         let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e
+         let e = BE.set_entity (ra, na, uri, E.abst a xt) in f tt e
       in
       BT.type_of err f st BR.empty_rtm t
-   | ra, na, uri, E.Abbr t ->
+   | ra, na, uri, E.Abbr (a, t) ->
       let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
          let xt = match xt with
 	    | B.Cast _ -> xt
-	    | _        -> B.Cast (E.empty_node, tt, xt)
+	    | _        -> B.Cast (tt, xt)
 	 in
-         let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
+         let e = BE.set_entity (ra, na, uri, E.abbr a xt) in f tt e
       in
       BT.type_of err f st BR.empty_rtm t
-   | _, _, _, E.Void       -> assert false
+   | _, _, _, E.Void            -> assert false
+
+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
+      | _, _, 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