Module Extensions

module Extensions: sig .. end

Dynamic extensions

Dynamic extensions

type 'a or_error = ('a, string) CCResult.t 

Type Definitions

type state = Logtk.Flex_state.t 
type env_action = (module Env.S) -> unit 
An extension is allowed to modify an environment
type prec_action = state -> Logtk.Compute_prec.t -> Logtk.Compute_prec.t 
Actions that modify the set of rules Compute_prec
type 'a state_actions = ('a -> state -> state) list 
type t = {
   name : string;
   prio : int; (*
the lower, the more urgent, the earlier it is loaded
   start_file_actions : string state_actions;
   post_parse_actions : Logtk.UntypedAST.statement Sequence.t state_actions;
   post_typing_actions : Logtk.TypeInference.typed_statement CCVector.ro_vector
   post_cnf_actions : Logtk.Statement.clause_t CCVector.ro_vector state_actions;
   ord_select_actions : (Logtk.Ordering.t * Selection.t) state_actions;
   ctx_actions : (module Ctx_intf.S) state_actions;
   prec_actions : prec_action list;
   env_actions : env_action list;
An extension contains a number of actions that can modify the Flex_state.t during preprocessing, or modify the Env_intf.S once it is built.
val default : t
Default extension. Does nothing.


val register : t -> unit
Register an extension to the (current) prover. Plugins should call this when they are loaded.
val extensions : unit -> t list
All currently available extensions
val by_name : string -> t option
Get an extension by its name, if any
val names : unit -> string Sequence.t
Names of loaded extensions