Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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 ())