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

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 929dcbce8..28a275548 100644
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -22,6 +22,8 @@ module BE = BrgEnvironment
 module BS = BrgSubstitution
 module BR = BrgReduction
 
+IFDEF TYPE THEN
+
 (* Internal functions *******************************************************)
 
 let level = 4
@@ -55,8 +57,9 @@ let assert_convertibility err f st m u w v =
    if BR.are_convertible st m zero u m zero w then f () else
    error3 err m v w u
 
-let assert_applicability err f st m u w v =
-   match BR.xwhd st m None u with 
+let assert_applicability err f st m a u w v =
+   let mode = if a.E.a_rest then zero else None in
+   match BR.xwhd st m mode u with 
       | _, B.Sort _                            ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (true, n, u), _) -> 
@@ -65,62 +68,64 @@ let assert_applicability err f st m u w v =
 	 error3 err m v w ~mu u
       | _                                      -> assert false (**)
 
-let rec b_type_of err f st m r =
-   if !G.trace >= level then log1 st "Now checking" m r;
-   match r with
-   | B.Sort (a, h)                   ->
-      let h = H.apply h in f r (B.Sort (a, h)) 
+let rec b_type_of err f st m z =
+IFDEF TRACE THEN
+   if !G.ct >= level then log1 st "Now checking" m z
+ELSE () END;
+   match z with
+   | B.Sort k                        ->
+      let k = H.apply k in f z (B.Sort k) 
    | B.LRef (_, i)                   ->
       begin match BR.get m i with
-         | B.Abst (_, _, w)          ->
-	    f r (BS.lift (succ i) (0) w)
-	 | B.Abbr (B.Cast (_, w, _)) -> 
-	    f r (BS.lift (succ i) (0) w)
-	 | B.Abbr _                  -> assert false
-	 | B.Void                    -> 
-	    error1 err "reference to excluded variable" m r
+         | B.Abst (_, _, w)       ->
+	    f z (BS.lift (succ i) (0) w)
+	 | B.Abbr (B.Cast (w, _)) -> 
+	    f z (BS.lift (succ i) (0) w)
+	 | B.Abbr _               -> assert false
+	 | B.Void                 -> 
+	    error1 err "reference to excluded variable" m z
       end
-   | B.GRef (_, uri)                 ->
-      begin match BE.get_entity uri with
-         | _, _, _, E.Abst w                  -> f r w
-	 | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f r w
+   | B.GRef (_, u)                   ->
+      begin match BE.get_entity u with
+         | _, _, _, E.Abst (_, w)             -> f z w
+	 | _, _, _, E.Abbr (_, B.Cast (w, _)) -> f z w
 	 | _, _, _, E.Abbr _                  -> assert false
 	 | _, _, _, E.Void                    ->
-            error1 err "reference to unknown entry" m r
+            error1 err "reference to unknown entry" m z
       end
-   | B.Bind (a, B.Abbr v, t)         ->
+   | B.Bind (y, B.Abbr v, t)         ->
       let f rv rt tt =
-         f (S.sh2 v rv t rt r (B.bind_abbr a)) (B.bind_abbr a rv tt)
+         f (S.sh2 v rv t rt z (B.bind_abbr y)) (B.bind_abbr y rv tt)
       in
       let f rv m = b_type_of err (f rv) st m t in
-      let f rv = f rv (BR.push m a (B.abbr rv)) in
+      let f rv = f rv (BR.push m y (B.abbr rv)) in
       let f rv vv = match rv with 
 	 | B.Cast _ -> f rv
-         | _        -> f (B.Cast (E.empty_node, vv, rv))
+         | _        -> f (B.Cast (vv, rv))
       in
       type_of err f st m v
-   | B.Bind (a, B.Abst (x, n, u), t) ->
+   | B.Bind (y, B.Abst (r, n, u), t) ->
       let f ru rt tt =
-	 f (S.sh2 u ru t rt r (B.bind_abst x n a)) (B.bind_abst x (N.minus st n 1) a ru tt)
+	 f (S.sh2 u ru t rt z (B.bind_abst r n y)) (B.bind_abst r (N.minus st n 1) y ru tt)
       in
       let f ru m = b_type_of err (f ru) st m t in
-      let f ru _ = f ru (BR.push m a (B.abst x n ru)) in
+      let f ru _ = f ru (BR.push m y (B.abst r n ru)) in
       type_of err f st m u
-   | B.Bind (a, B.Void, t)           ->
+   | B.Bind (y, B.Void, t)           ->
       let f rt tt = 
-         f (S.sh1 t rt r (B.bind_void a)) (B.bind_void a tt)
+         f (S.sh1 t rt z (B.bind_void y)) (B.bind_void y tt)
       in
-      b_type_of err f st (BR.push m a B.Void) t
+      b_type_of err f st (BR.push m y B.Void) t
    | B.Appl (a, v, t)                ->
       let f rv vv rt tt = 
-         let f _ = f (S.sh2 v rv t rt r (B.appl a)) (B.appl a rv tt) in
-         assert_applicability err f st m tt vv rv
+         let f _ = f (S.sh2 v rv t rt z (B.appl a)) (B.appl a rv tt) in
+         assert_applicability err f st m a tt vv rv
       in
       let f rv vv = b_type_of err (f rv vv) st m t in
       type_of err f st m v
-   | B.Cast (a, u, t)                ->
+   | B.Cast (u, t)                   ->
       let f ru rt tt =  
-	 let f _ = f (S.sh2 u ru t rt r (B.cast a)) ru in
+	 let f _ = f (S.sh2 u ru t rt z (B.cast)) ru in
          assert_convertibility err f st m ru tt rt
       in
       let f ru _ = b_type_of err (f ru) st m t in
@@ -128,4 +133,6 @@ let rec b_type_of err f st m r =
 
 (* Interface functions ******************************************************)
 
-and type_of err f st m r = b_type_of err f st m r
+and type_of err f st m t = b_type_of err f st m t
+
+END