From 56415e42c04f40e9c8f7cfc59a3a3d87c3d373f7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 29 Apr 2004 13:59:11 +0000 Subject: [PATCH] snapshot --- helm/matita/.depend | 7 ++- helm/matita/Makefile.in | 3 +- helm/matita/configure.ac | 1 + helm/matita/matita.ml | 14 ++++- helm/matita/matitaConsole.ml | 74 ++++++++++++++++++++---- helm/matita/matitaConsole.mli | 24 ++++++-- helm/matita/matitaDisambiguator.ml | 13 +++-- helm/matita/matitaDisambiguator.mli | 9 +-- helm/matita/matitaGui.ml | 19 +++--- helm/matita/matitaGui.mli | 9 ++- helm/matita/matitaInterpreter.ml | 89 +++++++++++++++++++++++++++++ helm/matita/matitaInterpreter.mli | 33 +++++++++++ helm/matita/matitaTypes.ml | 15 ++++- 13 files changed, 265 insertions(+), 45 deletions(-) create mode 100644 helm/matita/matitaInterpreter.ml create mode 100644 helm/matita/matitaInterpreter.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 433e976fd..4576d80ba 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -10,10 +10,12 @@ matitaGui.cmo: matitaConsole.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi \ matitaGui.cmi matitaGui.cmx: matitaConsole.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmx \ matitaGui.cmi +matitaInterpreter.cmo: matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi +matitaInterpreter.cmx: matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ - matitaGui.cmi matitaProof.cmi matitaTypes.cmo + matitaGui.cmi matitaInterpreter.cmi matitaProof.cmi matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ - matitaGui.cmx matitaProof.cmx matitaTypes.cmx + matitaGui.cmx matitaInterpreter.cmx matitaProof.cmx matitaTypes.cmx matitaProof.cmo: matitaTypes.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo @@ -21,4 +23,5 @@ matitaTypes.cmx: buildTimeConf.cmx matitaDisambiguator.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo matitaGui.cmi: matitaGeneratedGui.cmi +matitaInterpreter.cmi: matitaTypes.cmo matitaProof.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 9b28fd8c9..144ba5677 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -19,7 +19,8 @@ CMOS = \ matitaConsole.cmo \ matitaGui.cmo \ matitaProof.cmo \ - matitaDisambiguator.cmo + matitaDisambiguator.cmo \ + matitaInterpreter.cmo CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) all: matita diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 82ac6a721..bfaea8406 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -29,6 +29,7 @@ fi FINDLIB_REQUIRES="\ lablgtk2.glade \ +pcre \ helm-cic_omdoc \ helm-cic_transformations \ helm-registry \ diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index b71463860..dd813debe 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -53,12 +53,22 @@ let disambiguator = ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () +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 (); + set_proof proof +let interpreter = + new MatitaInterpreter.interpreter + ~disambiguator ~console:gui#console ~get_proof ~new_proof () (** quit program, possibly asking for confirmation *) let quit () = GMain.Main.quit () let _ = gui#setQuitCallback quit; + gui#setPhraseCallback interpreter#evalPhrase; gui#main#debugMenu#misc#hide (); ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> if has_proof () && @@ -74,9 +84,7 @@ let _ = disambiguator#disambiguateTerm (Stream.of_string input) in let proof = MatitaProof.proof ~typ:term ~metasenv () in -(* proof#status#attach ... FINQUI *) - proof#status#notify (); - set_proof proof; + new_proof proof; debug_print ("new proof, goal is: " ^ CicPp.ppterm term))) (** *) diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index c1866f3f3..a2c0515bd 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -23,30 +23,82 @@ * http://helm.cs.unibo.it/ *) -let default_prompt = "## " +let default_prompt = "# " +let default_phrase_sep = "." +let default_callback = fun (phrase: string) -> () + +let history_size = 100 let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] +let prompt_props = [ ] -class console ?(prompt = default_prompt) obj = -(* let read_only = console#buffer#create_tag [ `EDITABLE false ] in *) +class console + ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) + ?(callback = default_callback) + obj += + let ui_mark = `NAME "USER_INPUT_START" in object (self) inherit GText.view obj - method read_phrase () = prompt ^ "foo" - method echo_prompt () = + val mutable _phrase_sep = phrase_sep + method phrase_sep = _phrase_sep + method set_phrase_sep sep = _phrase_sep <- sep + + val mutable _callback = callback + method set_callback f = _callback <- f + +(* + (* TODO Zack: implement history. + IDEA: use CTRL-P/N a la emacs. + ISSUE: per-phrase or per-line history? *) + val phrases_history = Array.create history_size None + val mutable history_last_index = -1 + val mutable history_cur_index = -1 +*) + + initializer let buf = self#buffer in - buf#insert ~iter:buf#end_iter ~tags:[] prompt; - self#lock + (* create "USER_INPUT_START" mark. This mark will always point to the + * beginning of user input not yet processed *) + ignore (buf#create_mark ~name:"USER_INPUT_START" + ~left_gravity:true buf#start_iter); + ignore (self#event#connect#key_press (fun key -> (* handle return ev. *) + if GdkEvent.Key.keyval key = GdkKeysyms._Return then begin + let insert_point = buf#get_iter_at_mark `INSERT in + if insert_point#compare buf#end_iter = 0 then (* insert pt. at end *) + let inserted_text = + buf#get_text ~start:(buf#get_iter_at_mark ui_mark) + ~stop:buf#end_iter () + in + let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in + if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *) + self#lock; + _callback inserted_text + end + end; + false (* continue event processing *))) + + (* lock old text and bump USER_INPUT_START mark *) method private lock = let buf = self#buffer in let read_only = buf#create_tag [`EDITABLE false] in - buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter + let stop = buf#end_iter in + buf#apply_tag read_only ~start:buf#start_iter ~stop; + buf#move_mark ui_mark stop + + method echo_prompt () = + let buf = self#buffer in + buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt; + self#lock + method echo_message msg = let buf = self#buffer in buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] (msg ^ "\n"); self#lock + method echo_error msg = let buf = self#buffer in buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] @@ -54,7 +106,9 @@ class console ?(prompt = default_prompt) obj = self#lock end -let console ?(prompt = default_prompt) +let console + ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) + ?(callback = default_callback) ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -63,5 +117,5 @@ let console ?(prompt = default_prompt) ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in - new console ~prompt view#as_view + new console ~prompt ~phrase_sep ~callback view#as_view diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index 1bc5f7b95..ee7b8d4fb 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -23,19 +23,33 @@ * http://helm.cs.unibo.it/ *) -class console: ?prompt:string -> Gtk.text_view Gtk.obj -> +class console: + ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> + Gtk.text_view Gtk.obj -> object inherit GText.view - method read_phrase : unit -> string + method echo_prompt : unit -> unit + method echo_message : string -> unit + method echo_error : string -> unit - method echo_prompt : unit -> unit - method echo_message : string -> unit - method echo_error : string -> unit + method phrase_sep : string + method set_phrase_sep : string -> unit + + (** override previous callback definition *) + method set_callback : (string -> unit) -> unit end + (** @param prompt user prompt (default "# ") + * @param phrase_sep phrase separator (default ".") + * @param callback callback invoked upon reading of a phrase. Callback + * may be invoked more than once if multiple phrases have been inserted before + * hitting return (default: do nothing) *) val console : ?prompt:string -> + ?phrase_sep:string -> + ?callback:(string -> unit) -> + ?buffer:GText.buffer -> ?editable:bool -> ?cursor_visible:bool -> diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 51e60bb18..87215fba1 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -74,11 +74,16 @@ class disambiguator method env = _env method setEnv e = _env <- e - method disambiguateTermAst ?(context = []) ?(metasenv = []) ?(env = _env) - termAst - = + method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst = + let (save_state, env) = + match env with + | Some env -> (false, env) + | None -> (true, _env) + in match disambiguate_term mqiconn context metasenv termAst ~aliases:env with - | [ x ] -> x + | [ (env, metasenv, term) as x ] -> + if save_state then self#setEnv env; + x | _ -> assert false method disambiguateTerm ?context ?metasenv ?env stream = diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index ce89b6e08..8397e4dbf 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -23,10 +23,7 @@ * http://helm.cs.unibo.it/ *) -class parserr: unit -> - object - inherit MatitaTypes.parserr - end +class parserr: unit -> MatitaTypes.parserr class disambiguator: parserr:MatitaTypes.parserr -> (** parser *) @@ -34,7 +31,5 @@ class disambiguator: chooseUris:MatitaTypes.choose_uris_callback -> chooseInterp:MatitaTypes.choose_interp_callback -> unit -> - object - inherit MatitaTypes.disambiguator - end + MatitaTypes.disambiguator diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6ad3e81e0..95882a0f1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -55,11 +55,6 @@ class gui file = [ toolbar#toolBarEventBox; proof#proofWinEventBox ] in let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in - let _ = - console#echo_message "message"; - console#echo_error "error"; - console#echo_prompt () - in object (self) initializer (* glade's check widgets *) @@ -84,14 +79,18 @@ class gui file = List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; main#helpMenu#set_right_justified true; - (* uri choice *) - () + (* console *) + console#echo_message "message"; + console#echo_error "error"; + console#echo_prompt (); + console#misc#grab_focus () - method toolbar = toolbar - method main = main method about = about + method console = console method fileSel = fileSel + method main = main method proof = proof + method toolbar = toolbar method newUriDialog () = let dialog = new uriChoiceDialog ~file () in @@ -122,5 +121,7 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback + method setPhraseCallback = console#set_callback + end diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 848f52bf6..60ab37a65 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -36,9 +36,10 @@ class gui : string -> object - method setQuitCallback : (unit -> unit) -> unit + method setQuitCallback : (unit -> unit) -> unit + method setPhraseCallback : (string -> unit) -> unit - (** {2 Access to low-level GTK widgets} *) + (** {2 Access to lower-level GTK widgets} *) method about : MatitaGeneratedGui.aboutWin method fileSel : MatitaGeneratedGui.fileSelectionWin @@ -46,6 +47,10 @@ class gui : method proof : MatitaGeneratedGui.proofWin method toolbar : MatitaGeneratedGui.toolBarWin + (** {2 Access to GUI useful components} *) + + method console: MatitaConsole.console + (** {2 Dialogs instantiation} * methods below create a new window on each invocation. You should * remember to destroy windows after use *) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml new file mode 100644 index 000000000..8ec043a1b --- /dev/null +++ b/helm/matita/matitaInterpreter.ml @@ -0,0 +1,89 @@ +(* 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/ + *) + +type state_tag = [ `Command | `Proof ] + +class type interpreterState = + object + (** eval a toplevel phrase in the current state and return the new state + *) + method evalPhrase: string -> state_tag + end + +class commandState + ~(disambiguator: MatitaTypes.disambiguator) + ~(console: MatitaConsole.console) + ~new_proof () += + object + method evalPhrase s: state_tag = + let command = CicTextualParser2.parse_command (Stream.of_string s) in + match command with + | CommandAst.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 + new_proof proof; + `Proof + | _ -> + MatitaTypes.not_implemented (* TODO Zack *) + "MatitaInterpreter.commandState#evalPhrase: commands other than full theorem ones"; + `Proof + end + +class proofState + ~(disambiguator: MatitaTypes.disambiguator) + ~(console: MatitaConsole.console) + ~get_proof () += + object + method evalPhrase (s: string): state_tag = + (* TODO Zack *) + MatitaTypes.not_implemented "MatitaInterpreter.proofState#evalPhrase"; + `Command + end + +class interpreter + ~(disambiguator: MatitaTypes.disambiguator) + ~(console: MatitaConsole.console) + ~(get_proof: unit -> MatitaTypes.proof) + ~(new_proof: MatitaTypes.proof -> unit) + () += + let commandState = + lazy (new commandState ~disambiguator ~console ~new_proof ()) + in + let proofState = + lazy (new proofState ~disambiguator ~console ~get_proof ()) + in + object + val mutable state = Lazy.force commandState + + method evalPhrase s = + match state#evalPhrase s with + | `Command -> state <- Lazy.force commandState + | `Proof -> state <- Lazy.force proofState + end + diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli new file mode 100644 index 000000000..fc529c3c0 --- /dev/null +++ b/helm/matita/matitaInterpreter.mli @@ -0,0 +1,33 @@ +(* 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/ + *) + +class interpreter: + disambiguator:MatitaTypes.disambiguator -> + console:MatitaConsole.console -> + get_proof:(unit -> MatitaTypes.proof) -> + new_proof:(MatitaTypes.proof -> unit) -> + unit -> + MatitaTypes.interpreter + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 4e81148c3..27783ec67 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -36,7 +36,7 @@ let debug_print s = 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.def" +let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" class type observer = (* "observer" pattern *) @@ -80,12 +80,17 @@ class type disambiguator = (* TODO Zack: as long as matita doesn't support MDI inteface, * disambiguateTerm will return a single term *) - (** @param env defaults to self#env *) + (** @param env disambiguation environment. If this parameter is given the + * disambiguator act statelessly, that is internal disambiguation status + * want be changed but only returned. If this parameter is not given the + * internal one will be used and updated with the disambiguation status + * resulting from the disambiguation *) method disambiguateTerm: ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> char Stream.t -> (DisambiguateTypes.environment * Cic.metasenv * Cic.term) + (** @param env @see disambiguateTerm above *) method disambiguateTermAst: ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> @@ -124,6 +129,12 @@ class type proof = method setStatus: proofStatus -> unit end + (** interpreter for toplevel phrases given via console *) +class type interpreter = + object + method evalPhrase: string -> unit + end + (** {2 shorthands} *) type namer = ProofEngineTypes.mk_fresh_name_type -- 2.39.2