Objects are now used to represent also the tactic status.

[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 e02bd159fe0d13544c5cc33252810b2d5bdcff0e..8edf316f695222e86dab1343fb360af59e46029d 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -660,14 +660,12 @@ let rec eval_ng_tac (text, prefix_len, tac) =
 ;;
       
 let subst_metasenv_and_fix_names s =
-  let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+  let u,h,metasenv, subst,o = s#obj in
   let o = 
     NCicUntrusted.map_obj_kind ~skip_body:true 
      (NCicUntrusted.apply_subst subst []) o
   in
-  { s with NTacStatus.istatus =
-     { s.NTacStatus.istatus with NTacStatus.pstatus =
-        u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
+   s#set_obj (u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
 let rec eval_ncommand opts status (text,prefix_len,cmd) =
@@ -675,52 +673,49 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NQed loc ->
       (match status.GrafiteTypes.ng_status with
-       | GrafiteTypes.ProofMode
-          { NTacStatus.istatus =
-             { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
-            let uri,height,menv,subst,obj_kind = pstatus in
-             if menv <> [] then
-              raise
-               (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
-             else
-              let obj_kind =
-               NCicUntrusted.map_obj_kind 
-                (NCicUntrusted.apply_subst subst []) obj_kind in
-              let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
-              (* fix the height inside the object *)
-              let rec fix () = function 
-                | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
-                   NCic.Const (NReference.reference_of_spec u
-                    (match spec with
-                    | NReference.Def _ -> NReference.Def height
-                    | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-                    | NReference.CoFix _ -> NReference.CoFix height
-                    | NReference.Ind _ | NReference.Con _
-                    | NReference.Decl as s -> s))
-                | t -> NCicUtils.map (fun _ () -> ()) () fix t
-              in
-              let obj_kind = 
-                match obj_kind with
-                | NCic.Fixpoint _ -> 
-                    NCicUntrusted.map_obj_kind (fix ()) obj_kind 
-                | _ -> obj_kind
-              in
-              let obj = uri,height,[],[],obj_kind in
-               NCicTypeChecker.typecheck_obj obj;
-               let estatus = NCicLibrary.add_obj estatus uri obj in
-               let objs = NCicElim.mk_elims obj in
-               let timestamp,uris_rev =
-                 List.fold_left
-                  (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
-                    NCicTypeChecker.typecheck_obj obj;
-                    let estatus = NCicLibrary.add_obj estatus uri obj in
-                     estatus,uri::uris_rev
-                  ) (estatus,[]) objs in
-               let uris = uri::List.rev uris_rev in
-                GrafiteTypes.set_estatus estatus
-                 {status with 
-                  GrafiteTypes.ng_status = 
-                   GrafiteTypes.CommandMode estatus },`New uris
+       | GrafiteTypes.ProofMode estatus ->
+          let uri,height,menv,subst,obj_kind = estatus#obj in
+           if menv <> [] then
+            raise
+             (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
+           else
+            let obj_kind =
+             NCicUntrusted.map_obj_kind 
+              (NCicUntrusted.apply_subst subst []) obj_kind in
+            let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+            (* fix the height inside the object *)
+            let rec fix () = function 
+              | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
+                 NCic.Const (NReference.reference_of_spec u
+                  (match spec with
+                  | NReference.Def _ -> NReference.Def height
+                  | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+                  | NReference.CoFix _ -> NReference.CoFix height
+                  | NReference.Ind _ | NReference.Con _
+                  | NReference.Decl as s -> s))
+              | t -> NCicUtils.map (fun _ () -> ()) () fix t
+            in
+            let obj_kind = 
+              match obj_kind with
+              | NCic.Fixpoint _ -> 
+                  NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+              | _ -> obj_kind
+            in
+            let obj = uri,height,[],[],obj_kind in
+             NCicTypeChecker.typecheck_obj obj;
+             let estatus = NCicLibrary.add_obj estatus uri obj in
+             let objs = NCicElim.mk_elims obj in
+             let timestamp,uris_rev =
+               List.fold_left
+                (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
+                  NCicTypeChecker.typecheck_obj obj;
+                  let estatus = NCicLibrary.add_obj estatus uri obj in
+                   estatus,uri::uris_rev
+                ) (estatus,[]) objs in
+             let uris = uri::List.rev uris_rev in
+              {status with 
+               GrafiteTypes.ng_status = 
+                GrafiteTypes.CommandMode (estatus :> NEstatus.status)},`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.NObj (loc,obj) ->
      let estatus =
@@ -738,9 +733,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
          GrafiteTypes.ng_status = 
           GrafiteTypes.ProofMode
            (subst_metasenv_and_fix_names
-            { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
-             }
+             ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))
+      }
      in
      (match nmenv with
          [] ->