X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgValidity.ml;h=a1401c125a1a01c114daeac350170b88a0c80288;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=ad4154fc17241316160c8405211210d7471720ee;hpb=c2a2ecf1a9d02b03b9e840e01128632663e5d8a5;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index ad4154fc1..a1401c125 100644
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -46,58 +46,67 @@ let zero = Some 0
 let one = Some 1
 
 let assert_convertibility err f st m u t =
-   if !G.trace >= level then warn "Asserting convertibility for cast";
+IFDEF TRACE THEN
+   if !G.ct >= level then warn "Asserting convertibility for cast"
+ELSE () END;
    if BR.are_convertible st m zero u m one t then f () else
    error2 err m u m t
 
-let assert_applicability err f st m v t =
-   if !G.trace >= level then warn "Asserting applicability";
-   match BR.xwhd st m None t with 
-      | _, B.Sort _                            ->
-         error1 err "not a function" m t
+let assert_applicability err f st m a v t =
+   let mode, msg = if a.E.a_rest then one, "restricted" else None, "extended" in 
+IFDEF TRACE THEN
+   if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability")
+ELSE () END;
+   match BR.xwhd st m mode t with 
       | mw, B.Bind (_, B.Abst (true, n, w), _) ->
          if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
          else begin
-            if !G.trace >= level then warn "Asserting convertibility for application";
+IFDEF TRACE THEN
+            if !G.ct >= level then warn "Asserting convertibility for application"
+ELSE () END;
             if BR.are_convertible st mw zero w m one v then f () else
 	    error2 err mw w m v
          end
-      | _                                -> assert false (**)
+      | _, B.Sort _                            ->
+         error1 err "not a function" m t
+      | _                                      -> assert false (**)
 
-let rec b_validate err f st m x =
-   if !G.trace >= level then log1 st "Now checking" m x;
-   match x with
+let rec b_validate err f st m y =
+IFDEF TRACE THEN
+   if !G.ct >= level then log1 st "Now checking" m y
+ELSE () END;
+   match y with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->
       begin match BR.get m i with
          | B.Abst _
 	 | B.Abbr _ -> f ()
 	 | B.Void   -> 
-	    error1 err "reference to excluded variable" m x
+	    error1 err "reference to excluded variable" m y
       end
    | B.GRef (_, uri)  ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abst _
 	 | _, _, _, E.Abbr _ -> f ()
 	 | _, _, _, E.Void   ->
-            error1 err "reference to unknown entry" m x
+            error1 err "reference to unknown entry" m y
       end
-   | B.Bind (a, b, t) ->
-      let f () = b_validate err f st (BR.push m a b) t in
+   | B.Bind (y, b, t) ->
+      let f () = b_validate err f st (BR.push m y b) t in
       begin match b with 
          | B.Abst (_, n, u) -> validate err f st m u
          | B.Abbr v         -> validate err f st m v
          | B.Void           -> f ()
       end
-   | B.Appl (_, v, t)        ->
-      let f () = assert_applicability err f st m v t in
+   | B.Appl (a, v, t)       ->
+      let f () = assert_applicability err f st m a v t in
       let f () = b_validate err f st m t in
       validate err f st m v
-   | B.Cast (_, u, t)        ->
+   | B.Cast (u, t)          ->
       let f () = assert_convertibility err f st m u t in
       let f () = b_validate err f st m t in
       validate err f st m u
 
 (* Interface functions ******************************************************)
 
-and validate err f st m x = b_validate err f st m x
+and validate err f st m t = b_validate err f st m t