sig
  type cluster
  val dummy : unit -> Wp.Definitions.cluster
  val cluster :
    id:string ->
    ?title:string ->
    ?position:Filepath.position -> unit -> Wp.Definitions.cluster
  val axiomatic : Wp.LogicUsage.axiomatic -> Wp.Definitions.cluster
  val section : Wp.LogicUsage.logic_section -> Wp.Definitions.cluster
  val compinfo : Cil_types.compinfo -> Wp.Definitions.cluster
  val matrix : unit -> Wp.Definitions.cluster
  val cluster_id : Wp.Definitions.cluster -> string
  val cluster_title : Wp.Definitions.cluster -> string
  val cluster_position : Wp.Definitions.cluster -> Filepath.position option
  val cluster_age : Wp.Definitions.cluster -> int
  val cluster_compare :
    Wp.Definitions.cluster -> Wp.Definitions.cluster -> int
  val pp_cluster : Stdlib.Format.formatter -> Wp.Definitions.cluster -> unit
  val iter : (Wp.Definitions.cluster -> unit) -> unit
  type trigger = (Wp.Lang.F.var, Wp.Lang.lfun) Qed.Engine.ftrigger
  type typedef =
      (Wp.Lang.F.tau, Wp.Lang.field, Wp.Lang.lfun) Qed.Engine.ftypedef
  type dlemma = {
    l_name : string;
    l_cluster : Wp.Definitions.cluster;
    l_kind : Wp.LogicUsage.lkind;
    l_types : int;
    l_forall : Wp.Lang.F.var list;
    l_triggers : Wp.Definitions.trigger list list;
    l_lemma : Wp.Lang.F.pred;
  }
  type definition =
      Logic of Wp.Lang.F.tau
    | Function of Wp.Lang.F.tau * Wp.Definitions.recursion * Wp.Lang.F.term
    | Predicate of Wp.Definitions.recursion * Wp.Lang.F.pred
    | Inductive of Wp.Definitions.dlemma list
  and recursion = Def | Rec
  type dfun = {
    d_lfun : Wp.Lang.lfun;
    d_cluster : Wp.Definitions.cluster;
    d_types : int;
    d_params : Wp.Lang.F.var list;
    d_definition : Wp.Definitions.definition;
  }
  module Trigger :
    sig
      val of_term : Wp.Lang.F.term -> Wp.Definitions.trigger
      val of_pred : Wp.Lang.F.pred -> Wp.Definitions.trigger
      val vars : Wp.Definitions.trigger -> Wp.Lang.F.Vars.t
    end
  val find_symbol : Wp.Lang.lfun -> Wp.Definitions.dfun
  val define_symbol : Wp.Definitions.dfun -> unit
  val update_symbol : Wp.Definitions.dfun -> unit
  val find_name : string -> Wp.Definitions.dlemma
  val find_lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
  val compile_lemma :
    (Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma) ->
    Wp.LogicUsage.logic_lemma -> unit
  val define_lemma : Wp.Definitions.dlemma -> unit
  val define_type :
    Wp.Definitions.cluster -> Cil_types.logic_type_info -> unit
  val call_fun :
    result:Wp.Lang.F.tau ->
    Wp.Lang.lfun ->
    (Wp.Lang.lfun -> Wp.Definitions.dfun) ->
    Wp.Lang.F.term list -> Wp.Lang.F.term
  val call_pred :
    Wp.Lang.lfun ->
    (Wp.Lang.lfun -> Wp.Definitions.dfun) ->
    Wp.Lang.F.term list -> Wp.Lang.F.pred
  type axioms = Wp.Definitions.cluster * Wp.LogicUsage.logic_lemma list
  class virtual visitor :
    Wp.Definitions.cluster ->
    object
      method do_local : Wp.Definitions.cluster -> bool
      method virtual on_cluster : Wp.Definitions.cluster -> unit
      method virtual on_comp :
        Cil_types.compinfo -> (Wp.Lang.field * Wp.Lang.F.tau) list -> unit
      method virtual on_dfun : Wp.Definitions.dfun -> unit
      method virtual on_dlemma : Wp.Definitions.dlemma -> unit
      method virtual on_icomp :
        Cil_types.compinfo -> (Wp.Lang.field * Wp.Lang.F.tau) list -> unit
      method virtual on_library : string -> unit
      method virtual on_type :
        Cil_types.logic_type_info -> Wp.Definitions.typedef -> unit
      method virtual section : string -> unit
      method set_local : Wp.Definitions.cluster -> unit
      method vadt : Wp.Lang.ADT.t -> unit
      method vcluster : Wp.Definitions.cluster -> unit
      method vcomp : Cil_types.compinfo -> unit
      method vfield : Wp.Lang.Field.t -> unit
      method vgoal : Wp.Definitions.axioms option -> Wp.Lang.F.pred -> unit
      method vicomp : Cil_types.compinfo -> unit
      method vlemma : Wp.LogicUsage.logic_lemma -> unit
      method vlemmas : unit
      method vlibrary : string -> unit
      method vparam : Wp.Lang.F.var -> unit
      method vpred : Wp.Lang.F.pred -> unit
      method vself : unit
      method vsymbol : Wp.Lang.lfun -> unit
      method vsymbols : unit
      method vtau : Wp.Lang.F.tau -> unit
      method vterm : Wp.Lang.F.term -> unit
      method vtype : Cil_types.logic_type_info -> unit
      method vtypes : unit
    end
end