Commit 2e871443 authored by POTTIER Francois's avatar POTTIER Francois

More macros for naming conventions.

parent 69947333
......@@ -124,7 +124,7 @@ let print_equiv t1 t2 =
printf "equiv: %a ~ %a = %b\n%!"
nhprint t1
nhprint t2
(equiv t1 t2)
(equiv_term t1 t2)
let () =
print_equiv id id;
......@@ -143,7 +143,7 @@ let () =
let print_wf t =
printf "wf(%a) = %b\n%!"
nhprint t
(try wf t; true with IllFormed _ -> false)
(try wf_term t; true with IllFormed _ -> false)
let () =
evaluate print_wf
......@@ -20,8 +20,9 @@
(* [wf_terms] is a variant of [ba_term] that returns no result, but can still
raise [IllFormed]. *)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
#define BAS_FUN(term) BA_FUN(CONCAT(term, s))
#define __BA \
exception IllFormed = KitBa.IllFormed \
......@@ -33,7 +34,7 @@
#define BA(term) \
let BA_FUN(term) t = \
new BA_CLASS # VISIT(term) () t \
let CONCAT(ba_, CONCAT(term, s)) ts = \
let BAS_FUN(term) ts = \
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (BA_FUN(term) t)) \
Atom.Set.empty ts \
......@@ -62,7 +63,8 @@
using [Atom.show] both at free name occurrences and bound name occurrences.
It is a debugging tool. *)
#define SHOW_CLASS __show
#define SHOW_CLASS __show
#define SHOW_FUN(term) CONCAT(show_, term)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
......@@ -71,7 +73,7 @@
end
#define SHOW(term) \
let CONCAT(show_, term) t = \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t
(* -------------------------------------------------------------------------- *)
......@@ -84,7 +86,8 @@
(* TEMPORARY use string * loc so as to be able to give a location *)
#define IMPORT_CLASS __import
#define IMPORT_CLASS __import
#define IMPORT_FUN(term) CONCAT(import_, term)
#define __IMPORT \
exception Unbound = KitImport.Unbound \
......@@ -94,7 +97,7 @@
end
#define IMPORT(term) \
let CONCAT(import_, term) env t = \
let IMPORT_FUN(term) env t = \
new IMPORT_CLASS # VISIT(term) env t
(* -------------------------------------------------------------------------- *)
......@@ -103,7 +106,8 @@
This is the proper way of displaying a term. [export] expects every free
name occurrence to be in the domain of [env]. *)
#define EXPORT_CLASS __export
#define EXPORT_CLASS __export
#define EXPORT_FUN(term) CONCAT(export_, term)
#define __EXPORT \
class ['self] EXPORT_CLASS = object (_ : 'self) \
......@@ -112,7 +116,7 @@
end
#define EXPORT(term) \
let CONCAT(export_, term) env t = \
let EXPORT_FUN(term) env t = \
new EXPORT_CLASS # VISIT(term) env t
(* -------------------------------------------------------------------------- *)
......@@ -122,7 +126,8 @@
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
#define SIZE_CLASS __size
#define SIZE_CLASS __size
#define SIZE_FUN(term) CONCAT(size_, term)
#define __SIZE \
class ['self] SIZE_CLASS = object (_ : 'self) \
......@@ -134,14 +139,15 @@
end
#define SIZE(term) \
let CONCAT(size_, term) t = \
let SIZE_FUN(term) t = \
new SIZE_CLASS # VISIT(term) () t
(* -------------------------------------------------------------------------- *)
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
#define EQUIV_CLASS __equiv
#define EQUIV_CLASS __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
#define __EQUIV \
class EQUIV_CLASS = object \
......@@ -150,7 +156,7 @@
end
#define EQUIV(term) \
let equiv t1 t2 = \
let EQUIV_FUN(term) t1 t2 = \
VisitorsRuntime.wrap2 \
(new EQUIV_CLASS # VISIT(term) KitEquiv.empty) \
t1 t2
......
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