1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: environ.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
19
(* The type of environments. *)
21
type named_context_val = Pre_env.named_context_val
23
type env = Pre_env.env
26
let env_of_pre_env env = env
28
let empty_named_context_val = empty_named_context_val
30
let empty_env = empty_env
32
let engagement env = env.env_stratification.env_engagement
33
let universes env = env.env_stratification.env_universes
34
let named_context env = env.env_named_context
35
let named_context_val env = env.env_named_context,env.env_named_vals
36
let rel_context env = env.env_rel_context
38
let empty_context env =
39
env.env_rel_context = empty_rel_context
40
&& env.env_named_context = empty_named_context
43
let lookup_rel n env =
44
Sign.lookup_rel n env.env_rel_context
46
let evaluable_rel n env =
48
match lookup_rel n env with
54
let nb_rel env = env.env_nb_rel
56
let push_rel = push_rel
58
let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
60
let push_rec_types (lna,typarray,_) env =
61
let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
62
Array.fold_left (fun e assum -> push_rel assum e) env ctxt
64
let reset_rel_context env =
66
env_rel_context = empty_rel_context;
70
let fold_rel_context f env ~init =
71
let rec fold_right env =
72
match env.env_rel_context with
78
env_rel_val = List.tl env.env_rel_val;
79
env_nb_rel = env.env_nb_rel - 1 } in
80
f env rd (fold_right env)
85
let named_context_of_val = fst
86
let named_vals_of_val = snd
88
(* [map_named_val f ctxt] apply [f] to the body and the type of
90
*** /!\ *** [f t] should be convertible with t *)
91
let map_named_val f (ctxt,ctxtv) =
93
List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in
96
let empty_named_context = empty_named_context
98
let push_named = push_named
99
let push_named_context_val = push_named_context_val
101
let val_of_named_context ctxt =
102
List.fold_right push_named_context_val ctxt empty_named_context_val
105
let lookup_named id env = Sign.lookup_named id env.env_named_context
106
let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt
108
let eq_named_context_val c1 c2 =
109
c1 == c2 || named_context_of_val c1 = named_context_of_val c2
111
(* A local const is evaluable if it is defined *)
113
let named_type id env =
114
let (_,_,t) = lookup_named id env in t
116
let named_body id env =
117
let (_,b,_) = lookup_named id env in b
119
let evaluable_named id env =
121
match named_body id env with
124
with Not_found -> false
126
let reset_with_named_context (ctxt,ctxtv) env =
128
env_named_context = ctxt;
129
env_named_vals = ctxtv;
130
env_rel_context = empty_rel_context;
134
let reset_context = reset_with_named_context empty_named_context_val
136
let fold_named_context f env ~init =
137
let rec fold_right env =
138
match env.env_named_context with
142
reset_with_named_context (ctxt,List.tl env.env_named_vals) env in
143
f env d (fold_right env)
146
let fold_named_context_reverse f ~init env =
147
Sign.fold_named_context_reverse f ~init:init (named_context env)
149
(* Global constants *)
151
let lookup_constant = lookup_constant
153
let add_constant kn cs env =
155
Cmap.add kn (cs,ref None) env.env_globals.env_constants in
157
{ env.env_globals with
158
env_constants = new_constants } in
159
{ env with env_globals = new_globals }
161
(* constant_type gives the type of a constant *)
162
let constant_type env kn =
163
let cb = lookup_constant kn env in
166
type const_evaluation_result = NoBody | Opaque
168
exception NotEvaluableConst of const_evaluation_result
170
let constant_value env kn =
171
let cb = lookup_constant kn env in
172
if cb.const_opaque then raise (NotEvaluableConst Opaque);
173
match cb.const_body with
174
| Some l_body -> Declarations.force l_body
175
| None -> raise (NotEvaluableConst NoBody)
177
let constant_opt_value env cst =
178
try Some (constant_value env cst)
179
with NotEvaluableConst _ -> None
181
(* A global const is evaluable if it is defined and not opaque *)
182
let evaluable_constant cst env =
183
try let _ = constant_value env cst in true
184
with Not_found | NotEvaluableConst _ -> false
186
(* Mutual Inductives *)
187
let lookup_mind = lookup_mind
188
let scrape_mind = scrape_mind
191
let add_mind kn mib env =
192
let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
194
{ env.env_globals with
195
env_inductives = new_inds } in
196
{ env with env_globals = new_globals }
198
(* Universe constraints *)
199
let set_universes g env =
200
if env.env_stratification.env_universes == g then env
202
{ env with env_stratification =
203
{ env.env_stratification with env_universes = g } }
205
let add_constraints c env =
206
if c == Constraint.empty then
209
let s = env.env_stratification in
210
{ env with env_stratification =
211
{ s with env_universes = merge_constraints c s.env_universes } }
213
let set_engagement c env = (* Unsafe *)
214
{ env with env_stratification =
215
{ env.env_stratification with env_engagement = Some c } }
217
(* Lookup of section variables *)
218
let lookup_constant_variables c env =
219
let cmap = lookup_constant c env in
220
Sign.vars_of_named_context cmap.const_hyps
222
let lookup_inductive_variables (kn,i) env =
223
let mis = lookup_mind kn env in
224
Sign.vars_of_named_context mis.mind_hyps
226
let lookup_constructor_variables (ind,_) env =
227
lookup_inductive_variables ind env
229
(* Returns the list of global variables in a term *)
231
let vars_of_global env constr =
232
match kind_of_term constr with
234
| Const kn -> lookup_constant_variables kn env
235
| Ind ind -> lookup_inductive_variables ind env
236
| Construct cstr -> lookup_constructor_variables cstr env
239
let global_vars_set env constr =
240
let rec filtrec acc c =
241
let vl = vars_of_global env c in
242
let acc = List.fold_right Idset.add vl acc in
243
fold_constr filtrec acc c
245
filtrec Idset.empty constr
248
(* [keep_hyps env ids] keeps the part of the section context of [env] which
249
contains the variables of the set [ids], and recursively the variables
250
contained in the types of the needed variables. *)
252
let keep_hyps env needed =
254
Sign.fold_named_context_reverse
255
(fun need (id,copt,t) ->
256
if Idset.mem id need then
259
| None -> Idset.empty
260
| Some c -> global_vars_set env c in
262
(global_vars_set env t)
263
(Idset.union globc need)
266
(named_context env) in
267
Sign.fold_named_context
268
(fun (id,_,_ as d) nsign ->
269
if Idset.mem id really_needed then add_named_decl d nsign
272
~init:empty_named_context
276
let add_modtype ln mtb env =
277
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
279
{ env.env_globals with
280
env_modtypes = new_modtypes } in
281
{ env with env_globals = new_globals }
283
let shallow_add_module mp mb env =
284
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
286
{ env.env_globals with
287
env_modules = new_mods } in
288
{ env with env_globals = new_globals }
290
let rec scrape_alias mp env =
292
let mp1 = MPmap.find mp env.env_globals.env_alias in
297
let lookup_module mp env =
298
let mp = scrape_alias mp env in
299
MPmap.find mp env.env_globals.env_modules
301
let lookup_modtype ln env =
302
let mp = scrape_alias ln env in
303
MPmap.find mp env.env_globals.env_modtypes
305
let register_alias mp1 mp2 env =
306
let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in
308
{ env.env_globals with
309
env_alias = new_alias } in
310
{ env with env_globals = new_globals }
312
let lookup_alias mp env =
313
MPmap.find mp env.env_globals.env_alias
317
type unsafe_judgment = {
321
let make_judge v tj =
325
let j_val j = j.uj_val
326
let j_type j = j.uj_type
328
type unsafe_type_judgment = {
332
(*s Compilation of global declaration *)
334
let compile_constant_body = Cbytegen.compile_constant_body
336
exception Hyp_not_found
338
let rec apply_to_hyp (ctxt,vals) id f =
339
let rec aux rtail ctxt vals =
340
match ctxt, vals with
341
| (idc,c,ct as d)::ctxt, v::vals ->
343
(f ctxt d rtail)::ctxt, v::vals
345
let ctxt',vals' = aux (d::rtail) ctxt vals in
347
| [],[] -> raise Hyp_not_found
348
| _, _ -> assert false
351
let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
352
let rec aux ctxt vals =
354
| (idc,c,ct as d)::ctxt, v::vals ->
356
let sign = ctxt,vals in
357
push_named_context_val (f d sign) sign
359
let (ctxt,vals as sign) = aux ctxt vals in
360
push_named_context_val (g d sign) sign
361
| [],[] -> raise Hyp_not_found
362
| _,_ -> assert false
365
let insert_after_hyp (ctxt,vals) id d check =
366
let rec aux ctxt vals =
367
match ctxt, vals with
368
| (idc,c,ct)::ctxt', v::vals' ->
369
if idc = id then begin
371
push_named_context_val d (ctxt,vals)
373
let ctxt,vals = aux ctxt vals in
375
| [],[] -> raise Hyp_not_found
376
| _, _ -> assert false
380
(* To be used in Logic.clear_hyps *)
381
let remove_hyps ids check_context check_value (ctxt, vals) =
382
List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
383
if List.mem id ids then
386
let nd = check_context d in
387
let nv = check_value v in
388
(nd::ctxt,(id',nv)::vals))
395
(*spiwack: the following functions assemble the pieces of the retroknowledge
396
note that the "consistent" register function is available in the module
397
Safetyping, Environ only synchronizes the proactive and the reactive parts*)
401
(* lifting of the "get" functions works also for "mem"*)
402
let retroknowledge f env =
405
let registered env field =
406
retroknowledge mem env field
408
(* spiwack: this unregistration function is not in operation yet. It should
410
(* this unregistration function assumes that no "constr" can hold two different
411
places in the retroknowledge. There is no reason why it shouldn't be true,
412
but in case someone needs it, remember to add special branches to the
413
unregister function *)
414
let unregister env field =
416
| KInt31 (_,Int31Type) ->
417
(*there is only one matching kind due to the fact that Environ.env
418
is abstract, and that the only function which add elements to the
419
retroknowledge is Environ.register which enforces this shape *)
420
(match retroknowledge find env field with
421
| Ind i31t -> let i31c = Construct (i31t, 1) in
422
{env with retroknowledge =
423
remove (retroknowledge clear_info env i31c) field}
425
|_ -> {env with retroknowledge =
427
remove (retroknowledge clear_info env
428
(retroknowledge find env field)) field
430
retroknowledge remove env field}
434
(* the Environ.register function syncrhonizes the proactive and reactive
438
(* subfunction used for static decompilation of int31 (after a vm_compute,
439
see pretyping/vnorm.ml for more information) *)
440
let constr_of_int31 =
441
let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
442
digit of i and adds 1 to it
443
(nth_digit_plus_one 1 3 = 2) *)
444
if (land) i ((lsl) 1 n) = 0 then
449
fun ind -> fun digit_ind -> fun tag ->
451
Array.init 31 (fun n -> mkConstruct
452
(digit_ind, nth_digit_plus_one i (30-n)))
454
mkApp(mkConstruct(ind, 1), array_of_int tag)
457
(* subfunction which adds the information bound to the constructor of
458
the int31 type to the reactive retroknowledge *)
459
let add_int31c retroknowledge c =
460
let rk = add_vm_constant_static_info retroknowledge c
461
Cbytegen.compile_structured_int31
463
add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation
466
(* subfunction which adds the compiling information of an
467
int31 operation which has a specific vm instruction (associates
468
it to the name of the coq definition in the reactive retroknowledge) *)
469
let add_int31_op retroknowledge v n op kn =
470
add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
473
fun env field value ->
474
(* subfunction which shortens the (very often use) registration of binary
475
operators to the reactive retroknowledge. *)
476
let add_int31_binop_from_const op =
478
| Const kn -> retroknowledge add_int31_op env value 2
480
| _ -> anomaly "Environ.register: should be a constant"
482
let add_int31_unop_from_const op =
484
| Const kn -> retroknowledge add_int31_op env value 1
486
| _ -> anomaly "Environ.register: should be a constant"
488
(* subfunction which completes the function constr_of_int31 above
489
by performing the actual retroknowledge operations *)
490
let add_int31_decompilation_from_type rk =
491
(* invariant : the type of bits is registered, otherwise the function
492
would raise Not_found. The invariant is enforced in safe_typing.ml *)
494
| KInt31 (grp, Int31Type) ->
495
(match Retroknowledge.find rk (KInt31 (grp,Int31Bits)) with
499
Retroknowledge.add_vm_decompile_constant_info rk
500
value (constr_of_int31 i31t i31bit_type)
501
| _ -> anomaly "Environ.register: should be an inductive type")
502
| _ -> anomaly "Environ.register: Int31Bits should be an inductive type")
503
| _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field"
505
{env with retroknowledge =
506
let retroknowledge_with_reactive_info =
508
| KInt31 (_, Int31Type) ->
509
let i31c = match value with
510
| Ind i31t -> (Construct (i31t, 1))
511
| _ -> anomaly "Environ.register: should be an inductive type"
513
add_int31_decompilation_from_type
514
(add_vm_before_match_info
515
(retroknowledge add_int31c env i31c)
516
value Cbytegen.int31_escape_before_match)
517
| KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
518
| KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
519
| KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
520
| KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
521
| KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
522
| KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const
523
Cbytecodes.Ksubcarrycint31
524
| KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
525
| KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
526
| KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
529
retroknowledge add_int31_op env value 3
530
Cbytecodes.Kdiv21int31 kn
531
| _ -> anomaly "Environ.register: should be a constant")
532
| KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
533
| KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
536
retroknowledge add_int31_op env value 3
537
Cbytecodes.Kaddmuldivint31 kn
538
| _ -> anomaly "Environ.register: should be a constant")
539
| KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
540
| KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
541
| KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
542
| _ -> env.retroknowledge
544
Retroknowledge.add_field retroknowledge_with_reactive_info field value
548
(**************************************************************)
549
(* spiwack: the following definitions are used by the function
550
[assumptions] which gives as an output the set of all
551
axioms and sections variables on which a given term depends
552
in a context (expectingly the Global context) *)
554
type context_object =
555
| Variable of identifier (* A section variable or a Let definition *)
556
| Axiom of constant (* An axiom or a constant. *)
557
| Opaque of constant (* An opaque constant. *)
559
(* Defines a set of [assumption] *)
560
module OrderedContextObject =
562
type t = context_object
565
| Variable i1 , Variable i2 -> id_ord i1 i2
566
| Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
567
(* spiwack: it would probably be cleaner
568
to provide a [kn_ord] function *)
569
| Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
570
| Variable _ , Axiom _ -> -1
571
| Axiom _ , Variable _ -> 1
576
module ContextObjectSet = Set.Make (OrderedContextObject)
577
module ContextObjectMap = Map.Make (OrderedContextObject)
580
let assumptions ?(add_opaque=false) st (* t env *) =
581
let (idts,knst) = st in
582
(* Infix definition for chaining function that accumulate
583
on a and a ContextObjectSet, ContextObjectMap. *)
584
let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
585
(* This function eases memoization, by checking if an object is already
586
stored before trying and applying a function.
587
If the object is there, the function is not fired (we are in a
588
particular case where memoized object don't need a treatment at all).
589
If the object isn't there, it is stored and the function is fired*)
590
let try_and_go o f s m =
591
if ContextObjectSet.mem o s then
594
f (ContextObjectSet.add o s) m
596
let identity2 s m = (s,m) in
597
(* Goes recursively into the term to see if it depends on assumptions
598
the 3 important cases are : - Const _ where we need to first unfold
599
the constant and return the needed assumptions of its body in the
601
- Rel _ which means the term is a variable
602
which has been bound earlier by a Lambda or a Prod (returns [] ),
603
- Var _ which means that the term refers
604
to a section variable or a "Let" definition, in the former it is
605
an assumption of [t], in the latter is must be unfolded like a Const.
606
The other cases are straightforward recursion.
607
Calls to the environment are memoized, thus avoiding to explore
608
the DAG of the environment as if it was a tree (can cause
609
exponential behavior and prevent the algorithm from terminating
610
in reasonable time). [s] is a set of [context_object], representing
611
the object already visited.*)
612
let rec aux t env s acc =
613
match kind_of_term t with
614
| Var id -> aux_memoize_id id env s acc
616
Util.anomaly "Environ.assumption: does not expect a meta or an evar"
617
| Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) ->
618
((aux e1 env)**(aux e2 env)) s acc
619
| LetIn (_,e1,e2,e3) -> ((aux e1 env)**
623
| App (e1, e_array) -> ((aux e1 env)**
625
(fun e f -> (aux e env)**f)
628
| Case (_,e1,e2,e_array) -> ((aux e1 env)**
631
(fun e f -> (aux e env)**f)
634
| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
636
(fun e f -> (aux e env)**f)
637
e1_array identity2) **
639
(fun e f -> (aux e env)**f)
642
| Const kn -> aux_memoize_kn kn env s acc
643
| _ -> (s,acc) (* closed atomic types + rel *)
645
and add_id id env s acc =
646
(* a Var can be either a variable, or a "Let" definition.*)
647
match lookup_named id env with
649
(s,ContextObjectMap.add (Variable id) t acc)
650
| (_,Some bdy,_) -> aux bdy env s acc
652
and aux_memoize_id id env =
653
try_and_go (Variable id) (add_id id env)
655
and add_kn kn env s acc =
656
let cb = lookup_constant kn env in
659
match cb.Declarations.const_type with
660
| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
661
| NonPolymorphicType t -> t
663
(s,ContextObjectMap.add cst ctype acc)
666
if cb.Declarations.const_body <> None
667
&& (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
673
match cb.Declarations.const_body with
674
| None -> do_type (Axiom kn)
675
| Some body -> aux (Declarations.force body) env s acc
677
and aux_memoize_kn kn env =
678
try_and_go (Axiom kn) (add_kn kn env)
681
snd (aux t env (ContextObjectSet.empty) (ContextObjectMap.empty))
added
removed
kernel/environ.ml
