package rocq-runtime
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20
doc/rocq-runtime.engine/Termops/index.html
Module TermopsSource
This file defines various utilities for term manipulation that are not needed in the kernel.
val push_rel_assum :
(Names.Name.t EConstr.binder_annot * EConstr.types) ->
Environ.env ->
Environ.envabout contexts
val push_rels_assum :
(Names.Name.t Constr.binder_annot * Constr.types) list ->
Environ.env ->
Environ.envval push_named_rec_types :
(Names.Name.t Constr.binder_annot array * Constr.types array * 'a) ->
Environ.env ->
Environ.envAssociates the contents of an identifier in a rel_context. Raise Not_found if there is no such identifier.
Functions that build argument lists matching a block of binders or a context. rel_vect n m builds |Rel (n+m);...;Rel(n+1)|
Prod/Lambda/LetIn destructors on 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.constrval map_constr_with_full_binders :
Environ.env ->
Evd.evar_map ->
(EConstr.rel_declaration -> 'a -> 'a) ->
('a -> EConstr.constr -> EConstr.constr) ->
'a ->
EConstr.constr ->
EConstr.constrval fold_constr_with_full_binders :
Environ.env ->
Evd.evar_map ->
(EConstr.rel_declaration -> 'a -> 'a) ->
('a -> 'b -> EConstr.constr -> 'b) ->
'a ->
'b ->
EConstr.constr ->
'boccur checks
val occur_var_indirectly :
Environ.env ->
Evd.evar_map ->
Names.Id.t ->
EConstr.constr ->
Names.GlobRef.t optionval occur_var_in_decl :
Environ.env ->
Evd.evar_map ->
Names.Id.t ->
EConstr.named_declaration ->
boolval occur_vars_in_decl :
Environ.env ->
Evd.evar_map ->
Names.Id.Set.t ->
EConstr.named_declaration ->
boolAs occur_var but assume the identifier not to be a section variable
val free_rels_and_unqualified_refs :
Evd.evar_map ->
EConstr.constr ->
Int.Set.t * Names.Id.Set.tdependent m t tests whether m is a subterm of t
for visible vars only
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.constrreplace_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
val replace_term :
Evd.evar_map ->
EConstr.constr ->
EConstr.constr ->
EConstr.constr ->
EConstr.constrreplace_term d e c replaces d by e in c
Alternative term equalities
val compare_constr_univ :
Environ.env ->
Evd.evar_map ->
(Conversion.conv_pb -> EConstr.constr -> EConstr.constr -> bool) ->
Conversion.conv_pb ->
EConstr.constr ->
EConstr.constr ->
boolval constr_cmp :
Environ.env ->
Evd.evar_map ->
Conversion.conv_pb ->
EConstr.constr ->
EConstr.constr ->
boolval eta_expand_instantiation :
?evars:CClosure.evar_handler ->
Environ.env ->
Constr.constr array ->
Constr.rel_context ->
Constr.constr arrayprod_applist forall (x1:B1;...;xn:Bn), B a1...an
val prod_applist_decls :
Evd.evar_map ->
int ->
EConstr.constr ->
EConstr.constr list ->
EConstr.constrIn 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.
Remove recursively the casts around a term i.e. strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c.
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.
nb_prod sigma t counts the number of head products in t, ignoring casts.
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.
val adjust_app_list_size :
EConstr.constr ->
EConstr.constr list ->
EConstr.constr ->
EConstr.constr list ->
EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr listval adjust_app_array_size :
EConstr.constr ->
EConstr.constr array ->
EConstr.constr ->
EConstr.constr array ->
EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr arrayname contexts
Set of local names
val process_rel_context :
(EConstr.rel_declaration -> Environ.env -> Environ.env) ->
Environ.env ->
Environ.envother signature iterators
val assums_of_rel_context :
('c, 't, 'r) Context.Rel.pt ->
((Names.Name.t, 'r) Context.pbinder_annot * 't) listval map_rel_context_in_env :
(Environ.env -> Constr.constr -> Constr.constr) ->
Environ.env ->
Constr.rel_context ->
Constr.rel_contextval fold_named_context_both_sides :
('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
Constr.named_context ->
init:'a ->
'aval compact_named_context :
Evd.evar_map ->
EConstr.named_context ->
EConstr.compacted_contextval global_vars_set_of_decl :
Environ.env ->
Evd.evar_map ->
EConstr.named_declaration ->
Names.Id.Set.tval global_app_of_constr :
Evd.evar_map ->
EConstr.constr ->
(Names.GlobRef.t * EConstr.EInstance.t) * EConstr.constr optionval dependency_closure :
Environ.env ->
Evd.evar_map ->
EConstr.named_context ->
Names.Id.Set.t ->
Names.Id.t listGives an ordered list of hypotheses, closed by dependencies, containing a given set
Test if an identifier is the basename of a global reference
Debug pretty-printers
val pr_evar_map_filter :
?with_univs:bool ->
(Evar.t -> Evd.any_evar_info -> bool) ->
Environ.env ->
Evd.evar_map ->
Pp.tNOTE: to print terms you always want to use functions in Printer, not these ones which are for very special cases.