1. metadata are no longer stored in .moo files.

[helm.git] / helm / ocaml / grafite / grafiteMarshal.ml

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index dd9febedbc66fe9f384395fe47229a972b6eb905..8b4f8858b8bf8f3b33b0b50f0670c1499d370d80 100644 (file)
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -28,24 +28,48 @@ 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 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, term, close) ->
+      GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close)
+  | GrafiteAst.Notation _
+  | GrafiteAst.Alias _ as cmd -> cmd
+  | cmd ->
+      prerr_endline "Found a command not expected in a .moo:";
+      prerr_endline (GrafiteAstPp.pp_cic_command 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 +91,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))
     ()