From c53208425a6bbd9890ab35c637a44d997c8ac263 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 21 Dec 2005 16:12:01 +0000 Subject: [PATCH] reimplemented specific marshallars on top of generic HMarshal marshaller --- helm/matita/matitaExcPp.ml | 13 ++---- helm/ocaml/grafite/grafiteMarshal.ml | 57 ++++++--------------------- helm/ocaml/grafite/grafiteMarshal.mli | 5 --- helm/ocaml/lexicon/lexiconMarshal.ml | 57 ++++++--------------------- helm/ocaml/lexicon/lexiconMarshal.mli | 7 +--- helm/ocaml/library/libraryNoDb.ml | 46 ++++----------------- 6 files changed, 39 insertions(+), 146 deletions(-) diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index e9e7f488f..7183b8c03 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -44,16 +44,11 @@ let rec to_string = | Unix.Unix_error (code, api, param) -> let err = Unix.error_message code in None, "Unix Error (" ^ api ^ "): " ^ err - | GrafiteMarshal.Corrupt_moo fname -> - None, sprintf ".moo file '%s' is corrupt (shorter than expected)" fname - | GrafiteMarshal.Checksum_failure fname -> + | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname + | HMarshal.Format_mismatch fname + | HMarshal.Version_mismatch fname -> None, - sprintf "checksum failed for .moo file '%s', please recompile it'" fname - | GrafiteMarshal.Version_mismatch fname -> - None, - sprintf - (".moo file '%s' has been compiled by a different version of matita, " - ^^ "please recompile it") + sprintf "format/version mismatch for file '%s', please recompile it'" fname | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index 0c4488091..685a7e948 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -23,17 +23,21 @@ * http://helm.cs.unibo.it/ *) -exception Checksum_failure of string -exception Corrupt_moo of string -exception Version_mismatch of string - type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list -let marshal_flags = [] +let format_name = "grafite" + +let save_moo_to_file ~fname moo = + HMarshal.save ~fmt:format_name ~version:GrafiteAst.magic ~fname moo + +let load_moo_from_file ~fname = + let raw = HMarshal.load ~fmt:format_name ~version:GrafiteAst.magic ~fname in + (raw: moo) let rehash_cmd_uris = - let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + let rehash_uri uri = + UriManager.uri_of_string (UriManager.string_of_uri uri) in function | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in @@ -46,44 +50,9 @@ let rehash_cmd_uris = prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd); assert false -(** .moo file format - * - an integer -- magic number -- denoting the version of the dumped data - * structure. Different magic numbers stand for incompatible data structures - * - an integer -- checksum -- denoting the hash value (computed with - * Hashtbl.hash) of the string representation of the dumped data structur - * - marshalled data: list of GrafiteAst.command - *) - -let save_moo ~fname moo = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - ensure_path_exists fname; - let oc = open_out fname in - let marshalled = Marshal.to_string (List.rev moo) marshal_flags in - let checksum = Hashtbl.hash marshalled in - output_binary_int oc GrafiteAst.magic; - output_binary_int oc checksum; - output_string oc marshalled; - close_out oc +let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo) let load_moo ~fname = - let ic = open_in fname in - HExtlib.finally - (fun () -> close_in ic) - (fun () -> - try - let moo_magic = input_binary_int ic in - if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname); - let moo_checksum = input_binary_int ic in - let marshalled = HExtlib.input_all ic in - let checksum = Hashtbl.hash marshalled in - if checksum <> moo_checksum then raise (Checksum_failure fname); - let (moo:moo) = - Marshal.from_string marshalled 0 - in - List.map rehash_cmd_uris moo - with End_of_file -> raise (Corrupt_moo fname)) - () + let moo = load_moo_from_file ~fname in + List.map rehash_cmd_uris moo diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli index 4b49cfc41..e60ad39d8 100644 --- a/helm/ocaml/grafite/grafiteMarshal.mli +++ b/helm/ocaml/grafite/grafiteMarshal.mli @@ -23,11 +23,6 @@ * http://helm.cs.unibo.it/ *) - (** name of the corrupt .moo file *) -exception Checksum_failure of string -exception Corrupt_moo of string -exception Version_mismatch of string - type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list diff --git a/helm/ocaml/lexicon/lexiconMarshal.ml b/helm/ocaml/lexicon/lexiconMarshal.ml index bd87a9521..8b6ad8312 100644 --- a/helm/ocaml/lexicon/lexiconMarshal.ml +++ b/helm/ocaml/lexicon/lexiconMarshal.ml @@ -23,16 +23,20 @@ * http://helm.cs.unibo.it/ *) -exception Checksum_failure of string -exception Corrupt_lexicon of string -exception Version_mismatch of string - type lexicon = LexiconAst.command list -let marshal_flags = [] +let format_name = "lexicon" + +let save_lexicon_to_file ~fname lexicon = + HMarshal.save ~fmt:format_name ~version:LexiconAst.magic ~fname lexicon + +let load_lexicon_from_file ~fname = + let raw = HMarshal.load ~fmt:format_name ~version:LexiconAst.magic ~fname in + (raw: lexicon) let rehash_cmd_uris = - let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + let rehash_uri uri = + UriManager.uri_of_string (UriManager.string_of_uri uri) in function | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) -> let rec aux = @@ -53,44 +57,9 @@ let rehash_cmd_uris = prerr_endline (LexiconAstPp.pp_command cmd); assert false -(** .lexicon file format - * - an integer -- magic number -- denoting the version of the dumped data - * structure. Different magic numbers stand for incompatible data structures - * - an integer -- checksum -- denoting the hash value (computed with - * Hashtbl.hash) of the string representation of the dumped data structur - * - marshalled data: list of LexiconAst.command - *) - -let save_lexicon ~fname lexicon = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - ensure_path_exists fname; - let oc = open_out fname in - let marshalled = Marshal.to_string (List.rev lexicon) marshal_flags in - let checksum = Hashtbl.hash marshalled in - output_binary_int oc LexiconAst.magic; - output_binary_int oc checksum; - output_string oc marshalled; - close_out oc +let save_lexicon ~fname lexicon = save_lexicon_to_file ~fname (List.rev lexicon) let load_lexicon ~fname = - let ic = open_in fname in - HExtlib.finally - (fun () -> close_in ic) - (fun () -> - try - let lexicon_magic = input_binary_int ic in - if lexicon_magic <> LexiconAst.magic then raise (Version_mismatch fname); - let lexicon_checksum = input_binary_int ic in - let marshalled = HExtlib.input_all ic in - let checksum = Hashtbl.hash marshalled in - if checksum <> lexicon_checksum then raise (Checksum_failure fname); - let (lexicon:lexicon) = - Marshal.from_string marshalled 0 - in - List.map rehash_cmd_uris lexicon - with End_of_file -> raise (Corrupt_lexicon fname)) - () + let lexicon = load_lexicon_from_file ~fname in + List.map rehash_cmd_uris lexicon diff --git a/helm/ocaml/lexicon/lexiconMarshal.mli b/helm/ocaml/lexicon/lexiconMarshal.mli index 9ef291842..930d73f8d 100644 --- a/helm/ocaml/lexicon/lexiconMarshal.mli +++ b/helm/ocaml/lexicon/lexiconMarshal.mli @@ -23,15 +23,10 @@ * http://helm.cs.unibo.it/ *) - (** name of the corrupt .lexicon file *) -exception Checksum_failure of string -exception Corrupt_lexicon of string -exception Version_mismatch of string - type lexicon = LexiconAst.command list val save_lexicon: fname:string -> lexicon -> unit - (** @raise Corrupt_lexicon *) + (** @raise HMarshal.* *) val load_lexicon: fname:string -> lexicon diff --git a/helm/ocaml/library/libraryNoDb.ml b/helm/ocaml/library/libraryNoDb.ml index 0a03a4a7e..bb1c5bb77 100644 --- a/helm/ocaml/library/libraryNoDb.ml +++ b/helm/ocaml/library/libraryNoDb.ml @@ -30,50 +30,20 @@ exception Corrupt_metadata of string exception Version_mismatch of string let magic = 1 +let format_name = "metadata" type metadata = | Dependency of string (* baseuri without trailing slash *) let eq_metadata (m1:metadata) (m2:metadata) = m1 = m2 -let marshal_flags = [] +let save_metadata_to_file ~fname metadata = + HMarshal.save ~fmt:format_name ~version:magic ~fname metadata -(** .metadata file format - * - an integer -- magic number -- denoting the version of the dumped data - * structure. Different magic numbers stand for incompatible data structures - * - an integer -- checksum -- denoting the hash value (computed with - * Hashtbl.hash) of the string representation of the dumped data structur - * - marshalled data: list of metadata - *) - -let save_metadata ~fname metadata = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - ensure_path_exists fname; - let oc = open_out fname in - let marshalled = Marshal.to_string metadata marshal_flags in - let checksum = Hashtbl.hash marshalled in - output_binary_int oc magic; - output_binary_int oc checksum; - output_string oc marshalled; - close_out oc +let load_metadata_from_file ~fname = + let raw = HMarshal.load ~fmt:format_name ~version:magic ~fname in + (raw: metadata list) -let load_metadata ~fname = - let ic = open_in fname in - HExtlib.finally - (fun () -> close_in ic) - (fun () -> - try - let file_magic = input_binary_int ic in - if file_magic <> magic then raise (Version_mismatch fname); - let file_checksum = input_binary_int ic in - let marshalled = HExtlib.input_all ic in - let checksum = Hashtbl.hash marshalled in - if checksum <> file_checksum then raise (Checksum_failure fname); - let (metadata:metadata list) = Marshal.from_string marshalled 0 in - metadata - with End_of_file -> raise (Corrupt_metadata fname)) - () +let save_metadata ~fname metadata = save_metadata_to_file ~fname metadata +let load_metadata ~fname = load_metadata_from_file ~fname -- 2.39.2