diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 47 |
1 files changed, 23 insertions, 24 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 61e7c6f5cb..a92e94d97b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,7 +18,6 @@ open Constrexpr open Notation_term open Pretyping open Misctypes -open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) @@ -39,7 +38,7 @@ open Decl_kinds of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -62,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env @@ -71,12 +70,12 @@ type ltac_sign = { (** Variables of Ltac which may be bound to a term *) ltac_bound : Id.Set.t; (** Other variables of Ltac *) + ltac_extra : Genintern.Store.t; + (** Arbitrary payload *) } 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 : env -> constr_expr -> glob_constr @@ -84,13 +83,13 @@ val intern_constr : env -> constr_expr -> glob_constr val intern_type : env -> constr_expr -> glob_constr val intern_gen : typing_constraint -> env -> - ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list +val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -101,7 +100,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types -> constr Evd.in_evar_universe_context + constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -109,32 +108,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> constr + ?impls:internalization_env -> constr_expr -> EConstr.constr val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> EConstr.constr val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types + ?impls:internalization_env -> constr_expr -> EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - constr * Impargs.manual_implicits + EConstr.constr * Impargs.manual_implicits val interp_casted_constr_evars_impls : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> - constr * Impargs.manual_implicits + ?impls:internalization_env -> constr_expr -> EConstr.types -> + EConstr.constr * Impargs.manual_implicits val interp_type_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - types * Impargs.manual_implicits + EConstr.types * Impargs.manual_implicits (** Interprets constr patterns *) @@ -153,22 +152,22 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types (** Interpret contexts: returns extended env and context *) val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder list -> - internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) + env -> evar_map ref -> local_binder_expr list -> + internalization_env * ((env * EConstr.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) *) +(* env -> evar_map -> local_binder_expr 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 -> *) +(* env -> evar_map -> local_binder_expr list -> *) (* internalization_env * *) (* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) @@ -177,9 +176,9 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : Context.Named.t -> Id.t -> constr -val global_reference : Id.t -> constr -val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference +val global_reference : Id.t -> Globnames.global_reference +val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference (** 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. *) |