AlphaLibMacros.cppo.ml 16.3 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
(* [ba_term] computes the set of bound atoms of a term. *)
59

POTTIER Francois's avatar
POTTIER Francois committed
60 61
#define BA_CLASS     __ba
#define BA_FUN(term) CONCAT(ba_, term)
62

63
#define __BA                                                                   \
64
  class ['self] BA_CLASS = object (_ : 'self)                                  \
65 66
    inherit [_] reduce                                                         \
    inherit [_] KitBa.reduce                                                   \
67
  end                                                                          \
68 69

#define BA(term)                                                               \
70 71
  let BA_FUN(term) t =                                                         \
    new BA_CLASS # VISIT(term) () t                                            \
72 73 74

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

POTTIER Francois's avatar
POTTIER Francois committed
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
(* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
   that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
   that is, no atom is bound twice along a branch. It returns [true] if these
   two conditions are satisfied. *)

#define AVOIDS_CLASS     __avoids
#define AVOIDS_FUN(term) CONCAT(avoids_, term)

#define __AVOIDS                                                               \
  class ['self] AVOIDS_CLASS = object (_ : 'self)                              \
    inherit [_] iter                                                           \
    inherit [_] KitAvoids.iter                                                 \
  end                                                                          \

#define AVOIDS(term)                                                           \
  let AVOIDS_FUN(term) env t =                                                 \
    KitAvoids.handle_Shadowing (new AVOIDS_CLASS # VISIT(term)) env t          \

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

95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
   is bound twice within this term (not even along different branches). *)

(* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
   no atom is bound twice within this list (not even within two distinct list
   elements). *)

(* [guq_term] and [guq_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 GUQ_CLASS      __guq
#define GUQ_FUN(term)  CONCAT(guq_, term)
#define GUQS_FUN(term) GUQ_FUN(CONCAT(term, s))

#define __GUQ                                                                  \
  class ['self] GUQ_CLASS = object (_ : 'self)                                 \
    inherit [_] reduce                                                         \
    inherit [_] KitGuq.reduce                                                  \
  end                                                                          \

#define GUQ(term)                                                              \
  let GUQ_FUN(term) t =                                                        \
    new GUQ_CLASS # VISIT(term) () t                                           \
  let GUQS_FUN(term) ts =                                                      \
120
    List.fold_left                                                             \
121
      (fun accu t -> Atom.Set.disjoint_union accu (GUQ_FUN(term) t))           \
122
      Atom.Set.empty ts                                                        \
123 124 125 126
  let GUQ_FUN(term) t =                                                        \
    Atom.Set.handle_NonDisjointUnion GUQ_FUN(term) t                           \
  let GUQS_FUN(term) t =                                                       \
    Atom.Set.handle_NonDisjointUnion GUQS_FUN(term) t                          \
127 128 129 130

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

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

133 134 135
#define COPY_CLASS     __copy
#define COPY_FUN(term) CONCAT(copy_, term)

136
#define __COPY                                                                 \
137
  class ['self] COPY_CLASS = object (_ : 'self)                                \
138 139
    inherit [_] map                                                            \
    inherit [_] KitCopy.map                                                    \
140
  end                                                                          \
141 142

#define COPY(term)                                                             \
143
  let COPY_FUN(term) t =                                                       \
144
    new COPY_CLASS # VISIT(term) KitCopy.empty t                               \
145 146 147

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

POTTIER Francois's avatar
POTTIER Francois committed
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
(* [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                       \

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

167 168 169
(* [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. *)
170

171 172
#define SHOW_CLASS     __show
#define SHOW_FUN(term) CONCAT(show_, term)
173

174
#define __SHOW                                                                 \
175
  class ['self] SHOW_CLASS = object (_ : 'self)                                \
176 177
    inherit [_] map                                                            \
    inherit [_] KitShow.map                                                    \
178
  end                                                                          \
179 180

#define SHOW(term)                                                             \
181
  let SHOW_FUN(term) t =                                                       \
182
    new SHOW_CLASS # VISIT(term) () t                                          \
183 184 185

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

186 187 188 189
(* [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,
190 191 192 193
   the exception [Unbound] is raised. *)

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

194 195
#define IMPORT_CLASS     __import
#define IMPORT_FUN(term) CONCAT(import_, term)
196

197
#define __IMPORT                                                               \
198
  exception Unbound = KitImport.Unbound                                        \
199
  class ['self] IMPORT_CLASS = object (_ : 'self)                              \
200 201
    inherit [_] map                                                            \
    inherit [_] KitImport.map                                                  \
202
  end                                                                          \
203 204

#define IMPORT(term)                                                           \
205
  let IMPORT_FUN(term) env t =                                                 \
206
    new IMPORT_CLASS # VISIT(term) env t                                       \
207 208 209

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

210 211 212
(* [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]. *)
213

214 215
#define EXPORT_CLASS     __export
#define EXPORT_FUN(term) CONCAT(export_, term)
216

217
#define __EXPORT                                                               \
218
  class ['self] EXPORT_CLASS = object (_ : 'self)                              \
219 220
    inherit [_] map                                                            \
    inherit [_] KitExport.map                                                  \
221
  end                                                                          \
222 223

#define EXPORT(term)                                                           \
224
  let EXPORT_FUN(term) env t =                                                 \
225
    new EXPORT_CLASS # VISIT(term) env t                                       \
226 227 228

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

229
(* [size_term] computes the size of its argument. *)
230 231 232 233

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

234 235
#define SIZE_CLASS     __size
#define SIZE_FUN(term) CONCAT(size_, term)
236

237
#define __SIZE                                                                 \
238
  class ['self] SIZE_CLASS = object (_ : 'self)                                \
239 240 241
    inherit [_] reduce as super                                                \
    inherit [_] KitTrivial.reduce                                              \
    inherit [_] VisitorsRuntime.addition_monoid                                \
POTTIER Francois's avatar
POTTIER Francois committed
242 243
    method! VISIT(term) env t =                                                \
      1 + super # VISIT(term) env t                                            \
244
  end                                                                          \
245 246

#define SIZE(term)                                                             \
247
  let SIZE_FUN(term) t =                                                       \
248
    new SIZE_CLASS # VISIT(term) () t                                          \
POTTIER Francois's avatar
POTTIER Francois committed
249 250 251

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

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

254 255
#define EQUIV_CLASS     __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
256

POTTIER Francois's avatar
POTTIER Francois committed
257
#define __EQUIV                                                                \
258
  class EQUIV_CLASS = object                                                   \
POTTIER Francois's avatar
POTTIER Francois committed
259 260
    inherit [_] iter2                                                          \
    inherit [_] KitEquiv.iter2                                                 \
261
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
262 263

#define EQUIV(term)                                                            \
264
  let EQUIV_FUN(term) t1 t2 =                                                  \
POTTIER Francois's avatar
POTTIER Francois committed
265
    VisitorsRuntime.wrap2                                                      \
266
      (new EQUIV_CLASS # VISIT(term) KitEquiv.empty)                           \
267
      t1 t2                                                                    \
POTTIER Francois's avatar
POTTIER Francois committed
268 269 270

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

271 272 273 274 275
(* [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
276 277 278 279 280 281 282 283 284 285 286

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

287 288 289 290 291 292 293 294 295 296
(* Global uniqueness can be preserved, if desired, by copying the things that
   are grafted into [t]. The user decides which [copy] operation should be used.
   It could be [copy_thing], or it could be the identity. *)

#define SUBST_CLASS(Var)      CONCAT(__subst_, Var)
#define SUBST_FUN(Var, term)  CONCAT(subst_, CONCAT(Var, CONCAT(_, term)))
#define SUBST_FUN1(Var, term) CONCAT(SUBST_FUN(Var, term), 1)

#define __SUBST(Var)                                                           \
  class SUBST_CLASS(Var) copy = object                                         \
POTTIER Francois's avatar
POTTIER Francois committed
297 298
    inherit [_] endo (* we could also use [map] *)                             \
    inherit [_] KitSubst.map                                                   \
299
    method! private VISIT(Var) sigma this x =                                  \
300
      KitSubst.apply copy sigma this x                                         \
301
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
302

303 304 305 306 307
#define SUBST(Var, term)                                                       \
  let SUBST_FUN(Var, term) copy sigma t =                                      \
    (new SUBST_CLASS(Var) copy) # VISIT(term) sigma t                          \
  let SUBST_FUN1(Var, term) copy u x t =                                       \
    SUBST_FUN(Var, term) copy (Atom.Map.singleton x u) t                       \
308 309

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