package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TermopsSource

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

about contexts

Sourceval push_named_rec_types : (Names.Name.t Constr.binder_annot array * Constr.types array * 'a) -> Environ.env -> Environ.env
Sourceval lookup_rel_id : Names.Id.t -> ('c, 't, 'r) 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.

Sourceval 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)|

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

Prod/Lambda/LetIn destructors on constr

Sourceval it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
Sourceval it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
Generic iterators on constr
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval drop_extra_implicit_args : Evd.evar_map -> EConstr.constr -> EConstr.constr

occur checks

Sourceexception Occur
Sourceval occur_meta : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_existential : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_meta_or_existential : Evd.evar_map -> EConstr.constr -> bool
Sourceval occur_metavariable : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
Sourceval occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
Sourceval occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
Sourceval occur_var_indirectly : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> Names.GlobRef.t option
Sourceval occur_var_in_decl : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
Sourceval 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

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

dependent m t tests whether m is a subterm of t

Sourceval dependent_no_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
Sourceval dependent_in_decl : Evd.evar_map -> EConstr.constr -> EConstr.named_declaration -> bool
Sourceval count_occurrences : Evd.evar_map -> EConstr.constr -> EConstr.constr -> int
Sourceval collect_metas : Evd.evar_map -> EConstr.constr -> int list

for visible vars only

Sourcetype meta_value_map = (Constr.metavariable * Constr.constr) list
Sourcetype 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

Sourceval 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

Sourceval base_sort_cmp : Conversion.conv_pb -> Sorts.t -> Sorts.t -> bool

Alternative term equalities

Sourceval eta_expand_instantiation : ?evars:CClosure.evar_handler -> Environ.env -> Constr.constr array -> Constr.rel_context -> Constr.constr array

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

  • returns

    B[a1...an]

Sourceval prod_applist_decls : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr

In prod_applist_decls 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.

Sourceval 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.

Sourceval nb_lam : Evd.evar_map -> EConstr.constr -> int

nb_lam sigma t counts the number of head lambda abstractions in t, ignoring casts. For instance on fun x1 x2 x3 => c (where c is not itself a lambda abstraction) it returns 3.

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

nb_prod sigma t counts the number of head products in t, ignoring casts.

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

Variant of nb_prod which also does zeta-reduction (i.e. reduces let-ins) along the way.

last_arg sigma t returns the last argument of t. Fails if t is not an application.

Sourcetype names_context = Names.Name.t list

name contexts

Sourceval lookup_name_of_rel : int -> names_context -> Names.Name.t
Sourceval lookup_rel_of_name : Names.Id.t -> names_context -> int
Sourceval empty_names_context : names_context
Sourceval ids_of_rel_context : ('c, 't, 'r) Context.Rel.pt -> Names.Id.t list
Sourceval ids_of_named_context : ('c, 't, 'r) Context.Named.pt -> Names.Id.t list
Sourceval ids_of_context : Environ.env -> Names.Id.t list
Sourceval names_of_rel_context : Environ.env -> names_context
Sourceval env_rel_context_chop : int -> Environ.env -> Environ.env * EConstr.rel_context
Sourceval vars_of_env : Environ.env -> Names.Id.Set.t

Set of local names

other signature iterators

Sourceval assums_of_rel_context : ('c, 't, 'r) Context.Rel.pt -> ((Names.Name.t, 'r) Context.pbinder_annot * 't) list
Sourceval fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a
Sourceval mem_named_context_val : Names.Id.t -> Environ.named_context_val -> bool
Sourceval clear_named_body : Names.Id.t -> Environ.env -> Environ.env

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

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

Test if an identifier is the basename of a global reference

Sourceval is_template_polymorphic_ref : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
Sourceval is_template_polymorphic_ind : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Prop : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Set : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_Type : Evd.evar_map -> EConstr.constr -> bool
Sourceval reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
Debug pretty-printers
Sourceval pr_global_env : Environ.env -> Names.GlobRef.t -> Pp.t
Sourceval pr_existential_key : Environ.env -> Evd.evar_map -> Evar.t -> Pp.t
Sourceval evar_suggested_name : Environ.env -> Evd.evar_map -> Evar.t -> Names.Id.t
Sourceval pr_evar_info : Environ.env -> Evd.evar_map -> 'a Evd.evar_info -> Pp.t
Sourceval pr_evar_constraints : Evd.evar_map -> Evd.evar_constraint list -> Pp.t
Sourceval pr_evar_map : ?with_univs:bool -> int option -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> Evd.any_evar_info -> bool) -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_evd_level : Evd.evar_map -> Univ.Level.t -> Pp.t
Sourceval pr_evd_qvar : Evd.evar_map -> Sorts.QVar.t -> Pp.t
Sourcemodule Internal : sig ... end

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

Sourceval pr_evar_universe_context : UState.t -> Pp.t
  • deprecated (9.0) Use [UState.pr] instead