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

4 files changed, 167 insertions, 108 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f859d0b421..24cc7aef80 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -837,7 +837,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
 
-let check_problems_are_solved env evd =
+let check_problems_are_solved evd =
   match snd (extract_all_conv_pbs evd) with
   | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
   | _ -> ()
@@ -915,7 +915,7 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = aux evd pbs false [] in
-  check_problems_are_solved env heuristic_solved_evd;
+  check_problems_are_solved heuristic_solved_evd;
   solve_unconstrained_impossible_cases heuristic_solved_evd
 
 (* Main entry points *)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 655dc1c1a2..c4961873a0 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -37,6 +37,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -
 
 val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
 
+(** Check all pending unification problems are solved and raise an
+    error otherwise *)
+
+val check_problems_are_solved : evar_map -> unit
+
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : constr * types stack -> constr * types stack ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6253fcfbfb..0af88d1dc3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,7 +44,7 @@ open Evarconv
 open Pattern
 open Misctypes
 
-type typing_constraint = OfType of types option | IsType
+type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = (Id.t * constr_under_binders) list
 type unbound_ltac_var_map = (Id.t * Id.t option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
@@ -103,46 +103,78 @@ let interp_elimination_sort = function
   | GSet  -> InSet
   | GType _ -> InType
 
-let resolve_evars env evdref fail_evar resolve_classes =
-  if resolve_classes then
-    (evdref := Typeclasses.resolve_typeclasses 
+type inference_flags = {
+  use_typeclasses : bool;
+  use_unif_heuristics : bool;
+  use_hook : (env -> evar_map -> evar -> constr) option;
+  fail_evar : bool;
+  expand_evars : bool
+}
+
+let apply_typeclasses env evdref fail_evar =
+  evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
      ~split:true ~fail:fail_evar env !evdref;
-     if Flags.is_program_mode () then (* Try optionally solving the obligations *)
-       evdref := Typeclasses.resolve_typeclasses 
-       ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref;     
-    );
+  if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+    evdref := Typeclasses.resolve_typeclasses
+      ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref
+
+let apply_inference_hook hook initial_sigma evdref =
+  evdref := fold_undefined (fun evk evi sigma ->
+    if not (Evd.mem initial_sigma evk) &&
+      is_undefined sigma evk (* i.e. not defined by side-effect *)
+    then
+      try
+        let c = hook sigma evk in
+        Evd.define evk c sigma
+      with Exit ->
+        sigma
+    else
+      sigma) !evdref !evdref
+
+let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  evdref :=
-    (try consider_remaining_unif_problems
-	   ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
-     with e when Errors.noncritical e ->
-       let e = Errors.push e in if fail_evar then raise e else !evdref)
-
-let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
-  let evdref = ref evd in
-  resolve_evars env evdref fail_evar use_classes;
-  let rec proc_rec c =
-    let c = Reductionops.whd_evar !evdref c in
-    match kind_of_term c with
-    | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
-        let sigma = !evdref in
-	(try
-	   let c = hook env sigma ev in
-	   evdref := Evd.define evk c !evdref;
-	   c
-	 with Exit ->
-           if fail_evar then
-	     let evi = Evd.find_undefined sigma evk in
-             let (loc,src) = evar_source evk !evdref in
-	     Pretype_errors.error_unsolvable_implicit loc env sigma evi src None
-           else
-             c)
-    | _ -> map_constr proc_rec c in
-  let c = proc_rec c in
-  (* Side-effect *)
-  !evdref,c
+  try evdref := consider_remaining_unif_problems
+	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in if fail_evar then raise e
+
+let check_typeclasses_instances_are_solved env sigma =
+  (* Naive way, call resolution again with failure flag *)
+  apply_typeclasses env (ref sigma) true
+
+let check_extra_evars_are_solved env initial_sigma sigma =
+  Evd.fold_undefined
+    (fun evk evi () ->
+      if not (Evd.mem initial_sigma evk) then
+        let (loc,k) = evar_source evk sigma in
+	match k with
+	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+	| _ ->
+	    let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
+	    error_unsolvable_implicit loc env sigma evi k None) sigma ()
+
+let check_evars_are_solved env initial_sigma sigma =
+  check_typeclasses_instances_are_solved env sigma;
+  check_problems_are_solved sigma;
+  check_extra_evars_are_solved env initial_sigma sigma
+
+(* Try typeclasses, hooks, unification heuristics ... *)
+
+let solve_remaining_evars flags env initial_sigma sigma =
+  let evdref = ref sigma in
+  if flags.use_typeclasses then apply_typeclasses env evdref false;
+  if Option.has_some flags.use_hook then
+    apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref;
+  if flags.use_unif_heuristics then apply_heuristics env evdref false;
+  if flags.fail_evar then check_evars_are_solved env initial_sigma !evdref;
+  !evdref
+
+let process_inference_flags flags env initial_sigma (sigma,c) =
+  let sigma = solve_remaining_evars flags env initial_sigma sigma in
+  let c = if flags.expand_evars then nf_evar sigma c else c in
+  sigma,c
 
 (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
@@ -717,62 +749,72 @@ and pretype_type valcon env evdref lvar = function
 	      error_unexpected_type_loc
                 (loc_of_glob_constr c) env !evdref tj.utj_val v
 
-let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
+let ise_pretype_gen flags sigma env lvar kind c =
+  let evdref = ref sigma in
   let c' = match kind with
+    | WithoutTypeConstraint ->
+        (pretype empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-	  (pretype tycon env evdref lvar c).uj_val
+	(pretype (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
 	(pretype_type empty_valcon env evdref lvar c).utj_val 
   in
-    resolve_evars env evdref fail_evar resolve_classes;
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-      if fail_evar then check_evars env Evd.empty !evdref c;
-      c
+  process_inference_flags flags env sigma (!evdref,c')
 
 (* TODO: comment faire remonter l'information si le typage a resolu des
    variables du sigma original. il faudrait que la fonction de typage
    retourne aussi le nouveau sigma...
 *)
 
+let default_inference_flags fail = {
+  use_typeclasses = true;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = fail;
+  expand_evars = true }
+
+let no_classes_no_fail_inference_flags = {
+  use_typeclasses = false;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = false;
+  expand_evars = true }
+
+let all_and_fail_flags = default_inference_flags true
+let all_no_fail_flags = default_inference_flags false
+
+let on_judgment f j =
+  let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
+  let (c,_,t) = destCast (f c) in
+  {uj_val = c; uj_type = t}
+
 let understand_judgment sigma env c =
   let evdref = ref sigma in
   let j = pretype empty_tycon env evdref ([],[]) c in
-    resolve_evars env evdref true true;
-    let j = j_nf_evar !evdref j in
-      check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-      j
+  on_judgment (fun c ->
+    snd (process_inference_flags all_and_fail_flags env sigma (!evdref,c))) j
 
 let understand_judgment_tcc evdref env c =
   let j = pretype empty_tycon env evdref ([],[]) c in
-    resolve_evars env evdref false true;
-    j_nf_evar !evdref j
-
-(* Raw calls to the unsafe inference machine: boolean says if we must
-   fail on unresolved evars; the unsafe_judgment list allows us to
-   extend env with some bindings *)
-
-let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
-  let evdref = ref sigma in
-  let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
-    !evdref, c
+  on_judgment (fun c ->
+    let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
+    evdref := evd; c) j
 
 (** Entry points of the high-level type synthesis algorithm *)
 
-let understand_gen kind sigma env c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
-
-let understand sigma env ?expected_type:exptyp c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
-
-let understand_type sigma env c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
+let understand
+    ?(flags=all_and_fail_flags)
+    ?(expected_type=WithoutTypeConstraint)
+    sigma env c =
+  snd (ise_pretype_gen flags sigma env ([],[]) expected_type c)
 
-let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
-  ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
+let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c =
+  ise_pretype_gen flags sigma env ([],[]) expected_type c
 
-let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-  ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
+let understand_tcc_evars ?(flags=all_no_fail_flags) evdref env ?(expected_type=WithoutTypeConstraint) c =
+  let sigma, c = ise_pretype_gen flags !evdref env ([],[]) expected_type c in
+  evdref := sigma;
+  c
 
-let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-  pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
+let understand_ltac flags sigma env lvar kind c =
+  ise_pretype_gen flags sigma env lvar kind c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 04d29ac28d..df65f10f33 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -26,7 +26,7 @@ open Misctypes
 val search_guard :
   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 = (Id.t * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (Id.t * Id.t option) list
@@ -34,6 +34,22 @@ 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
 
+type inference_flags = {
+  use_typeclasses : bool;
+  use_unif_heuristics : bool;
+  use_hook : (env -> evar_map -> evar -> constr) option;
+  fail_evar : bool;
+  expand_evars : bool
+}
+
+val default_inference_flags : bool -> inference_flags
+
+val no_classes_no_fail_inference_flags : inference_flags
+
+val all_no_fail_flags : inference_flags
+
+val all_and_fail_flags : inference_flags
+
 (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
@@ -41,42 +57,32 @@ val allow_anonymous_refs : bool ref
     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 -> glob_constr -> open_constr
+val understand_tcc : ?flags:inference_flags -> evar_map -> env ->
+  ?expected_type:typing_constraint -> glob_constr -> open_constr
 
-val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-  evar_map ref -> env -> typing_constraint -> glob_constr -> constr
+val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
+  ?expected_type:typing_constraint -> glob_constr -> constr
 
 (** More general entry point with evars from ltac *)
 
-(** Generic call to the interpreter from glob_constr to constr, failing
-    unresolved holes in the glob_constr cannot be instantiated.
+(** Generic call to the interpreter from glob_constr to constr
 
-    In [understand_ltac expand_evars sigma env ltac_env constraint c],
+    In [understand_ltac flags sigma env ltac_env constraint c],
 
-    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
+    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_ltac : ?resolve_classes:bool ->
-  bool -> evar_map -> env -> ltac_var_map ->
+val understand_ltac : inference_flags ->
+  evar_map -> env -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
 (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
-val understand : evar_map -> env -> ?expected_type:Term.types ->
-  glob_constr -> constr
-
-(** Idem but the glob_constr is intended to be a type *)
-
-val understand_type : evar_map -> env -> glob_constr -> constr
-
-(** A generalization of the two previous case *)
-
-val understand_gen : typing_constraint -> evar_map -> env ->
-  glob_constr -> constr
+val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
+  evar_map -> env -> glob_constr -> constr
 
 (** Idem but returns the judgment of the understood term *)
 
@@ -85,6 +91,17 @@ 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 -> glob_constr -> unsafe_judgment
 
+(** Trying to solve remaining evars and remaining conversion problems
+    with type classes, heuristics, and possibly an external solver *)
+
+val solve_remaining_evars : inference_flags ->
+  env -> (* initial map *) evar_map -> (* map to solve *) evar_map -> evar_map
+
+(** Checking evars are all solved and reporting an appropriate error message *)
+
+val check_evars_are_solved :
+  env -> (* initial map: *) evar_map -> (* map to check: *) evar_map -> unit
+
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
@@ -95,9 +112,9 @@ val pretype_type :
   val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
-val pretype_gen :
-  bool -> bool -> bool -> evar_map ref -> env ->
-  ltac_var_map -> typing_constraint -> glob_constr -> constr
+val ise_pretype_gen :
+  inference_flags -> evar_map -> env ->
+  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
 
 (**/**)
 
@@ -108,8 +125,3 @@ val constr_out : Dyn.t -> constr
 
 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