(* The conventional name of the visitor methods. *) #define VISIT(term) \ CONCAT(visit_, term) (* For comments about the operations that follow, see [ToolboxOutput.ml]. *) (* -------------------------------------------------------------------------- *) #define FA_CLASS __fa #define FA_FUN(term) CONCAT(fa_, term) #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 (* -------------------------------------------------------------------------- *) #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 = \ match FILTER_FUN(term) (fun y -> Atom.equal x y) t with \ | None -> false \ | Some _ -> true \ (* -------------------------------------------------------------------------- *) #define BA_CLASS __ba #define BA_FUN(term) CONCAT(ba_, term) #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 \ (* -------------------------------------------------------------------------- *) #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 \ (* -------------------------------------------------------------------------- *) #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 [_] iter \ inherit [_] KitGuq.iter \ end \ #define GUQ(term) \ let GUQ_FUN(term) t = \ new GUQ_CLASS # VISIT(term) () t \ let GUQS_FUN(term) ts = \ let o = new GUQ_CLASS in \ List.iter (o # VISIT(term) ()) ts \ 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 \ (* -------------------------------------------------------------------------- *) #define COPY_CLASS __copy #define COPY_FUN(term) CONCAT(copy_, term) #define __COPY \ class ['self] COPY_CLASS = object (_ : 'self) \ inherit [_] map \ inherit [_] KitCopy.map \ end \ #define COPY(term) \ let COPY_FUN(term) t = \ new COPY_CLASS # VISIT(term) KitCopy.empty t \ (* -------------------------------------------------------------------------- *) #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 \ (* -------------------------------------------------------------------------- *) (* TEMPORARY use string * loc so as to be able to give a location *) #define IMPORT_FUN(term) CONCAT(import_, term) #define __IMPORT \ exception Unbound = KitImport.Unbound \ #define IMPORT(term) \ let IMPORT_FUN(term) env t = \ (object \ inherit [_] map \ inherit [_] KitImport.map \ end) # VISIT(term) env t \ (* -------------------------------------------------------------------------- *) #define EXPORT_CLASS __export #define EXPORT_FUN(term) CONCAT(export_, term) #define __EXPORT \ class ['self] EXPORT_CLASS = object (_ : 'self) \ inherit [_] map \ inherit [_] KitExport.map \ end \ #define EXPORT(term) \ let EXPORT_FUN(term) env t = \ new EXPORT_CLASS # VISIT(term) env t \ (* -------------------------------------------------------------------------- *) #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 \ (* -------------------------------------------------------------------------- *) (* [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. *) #define SIZE_CLASS __size #define SIZE_FUN(term) CONCAT(size_, term) #define __SIZE \ class ['self] SIZE_CLASS = object (_ : 'self) \ inherit [_] iter as super \ inherit [_] KitTrivial.iter \ val mutable accu = 0 \ method accu = accu \ method! VISIT(term) env t = \ accu <- accu + 1; \ super # VISIT(term) env t \ end \ #define SIZE(term) \ let SIZE_FUN(term) t = \ let o = new SIZE_CLASS in \ o # VISIT(term) () t; \ o # accu \ (* -------------------------------------------------------------------------- *) #define EQUIV_CLASS __equiv #define EQUIV_FUN(term) CONCAT(equiv_, term) #define __EQUIV \ class EQUIV_CLASS = object \ inherit [_] iter2 \ inherit [_] KitEquiv.iter2 \ end \ #define EQUIV(term) \ let EQUIV_FUN(term) t1 t2 = \ VisitorsRuntime.wrap2 \ (new EQUIV_CLASS # VISIT(term) KitEquiv.empty) \ t1 t2 \ (* -------------------------------------------------------------------------- *) #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 \ inherit [_] endo (* we could also use [map] *) \ inherit [_] KitSubst.map \ method! private VISIT(Var) sigma this x = \ KitSubst.apply copy sigma this x \ end \ #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 \ (* -------------------------------------------------------------------------- *) (* 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) \ (* -------------------------------------------------------------------------- *)