package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type pa_constructor = {
  1. cnode : int;
  2. arity : int;
  3. args : int list;
}
type pa_fun = {
  1. fsym : int;
  2. fnargs : int;
}
module PafMap : CSig.MapS with type key = pa_fun
module PacMap : CSig.MapS with type key = pa_constructor
type cinfo = {
  1. ci_constr : Constr.pconstructor;
  2. ci_arity : int;
  3. ci_nhyps : int;
}
type term =
  1. | Symb of Constr.constr
  2. | Product of Sorts.t * Sorts.t
  3. | Eps of Names.Id.t
  4. | Appli of term * term
  5. | Constructor of cinfo
module Constrhash : Hashtbl.S with type key = Constr.constr
module Termhash : Hashtbl.S with type key = term
type ccpattern =
  1. | PApp of term * ccpattern list
  2. | PVar of int
type rule =
  1. | Congruence
  2. | Axiom of Constr.constr * bool
  3. | Injection of int * pa_constructor * int * pa_constructor * int
type from =
  1. | Goal
  2. | Hyp of Constr.constr
  3. | HeqG of Constr.constr
  4. | HeqnH of Constr.constr * Constr.constr
type 'a eq = {
  1. lhs : int;
  2. rhs : int;
  3. rule : 'a;
}
type equality = rule eq
type disequality = from eq
type patt_kind =
  1. | Normal
  2. | Trivial of Constr.types
  3. | Creates_variables
type quant_eq = {
  1. qe_hyp_id : Names.Id.t;
  2. qe_pol : bool;
  3. qe_nvars : int;
  4. qe_lhs : ccpattern;
  5. qe_lhs_valid : patt_kind;
  6. qe_rhs : ccpattern;
  7. qe_rhs_valid : patt_kind;
}
type inductive_status =
  1. | Unknown
  2. | Partial of pa_constructor
  3. | Partial_applied
  4. | Total of int * pa_constructor
type representative = {
  1. mutable weight : int;
  2. mutable lfathers : Int.Set.t;
  3. mutable fathers : Int.Set.t;
  4. mutable inductive_status : inductive_status;
  5. class_type : Constr.types;
  6. mutable functions : Int.Set.t PafMap.t;
}
type cl =
  1. | Rep of representative
  2. | Eqto of int * equality
type vertex =
  1. | Leaf
  2. | Node of int * int
type node = {
  1. mutable clas : cl;
  2. mutable cpath : int;
  3. mutable constructors : int PacMap.t;
  4. vertex : vertex;
  5. term : term;
}
type forest = {
  1. mutable max_size : int;
  2. mutable size : int;
  3. mutable map : node array;
  4. axioms : (term * term) Constrhash.t;
  5. mutable epsilons : pa_constructor list;
  6. syms : int Termhash.t;
}
type state
type explanation =
  1. | Discrimination of int * pa_constructor * int * pa_constructor
  2. | Contradiction of disequality
  3. | Incomplete
type matching_problem
val term_equal : term -> term -> bool
val constr_of_term : term -> Constr.constr
val debug_congruence : CDebug.t
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.constr -> term -> term -> unit
val add_disequality : state -> from -> term -> term -> unit
val add_quant : state -> Names.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 execute : bool -> state -> explanation option
val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct