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
|
(***********************************************************************)
(* 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 print_modpath env 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 as e ->
match mp with
| MPbound mbid -> Nameops.pr_id (id_of_mbid mbid)
| _ -> raise e
let print_kn env kn =
let qid = Nametab.shortest_qualid_of_modtype kn in
pr_qualid qid
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 env 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 -> str " := " ++ print_modexpr env mexpr
| Some mp, _, _ -> str " == " ++ print_modpath env mp
in
str "Module " ++ name ++ str" : " ++ print_modtype env mb.mod_type ++ body
and print_modtype env mty = match mty with
| MTBident kn -> print_kn env kn
| MTBfunsig (mbid,mtb1,mtb2) ->
(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env
in *)
hov 2 (str "Funsig" ++ spc () ++ str "(" ++
pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype env mtb1 ++
str ")" ++ spc() ++ print_modtype env mtb2)
| MTBsig (msid,sign) ->
hv 2 (str "Sig" ++ spc () ++ print_sig env msid sign ++ brk (1,-2) ++ str "End")
and print_sig env 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 env 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 env mexpr = match mexpr with
| MEBident mp -> print_modpath env mp
| MEBfunctor (mbid,mty,mexpr) ->
(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env
in *)
hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++
str ":" ++ print_modtype env mty ++
str "]" ++ spc () ++ print_modexpr env mexpr)
| MEBstruct (msid, struc) ->
hv 2 (str "Struct" ++ spc () ++ print_struct env 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 env) lapp ++ str")")
let print_module with_body mp =
let env = Global.env() in
let name = print_modpath env mp in
print_module name env with_body (Environ.lookup_module mp env) ++ fnl ()
let print_modtype kn =
let env = Global.env() in
let name = print_kn env kn in
str "Module Type " ++ name ++ str " = " ++
print_modtype env (Environ.lookup_modtype kn env) ++ fnl ()
|
