X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteMarshal.ml;h=8c6928b7b6423b41e217c70074bd49322721ffd1;hb=55ba0a660f91e491e904dad63b14ddf2bcc2754d;hp=dd9febedbc66fe9f384395fe47229a972b6eb905;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index dd9febedb..8c6928b7b 100644
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -27,25 +27,50 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
+type ast_command = Cic.obj GrafiteAst.command
+type moo = ast_command list
 
 let marshal_flags = []
 
+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.Interpretation (loc, dsc, args, cic_appl_pattern) ->
+      let rec aux =
+        function
+        | CicNotationPt.UriPattern uri ->
+            CicNotationPt.UriPattern (rehash_uri uri)
+        | CicNotationPt.ApplPattern args ->
+            CicNotationPt.ApplPattern (List.map aux args)
+        | CicNotationPt.VarPattern _
+        | CicNotationPt.ImplicitPattern as pat -> pat
+      in
+      let appl_pattern = aux cic_appl_pattern in
+      GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
+  | GrafiteAst.Coercion (loc, uri, close) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close)
+  | GrafiteAst.Notation _
+  | GrafiteAst.Alias _ as cmd -> cmd
+  | 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
+
 (** .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
+ * - marshalled data: list of GrafiteAst.command
  *)
 
-let save_moo ~fname (moo, metadata) =
+let save_moo ~fname moo =
  let oc = open_out fname in
- let marshalled = 
-   Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags 
- 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;
@@ -67,7 +92,7 @@ let load_moo ~fname =
         let (moo:moo) =
           Marshal.from_string marshalled 0
         in
-        moo
+        List.map rehash_cmd_uris moo
       with End_of_file -> raise (Corrupt_moo fname))
     ()