From cb4a6b537f02b3efff1d9d7ca7dd0b8cf2bc0d3e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Wed, 1 Feb 2017 09:04:28 +0100
Subject: [PATCH] Added [disjoint].
---
src/Toolbox.cppo.ml | 15 ++++++++++++---
1 file changed, 12 insertions(+), 3 deletions(-)
diff --git a/src/Toolbox.cppo.ml b/src/Toolbox.cppo.ml
index b9aacf4..a2efe8d 100644
--- a/src/Toolbox.cppo.ml
+++ b/src/Toolbox.cppo.ml
@@ -144,15 +144,24 @@ end
let ba : nominal_term -> Atom.Set.t =
new ba # visit_term ()
+let ba_list ts =
+ List.fold_left
+ (fun accu t -> Atom.Set.disjoint_union accu (ba t))
+ Atom.Set.empty ts
+
(* [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.*)
+ binding position. *)
let wf t =
let (_ : Atom.Set.t) = ba t in ()
-(* TEMPORARY add a disjointness check; this boils down to checking that a
- list of terms is well-formed. *)
+(* [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 disjoint ts =
+ let (_ : Atom.Set.t) = ba_list ts in ()
(* -------------------------------------------------------------------------- *)
--
GitLab