diff options
-rw-r--r-- | interp/constrintern.ml | 13 | ||||
-rw-r--r-- | interp/modintern.ml | 36 | ||||
-rw-r--r-- | interp/modintern.mli | 3 | ||||
-rw-r--r-- | library/declaremods.ml | 23 | ||||
-rw-r--r-- | library/declaremods.mli | 12 | ||||
-rw-r--r-- | library/library.ml | 4 | ||||
-rw-r--r-- | tactics/auto.ml | 9 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 4 | ||||
-rw-r--r-- | tools/coqdoc/coqdoc.sty | 35 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 1 | ||||
-rw-r--r-- | tools/coqdoc/index.mll | 23 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 24 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 110 |
14 files changed, 206 insertions, 93 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b867bfd69..ac4639b43 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -161,9 +161,9 @@ let type_of_logical_kind = function | Method -> "meth") | IsAssumption a -> (match a with - | Definitional -> "def" - | Logical -> "prf" - | Conjectural -> "prf") + | Definitional -> "defax" + | Logical -> "prfax" + | Conjectural -> "prfax") | IsProof th -> (match th with | Theorem @@ -200,6 +200,10 @@ let remove_sections dir = (* Theorem/Lemma outside its outer section of definition *) dir +let dump_reference loc filepath modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) filepath modpath ident ty) + let add_glob_gen loc sp lib_dp ty = let mod_dp,id = repr_path sp in let mod_dp = remove_sections mod_dp in @@ -207,8 +211,7 @@ let add_glob_gen loc sp lib_dp ty = let filepath = string_of_dirpath lib_dp in let modpath = string_of_dirpath mod_dp_trunc in let ident = string_of_id id in - dump_string (Printf.sprintf "R%d %s %s %s %s\n" - (fst (unloc loc)) filepath modpath ident ty) + dump_reference loc filepath modpath ident ty let add_glob loc ref = let sp = Nametab.sp_of_global ref in diff --git a/interp/modintern.ml b/interp/modintern.ml index 68978080b..cd55ec74d 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -60,19 +60,51 @@ let lookup_qualid (modtype:bool) qid = *) + +let split_modpath mp = + let rec aux = function + | MPfile dp -> dp, [] + | MPbound mbid -> + Lib.library_dp (), [id_of_mbid mbid] + | MPself msid -> Lib.library_dp (), [id_of_msid msid] + | MPdot (mp,l) -> let (mp', lab) = aux mp in + (mp', id_of_label l :: lab) + in + let (mp, l) = aux mp in + mp, l + +let dump_moddef loc mp ty = + if !Flags.dump then + let (dp, l) = split_modpath mp in + let fp = string_of_dirpath dp in + let mp = string_of_dirpath (make_dirpath l) in + Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp) + +let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl + +let dump_modref loc mp ty = + if !Flags.dump then + let (dp, l) = split_modpath mp in + let fp = string_of_dirpath dp in + let mp = string_of_dirpath (make_dirpath (drop_last l)) in + Flags.dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) fp mp "<>" ty) + (* Search for the head of [qid] in [binders]. If found, returns the module_path/kernel_name created from the dirpath and the basename. Searches Nametab otherwise. *) let lookup_module (loc,qid) = try - Nametab.locate_module qid + let mp = Nametab.locate_module qid in + dump_modref loc mp "modtype"; mp with | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) let lookup_modtype (loc,qid) = try - Nametab.locate_modtype qid + let mp = Nametab.locate_modtype qid in + dump_modref loc mp "mod"; mp with | Not_found -> Modops.error_not_a_modtype_loc loc (string_of_qualid qid) diff --git a/interp/modintern.mli b/interp/modintern.mli index 1f27e3c18..c14b6481e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -26,3 +26,6 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry val lookup_module : qualid located -> module_path + +val dump_moddef : loc -> module_path -> string -> unit +val dump_modref : loc -> module_path -> string -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index 0bb74f74a..bb6d947c5 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -663,7 +663,7 @@ let start_module interp_modtype export id args res_o = openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_module id = @@ -717,7 +717,8 @@ let end_module id = if mp_of_kn (snd newoname) <> mp then anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state () (* to prevent recaching *) + Lib.add_frozen_state () (* to prevent recaching *); + mp @@ -819,7 +820,7 @@ let start_modtype interp_modtype id args = openmodtype_info := mbids; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state () + Lib.add_frozen_state (); mp let end_modtype id = @@ -843,14 +844,15 @@ let end_modtype id = anomaly "Kernel and Library names do not match"; - Lib.add_frozen_state ()(* to prevent recaching *) + Lib.add_frozen_state ()(* to prevent recaching *); + ln let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in try - let _ = Global.start_modtype id in + let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let base_mty = interp_modtype (Global.env()) mty in @@ -865,7 +867,8 @@ let declare_modtype interp_modtype id args mty = (* and declare the module type as a whole *) Summary.unfreeze_summaries fs; - ignore (add_leaf id (in_modtype (Some entry, substobjs))) + ignore (add_leaf id (in_modtype (Some entry, substobjs))); + mmp with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e @@ -1017,7 +1020,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let fs = Summary.freeze_summaries () in try - let _ = Global.start_module id in + let mmp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let mty_entry_o, mty_sub_o = match mty_o with @@ -1073,7 +1076,8 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = | _ -> None in ignore (add_leaf id - (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) + (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))); + mmp | _ -> let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in let (sub,mbids,msid,objs) = substobjs in @@ -1082,7 +1086,8 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let substituted = subst_substobjs dir mp substobjs in ignore (add_leaf id - (in_module (Some (entry, mty_sub_o), substobjs, substituted))) + (in_module (Some (entry, mty_sub_o), substobjs, substituted))); + mmp with e -> (* Something wrong: undo the whole process *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 717fddf79..1f7f6ada0 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -40,25 +40,25 @@ val declare_module : (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> - 'modexpr option -> unit + 'modexpr option -> module_path val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> - ('modtype * bool) option -> unit + ('modtype * bool) option -> module_path -val end_module : identifier -> unit +val end_module : identifier -> module_path (*s Module types *) val declare_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit + identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path val start_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> unit + identifier -> (identifier located list * 'modtype) list -> module_path -val end_modtype : identifier -> unit +val end_modtype : identifier -> module_path (*s Objects of a module. They come in two lists: the substitutive ones diff --git a/library/library.ml b/library/library.ml index e53c0cd1a..c014865fe 100644 --- a/library/library.ml +++ b/library/library.ml @@ -536,6 +536,10 @@ let require_library qidl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); + if !Flags.dump then List.iter2 (fun (loc, _) dp -> + Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (unloc loc)) (string_of_dirpath dp) "lib")) + qidl modrefl; if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () diff --git a/tactics/auto.ml b/tactics/auto.ml index e9424ed0c..e41bebea1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -432,16 +432,17 @@ let add_hints local dbnames0 h = add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> let f r = - let r = Syntax_def.global_with_alias r in - let r' = match r with + let gr = Syntax_def.global_with_alias r in + let r' = match gr with | ConstRef c -> EvalConstRef c | VarRef c -> EvalVarRef c | _ -> errorlabstrm "evalref_of_ref" - (str "Cannot coerce" ++ spc () ++ pr_global r ++ spc () ++ + (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference") in - (r,r') in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> let add_one qid = diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index cd38f318c..6885d0b29 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -336,7 +336,7 @@ Proof. firstorder. Qed. (** [R] is Reflexive, hence we can build the needed proof. *) -Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) : +Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] : Morphism R' (m x). Proof. simpl_relation. Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index d22398166..c5a8f3d30 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]]. Existing Instance setoid_morphism. Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) := - Reflexive_partial_app_morphism x. + Reflexive_partial_app_morphism. Existing Instance setoid_partial_app_morphism. @@ -148,7 +148,7 @@ Ltac obligations_tactic ::= morphism_tac. using [iff_impl_id_morphism] if the proof is in [Prop] and [eq_arrow_id_morphism] if it is in Type. *) -Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. +Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) Basics.id. (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index ca3e08f7f..ca454d852 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -44,6 +44,13 @@ % macro for typesetting constant identifiers \newcommand{\coqdoccst}[1]{\textsf{#1}} +% macro for typesetting module identifiers +\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}} + +% macro for typesetting module constant identifiers (e.g. Parameters in +% module types) +\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}} + % macro for typesetting inductive type identifiers \newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}} @@ -62,13 +69,15 @@ \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } -\usepackage{hyperref} -\hypersetup{colorlinks=true,linkcolor=black} +\usepackage[pdftex]{hyperref} +\hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} +\usepackage[all]{hypcap} +\usepackage{xr} %\usepackage{color} %\usepackage{multind} %\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} -\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}} +\newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}} \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}} \newcommand{\coqdocvar}[1]{{\textit{#1}}} @@ -82,7 +91,6 @@ %\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} %\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} \newcommand{\coqvariable}[2]{\coqdocid{#2}} -\newcommand{\coqaxiom}[2]{\coqdocid{#2}} \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} @@ -113,6 +121,25 @@ \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} +\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}} + +%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}} + +\newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection + \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}} + +\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}} +\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}} + +\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}} + + %HEVEA\newcommand{\lnot}{\coqwkw{not}} %HEVEA\newcommand{\lor}{\coqwkw{or}} %HEVEA\newcommand{\land}{\&} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index ec04017c4..9831ca3cb 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -29,6 +29,7 @@ type entry_type = | TacticDefinition | Abbreviation | Notation + | Section val type_name : entry_type -> string diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 1fa7c2498..ab23f2210 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -36,6 +36,7 @@ type entry_type = | TacticDefinition | Abbreviation | Notation + | Section type index_entry = | Def of string * entry_type @@ -50,7 +51,13 @@ let table = Hashtbl.create 97 (** [table] is used to store references and definitions *) let full_ident sp id = - if sp <> "<>" then sp ^ "." ^ id else id + if sp <> "<>" then + if id <> "<>" then + sp ^ "." ^ id + else sp + else if id <> "<>" + then id + else "" let add_def loc ty sp id = Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) @@ -195,7 +202,8 @@ let type_name = function | TacticDefinition -> "tactic" | Abbreviation -> "abbreviation" | Notation -> "notation" - + | Section -> "section" + let all_entries () = let gl = ref [] in let add_g s m t = gl := (s,(m,t)) :: !gl in @@ -421,14 +429,15 @@ and module_refs = parse | "meth" -> Method | "inst" -> Instance | "var" -> Variable - | "ax" -> Axiom + | "defax" | "prfax" | "ax" -> Axiom | "syndef" -> Abbreviation | "not" -> Notation + | "lib" -> Library + | "mod" | "modtype" -> Module + | "tac" -> TacticDefinition + | "sec" -> Section | s -> raise (Invalid_argument ("type_of_string:" ^ s)) -(* | Library *) -(* | Module *) -(* | TacticDefinition *) - + let read_glob f = let c = open_in f in let cur_mod = ref "" in diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 5b68e94cc..009e4dd11 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -36,17 +36,17 @@ let is_keyword = "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; - "Resolve"; "Unfold"; "Immediate"; "Implicit"; "Import"; "Inductive"; + "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; "Unset"; "Variable"; "Variables"; "Notation"; "Reserved Notation"; "Tactic Notation"; - "Delimit"; "Bind"; "Open"; "Scope"; - "Boxed"; "Unboxed"; - "Arguments"; + "Delimit"; "Bind"; "Open"; "Scope"; + "Boxed"; "Unboxed"; "Inline"; + "Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Class"; "Instantiation"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; @@ -65,7 +65,8 @@ let is_tactic = "cut"; "assumption"; "exact"; "split"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; - "replace"; "setoid_replace"; "inversion"; "pattern"; + "replace"; "setoid_replace"; "inversion"; "inversion_clear"; + "pattern"; "intuition"; "congruence"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ] @@ -190,7 +191,9 @@ module Latex = struct let start_module () = if not !short then begin - printf "\\coqdocmodule{"; + printf "\\coqlibrary{"; + label_ident !current_module; + printf "}{"; raw_ident !current_module; printf "}\n\n" end @@ -231,13 +234,14 @@ module Latex = struct raw_ident s i*) - let ident_ref m fid typ s = + let ident_ref m fid typ s = + let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with | Local -> - printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}" + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" | Coqlib when !externals -> let _m = Filename.concat !coqlib m in - printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}" + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" | Coqlib | Unknown -> raw_ident s diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b63c59d93..2cea826a7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -273,6 +273,11 @@ let print_located_module r = str "No module is referred to by name ") ++ pr_qualid qid in msgnl msg +let global_with_alias r = + let gr = global_with_alias r in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + gr + (**********) (* Syntax *) @@ -309,6 +314,10 @@ let dump_definition (loc, id) sec s = Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) (string_of_dirpath (current_dirpath sec)) (string_of_id id)) +let dump_reference loc modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty) + let dump_constraint ((loc, n), _, _) sec ty = match n with | Name id -> dump_definition (loc, id) sec ty @@ -408,7 +417,7 @@ let vernac_import export refl = List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export id binders_ast mty_ast_o = +let vernac_declare_module export (loc, id) binders_ast mty_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -420,13 +429,15 @@ let vernac_declare_module export id binders_ast mty_ast_o = "Remove the \"Export\" and \"Import\" keywords from every functor " ^ "argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) None; + id binders_ast (Some mty_ast_o) None + in + Modintern.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = +let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -439,15 +450,17 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in - Declaremods.start_module Modintern.interp_modtype export - id binders_ast mty_ast_o; - if_verbose message - ("Interactive Module "^ string_of_id id ^" started") ; - List.iter - (fun (export,id) -> - Option.iter - (fun export -> vernac_import export [Ident (dummy_loc,id)]) export - ) argsexport + let mp = Declaremods.start_module Modintern.interp_modtype export + id binders_ast mty_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("Interactive Module "^ string_of_id id ^" started") ; + List.iter + (fun (export,id) -> + Option.iter + (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + ) argsexport | Some _ -> let binders_ast = List.map (fun (export,idl,ty) -> @@ -456,21 +469,24 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = " the definition is interactive. Remove the \"Export\" and " ^ "\"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o; - if_verbose message - ("Module "^ string_of_id id ^" is defined"); - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) - export - -let vernac_end_module export id = - Declaremods.end_module id; + id binders_ast mty_ast_o mexpr_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("Module "^ string_of_id id ^" is defined"); + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + export + +let vernac_end_module export (loc,id) = + let mp = Declaremods.end_module id in + Modintern.dump_modref loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined") ; Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_declare_module_type id binders_ast mty_ast_o = +let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; @@ -482,7 +498,8 @@ let vernac_declare_module_type id binders_ast mty_ast_o = (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in - Declaremods.start_modtype Modintern.interp_modtype id binders_ast; + let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter @@ -499,14 +516,16 @@ let vernac_declare_module_type id binders_ast mty_ast_o = " the definition is interactive. Remove the \"Export\" " ^ "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - Declaremods.declare_modtype Modintern.interp_modtype - id binders_ast base_mty; + let mp = Declaremods.declare_modtype Modintern.interp_modtype + id binders_ast base_mty in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_end_modtype id = - Declaremods.end_modtype id; +let vernac_end_modtype (loc,id) = + let mp = Declaremods.end_modtype id in + Modintern.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") @@ -544,20 +563,25 @@ let vernac_record struc binders sort nameopt cfs = (* Sections *) -let vernac_begin_section id = +let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); + if !Flags.dump then dump_definition lid true "sec"; Lib.open_section id -let vernac_end_section = Lib.close_section +let vernac_end_section (loc, id) = + if !Flags.dump then + dump_reference loc + (string_of_dirpath (current_dirpath true)) "<>" "sec"; + Lib.close_section id -let vernac_end_segment id = +let vernac_end_segment lid = check_no_pending_proofs (); let o = try Lib.what_is_opened () with Not_found -> error "There is nothing to end." in match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid + | _,Lib.OpenedModtype _ -> vernac_end_modtype lid + | _,Lib.OpenedSection _ -> vernac_end_section lid | _ -> anomaly "No more opened things" let vernac_require import _ qidl = @@ -732,7 +756,7 @@ let vernac_hints = Auto.add_hints let vernac_syntactic_definition lid = dump_definition lid false "syndef"; Command.syntax_definition (snd lid) - + let vernac_declare_implicits local r = function | Some imps -> Impargs.declare_manual_implicits local (global_with_alias r) false @@ -1263,18 +1287,18 @@ let interp c = match c with | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) - | VernacDeclareModule (export,(_,id),bl,mtyo) -> - vernac_declare_module export id bl mtyo - | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> - vernac_define_module export id bl mtyo mexpro - | VernacDeclareModuleType ((_,id),bl,mtyo) -> - vernac_declare_module_type id bl mtyo + | VernacDeclareModule (export,lid,bl,mtyo) -> + vernac_declare_module export lid bl mtyo + | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> + vernac_define_module export lid bl mtyo mexpro + | VernacDeclareModuleType (lid,bl,mtyo) -> + vernac_declare_module_type lid bl mtyo | VernacInclude (in_ast) -> vernac_include in_ast (* Gallina extensions *) - | VernacBeginSection (_,id) -> vernac_begin_section id + | VernacBeginSection lid -> vernac_begin_section lid - | VernacEndSegment (_,id) -> vernac_end_segment id + | VernacEndSegment lid -> vernac_end_segment lid | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl |