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=e6704d0a967e52648d43fabdba92bbd148044fc4;hpb=ac97468f5422efc770316286cb807e3d3245a474;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index e6704d0a9..a1401c125 100644
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -10,25 +10,25 @@
       V_______________________________________________________________ *)
 
 module L  = Log
-module E  = Entity
 module G  = Options
-module S  = Status
+module N  = Layer
+module E  = Entity
 module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
 
 (* Internal functions *******************************************************)
 
-let level = 3
+let level = 4
 
-let warn s = L.warn level s
+let warn s = L.warn (pred level) s
 
 let message1 st1 m t1 =
    L.et_items1 "In the environment" m st1 t1
 
 let log1 st s m t =
    let s =  s ^ " the term" in
-   L.log st BR.specs level (message1 s m t) 
+   L.log st BR.specs (pred level) (message1 s m t) 
 
 let error1 err s m t =
    err (message1 s m t)
@@ -46,55 +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 _                      ->
+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
+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
+      | _, B.Sort _                            ->
          error1 err "not a function" m t
-      | mw, B.Bind (_, B.Abst (_, w), _) ->
-         if !G.trace >= level then warn "Asserting convertibility for application";
-         if BR.are_convertible st mw zero w m one v then f () else
-	 error2 err mw w m v
-      | _                                -> assert false (**)
-
-let rec b_validate err f st m x =
-   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
-   match x with
+      | _                                      -> assert false (**)
+
+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 ()
+         | 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