diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /parsing/printmod.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'parsing/printmod.ml')
-rw-r--r-- | parsing/printmod.ml | 59 |
1 files changed, 40 insertions, 19 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index b4a8fdfd..b46cf42d 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -68,12 +68,17 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn +(** Each time we have to print a non-globally visible structure, + we place its elements in a fake fresh namespace. *) + +let mk_fake_top = + let r = ref 0 in + fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r)) + let nametab_register_dir mp = - let id = id_of_string "FAKETOP" in - let fp = Libnames.make_path empty_dirpath id in + let id = mk_fake_top () in let dir = make_dirpath [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))); - fp + Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath))) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here @@ -81,9 +86,10 @@ let nametab_register_dir mp = the user names. This works nonetheless since we search now [Nametab.the_globrevtab] modulo user name. *) -let nametab_register_body mp fp (l,body) = +let nametab_register_body mp dir (l,body) = let push id ref = - Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref + Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir))) + (make_path dir id) ref in match body with | SFBmodule _ -> () (* TODO *) @@ -99,6 +105,27 @@ let nametab_register_body mp fp (l,body) = mip.mind_consnames) mib.mind_packets +let nametab_register_module_body mp struc = + (* If [mp] is a globally visible module, we simply import it *) + try Declaremods.really_import_module mp + with Not_found -> + (* Otherwise we try to emulate an import by playing with nametab *) + nametab_register_dir mp; + List.iter (nametab_register_body mp empty_dirpath) struc + +let nametab_register_module_param mbid seb = + (* For algebraic seb, we use a Declaremods function that converts into mse *) + try Declaremods.process_module_seb_binding mbid seb + with e when Errors.noncritical e -> + (* Otherwise, for expanded structure, we try to play with the nametab *) + match seb with + | SEBstruct struc -> + let mp = MPbound mbid in + let dir = make_dirpath [id_of_mbid mbid] in + nametab_register_dir mp; + List.iter (nametab_register_body mp dir) struc + | _ -> () + let print_body is_impl env mp (l,body) = let name = str (string_of_label l) in hov 2 (match body with @@ -126,19 +153,11 @@ let print_body is_impl env mp (l,body) = try let env = Option.get env in Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib - with _ -> + with e when Errors.noncritical e -> (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 @@ -156,7 +175,7 @@ let rec print_modtype env mp locals mty = 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 _ -> ()); + nametab_register_module_param mbid seb1; hov 2 (str "Funsig" ++ spc () ++ str "(" ++ pr_id (id_of_mbid mbid) ++ str ":" ++ print_modtype env mp1 locals seb1 ++ @@ -164,6 +183,7 @@ let rec print_modtype env mp locals mty = | SEBstruct (sign) -> let env' = Option.map (Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp sign; hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -190,13 +210,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with (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 _ -> ()); + nametab_register_module_param mbid typ; hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ 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 + nametab_register_module_body mp struc; hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++ brk (1,-2) ++ str "End") | SEBapply _ -> @@ -243,7 +264,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; print_module' (Some (Global.env ())) mp with_body me ++ fnl () - with _ -> + with e when Errors.noncritical e -> print_module' None mp with_body me ++ fnl () let print_modtype kn = @@ -254,5 +275,5 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_modtype' (Some (Global.env ())) kn mtb.typ_expr - with _ -> + with e when Errors.noncritical e -> print_modtype' None kn mtb.typ_expr)) |