Module Cc_plugin.CcalgoSource

Sourcetype pa_constructor = {
  1. cnode : int;
  2. arity : int;
  3. args : int list;
}
Sourcetype pa_fun = {
  1. fsym : int;
  2. fnargs : int;
}
Sourcemodule PafMap : CSig.MapS with type key = pa_fun
Sourcetype cinfo = {
  1. ci_constr : Constr.pconstructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
Sourcetype term =
  1. | Symb of Constr.constr
  2. | Product of Sorts.t * Sorts.t
  3. | Eps of Names.Id.t
  4. | Appli of term * term
  5. | Constructor of cinfo
Sourcemodule Constrhash : Stdlib.Hashtbl.S with type key = Constr.constr
Sourcemodule Termhash : Stdlib.Hashtbl.S with type key = term
Sourcetype ccpattern =
  1. | PApp of term * ccpattern list
  2. | PVar of int
Sourcetype rule =
  1. | Congruence
  2. | Axiom of Constr.constr * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
Sourcetype from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Constr.constr
  4. | HeqnH of Constr.constr * Constr.constr
Sourcetype 'a eq = {
  1. lhs : int;
  2. rhs : int;
  3. rule : 'a;
}
Sourcetype equality = rule eq
Sourcetype disequality = from eq
Sourcetype patt_kind =
  1. | Normal
  2. | Trivial of Constr.types
  3. | Creates_variables
Sourcetype quant_eq = {
  1. qe_hyp_id : Names.Id.t;
  2. qe_pol : bool;
  3. qe_nvars : int;
  4. qe_lhs : ccpattern;
  5. qe_lhs_valid : patt_kind;
  6. qe_rhs : ccpattern;
  7. qe_rhs_valid : patt_kind;
}
Sourcetype inductive_status =
  1. | Unknown
  2. | Partial of pa_constructor
  3. | Partial_applied
  4. | Total of int * pa_constructor
Sourcetype representative = {
  1. mutable weight : int;
  2. mutable lfathers : Int.Set.t;
  3. mutable fathers : Int.Set.t;
  4. mutable inductive_status : inductive_status;
  5. class_type : Constr.types;
  6. mutable functions : Int.Set.t PafMap.t;
}
Sourcetype cl =
  1. | Rep of representative
  2. | Eqto of int * equality
Sourcetype vertex =
  1. | Leaf
  2. | Node of int * int
Sourcetype node = {
  1. mutable clas : cl;
  2. mutable cpath : int;
  3. mutable constructors : int PacMap.t;
  4. vertex : vertex;
  5. term : term;
}
Sourcetype forest = {
  1. mutable max_size : int;
  2. mutable size : int;
  3. mutable map : node array;
  4. axioms : (term * term) Constrhash.t;
  5. mutable epsilons : pa_constructor list;
  6. syms : int Termhash.t;
}
Sourcetype state
Sourcetype explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete
Sourcetype matching_problem
Sourceval term_equal : term -> term -> bool
Sourceval constr_of_term : term -> Constr.constr
Sourceval debug_congruence : CDebug.t
Sourceval forest : state -> forest
Sourceval axioms : forest -> (term * term) Constrhash.t
Sourceval epsilons : forest -> pa_constructor list
Sourceval empty : int -> Goal.goal Evd.sigma -> state
Sourceval add_term : state -> term -> int
Sourceval add_equality : state -> Constr.constr -> term -> term -> unit
Sourceval add_disequality : state -> from -> term -> term -> unit
Sourceval add_quant : state -> Names.Id.t -> bool -> (int * patt_kind * ccpattern * patt_kind * ccpattern) -> unit
Sourceval find : forest -> int -> int
Sourceval find_oldest_pac : forest -> int -> pa_constructor -> int
Sourceval term : forest -> int -> term
Sourceval get_constructor_info : forest -> int -> cinfo
Sourceval subterms : forest -> int -> int * int
Sourceval join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list
Sourceval execute : bool -> state -> explanation option
Sourceval pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t