diff options
Diffstat (limited to 'plugins/cc/ccalgo.mli')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 132 |
1 files changed, 83 insertions, 49 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index e4713728..c72843d5 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,40 +10,39 @@ open Util open Term open Names +type pa_constructor = + { cnode : int; + arity : int; + args : int list} + +type pa_fun= + {fsym:int; + fnargs:int} + + +module PafMap : Map.S with type key = pa_fun +module PacMap : Map.S with type key = pa_constructor + type cinfo = - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* 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 + | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) -val term_equal : term -> term -> bool +module Constrhash : Hashtbl.S with type key = constr +module Termhash : Hashtbl.S with type key = term -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 @@ -61,17 +60,67 @@ type equality = rule eq type disequality = from eq +type patt_kind = + Normal + | Trivial of types + | Creates_variables + +type quant_eq= + {qe_hyp_id: 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 : Term.types; + mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) + +type cl = Rep of representative| Eqto of int*equality + +type vertex = Leaf| Node of (int*int) + +type node = + {mutable clas:cl; + mutable cpath: int; + mutable constructors: int PacMap.t; + vertex:vertex; + term:term} + +type 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} + +type state + type explanation = Discrimination of (int*pa_constructor*int*pa_constructor) | Contradiction of disequality | Incomplete -module Constrhash : Hashtbl.S with type key = constr -module Termhash : Hashtbl.S with type key = term +type matching_problem + +val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit +val debug : Pp.std_ppcmds -> unit val forest : state -> forest @@ -87,7 +136,7 @@ val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit -val add_quant : state -> identifier -> bool -> +val add_quant : state -> Id.t -> bool -> int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -96,6 +145,8 @@ val find : forest -> int -> int val find_pac : forest -> int -> pa_constructor -> int +val find_oldest_pac : forest -> int -> pa_constructor -> int + val term : forest -> int -> term val get_constructor_info : forest -> int -> cinfo @@ -105,25 +156,7 @@ 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 make_fun_table : state -> Int.Set.t PafMap.t val do_match : state -> (quant_eq * int array) list ref -> matching_problem Stack.t -> unit @@ -136,8 +169,9 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option +val pr_idx_term : forest -> int -> Pp.std_ppcmds - +val empty_forest: unit -> forest @@ -161,7 +195,7 @@ type term = type rule = Congruence - | Axiom of Names.identifier + | Axiom of Names.Id.t | Injection of int*int*int*int type equality = @@ -207,19 +241,19 @@ val process_rec : UF.t -> equality list -> int list val cc : UF.t -> unit val make_uf : - (Names.identifier * (term * term)) list -> UF.t + (Names.Id.t * (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 + UF.t -> (Names.Id.t * (term * term)) list -> + (Names.Id.t * (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)) + (Names.Id.t * (int * int)) list -> + (Names.Id.t * (int * int)) *) |