Commit 542e762d authored by POTTIER Francois's avatar POTTIER Francois

More macros.

parent 21d89337
......@@ -84,3 +84,19 @@
#define SIZE(term) \
let CONCAT(size_, term) t = \
new size # CONCAT(visit_, term) () t
(* -------------------------------------------------------------------------- *)
(* [equiv] tests whether two terms are alpha-equivalent. *)
#define __EQUIV \
class equiv = object \
inherit [_] iter2 \
inherit [_] KitEquiv.iter2 \
end
#define EQUIV(term) \
let equiv t1 t2 = \
VisitorsRuntime.wrap2 \
(new equiv # CONCAT(visit_, term) KitEquiv.empty) \
t1 t2
......@@ -99,6 +99,9 @@ EXPORT(term)
__SIZE
SIZE(term)
__EQUIV
EQUIV(term)
(* -------------------------------------------------------------------------- *)
(* [fa] computes the free atoms of a term. *)
......@@ -164,18 +167,6 @@ let subst1 u x t =
(* -------------------------------------------------------------------------- *)
(* [equiv] tests whether two terms are alpha-equivalent. *)
class equiv = object
inherit [_] iter2
inherit [_] KitEquiv.iter2
end
let equiv : nominal_term -> nominal_term -> bool =
VisitorsRuntime.wrap2 (new equiv # visit_term KitEquiv.empty)
(* -------------------------------------------------------------------------- *)
(* [ba] computes the set of bound atoms of a term and (at the same time)
checks that this term is well-formed, that is, no atom is bound twice. The
exception [IllFormed x] is raised if the atom [x] occurs twice in a binding
......
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