diff options
Diffstat (limited to 'parsing/printmod.ml')
| -rw-r--r-- | parsing/printmod.ml | 108 |
1 files changed, 67 insertions, 41 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index aaf4a662..0bdae7c7 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -42,73 +42,98 @@ let print_kn locals kn = pr_qualid qid with Not_found -> - let (mp,_,l) = repr_kn kn in - print_local_modpath locals mp ++ str"." ++ pr_lab l + try + print_local_modpath locals kn + with + Not_found -> print_modpath locals kn let rec flatten_app mexpr l = match mexpr with - | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l) + | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l) | mexpr -> mexpr::l let rec print_module name locals 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 -> + let body = match with_body, mb.mod_expr with + | false, _ + | true, None -> mt() + | true, Some mexpr -> spc () ++ str ":= " ++ print_modexpr locals mexpr - | Some mp, _, _ -> str " == " ++ print_modpath locals mp in - hv 2 (str "Module " ++ name ++ spc () ++ str": " ++ - print_modtype locals mb.mod_type ++ body) - -and print_modtype locals mty = match mty with - | MTBident kn -> print_kn locals kn - | MTBfunsig (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 ++ - str ")" ++ spc() ++ print_modtype locals' mtb2) - | MTBsig (msid,sign) -> + let modtype = match mb.mod_type with + None -> str "" + | Some t -> str": " ++ + print_modtype locals t + in + hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body) + +and print_modtype 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 (msid,sign) -> hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End") + | SEBapply (mexpr,marg,_) -> + let lapp = flatten_app mexpr [marg] 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")") + | SEBwith(seb,With_definition_body(idl,cb))-> + let s = (String.concat "." (List.map string_of_id idl)) in + hov 2 (print_modtype 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() ++ + str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) and print_sig locals msid sign = let print_spec (l,spec) = (match spec with - | SPBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SPBconst {const_body=None} - | SPBconst {const_opaque=true} -> str "Parameter " - | SPBmind _ -> str "Inductive " - | SPBmodule _ -> str "Module " - | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + | 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 " + | SFBalias (mp,_) -> str "Module" + | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign and print_struct locals msid struc = let print_body (l,body) = (match body with - | SEBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SEBconst {const_body=Some _; const_opaque=true} -> str "Theorem " - | SEBconst {const_body=None} -> str "Parameter " - | SEBmind _ -> str "Inductive " - | SEBmodule _ -> str "Module " - | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + | 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 " + | SFBalias (mp,_) -> 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 - | MEBident mp -> print_modpath locals mp - | MEBfunctor (mbid,mty,mexpr) -> + | 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 locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ - str ":" ++ print_modtype locals mty ++ + str ":" ++ print_modtype locals mty.typ_expr ++ str "]" ++ spc () ++ print_modexpr locals' mexpr) - | MEBstruct (msid, struc) -> + | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") - | MEBapply (mexpr,marg,_) -> + | 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" let rec printable_body dir = @@ -128,6 +153,7 @@ let print_module with_body mp = print_module name [] with_body (Global.lookup_module mp) ++ 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 [] (Global.lookup_modtype kn) ++ fnl () + str "Module Type " ++ name ++ str " = " ++ + print_modtype [] mtb.typ_expr ++ fnl () |