From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- parsing/printmod.ml | 242 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 171 insertions(+), 71 deletions(-) (limited to 'parsing/printmod.ml') 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 *) -(* !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)) -- cgit v1.2.3