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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \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 {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)
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)
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 rec printable_body dir =
let dir = dirpath_prefix dir in
dir = empty_dirpath ||
try
match Nametab.locate_dir (qualid_of_dirpath dir) with
DirOpenModtype _ -> false
| DirModule _ | DirOpenModule _ -> printable_body dir
| _ -> true
with
Not_found -> true
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 ()
|
