From 6b376edd098a251ff27494706f95863b15021945 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 31 Oct 2024 13:30:53 +0100 Subject: [PATCH] Remove My_zip The module `My_Zip` contains only function which is called once in `Solving_loop`. This commit cleans the code and move it in `Solving_loop` directly. Technically, `Solving_loop` is a part of the binary, but as everyone knows, most of the code of this module will be push into the library after we design a good API. --- src/bin/common/solving_loop.ml | 11 ++++- src/lib/dune | 2 +- src/lib/util/my_zip.ml | 78 ---------------------------------- src/lib/util/my_zip.mli | 48 --------------------- 4 files changed, 11 insertions(+), 128 deletions(-) delete mode 100644 src/lib/util/my_zip.ml delete mode 100644 src/lib/util/my_zip.mli diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 10db9c475..a35411d7b 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -305,6 +305,15 @@ let process_source ?selector_inst ~print_status src = end | `Stdin -> () in + let extract_zip_file f = + let cin = Zip.open_in f in + Fun.protect ~finally:(fun () -> Zip.close_in cin) @@ fun () -> + match Zip.entries cin with + | [e] when not @@ e.Zip.is_directory -> + Zip.read_entry cin e + | _ -> + fatal_error "the zip archive '%s' should contain exactly one file" f + in (* Prepare the input source for Dolmen from an input source for Alt-Ergo. *) let mk_files src = let lang = @@ -316,7 +325,7 @@ let process_source ?selector_inst ~print_status src = let src = match src with | `File path when Filename.check_suffix path ".zip" -> - let content = AltErgoLib.My_zip.extract_zip_file path in + let content = extract_zip_file path in `Raw (Filename.(chop_extension path |> basename), content) | `File _ | `Raw _ | `Stdin -> src in diff --git a/src/lib/dune b/src/lib/dune index 30cc3b00b..67f3b0de3 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -61,7 +61,7 @@ ; util Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue Options Timers Util Vec Version Steps Printer - My_zip My_list Theories Nest Compat + My_list Theories Nest Compat ) (js_of_ocaml diff --git a/src/lib/util/my_zip.ml b/src/lib/util/my_zip.ml deleted file mode 100644 index d3efd8fd1..000000000 --- a/src/lib/util/my_zip.ml +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to - generate the.js file for try-Alt-Ergo. *) - -module ZipWrapper = struct - include Zip - let filename e = e.Zip.filename - let is_directory e = e.Zip.is_directory -end - -include ZipWrapper - -let extract_zip_file f = - let cin = open_in f in - try - match entries cin with - | [e] when not @@ is_directory e -> - if Options.get_verbose () then - Printer.print_dbg - ~module_name:"My_zip" ~function_name:"extract_zip_file" - "I'll read the content of '%s' in the given zip" - (filename e); - let content = read_entry cin e in - close_in cin; - content - | _ -> - close_in cin; - raise (Arg.Bad - (Format.sprintf "%s '%s' %s@?" - "The zipped file" f - "should contain exactly one file.")) - with e -> - close_in cin; - raise e - -(* !! This commented code is used when compiling to javascript !! - module DummyZip = struct - type entry = unit - type in_file = unit - - let s = "Zip module not available for your setting or has been disabled !" - - let open_in _ = failwith s - let close_in _ = failwith s - let entries _ = failwith s - let read_entry _ _ = failwith s - let filename _ = failwith s - let is_directory _ = failwith s - end - - include DummyZip -*) diff --git a/src/lib/util/my_zip.mli b/src/lib/util/my_zip.mli deleted file mode 100644 index 65ff2a6b6..000000000 --- a/src/lib/util/my_zip.mli +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to - generate the.js file for try-Alt-Ergo **) - -type in_file -type entry - -val open_in : string -> in_file - -val close_in : in_file -> unit - -val entries : in_file -> entry list - -val read_entry : in_file -> entry -> string - -val filename : entry -> string - -val is_directory : entry -> bool - -val extract_zip_file : string -> string -(** [extract_zip_file filename] extract the unique file of the zip archive - [filename] and its content. *)