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: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
22
| CompilingLibrary of object_prefix
23
| OpenedModule of bool option * object_prefix * Summary.frozen
24
| ClosedModule of library_segment
25
| OpenedModtype of object_prefix * Summary.frozen
26
| ClosedModtype of library_segment
27
| OpenedSection of object_prefix * Summary.frozen
28
| ClosedSection of library_segment
29
| FrozenState of Summary.frozen
31
and library_entry = object_name * node
33
and library_segment = library_entry list
35
type lib_objects = (Names.identifier * obj) list
37
let iter_objects f i prefix =
38
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
40
let load_objects = iter_objects load_object
41
let open_objects = iter_objects open_object
43
let subst_objects prefix subst seg =
44
let subst_one = fun (id,obj as node) ->
45
let obj' = subst_object (make_oname prefix id, subst, obj) in
46
if obj' == obj then node else
49
list_smartmap subst_one seg
51
let load_and_subst_objects i prefix subst seg =
52
List.rev (List.fold_left (fun seg (id,obj as node) ->
53
let obj' = subst_object (make_oname prefix id, subst, obj) in
54
let node = if obj == obj' then node else (id, obj') in
55
load_object i (make_oname prefix id, obj');
58
let classify_segment seg =
59
let rec clean ((substl,keepl,anticipl) as acc) = function
60
| (_,CompilingLibrary _) :: _ | [] -> acc
61
| ((sp,kn as oname),Leaf o) :: stk ->
62
let id = Names.id_of_label (Names.label kn) in
63
(match classify_object (oname,o) with
64
| Dispose -> clean acc stk
66
clean (substl, (id,o')::keepl, anticipl) stk
68
clean ((id,o')::substl, keepl, anticipl) stk
70
clean (substl, keepl, o'::anticipl) stk)
71
| (_,ClosedSection _) :: stk -> clean acc stk
72
(* LEM; TODO: Understand what this does and see if what I do is the
73
correct thing for ClosedMod(ule|type) *)
74
| (_,ClosedModule _) :: stk -> clean acc stk
75
| (_,ClosedModtype _) :: stk -> clean acc stk
76
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
77
| (_,OpenedModule _) :: _ -> error "there are still opened modules"
78
| (_,OpenedModtype _) :: _ -> error "there are still opened module types"
79
| (_,FrozenState _) :: stk -> clean acc stk
81
clean ([],[],[]) (List.rev seg)
84
let segment_of_objects prefix =
85
List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj))
87
(* We keep trace of operations in the stack [lib_stk].
88
[path_prefix] is the current path of sections, where sections are stored in
89
``correct'' order, the oldest coming first in the list. It may seems
90
costly, but in practice there is not so many openings and closings of
91
sections, but on the contrary there are many constructions of section
92
paths based on the library path. *)
94
let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
96
let lib_stk = ref ([] : library_segment)
98
let comp_name = ref None
101
match !comp_name with Some m -> m | None -> default_library
103
(* [path_prefix] is a pair of absolute dirpath and a pair of current
104
module path and relative section path *)
105
let path_prefix = ref initial_prefix
107
let sections_depth () =
108
List.length (Names.repr_dirpath (snd (snd !path_prefix)))
110
let sections_are_opened () =
111
match Names.repr_dirpath (snd (snd !path_prefix)) with
115
let cwd () = fst !path_prefix
117
let current_dirpath sec =
118
Libnames.drop_dirpath_prefix (library_dp ())
120
else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
122
let make_path id = Libnames.make_path (cwd ()) id
124
let path_of_include () =
125
let dir = Names.repr_dirpath (cwd ()) in
126
let new_dir = List.tl dir in
127
let id = List.hd dir in
128
Libnames.make_path (Names.make_dirpath new_dir) id
130
let current_prefix () = snd !path_prefix
133
let mp,dir = current_prefix () in
134
Names.make_kn mp dir (Names.label_of_id id)
137
let mp,dir = current_prefix () in
138
Names.make_con mp dir (Names.label_of_id id)
141
let make_oname id = make_path id, make_kn id
143
let recalc_path_prefix () =
144
let rec recalc = function
145
| (sp, OpenedSection (dir,_)) :: _ -> dir
146
| (sp, OpenedModule (_,dir,_)) :: _ -> dir
147
| (sp, OpenedModtype (dir,_)) :: _ -> dir
148
| (sp, CompilingLibrary dir) :: _ -> dir
150
| [] -> initial_prefix
152
path_prefix := recalc !lib_stk
154
let pop_path_prefix () =
155
let dir,(mp,sec) = !path_prefix in
156
path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
159
let rec find = function
160
| [] -> raise Not_found
161
| ent::l -> if p ent then ent else find l
166
let rec find = function
167
| [] -> raise Not_found
168
| ent::l -> if p ent then ent,l else find l
172
let split_lib_gen test =
173
let rec collect after equal = function
174
| hd::strict_before as before ->
175
if test hd then collect after (hd::equal) strict_before else after,equal,before
176
| [] as before -> after,equal,before
178
let rec findeq after = function
181
then Some (collect after [hd] before)
183
| (sp,ClosedModule seg)
184
| (sp,ClosedModtype seg)
185
| (sp,ClosedSection seg) ->
186
(match findeq after seg with
187
| None -> findeq (hd::after) before
188
| Some (sub_after,sub_equal,sub_before) ->
189
Some (sub_after, sub_equal, (List.append sub_before before)))
190
| _ -> findeq (hd::after) before)
193
match findeq [] !lib_stk with
194
| None -> error "no such entry"
197
let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
199
(* Adding operations. *)
201
let add_entry sp node =
202
lib_stk := (sp,node) :: !lib_stk
206
fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
208
let add_anonymous_entry node =
209
let id = anonymous_id () in
210
let name = make_oname id in
214
let add_absolutely_named_leaf sp obj =
215
cache_object (sp,obj);
216
add_entry sp (Leaf obj)
218
let add_leaf id obj =
219
if fst (current_prefix ()) = Names.initial_path then
220
error ("No session module started (use -top dir)");
221
let oname = make_oname id in
222
cache_object (oname,obj);
223
add_entry oname (Leaf obj);
226
let add_discharged_leaf id obj =
227
let oname = make_oname id in
228
let newobj = rebuild_object obj in
229
cache_object (oname,newobj);
230
add_entry oname (Leaf newobj)
232
let add_leaves id objs =
233
let oname = make_oname id in
235
add_entry oname (Leaf obj);
236
load_object 1 (oname,obj)
238
List.iter add_obj objs;
241
let add_anonymous_leaf obj =
242
let id = anonymous_id () in
243
let oname = make_oname id in
244
cache_object (oname,obj);
245
add_entry oname (Leaf obj)
247
let add_frozen_state () =
248
let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
253
let is_something_opened = function
254
(_,OpenedSection _) -> true
255
| (_,OpenedModule _) -> true
256
| (_,OpenedModtype _) -> true
260
let current_mod_id () =
261
try match find_entry_p is_something_opened with
262
| oname,OpenedModule (_,_,nametab) ->
264
| oname,OpenedModtype (_,nametab) ->
266
| _ -> error "you are not in a module"
268
error "no opened modules"
271
let start_module export id mp nametab =
272
let dir = extend_dirpath (fst !path_prefix) id in
273
let prefix = dir,(mp,Names.empty_dirpath) in
274
let oname = make_path id, make_kn id in
275
if Nametab.exists_module dir then
276
errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
277
add_entry oname (OpenedModule (export,prefix,nametab));
278
path_prefix := prefix;
280
(* add_frozen_state () must be called in declaremods *)
284
try match find_entry_p is_something_opened with
285
| oname,OpenedModule (_,_,nametab) ->
286
let id' = basename (fst oname) in
288
errorlabstrm "end_module" (str "last opened module is " ++ pr_id id');
290
| oname,OpenedModtype _ ->
291
let id' = basename (fst oname) in
292
errorlabstrm "end_module"
293
(str "module type " ++ pr_id id' ++ str " is still opened")
294
| oname,OpenedSection _ ->
295
let id' = basename (fst oname) in
296
errorlabstrm "end_module"
297
(str "section " ++ pr_id id' ++ str " is still opened")
300
error "no opened modules"
302
let (after,modopening,before) = split_lib oname in
304
add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
305
let prefix = !path_prefix in
306
(* LEM: This module business seems more complicated than sections;
307
shouldn't a backtrack into a closed module also do something
308
with global.ml, given that closing a module does?
311
recalc_path_prefix ();
312
(* add_frozen_state must be called after processing the module,
313
because we cannot recache interactive modules *)
314
(oname, prefix, nametab,after)
316
let start_modtype id mp nametab =
317
let dir = extend_dirpath (fst !path_prefix) id in
318
let prefix = dir,(mp,Names.empty_dirpath) in
319
let sp = make_path id in
320
let name = sp, make_kn id in
321
if Nametab.exists_cci sp then
322
errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
323
add_entry name (OpenedModtype (prefix,nametab));
324
path_prefix := prefix;
329
try match find_entry_p is_something_opened with
330
| oname,OpenedModtype (_,nametab) ->
331
let id' = basename (fst oname) in
333
errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id');
335
| oname,OpenedModule _ ->
336
let id' = basename (fst oname) in
337
errorlabstrm "end_modtype"
338
(str "module " ++ pr_id id' ++ str " is still opened")
339
| oname,OpenedSection _ ->
340
let id' = basename (fst oname) in
341
errorlabstrm "end_modtype"
342
(str "section " ++ pr_id id' ++ str " is still opened")
345
error "no opened module types"
347
let (after,modtypeopening,before) = split_lib sp in
349
add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
350
let dir = !path_prefix in
351
recalc_path_prefix ();
352
(* add_frozen_state must be called after processing the module type.
353
This is because we cannot recache interactive module types *)
354
(sp,dir,nametab,after)
358
let contents_after = function
360
| Some sp -> let (after,_,_) = split_lib sp in after
364
let check_for_comp_unit () =
365
let is_decl = function (_,FrozenState _) -> false | _ -> true in
367
let _ = find_entry_p is_decl in
368
error "a module cannot be started after some declarations"
371
(* TODO: use check_for_module ? *)
372
let start_compilation s mp =
373
if !comp_name <> None then
374
error "compilation unit is already started";
375
if snd (snd (!path_prefix)) <> Names.empty_dirpath then
376
error "some sections are already opened";
377
let prefix = s, (mp, Names.empty_dirpath) in
378
let _ = add_anonymous_entry (CompilingLibrary prefix) in
380
path_prefix := prefix
382
let end_compilation dir =
384
try match find_entry_p is_something_opened with
385
| _, OpenedSection _ -> error "There are some open sections"
386
| _, OpenedModule _ -> error "There are some open modules"
387
| _, OpenedModtype _ -> error "There are some open module types"
393
function (_,CompilingLibrary _) -> true | x -> is_something_opened x
396
try match find_entry_p module_p with
397
(oname, CompilingLibrary prefix) -> oname
400
Not_found -> anomaly "No module declared"
403
match !comp_name with
404
| None -> anomaly "There should be a module name..."
406
if m <> dir then anomaly
407
("The current open module has name "^ (Names.string_of_dirpath m) ^
408
" and not " ^ (Names.string_of_dirpath m));
410
let (after,_,before) = split_lib oname in
414
(* Returns true if we are inside an opened module type *)
416
let opened_p = function
417
| _, OpenedModtype _ -> true
421
let _ = find_entry_p opened_p in true
425
(* Returns true if we are inside an opened module *)
427
let opened_p = function
428
| _, OpenedModule _ -> true
432
let _ = find_entry_p opened_p in true
437
(* Returns the most recent OpenedThing node *)
438
let what_is_opened () = find_entry_p is_something_opened
440
(* Discharge tables *)
442
(* At each level of section, we remember
443
- the list of variables in this section
444
- the list of variables on which each constant depends in this section
445
- the list of variables on which each inductive depends in this section
446
- the list of substitution to do at section closing
448
type binding_kind = Explicit | Implicit
450
type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
451
type variable_context = variable_info list
452
type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
455
ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
458
sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
460
let add_section_variable id impl keep =
462
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
463
| (vars,repl,abs)::sl ->
464
sectab := ((id,impl,keep)::vars,repl,abs)::sl
466
let extract_hyps (secs,ohyps) =
467
let rec aux = function
468
| ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
469
| ((id,impl,Some (ty,keep))::idl,hyps) ->
470
if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
471
(id,impl,None,ty) :: aux (idl,hyps)
473
| (id::idl,hyps) -> aux (idl,hyps)
477
let instance_from_variable_context sign =
478
let rec inst_rec = function
479
| (id,b,None,_) :: sign -> id :: inst_rec sign
480
| _ :: sign -> inst_rec sign
482
Array.of_list (inst_rec sign)
484
let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
486
let add_section_replacement f g hyps =
489
| (vars,exps,abs)::sl ->
490
let sechyps = extract_hyps (vars,hyps) in
491
let args = instance_from_variable_context (List.rev sechyps) in
492
sectab := (vars,f args exps,g sechyps abs)::sl
494
let add_section_kn kn =
495
let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
496
add_section_replacement f f
498
let add_section_constant kn =
499
let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
500
add_section_replacement f f
502
let replacement_context () = pi2 (List.hd !sectab)
504
let variables_context () = pi1 (List.hd !sectab)
506
let section_segment_of_constant con =
507
Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
509
let section_segment_of_mutual_inductive kn =
510
Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
512
let rec list_mem_assoc_in_triple x = function
513
[] -> raise Not_found
514
| (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
516
let section_instance = function
518
if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
521
Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
522
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
523
Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
525
let is_in_section ref =
526
try ignore (section_instance ref); true with Not_found -> false
528
let init_sectab () = sectab := []
529
let freeze_sectab () = !sectab
530
let unfreeze_sectab s = sectab := s
533
Summary.declare_summary "section-context"
534
{ Summary.freeze_function = freeze_sectab;
535
Summary.unfreeze_function = unfreeze_sectab;
536
Summary.init_function = init_sectab;
537
Summary.survive_module = false;
538
Summary.survive_section = false }
543
(* XML output hooks *)
544
let xml_open_section = ref (fun id -> ())
545
let xml_close_section = ref (fun id -> ())
547
let set_xml_open_section f = xml_open_section := f
548
let set_xml_close_section f = xml_close_section := f
550
let open_section id =
551
let olddir,(mp,oldsec) = !path_prefix in
552
let dir = extend_dirpath olddir id in
553
let prefix = dir, (mp, extend_dirpath oldsec id) in
554
let name = make_path id, make_kn id (* this makes little sense however *) in
555
if Nametab.exists_section dir then
556
errorlabstrm "open_section" (pr_id id ++ str " already exists");
557
let sum = freeze_summaries() in
558
add_entry name (OpenedSection (prefix, sum));
559
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
560
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
561
path_prefix := prefix;
562
if !Flags.xml_export then !xml_open_section id;
566
(* Restore lib_stk and summaries as before the section opening, and
567
add a ClosedSection object. *)
569
let discharge_item ((sp,_ as oname),e) =
572
Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
573
| FrozenState _ -> None
574
| ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None
575
| OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
576
anomaly "discharge_item"
578
let close_section id =
580
try match find_entry_p is_something_opened with
581
| oname,OpenedSection (_,fs) ->
582
let id' = basename (fst oname) in
584
errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
588
error "No opened section."
590
let (secdecls,secopening,before) = split_lib oname in
592
let full_olddir = fst !path_prefix in
594
add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening)));
595
if !Flags.xml_export then !xml_close_section id;
596
let newdecls = List.map discharge_item secdecls in
597
Summary.section_unfreeze_summaries fs;
598
List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
599
Cooking.clear_cooking_sharing ();
600
Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
605
let (inLabel,outLabel) =
606
declare_object {(default_object "DOT") with
607
classify_function = (fun _ -> Dispose)}
609
let recache_decl = function
610
| (sp, Leaf o) -> cache_object (sp,o)
611
| (_,OpenedSection _) -> add_section ()
614
let recache_context ctx =
615
List.iter recache_decl ctx
617
let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
619
let has_top_frozen_state () =
620
let rec aux = function
621
| (sp, FrozenState _)::_ -> Some sp
622
| (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
626
let set_lib_stk new_lib_stk =
627
lib_stk := new_lib_stk;
628
recalc_path_prefix ();
629
let spf = match find_entry_p is_frozen_state with
630
| (sp, FrozenState f) -> unfreeze_summaries f; sp
633
let (after,_,_) = split_lib spf in
635
recache_context after
637
| Not_found -> error "Tried to set environment to an incoherent state."
639
let reset_to_gen test =
640
let (_,_,before) = split_lib_gen test in
643
let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
645
let reset_to_state sp =
646
let (_,eq,before) = split_lib sp in
647
(* if eq a frozen state, we'll reset to it *)
649
| [_,FrozenState f] -> lib_stk := eq@before; unfreeze_summaries f
650
| _ -> error "Not a frozen state"
654
* We will need to muck with frozen states in after, too!
655
* Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype)
657
let delete_gen test =
658
let (after,equal,before) = split_lib_gen test in
659
let rec chop_at_dot = function
661
| (_, Leaf o)::t when object_tag o = "DOT" -> t
662
| _::t -> chop_at_dot t
663
and chop_before_dot = function
665
| (_, Leaf o)::t as l when object_tag o = "DOT" -> l
666
| _::t -> chop_before_dot t
668
set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
670
let delete sp = delete_gen (fun x -> (fst x) = sp)
672
let reset_name (loc,id) =
675
find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
677
user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
681
let remove_name (loc,id) =
684
find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
686
user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
690
let is_mod_node = function
691
| OpenedModule _ | OpenedModtype _ | OpenedSection _
692
| ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true
693
| Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
694
|| t = "MODULE ALIAS"
697
(* Reset on a module or section name in order to bypass constants with
700
let reset_mod (loc,id) =
703
find_split_p (fun (sp,node) ->
704
let (_,spi) = repr_path (fst sp) in id = spi
707
user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
711
let mark_end_of_command, current_command_label, set_command_label =
715
(_,Leaf o)::_ when object_tag o = "DOT" -> ()
716
| _ -> incr n;add_anonymous_leaf (inLabel !n)),
722
| (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
725
(* Reset the label registered by [mark_end_of_command()] with number n. *)
727
let current = current_command_label() in
729
let res = reset_to_gen (is_label_n n) in
730
set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
732
else (* optimisation to avoid recaching when not necessary (why is it so long??) *)
735
| x :: ls -> (lib_stk := ls;set_command_label (n-1))
737
let rec back_stk n stk =
739
(sp,Leaf o)::tail when object_tag o = "DOT" ->
740
if n=0 then sp else back_stk (n-1) tail
741
| _::tail -> back_stk n tail
742
| [] -> error "Reached begin of command history"
744
let back n = reset_to (back_stk n !lib_stk)
746
(* State and initialization. *)
748
type frozen = Names.dir_path option * library_segment
750
let freeze () = (!comp_name, !lib_stk)
752
let unfreeze (mn,stk) =
755
recalc_path_prefix ()
761
path_prefix := initial_prefix;
766
let initial_state = ref None
768
let declare_initial_state () =
769
let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
770
initial_state := Some name
772
let reset_initial () =
773
match !initial_state with
775
error "Resetting to the initial state is possible only interactively"
777
begin match split_lib sp with
778
| (_,[_,FrozenState fs as hd],before) ->
779
lib_stk := hd::before;
780
recalc_path_prefix ();
782
unfreeze_summaries fs
789
let mp_of_global ref =
791
| VarRef id -> fst (current_prefix ())
792
| ConstRef cst -> Names.con_modpath cst
793
| IndRef ind -> Names.ind_modpath ind
794
| ConstructRef constr -> Names.constr_modpath constr
796
let rec dp_of_mp modp =
798
| Names.MPfile dp -> dp
799
| Names.MPbound _ | Names.MPself _ -> library_dp ()
800
| Names.MPdot (mp,_) -> dp_of_mp mp
802
let rec split_mp mp =
804
| Names.MPfile dp -> dp, Names.empty_dirpath
805
| Names.MPdot (prfx, lbl) ->
806
let mprec, dprec = split_mp prfx in
807
mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
808
| Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id]
809
| Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id]
811
let split_modpath mp =
812
let rec aux = function
813
| Names.MPfile dp -> dp, []
814
| Names.MPbound mbid ->
815
library_dp (), [Names.id_of_mbid mbid]
816
| Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
817
| Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
818
(mp', Names.id_of_label l :: lab)
820
let (mp, l) = aux mp in
823
let library_part ref =
825
| VarRef id -> library_dp ()
826
| _ -> dp_of_mp (mp_of_global ref)
828
let remove_section_part ref =
829
let sp = Nametab.sp_of_global ref in
830
let dir,_ = repr_path sp in
833
anomaly "remove_section_part not supported on local variables"
835
if is_dirpath_prefix_of dir (cwd ()) then
836
(* Not yet (fully) discharged *)
837
extract_dirpath_prefix (sections_depth ()) (cwd ())
839
(* Theorem/Lemma outside its outer section of definition *)
842
(************************)
843
(* Discharging names *)
846
let (mp,dir,l) = Names.repr_kn kn in
847
Names.make_kn mp (dirpath_prefix dir) l
850
let (mp,dir,l) = Names.repr_con con in
851
Names.make_con mp (dirpath_prefix dir) l
853
let con_defined_in_sec kn =
854
let _,dir,_ = Names.repr_con kn in
855
dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
857
let defined_in_sec kn =
858
let _,dir,_ = Names.repr_kn kn in
859
dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
861
let discharge_global = function
862
| ConstRef kn when con_defined_in_sec kn ->
863
ConstRef (pop_con kn)
864
| IndRef (kn,i) when defined_in_sec kn ->
866
| ConstructRef ((kn,i),j) when defined_in_sec kn ->
867
ConstructRef ((pop_kn kn,i),j)
870
let discharge_kn kn =
871
if defined_in_sec kn then pop_kn kn else kn
873
let discharge_con cst =
874
if con_defined_in_sec cst then pop_con cst else cst
876
let discharge_inductive (kn,i) =
added
removed
library/lib.ml
