+logicalOperations.cmo: logicalOperations.cmi
+logicalOperations.cmx: logicalOperations.cmi
matitaConsole.cmo: matitaConsole.cmi
matitaConsole.cmx: matitaConsole.cmi
matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
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 \
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
matitaGui.cmo \
matitaProof.cmo \
matitaDisambiguator.cmo \
- matitaInterpreter.cmo
+ matitaInterpreter.cmo \
+ matitaMathView.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
all: matita
let debug = @DEBUG@;;
+module Transformer = @TRANSFORMER_MODULE@;;
+
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 \
"
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)
<key name="db_map">mathql_db_map.txt</key>
<section name="mysql_connection">
<key name="host">mowgli.cs.unibo.it</key>
+<!-- <key name="host">localhost</key> -->
<key name="database">mowgli</key>
<!-- <key name="port"></key> -->
<!-- <key name="password"></key> -->
<section name="getter">
<key name="mode">remote</key>
<key name="url">http://mowgli.cs.unibo.it:58081/</key>
+<!-- <key name="url">http://localhost:58081/</key> -->
</section>
</helm_registry>
<property name="default_height">600</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
<widget class="GtkVBox" id="MainWinShape">
<property name="default_height">525</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
<widget class="GtkEventBox" id="ProofWinEventBox">
<property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
<child>
<widget class="GtkScrolledWindow" id="ScrolledProof">
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkViewport" id="viewport1">
- <property name="visible">True</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
-
- <child>
- <placeholder/>
- </child>
- </widget>
+ <placeholder/>
</child>
</widget>
</child>
<property name="modal">True</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="show_fileops">True</property>
<child internal-child="cancel_button">
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
<property name="modal">False</property>
<property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
<widget class="GtkEventBox" id="ToolBarEventBox">
<property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
<child>
<widget class="GtkVBox" id="vbox1">
<property name="label" translatable="yes">button1</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
<property name="label" translatable="yes">button2</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
<property name="label" translatable="yes">button3</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
<property name="label" translatable="yes">button4</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
<property name="modal">True</property>
<property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
<property name="label">gtk-cancel</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-6</property>
</widget>
</child>
<property name="label">gtk-ok</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-5</property>
</widget>
</child>
<property name="modal">True</property>
<property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
<property name="label">gtk-ok</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-5</property>
</widget>
</child>
<property name="modal">True</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
<property name="label">gtk-cancel</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-6</property>
</widget>
</child>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">0</property>
<child>
<property name="yalign">0.5</property>
<property name="xscale">0</property>
<property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
<child>
<widget class="GtkHBox" id="hbox3">
<property name="label" translatable="yes">Try Constants</property>
<property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">0</property>
</widget>
</child>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">0</property>
<child>
<property name="yalign">0.5</property>
<property name="xscale">0</property>
<property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
<child>
<widget class="GtkHBox" id="hbox1">
<property name="modal">True</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
<property name="label">gtk-help</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-11</property>
</widget>
</child>
<property name="label">gtk-cancel</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-6</property>
</widget>
</child>
<property name="label">gtk-ok</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-5</property>
</widget>
</child>
<property name="modal">False</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
<property name="label">gtk-cancel</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-6</property>
</widget>
</child>
<property name="label">gtk-ok</property>
<property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<property name="response_id">-5</property>
</widget>
</child>
~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 *)
() (* 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))
(** <DEBUGGING> *)
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
(** </DEBUGGING> *)
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 ()
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))
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))
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))
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))
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))
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))
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
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 :
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
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 :
?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 :
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 :
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
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
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
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
?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
?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
* 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)
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
| 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
* http://helm.cs.unibo.it/
*)
-exception Command_not_found of string
+exception Command_error of string
class interpreter:
disambiguator:MatitaTypes.disambiguator ->
--- /dev/null
+(* 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 []
+
--- /dev/null
+(* 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
+
* 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
method toString =
let (xml, bodyxml) = self#toXml in
let buf = Buffer.create 10240 in
- Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
- Buffer.add_string buf "<!DOCTYPE ConstantType SYSTEM \"http://mowgli.cs.unibo.it:58081/getdtd?uri=cic.dtd\">\n";
- Buffer.add_string buf "<ProofStatus>\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 -> "<CurrentGoal />"
- | Some goal -> Printf.sprintf "<CurrentGoal>%d</CurrentGoal>" goal);
- Buffer.add_string buf "\n</ProofStatus>";
+ List.iter (Buffer.add_string buf)
+ [ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+ "<!DOCTYPE ConstantType SYSTEM \"http://mowgli.cs.unibo.it:58081/getdtd?uri=cic.dtd\">\n";
+ "<ProofStatus>\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 "<CurrentGoal>%d</CurrentGoal>" self#goal
+ else
+ "<CurrentGoal />");
+ "\n</ProofStatus>"
+ ];
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 ()
* 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
-
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
(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 *)
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 *)
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
projects / helm.git / commitdiff