module BS = BrgSubstitution
module BR = BrgReduction
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
-let level = 3
+let level = 4
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)
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
- | _, B.Sort _ ->
+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 (_, u), _) ->
+ | mu, B.Bind (_, B.Abst (true, n, u), _) ->
+ if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function type" m u else
if BR.are_convertible st mu zero u m zero w then f () else
error3 err m v w ~mu u
- | _ -> assert false (**)
+ | _ -> assert false (**)
-let rec b_type_of err f st m x =
- if !G.trace >= level then log1 st "Now checking" m x;
- match x with
- | B.Sort (a, h) ->
- let h = H.apply h in f x (B.Sort (a, h))
- | B.LRef (_, i) ->
+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 x (BS.lift (succ i) (0) w)
- | B.Abbr (B.Cast (_, w, _)) ->
- f x (BS.lift (succ i) (0) w)
- | B.Abbr _ -> assert false
- | B.Void ->
- error1 err "reference to excluded variable" m x
+ | 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 x w
- | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f x 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 x
+ error1 err "reference to unknown entry" m z
end
- | B.Bind (a, B.Abbr v, t) ->
- let f xv xt tt =
- f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+ | B.Bind (y, B.Abbr v, t) ->
+ let f rv rt tt =
+ f (S.sh2 v rv t rt z (B.bind_abbr y)) (B.bind_abbr y rv tt)
in
- let f xv m = b_type_of err (f xv) st m t in
- let f xv = f xv (BR.push m a (B.abbr xv)) in
- let f xv vv = match xv with
- | B.Cast _ -> f xv
- | _ -> f (B.Cast (E.empty_node, vv, xv))
+ let f rv m = b_type_of err (f rv) st m t 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 (vv, rv))
in
type_of err f st m v
- | B.Bind (a, B.Abst (n, u), t) ->
- let f xu xt tt =
- f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st n 1) a xu tt)
+ | B.Bind (y, B.Abst (r, n, u), t) ->
+ let f ru rt 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 xu m = b_type_of err (f xu) st m t in
- let f xu _ = f xu (BR.push m a (B.abst n xu)) in
+ let f ru m = b_type_of err (f ru) st m t 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) ->
- let f xt tt =
- f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+ | B.Bind (y, B.Void, t) ->
+ let f rt 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.Appl (a, v, t) ->
- let f xv vv xt tt =
- let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
- assert_applicability err f st m tt vv xv
+ 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 z (B.appl a)) (B.appl a rv tt) in
+ assert_applicability err f st m a tt vv rv
in
- let f xv vv = b_type_of err (f xv vv) st m t 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) ->
- let f xu xt tt =
- let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
- assert_convertibility err f st m xu tt xt
+ | B.Cast (u, t) ->
+ let f ru rt tt =
+ 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 xu _ = b_type_of err (f xu) st m t in
+ let f ru _ = b_type_of err (f ru) st m t in
type_of err f st m u
(* Interface functions ******************************************************)
-and type_of err f st m x = b_type_of err f st m x
+and type_of err f st m t = b_type_of err f st m t
+
+END
projects / helm.git / blobdiff