summaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
blob: e366bc97450e087a2eda685f24f32160b3f66dd4 (plain)
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
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: mod_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)

open Util
open Names
open Univ
open Declarations
open Entries
open Environ
open Term_typing
open Modops
open Subtyping
open Mod_subst

exception Not_path

let path_of_mexpr = function
  | MSEident mp -> mp
  | _ -> raise Not_path

let rec list_split_assoc k rev_before = function
  | [] -> raise Not_found
  | (k',b)::after when k=k' -> rev_before,b,after
  | h::tail -> list_split_assoc k (h::rev_before) tail

let rec list_fold_map2 f e = function
  |  []  -> (e,[],[])
  |  h::t ->
       let e',h1',h2' = f e h in
       let e'',t1',t2' = list_fold_map2 f e' t in
	 e'',h1'::t1',h2'::t2'

let discr_resolver env mtb =
     match mtb.typ_expr with
	SEBstruct _ -> 
	  mtb.typ_delta
      | _ -> (*case mp is a functor *)
	  empty_delta_resolver
	
let rec rebuild_mp mp l =
  match l with
      []-> mp
    | i::r -> rebuild_mp (MPdot(mp,i)) r 
	
let rec check_with env sign with_decl alg_sign mp equiv = 
  let sign,wd,equiv,cst= match with_decl with
    | With_Definition (id,_) ->
	let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
	  sign,With_definition_body(id,cb),equiv,cst
    | With_Module (id,mp1) -> 
	let sign,equiv,cst = 
	  check_with_aux_mod env sign with_decl mp equiv in
	  sign,With_module_body(id,mp1),equiv,cst in
    if alg_sign = None then
      sign,None,equiv,cst
    else
      sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
	    
and check_with_aux_def env sign with_decl mp equiv = 
  let sig_b = match sign with 
    | SEBstruct(sig_b) -> sig_b
    | _ -> error_signature_expected sign
  in
  let id,idl = match with_decl with
    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
    | With_Definition ([],_) | With_Module ([],_) -> assert false
  in
  let l = label_of_id id in
    try
      let rev_before,spec,after = list_split_assoc l [] sig_b in
      let before = List.rev rev_before in
      let env' = Modops.add_signature mp before equiv env in
	match with_decl with
          | With_Definition ([],_) -> assert false
	  | With_Definition ([id],c) ->
	      let cb = match spec with
		  SFBconst cb -> cb
		| _ -> error_not_a_constant l
	      in
		begin
		  match cb.const_body with
		    | None ->
			let (j,cst1) = Typeops.infer env' c in
			let typ = Typeops.type_of_constant_type env' cb.const_type in
			let cst2 = Reduction.conv_leq env' j.uj_type typ in
			let cst =
			  Constraint.union
			    (Constraint.union cb.const_constraints cst1)
			    cst2 in
			let body = Some (Declarations.from_val j.uj_val) in
			let cb' = {cb with
				     const_body = body;
				     const_body_code = Cemitcodes.from_val
                            (compile_constant_body env' body false false);
                                     const_constraints = cst} in
			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
		    | Some b ->
			let cst1 = Reduction.conv env' c (Declarations.force b) in
			let cst = Constraint.union cb.const_constraints cst1 in
			let body = Some (Declarations.from_val c) in
			let cb' = {cb with
				     const_body = body;
				     const_body_code = Cemitcodes.from_val
                            (compile_constant_body env' body false false);
                                     const_constraints = cst} in
			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
	      end
	  | With_Definition (_::_,c) ->
	      let old = match spec with
		  SFBmodule msb -> msb
		| _ -> error_not_a_module (string_of_label l)
	      in
		begin
		  match old.mod_expr with
                    | None ->
			let new_with_decl = With_Definition (idl,c) in 
			let sign,cb,cst = 
			  check_with_aux_def env' old.mod_type new_with_decl 
			    (MPdot(mp,l)) old.mod_delta in
			let new_spec = SFBmodule({old with
						    mod_type = sign;
						    mod_type_alg = None}) in
			  SEBstruct(before@((l,new_spec)::after)),cb,cst
                    | Some msb ->
			error_a_generative_module_expected l
		end
	  | _ -> anomaly "Modtyping:incorrect use of with"
    with
	Not_found -> error_no_such_label l
      | Reduction.NotConvertible -> error_with_incorrect l

and check_with_aux_mod env sign with_decl mp equiv = 
  let sig_b = match sign with 
    | SEBstruct(sig_b) ->sig_b
    | _ -> error_signature_expected sign
  in
  let id,idl = match with_decl with
    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
    | With_Definition ([],_) | With_Module ([],_) -> assert false
  in
  let l = label_of_id id in
    try
      let rev_before,spec,after = list_split_assoc l [] sig_b in
      let before = List.rev rev_before in
      let rec mp_rec = function
	| [] -> mp
	| i::r -> MPdot(mp_rec r,label_of_id i)
      in
      let env' = Modops.add_signature mp before equiv env in
	match with_decl with
          | With_Module ([],_) -> assert false
	  | With_Module ([id], mp1) ->
	      let old = match spec with
		  SFBmodule msb -> msb
		| _ -> error_not_a_module (string_of_label l)
	      in
	      let mb_mp1 = (lookup_module mp1 env) in
	      let mtb_mp1 = 
		module_type_of_module env' None mb_mp1  in
	      let cst =
		match old.mod_expr with
		    None ->
		      begin
			try Constraint.union
			  (check_subtypes env' mtb_mp1 
			     (module_type_of_module env' None old))
			  old.mod_constraints
			with Failure _ -> error_with_incorrect (label_of_id id)
		      end
		  | Some (SEBident(mp')) ->
		      check_modpath_equiv env' mp1 mp';
		      old.mod_constraints
		  | _ ->  error_a_generative_module_expected l
	      in
	      let new_mb = strengthen_and_subst_mb mb_mp1
		(MPdot(mp,l)) env false in
	      let new_spec = SFBmodule {new_mb with 
					  mod_mp = MPdot(mp,l);
					  mod_expr = Some (SEBident mp1);
					  mod_constraints = cst} in
		(* we propagate the new equality in the rest of the signature
		   with the identity substitution accompagned by the new resolver*)
	      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
	      add_delta_resolver equiv new_mb.mod_delta,cst
          | With_Module (idc,mp1) -> 
	      let old = match spec with
		  SFBmodule msb -> msb
		| _ -> error_not_a_module (string_of_label l)
	      in
	      begin
		match old.mod_expr with
		    None ->
		      let new_with_decl = With_Module (idl,mp1) in
		      let sign,equiv',cst =
			check_with_aux_mod env'
			  old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in
		      let new_equiv = add_delta_resolver equiv equiv' in
		      let new_spec = SFBmodule {old with 
						  mod_type = sign;
						  mod_type_alg = None;
						  mod_delta = equiv'}
		      in
		      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in
			SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
		      new_equiv,cst
		  | Some (SEBident(mp')) ->
		      let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
			check_modpath_equiv env' mpnew mp;
			  SEBstruct(before@(l,spec)::after)
			    ,equiv,Constraint.empty
		  | _ ->
		      error_a_generative_module_expected l
              end
	  | _ -> anomaly "Modtyping:incorrect use of with"
    with
	Not_found -> error_no_such_label l
      | Reduction.NotConvertible -> error_with_incorrect l

and translate_module env mp inl me =
  match me.mod_entry_expr, me.mod_entry_type with
    | None, None ->
	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
    | None, Some mte ->
	let mtb = translate_module_type env mp inl mte in
	  { mod_mp = mp;
	    mod_expr = None;
	    mod_type = mtb.typ_expr;
	    mod_type_alg = mtb.typ_expr_alg;
	    mod_delta = mtb.typ_delta;
	    mod_constraints = mtb.typ_constraints; 
	    mod_retroknowledge = []}
   | Some mexpr, _ ->
	let sign,alg_implem,resolver,cst1 =
	  translate_struct_module_entry env mp inl mexpr in
	let sign,alg1,resolver,cst2 =
	  match me.mod_entry_type with
	    | None ->
		sign,None,resolver,Constraint.empty
	    | Some mte ->
		let mtb = translate_module_type env mp inl mte in
                let cst = check_subtypes env
		  {typ_mp = mp;
		   typ_expr = sign;
		   typ_expr_alg = None;
		   typ_constraints = Constraint.empty;
		   typ_delta = resolver;}
		  mtb
		in
		  mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst
	in
	  { mod_mp = mp;
	    mod_type = sign;
	    mod_expr = Some alg_implem;
	    mod_type_alg = alg1;
	    mod_constraints = Univ.Constraint.union cst1 cst2;
	    mod_delta = resolver;
	    mod_retroknowledge = []} 
	    (* spiwack: not so sure about that. It may
	       cause a bug when closing nested modules.
	       If it does, I don't really know how to
	       fix the bug.*)


and translate_struct_module_entry env mp inl mse  = match mse with
  | MSEident mp1 ->
      let mb = lookup_module mp1 env in 
      let mb' = strengthen_and_subst_mb mb mp env false in
	mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty
  | MSEfunctor (arg_id, arg_e, body_expr) ->
      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) 
	env in
      let sign,alg,resolver,cst =
	translate_struct_module_entry env' mp inl body_expr in
      SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver,
      Univ.Constraint.union cst mtb.typ_constraints
  | MSEapply (fexpr,mexpr) ->
      let sign,alg,resolver,cst1 =
	translate_struct_module_entry env mp inl fexpr
      in
      let farg_id, farg_b, fbody_b = destr_functor env sign in
      let mtb,mp1 = 
	try
	  let mp1 = path_of_mexpr mexpr in
	      let mtb = module_type_of_module env None (lookup_module mp1 env) in
		mtb,mp1
	with
	  | Not_path -> error_application_to_not_path mexpr
	      (* place for nondep_supertype *) in
      let cst = check_subtypes env mtb farg_b in
      let mp_delta = discr_resolver env mtb in
      let mp_delta = if not inl then mp_delta else
	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
      in
      let subst = map_mbid farg_id mp1 mp_delta in
	(subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
      (subst_codom_delta_resolver subst resolver),
      Univ.Constraint.union cst1 cst
  | MSEwith(mte, with_decl) ->
      let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in
      let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in
	sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2
	  
and translate_struct_type_entry env inl mse = match mse with
  | MSEident mp1 ->
      let mtb = lookup_modtype mp1 env in 
	mtb.typ_expr,
      Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty
  | MSEfunctor (arg_id, arg_e, body_expr) ->
      let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env  in
      let sign,alg,resolve,mp_from,cst =
	translate_struct_type_entry env' inl body_expr in
	SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from,
      Univ.Constraint.union cst mtb.typ_constraints
  | MSEapply (fexpr,mexpr) ->
      let sign,alg,resolve,mp_from,cst1 =
	translate_struct_type_entry env inl fexpr
      in
      let farg_id, farg_b, fbody_b = destr_functor env sign in
      let mtb,mp1 = 
	try
	  let mp1 = path_of_mexpr mexpr in
	  let mtb = module_type_of_module env None (lookup_module mp1 env) in
	    mtb,mp1
	with
	  | Not_path -> error_application_to_not_path mexpr
	      (* place for nondep_supertype *) in
      let cst2 = check_subtypes env mtb farg_b in
      let mp_delta = discr_resolver env mtb in
      let mp_delta = if not inl then mp_delta else
	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
      in
      let subst = map_mbid farg_id mp1 mp_delta in
	(subst_struct_expr subst fbody_b),None,
      (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2
  | MSEwith(mte, with_decl) ->
      let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
      let sign,alg,resolve,cst1 = 
	check_with env sign with_decl alg mp_from resolve in
	sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1    

and translate_module_type env mp inl mte =
	let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
	let mtb = subst_modtype_and_resolver
	  {typ_mp = mp_from;
	   typ_expr = sign;
	   typ_expr_alg = None;
	   typ_constraints = cst;
	   typ_delta = resolve} mp env
	in {mtb with typ_expr_alg = alg}

let rec translate_struct_include_module_entry env mp inl mse  = match mse with
  | MSEident mp1 ->
      let mb = lookup_module mp1 env in 
      let mb' = strengthen_and_subst_mb mb mp env true in
      let mb_typ = clean_bounded_mod_expr mb'.mod_type in 
	mb_typ, mb'.mod_delta,Univ.Constraint.empty
  | MSEapply (fexpr,mexpr) ->
      let sign,resolver,cst1 =
	translate_struct_include_module_entry env mp inl fexpr in
      let farg_id, farg_b, fbody_b = destr_functor env sign in
      let mtb,mp1 = 
	try
	  let mp1 = path_of_mexpr mexpr in
	      let mtb = module_type_of_module env None (lookup_module mp1 env) in
		mtb,mp1
	with
	  | Not_path -> error_application_to_not_path mexpr
	      (* place for nondep_supertype *) in
      let cst = check_subtypes env mtb farg_b in
      let mp_delta =  discr_resolver env mtb in
      let mp_delta = if not inl then mp_delta else
	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
      in
      let subst = map_mbid farg_id mp1 mp_delta in
	(subst_struct_expr subst fbody_b),
      (subst_codom_delta_resolver subst resolver),
      Univ.Constraint.union cst1 cst
  | _ -> error ("You cannot Include a high-order structure.")
  

let rec add_struct_expr_constraints env = function
  | SEBident _ -> env

  | SEBfunctor (_,mtb,meb) ->
      add_struct_expr_constraints
	(add_modtype_constraints env mtb) meb

  | SEBstruct (structure_body) ->
      List.fold_left
        (fun env (l,item) -> add_struct_elem_constraints env item)
        env
        structure_body

  | SEBapply (meb1,meb2,cst) ->
      Environ.add_constraints cst
        (add_struct_expr_constraints
	  (add_struct_expr_constraints env meb1)
	  meb2)
  | SEBwith(meb,With_definition_body(_,cb))->
      Environ.add_constraints cb.const_constraints
	(add_struct_expr_constraints env meb)
  | SEBwith(meb,With_module_body(_,_))->
      add_struct_expr_constraints env meb
		
and add_struct_elem_constraints env = function 
  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
  | SFBmodule mb -> add_module_constraints env mb
  | SFBmodtype mtb -> add_modtype_constraints env mtb

and add_module_constraints env mb =
  let env = match mb.mod_expr with
    | None -> env
    | Some meb -> add_struct_expr_constraints env meb
  in
  let env =
    add_struct_expr_constraints env mb.mod_type
  in
    Environ.add_constraints mb.mod_constraints env

and add_modtype_constraints env mtb =
  Environ.add_constraints mtb.typ_constraints
    (add_struct_expr_constraints env mtb.typ_expr)


let rec struct_expr_constraints cst = function
  | SEBident _ -> cst

  | SEBfunctor (_,mtb,meb) ->
      struct_expr_constraints
	(modtype_constraints cst mtb) meb

  | SEBstruct (structure_body) ->
      List.fold_left
        (fun cst (l,item) -> struct_elem_constraints cst item)
        cst
        structure_body

  | SEBapply (meb1,meb2,cst1) ->
      struct_expr_constraints
	(struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
	meb2
  | SEBwith(meb,With_definition_body(_,cb))->
      struct_expr_constraints
        (Univ.Constraint.union cb.const_constraints cst) meb
  | SEBwith(meb,With_module_body(_,_))->
      struct_expr_constraints  cst meb	
		
and struct_elem_constraints cst = function 
  | SFBconst cb -> cst
  | SFBmind mib -> cst
  | SFBmodule mb -> module_constraints cst mb
  | SFBmodtype mtb -> modtype_constraints cst mtb

and module_constraints cst mb =
  let cst = match mb.mod_expr with
    | None -> cst
    | Some meb -> struct_expr_constraints cst meb in
  let cst = 
      struct_expr_constraints cst mb.mod_type in
  Univ.Constraint.union mb.mod_constraints cst

and modtype_constraints cst mtb =
  struct_expr_constraints  (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr


let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
let module_constraints = module_constraints Univ.Constraint.empty