aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
blob: efbee6af2bed2fb4a2176796df804118c6278763 (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
(************************************************************************)
(*  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        *)
(************************************************************************)

(*i $Id$ 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
  | MEident mb -> mb
  | _ -> raise Not_path

let rec replace_first p k = function 
  | [] -> [] 
  | h::t when p h -> k::t
  | h::t -> h::(replace_first p k t)

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 type_modpath env mp = 
  strengthen env (lookup_module mp env).mod_type mp

let rec translate_modtype env mte =
  match mte with
    | MTEident ln -> MTBident ln
    | MTEfunsig (arg_id,arg_e,body_e) -> 
	let arg_b = translate_modtype env arg_e in
	let env' = 
	  add_module (MPbound arg_id) (module_body_of_type arg_b) env in
	let body_b = translate_modtype env' body_e in
	  MTBfunsig (arg_id,arg_b,body_b)
    | MTEsig (msid,sig_e) ->
	let str_b,sig_b = translate_entry_list env msid false sig_e in
	  MTBsig (msid,sig_b)
    | MTEwith (mte, with_decl) ->
	let mtb = translate_modtype env mte in
	  merge_with env mtb with_decl

and merge_with env mtb with_decl = 
  let msid,sig_b = match (Modops.scrape_modtype env mtb) with 
    | MTBsig(msid,sig_b) -> msid,sig_b 
    | _ -> error_signature_expected mtb
  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 (MPself msid) before env in
      let new_spec = match with_decl with
        | With_Definition ([],_)
        | With_Module ([],_) -> assert false
	| With_Definition ([id],c) -> 
	    let cb = match spec with
		SPBconst cb -> cb
	      | _ -> error_not_a_constant l
	    in 
	      begin
		match cb.const_body with
		  | None -> 
		      let (j,cst1) = Typeops.infer env' c in
		      let cst2 = 
			Reduction.conv_leq env' j.uj_type cb.const_type in
		      let cst = 
			Constraint.union 
			  (Constraint.union cb.const_constraints cst1)
			  cst2 in
                      let body = Some (Declarations.from_val j.uj_val) in
			SPBconst {cb with 
				    const_body = body;
			            const_body_code = Cemitcodes.from_val
                        (compile_constant_body env' body false false);
                                    const_constraints = 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
			SPBconst {cb with 
				    const_body = body;
				    const_body_code = Cemitcodes.from_val
                        (compile_constant_body env' body false false);
                                    const_constraints = cst}
	      end	
(* and what about msid's ????? Don't they clash ? *)
	| With_Module ([id], mp) ->
	    let old = match spec with
		SPBmodule msb -> msb
	      | _ -> error_not_a_module (string_of_label l)
	    in
	    let mtb = type_modpath env' mp in
	 (* here, using assertions in substitutions, 
	    we check that there is no msid bound in mtb *)
	    begin
	      try 
		let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
		  ()
	      with
		  Failure _ -> error_circular_with_module id
	    end;
	    let cst =
              try check_subtypes env' mtb old.msb_modtype
              with Failure _ -> error_with_incorrect (label_of_id id) in
	    let equiv = 
 	      match old.msb_equiv with
		| None -> Some mp
		| Some mp' -> 
		    check_modpath_equiv env' mp mp';
		    Some mp
	    in
	    let msb =
	      {msb_modtype = mtb; 
	       msb_equiv = equiv; 
	       msb_constraints = Constraint.union old.msb_constraints cst }
	    in
	      SPBmodule msb
	| With_Definition (_::_,_)
        | With_Module (_::_,_) -> 
	    let old = match spec with
		SPBmodule msb -> msb
	      | _ -> error_not_a_module (string_of_label l)
	    in
	      begin
		match old.msb_equiv with
                   None ->
                    let new_with_decl = match with_decl with
                       With_Definition (_,c) -> With_Definition (idl,c)
                     | With_Module (_,c) -> With_Module (idl,c) in
                    let modtype = 
                     merge_with env' old.msb_modtype new_with_decl in
                    let msb =
	              {msb_modtype = modtype; 
	               msb_equiv = None; 
	               msb_constraints = old.msb_constraints }
	            in
	             SPBmodule msb
                 | Some mp ->
                    error_a_generative_module_expected l
              end
      in
	MTBsig(msid,  before@(l,new_spec)::after)
    with
	Not_found -> error_no_such_label l
      | Reduction.NotConvertible -> error_with_incorrect l

and translate_entry_list env msid is_definition sig_e = 
  let mp = MPself msid in
  let do_entry env (l,e) = 
    let kn = make_kn mp empty_dirpath l in
    let con = make_con mp empty_dirpath l in
    match e with
      | SPEconst ce ->
	  let cb = translate_constant env con ce in
	    begin match cb.const_hyps with
	      |	(_::_) -> error_local_context (Some l)
	      | [] ->
		  add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb)
	    end
      | SPEmind mie -> 
	  let mib = translate_mind env mie in
	    begin match mib.mind_hyps with
	      |	(_::_) -> error_local_context (Some l)
	      | [] ->
		  add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
	    end
      | SPEmodule me ->
	  let mb = translate_module env is_definition me in
	  let mspec = 
	    { msb_modtype = mb.mod_type;
	      msb_equiv = mb.mod_equiv;
	      msb_constraints = mb.mod_constraints }
	  in
	  let mp' = MPdot (mp,l) in
	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
      | SPEmodtype mte ->
	  let mtb = translate_modtype env mte in
	    add_modtype kn mtb env, (l, SEBmodtype mtb), (l, SPBmodtype mtb)
  in
  let _,str_b,sig_b = list_fold_map2 do_entry env sig_e
  in
    str_b,sig_b

(* if [is_definition=true], [mod_entry_expr] may be any expression.
   Otherwise it must be a path *)

and translate_module env is_definition 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_modtype env mte in
	{ mod_expr = None;
	  mod_user_type = Some mtb;
	  mod_type = mtb;
	  mod_equiv = None;
	  mod_constraints = Constraint.empty }
    | Some mexpr, _ -> 
	let meq_o = (* do we have a transparent module ? *)
	  try       (* TODO: transparent field in module_entry *)
	    match me.mod_entry_type with
	      | None -> Some (path_of_mexpr mexpr)
	      | Some _ -> None
	  with 
	    | Not_path -> None
	in
	let meb,mtb1 = 
	  if is_definition then
	    translate_mexpr env mexpr
	  else 
	    let mp = 
	      try 
		path_of_mexpr mexpr 
	      with 
		| Not_path -> error_declaration_not_path mexpr
	    in
	      MEBident mp, type_modpath env mp
	in
	let mtb, mod_user_type, cst =
	  match me.mod_entry_type with
	    | None -> mtb1, None, Constraint.empty
	    | Some mte -> 
		let mtb2 = translate_modtype env mte in
                let cst =
                  try check_subtypes env mtb1 mtb2
                  with Failure _ -> error "not subtype" in
		mtb2, Some mtb2, cst
	in
	  { mod_type = mtb;
	    mod_user_type = mod_user_type;
	    mod_expr = Some meb;
	    mod_equiv = meq_o;
	    mod_constraints = cst }

(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
and translate_mexpr env mexpr = match mexpr with
  | MEident mp -> 
      MEBident mp,
      type_modpath env mp
  | MEfunctor (arg_id, arg_e, body_expr) ->
      let arg_b = translate_modtype env arg_e in
      let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
      let (body_b,body_tb) = translate_mexpr env' body_expr in
	MEBfunctor (arg_id, arg_b, body_b), 
	MTBfunsig (arg_id, arg_b, body_tb)
  | MEapply (fexpr,mexpr) ->
      let feb,ftb = translate_mexpr env fexpr in
      let ftb = scrape_modtype env ftb in
      let farg_id, farg_b, fbody_b = destr_functor ftb in
      let meb,mtb = translate_mexpr env mexpr in
      let cst =
        try check_subtypes env mtb farg_b
        with Failure _ ->
          error "" in
      let mp = 
	try
	  path_of_mexpr mexpr 
	with
	  | Not_path -> error_application_to_not_path mexpr
	      (* place for nondep_supertype *)
      in
       let resolve = Modops.resolver_of_environment farg_id farg_b mp env in
	MEBapply(feb,meb,cst),
        (* This is the place where the functor formal parameter is
           substituted by the given argument to compute the type of the
           functor application. *)
	subst_modtype
         (map_mbid farg_id mp (Some resolve)) fbody_b
  | MEstruct (msid,structure) ->
      let structure,signature = translate_entry_list env msid true structure in
	MEBstruct (msid,structure),
	MTBsig (msid,signature)


(* is_definition is true - me.mod_entry_expr may be any expression *)
let translate_module env me = translate_module env true me

let rec add_module_expr_constraints env = function
  | MEBident _ -> env

  | MEBfunctor (_,mtb,meb) -> 
      add_module_expr_constraints (add_modtype_constraints env mtb) meb

  | MEBstruct (_,mod_struct_body) ->
      List.fold_left 
        (fun env (l,item) -> add_struct_elem_constraints env item)
        env
        mod_struct_body

  | MEBapply (meb1,meb2,cst) ->
      Environ.add_constraints cst 
        (add_module_expr_constraints 
	  (add_module_expr_constraints env meb1) 
	  meb2)

and add_struct_elem_constraints env = function 
  | SEBconst cb -> Environ.add_constraints cb.const_constraints env
  | SEBmind mib -> Environ.add_constraints mib.mind_constraints env
  | SEBmodule mb -> add_module_constraints env mb
  | SEBmodtype mtb -> add_modtype_constraints env mtb

and add_module_constraints env mb = 
  (* if there is a body, the mb.mod_type is either inferred from the
     body and hence uninteresting or equal to the non-empty
     user_mod_type *)
  let env = match mb.mod_expr with
    | None -> add_modtype_constraints env mb.mod_type
    | Some meb -> add_module_expr_constraints env meb
  in
  let env = match mb.mod_user_type with
    | None -> env
    | Some mtb -> add_modtype_constraints env mtb
  in
    Environ.add_constraints mb.mod_constraints env

and add_modtype_constraints env = function
  | MTBident _ -> env
  | MTBfunsig (_,mtb1,mtb2) ->
      add_modtype_constraints
        (add_modtype_constraints env mtb1)
        mtb2
  | MTBsig (_,mod_sig_body) ->
      List.fold_left 
        (fun env (l,item) -> add_sig_elem_constraints env item)
        env
        mod_sig_body

and add_sig_elem_constraints env = function 
  | SPBconst cb -> Environ.add_constraints cb.const_constraints env
  | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
  | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> 
      add_modtype_constraints (Environ.add_constraints cst env) mtb
  | SPBmodtype mtb -> add_modtype_constraints env mtb