Commit a5b3a04d authored by POTTIER Francois's avatar POTTIER Francois

Macros for [fa].

parent d920b8a3
......@@ -5,6 +5,23 @@
(* -------------------------------------------------------------------------- *)
(* [fa_term] computes the set of the free atoms of a term. *)
#define FA_CLASS __fa
#define FA_FUN(term) CONCAT(fa_, term)
#define __FA \
class FA_CLASS = object \
inherit [_] reduce \
inherit [_] KitFa.reduce \
end \
#define FA(term) \
let FA_FUN(term) t = \
new FA_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* [filter_term p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
......
......@@ -84,6 +84,9 @@ type nominal_term =
#include "AlphaLibMacros.cppo.ml"
__FA
FA(term)
__FILTER
FILTER(term)
......@@ -113,16 +116,4 @@ SUBST(term, term)
(* -------------------------------------------------------------------------- *)
(* [fa] computes the free atoms of a term. *)
class fa = object
inherit [_] reduce
inherit [_] KitFa.reduce
end
let fa : nominal_term -> Atom.Set.t =
new fa # visit_term ()
(* -------------------------------------------------------------------------- *)
end
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