module BS = BrgSubstitution
module BR = BrgReduction
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
let level = 4
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 x u w v =
- let mode = if x then None else zero in
+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
| _ -> assert false (**)
let rec b_type_of err f st m z =
- if !G.ct >= level then log1 st "Now checking" 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)
end
| 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 ->
+ | _, _, _, 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 z
end
| B.Bind (y, B.Abbr v, t) ->
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 y B.Void) t
- | B.Appl (x, v, t) ->
+ | B.Appl (a, v, t) ->
let f rv vv rt tt =
- let f _ = f (S.sh2 v rv t rt z (B.appl x)) (B.appl x rv tt) in
- assert_applicability err f st m x 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
(* Interface functions ******************************************************)
and type_of err f st m t = b_type_of err f st m t
+
+END