diff options
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | library/declaremods.ml | 18 | ||||
| -rw-r--r-- | library/declaremods.mli | 4 | ||||
| -rw-r--r-- | library/libnames.ml | 52 | ||||
| -rw-r--r-- | library/libnames.mli | 11 | ||||
| -rw-r--r-- | library/nametab.ml | 5 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 90 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 3 | ||||
| -rw-r--r-- | parsing/printer.ml | 100 | ||||
| -rw-r--r-- | parsing/printer.mli | 5 | ||||
| -rw-r--r-- | parsing/printmod.ml | 241 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
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 |