From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/pretyping.mli | 152 ++++++++++++++++++++++++++++-------------------- 1 file changed, 88 insertions(+), 64 deletions(-) (limited to 'pretyping/pretyping.mli') diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index a785b432..7d1e0c9b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> int list list -> rec_declaration -> int array + Loc.t -> env -> int list list -> rec_declaration -> int array -type typing_constraint = OfType of types option | IsType +type typing_constraint = OfType of types | IsType | WithoutTypeConstraint + +type var_map = Pattern.constr_under_binders Id.Map.t +type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} + +val empty_lvar : ltac_var_map -type var_map = (identifier * Pattern.constr_under_binders) list -type unbound_ltac_var_map = (identifier * identifier option) list -type ltac_var_map = var_map * unbound_ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -module type S = -sig +type inference_flags = { + use_typeclasses : bool; + use_unif_heuristics : bool; + use_hook : (env -> evar_map -> evar -> constr) option; + fail_evar : bool; + expand_evars : bool +} - module Cases : Cases.S +val default_inference_flags : bool -> inference_flags - (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - val allow_anonymous_refs : bool ref +val no_classes_no_fail_inference_flags : inference_flags - (** Generic call to the interpreter from glob_constr to open_constr, leaving - unresolved holes as evars and returning the typing contexts of - these evars. Work as [understand_gen] for the rest. *) +val all_no_fail_flags : inference_flags - val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr +val all_and_fail_flags : inference_flags - val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> glob_constr -> constr +(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +val allow_anonymous_refs : bool ref + +(** Generic call to the interpreter from glob_constr to open_constr, leaving + unresolved holes as evars and returning the typing contexts of + these evars. Work as [understand_gen] for the rest. *) - (** More general entry point with evars from ltac *) +val understand_tcc : ?flags:inference_flags -> env -> evar_map -> + ?expected_type:typing_constraint -> glob_constr -> open_constr - (** Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the glob_constr cannot be instantiated. +val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> + ?expected_type:typing_constraint -> glob_constr -> constr - In [understand_ltac expand_evars sigma env ltac_env constraint c], +(** More general entry point with evars from ltac *) - resolve_classes : launch typeclass resolution after typechecking. - expand_evars : expand inferred evars by their value if any - sigma : initial set of existential variables (typically dependent subgoals) - ltac_env : partial substitution of variables (used for the tactic language) - constraint : tell if interpreted as a possibly constrained term or a type - *) +(** Generic call to the interpreter from glob_constr to constr - val understand_ltac : ?resolve_classes:bool -> - bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + In [understand_ltac flags sigma env ltac_env constraint c], - (** Standard call to get a constr from a glob_constr, resolving implicit args *) + flags: tell how to manage evars + sigma: initial set of existential variables (typically current goals) + ltac_env: partial substitution of variables (used for the tactic language) + constraint: tell if interpreted as a possibly constrained term or a type +*) - val understand : evar_map -> env -> ?expected_type:Term.types -> - glob_constr -> constr +val understand_ltac : inference_flags -> + env -> evar_map -> ltac_var_map -> + typing_constraint -> glob_constr -> pure_open_constr - (** Idem but the glob_constr is intended to be a type *) +(** Standard call to get a constr from a glob_constr, resolving implicit args *) - val understand_type : evar_map -> env -> glob_constr -> constr +val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> + env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context - (** A generalization of the two previous case *) +(** Idem but returns the judgment of the understood term *) - val understand_gen : typing_constraint -> evar_map -> env -> - glob_constr -> constr +val understand_judgment : env -> evar_map -> + glob_constr -> unsafe_judgment Evd.in_evar_universe_context - (** Idem but returns the judgment of the understood term *) +(** Idem but do not fail on unresolved evars *) +val understand_judgment_tcc : env -> evar_map ref -> + glob_constr -> unsafe_judgment - val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment +(** Trying to solve remaining evars and remaining conversion problems + with type classes, heuristics, and possibly an external solver *) +(* For simplicity, it is assumed that current map has no other evars + with candidate and no other conversion problems that the one in + [pending], however, it can contain more evars than the pending ones. *) - (** Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment +val solve_remaining_evars : inference_flags -> + env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map - (**/**) - (** Internal of Pretyping... *) - val pretype : - bool -> type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment +(** Checking evars are all solved and reporting an appropriate error message *) - val pretype_type : - bool -> val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment +val check_evars_are_solved : + env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit - val pretype_gen : - bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> glob_constr -> constr +(**/**) +(** Internal of Pretyping... *) +val pretype : + bool -> type_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_judgment - (**/**) +val pretype_type : + bool -> val_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_type_judgment -end +val ise_pretype_gen : + inference_flags -> env -> evar_map -> + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr -module Pretyping_F (C : Coercion.S) : S -module Default : S +(**/**) (** To embed constr in glob_constr *) val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr -val interp_sort : glob_sort -> sorts +val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family -(** Last chance for solving evars, possibly using external solver *) -val solve_remaining_evars : bool -> bool -> - (env -> evar_map -> existential -> constr) -> - env -> evar_map -> pure_open_constr -> pure_open_constr +val genarg_interp_hook : + (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t -> + Genarg.glob_generic_argument -> constr * evar_map) Hook.t -- cgit v1.2.3