Commit d4b59a0e authored by POTTIER Francois's avatar POTTIER Francois

Macros for [wf_term] and [wf_terms].

parent 3012ceb1
......@@ -143,7 +143,8 @@ let () =
let print_wf t =
printf "wf(%a) = %b\n%!"
nhprint t
(try wf_term t; true with IllFormed _ -> false)
(wf_term t)
let () =
evaluate print_wf
evaluate print_wf;
print_wf (TApp (id, id))
......@@ -14,15 +14,21 @@
the same time checks that no atom is bound twice, raising [IllFormed x]
if an atom [x] is bound twice -- possibly in different list elements. *)
(* [wf_term] is a variant of [ba_term] that returns no result, but can still
raise [IllFormed]. *)
(* [wf_term] is a variant of [ba_term] that returns a Boolean result. *)
(* [wf_terms] is a variant of [ba_term] that returns no result, but can still
raise [IllFormed]. *)
(* [wf_terms] is a variant of [ba_term] that returns a Boolean result. The
call [wf_terms ts] tests whether the terms in the list [ts] are well-formed
and pairwise bound-atom-disjoint. *)
(* [wf_term] and [wf_terms] should be used only in debugging mode, typically
in an [assert] construct. They print the identity of one offending atom
on the standard error channel. *)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
#define BAS_FUN(term) BA_FUN(CONCAT(term, s))
#define WF_FUN(term) CONCAT(wf_, term)
#define WFS_FUN(term) WF_FUN(CONCAT(term, s))
#define __BA \
exception IllFormed = KitBa.IllFormed \
......@@ -38,6 +44,10 @@
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (BA_FUN(term) t)) \
Atom.Set.empty ts \
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
(* -------------------------------------------------------------------------- *)
......
......@@ -132,20 +132,6 @@ let fa' : nominal_term -> Atom.Set.t =
__BA
BA(term)
(* [wf t] checks whether the term [t] is well-formed, and returns no result.
The exception [IllFormed x] is raised if the atom [x] occurs twice in a
binding position. *)
let wf_term t =
let (_ : Atom.Set.t) = ba_term t in ()
(* [disjoint ts] checks that the terms in the list [ts] are well-formed and
disjoint. The exception [IllFormed x] is raised if the atom [x] occurs
twice in a binding position. *)
let wf_terms ts =
let (_ : Atom.Set.t) = ba_terms ts in ()
(* -------------------------------------------------------------------------- *)
(* [filter p t] returns a free atom of the term [t] that satisfies the
......
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