Module `Termops`Source

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

val push_rel_assum : 
  (Names.Name.t Context.binder_annot * EConstr.types) ->
  Environ.env ->
  Environ.env

about contexts

Source

val push_rels_assum : 
  (Names.Name.t Context.binder_annot * Constr.types) list ->
  Environ.env ->
  Environ.env

Source

val push_named_rec_types : 
  (Names.Name.t Context.binder_annot array * Constr.types array * 'a) ->
  Environ.env ->
  Environ.env

Source

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.

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

Sourceval mkProd_or_LetIn : EConstr.rel_declaration -> EConstr.types -> EConstr.types

iterators/destructors on terms

Sourceval mkProd_wo_LetIn : EConstr.rel_declaration -> EConstr.types -> EConstr.types

Source

val it_mkProd : 
  EConstr.types ->
  (Names.Name.t Context.binder_annot * EConstr.types) list ->
  EConstr.types

Source

val it_mkLambda : 
  EConstr.constr ->
  (Names.Name.t Context.binder_annot * EConstr.types) list ->
  EConstr.constr

Sourceval it_mkProd_or_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types

Sourceval it_mkProd_wo_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types

Sourceval it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr

Source

val it_mkNamedProd_or_LetIn : 
  EConstr.types ->
  EConstr.named_context ->
  EConstr.types

Source

val it_mkNamedProd_wo_LetIn : 
  Constr.types ->
  Constr.named_context ->
  Constr.types

Source

val it_mkNamedLambda_or_LetIn : 
  EConstr.constr ->
  EConstr.named_context ->
  EConstr.constr

Source

val it_mkLambda_or_LetIn_from_no_LetIn : 
  Constr.constr ->
  Constr.rel_context ->
  Constr.constr

Generic iterators on constr

Source

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

Source

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

Source

val fold_constr_with_binders : 
  Evd.evar_map ->
  ('a -> 'a) ->
  ('a -> 'b -> EConstr.constr -> 'b) ->
  'a ->
  'b ->
  EConstr.constr ->
  'b

Source

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

Sourceval strip_head_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr

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

Source

val occur_metavariable : 
  Evd.evar_map ->
  Constr.metavariable ->
  EConstr.constr ->
  bool

Sourceval occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool

Source

val occur_var : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  EConstr.constr ->
  bool

Source

val occur_var_indirectly : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  EConstr.constr ->
  Names.GlobRef.t option

Source

val occur_var_in_decl : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  EConstr.named_declaration ->
  bool

Source

val occur_vars : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.Set.t ->
  EConstr.constr ->
  bool

Source

val occur_vars_in_decl : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.Set.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

Source

val local_occur_var_in_decl : 
  Evd.evar_map ->
  Names.Id.t ->
  EConstr.named_declaration ->
  bool

Sourceval free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t

Source

val 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

Source

val dependent_no_evar : 
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

val 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

Sourceval collect_vars : Evd.evar_map -> EConstr.constr -> Names.Id.Set.t

for visible vars only

Sourcetype meta_value_map = (Constr.metavariable * Constr.constr) list

Sourceval subst_meta : meta_value_map -> Constr.constr -> Constr.constr

Sourceval isMetaOf : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool

Sourcetype meta_type_map = (Constr.metavariable * Constr.types) list

Type assignment for metavariables

Sourceval pop : EConstr.constr -> EConstr.constr

pop c lifts by -1 the positive indexes in c

...

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

Source

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.

Source

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

subst_term d c replaces d by Rel 1 in c

Source

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

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

Source

val compare_constr_univ : 
  Evd.evar_map ->
  (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) ->
  Reduction.conv_pb ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

val constr_cmp : 
  Evd.evar_map ->
  Reduction.conv_pb ->
  EConstr.constr ->
  EConstr.constr ->
  bool

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

Sourceval eta_reduce_head : Evd.evar_map -> EConstr.constr -> EConstr.constr

Source

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]

Source

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.

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

Sourcetype subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t

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.

Source

val filtering : 
  Evd.evar_map ->
  EConstr.rel_context ->
  Reduction.conv_pb ->
  EConstr.constr ->
  EConstr.constr ->
  subst

Source

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

Source

val align_prod_letin : 
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  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

Sourceval last_arg : Evd.evar_map -> EConstr.constr -> EConstr.constr

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

Source

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

Force the decomposition of a term as an applicative one

Source

val adjust_app_list_size : 
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list

Source

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

Sourcetype names_context = Names.Name.t list

name contexts

Sourceval add_name : Names.Name.t -> names_context -> names_context

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

Source

val context_chop : 
  int ->
  Constr.rel_context ->
  Constr.rel_context * Constr.rel_context

Source

val 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

Sourceval add_vname : Names.Id.Set.t -> Names.Name.t -> Names.Id.Set.t

Source

val process_rel_context : 
  (EConstr.rel_declaration -> Environ.env -> Environ.env) ->
  Environ.env ->
  Environ.env

other signature iterators

Source

val 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].

Source

val 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].

Source

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

Source

val map_rel_context_in_env : 
  (Environ.env -> Constr.constr -> Constr.constr) ->
  Environ.env ->
  Constr.rel_context ->
  Constr.rel_context

Source

val 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 compact_named_context : Constr.named_context -> Constr.compacted_context

Source

val map_rel_decl : 
  ('a -> 'b) ->
  ('a, 'a) Context.Rel.Declaration.pt ->
  ('b, 'b) Context.Rel.Declaration.pt

Source

val 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

Source

val global_vars : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Names.Id.t list

Source

val global_vars_set : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Names.Id.Set.t

Source

val global_vars_set_of_decl : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.named_declaration ->
  Names.Id.Set.t

Source

val global_app_of_constr : 
  Evd.evar_map ->
  EConstr.constr ->
  (Names.GlobRef.t * EConstr.EInstance.t) * EConstr.constr option

Source

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

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

Test if an identifier is the basename of a global reference

Source

val global_of_constr : 
  Evd.evar_map ->
  EConstr.constr ->
  Names.GlobRef.t * EConstr.EInstance.t

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.

Source

val 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

Source

val pr_evar_map : 
  ?with_univs:bool ->
  int option ->
  Environ.env ->
  Evd.evar_map ->
  Pp.t

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.engine/Termops/index.html

Module `Termops`Source

Generic iterators on constr

...

Debug pretty-printers

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.engine/Termops/index.html

Module TermopsSource

Generic iterators on constr

...

Debug pretty-printers

Module `Termops`Source