+ L.box level; log1 "Now scanning" c t;
+ step f ~delta:true ~rt:true c empty_machine t
+
+let rec ac_nfs f ~si r c m1 u m2 t =
+(* L.warn "entering R.are_convertible_aux"; *)
+ log2 "Now converting nfs" c u t;
+ match u, t with
+ | B.Sort (_, h1), B.Sort (_, h2) ->
+ if h1 = h2 then f r else f false
+ | B.LRef (B.Entry (e1, B.Abst _) :: _, i1),
+ B.LRef (B.Entry (e2, B.Abst _) :: _, i2) ->
+ P.add ~zeta:(i1+i2-e1-e2) ();
+ if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
+ | B.GRef (B.Entry (e1, B.Abst _) :: _, _),
+ B.GRef (B.Entry (e2, B.Abst _) :: _, _) ->
+ if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
+ | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _),
+ B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) ->
+ if e1 = e2 then
+ let f r =
+ if r then f r
+ else begin
+ P.add ~gdelta:2 ();
+ ac f ~si true c m1 v1 m2 v2
+ end
+ in
+ ac_stacks f ~si r c m1 m2
+ else if e1 < e2 then begin
+ P.add ~gdelta:1 ();
+ step (ac_nfs f ~si r c m1 u) c m2 v2
+ end else begin
+ P.add ~gdelta:1 ();
+ step (ac_nfs_rev f ~si r c m2 t) c m1 v1
+ end
+ | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
+ P.add ~gdelta:1 ();
+ step (ac_nfs f ~si r c m1 u) c m2 v2
+ | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
+ P.add ~gdelta:1 ();
+ step (ac_nfs_rev f ~si r c m2 t) c m1 v1
+ | B.Bind (a1, (B.Abst w1 as b1), t1),
+ B.Bind (a2, (B.Abst w2 as b2), t2) ->
+ let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in
+ let g m1 = push (g m1) m2 a2 b2 in
+ let f r = if r then push g m1 a1 b1 else f false in
+ ac f ~si r c m1 w1 m2 w2
+ | B.Sort _, B.Bind (a, b, t) when si ->
+ P.add ~si:1 ();
+ let f m1 m2 = ac f ~si r c m1 u m2 t in
+ let f m1 = push (f m1) m2 a b in
+ push f m1 a b
+ | _ -> f false
+
+and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t
+
+and ac f ~si r c m1 t1 m2 t2 =
+(* L.warn "entering R.are_convertible"; *)
+ let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in
+ if r = false then f false else step g c m1 t1
+
+and ac_stacks f ~si r c m1 m2 =
+(* L.warn "entering R.are_convertible_stacks"; *)
+ let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
+ let map f r (v1, h1) (v2, h2) =
+ let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in
+ S.lift f h1 (0) v1
+ in
+ if List.length m1.s <> List.length m2.s then
+ begin
+(* L.warn (Printf.sprintf "Different lengths: %u %u"
+ (List.length m1.s) (List.length m2.s)
+ ); *)
+ f false
+ end
+ else
+ C.list_fold_left2 f map r m1.s m2.s