diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 142 |
1 files changed, 85 insertions, 57 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 4357e504..7bb8c374 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretyping.mli,v 1.28.2.1 2004/07/16 19:30:46 herbelin Exp $ i*) +(*i $Id: pretyping.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) (*i*) open Names @@ -18,69 +18,97 @@ open Rawterm open Evarutil (*i*) -type var_map = (identifier * unsafe_judgment) list - -(* constr with holes *) -type open_constr = evar_map * constr - - -(* Generic call to the interpreter from rawconstr to constr, failing - unresolved holes in the rawterm cannot be instantiated. - - In [understand_gen sigma env varmap typopt raw], - - sigma : initial set of existential variables (typically dependent subgoals) - varmap : partial subtitution of variables (used for the tactic language) - metamap : partial subtitution of meta (used for the tactic language) - typopt : is not None, this is the expected type for raw (used to define evars) -*) -val understand_gen : - evar_map -> env -> var_map - -> expected_type:(constr option) -> rawconstr -> constr +type typing_constraint = OfType of types option | IsType -val understand_gen_ltac : - evar_map -> env -> var_map * (identifier * identifier option) list - -> expected_type:(constr option) -> rawconstr -> constr - -(* Generic call to the interpreter from rawconstr to constr, turning - unresolved holes into metas. Returns also the typing context of - these metas. Work as [understand_gen] for the rest. *) -val understand_gen_tcc : - evar_map -> env -> var_map - -> constr option -> rawconstr -> open_constr - -(* Standard call to get a constr from a rawconstr, resolving implicit args *) -val understand : evar_map -> env -> rawconstr -> constr +type var_map = (identifier * unsafe_judgment) list +type unbound_ltac_var_map = (identifier * identifier option) list + +module type S = +sig + + module Cases : Cases.S + + (* 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 rawconstr to open_constr, leaving + unresolved holes as evars and returning the typing contexts of + these evars. Work as [understand_gen] for the rest. *) + + val understand_tcc : + evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr + + val understand_tcc_evars : + evar_defs ref -> env -> typing_constraint -> rawconstr -> constr + + (* More general entry point with evars from ltac *) + + (* Generic call to the interpreter from rawconstr to constr, failing + unresolved holes in the rawterm cannot be instantiated. + + In [understand_ltac sigma env ltac_env constraint c], + + 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 + *) + + val understand_ltac : + evar_map -> env -> var_map * unbound_ltac_var_map -> + typing_constraint -> rawconstr -> evar_defs * constr + + (* Standard call to get a constr from a rawconstr, resolving implicit args *) + + val understand : evar_map -> env -> ?expected_type:Term.types -> + rawconstr -> constr + + (* Idem but the rawconstr is intended to be a type *) + + val understand_type : evar_map -> env -> rawconstr -> constr + + (* A generalization of the two previous case *) + + val understand_gen : typing_constraint -> evar_map -> env -> + rawconstr -> constr + + (* Idem but returns the judgment of the understood term *) + + val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + + (* Idem but do not fail on unresolved evars *) + val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + + + (*i*) + (* Internal of Pretyping... + *) + val pretype : + type_constraint -> env -> evar_defs ref -> + var_map * (identifier * identifier option) list -> + rawconstr -> unsafe_judgment + + val pretype_type : + val_constraint -> env -> evar_defs ref -> + var_map * (identifier * identifier option) list -> + rawconstr -> unsafe_type_judgment -(* Idem but the rawconstr is intended to be a type *) -val understand_type : evar_map -> env -> rawconstr -> constr + val pretype_gen : + evar_defs ref -> env -> + var_map * (identifier * identifier option) list -> + typing_constraint -> rawconstr -> constr -(* Idem but returns the judgment of the understood term *) -val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + (*i*) + +end -(* Idem but returns the judgment of the understood type *) -val understand_type_judgment : evar_map -> env -> rawconstr - -> unsafe_type_judgment +module Pretyping_F (C : Coercion.S) : S +module Default : S (* To embed constr in rawconstr *) + val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr -(*i*) -(* Internal of Pretyping... - * Unused outside, but useful for debugging - *) -val pretype : - type_constraint -> env -> evar_defs -> - var_map * (identifier * identifier option) list -> - rawconstr -> unsafe_judgment - -val pretype_type : - val_constraint -> env -> evar_defs -> - var_map * (identifier * identifier option) list -> - rawconstr -> unsafe_type_judgment -(*i*) - -val interp_sort : rawsort -> sorts - +val interp_sort : rawsort -> sorts val interp_elimination_sort : rawsort -> sorts_family + |