diff options
Diffstat (limited to 'plugins/cc/ccalgo.mli')
-rw-r--r-- | plugins/cc/ccalgo.mli | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli new file mode 100644 index 00000000..5f56c7e6 --- /dev/null +++ b/plugins/cc/ccalgo.mli @@ -0,0 +1,222 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Util +open Term +open Names + +type cinfo = + {ci_constr: constructor; (* inductive type *) + ci_arity: int; (* # args *) + ci_nhyps: int} (* # projectable args *) + +type term = + Symb of constr + | Product of sorts_family * sorts_family + | Eps of identifier + | Appli of term*term + | Constructor of cinfo (* constructor arity + nhyps *) + +type patt_kind = + Normal + | Trivial of types + | Creates_variables + +type ccpattern = + PApp of term * ccpattern list + | PVar of int + +type pa_constructor = + { cnode : int; + arity : int; + args : int list} + +module PacMap : Map.S with type key = pa_constructor + +type forest + +type state + +type rule= + Congruence + | Axiom of constr * bool + | Injection of int * pa_constructor * int * pa_constructor * int + +type from= + Goal + | Hyp of constr + | HeqG of constr + | HeqnH of constr*constr + +type 'a eq = {lhs:int;rhs:int;rule:'a} + +type equality = rule eq + +type disequality = from eq + +type explanation = + Discrimination of (int*pa_constructor*int*pa_constructor) + | Contradiction of disequality + | Incomplete + +val constr_of_term : term -> constr + +val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit + +val forest : state -> forest + +val axioms : forest -> (constr, term * term) Hashtbl.t + +val epsilons : forest -> pa_constructor list + +val empty : int -> Proof_type.goal Tacmach.sigma -> state + +val add_term : state -> term -> int + +val add_equality : state -> constr -> term -> term -> unit + +val add_disequality : state -> from -> term -> term -> unit + +val add_quant : state -> identifier -> bool -> + int * patt_kind * ccpattern * patt_kind * ccpattern -> unit + +val tail_pac : pa_constructor -> pa_constructor + +val find : forest -> int -> int + +val find_pac : forest -> int -> pa_constructor -> int + +val term : forest -> int -> term + +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 + +type quant_eq= + {qe_hyp_id: identifier; + qe_pol: bool; + qe_nvars:int; + qe_lhs: ccpattern; + qe_lhs_valid:patt_kind; + qe_rhs: ccpattern; + qe_rhs_valid:patt_kind} + + +type pa_fun= + {fsym:int; + fnargs:int} + +type matching_problem + +module PafMap: Map.S with type key = pa_fun + +val make_fun_table : state -> Intset.t PafMap.t + +val do_match : state -> + (quant_eq * int array) list ref -> matching_problem Stack.t -> unit + +val init_pb_stack : state -> matching_problem Stack.t + +val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun + +val find_instances : state -> (quant_eq * int array) list + +val execute : bool -> state -> explanation option + + + + + + + + + + + + + +(*type pa_constructor + + +module PacMap:Map.S with type key=pa_constructor + +type term = + Symb of Term.constr + | Eps + | Appli of term * term + | Constructor of Names.constructor*int*int + +type rule = + Congruence + | Axiom of Names.identifier + | Injection of int*int*int*int + +type equality = + {lhs : int; + rhs : int; + rule : rule} + +module ST : +sig + type t + val empty : unit -> t + val enter : int -> int * int -> t -> unit + val query : int * int -> t -> int + val delete : int -> t -> unit + val delete_list : int list -> t -> unit +end + +module UF : +sig + type t + exception Discriminable of int * int * int * int * t + val empty : unit -> t + val find : t -> int -> int + val size : t -> int -> int + val get_constructor : t -> int -> Names.constructor + val pac_arity : t -> int -> int * int -> int + val mem_node_pac : t -> int -> int * int -> int + val add_pacs : t -> int -> pa_constructor PacMap.t -> + int list * equality list + val term : t -> int -> term + val subterms : t -> int -> int * int + val add : t -> term -> int + val union : t -> int -> int -> equality -> int list * equality list + val join_path : t -> int -> int -> + ((int*int)*equality) list* + ((int*int)*equality) list +end + + +val combine_rec : UF.t -> int list -> equality list +val process_rec : UF.t -> equality list -> int list + +val cc : UF.t -> unit + +val make_uf : + (Names.identifier * (term * term)) list -> UF.t + +val add_one_diseq : UF.t -> (term * term) -> int * int + +val add_disaxioms : + UF.t -> (Names.identifier * (term * term)) list -> + (Names.identifier * (int * int)) list + +val check_equal : UF.t -> int * int -> bool + +val find_contradiction : UF.t -> + (Names.identifier * (int * int)) list -> + (Names.identifier * (int * int)) +*) + + |