X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteMarshal.ml;h=e786d500154f4747b0128bdcf323178793278244;hb=951069678fea0d6dcdde984320ec5057ddc57c3c;hp=dd9febedbc66fe9f384395fe47229a972b6eb905;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index dd9febedb..e786d5001 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -23,51 +23,38 @@ * http://helm.cs.unibo.it/ *) -exception Checksum_failure of string -exception Corrupt_moo of string -exception Version_mismatch of string +(* $Id$ *) -type ast_command = (Cic.term, Cic.obj) GrafiteAst.command -type moo = ast_command list * GrafiteAst.metadata list (** *) +type ast_command = Cic.obj GrafiteAst.command +type moo = ast_command list -let marshal_flags = [] +let format_name = "grafite" -(** .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 pair: first component is a list of GrafiteAst.command (real moo - * content), second component is a list of GrafiteAst.metadata - *) +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 + function + | GrafiteAst.Default (loc, name, uris) -> + let uris = List.map rehash_uri uris in + GrafiteAst.Default (loc, name, uris) + | GrafiteAst.Coercion (loc, uri, close) -> + GrafiteAst.Coercion (loc, rehash_uri uri, close) + | cmd -> + prerr_endline "Found a command not expected in a .moo:"; + let obj_pp _ = assert false in + prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd); + assert false -let save_moo ~fname (moo, metadata) = - let oc = open_out fname in - let marshalled = - Marshal.to_string (List.rev moo, List.rev metadata) 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 - moo - with End_of_file -> raise (Corrupt_moo fname)) - () + let moo = load_moo_from_file ~fname in + List.map rehash_cmd_uris moo