Module `Imandra_surface.Plugin`

Event Plugins

Plugins are individual objects that can register to be called whenever a new event is defined (new function, new type, etc.)

A typical usage is code generators based on types (pretty printers, serializers, etc.) as seen in src/codegen (the library imandra-base.codegen).

type actions = < exec_code : Code_fragment.t -> unit; >: actions available to a plugin

type snapshot = < restore : unit; >

class virtual t : object ... end: A plugin, with virtual methods to overload

class virtual syn_fun : object ... end: A plugin specialized to work on (syntactic) function definitions. Just define on_syn_fun.

class virtual ty : object ... end: A plugin specialized to work on type definitions. Just define on_ty.

type set: A set of plugins, packaging several plugins together. Imandra's main state has such a set of plugins.

val global : set: Global set of plugins

val mk_set : unit -> set: Create a set of plugins

val add_plugin : set -> t -> unit: Register a plugin to be called when new events are processed.

val size_plugins : set -> int
val iter_plugins : set -> (t -> unit) -> unit
val map_plugins : set -> (t -> 'a) -> 'a list
val mem_plugins : set -> t -> bool: Is the plugin in this set already? (based on p#name)

val with_disabled_all : set -> (unit -> 'a) -> 'a