package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file extensions.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Dynamic extensions} *)

open Logtk

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

(** {2 Type Definitions} *)

type state = Flex_state.t

(** An extension is allowed to modify an environment *)
type env_action = (module Env.S) -> unit

type prec_action = state -> Compute_prec.t -> Compute_prec.t
(** Actions that modify the set of rules {!Compute_prec} *)

type 'a state_actions = ('a -> state -> state) list
(* a list of actions parametrized by ['a] *)

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 : UntypedAST.statement Iter.t state_actions;
  post_typing_actions : TypeInference.typed_statement CCVector.ro_vector state_actions;
  post_cnf_actions: Statement.clause_t CCVector.ro_vector state_actions;
  ord_select_actions : (Ordering.t * Selection.t) state_actions;
  ctx_actions : (module Ctx_intf.S) state_actions;
  prec_actions : prec_action list;
  env_actions : env_action list;
}

let default = {
  name="<no name>";
  prio = 50;
  prec_actions= [];
  start_file_actions=[];
  post_parse_actions=[];
  post_typing_actions=[];
  post_cnf_actions=[];
  ord_select_actions=[];
  ctx_actions=[];
  env_actions=[];
}

(** {2 Registration} *)

let section = Const.section

let __current : t or_error ref = ref (CCResult.Error "could not load plugin")

let _extensions = Hashtbl.create 11

let register self =
  (* register by name, if loading succeeded *)
  if not (Hashtbl.mem _extensions self.name)
  then (
    Util.debugf ~section 1 "register extension `%s`..." (fun k->k self.name);
    Hashtbl.replace _extensions self.name self
  );
  __current := CCResult.Ok self

let cmp_prio_name a b =
  if a.prio = b.prio
  then String.compare a.name b.name
  else compare a.prio b.prio

let extensions () =
  CCHashtbl.values _extensions
  |> Iter.sort_uniq ~cmp:cmp_prio_name  (* sort by increasing priority *)
  |> Iter.to_list

let by_name name =
  try Some (Hashtbl.find _extensions name)
  with Not_found -> None

let names () = CCHashtbl.keys _extensions