Commit 6219e27d authored by POTTIER Francois's avatar POTTIER Francois

Macros for [filter], [closed], [occurs].

parent d4b59a0e
......@@ -5,6 +5,37 @@
(* -------------------------------------------------------------------------- *)
(* [filter_term p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
(* [closed_term t] tests whether the term [t] is closed, that is, whether
[t] has no free atom. *)
(* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
#define FILTER_CLASS __filter
#define FILTER_FUN(term) CONCAT(filter_, term)
#define CLOSED_FUN(term) CONCAT(closed_, term)
#define OCCURS_FUN(term) CONCAT(occurs_, term)
#define __FILTER \
class FILTER_CLASS p = object \
inherit [_] iter \
inherit KitFa.filter p \
end \
#define FILTER(term) \
let FILTER_FUN(term) p t = \
KitFa.wrap ((new FILTER_CLASS p) # VISIT(term) KitFa.empty) t \
let CLOSED_FUN(term) t = \
match FILTER_FUN(term) (fun _ -> true) t with \
| None -> true \
| Some _ -> false \
let OCCURS_FUN(term) x t = \
FILTER_FUN(term) (fun y -> Atom.equal x y) t \
(* -------------------------------------------------------------------------- *)
(* [ba_term] 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
......@@ -35,7 +66,7 @@
class ['self] BA_CLASS = object (_ : 'self) \
inherit [_] reduce \
inherit [_] KitBa.reduce \
end
end \
#define BA(term) \
let BA_FUN(term) t = \
......@@ -47,7 +78,7 @@
let WF_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion BA_FUN(term) t \
let WFS_FUN(term) t = \
Atom.Set.handle_NonDisjointUnion BAS_FUN(term) t
Atom.Set.handle_NonDisjointUnion BAS_FUN(term) t \
(* -------------------------------------------------------------------------- *)
......@@ -61,11 +92,11 @@
class ['self] COPY_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitCopy.map \
end
end \
#define COPY(term) \
let COPY_FUN(term) t = \
new COPY_CLASS # VISIT(term) KitCopy.empty t
new COPY_CLASS # VISIT(term) KitCopy.empty t \
(* -------------------------------------------------------------------------- *)
......@@ -80,11 +111,11 @@
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
......@@ -104,11 +135,11 @@
class ['self] IMPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
end
end \
#define IMPORT(term) \
let IMPORT_FUN(term) env t = \
new IMPORT_CLASS # VISIT(term) env t
new IMPORT_CLASS # VISIT(term) env t \
(* -------------------------------------------------------------------------- *)
......@@ -123,11 +154,11 @@
class ['self] EXPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitExport.map \
end
end \
#define EXPORT(term) \
let EXPORT_FUN(term) env t = \
new EXPORT_CLASS # VISIT(term) env t
new EXPORT_CLASS # VISIT(term) env t \
(* -------------------------------------------------------------------------- *)
......@@ -146,11 +177,11 @@
inherit [_] VisitorsRuntime.addition_monoid \
method! VISIT(term) env t = \
1 + super # VISIT(term) env t \
end
end \
#define SIZE(term) \
let SIZE_FUN(term) t = \
new SIZE_CLASS # VISIT(term) () t
new SIZE_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
......@@ -163,13 +194,13 @@
class EQUIV_CLASS = object \
inherit [_] iter2 \
inherit [_] KitEquiv.iter2 \
end
end \
#define EQUIV(term) \
let EQUIV_FUN(term) t1 t2 = \
VisitorsRuntime.wrap2 \
(new EQUIV_CLASS # VISIT(term) KitEquiv.empty) \
t1 t2
t1 t2 \
(* -------------------------------------------------------------------------- *)
......@@ -206,10 +237,12 @@
inherit [_] KitSubst.map \
method! private VISIT(Var) sigma this x = \
KitSubst.apply COPY_FUN(thing) sigma this x \
end
end \
#define SUBST(thing, term) \
let SUBST_FUN(thing, term) sigma t = \
new SUBST_CLASS(thing) # VISIT(term) sigma t \
let SUBST_FUN1(thing, term) u x t = \
SUBST_FUN(thing, term) (Atom.Map.singleton x u) t
SUBST_FUN(thing, term) (Atom.Map.singleton x u) t \
(* -------------------------------------------------------------------------- *)
......@@ -84,6 +84,12 @@ type nominal_term =
(* -------------------------------------------------------------------------- *)
__FILTER
FILTER(term)
__BA
BA(term)
__COPY
COPY(term)
......@@ -129,37 +135,4 @@ let fa' : nominal_term -> Atom.Set.t =
(* -------------------------------------------------------------------------- *)
__BA
BA(term)
(* -------------------------------------------------------------------------- *)
(* [filter p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
(* [pick_fa t] returns a free atom of the term [t], if there is one. *)
(* [closed t] tests whether the term [t] is closed, i.e., has no free atom. *)
(* [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 =
KitFa.wrap ((new filter p) # visit_term KitFa.empty)
let pick_fa : nominal_term -> Atom.t option =
filter (fun _ -> true)
let closed (t : nominal_term) : bool =
match pick_fa t with None -> true | Some _ -> false
let occurs x =
filter (fun y -> Atom.equal x y)
(* -------------------------------------------------------------------------- *)
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