Commit 01945269 authored by POTTIER Francois's avatar POTTIER Francois

Beginning of work on the [ba] macros.

parent 35a598cf
(* -------------------------------------------------------------------------- *)
(* [copy] returns a copy of its argument where every bound name has been
(* [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
position. *)
(* [ba_terms] computes the set of bound atoms of a list of terms and at
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_terms] is a variant of [ba_term] that returns no result, but can still
raise [IllFormed]. *)
#define __BA \
exception IllFormed = KitBa.IllFormed \
class ['self] __ba = object (_ : 'self) \
inherit [_] reduce \
inherit [_] KitBa.reduce \
end
#define BA(term) \
let CONCAT(ba_, term) t = \
new __ba # CONCAT(visit_, term) () t \
let CONCAT(ba_, CONCAT(term, s)) ts = \
List.fold_left \
(fun accu t -> Atom.Set.disjoint_union accu (CONCAT(ba_, term) t)) \
Atom.Set.empty ts \
(* -------------------------------------------------------------------------- *)
(* [copy_term] returns a copy of its argument where every bound name has been
replaced with a fresh copy, and every free name is unchanged. *)
#define __COPY \
......@@ -15,9 +49,9 @@
(* -------------------------------------------------------------------------- *)
(* [show] converts its argument to a raw term, in a NONHYGIENIC manner, using
[Atom.show] both at free name occurrences and bound name occurrences. It
is a debugging tool. *)
(* [show_term] converts its argument to a raw term, in a NONHYGIENIC manner,
using [Atom.show] both at free name occurrences and bound name occurrences.
It is a debugging tool. *)
#define __SHOW \
class ['self] __show = object (_ : 'self) \
......@@ -31,15 +65,16 @@
(* -------------------------------------------------------------------------- *)
(* [import] converts a raw term to a nominal term that satisfies the Global
Uniqueness Hypothesis, that is, a nominal term where every binding name
occurrence is represented by a unique atom. [import] expects every free
name occurrence to be in the domain of [env]. If that is not the case,
(* [import_term] converts a raw term to a nominal term that satisfies the
Global Uniqueness Hypothesis, that is, a nominal term where every binding
name occurrence is represented by a unique atom. [import] expects every
free name occurrence to be in the domain of [env]. If that is not the case,
the exception [Unbound] is raised. *)
(* TEMPORARY use string * loc so as to be able to give a location *)
#define __IMPORT \
exception Unbound = KitImport.Unbound \
class ['self] __import = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
......@@ -51,9 +86,9 @@
(* -------------------------------------------------------------------------- *)
(* [export] converts a nominal term to a raw term, in a hygienic manner. This
is the proper way of displaying a term. [export] expects every free name
occurrence to be in the domain of [env]. *)
(* [export_term] converts a nominal term to a raw term, in a hygienic manner.
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 ['self] __export = object (_ : 'self) \
......@@ -67,7 +102,7 @@
(* -------------------------------------------------------------------------- *)
(* [size] computes the size of its argument. *)
(* [size_term] computes the size of its argument. *)
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
......@@ -87,7 +122,7 @@
(* -------------------------------------------------------------------------- *)
(* [equiv] tests whether two terms are alpha-equivalent. *)
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
#define __EQUIV \
class __equiv = object \
......@@ -103,7 +138,8 @@
(* -------------------------------------------------------------------------- *)
(* [subst] applies a substitution to a nominal term, yielding a nominal term. *)
(* [subst_thing_term] applies a substitution to a nominal term, yielding a
nominal term. *)
(* A substitution is a finite map of atoms to nominal things. Things need not
be terms: this is a thing-in-term substitution, substituting things for
......
......@@ -129,39 +129,22 @@ let fa' : nominal_term -> Atom.Set.t =
(* -------------------------------------------------------------------------- *)
(* [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
position. *)
exception IllFormed = KitBa.IllFormed
class ['self] ba = object (_ : 'self)
inherit [_] reduce
inherit [_] KitBa.reduce
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
__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 t =
let (_ : Atom.Set.t) = ba t in ()
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 disjoint ts =
let (_ : Atom.Set.t) = ba_list ts in ()
let wf_terms ts =
let (_ : Atom.Set.t) = ba_terms ts in ()
(* -------------------------------------------------------------------------- *)
......
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