pretyping/pretyping.ml

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

6 files changed, 45 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f7c739fe6..c552be7d6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -393,15 +393,18 @@ let rec find_row_ind = function
 
 exception NotCoercible
 
-let inh_coerce_to_ind isevars env ty tyi =
+let inh_coerce_to_ind isevars env tmloc ty tyi =
   let (mib,mip) = Inductive.lookup_mind_specif env tyi in
   let (ntys,_) = splay_prod env (evars_of isevars) mip.mind_nf_arity in
-   let (_,evarl) =
+  let hole_source = match tmloc with 
+    | Some loc -> fun i -> (loc, TomatchTypeParameter (tyi,i))
+    | None -> fun _ -> (dummy_loc, InternalHole) in
+   let (_,evarl,_) =
     List.fold_right
-      (fun (na,ty) (env,evl) ->
+      (fun (na,ty) (env,evl,n) ->
 	 (push_rel (na,None,ty) env,
-	    (new_isevar isevars env (dummy_loc, InternalHole) ty)::evl))
-      ntys (env,[]) in
+	    (new_isevar isevars env (hole_source n) ty)::evl,n+1))
+      ntys (env,[],1) in
   let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
@@ -414,11 +417,11 @@ let inh_coerce_to_ind isevars env ty tyi =
  * use the function above.
  *)
 
-let unify_tomatch_with_patterns isevars env typ = function
+let unify_tomatch_with_patterns isevars env tmloc typ = function
   | Some (cloc,(cstr,_ as c)) ->
       (let tyi = inductive_of_constructor c in
        try 
-	 let indtyp = inh_coerce_to_ind isevars env typ tyi in
+	 let indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in
 	 IsInd (typ,find_rectype env (evars_of isevars) typ)
        with NotCoercible ->
 	 (* 2 cases : Not the right inductive or not an inductive at all *)
@@ -435,7 +438,8 @@ let unify_tomatch_with_patterns isevars env typ = function
 let coerce_row typing_fun isevars env cstropt tomatch =
   let j = typing_fun empty_tycon env tomatch in
   let typ = body_of_type j.uj_type in
-  let t = unify_tomatch_with_patterns isevars env typ cstropt in
+  let loc = loc_of_rawconstr tomatch in
+  let t = unify_tomatch_with_patterns isevars env (Some loc) typ cstropt in
   (j.uj_val,t)
 
 let coerce_to_indtype typing_fun isevars env matx tomatchl =
@@ -452,7 +456,7 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
 let to_mutind env isevars tm c t =
   match c with
     | Some body -> NotInd (c,t)
-    | None -> unify_tomatch_with_patterns isevars env t (find_row_ind tm)
+    | None -> unify_tomatch_with_patterns isevars env None t (find_row_ind tm)
 
 let type_of_tomatch = function
   | IsInd (t,_) -> t
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cc8b0ed8b..4a60fce3d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -24,6 +24,7 @@ type pretype_error =
   (* Unification *)
   | OccurCheck of int * constr
   | NotClean of int * constr
+  | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -135,6 +136,9 @@ let error_not_clean env sigma ev c =
   let c = nf_evar sigma c in
   raise (PretypeError (env_ise sigma env, NotClean (ev,c)))
 
+let error_unsolvable_implicit loc env sigma e =
+  raise (PretypeError (env_ise sigma env, UnsolvableImplicit e))
+
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index c3921f245..cb26d3078 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -26,6 +26,7 @@ type pretype_error =
   (* Unification *)
   | OccurCheck of int * constr
   | NotClean of int * constr
+  | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -77,6 +78,8 @@ val error_occur_check : env ->  Evd.evar_map -> int -> constr -> 'b
 
 val error_not_clean : env ->  Evd.evar_map -> int -> constr -> 'b
 
+val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b
+
 (*s Ml Case errors *)
 
 val error_cant_find_case_type_loc :
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0f376ae5e..250fc70dc 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -50,6 +50,7 @@ type hole_kind =
   | QuestionMark
   | CasesType
   | InternalHole
+  | TomatchTypeParameter of inductive * int
 
 type 'ctxt reference =
   | RConst of constant * 'ctxt
@@ -163,9 +164,8 @@ let rec subst_raw subst raw =
       let ref' = subst_global subst ref in 
 	if ref' == ref then raw else
 	  RHole (loc,ImplicitArg (ref',i))
-  | RHole (loc, 
-	   (AbstractionType _ | QuestionMark | CasesType | InternalHole)) ->
-      raw
+  | RHole (loc, (AbstractionType _ | QuestionMark | CasesType |
+      InternalHole | TomatchTypeParameter _)) -> raw
 
   | RCast (loc,r1,r2) -> 
       let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index e8b0726c9..5f155aa2d 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -49,6 +49,7 @@ type hole_kind =
   | QuestionMark
   | CasesType
   | InternalHole
+  | TomatchTypeParameter of inductive * int
 
 type 'ctxt reference =
   | RConst of constant * 'ctxt
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a64c3b800..63b310bc3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -26,6 +26,7 @@ open Cases
 open Logic
 open Printer
 open Ast
+open Rawterm
 
 let guill s = "\""^s^"\""
 
@@ -278,6 +279,24 @@ let explain_not_clean ctx ev t =
   str" with a term using variable " ++ var ++ spc () ++
   str"which is not in its scope."
 
+let explain_unsolvable_implicit env = function
+  | QuestionMark -> str "Cannot infer a term for this placeholder"
+  | CasesType ->
+      str "Cannot infer the type of this pattern-matching problem"
+  | AbstractionType (Name id) ->
+      str "Cannot infer a type for " ++ Nameops.pr_id id
+  | AbstractionType Anonymous ->
+      str "Cannot infer a type of this anonymous abstraction"
+  | ImplicitArg (c,n) ->
+      str "Cannot infer the " ++ pr_ord n ++
+      str " implicit argument of " ++ Nametab.pr_global_env None c
+  | InternalHole ->
+      str "Cannot infer a term for an internal placeholder"
+  | TomatchTypeParameter (tyi,n) ->
+      str "Cannot infer the " ++ pr_ord n ++
+      str " argument of the inductive type (" ++ pr_inductive env tyi ++
+      str ") of this term"
+
 let explain_var_not_found ctx id = 
   str "The variable" ++ spc () ++ str (string_of_id id) ++
   spc ()  ++ str "was not found" ++ 
@@ -339,6 +358,8 @@ let explain_pretype_error ctx = function
       explain_occur_check ctx n c
   | NotClean (n,c) ->
       explain_not_clean ctx n c
+  | UnsolvableImplicit k ->
+      explain_unsolvable_implicit ctx k
   | VarNotFound id ->
       explain_var_not_found ctx id
   | UnexpectedType (actual,expected) ->