summaryrefslogtreecommitdiff
path: root/parsing/printmod.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printmod.ml')
-rw-r--r--parsing/printmod.ml242
1 files changed, 171 insertions, 71 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 6339ed8f..9cf76585 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -12,6 +12,27 @@ open Names
open Declarations
open Nameops
open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+ - The "short" one, that just prints the names of the fields.
+ - The "rich" one, that also tries to print the types of the fields.
+ The short version used to be the default behavior, but now we print
+ types by default. The following option allows to change this.
+ Technically, the environments in this file are either None in
+ the "short" mode or (Some env) in the "rich" one.
+*)
+
+let short = ref false
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "short module printing";
+ optkey = ["Short";"Module";"Printing"];
+ optread = (fun () -> !short) ;
+ optwrite = ((:=) short) }
let get_new_id locals id =
let rec get_id l id =
@@ -47,92 +68,141 @@ let print_kn locals kn =
with
Not_found -> print_modpath locals kn
-let rec flatten_app mexpr l = match mexpr with
- | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
- | mexpr -> mexpr::l
+let nametab_register_dir mp =
+ let id = id_of_string "FAKETOP" in
+ let fp = Libnames.make_path empty_dirpath id in
+ let dir = make_dirpath [id] in
+ Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
+ fp
-let rec print_module name locals with_body mb =
- let body = match with_body, mb.mod_expr with
- | false, _
- | true, None -> mt()
- | true, Some mexpr ->
- spc () ++ str ":= " ++ print_modexpr locals mexpr
- in
+(** Nota: the [global_reference] we register in the nametab below
+ might differ from internal ones, since we cannot recreate here
+ the canonical part of constant and inductive names, but only
+ the user names. This works nonetheless since we search now
+ [Nametab.the_globrevtab] modulo user name. *)
- let modtype =
- match mb.mod_type with
- | t -> spc () ++ str": " ++
- print_modtype locals t
+let nametab_register_body mp fp (l,body) =
+ let push id ref =
+ Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
in
- hv 2 (str "Module " ++ name ++ modtype ++ body)
+ match body with
+ | SFBmodule _ -> () (* TODO *)
+ | SFBmodtype _ -> () (* TODO *)
+ | SFBconst _ ->
+ push (id_of_label l) (ConstRef (make_con mp empty_dirpath l))
+ | SFBmind mib ->
+ let mind = make_mind mp empty_dirpath l in
+ Array.iteri
+ (fun i mip ->
+ push mip.mind_typename (IndRef (mind,i));
+ Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1)))
+ mip.mind_consnames)
+ mib.mind_packets
+
+let print_body is_impl env mp (l,body) =
+ let name = str (string_of_label l) in
+ hov 2 (match body with
+ | SFBmodule _ -> str "Module " ++ name
+ | SFBmodtype _ -> str "Module Type " ++ name
+ | SFBconst cb ->
+ (match cb.const_body with
+ | Def _ -> str "Definition "
+ | OpaqueDef _ when is_impl -> str "Theorem "
+ | _ -> str "Parameter ") ++ name ++
+ (match env with
+ | None -> mt ()
+ | Some env ->
+ str " :" ++ spc () ++
+ hov 0 (Printer.pr_ltype_env env
+ (Typeops.type_of_constant_type env cb.const_type)) ++
+ (match cb.const_body with
+ | Def l when is_impl ->
+ spc () ++
+ hov 2 (str ":= " ++
+ Printer.pr_lconstr_env env (Declarations.force l))
+ | _ -> mt ()) ++
+ str ".")
+ | SFBmind mib ->
+ try
+ let env = Option.get env in
+ Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
+ with _ ->
+ (if mib.mind_finite then str "Inductive " else str "CoInductive")
+ ++ name)
+
+let print_struct is_impl env mp struc =
+ begin
+ (* If [mp] is a globally visible module, we simply import it *)
+ try Declaremods.really_import_module mp
+ with _ ->
+ (* Otherwise we try to emulate an import by playing with nametab *)
+ let fp = nametab_register_dir mp in
+ List.iter (nametab_register_body mp fp) struc
+ end;
+ prlist_with_sep spc (print_body is_impl env mp) struc
-and print_modtype locals mty =
+let rec flatten_app mexpr l = match mexpr with
+ | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l)
+ | SEBident mp -> mp::l
+ | _ -> assert false
+
+let rec print_modtype env mp locals mty =
match mty with
| SEBident kn -> print_kn locals kn
| SEBfunctor (mbid,mtb1,mtb2) ->
- (* let env' = Modops.add_module (MPbid mbid)
- (Modops.body_of_type mtb) env
- in *)
- let locals' = (mbid, get_new_id locals (id_of_mbid mbid))
- ::locals in
- hov 2 (str "Funsig" ++ spc () ++ str "(" ++
- pr_id (id_of_mbid mbid) ++ str " : " ++
- print_modtype locals mtb1.typ_expr ++
- str ")" ++ spc() ++ print_modtype locals' mtb2)
- | SEBstruct (sign) ->
- hv 2 (str "Sig" ++ spc () ++ print_sig locals sign ++ brk (1,-2) ++ str "End")
- | SEBapply (mexpr,marg,_) ->
- let lapp = flatten_app mexpr [marg] in
+ let mp1 = MPbound mbid in
+ let env' = Option.map
+ (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
+ let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
+ let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
+ in
+ (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+ hov 2 (str "Funsig" ++ spc () ++ str "(" ++
+ pr_id (id_of_mbid mbid) ++ str ":" ++
+ print_modtype env mp1 locals seb1 ++
+ str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
+ | SEBstruct (sign) ->
+ let env' = Option.map
+ (Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+ hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
+ brk (1,-2) ++ str "End")
+ | SEBapply _ ->
+ let lapp = flatten_app mty [] in
let fapp = List.hd lapp in
let mapp = List.tl lapp in
- hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++
- prlist_with_sep spc (print_modexpr locals) mapp ++ str")")
+ hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
+ prlist_with_sep spc (print_modpath locals) mapp ++ str")")
| SEBwith(seb,With_definition_body(idl,cb))->
+ let env' = None in (* TODO: build a proper environment if env <> None *)
let s = (String.concat "." (List.map string_of_id idl)) in
- hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
+ hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
| SEBwith(seb,With_module_body(idl,mp))->
let s =(String.concat "." (List.map string_of_id idl)) in
- hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
+ hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
-and print_sig locals sign =
- let print_spec (l,spec) = (match spec with
- | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
- | SFBconst {const_body=None}
- | SFBconst {const_opaque=true} -> str "Parameter "
- | SFBmind _ -> str "Inductive "
- | SFBmodule _ -> str "Module "
- | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
- in
- prlist_with_sep spc print_spec sign
-
-and print_struct locals struc =
- let print_body (l,body) = (match body with
- | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition "
- | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
- | SFBconst {const_body=None} -> str "Parameter "
- | SFBmind _ -> str "Inductive "
- | SFBmodule _ -> str "Module "
- | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
- in
- prlist_with_sep spc print_body struc
-
-and print_modexpr locals mexpr = match mexpr with
+let rec print_modexpr env mp locals mexpr = match mexpr with
| SEBident mp -> print_modpath locals mp
| SEBfunctor (mbid,mty,mexpr) ->
-(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env
- in *)
+ let mp' = MPbound mbid in
+ let env' = Option.map
+ (Modops.add_module (Modops.module_body_of_type mp' mty)) env in
+ let typ = Option.default mty.typ_expr mty.typ_expr_alg in
let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
+ (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
- str ":" ++ print_modtype locals mty.typ_expr ++
- str ")" ++ spc () ++ print_modexpr locals' mexpr)
- | SEBstruct ( struc) ->
- hv 2 (str "Struct" ++ spc () ++ print_struct locals struc ++ brk (1,-2) ++ str "End")
- | SEBapply (mexpr,marg,_) ->
- let lapp = flatten_app mexpr [marg] in
- hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
- | SEBwith (_,_)-> anomaly "Not avaible yet"
+ str ":" ++ print_modtype env mp' locals typ ++
+ str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
+ | SEBstruct struc ->
+ let env' = Option.map
+ (Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+ hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
+ brk (1,-2) ++ str "End")
+ | SEBapply _ ->
+ let lapp = flatten_app mexpr [] in
+ hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+ | SEBwith (_,_)-> anomaly "Not available yet"
let rec printable_body dir =
@@ -146,13 +216,43 @@ let rec printable_body dir =
with
Not_found -> true
+(** Since we might play with nametab above, we should reset to prior
+ state after the printing *)
-let print_module with_body mp =
+let print_modexpr' env mp mexpr =
+ States.with_state_protection (print_modexpr env mp []) mexpr
+let print_modtype' env mp mty =
+ States.with_state_protection (print_modtype env mp []) mty
+
+let print_module' env mp with_body mb =
let name = print_modpath [] mp in
- print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
+ let body = match with_body, mb.mod_expr with
+ | false, _
+ | true, None -> mt()
+ | true, Some mexpr ->
+ spc () ++ str ":= " ++ print_modexpr' env mp mexpr
+ in
+ let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type
+ in
+ hv 0 (str "Module " ++ name ++ modtype ++ body)
+
+exception ShortPrinting
+
+let print_module with_body mp =
+ let me = Global.lookup_module mp in
+ try
+ if !short then raise ShortPrinting;
+ print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
+ with _ ->
+ print_module' None mp with_body me ++ fnl ()
let print_modtype kn =
let mtb = Global.lookup_modtype kn in
let name = print_kn [] kn in
- str "Module Type " ++ name ++ str " = " ++
- print_modtype [] mtb.typ_expr ++ fnl ()
+ hv 1
+ (str "Module Type " ++ name ++ str " =" ++ spc () ++
+ (try
+ if !short then raise ShortPrinting;
+ print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+ with _ ->
+ print_modtype' None kn mtb.typ_expr))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 14:01:53 +0000