Initial implementation of statuses using objects in place of nested records.

[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 6e6a5bc733d364b9ac16179660129d6c0b8bd7ac..e0bcd031e1bcd07e2a121ebade0bb5c96df7e67a 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -471,10 +471,7 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
    (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 }
+ NCicUnifHint.add_user_provided_hint status t n
 ;;
 
 let inject_unification_hint =
@@ -491,11 +488,11 @@ let eval_unification_hint status t n =
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = GrafiteTypes.set_estatus estatus 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 = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in
- let status = GrafiteTypes.set_dump dump status in
+ let dstatus =
+  basic_eval_unification_hint (t,n) (GrafiteTypes.get_dstatus status) in
+ let dump = inject_unification_hint (t,n)::dstatus#dump in
+ let dstatus = dstatus#set_dump dump in
+ let status = GrafiteTypes.set_dstatus dstatus status in
   status,`Old []
 ;;
 
@@ -748,11 +745,11 @@ 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 =
-      NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus
-     in
-     let status = GrafiteTypes.set_rstatus rstatus status in
+     let dstatus = GrafiteTypes.get_dstatus status in
+     let dstatus =
+       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+        dstatus in
+     let status = GrafiteTypes.set_dstatus dstatus 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
@@ -830,17 +827,18 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
-               let timestamp = NCicLibrary.add_obj uri obj in
+               let dstatus = estatus.NEstatus.rstatus in
+               let dstatus = NCicLibrary.add_obj dstatus uri obj in
                let objs = NCicElim.mk_elims obj in
                let timestamp,uris_rev =
                  List.fold_left
-                  (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj ->
+                  (fun (dstatus,uris_rev) (uri,_,_,_,_) as obj ->
                     NCicTypeChecker.typecheck_obj obj;
-                    let timestamp = NCicLibrary.add_obj uri obj in
-                     timestamp,uri::uris_rev
-                  ) (timestamp,[]) objs in
+                    let dstatus = NCicLibrary.add_obj dstatus uri obj in
+                     dstatus,uri::uris_rev
+                  ) (dstatus,[]) objs in
                let uris = uri::List.rev uris_rev in
-                GrafiteTypes.set_library_db timestamp
+                GrafiteTypes.set_dstatus dstatus
                  {status with 
                   GrafiteTypes.ng_status = 
                    GrafiteTypes.CommandMode estatus },`New uris