package libzipperposition

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

Actions that modify the set of rules Compute_prec

type 'a state_actions = ('a -> state -> state) list
type 'a modifiers = ('a -> 'a) list
type t = {
  1. name : string;
  2. prio : int;
    (*

    the lower, the more urgent, the earlier it is loaded

    *)
  3. start_file_actions : string state_actions;
  4. post_parse_actions : Logtk.UntypedAST.statement Iter.t state_actions;
  5. post_typing_actions : Logtk.TypeInference.typed_statement CCVector.ro_vector state_actions;
  6. post_cnf_modifiers : Logtk.Cnf.c_statement Iter.t modifiers;
  7. post_cnf_actions : Logtk.Statement.clause_t CCVector.ro_vector state_actions;
  8. ord_select_actions : (Logtk.Ordering.t * Selection.t) state_actions;
  9. ctx_actions : (module Ctx_intf.S) state_actions;
  10. prec_actions : prec_action list;
  11. 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.

Registration

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 Iter.t

Names of loaded extensions