snapshot

[helm.git] / helm / matita / matitaProof.ml

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
new file mode 100644 (file)
index 0000000..5612043
--- /dev/null
+++ b/helm/matita/matitaProof.ml
@@ -0,0 +1,109 @@
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+class proofStatus ~uri ~typ =
+  object
+    inherit MatitaTypes.subject
+
+    val mutable _proof = (uri, [ 1, [], typ ], Cic.Meta (1, []), typ)
+    val mutable _goal = Some 1
+
+    method proof = _proof
+    method setProof p = _proof <- p
+    method goal = _goal
+    method setGoal g = _goal <- g
+    method status =
+      _proof,
+      (match _goal with Some g -> g | None -> raise MatitaTypes.No_proof)
+    method setStatus (p, g) =
+      _proof <- p;
+      _goal <- Some g
+
+    method to_xml =
+      let (uri, metasenv, bo, ty) = _proof in
+      let currentproof =
+        (* TODO CSC: Wrong: [] is just plainly wrong *)
+        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+      in
+      let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
+        Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
+      in
+      let xml, bodyxml =
+        match Cic2Xml.print_object uri ~ids_to_inner_sorts
+          ~ask_dtd_to_the_getter:true acurrentproof
+        with
+        | xml, Some bodyxml -> xml, bodyxml
+        | _, None -> assert false
+      in
+      (xml, bodyxml)
+
+  end
+
+class proof ~uri ~typ =
+  object
+    val mutable _status = new proofStatus ~uri ~typ
+    method status = _status
+    method setStatus s = _status <- s
+  end
+
+class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) =
+  object
+    val statusBackup = status#status
+
+    method execute () =
+      let (new_proof, new_goals) = tactic status#status in
+      status#setProof new_proof;
+      status#setGoal
+        (match new_goals, new_proof with
+        | goal :: _, _ -> Some goal
+        | [], (_, (goal, _, _) :: _, _, _) ->
+            (* the tactic left no open goal: let's choose the first open goal *)
+            (* TODO CSC: here we could implement and use a proof-tree like
+             * notion... *)
+            Some goal
+        | _, _ -> None);
+      status#notify ()
+
+    method undo () =
+      status#setStatus statusBackup;
+      status#notify ()
+  end
+
+let intros ?namer =
+  new tacticCommand
+    ~tactic:(PrimitiveTactics.intros_tac ?mk_fresh_name_callback:namer ())
+
+let reflexivity = new tacticCommand ~tactic:EqualityTactics.reflexivity_tac
+let symmetry =  new tacticCommand ~tactic:EqualityTactics.symmetry_tac
+let transitivity term =
+  new tacticCommand ~tactic:(EqualityTactics.transitivity_tac ~term)
+
+let exists = new tacticCommand ~tactic:IntroductionTactics.exists_tac
+let split = new tacticCommand ~tactic:IntroductionTactics.split_tac
+let left = new tacticCommand ~tactic:IntroductionTactics.left_tac
+let right = new tacticCommand ~tactic:IntroductionTactics.right_tac
+
+let assumption = new tacticCommand ~tactic:VariousTactics.assumption_tac
+