KitFa.ml 3.32 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7
(* These kits serve to compute the free atoms of a term. *)

(* This computation can be viewed either as an instance of [iter], where the
   free atoms are accumulated in a reference, or as an instance of [reduce],
   where the free atoms are computed bottom-up. The latter approach uses set
   insertion operations, whereas the latter uses set union operations. *)

POTTIER Francois's avatar
POTTIER Francois committed
8 9 10 11 12 13 14
(* A micro-benchmark indicates that the [iter]-based computation consistently
   allocates less memory, especially in the major heap, yet the [reduce]-based
   computation consistently is slightly faster (by a few percent), perhaps
   because it does not involve mutable state, so does not have to suffer the
   write barrier. The micro-benchmark was carried out with randomly-generated
   closed lambda-terms. *)

POTTIER Francois's avatar
POTTIER Francois committed
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 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
(* -------------------------------------------------------------------------- *)

(* The auxiliary class [scope] defines the environment to be a set of atoms
   (the atoms that are currently in scope). It defines the method [extend]
   so as to update this set. *)

class ['self] scope = object (_ : 'self)
  method private extend = Atom.Set.add
end

(* -------------------------------------------------------------------------- *)

(* The auxiliary class [free] inherits [scope] and further defines the method
   [visit_'fn] so that, at a free name occurrence: -1. if the name is local,
   nothing happens; -2. if the name is free, then the method [visit_free] is
   invoked. *)

class virtual ['self] free = object (self : 'self)
  inherit [_] scope
  method private visit_'fn env x =
    if not (Atom.Set.mem x env) then
      self#visit_free x
  method virtual visit_free: _
end

(* -------------------------------------------------------------------------- *)

(* Computing the free atoms of a term, via [iter]. *)

(* The environment is a set of atoms (the atoms that are currently in scope). *)

(* We use a mutable instance variable to keep track of the free atoms that
   have been accumulated so far. (One could also use a reference and store
   it in the environment, which would then be a pair. That would be slightly
   clumsier.) *)

type env =
  Atom.Set.t

let empty =
  Atom.Set.empty

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

  val mutable accu = Atom.Set.empty

  method accu = accu (* must be public *)

  method private visit_free x =
    accu <- Atom.Set.add x accu

end

(* -------------------------------------------------------------------------- *)

(* Computing the free atoms of a term, via [reduce]. *)

(* In this style, no environment is required. *)

(* type env = unit *)

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

  (* The monoid of sets of atoms is used. *)
POTTIER Francois's avatar
POTTIER Francois committed
80
  inherit [_] Atom.Set.union_monoid
POTTIER Francois's avatar
POTTIER Francois committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107

  method private extend _x () = ()

  (* The atom [x] is removed from the set of free atoms when the scope of [x]
     is exited. *)
  method private restrict = Atom.Set.remove

  method private visit_'fn () x = Atom.Set.singleton x

end

(* -------------------------------------------------------------------------- *)

(* Testing whether a term has a free atom that satisfies a predicate [p]. *)

exception Found of Atom.t

class filter (p : Atom.t -> bool) = object
  inherit [_] free
  method visit_free x =
    if p x then
      raise (Found x)
end

let wrap (f : 'term -> unit) : 'term -> Atom.t option =
  fun t ->
    try f t; None with Found x -> Some x