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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
open Pp
open Util
open Names
open Declarations
open Environ
open Mod_checking
(*
let type_modpath env mp =
strengthen env (lookup_module mp env).mod_type mp
let rec check_spec_body env mp lab = function
| SPBconst cb ->
let kn = mp, empty_dirpath, lab in
check_constant_declaration env kn cb
| SPBmind mib ->
let kn = mp, empty_dirpath, lab in
Indtypes.check_inductive env kn mib
| SPBmodule msb ->
check_mod_spec env msb;
Modops.add_module (MPdot(mp,lab)) (module_body_of_type msb.msb_modtype)
(add_modtype_constraints env msb.msb_modtype)
| SPBmodtype mty ->
let kn = mp, empty_dirpath, lab in
check_modtype env mty;
add_modtype kn mty (add_modtype_constraints env mty)
and check_mod_spec env msb =
let env' = add_constraints msb.msb_constraints env in
check_modtype env' msb.msb_modtype;
(* Subtyping.check_equal env' msb.msb_modtype (MTBident *)
(* TODO: check equiv *)
env'
(* !!!: modtype needs mp (the name it will be given) because
submodule should be added without reference to self *)
and check_modtype env = function
| MTBident kn ->
(try let _ = lookup_modtype kn env in ()
with Not_found -> failwith ("unbound module type "(*^string_of_kn kn*)))
| MTBfunsig (mbid,marg,mbody) ->
check_modtype env marg;
let env' =
add_module (MPbound mbid) (module_body_of_type marg)
(add_modtype_constraints env marg) in
check_modtype env' mbody
| MTBsig (msid,sign) ->
let _ =
List.fold_left (fun env (lab,mb) ->
check_spec_body env (MPself msid) lab mb) env sign in
()
let elem_spec_of_body (lab,e) =
lab,
match e with
SEBconst cb -> SPBconst cb
| SEBmind mind -> SPBmind mind
| SEBmodule msb -> SPBmodule (module_spec_of_body msb)
| SEBmodtype mtb -> SPBmodtype mtb
let rec check_module env mb =
let env' = add_module_constraints env mb in
(* mod_type *)
check_modtype env' mb.mod_type;
(* mod_expr *)
let msig =
match mb.mod_expr with
Some mex ->
let msig = infer_mod_expr env' mex in
Subtyping.check_subtypes env' msig mb.mod_type;
msig
| None -> mb.mod_type in
(* mod_user_type *)
(match mb.mod_user_type with
Some usig -> Subtyping.check_subtypes env' msig usig
| None -> ());
(* mod_equiv *)
(match mb.mod_equiv with
Some mid ->
if mb.mod_expr <> Some(MEBident mid) then
failwith "incorrect module alias"
| None -> ());
and infer_mod_expr env = function
MEBident mp -> type_modpath env mp
| MEBstruct(msid,msb) ->
let mp = MPself msid in
let _ =
List.fold_left (fun env (lab,mb) ->
struct_elem_body env mp lab mb) env msb in
MTBsig(msid,List.map elem_spec_of_body msb)
| MEBfunctor (arg_id, arg, body) ->
check_modtype env arg;
let env' = add_module (MPbound arg_id) (module_body_of_type arg) env in
let body_ty = infer_mod_expr env' body in
MTBfunsig (arg_id, arg, body_ty)
| MEBapply (fexpr,MEBident mp,_) ->
let ftb = infer_mod_expr env fexpr in
let ftb = scrape_modtype env ftb in
let farg_id, farg_b, fbody_b = destr_functor ftb in
let mtb = type_modpath env mp in
Subtyping.check_subtypes env mtb farg_b;
subst_modtype (map_mbid farg_id mp) fbody_b
| MEBapply _ ->
failwith "functor argument must be a module variable"
and struct_elem_body env mp lab = function
| SEBconst cb ->
let kn = mp, empty_dirpath, lab in
check_constant_declaration env kn cb
| SEBmind mib ->
let kn = mp, empty_dirpath, lab in
Indtypes.check_inductive env kn mib
| SEBmodule msb ->
check_module env msb;
(*msgnl(str"MODULE OK: "++prkn(make_kn mp empty_dirpath lab)++fnl());*)
Modops.add_module (MPdot(mp,lab)) msb
(add_module_constraints env msb)
| SEBmodtype mty ->
check_modtype env mty;
add_modtype (mp, empty_dirpath, lab) mty
(add_modtype_constraints env mty)
*)
(************************************************************************)
(*
* Global environment
*)
let genv = ref empty_env
let reset () = genv := empty_env
let get_env () = !genv
let set_engagement c =
genv := set_engagement c !genv
(* full_add_module adds module with universes and constraints *)
let full_add_module dp mb digest =
let env = !genv in
let mp = MPfile dp in
let env = add_module_constraints env mb in
let env = Modops.add_module mp mb env in
genv := add_digest env dp digest
(* Check that the engagement expected by a library matches the initial one *)
let check_engagement env c =
match engagement env, c with
| Some ImpredicativeSet, Some ImpredicativeSet -> ()
| _, None -> ()
| _, Some ImpredicativeSet ->
error "Needs option -impredicative-set"
(* Libraries = Compiled modules *)
let report_clash f caller dir =
let msg =
str "compiled library " ++ str(string_of_dirpath caller) ++
spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
str(string_of_dirpath dir) ++ fnl() in
f msg
let check_imports f caller env needed =
let check (dp,stamp) =
try
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
with Not_found ->
error ("Reference to unknown module " ^ (string_of_dirpath dp))
in
List.iter check needed
(* Remove the body of opaque constants in modules *)
(* also remove mod_expr ? *)
let rec lighten_module mb =
{ mb with
mod_expr = Option.map lighten_modexpr mb.mod_expr;
mod_type = Option.map lighten_modexpr mb.mod_type }
and lighten_struct struc =
let lighten_body (l,body) = (l,match body with
| SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
| (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
| SFBmodule m -> SFBmodule (lighten_module m)
| SFBmodtype m -> SFBmodtype
({m with
typ_expr = lighten_modexpr m.typ_expr}))
in
List.map lighten_body struc
and lighten_modexpr = function
| SEBfunctor (mbid,mty,mexpr) ->
SEBfunctor (mbid,
({mty with
typ_expr = lighten_modexpr mty.typ_expr}),
lighten_modexpr mexpr)
| SEBident mp as x -> x
| SEBstruct (msid, struc) ->
SEBstruct (msid, lighten_struct struc)
| SEBapply (mexpr,marg,u) ->
SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
| SEBwith (seb,wdcl) ->
SEBwith (lighten_modexpr seb,wdcl)
let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
type compiled_library =
dir_path *
module_body *
(dir_path * Digest.t) list *
engagement option
(* When the module is checked, digests do not need to match, but a
warning is issued in case of mismatch *)
let import (dp,mb,depends,engmt as vo) digest =
Validate.val_vo (Obj.repr vo);
prerr_endline "*** vo validated ***";
let env = !genv in
check_imports msg_warning dp env depends;
check_engagement env engmt;
check_module env mb;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
full_add_module dp mb digest
(* When the module is admitted, digests *must* match *)
let unsafe_import (dp,mb,depends,engmt) digest =
let env = !genv in
check_imports (errorlabstrm"unsafe_import") dp env depends;
check_engagement env engmt;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
full_add_module dp mb digest
|
