diff options
author | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-24 10:51:29 +0000 |
---|---|---|
committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-24 10:51:29 +0000 |
commit | a0726f4ae896bb668d4da4c96501686b25cd82cd (patch) | |
tree | 515ce8961dccff9f0362fc42d9c7a299802aea78 | |
parent | 90d7d595fd0b46f4c9766b747bd7f57428376e12 (diff) |
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
-rw-r--r-- | contrib/funind/functional_principles_types.ml | 5 | ||||
-rw-r--r-- | contrib/funind/indfun.ml | 63 | ||||
-rw-r--r-- | contrib/funind/indfun_common.ml | 41 | ||||
-rw-r--r-- | contrib/funind/indfun_common.mli | 6 | ||||
-rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 17 | ||||
-rw-r--r-- | contrib/funind/rawterm_to_relation.mli | 1 |
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 |