Cc_plugin.Ccalgo
module PacMap : CSig.MapS with type key = pa_constructor
module ATerm : sig ... end
type rule =
| Congruence |
| Axiom of Constr.constr * bool |
| Injection of int * pa_constructor * int * pa_constructor * int |
type from =
| Goal |
| Hyp of Constr.constr |
| HeqG of Constr.constr |
| HeqnH of Constr.constr * Constr.constr |
type quant_eq = {
qe_hyp_id : Names.Id.t; |
qe_pol : bool; |
qe_nvars : int; |
qe_lhs : ccpattern; |
qe_lhs_valid : patt_kind; |
qe_rhs : ccpattern; |
qe_rhs_valid : patt_kind; |
}
type inductive_status =
| Unknown |
| Partial of pa_constructor |
| Partial_applied |
| Total of int * pa_constructor |
type representative = {
mutable weight : int; |
mutable lfathers : Int.Set.t; |
mutable fathers : Int.Set.t; |
mutable inductive_status : inductive_status; |
class_type : Constr.types; |
mutable functions : Int.Set.t PafMap.t; |
}
type forest = {
mutable max_size : int; |
mutable size : int; |
mutable map : node array; |
axioms : (ATerm.t * ATerm.t) Constrhash.t; |
mutable epsilons : pa_constructor list; |
syms : int Termhash.t; |
}
type explanation =
| Discrimination of int * pa_constructor * int * pa_constructor |
| Contradiction of disequality |
| Incomplete |
val debug_congruence : CDebug.t
val epsilons : forest -> pa_constructor list
val empty : Environ.env -> Evd.evar_map -> int -> state
val add_equality : state -> Constr.constr -> ATerm.t -> ATerm.t -> unit
val tail_pac : pa_constructor -> pa_constructor
val find : forest -> int -> int
val find_oldest_pac : forest -> int -> pa_constructor -> int
val subterms : forest -> int -> int * int
val execute : bool -> state -> explanation option
val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t