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 e5ad5973e6af05a67fb3be44640171e666933eb7..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) *)
 
@@ -707,8 +713,8 @@ let exact rendering_window =
 let apply rendering_window =
  call_tactic_with_input ProofEngine.apply rendering_window
 ;;
-let elimintrossimpl rendering_window =
- call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
+let elimsimplintros rendering_window =
+ call_tactic_with_input ProofEngine.elim_simpl_intros rendering_window
 ;;
 let elimtype rendering_window =
  call_tactic_with_input ProofEngine.elim_type rendering_window
@@ -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 =
@@ -1267,7 +1295,9 @@ let searchPattern rendering_window () =
             " <h1>Objects that can actually be applied: </h1> " ^
             String.concat "<br>" uris' ^ exc ^
             " <h1>Number of false matches: " ^
-             string_of_int (List.length uris - List.length uris') ^ "</h1>"
+             string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+            " <h1>Number of good matches: " ^
+             string_of_int (List.length uris') ^ "</h1>"
            in
             output_html outputhtml html' ;
             let uri' = user_uri_choice uris' in
@@ -1546,8 +1576,8 @@ class rendering_window output proofw (label : GMisc.label) =
  let applyb =
   GButton.button ~label:"Apply"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let elimintrossimplb =
-  GButton.button ~label:"ElimIntrosSimpl"
+ let elimsimplintrosb =
+  GButton.button ~label:"ElimSimplIntros"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
  let elimtypeb =
   GButton.button ~label:"ElimType"
@@ -1590,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>"
@@ -1631,7 +1682,7 @@ object(self)
   ignore(searchpatternb#connect#clicked (searchPattern self)) ;
   ignore(exactb#connect#clicked (exact self)) ;
   ignore(applyb#connect#clicked (apply self)) ;
-  ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
+  ignore(elimsimplintrosb#connect#clicked (elimsimplintros self)) ;
   ignore(elimtypeb#connect#clicked (elimtype self)) ;
   ignore(whdb#connect#clicked (whd self)) ;
   ignore(reduceb#connect#clicked (reduce self)) ;
@@ -1645,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))