KitEquiv.ml 1.26 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
(* This kit serves to construct an alpha-equivalence test. *)

(* The environment contains two maps of atoms to de Bruijn levels, as well as
   the current de Bruijn level. The equivalence test can in fact be viewed as
   two independent conversions to a locally-nameless representation, followed
   with a syntactic comparison of the two terms thus obtained. *)

type m =
  int Atom.Map.t

type env =
  m * m * int

let empty =
  Atom.Map.empty, Atom.Map.empty, 0

type status =
  | Local of int (* a de Bruijn level *)
  | Free         (* a free name *)

let lookup (m : m) (x : Atom.t) : status =
  try
    (* A local name. *)
    Local (Atom.Map.find x m)
  with Not_found ->
    Free

let extend (m : m) (n : int) (x : Atom.t) : m =
  Atom.Map.add x n m

let extend x1 x2 (m1, m2, n) =
  let m1 = extend m1 n x1
  and m2 = extend m2 n x2
  and n = n + 1 in
  m1, m2, n

let lookup (m1, m2, _) x1 x2 =
  match lookup m1 x1, lookup m2 x2 with
  | Local i1, Local i2 ->
      if i1 <> i2 then
        VisitorsRuntime.fail()
  | Free, Free ->
      if not (Atom.equal x1 x2) then
        VisitorsRuntime.fail()
  | Local _, Free
  | Free, Local _ ->
      VisitorsRuntime.fail()

class ['self] iter2 = object (_ : 'self)
  method private extend = extend
  method private visit_'fn = lookup
end