aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/names.mli1
-rw-r--r--library/declaremods.ml18
-rw-r--r--library/declaremods.mli4
-rw-r--r--library/libnames.ml52
-rw-r--r--library/libnames.mli11
-rw-r--r--library/nametab.ml5
-rw-r--r--parsing/prettyp.ml90
-rw-r--r--parsing/prettyp.mli3
-rw-r--r--parsing/printer.ml100
-rw-r--r--parsing/printer.mli5
-rw-r--r--parsing/printmod.ml241
-rw-r--r--plugins/extraction/table.ml9
-rw-r--r--toplevel/vernacentries.ml11
13 files changed, 363 insertions, 187 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index acc764028..1f9f65b5c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -105,6 +105,7 @@ val label : kernel_name -> label
val string_of_kn : kernel_name -> string
val pr_kn : kernel_name -> Pp.std_ppcmds
+val kn_ord : kernel_name -> kernel_name -> int
module KNset : Set.S with type elt = kernel_name
module KNpred : Predicate.S with type elt = kernel_name
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 68d928aef..2b29868bd 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -525,6 +525,24 @@ let process_module_bindings argids args =
in
List.iter2 process_arg argids args
+(* Same with module_type_body *)
+
+let rec seb2mse = function
+ | SEBident mp -> MSEident mp
+ | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
+ | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
+ | SEBwith (s,With_definition_body(l,cb)) ->
+ (match cb.const_body with
+ | Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c))
+ | _ -> assert false)
+ | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let process_module_seb_binding mbid seb =
+ process_module_bindings [id_of_mbid mbid]
+ [mbid,
+ (seb2mse seb,
+ { ann_inline = DefaultInline; ann_scope_subst = [] })]
+
let intern_args interp_modtype (idl,(arg,ann)) =
let inl = inline_annot ann in
let lib_dir = Lib.library_dp() in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 21a7aeabe..9d44ba973 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -152,3 +152,7 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
(** For translator *)
val process_module_bindings : module_ident list ->
(mod_bound_id * (module_struct_entry annotated)) list -> unit
+
+(** For Printer *)
+val process_module_seb_binding :
+ mod_bound_id -> Declarations.struct_expr_body -> unit
diff --git a/library/libnames.ml b/library/libnames.ml
index 733c45af2..c82b3476e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -76,25 +76,37 @@ let constr_of_global = function
let constr_of_reference = constr_of_global
let reference_of_constr = global_of_constr
-(* outside of the kernel, names are ordered on their canonical part *)
+let global_ord_gen fc fmi x y =
+ let ind_ord (indx,ix) (indy,iy) =
+ let c = Pervasives.compare ix iy in
+ if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+ in
+ match x, y with
+ | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
+ | IndRef indx, IndRef indy -> ind_ord indx indy
+ | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
+ let c = Pervasives.compare jx jy in
+ if c = 0 then ind_ord indx indy else c
+ | _, _ -> Pervasives.compare x y
+
+let global_ord_can = global_ord_gen canonical_con canonical_mind
+let global_ord_user = global_ord_gen user_con user_mind
+
+(* By default, [global_reference] are ordered on their canonical part *)
+
module RefOrdered = struct
type t = global_reference
- let compare x y =
- let make_name = function
- | ConstRef con ->
- ConstRef(constant_of_kn(canonical_con con))
- | IndRef (kn,i) ->
- IndRef(mind_of_kn(canonical_mind kn),i)
- | ConstructRef ((kn,i),j )->
- ConstructRef((mind_of_kn(canonical_mind kn),i),j)
- | VarRef id -> VarRef id
- in
- Pervasives.compare (make_name x) (make_name y)
+ let compare = global_ord_can
end
-
+
+module RefOrdered_env = struct
+ type t = global_reference
+ let compare = global_ord_user
+end
+
module Refset = Set.Make(RefOrdered)
module Refmap = Map.Make(RefOrdered)
-
+
(* Extended global references *)
type syndef_name = kernel_name
@@ -103,6 +115,18 @@ type extended_global_reference =
| TrueGlobal of global_reference
| SynDef of syndef_name
+(* We order [extended_global_reference] via their user part
+ (cf. pretty printer) *)
+
+module ExtRefOrdered = struct
+ type t = extended_global_reference
+ let compare x y =
+ match x, y with
+ | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+ | SynDef knx, SynDef kny -> kn_ord knx kny
+ | _, _ -> Pervasives.compare x y
+end
+
(**********************************************)
let pr_dirpath sl = (str (string_of_dirpath sl))
diff --git a/library/libnames.mli b/library/libnames.mli
index 1f49b6a4f..18b6ac49a 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -51,7 +51,11 @@ module RefOrdered : sig
type t = global_reference
val compare : global_reference -> global_reference -> int
end
-
+
+module RefOrdered_env : sig
+ type t = global_reference
+ val compare : global_reference -> global_reference -> int
+end
module Refset : Set.S with type elt = global_reference
module Refmap : Map.S with type key = global_reference
@@ -64,6 +68,11 @@ type extended_global_reference =
| TrueGlobal of global_reference
| SynDef of syndef_name
+module ExtRefOrdered : sig
+ type t = extended_global_reference
+ val compare : t -> t -> int
+end
+
(** {6 Dirpaths } *)
val pr_dirpath : dir_path -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index e43ae650c..c6f04b016 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -287,10 +287,7 @@ let the_dirtab = ref (DirTab.empty : dirtab)
(* Reversed name tables ***************************************************)
(* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(struct
- type t=extended_global_reference
- let compare = compare
- end)
+module Globrevtab = Map.Make(ExtRefOrdered)
type globrevtab = full_path Globrevtab.t
let the_globrevtab = ref (Globrevtab.empty : globrevtab)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 87f11030e..4d35ac708 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -335,87 +335,11 @@ let assumptions_for_print lna =
(*********************)
(* *)
-let print_params env params =
- if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
-
-let print_constructors envpar names types =
- let pc =
- prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
- (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
- (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
- in
- hv 0 (str " " ++ pc)
-
-let build_inductive sp tyi =
- let (mib,mip) = Global.lookup_inductive (sp,tyi) in
- let params = mib.mind_params_ctxt in
- let args = extended_rel_list 0 params in
- let env = Global.env() in
- let fullarity = match mip.mind_arity with
- | Monomorphic ar -> ar.mind_user_arity
- | Polymorphic ar ->
- it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
- let arity = hnf_prod_applist env fullarity args in
- let cstrtypes = type_of_constructors env (sp,tyi) in
- let cstrtypes =
- Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
- let cstrnames = mip.mind_consnames in
- (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
-
-let print_one_inductive (sp,tyi) =
- let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
- let env = Global.env () in
- let envpar = push_rel_context params env in
- hov 0 (
- pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++
- str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
- brk(0,2) ++ print_constructors envpar cstrnames cstrtypes
-
-let pr_mutual_inductive finite indl =
- hov 0 (
- str (if finite then "Inductive " else "CoInductive ") ++
- prlist_with_sep (fun () -> fnl () ++ str" with ")
- print_one_inductive indl)
-
-let get_fields =
- let rec prodec_rec l subst c =
- match kind_of_term c with
- | Prod (na,t,c) ->
- let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
- prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
- | LetIn (na,b,_,c) ->
- let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
- prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
- | _ -> List.rev l
- in
- prodec_rec [] []
-
-let pr_record (sp,tyi) =
- let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
- let env = Global.env () in
- let envpar = push_rel_context params env in
- let fields = get_fields cstrtypes.(0) in
- hov 0 (
- hov 0 (
- str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++
- print_params env params ++
- str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
- str ":= " ++ pr_id cstrnames.(0)) ++
- brk(1,2) ++
- hv 2 (str "{ " ++
- prlist_with_sep (fun () -> str ";" ++ brk(2,0))
- (fun (id,b,c) ->
- pr_id id ++ str (if b then " : " else " := ") ++
- pr_lconstr_env envpar c) fields) ++ str" }")
-
let gallina_print_inductive sp =
- let (mib,mip) = Global.lookup_inductive (sp,0) in
+ let env = Global.env() in
+ let mib = Environ.lookup_mind sp env in
let mipv = mib.mind_packets in
- let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
- (if mib.mind_record & not !Flags.raw_print then
- pr_record (List.hd names)
- else
- pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
+ pr_mutual_inductive_body env mib ++ fnl () ++
with_line_skip
(print_inductive_implicit_args sp mipv @
print_inductive_argument_scopes sp mipv)
@@ -606,11 +530,9 @@ let print_full_pure_context () =
++ str "." ++ fnl () ++ fnl ()
| "INDUCTIVE" ->
let mind = Global.mind_of_delta (mind_of_kn kn) in
- let (mib,mip) = Global.lookup_inductive (mind,0) in
- let mipv = mib.mind_packets in
- let names = list_tabulate (fun x -> (mind,x)) (Array.length mipv) in
- pr_mutual_inductive mib.mind_finite names ++ str "." ++
- fnl () ++ fnl ()
+ let mib = Global.lookup_mind mind in
+ pr_mutual_inductive_body (Global.env()) mib ++
+ str "." ++ fnl () ++ fnl ()
| "MODULE" ->
(* TODO: make it reparsable *)
let (mp,_,l) = repr_kn kn in
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 3e05684c3..6d9c6ecc6 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -34,9 +34,6 @@ val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
val print_eval :
reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
-(** This function is exported for the graphical user-interface pcoq *)
-val build_inductive : mutual_inductive -> int ->
- global_reference * rel_context * types * identifier array * types array
val print_name : reference or_by_notation -> std_ppcmds
val print_opaque_name : reference -> std_ppcmds
val print_about : reference or_by_notation -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index f1f5d4c9f..d9b6d8082 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -539,3 +539,103 @@ let pr_instance_gmap insts =
prlist_with_sep fnl (fun (gr, insts) ->
prlist_with_sep fnl pr_instance (cmap_to_list insts))
(Gmap.to_list insts)
+
+(** Inductive declarations *)
+
+open Declarations
+open Termops
+open Reduction
+open Inductive
+open Inductiveops
+
+let print_params env params =
+ if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
+
+let print_constructors envpar names types =
+ let pc =
+ prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+ (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
+ (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
+ in
+ hv 0 (str " " ++ pc)
+
+let build_ind_type env mip =
+ match mip.mind_arity with
+ | Monomorphic ar -> ar.mind_user_arity
+ | Polymorphic ar ->
+ it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
+
+let print_one_inductive env mib (mip,ind_typ) =
+ let params = mib.mind_params_ctxt in
+ (* In case of lets in params, mind_nparams <> List.length params *)
+ let lparams = List.length params in
+ let args = extended_rel_list 0 params in
+ let arity = hnf_prod_applist env ind_typ args in
+ let envpar = push_rel_context params env in
+ let cstrtypes =
+ Array.map (fun c -> hnf_prod_applist envpar (lift lparams c) args)
+ mip.mind_user_lc
+ in
+ hov 0 (
+ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++
+ str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
+ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mib =
+ let mips = Array.to_list mib.mind_packets in
+ let ind_types = List.map (build_ind_type env) mips in
+ let mips_types = List.combine mips ind_types in
+ let ind_ctxt =
+ List.rev_map (fun (m,t) -> (Name m.mind_typename, None, t)) mips_types
+ in
+ let envind = push_rel_context ind_ctxt env in
+ hov 0 (
+ str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
+ prlist_with_sep (fun () -> fnl () ++ str" with ")
+ (print_one_inductive envind mib) mips_types)
+
+let get_fields =
+ let rec prodec_rec l subst c =
+ match kind_of_term c with
+ | Prod (na,t,c) ->
+ let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+ prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
+ | LetIn (na,b,_,c) ->
+ let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+ prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
+ | _ -> List.rev l
+ in
+ prodec_rec [] []
+
+let print_record env mib =
+ let mip = mib.mind_packets.(0) in
+ let ind_typ = build_ind_type env mip in
+ let ind_name = mip.mind_typename in
+ let envind = push_rel_context [(Name ind_name, None, ind_typ)] env in
+ let params = mib.mind_params_ctxt in
+ let lparams = List.length params in
+ let args = extended_rel_list 0 params in
+ let arity = hnf_prod_applist env ind_typ args in
+ let envpar = push_rel_context params envind in
+ let cstr_typ =
+ hnf_prod_applist envpar (lift lparams mip.mind_user_lc.(0)) args
+ in
+ let fields = get_fields cstr_typ in
+ hov 0 (
+ hov 0 (
+ str "Record " ++ pr_id ind_name ++ brk(1,4) ++
+ print_params env params ++
+ str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
+ str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+ brk(1,2) ++
+ hv 2 (str "{ " ++
+ prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+ (fun (id,b,c) ->
+ pr_id id ++ str (if b then " : " else " := ") ++
+ pr_lconstr_env envpar c) fields) ++ str" }")
+
+let pr_mutual_inductive_body env mib =
+ if mib.mind_record & not !Flags.raw_print then
+ print_record env mib
+ else
+ print_mutual_inductive env mib
diff --git a/parsing/printer.mli b/parsing/printer.mli
index ca91cfd4f..713484a76 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -143,3 +143,8 @@ val default_printer_pr : printer_pr
val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
Pp.std_ppcmds
+
+(** Inductive declarations *)
+
+val pr_mutual_inductive_body :
+ env -> Declarations.mutual_inductive_body -> std_ppcmds
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 9440a61bf..f258da587 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -12,6 +12,26 @@ 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;
+ 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,95 +67,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
-and print_modtype locals mty =
+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 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
+
+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) = str (match spec with
- | SFBconst cb ->
- (match cb.const_body with
- | Def _ -> "Definition "
- | Undef _ | OpaqueDef _ -> "Parameter ")
- | SFBmind _ -> "Inductive "
- | SFBmodule _ -> "Module "
- | SFBmodtype _ -> "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) = str (match body with
- | SFBconst cb ->
- (match cb.const_body with
- | Undef _ -> "Parameter "
- | Def _ -> "Definition "
- | OpaqueDef _ -> "Theorem ")
- | SFBmind _ -> "Inductive "
- | SFBmodule _ -> "Module "
- | SFBmodtype _ -> "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 =
@@ -149,13 +215,42 @@ 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 ()
+ str "Module Type " ++ name ++ str " = " ++
+ (try
+ if !short then raise ShortPrinting;
+ print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+ with _ ->
+ print_modtype' None kn mtb.typ_expr)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 725a70559..ad5424deb 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -19,12 +19,11 @@ open Util
open Pp
open Miniml
-(** Sets and maps for [global_reference] that do _not_ work modulo
- name equivalence (otherwise use Refset / Refmap ) *)
+(** Sets and maps for [global_reference] that use the "user" [kernel_name]
+ instead of the canonical one *)
-module RefOrd = struct type t = global_reference let compare = compare end
-module Refmap' = Map.Make(RefOrd)
-module Refset' = Set.Make(RefOrd)
+module Refmap' = Map.Make(RefOrdered_env)
+module Refset' = Set.Make(RefOrdered_env)
(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a9e390538..51fd69149 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -199,9 +199,14 @@ let print_modtype r =
let (loc,qid) = qualid_of_reference r in
try
let kn = Nametab.locate_modtype qid in
- msgnl (Printmod.print_modtype kn)
- with
- Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid)
+ msgnl (Printmod.print_modtype kn)
+ with Not_found ->
+ (* Is there a module of this name ? If yes we display its type *)
+ try
+ let mp = Nametab.locate_module qid in
+ msgnl (Printmod.print_module false mp)
+ with Not_found ->
+ msgnl (str"Unknown Module Type or Module " ++ pr_qualid qid)
let dump_universes_gen g s =
let output = open_out s in