More statuses converted to objects.

[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 4abfc933eb7b59b83b413d07c1128e4e92d3ea37..b1cc9d671f5acd17f0fcbf64931c4b220c3e7fd2 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -86,11 +86,11 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
-       ~automation_cache:status.GrafiteTypes.automation_cache
+       ~automation_cache:status#automation_cache
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.AutoBatch (_,params) ->
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
-       ~automation_cache:status.GrafiteTypes.automation_cache
+       ~automation_cache:status#automation_cache
   | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
       Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
         ~pattern what
@@ -112,7 +112,7 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Demodulate (_, params) -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~params 
-          ~automation_cache:status.GrafiteTypes.automation_cache
+          ~automation_cache:status#automation_cache
   | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -183,12 +183,12 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
   | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
      Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1
+      ~automation_cache:status#automation_cache just ty id t1
   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
      Declarative.we_need_to_prove t id t2
   | GrafiteAst.Bydone (_, t) ->
      Declarative.bydone ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache t
+      ~automation_cache:status#automation_cache t
   | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
      Declarative.we_proceed_by_cases_on t t1
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
@@ -197,14 +197,14 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
      Declarative.existselim ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+      ~automation_cache:status#automation_cache just id1 t1 id2 t2
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,just,id1,t1,id2,t2) ->
      Declarative.andelim ~dbd:(LibraryDb.instance ())
-      ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+      ~automation_cache:status#automation_cache just id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
      Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
-      ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont
+      ~automation_cache:status#automation_cache termine t1 t2 cont
 
 let classify_tactic tactic = 
   match tactic with
@@ -347,13 +347,13 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
   proof', opened_goals
  in
  let incomplete_proof =
-   match status.GrafiteTypes.proof_status with
+   match status#proof_status with
    | GrafiteTypes.Incomplete_proof p -> p
    | _ -> assert false
  in
- { status with GrafiteTypes.proof_status =
-    GrafiteTypes.Incomplete_proof
-     { incomplete_proof with GrafiteTypes.proof = proof } },
+  status#set_proof_status
+   (GrafiteTypes.Incomplete_proof
+     { incomplete_proof with GrafiteTypes.proof = proof }),
  opened_goals, closed_goals
 
 let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (status, goal) =
@@ -381,13 +381,13 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (
   proof', opened_goals
  in
  let incomplete_proof =
-   match status.GrafiteTypes.proof_status with
+   match status#proof_status with
    | GrafiteTypes.Incomplete_proof p -> p
    | _ -> assert false
  in
- { status with GrafiteTypes.proof_status =
-    GrafiteTypes.Incomplete_proof
-     { incomplete_proof with GrafiteTypes.proof = proof } },
+  status#set_proof_status
+   (GrafiteTypes.Incomplete_proof
+     { incomplete_proof with GrafiteTypes.proof = proof }),
  opened_goals, closed_goals
 type eval_ast =
  {ea_go:
@@ -508,7 +508,7 @@ let add_coercions_of_lemmas lemmas status =
       lemmas
   in
   let status = GrafiteTypes.add_moo_content moo_content status in 
-  {status with GrafiteTypes.coercions = CoercDb.dump () }, 
+   status#set_coercions (CoercDb.dump ()), 
   lemmas
 
 let eval_coercion status ~add_composites uri arity saturations =
@@ -581,11 +581,11 @@ let non_punctuation_tactical_of_ast (text,prefix_len,punct) =
 let eval_tactical status tac =
   let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in
   let status =  (* is proof completed? *)
-    match status.GrafiteTypes.proof_status with
+    match status#proof_status with
     | GrafiteTypes.Incomplete_proof
        { GrafiteTypes.stack = stack; proof = proof }
       when Continuationals.Stack.is_empty stack ->
-        { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof }
+       status#set_proof_status (GrafiteTypes.Proof proof)
     | _ -> status
   in
   status
@@ -672,7 +672,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NQed loc ->
-      (match status.GrafiteTypes.ng_status with
+      (match status#ng_status with
        | GrafiteTypes.ProofMode estatus ->
           let uri,height,menv,subst,obj_kind = estatus#obj in
            if menv <> [] then
@@ -713,13 +713,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                    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
+              status#set_ng_status
+               (GrafiteTypes.CommandMode (estatus :> NEstatus.status)),`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.NObj (loc,obj) ->
      let estatus =
-       match status.GrafiteTypes.ng_status with
+       match status#ng_status with
        | GrafiteTypes.ProofMode _ -> assert false
        | GrafiteTypes.CommandMode es -> es 
      in
@@ -729,12 +728,10 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
      let uri,height,nmenv,nsubst,nobj = obj in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
      let status =
-      { status with
-         GrafiteTypes.ng_status = 
-          GrafiteTypes.ProofMode
-           (subst_metasenv_and_fix_names
-             ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))
-      }
+      status#set_ng_status
+       (GrafiteTypes.ProofMode
+         (subst_metasenv_and_fix_names
+           ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus)))
      in
      (match nmenv with
          [] ->
@@ -754,13 +751,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        assert false (* TODO: for user input *)
   | GrafiteAst.Index (loc,Some key,uri) -> 
       let universe = 
-        status.GrafiteTypes.automation_cache.AutomationCache.univ
+        status#automation_cache.AutomationCache.univ
       in
       let universe = Universe.index universe key (CicUtil.term_of_uri uri) in
       let cache = { 
-        status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } 
+        status#automation_cache with AutomationCache.univ = universe } 
       in
-      let status = { status with GrafiteTypes.automation_cache = cache } in
+      let status = status#set_automation_cache cache in
 (* debug
       let msg =
        let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
@@ -772,20 +769,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,`Old [] 
   | GrafiteAst.Select (_,uri) as cmd ->
-      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old []
+      if List.mem cmd status#moo_content_rev then status, `Old []
       else 
        let cache = 
-         AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+         AutomationCache.add_term_to_active status#automation_cache
            [] [] [] (CicUtil.term_of_uri uri) None
        in
-       let status = { status with GrafiteTypes.automation_cache = cache } in
+       let status = status#set_automation_cache cache in
        let status = GrafiteTypes.add_moo_content [cmd] status in
        status, `Old []
   | GrafiteAst.Pump (_,steps) ->
       let cache = 
-        AutomationCache.pump status.GrafiteTypes.automation_cache steps
+        AutomationCache.pump status#automation_cache steps
       in
-      let status = { status with GrafiteTypes.automation_cache = cache } in
+      let status = status#set_automation_cache cache in
       status, `Old []
   | GrafiteAst.PreferCoercion (loc, coercion) ->
      eval_prefer_coercion status coercion
@@ -849,7 +846,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Print (_,_) -> status,`Old []
   | GrafiteAst.Qed loc ->
       let uri, metasenv, _subst, bo, ty, attrs =
-        match status.GrafiteTypes.proof_status with
+        match status#proof_status with
         | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) ->
             uri, metasenv, subst, body, ty, attrs
         | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) -> 
@@ -867,7 +864,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
       let status, lemmas = add_obj uri obj status in
-       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       status#set_proof_status GrafiteTypes.No_proof,
         (*CSC: I throw away the arities *)
         `Old (uri::lemmas)
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
@@ -924,10 +921,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          let _subst = [] in
          let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
-         { status with GrafiteTypes.proof_status =
-            GrafiteTypes.Incomplete_proof
-            { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
-         },
+          status#set_proof_status
+           (GrafiteTypes.Incomplete_proof
+            { GrafiteTypes.proof = initial_proof; stack = initial_stack }),
           `Old []
      | _ ->
          if metasenv <> [] then
@@ -936,12 +932,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
             CicMetaSubst.ppmetasenv [] metasenv));
          let status, lemmas = add_obj uri obj status in 
          let status,new_lemmas = add_coercions_of_lemmas lemmas status in
-          {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+          status#set_proof_status GrafiteTypes.No_proof,
            `Old (uri::new_lemmas@lemmas)
  in
-  match status.GrafiteTypes.proof_status with
+  match status#proof_status with
      GrafiteTypes.Intermediate _ ->
-      {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
+      status#set_proof_status GrafiteTypes.No_proof,uris
    | _ -> status,uris
 
 } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
@@ -965,7 +961,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
-      (match status.GrafiteTypes.ng_status with
+      (match status#ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus =
@@ -975,7 +971,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               subst_metasenv_and_fix_names nstatus)
             nstatus tacl
          in
-         { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+          status#set_ng_status (GrafiteTypes.ProofMode nstatus),
          `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status =