From 015263908d9142798bcbddbe4c4d13f71e08c5c3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 1 Oct 2004 12:41:18 +0000 Subject: [PATCH] snapshot --- helm/matita/.depend | 6 ++ helm/matita/Makefile.in | 3 +- helm/matita/buildTimeConf.ml.in | 2 + helm/matita/configure.ac | 5 + helm/matita/matita.conf.xml.sample | 2 + helm/matita/matita.glade | 84 +++++++++++++-- helm/matita/matita.ml | 49 +++++++-- helm/matita/matitaGeneratedGui.ml | 68 +++++++----- helm/matita/matitaGeneratedGui.mli | 61 ++++++----- helm/matita/matitaInterpreter.ml | 122 +++++++++++++++++---- helm/matita/matitaInterpreter.mli | 2 +- helm/matita/matitaMathView.ml | 163 +++++++++++++++++++++++++++++ helm/matita/matitaMathView.mli | 37 +++++++ helm/matita/matitaProof.ml | 117 ++++++--------------- helm/matita/matitaProof.mli | 36 ++----- helm/matita/matitaTypes.ml | 94 +++++++++-------- 16 files changed, 602 insertions(+), 249 deletions(-) create mode 100644 helm/matita/matitaMathView.ml create mode 100644 helm/matita/matitaMathView.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 8d7e4e7b9..0034c0c4a 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,3 +1,5 @@ +logicalOperations.cmo: logicalOperations.cmi +logicalOperations.cmx: logicalOperations.cmi matitaConsole.cmo: matitaConsole.cmi matitaConsole.cmx: matitaConsole.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi @@ -14,6 +16,8 @@ matitaInterpreter.cmo: matitaConsole.cmi matitaProof.cmi matitaTypes.cmo \ matitaInterpreter.cmi matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \ matitaInterpreter.cmi +matitaMathView.cmo: matitaTypes.cmo matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaMathView.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ matitaGui.cmi matitaInterpreter.cmi matitaProof.cmi matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ @@ -22,8 +26,10 @@ matitaProof.cmo: matitaTypes.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmx: buildTimeConf.cmx +logicalOperations.cmi: matitaTypes.cmo matitaDisambiguator.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo matitaGui.cmi: matitaConsole.cmi matitaGeneratedGui.cmi matitaInterpreter.cmi: matitaConsole.cmi matitaTypes.cmo +matitaMathView.cmi: matitaTypes.cmo matitaProof.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 144ba5677..4dc9731b3 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -20,7 +20,8 @@ CMOS = \ matitaGui.cmo \ matitaProof.cmo \ matitaDisambiguator.cmo \ - matitaInterpreter.cmo + matitaInterpreter.cmo \ + matitaMathView.cmo CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) all: matita diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 525c678b4..665bb4908 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -25,3 +25,5 @@ let debug = @DEBUG@;; +module Transformer = @TRANSFORMER_MODULE@;; + diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index bfaea8406..0602d067d 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -29,12 +29,14 @@ fi FINDLIB_REQUIRES="\ lablgtk2.glade \ +lablgtkmathview \ pcre \ helm-cic_omdoc \ helm-cic_transformations \ helm-registry \ helm-tactics \ helm-xml \ +helm-xmldiff \ helm-disambiguator \ helm-mathql_interpreter \ " @@ -80,8 +82,11 @@ if test "$DEBUG" = "true"; then echo "debugging enabled" fi +TRANSFORMER_MODULE=ApplyTransformation + AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) +AC_SUBST(TRANSFORMER_MODULE) AC_SUBST(FINDLIB_REQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 3209bf1ab..7df0d1961 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -8,6 +8,7 @@ mathql_db_map.txt
mowgli.cs.unibo.it + mowgli @@ -29,5 +30,6 @@
remote http://mowgli.cs.unibo.it:58081/ +
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index de66dbf30..07c46bd4b 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -13,6 +13,11 @@ 600 True False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST @@ -328,10 +333,17 @@ 525 True False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST True + True + False @@ -342,14 +354,7 @@ GTK_CORNER_TOP_LEFT - - True - GTK_SHADOW_IN - - - - - + @@ -365,6 +370,11 @@ True True False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -373,6 +383,7 @@ True True GTK_RELIEF_NORMAL + True @@ -382,6 +393,7 @@ True True GTK_RELIEF_NORMAL + True @@ -396,10 +408,17 @@ False False False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST True + True + False @@ -422,6 +441,7 @@ button1 True GTK_RELIEF_NORMAL + True @@ -433,6 +453,7 @@ button2 True GTK_RELIEF_NORMAL + True @@ -444,6 +465,7 @@ button3 True GTK_RELIEF_NORMAL + True @@ -455,6 +477,7 @@ button4 True GTK_RELIEF_NORMAL + True @@ -492,6 +515,11 @@ True False False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -513,6 +541,7 @@ gtk-cancel True GTK_RELIEF_NORMAL + True -6 @@ -525,6 +554,7 @@ gtk-ok True GTK_RELIEF_NORMAL + True -5 @@ -568,6 +598,11 @@ True False False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -589,6 +624,7 @@ gtk-ok True GTK_RELIEF_NORMAL + True -5 @@ -616,6 +652,11 @@ True True False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -637,6 +678,7 @@ gtk-cancel True GTK_RELIEF_NORMAL + True -6 @@ -647,6 +689,7 @@ True True GTK_RELIEF_NORMAL + True 0 @@ -656,6 +699,10 @@ 0.5 0 0 + 0 + 0 + 0 + 0 @@ -716,6 +763,7 @@ Try Constants True GTK_RELIEF_NORMAL + True 0 @@ -726,6 +774,7 @@ True True GTK_RELIEF_NORMAL + True 0 @@ -735,6 +784,10 @@ 0.5 0 0 + 0 + 0 + 0 + 0 @@ -918,6 +971,11 @@ True True False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -939,6 +997,7 @@ gtk-help True GTK_RELIEF_NORMAL + True -11 @@ -951,6 +1010,7 @@ gtk-cancel True GTK_RELIEF_NORMAL + True -6 @@ -963,6 +1023,7 @@ gtk-ok True GTK_RELIEF_NORMAL + True -5 @@ -1024,6 +1085,11 @@ False True False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST True @@ -1045,6 +1111,7 @@ gtk-cancel True GTK_RELIEF_NORMAL + True -6 @@ -1057,6 +1124,7 @@ gtk-ok True GTK_RELIEF_NORMAL + True -5 diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 8954ec704..5fb0cb906 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -54,12 +54,45 @@ let disambiguator = ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () +let proof_viewer = + let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in + MatitaMathView.proof_viewer ~mml_of_cic_object ~show:true + ~packing:(gui#proof#scrolledProof#add) () +(* +let sequent_viewer = + let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in + MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true + ~packing:(gui#main#scrolledSequents#add) () +*) -let new_proof proof = - (* TODO Zack: high level function which create a new proof object and register - * to it the widgets which must be refreshed upon status changes *) -(* proof#status#attach ... *) - proof#status#notify (); +let new_proof (proof: MatitaTypes.proof) = + (* TODO Zack a lot: + * - ids_to_inner_types, ids_to_inner_sorts handling + * - sequent viewer notification + *) + let xmldump_observer _ (status, _) = print_endline proof#toString in + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + xmldump_observer); +(* + let proof_observer _ (status, ()) = +prerr_endline "proof_observer"; + let ((uri_opt, metasenv, bo, ty), _) = status in + let uri = MatitaTypes.unopt_uri uri_opt in + (* TODO CSC [] is wrong *) + let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in +try + ignore (proof_viewer#load_proof uri proof) +with exn -> +prerr_endline "proof_observer exception:"; +prerr_endline (Printexc.to_string exn); +raise exn + in + let proof_observer_id = + proof#attach_observer ~interested_in:StatefulProofEngine.all_events + proof_observer + in +*) + proof#notify; set_proof (Some proof) let quit () = (* quit program, asking for confirmation if needed *) @@ -94,10 +127,10 @@ let _ = () (* abort new proof process *) else let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in - let (env, metasenv, term) = + let (env, metasenv, expr) = disambiguator#disambiguateTerm (Stream.of_string input) in - let proof = MatitaProof.proof ~typ:term ~metasenv () in + let proof = MatitaProof.proof ~typ:expr ~metasenv () in new_proof proof)) (** *) @@ -129,7 +162,7 @@ let _ = prerr_endline (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ())); addDebugItem "dump proof status to stdout" (fun _ -> - print_endline ((get_proof ())#status#toString)); + print_endline ((get_proof ())#toString)); end (** *) diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 5ef77f8f3..09ecc1c57 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -169,10 +169,6 @@ class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata)) method scrolledProof = scrolledProof - val viewport1 = - new GBin.viewport (GtkBin.Viewport.cast - (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata)) - method viewport1 = viewport1 method reparent parent = proofWinEventBox#misc#reparent parent; toplevel#destroy () @@ -220,6 +216,10 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata)) method vbox1 = vbox1 + val vbuttonbox1 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"vbuttonbox1" ~info:"GtkVButtonBox" xmldata)) + method vbuttonbox1 = vbuttonbox1 val button1 = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"button1" ~info:"GtkButton" xmldata)) @@ -245,18 +245,22 @@ class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val confirmationDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val confirmationDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) method confirmationDialog = confirmationDialog val dialog_vbox1 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata)) method dialog_vbox1 = dialog_vbox1 + val dialog_action_area1 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area1 = dialog_action_area1 val confirmationDialogCancelButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata)) @@ -278,18 +282,22 @@ class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val aboutWin : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val aboutWin = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata)) method aboutWin = aboutWin val dialog_vbox2 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"dialog-vbox2" ~info:"GtkVBox" xmldata)) method dialog_vbox2 = dialog_vbox2 + val dialog_action_area2 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area2" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area2 = dialog_action_area2 val aboutDismissButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata)) @@ -303,18 +311,22 @@ class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val uriChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val uriChoiceDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) method uriChoiceDialog = uriChoiceDialog val dialog_vbox3 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata)) method dialog_vbox3 = dialog_vbox3 + val dialog_action_area3 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area3 = dialog_action_area3 val uriChoiceAbortButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata)) @@ -400,18 +412,22 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val interpChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val interpChoiceDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata)) method interpChoiceDialog = interpChoiceDialog val dialog_vbox4 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"dialog-vbox4" ~info:"GtkVBox" xmldata)) method dialog_vbox4 = dialog_vbox4 + val dialog_action_area4 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area4" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area4 = dialog_action_area4 val interpChoiceHelpButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata)) @@ -441,18 +457,22 @@ class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val emptyDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast + val emptyDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) method emptyDialog = emptyDialog val emptyDialogVBox = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata)) method emptyDialogVBox = emptyDialogVBox + val dialog_action_area5 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area5 = dialog_action_area5 val emptyDialogCancelButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata)) diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index e2aa8cb98..2889d9279 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -90,7 +90,6 @@ class proofWin : val proofWinEventBox : GBin.event_box val scrolledProof : GBin.scrolled_window val toplevel : GWindow.window - val viewport1 : GBin.viewport val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit @@ -99,7 +98,6 @@ class proofWin : method reparent : GObj.widget -> unit method scrolledProof : GBin.scrolled_window method toplevel : GWindow.window - method viewport1 : GBin.viewport method xml : Glade.glade_xml Gtk.obj end class fileSelectionWin : @@ -135,6 +133,7 @@ class toolBarWin : val toolBarWin : GWindow.window val toplevel : GWindow.window val vbox1 : GPack.box + val vbuttonbox1 : GPack.button_box val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method button1 : GButton.button @@ -147,6 +146,7 @@ class toolBarWin : method toolBarWin : GWindow.window method toplevel : GWindow.window method vbox1 : GPack.box + method vbuttonbox1 : GPack.button_box method xml : Glade.glade_xml Gtk.obj end class confirmationDialog : @@ -155,24 +155,24 @@ class confirmationDialog : ?autoconnect:bool -> unit -> object - val confirmationDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val confirmationDialog : GWindow.dialog_any val confirmationDialogCancelButton : GButton.button val confirmationDialogLabel : GMisc.label val confirmationDialogOkButton : GButton.button + val dialog_action_area1 : GPack.button_box val dialog_vbox1 : GPack.box - val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val toplevel : GWindow.dialog_any val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit - method confirmationDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method confirmationDialog : GWindow.dialog_any method confirmationDialogCancelButton : GButton.button method confirmationDialogLabel : GMisc.label method confirmationDialogOkButton : GButton.button + method dialog_action_area1 : GPack.button_box method dialog_vbox1 : GPack.box method reparent : GObj.widget -> unit - method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method toplevel : GWindow.dialog_any method xml : Glade.glade_xml Gtk.obj end class aboutWin : @@ -182,17 +182,19 @@ class aboutWin : unit -> object val aboutDismissButton : GButton.button - val aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val aboutWin : GWindow.dialog_any + val dialog_action_area2 : GPack.button_box val dialog_vbox2 : GPack.box - val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val toplevel : GWindow.dialog_any val xml : Glade.glade_xml Gtk.obj method aboutDismissButton : GButton.button - method aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method aboutWin : GWindow.dialog_any method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method dialog_action_area2 : GPack.button_box method dialog_vbox2 : GPack.box method reparent : GObj.widget -> unit - method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method toplevel : GWindow.dialog_any method xml : Glade.glade_xml Gtk.obj end class uriChoiceDialog : @@ -203,6 +205,7 @@ class uriChoiceDialog : object val alignment1 : GBin.alignment val alignment2 : GBin.alignment + val dialog_action_area3 : GPack.button_box val dialog_vbox3 : GPack.box val entry1 : GEdit.entry val hbox1 : GPack.box @@ -214,12 +217,11 @@ class uriChoiceDialog : val label2 : GMisc.label val label3 : GMisc.label val scrolledwindow1 : GBin.scrolled_window - val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val toplevel : GWindow.dialog_any val uriChoiceAbortButton : GButton.button val uriChoiceAutoButton : GButton.button val uriChoiceConstantsButton : GButton.button - val uriChoiceDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val uriChoiceDialog : GWindow.dialog_any val uriChoiceLabel : GMisc.label val uriChoiceSelectedButton : GButton.button val uriChoiceTreeView : GTree.view @@ -229,6 +231,7 @@ class uriChoiceDialog : method alignment2 : GBin.alignment method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method dialog_action_area3 : GPack.button_box method dialog_vbox3 : GPack.box method entry1 : GEdit.entry method hbox1 : GPack.box @@ -241,12 +244,11 @@ class uriChoiceDialog : method label3 : GMisc.label method reparent : GObj.widget -> unit method scrolledwindow1 : GBin.scrolled_window - method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method toplevel : GWindow.dialog_any method uriChoiceAbortButton : GButton.button method uriChoiceAutoButton : GButton.button method uriChoiceConstantsButton : GButton.button - method uriChoiceDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method uriChoiceDialog : GWindow.dialog_any method uriChoiceLabel : GMisc.label method uriChoiceSelectedButton : GButton.button method uriChoiceTreeView : GTree.view @@ -259,27 +261,27 @@ class interpChoiceDialog : ?autoconnect:bool -> unit -> object + val dialog_action_area4 : GPack.button_box val dialog_vbox4 : GPack.box val interpChoiceCancelButton : GButton.button - val interpChoiceDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val interpChoiceDialog : GWindow.dialog_any val interpChoiceHelpButton : GButton.button val interpChoiceOkButton : GButton.button val label6 : GMisc.label - val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val toplevel : GWindow.dialog_any val vbox3 : GPack.box val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method dialog_action_area4 : GPack.button_box method dialog_vbox4 : GPack.box method interpChoiceCancelButton : GButton.button - method interpChoiceDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method interpChoiceDialog : GWindow.dialog_any method interpChoiceHelpButton : GButton.button method interpChoiceOkButton : GButton.button method label6 : GMisc.label method reparent : GObj.widget -> unit - method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method toplevel : GWindow.dialog_any method vbox3 : GPack.box method xml : Glade.glade_xml Gtk.obj end @@ -289,23 +291,24 @@ class emptyDialog : ?autoconnect:bool -> unit -> object - val emptyDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val dialog_action_area5 : GPack.button_box + val emptyDialog : GWindow.dialog_any val emptyDialogCancelButton : GButton.button val emptyDialogLabel : GMisc.label val emptyDialogOkButton : GButton.button val emptyDialogVBox : GPack.box - val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val toplevel : GWindow.dialog_any val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit - method emptyDialog : - [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method dialog_action_area5 : GPack.button_box + method emptyDialog : GWindow.dialog_any method emptyDialogCancelButton : GButton.button method emptyDialogLabel : GMisc.label method emptyDialogOkButton : GButton.button method emptyDialogVBox : GPack.box method reparent : GObj.widget -> unit - method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method toplevel : GWindow.dialog_any method xml : Glade.glade_xml Gtk.obj end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index f5dd123f5..6eb43600c 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -23,11 +23,20 @@ * http://helm.cs.unibo.it/ *) +(** Interpreter for textual phrases coming from matita's console (textual entry +* window at the bottom of the main window). +* +* Interpreter is either in `Command state or in `Proof state (see state_tag type +* below). In `Command state commands for starting proofs are accepted, but +* tactic and tactical applications are not. In `Proof state both +* tactic/tacticals and commands are accepted. +*) + open Printf type state_tag = [ `Command | `Proof ] -exception Command_not_found of string +exception Command_error of string class virtual interpreterState ~(console: MatitaConsole.console) = object (self) @@ -41,33 +50,41 @@ class virtual interpreterState ~(console: MatitaConsole.console) = method evalPhrase s = self#evalTactical (self#parsePhrase s) end + (** Implements phrases that should be accepted in all states *) +class sharedState + ~(disambiguator: MatitaTypes.disambiguator) + ~(proof_handler: MatitaTypes.proof_handler) + ~(console: MatitaConsole.console) + () += + object (self) + inherit interpreterState ~console + method evalTactical = function + | TacticAst.Command TacticAst.Quit -> + proof_handler.MatitaTypes.quit (); + `Command (* dummy answer, useless *) + | TacticAst.Command TacticAst.Proof -> + (* do nothing, just for compatibility with coq syntax *) + `Command + | tactical -> + raise (Command_error (TacticAstPp.pp_tactical tactical)) + end + + (** Implements phrases that should be accepted only in `Command state *) class commandState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) () = + let shared = new sharedState ~disambiguator ~proof_handler ~console () in object (self) inherit interpreterState ~console method evalTactical = function -(* - | TacticAst.Command _ -> failwith "1" - | TacticAst.Tactic _ -> failwith "2" - | TacticAst.LocatedTactical _ -> failwith "3" - | TacticAst.Fail -> failwith "4" - | TacticAst.Do (_, _) -> failwith "5" - | TacticAst.IdTac -> failwith "6" - | TacticAst.Repeat _ -> failwith "7" - | TacticAst.Seq _ -> failwith "8" - | TacticAst.Then (_, _) -> failwith "9" - | TacticAst.Tries _ -> failwith "10" - | TacticAst.Try _ -> failwith "11" -*) | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) -> let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in let proof = MatitaProof.proof ~typ:expr ~metasenv () in proof_handler.MatitaTypes.new_proof proof; `Proof @@ -77,28 +94,87 @@ class commandState | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) `Command - | tactical -> - raise (Command_not_found (TacticAstPp.pp_tactical tactical)) + | tactical -> shared#evalTactical tactical end +let rec lookup_tactic = function + | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic + | TacticAst.Intros (_, names) -> + let namer = + (** use names given by the user as long as they are availble, then + * fallback on default fresh name generator *) + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = Cic.Name (List.nth names !count) in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name metasenv context name ~typ + in + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:namer () + | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac + | TacticAst.Assumption -> VariousTactics.assumption_tac + | TacticAst.Contradiction -> NegationTactics.contradiction_tac + | TacticAst.Exists -> IntroductionTactics.exists_tac + | TacticAst.Fourier -> FourierR.fourier_tac + | TacticAst.Left -> IntroductionTactics.left_tac + | TacticAst.Right -> IntroductionTactics.right_tac + | TacticAst.Ring -> Ring.ring_tac + | TacticAst.Split -> IntroductionTactics.split_tac + | TacticAst.Symmetry -> EqualityTactics.symmetry_tac +(* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | TacticAst.Absurd + | TacticAst.Apply of 'term + | TacticAst.Change of 'term * 'term * 'ident option + | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option + | TacticAst.Cut of 'term + | TacticAst.Decompose of 'ident * 'ident list + | TacticAst.Discriminate of 'ident + | TacticAst.Elim of 'term * 'term option + | TacticAst.ElimType of 'term + | TacticAst.Exact of 'term + | TacticAst.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.Intros of int option * 'ident list + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace of 'term * 'term + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option + | TacticAst.Transitivity of 'term +*) + | _ -> + MatitaTypes.not_implemented "some tactic" + + (** Implements phrases that should be accepted only in `Proof state, basically + * tacticals *) class proofState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) () = - let commandState = - new commandState ~disambiguator ~proof_handler ~console () - in - object + let shared = new sharedState ~disambiguator ~proof_handler ~console () in + object (self) inherit interpreterState ~console method evalTactical = function + | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> proof_handler.MatitaTypes.set_proof None; `Command - | tactical -> (* fallback on command state *) - commandState#evalTactical tactical + | TacticAst.Seq tacticals -> + (* TODO Zack check for proof completed at each step? *) + List.iter (fun t -> ignore (self#evalTactical t)) tacticals; + `Proof + | TacticAst.Tactic tactic_phrase -> + let tactic = lookup_tactic tactic_phrase in + (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic; + `Proof + | tactical -> shared#evalTactical tactical end class interpreter diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index a19c1c921..1e4b7f7a9 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception Command_not_found of string +exception Command_error of string class interpreter: disambiguator:MatitaTypes.disambiguator -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml new file mode 100644 index 000000000..c323dbbf0 --- /dev/null +++ b/helm/matita/matitaMathView.ml @@ -0,0 +1,163 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* 29/01/2003 Claudio Sacerdoti Coen *) +(* *) +(* *) +(***************************************************************************) + +open MatitaTypes + +(* List utility functions *) +exception Skip;; + +let list_map_fail f = + let rec aux = + function + [] -> [] + | he::tl -> + try + let he' = f he in + he'::(aux tl) + with Skip -> + (aux tl) + in + aux +;; +(* End of the list utility functions *) + +class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj = + object(self) + + inherit GMathViewAux.multi_selection_math_view obj + + val mutable current_infos = None + + method get_selected_terms = + let selections = self#get_selections in + list_map_fail + (function node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + Some (ids_to_terms,_,_) -> + let id = xpath in + (try + Hashtbl.find ids_to_terms id + with _ -> raise Skip) + | None -> assert false (* "ERROR: No current term!!!" *) + ) selections + + method get_selected_hypotheses = + let selections = self#get_selections in + list_map_fail + (function node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + Some (_,_,ids_to_hypotheses) -> + let id = xpath in + (try + Hashtbl.find ids_to_hypotheses id + with _ -> raise Skip) + | None -> assert false (* "ERROR: No current term!!!" *) + ) selections + + method load_sequent metasenv sequent = + let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = + mml_of_cic_sequent metasenv sequent + in + self#load_root ~root:sequent_mml#get_documentElement ; + current_infos <- + Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + end +;; + +class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj = + object(self) + + inherit GMathViewAux.single_selection_math_view obj + + val mutable current_infos = None + val mutable current_mml = None + + method load_proof uri currentproof = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = Cic2acic.acic_object_of_cic_object currentproof + in + let mml = + mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in + current_infos <- + Some + (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses); + (match current_mml with + None -> + self#load_root ~root:mml#get_documentElement ; + current_mml <- Some mml + | Some current_mml' -> + self#freeze ; + XmlDiff.update_dom ~from:current_mml' mml ; + self#thaw); + (acic, ids_to_inner_types, ids_to_inner_sorts) + end + + (** constructors *) + +let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent) = + GtkBase.Widget.size_params + ~cont:(OgtkMathViewProps.pack_return (fun p -> + OgtkMathViewProps.set_params + (new sequent_viewer ~mml_of_cic_sequent + (GtkMathViewProps.MathView_GMetaDOM.create p)) + ?font_size:None ?log_verbosity:None)) + ?width:None ?height:None [] + +let proof_viewer ~(mml_of_cic_object: mml_of_cic_object) = + GtkBase.Widget.size_params + ~cont:(OgtkMathViewProps.pack_return (fun p -> + OgtkMathViewProps.set_params + (new proof_viewer ~mml_of_cic_object + (GtkMathViewProps.MathView_GMetaDOM.create p)) + ?font_size:None ?log_verbosity:None)) + ?width:None ?height:None [] + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli new file mode 100644 index 000000000..51a1743f6 --- /dev/null +++ b/helm/matita/matitaMathView.mli @@ -0,0 +1,37 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val sequent_viewer : + mml_of_cic_sequent:MatitaTypes.mml_of_cic_sequent -> + ?packing:(GObj.widget -> unit) -> ?show:bool -> + unit -> + MatitaTypes.sequent_viewer + +val proof_viewer : + mml_of_cic_object:MatitaTypes.mml_of_cic_object -> + ?packing:(GObj.widget -> unit) -> ?show:bool -> + unit -> + MatitaTypes.proof_viewer + diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 6c73b4b14..98b9cf02c 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -23,33 +23,30 @@ * http://helm.cs.unibo.it/ *) -class proofStatus ~typ ~metasenv ~uri () = +class proof ?uri ~typ ~metasenv ~body () = object (self) - inherit MatitaTypes.subject - val mutable _proof = (uri, (1, [], typ) :: metasenv, Cic.Meta (1, []), typ) - val mutable _goal = Some 1 - - method proof = _proof - method setProof p = _proof <- p - method goal = _goal - method setGoal g = _goal <- g - method status = - _proof, - (match _goal with Some g -> g | None -> raise MatitaTypes.No_proof) - method setStatus (p, g) = - _proof <- p; - _goal <- Some g + inherit [unit] StatefulProofEngine.status ?uri ~typ ~body ~metasenv + (fun _ -> ()) + (fun _ _ -> ()) + () + + method private currentProof = + let (uri, metasenv, bo, ty) = self#proof in + let uri = + match uri with + | Some uri -> uri + | None -> MatitaTypes.untitled_con_uri + in + (* TODO CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) method toXml = - let (uri, metasenv, bo, ty) = _proof in - let currentproof = - (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv, bo, ty, []) - in + let currentproof = self#currentProof in let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof in + let uri = MatitaTypes.unopt_uri self#uri in let xml, bodyxml = match Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true acurrentproof @@ -62,71 +59,25 @@ class proofStatus ~typ ~metasenv ~uri () = method toString = let (xml, bodyxml) = self#toXml in let buf = Buffer.create 10240 in - Buffer.add_string buf "\n"; - Buffer.add_string buf "\n"; - Buffer.add_string buf "\n"; - Buffer.add_string buf (Misc.strip_xml_headings (Xml.pp_to_string xml)); - Buffer.add_string buf (Misc.strip_xml_headings(Xml.pp_to_string bodyxml)); - Buffer.add_string buf - (match _goal with - | None -> "" - | Some goal -> Printf.sprintf "%d" goal); - Buffer.add_string buf "\n"; + List.iter (Buffer.add_string buf) + [ "\n"; + "\n"; + "\n"; + (Misc.strip_xml_headings (Xml.pp_to_string xml)); + (Misc.strip_xml_headings(Xml.pp_to_string bodyxml)); + (if not (self#proof_completed) then + Printf.sprintf "%d" self#goal + else + ""); + "\n" + ]; Buffer.contents buf end -let proofStatus ~typ ?(metasenv = []) ?(uri = MatitaTypes.untitled_con_uri) () = - new proofStatus ~typ ~metasenv ~uri () - -let proofStatus_of_string s = - MatitaTypes.not_implemented "MatitaProof.proofStatus_of_string" - -class proof ~typ ?metasenv ?uri () = - object - val mutable _status = proofStatus ~typ ?metasenv ?uri () - method status = _status - method setStatus s = _status <- s - end - -let proof = new proof - -class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) = - object - val statusBackup = status#status - - method execute () = - let (new_proof, new_goals) = tactic status#status in - status#setProof new_proof; - status#setGoal - (match new_goals, new_proof with - | goal :: _, _ -> Some goal - | [], (_, (goal, _, _) :: _, _, _) -> - (* the tactic left no open goal: let's choose the first open goal *) - (* TODO CSC: here we could implement and use a proof-tree like - * notion... *) - Some goal - | _, _ -> None); - status#notify () - - method undo () = - status#setStatus statusBackup; - status#notify () - end - -let intros ?namer = - new tacticCommand - ~tactic:(PrimitiveTactics.intros_tac ?mk_fresh_name_callback:namer ()) - -let reflexivity = new tacticCommand ~tactic:EqualityTactics.reflexivity_tac -let symmetry = new tacticCommand ~tactic:EqualityTactics.symmetry_tac -let transitivity term = - new tacticCommand ~tactic:(EqualityTactics.transitivity_tac ~term) - -let exists = new tacticCommand ~tactic:IntroductionTactics.exists_tac -let split = new tacticCommand ~tactic:IntroductionTactics.split_tac -let left = new tacticCommand ~tactic:IntroductionTactics.left_tac -let right = new tacticCommand ~tactic:IntroductionTactics.right_tac - -let assumption = new tacticCommand ~tactic:VariousTactics.assumption_tac +let proof ?uri ~metasenv ~typ () = + let metasenv = (1, [], typ) :: metasenv in + let body = Cic.Meta (1,[]) in + let _ = CicTypeChecker.type_of_aux' metasenv [] typ in + new proof ~typ ~metasenv ~body ?uri () diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli index 97551eb8c..9293e330a 100644 --- a/helm/matita/matitaProof.mli +++ b/helm/matita/matitaProof.mli @@ -23,33 +23,15 @@ * http://helm.cs.unibo.it/ *) -val proofStatus: - typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit -> - MatitaTypes.proofStatus - - (** inverse function of proofStatus#toString / proofStatus#toOutchan *) -val proofStatus_of_string: string -> MatitaTypes.proofStatus - + (** create a new proof object. Typecheck the resulting sequent. + * @param typ goal type + * @param metasenv metasenv returned by the disambiguator, this will not be + * the final metasenv of the first sequence, meta corresponding to typ will + * be added + * @param uri new proof uri *) val proof: - typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit -> + ?uri:UriManager.uri -> + metasenv:Cic.metasenv -> typ:Cic.term -> + unit -> MatitaTypes.proof -(** {2 tactic commands builders} *) - -(* TODO Zack: these are just some examples, a lot of other tactics/tacticals - * must be added here *) - -val intros: ?namer:MatitaTypes.namer -> - MatitaTypes.proofStatus -> MatitaTypes.command - -val reflexivity: MatitaTypes.proofStatus -> MatitaTypes.command -val symmetry: MatitaTypes.proofStatus -> MatitaTypes.command -val transitivity: Cic.term -> MatitaTypes.proofStatus -> MatitaTypes.command - -val exists: MatitaTypes.proofStatus -> MatitaTypes.command -val split: MatitaTypes.proofStatus -> MatitaTypes.command -val left: MatitaTypes.proofStatus -> MatitaTypes.command -val right: MatitaTypes.proofStatus -> MatitaTypes.command - -val assumption: MatitaTypes.proofStatus -> MatitaTypes.command - diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 864e9604c..2811fd5d4 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -38,28 +38,10 @@ exception No_proof (** no current proof is available *) let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" -class type observer = - (* "observer" pattern *) - object - method update: unit -> unit - end - -class subject = - (* "observer" pattern *) - object - val mutable observers = [] - method attach (o: observer) = observers <- o :: observers - method detach (o: observer) = - observers <- List.filter (fun o' -> o' != o) observers - method notify () = List.iter (fun o -> o#update ()) observers - end - -class type command = - (* "command" pattern *) - object - method execute: unit -> unit - method undo: unit -> unit - end +let unopt_uri ?(kind = `Con) = function + | Some uri -> uri + | None -> + (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri) class type parserr = (* "parser" is a keyword :-( *) object @@ -95,23 +77,9 @@ class type disambiguator = (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end -class type proofStatus = +class type proof = object - inherit subject - - (** {3 properties} *) - - method proof: ProofEngineTypes.proof - method setProof: ProofEngineTypes.proof -> unit - - method goal: ProofEngineTypes.goal option - method setGoal: ProofEngineTypes.goal option -> unit - - (** @raise MatitaTypes.No_proof *) - method status: ProofEngineTypes.status (* proof, goal *) - method setStatus: ProofEngineTypes.status -> unit - - (** {3 actions} *) + inherit [unit] StatefulProofEngine.status (** return a pair of "xml" (as defined in Xml module) representing the * * current proof type and body, respectively *) @@ -119,13 +87,6 @@ class type proofStatus = method toString: string end -class type proof = - object - (** {3 status} *) - method status: proofStatus - method setStatus: proofStatus -> unit - end - type proof_handler = { get_proof: unit -> proof; (* return current proof or fail *) set_proof: proof option -> unit; (* set a proof option as current proof *) @@ -141,6 +102,49 @@ class type interpreter = method evalPhrase: string -> unit end +(** {2 MathML widgets} *) + +type mml_of_cic_sequent = + Cic.metasenv -> int * Cic.context * Cic.term -> + Gdome.document * + ((Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t) + +type mml_of_cic_object = + explode_all:bool -> UriManager.uri -> Cic.annobj -> + (string, string) Hashtbl.t -> + (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document + +class type sequent_viewer = + object + inherit GMathViewAux.multi_selection_math_view + + (** @return the list of selected terms. Selections which are not terms are + * ignored *) + method get_selected_terms: Cic.term list + + (** @return the list of selected hypothese. Selections which are not + * hypotheses are ignored *) + method get_selected_hypotheses: Cic.hypothesis list + + (** load a sequent and render it into parent widget *) + method load_sequent: Cic.metasenv -> Cic.conjecture -> unit + end + +class type proof_viewer = + object + inherit GMathViewAux.single_selection_math_view + + (** @return the annotated cic term and the ids_to_inner_types and + * ids_to_inner_sorts maps *) + method load_proof : + UriManager.uri -> Cic.obj -> + Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t * + (Cic.id, string) Hashtbl.t + + end + (** {2 shorthands} *) type namer = ProofEngineTypes.mk_fresh_name_type -- 2.39.2