- let sc, st = s ^ " in the context", "the term" in
- L.log O.specs level (L.ct_items1 sc c st t)
-
-let log2 s c u t =
- let sc, su, st = s ^ " in the context", "the term", "and the term" in
- L.log O.specs level (L.ct_items2 sc c su u st t)
-
-let empty_machine = {
- c = B.empty_context; s = []
-}
-
-let get f c m i =
- let f e = function
- | Some (_, b) -> f e b
- | None -> error i
+ let sc, st = s ^ " in the environment", "the term" in
+ L.log O.specs level (L.et_items1 sc c st t)
+
+let log2 s cu u ct t =
+ let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+ L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+
+let are_alpha_convertible err f t1 t2 =
+ let rec aux f = function
+ | B.Sort (_, p1), B.Sort (_, p2)
+ | B.LRef (_, p1), B.LRef (_, p2) ->
+ if p1 = p2 then f () else err ()
+ | B.GRef (_, u1), B.GRef (_, u2) ->
+ if U.eq u1 u2 then f () else err ()
+ | B.Cast (_, v1, t1), B.Cast (_, v2, t2)
+ | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
+ let f _ = aux f (t1, t2) in
+ aux f (v1, v2)
+ | B.Bind (b1, t1), B.Bind (b2, t2) ->
+ let f _ = aux f (t1, t2) in
+ aux_bind f (b1, b2)
+ | _ -> err ()
+ and aux_bind f = function
+ | B.Abbr (_, v1), B.Abbr (_, v2)
+ | B.Abst (_, v1), B.Abst (_, v2) -> aux f (v1, v2)
+ | B.Void _, B.Void _ -> f ()
+ | _ -> err ()