package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

This file defines various utilities for term manipulation that are not needed in the kernel.

about contexts

val push_named_rec_types : (Names.Name.t Context.binder_annot array * Constr.types array * 'a) -> Environ.env -> Environ.env
val lookup_rel_id : Names.Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't

Associates the contents of an identifier in a rel_context. Raise Not_found if there is no such identifier.

val rel_vect : int -> int -> Constr.constr array

Functions that build argument lists matching a block of binders or a context. rel_vect n m builds |Rel (n+m);...;Rel(n+1)|

val rel_list : int -> int -> EConstr.constr list

iterators/destructors on terms

val it_mkProd_or_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkProd_wo_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val it_mkNamedProd_or_LetIn : EConstr.types -> EConstr.named_context -> EConstr.types
val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
val it_mkNamedLambda_or_LetIn : EConstr.constr -> EConstr.named_context -> EConstr.constr
val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
Generic iterators on constr
val map_constr_with_binders_left_to_right : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
val map_constr_with_full_binders : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr

fold_constr_with_binders g f n acc c folds f n on the immediate subterms of c starting from acc and proceeding from left to right according to the usual representation of the constructions as fold_constr but it carries an extra data n (typically a lift index) which is processed by g (which typically add 1 to n) at each binder traversal; it is not recursive

val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val fold_constr_with_full_binders : Environ.env -> Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val strip_head_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
val drop_extra_implicit_args : Evd.evar_map -> EConstr.constr -> EConstr.constr

occur checks

exception Occur
val occur_meta : Evd.evar_map -> EConstr.constr -> bool
val occur_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_meta_or_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_metavariable : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
val occur_var_indirectly : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> Names.GlobRef.t option
val occur_var_in_decl : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
val occur_vars : Environ.env -> Evd.evar_map -> Names.Id.Set.t -> EConstr.constr -> bool
val occur_vars_in_decl : Environ.env -> Evd.evar_map -> Names.Id.Set.t -> EConstr.named_declaration -> bool
val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool

As occur_var but assume the identifier not to be a section variable

val local_occur_var_in_decl : Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t
val free_rels_and_unqualified_refs : Evd.evar_map -> EConstr.constr -> Int.Set.t * Names.Id.Set.t
val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool

dependent m t tests whether m is a subterm of t

val dependent_no_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val dependent_in_decl : Evd.evar_map -> EConstr.constr -> EConstr.named_declaration -> bool
val count_occurrences : Evd.evar_map -> EConstr.constr -> EConstr.constr -> int
val collect_metas : Evd.evar_map -> EConstr.constr -> int list
val collect_vars : Evd.evar_map -> EConstr.constr -> Names.Id.Set.t

for visible vars only

type meta_value_map = (Constr.metavariable * Constr.constr) list
val isMetaOf : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
type meta_type_map = (Constr.metavariable * Constr.types) list

Type assignment for metavariables

pop c lifts by -1 the positive indexes in c

...

Substitution of an arbitrary large term. Uses equality modulo reduction of let

val replace_term_gen : Evd.evar_map -> (Evd.evar_map -> int -> EConstr.constr -> bool) -> int -> EConstr.constr -> EConstr.constr -> EConstr.constr

replace_term_gen eq arity e c replaces matching subterms according to eq by e in c. If arity is non-zero applications of larger length are handled atomically.

subst_term d c replaces d by Rel 1 in c

replace_term d e c replaces d by e in c

val base_sort_cmp : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool

Alternative term equalities

val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val eta_reduce_head : Evd.evar_map -> EConstr.constr -> EConstr.constr
val prod_applist : Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr

prod_applist forall (x1:B1;...;xn:Bn), B a1...an

  • returns

    B[a1...an]

val prod_applist_assum : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr

In prod_applist_assum n c args, c is supposed to have the form ∀Γ.c with Γ of length m and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded. Note that n counts both let-ins and prods, while the length of args only counts prods. In other words, varying n changes how many trailing let-ins are expanded.

val strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr

Remove recursively the casts around a term i.e. strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c.

exception CannotFilter

Lightweight first-order filtering procedure. Unification variables ar represented by (untyped) Evars. filtering c1 c2 returns the substitution n'th evar -> (context,term), or raises CannotFilter. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts.

val decompose_prod_letin : Evd.evar_map -> EConstr.constr -> int * EConstr.rel_context * EConstr.constr
val nb_lam : Evd.evar_map -> EConstr.constr -> int

nb_lam $ x_1:T_1...x_n:T_nc $ where $ c $ is not an abstraction gives $ n $ (casts are ignored)

val nb_prod : Evd.evar_map -> EConstr.constr -> int

Similar to nb_lam, but gives the number of products instead

val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.constr -> int

Similar to nb_prod, but zeta-contracts let-in on the way

Get the last arg of a constr intended to be an application

val decompose_app_vect : Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr array

Force the decomposition of a term as an applicative one

val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array
type names_context = Names.Name.t list

name contexts

val lookup_name_of_rel : int -> names_context -> Names.Name.t
val lookup_rel_of_name : Names.Id.t -> names_context -> int
val empty_names_context : names_context
val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Names.Id.t list
val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list
val ids_of_context : Environ.env -> Names.Id.t list
val names_of_rel_context : Environ.env -> names_context
  • deprecated Use synonymous [Context.Rel.chop_nhyps].
val env_rel_context_chop : int -> Environ.env -> Environ.env * EConstr.rel_context
val vars_of_env : Environ.env -> Names.Id.Set.t

Set of local names

other signature iterators

val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Names.Name.t Context.binder_annot * 't) list
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.lift_rel_context].
val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.substl_rel_context].
val smash_rel_context : Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.smash_rel_context].
val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
  • deprecated Use synonymous [Context.Rel.map_with_binders].
val fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a
val mem_named_context_val : Names.Id.t -> Environ.named_context_val -> bool
val compact_named_context : Constr.named_context -> Constr.compacted_context
val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
val global_vars_set : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.Set.t
val global_vars_set_of_decl : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.Set.t
val global_app_of_constr : Evd.evar_map -> EConstr.constr -> (Names.GlobRef.t * EConstr.EInstance.t) * EConstr.constr option
val dependency_closure : Environ.env -> Evd.evar_map -> EConstr.named_context -> Names.Id.Set.t -> Names.Id.t list

Gives an ordered list of hypotheses, closed by dependencies, containing a given set

val is_section_variable : Environ.env -> Names.Id.t -> bool

Test if an identifier is the basename of a global reference

  • deprecated Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
val is_global : Evd.evar_map -> Names.GlobRef.t -> EConstr.constr -> bool
  • deprecated Use [EConstr.isRefX] instead.
val isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
  • deprecated Use [EConstr.isRef] instead.
val is_template_polymorphic_ind : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_Prop : Evd.evar_map -> EConstr.constr -> bool
val is_Set : Evd.evar_map -> EConstr.constr -> bool
val is_Type : Evd.evar_map -> EConstr.constr -> bool
val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
Debug pretty-printers
val pr_existential_key : Environ.env -> Evd.evar_map -> Evar.t -> Pp.t
val evar_suggested_name : Environ.env -> Evd.evar_map -> Evar.t -> Names.Id.t
val pr_evar_info : Environ.env -> Evd.evar_map -> Evd.evar_info -> Pp.t
val pr_evar_constraints : Evd.evar_map -> Evd.evar_constraint list -> Pp.t
val pr_evar_map : ?with_univs:bool -> int option -> Environ.env -> Evd.evar_map -> Pp.t
val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> Evd.evar_info -> bool) -> Environ.env -> Evd.evar_map -> Pp.t
val pr_metaset : Evd.Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : Evd.evar_map -> Univ.Level.t -> Pp.t
module Internal : sig ... end

NOTE: to print terms you always want to use functions in Printer, not these ones which are for very special cases.

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