diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 73 |
1 files changed, 39 insertions, 34 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ebee4eda..acb13a8b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) (*i*) open Names @@ -30,45 +30,45 @@ open Pretyping - check all variables are bound - make absolute the references to global objets - resolution of symbolic notations using scopes - - insert existential variables for implicit arguments + - insertion of implicit arguments *) -(* To interpret implicits and arg scopes of recursive variables while - internalizing inductive types and recursive definitions, and also +(* To interpret implicit arguments and arg scopes of recursive variables + while internalizing inductive types and recursive definitions, and also projection while typing records. the third and fourth arguments associate a list of implicit positions and scopes to identifiers declared in the [rel_context] of [env] *) -type var_internalization_type = Inductive | Recursive | Method +type var_internalization_type = + | Inductive of identifier list (* list of params *) + | Recursive + | Method 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 * - Impargs.implicits_list * - scope_name option 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.implicits_list * (* signature of impargs 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 (* Contains also a list of identifiers to automatically apply to the variables*) -type full_internalization_env = - identifier list * internalization_env - -val empty_internalization_env : full_internalization_env +val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val set_internalization_env_params : - internalization_env -> identifier list -> full_internalization_env - -val compute_full_internalization_env : env -> - var_internalization_type -> - identifier list -> identifier list -> types list -> - Impargs.manual_explicitation list list -> full_internalization_env +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 @@ -83,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr val intern_type : evar_map -> env -> constr_expr -> rawconstr val intern_gen : bool -> evar_map -> env -> - ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr val intern_pattern : env -> cases_pattern_expr -> @@ -97,7 +97,7 @@ val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder (* Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr (* Particular instances *) @@ -105,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env -> val interp_constr : evar_map -> env -> constr_expr -> constr -val interp_type : evar_map -> env -> ?impls:full_internalization_env -> - constr_expr -> types +val interp_type : evar_map -> env -> ?impls:internalization_env -> + constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr -val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> +val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> constr_expr -> types -> constr (* 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:full_internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:full_internalization_env -> + env -> ?impls:internalization_env -> constr_expr -> types * manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> - env -> ?impls:full_internalization_env -> + env -> ?impls:internalization_env -> constr_expr -> constr * manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> - ?impls:full_internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> +val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -160,13 +160,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types val interp_context_gen : (env -> rawconstr -> types) -> (env -> rawconstr -> unsafe_judgment) -> - ?fail_anonymous:bool -> + ?global_level:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits -val interp_context : ?fail_anonymous:bool -> +val interp_context : ?global_level:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits -val interp_context_evars : ?fail_anonymous:bool -> +val interp_context_evars : ?global_level:bool -> evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) @@ -177,10 +177,15 @@ val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -(* Interprets into a abbreviatable 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:full_internalization_env -> - identifier list * identifier list -> constr_expr -> interpretation +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 *) val for_grammar : ('a -> 'b) -> 'a -> 'b |