AlphaLibMacros.cppo.ml 15.1 KB
Newer Older
1
(* The conventional name of the visitor methods. *)
POTTIER Francois's avatar
POTTIER Francois committed
2 3 4 5

#define VISIT(term)                                                            \
  CONCAT(visit_, term)

6
(* -------------------------------------------------------------------------- *)
POTTIER Francois's avatar
POTTIER Francois committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

(* [fa_term] computes the set of the free atoms of a term. *)

#define FA_CLASS     __fa
#define FA_FUN(term) CONCAT(fa_, term)

#define __FA                                                                   \
  class FA_CLASS = object                                                      \
    inherit [_] reduce                                                         \
    inherit [_] KitFa.reduce                                                   \
  end                                                                          \

#define FA(term)                                                               \
  let FA_FUN(term) t =                                                         \
    new FA_CLASS # VISIT(term) () t                                            \

(* -------------------------------------------------------------------------- *)
24

25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
(* [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 =                                                   \
52
    match FILTER_FUN(term) (fun y -> Atom.equal x y) t with                    \
53 54
    | None -> false                                                            \
    | Some _ -> true                                                           \
55 56 57

(* -------------------------------------------------------------------------- *)

58 59 60 61 62 63 64 65 66
(* [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. *)

67
(* [wf_term] is a variant of [ba_term] that returns a Boolean result. *)
68

69 70 71 72 73 74 75
(* [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. *)
76

77 78 79
#define BA_CLASS      __ba
#define BA_FUN(term)  CONCAT(ba_, term)
#define BAS_FUN(term) BA_FUN(CONCAT(term, s))
80 81
#define WF_FUN(term)  CONCAT(wf_, term)
#define WFS_FUN(term) WF_FUN(CONCAT(term, s))
82

83 84
#define __BA                                                                   \
  exception IllFormed = KitBa.IllFormed                                        \
85
  class ['self] BA_CLASS = object (_ : 'self)                                  \
86 87
    inherit [_] reduce                                                         \
    inherit [_] KitBa.reduce                                                   \
88
  end                                                                          \
89 90

#define BA(term)                                                               \
91 92
  let BA_FUN(term) t =                                                         \
    new BA_CLASS # VISIT(term) () t                                            \
93
  let BAS_FUN(term) ts =                                                       \
94
    List.fold_left                                                             \
95
      (fun accu t -> Atom.Set.disjoint_union accu (BA_FUN(term) t))            \
96
      Atom.Set.empty ts                                                        \
97 98 99
  let WF_FUN(term) t =                                                         \
    Atom.Set.handle_NonDisjointUnion BA_FUN(term) t                            \
  let WFS_FUN(term) t =                                                        \
100
    Atom.Set.handle_NonDisjointUnion BAS_FUN(term) t                           \
101 102 103 104

(* -------------------------------------------------------------------------- *)

(* [copy_term] returns a copy of its argument where every bound name has been
105 106
   replaced with a fresh copy, and every free name is unchanged. *)

107 108 109
#define COPY_CLASS     __copy
#define COPY_FUN(term) CONCAT(copy_, term)

110
#define __COPY                                                                 \
111
  class ['self] COPY_CLASS = object (_ : 'self)                                \
112 113
    inherit [_] map                                                            \
    inherit [_] KitCopy.map                                                    \
114
  end                                                                          \
115 116

#define COPY(term)                                                             \
117
  let COPY_FUN(term) t =                                                       \
118
    new COPY_CLASS # VISIT(term) KitCopy.empty t                               \
119 120 121

(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
(* [avoid_term bad] returns a copy of its argument where some bound names have
   been replaced with a fresh copy, so as to ensure that no bound name is in
   the set [bad]. *)

#define AVOID_CLASS     __avoid
#define AVOID_FUN(term) CONCAT(avoid_, term)

#define __AVOID                                                                \
  class ['self] AVOID_CLASS bad = object (_ : 'self)                           \
    inherit [_] map                                                            \
    inherit [_] KitAvoid.map bad                                               \
  end                                                                          \

#define AVOID(term)                                                            \
  let AVOID_FUN(term) bad t =                                                  \
    (new AVOID_CLASS bad) # VISIT(term) KitAvoid.empty t                       \

(* -------------------------------------------------------------------------- *)

141 142 143
(* [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. *)
144

145 146
#define SHOW_CLASS     __show
#define SHOW_FUN(term) CONCAT(show_, term)
147

148
#define __SHOW                                                                 \
149
  class ['self] SHOW_CLASS = object (_ : 'self)                                \
150 151
    inherit [_] map                                                            \
    inherit [_] KitShow.map                                                    \
152
  end                                                                          \
153 154

#define SHOW(term)                                                             \
155
  let SHOW_FUN(term) t =                                                       \
156
    new SHOW_CLASS # VISIT(term) () t                                          \
157 158 159

(* -------------------------------------------------------------------------- *)

160 161 162 163
(* [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,
164 165 166 167
   the exception [Unbound] is raised. *)

(* TEMPORARY use string * loc so as to be able to give a location *)

168 169
#define IMPORT_CLASS     __import
#define IMPORT_FUN(term) CONCAT(import_, term)
170

171
#define __IMPORT                                                               \
172
  exception Unbound = KitImport.Unbound                                        \
173
  class ['self] IMPORT_CLASS = object (_ : 'self)                              \
174 175
    inherit [_] map                                                            \
    inherit [_] KitImport.map                                                  \
176
  end                                                                          \
177 178

#define IMPORT(term)                                                           \
179
  let IMPORT_FUN(term) env t =                                                 \
180
    new IMPORT_CLASS # VISIT(term) env t                                       \
181 182 183

(* -------------------------------------------------------------------------- *)

184 185 186
(* [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]. *)
187

188 189
#define EXPORT_CLASS     __export
#define EXPORT_FUN(term) CONCAT(export_, term)
190

191
#define __EXPORT                                                               \
192
  class ['self] EXPORT_CLASS = object (_ : 'self)                              \
193 194
    inherit [_] map                                                            \
    inherit [_] KitExport.map                                                  \
195
  end                                                                          \
196 197

#define EXPORT(term)                                                           \
198
  let EXPORT_FUN(term) env t =                                                 \
199
    new EXPORT_CLASS # VISIT(term) env t                                       \
200 201 202

(* -------------------------------------------------------------------------- *)

203
(* [size_term] computes the size of its argument. *)
204 205 206 207

(* Beware: this counts the nodes whose type is [term], but does not count the
   nodes of other types. *)

208 209
#define SIZE_CLASS     __size
#define SIZE_FUN(term) CONCAT(size_, term)
210

211
#define __SIZE                                                                 \
212
  class ['self] SIZE_CLASS = object (_ : 'self)                                \
213 214 215
    inherit [_] reduce as super                                                \
    inherit [_] KitTrivial.reduce                                              \
    inherit [_] VisitorsRuntime.addition_monoid                                \
POTTIER Francois's avatar
POTTIER Francois committed
216 217
    method! VISIT(term) env t =                                                \
      1 + super # VISIT(term) env t                                            \
218
  end                                                                          \
219 220

#define SIZE(term)                                                             \
221
  let SIZE_FUN(term) t =                                                       \
222
    new SIZE_CLASS # VISIT(term) () t                                          \
POTTIER Francois's avatar
POTTIER Francois committed
223 224 225

(* -------------------------------------------------------------------------- *)

226
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
POTTIER Francois's avatar
POTTIER Francois committed
227

228 229
#define EQUIV_CLASS     __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
230

POTTIER Francois's avatar
POTTIER Francois committed
231
#define __EQUIV                                                                \
232
  class EQUIV_CLASS = object                                                   \
POTTIER Francois's avatar
POTTIER Francois committed
233 234
    inherit [_] iter2                                                          \
    inherit [_] KitEquiv.iter2                                                 \
235
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
236 237

#define EQUIV(term)                                                            \
238
  let EQUIV_FUN(term) t1 t2 =                                                  \
POTTIER Francois's avatar
POTTIER Francois committed
239
    VisitorsRuntime.wrap2                                                      \
240
      (new EQUIV_CLASS # VISIT(term) KitEquiv.empty)                           \
241
      t1 t2                                                                    \
POTTIER Francois's avatar
POTTIER Francois committed
242 243 244

(* -------------------------------------------------------------------------- *)

245 246 247 248 249
(* [subst_thing_term] applies a substitution to a nominal term,
   yielding a nominal term. *)

(* [subst_thing_term1] applies a singleton substitution to a nominal term,
   yielding a nominal term. *)
POTTIER Francois's avatar
POTTIER Francois committed
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267

(* 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
   variables in terms. *)

(* When applying a substitution [sigma] to a term [t], the GUH guarantees that
   the free atoms of (the codomain of) [sigma] cannot be captured by a binder
   within [t]. The GUH also guarantees that a binder within [t] cannot appear
   in the domain of [sigma], which means that we can go down into [t] and apply
   [sigma] to every variable. *)

(* The GUH is preserved by copying the things that are grafted into [t]. Thus,
   it is not even necessary that [sigma] and [t] be disjoint, or that the
   things in the codomain of [sigma] be pairwise disjoint. One should note,
   however, that the result of the substitution is not disjoint with [t], so
   one should no longer use [t] after the substitution (or, one should apply
   the substitution to a copy). *)

268 269 270 271
#define SUBST_CLASS(thing)      CONCAT(__subst_, thing)
#define SUBST_FUN(thing, term)  CONCAT(subst_, CONCAT(thing, CONCAT(_, term)))
#define SUBST_FUN1(thing, term) CONCAT(SUBST_FUN(thing, term), 1)

POTTIER Francois's avatar
POTTIER Francois committed
272
#define __SUBST(thing, Var)                                                    \
273
  class SUBST_CLASS(thing) = object                                            \
POTTIER Francois's avatar
POTTIER Francois committed
274 275
    inherit [_] endo (* we could also use [map] *)                             \
    inherit [_] KitSubst.map                                                   \
276 277
    method! private VISIT(Var) sigma this x =                                  \
      KitSubst.apply COPY_FUN(thing) sigma this x                              \
278
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
279 280

#define SUBST(thing, term)                                                     \
281 282 283
  let SUBST_FUN(thing, term) sigma t =                                         \
    new SUBST_CLASS(thing) # VISIT(term) sigma t                               \
  let SUBST_FUN1(thing, term) u x t =                                          \
284 285 286
    SUBST_FUN(thing, term) (Atom.Map.singleton x u) t                          \

(* -------------------------------------------------------------------------- *)