package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Extracting an inductive type from a construction

find_m*type env sigma c coerce c to an recursive type (I args). find_rectype, find_inductive and find_coinductive respectively accepts any recursive type, only an inductive type and only a coinductive type. They raise Not_found if not convertible to a recursive type.

val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val find_coinductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif

Fetching information in the environment about an inductive type. Raises an anomaly if the inductive type is not found.

Functions to build standard types related to inductive

val instantiate_inductive_constraints : Declarations.mutual_inductive_body -> Univ.Instance.t -> Univ.Constraints.t
type param_univs = (unit -> Univ.Universe.t) list
val make_param_univs : Environ.env -> Constr.constr array -> param_univs

The constr array is the types of the arguments to a template polymorphic inductive.

val constrained_type_of_inductive : mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : mind_specif Univ.puniverses -> param_univs -> Constr.types Univ.constrained
val relevance_of_inductive : Environ.env -> Names.inductive -> Sorts.relevance
val type_of_inductive : mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : ?polyprop:bool -> mind_specif Univ.puniverses -> param_univs -> Constr.types
val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool

Return type as quoted by the user

val constrained_type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types Univ.constrained
val type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types
val arities_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array

Return constructor types in normal form

val type_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array

Return constructor types in user form

val abstract_constructor_type_relatively_to_inductive_types_context : int -> Names.MutInd.t -> Constr.types -> Constr.types

Turns a constructor type recursively referring to inductive types into the same constructor type referring instead to a context made from the abstract declaration of the inductive types (e.g. turns nat->nat into mkArrowR (Rel 1) (Rel 2)); takes as arguments the number of inductive types in the block and the name of the block

val inductive_params : mind_specif -> int

Given a pattern-matching represented compactly, expands it so as to produce lambda and let abstractions in front of the return clause and the pattern branches.

Dual operation of the above. Fails if the return clause or branch has not the expected form.

instantiate_context u subst nas ctx applies both u and subst to ctx while replacing names using nas (order reversed). In particular, assumes that ctx and nas have the same length.

type_case_branches env (I,args) (p:A) c computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end It computes the type of every branch (pattern variables are introduced by products), the type for the whole expression, and the universe constraints generated.

Return the arity of an inductive type

val inductive_sort_family : Declarations.one_inductive_body -> Sorts.family
val check_case_info : Environ.env -> Constr.pinductive -> Sorts.relevance -> Constr.case_info -> unit

Check a case_info actually correspond to a Case expression on the given inductive type.

Guard conditions for fix and cofix-points.
val is_primitive_positive_container : Environ.env -> Names.Constant.t -> bool

is_primitive_positive_container env c tells if the constant c is registered as a primitive type that can be seen as a container where the occurrences of its parameters are positive, in which case the positivity and guard conditions are extended to allow inductive types to nest their subterms in these containers.

val check_fix : Environ.env -> Constr.fixpoint -> unit

When chk is false, the guard condition is not actually checked.

val check_cofix : Environ.env -> Constr.cofixpoint -> unit
Support for sort-polymorphic inductive types

The "polyprop" optional argument below controls the "Prop-polymorphism". By default, it is allowed. But when "polyprop=false", the following exception is raised when a polymorphic singleton inductive type becomes Prop due to parameter instantiation. This is used by the Ocaml extraction, which cannot handle (yet?) Prop-polymorphism.

exception SingletonInductiveBecomesProp of Names.Id.t
val max_inductive_sort : Sorts.t array -> Univ.Universe.t
Debug
type size =
  1. | Large
  2. | Strict
type subterm_spec =
  1. | Subterm of size * Declarations.wf_paths
  2. | Dead_code
  3. | Not_subterm
type guard_env = {
  1. env : Environ.env;
    (*

    dB of last fixpoint

    *)
  2. rel_min : int;
    (*

    dB of variables denoting subterms

    *)
  3. genv : subterm_spec Stdlib.Lazy.t list;
}
type stack_element =
  1. | SClosure of guard_env * Constr.constr
  2. | SArg of subterm_spec Stdlib.Lazy.t
val subterm_specif : guard_env -> stack_element list -> Constr.constr -> subterm_spec
val abstract_mind_lc : int -> int -> Names.MutInd.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array
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