diff options
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r-- | interp/constrintern.mli | 152 |
1 files changed, 80 insertions, 72 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b8b3d995..792e6f63 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,15 +8,18 @@ open Names open Term -open Sign +open Context open Evd open Environ open Libnames +open Globnames open Glob_term open Pattern -open Topconstr -open Termops +open Constrexpr +open Notation_term open Pretyping +open Misctypes +open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) @@ -37,7 +40,7 @@ open Pretyping of [env] *) type var_internalization_type = - | Inductive of identifier list (* list of params *) + | Inductive of Id.t list (* list of params *) | Recursive | Method | Variable @@ -46,14 +49,14 @@ type var_internalization_data = var_internalization_type * (** type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) - identifier list * + Id.t list * (** impargs to automatically add to the variable, e.g. for "JMeq A a B b" in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) Impargs.implicit_status list * (** signature of impargs of the variable *) - scope_name option list (** subscopes of the args of the variable *) + Notation_term.scope_name option list (** subscopes of the args of the variable *) (** A map of free variables to their implicit arguments and scopes *) -type internalization_env = var_internalization_data Idmap.t +type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env @@ -61,79 +64,81 @@ val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data val compute_internalization_env : env -> var_internalization_type -> - identifier list -> types list -> Impargs.manual_explicitation list list -> + Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = identifier list * unbound_ltac_var_map +type ltac_sign = { + ltac_vars : Id.Set.t; + (** Variables of Ltac which may be bound to a term *) + ltac_bound : Id.Set.t; + (** Other variables of Ltac *) +} -type glob_binder = (name * binding_kind * glob_constr option * glob_constr) +val empty_ltac_sign : ltac_sign + +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> glob_constr +val intern_constr : env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> glob_constr +val intern_type : env -> constr_expr -> glob_constr -val intern_gen : bool -> evar_map -> env -> +val intern_gen : typing_constraint -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> - Names.identifier list * - ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list - -val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list + Id.t list * (Id.t Id.Map.t * cases_pattern) list -(** {6 Composing internalization with pretyping } *) +val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list -(** Main interpretation function *) - -val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> - constr_expr -> constr +(** {6 Composing internalization with type inference (pretyping) } *) -(** Particular instances *) +(** Main interpretation functions expecting evars to be all resolved *) -val interp_constr : evar_map -> env -> - constr_expr -> constr +val interp_constr : env -> evar_map -> ?impls:internalization_env -> + constr_expr -> constr Evd.in_evar_universe_context -val interp_type : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types +val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> + constr_expr -> types -> constr Evd.in_evar_universe_context -val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_type : env -> evar_map -> ?impls:internalization_env -> + constr_expr -> types Evd.in_evar_universe_context -val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr +(** Main interpretation function expecting evars to be all resolved *) -val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types -> constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr -(** Accepting evars and giving back the manual implicits in addition. *) +(** Accepting unresolved evars *) -val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits +val interp_constr_evars : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> constr -val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:internalization_env -> - constr_expr -> types * Impargs.manual_implicits +val interp_casted_constr_evars : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> types -> constr -val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:internalization_env -> - constr_expr -> constr * Impargs.manual_implicits +val interp_type_evars : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> types -val interp_casted_constr_evars : evar_map ref -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr +(** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env -> - constr_expr -> types +val interp_constr_evars_impls : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> + constr * Impargs.manual_implicits -(** {6 Build a judgment } *) +val interp_casted_constr_evars_impls : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> types -> + constr * Impargs.manual_implicits -val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment +val interp_type_evars_impls : env -> evar_map ref -> + ?impls:internalization_env -> constr_expr -> + types * Impargs.manual_implicits (** Interprets constr patterns *) val intern_constr_pattern : - evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) @@ -144,39 +149,42 @@ val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) -val interp_binder : evar_map -> env -> name -> constr_expr -> types +val interp_binder : env -> evar_map -> Name.t -> constr_expr -> + types Evd.in_evar_universe_context -val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types (** Interpret contexts: returns extended env and context *) -val interp_context_gen : (env -> glob_constr -> types) -> - (env -> glob_constr -> unsafe_judgment) -> +val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> - evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) - -val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> - evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) + env -> evar_map ref -> local_binder list -> + internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> - evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) +(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) +(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) +(* ?global_level:bool -> ?impl_env:internalization_env -> *) +(* env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) + +(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) +(* env -> evar_map -> local_binder list -> *) +(* internalization_env * *) +(* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -val is_global : identifier -> bool -val construct_reference : named_context -> identifier -> constr -val global_reference : identifier -> constr -val global_reference_in_absolute_module : dir_path -> identifier -> constr - -(** Interprets a term as the left-hand side of a notation; the boolean - list is a set and this set is [true] for a variable occurring in - term position, [false] for a variable occurring in binding - position; [true;false] if in both kinds of position *) -val interp_aconstr : ?impls:internalization_env -> - (identifier * notation_var_internalization_type) list -> - (identifier * identifier) list -> constr_expr -> - (identifier * (subscopes * notation_var_internalization_type)) list * aconstr +val is_global : Id.t -> bool +val construct_reference : named_context -> Id.t -> constr +val global_reference : Id.t -> constr +val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr + +(** Interprets a term as the left-hand side of a notation. The returned map is + guaranteed to have the same domain as the input one. *) +val interp_notation_constr : ?impls:internalization_env -> + notation_interp_env -> constr_expr -> + (subscopes * notation_var_internalization_type) Id.Map.t * + notation_constr (** Globalization options *) val parsing_explicit : bool ref |