Module `Cc_plugin.Ccalgo`Source

Sourcetype pa_constructor = {

cnode : int;
arity : int;
args : int list;

}

Sourcetype pa_fun = {

fsym : int;
fnargs : int;

}

Sourcemodule PafMap : CSig.MapS with type key = pa_fun

Sourcemodule PacMap : CSig.MapS with type key = pa_constructor

Sourcetype cinfo = {

ci_constr : Constr.pconstructor;
ci_arity : int;
ci_nhyps : int;

}

Sourcetype term =

| Symb of Constr.constr
| Product of Sorts.t * Sorts.t
| Eps of Names.Id.t
| Appli of term * term
| Constructor of cinfo

Sourcemodule Constrhash : Stdlib.Hashtbl.S with type key = Constr.constr

Sourcemodule Termhash : Stdlib.Hashtbl.S with type key = term

Sourcetype ccpattern =

| PApp of term * ccpattern list
| PVar of int

Sourcetype rule =

| Congruence
| Axiom of Constr.constr * bool
| Injection of int * pa_constructor * int * pa_constructor * int

Sourcetype from =

| Goal
| Hyp of Constr.constr
| HeqG of Constr.constr
| HeqnH of Constr.constr * Constr.constr

Sourcetype 'a eq = {

lhs : int;
rhs : int;
rule : 'a;

}

Sourcetype equality = rule eq

Sourcetype disequality = from eq

Sourcetype patt_kind =

| Normal
| Trivial of Constr.types
| Creates_variables

Sourcetype 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;

}

Sourcetype inductive_status =

| Unknown
| Partial of pa_constructor
| Partial_applied
| Total of int * pa_constructor

Sourcetype 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;

}

Sourcetype cl =

| Rep of representative
| Eqto of int * equality

Sourcetype vertex =

| Leaf
| Node of int * int

Sourcetype node = {

mutable clas : cl;
mutable cpath : int;
mutable constructors : int PacMap.t;
vertex : vertex;
term : term;

}

Sourcetype forest = {

mutable max_size : int;
mutable size : int;
mutable map : node array;
axioms : (term * term) Constrhash.t;
mutable epsilons : pa_constructor list;
syms : int Termhash.t;

}

Sourcetype state

Sourcetype explanation =

| Discrimination of int * pa_constructor * int * pa_constructor
| Contradiction of disequality
| 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

Source

val add_quant : 
  state ->
  Names.Id.t ->
  bool ->
  (int * patt_kind * ccpattern * patt_kind * ccpattern) ->
  unit

Sourceval tail_pac : pa_constructor -> pa_constructor

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

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cc_plugin/Cc_plugin/Ccalgo/index.html

Module `Cc_plugin.Ccalgo`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/cc_plugin/Cc_plugin/Ccalgo/index.html

Module Cc_plugin.CcalgoSource

Module `Cc_plugin.Ccalgo`Source