Module Extensions

module Extensions: sig .. end

Dynamic extensions

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

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 state_actions;`
`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

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