diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 107 |
1 files changed, 49 insertions, 58 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 767ec9ff..be78837f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,39 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: constrintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Term open Sign open Evd open Environ open Libnames -open Rawterm +open Glob_term open Pattern open Topconstr open Termops open Pretyping -(*i*) -(*s Translation from front abstract syntax of term to untyped terms (rawconstr) +(** Translation from front abstract syntax of term to untyped terms (glob_constr) *) - The translation performs: +(** The translation performs: - resolution of names : - check all variables are bound - make absolute the references to global objets - resolution of symbolic notations using scopes - insertion of implicit arguments -*) -(* To interpret implicit arguments and arg scopes of recursive variables + To interpret implicit arguments and arg scopes of recursive variables while internalizing inductive types and recursive definitions, and also projection while typing records. @@ -45,22 +40,21 @@ type var_internalization_type = | Inductive of identifier list (* list of params *) | Recursive | Method + | Variable 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 *) + (** 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 * - (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" + (** 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 *) + 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 = - (identifier * var_internalization_data) list +(** A map of free variables to their implicit arguments and scopes *) +type internalization_env = var_internalization_data Idmap.t -(* Contains also a list of identifiers to automatically apply to the variables*) val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> @@ -70,43 +64,41 @@ val compute_internalization_env : env -> var_internalization_type -> identifier list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type manual_implicits = (explicitation * (bool * bool * bool)) list - type ltac_sign = identifier list * unbound_ltac_var_map -type raw_binder = (name * binding_kind * rawconstr option * rawconstr) +type glob_binder = (name * binding_kind * glob_constr option * glob_constr) -(*s Internalisation performs interpretation of global names and notations *) +(** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> rawconstr +val intern_constr : evar_map -> env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> rawconstr +val intern_type : evar_map -> env -> constr_expr -> glob_constr val intern_gen : bool -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> - constr_expr -> rawconstr + constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * - ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list -val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list +val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list -(*s Composing internalization with pretyping *) +(** {6 Composing internalization with pretyping } *) -(* Main interpretation function *) +(** Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr -(* Particular instances *) +(** Particular instances *) val interp_constr : evar_map -> env -> constr_expr -> constr val interp_type : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types + constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr @@ -115,18 +107,18 @@ val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * c val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> constr_expr -> types -> constr -(* Accepting evars and giving back the manual implicits in addition. *) +(** Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> types * manual_implicits + constr_expr -> types * Impargs.manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> constr * manual_implicits + constr_expr -> constr * Impargs.manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -> constr @@ -134,58 +126,57 @@ val interp_casted_constr_evars : evar_map ref -> env -> val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -(*s Build a judgment *) +(** {6 Build a judgment } *) val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment -(* Interprets constr patterns *) +(** Interprets constr patterns *) val intern_constr_pattern : evar_map -> 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 *) +(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) val intern_reference : reference -> global_reference -(* Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> rawconstr +(** Expands abbreviations (syndef); raise an error if not existing *) +val interp_reference : ltac_sign -> reference -> glob_constr -(* Interpret binders *) +(** Interpret binders *) val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types -(* Interpret contexts: returns extended env and context *) +(** Interpret contexts: returns extended env and context *) -val interp_context_gen : (env -> rawconstr -> types) -> - (env -> rawconstr -> unsafe_judgment) -> - ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits +val interp_context_gen : (env -> glob_constr -> types) -> + (env -> glob_constr -> unsafe_judgment) -> + ?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 -> - evar_map -> env -> local_binder list -> (env * rel_context) * 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) -val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * 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) -(* Locating references of constructions, possibly via a syntactic definition *) -(* (these functions do not modify the glob file) *) +(** 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 *) - +(** 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 -(* Globalization leak for Grammar *) +(** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |