KitAvoids.ml 676 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 25
(* This kit serves to test whether the bound atoms of a term avoid a certain
   set of in-scope atoms and at the same time check that there is no shadowing
   inside this term (i.e., no atom is bound twice along a branch). *)

exception Shadowing of Atom.t

class ['self] iter = object (_ : 'self)

  method private extend x env =
    if Atom.Set.mem x env then
      (* There is shadowing: the atom [x] is already in scope. *)
      raise (Shadowing x)
    else
      Atom.Set.add x env

  method private visit_'fn _env _x = ()

end

let handle_Shadowing f env x =
  try
    f env x; true
  with Shadowing x ->
    Printf.eprintf "Shadowing: %s\n%!" (Atom.show x);
    false