A uniformization step around understand_* and interp_* functions.

- Clarification of the existence of three algorithms for solving
  unconstrained evars:
  - the type-class mechanism
  - the heuristics for solving pending conversion problems and multi-candidates
  - Declare Implicit Tactic (when called from tactics)

  Main function for solving unconstrained evars (when not using
  understand): Pretyping.solve_remaining_evars

- Clarification of the existence of three corresponding kinds of
  errors when reporting about unsolved evars:

  Main function for checking resolution of evars independently of the
  understand functions: Pretyping.check_evars_are_solved

- Introduction of inference flags in pretyping for governing which
  combination of the algorithms to use when calling some understand
  function; there is also a flag of expanding or not evars and for
  requiring or not the resolution of all evars

- Less hackish way of managing Pretyping.type_constraint: all three
  different possibilities are now represented by three different
  constructors

- Main semantical changes done:
  - solving unconstrained evars and reporting is not any longer mixed:
    one first tries to find unconstrained evars by any way possible;
    one eventually reports on the existence of unsolved evars using
    check_evars_are_solved
  - checking unsolved evars is now done by looking at the evar map,
    not by looking at the evars occurring in the terms to pretype; the
    only observed consequence so far is in Cases.v because of subterms
    (surprisingly) disappering after compilation of pattern-matching
  - the API changed, see dev/doc/changes.txt

Still to do:

- Find more uniform naming schemes:
  - for distinguishing when sigma is passed as a reference or as a value
    (are used: suffix _evars, prefix e_)
  - for distinguishing when evars are allowed to remain uninstantiated or not
    (are used: suffix _evars, again, suffix _tcc, infix _open_)
  - be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
  "preinfer", or "pretype". Grammatically, "understanding a term" looks
  strange.
- Investigate whether the inference flags in tacinterp.ml are really
  what we want (e.g. do we really want that heuristic remains
  activated when typeclasses are explicitly deactivated, idem in
  Tacinterp.interp_open_constr where flags are strange).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 76 insertions, 109 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 339a01d97..6eed1d0ed 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,8 +1659,8 @@ let extract_ids env =
 
 let scope_of_type_kind = function
   | IsType -> Some Notation.type_scope
-  | OfType (Some typ) -> compute_type_scope typ
-  | OfType None -> None
+  | OfType typ -> compute_type_scope typ
+  | WithoutTypeConstraint -> None
 
 let intern_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
@@ -1671,7 +1671,7 @@ let intern_gen kind sigma env
 			 impls = impls}
     allow_patvar (ltacvars, []) c
 
-let intern_constr sigma env c = intern_gen (OfType None) sigma env c
+let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c
 
 let intern_type sigma env c = intern_gen IsType sigma env c
 
@@ -1688,81 +1688,64 @@ let intern_pattern globalenv patt =
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
-let interp_gen kind sigma env
-               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
-               c =
-  let c = intern_gen kind ~impls ~allow_patvar ~ltacvars sigma env c in
-    understand_gen kind sigma env c
+(* All evars resolved *)
+
+let interp_gen kind sigma env ?(impls=empty_internalization_env) c =
+  let c = intern_gen kind ~impls sigma env c in
+  understand ~expected_type:kind sigma env c
 
-let interp_constr sigma env c =
-  interp_gen (OfType None) sigma env c
+let interp_constr sigma env ?(impls=empty_internalization_env) c =
+  interp_gen WithoutTypeConstraint sigma env c
 
 let interp_type sigma env ?(impls=empty_internalization_env) c =
   interp_gen IsType sigma env ~impls c
 
 let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
-  interp_gen (OfType (Some typ)) sigma env ~impls c
+  interp_gen (OfType typ) sigma env ~impls c
+
+(* Not all evars expected to be resolved *)
 
 let interp_open_constr sigma env c =
   understand_tcc sigma env (intern_constr sigma env c)
 
-let interp_open_constr_patvar sigma env c =
-  let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in
-  let sigma = ref sigma in
-  let evars = ref (Id.Map.empty : glob_constr Id.Map.t) in
-  let rec patvar_to_evar r = match r with
-    | GPatVar (loc,(_,id)) ->
-	( try Id.Map.find id !evars
-	  with Not_found ->
-	    let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
-	    let ev = Evarutil.e_new_evar sigma env ev in
-	    let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
-	    evars := Id.Map.add id rev !evars;
-	    rev
-	)
-    | _ -> map_glob_constr patvar_to_evar r in
-  let raw = patvar_to_evar raw in
-    understand_tcc !sigma env raw
-
-let interp_constr_judgment sigma env c =
-  understand_judgment sigma env (intern_constr sigma env c)
-
-let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
-    env ?(impls=empty_internalization_env) kind c =
-  let evdref =
-    match evdref with
-    | None -> ref Evd.empty
-    | Some evdref -> evdref
-  in
-  let istype = kind == IsType in
-  let c = intern_gen kind ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
-    understand_tcc_evars ~fail_evar evdref env kind c, imps
+(* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
-    env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
+let interp_constr_evars_gen_impls evdref
+    env ?(impls=empty_internalization_env) expected_type c =
+  let c = intern_gen expected_type ~impls !evdref env c in
+  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
+    understand_tcc_evars evdref env ~expected_type c, imps
 
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
+let interp_constr_evars_impls evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls evdref env ~impls WithoutTypeConstraint c
 
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
+let interp_casted_constr_evars_impls evdref env ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen_impls evdref env ~impls (OfType typ) c
 
-let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
-  let c = intern_gen kind ~impls !evdref env c in
-    understand_tcc_evars evdref env kind c
+let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls evdref env ~impls IsType c
+
+(* Not all evars expected to be resolved, with side-effect on evars *)
+
+let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c =
+  let c = intern_gen expected_type ~impls !evdref env c in
+  understand_tcc_evars evdref env ~expected_type c
+
+let interp_constr_evars evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen evdref env WithoutTypeConstraint ~impls c
 
 let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
+  interp_constr_evars_gen evdref env ~impls (OfType typ) c
 
 let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
+(* Miscellaneous *)
+
 type ltac_sign = Id.t list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
-  let c = intern_gen (if as_type then IsType else OfType None)
+  let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
             ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
 
@@ -1787,37 +1770,38 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
 let interp_binder sigma env na t =
   let t = intern_gen IsType sigma env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand_type sigma env t'
+  understand ~expected_type:IsType sigma env t'
 
 let interp_binder_evars evdref env na t =
   let t = intern_gen IsType !evdref env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand_tcc_evars evdref env IsType t'
+  understand_tcc_evars evdref env ~expected_type:IsType t'
 
 open Environ
 
 let my_intern_constr sigma env lvar acc c =
   internalize sigma env acc false lvar c
 
-let intern_context global_level sigma env impl_env params =
+let intern_context global_level sigma env impl_env binders =
   try
   let lvar = (([],[]), []) in
   let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
-	      tmp_scope = None; scopes = []; impls = impl_env}, []) params in
+	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_gen understand_type understand_judgment env bl =
+let interp_rawcontext_evars evdref env bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
 	match b with
 	    None ->
 	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-	      let t = understand_type env t' in
+	      let t =
+                understand_tcc_evars evdref env ~expected_type:IsType t' in
 	      let d = (na,None,t) in
 	      let impls =
 		if k == Implicit then
@@ -1827,21 +1811,14 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_judgment env b in
+	      let c = understand_judgment_tcc evdref env b in
 	      let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
 		(push_rel d env, d::params, succ n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
-  let int_env,bl = intern_context global_level sigma env impl_env params in
-    int_env, interp_rawcontext_gen understand_type understand_judgment env bl
-
-let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
-  interp_context_gen (understand_type sigma)
-    (understand_judgment sigma) ~global_level ~impl_env sigma env params
-
 let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
-  interp_context_gen (fun env t -> understand_tcc_evars evdref env IsType t)
-    (understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
+  let int_env,bl = intern_context global_level !evdref env impl_env params in
+  let x = interp_rawcontext_evars evdref env bl in
+  int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index e352c7f7a..32e878165 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,51 +88,47 @@ val intern_pattern : env -> cases_pattern_expr ->
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
-(** {6 Composing internalization with pretyping } *)
+(** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Main interpretation function *)
+(** Main interpretation functions expecting evars to be all resolved *)
 
-val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+val interp_constr : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> constr
 
-(** Particular instances *)
-
-val interp_constr : evar_map -> env ->
-  constr_expr -> constr
+val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
+  constr_expr -> types -> constr
 
 val interp_type : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
-val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
-
-val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
-
-val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
-  constr_expr -> types -> constr
+(** Main interpretation function expecting evars to be all resolved *)
 
-(** Accepting evars and giving back the manual implicits in addition. *)
-
-val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
-  ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
+val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> types * Impargs.manual_implicits
+(** Accepting unresolved evars *)
 
-val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> constr * Impargs.manual_implicits
+val interp_constr_evars : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> constr
 
 val interp_casted_constr_evars : evar_map ref -> env ->
   ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
-  constr_expr -> types
+val interp_type_evars : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> types
+
+(** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-(** {6 Build a judgment  } *)
+val interp_constr_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr ->
+  constr * Impargs.manual_implicits
 
-val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+val interp_casted_constr_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> types ->
+  constr * Impargs.manual_implicits
+
+val interp_type_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr ->
+  types * Impargs.manual_implicits
 
 (** Interprets constr patterns *)
 
@@ -154,16 +150,10 @@ val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
 
 (** Interpret contexts: returns extended env and context *)
 
-val interp_context_gen : (env -> glob_constr -> types) ->
-  (env -> glob_constr -> unsafe_judgment) ->
+val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-  
-val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-
-val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+  evar_map ref -> env -> local_binder list ->
+  internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)