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=27f471f9a81eb8899f05f6cf9ed0492f049ab66c;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml
index 27f471f9a..b1cd52523 100644
--- a/helm/software/helena/src/basic_rg/brgUntrusted.ml
+++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml
@@ -11,28 +11,56 @@
 
 module U  = NUri
 module L  = Log
+module Y  = Time
+module G  = Options
 module E  = Entity
 module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
 module BT = BrgType
+module BV = BrgValidity
 
 (* Interface functions ******************************************************)
 
+IFDEF TYPE THEN
+
 (* to share *)
 let type_check err f st = function
-   | a, uri, E.Abst (n, 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 (a, uri, E.Abst (n, xt)) in f tt e
+         let e = BE.set_entity (ra, na, uri, E.abst a xt) in f tt e
       in
-      L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
-   | a, uri, E.Abbr t      ->
+      BT.type_of err f st BR.empty_rtm 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 ([], tt, xt)
+	    | _        -> B.Cast (tt, xt)
 	 in
-         let e = BE.set_entity (a, 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
-      L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
-   | _, _, E.Void          -> assert false
+      BT.type_of err f st BR.empty_rtm t
+   | _, _, _, 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
+   in
+   let err msg = err (L.Uri uri :: msg) 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