Module Cc_core_plugin.Ccalgo

type pa_constructor = {
  1. cnode : int;
  2. arity : int;
  3. args : int list;
}
type constructor =
  1. | Construct of Constr.pconstructor
  2. | Int of Uint63.t
  3. | Float of Float64.t
  4. | String of Pstring.t
type cinfo = {
  1. ci_constr : constructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
type 'a term
module ATerm : sig ... end
type ccpattern =
  1. | PApp of ATerm.t * ccpattern list
  2. | PVar of int * ccpattern list
type axiom
val constr_of_axiom : axiom -> Constr.constr
type rule =
  1. | Congruence
  2. | Axiom of axiom * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
type from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Names.Id.t
  4. | HeqnH of Names.Id.t * Names.Id.t
type 'a eq = {
  1. lhs : int;
  2. rhs : int;
  3. rule : 'a;
}
type equality = rule eq
type disequality = from eq
type patt_kind =
  1. | Normal
  2. | Trivial of Constr.types
  3. | Creates_variables
type forest
type state
type explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete of (EConstr.t * int) list
val debug_congruence : CDebug.t
val forest : state -> forest
val axioms : forest -> axiom -> ATerm.t * ATerm.t
val empty : Environ.env -> Evd.evar_map -> int -> state
val add_aterm : state -> ATerm.t -> int
val add_equality : state -> Names.Id.t -> ATerm.t -> ATerm.t -> unit
val add_disequality : state -> from -> ATerm.t -> ATerm.t -> unit
val add_quant : state -> Names.Id.t -> bool -> (int * patt_kind * ccpattern * patt_kind * ccpattern) -> unit
val tail_pac : pa_constructor -> pa_constructor
val find_oldest_pac : forest -> int -> pa_constructor -> int
val aterm : forest -> int -> ATerm.t
val get_constructor_info : forest -> int -> cinfo
val subterms : forest -> int -> int * int
val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list
val execute : bool -> state -> explanation option
val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t