Opened the possibility to type Ltac patterns but it is not fully functional yet

- to type patterns w/o losing the information of what subterm is a hole
  would need to remember where holes were in "understand", but "understand"
  needs sometimes to instantiate evars to ensure the type of an evar
  is not its original type but the type of its instance (what can
  e.g. lower a universe level); we would need here to update evars
  type at the same time we define them but this would need in turn to
  check the convertibility of the actual and expected type since otherwise
  type-checking constraints may disappear;
- typing pattern is apparently expensive in time; is it worth to do it
  for the benefit of pattern-matching compilation and coercion insertion?

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

6 files changed, 54 insertions, 25 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0d9a51ba37..ccba1d2cc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -32,6 +32,7 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
+  | MatchingVar of bool * identifier
 
 (* The type of mappings for existential variables *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3974e65b42..b82e6d998d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -94,6 +94,7 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
+  | MatchingVar of bool * identifier
 
 (*********************************************************************)
 (*** Existential variables and unification states ***)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 9acdd15855..7b8c623607 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -89,7 +89,10 @@ let head_of_constr_reference c = match kind_of_term c with
   | Var id -> VarRef id
   | _ -> anomaly "Not a rigid reference"
 
-let rec pattern_of_constr t =
+open Evd
+
+let pattern_of_constr sigma t =
+  let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
@@ -100,11 +103,25 @@ let rec pattern_of_constr t =
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
-    | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
+    | App (f,a) ->
+        (match 
+          match kind_of_term f with
+            Evar (evk,args) ->
+              (match snd (Evd.evar_source evk sigma) with
+                  MatchingVar (true,n) -> Some n
+                | _ -> None)
+            | _ -> None
+          with
+            | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a))
+            | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a))
     | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind sp        -> PRef (canonical_gr (IndRef sp))
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
-    | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
+    | Evar (evk,ctxt) ->
+        (match snd (Evd.evar_source evk sigma) with
+          | MatchingVar (b,n) -> assert (not b); PMeta (Some n)
+          | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+          | _ -> PMeta None)
     | Case (ci,p,a,br) ->
 	let cip = ci.ci_pp_info in
 	let no = Some (ci.ci_npar,cip.ind_nargs) in
@@ -113,6 +130,7 @@ let rec pattern_of_constr t =
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
     | CoFix f -> PCoFix f
+  in pattern_of_constr t
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -144,11 +162,12 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern subst pat = match pat with
+let rec subst_pattern subst pat =
+  match pat with
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr t
+	 pattern_of_constr Evd.empty t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index b0229ab618..0e87025fc8 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : constr -> constr_pattern
+val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern
 
 (* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 288eb9da22..cfe028aa51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -108,15 +108,16 @@ sig
   (* 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],
+     In [understand_ltac expand_evars 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
   *)
 
   val understand_ltac :
-    evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -156,7 +157,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_map ref -> env ->
+    bool -> bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
@@ -307,7 +308,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | RPatVar (loc,(someta,n)) ->
-	anomaly "Found a pattern variable in a rawterm to type"
+	let ty =
+          match tycon with
+            | Some (None, ty) -> ty
+            | None | Some _ ->
+		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+        let k = MatchingVar (someta,n) in
+	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | RHole (loc,k) ->
 	let ty =
@@ -418,7 +425,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	          let sigma =  !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
-		  make_judge c t
+		  make_judge c (* use this for keeping evars: resj.uj_val *) t
               | _ -> resj end
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -661,7 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env !evdref tj.utj_val v
 
-  let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+  let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -673,7 +680,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
-    let c = nf_evar !evdref c' in
+    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
 
@@ -701,30 +708,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
-  let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+  let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
   let understand_gen kind sigma env c =
-    snd (ise_pretype_gen true true sigma env ([],[]) kind 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 sigma env ([],[]) (OfType 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 sigma env ([],[]) IsType c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
 
-  let understand_ltac sigma env lvar kind c =
-    ise_pretype_gen false false sigma env lvar kind c
+  let understand_ltac expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false false sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-    ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
   let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-    pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
 end
 
 module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e3b18f73cb..75bd7874e7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -51,15 +51,16 @@ sig
   (* 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],
+     In [understand_ltac expand_evars 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
   *)
 
   val understand_ltac :
-    evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -97,7 +98,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_map ref -> env ->
+    bool -> bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr