From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Jun 2009 17:37:05 +0000 (+0000)
Subject: FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
X-Git-Tag: make_still_working~3864
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6c887944d48d718f372a57f1609f3d059908aa8;p=helm.git

FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

Instead of serializing closures (of type status -> status), we now
serialize data. This is achieved by implementing an existential type

       NCicLibrary.Serializer(struct type status end).obj

whose semantics is "\exists 'a. 'a -> status -> status"
and by putting in the dump a list of these existential types.

The current implementation is the type-unsafe one based internally on Obj.magic.
However, the interface is (should be?) type-safe.
Other type-safe implementations could be derived by the ocaml m.l. thread on
existential types. In particular, I remember implementations via:
  - references
  - functors
  - exceptions
  - impredicative encoding via polymorphic methods


This fix allow to change the Matita code without invalidating the library.


(Critical) things still to be done:
 - decompilation
 - refreshment of URIs
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9b454f294..bb01585d1 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -470,16 +470,22 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
+let basic_eval_unification_hint (t,n) status =
+ let hstatus =
+  NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
+ in
+  { status with NRstatus.uhint_db = hstatus }
+;;
+
+let inject_unification_hint =
+ NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
+;;
+
 let eval_unification_hint status t n = 
- let aux status =
-  let hstatus =
-   NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
-  in
-   { status with NRstatus.uhint_db = hstatus } in
- let rstatus = aux (GrafiteTypes.get_rstatus status) in
+ let rstatus =
+  basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in
  let status = GrafiteTypes.set_rstatus rstatus status in
- let dump = GrafiteTypes.get_dump status in
- let dump = fun status -> aux (dump status) in
+ let dump = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in
  let status = GrafiteTypes.set_dump dump status in
   status,`Old []
 ;;
@@ -736,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      let status = eval_from_moo.efm_go status moopath in
      let rstatus = GrafiteTypes.get_rstatus status in
      let rstatus =
-      NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in
+      NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus
+     in
      let status = GrafiteTypes.set_rstatus rstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 60bfc6921..de578d7ca 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -184,10 +184,11 @@ let initial_status lexicon_status baseuri = {
     ng_status = GrafiteTypes.CommandMode { 
       NEstatus.lstatus = lexicon_status;
       NEstatus.rstatus = {
+       NRstatus.refiner_status = {
         NRstatus.uhint_db = NCicUnifHint.empty_db;
         NRstatus.coerc_db = NCicCoercion.empty_db;
-        NRstatus.library_db = NCicLibrary.time0;
-        NRstatus.dump = fun x -> x;
+        NRstatus.library_db = NCicLibrary.time0 };
+       NRstatus.dump = []
       };
   }
 }
diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 6a57c4a00..0b9a4a7da 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -78,22 +78,6 @@ let set_lexicon new_lexicon_status new_grafite_status =
                new_lexicon_status }}}}
 ;; 
 
-let set_coercions db new_grafite_status = 
-  { new_grafite_status with ng_status =
-   match new_grafite_status.ng_status with
-   | CommandMode estatus -> 
-      CommandMode 
-        { estatus with NEstatus.rstatus = 
-          { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }}
-   | ProofMode t -> 
-       ProofMode 
-        { t with NTacStatus.istatus = 
-          { t.NTacStatus.istatus with NTacStatus.estatus = 
-            { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus =
-              { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db
-        }}}}}
-;; 
-
 let get_estatus x = 
   match x.ng_status with
   | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
@@ -110,19 +94,32 @@ let set_estatus e x =
     | CommandMode _ -> CommandMode e}
 ;;
 
-let get_rstatus x = (get_estatus x).NEstatus.rstatus;;
+let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
+
+let get_rstatus x = (get_dstatus x).NRstatus.refiner_status;;
 
 let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;;
 
 let get_library_db x = (get_rstatus x).NRstatus.library_db;;
 
-let get_dump x = (get_rstatus x).NRstatus.dump;;
+let get_dump x = (get_dstatus x).NRstatus.dump;;
 
-let set_rstatus h x =
+let set_dstatus h x =
  let estatus = get_estatus x in
   set_estatus { estatus with NEstatus.rstatus = h } x
 ;;
 
+let set_rstatus h x =
+ let dstatus = get_dstatus x in
+  set_dstatus { dstatus with NRstatus.refiner_status = h } x
+;;
+
+let set_coercions db x = 
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.coerc_db = db } x
+;;
+
+
 let set_hstatus h x =
  let rstatus = get_rstatus x in
   set_rstatus { rstatus with NRstatus.uhint_db = h} x
@@ -275,8 +272,4 @@ let dump_status status =
   List.iter 
     (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
   
-let get_coercions new_grafite_status = 
-   let e = get_estatus new_grafite_status in
-   e.NEstatus.rstatus.NRstatus.coerc_db 
-;;
-
+let get_coercions x = (get_rstatus x).NRstatus.coerc_db;;
diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index 4d693ea6b..4caba49d1 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -78,7 +78,7 @@ val get_estatus : status -> NEstatus.extra_status
 val get_rstatus : status -> NRstatus.refiner_status
 val get_hstatus : status -> NCicUnifHint.db
 val get_library_db : status -> NCicLibrary.timestamp
-val get_dump : status -> (NRstatus.refiner_status -> NRstatus.refiner_status)
+val get_dump : status -> NRstatus.Serializer.obj list
 val get_coercions: status -> NCicCoercion.db
 
 val set_stack: Continuationals.Stack.t -> status -> status
@@ -89,5 +89,5 @@ val set_estatus : NEstatus.extra_status -> status -> status
 val set_rstatus : NRstatus.refiner_status -> status -> status
 val set_hstatus : NCicUnifHint.db -> status -> status
 val set_library_db : NCicLibrary.timestamp -> status -> status
-val set_dump : (NRstatus.refiner_status -> NRstatus.refiner_status) -> status -> status
+val set_dump : NRstatus.Serializer.obj list -> status -> status
 
diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 5002e58ab..b302da1f2 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -200,7 +200,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~rdb:estatus.NEstatus.rstatus
+        ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
         ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
         ~expty 
         ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
@@ -688,7 +688,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~rdb:estatus.NEstatus.rstatus
+           ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
            ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
@@ -783,7 +783,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~mk_choice:ncic_mk_choice
       ~mk_implicit
       ~uri:(OCic2NCic.nuri_of_ouri uri)
-      ~rdb:estatus.NEstatus.rstatus
+      ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
       ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
       ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) 
       (text,prefix_len,obj)) in
diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml
index a225f439d..a49174b11 100644
--- a/helm/software/components/grafite_parser/nEstatus.ml
+++ b/helm/software/components/grafite_parser/nEstatus.ml
@@ -13,6 +13,6 @@
 
 type extra_status = {
         lstatus : LexiconEngine.status;
-        rstatus : NRstatus.refiner_status;
+        rstatus : NRstatus.dumpable_refiner_status;
 }
 
diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli
index a225f439d..a49174b11 100644
--- a/helm/software/components/grafite_parser/nEstatus.mli
+++ b/helm/software/components/grafite_parser/nEstatus.mli
@@ -13,6 +13,6 @@
 
 type extra_status = {
         lstatus : LexiconEngine.status;
-        rstatus : NRstatus.refiner_status;
+        rstatus : NRstatus.dumpable_refiner_status;
 }
 
diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index cff822316..414e5c5de 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -26,8 +26,6 @@ let cache = ref NUri.UriMap.empty;;
 
 let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
 
-let magic = 0;;
-
 let path_of_baseuri baseuri =
  let uri = NUri.string_of_uri baseuri in
  let path = String.sub uri 4 (String.length uri - 4) in
@@ -37,6 +35,18 @@ let path_of_baseuri baseuri =
   path ^ ".ng"
 ;;
 
+let magic = 0;;
+
+let require0 ~baseuri =
+ let ch = open_in (path_of_baseuri baseuri) in
+ let mmagic,dump = Marshal.from_channel ch in
+  close_in ch;
+  if mmagic <> magic then
+   raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
+  else
+   dump
+;;
+
 let serialize ~baseuri dump =
  let ch = open_out (path_of_baseuri baseuri) in
  Marshal.to_channel ch (magic,dump) [Marshal.Closures];
@@ -47,18 +57,40 @@ let serialize ~baseuri dump =
     Marshal.to_channel ch (magic,obj) [];
     close_out ch
   ) !storage;
- time_travel time0;
+ time_travel time0
 ;;
 
-let require ~baseuri =
- let ch = open_in (path_of_baseuri baseuri) in
- let mmagic,dump = Marshal.from_channel ch in
-  close_in ch;
-  if mmagic <> magic then
-   raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
-  else
-   dump
-;;
+module type Serializer =
+ sig
+  type status
+  type obj
+  val register: string -> ('a -> status -> status) -> ('a -> obj)
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val require: baseuri:NUri.uri -> status -> status
+ end
+
+module Serializer(S: sig type status end) =
+ struct
+  type status = S.status
+  type obj = Obj.t
+
+  let require1 = ref (fun _ -> assert false (* unknown data*))
+  let already_registered = ref []
+
+  let register tag require =
+   assert (not (List.mem tag !already_registered));
+   already_registered := tag :: !already_registered;
+   require1 :=
+    (fun (tag',data) as x ->
+     if tag=tag' then Obj.magic require data else Obj.magic !require1 x);
+   Obj.magic (fun x -> tag,x)
+
+  let serialize = serialize
+
+  let require ~baseuri status =
+   let dump = require0 ~baseuri in
+    List.fold_right (Obj.magic !require1) dump status
+end
 
 let decompile ~baseuri =
  Unix.unlink (path_of_baseuri baseuri)
@@ -67,7 +99,7 @@ let decompile ~baseuri =
 
 (* the miracles of Marshal... *)
 let fetch_obj uri =
- let obj = require ~baseuri:uri in
+ let obj = require0 ~baseuri:uri in
   (* here we need to refresh the URIs! *)
   obj
 ;;
@@ -141,4 +173,3 @@ let get_obj u =
 ;;
 
 let clear_cache () = cache := NUri.UriMap.empty;;
-
diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 11a608e1d..f94c65682 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -25,8 +25,17 @@ val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
 val clear_cache : unit -> unit
 
 val time_travel: timestamp -> unit
-val serialize: baseuri:NUri.uri -> ('status -> 'status) -> unit
-val require: baseuri:NUri.uri -> 'status -> 'status
 val decompile: baseuri:NUri.uri -> unit
 
+module type Serializer =
+ sig
+  type status
+  type obj
+  val register: string -> ('a -> status -> status) -> ('a -> obj)
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val require: baseuri:NUri.uri -> status -> status
+ end
+
+module Serializer(S: sig type status end): Serializer with type status= S.status
+
 (* EOF *)
diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bd7f72e70..6aba5a993 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -272,10 +272,9 @@ let _ =
           let bo = curryfy [] bo in
           (try 
             let rdb = { 
-                NRstatus.uhint_db = NCicUnifHint.empty_db; 
-                NRstatus.coerc_db = NCicCoercion.empty_db;
-                NRstatus.library_db = NCicLibrary.time0;
-                NRstatus.dump = fun x -> x
+               NRstatus.uhint_db = NCicUnifHint.empty_db; 
+               NRstatus.coerc_db = NCicCoercion.empty_db;
+               NRstatus.library_db = NCicLibrary.time0
             } in 
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None
diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 0ef8755f4..26ef2684c 100644
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -15,6 +15,12 @@ type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
         library_db : NCicLibrary.timestamp;
-        dump: refiner_status -> refiner_status
 }
 
+module Serializer =
+ NCicLibrary.Serializer(struct type status = refiner_status end)
+
+type dumpable_refiner_status = {
+        refiner_status : refiner_status;
+        dump: Serializer.obj list
+}
diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 6cf9ddd4f..729f6ba6e 100644
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -15,5 +15,11 @@ type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
         library_db : NCicLibrary.timestamp;
-        dump: refiner_status -> refiner_status
+}
+
+module Serializer: NCicLibrary.Serializer with type status = refiner_status
+
+type dumpable_refiner_status = {
+        refiner_status : refiner_status;
+        dump: Serializer.obj list
 }
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 6aaf4a4a8..ba0308068 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -84,7 +84,7 @@ let relocate status destination (name,source,t as orig) =
     NCicMetaSubst.delift 
        ~unify:(fun m s c t1 t2 -> 
          try Some (NCicUnification.unify 
-           status.estatus.NEstatus.rstatus m s c t1 t2)
+           status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2)
          with 
           | NCicUnification.UnificationFailure _ 
           | NCicUnification.Uncertain _ -> None) 
@@ -147,7 +147,7 @@ let unify status ctx a b =
   let status, (_,_,b) = relocate status ctx b in
   let n,h,metasenv,subst,o = status.pstatus in
   let metasenv, subst = 
-    NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b
+    NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b
   in
   { status with pstatus = n,h,metasenv,subst,o }
 ;;
@@ -160,7 +160,7 @@ let refine status ctx term expty =
         let status, (n,_, e) = relocate status ctx e in status, n, Some e
   in
   let name,height,metasenv,subst,obj = status.pstatus in
-  let rdb = status.estatus.NEstatus.rstatus in
+  let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
   let metasenv, subst, t, ty = 
    NCicRefiner.typeof rdb metasenv subst ctx term expty
   in
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 3c7db84cd..8acc424a9 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -89,7 +89,7 @@ let save_moo grafite_status =
        grafite_status.GrafiteTypes.moo_content_rev;
      LexiconMarshal.save_lexicon lexicon_fname
        (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev;
-     NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri)
+     NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
       (GrafiteTypes.get_dump grafite_status)
   | _ -> clean_current_baseuri grafite_status 
 ;;
diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index eb115636f..5ed1d41b4 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -254,7 +254,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-       NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
+       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with 
diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 7580ebf29..c0c3d0941 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -274,7 +274,7 @@ let compile atstart options fname =
         (* FG: we do not generate .moo when dumping .mma files *)
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-        NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
          (GrafiteTypes.get_dump grafite_status)
      end;
      let tm = Unix.gmtime elapsed in