1 files changed, 141 insertions, 83 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 85ee28db..9a750858 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,31 +1,32 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 
-let pr_dirpath dp = str (string_of_dirpath dp)
-let default_root_prefix = make_dirpath []
+let pr_dirpath dp = str (DirPath.to_string dp)
+let default_root_prefix = DirPath.empty
 let split_dirpath d =
-  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+  let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
+let extend_dirpath p id = DirPath.make (id :: DirPath.repr p)
 
 type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath (List.map id_of_string p.dirpath)
+  DirPath.make (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
-  match repr_dirpath dir with
+  match DirPath.repr dir with
       [] -> failwith "path_of_dirpath"
     | l::dir ->
-        {dirpath=List.map string_of_id dir;basename=string_of_id l}
+        {dirpath=List.map Id.to_string dir;basename=Id.to_string l}
 let pr_dirlist dp =
   prlist_with_sep (fun _ -> str".") str (List.rev dp)
 let pr_path sp =
@@ -33,37 +34,26 @@ let pr_path sp =
       [] -> str sp.basename
     | sl -> pr_dirlist sl ++ str"." ++ str sp.basename
 
-type library_objects
-
-type compilation_unit_name = dir_path
-
-type library_disk = {
-  md_name : compilation_unit_name;
-  md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
-  md_objects : library_objects;
-  md_deps : (compilation_unit_name * Digest.t) list;
-  md_imports : compilation_unit_name list }
-
 (************************************************************************)
-(*s Modules on disk contain the following informations (after the magic
-    number, and before the digest). *)
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [libraries_table]. *)
 
 type library_t = {
-  library_name : compilation_unit_name;
-  library_filename : System.physical_path;
-  library_compiled : Safe_typing.compiled_library;
-  library_deps : (compilation_unit_name * Digest.t) list;
-  library_digest : Digest.t }
+  library_name : Cic.compilation_unit_name;
+  library_filename : CUnix.physical_path;
+  library_compiled : Cic.compiled_library;
+  library_opaques : Cic.opaque_table;
+  library_deps : Cic.library_deps;
+  library_digest : Cic.vodigest;
+  library_extra_univs : Univ.constraints }
 
 module LibraryOrdered =
   struct
-    type t = dir_path
+    type t = DirPath.t
     let compare d1 d2 =
       Pervasives.compare
-        (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+        (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
   end
 
 module LibrarySet = Set.Make(LibraryOrdered)
@@ -80,7 +70,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (string_of_dirpath dir))
+    error ("Unknown library " ^ (DirPath.to_string dir))
 
 let library_full_filename dir = (find_library dir).library_filename
 
@@ -90,6 +80,29 @@ let library_full_filename dir = (find_library dir).library_filename
 let register_loaded_library m =
   libraries_table := LibraryMap.add m.library_name m !libraries_table
 
+(* Map from library names to table of opaque terms *)
+let opaque_tables = ref LibraryMap.empty
+let opaque_univ_tables = ref LibraryMap.empty
+
+let access_opaque_table dp i =
+  let t =
+    try LibraryMap.find dp !opaque_tables
+    with Not_found -> assert false
+  in
+  assert (i < Array.length t);
+  Future.force t.(i)
+
+let access_opaque_univ_table dp i =
+  try
+    let t = LibraryMap.find dp !opaque_univ_tables in
+    assert (i < Array.length t);
+    Future.force t.(i)
+  with Not_found -> Univ.empty_constraint
+
+
+let _ = Declarations.indirect_opaque_access := access_opaque_table
+let _ = Declarations.indirect_opaque_univ_access := access_opaque_univ_table
+
 let check_one_lib admit (dir,m) =
   let file = m.library_filename in
   let md = m.library_compiled in
@@ -98,22 +111,23 @@ let check_one_lib admit (dir,m) =
      also check if it carries a validation certificate (yet to
      be implemented). *)
   if LibrarySet.mem dir admit then
-    (Flags.if_verbose msgnl
+    (Flags.if_verbose ppnl
       (str "Admitting library: " ++ pr_dirpath dir);
-      Safe_typing.unsafe_import file md dig)
+      Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
-    (Flags.if_verbose msgnl
+    (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import file md dig);
-  Flags.if_verbose msg(fnl());
+      Safe_typing.import file md m.library_extra_univs dig);
+  Flags.if_verbose pp (fnl());
+  pp_flush ();
   register_loaded_library m
 
 (*************************************************************************)
 (*s Load path. Mapping from physical to logical paths etc.*)
 
-type logical_path = dir_path
+type logical_path = DirPath.t
 
-let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
 let get_load_paths () = fst !load_paths
 
@@ -147,20 +161,23 @@ let canonical_path_name p =
 
 let find_logical_path phys_dir =
   let phys_dir = canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
+  let physical, logical = !load_paths in
+  match List.filter2 (fun p d -> p = phys_dir) physical logical with
   | _,[dir] -> dir
   | _,[] -> default_root_prefix
-  | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
 
 let remove_load_path dir =
-  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+  let physical, logical = !load_paths in
+  load_paths := List.filter2 (fun p d -> p <> dir) physical logical
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
-    match list_filter2 (fun p d -> p = phys_path) !load_paths with
+  let physical, logical = !load_paths in
+    match List.filter2 (fun p d -> p = phys_path) physical logical with
       | _,[dir] ->
 	  if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
@@ -171,7 +188,7 @@ let add_load_path (phys_path,coq_path) =
 	    begin
               (* Assume the user is concerned by library naming *)
 	      if dir <> default_root_prefix then
-		Flags.if_warn msg_warning
+		msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
@@ -180,10 +197,11 @@ let add_load_path (phys_path,coq_path) =
 	    end
       | _,[] ->
 	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-      | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
 
 let load_paths_of_dir_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_paths)
+  let physical, logical = !load_paths in
+  fst (List.filter2 (fun p d -> d = dir) physical logical)
 
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
@@ -197,7 +215,7 @@ let locate_absolute_library dir =
   let loadpath = load_paths_of_dir_path pref in
   if loadpath = [] then raise LibUnmappedDir;
   try
-    let name = string_of_id base^".vo" in
+    let name = Id.to_string base^".vo" in
     let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
@@ -220,7 +238,7 @@ let locate_qualified_library qid =
     let name =  qid.basename^".vo" in
     let path, file = System.where_in_path loadpath name in
     let dir =
-      extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
+      extend_dirpath (find_logical_path path) (Id.of_string qid.basename) in
     (* Look if loaded *)
     try
       (dir, library_full_filename dir)
@@ -228,28 +246,29 @@ let locate_qualified_library qid =
       (dir, file)
   with Not_found -> raise LibNotFound
 
-let explain_locate_library_error qid = function
-  | LibUnmappedDir ->
-      let prefix = qid.dirpath in
-      errorlabstrm "load_absolute_library_from"
-      (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
-      str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
-  | LibNotFound ->
-      errorlabstrm "load_absolute_library_from"
-      (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
-  | e -> raise e
+let error_unmapped_dir qid =
+  let prefix = qid.dirpath in
+  errorlabstrm "load_absolute_library_from"
+    (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
+     str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
+
+let error_lib_not_found qid =
+  errorlabstrm "load_absolute_library_from"
+    (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
   try
     locate_absolute_library dir
-  with e ->
-    explain_locate_library_error (path_of_dirpath dir) e
+  with
+    | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
+    | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
 
 let try_locate_qualified_library qid =
   try
     locate_qualified_library qid
-  with e ->
-    explain_locate_library_error qid e
+  with
+    | LibUnmappedDir -> error_unmapped_dir qid
+    | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
@@ -257,7 +276,7 @@ let try_locate_qualified_library qid =
 (*s Loading from disk to cache (preparation phase) *)
 
 let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
+  snd (System.raw_extern_intern Coq_config.vo_magic_number)
 
 let with_magic_number_check f a =
   try f a
@@ -270,12 +289,16 @@ let with_magic_number_check f a =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md f table digest = {
+open Cic
+
+let mk_library md f table digest cst = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
+  library_compiled = md.md_compiled;
+  library_opaques = table;
   library_deps = md.md_deps;
-  library_digest = digest }
+  library_digest = digest;
+  library_extra_univs = cst }
 
 let name_clash_message dir mdir f =
   str ("The file " ^ f ^ " contains library") ++ spc () ++
@@ -286,22 +309,56 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose msg (str"[intern "++str f++str" ...");
-  let (md,table,digest) =
+  Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
+  let (md,table,opaque_csts,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
-      let (md:library_disk) = System.marshal_in f ch in
-      let digest = System.marshal_in f ch in
-      let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
-      close_in ch;
+      let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+      let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
+      let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
+      let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
+      let (table:Cic.opaque_table), pos, checksum =
+        System.marshal_in_segment f ch in
+      (* Verification of the final checksum *)
+      let () = close_in ch in
+      let ch = open_in f in
+      if not (String.equal (Digest.channel ch pos) checksum) then
+        errorlabstrm "intern_from_file" (str "Checksum mismatch");
+      let () = close_in ch in
       if dir <> md.md_name then
-        errorlabstrm "load_physical_library"
+        errorlabstrm "intern_from_file"
           (name_clash_message dir md.md_name f);
-      Flags.if_verbose msgnl(str" done]");
-      md,table,digest
-    with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+      if tasks <> None || discharging <> None then
+        errorlabstrm "intern_from_file"
+          (str "The file "++str f++str " contains unfinished tasks");
+      if opaque_csts <> None then begin
+        pp (str " (was a vio file) ");
+      Option.iter (fun (_,_,b) -> if not b then
+        errorlabstrm "intern_from_file"
+          (str "The file "++str f++str " is still a .vio"))
+        opaque_csts;
+      Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
+      end;
+      (* Verification of the unmarshalled values *)
+      Validate.validate !Flags.debug Values.v_lib md;
+      Validate.validate !Flags.debug Values.v_opaques table;
+      Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      let digest =
+        if opaque_csts <> None then Cic.Dviovo (digest,udg)
+        else (Cic.Dvo digest) in
+      md,table,opaque_csts,digest
+    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  mk_library md f table digest
+  opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+  Option.iter (fun (opaque_csts,_,_) ->
+    opaque_univ_tables :=
+      LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+    opaque_csts;
+  let extra_cst =
+    Option.default Univ.empty_constraint
+      (Option.map (fun (_,cs,_) ->
+         Univ.ContextSet.constraints cs) opaque_csts) in
+  mk_library md f table digest extra_cst
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
@@ -317,14 +374,15 @@ let rec intern_library seen (dir, f) needed =
   try let _ = find_library dir in needed
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
-  if List.mem_assoc dir needed then needed
+  if List.mem_assoc_f DirPath.equal 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
     let seen' = LibrarySet.add dir seen in
     let deps =
-      List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in
-    (dir,m) :: List.fold_right (intern_library seen') deps needed
+      Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps
+    in
+    (dir,m) :: Array.fold_right (intern_library seen') deps needed
 
 (* Compute the reflexive transitive dependency closure *)
 let rec fold_deps seen ff (dir,f) (s,acc) =
@@ -332,9 +390,9 @@ let rec fold_deps seen ff (dir,f) (s,acc) =
   if LibrarySet.mem dir s then (s,acc)
   else
     let deps = get_deps (dir,f) in
-    let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
+    let deps = Array.map (fun (d,_) -> try_locate_absolute_library d) deps in
     let seen' = LibrarySet.add dir seen in
-    let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in
+    let (s',acc') = Array.fold_right (fold_deps seen' ff) deps (s,acc) in
     (LibrarySet.add dir s', ff dir acc')
 
 and fold_deps_list seen ff modl needed =
@@ -358,14 +416,14 @@ let recheck_library ~norec ~admit ~check =
   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() ++
+  Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
-  Flags.if_verbose msgnl(str"Modules were successfully checked")
+  Flags.if_verbose ppnl (str"Modules were successfully checked")
 
 open Printf
 
 let mem s =
   let m = try_find_library s in
-  h 0 (str (sprintf "%dk" (size_kb m)))
+  h 0 (str (sprintf "%dk" (CObj.size_kb m)))