diff options
| -rw-r--r-- | .depend | 19 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 7 | ||||
| -rw-r--r-- | kernel/names.mli | 5 | ||||
| -rwxr-xr-x | library/nametab.ml | 60 | ||||
| -rwxr-xr-x | library/nametab.mli | 3 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 25 | ||||
| -rw-r--r-- | parsing/printmod.ml | 96 | ||||
| -rw-r--r-- | parsing/printmod.mli | 14 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 17 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
13 files changed, 219 insertions, 40 deletions
@@ -109,6 +109,7 @@ parsing/printer.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi +parsing/printmod.cmi: kernel/names.cmi lib/pp.cmi parsing/search.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi \ @@ -840,18 +841,18 @@ parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \ pretyping/inductiveops.cmi pretyping/instantiate.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi library/nameops.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ - kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - pretyping/syntax_def.cmi kernel/term.cmi pretyping/termops.cmi \ - lib/util.cmi parsing/prettyp.cmi + parsing/printmod.cmi kernel/reduction.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi parsing/prettyp.cmi parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ library/global.cmx library/impargs.cmx kernel/inductive.cmx \ pretyping/inductiveops.cmx pretyping/instantiate.cmx library/lib.cmx \ library/libnames.cmx library/libobject.cmx library/nameops.cmx \ kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ - kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - pretyping/syntax_def.cmx kernel/term.cmx pretyping/termops.cmx \ - lib/util.cmx parsing/prettyp.cmi + parsing/printmod.cmx kernel/reduction.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ kernel/environ.cmi parsing/extend.cmi library/global.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ @@ -864,6 +865,12 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ parsing/ppconstr.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \ pretyping/termops.cmx lib/util.cmx parsing/printer.cmi +parsing/printmod.cmo: kernel/declarations.cmi kernel/environ.cmi \ + library/global.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ + parsing/printmod.cmi +parsing/printmod.cmx: kernel/declarations.cmx kernel/environ.cmx \ + library/global.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ + parsing/printmod.cmi parsing/q_coqast.cmo: parsing/coqast.cmi parsing/genarg.cmi \ library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi parsing/q_util.cmi \ pretyping/rawterm.cmi proofs/tacexpr.cmo @@ -109,7 +109,8 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo \ parsing/termast.cmo parsing/astterm.cmo parsing/astmod.cmo \ parsing/extend.cmo parsing/esyntax.cmo \ parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \ - parsing/coqlib.cmo parsing/prettyp.cmo parsing/search.cmo + parsing/coqlib.cmo parsing/printmod.cmo parsing/prettyp.cmo \ + parsing/search.cmo HIGHPARSING= parsing/g_prim.cmo parsing/g_basevernac.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 62fc841e6..fb342b221 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -43,8 +43,8 @@ let pptype = (fun x -> pp(prtype x)) let prid id = pp (pr_id id) let prlab l = pp (pr_lab l) -let prmsid msid = pp (str (string_of_msid msid)) -let prmbid mbid = pp (str (string_of_mbid mbid)) +let prmsid msid = pp (str (debug_string_of_msid msid)) +let prmbid mbid = pp (str (debug_string_of_mbid mbid)) let prdir dir = pp (pr_dirpath dir) diff --git a/kernel/names.ml b/kernel/names.ml index 0209d1c33..b67fd32ad 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -71,7 +71,7 @@ let string_of_dirpath = function let u_number = ref 0 type uniq_ident = int * string * dir_path -let make_uid dir s = incr u_number;(!u_number,s,dir) +let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) let string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" @@ -83,11 +83,12 @@ module Umap = Map.Make(struct type mod_self_id = uniq_ident let make_msid = make_uid -let string_of_msid = string_of_uid +let debug_string_of_msid = string_of_uid type mod_bound_id = uniq_ident let make_mbid = make_uid -let string_of_mbid = string_of_uid +let debug_string_of_mbid = string_of_uid +let id_of_mbid (_,s,_) = s type label = string let mk_label l = l diff --git a/kernel/names.mli b/kernel/names.mli index b1bcc0b83..d9b9ddc9c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -48,13 +48,14 @@ 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 string_of_msid : mod_self_id -> string +val debug_string_of_msid : mod_self_id -> string (*s Unique names for bound modules *) type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id -val string_of_mbid : mod_bound_id -> string +val id_of_mbid : mod_bound_id -> identifier +val debug_string_of_mbid : mod_bound_id -> string (*s Names of structure elements *) type label diff --git a/library/nametab.ml b/library/nametab.ml index 1f8111a2c..5e1464f10 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -46,10 +46,17 @@ module Globtab = Map.Make(struct type t=extended_global_reference let compare = compare end) type globtab = section_path Globtab.t - let the_globtab = ref (Globtab.empty : globtab) +type mprewtab = dir_path MPmap.t +let the_modrewtab = ref (MPmap.empty : mprewtab) + + +type knrewtab = section_path KNmap.t +let the_modtyperewtab = ref (KNmap.empty : knrewtab) + + let sp_of_global ctx_opt ref = match (ctx_opt,ref) with | Some ctx, VarRef id -> @@ -194,7 +201,9 @@ let push_syntactic_definition visibility sp kn = let push = push_cci -let push_modtype vis sp kn = push_idtree the_modtypetab vis sp (kn,sp) +let push_modtype vis sp kn = + push_idtree the_modtypetab vis sp (kn,sp); + the_modtyperewtab := KNmap.add kn sp !the_modtyperewtab (* This is for dischargeable non-cci objects (removed at the end of the @@ -208,8 +217,11 @@ let push_object visibility sp = let push_tactic = push_object (* This is to remember absolute Section/Module names and to avoid redundancy *) -let push_dir = push_modidtree the_dirtab - +let push_dir vis dir dir_ref = + push_modidtree the_dirtab vis dir dir_ref; + match dir_ref with + DirModule (_,(mp,_)) -> the_modrewtab := MPmap.add mp dir !the_modrewtab + | _ -> () (* As before we start with generic functions *) @@ -346,17 +358,30 @@ let exists_modtype sp = (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x is a qualid that denotes the same object. *) -let shortest_qualid_of_global env ref = - let sp = sp_of_global env ref in - let (pth,id) = repr_path sp in +let shortest_qualid locate ref dir_path id = let rec find_visible dir qdir = let qid = make_qualid qdir id in if (try locate qid = ref with Not_found -> false) then qid else match dir with - | [] -> qualid_of_sp sp + | [] -> make_qualid dir_path id | a::l -> find_visible l (add_dirpath_prefix a qdir) in - find_visible (repr_dirpath pth) (make_dirpath []) + find_visible (repr_dirpath dir_path) empty_dirpath + +let shortest_qualid_of_global env ref = + let sp = sp_of_global env ref in + let (pth,id) = repr_path sp in + shortest_qualid locate ref pth id + +let shortest_qualid_of_module mp = + let dir = MPmap.find mp !the_modrewtab in + let dir,id = split_dirpath dir in + shortest_qualid locate_module mp dir id + +let shortest_qualid_of_modtype kn = + let sp = KNmap.find kn !the_modtyperewtab in + let dir,id = repr_path sp in + shortest_qualid locate_modtype kn dir id let pr_global_env env ref = (* Il est important de laisser le let-in, car les streams s'évaluent @@ -377,28 +402,35 @@ let global_inductive (loc,qid as locqid) = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * objtab * knsptab * globtab +type frozen = ccitab * dirtab * objtab * knsptab + * globtab * mprewtab * knrewtab let init () = the_ccitab := Idmap.empty; the_dirtab := ModIdmap.empty; the_objtab := Idmap.empty; the_modtypetab := Idmap.empty; - the_globtab := Globtab.empty + the_globtab := Globtab.empty; + the_modrewtab := MPmap.empty; + the_modtyperewtab := KNmap.empty let freeze () = !the_ccitab, !the_dirtab, !the_objtab, !the_modtypetab, - !the_globtab + !the_globtab, + !the_modrewtab, + !the_modtyperewtab -let unfreeze (mc,md,mo,mt,gt) = +let unfreeze (mc,md,mo,mt,gt,mrt,mtrt) = the_ccitab := mc; the_dirtab := md; the_objtab := mo; the_modtypetab := mt; - the_globtab := gt + the_globtab := gt; + the_modrewtab := mrt; + the_modtyperewtab := mtrt let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index 626a529e6..7456f3a4c 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -56,6 +56,9 @@ val id_of_global : Sign.named_context option -> global_reference -> identifier (* Printing of global references using names as short as possible *) val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds +val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_modtype : kernel_name -> qualid + exception GlobalizationError of qualid exception GlobalizationConstantError of qualid diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index b535f1e24..ede831944 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -79,6 +79,10 @@ GEXTEND Gram | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = qualid -> VernacPrint (PrintName qid) | IDENT "Print" -> VernacPrint PrintLocalContext + | IDENT "Print"; IDENT "Module"; "Type"; qid = qualid -> + VernacPrint (PrintModuleType qid) + | IDENT "Print"; IDENT "Module"; qid = qualid -> + VernacPrint (PrintModule qid) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) (* Searching the environment *) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 159b082f0..0808001bb 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -25,6 +25,7 @@ open Declare open Impargs open Libobject open Printer +open Printmod open Libnames open Nametab @@ -262,7 +263,7 @@ let print_mutual sp = let print_section_variable sp = let (d,_) = get_variable sp in let l = implicits_of_var sp in - (print_named_decl d ++ print_impl_args l ++ fnl ()) + (print_named_decl d ++ print_impl_args l) let print_body = function | Some c -> prterm c @@ -288,34 +289,34 @@ let print_constant with_values sep sp = print_typed_body (val_0,typ) else (prtype typ ++ fnl ()))) ++ - print_impl_args impls ++ fnl ()) + print_impl_args impls) -let print_inductive sp = (print_mutual sp ++ fnl ()) +let print_inductive sp = (print_mutual sp) let print_syntactic_def sep kn = let l = label kn in let c = Syntax_def.search_syntactic_definition kn in (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ()) - -let print_module with_values kn = +(*let print_module with_values kn = str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl () let print_modtype kn = str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl () - +*) let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = let tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> - print_section_variable (basename sp) + print_section_variable (basename sp) ++ fnl () | (_,("CONSTANT"|"PARAMETER")) -> - print_constant with_values sep kn + print_constant with_values sep kn ++ fnl () | (_,"INDUCTIVE") -> - print_inductive kn + print_inductive kn ++ fnl () | (_,"MODULE") -> - print_module with_values kn + let (mp,_,l) = repr_kn kn in + print_module with_values (MPdot (mp,l)) ++ fnl () | (_,"MODULE TYPE") -> - print_modtype kn + print_modtype kn ++ fnl () | (_,"AUTOHINT") -> (* (str" Hint Marker" ++ fnl ())*) (mt ()) @@ -323,7 +324,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = (* (str" Grammar Marker" ++ fnl ())*) (mt ()) | (_,"SYNTAXCONSTANT") -> - print_syntactic_def sep kn + print_syntactic_def sep kn ++ fnl () | (_,"PPSYNTAX") -> (* (str" Syntax Marker" ++ fnl ())*) (mt ()) diff --git a/parsing/printmod.ml b/parsing/printmod.ml new file mode 100644 index 000000000..075fdb03d --- /dev/null +++ b/parsing/printmod.ml @@ -0,0 +1,96 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +open Pp +open Util +open Names +open Declarations +open Nameops +open Libnames + +let print_modpath env mp = + try (* must be with let because streams are lazy! *) + let qid = Nametab.shortest_qualid_of_module mp in pr_qualid qid + with + | Not_found as e -> + match mp with + | MPbound mbid -> Nameops.pr_id (id_of_mbid mbid) + | _ -> raise e + +let print_kn env kn = + let qid = Nametab.shortest_qualid_of_modtype kn in + pr_qualid qid + +let rec flatten_app mexpr l = match mexpr with + | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l) + | mexpr -> mexpr::l + +let rec print_module name env with_body mb = + let body = match mb.mod_equiv, with_body, mb.mod_expr with + | None, false, _ + | None, true, None -> mt() + | None, true, Some mexpr -> str " := " ++ print_modexpr env mexpr + | Some mp, _, _ -> str " == " ++ print_modpath env mp + in + str "Module " ++ name ++ str" : " ++ print_modtype env mb.mod_type ++ body + +and print_modtype env mty = match mty with + | MTBident kn -> print_kn env kn + | MTBfunsig (mbid,mtb1,mtb2) -> +(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env + in *) + hov 2 (str "Funsig" ++ spc () ++ str "(" ++ + pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype env mtb1 ++ + str ")" ++ spc() ++ print_modtype env mtb2) + | MTBsig (msid,sign) -> + hv 2 (str "Sig" ++ spc () ++ print_sig env msid sign ++ brk (1,-2) ++ str "End") + +and print_sig env msid sign = + let print_spec (l,spec) = (match spec with + | SPBconst _ -> str "Definition " + | SPBmind _ -> str "Inductive " + | SPBmodule _ -> str "Module " + | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + in + prlist_with_sep spc print_spec sign + +and print_struct env msid struc = + let print_body (l,body) = (match body with + | SEBconst _ -> str "Definition " + | SEBmind _ -> str "Inductive " + | SEBmodule _ -> str "Module " + | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + in + prlist_with_sep spc print_body struc + +and print_modexpr env mexpr = match mexpr with + | MEBident mp -> print_modpath env mp + | MEBfunctor (mbid,mty,mexpr) -> +(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env + in *) + hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ + str ":" ++ print_modtype env mty ++ + str "]" ++ spc () ++ print_modexpr env mexpr) + | MEBstruct (msid, struc) -> + hv 2 (str "Struct" ++ spc () ++ print_struct env msid struc ++ brk (1,-2) ++ str "End") + | MEBapply (mexpr,marg,_) -> + let lapp = flatten_app mexpr [marg] in + hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr env) lapp ++ str")") + + + +let print_module with_body mp = + let env = Global.env() in + let name = print_modpath env mp in + print_module name env with_body (Environ.lookup_module mp env) ++ fnl () + +let print_modtype kn = + let env = Global.env() in + let name = print_kn env kn in + str "Module Type " ++ name ++ str " = " ++ + print_modtype env (Environ.lookup_modtype kn env) ++ fnl () diff --git a/parsing/printmod.mli b/parsing/printmod.mli new file mode 100644 index 000000000..ed23fb501 --- /dev/null +++ b/parsing/printmod.mli @@ -0,0 +1,14 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +open Pp +open Names + +val print_module : bool -> module_path -> std_ppcmds + +val print_modtype : kernel_name -> std_ppcmds diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8b41ba038..904db670f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -173,6 +173,21 @@ let print_modules () = str"Loaded and not imported modules: " ++ pr_vertical_list pr_dirpath only_loaded + +let print_module (loc,qid) = + try + let mp = Nametab.locate_module qid in + msgnl (Printmod.print_module true mp) + with + Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid) + +let print_modtype (loc,qid) = + try + let kn = Nametab.locate_modtype qid in + msgnl (Printmod.print_modtype kn) + with + Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid) + let dump_universes s = let output = open_out s in try @@ -792,6 +807,8 @@ let vernac_print = function | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent | PrintLoadPath -> (* For compatibility ? *) print_loadpath () | PrintModules -> msg (print_modules ()) + | PrintModule qid -> print_module qid + | PrintModuleType qid -> print_modtype qid | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 869760411..d8d67a357 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -39,6 +39,8 @@ type printable = | PrintGrammar of string * string | PrintLoadPath | PrintModules + | PrintModule of qualid located + | PrintModuleType of qualid located | PrintMLLoadPath | PrintMLModules | PrintName of qualid located |