AlphaLibMacros.cppo.ml 14 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
(* For comments about the operations that follow, see [ToolboxOutput.ml].     *)
POTTIER Francois's avatar
POTTIER Francois committed
7

8
(* -------------------------------------------------------------------------- *)
POTTIER Francois's avatar
POTTIER Francois committed
9 10 11 12

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

13 14 15 16 17 18 19 20 21 22 23 24
#define __FA                                                                   \
  class FA_CLASS = object                                                      \
    inherit [_] iter                                                           \
    inherit [_] KitFa.iter                                                     \
  end                                                                          \

#define FA(term)                                                               \
  let FA_FUN(term) t =                                                         \
    let o = new FA_CLASS in                                                    \
    o # VISIT(term) KitFa.empty t;                                             \
    o # accu

POTTIER Francois's avatar
POTTIER Francois committed
25
(* -------------------------------------------------------------------------- *)
26

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

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

POTTIER Francois's avatar
POTTIER Francois committed
52 53
#define BA_CLASS     __ba
#define BA_FUN(term) CONCAT(ba_, term)
54

55 56 57 58 59 60 61 62 63 64 65 66
#define __BA                                                                   \
  class ['self] BA_CLASS = object (_ : 'self)                                  \
    inherit [_] iter                                                           \
    inherit [_] KitBa.iter                                                     \
  end                                                                          \

#define BA(term)                                                               \
  let BA_FUN(term) t =                                                         \
    let o = new BA_CLASS in                                                    \
    o # VISIT(term) () t;                                                      \
    o # accu                                                                   \

67 68
(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
#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          \

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

84 85 86 87 88 89
#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)                                 \
90 91
    inherit [_] iter                                                           \
    inherit [_] KitGuq.iter                                                    \
92 93 94 95 96 97
  end                                                                          \

#define GUQ(term)                                                              \
  let GUQ_FUN(term) t =                                                        \
    new GUQ_CLASS # VISIT(term) () t                                           \
  let GUQS_FUN(term) ts =                                                      \
98 99
    let o = new GUQ_CLASS in                                                   \
    List.iter (o # VISIT(term) ()) ts                                          \
100 101 102 103
  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                          \
104 105 106

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

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
#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                       \

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

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

139
#define IMPORT_FUN(term) CONCAT(import_, term)
140

141
#define __IMPORT                                                               \
142
  exception Unbound = KitImport.Unbound                                        \
143 144

#define IMPORT(term)                                                           \
145
  let IMPORT_FUN(term) env t =                                                 \
146 147 148 149
    (object                                                                    \
      inherit [_] map                                                          \
      inherit [_] KitImport.map                                                \
    end) # VISIT(term) env t                                                   \
150 151 152

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

153 154
#define EXPORT_CLASS     __export
#define EXPORT_FUN(term) CONCAT(export_, term)
155

156
#define __EXPORT                                                               \
157
  class ['self] EXPORT_CLASS = object (_ : 'self)                              \
158 159
    inherit [_] map                                                            \
    inherit [_] KitExport.map                                                  \
160
  end                                                                          \
161 162

#define EXPORT(term)                                                           \
163
  let EXPORT_FUN(term) env t =                                                 \
164
    new EXPORT_CLASS # VISIT(term) env t                                       \
165 166 167

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

168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
#define SHOW_CLASS     __show
#define SHOW_FUN(term) CONCAT(show_, term)

#define __SHOW                                                                 \
  class ['self] SHOW_CLASS = object (_ : 'self)                                \
    inherit [_] map                                                            \
    inherit [_] KitShow.map                                                    \
  end                                                                          \

#define SHOW(term)                                                             \
  let SHOW_FUN(term) t =                                                       \
    new SHOW_CLASS # VISIT(term) () t                                          \

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

183 184 185 186 187 188 189
(* [size] could be defined in terms of [reduce]. We prefer to define it in
   terms of [iter] because we wish to eliminate our dependency on [reduce]
   visitors. *)

(* We use a mutable field [accu], but could also let the environment be a
   reference. *)

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

193
#define __SIZE                                                                 \
194
  class ['self] SIZE_CLASS = object (_ : 'self)                                \
195 196 197 198
    inherit [_] iter as super                                                  \
    inherit [_] KitTrivial.iter                                                \
    val mutable accu = 0                                                       \
    method accu = accu                                                         \
POTTIER Francois's avatar
POTTIER Francois committed
199
    method! VISIT(term) env t =                                                \
200 201
      accu <- accu + 1;                                                        \
      super # VISIT(term) env t                                                \
202
  end                                                                          \
203 204

#define SIZE(term)                                                             \
205
  let SIZE_FUN(term) t =                                                       \
206 207 208
    let o = new SIZE_CLASS in                                                  \
    o # VISIT(term) () t;                                                      \
    o # accu                                                                   \
POTTIER Francois's avatar
POTTIER Francois committed
209 210 211

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

212 213
#define EQUIV_CLASS     __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
214

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

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

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

229 230 231 232 233 234
#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
235 236
    inherit [_] endo (* we could also use [map] *)                             \
    inherit [_] KitSubst.map                                                   \
237
    method! private VISIT(Var) sigma this x =                                  \
238
      KitSubst.apply copy sigma this x                                         \
239
  end                                                                          \
POTTIER Francois's avatar
POTTIER Francois committed
240

241 242 243 244 245
#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                       \
246 247

(* -------------------------------------------------------------------------- *)
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279

(* Summary macros. *)

#define __ALL \
  __FA \
  __FILTER \
  __BA \
  __AVOIDS \
  __GUQ \
  __COPY \
  __AVOID \
  __IMPORT \
  __EXPORT \
  __SHOW \
  __SIZE \
  __EQUIV \

#define ALL(term) \
  FA(term) \
  FILTER(term) \
  BA(term) \
  AVOIDS(term) \
  GUQ(term) \
  COPY(term) \
  AVOID(term) \
  IMPORT(term) \
  EXPORT(term) \
  SHOW(term) \
  SIZE(term) \
  EQUIV(term) \

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