X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=4a730283208354abffc7529ac3822640747923f0;hb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;hp=e5ad5973e6af05a67fb3be44640171e666933eb7;hpb=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e5ad5973e..4a7302832 100644
--- 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 () =
"
Objects that can actually be applied:
" ^
String.concat "
" uris' ^ exc ^
" Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "
"
+ string_of_int (List.length uris - List.length uris') ^ "" ^
+ " Number of good matches: " ^
+ string_of_int (List.length uris') ^ "
"
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:""
@@ -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))