doc of coqchk + improved module cache and computation of module sets

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

2 files changed, 54 insertions, 159 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 7169d709f5..f8844975ac 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -70,6 +70,7 @@ module LibraryOrdered =
         (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
   end
 
+module LibrarySet = Set.Make(LibraryOrdered)
 module LibraryMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
@@ -100,7 +101,7 @@ let check_one_lib admit (dir,m) =
   (* Look up if the library is to be admitted correct. We could
      also check if it carries a validation certificate (yet to
      be implemented). *)
-  if LibraryMap.mem dir admit then
+  if LibrarySet.mem dir admit then
     (Flags.if_verbose msgnl
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md dig)
@@ -200,7 +201,6 @@ let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 exception LibUnmappedDir
 exception LibNotFound
-type library_location = LibLoaded | LibInPath
 
 let locate_absolute_library dir =
   (* Search in loadpath *)
@@ -234,9 +234,9 @@ let locate_qualified_library qid =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)
     try 
-      (LibLoaded, dir, library_full_filename dir)      
+      (dir, library_full_filename dir)      
     with Not_found ->
-      (LibInPath, dir, file)
+      (dir, file)
   with Not_found -> raise LibNotFound
 
 let explain_locate_library_error qid = function
@@ -258,8 +258,7 @@ let try_locate_absolute_library dir =
 
 let try_locate_qualified_library qid =
   try
-    let (_,dir,f) = locate_qualified_library qid in
-    dir,f
+    locate_qualified_library qid
   with e -> 
     explain_locate_library_error qid e
 
@@ -291,7 +290,15 @@ let mk_library md f digest = {
   library_deps = md.md_deps;
   library_digest = digest }
 
-let intern_from_file f =
+let name_clash_message dir mdir f =
+  str ("The file " ^ f ^ " contains library") ++ spc () ++
+  pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
+  pr_dirpath dir
+
+(* Dependency graph *)
+let depgraph = ref LibraryMap.empty
+
+let intern_from_file (dir, f) =
   Flags.if_verbose msg (str"[intern "++str f++str" ...");
   let (md,digest) = 
     try
@@ -299,60 +306,67 @@ let intern_from_file f =
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
       close_in ch;
+      if dir <> md.md_name then
+        errorlabstrm "load_physical_library"
+          (name_clash_message dir md.md_name f);
       Flags.if_verbose msgnl(str" done]");
       md,digest
     with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+  depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; 
   mk_library md f digest
 
-
-let name_clash_message dir mdir f =
-  str ("The file " ^ f ^ " contains library") ++ spc () ++
-  pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
-  pr_dirpath dir
-
-let rec library_dep dir needed =
-  try let _ = find_library dir in needed
+let get_deps (dir, f) =
+  try LibraryMap.find dir !depgraph
   with Not_found ->
-  try let _ = LibraryMap.find dir needed in needed
-  with Not_found ->
-    let (_,f) = try_locate_absolute_library dir in
-    let m = intern_from_file f in
-    let deps = m.library_deps in
-    if dir <> m.library_name then
-      errorlabstrm "load_physical_library"
-        (name_clash_message dir m.library_name f);
-    LibraryMap.add dir f
-      (List.fold_right (fun (d,_) n -> library_dep d n) deps needed)
+    let _ = intern_from_file (dir,f) in
+    LibraryMap.find dir !depgraph
 
+(* Read a compiled library and all dependencies, in reverse order.
+   Do not include files that are already in the context. *)
 let rec intern_library (dir, f) needed =
   (* Look if in the current logical environment *)
   try let _ = find_library dir in needed
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
-  try let _ = List.assoc dir needed in needed
-  with Not_found ->
-  (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-  let m = intern_from_file f in
-  if dir <> m.library_name then
-    errorlabstrm "load_physical_library"
-      (name_clash_message dir m.library_name f);
-  (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
+  if List.mem_assoc dir needed then needed
+  else
+    (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+    let m = intern_from_file (dir,f) in
+    (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
 
 (* digest error with checked modules could be a warning *)
 and intern_mandatory_library (dir,_) needed =
   intern_library (try_locate_absolute_library dir) needed
 
+(* Compute the reflexive transitive dependency closure *)
+let rec fold_deps ff (dir,f) s =
+  if  LibrarySet.mem dir s then s
+  else
+    let deps = get_deps (dir,f) in
+    let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
+    ff dir (List.fold_right (fold_deps ff) deps s)
+
+and fold_deps_list  ff modl needed =
+  List.fold_right (fold_deps ff) modl needed
+
 let recheck_library ~norec ~admit ~check =
-  let nrl = List.map (fun q -> fst(try_locate_qualified_library q)) norec in
-  let al =  List.map (fun q -> fst(try_locate_qualified_library q)) admit in
-  let admit = List.fold_right library_dep (nrl@al) LibraryMap.empty in
-  let admit = List.fold_right LibraryMap.remove nrl admit in
-  let modl = List.map try_locate_qualified_library (norec@check) in
-  let needed = List.rev (List.fold_right intern_library modl []) in
+  let ml = List.map try_locate_qualified_library check in
+  let nrl = List.map try_locate_qualified_library norec in
+  let al =  List.map try_locate_qualified_library admit in
+  let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in
+  (* first compute the closure of norec, remove closure of check,
+     add closure of admit, and finally remove norec and check *)
+  let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
+  let nochk = fold_deps_list LibrarySet.remove ml nochk in
+  let nochk = fold_deps_list LibrarySet.add al nochk in
+  (* explicitely required modules cannot be skipped... *)
+  let nochk =
+    List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
+  (* *)
   Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
-  List.iter (check_one_lib admit) needed;
+  List.iter (check_one_lib nochk) needed;
   Flags.if_verbose msgnl(str"Modules were successfully checked")
 
 open Printf
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4bed9796a7..4b156e7ecd 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -15,125 +15,6 @@ open Declarations
 open Environ
 open Mod_checking
 
-(*
-let type_modpath env mp = 
-  strengthen env (lookup_module mp env).mod_type mp
-
-let rec check_spec_body env mp lab = function
-  | SPBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SPBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SPBmodule msb ->
-      check_mod_spec env msb;
-      Modops.add_module (MPdot(mp,lab)) (module_body_of_type msb.msb_modtype)
-        (add_modtype_constraints env msb.msb_modtype)
-  | SPBmodtype mty ->
-      let kn = mp, empty_dirpath, lab in
-      check_modtype env mty;
-      add_modtype kn mty (add_modtype_constraints env mty)
-
-and check_mod_spec env msb =
-  let env' = add_constraints msb.msb_constraints env in
-  check_modtype env' msb.msb_modtype;
-
-(*  Subtyping.check_equal env' msb.msb_modtype (MTBident *)
-  (* TODO: check equiv *)
-  env'
-
-(* !!!: modtype needs mp (the name it will be given) because
-   submodule should be added without reference to self *)
-and check_modtype env = function
-  | MTBident kn ->
-      (try let _ = lookup_modtype kn env in ()
-      with Not_found -> failwith ("unbound module type "(*^string_of_kn kn*)))
-  | MTBfunsig (mbid,marg,mbody) ->
-      check_modtype env marg;
-      let env' = 
-	add_module (MPbound mbid) (module_body_of_type marg)
-          (add_modtype_constraints env marg) in
-      check_modtype env' mbody
-  | MTBsig (msid,sign) ->
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          check_spec_body env (MPself msid) lab mb) env sign in
-      ()
-
-
-let elem_spec_of_body (lab,e) =
-  lab,
-  match e with
-      SEBconst cb -> SPBconst cb
-    | SEBmind mind -> SPBmind mind
-    | SEBmodule msb -> SPBmodule (module_spec_of_body msb)
-    | SEBmodtype mtb -> SPBmodtype mtb
-
-let rec check_module env mb =
-  let env' = add_module_constraints env mb in
-  (* mod_type *)
-  check_modtype env' mb.mod_type;
-  (* mod_expr *)
-  let msig =
-    match mb.mod_expr with
-        Some mex ->
-          let msig = infer_mod_expr env' mex in
-          Subtyping.check_subtypes env' msig mb.mod_type;
-          msig
-      | None -> mb.mod_type in
-  (* mod_user_type *)
-  (match mb.mod_user_type with
-      Some usig -> Subtyping.check_subtypes env' msig usig
-    | None -> ());
-  (* mod_equiv *)
-  (match mb.mod_equiv with
-      Some mid ->
-        if mb.mod_expr <> Some(MEBident mid) then
-          failwith "incorrect module alias"
-    | None -> ());
-
-and infer_mod_expr env = function
-    MEBident mp -> type_modpath env mp
-  | MEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let _ =
-        List.fold_left (fun env (lab,mb) ->
-          struct_elem_body env mp lab mb) env msb in
-      MTBsig(msid,List.map elem_spec_of_body msb)
-  | MEBfunctor (arg_id, arg, body) ->
-      check_modtype env arg;
-      let env' = add_module (MPbound arg_id) (module_body_of_type arg) env in
-      let body_ty = infer_mod_expr env' body in
-      MTBfunsig (arg_id, arg, body_ty)
-  | MEBapply (fexpr,MEBident mp,_) ->
-      let ftb = infer_mod_expr env fexpr in
-      let ftb = scrape_modtype env ftb in
-      let farg_id, farg_b, fbody_b = destr_functor ftb in
-      let mtb = type_modpath env mp in
-      Subtyping.check_subtypes env mtb farg_b;
-      subst_modtype (map_mbid farg_id mp) fbody_b
-  | MEBapply _ ->
-      failwith "functor argument must be a module variable"
-
-and struct_elem_body env mp lab = function
-  | SEBconst cb ->
-      let kn = mp, empty_dirpath, lab in
-      check_constant_declaration env kn cb
-  | SEBmind mib ->
-      let kn = mp, empty_dirpath, lab in
-      Indtypes.check_inductive env kn mib
-  | SEBmodule msb ->
-      check_module env msb;
-(*msgnl(str"MODULE OK: "++prkn(make_kn mp empty_dirpath lab)++fnl());*)
-      Modops.add_module (MPdot(mp,lab)) msb 
-        (add_module_constraints env msb)
-  | SEBmodtype mty ->
-      check_modtype env mty;
-      add_modtype (mp, empty_dirpath, lab) mty
-        (add_modtype_constraints env mty)
-*)
-
 (************************************************************************)
 (*
  * Global environment