modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 77 insertions, 62 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 11923a3e24..8766467fce 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -40,7 +40,9 @@ let make_strength_2 () =
 
 (* Variables. *)
 
-type variable_declaration = constr * strength * bool
+type sticky = bool
+
+type variable_declaration = constr * strength * sticky
 
 let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 
@@ -49,10 +51,10 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,(id,(ty,_,_) as vd)) = 
+let cache_variable (sp,(id,(ty,_,_) as vd,imps)) = 
   Global.push_var (id,ty);
   Nametab.push id sp;
-  declare_var_implicits id;
+  if imps then declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
 
 let load_variable _ = anomaly "we shouldn't load a variable"
@@ -70,34 +72,36 @@ let (in_variable, out_variable) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
-let declare_variable id ((ty,_,_) as obj) =
-  let _ = add_leaf id CCI (in_variable (id,obj)) in
+let declare_variable id obj =
+  let _ = add_leaf id CCI (in_variable ((id,obj),is_implicit_args())) in
   ()
 
 (* Parameters. *)
 
-let cache_parameter (sp,c) =
+let cache_parameter (sp,(c,imps)) =
   Global.add_parameter sp c;
   Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  if imps then declare_constant_implicits sp
+
+let load_parameter (sp,(_,imps)) =
+  if imps then declare_constant_implicits sp
 
 let open_parameter (sp,_) =
-  Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  Nametab.push (basename sp) sp
 
 let specification_parameter obj = obj
 
 let (in_parameter, out_parameter) =
   let od = {
     cache_function = cache_parameter;
-    load_function = (fun _ -> ());
+    load_function = load_parameter;
     open_function = open_parameter;
     specification_function = specification_parameter } 
   in
   declare_object ("PARAMETER", od)
 
 let declare_parameter id c =
-  let _ = add_leaf id CCI (in_parameter c) in ()
+  let _ = add_leaf id CCI (in_parameter (c,is_implicit_args())) in ()
 
 (* Constants. *)
 
@@ -110,14 +114,14 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
 	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
 
-let cache_constant (sp,((ce,_) as cd)) =
+let cache_constant (sp,((ce,_) as cd,imps)) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
-  declare_constant_implicits sp;
+  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
-let load_constant (sp,((ce,_) as cd)) =
-  declare_constant_implicits sp;
+let load_constant (sp,((ce,_) as cd,imps)) =
+  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
 let open_constant (sp,_) =
@@ -135,7 +139,7 @@ let (in_constant, out_constant) =
   declare_object ("CONSTANT", od)
 
 let declare_constant id cd =
-  let _ = add_leaf id CCI (in_constant cd) in ()
+  let _ = add_leaf id CCI (in_constant (cd,is_implicit_args())) in ()
 
  
 (* Inductives. *)
@@ -147,15 +151,15 @@ let push_inductive_names sp mie =
        List.iter (fun x -> Nametab.push x sp) cnames)
     mie.mind_entry_inds
 
-let cache_inductive (sp,mie) =
+let cache_inductive (sp,(mie,imps)) =
   Global.add_mind sp mie;
   push_inductive_names sp mie;
-  declare_inductive_implicits sp
+  if imps then declare_inductive_implicits sp
 
-let load_inductive (sp,_) =
-  declare_inductive_implicits sp
+let load_inductive (sp,(_,imps)) =
+  if imps then declare_inductive_implicits sp
 
-let open_inductive (sp,mie) =
+let open_inductive (sp,(mie,_)) =
   push_inductive_names sp mie
 
 let specification_inductive obj = obj
@@ -163,7 +167,7 @@ let specification_inductive obj = obj
 let (in_inductive, out_inductive) =
   let od = {
     cache_function = cache_inductive;
-    load_function = (fun _ -> ());
+    load_function = load_inductive;
     open_function = open_inductive;
     specification_function = specification_inductive } 
   in
@@ -174,7 +178,7 @@ let declare_mind mie =
     | (id,_,_,_)::_ -> id
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let sp = add_leaf id CCI (in_inductive mie) in
+  let sp = add_leaf id CCI (in_inductive (mie,is_implicit_args())) in
   sp
 
 
@@ -297,7 +301,7 @@ let declare_eliminations sp i =
     declare_constant (id_of_string na)
       ({ const_entry_body = Cooked c; const_entry_type = None }, 
        NeverDischarge);
-    pPNL [< 'sTR na; 'sTR " is defined" >]
+    if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
   let sigma = Evd.empty in
diff --git a/library/declare.mli b/library/declare.mli
index 15722dbc0a..c4644b4654 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,7 +20,9 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
-type variable_declaration = constr * strength * bool
+type sticky = bool
+
+type variable_declaration = constr * strength * sticky
 val declare_variable : identifier -> variable_declaration -> unit
 
 type constant_declaration = constant_entry * strength
@@ -43,7 +45,8 @@ val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : section_path -> identifier * typed_type * strength * bool
+val out_variable : 
+  section_path -> identifier * typed_type * strength * sticky
 val variable_strength : identifier -> strength
 
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 8198732826..1a9b741c42 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -31,11 +31,8 @@ let implicitely f x =
   end
 
 let auto_implicits ty =
-  if !implicit_args then
-    let genv = Global.env() in
-    Impl_auto (poly_args genv Evd.empty ty)
-  else
-    No_impl
+  let genv = Global.env() in
+  Impl_auto (poly_args genv Evd.empty ty)
 
 let list_of_implicits = function 
   | Impl_auto l -> l
@@ -55,7 +52,10 @@ let declare_constant_manual_implicits sp imps =
   constants_table := Spmap.add sp (Impl_manual imps) !constants_table
 
 let constant_implicits sp =
-  Spmap.find sp !constants_table
+  try Spmap.find sp !constants_table with Not_found -> No_impl
+
+let constant_implicits_list sp =
+  list_of_implicits (constant_implicits sp)
 
 (* Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -75,12 +75,16 @@ let declare_inductive_implicits sp =
   inductives_table := Spmap.add sp imps !inductives_table
     
 let inductive_implicits (sp,i) =
-  let imps = Spmap.find sp !inductives_table in
-  fst imps.(i)
+  try
+    let imps = Spmap.find sp !inductives_table in fst imps.(i)
+  with Not_found -> 
+    No_impl
 
 let constructor_implicits ((sp,i),j) =
-  let imps = Spmap.find sp !inductives_table in
-  (snd imps.(i)).(pred j)
+  try
+    let imps = Spmap.find sp !inductives_table in (snd imps.(i)).(pred j)
+  with Not_found -> 
+    No_impl
 
 let constructor_implicits_list constr_sp = 
   list_of_implicits (constructor_implicits constr_sp)
@@ -88,9 +92,6 @@ let constructor_implicits_list constr_sp =
 let inductive_implicits_list ind_sp =
   list_of_implicits (inductive_implicits ind_sp)
 
-let constant_implicits_list sp =
-  list_of_implicits (constant_implicits sp)
-
 (* Variables. *)
 
 let var_table = ref Idmap.empty
@@ -101,11 +102,12 @@ let declare_var_implicits id =
   var_table := Idmap.add id imps !var_table
 
 let implicits_of_var _ id =
-  list_of_implicits (Idmap.find id !var_table)
+  list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
 
 (* Registration as global tables and roolback. *)
 
-type frozen_t = implicits Spmap.t 
+type frozen_t = bool
+              * implicits Spmap.t 
               * (implicits * implicits array) array Spmap.t 
               * implicits Idmap.t
 
@@ -115,9 +117,10 @@ let init () =
   var_table := Idmap.empty
 
 let freeze () =
-  !constants_table, !inductives_table, !var_table
+  (!implicit_args,!constants_table, !inductives_table, !var_table)
 
-let unfreeze (ct,it,vt) =
+let unfreeze (imps,ct,it,vt) =
+  implicit_args := imps;
   constants_table := ct;
   inductives_table := it;
   var_table := vt
diff --git a/library/lib.ml b/library/lib.ml
index f79c22c58c..a6686168da 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,12 +8,13 @@ open Summary
 
 type node = 
   | Leaf of obj
+  | Module of string
   | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
-and library_segment = (section_path * node) list
+and library_entry = section_path * node
 
-type library_entry = section_path * node
+and library_segment = library_entry list
 
 
 (* We keep trace of operations in the stack [lib_stk]. 
@@ -109,13 +110,15 @@ let check_for_module () =
   let is_decl = function (_,FrozenState _) -> false | _ -> true in
   try
     let _ = find_entry_p is_decl in
-    error "a module can not be opened after some declarations"
+    error "a module can not be started after some declarations"
   with Not_found -> ()
 
-let open_module s =
-  if !module_name <> None then error "a module is already opened";
-  check_for_module ();
-  module_name := Some s
+let start_module s =
+  if !module_name <> None then error "a module is already started";
+  if !path_prefix <> [] then error "some sections are already opened";
+  module_name := Some s;
+  let _ = add_anonymous_entry (Module s) in
+  path_prefix := [s]
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
@@ -135,15 +138,16 @@ let close_section s =
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
-   closed sections and frozen states are removed. *)
+   frozen states are removed. *)
 
 let export_module () =
   if !module_name = None then error "no module declared";
   let rec export acc = function
-    | [] -> acc
+    | (_,Module _) :: _ -> acc
     | (_,Leaf _) as node :: stk -> export (node::acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,FrozenState _) :: stk -> export acc stk
+    | _ -> assert false
   in
   export [] !lib_stk
 
diff --git a/library/lib.mli b/library/lib.mli
index 2fe172f9f6..36b49bbeb2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,12 +13,13 @@ open Summary
 
 type node = 
   | Leaf of obj
+  | Module of string
   | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
-and library_segment = (section_path * node) list
+and library_entry = section_path * node
 
-type library_entry = section_path * node
+and library_segment = library_entry list
 
 
 (*s Adding operations (which calls the [cache] method, and getting the
@@ -39,7 +40,7 @@ val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
 val is_section_p : section_path -> bool
 
-val open_module : string -> unit
+val start_module : string -> unit
 val export_module : unit -> library_segment
 
 
diff --git a/library/library.ml b/library/library.ml
index cbd4789532..913f396d94 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -63,7 +63,7 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | _,FrozenState _ -> ()
+    | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
   in
@@ -91,8 +91,8 @@ let load_objects decls =
 
 let rec load_module_from doexp s f =
   let (fname,ch) = raw_intern_module f in
-  let md = input_value ch in
-  let digest = input_value ch in
+  let md = System.marshal_in ch in
+  let digest = System.marshal_in ch in
   close_in ch;
   let m = { module_name = md.md_name;
 	    module_compiled_env = md.md_compiled_env;
@@ -151,11 +151,11 @@ let save_module_to s f =
     md_compiled_env = Global.export s;
     md_declarations = seg;
     md_deps = current_imports () } in
-  let (_,ch) = raw_extern_module f in
-  output_value ch md;
+  let (f',ch) = raw_extern_module f in
+  System.marshal_out ch md;
   flush ch;
-  let di = Digest.file f in
-  output_value ch di;
+  let di = Digest.file f' in
+  System.marshal_out ch di;
   close_out ch