package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.engine/Termops/index.html

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 econstr

  • deprecated (8.17) Use synonymous [EConstr.mkProd_or_LetIn].
  • deprecated (8.17) Use synonymous [EConstr.mkProd_wo_LetIn].
  • deprecated (8.17) Use synonymous [EConstr.it_mkProd].
  • deprecated (8.17) Use synonymous [EConstr.it_mkLambda].
  • deprecated (8.17) Use synonymous [EConstr.it_mkProd_or_LetIn].
  • deprecated (8.17) Use synonymous [EConstr.it_mkProd_wo_LetIn].
Sourceval it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
  • deprecated (8.17) Use synonymous [Term.it_mkLambda_or_LetIn].
  • deprecated (8.17) Use synonymous [EConstr.it_mkNamedProd_or_LetIn].
  • deprecated (8.17) Use synonymous [EConstr.it_mkNamedLambda_or_LetIn].

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

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 $ x_1:T_1...x_n:T_nc $ where $ c $ is not an abstraction gives $ n $ (casts are ignored)

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

Similar to nb_lam, but gives the number of products instead

Sourceval 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

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
  • deprecated (8.16) Use synonymous [Context.Rel.chop_nhyps].
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 lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
  • deprecated (8.15) Use synonymous [Vars.lift_rel_context].
Sourceval substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
  • deprecated (8.15) Use synonymous [Vars.substl_rel_context].
Sourceval smash_rel_context : Constr.rel_context -> Constr.rel_context
  • deprecated (8.15) Use synonymous [Vars.smash_rel_context].
Sourceval map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c, 'r) Context.Rel.pt -> ('c, 'c, 'r) Context.Rel.pt
  • deprecated (8.15) Use synonymous [Context.Rel.map_with_binders].
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 map_rel_decl : ('r1 -> 'r2) -> ('a -> 'b) -> ('a, 'a, 'r1) Context.Rel.Declaration.pt -> ('b, 'b, 'r2) Context.Rel.Declaration.pt
  • deprecated (8.20) Use [Context.Rel.Declaration.map_constr_het]
Sourceval map_named_decl : ('r1 -> 'r2) -> ('a -> 'b) -> ('a, 'a, 'r1) Context.Named.Declaration.pt -> ('b, 'b, 'r2) Context.Named.Declaration.pt
  • deprecated (8.20) Use [Context.Named.Declaration.map_constr_het]
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

  • deprecated (8.12) Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
  • deprecated (8.12) Use [EConstr.isRefX] instead.
Sourceval isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
  • deprecated (8.12) Use [EConstr.isRef] instead.
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 [Evd.pr_ustate] instead