summaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml233
1 files changed, 171 insertions, 62 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 4a4e90c1..ce3d2520 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml 10269 2007-10-29 11:09:43Z notin $ *)
+(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *)
open Pp
open Util
@@ -22,9 +22,11 @@ type node =
| Leaf of obj
| CompilingLibrary of object_prefix
| OpenedModule of bool option * object_prefix * Summary.frozen
+ | ClosedModule of library_segment
| OpenedModtype of object_prefix * Summary.frozen
+ | ClosedModtype of library_segment
| OpenedSection of object_prefix * Summary.frozen
- | ClosedSection
+ | ClosedSection of library_segment
| FrozenState of Summary.frozen
and library_entry = object_name * node
@@ -60,7 +62,11 @@ let classify_segment seg =
clean ((id,o')::substl, keepl, anticipl) stk
| Anticipate o' ->
clean (substl, keepl, o'::anticipl) stk)
- | (oname,ClosedSection) :: stk -> clean acc stk
+ | (_,ClosedSection _) :: stk -> clean acc stk
+ (* LEM; TODO: Understand what this does and see if what I do is the
+ correct thing for ClosedMod(ule|type) *)
+ | (_,ClosedModule _) :: stk -> clean acc stk
+ | (_,ClosedModtype _) :: stk -> clean acc stk
| (_,OpenedSection _) :: _ -> error "there are still opened sections"
| (_,OpenedModule _) :: _ -> error "there are still opened modules"
| (_,OpenedModtype _) :: _ -> error "there are still opened module types"
@@ -92,11 +98,15 @@ let library_dp () =
module path and relative section path *)
let path_prefix = ref initial_prefix
-
let cwd () = fst !path_prefix
let make_path id = Libnames.make_path (cwd ()) id
+let path_of_include () =
+ let dir = Names.repr_dirpath (cwd ()) in
+ let new_dir = List.tl dir in
+ let id = List.hd dir in
+ Libnames.make_path (Names.make_dirpath new_dir) id
let current_prefix () = snd !path_prefix
@@ -150,18 +160,32 @@ let find_split_p p =
in
find !lib_stk
-let split_lib sp =
+let split_lib_gen test =
let rec collect after equal = function
- | ((sp',_) as hd)::before ->
- if sp = sp' then collect after (hd::equal) before else after,equal,hd::before
- | [] -> after,equal,[]
+ | hd::strict_before as before ->
+ if test hd then collect after (hd::equal) strict_before else after,equal,before
+ | [] as before -> after,equal,before
in
let rec findeq after = function
- | ((sp',_) as hd)::before ->
- if sp = sp' then collect after [hd] before else findeq (hd::after) before
- | [] -> error "no such entry"
- in
- findeq [] !lib_stk
+ | hd :: before ->
+ if test hd
+ then Some (collect after [hd] before)
+ else (match hd with
+ | (sp,ClosedModule seg)
+ | (sp,ClosedModtype seg)
+ | (sp,ClosedSection seg) ->
+ (match findeq after seg with
+ | None -> findeq (hd::after) before
+ | Some (sub_after,sub_equal,sub_before) ->
+ Some (sub_after, sub_equal, (List.append sub_before before)))
+ | _ -> findeq (hd::after) before)
+ | [] -> None
+ in
+ match findeq [] !lib_stk with
+ | None -> error "no such entry"
+ | Some r -> r
+
+let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
(* Adding operations. *)
@@ -190,9 +214,9 @@ let add_leaf id obj =
add_entry oname (Leaf obj);
oname
-let add_discharged_leaf id obj =
+let add_discharged_leaf id varinfo obj =
let oname = make_oname id in
- let newobj = rebuild_object obj in
+ let newobj = rebuild_object (varinfo, obj) in
cache_object (oname,newobj);
add_entry oname (Leaf newobj)
@@ -216,12 +240,25 @@ let add_frozen_state () =
(* Modules. *)
+
let is_something_opened = function
(_,OpenedSection _) -> true
| (_,OpenedModule _) -> true
| (_,OpenedModtype _) -> true
| _ -> false
+
+let current_mod_id () =
+ try match find_entry_p is_something_opened with
+ | oname,OpenedModule (_,_,nametab) ->
+ basename (fst oname)
+ | oname,OpenedModtype (_,nametab) ->
+ basename (fst oname)
+ | _ -> error "you are not in a module"
+ with Not_found ->
+ error "no opened modules"
+
+
let start_module export id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
let prefix = dir,(mp,empty_dirpath) in
@@ -253,9 +290,15 @@ let end_module id =
with Not_found ->
error "no opened modules"
in
- let (after,_,before) = split_lib oname in
+ let (after,modopening,before) = split_lib oname in
lib_stk := before;
+ add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
let prefix = !path_prefix in
+ (* LEM: This module business seems more complicated than sections;
+ shouldn't a backtrack into a closed module also do something
+ with global.ml, given that closing a module does?
+ TODO
+ *)
recalc_path_prefix ();
(* add_frozen_state must be called after processing the module,
because we cannot recache interactive modules *)
@@ -292,8 +335,9 @@ let end_modtype id =
with Not_found ->
error "no opened module types"
in
- let (after,_,before) = split_lib sp in
+ let (after,modtypeopening,before) = split_lib sp in
lib_stk := before;
+ add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
let dir = !path_prefix in
recalc_path_prefix ();
(* add_frozen_state must be called after processing the module type.
@@ -396,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened
type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
let sectab =
- ref ([] : (identifier list * Cooking.work_list * abstr_list) list)
+ ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
let add_section () =
sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
-let add_section_variable id =
+let add_section_variable id impl keep =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+ | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
let rec extract_hyps = function
- | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+ | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
| (id::idl,hyps) -> extract_hyps (idl,hyps)
| [], _ -> []
@@ -429,6 +474,8 @@ let add_section_constant kn =
let replacement_context () = pi2 (List.hd !sectab)
+let variables_context () = pi1 (List.hd !sectab)
+
let section_segment_of_constant con =
Cmap.find con (fst (pi3 (List.hd !sectab)))
@@ -442,15 +489,15 @@ let section_instance = function
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
KNmap.find kn (snd (pi2 (List.hd !sectab)))
-let init () = sectab := []
-let freeze () = !sectab
-let unfreeze s = sectab := s
+let init_sectab () = sectab := []
+let freeze_sectab () = !sectab
+let unfreeze_sectab s = sectab := s
let _ =
Summary.declare_summary "section-context"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init;
+ { Summary.freeze_function = freeze_sectab;
+ Summary.unfreeze_function = unfreeze_sectab;
+ Summary.init_function = init_sectab;
Summary.survive_module = false;
Summary.survive_section = false }
@@ -476,7 +523,7 @@ let open_section id =
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
path_prefix := prefix;
- if !Options.xml_export then !xml_open_section id;
+ if !Flags.xml_export then !xml_open_section id;
add_section ()
@@ -486,9 +533,9 @@ let open_section id =
let discharge_item ((sp,_ as oname),e) =
match e with
| Leaf lobj ->
- option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
| FrozenState _ -> None
- | ClosedSection -> None
+ | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
anomaly "discharge_item"
@@ -504,21 +551,29 @@ let close_section id =
with Not_found ->
error "no opened section"
in
- let (secdecls,_,before) = split_lib oname in
+ let var_info = List.map
+ (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
+ (variables_context ())
+ in
+ let (secdecls,secopening,before) = split_lib oname in
lib_stk := before;
let full_olddir = fst !path_prefix in
pop_path_prefix ();
- add_entry (make_oname id) ClosedSection;
- if !Options.xml_export then !xml_close_section id;
+ add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening)));
+ if !Flags.xml_export then !xml_close_section id;
let newdecls = List.map discharge_item secdecls in
Summary.section_unfreeze_summaries fs;
- List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
+ List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls;
Cooking.clear_cooking_sharing ();
Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
(*****************)
(* Backtracking. *)
+let (inLabel,outLabel) =
+ declare_object {(default_object "DOT") with
+ classify_function = (fun _ -> Dispose)}
+
let recache_decl = function
| (sp, Leaf o) -> cache_object (sp,o)
| (_,OpenedSection _) -> add_section ()
@@ -529,16 +584,58 @@ let recache_context ctx =
let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
-let reset_to sp =
- let (_,_,before) = split_lib sp in
- lib_stk := before;
+let has_top_frozen_state () =
+ let rec aux = function
+ | (sp, FrozenState _)::_ -> Some sp
+ | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
+ | _ -> None
+ in aux !lib_stk
+
+let set_lib_stk new_lib_stk =
+ lib_stk := new_lib_stk;
recalc_path_prefix ();
let spf = match find_entry_p is_frozen_state with
| (sp, FrozenState f) -> unfreeze_summaries f; sp
| _ -> assert false
in
let (after,_,_) = split_lib spf in
- recache_context after
+ try
+ recache_context after
+ with
+ | Not_found -> error "Tried to set environment to an incoherent state."
+
+let reset_to_gen test =
+ let (_,_,before) = split_lib_gen test in
+ set_lib_stk before
+
+let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
+
+let reset_to_state sp =
+ let (_,eq,before) = split_lib sp in
+ (* if eq a frozen state, we'll reset to it *)
+ match eq with
+ | [_,FrozenState f] -> lib_stk := eq@before; unfreeze_summaries f
+ | _ -> error "Not a frozen state"
+
+
+(* LEM: TODO
+ * We will need to muck with frozen states in after, too!
+ * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype)
+ *)
+let delete_gen test =
+ let (after,equal,before) = split_lib_gen test in
+ let rec chop_at_dot = function
+ | [] as l -> l
+ | (_, Leaf o)::t when object_tag o = "DOT" -> t
+ | _::t -> chop_at_dot t
+ and chop_before_dot = function
+ | [] as l -> l
+ | (_, Leaf o)::t as l when object_tag o = "DOT" -> l
+ | _::t -> chop_before_dot t
+ in
+ set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
+
+let delete sp = delete_gen (fun x -> (fst x) = sp)
let reset_name (loc,id) =
let (sp,_) =
@@ -549,10 +646,20 @@ let reset_name (loc,id) =
in
reset_to sp
+let remove_name (loc,id) =
+ let (sp,_) =
+ try
+ find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
+ with Not_found ->
+ user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
+ in
+ delete sp
+
let is_mod_node = function
| OpenedModule _ | OpenedModtype _ | OpenedSection _
- | ClosedSection -> true
- | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+ | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true
+ | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+ || t = "MODULE ALIAS"
| _ -> false
(* Reset on a module or section name in order to bypass constants with
@@ -567,19 +674,7 @@ let reset_mod (loc,id) =
with Not_found ->
user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
in
- lib_stk := before;
- recalc_path_prefix ();
- let spf = match find_entry_p is_frozen_state with
- | (sp, FrozenState f) -> unfreeze_summaries f; sp
- | _ -> assert false
- in
- let (after,_,_) = split_lib spf in
- recache_context after
-
-
-let (inLabel,outLabel) =
- declare_object {(default_object "DOT") with
- classify_function = (fun _ -> Dispose)}
+ set_lib_stk before
let mark_end_of_command, current_command_label, set_command_label =
let n = ref 0 in
@@ -590,17 +685,23 @@ let mark_end_of_command, current_command_label, set_command_label =
(fun () -> !n),
(fun x -> n:=x)
-let rec reset_label_stk n stk =
- match stk with
- (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp
- | _::tail -> reset_label_stk n tail
- | [] -> error "Unknown state number"
+let is_label_n n x =
+ match x with
+ | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
+ | _ -> false
+(* Reset the label registered by [mark_end_of_command()] with number n. *)
let reset_label n =
- let res = reset_label_stk n !lib_stk in
- set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
- reset_to res
-
+ let current = current_command_label() in
+ if n < current then
+ let res = reset_to_gen (is_label_n n) in
+ set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
+ res
+ else (* optimisation to avoid recaching when not necessary (why is it so long??) *)
+ match !lib_stk with
+ | [] -> ()
+ | x :: ls -> (lib_stk := ls;set_command_label (n-1))
+
let rec back_stk n stk =
match stk with
(sp,Leaf o)::tail when object_tag o = "DOT" ->
@@ -688,6 +789,14 @@ let remove_section_part ref =
(************************)
(* Discharging names *)
+let pop_kn kn =
+ let (mp,dir,l) = Names.repr_kn kn in
+ Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con =
+ let (mp,dir,l) = Names.repr_con con in
+ Names.make_con mp (dirpath_prefix dir) l
+
let con_defined_in_sec kn =
let _,dir,_ = repr_con kn in
dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 03:57:26 +0000