aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
blob: d007af08eb9557d6bff17a97956618784d43efbf (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
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
(***********************************************************************)
(*  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       *)
(***********************************************************************)

(* $Id$ *)

open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Entries
open Typeops
open Type_errors
open Indtypes
open Term_typing
open Modops
open Subtyping
open Mod_typing

type modvariant = 
  | NONE 
  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
      * (* optional result type *) module_type_body option
  | LIBRARY of dir_path

type module_info = 
    { msid : mod_self_id;
      modpath : module_path;
      seed : dir_path; (* the "seed" of unique identifier generator *)
      label : label;
      variant : modvariant}

let check_label l labset = 
  if Labset.mem l labset then error_existing_label l

type library_info = dir_path * Digest.t

type safe_environment = 
    { old : safe_environment;
      env : env;
      modinfo : module_info;
      labset : Labset.t;
      revsign : module_signature_body;
      revstruct : module_structure_body;
      imports : library_info list;
      loads : (module_path * module_body) list }

(*
  { old = senv.old;
    env = ;
    modinfo = senv.modinfo;
    labset = ;
    revsign = ;
    imports = senv.imports ;
    loads = senv.loads }
*)


(* a small hack to avoid variants and an unused case in all functions *)
let rec empty_environment = 
  { old = empty_environment; 
    env = empty_env;
    modinfo = {
      msid = initial_msid;
      modpath = initial_path;
      seed = initial_dir;
      label = mk_label "_";
      variant = NONE};
    labset = Labset.empty;
    revsign = [];
    revstruct = [];
    imports = [];
    loads = [] }

let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env


(* Insertion of section variables. They are now typed before being
   added to the environment. *)

(* Same as push_named, but check that the variable is not already
   there. Should *not* be done in Environ because tactics add temporary
   hypothesis many many times, and the check performed here would
   cost too much. *)
let safe_push_named (id,_,_ as d) env =
  let _ =
    try
      let _ = lookup_named id env in 
      error ("identifier "^string_of_id id^" already defined")
    with Not_found -> () in
  Environ.push_named d env

let push_named_def (id,b,topt) senv =
  let (c,typ,cst) = translate_local_def senv.env (b,topt) in
  let env' = add_constraints cst senv.env in
  let env'' = safe_push_named (id,Some c,typ) env' in
  (cst, {senv with env=env''})

let push_named_assum (id,t) senv =
  let (t,cst) = translate_local_assum senv.env t in
  let env' = add_constraints cst senv.env in
  let env'' = safe_push_named (id,None,t) env' in
  (cst, {senv with env=env''})


(* Insertion of constants and parameters in environment. *)

type global_declaration = 
  | ConstantEntry of constant_entry
  | GlobalRecipe of Cooking.recipe

let hcons_constant_body cb =
  let body = match cb.const_body with
      None -> None
    | Some l_constr -> let constr = Declarations.force l_constr in
	Some (Declarations.from_val (hcons1_constr constr))
  in
    { cb with
	const_body = body;
	const_type = hcons1_constr cb.const_type }

let add_constant dir l decl senv =
  check_label l senv.labset;
  let cb = match decl with 
      ConstantEntry ce -> translate_constant senv.env ce
    | GlobalRecipe r ->
        let cb = translate_recipe senv.env r in
        if dir = empty_dirpath then hcons_constant_body cb else cb
  in
(*  let cb = if dir = empty_dirpath then hcons_constant_body cb else cb in*)
  let env' = Environ.add_constraints cb.const_constraints senv.env in
  let kn = make_kn senv.modinfo.modpath dir l in
  let env'' = Environ.add_constant kn cb env' in
  kn, { old = senv.old;
	env = env'';
	modinfo = senv.modinfo;
	labset = Labset.add l senv.labset;
	revsign = (l,SPBconst cb)::senv.revsign;
	revstruct = (l,SEBconst cb)::senv.revstruct;
	imports = senv.imports;
	loads = senv.loads }
    

(* Insertion of inductive types. *)

let add_mind dir l mie senv =
  if mie.mind_entry_inds = [] then 
    anomaly "empty inductive types declaration"; 
            (* this test is repeated by translate_mind *)
  let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
  if l <> label_of_id id then
    anomaly ("the label of inductive packet and its first inductive"^
	     " type do not match");
  check_label l senv.labset; 
    (* TODO: when we will allow reorderings we will have to verify 
       all labels *)
  let mib = translate_mind senv.env mie in
  let env' = Environ.add_constraints mib.mind_constraints senv.env in
  let kn = make_kn senv.modinfo.modpath dir l in
  let env'' = Environ.add_mind kn mib env' in
  kn, { old = senv.old;
	env = env'';
	modinfo = senv.modinfo;
	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
	revsign = (l,SPBmind mib)::senv.revsign;
	revstruct = (l,SEBmind mib)::senv.revstruct;
	imports = senv.imports;
	loads = senv.loads }


(* Insertion of module types *)

let add_modtype l mte senv = 
  check_label l senv.labset; 
  let mtb = translate_modtype senv.env mte in
  let env' = add_modtype_constraints senv.env mtb in
  let kn = make_kn senv.modinfo.modpath empty_dirpath l in
  let env'' = Environ.add_modtype kn mtb env' in
  kn, { old = senv.old;
	env = env'';
	modinfo = senv.modinfo;
	labset = Labset.add l senv.labset;
	revsign = (l,SPBmodtype mtb)::senv.revsign;
	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
	imports = senv.imports;
	loads = senv.loads }



(* full_add_module adds module with universes and constraints *)
let full_add_module mp mb env =
  let env = add_module_constraints env mb in
  let env = Modops.add_module mp mb env in
    env

(* Insertion of modules *)

let add_module l me senv = 
  check_label l senv.labset; 
  let mb = translate_module senv.env me in
  let mspec = module_spec_of_body mb in
  let mp = MPdot(senv.modinfo.modpath, l) in
  let env' = full_add_module mp mb senv.env in
  mp, { old = senv.old;
	env = env';
	modinfo = senv.modinfo;
	labset = Labset.add l senv.labset;
	revsign = (l,SPBmodule mspec)::senv.revsign;
	revstruct = (l,SEBmodule mb)::senv.revstruct;
	imports = senv.imports;
	loads = senv.loads }


(* Interactive modules *)

let start_module l params result senv = 
  check_label l senv.labset; 
  let rec trans_params env = function 
    | [] -> env,[] 
    | (mbid,mte)::rest -> 
	let mtb = translate_modtype env mte in
	let env = 
	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
	in
	let env,transrest = trans_params env rest in
	env, (mbid,mtb)::transrest
  in
  let env,params_body = trans_params senv.env params in
  let check_sig mtb = match scrape_modtype env mtb with
    | MTBsig _ -> ()
    | MTBfunsig _ -> error_result_must_be_signature mtb 
    | _ -> anomaly "start_module: modtype not scraped"
  in
  let result_body = option_app (translate_modtype env) result in
  ignore (option_app check_sig result_body);
  let msid = make_msid senv.modinfo.seed (string_of_label l) in
  let mp = MPself msid in
  let modinfo = { msid = msid;
		  modpath = mp;
		  seed = senv.modinfo.seed;
		  label = l;
		  variant = STRUCT(params_body,result_body) }
  in
  mp, { old = senv;
	env = env;
	modinfo = modinfo;
	labset = Labset.empty;
	revsign = [];
	revstruct = [];
	imports = senv.imports;
	loads = [] }



let end_module l senv = 
  let oldsenv = senv.old in
  let modinfo = senv.modinfo in
  let params, restype = 
    match modinfo.variant with
      | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
      | STRUCT(params,restype) -> (params,restype)
  in
  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
  if not (empty_context senv.env) then error_local_context None;
  let functorize_type = 
    List.fold_right 
      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
      params
  in
  let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
  let mtb, mod_user_type, cst = 
    match restype with
      | None -> functorize_type auto_tb, None, Constraint.empty
      | Some res_tb -> 
	  let cst = check_subtypes senv.env auto_tb res_tb in
	  let mtb = functorize_type res_tb in
	    mtb, Some mtb, cst
  in
  let mexpr = 
    List.fold_right
      (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
      params
      (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
  in
  let mb = 
    { mod_expr = Some mexpr;
      mod_user_type = mod_user_type;
      mod_type = mtb;
      mod_equiv = None;
      mod_constraints = cst }
  in
  let mspec = 
    { msb_modtype = mtb;
      msb_equiv = None;
      msb_constraints = Constraint.empty } 
  in
  let mp = MPdot (oldsenv.modinfo.modpath, l) in
  let newenv = oldsenv.env in
  let newenv = 
    List.fold_left
      (fun env (mp,mb) -> full_add_module mp mb env) 
      newenv
      senv.loads
  in
  let newenv = 
    full_add_module mp mb newenv
  in 
  mp, { old = oldsenv.old;
	env = newenv;
	modinfo = oldsenv.modinfo;
	labset = Labset.add l oldsenv.labset;
	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
	imports = senv.imports;
	loads = senv.loads@oldsenv.loads }


(* Interactive module types *)

let start_modtype l params senv = 
  check_label l senv.labset; 
  let rec trans_params env = function 
    | [] -> env,[] 
    | (mbid,mte)::rest -> 
	let mtb = translate_modtype env mte in
	let env = 
	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
	in
	let env,transrest = trans_params env rest in
	env, (mbid,mtb)::transrest
  in
  let env,params_body = trans_params senv.env params in
  let msid = make_msid senv.modinfo.seed (string_of_label l) in
  let mp = MPself msid in
  let modinfo = { msid = msid;
		  modpath = mp;
		  seed = senv.modinfo.seed;
		  label = l;
		  variant = SIG params_body }
  in
  mp, { old = senv;
	env = env;
	modinfo = modinfo;
	labset = Labset.empty;
	revsign = [];
	revstruct = [];
	imports = senv.imports;
	loads = [] }

let end_modtype l senv = 
  let oldsenv = senv.old in
  let modinfo = senv.modinfo in
  let params = 
    match modinfo.variant with
      | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
      | SIG params -> params
  in
  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
  if not (empty_context senv.env) then error_local_context None;
  let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
  let mtb = 
    List.fold_right 
      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
      params
      res_tb
  in
  let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
  let newenv = oldsenv.env in
  let newenv = 
    List.fold_left
      (fun env (mp,mb) -> full_add_module mp mb env) 
      newenv
      senv.loads
  in
  let newenv = 
    add_modtype_constraints newenv mtb 
  in
  let newenv = 
    Environ.add_modtype kn mtb newenv
  in 
  kn, { old = oldsenv.old;
	env = newenv;
	modinfo = oldsenv.modinfo;
	labset = Labset.add l oldsenv.labset;
	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
	imports = senv.imports;
	loads = senv.loads@oldsenv.loads }
  

let current_modpath senv = senv.modinfo.modpath
let current_msid senv = senv.modinfo.msid


let add_constraints cst senv = 
  {senv with env = Environ.add_constraints cst senv.env}

(* Check that the engagement expected by a library matches the initial one *)
let check_engagement env c =
  match Environ.engagement env, c with
    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
    | _, None -> ()
    | _, Some ImpredicativeSet ->
        error "Needs option -impredicative-set"

let set_engagement c senv =
  {senv with env = Environ.set_engagement c senv.env}


(* Libraries = Compiled modules *)

type compiled_library = 
    dir_path * module_body * library_info list * engagement option


(* We check that only initial state Require's were performed before 
   [start_library] was called *)

let start_library dir senv =
  if not (senv.revsign = [] &&
	  senv.modinfo.msid = initial_msid &&
	  senv.modinfo.variant = NONE)
  then
    anomaly "Safe_typing.start_library: environment should be empty";
  let dir_path,l = 
    match (repr_dirpath dir) with
	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
      | hd::tl ->
	  make_dirpath tl, label_of_id hd
  in
  let msid = make_msid dir_path (string_of_label l) in
  let mp = MPself msid in
  let modinfo = { msid = msid;
		  modpath = mp;
		  seed = dir;
		  label = l;
		  variant = LIBRARY dir }
  in
  mp, { old = senv;
	env = senv.env;
	modinfo = modinfo;
	labset = Labset.empty;
	revsign = [];
	revstruct = [];
	imports = senv.imports;
	loads = [] }


let export senv dir = 
  let modinfo = senv.modinfo in
  begin
    match modinfo.variant with
      | LIBRARY dp -> 
	  if dir <> dp then
	    anomaly "We are not exporting the right library!"
      | _ ->
	  anomaly "We are not exporting the library"
  end;
  (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
    (* error_export_simple *) (); *)
  let mb = 
    { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct));
      mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
      mod_user_type = None;
      mod_equiv = None;
      mod_constraints = Constraint.empty }
  in
    modinfo.msid, (dir,mb,senv.imports,engagement senv.env)


let check_imports senv needed =
  let imports = senv.imports in
  let check (id,stamp) =
    try
      let actual_stamp = List.assoc id imports in
      if stamp <> actual_stamp then
	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
    with Not_found -> 
      error ("Reference to unknown module " ^ (string_of_dirpath id))
  in
  List.iter check needed

(* we have an inefficiency: Since loaded files are added to the
environment every time a module is closed, their components are
calculated many times. Thic could be avoided in several ways:

1 - for each file create a dummy environment containing only this
file's components, merge this environment with the global
environment, and store for the future (instead of just its type)

2 - create "persistent modules" environment table in Environ add put
loaded by side-effect once and for all (like it is done in OCaml).
Would this be correct with respect to undo's and stuff ?
*)
 
let import (dp,mb,depends,engmt) digest senv = 
  check_imports senv depends;
  check_engagement senv.env engmt;
  let mp = MPfile dp in
  let env = senv.env in
  mp, { senv with 
	  env = full_add_module mp mb env; 
	  imports = (dp,digest)::senv.imports;
	  loads = (mp,mb)::senv.loads }


(** Remove the body of opaque constants in modules *)
 
let rec lighten_module mb =
  { mb with
    mod_expr = option_app lighten_modexpr mb.mod_expr;
    mod_type = lighten_modtype mb.mod_type;
    mod_user_type = option_app lighten_modtype mb.mod_user_type }

and lighten_modtype = function
  | MTBident kn as x -> x
  | MTBfunsig (mbid,mtb1,mtb2) ->
      MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2)
  | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign)

and lighten_modspec ms =
  { ms with msb_modtype = lighten_modtype ms.msb_modtype }

and lighten_sig sign = 
  let lighten_spec (l,spec) = (l,match spec with
    | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None}
    | (SPBconst _ | SPBmind _) as x -> x
    | SPBmodule m -> SPBmodule (lighten_modspec m)
    | SPBmodtype m -> SPBmodtype (lighten_modtype m))
  in
    List.map lighten_spec sign

and lighten_struct struc = 
  let lighten_body (l,body) = (l,match body with
    | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None}
    | (SEBconst _ | SEBmind _) as x -> x
    | SEBmodule m -> SEBmodule (lighten_module m)
    | SEBmodtype m -> SEBmodtype (lighten_modtype m))
  in
    List.map lighten_body struc

and lighten_modexpr = function
  | MEBfunctor (mbid,mty,mexpr) ->
      MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr)
  | MEBident mp as x -> x
  | MEBstruct (msid, struc) ->
      MEBstruct (msid, lighten_struct struc)
  | MEBapply (mexpr,marg,u) ->
      MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)

let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)


type judgment = unsafe_judgment

let j_val j = j.uj_val
let j_type j = j.uj_type

let safe_infer senv = infer (env_of_senv senv)
    
let typing senv = Typeops.typing (env_of_senv senv)