message d'erreur de garde des cofix

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

5 files changed, 44 insertions, 40 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 56f6cb8a1e..fa89c847be 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -722,7 +722,7 @@ let rec scrape_mind env kn =
 (***********************************************************************)
 (* Co-fixpoints. *)
 
-exception CoFixGuardError of guard_error
+exception CoFixGuardError of env * guard_error
 
 let anomaly_ill_typed () =
   anomaly "check_one_cofix: too many arguments applied to constructor"
@@ -735,7 +735,7 @@ let rec codomain_is_coind env c =
     | _ -> 
 	(try find_coinductive env b
         with Not_found ->
-	  raise (CoFixGuardError (CodomainNotInductiveType b)))
+	  raise (CoFixGuardError (env, CodomainNotInductiveType b)))
 
 let check_one_cofix env nbfix def deftype = 
   let rec check_rec_call env alreadygrd n vlra  t =
@@ -746,18 +746,15 @@ let check_one_cofix env nbfix def deftype =
       match kind_of_term c with 
 	| Meta _ -> true
 	      
-	| Rel p -> 
-             if n <= p && p < n+nbfix then
-	       (* recursive call *)
-               if alreadygrd then
-		 if List.for_all (noccur_with_meta n nbfix) args then
-		   true
-		 else 
-		   raise (CoFixGuardError NestedRecursiveOccurrences)
-               else 
-		 raise (CoFixGuardError (UnguardedRecursiveCall t))
-             else  
-	       error "check_one_cofix: ???"  (* ??? *)
+	| Rel p when  n <= p && p < n+nbfix ->
+	    (* recursive call *)
+            if alreadygrd then
+	      if List.for_all (noccur_with_meta n nbfix) args then
+		true
+	      else 
+		raise (CoFixGuardError (env,NestedRecursiveOccurrences))
+            else 
+	      raise (CoFixGuardError (env,UnguardedRecursiveCall t))
 		 
 	| Construct (_,i as cstr_kn)  ->
             let lra =vlra.(i-1) in 
@@ -770,7 +767,7 @@ let check_one_cofix env nbfix def deftype =
                     if noccur_with_meta n nbfix t
                     then process_args_of_constr (lr, lrar)
                     else raise (CoFixGuardError
-		                 (RecCallInNonRecArgOfConstructor t))
+		                 (env,RecCallInNonRecArgOfConstructor t))
                   else
                     let spec = dest_subterms rar in
                     check_rec_call env true n spec t &&
@@ -785,7 +782,7 @@ let check_one_cofix env nbfix def deftype =
               check_rec_call (push_rel (x, None, a) env)
 		alreadygrd (n+1)  vlra b
             else 
-	      raise (CoFixGuardError (RecCallInTypeOfAbstraction t))
+	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 	      
 	| CoFix (j,(_,varit,vdefs as recdef)) ->
             if (List.for_all (noccur_with_meta n nbfix) args)
@@ -798,9 +795,9 @@ let check_one_cofix env nbfix def deftype =
 		&&
 		(List.for_all (check_rec_call env alreadygrd (n+1) vlra) args) 
               else 
-		raise (CoFixGuardError (RecCallInTypeOfDef c))
+		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
 	    else
-	      raise (CoFixGuardError (UnguardedRecursiveCall c))
+	      raise (CoFixGuardError (env,UnguardedRecursiveCall c))
 
 	| Case (_,p,tm,vrest) ->
             if (noccur_with_meta n nbfix p) then
@@ -808,13 +805,13 @@ let check_one_cofix env nbfix def deftype =
 		if (List.for_all (noccur_with_meta n nbfix) args) then
 		  (array_for_all (check_rec_call env alreadygrd n vlra) vrest)
 		else 
-		  raise (CoFixGuardError (RecCallInCaseFun c))
+		  raise (CoFixGuardError (env,RecCallInCaseFun c))
               else 
-		raise (CoFixGuardError (RecCallInCaseArg c))
+		raise (CoFixGuardError (env,RecCallInCaseArg c))
             else 
-	      raise (CoFixGuardError (RecCallInCasePred c))
+	      raise (CoFixGuardError (env,RecCallInCasePred c))
               
-	| _    -> raise (CoFixGuardError NotGuardedForm) in 
+	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in 
   let (mind, _) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
   check_rec_call env false 1 (dest_subterms vlra) def
@@ -829,6 +826,6 @@ let check_cofix env (bodynum,(names,types,bodies as recdef)) =
     try 
       let _ = check_one_cofix fixenv nbfix bodies.(i) types.(i)
       in ()
-    with CoFixGuardError err -> 
-      error_ill_formed_rec_body fixenv err names i
+    with CoFixGuardError (errenv,err) -> 
+      error_ill_formed_rec_body errenv err names i
   done
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f37a6cb031..c0538c36a0 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -32,7 +32,7 @@ type guard_error =
   | RecCallInCaseFun of constr
   | RecCallInCaseArg of constr
   | RecCallInCasePred of constr
-  | NotGuardedForm
+  | NotGuardedForm of constr
 
 type arity_error =
   | NonInformativeToInformative
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b194dac975..b4897d6127 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -34,7 +34,7 @@ type guard_error =
   | RecCallInCaseFun of constr
   | RecCallInCaseArg of constr
   | RecCallInCasePred of constr
-  | NotGuardedForm
+  | NotGuardedForm of constr
 
 type arity_error =
   | NonInformativeToInformative
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 584b2c92c2..eebd0d6fbe 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -230,8 +230,9 @@ let explain_ill_formed_rec_body k ctx err names i vdefs =
       (str "Not allowed recursive call in the argument of cases")
   | RecCallInCasePred c ->
       (str "Not allowed recursive call in the type of cases in")
-  | NotGuardedForm ->
-      (str "Definition not in guarded form")
+  | NotGuardedForm c ->
+      str "Sub-expression " ++ prterm_env ctx c ++ spc() ++
+      str "not in guarded form (should be a constructor, Cases or CoFix)"
 in
   let pvd = P.pr_term k ctx vdefs.(i) in
   let s =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e62df6e766..3270ef4516 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -254,28 +254,34 @@ let explain_ill_formed_rec_body ctx err names i =
      str "Recursive call to " ++ called ++ str " had not enough arguments"
 
   (* CoFixpoint guard errors *)
-  (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
   | CodomainNotInductiveType c ->
-      str "The codomain is" ++ spc () ++ prterm c ++ spc () ++
+      str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++
       str "which should be a coinductive type"
   | NestedRecursiveOccurrences ->
-      str "Nested recursive occurrences"
+      str "nested recursive occurrences"
   | UnguardedRecursiveCall c ->
-      str "Unguarded recursive call"
+      str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c
   | RecCallInTypeOfAbstraction c ->
-      str "Not allowed recursive call in the domain of an abstraction"
+      str "recursive call forbidden in the domain of an abstraction:" ++
+      spc() ++ prterm_env ctx c
   | RecCallInNonRecArgOfConstructor c ->
-      str "Not allowed recursive call in a non-recursive argument of constructor"
+      str "recursive call on a non-recursive argument of constructor" ++
+      spc() ++ prterm_env ctx c
   | RecCallInTypeOfDef c ->
-      str "Not allowed recursive call in the type of a recursive definition"
+      str "recursive call forbidden in the type of a recursive definition" ++
+      spc() ++ prterm_env ctx c
   | RecCallInCaseFun c ->
-      str "Not allowed recursive call in a branch of cases"
+      str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c
   | RecCallInCaseArg c -> 
-      str "Not allowed recursive call in the argument of cases"
+      str "recursive call in the argument of cases in" ++ spc() ++
+      prterm_env ctx c
   | RecCallInCasePred c ->
-      str "Not allowed recursive call in the type of cases in"
-  | NotGuardedForm ->
-      str "Definition not in guarded form"
+      str "recursive call in the type of cases in" ++  spc() ++
+      prterm_env ctx c
+  | NotGuardedForm c ->
+      str "sub-expression " ++ prterm_env ctx c ++ spc() ++
+      str "not in guarded form" ++ spc()++
+      str"(should be a constructor, abstraction, Cases, CoFix or recursive call)"
   in
   prt_name i ++ str" is ill-formed." ++ fnl() ++
   pr_ne_context_of (str "In environment") ctx ++