| products/sources/formale Sprachen/Coq/plugins/cc/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: compute_sturm.prf Sprache: SMLOriginal von: Coq© |
|
||||||
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Constr open Names type pa_constructor = { cnode : int; arity : int; args : int list} type pa_fun= {fsym:int; fnargs:int} module PafMap : CSig.MapS with type key = pa_fun module PacMap : CSig.MapS with type key = pa_constructor type cinfo = {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) type term = Symb of constr | Product of Sorts.t * Sorts.t | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) module Constrhash : Hashtbl.S with type key = constr module Termhash : Hashtbl.S with type key = term type ccpattern = PApp of term * ccpattern list | PVar of int 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 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 : 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 type matching_problem val term_equal : term -> term -> bool val constr_of_term : term -> constr val debug : (unit -> Pp.t) -> unit val forest : state -> forest val axioms : forest -> (term * term) Constrhash.t val epsilons : forest -> pa_constructor list val empty : int -> Goal.goal Evd.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 -> Id.t -> bool -> int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor val find : forest -> int -> int val find_oldest_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 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 val init_pb_stack : state -> matching_problem Stack.t val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t val empty_forest: unit -> forest (*type pa_constructor module PacMap:CSig.MapS 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.Id.t | 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.Id.t * (term * term)) list -> UF.t val add_one_diseq : UF.t -> (term * term) -> int * int val add_disaxioms : 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.Id.t * (int * int)) list -> (Names.Id.t * (int * int)) *) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
