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 6d7632f7572ce7548f6c697a4e65d40bbbbea412..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
@@ -773,7 +785,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       (match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode
           { NTacStatus.istatus =
-             {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
+             { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
             let uri,height,menv,subst,obj_kind = pstatus in
              if menv <> [] then
               raise
@@ -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 lexicon_status },`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;
@@ -809,12 +821,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       NCicEnvironment.add_constraint strict [false,u1] [false,u2];
       status, `New [u1;u2]
   | GrafiteAst.NObj (loc,obj) ->
-     let lexicon_status =
+     let estatus =
        match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode _ -> assert false
-       | GrafiteTypes.CommandMode ls -> ls in
-     let lexicon_status,obj =
-      GrafiteDisambiguate.disambiguate_nobj lexicon_status
+       | GrafiteTypes.CommandMode es -> es 
+     in
+     let estatus,obj =
+      GrafiteDisambiguate.disambiguate_nobj estatus
        ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
      let uri,height,nmenv,nsubst,nobj = obj in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
@@ -824,7 +837,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           GrafiteTypes.ProofMode
            (subst_metasenv_and_fix_names
             { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}})
+             istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
              }
      in
      (match nmenv with