module C = Cps
module L = Log
module E = Entity
+module G = Options
module J = Marks
+module S = Status
module Z = Bag
module ZO = BagOutput
module ZE = BagEnvironment
(* Internal functions *******************************************************)
+let level = 4
+
let term_of_whdr = function
| Sort_ h -> Z.Sort h
| LRef_ (i, _) -> Z.LRef i
| GRef_ (_, uri, _) -> Z.GRef uri
| Bind_ (a, l, w, t) -> Z.bind_abst a l w t
-let level = 5
-
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
L.log ZO.specs level (L.et_items1 sc c st t)
in
whd aux c m x
-let ho_whd f c t =
- let f r = L.unbox level; f r in
- L.box level; log1 "Now scanning" c t;
+let ho_whd f st c t =
+ if !G.trace >= level then log1 "Now scanning" c t;
ho_whd f c empty_machine t
-let rec are_convertible f ~si a c m1 t1 m2 t2 =
+let rec are_convertible f st a c m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
let rec aux m1 r1 m2 r2 =
(* L.warn "entering R.are_convertible_aux"; *)
let u, t = term_of_whdr r1, term_of_whdr r2 in
- log2 "Now really converting" c u c t;
+ if !G.trace >= level then log2 "Now really converting" c u c t;
match r1, r2 with
| Sort_ h1, Sort_ h2 ->
if h1 = h2 then f a else f false
| LRef_ (i1, _), LRef_ (i2, _) ->
- if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ ((E.Apix a1 :: _), _, E.Abst _),
GRef_ ((E.Apix a2 :: _), _, E.Abst _) ->
- if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ ((E.Apix a1 :: _), _, E.Abbr v1),
GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) ->
if a1 = a2 then
let f a =
- if a then f a else are_convertible f ~si true c m1 v1 m2 v2
+ if a then f a else are_convertible f st true c m1 v1 m2 v2
in
- are_convertible_stacks f ~si a c m1 m2
+ are_convertible_stacks f st a c m1 m2
else
if a1 < a2 then whd (aux m1 r1) c m2 v2 else
whd (aux_rev m2 r2) c m1 v1
let l = J.new_location () in
let h c =
let m1, m2 = inc m1, inc m2 in
- let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
+ let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
ZS.subst f l l1 t1
in
let f r = if r then push "!" h c m1 a1 l w1 else f false in
- are_convertible f ~si a c m1 w1 m2 w2
+ are_convertible f st a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
- | Sort_ _, Bind_ (a2, l2, w2, t2) when si ->
+ | Sort_ _, Bind_ (a2, l2, w2, t2) when st.S.si ->
let m1, m2 = inc m1, inc m2 in
- let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in
+ let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
push "nsi" f c m2 a2 l2 w2
| _ -> f false
and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
let g m1 r1 = whd (aux m1 r1) c m2 t2 in
if a = false then f false else whd g c m1 t1
-and are_convertible_stacks f ~si a c m1 m2 =
+and are_convertible_stacks f st a c m1 m2 =
(* L.warn "entering R.are_convertible_stacks"; *)
let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
- let map f a v1 v2 = are_convertible f ~si a c mm1 v1 mm2 v2 in
+ let map f a v1 v2 = are_convertible f st a c mm1 v1 mm2 v2 in
if List.length m1.s <> List.length m2.s then
begin
(* L.warn (Printf.sprintf "Different lengths: %u %u"
else
C.list_fold_left2 f map a m1.s m2.s
-let are_convertible f ?(si=false) c u t =
- let f b = L.unbox level; f b in
- L.box level; log2 "Now converting" c u c t;
- are_convertible f ~si true c empty_machine u empty_machine t
+let are_convertible f st c u t =
+ if !G.trace >= level then log2 "Now converting" c u c t;
+ are_convertible f st true c empty_machine u empty_machine t