Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry...

[helm.git] / helm / gTopLevel / gTopLevel.ml
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml

index d0aef1a04210608320f73eaf3b50a8baebb49212..4a730283208354abffc7529ac3822640747923f0 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -61,15 +61,21 @@ let htmlfooter =
  
  (*
  let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
-*)
  let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+*)
+
+let prooffile = "/home/galata/miohelm/currentproof";;
+let prooffiletype = "/home/galata/miohelm/currentprooftype";;
+
  (*CSC: the getter should handle the innertypes, not the FS *)
  (*
  let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
-*)
  let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+*)
+
+let innertypesfile = "/home/galata/miohelm/innertypes";;
+let constanttypefile = "/home/galata/miohelm/constanttype";;
+
  
  (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  
@@ -747,7 +753,29 @@ let fourier rendering_window =
  let rewritesimpl rendering_window =
   call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
  ;;
-
+let reflexivity rendering_window =
+ call_tactic ProofEngine.reflexivity rendering_window
+;;
+let symmetry rendering_window =
+ call_tactic ProofEngine.symmetry rendering_window
+;;
+let transitivity rendering_window =
+ call_tactic_with_input ProofEngine.transitivity rendering_window
+;;
+let left rendering_window =
+ call_tactic ProofEngine.left rendering_window
+;;
+let right rendering_window =
+ call_tactic ProofEngine.right rendering_window
+;;
+let assumption rendering_window =
+ call_tactic ProofEngine.assumption rendering_window
+;;
+(*
+let prova_tatticali rendering_window =
+ call_tactic ProofEngine.prova_tatticali rendering_window
+;;
+*)
  
  
  let whd_in_scratch scratch_window =
@@ -1592,6 +1620,27 @@ class rendering_window output proofw (label : GMisc.label) =
   let rewritesimplb =
    GButton.button ~label:"RewriteSimpl ->"
     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let reflexivityb =
+  GButton.button ~label:"Reflexivity"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let symmetryb =
+  GButton.button ~label:"Symmetry"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let transitivityb =
+  GButton.button ~label:"Transitivity"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let leftb =
+  GButton.button ~label:"Left"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rightb =
+  GButton.button ~label:"Right"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let assumptionb =
+  GButton.button ~label:"Assumption"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let prova_tatticalib =
+  GButton.button ~label:"Prova_tatticali"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
   let outputhtml =
    GHtml.xmhtml
     ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1647,6 +1696,15 @@ object(self)
    ignore(clearb#connect#clicked (clear self)) ;
    ignore(fourierb#connect#clicked (fourier self)) ;
    ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
+  ignore(reflexivityb#connect#clicked (reflexivity self)) ;
+  ignore(symmetryb#connect#clicked (symmetry self)) ;
+  ignore(transitivityb#connect#clicked (transitivity self)) ;
+  ignore(leftb#connect#clicked (left self)) ;
+  ignore(rightb#connect#clicked (right self)) ;
+  ignore(assumptionb#connect#clicked (assumption self)) ;
+(*
+  ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ;
+*)
    ignore(introsb#connect#clicked (intros self)) ;
    Logger.log_callback :=
     (Logger.log_to_html ~print_and_flush:(output_html outputhtml))