From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 25 Feb 2018 22:43:42 +0100 Subject: [located] Push inner locations in `reference` to a CAst.t node. The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. --- vernac/vernacentries.ml | 58 ++++++++++++++++++++++++------------------------- 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'vernac/vernacentries.ml') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b3eb13fb7..3dbe8b0c0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -185,28 +185,28 @@ let print_modules () = let print_module r = - let (loc,qid) = qualid_of_reference r in + let qid = qualid_of_reference r in try - let globdir = Nametab.locate_dir qid in + let globdir = Nametab.locate_dir qid.v in match globdir with DirModule { obj_dir; obj_mp; _ } -> Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v) let print_modtype r = - let (loc,qid) = qualid_of_reference r in + let qid = qualid_of_reference r in try - let kn = Nametab.locate_modtype qid in + let kn = Nametab.locate_modtype qid.v in Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try - let mp = Nametab.locate_module qid in + let mp = Nametab.locate_module qid.v in Printmod.print_module false mp with Not_found -> - user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -390,7 +390,7 @@ let err_notfound_library ?loc ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in try msg_found_library (Library.locate_qualified_library ~warn:false qid) with | Library.LibUnmappedDir -> err_unmapped_library ?loc qid @@ -398,13 +398,13 @@ let print_located_library r = let smart_global r = let gr = Smartlocate.smart_global r in - Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr; - gr + Dumpglob.add_glob ?loc:r.loc gr; + gr let dump_global r = try let gr = Smartlocate.smart_global r in - Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr + Dumpglob.add_glob ?loc:r.loc gr with e when CErrors.noncritical e -> () (**********) (* Syntax *) @@ -640,7 +640,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -679,7 +679,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); - Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export + Option.iter (fun export -> vernac_import export [make @@ Ident id]) export let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) @@ -704,7 +704,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (Loc.tag id)]) export + (fun export -> vernac_import export [make @@ Ident id]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -719,14 +719,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) + Option.iter (fun export -> vernac_import export [make @@ Ident id]) export let vernac_end_module export {loc;v=id} = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [Ident (Loc.tag ?loc id)]) export + Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then @@ -751,7 +751,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (Loc.tag id)]) export + (fun export -> vernac_import export [make ?loc @@ Ident id]) export ) argsexport | _ :: _ -> @@ -817,11 +817,11 @@ let vernac_require from import qidl = let root = match from with | None -> None | Some from -> - let (_, qid) = Libnames.qualid_of_reference from in - let (hd, tl) = Libnames.repr_qualid qid in + let qid = Libnames.qualid_of_reference from in + let (hd, tl) = Libnames.repr_qualid qid.v in Some (Libnames.add_dirpath_suffix hd tl) in - let locate (loc, qid) = + let locate {loc;v=qid} = try let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in @@ -832,7 +832,7 @@ let vernac_require from import qidl = in let modrefl = List.map locate qidl in if Dumpglob.dump () then - List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); + List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import (* Coercions and canonical structures *) @@ -1688,10 +1688,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = - match glnumopt,ref_or_by_not with - | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *) + match glnumopt, ref_or_by_not.v with + | None,AN {v=Ident id} -> (* goal number not given, catch any failure *) (try get_nth_goal 1,id with _ -> raise NoHyp) - | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) + | Some n,AN {v=Ident id} -> (* goal number given, catch if wong *) (try get_nth_goal n,id with Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" @@ -1774,7 +1774,7 @@ let vernac_print ~atts env sigma = | PrintStrategy r -> print_strategy r let global_module r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in try Nametab.full_name_module qid with Not_found -> user_err ?loc ~hdr:"global_module" @@ -1858,10 +1858,10 @@ let vernac_search ~atts s gopt r = Search.prioritize_search) pr_search let vernac_locate = function - | LocateAny (AN qid) -> print_located_qualid qid - | LocateTerm (AN qid) -> print_located_term qid - | LocateAny (ByNotation { CAst.v=(ntn, sc)}) (** TODO : handle Ltac notations *) - | LocateTerm (ByNotation { CAst.v=(ntn, sc)}) -> + | LocateAny {v=AN qid} -> print_located_qualid qid + | LocateTerm {v=AN qid} -> print_located_term qid + | LocateAny {v=ByNotation (ntn, sc)} (** TODO : handle Ltac notations *) + | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = Pfedit.get_current_context () in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc -- cgit v1.2.3