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

1 files changed, 34 insertions, 17 deletions

diff --git a/library/lib.ml b/library/lib.ml
index ce3d2520..fa71bb2f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *)
+(* $Id: lib.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Pp
 open Util
@@ -214,9 +214,9 @@ let add_leaf id obj =
   add_entry oname (Leaf obj);
   oname
 
-let add_discharged_leaf id varinfo obj =
+let add_discharged_leaf id obj =
   let oname = make_oname id in
-  let newobj = rebuild_object (varinfo, obj) in
+  let newobj = rebuild_object obj in
   cache_object (oname,newobj);
   add_entry oname (Leaf newobj)
 
@@ -436,11 +436,14 @@ let what_is_opened () = find_entry_p is_something_opened
    - the list of variables on which each inductive depends in this section
    - the list of substitution to do at section closing 
 *)
+type binding_kind = Explicit | Implicit
 
-type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
+type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
@@ -451,25 +454,34 @@ let add_section_variable id impl keep =
     | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
 let rec extract_hyps = function
-  | ((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,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
+  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
   | (id::idl,hyps) -> extract_hyps (idl,hyps)
   | [], _ -> []
 
+let instance_from_variable_context sign =
+  let rec inst_rec = function
+    | (id,b,None,_) :: sign -> id :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
+
+let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
+
 let add_section_replacement f g hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
     let sechyps = extract_hyps (vars,hyps) in
-    let args = Sign.instance_from_named_context (List.rev sechyps) in
-    sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+    let args = instance_from_variable_context (List.rev sechyps) in
+    sectab := (vars,f args exps,g sechyps abs)::sl
 	
 let add_section_kn kn =
-  let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+  let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
   add_section_replacement f f
 
 let add_section_constant kn =
-  let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
   add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
@@ -482,13 +494,22 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
+let rec list_mem_assoc_in_triple x = function
+    [] -> raise Not_found
+  | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
+
 let section_instance = function
-  | VarRef id -> [||]
+  | VarRef id ->
+      if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
+      else raise Not_found
   | ConstRef con ->
       Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
+let is_in_section ref =
+  try ignore (section_instance ref); true with Not_found -> false
+
 let init_sectab () = sectab := []
 let freeze_sectab () = !sectab
 let unfreeze_sectab s = sectab := s
@@ -551,10 +572,6 @@ let close_section id =
     with Not_found ->
       error "no opened section"
   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
@@ -563,7 +580,7 @@ let close_section id =
   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 var_info o)) newdecls;
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
   Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)