From e82a571c3b5fd79a79b67cf30714f2e54c4c8371 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 21 Oct 2008 14:06:14 +0000 Subject: warning message when a qualid to extract can be both a module or a cst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11485 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/common.ml | 8 ++--- contrib/extraction/extract_env.ml | 62 +++++++++++++++++++++------------------ contrib/extraction/table.ml | 56 +++++++++++++++++++++++------------ contrib/extraction/table.mli | 6 ++-- 4 files changed, 77 insertions(+), 55 deletions(-) diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 2be509954..9a06ed49e 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -255,7 +255,7 @@ let rec record_contents_fstlev struc = let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in let addfix mp r = - add_ext_mpmem Term mp (modular_rename false (id_of_global r)) + add_ext_mpmem Term mp (modular_rename false (safe_id_of_global r)) in let f mp = function | (l,SEdecl (Dind (_,ind))) -> @@ -327,7 +327,7 @@ let create_modular_renamings struc = let add upper r = let mp = modpath_of_r r in let l = mp_create_renaming mp in - let s = modular_rename upper (id_of_global r) in + let s = modular_rename upper (safe_id_of_global r) in add_global_ids (id_of_string s); add_renaming r (s::l); begin try @@ -378,8 +378,8 @@ let create_mono_renamings struc = let mycase = if upper then uppercase_id else lowercase_id in let id = if l = [""] then - next_ident_away (mycase (id_of_global r)) (global_ids_list ()) - else id_of_string (modular_rename upper (id_of_global r)) + next_ident_away (mycase (safe_id_of_global r)) (global_ids_list ()) + else id_of_string (modular_rename upper (safe_id_of_global r)) in add_global_ids id; add_renaming r ((string_of_id id)::l) diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index a1c3331c6..8eb7a6b4a 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -427,51 +427,55 @@ let init modular = reset (); if modular && lang () = Scheme then error_scheme () +(* From a list of [reference], let's retrieve whether they correspond + to modules or [global_reference]. Warn the user if both is possible. *) + +let rec locate_ref = function + | [] -> [],[] + | r::l -> + let q = snd (qualid_of_reference r) in + let mpo = try Some (Nametab.locate_module q) with Not_found -> None + and ro = try Some (Nametab.locate q) with Not_found -> None in + match mpo, ro with + | None, None -> Nametab.error_global_not_found q + | None, Some r -> let refs,mps = locate_ref l in r::refs,mps + | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps + | Some mp, Some r -> + warning_both_mod_and_cst q mp r; + let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when extracting to a file with the command: \verb!Extraction "file"! [qualid1] ... [qualidn]. *) -let full_extraction f qualids = +let full_extr f (refs,mps) = init false; - let rec find = function - | [] -> [],[] - | q::l -> - let refs,mps = find l in - try - let mp = Nametab.locate_module (snd (qualid_of_reference q)) in - if is_modfile mp then error_MPfile_as_mod mp true; - refs,(mp::mps) - with Not_found -> (Nametab.global q)::refs, mps - in - let refs,mps = find qualids in + List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps; let struc = optimize_struct refs (mono_environment refs mps) in warning_axioms (); print_structure_to_file (mono_filename f) struc; reset () +let full_extraction f lr = full_extr f (locate_ref lr) (*s Simple extraction in the Coq toplevel. The vernacular command is \verb!Extraction! [qualid]. *) -let simple_extraction qid = - init false; - try - let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in - if is_modfile mp then error_MPfile_as_mod mp true; - full_extraction None [qid] - with Not_found -> - let r = Nametab.global qid in - if is_custom r then - msgnl (str "User defined extraction:" ++ spc () ++ - str (find_custom r) ++ fnl ()) - else - let struc = optimize_struct [r] (mono_environment [r] []) in - let d = get_decl_in_structure r struc in - warning_axioms (); - print_one_decl struc (modpath_of_r r) d; - reset () +let simple_extraction r = match locate_ref [r] with + | ([], [mp]) as p -> full_extr None p + | [r],[] -> + init false; + if is_custom r then + msgnl (str "User defined extraction:" ++ spc () ++ + str (find_custom r) ++ fnl ()) + else + let struc = optimize_struct [r] (mono_environment [r] []) in + let d = get_decl_in_structure r struc in + warning_axioms (); + print_one_decl struc (modpath_of_r r) d; + reset () + | _ -> assert false (*s (Recursive) Extraction of a library. The vernacular command is diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 5bfc3688f..289074b62 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -197,27 +197,33 @@ let reset_tables () = WARNING: for inductive objects, an extract_inductive must have been done before. *) -let id_of_global = function +let safe_id_of_global = function | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false -let pr_global r = - try Printer.pr_global r - with _ -> pr_id (id_of_global r) +let safe_pr_global r = + try Printer.pr_global r + with _ -> pr_id (safe_id_of_global r) (* idem, but with qualification, and only for constants. *) -let pr_long_global r = - try Printer.pr_global r +let safe_pr_long_global r = + try Printer.pr_global r with _ -> match r with - | ConstRef kn -> - let mp,_,l = repr_con kn in + | ConstRef kn -> + let mp,_,l = repr_con kn in str ((string_of_mp mp)^"."^(string_of_label l)) | _ -> assert false +let pr_long_mp mp = + let lid = repr_dirpath (Nametab.dir_of_mp mp) in + str (String.concat "." (List.map string_of_id (List.rev lid))) + +let pr_long_global ref = pr_sp (Nametab.sp_of_global ref) + (*S Warning and Error messages. *) let err s = errorlabstrm "Extraction" s @@ -229,7 +235,7 @@ let warning_axioms () = let s = if List.length info_axioms = 1 then "axiom" else "axioms" in msg_warning (str ("The following "^s^" must be realized in the extracted code:") - ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) ++ str "." ++ fnl ()) end; let log_axioms = Refset.elements !log_axioms in @@ -239,15 +245,27 @@ let warning_axioms () = in msg_warning (str ("The following logical "^s^" encountered:") ++ - hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++ + hov 1 + (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") + ++ str "Having invalid logical axiom in the environment when extracting" ++ spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ fnl ()) end +let warning_both_mod_and_cst q mp r = + msg_warning + (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ + str "do you mean module " ++ + pr_long_mp mp ++ + str " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + str "First choice is assumed, for the second one please use " ++ + str "fully qualified name." ++ fnl ()) + let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ - pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ str " type variable(s).") let check_inside_module () = @@ -265,10 +283,10 @@ let check_inside_section () = str "Close it and try again.") let error_constant r = - err (pr_global r ++ str " is not a constant.") + err (safe_pr_global r ++ str " is not a constant.") let error_inductive r = - err (pr_global r ++ spc () ++ str "is not an inductive type.") + err (safe_pr_global r ++ spc () ++ str "is not an inductive type.") let error_nb_cons () = err (str "Not the right number of constructors.") @@ -284,7 +302,7 @@ let error_scheme () = err (str "No Scheme modular extraction available yet.") let error_not_visible r = - err (pr_global r ++ str " is not directly visible.\n" ++ + err (safe_pr_global r ++ str " is not directly visible.\n" ++ str "For example, it may be inside an applied functor." ++ str "Use Recursive Extraction to get the whole environment.") @@ -296,9 +314,9 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let error_record r = - err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++ - str "To help extraction, please use an explicit name.") +let error_record r = + err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++ + fnl () ++ str "To help extraction, please use an explicit name.") let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> if not (Library.library_is_loaded dp) then @@ -481,11 +499,11 @@ let print_extraction_inline () = (str "Extraction Inline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++ + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++ str "Extraction NoInline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ())) + (p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ())) (* Reset part *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index c65c2edfe..628e035bb 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -13,13 +13,13 @@ open Libnames open Miniml open Declarations -val id_of_global : global_reference -> identifier -val pr_long_global : global_reference -> Pp.std_ppcmds - +val safe_id_of_global : global_reference -> identifier (*s Warning and Error messages. *) val warning_axioms : unit -> unit +val warning_both_mod_and_cst : + qualid -> module_path -> global_reference -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a -- cgit v1.2.3