diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 67 |
1 files changed, 45 insertions, 22 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b39f6e18b..b08b8dd1f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -33,19 +33,42 @@ open Pretyping - insert existential variables for implicit arguments *) -(* To interpret implicits and arg scopes of recursive variables in - inductive types and recursive definitions; mention of a list of - implicits arguments in the ``rel'' part of [env]; the second - argument associates a list of implicit positions and scopes to - identifiers declared in the [rel_context] of [env] *) +(* To interpret implicits and arg scopes of recursive variables while + internalizing inductive types and recursive definitions, and also + projection while typing records. -type var_internalisation_type = Inductive | Recursive | Method + the third and fourth arguments associate a list of implicit + positions and scopes to identifiers declared in the [rel_context] + of [env] *) -type var_internalisation_data = - var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list +type var_internalization_type = Inductive | Recursive | Method -type implicits_env = (identifier * var_internalisation_data) list -type full_implicits_env = identifier list * implicits_env +type var_internalization_data = + var_internalization_type * + identifier list * + Impargs.implicits_list * + scope_name option list + +(* 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 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 type manual_implicits = (explicitation * (bool * bool * bool)) list @@ -60,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_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr val intern_pattern : env -> cases_pattern_expr -> @@ -69,12 +92,12 @@ val intern_pattern : env -> cases_pattern_expr -> val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list -(*s Composing internalisation with pretyping *) +(*s Composing internalization with pretyping *) (* Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr (* Particular instances *) @@ -82,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_implicits_env -> +val interp_type : evar_map -> env -> ?impls:full_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_implicits_env -> +val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr (* Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> - ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits + ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> - env -> ?impls:full_implicits_env -> + env -> ?impls:full_internalization_env -> constr_expr -> types * manual_implicits val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> - env -> ?impls:full_implicits_env -> + env -> ?impls:full_internalization_env -> constr_expr -> constr * manual_implicits val interp_casted_constr_evars : evar_defs ref -> env -> - ?impls:full_implicits_env -> constr_expr -> types -> constr + ?impls:full_internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> +val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -147,8 +170,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Interprets into a abbreviatable constr *) -val interp_aconstr : implicits_env -> identifier list * identifier list - -> constr_expr -> interpretation +val interp_aconstr : ?impls:full_internalization_env -> + identifier list * identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |