EXPERIMENTAL COMMIT (by CSC,actuall :-)

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

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;