KitAvoid.ml 589 Bytes
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13
(* This kit serves to construct an [avoid] function for terms. This
   function renames the bound names of a term, if necessary, so as
   to avoid a certain set of bad names. *)

type env =
  KitCopy.env

let empty =
  KitCopy.empty

let lookup =
  KitCopy.lookup

14
let extend bad env x =
POTTIER Francois's avatar
POTTIER Francois committed
15 16
  (* If [x] is bad, it must be renamed. Otherwise, keep it. *)
  if Atom.Set.mem x bad then
17
    KitCopy.extend env x
POTTIER Francois's avatar
POTTIER Francois committed
18
  else
19
    env, x
POTTIER Francois's avatar
POTTIER Francois committed
20 21

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