new options activated

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

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index ad4154fc17241316160c8405211210d7471720ee..c616b22df68c023eedc60257548cc96d9279a446 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -46,41 +46,42 @@ 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";
+   if !G.ct >= level then warn "Asserting convertibility for cast";
    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 x v t =
+   let mode, msg = if x then None, "extended" else one, "restricted" in 
+   if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability");
+   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";
+            if !G.ct >= 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
          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 =
+   if !G.ct >= level then log1 st "Now checking" m y;
+   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
@@ -89,8 +90,8 @@ let rec b_validate err f st m x =
          | 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 (_, x, v, t)    ->
+      let f () = assert_applicability err f st m x v t in
       let f () = b_validate err f st m t in
       validate err f st m v
    | B.Cast (_, u, t)        ->
@@ -100,4 +101,4 @@ let rec b_validate err f st m x =
 
 (* 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