package coq

  1. Overview
  2. Docs
package coq
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 Context.binder_annot array * Constr.types array * 'a) -> Environ.env -> Environ.env
Sourceval 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.

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

iterators/destructors on terms

Sourceval it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
Sourceval it_mkNamedProd_or_LetIn : EConstr.types -> EConstr.named_context -> EConstr.types
Sourceval it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
Sourceval it_mkNamedLambda_or_LetIn : EConstr.constr -> EConstr.named_context -> EConstr.constr
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

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

Sourceval fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
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 : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool

Alternative term equalities

Sourceval eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool

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

  • returns

    B[a1...an]

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

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.

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

Sourceval decompose_prod_letin : Evd.evar_map -> EConstr.constr -> int * EConstr.rel_context * EConstr.constr
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

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

Force the decomposition of a term as an applicative one

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) Context.Rel.pt -> Names.Id.t list
Sourceval ids_of_named_context : ('c, 't) 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 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) Context.Rel.pt -> (Names.Name.t Context.binder_annot * 't) list
Sourceval lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.lift_rel_context].
Sourceval substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.substl_rel_context].
Sourceval smash_rel_context : Constr.rel_context -> Constr.rel_context
  • deprecated Use synonymous [Vars.smash_rel_context].
Sourceval 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].
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 : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
Sourceval map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
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 Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
Sourceval is_global : Evd.evar_map -> Names.GlobRef.t -> EConstr.constr -> bool
  • deprecated Use [EConstr.isRefX] instead.
Sourceval isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
  • deprecated Use [EConstr.isRef] instead.
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_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 -> 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.evar_info -> bool) -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_metaset : Evd.Metaset.t -> Pp.t
Sourceval pr_evar_universe_context : UState.t -> Pp.t
Sourceval pr_evd_level : Evd.evar_map -> Univ.Level.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.

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