ProofEngine.proof is now an abstract data type (since we plan to have OMDoc

in the future as the persistent format).

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7c28c22ced477ee65adad54bba34af1d2c5ed763..7ed63cb102abdbc20c0072b4812254cda01a4488 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -480,7 +480,7 @@ let save_obj uri obj =
 ;;
 
 let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
      if
@@ -569,10 +569,10 @@ let mk_fresh_name_callback context name ~typ =
 let refresh_proof (output : TermViewer.proof_viewer) =
  try
   let uri,currentproof =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
-       ProofEngine.proof := Some(uri,metasenv,bo,ty);
+       ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ;
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
@@ -587,7 +587,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
    ignore (output#load_proof uri currentproof)
  with
   e ->
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,metasenv,bo,ty) ->
 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
@@ -606,7 +606,7 @@ let refresh_goals ?(empty_notebook=true) notebook =
        notebook#proofw#unload
    | Some metano ->
       let metasenv =
-       match !ProofEngine.proof with
+       match ProofEngine.get_proof () with
           None -> assert false
         | Some (_,metasenv,_,_) -> metasenv
       in
@@ -642,7 +642,7 @@ let metano =
    | Some m -> m
 in
 let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (_,metasenv,_,_) -> metasenv
 in
@@ -701,8 +701,8 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.proof :=
-             Some (uri, metasenv, bo, ty) ;
+            ProofEngine.set_proof
+             (Some (uri, metasenv, bo, ty)) ;
             ProofEngine.goal :=
              (match metasenv with
                  [] -> None
@@ -876,7 +876,7 @@ let setgoal metano =
  let notebook = (rendering_window ())#notebook in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let metasenv =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> assert false
     | Some (_,metasenv,_,_) -> metasenv
   in
@@ -1579,8 +1579,8 @@ prerr_endline ("######################## " ^ xxx) ;
   try
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
-     ProofEngine.proof :=
-      Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
+     ProofEngine.set_proof
+      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
      ProofEngine.goal := Some 1 ;
      refresh_goals notebook ;
      refresh_proof output ;
@@ -1622,7 +1622,7 @@ let check scratch_window () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let metasenv =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> []
     | Some (_,metasenv,_,_) -> metasenv
   in
@@ -1671,8 +1671,8 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.proof :=
-       Some (uri, metasenv, bo, ty) ;
+      ProofEngine.set_proof
+       (Some (uri, metasenv, bo, ty)) ;
       ProofEngine.goal := None ;
       refresh_goals notebook ;
       refresh_proof output ;
@@ -2143,7 +2143,7 @@ let searchPattern () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
     let proof =
-     match !ProofEngine.proof with
+     match ProofEngine.get_proof () with
         None -> assert false
       | Some proof -> proof
     in
@@ -2830,7 +2830,7 @@ class rendering_window output (notebook : notebook) =
    ~callback:
      (function _ ->
        ApplyStylesheets.reload_stylesheets () ;
-       if !ProofEngine.proof <> None then
+       if ProofEngine.get_proof () <> None then
         try
          refresh_goals notebook ;
          refresh_proof output

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 31804290930e10986ab38194c8a709e3bdc9a2b6..79b489f548532023344c2498d981d92611f12921 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -111,7 +111,7 @@ module Make (C: Callbacks) : Tactics =
   struct
 
    let call_tactic tactic () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      begin
       try
@@ -123,29 +123,29 @@ module Make (C: Callbacks) : Tactics =
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals ()
        | RefreshProofException e ->
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals () ;
           C.refresh_proof ()
        | e ->
           C.output_html
            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal
      end
 
    let call_tactic_with_input tactic ?term () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      let uri,metasenv,bo,ty =
-      match !ProofEngine.proof with
+      match ProofEngine.get_proof () with
          None -> assert false
        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
      in
@@ -165,7 +165,7 @@ module Make (C: Callbacks) : Tactics =
          | Some t -> (C.term_editor ())#set_term t);
          (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
         in
-         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+         ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
          tactic expr ;
          C.refresh_goals () ;
          C.refresh_proof () ;
@@ -175,27 +175,27 @@ module Make (C: Callbacks) : Tactics =
            C.output_html
             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
              "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal ;
            C.refresh_goals ()
         | RefreshProofException e ->
            C.output_html
             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
              "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal ;
            C.refresh_goals () ;
            C.refresh_proof ()
         | e ->
            C.output_html
             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal
 
   let call_tactic_with_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
@@ -209,21 +209,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->
@@ -236,7 +236,7 @@ module Make (C: Callbacks) : Tactics =
   let call_tactic_with_goal_inputs tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      try
       match (C.sequent_viewer ())#get_selected_terms with
@@ -252,34 +252,34 @@ module Make (C: Callbacks) : Tactics =
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals ()
       | RefreshProofException e ->
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals () ;
          C.refresh_proof ()
       | e ->
          C.output_html
           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal
 
   let call_tactic_with_input_and_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
          begin
           try
            let uri,metasenv,bo,ty =
-            match !ProofEngine.proof with
+            match ProofEngine.get_proof () with
                None -> assert false
              | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
            in
@@ -294,7 +294,7 @@ module Make (C: Callbacks) : Tactics =
             let (metasenv',expr) =
              (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
             in
-             ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+             ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
              tactic ~goal_input:term ~input:expr ;
              C.refresh_goals () ;
              C.refresh_proof () ;
@@ -304,21 +304,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->
@@ -376,7 +376,7 @@ module Make (C: Callbacks) : Tactics =
   let call_tactic_with_hypothesis_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_hypotheses with
        [hypothesis] ->
@@ -390,21 +390,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 448c83a18fe925f0db84af9c2ded5cb45ebe8f15..5d06c95d21b55a94c72178eba18d9198771d68db 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -90,7 +90,7 @@ let to_sequent id ids_to_terms ids_to_father_ids =
   let term = Hashtbl.find ids_to_terms id in
   let context = get_context ids_to_terms ids_to_father_ids id in
    let metasenv =
-    match !P.proof with
+    match P.get_proof () with
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in
@@ -106,7 +106,7 @@ let focus id ids_to_terms ids_to_father_ids =
   let term = Hashtbl.find ids_to_terms id in
   let context = get_context ids_to_terms ids_to_father_ids id in
    let metasenv =
-    match !P.proof with
+    match P.get_proof () with
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 491fe5224f2098cf1fc87765a52c62e5e99db4f4..eeef8ff2d27e172c3083b5619d5fae62608f0afc 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -31,8 +31,11 @@ open ProofEngineTypes
 let proof = ref (None : proof option)
 let goal = ref (None : goal option)
 
+let get_proof () = !proof;;
+let set_proof p = proof := p;;
+
 let get_current_status_as_xml () =
-  match !proof with
+  match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
       let currentproof =
@@ -54,12 +57,12 @@ let get_current_status_as_xml () =
 ;;
 
 let apply_tactic ~tactic =
- match !proof,!goal with
+ match get_proof (),!goal with
   | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
      let (newproof, newgoals) = tactic ~status:(proof', goal') in
-      proof := Some newproof;
+      set_proof (Some newproof);
       goal :=
        (match newgoals, newproof with
            goal::_, _ -> Some goal
@@ -115,7 +118,7 @@ let metas_in_term term =
 (* are efficiency reasons.                                                   *)
 let perforate context term ty =
  let module C = Cic in
-  match !proof with
+  match get_proof () with
      None -> assert false
    | Some (uri,metasenv,bo,gty as proof') ->
       let newmeta = new_meta proof' in
@@ -137,7 +140,7 @@ let perforate context term ty =
           let metasenv'' =
            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
           in
-           proof := Some (uri,metasenv'',bo',gty) ;
+           set_proof (Some (uri,metasenv'',bo',gty)) ;
            goal := Some newmeta
 
 
@@ -148,7 +151,7 @@ let perforate context term ty =
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function terms ty =
  let metasenv =
-  match !proof with
+  match get_proof () with
      None -> []
    | Some (_,metasenv,_,_) -> metasenv
  in

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 4b7db8fe6346dce46302692bad87de265fa89648..dd7e1c4128b48df9eb5313994656c837e09d71b1 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -24,7 +24,8 @@
  *)
 
   (* proof engine status *)
-val proof : ProofEngineTypes.proof option ref
+val get_proof : unit -> ProofEngineTypes.proof option
+val set_proof : ProofEngineTypes.proof option -> unit
 val goal : ProofEngineTypes.goal option ref
 
   (** return a pair of "xml" (as defined in Xml module) representing the current
@@ -99,8 +100,3 @@ val injection : Cic.term -> unit
 val discriminate : Cic.term -> unit
 val decide_equality : unit -> unit
 val compare : Cic.term -> unit
-
-
-(*
-val prova_tatticali : unit -> unit
-*)