Amelioration des messages d'erreur de Fucntion

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

6 files changed, 93 insertions, 40 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index f83eae8d3..7aec837d8 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -346,6 +346,7 @@ let generate_functional_principle
     interactive_proof
     old_princ_type sorts new_princ_name funs i proof_tac
     =
+  try 
   let f = funs.(i) in
   let type_sort = Termops.new_sort_in_family InType in
   let new_sorts =
@@ -393,6 +394,10 @@ let generate_functional_principle
     build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook 
   in
   save false new_princ_name entry g_kind hook
+  with 
+    | Defining_principle _ as e -> raise e
+    | e -> raise (Defining_principle e)
+
 (*   defined  () *)
 
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index f17ae6450..cfaa2d4d7 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -240,23 +240,36 @@ let prepare_body (name,annot,args,types,body) rt =
   (fun_args,rt')
 
 
-let derive_inversion fix_names = 
-  try
-    Invfun.derive_correctness 
-      Functional_principles_types.make_scheme
-      functional_induction 
-      (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
-      (*i The next call to mk_rel_id is valid since we have just construct the graph 
-	Ensures by : register_built
-	i*) 
-      (List.map
-	 (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
-	 fix_names
-      )
-  with e -> 
-    msg_warning 
-      (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
-	  
+let derive_inversion fix_names =
+  try 
+    (* we first transform the fix_names identifier into their corresponding constant *)
+    let fix_names_as_constant = 
+      List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names 
+    in 
+    (* 
+       Then we check that the graphs have been defined 
+       If one of the graphs haven't been defined 
+       we do nothing
+    *)
+    List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
+    try
+      Invfun.derive_correctness 
+	Functional_principles_types.make_scheme
+	functional_induction 
+	fix_names_as_constant
+	(*i The next call to mk_rel_id is valid since we have just construct the graph 
+	  Ensures by : register_built
+	  i*) 
+	(List.map
+	   (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+	   fix_names
+	)
+    with e -> 
+      msg_warning 
+	(str "Cannot define correction of function and graph" ++ 
+	   if do_observe () then Cerrors.explain_exn e else mt ())
+  with _ -> ()
+
 let generate_principle 
     is_general do_built fix_rec_l recdefs  interactive_proof parametrize 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
@@ -312,8 +325,18 @@ let generate_principle
 	()
       end
   with e -> 
-    Pp.msg_warning (Cerrors.explain_exn e) 
-
+    match e with 
+      | Building_graph e -> 
+	    Pp.msg_warning 
+	    (str "Cannot define graph(s) for " ++ 
+	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	       if do_observe () then Cerrors.explain_exn e else mt ())
+      | Defining_principle e -> 
+	    Pp.msg_warning
+	    (str "Cannot define principle(s) for "++ 
+	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	       if do_observe () then Cerrors.explain_exn e else mt ())
+      | _ -> anomaly ""
 
 let register_struct is_rec fixpoint_exprl = 
   match fixpoint_exprl with 
@@ -513,7 +536,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	    interactive_proof
 	    true
 	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	  if register_built then derive_inversion  fix_names;
+	  if register_built then derive_inversion fix_names;
 	  true;
   in
   ()
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index a7f7dbf82..4e1e13092 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -278,11 +278,14 @@ type function_info =
     }
       
 
-type function_db  = function_info list
+(* type function_db  = function_info list *)
+
+(* let function_table = ref ([] : function_db) *)
 
-let function_table = ref ([] : function_db)
-  
 
+let from_function = ref Cmap.empty
+let from_graph = ref Indmap.empty
+(*
 let rec do_cache_info finfo = function 
   | [] -> raise Not_found 
   | (finfo'::finfos as l) -> 
@@ -301,6 +304,12 @@ let cache_Function (_,(finfos)) =
   in  
   if new_tbl != !function_table 
   then function_table := new_tbl
+*)
+
+let cache_Function (_,finfos) = 
+  from_function := Cmap.add finfos.function_constant finfos !from_function;
+  from_graph := Indmap.add finfos.graph_ind finfos !from_graph
+
 
 let load_Function _  = cache_Function
 let open_Function _ = cache_Function
@@ -386,7 +395,8 @@ let pr_info f_info =
     str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
     str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 
 
-let pr_table l = 
+let pr_table tb = 
+  let l = Cmap.fold (fun k v acc -> v::acc) tb [] in 
   Util.prlist_with_sep fnl pr_info l
 
 let in_Function,out_Function = 
@@ -405,17 +415,16 @@ let in_Function,out_Function =
 
 (* Synchronisation with reset *)
 let freeze () = 
-  let tbl = !function_table in 
-(*   Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *)
-  tbl
-
-let unfreeze l = 
+  !from_function,!from_graph
+let unfreeze (functions,graphs) = 
 (*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
-  function_table :=
- l
+  from_function := functions;
+  from_graph := graphs
+
 let init () = 
 (*   Pp.msgnl (str "reseting function_table");  *)
-  function_table := []
+  from_function := Cmap.empty;
+  from_graph := Indmap.empty
 
 let _ = 
   Summary.declare_summary "functions_db_sum"
@@ -434,11 +443,11 @@ let find_or_none id =
 
 
 let find_Function_infos f = 
-  List.find (fun finfo ->  finfo.function_constant = f) !function_table
+  Cmap.find f !from_function
 
 
 let find_Function_of_graph ind = 
-  List.find (fun finfo ->  finfo.graph_ind = ind) !function_table
+  Indmap.find ind !from_graph
   
 let update_Function finfo = 
 (*   Pp.msgnl (pr_info finfo); *)
@@ -472,7 +481,7 @@ let add_Function is_general f =
   in
   update_Function finfos
 
-let pr_table () = pr_table !function_table
+let pr_table () = pr_table !from_function
 (*********************************)
 (* Debuging *)
 let function_debug = ref false 
@@ -495,3 +504,5 @@ let do_observe () =
       
       
     
+exception Building_graph of exn 
+exception Defining_principle of exn
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 1c8d880a2..7da1d6f0b 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -108,6 +108,10 @@ val pr_info : function_info -> Pp.std_ppcmds
 val pr_table : unit -> Pp.std_ppcmds
 
 
-val function_debug : bool ref 
+(* val function_debug : bool ref  *)
 val do_observe : unit -> bool
 
+(* To localize pb *)
+exception Building_graph of exn 
+exception Defining_principle of exn
+
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index d58dfba33..a24e5845b 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1074,7 +1074,7 @@ let rec rebuild_return_type rt =
     | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
 
 
-let build_inductive 
+let do_build_inductive 
     parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  
     returned_types 
     (rtl:rawconstr list) =
@@ -1226,7 +1226,7 @@ let build_inductive
   try 
     with_full_print (Options.silently (Command.build_mutual rel_inds)) true
   with 
-    | UserError(s,msg) ->
+    | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let msg = 		     
@@ -1235,7 +1235,7 @@ let build_inductive
 	    msg
 	in
 	observe (msg);
-	raise (UserError(s, msg))
+	raise e
     | e -> 
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
@@ -1245,4 +1245,13 @@ let build_inductive
 	    Cerrors.explain_exn e
 	in
  	observe msg;
-	raise (UserError("",msg))
+	raise e
+
+
+
+let build_inductive parametrize funnames funsargs returned_types rtl = 
+  try 
+    do_build_inductive  parametrize funnames funsargs returned_types rtl
+  with e -> raise (Building_graph e)
+      
+
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 9cd041236..33d1cacc7 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,5 +1,6 @@
 
 
+
 (*
   [build_inductive parametrize funnames funargs returned_types bodies] 
   constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments