AlphaLibMacros.cppo.ml 14.2 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 53 54
    match FILTER_FUN(term) (fun y -> Atom.equal x y) t with                    \
    | None -> true                                                             \
    | Some _ -> false                                                          \
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

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

122 123 124
(* [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. *)
125

126 127
#define SHOW_CLASS     __show
#define SHOW_FUN(term) CONCAT(show_, term)
128

129
#define __SHOW                                                                 \
130
  class ['self] SHOW_CLASS = object (_ : 'self)                                \
131 132
    inherit [_] map                                                            \
    inherit [_] KitShow.map                                                    \
133
  end                                                                          \
134 135

#define SHOW(term)                                                             \
136
  let SHOW_FUN(term) t =                                                       \
137
    new SHOW_CLASS # VISIT(term) () t                                          \
138 139 140

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

141 142 143 144
(* [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,
145 146 147 148
   the exception [Unbound] is raised. *)

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

149 150
#define IMPORT_CLASS     __import
#define IMPORT_FUN(term) CONCAT(import_, term)
151

152
#define __IMPORT                                                               \
153
  exception Unbound = KitImport.Unbound                                        \
154
  class ['self] IMPORT_CLASS = object (_ : 'self)                              \
155 156
    inherit [_] map                                                            \
    inherit [_] KitImport.map                                                  \
157
  end                                                                          \
158 159

#define IMPORT(term)                                                           \
160
  let IMPORT_FUN(term) env t =                                                 \
161
    new IMPORT_CLASS # VISIT(term) env t                                       \
162 163 164

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

165 166 167
(* [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]. *)
168

169 170
#define EXPORT_CLASS     __export
#define EXPORT_FUN(term) CONCAT(export_, term)
171

172
#define __EXPORT                                                               \
173
  class ['self] EXPORT_CLASS = object (_ : 'self)                              \
174 175
    inherit [_] map                                                            \
    inherit [_] KitExport.map                                                  \
176
  end                                                                          \
177 178

#define EXPORT(term)                                                           \
179
  let EXPORT_FUN(term) env t =                                                 \
180
    new EXPORT_CLASS # VISIT(term) env t                                       \
181 182 183

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

184
(* [size_term] computes the size of its argument. *)
185 186 187 188

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

189 190
#define SIZE_CLASS     __size
#define SIZE_FUN(term) CONCAT(size_, term)
191

192
#define __SIZE                                                                 \
193
  class ['self] SIZE_CLASS = object (_ : 'self)                                \
194 195 196
    inherit [_] reduce as super                                                \
    inherit [_] KitTrivial.reduce                                              \
    inherit [_] VisitorsRuntime.addition_monoid                                \
POTTIER Francois's avatar
POTTIER Francois committed
197 198
    method! VISIT(term) env t =                                                \
      1 + super # VISIT(term) env t                                            \
199
  end                                                                          \
200 201

#define SIZE(term)                                                             \
202
  let SIZE_FUN(term) t =                                                       \
203
    new SIZE_CLASS # VISIT(term) () t                                          \
POTTIER Francois's avatar
POTTIER Francois committed
204 205 206

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

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

209 210
#define EQUIV_CLASS     __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
211

POTTIER Francois's avatar
POTTIER Francois committed
212
#define __EQUIV                                                                \
213
  class EQUIV_CLASS = object                                                   \
POTTIER Francois's avatar
POTTIER Francois committed
214 215
    inherit [_] iter2                                                          \
    inherit [_] KitEquiv.iter2                                                 \
216
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
217 218

#define EQUIV(term)                                                            \
219
  let EQUIV_FUN(term) t1 t2 =                                                  \
POTTIER Francois's avatar
POTTIER Francois committed
220
    VisitorsRuntime.wrap2                                                      \
221
      (new EQUIV_CLASS # VISIT(term) KitEquiv.empty)                           \
222
      t1 t2                                                                    \
POTTIER Francois's avatar
POTTIER Francois committed
223 224 225

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

226 227 228 229 230
(* [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
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248

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

249 250 251 252
#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
253
#define __SUBST(thing, Var)                                                    \
254
  class SUBST_CLASS(thing) = object                                            \
POTTIER Francois's avatar
POTTIER Francois committed
255 256
    inherit [_] endo (* we could also use [map] *)                             \
    inherit [_] KitSubst.map                                                   \
257 258
    method! private VISIT(Var) sigma this x =                                  \
      KitSubst.apply COPY_FUN(thing) sigma this x                              \
259
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
260 261

#define SUBST(thing, term)                                                     \
262 263 264
  let SUBST_FUN(thing, term) sigma t =                                         \
    new SUBST_CLASS(thing) # VISIT(term) sigma t                               \
  let SUBST_FUN1(thing, term) u x t =                                          \
265 266 267
    SUBST_FUN(thing, term) (Atom.Map.singleton x u) t                          \

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