Quelle globEnv.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Names
open Environ
open Evd
open EConstr
open Ltac_pretype
open Evarutil

(** Type of environment extended with naming and ltac interpretation data *)

type t

(** To embed constr in glob_constr *)

type 'a obj_interp_fun =
  ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint ->
  'a -> unsafe_judgment * Evd.evar_map

val register_constr_interp0 :
  ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit

(** {6 Pretyping name management} *)

(** The following provides a level of abstraction for the kind of
    environment used for type inference (so-called pretyping); in
    particular:
    - it supports that term variables can be interpreted as Ltac
      variables pointing to the effective expected name
    - it incrementally and lazily computes the renaming of rel
      variables used to build purely-named evar contexts
*)

(** Build a pretyping environment from an ltac environment *)

val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t

(** Export the underlying environment *)

val env : t -> env
val renamed_env : t -> env
val lfun : t -> unbound_ltac_var_map

val vars_of_env : t -> Id.Set.t

(** Push to the environment, returning the declaration(s) with interpreted names *)

val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t

(** Declare an evar using renaming information *)

val new_evar : t -> evar_map -> ?src:Evar_kinds.t Loc.located ->
  ?naming:Namegen.intro_pattern_naming_expr -> ?relevance:ERelevance.t ->
  constr -> evar_map * constr

val new_type_evar : t -> evar_map -> src:Evar_kinds.t Loc.located -> evar_map * constr

(** Lookup the ident in the context that would be used for an evar in
    this environment, producing a term (Var or Rel) valid in [renamed_env]. *)
val lookup_renamed : t -> Id.t -> constr

(** [hide_variable env id] tells to hide the binding of [id] in
    the ltac environment part of [env]. It is useful e.g.
    for the dual status of [y] as term and binder. This is the case
    of [match y return p with ... end] which implicitly denotes
    [match z as z return p with ... end] when [y] is bound to a
    variable [z] and [match t as y return p with ... end] when [y]
    is bound to a non-variable term [t]. In the latter case, the
    binding of [y] to [t] should be hidden in [p]. *)

val hide_variable : t -> Id.t -> t

(** In case a variable is not bound by a term binder, look if it has
    an interpretation as a term in the ltac_var_map *)

val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> evar_map * unsafe_judgment) ->
  t -> evar_map -> Id.t -> evar_map * unsafe_judgment

(** Interp an identifier as an ltac variable bound to an identifier,
    or as the identifier itself if not bound to an ltac variable *)

val interp_ltac_id : t -> Id.t -> Id.t

(** Interpreting a generic argument, typically a "ltac:(...)", taking
    into account the possible renaming *)

val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint ->
  Genarg.glob_generic_argument -> unsafe_judgment * evar_map

quality100%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.