1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
open Pp
open Util
open Names
open Declarations
open Nameops
open Libnames
let get_new_id locals id =
let rec get_id l id =
let dir = make_dirpath [id] in
if not (Nametab.exists_module dir) then
id
else
get_id (id::l) (Nameops.next_ident_away id l)
in
get_id (List.map snd locals) id
let rec print_local_modpath locals = function
| MPbound mbid -> pr_id (List.assoc mbid locals)
| MPdot(mp,l) ->
print_local_modpath locals mp ++ str "." ++ pr_lab l
| MPself _ | MPfile _ -> raise Not_found
let print_modpath locals mp =
try (* must be with let because streams are lazy! *)
let qid = Nametab.shortest_qualid_of_module mp in
pr_qualid qid
with
| Not_found -> print_local_modpath locals mp
let print_kn locals kn =
try
let qid = Nametab.shortest_qualid_of_modtype kn in
pr_qualid qid
with
Not_found ->
let (mp,_,l) = repr_kn kn in
print_local_modpath locals mp ++ str"." ++ pr_lab l
let rec flatten_app mexpr l = match mexpr with
| MEBapply (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 ->
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) ->
hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
and print_sig locals msid sign =
let print_spec (l,spec) = (match spec with
| SPBconst _ -> str "Definition "
| SPBmind _ -> str "Inductive "
| SPBmodule _ -> str "Module "
| SPBmodtype _ -> 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 _ -> str "Definition "
| SEBmind _ -> str "Inductive "
| SEBmodule _ -> str "Module "
| SEBmodtype _ -> 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) ->
(* 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 "]" ++ spc () ++ print_modexpr locals' mexpr)
| MEBstruct (msid, struc) ->
hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
| MEBapply (mexpr,marg,_) ->
let lapp = flatten_app mexpr [marg] in
hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
let print_module with_body mp =
let name = print_modpath [] mp in
print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
let print_modtype kn =
let name = print_kn [] kn in
str "Module Type " ++ name ++ str " = " ++
print_modtype [] (Global.lookup_modtype kn) ++ fnl ()
|
