Move the ObjFile module to its own file.

5 files changed, 264 insertions, 244 deletions

diff --git a/lib/lib.mllib b/lib/lib.mllib
index 2db59712b9..4e08e87084 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -14,6 +14,7 @@ CWarnings
 AcyclicGraph
 Rtree
 System
+ObjFile
 Explore
 CProfile
 Future
diff --git a/lib/objFile.ml b/lib/objFile.ml
new file mode 100644
index 0000000000..190b1833bd
--- /dev/null
+++ b/lib/objFile.ml
@@ -0,0 +1,229 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open System
+
+let magic_number = 0x436F7121l (* "Coq!" *)
+
+let error_corrupted file s =
+  CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+
+let open_trapping_failure name =
+  try open_out_bin name
+  with e when CErrors.noncritical e ->
+    CErrors.user_err ~hdr:"System.open" (str "Can't open " ++ str name)
+
+(*
+
+int32: big-endian, 4 bytes
+int64: big-endian, 8 bytes
+
+-- string --
+int32 | length of the next field
+data  |
+
+-- segment summary --
+string | name
+int64  | absolute position
+int64  | length (without hash)
+hash   | MD5 (16 bytes)
+
+-- segment --
+...  | binary data
+hash | MD5 (16 bytes)
+
+-- summary --
+int32 | number of segment summaries
+s1    |
+...   | segment summaries
+sn    |
+
+-- vo --
+int32   | magic number
+int32   | Coq version
+int64   | absolute position of the summary
+...     | segments
+summary |
+
+*)
+
+type segment = {
+  name : string;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
+}
+
+type in_handle = {
+  in_filename : string;
+  in_channel : in_channel;
+  in_segments : segment CString.Map.t;
+}
+
+type out_handle = {
+  out_filename : string;
+  out_channel : out_channel;
+  mutable out_segments : segment CString.Map.t;
+}
+
+let input_int32 ch =
+  let accu = ref 0l in
+  for _i = 0 to 3 do
+    let c = input_byte ch in
+    accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c)
+  done;
+  !accu
+
+let input_int64 ch =
+  let accu = ref 0L in
+  for _i = 0 to 7 do
+    let c = input_byte ch in
+    accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c)
+  done;
+  !accu
+
+let output_int32 ch n =
+  for i = 0 to 3 do
+    output_byte ch (Int32.to_int (Int32.shift_right_logical n (24 - 8 * i)))
+  done
+
+let output_int64 ch n =
+  for i = 0 to 7 do
+    output_byte ch (Int64.to_int (Int64.shift_right_logical n (56 - 8 * i)))
+  done
+
+let input_segment_summary ch =
+  let nlen = input_int32 ch in
+  let name = really_input_string ch (Int32.to_int nlen) in
+  let pos = input_int64 ch in
+  let len = input_int64 ch in
+  let hash = Digest.input ch in
+  { name; pos; len; hash }
+
+let output_segment_summary ch seg =
+  let nlen = Int32.of_int (String.length seg.name) in
+  let () = output_int32 ch nlen in
+  let () = output_string ch seg.name in
+  let () = output_int64 ch seg.pos in
+  let () = output_int64 ch seg.len in
+  let () = Digest.output ch seg.hash in
+  ()
+
+let rec input_segment_summaries ch n accu =
+  if Int32.equal n 0l then accu
+  else
+    let s = input_segment_summary ch in
+    let accu = CString.Map.add s.name s accu in
+    input_segment_summaries ch (Int32.pred n) accu
+
+let marshal_in_segment (type a) h ~segment : a * Digest.t =
+  let { in_channel = ch } = h in
+  let s = CString.Map.find segment h.in_segments in
+  let () = LargeFile.seek_in ch s.pos in
+  let (v : a) = marshal_in h.in_filename ch in
+  let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in
+  let h = Digest.input ch in
+  let () = assert (String.equal h s.hash) in
+  (v, s.hash)
+
+let marshal_out_segment h ~segment v =
+  let { out_channel = ch } = h in
+  let () = assert (not (CString.Map.mem segment h.out_segments)) in
+  let pos = LargeFile.pos_out ch in
+  let () = Marshal.to_channel ch v [] in
+  let () = flush ch in
+  let pos' = LargeFile.pos_out ch in
+  let len = Int64.sub pos' pos in
+  let hash =
+    let in_ch = open_in h.out_filename in
+    let () = LargeFile.seek_in in_ch pos in
+    let digest = Digest.channel in_ch (Int64.to_int len) in
+    let () = close_in in_ch in
+    digest
+  in
+  let () = Digest.output ch hash in
+  let s = { name = segment; pos; len; hash } in
+  let () = h.out_segments <- CString.Map.add segment s h.out_segments in
+  ()
+
+let marshal_out_binary h ~segment =
+  let { out_channel = ch } = h in
+  let () = assert (not (CString.Map.mem segment h.out_segments)) in
+  let pos = LargeFile.pos_out ch in
+  let finish () =
+    let () = flush ch in
+    let pos' = LargeFile.pos_out ch in
+    let len = Int64.sub pos' pos in
+    let hash =
+      let in_ch = open_in h.out_filename in
+      let () = LargeFile.seek_in in_ch pos in
+      let digest = Digest.channel in_ch (Int64.to_int len) in
+      let () = close_in in_ch in
+      digest
+    in
+    let () = Digest.output ch hash in
+    let s = { name = segment; pos; len; hash } in
+    h.out_segments <- CString.Map.add segment s h.out_segments
+  in
+  ch, finish
+
+let open_in ~file =
+  try
+    let ch = open_in_bin file in
+    let magic = input_int32 ch in
+    let version = input_int32 ch in
+    let () =
+      if not (Int32.equal magic magic_number) then
+        let e = { filename = file; actual = version; expected = magic_number } in
+        raise (Bad_magic_number e)
+    in
+    let () =
+      let expected = Coq_config.vo_version in
+      if not (Int32.equal version expected) then
+        let e = { filename = file; actual = version; expected } in
+        raise (Bad_version_number e)
+    in
+    let summary_pos = input_int64 ch in
+    let () = LargeFile.seek_in ch summary_pos in
+    let nsum = input_int32 ch in
+    let seg = input_segment_summaries ch nsum CString.Map.empty in
+    { in_filename = file; in_channel = ch; in_segments = seg }
+  with
+  | End_of_file -> error_corrupted file "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted file s
+
+let close_in ch =
+  close_in ch.in_channel
+
+let get_segment ch ~segment =
+  CString.Map.find segment ch.in_segments
+
+let segments ch = ch.in_segments
+
+let open_out ~file =
+  let ch = open_trapping_failure file in
+  let () = output_int32 ch magic_number in
+  let () = output_int32 ch Coq_config.vo_version in
+  let () = output_int64 ch 0L (* placeholder *) in
+  { out_channel = ch; out_segments = CString.Map.empty; out_filename = file }
+
+let close_out { out_channel = ch; out_segments = seg } =
+  let () = flush ch in
+  let pos = LargeFile.pos_out ch in
+  (* Write the segment summary *)
+  let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in
+  let iter _ s = output_segment_summary ch s in
+  let () = CString.Map.iter iter seg in
+  (* Overwrite the position place holder *)
+  let () = LargeFile.seek_out ch 8L in
+  let () = output_int64 ch pos in
+  let () = flush ch in
+  close_out ch
diff --git a/lib/objFile.mli b/lib/objFile.mli
new file mode 100644
index 0000000000..36db7f4208
--- /dev/null
+++ b/lib/objFile.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val magic_number : int32
+
+type segment = {
+  name : string;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
+}
+
+type in_handle
+type out_handle
+
+val open_in : file:string -> in_handle
+val close_in : in_handle -> unit
+val marshal_in_segment : in_handle -> segment:string -> 'a * Digest.t
+val get_segment : in_handle -> segment:string -> segment
+val segments : in_handle -> segment CString.Map.t
+
+val open_out : file:string -> out_handle
+val close_out : out_handle -> unit
+val marshal_out_segment : out_handle -> segment:string -> 'a -> unit
+val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit)
+(** Low-level API. This function returns a channel and a closure. The channel
+    should only be written to, and once done, the closure should be invoked. *)
diff --git a/lib/system.ml b/lib/system.ml
index 32e5a53821..4e98651d6e 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -240,220 +240,6 @@ let with_magic_number_check f a =
     spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
-module ObjFile =
-struct
-
-let magic_number = 0x436F7121l (* "Coq!" *)
-
-(*
-
-int32: big-endian, 4 bytes
-int64: big-endian, 8 bytes
-
--- string --
-int32 | length of the next field
-data  |
-
--- segment summary --
-string | name
-int64  | absolute position
-int64  | length (without hash)
-hash   | MD5 (16 bytes)
-
--- segment --
-...  | binary data
-hash | MD5 (16 bytes)
-
--- summary --
-int32 | number of segment summaries
-s1    |
-...   | segment summaries
-sn    |
-
--- vo --
-int32   | magic number
-int32   | Coq version
-int64   | absolute position of the summary
-...     | segments
-summary |
-
-*)
-
-type segment = {
-  name : string;
-  pos : int64;
-  len : int64;
-  hash : Digest.t;
-}
-
-type in_handle = {
-  in_filename : string;
-  in_channel : in_channel;
-  in_segments : segment CString.Map.t;
-}
-
-type out_handle = {
-  out_filename : string;
-  out_channel : out_channel;
-  mutable out_segments : segment CString.Map.t;
-}
-
-let input_int32 ch =
-  let accu = ref 0l in
-  for _i = 0 to 3 do
-    let c = input_byte ch in
-    accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c)
-  done;
-  !accu
-
-let input_int64 ch =
-  let accu = ref 0L in
-  for _i = 0 to 7 do
-    let c = input_byte ch in
-    accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c)
-  done;
-  !accu
-
-let output_int32 ch n =
-  for i = 0 to 3 do
-    output_byte ch (Int32.to_int (Int32.shift_right_logical n (24 - 8 * i)))
-  done
-
-let output_int64 ch n =
-  for i = 0 to 7 do
-    output_byte ch (Int64.to_int (Int64.shift_right_logical n (56 - 8 * i)))
-  done
-
-let input_segment_summary ch =
-  let nlen = input_int32 ch in
-  let name = really_input_string ch (Int32.to_int nlen) in
-  let pos = input_int64 ch in
-  let len = input_int64 ch in
-  let hash = Digest.input ch in
-  { name; pos; len; hash }
-
-let output_segment_summary ch seg =
-  let nlen = Int32.of_int (String.length seg.name) in
-  let () = output_int32 ch nlen in
-  let () = output_string ch seg.name in
-  let () = output_int64 ch seg.pos in
-  let () = output_int64 ch seg.len in
-  let () = Digest.output ch seg.hash in
-  ()
-
-let rec input_segment_summaries ch n accu =
-  if Int32.equal n 0l then accu
-  else
-    let s = input_segment_summary ch in
-    let accu = CString.Map.add s.name s accu in
-    input_segment_summaries ch (Int32.pred n) accu
-
-let marshal_in_segment (type a) h ~segment : a * Digest.t =
-  let { in_channel = ch } = h in
-  let s = CString.Map.find segment h.in_segments in
-  let () = LargeFile.seek_in ch s.pos in
-  let (v : a) = marshal_in h.in_filename ch in
-  let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in
-  let h = Digest.input ch in
-  let () = assert (String.equal h s.hash) in
-  (v, s.hash)
-
-let marshal_out_segment h ~segment v =
-  let { out_channel = ch } = h in
-  let () = assert (not (CString.Map.mem segment h.out_segments)) in
-  let pos = LargeFile.pos_out ch in
-  let () = Marshal.to_channel ch v [] in
-  let () = flush ch in
-  let pos' = LargeFile.pos_out ch in
-  let len = Int64.sub pos' pos in
-  let hash =
-    let in_ch = open_in h.out_filename in
-    let () = LargeFile.seek_in in_ch pos in
-    let digest = Digest.channel in_ch (Int64.to_int len) in
-    let () = close_in in_ch in
-    digest
-  in
-  let () = Digest.output ch hash in
-  let s = { name = segment; pos; len; hash } in
-  let () = h.out_segments <- CString.Map.add segment s h.out_segments in
-  ()
-
-let marshal_out_binary h ~segment =
-  let { out_channel = ch } = h in
-  let () = assert (not (CString.Map.mem segment h.out_segments)) in
-  let pos = LargeFile.pos_out ch in
-  let finish () =
-    let () = flush ch in
-    let pos' = LargeFile.pos_out ch in
-    let len = Int64.sub pos' pos in
-    let hash =
-      let in_ch = open_in h.out_filename in
-      let () = LargeFile.seek_in in_ch pos in
-      let digest = Digest.channel in_ch (Int64.to_int len) in
-      let () = close_in in_ch in
-      digest
-    in
-    let () = Digest.output ch hash in
-    let s = { name = segment; pos; len; hash } in
-    h.out_segments <- CString.Map.add segment s h.out_segments
-  in
-  ch, finish
-
-let open_in ~file =
-  try
-    let ch = open_in_bin file in
-    let magic = input_int32 ch in
-    let version = input_int32 ch in
-    let () =
-      if not (Int32.equal magic magic_number) then
-        let e = { filename = file; actual = version; expected = magic_number } in
-        raise (Bad_magic_number e)
-    in
-    let () =
-      let expected = Coq_config.vo_version in
-      if not (Int32.equal version expected) then
-        let e = { filename = file; actual = version; expected } in
-        raise (Bad_version_number e)
-    in
-    let summary_pos = input_int64 ch in
-    let () = LargeFile.seek_in ch summary_pos in
-    let nsum = input_int32 ch in
-    let seg = input_segment_summaries ch nsum CString.Map.empty in
-    { in_filename = file; in_channel = ch; in_segments = seg }
-  with
-  | End_of_file -> error_corrupted file "premature end of file"
-  | Failure s | Sys_error s -> error_corrupted file s
-
-let close_in ch =
-  close_in ch.in_channel
-
-let get_segment ch ~segment =
-  CString.Map.find segment ch.in_segments
-
-let segments ch = ch.in_segments
-
-let open_out ~file =
-  let ch = open_trapping_failure file in
-  let () = output_int32 ch magic_number in
-  let () = output_int32 ch Coq_config.vo_version in
-  let () = output_int64 ch 0L (* placeholder *) in
-  { out_channel = ch; out_segments = CString.Map.empty; out_filename = file }
-
-let close_out { out_channel = ch; out_segments = seg } =
-  let () = flush ch in
-  let pos = LargeFile.pos_out ch in
-  (* Write the segment summary *)
-  let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in
-  let iter _ s = output_segment_summary ch s in
-  let () = CString.Map.iter iter seg in
-  (* Overwrite the position place holder *)
-  let () = LargeFile.seek_out ch 8L in
-  let () = output_int64 ch pos in
-  let () = flush ch in
-  close_out ch
-
-end
-
 (* Time stamps. *)
 
 type time = float * float * float
diff --git a/lib/system.mli b/lib/system.mli
index 7e02b76203..4a8c35b6ea 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -88,36 +88,6 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 val marshal_out : out_channel -> 'a -> unit
 val marshal_in : string -> in_channel -> 'a
 
-module ObjFile :
-sig
-
-val magic_number : int32
-
-type segment = {
-  name : string;
-  pos : int64;
-  len : int64;
-  hash : Digest.t;
-}
-
-type in_handle
-type out_handle
-
-val open_in : file:string -> in_handle
-val close_in : in_handle -> unit
-val marshal_in_segment : in_handle -> segment:string -> 'a * Digest.t
-val get_segment : in_handle -> segment:string -> segment
-val segments : in_handle -> segment CString.Map.t
-
-val open_out : file:string -> out_handle
-val close_out : out_handle -> unit
-val marshal_out_segment : out_handle -> segment:string -> 'a -> unit
-val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit)
-(** Low-level API. This function returns a channel and a closure. The channel
-    should only be written to, and once done, the closure should be invoked. *)
-
-end
-
 (** {6 Time stamps.} *)
 
 type time