EXPERIMENTAL COMMIT (by CSC,actuall :-)

This commit partially implements (in NCicLibrary) serialization for NG.
It creates several .matita/matita/.../foo.ng files that are ocaml dumps
of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied
to the current status.

The test tests/ng_includeB.ma shows how unification hints are preserved.

TODO:
 a) decompilation is implemented in NCicLibrary, but not called anywhere
 b) serialization of objects (and "query" db (and old to new cache??)) not
    implemented yet
 c) objects are removed from the library, but not from the environment!

diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index efadc681eee16cb3cd170845fdd1c7549fbb89b0..f17459162ce81c0ad9c5352cca5e9d99f43cb81c 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,6 +1,11 @@
 gallina8Parser.cmi: types.cmx 
 grafiteParser.cmi: types.cmx 
 grafite.cmi: types.cmx 
+engine.cmi: 
+types.cmo: 
+types.cmx: 
+options.cmo: 
+options.cmx: 
 gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmx gallina8Parser.cmi 

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1e777ab83a148ab1c863b06ab7db83d0b142fde0..9b454f29429647d6a4bb6202ae6e4a6b7357d382 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -471,8 +471,16 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
 let eval_unification_hint status t n = 
-  (* XXX no undo *)        
-  NCicUnifHint.add_user_provided_hint 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 status = GrafiteTypes.set_rstatus rstatus status in
+ let dump = GrafiteTypes.get_dump status in
+ let dump = fun status -> aux (dump status) in
+ let status = GrafiteTypes.set_dump dump status in
   status,`Old []
 ;;
 
@@ -726,6 +734,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      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
+     let status = GrafiteTypes.set_rstatus rstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
      let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
@@ -785,20 +797,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
-               NCicLibrary.add_obj uri obj;
+               let timestamp = NCicLibrary.add_obj uri obj in
                let objs = NCicElim.mk_elims obj in
-               let uris =
-                uri::
-                 List.map
-                  (fun (uri,_,_,_,_) as obj ->
+               let timestamp,uris_rev =
+                 List.fold_left
+                  (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj ->
                     NCicTypeChecker.typecheck_obj obj;
-                    NCicLibrary.add_obj uri obj;
-                    uri
-                  ) objs
-               in
-                {status with 
-                 GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode estatus },`New uris
+                    let timestamp = NCicLibrary.add_obj uri obj in
+                     timestamp,uri::uris_rev
+                  ) (timestamp,[]) objs in
+               let uris = uri::List.rev uris_rev in
+                GrafiteTypes.set_library_db timestamp
+                 {status with 
+                  GrafiteTypes.ng_status = 
+                   GrafiteTypes.CommandMode estatus },`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index a773ea401a9361a88cf982402bf58af8ae7bec46..60bfc69217b71425f922440ec50c69a0bba50637 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -171,6 +171,7 @@ let time_travel ~present ~past =
    uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
   List.iter LibrarySync.remove_obj objs_to_remove;
   CoercDb.restore past.GrafiteTypes.coercions;
+  NCicLibrary.time_travel (GrafiteTypes.get_library_db past)
 ;;
 
 let initial_status lexicon_status baseuri = {
@@ -185,6 +186,8 @@ let initial_status lexicon_status baseuri = {
       NEstatus.rstatus = {
         NRstatus.uhint_db = NCicUnifHint.empty_db;
         NRstatus.coerc_db = NCicCoercion.empty_db;
+        NRstatus.library_db = NCicLibrary.time0;
+        NRstatus.dump = fun x -> x;
       };
   }
 }

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 2ee136dfe753e56dbf7dd3781432ad7a72fc769b..6a57c4a003f4e134be9a636e5de75987dbc6733c 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -100,6 +100,48 @@ let get_estatus x =
   | CommandMode e -> e
 ;;
 
+let set_estatus e x =
+ { x with ng_status =
+   match x.ng_status with
+      ProofMode t ->
+       ProofMode
+        {t with NTacStatus.istatus =
+         {t.NTacStatus.istatus with NTacStatus.estatus = e}}
+    | CommandMode _ -> CommandMode e}
+;;
+
+let get_rstatus x = (get_estatus x).NEstatus.rstatus;;
+
+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 set_rstatus h x =
+ let estatus = get_estatus x in
+  set_estatus { estatus with NEstatus.rstatus = h } x
+;;
+
+let set_hstatus h x =
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.uhint_db = h} x
+;;
+
+let set_library_db h x =
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.library_db = h} x
+;;
+
+let set_dump h x =
+ let estatus = get_estatus x in
+  set_estatus
+  { estatus with NEstatus.rstatus =
+     { estatus.NEstatus.rstatus with
+        NRstatus.dump = h}}
+  x
+;;
+
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index c874d43f632cde6e6b44893e32e7df403ea503f0..4d693ea6b3be77bbf56fc3469a68a7fe18102eae 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -75,10 +75,19 @@ val get_proof_context : status -> int -> Cic.context
 val get_proof_conclusion : status -> int -> Cic.term
 val get_lexicon : status -> LexiconEngine.status
 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_coercions: status -> NCicCoercion.db
 
 val set_stack: Continuationals.Stack.t -> status -> status
 val set_metasenv: Cic.metasenv -> status -> status
 val set_lexicon : LexiconEngine.status -> status -> status
 val set_coercions: NCicCoercion.db -> status -> status 
+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
 

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index e2d800157dd4d57c4f44852dd6735b6dfc6ebd0e..8c988de2f52b8f4d144051b8a2e7975aa96d5ec9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -12,10 +12,19 @@
 (* $Id$ *)
 
 exception ObjectNotFound of string Lazy.t
+exception LibraryOutOfSync of string Lazy.t
 
-let storage = ref [];;
+type timestamp =
+ (NUri.uri * NCic.obj) list *
+ (NUri.uri * string * NReference.reference) list *
+ NCic.obj NUri.UriMap.t;;
 
+let time0 = [],[],NUri.UriMap.empty;;
+let storage = ref [];;
 let aliases = ref [];;
+let cache = ref NUri.UriMap.empty;;
+
+let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
 
 let resolve name =
  try
@@ -63,28 +72,56 @@ let add_obj u obj =
               (NReference.Ind (inductive,i,leftno))]
          ) il)
   in
-   aliases := references @ !aliases
+  aliases := references @ !aliases;
+  !storage,!aliases,!cache
 ;;
 
-let cache = NUri.UriHash.create 313;;
-
 let get_obj u =
  try List.assq u !storage
  with Not_found ->
-  try NUri.UriHash.find cache u
+  try NUri.UriMap.find u !cache
   with Not_found ->
     (* in the final implementation should get it from disk *)
     let ouri = NCic2OCic.ouri_of_nuri u in
     try
       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
       let l = OCic2NCic.convert_obj ouri o in
-      List.iter (fun (u,_,_,_,_ as o) -> 
-  (*       prerr_endline ("+"^NUri.string_of_uri u);  *)
-        NUri.UriHash.add cache u o) l;
+      List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
       HExtlib.list_last l
     with CicEnvironment.Object_not_found u -> 
       raise (ObjectNotFound 
                (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
 ;;
 
-let clear_cache () = NUri.UriHash.clear cache;;
+let clear_cache () = cache := NUri.UriMap.empty;;
+
+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
+ let path = Helm_registry.get "matita.basedir" ^ path in
+ let dirname = Filename.dirname path in
+  HExtlib.mkdir dirname;
+  path ^ ".ng"
+;;
+
+let serialize ~baseuri dump =
+ let ch = open_out (path_of_baseuri baseuri) in
+ Marshal.to_channel ch (magic,dump) [Marshal.Closures];
+ close_out ch
+;;
+
+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
+;;
+
+let decompile ~baseuri =
+ Unix.unlink (path_of_baseuri baseuri)
+;;

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index fe3262109bd7ba9d93054e25ed73832484d60436..11a608e1da89af9471780685a8e04ba6833bbe43 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -12,12 +12,21 @@
 (* $Id$ *)
 
 exception ObjectNotFound of string Lazy.t
+exception LibraryOutOfSync of string Lazy.t
 
-val add_obj: NUri.uri -> NCic.obj -> unit
+type timestamp
+val time0: timestamp
+
+val add_obj: NUri.uri -> NCic.obj -> timestamp
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
-val get_obj: NUri.uri -> NCic.obj
+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
+
 (* EOF *)

diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml
index e94ee90372cc095dd297fd4db7831c46e42076af..5d810729404c5ea739e735e877edfe9bf6dfdf8d 100644 (file)
--- a/helm/software/components/ng_kernel/nUri.ml
+++ b/helm/software/components/ng_kernel/nUri.ml
@@ -53,3 +53,4 @@ module HT = struct
 end;;
 
 module UriHash = Hashtbl.Make(HT);;
+module UriMap = Map.Make(HT);;

diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli
index 56b49ce88312fdb130fa99ea0bcf03171cf32bbb..323da90c3b60941e57c582637565be56996289cb 100644 (file)
--- a/helm/software/components/ng_kernel/nUri.mli
+++ b/helm/software/components/ng_kernel/nUri.mli
@@ -20,4 +20,4 @@ val eq: uri -> uri -> bool
 val compare: uri -> uri -> int
 
 module UriHash: Hashtbl.S with type key = uri
-
+module UriMap: Map.S with type key = uri

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index ee4b6b3d3baccb6450ca6a5aa51a98b0f383965a..632748f9271d13f866deda1d4ca2486de8baea07 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -3,8 +3,8 @@ nCicMetaSubst.cmi:
 nCicCoercion.cmi: 
 nCicUnifHint.cmi: 
 nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi 
-nCicUnification.cmi: nCicUnifHint.cmi 
-nCicRefiner.cmi: nCicUnifHint.cmi 
+nCicUnification.cmi: nRstatus.cmi 
+nCicRefiner.cmi: nRstatus.cmi 
 nDiscriminationTree.cmo: nDiscriminationTree.cmi 
 nDiscriminationTree.cmx: nDiscriminationTree.cmi 
 nCicMetaSubst.cmo: nCicMetaSubst.cmi 
@@ -15,7 +15,11 @@ nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
 nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi 
 nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi 
 nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi 
-nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi 
-nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi 
-nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi 
-nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi 
+nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
+    nCicUnification.cmi 
+nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
+    nCicUnification.cmi 
+nCicRefiner.cmo: nRstatus.cmi nCicUnification.cmi nCicMetaSubst.cmi \
+    nCicCoercion.cmi nCicRefiner.cmi 
+nCicRefiner.cmx: nRstatus.cmx nCicUnification.cmx nCicMetaSubst.cmx \
+    nCicCoercion.cmx nCicRefiner.cmi 

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 51f0482a525825451ec729a0f9ac14aad34929f8..bd7f72e70b1d3040448f71290e097fc5a54f0964 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -273,7 +273,9 @@ let _ =
           (try 
             let rdb = { 
                 NRstatus.uhint_db = NCicUnifHint.empty_db; 
-                NRstatus.coerc_db = NCicCoercion.empty_db 
+                NRstatus.coerc_db = NCicCoercion.empty_db;
+                NRstatus.library_db = NCicLibrary.time0;
+                NRstatus.dump = fun x -> x
             } in 
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 9bd934c3b05ba86927634e925555a7bb84aba0a8..9532ba985e67553e771ec495c032757226ea22fd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -62,9 +62,7 @@ let index_hint hdb context t1 t2 precedence =
 
 let empty_db = DB.empty ;;
 
-let user_db = ref empty_db ;;
-
-let add_user_provided_hint t precedence =
+let add_user_provided_hint db t precedence =
   let u = UriManager.uri_of_string "cic:/foo/bar.con" in
   let c, a, b = 
     let rec aux ctx = function
@@ -80,7 +78,7 @@ let add_user_provided_hint t precedence =
     in
       aux [] (fst (OCic2NCic.convert_term u t))
   in
-  user_db := index_hint !user_db c a b precedence
+   index_hint db c a b precedence
 ;;
 
 let db () = 
@@ -139,10 +137,13 @@ let db () =
           else [])
       [] (CoercDb.to_list (CoercDb.dump ()))
   in
+  prerr_endline "MISTERO";
+  assert false (* ERA
   List.fold_left 
     (fun db -> function 
      | (ctx,b1,b2) -> index_hint db ctx b1 b2 0)
     !user_db (List.flatten hints)
+*)
 ;;
 
 let saturate ?(delta=0) metasenv subst context ty goal_arity =

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 7582c3df61f5f2fed4c3ed23fe8d1331590507e5..bb8bc6af16bd436edb7f0a52cb840c474fff1793 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -16,7 +16,7 @@ type db
 val index_hint: 
   db -> NCic.context -> NCic.term -> NCic.term -> int -> db
 
-val add_user_provided_hint : Cic.term -> int -> unit 
+val add_user_provided_hint : db -> Cic.term -> int -> db 
 
 val empty_db : db
 

diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 02eee9837723853c3d616673da31924977b2cc1f..0ef8755f4b0fa756f0a7a5e544f3c3b2b2013aaf 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -14,5 +14,7 @@
 type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
+        library_db : NCicLibrary.timestamp;
+        dump: refiner_status -> refiner_status
 }
 

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 46634a6799785e7e81b8df74b8cdc7722ccaccd4..6cf9ddd4fa9c136b77ff8c4cc14b771e55a06880 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -14,4 +14,6 @@
 type refiner_status = {
         coerc_db : NCicCoercion.db;
         uhint_db : NCicUnifHint.db;
+        library_db : NCicLibrary.timestamp;
+        dump: refiner_status -> refiner_status
 }

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index d701a50ae44441caed18e3acc5e0eb2280397db3..3c7db84cdc8c0affd7c48eb72c7efda60fdd038e 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -88,7 +88,9 @@ let save_moo grafite_status =
      GrafiteMarshal.save_moo moo_fname
        grafite_status.GrafiteTypes.moo_content_rev;
      LexiconMarshal.save_lexicon lexicon_fname
-       (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
+       (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev;
+     NCicLibrary.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 1f880575e063860d85663f711e5390babf74e258..eb115636f8360c07a461c39d4d10c25e38f847ec 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -222,11 +222,12 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev,dump = 
       match !grafite_status with
       |  s::_ ->
          s.proof_status, s.moo_content_rev,
-          (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev
+          (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev,
+          GrafiteTypes.get_dump s
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -253,6 +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;
        exit 0
      end
   with 

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index a4e879a36e985432df1ac7c16e3914702e924735..7580ebf2969545acb112ac0f2ca909bdc466feaa 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -274,6 +274,8 @@ 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)
+         (GrafiteTypes.get_dump grafite_status)
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index ccbafd0cdb51de3a32f94b18e408b0a402543405..190d7bf6dc2bbb536b5b32fa7cce9680c6d25a6f 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -1,5 +1,5 @@
-TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
 dependent_guarded_bove_capretta.ma nat/nat.ma
 interactive/test5.ma 
 TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
@@ -35,8 +35,8 @@ TPTP/Veloci/COL063-3.p.ma logic/equality.ma
 TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
 formal_topology.ma logic/connectives.ma
 TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-test2.ma coq.ma
 replace.ma coq.ma
+test2.ma coq.ma
 TPTP/Veloci/COL064-7.p.ma logic/equality.ma
 TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
@@ -86,8 +86,8 @@ letrec.ma
 TPTP/Veloci/BOO001-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP160-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP600-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
 TPTP/Veloci/COL063-5.p.ma logic/equality.ma
+TPTP/Veloci/GRP512-1.p.ma logic/equality.ma
 continuationals.ma coq.ma
 TPTP/Veloci/GRP490-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO034-1.p.ma logic/equality.ma
@@ -101,8 +101,8 @@ TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
 TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
 change.ma coq.ma
-TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP168-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO075-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP143-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP586-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP561-1.p.ma logic/equality.ma
@@ -118,8 +118,8 @@ TPTP/Veloci/RNG007-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP548-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP182-3.p.ma logic/equality.ma
 TPTP/Veloci/COL048-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
 TPTP/Veloci/BOO005-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP189-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP556-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP146-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-4.p.ma logic/equality.ma
@@ -142,8 +142,8 @@ TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
 TPTP/Veloci/COL062-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP492-1.p.ma logic/equality.ma
 cut.ma coq.ma
-TPTP/Veloci/COL018-1.p.ma logic/equality.ma
 TPTP/Veloci/LAT034-1.p.ma logic/equality.ma
+TPTP/Veloci/COL018-1.p.ma logic/equality.ma
 tinycals.ma logic/connectives.ma
 coercions_contravariant.ma logic/equality.ma nat/nat.ma
 interactive/automatic_insertion.ma 
@@ -151,11 +151,11 @@ clearbody.ma coq.ma
 TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
 TPTP/Veloci/COL060-2.p.ma logic/equality.ma
 TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
 TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
-TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
 ng_commands.ma nat/nat.ma ng_pts.ma
@@ -166,22 +166,25 @@ TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
 fguidi.ma logic/connectives.ma nat/nat.ma
 TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
-TPTP/Veloci/COL083-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
+TPTP/Veloci/COL083-1.p.ma logic/equality.ma
 coercions_propagation.ma logic/connectives.ma nat/orders.ma
 TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
 interactive/test_instance.ma 
 TPTP/Veloci/COL012-1.p.ma logic/equality.ma
+ng_lexiconn.ma ng_pts.ma
 TPTP/Veloci/COL063-2.p.ma logic/equality.ma
 first.ma 
+ng_coercions.ma 
 TPTP/Veloci/COL045-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO005-4.p.ma logic/equality.ma
 interactive/test7.ma 
 bad_induction.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
+ng_include.ma nat/plus.ma ng_pts.ma
 color.ma logic/equality.ma nat/nat.ma
 TPTP/Veloci/COL064-6.p.ma logic/equality.ma
 metasenv_ordering.ma coq.ma
@@ -192,8 +195,8 @@ TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
 pullback.ma logic/equality.ma
 TPTP/Veloci/COL086-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP151-1.p.ma logic/equality.ma
-TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP616-1.p.ma logic/equality.ma
+TPTP/Veloci/LCL161-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP023-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP206-1.p.ma logic/equality.ma
 decompose.ma logic/connectives.ma
@@ -208,8 +211,8 @@ dependent_type_inference.ma nat/nat.ma
 TPTP/Veloci/GRP456-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP159-1.p.ma logic/equality.ma
 TPTP/Veloci/ROB030-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP577-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
 rewrite.ma coq.ma
 bad_tests/auto.ma coq.ma
@@ -222,16 +225,16 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
-TPTP/Veloci/COL004-3.p.ma logic/equality.ma
+TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
+TPTP/Veloci/COL004-3.p.ma logic/equality.ma
 TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
 apply.ma coq.ma
 TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP145-1.p.ma logic/equality.ma
-TPTP/Veloci/COL063-4.p.ma logic/equality.ma
 TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
+TPTP/Veloci/COL063-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
 paramodulation.ma coq.ma
@@ -240,8 +243,8 @@ coercions_nonuniform.ma
 TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
 TPTP/Veloci/COL064-8.p.ma logic/equality.ma
 TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
 TPTP/Veloci/COL050-1.p.ma logic/equality.ma
+TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
 TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
 TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
 TPTP/Veloci/COL061-3.p.ma logic/equality.ma
@@ -250,9 +253,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma
 compose.ma logic/equality.ma
 TPTP/Veloci/COL025-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-letrecand.ma nat/nat.ma
 unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
 hard_refine.ma coq.ma
+letrecand.ma nat/nat.ma
 paramodulation/group.ma coq.ma
 TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
 TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
@@ -269,8 +272,8 @@ TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
 TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
 unfold.ma coq.ma
-TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
 TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO071-1.p.ma logic/equality.ma
 TPTP/Veloci/BOO013-4.p.ma logic/equality.ma
 TPTP/Veloci/GRP582-1.p.ma logic/equality.ma
@@ -290,8 +293,9 @@ injection.ma coq.ma
 second.ma first.ma
 TPTP/Veloci/COL062-2.p.ma logic/equality.ma
 match_inference.ma 
-simpl.ma coq.ma
 unifhint_simple.ma logic/equality.ma
+ng_includeB.ma ng_include.ma
+simpl.ma coq.ma
 TPTP/Veloci/COL063-6.p.ma logic/equality.ma
 TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
 third.ma first.ma second.ma

diff --git a/helm/software/matita/tests/ng_include.ma b/helm/software/matita/tests/ng_include.ma
new file mode 100644 (file)
index 0000000..4584afd
--- /dev/null
+++ b/helm/software/matita/tests/ng_include.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ng_pts.ma".
+include "nat/plus.ma".
+
+(*
+ndefinition x ≝ O.
+*)
+(*ndefinition y ≝ cic:/matita/tests/ng_commands/x.def(1).*)
+
+axiom P: nat → Prop.
+
+unification hint 0 (∀n. P (0 + n) = P n) .
+
+ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p.
\ No newline at end of file

diff --git a/helm/software/matita/tests/ng_includeB.ma b/helm/software/matita/tests/ng_includeB.ma
new file mode 100644 (file)
index 0000000..f7e1e29
--- /dev/null
+++ b/helm/software/matita/tests/ng_includeB.ma
@@ -0,0 +1,17 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ng_include.ma".
+
+ntheorem foo: ∀n. ∀H:(P (? + n) → Prop). ∀p:P n. H p.