Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ce2af709a08427404ca712d5cf7779322fed4c80..9bab1ff9b6971965c6e1d28f29173ff342289a48 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -60,26 +60,14 @@ let htmlfooter =
  "</html>"
 ;;
 
-(* TASSI *)
-let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
-let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
-
-(*
-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 *)
 
-(* TASSI *)
-let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
-let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
-
-(*
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
-*)
+let innertypesfile = "/home/galata/miohelm/innertypes";;
+let constanttypefile = "/home/galata/miohelm/constanttype";;
 
 let empty_id_to_uris = ([],function _ -> None);;
 
@@ -1909,9 +1897,17 @@ let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
 let reflexivity = call_tactic ProofEngine.reflexivity;;
 let symmetry = call_tactic ProofEngine.symmetry;;
 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
+let exists = call_tactic ProofEngine.exists;;
+let split = call_tactic ProofEngine.split;;
 let left = call_tactic ProofEngine.left;;
 let right = call_tactic ProofEngine.right;;
 let assumption = call_tactic ProofEngine.assumption;;
+let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
+let absurd = call_tactic_with_input ProofEngine.absurd;;
+let contradiction = call_tactic ProofEngine.contradiction;;
+(* Galla: come dare alla tattica la lista di termini da decomporre?
+let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
+*)
 
 let whd_in_scratch scratch_window =
  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
@@ -2355,6 +2351,12 @@ object(self)
    let transitivityb =
     GButton.button ~label:"Transitivity"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let existsb =
+    GButton.button ~label:"Exists"
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let splitb =
+    GButton.button ~label:"Split"
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let leftb =
     GButton.button ~label:"Left"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2364,9 +2366,21 @@ object(self)
    let assumptionb =
     GButton.button ~label:"Assumption"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let generalizeb =
+    GButton.button ~label:"Generalize"
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox6 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+   let absurdb =
+    GButton.button ~label:"Absurd"
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+   let contradictionb =
+    GButton.button ~label:"Contradiction"
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let searchpatternb =
     GButton.button ~label:"SearchPattern_Apply"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+
    ignore(exactb#connect#clicked exact) ;
    ignore(applyb#connect#clicked apply) ;
    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
@@ -2386,9 +2400,14 @@ object(self)
    ignore(reflexivityb#connect#clicked reflexivity) ;
    ignore(symmetryb#connect#clicked symmetry) ;
    ignore(transitivityb#connect#clicked transitivity) ;
+   ignore(existsb#connect#clicked exists) ;
+   ignore(splitb#connect#clicked split) ;
    ignore(leftb#connect#clicked left) ;
    ignore(rightb#connect#clicked right) ;
    ignore(assumptionb#connect#clicked assumption) ;
+   ignore(generalizeb#connect#clicked generalize) ;
+   ignore(absurdb#connect#clicked absurd) ;
+   ignore(contradictionb#connect#clicked contradiction) ;
    ignore(introsb#connect#clicked intros) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
@@ -2638,12 +2657,17 @@ let initialize_everything () =
 
 let _ =
  if !usedb then
+(*<<<<<<< gTopLevel.ml
+(* Mqint.init "dbname=helm_mowgli" ; *)
+Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
+=======*)
   begin
    Mqint.set_database Mqint.postgres_db ;
    (* Mqint.init "dbname=helm_mowgli" ; *)
    (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
    Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ;
   end ;
+(*>>>>>>> 1.35.2.34*)
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  if !usedb then Mqint.close ();