summaryrefslogtreecommitdiff
path: root/pretyping/pretyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.mli')
-rw-r--r--pretyping/pretyping.mli76
1 files changed, 41 insertions, 35 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b94f9789..47b3ec87 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,24 +1,26 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** This file implements type inference. It maps [glob_constr]
+ (i.e. untyped terms whose names are located) to [constr]. In
+ particular, it drives complex pattern-matching problems ("match")
+ into elementary ones, insertion of coercions and resolution of
+ implicit arguments. *)
-(*i*)
open Names
open Sign
open Term
open Environ
open Evd
-open Rawterm
+open Glob_term
open Evarutil
-(*i*)
-(* An auxiliary function for searching for fixpoint guard indexes *)
+(** An auxiliary function for searching for fixpoint guard indexes *)
val search_guard :
Util.loc -> env -> int list list -> rec_declaration -> int array
@@ -28,30 +30,31 @@ type typing_constraint = OfType of types option | IsType
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 rawconstr_ltac_closure = ltac_var_map * rawconstr
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+type pure_open_constr = evar_map * constr
module type S =
sig
module Cases : Cases.S
- (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+ (** 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
+ (** 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 understand_tcc : ?resolve_classes:bool ->
- evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+ evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
- evar_map ref -> env -> typing_constraint -> rawconstr -> constr
+ evar_map ref -> env -> typing_constraint -> glob_constr -> constr
- (* More general entry point with evars from ltac *)
+ (** 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.
+ (** Generic call to the interpreter from glob_constr to constr, failing
+ unresolved holes in the glob_constr cannot be instantiated.
In [understand_ltac expand_evars sigma env ltac_env constraint c],
@@ -63,56 +66,59 @@ sig
val understand_ltac :
bool -> evar_map -> env -> ltac_var_map ->
- typing_constraint -> rawconstr -> evar_map * constr
+ typing_constraint -> glob_constr -> pure_open_constr
- (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+ (** Standard call to get a constr from a glob_constr, resolving implicit args *)
val understand : evar_map -> env -> ?expected_type:Term.types ->
- rawconstr -> constr
+ glob_constr -> constr
- (* Idem but the rawconstr is intended to be a type *)
+ (** Idem but the glob_constr is intended to be a type *)
- val understand_type : evar_map -> env -> rawconstr -> constr
+ val understand_type : evar_map -> env -> glob_constr -> constr
- (* A generalization of the two previous case *)
+ (** A generalization of the two previous case *)
val understand_gen : typing_constraint -> evar_map -> env ->
- rawconstr -> constr
+ glob_constr -> constr
- (* Idem but returns the judgment of the understood term *)
+ (** Idem but returns the judgment of the understood term *)
- val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+ val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
- (* Idem but do not fail on unresolved evars *)
- val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
+ (** Idem but do not fail on unresolved evars *)
+ val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
- (*i*)
- (* Internal of Pretyping...
- *)
+ (**/**)
+ (** Internal of Pretyping... *)
val pretype :
type_constraint -> env -> evar_map ref ->
- ltac_var_map -> rawconstr -> unsafe_judgment
+ ltac_var_map -> glob_constr -> unsafe_judgment
val pretype_type :
val_constraint -> env -> evar_map ref ->
- ltac_var_map -> rawconstr -> unsafe_type_judgment
+ ltac_var_map -> glob_constr -> unsafe_type_judgment
val pretype_gen :
bool -> bool -> bool -> evar_map ref -> env ->
- ltac_var_map -> typing_constraint -> rawconstr -> constr
+ ltac_var_map -> typing_constraint -> glob_constr -> constr
- (*i*)
+ (**/**)
end
module Pretyping_F (C : Coercion.S) : S
module Default : S
-(* To embed constr in rawconstr *)
+(** To embed constr in glob_constr *)
val constr_in : constr -> Dyn.t
val constr_out : Dyn.t -> constr
-val interp_sort : rawsort -> sorts
-val interp_elimination_sort : rawsort -> sorts_family
+val interp_sort : glob_sort -> 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