Imported Upstream version 8.5~beta1+dfsg

1 files changed, 68 insertions, 40 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f7817611..9b671bcf 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -1,21 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
-open Sign
 open Environ
 open Evd
-open Evarutil
 open Mod_subst
-open Glob_term
 open Unification
+open Misctypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
@@ -27,10 +24,8 @@ type clausenv = {
 				    out *)
   templtyp : constr freelisted (** its type *)}
 
-(** Substitution is not applied on templenv (because [subst_clenv] is
-   applied only on hints which typing env is overwritten by the
-   goal env) *)
-val subst_clenv : substitution -> clausenv -> clausenv
+
+val map_clenv : (constr -> constr) -> clausenv -> clausenv
 
 (** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
@@ -50,6 +45,9 @@ val mk_clenv_from_n :
 val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
+(** Refresh the universes in a clenv *)
+val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
+
 (** {6 linking of clenvs } *)
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
@@ -66,11 +64,6 @@ val clenv_unify :
 val clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
-(** same as above ([allow_K=false]) but replaces remaining metas
-   with fresh evars if [evars_flag] is [true] *)
-val evar_clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
@@ -89,9 +82,6 @@ val clenv_missing : clausenv -> metavariable list
 exception NoSuchBinding
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
-(** defines metas corresponding to the name of the bindings *)
-val clenv_match_args : arg_bindings -> clausenv -> clausenv
-
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
 (** start with a clenv to refine with a given term with bindings *)
@@ -104,31 +94,14 @@ val make_clenv_binding_env_apply :
    clausenv
 
 val make_clenv_binding_apply :
-  Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> constr * constr -> constr bindings ->
    clausenv
+
+val make_clenv_binding_env :
+  env -> evar_map -> constr * constr -> constr bindings -> clausenv
+
 val make_clenv_binding :
-  Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
-
-(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
-   [lmetas] is a list of metas to be applied to a proof of [t] so that
-   it produces the unification pattern [ccl]; [sigma'] is [sigma]
-   extended with [lmetas]; if [n] is defined, it limits the size of
-   the list even if [ccl] is still a product; otherwise, it stops when
-   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
-   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
-   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
-   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
-val clenv_environments :
- evar_map -> int option -> types -> evar_map * constr list * types
-
-(** [clenv_environments_evars env sigma n t] does the same but returns
-   a list of Evar's defined in [env] and extends [sigma] accordingly *)
-val clenv_environments_evars :
- env -> evar_map -> int option -> types -> evar_map * constr list * types
-
-(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
-val clenv_conv_leq :
- env -> evar_map -> types -> constr -> int -> constr list
+  env -> evar_map -> constr * constr -> constr bindings -> clausenv
 
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
@@ -137,3 +110,58 @@ val clenv_push_prod : clausenv -> clausenv
 (** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
+(** {6 Evar-based clauses} *)
+
+(** The following code is an adaptation of the [make_clenv_*] functions above,
+    except that it uses evars instead of metas, and naturally fits in the new
+    refinement monad. It should eventually replace all uses of the
+    aforementioned functions.
+
+    A clause is constructed as follows: assume a type [t := forall (x1 : A1) ...
+    (xn : An), T], we instantiate all the [xi] with a fresh evar [ei] and
+    return [T(xi := ei)] together with the [ei] enriched with a bit of
+    additional data. This is the simple part done by [make_evar_clause].
+
+    The problem lies in the fact we want to solve such holes with some
+    [constr bindings]. This entails some subtleties, because the provided terms
+    may only be well-typed up to a coercion, which we can only infer if we have
+    enough typing information. The meta machinery could insert coercions through
+    tricky instantiation delays. The only solution we have now is to delay the
+    tentative resolution of clauses by providing the [solve_evar_clause]
+    function, to be called at a smart enough time.
+*)
+
+type hole = {
+  hole_evar : constr;
+  (** The hole itself. Guaranteed to be an evar. *)
+  hole_type : types;
+  (** Type of the hole in the current environment. *)
+  hole_deps  : bool;
+  (** Whether the remainder of the clause was dependent in the hole. Note that
+      because let binders are substituted, it does not mean that it actually
+      appears somewhere in the returned clause. *)
+  hole_name : Name.t;
+  (** Name of the hole coming from its binder. *)
+}
+
+type clause = {
+  cl_holes : hole list;
+  cl_concl : types;
+}
+
+val make_evar_clause : env -> evar_map -> ?len:int -> types ->
+  (evar_map * clause)
+(** An evar version of {!make_clenv_binding}. Given a type [t],
+    [evar_environments env sigma ~len t bl] tries to eliminate at most [len]
+    products of the type [t] by filling it with evars. It returns the resulting
+    type together with the list of holes generated. Assumes that [t] is
+    well-typed in the environment. *)
+
+val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
+  evar_map
+(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
+    in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
+    the environment. The boolean [hyps] is a compatibility flag that allows to
+    consider arguments to be dependent only when they appear in hypotheses and
+    not in the conclusion. This boolean is only used when [bl] is of the form
+    [ImplicitBindings _]. *)