Commit 87136d34 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A comment and a small refactoring.

parent 13c6b59c
...@@ -91,6 +91,9 @@ type debruijn_term = ...@@ -91,6 +91,9 @@ type debruijn_term =
(* [size] computes the size of its argument. *) (* [size] computes the size of its argument. *)
(* Beware: this counts the nodes whose type is [term] nodes, but does not count
the nodes of other types. *)
class ['self] size = object (_ : 'self) class ['self] size = object (_ : 'self)
inherit [_] reduce as super inherit [_] reduce as super
inherit [_] KitTrivial.reduce inherit [_] KitTrivial.reduce
...@@ -299,12 +302,13 @@ let wf t = ...@@ -299,12 +302,13 @@ let wf t =
(* [occurs x t] tests whether the atom [x] occurs free in [t]. *) (* [occurs x t] tests whether the atom [x] occurs free in [t]. *)
class filter p = object
inherit [_] iter
inherit KitFa.filter p
end
let filter p : nominal_term -> Atom.t option = let filter p : nominal_term -> Atom.t option =
let filter = object KitFa.wrap ((new filter p) # visit_term KitFa.empty)
inherit [_] iter
inherit KitFa.filter p
end in
KitFa.wrap (filter # visit_term KitFa.empty)
let pick_fa : nominal_term -> Atom.t option = let pick_fa : nominal_term -> Atom.t option =
filter (fun _ -> true) filter (fun _ -> true)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment