(* Interface functions ******************************************************)
let rec b_type_of f g c x =
+(* L.warn "Entering T.b_type_of"; *)
log1 "Now checking" c x;
match x with
| B.Sort h ->
f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt)
in
let f xv cc = b_type_of (f xv) g cc t in
- let f xv = B.push (f xv) c l id (B.Abbr xv) in
+ let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> f (B.Cast (vv, xv))
f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt)
in
let f xu cc = b_type_of (f xu) g cc t in
- let f xu _ = B.push (f xu) c l id (B.Abst xu) in
+ let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in
type_of f g c u
| B.Bind (l, id, B.Void, t) ->
let f xt tt =
f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt)
in
let f cc = b_type_of f g cc t in
- B.push f c l id B.Void
+ B.push "type void" f c l id B.Void
| B.Appl (v, t) ->
let f xv vv xt tt = function
| R.Abst w ->
L.log O.specs (succ level) (L.t_items1 "Just scanned" c w);
L.unbox (succ level);
let f a =
- L.box (succ level);
- L.warn (Printf.sprintf "Convertible: %b" a);
- L.unbox (succ level);
+(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt)
else error3 c xv vv w
in
type_of f g c v
| B.Cast (u, t) ->
let f xu xt tt a =
- L.box (succ level);
- L.warn (Printf.sprintf "Convertible: %b" a);
- L.unbox (succ level);
+ (* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu
in
let f xu xt tt = R.are_convertible (f xu xt tt) c xu tt in