Make the interface of System.raw_extern_intern much saner.

There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.

5 files changed, 58 insertions, 71 deletions

diff --git a/checker/check.ml b/checker/check.ml
index c835cec82..2bc470aea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -271,20 +271,10 @@ let try_locate_qualified_library qid =
     | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
+(*s Low-level interning of libraries from files *)
 
-(*s Loading from disk to cache (preparation phase) *)
-
-let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number)
-
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let raw_intern_library f =
+  System.raw_intern_state Coq_config.vo_magic_number f
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -312,7 +302,7 @@ let intern_from_file (dir, f) =
   Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
   let (sd,md,table,opaque_csts,digest) =
     try
-      let ch = with_magic_number_check raw_intern_library f in
+      let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
       let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
       let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
diff --git a/lib/system.ml b/lib/system.ml
index 139effd9f..ddc56956c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -174,47 +174,42 @@ let skip_in_segment f ch =
 
 exception Bad_magic_number of string
 
-let raw_extern_intern magic =
-  let extern_state filename =
-    let channel = open_trapping_failure filename in
-    output_binary_int channel magic;
+let raw_extern_state magic filename =
+  let channel = open_trapping_failure filename in
+  output_binary_int channel magic;
+  channel
+
+let raw_intern_state magic filename =
+  try
+    let channel = open_in_bin filename in
+    if not (Int.equal (input_binary_int filename channel) magic) then
+      raise (Bad_magic_number filename);
     channel
-  and intern_state filename =
-    try
-      let channel = open_in_bin filename in
-      if not (Int.equal (input_binary_int filename channel) magic) then
-        raise (Bad_magic_number filename);
-      channel
-    with
-    | End_of_file -> error_corrupted filename "premature end of file"
-    | Failure s | Sys_error s -> error_corrupted filename s
-  in
-  (extern_state,intern_state)
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted filename s
 
-let extern_intern magic =
-  let (raw_extern,raw_intern) = raw_extern_intern magic in
-  let extern_state filename val_0 =
-    try
-      let channel = raw_extern filename in
-      try
-        marshal_out channel val_0;
-        close_out channel
-      with reraise ->
-	let reraise = Errors.push reraise in
-        let () = try_remove filename in
-        iraise reraise
-    with Sys_error s ->
-      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
-  and intern_state filename =
+let extern_state magic filename val_0 =
+  try
+    let channel = raw_extern_state magic filename in
     try
-      let channel = raw_intern filename in
-      let v = marshal_in filename channel in
-      close_in channel;
-      v
-    with Sys_error s ->
-      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
-  in
-  (extern_state,intern_state)
+      marshal_out channel val_0;
+      close_out channel
+    with reraise ->
+      let reraise = Errors.push reraise in
+      let () = try_remove filename in
+      iraise reraise
+  with Sys_error s ->
+    errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+
+let intern_state magic filename =
+  try
+    let channel = raw_intern_state magic filename in
+    let v = marshal_in filename channel in
+    close_in channel;
+    v
+  with Sys_error s ->
+    errorlabstrm "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
diff --git a/lib/system.mli b/lib/system.mli
index 5797502e9..247d528b9 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -36,11 +36,13 @@ val find_file_in_path :
 
 exception Bad_magic_number of string
 
-val raw_extern_intern : int ->
-  (string -> out_channel) * (string -> in_channel)
+val raw_extern_state : int -> string -> out_channel
 
-val extern_intern : int ->
-  (string -> 'a -> unit) * (string -> 'a)
+val raw_intern_state : int -> string -> in_channel
+
+val extern_state : int -> string -> 'a -> unit
+
+val intern_state : int -> string -> 'a
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
diff --git a/library/library.ml b/library/library.ml
index 0fb938e9b..6da9ccf68 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -19,10 +19,12 @@ open Lib
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
 
-(*s Loading from disk to cache (preparation phase) *)
+let raw_extern_library f =
+  System.raw_extern_state Coq_config.vo_magic_number f
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
+let raw_intern_library f =
+  System.with_magic_number_check
+    (System.raw_intern_state Coq_config.vo_magic_number) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -56,7 +58,7 @@ let in_delayed f ch =
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
   try
-    let ch = System.with_magic_number_check raw_intern_library f in
+    let ch = raw_intern_library f in
     let () = seek_in ch pos in
     let obj, _, digest' = System.marshal_in_segment f ch in
     let () = close_in ch in
@@ -434,7 +436,7 @@ let mk_summary m = {
 }
 
 let intern_from_file f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
   let (lmd : seg_lib delayed) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
@@ -489,7 +491,7 @@ let rec_intern_library libs mref =
   libs
 
 let native_name_from_filename f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
@@ -654,7 +656,7 @@ let start_library f =
 let load_library_todo f =
   let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
diff --git a/library/states.ml b/library/states.ml
index 4e55f0cdc..3cb6da12e 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,14 +21,12 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let (extern_state,intern_state) =
-  let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number in
-  (fun s ->
-    raw_extern s (freeze ~marshallable:`Yes)),
-  (fun s ->
-    unfreeze (with_magic_number_check raw_intern s);
-    Library.overwrite_library_filenames s)
+let extern_state s =
+  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+
+let intern_state s =
+  unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+  Library.overwrite_library_filenames s
 
 (* Rollback. *)