- added and exposed get_current_status_as_xml

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 4751cb23f93b725dd15292f6bac8c95c5711375a..491fe5224f2098cf1fc87765a52c62e5e99db4f4 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -31,34 +31,43 @@ open ProofEngineTypes
 let proof = ref (None : proof option)
 let goal = ref (None : goal option)
 
-let apply_or_can_apply_tactic ~try_only ~tactic =
+let get_current_status_as_xml () =
+  match !proof with
+     None -> assert false
+   | Some (uri, metasenv, bo, ty) ->
+      let currentproof =
+       (*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 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)
+;;
+
+let apply_tactic ~tactic =
  match !proof,!goal with
-    None,_
+  | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
      let (newproof, newgoals) = tactic ~status:(proof', goal') in
-      if not try_only then
-       begin
-        proof := Some newproof;
-        goal :=
-         (match newgoals, newproof with
-             goal::_, _ -> Some goal
-           | [], (_,(goal,_,_)::_,_,_) ->
-           (* the tactic left no open goal ; let's choose the first open goal *)
-(*CSC: here we could implement and use a proof-tree like notion... *)
-              Some goal
-           | _, _ -> None)
-       end
-;;
-
-let apply_tactic = apply_or_can_apply_tactic ~try_only:false;;
-
-let can_apply_tactic ~tactic =
- try
-  apply_or_can_apply_tactic ~try_only:true ~tactic ;
-  true
- with
-  Fail _ -> false
+      proof := Some newproof;
+      goal :=
+       (match newgoals, newproof with
+           goal::_, _ -> Some goal
+         | [], (_,(goal,_,_)::_,_,_) ->
+         (* the tactic left no open goal ; let's choose the first open goal *)
+         (*CSC: here we could implement and use a proof-tree like notion... *)
+            Some goal
+         | _, _ -> None)
 ;;
 
 (* metas_in_term term                                                *)
@@ -163,7 +172,6 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 
   (* primitive tactics *)
 
-let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros ?mk_fresh_name_callback () =
  apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
@@ -229,7 +237,8 @@ let right () = apply_tactic IntroductionTactics.right_tac
 
 let assumption () = apply_tactic VariousTactics.assumption_tac
 
-let generalize term = apply_tactic (VariousTactics.generalize_tac ~term)
+let generalize ?mk_fresh_name_callback terms =
+ apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms)
 
 let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
 let contradiction () = apply_tactic NegationTactics.contradiction_tac
@@ -237,10 +246,10 @@ let contradiction () = apply_tactic NegationTactics.contradiction_tac
 let decompose ~uris_choice_callback term =
  apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term)
 
-(*
-let decide_equality () = apply_tactic VariousTactics.decide_equality_tac
-let compare term1 term2 = apply_tactic (VariousTactics.compare_tac ~term1 ~term2)
-*)
+let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term)
+let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term)
+let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac
+let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term)
 
 (*
 let prova_tatticali () = apply_tactic Tacticals.prova_tac