package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
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 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_actions : Logtk.Statement.clause_t CCVector.ro_vector state_actions;
  7. ord_select_actions : (Logtk.Ordering.t * Selection.t) state_actions;
  8. ctx_actions : (module Ctx_intf.S) state_actions;
  9. prec_actions : prec_action list;
  10. 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct