diff options
-rw-r--r-- | Makefile.common | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.ml | 2 | ||||
-rw-r--r-- | interp/constrintern.ml | 164 | ||||
-rw-r--r-- | interp/constrintern.mli | 7 | ||||
-rw-r--r-- | interp/dumpglob.ml | 220 | ||||
-rw-r--r-- | interp/modintern.ml | 32 | ||||
-rw-r--r-- | interp/modintern.mli | 3 | ||||
-rw-r--r-- | kernel/names.ml | 4 | ||||
-rw-r--r-- | kernel/names.mli | 3 | ||||
-rw-r--r-- | lib/flags.ml | 17 | ||||
-rw-r--r-- | lib/flags.mli | 3 | ||||
-rw-r--r-- | library/lib.ml | 113 | ||||
-rw-r--r-- | library/lib.mli | 127 | ||||
-rw-r--r-- | library/library.ml | 32 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/index.mll | 13 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 18 | ||||
-rw-r--r-- | tools/coqdoc/pretty.mll | 2 | ||||
-rw-r--r-- | toplevel/classes.ml | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
-rw-r--r-- | toplevel/vernac.ml | 13 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 170 |
23 files changed, 491 insertions, 471 deletions
diff --git a/Makefile.common b/Makefile.common index f31b60a58..c0584b29c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -172,7 +172,7 @@ PRETYPING:=\ INTERP:=\ parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \ - interp/notation.cmo \ + interp/notation.cmo interp/dumpglob.cmo \ interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \ interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ @@ -509,7 +509,7 @@ PRINTERSCMO:=\ pretyping/unification.cmo pretyping/cases.cmo \ pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \ parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \ - interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo \ + interp/topconstr.cmo interp/notation.cmo interp/dumpglob.cmo interp/reserve.cmo \ library/impargs.cmo interp/constrextern.cmo \ interp/syntax_def.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \ proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 5ac428f6c..71aa7e99e 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -107,7 +107,8 @@ let declare_assumption env isevars idl is_coe k bl c nl = (str "Cannot declare an assumption while in proof editing mode.") let dump_definition (loc, id) s = - Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id)) + Dumpglob.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) + (string_of_id id)) let dump_constraint ty ((loc, n), _, _) = match n with diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index aa16bd4bb..26cb416ac 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -165,7 +165,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class try let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); + Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) ([], props) k.cl_props diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1ddcac276..54abacaf6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -124,150 +124,6 @@ let error_inductive_parameter_not_implicit loc = "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) (**********************************************************************) -(* Dump of globalization (to be used by coqdoc) *) -let token_number = ref 0 -let last_pos = ref 0 - -type coqdoc_state = Lexer.location_table * int * int - -let coqdoc_freeze () = - let lt = Lexer.location_table() in - let state = (lt,!token_number,!last_pos) in - token_number := 0; - last_pos := 0; - state - -let coqdoc_unfreeze (lt,tn,lp) = - Lexer.restore_location_table lt; - token_number := tn; - last_pos := lp - -open Decl_kinds - -let type_of_logical_kind = function - | IsDefinition def -> - (match def with - | Definition -> "def" - | Coercion -> "coe" - | SubClass -> "subclass" - | CanonicalStructure -> "canonstruc" - | Example -> "ex" - | Fixpoint -> "def" - | CoFixpoint -> "def" - | Scheme -> "scheme" - | StructureComponent -> "proj" - | IdentityCoercion -> "coe" - | Instance -> "inst" - | Method -> "meth") - | IsAssumption a -> - (match a with - | Definitional -> "defax" - | Logical -> "prfax" - | Conjectural -> "prfax") - | IsProof th -> - (match th with - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary -> "thm") - -let type_of_global_ref gr = - if Typeclasses.is_class gr then - "class" - else - match gr with - | ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) - | VarRef v -> - "var" ^ type_of_logical_kind (Decls.variable_kind v) - | IndRef ind -> - let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record then - if mib.Declarations.mind_finite then "rec" - else "corec" - else if mib.Declarations.mind_finite then "ind" - else "coind" - | ConstructRef _ -> "constr" - -let remove_sections dir = - if is_dirpath_prefix_of dir (Lib.cwd ()) then - (* Not yet (fully) discharged *) - extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) - else - (* 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 - let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in - 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_reference loc filepath modpath ident ty - -let add_glob loc ref = - let sp = Nametab.sp_of_global ref in - let lib_dp = Lib.library_part ref in - let ty = type_of_global_ref ref in - add_glob_gen loc sp lib_dp ty - -let add_glob loc ref = - if !Flags.dump && loc <> dummy_loc then add_glob loc ref - -let mp_of_kn kn = - let mp,sec,l = repr_kn kn in - MPdot (mp,l) - -let add_glob_kn loc kn = - let sp = Nametab.sp_of_syntactic_definition kn in - let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in - add_glob_gen loc sp lib_dp "syndef" - -let add_glob_kn loc ref = - if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref - -let add_local loc id = () -(* let mod_dp,id = repr_path sp in *) -(* let mod_dp = remove_sections mod_dp in *) -(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) -(* 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) *) - -let dump_binding loc id = () - -let loc_of_notation f loc args ntn = - if args=[] or ntn.[0] <> '_' then fst (unloc loc) - else snd (unloc (f (List.hd args))) - -let ntn_loc = loc_of_notation constr_loc -let patntn_loc = loc_of_notation cases_pattern_expr_loc - -let dump_notation_location pos ((path,df),sc) = - let rec next growing = - let loc = Lexer.location_function !token_number in - let (bp,_) = unloc loc in - if growing then if bp >= pos then loc else (incr token_number;next true) - else if bp = pos then loc - else if bp > pos then (decr token_number;next false) - else (incr token_number;next true) in - let loc = next (pos >= !last_pos) in - last_pos := pos; - let path = string_of_dirpath path in - let _sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df) - -(**********************************************************************) (* Contracting "{ _ }" in notations *) let rec wildcards ntn n = @@ -394,9 +250,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = let ntn,args = contract_notation ntn args in let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !dump then dump_notation_location (ntn_loc loc args ntn) df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_aconstr_in_rawconstr loc intern subst ([],env) c + if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.ntn_loc loc args ntn) df; + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in + subst_aconstr_in_rawconstr loc intern subst ([],env) c let set_type_scope (ids,tmp_scope,scopes) = (ids,Some Notation.type_scope,scopes) @@ -476,10 +332,10 @@ let check_no_explicitation l = let intern_qualid loc qid intern env args = try match Nametab.extended_locate qid with | TrueGlobal ref -> - add_glob loc ref; + Dumpglob.add_glob loc ref; RRef (loc, ref), args | SyntacticDef sp -> - add_glob_kn loc sp; + Dumpglob.add_glob_kn loc sp; let (ids,c) = Syntax_def.search_syntactic_definition loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; @@ -709,7 +565,7 @@ let find_constructor ref f aliases pats scopes = let v = Environ.constant_value (Global.env()) cst in unf (global_of_constr v) | ConstructRef cstr -> - add_glob loc r; + Dumpglob.add_glob loc r; cstr, [], pats | _ -> raise Not_found in unf r @@ -760,7 +616,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !dump then dump_notation_location (patntn_loc loc args ntn) df; + if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.patntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes c @@ -769,7 +625,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = let a = alias_of aliases in let (c,df) = Notation.interp_prim_token_cases_pattern loc p a (tmp_scope,scopes) in - if !dump then dump_notation_location (fst (unloc loc)) df; + if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> intern_pat (find_delimiters_scope loc key::scopes) aliases None e @@ -829,7 +685,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function | Anonymous -> env | Name id -> check_hidden_implicit_parameters id lvar; - dump_binding loc id; + Dumpglob.dump_binding loc id; (Idset.add id ids,tmpsc,scopes) let intern_typeclass_binders intern_type lvar env bl = @@ -1029,7 +885,7 @@ let internalise sigma globalenv env allow_patvar lvar c = intern_notation intern env loc ntn args | CPrim (loc, p) -> let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in - if !dump then dump_notation_location (fst (unloc loc)) df; + if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; c | CDelimiters (loc, key, e) -> intern (ids,None,find_delimiters_scope loc key::scopes) e diff --git a/interp/constrintern.mli b/interp/constrintern.mli index d3b8da8f9..27a46daf1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -144,10 +144,3 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr -> (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b - -(* Coqdoc utility functions *) -type coqdoc_state -val coqdoc_freeze : unit -> coqdoc_state -val coqdoc_unfreeze : coqdoc_state -> unit - -val add_glob : Util.loc -> global_reference -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml new file mode 100644 index 000000000..8cc6371f5 --- /dev/null +++ b/interp/dumpglob.ml @@ -0,0 +1,220 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + + +let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl + +(* Dump of globalization (to be used by coqdoc) *) + +let glob_file = ref Pervasives.stdout + +let open_glob_file f = + glob_file := Pervasives.open_out(f ^ ".glob") + +let close_glob_file () = + Pervasives.close_out !glob_file + +let dump_string s = + Pervasives.output_string !glob_file s + + + +(**********************************************************************) +(* Dump of globalization (to be used by coqdoc) *) +let token_number = ref 0 +let last_pos = ref 0 + +type coqdoc_state = Lexer.location_table * int * int + +let coqdoc_freeze () = + let lt = Lexer.location_table() in + let state = (lt,!token_number,!last_pos) in + token_number := 0; + last_pos := 0; + state + +let coqdoc_unfreeze (lt,tn,lp) = + Lexer.restore_location_table lt; + token_number := tn; + last_pos := lp + +open Decl_kinds + +let type_of_logical_kind = function + | IsDefinition def -> + (match def with + | Definition -> "def" + | Coercion -> "coe" + | SubClass -> "subclass" + | CanonicalStructure -> "canonstruc" + | Example -> "ex" + | Fixpoint -> "def" + | CoFixpoint -> "def" + | Scheme -> "scheme" + | StructureComponent -> "proj" + | IdentityCoercion -> "coe" + | Instance -> "inst" + | Method -> "meth") + | IsAssumption a -> + (match a with + | Definitional -> "defax" + | Logical -> "prfax" + | Conjectural -> "prfax") + | IsProof th -> + (match th with + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -> "thm") + +let type_of_global_ref gr = + if Typeclasses.is_class gr then + "class" + else + match gr with + | Libnames.ConstRef cst -> + type_of_logical_kind (Decls.constant_kind cst) + | Libnames.VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | Libnames.IndRef ind -> + let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in + if mib.Declarations.mind_record then + if mib.Declarations.mind_finite then "rec" + else "corec" + else if mib.Declarations.mind_finite then "ind" + else "coind" + | Libnames.ConstructRef _ -> "constr" + +let remove_sections dir = + if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + (* Not yet (fully) discharged *) + Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + else + (* Theorem/Lemma outside its outer section of definition *) + dir + +let dump_ref loc filepath modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) filepath modpath ident ty) + +let add_glob_gen loc sp lib_dp ty = + let mod_dp,id = Libnames.repr_path sp in + let mod_dp = remove_sections mod_dp in + let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in + let filepath = Names.string_of_dirpath lib_dp in + let modpath = Names.string_of_dirpath mod_dp_trunc in + let ident = Names.string_of_id id in + dump_ref loc filepath modpath ident ty + +let add_glob loc ref = + let sp = Nametab.sp_of_global ref in + let lib_dp = Lib.library_part ref in + let ty = type_of_global_ref ref in + add_glob_gen loc sp lib_dp ty + +let add_glob loc ref = + if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref + +let mp_of_kn kn = + let mp,sec,l = Names.repr_kn kn in + Names.MPdot (mp,l) + +let add_glob_kn loc kn = + let sp = Nametab.sp_of_syntactic_definition kn in + let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in + add_glob_gen loc sp lib_dp "syndef" + +let add_glob_kn loc ref = + if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref + +let add_local loc id = () +(* let mod_dp,id = repr_path sp in *) +(* let mod_dp = remove_sections mod_dp in *) +(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) +(* 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) *) + +let dump_binding loc id = () + +(* BEGIN obsolete *) + +let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented") + +let dump_def loc ref = + let curr_mp, _ = Lib.current_prefix() in + let lib_dp, curr_dp = Lib.split_mp curr_mp in + let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp curr_dp in + + let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in + let filepath = Names.string_of_dirpath lib_dp in + dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname) + +(* END obsolete *) + +let dump_definition (loc, id) sec s = + dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) + (Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id)) + +let dump_reference loc modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty) + +let dump_constraint ((loc, n), _, _) sec ty = + match n with + | Names.Name id -> dump_definition (loc, id) sec ty + | Names.Anonymous -> () + +let dump_modref loc mp ty = + if !Flags.dump then + let (dp, l) = Lib.split_modpath mp in + let fp = Names.string_of_dirpath dp in + let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) fp mp "<>" ty) + +let dump_moddef loc mp ty = + if !Flags.dump then + let (dp, l) = Lib.split_modpath mp in + let mp = Names.string_of_dirpath (Names.make_dirpath l) in + dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp) + +let dump_libref loc dp ty = + if !Flags.dump then + dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) + +let loc_of_notation f loc args ntn = + if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc) + else snd (Util.unloc (f (List.hd args))) + +let ntn_loc = loc_of_notation Topconstr.constr_loc +let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc + +let dump_notation_location pos ((path,df),sc) = + let rec next growing = + let loc = Lexer.location_function !token_number in + let (bp,_) = Util.unloc loc in + if growing then if bp >= pos then loc else (incr token_number; next true) + else if bp = pos then loc + else if bp > pos then (decr token_number;next false) + else (incr token_number;next true) in + let loc = next (pos >= !last_pos) in + last_pos := pos; + let path = Names.string_of_dirpath path in + let _sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df) + + diff --git a/interp/modintern.ml b/interp/modintern.ml index 0af11bad9..3482dd3a0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,34 +61,6 @@ 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 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. @@ -96,14 +68,14 @@ let dump_modref loc mp ty = let lookup_module (loc,qid) = try let mp = Nametab.locate_module qid in - dump_modref loc mp "modtype"; mp + Dumpglob.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 let mp = Nametab.locate_modtype qid in - dump_modref loc mp "mod"; mp + Dumpglob.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 c14b6481e..1f27e3c18 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -26,6 +26,3 @@ 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/kernel/names.ml b/kernel/names.ml index 975390cb9..3d80ad23e 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -86,6 +86,7 @@ type label = string type mod_self_id = uniq_ident let make_msid = make_uid +let repr_msid (n, id, dp) = (n, id, dp) let debug_string_of_msid = debug_string_of_uid let refresh_msid (_,s,dir) = make_uid dir s let string_of_msid = string_of_uid @@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s type mod_bound_id = uniq_ident let make_mbid = make_uid +let repr_mbid (n, id, dp) = (n, id, dp) let debug_string_of_mbid = debug_string_of_uid let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s @@ -116,7 +118,7 @@ type module_path = | MPdot of module_path * label let rec string_of_mp = function - | MPfile sl -> string_of_dirpath sl + | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")" | MPbound uid -> string_of_uid uid | MPself uid -> string_of_uid uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l diff --git a/kernel/names.mli b/kernel/names.mli index b19f93e2d..177768cf4 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -48,6 +48,7 @@ type mod_self_id (* The first argument is a file name - to prevent conflict between different files *) val make_msid : dir_path -> string -> mod_self_id +val repr_msid : mod_self_id -> int * string * dir_path val id_of_msid : mod_self_id -> identifier val label_of_msid : mod_self_id -> label val refresh_msid : mod_self_id -> mod_self_id @@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id +val repr_mbid : mod_bound_id -> int * string * dir_path val id_of_mbid : mod_bound_id -> identifier val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string @@ -82,7 +84,6 @@ type module_path = | MPdot of module_path * label (*i | MPapply of module_path * module_path in the future (maybe) i*) - val string_of_mp : module_path -> string module MPset : Set.S with type elt = module_path diff --git a/lib/flags.ml b/lib/flags.ml index 68e287f69..f2ab87b4b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -86,23 +86,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set let noglob = ref false let dump = ref false -let dump_file = ref "" -let dump_into_file f = dump := true; dump_file := f - -let dump_buffer = Buffer.create 8192 - -let dump_string = Buffer.add_string dump_buffer - -let dump_it () = - if !dump then begin - let mode = [Open_wronly; Open_creat] in - let c = open_out_gen mode 0o666 !dump_file in - output_string c (Buffer.contents dump_buffer); - Buffer.clear dump_buffer; - close_out c - end - -let _ = at_exit dump_it (* Flags.for the virtual machine *) diff --git a/lib/flags.mli b/lib/flags.mli index 08f9a279d..4cab30381 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -61,9 +61,6 @@ val is_unsafe : string -> bool val noglob : bool ref val dump : bool ref -val dump_into_file : string -> unit -val dump_string : string -> unit -val dump_it : unit -> unit (* Options for the virtual machine *) diff --git a/library/lib.ml b/library/lib.ml index 5e22c4d22..bb0ad74ca 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -10,7 +10,6 @@ open Pp open Util -open Names open Libnames open Nameops open Libobject @@ -33,7 +32,7 @@ and library_entry = object_name * node and library_segment = library_entry list -type lib_objects = (identifier * obj) list +type lib_objects = (Names.identifier * obj) list let iter_objects f i prefix = List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) @@ -53,7 +52,7 @@ let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc | ((sp,kn as oname),Leaf o) :: stk -> - let id = id_of_label (label kn) in + let id = Names.id_of_label (Names.label kn) in (match classify_object (oname,o) with | Dispose -> clean acc stk | Keep o' -> @@ -85,7 +84,7 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = default_library,(initial_path,empty_dirpath) +let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath) let lib_stk = ref ([] : library_segment) @@ -98,8 +97,21 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix +let sections_depth () = + List.length (Names.repr_dirpath (snd (snd !path_prefix))) + +let sections_are_opened () = + match Names.repr_dirpath (snd (snd !path_prefix)) with + [] -> false + | _ -> true + let cwd () = fst !path_prefix +let current_dirpath sec = + Libnames.drop_dirpath_prefix (library_dp ()) + (if sec then cwd () + else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ())) + let make_path id = Libnames.make_path (cwd ()) id let path_of_include () = @@ -112,25 +124,15 @@ let current_prefix () = snd !path_prefix let make_kn id = let mp,dir = current_prefix () in - Names.make_kn mp dir (label_of_id id) + Names.make_kn mp dir (Names.label_of_id id) let make_con id = let mp,dir = current_prefix () in - Names.make_con mp dir (label_of_id id) + Names.make_con mp dir (Names.label_of_id id) let make_oname id = make_path id, make_kn id - -let sections_depth () = - List.length (repr_dirpath (snd (snd !path_prefix))) - -let sections_are_opened () = - match repr_dirpath (snd (snd !path_prefix)) with - [] -> false - | _ -> true - - let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir @@ -194,7 +196,7 @@ let add_entry sp node = let anonymous_id = let n = ref 0 in - fun () -> incr n; id_of_string ("_" ^ (string_of_int !n)) + fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n)) let add_anonymous_entry node = let id = anonymous_id () in @@ -207,7 +209,7 @@ let add_absolutely_named_leaf sp obj = add_entry sp (Leaf obj) let add_leaf id obj = - if fst (current_prefix ()) = initial_path then + if fst (current_prefix ()) = Names.initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -261,7 +263,7 @@ let current_mod_id () = let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in - let prefix = dir,(mp,empty_dirpath) in + let prefix = dir,(mp,Names.empty_dirpath) in let oname = make_path id, make_kn id in if Nametab.exists_module dir then errorlabstrm "open_module" (pr_id id ++ str " already exists") ; @@ -306,7 +308,7 @@ let end_module id = let start_modtype id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in - let prefix = dir,(mp,empty_dirpath) in + let prefix = dir,(mp,Names.empty_dirpath) in let sp = make_path id in let name = sp, make_kn id in if Nametab.exists_cci sp then @@ -363,9 +365,9 @@ let check_for_comp_unit () = let start_compilation s mp = if !comp_name <> None then error "compilation unit is already started"; - if snd (snd (!path_prefix)) <> empty_dirpath then + if snd (snd (!path_prefix)) <> Names.empty_dirpath then error "some sections are already opened"; - let prefix = s, (mp, empty_dirpath) in + let prefix = s, (mp, Names.empty_dirpath) in let _ = add_anonymous_entry (CompilingLibrary prefix) in comp_name := Some s; path_prefix := prefix @@ -395,8 +397,8 @@ let end_compilation dir = | None -> anomaly "There should be a module name..." | Some m -> if m <> dir then anomaly - ("The current open module has name "^ (string_of_dirpath m) ^ - " and not " ^ (string_of_dirpath m)); + ("The current open module has name "^ (Names.string_of_dirpath m) ^ + " and not " ^ (Names.string_of_dirpath m)); in let (after,_,before) = split_lib oname in comp_name := None; @@ -437,13 +439,13 @@ let what_is_opened () = find_entry_p is_something_opened - the list of substitution to do at section closing *) -type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t +type abstr_list = Sign.named_context Names.Cmap.t * Sign.named_context Names.KNmap.t let sectab = - ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) let add_section () = - sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab + sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab let add_section_variable id impl keep = match !sectab with @@ -465,11 +467,11 @@ let add_section_replacement f g hyps = sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl let add_section_kn kn = - let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in + let f = (fun x (l1,l2) -> (l1,Names.KNmap.add kn x l2)) in add_section_replacement f f let add_section_constant kn = - let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in + let f = (fun x (l1,l2) -> (Names.Cmap.add kn x l1,l2)) in add_section_replacement f f let replacement_context () = pi2 (List.hd !sectab) @@ -477,17 +479,17 @@ let replacement_context () = pi2 (List.hd !sectab) let variables_context () = pi1 (List.hd !sectab) let section_segment_of_constant con = - Cmap.find con (fst (pi3 (List.hd !sectab))) + Names.Cmap.find con (fst (pi3 (List.hd !sectab))) let section_segment_of_mutual_inductive kn = - KNmap.find kn (snd (pi3 (List.hd !sectab))) + Names.KNmap.find kn (snd (pi3 (List.hd !sectab))) let section_instance = function | VarRef id -> [||] | ConstRef con -> - Cmap.find con (fst (pi2 (List.hd !sectab))) + Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - KNmap.find kn (snd (pi2 (List.hd !sectab))) + Names.KNmap.find kn (snd (pi2 (List.hd !sectab))) let init_sectab () = sectab := [] let freeze_sectab () = !sectab @@ -713,7 +715,7 @@ let back n = reset_to (back_stk n !lib_stk) (* State and initialization. *) -type frozen = dir_path option * library_segment +type frozen = Names.dir_path option * library_segment let freeze () = (!comp_name, !lib_stk) @@ -757,16 +759,37 @@ let reset_initial () = let mp_of_global ref = match ref with | VarRef id -> fst (current_prefix ()) - | ConstRef cst -> con_modpath cst - | IndRef ind -> ind_modpath ind - | ConstructRef constr -> constr_modpath constr + | ConstRef cst -> Names.con_modpath cst + | IndRef ind -> Names.ind_modpath ind + | ConstructRef constr -> Names.constr_modpath constr let rec dp_of_mp modp = match modp with - | MPfile dp -> dp - | MPbound _ | MPself _ -> library_dp () - | MPdot (mp,_) -> dp_of_mp mp - + | Names.MPfile dp -> dp + | Names.MPbound _ | Names.MPself _ -> library_dp () + | Names.MPdot (mp,_) -> dp_of_mp mp + +let rec split_mp mp = + match mp with + | Names.MPfile dp -> dp, Names.empty_dirpath + | Names.MPdot (prfx, lbl) -> + let mprec, dprec = split_mp prfx in + mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) + | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id] + | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id] + +let split_modpath mp = + let rec aux = function + | Names.MPfile dp -> dp, [] + | Names.MPbound mbid -> + library_dp (), [Names.id_of_mbid mbid] + | Names.MPself msid -> library_dp (), [Names.id_of_msid msid] + | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in + (mp', Names.id_of_label l :: lab) + in + let (mp, l) = aux mp in + mp, l + let library_part ref = match ref with | VarRef id -> library_dp () @@ -798,12 +821,12 @@ let pop_con con = Names.make_con mp (dirpath_prefix dir) l let con_defined_in_sec kn = - let _,dir,_ = repr_con kn in - dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + let _,dir,_ = Names.repr_con kn in + dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) let defined_in_sec kn = - let _,dir,_ = repr_kn kn in - dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + let _,dir,_ = Names.repr_kn kn in + dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) let discharge_global = function | ConstRef kn when con_defined_in_sec kn -> diff --git a/library/lib.mli b/library/lib.mli index 03498f5d9..80ce26fc6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -8,39 +8,31 @@ (*i $Id$ i*) -(*i*) -open Util -open Names -open Libnames -open Libobject -open Summary -open Mod_subst -(*i*) (*s This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) type node = - | Leaf of obj - | CompilingLibrary of object_prefix - | OpenedModule of bool option * object_prefix * Summary.frozen + | Leaf of Libobject.obj + | CompilingLibrary of Libnames.object_prefix + | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of object_prefix * Summary.frozen + | OpenedModtype of Libnames.object_prefix * Summary.frozen | ClosedModtype of library_segment - | OpenedSection of object_prefix * Summary.frozen + | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen -and library_segment = (object_name * node) list +and library_segment = (Libnames.object_name * node) list -type lib_objects = (identifier * obj) list +type lib_objects = (Names.identifier * Libobject.obj) list (*s Object iteratation functions. *) -val open_objects : int -> object_prefix -> lib_objects -> unit -val load_objects : int -> object_prefix -> lib_objects -> unit -val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects +val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit +val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit +val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects (* [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according @@ -48,23 +40,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects [Substitute], [Keep], [Anticipate] respectively. The order of each returned list is the same as in the input list. *) val classify_segment : - library_segment -> lib_objects * lib_objects * obj list + library_segment -> lib_objects * lib_objects * Libobject.obj list (* [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : - object_prefix -> lib_objects -> library_segment + Libnames.object_prefix -> lib_objects -> library_segment (*s Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : identifier -> obj -> object_name -val add_absolutely_named_leaf : object_name -> obj -> unit -val add_anonymous_leaf : obj -> unit +val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name +val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit +val add_anonymous_leaf : Libobject.obj -> unit (* this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : identifier -> obj list -> object_name +val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit @@ -81,19 +73,20 @@ val reset_label : int -> unit starting from a given section path. If not given, the entire segment is returned. *) -val contents_after : object_name option -> library_segment +val contents_after : Libnames.object_name option -> library_segment (*s Functions relative to current path *) (* User-side names *) -val cwd : unit -> dir_path -val make_path : identifier -> section_path -val path_of_include : unit -> section_path +val cwd : unit -> Names.dir_path +val current_dirpath : bool -> Names.dir_path +val make_path : Names.identifier -> Libnames.section_path +val path_of_include : unit -> Libnames.section_path (* Kernel-side names *) -val current_prefix : unit -> module_path * dir_path -val make_kn : identifier -> kernel_name -val make_con : identifier -> constant +val current_prefix : unit -> Names.module_path * Names.dir_path +val make_kn : Names.identifier -> Names.kernel_name +val make_con : Names.identifier -> Names.constant (* Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -102,53 +95,55 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool -val current_mod_id : unit -> module_ident +val current_mod_id : unit -> Names.module_ident (* Returns the most recent OpenedThing node *) -val what_is_opened : unit -> object_name * node +val what_is_opened : unit -> Libnames.object_name * node (*s Modules and module types *) val start_module : - bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix -val end_module : module_ident - -> object_name * object_prefix * Summary.frozen * library_segment + bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix +val end_module : Names.module_ident + -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment val start_modtype : - module_ident -> module_path -> Summary.frozen -> object_prefix -val end_modtype : module_ident - -> object_name * object_prefix * Summary.frozen * library_segment + Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix +val end_modtype : Names.module_ident + -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment (* [Lib.add_frozen_state] must be called after each of the above functions *) (*s Compilation units *) -val start_compilation : dir_path -> module_path -> unit -val end_compilation : dir_path -> object_prefix * library_segment +val start_compilation : Names.dir_path -> Names.module_path -> unit +val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment (* The function [library_dp] returns the [dir_path] of the current compiling library (or [default_library]) *) -val library_dp : unit -> dir_path +val library_dp : unit -> Names.dir_path (* Extract the library part of a name even if in a section *) -val dp_of_mp : module_path -> dir_path -val library_part : global_reference -> dir_path -val remove_section_part : global_reference -> dir_path +val dp_of_mp : Names.module_path -> Names.dir_path +val split_mp : Names.module_path -> Names.dir_path * Names.dir_path +val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list +val library_part : Libnames.global_reference -> Names.dir_path +val remove_section_part : Libnames.global_reference -> Names.dir_path (*s Sections *) -val open_section : identifier -> unit -val close_section : identifier -> unit +val open_section : Names.identifier -> unit +val close_section : Names.identifier -> unit (*s Backtracking (undo). *) -val reset_to : object_name -> unit -val reset_name : identifier located -> unit -val remove_name : identifier located -> unit -val reset_mod : identifier located -> unit -val reset_to_state : object_name -> unit +val reset_to : Libnames.object_name -> unit +val reset_name : Names.identifier Util.located -> unit +val remove_name : Names.identifier Util.located -> unit +val reset_mod : Names.identifier Util.located -> unit +val reset_to_state : Libnames.object_name -> unit -val has_top_frozen_state : unit -> object_name option +val has_top_frozen_state : unit -> Libnames.object_name option (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) @@ -168,28 +163,28 @@ val reset_initial : unit -> unit (* XML output hooks *) -val set_xml_open_section : (identifier -> unit) -> unit -val set_xml_close_section : (identifier -> unit) -> unit +val set_xml_open_section : (Names.identifier -> unit) -> unit +val set_xml_close_section : (Names.identifier -> unit) -> unit (*s Section management for discharge *) -val section_segment_of_constant : constant -> Sign.named_context -val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context +val section_segment_of_constant : Names.constant -> Sign.named_context +val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context -val section_instance : global_reference -> identifier array +val section_instance : Libnames.global_reference -> Names.identifier array -val add_section_variable : identifier -> bool -> Term.types option -> unit -val add_section_constant : constant -> Sign.named_context -> unit -val add_section_kn : kernel_name -> Sign.named_context -> unit +val add_section_variable : Names.identifier -> bool -> Term.types option -> unit +val add_section_constant : Names.constant -> Sign.named_context -> unit +val add_section_kn : Names.kernel_name -> Sign.named_context -> unit val replacement_context : unit -> - (identifier array Cmap.t * identifier array KNmap.t) + (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t) (*s Discharge: decrease the section level if in the current section *) -val discharge_kn : kernel_name -> kernel_name -val discharge_con : constant -> constant -val discharge_global : global_reference -> global_reference -val discharge_inductive : inductive -> inductive +val discharge_kn : Names.kernel_name -> Names.kernel_name +val discharge_con : Names.constant -> Names.constant +val discharge_global : Libnames.global_reference -> Libnames.global_reference +val discharge_inductive : Names.inductive -> Names.inductive diff --git a/library/library.ml b/library/library.ml index 2f74fe92b..272f01f7d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -18,7 +18,6 @@ open Safe_typing open Libobject open Lib open Nametab -open Declaremods (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) @@ -113,7 +112,7 @@ type compilation_unit_name = dir_path type library_disk = { md_name : compilation_unit_name; md_compiled : compiled_library; - md_objects : library_objects; + md_objects : Declaremods.library_objects; md_deps : (compilation_unit_name * Digest.t) list; md_imports : compilation_unit_name list } @@ -123,7 +122,7 @@ type library_disk = { type library_t = { library_name : compilation_unit_name; library_compiled : compiled_library; - library_objects : library_objects; + library_objects : Declaremods.library_objects; library_deps : (compilation_unit_name * Digest.t) list; library_imports : compilation_unit_name list; library_digest : Digest.t } @@ -540,19 +539,16 @@ let require_library qidl export = let modrefl = List.map try_locate_qualified_library qidl in let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then begin - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) - export - end + if Lib.is_modtype () || Lib.is_module () then + begin + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun exp -> + List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + 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; + if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () let require_library_from_file idopt file export = @@ -573,18 +569,18 @@ let require_library_from_file idopt file export = let import_module export (loc,qid) = try match Nametab.locate_module qid with - MPfile dir -> + | MPfile dir -> if Lib.is_modtype () || Lib.is_module () || not export then add_anonymous_leaf (in_import (dir, export)) else add_anonymous_leaf (in_require ([],[dir], Some export)) | mp -> - import_module export mp + Declaremods.import_module export mp with Not_found -> user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) + (loc,"import_library", + str ((string_of_qualid qid)^" is not a module")) (************************************************************************) (*s Initializing the compilation of a library. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index a4933a896..0d5d27538 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -441,7 +441,7 @@ let add_hints local dbnames0 h = (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference") in - if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index ab23f2210..e4d464236 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -238,7 +238,9 @@ let firstchar = let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] -let ident = firstchar identchar* +let id = firstchar identchar* +let pfx_id = (id '.')* +let ident = id | pfx_id id let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" let end_hide = "(*" space* "end" space+ "hide" space* "*)" @@ -405,10 +407,11 @@ and module_refs = parse { module_refs lexbuf } | ident { let id = lexeme lexbuf in - (try - add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id - with - Not_found -> () + (Printf.eprintf "DEBUG: id = %s\n" id; + try + add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id + with + Not_found -> () ); module_refs lexbuf } | eof diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0522bbac0..a75b7196d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -417,17 +417,14 @@ module Html = struct let stop_verbatim () = printf "</pre>\n" let module_ref m s = - printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" - (*i match find_module m with - | Local -> - printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" - | Coqlib | Unknown -> - raw_ident s - i*) + | Local -> + printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" + | Coqlib | Unknown -> + raw_ident s let ident_ref m fid s = match find_module m with @@ -446,6 +443,7 @@ module Html = struct printf "</span>" end else begin + Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc; try (match Index.find !current_module loc with | Def (fullid,_) -> diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index d78aabbf9..b2fa915b6 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -639,7 +639,7 @@ and notation_bol = parse and notation = parse | nl { Output.line_break(); notation_bol lexbuf } - | '"' { Output.char '"'; false } + | '"' { Output.char '"'} | token { let s = lexeme lexbuf in Output.symbol s; notation lexbuf } diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 30fee26a0..d07051b71 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -447,7 +447,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau try let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); + Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) ([], props) k.cl_props diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 02044b2cf..83a4703a2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -108,15 +108,11 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in - let coqdoc_init_state = Constrintern.coqdoc_freeze () in + let coqdoc_init_state = Dumpglob.coqdoc_freeze () in List.iter (fun (v,f) -> States.unfreeze init_state; - Constrintern.coqdoc_unfreeze coqdoc_init_state; - if !Flags.noglob then - Flags.dump := false - else - Flags.dump_into_file (f^".glob"); + Dumpglob.coqdoc_unfreeze coqdoc_init_state; if Flags.do_translate () then with_option translate_file (Vernac.compile v) f else diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c0ec55228..d3c556147 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -126,7 +126,7 @@ let rec vernac_com interpfun (loc,com) = let cl = !Pp.comments in (* end translator state *) (* coqdoc state *) - let cds = Constrintern.coqdoc_freeze() in + let cds = Dumpglob.coqdoc_freeze() in if !Flags.translate_file then begin let _,f = find_file_in_path (Library.get_load_paths ()) @@ -141,13 +141,13 @@ let rec vernac_com interpfun (loc,com) = chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds + Dumpglob.coqdoc_unfreeze cds with e -> if !Flags.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; - Constrintern.coqdoc_unfreeze cds; + Dumpglob.coqdoc_unfreeze cds; raise e end @@ -228,14 +228,15 @@ let compile verbosely f = let ldir,long_f_dot_v = Library.start_library f in let dumpstate = !Flags.dump in if not !Flags.noglob then - (Flags.dump_into_file (f ^ ".glob"); - Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n")); + (Flags.dump := true; + Dumpglob.open_glob_file f; + Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n")); if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in if Pfedit.get_all_proof_names () <> [] then (message "Error: There are pending proofs"; exit 1); if !Flags.xml_export then !xml_end_library (); - if !Flags.dump then Flags.dump_it (); + if !Flags.dump then Dumpglob.close_glob_file (); Flags.dump := dumpstate; Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2cea826a7..d1003bd83 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -275,7 +275,7 @@ let print_located_module r = let global_with_alias r = let gr = global_with_alias r in - if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; gr (**********) @@ -305,49 +305,31 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let current_dirpath sec = - drop_dirpath_prefix (Lib.library_dp ()) - (if sec then Lib.cwd () - else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())) - -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 - | Anonymous -> () - -let vernac_definition (local,_,_ as k) (_,id as lid) def hook = - if !Flags.dump then dump_definition lid false "def"; - match def with - | ProveBody (bl,t) -> (* local binders, typ *) - if Lib.is_modtype () then - errorlabstrm "Vernacentries.VernacDefinition" - (str "Proof editing mode not supported in module types") - else - let hook _ _ = () in - start_proof_and_print (local,DefinitionBody Definition) - [Some lid,(bl,t)] hook - | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with - | None -> None - | Some r -> - let (evc,env)= Command.get_current_context () in - Some (interp_redexp env evc r) in - declare_definition id k bl red_option c typ_opt hook - +let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = + if !Flags.dump then Dumpglob.dump_definition lid false "def"; + (match def with + | ProveBody (bl,t) -> (* local binders, typ *) + if Lib.is_modtype () then + errorlabstrm "Vernacentries.VernacDefinition" + (str "Proof editing mode not supported in module types") + else + let hook _ _ = () in + start_proof_and_print (local,DefinitionBody Definition) + [Some lid, (bl,t)] hook + | DefineBody (bl,red_option,c,typ_opt) -> + let red_option = match red_option with + | None -> None + | Some r -> + let (evc,env)= Command.get_current_context () in + Some (interp_redexp env evc r) in + declare_definition id k bl red_option c typ_opt hook) + let vernac_start_proof kind l lettop hook = if !Flags.dump then List.iter (fun (id, _) -> match id with - | Some lid -> dump_definition lid false "prf" - | None -> ()) l; + | Some lid -> Dumpglob.dump_definition lid false "prf" + | None -> ()) l; if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" @@ -381,28 +363,28 @@ let vernac_exact_proof c = let vernac_assumption kind l nl= let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> - if !dump then - List.iter (fun lid -> - if global then dump_definition lid false "ax" - else dump_definition lid true "var") idl; - declare_assumption idl is_coe kind [] c false false nl) l - + List.iter (fun (is_coe,(idl,c)) -> + if !dump then + List.iter (fun lid -> + if global then Dumpglob.dump_definition lid false "ax" + else Dumpglob.dump_definition lid true "var") idl; + declare_assumption idl is_coe kind [] c false false nl) l + let vernac_inductive f indl = if !dump then List.iter (fun ((lid, _, _, cstrs), _) -> - dump_definition lid false"ind"; + Dumpglob.dump_definition lid false"ind"; List.iter (fun (_, (lid, _)) -> - dump_definition lid false "constr") cstrs) + Dumpglob.dump_definition lid false "constr") cstrs) indl; build_mutual indl f let vernac_fixpoint l b = - List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l; + List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_recursive l b let vernac_cofixpoint l b = - List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l; + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_corecursive l b let vernac_scheme = build_scheme @@ -413,9 +395,11 @@ let vernac_combined_scheme = build_combined_scheme (* Modules *) let vernac_import export refl = - let import ref = Library.import_module export (qualid_of_reference ref) in - List.iter import refl; - Lib.add_frozen_state () + let import ref = + Library.import_module export (qualid_of_reference ref) + in + List.iter import refl; + Lib.add_frozen_state () let vernac_declare_module export (loc, id) binders_ast mty_ast_o = (* We check the state of the system (in section, in module type) @@ -433,9 +417,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = Modintern.interp_modtype Modintern.interp_modexpr 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 + Dumpglob.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 (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) @@ -453,7 +437,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = let mp = Declaremods.start_module Modintern.interp_modtype export id binders_ast mty_ast_o in - Modintern.dump_moddef loc mp "mod"; + Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Interactive Module "^ string_of_id id ^" started") ; List.iter @@ -473,7 +457,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast mty_ast_o mexpr_ast_o in - Modintern.dump_moddef loc mp "mod"; + Dumpglob.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)]) @@ -481,9 +465,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = 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 + Dumpglob.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 (loc,id) binders_ast mty_ast_o = @@ -499,7 +483,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in - Modintern.dump_moddef loc mp "modtype"; + Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter @@ -509,25 +493,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = ) argsexport | Some base_mty -> - let binders_ast = List.map - (fun (export,idl,ty) -> - if export <> None then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" " ^ - "and \"Import\" keywords from every functor argument.") - else (idl,ty)) binders_ast in - let mp = Declaremods.declare_modtype Modintern.interp_modtype + let binders_ast = List.map + (fun (export,idl,ty) -> + if export <> None then + error ("Arguments of a functor definition can be imported only if" ^ + " the definition is interactive. Remove the \"Export\" " ^ + "and \"Import\" keywords from every functor argument.") + else (idl,ty)) binders_ast in + 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") + Dumpglob.dump_moddef loc mp "modtype"; + if_verbose message + ("Module Type "^ string_of_id id ^" is defined") 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") + Dumpglob.dump_modref loc mp "modtype"; + if_verbose message + ("Module Type "^ string_of_id id ^" is defined") let vernac_include = function | CIMTE mty_ast -> @@ -544,7 +528,7 @@ let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> - if !dump then dump_definition lid false "constr"; id in + if !dump then Dumpglob.dump_definition lid false "constr"; id in let sigma = Evd.empty in let env = Global.env() in let s = interp_constr sigma env sort in @@ -553,11 +537,11 @@ let vernac_record struc binders sort nameopt cfs = | Sort s -> s | _ -> user_err_loc (constr_loc sort,"definition_structure", str "Sort expected") in - if !dump then ( - dump_definition (snd struc) false "rec"; + if !Flags.dump then ( + Dumpglob.dump_definition (snd struc) false "rec"; List.iter (fun (_, x) -> match x with - | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj" + | AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); ignore(Record.definition_structure (struc,binders,cfs,const,s)) @@ -565,13 +549,13 @@ let vernac_record struc binders sort nameopt cfs = let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); - if !Flags.dump then dump_definition lid true "sec"; + if !Flags.dump then Dumpglob.dump_definition lid true "sec"; Lib.open_section id let vernac_end_section (loc, id) = if !Flags.dump then - dump_reference loc - (string_of_dirpath (current_dirpath true)) "<>" "sec"; + Dumpglob.dump_reference loc + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section id let vernac_end_segment lid = @@ -586,7 +570,9 @@ let vernac_end_segment lid = let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in - Library.require_library qidl import + let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in + List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl; + Library.require_library qidl import let vernac_canonical r = Recordops.declare_canonical_structure (global_with_alias r) @@ -605,21 +591,21 @@ let vernac_identity_coercion stre id qids qidt = (* Type classes *) let vernac_class id par ar sup props = - if !dump then ( - dump_definition id false "class"; - List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props); + if !Flags.dump then ( + Dumpglob.dump_definition id false "class"; + List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props); Classes.new_class id par ar sup props let vernac_instance glob sup inst props pri = - if !dump then dump_constraint inst false "inst"; + if !Flags.dump then Dumpglob.dump_constraint inst false "inst"; ignore(Classes.new_instance ~global:glob sup inst props pri) let vernac_context l = - if !dump then List.iter (fun x -> dump_constraint x true "var") l; + if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l; Classes.context l let vernac_declare_instance id = - if !dump then dump_definition id false "inst"; + if !Flags.dump then Dumpglob.dump_definition id false "inst"; Classes.declare_instance false id (***********) @@ -754,7 +740,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef let vernac_hints = Auto.add_hints let vernac_syntactic_definition lid = - dump_definition lid false "syndef"; + Dumpglob.dump_definition lid false "syndef"; Command.syntax_definition (snd lid) let vernac_declare_implicits local r = function |