KitCopy.ml 617 Bytes
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
(* This kit serves to construct a [copy] function for terms. *)

(* An environment maps atoms to atoms. *)

type env =
  Atom.atom Atom.Map.t

let empty =
  Atom.Map.empty

let lookup env x =
  try
    Atom.Map.find x env
  with Not_found ->
    (* Outside of its domain, the renaming acts as the identity. *)
    x

let extend x env =
  (* Generate a fresh copy of [x]. *)
  let x' = Atom.fresha x in
  (* Extend [env] when descending in the body. *)
  x', Atom.Map.add x x' env

class ['self] map = object (_ : 'self)
POTTIER Francois's avatar
POTTIER Francois committed
25 26
  method private extend x env = extend x env
  method private visit_'fn env x = lookup env x
POTTIER Francois's avatar
POTTIER Francois committed
27
end