From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- parsing/argextend.ml4 | 2 +- parsing/egrammar.ml | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_xml.ml4 | 3 ++- parsing/prettyp.ml | 8 +++--- parsing/printer.ml | 65 +++++++++++++++++++++++++++++++++++++++++++++--- parsing/printer.mli | 11 ++++++++ parsing/printmod.ml | 59 +++++++++++++++++++++++++++++-------------- parsing/tacextend.ml4 | 4 +-- parsing/vernacextend.ml4 | 4 +-- 10 files changed, 126 insertions(+), 34 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 1888ef17..214a6b98 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -146,7 +146,7 @@ let possibly_empty_subentries loc (prods,act) = (* an exception rather than returning a value; *) (* declares loc because some code can refer to it; *) (* ensures loc is used to avoid "unused variable" warning *) - (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>) + (true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>) else (* Static optimisation *) (false, aux prods) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index c68ba137..12359776 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -365,4 +365,4 @@ let _ = let with_grammar_rule_protection f x = let fs = freeze () in try let a = f x in unfreeze fs; a - with e -> unfreeze fs; raise e + with reraise -> unfreeze fs; raise reraise diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d265729a..1609e541 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -126,7 +126,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let induction_arg_of_constr (c,lbind as clbind) = if lbind = NoBindings then try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) - with _ -> ElimOnConstr clbind + with e when Errors.noncritical e -> ElimOnConstr clbind else ElimOnConstr clbind let mkTacCase with_evar = function diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 9dd0e369..869674f4 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -104,7 +104,8 @@ let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) let get_xml_inductive_kn al = inductive_of_cdata (* uriType apparent synonym of uri *) - (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al) + (try get_xml_attr "uri" al + with e when Errors.noncritical e -> get_xml_attr "uriType" al) let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d3eb40d0..99e10908 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -273,7 +273,9 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids - (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> []) + (fun r -> + try List.hd (Arguments_renaming.arguments_names r) + with e when Errors.noncritical e -> []) ((<>) Anonymous) print_renames_list @@ -737,7 +739,7 @@ let print_coercions () = let index_of_class cl = try fst (class_info cl) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") @@ -747,7 +749,7 @@ let print_path_between cls clt = let p = try lookup_path_between_class (i,j) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") diff --git a/parsing/printer.ml b/parsing/printer.ml index 9f0cb00d..29ebe4fa 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -24,6 +24,7 @@ open Pfedit open Ppconstr open Constrextern open Tacexpr +open Declarations open Store.Field @@ -118,6 +119,63 @@ let pr_sort s = pr_glob_sort (extern_sort s) let _ = Termops.set_print_constr pr_lconstr_env + +(** Term printers resilient to [Nametab] errors *) + +(** When the nametab isn't up-to-date, the term printers above + could raise [Not_found] during [Nametab.shortest_qualid_of_global]. + In this case, we build here a fully-qualified name based upon + the kernel modpath and label of constants, and the idents in + the [mutual_inductive_body] for the inductives and constructors + (needs an environment for this). *) + +let id_of_global env = function + | ConstRef kn -> id_of_label (con_label kn) + | IndRef (kn,0) -> id_of_label (mind_label kn) + | IndRef (kn,i) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_typename + | ConstructRef ((kn,i),j) -> + (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1) + | VarRef v -> v + +let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp) + +let rec dirpath_of_mp = function + | MPfile sl -> sl + | MPbound uid -> make_dirpath [id_of_mbid uid] + | MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp) + +let dirpath_of_global = function + | ConstRef kn -> dirpath_of_mp (con_modpath kn) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + dirpath_of_mp (mind_modpath kn) + | VarRef _ -> empty_dirpath + +let qualid_of_global env r = + Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) + +let safe_gen f env c = + let orig_extern_ref = Constrextern.get_extern_reference () in + let extern_ref loc vars r = + try orig_extern_ref loc vars r + with e when Errors.noncritical e -> + Libnames.Qualid (loc, qualid_of_global env r) + in + Constrextern.set_extern_reference extern_ref; + try + let p = f env c in + Constrextern.set_extern_reference orig_extern_ref; + p + with e when Errors.noncritical e -> + Constrextern.set_extern_reference orig_extern_ref; + str "??" + +let safe_pr_lconstr_env = safe_gen pr_lconstr_env +let safe_pr_constr_env = safe_gen pr_constr_env +let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t +let safe_pr_constr t = safe_pr_constr_env (Global.env()) t + + (**********************************************************************) (* Global references *) @@ -389,7 +447,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = | None -> let exl = Evarutil.non_instantiated sigma in if exl = [] then - (str"No more subgoals." + (str"No more subgoals." ++ fnl () ++ emacs_print_dependent_evars sigma seeds) else let pei = pr_evars_int 1 exl in @@ -415,7 +473,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = v 0 ( int(List.length rest+1) ++ str" subgoals" ++ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () - ++ goals + ++ goals ++ fnl () ++ emacs_print_dependent_evars sigma seeds ) | g1::rest,a::l -> @@ -589,7 +647,7 @@ let pr_assumptionset env s = str (string_of_mp mp ^ "." ^ string_of_label lab) in let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ with _ -> mt () + try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in let (vars,axioms,opaque) = ContextObjectMap.fold (fun t typ r -> @@ -647,7 +705,6 @@ let pr_instance_gmap insts = (** Inductive declarations *) -open Declarations open Termops open Reduction open Inductive diff --git a/parsing/printer.mli b/parsing/printer.mli index a034f0ed..3abe90e7 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -31,6 +31,17 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +(** Same, but resilient to [Nametab] errors. Prints fully-qualified + names when [shortest_qualid_of_global] has failed. Prints "??" + in case of remaining issues (such as reference not in env). *) + +val safe_pr_lconstr_env : env -> constr -> std_ppcmds +val safe_pr_lconstr : constr -> std_ppcmds + +val safe_pr_constr_env : env -> constr -> std_ppcmds +val safe_pr_constr : constr -> std_ppcmds + + val pr_open_constr_env : env -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds diff --git a/parsing/printmod.ml b/parsing/printmod.ml index b4a8fdfd..b46cf42d 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -68,12 +68,17 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn +(** Each time we have to print a non-globally visible structure, + we place its elements in a fake fresh namespace. *) + +let mk_fake_top = + let r = ref 0 in + fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r)) + let nametab_register_dir mp = - let id = id_of_string "FAKETOP" in - let fp = Libnames.make_path empty_dirpath id in + let id = mk_fake_top () in let dir = make_dirpath [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))); - fp + Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -81,9 +86,10 @@ let nametab_register_dir mp = the user names. This works nonetheless since we search now [Nametab.the_globrevtab] modulo user name. *) -let nametab_register_body mp fp (l,body) = +let nametab_register_body mp dir (l,body) = let push id ref = - Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref + Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir))) + (make_path dir id) ref in match body with | SFBmodule _ -> () (* TODO *) @@ -99,6 +105,27 @@ let nametab_register_body mp fp (l,body) = mip.mind_consnames) mib.mind_packets +let nametab_register_module_body mp struc = + (* If [mp] is a globally visible module, we simply import it *) + try Declaremods.really_import_module mp + with Not_found -> + (* Otherwise we try to emulate an import by playing with nametab *) + nametab_register_dir mp; + List.iter (nametab_register_body mp empty_dirpath) struc + +let nametab_register_module_param mbid seb = + (* For algebraic seb, we use a Declaremods function that converts into mse *) + try Declaremods.process_module_seb_binding mbid seb + with e when Errors.noncritical e -> + (* Otherwise, for expanded structure, we try to play with the nametab *) + match seb with + | SEBstruct struc -> + let mp = MPbound mbid in + let dir = make_dirpath [id_of_mbid mbid] in + nametab_register_dir mp; + List.iter (nametab_register_body mp dir) struc + | _ -> () + let print_body is_impl env mp (l,body) = let name = str (string_of_label l) in hov 2 (match body with @@ -126,19 +153,11 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib - with _ -> + with e when Errors.noncritical e -> (if mib.mind_finite then str "Inductive " else str "CoInductive") ++ name) let print_struct is_impl env mp struc = - begin - (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.really_import_module mp - with _ -> - (* Otherwise we try to emulate an import by playing with nametab *) - let fp = nametab_register_dir mp in - List.iter (nametab_register_body mp fp) struc - end; prlist_with_sep spc (print_body is_impl env mp) struc let rec flatten_app mexpr l = match mexpr with @@ -156,7 +175,7 @@ let rec print_modtype env mp locals mty = let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ()); + nametab_register_module_param mbid seb1; hov 2 (str "Funsig" ++ spc () ++ str "(" ++ pr_id (id_of_mbid mbid) ++ str ":" ++ print_modtype env mp1 locals seb1 ++ @@ -164,6 +183,7 @@ let rec print_modtype env mp locals mty = | SEBstruct (sign) -> let env' = Option.map (Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp sign; hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -190,13 +210,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with (Modops.add_module (Modops.module_body_of_type mp' mty)) env in let typ = Option.default mty.typ_expr mty.typ_expr_alg in let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - (try Declaremods.process_module_seb_binding mbid typ with _ -> ()); + nametab_register_module_param mbid typ; hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ str ":" ++ print_modtype env mp' locals typ ++ str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr) | SEBstruct struc -> let env' = Option.map (Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp struc; hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -243,7 +264,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; print_module' (Some (Global.env ())) mp with_body me ++ fnl () - with _ -> + with e when Errors.noncritical e -> print_module' None mp with_body me ++ fnl () let print_modtype kn = @@ -254,5 +275,5 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_modtype' (Some (Global.env ())) kn mtb.typ_expr - with _ -> + with e when Errors.noncritical e -> print_modtype' None kn mtb.typ_expr)) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index dbc06856..77364180 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -188,11 +188,11 @@ let declare_tactic loc s cl = Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) $atomic_tactics$ - with e -> + with [ e when Errors.noncritical e -> Pp.msg_warning (Stream.iapp (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) - (Errors.print e)); + (Errors.print e)) ]; Egrammar.extend_tactic_grammar $se$ $gl$; List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> ]) diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 4f39019f..bcdf7cff 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -55,11 +55,11 @@ let declare_command loc s nt cl = declare_str_items loc [ <:str_item< do { try Vernacinterp.vinterp_add $se$ $funcl$ - with e -> + with [ e when Errors.noncritical e -> Pp.msg_warning (Stream.iapp (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)); + (Errors.print e)) ]; Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$ } >> ] -- cgit v1.2.3