]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/grafite/grafiteMarshal.ml
Huge reorganization of matita and ocaml.
[helm.git] / helm / ocaml / grafite / grafiteMarshal.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 exception Checksum_failure of string
27 exception Corrupt_moo of string
28 exception Version_mismatch of string
29
30 type ast_command = Cic.obj GrafiteAst.command
31 type moo = ast_command list
32
33 let marshal_flags = []
34
35 let rehash_cmd_uris =
36   let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
37   function
38   | GrafiteAst.Default (loc, name, uris) ->
39       let uris = List.map rehash_uri uris in
40       GrafiteAst.Default (loc, name, uris)
41   | GrafiteAst.Coercion (loc, uri, close) ->
42       GrafiteAst.Coercion (loc, rehash_uri uri, close)
43   | cmd ->
44       prerr_endline "Found a command not expected in a .moo:";
45       let obj_pp _ = assert false in
46       prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd);
47       assert false
48
49 (** .moo file format
50  * - an integer -- magic number -- denoting the version of the dumped data
51  *   structure. Different magic numbers stand for incompatible data structures
52  * - an integer -- checksum -- denoting the hash value (computed with
53  *   Hashtbl.hash) of the string representation of the dumped data structur
54  * - marshalled data: list of GrafiteAst.command
55  *)
56
57 let save_moo ~fname moo =
58  let ensure_path_exists path =
59    let dir = Filename.dirname path in
60    HExtlib.mkdir dir
61  in
62  ensure_path_exists fname;
63  let oc = open_out fname in
64  let marshalled = Marshal.to_string (List.rev moo) marshal_flags in
65  let checksum = Hashtbl.hash marshalled in
66  output_binary_int oc GrafiteAst.magic;
67  output_binary_int oc checksum;
68  output_string oc marshalled;
69  close_out oc
70
71 let load_moo ~fname =
72   let ic = open_in fname in
73   HExtlib.finally
74     (fun () -> close_in ic)
75     (fun () ->
76       try
77         let moo_magic = input_binary_int ic in
78         if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname);
79         let moo_checksum = input_binary_int ic in
80         let marshalled = HExtlib.input_all ic in
81         let checksum = Hashtbl.hash marshalled in
82         if checksum <> moo_checksum then raise (Checksum_failure fname);
83         let (moo:moo) =
84           Marshal.from_string marshalled 0
85         in
86         List.map rehash_cmd_uris moo
87       with End_of_file -> raise (Corrupt_moo fname))
88     ()
89