From ac813b7e251e4bac1a8a16befa628203775771ca Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 18 Jan 2005 18:15:25 +0000 Subject: [PATCH] snapshot, notably: - first commit of matitac --- helm/matita/.cvsignore | 2 + helm/matita/.depend | 71 +++++----- helm/matita/Makefile.in | 38 +++-- helm/matita/configure.ac | 12 +- helm/matita/matita.ml | 85 ++++-------- helm/matita/matitaConsole.ml | 61 ++++---- helm/matita/matitaConsole.mli | 15 +- helm/matita/matitaGui.ml | 18 --- helm/matita/matitaGui.mli | 10 +- helm/matita/matitaInterpreter.ml | 224 +++++++++++++++--------------- helm/matita/matitaInterpreter.mli | 3 +- helm/matita/matitaMathView.ml | 24 +++- helm/matita/matitaMathView.mli | 42 +++++- helm/matita/matitaProof.ml | 40 ++++++ helm/matita/matitaProof.mli | 17 +++ helm/matita/matitaTypes.ml | 143 ++++++------------- helm/matita/matitaTypes.mli | 193 +++++++++++++++++++++++++ helm/matita/matitac.ml | 113 +++++++++++++++ 18 files changed, 724 insertions(+), 387 deletions(-) create mode 100644 helm/matita/matitaTypes.mli create mode 100644 helm/matita/matitac.ml diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore index ef69ec2b7..381f91c1a 100644 --- a/helm/matita/.cvsignore +++ b/helm/matita/.cvsignore @@ -6,6 +6,8 @@ config.log autom4te.cache matita matita.opt +matitac +matitac.opt *.cm[aiox] *.cmxa *.[ao] diff --git a/helm/matita/.depend b/helm/matita/.depend index 9c279be54..2de9cd092 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,44 +1,47 @@ -matitaCicMisc.cmo: matitaTypes.cmo +matitaCicMisc.cmo: matitaTypes.cmi matitaCicMisc.cmx: matitaTypes.cmx -matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaTypes.cmo \ - matitaConsole.cmi -matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaTypes.cmx \ - matitaConsole.cmi -matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi +matitac.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi \ + matitaDisambiguator.cmi buildTimeConf.cmo +matitac.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmx \ + matitaDisambiguator.cmx buildTimeConf.cmx +matitaConsole.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ + buildTimeConf.cmo matitaConsole.cmi +matitaConsole.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ + buildTimeConf.cmx matitaConsole.cmi +matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi -matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi -matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi -matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ - matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi -matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ - matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi -matitaInterpreter.cmo: matitaConsole.cmi matitaGui.cmi matitaMathView.cmi \ - matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi -matitaInterpreter.cmx: matitaConsole.cmx matitaGui.cmx matitaMathView.cmx \ - matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi -matitaMathView.cmo: matitaCicMisc.cmo matitaGui.cmi matitaTypes.cmo \ +matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi +matitaGui.cmo: matitaMisc.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi \ + matitaConsole.cmi buildTimeConf.cmo matitaGui.cmi +matitaGui.cmx: matitaMisc.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ + matitaConsole.cmx buildTimeConf.cmx matitaGui.cmi +matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi +matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmi +matitaMathView.cmo: matitaTypes.cmi matitaGui.cmi matitaCicMisc.cmo \ matitaMathView.cmi -matitaMathView.cmx: matitaCicMisc.cmx matitaGui.cmx matitaTypes.cmx \ +matitaMathView.cmx: matitaTypes.cmx matitaGui.cmx matitaCicMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi -matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ - matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaMisc.cmi \ - matitaTypes.cmo -matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ - matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaMisc.cmx \ - matitaTypes.cmx -matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \ +matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ + matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaDisambiguator.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \ + matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaDisambiguator.cmx buildTimeConf.cmx +matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmo buildTimeConf.cmo \ matitaProof.cmi -matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ +matitaProof.cmx: matitaTypes.cmx matitaCicMisc.cmx buildTimeConf.cmx \ matitaProof.cmi -matitaTypes.cmo: buildTimeConf.cmo -matitaTypes.cmx: buildTimeConf.cmx -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 +matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi +matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi +matitaConsole.cmi: matitaTypes.cmi +matitaDisambiguator.cmi: matitaTypes.cmi +matitaGtkMisc.cmi: matitaTypes.cmi matitaGeneratedGui.cmi +matitaGui.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaConsole.cmi +matitaInterpreter.cmi: matitaTypes.cmi +matitaMathView.cmi: matitaTypes.cmi +matitaProof.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index a9ea5d40c..3d76d0d85 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -3,15 +3,19 @@ OCAMLFIND = @OCAMLFIND@ CAMLP4O = @CAMLP4O@ LABLGLADECC = @LABLGLADECC@ REQUIRES = @FINDLIB_REQUIRES@ +CREQUIRES = @FINDLIB_CREQUIRES@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ -OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O) +OCAML_FLAGS = -pp $(CAMLP4O) +PKGS = -package "$(REQUIRES)" +CPKGS = -package "$(CREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) +# objects for matita (GTK GUI) CMOS = \ buildTimeConf.cmo \ matitaMisc.cmo \ @@ -25,38 +29,54 @@ CMOS = \ matitaDisambiguator.cmo \ matitaMathView.cmo \ matitaInterpreter.cmo +# objects for matitac (batch compiler) +CCMOS = \ + buildTimeConf.cmo \ + matitaMisc.cmo \ + matitaTypes.cmo \ + matitaCicMisc.cmo \ + matitaProof.cmo \ + matitaDisambiguator.cmo \ + matitaInterpreter.cmo LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) -all: matita +all: matita matitac ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) +CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) -opt: matita.opt +opt: matita.opt matitac.opt else opt: @echo "Native code compilation is disabled" endif matita: $(LIB_DEPS) $(CMOS) matita.ml - $(OCAMLC) -linkpkg -o $@ $(CMOS) matita.ml + $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml - $(OCAMLOPT) -linkpkg -o $@ $(CMXS) matita.ml + $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml + +matitac: $(LIB_DEPS) $(CCMOS) matitac.ml + $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml +matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) $< > matitaGeneratedGui.ml $(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli %.cmi: %.mli - $(OCAMLC) -c $< + $(OCAMLC) $(PKGS) -c $< %.cmo %.cmi: %.ml - $(OCAMLC) -c $< + $(OCAMLC) $(PKGS) -c $< %.cmx: %.ml - $(OCAMLOPT) -c $< + $(OCAMLOPT) $(PKGS) -c $< clean: - rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o matita matita.opt + rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ + matita matita.opt matitac matitac.opt distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index d31611ba0..1af1fca87 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -27,9 +27,7 @@ else AC_MSG_ERROR(could not find camlp4o) fi -FINDLIB_REQUIRES="\ -lablgtk2.glade \ -lablgtkmathview \ +FINDLIB_CREQUIRES="\ pcre \ mysql \ unix \ @@ -38,9 +36,14 @@ helm-cic_transformations \ helm-registry \ helm-tactics \ helm-xml \ -helm-xmldiff \ helm-cic_textual_parser2 \ " +FINDLIB_REQUIRES="\ +$FINDLIB_CREQUIRES \ +lablgtk2.glade \ +lablgtkmathview \ +helm-xmldiff \ +" for r in $FINDLIB_REQUIRES do AC_MSG_CHECKING(for $r ocaml library) @@ -89,6 +92,7 @@ AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) AC_SUBST(TRANSFORMER_MODULE) AC_SUBST(FINDLIB_REQUIRES) +AC_SUBST(FINDLIB_CREQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 20111286e..364b58025 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -29,25 +29,13 @@ open MatitaGtkMisc open MatitaTypes open MatitaMisc -(** {2 Internal status} *) - -let (get_proof, set_proof, has_proof) = - let (current_proof: MatitaTypes.proof option ref) = ref None in - ((fun () -> (* get_proof *) - match !current_proof with - | Some proof -> proof - | None -> failwith "No current proof"), - (fun proof -> (* set_proof *) - current_proof := proof), - (fun () -> (* has_proof *) - !current_proof <> None)) - (** {2 Initialization} *) let _ = Helm_registry.load_from "matita.conf.xml"; GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; GMain.Main.init () + let parserr = new MatitaDisambiguator.parserr () let dbd = Mysql.quick_connect @@ -62,17 +50,19 @@ let disambiguator = ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () + +let currentProof = new MatitaProof.currentProof + let proof_viewer = MatitaMathView.proof_viewer_instance () let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = let set_goal goal = - if not (has_proof ()) then assert false; - (get_proof ())#set_goal goal + if not (currentProof#onGoing ()) then assert false; + currentProof#proof#set_goal goal in MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer ~set_goal () - -let new_proof (proof: MatitaTypes.proof) = +let _ = (* attach observers to proof status *) let proof_observer _ (status, ()) = let ((uri_opt, _, _, _), _) = status in proof_viewer#load_proof status; @@ -85,49 +75,34 @@ let new_proof (proof: MatitaTypes.proof) = sequents_viewer#load_sequents metasenv; sequents_viewer#goto_sequent goal) in - ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - sequents_observer); - ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - proof_observer); - proof#notify; - set_proof (Some proof) - -let quit () = (* quit program, asking for confirmation if needed *) - if not (has_proof ()) || - (ask_confirmation ~gui - ~msg:("Proof in progress, are you sure you want to quit?") ()) - then - GMain.Main.quit () - -let abort_proof () = - if has_proof () then begin - set_proof None; - sequents_viewer#reset - end - -let proof_handler = - { MatitaTypes.get_proof = get_proof; - MatitaTypes.abort_proof = abort_proof; - MatitaTypes.set_proof = set_proof; - MatitaTypes.has_proof = has_proof; - MatitaTypes.new_proof = new_proof; - MatitaTypes.quit = quit; - } + currentProof#addObserver sequents_observer; + currentProof#addObserver proof_observer; + currentProof#connect `Quit (fun () -> + (* quit program, asking for confirmation if needed *) + if not (currentProof#onGoing ()) || + (ask_confirmation ~gui + ~msg:("Proof in progress, are you sure you want to quit?") ()) + then + GMain.Main.quit (); + false); + currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) let interpreter = let console = (gui#console :> MatitaTypes.console) in + let currentProof = (currentProof :> MatitaTypes.currentProof) in new MatitaInterpreter.interpreter - ~disambiguator ~proof_handler ~console ~dbd () + ~disambiguator ~currentProof ~console ~dbd () (** {2 Script window handling} *) let script_forward _ = let buf = gui#script#scriptTextView#buffer in let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - if + let (success, hide) = interpreter#evalPhrase - (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()); - then + (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()) + in + if success then gui#lockScript (locked_iter#offset + interpreter#endOffset) let script_jump _ = @@ -138,9 +113,10 @@ let script_jump _ = let len = String.length raw_text in let rec parse offset = if offset < len then begin - if + let (success, hide) = interpreter#evalPhrase (String.sub raw_text offset (len - offset)) - then begin + in + if success then begin let new_offset = interpreter#endOffset + offset in gui#lockScript (new_offset + locked_iter#offset); parse new_offset @@ -162,7 +138,7 @@ let load_script fname = (** {2 GUI callbacks} *) let _ = - gui#setQuitCallback quit; + gui#setQuitCallback currentProof#quit; gui#setPhraseCallback interpreter#evalPhrase; gui#main#debugMenu#misc#hide (); ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> @@ -200,9 +176,6 @@ let _ = connect_button tbar#reflexivityButton (tac A.Reflexivity); connect_button tbar#symmetryButton (tac A.Symmetry); connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole)); - -(* connect_button tbar#simplifyButton FINQUI; *) - connect_button tbar#assumptionButton (tac A.Assumption); connect_button tbar#cutButton (tac_w_term (A.Cut hole)); connect_button tbar#autoButton (tac A.Auto) @@ -222,7 +195,7 @@ let _ = Helm_registry.set_bool "matita.auto_disambiguation" (not (Helm_registry.get_bool "matita.auto_disambiguation"))); addDebugItem "dump proof status to stdout" (fun _ -> - print_endline ((get_proof ())#toString)); + print_endline (currentProof#proof#toString)); addDebugItem "dump environment to \"env.dump\"" (fun _ -> let oc = open_out "env.dump" in CicEnvironment.dump_to_channel oc; diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 4735fdd4a..2f36fc647 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -27,10 +27,12 @@ open Printf open MatitaTypes +type callback = string -> command_outcome + (* let default_prompt = "# " *) let default_prompt = "" let default_phrase_sep = "." -let default_callback = fun (phrase: string) -> true +let default_callback = fun (phrase: string) -> (true, true) let bullet = "∙" let message_props = [ `STYLE `ITALIC ] @@ -146,12 +148,8 @@ class console method private invoke_callback phrase = history#add phrase; - if _callback phrase then begin - self#hide (); - self#clear () - end - (* else callback encountered troubles, don't hide console which - probably contains error message *) + let (success, hide) = _callback phrase in + if hide then self#hide () method clear () = let buf = self#buffer in @@ -216,33 +214,28 @@ class console method private next_phrase = try self#set_phrase history#next with History_failure -> () - method wrap_exn (f: unit -> unit) = - try - f (); - true - with - | StatefulProofEngine.Tactic_failure exn -> - self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn)); - false - | CicTextualParser2.Parse_error (floc, msg) -> - let buf = self#buffer in - let (x, y) = CicAst.loc_of_floc floc in - let red = buf#create_tag [`FOREGROUND "red"] in - let (start_error_pos, end_error_pos) = - buf#end_iter#backward_chars (String.length last_phrase - x), - buf#end_iter#backward_chars (String.length last_phrase - y) - in - if x - y = 0 then (* no region to highlight, let's add an hint about - where the error occured *) - buf#insert ~iter:end_error_pos ~tags:[red] bullet - else (* highlight the region where the error occured *) - buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos; - self#echo_error (sprintf "at character %d-%d: %s" x y msg); - false - | exn -> - self#echo_error (sprintf "Uncaught exception: %s" - (Printexc.to_string exn)); - false + method wrap_exn: 'a. (unit -> 'a) -> 'a option = + fun f -> + try + Some (f ()) + with exn -> + (match exn with (* highlight parse errors in user input *) + | CicTextualParser2.Parse_error (floc, msg) -> + let buf = self#buffer in + let (x, y) = CicAst.loc_of_floc floc in + let red = buf#create_tag [`FOREGROUND "red"] in + let (start_error_pos, end_error_pos) = + buf#end_iter#backward_chars (String.length last_phrase - x), + buf#end_iter#backward_chars (String.length last_phrase - y) + in + if x - y = 0 then (* no region to highlight, let's add an hint + about where the error occured *) + buf#insert ~iter:end_error_pos ~tags:[red] bullet + else (* highlight the region where the error occured *) + buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos; + | _ -> ()); + self#echo_error (explain exn); + None end diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index a8e272e22..d0d1a53d3 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -23,10 +23,12 @@ * http://helm.cs.unibo.it/ *) +type callback = string -> MatitaTypes.command_outcome + (** @param evbox event box to which keyboard shortcuts are registered; no * shortcut will be registered if evbox is not given *) class console: - ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> bool) -> + ?prompt:string -> ?phrase_sep:string -> ?callback:callback -> ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj -> object inherit GText.view @@ -51,14 +53,15 @@ class console: method set_phrase_sep : string -> unit (** override previous callback definition *) - method set_callback : (string -> bool) -> unit + method set_callback : callback -> unit method ignore_insert_text_signal: bool -> unit - (** execute a unit -> unit function, if it raises exceptions shows them as + (** execute a unit -> 'a function, if it raises exceptions shows them as * errors in the console. - * @return true if no exception has been raised, false otherwise *) - method wrap_exn : (unit -> unit) -> bool + * @return Some of the returned value if the given function suceeds, None + * otherwise *) + method wrap_exn : 'a. (unit -> 'a) -> 'a option end (** @param prompt user prompt (default "# ") @@ -69,7 +72,7 @@ class console: val console : ?prompt:string -> ?phrase_sep:string -> - ?callback:(string -> bool) -> + ?callback:callback -> ?evbox:GBin.event_box -> paned:GPack.paned -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6687ca69d..955ae13e5 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -23,24 +23,6 @@ * http://helm.cs.unibo.it/ *) -(* -class stringListModel' uriChoiceDialog = - let tree_view = uriChoiceDialog#uriChoiceTreeView in - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - let _ = tree_view#set_model (Some (list_store :> GTree.model)) in - let _ = tree_view#append_column view_column in - object - method append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - method clear () = list_store#clear () - end -*) - open Printf open MatitaGeneratedGui diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index dfb93cd18..39657c587 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -23,21 +23,13 @@ * http://helm.cs.unibo.it/ *) -(* -class type stringListModel = - object - method clear: unit -> unit - method append: string -> unit - end -*) - (** @param fname name of the Glade file describing the GUI *) class gui : string -> object method setQuitCallback : (unit -> unit) -> unit - method setPhraseCallback : (string -> bool) -> unit + method setPhraseCallback : (string -> MatitaTypes.command_outcome) -> unit (** {2 Access to lower-level GTK widgets} *) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index f99e11854..511a59314 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -26,9 +26,9 @@ (** 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 +* Interpreter is either in Command state or in Proof state (see state 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. *) @@ -36,8 +36,8 @@ open Printf open MatitaTypes - (** None means: "same state as before" *) -type state_tag = [ `Command | `Proof ] option +type state = Command | Proof +type outcome = New_state of state | Quiet | Echo of string exception Command_error of string @@ -53,6 +53,10 @@ let qualify name = baseuri ^ name else String.concat "/" [baseuri; name] +let split_obj = function + | Cic.Constant (name, body, ty, _) + | Cic.Variable (name, body, ty, _) -> (name, body, ty) + | _ -> assert false let canonical_context metano metasenv = try @@ -61,9 +65,9 @@ let canonical_context metano metasenv = with Not_found -> failwith (sprintf "Can't find canonical context for %d" metano) -let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) = - if proof_handler.MatitaTypes.has_proof () then - let proof = proof_handler.MatitaTypes.get_proof () in +let get_context_and_metasenv (currentProof:MatitaTypes.currentProof) = + if currentProof#onGoing () then + let proof = currentProof#proof in let metasenv = proof#metasenv in let goal = proof#goal in (canonical_context goal metasenv, metasenv) @@ -72,9 +76,9 @@ let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) = (** term AST -> Cic.term. Uses disambiguator and change imperatively the * metasenv as needed *) -let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast = - if proof_handler.MatitaTypes.has_proof () then begin - let proof = proof_handler.MatitaTypes.get_proof () in +let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast = + if currentProof#onGoing () then begin + let proof = currentProof#proof in let metasenv = proof#metasenv in let goal = proof#goal in let context = canonical_context goal metasenv in @@ -96,7 +100,7 @@ class virtual interpreterState = (** eval a toplevel phrase in the current state and return the new state *) method parsePhrase s = - match CicTextualParser2.parse_tactical (Stream.of_string s) with + match CicTextualParser2.parse_tactical s with | (TacticAst.LocatedTactical (loc', tac)) as tactical -> loc := Some loc'; (match tac with (* update interpreter history *) @@ -111,11 +115,11 @@ class virtual interpreterState = | _ -> assert false method virtual evalTactical: - (CicAst.term, string) TacticAst.tactical -> state_tag + (CicAst.term, string) TacticAst.tactical -> outcome method evalPhrase s = debug_print (sprintf "evaluating '%s'" s); - self#evalTactical (self#parsePhrase s) + self#evalTactical (self#parsePhrase (Stream.of_string s)) method evalAst ast = self#evalTactical ast @@ -126,16 +130,12 @@ class virtual interpreterState = end -let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy - (let gui = MatitaGui.instance () in - MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add - ()) - (** Implements phrases that should be accepted in all states *) class sharedState ~(disambiguator: MatitaTypes.disambiguator) - ~(proof_handler: MatitaTypes.proof_handler) + ~(currentProof: MatitaTypes.currentProof) ~(console: MatitaTypes.console) + ?(mathViewer: MatitaTypes.mathViewer option) ~(dbd: Mysql.dbd) () = @@ -143,23 +143,23 @@ class sharedState inherit interpreterState ~console method evalTactical = function | TacticAst.Command TacticAst.Quit -> - proof_handler.MatitaTypes.quit (); - Some `Command (* dummy answer, useless *) + currentProof#quit (); + assert false (* dummy answer, useless *) | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) - Some `Command + New_state Command | TacticAst.Command (TacticAst.Baseuri (Some uri)) -> baseuri := uri; console#echo_message (sprintf "base uri set to \"%s\"" uri); - None + Quiet | TacticAst.Command (TacticAst.Baseuri None) -> console#echo_message (sprintf "base uri is \"%s\"" !baseuri); - None + Quiet | TacticAst.Command (TacticAst.Check term) -> let (_, _, term,ugraph) = - disambiguate ~disambiguator ~proof_handler term + disambiguate ~disambiguator ~currentProof term in - let (context, metasenv) = get_context_and_metasenv proof_handler in + let (context, metasenv) = get_context_and_metasenv currentProof in let dummyno = CicMkImplicit.new_meta metasenv [] in let ty,ugraph1 = CicTypeChecker.type_of_aux' metasenv context term ugraph @@ -167,12 +167,10 @@ class sharedState (* TASSI: here ugraph1 is unused.... FIXME *) let expr = Cic.Cast (term, ty) in let sequent = (dummyno, context, expr) in - let widget = Lazy.force check_widget in - let gui = MatitaGui.instance () in - gui#check#checkWin#show (); - gui#main#showCheckMenuItem#set_active true; - widget#load_sequent (sequent::metasenv) dummyno; - None + (match mathViewer with + | None -> () + | Some v -> v#checkTerm sequent metasenv); + Quiet | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) -> let uris = match search_kind with @@ -181,7 +179,7 @@ class sharedState | _ -> assert false in (* TODO ZACK: show URIs to the user *) - None + Quiet | tactical -> raise (Command_error (TacticAstPp.pp_tactical tactical)) end @@ -262,15 +260,30 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = *) (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) - (** Implements phrases that should be accepted only in `Command state *) + (* TODO Zack a lot more to be done here: + * - save object to disk in xml format + * - register uri to the getter + * - save universe file *) +let add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph () = + let name = UriManager.name_of_uri uri in + let obj = Cic.Constant (name, body, ty, []) in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_term uri (obj, ugraph); + MetadataDb.index_constant ~dbd + ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty + + (** Implements phrases that should be accepted only in Command state *) class commandState ~(disambiguator: MatitaTypes.disambiguator) - ~(proof_handler: MatitaTypes.proof_handler) + ~(currentProof: MatitaTypes.currentProof) ~(console: MatitaTypes.console) + ?mathViewer ~(dbd: Mysql.dbd) () = - let shared = new sharedState ~disambiguator ~proof_handler ~console ~dbd () in + let shared = + new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () + in object (self) inherit interpreterState ~console @@ -282,8 +295,8 @@ class commandState in let uri = UriManager.uri_of_string (qualify name ^ ".con") in let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in - proof_handler.MatitaTypes.new_proof proof; - Some `Proof + currentProof#start proof; + New_state Proof | TacticAst.Command (TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) -> let (_, metasenv, type_cic, ugraph) = @@ -299,18 +312,10 @@ class commandState let (subst, metasenv, ugraph) = CicUnification.fo_unif metasenv [] body_type type_cic ugraph in - let body_cic = CicMetaSubst.apply_subst subst body_cic in - let type_cic = CicMetaSubst.apply_subst subst type_cic in - let obj = - Cic.Constant - ((UriManager.name_of_uri uri), (Some body_cic),type_cic,[]) - in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd - ~owner:(Helm_registry.get "matita.owner") ~uri - ~body:(Some body_cic) ~ty:type_cic; - None + let body = CicMetaSubst.apply_subst subst body_cic in + let ty = CicMetaSubst.apply_subst subst type_cic in + add_constant_to_world ~dbd ~uri ~body ~ty ~ugraph (); + Quiet | TacticAst.Command (TacticAst.Inductive (params, indTypes)) -> let (uri, (indTypes, params, leftno)) = inddef_of_ast params indTypes disambiguator @@ -324,13 +329,26 @@ class commandState CicEnvironment.put_inductive_definition uri (obj, ugraph); MetadataDb.index_inductive_def ~dbd ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes; - None + let msgs = ref [] in + let elim sort = + try + let obj = CicElim.elim_of ~sort uri 0 in + let (name, body, ty) = split_obj obj in + let uri = UriManager.uri_of_string (qualify name ^ ".con") in + (* TODO Zack: make CicElim returns a universe *) + let ugraph = CicUniv.empty_ugraph in + add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph (); + msgs := (sprintf "%s defined" name) :: !msgs; + with CicElim.Can_t_eliminate -> () + in + List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + Echo (String.concat "\n" (List.rev !msgs)) | TacticAst.Command TacticAst.Quit -> - proof_handler.MatitaTypes.quit (); - Some `Command (* dummy answer, useless *) + currentProof#quit (); + New_state Command (* dummy answer, useless *) | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) - Some `Command + New_state Command | tactical -> shared#evalTactical tactical end @@ -348,17 +366,18 @@ let namer_of names = end else FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - (** Implements phrases that should be accepted only in `Proof state, basically + (** Implements phrases that should be accepted only in Proof state, basically * tacticals *) class proofState ~(disambiguator: MatitaTypes.disambiguator) - ~(proof_handler: MatitaTypes.proof_handler) + ~(currentProof: MatitaTypes.currentProof) ~(console: MatitaTypes.console) + ?mathViewer ~(dbd: Mysql.dbd) () = let disambiguate ast = - let (_, _, term, _) = disambiguate ~disambiguator ~proof_handler ast in + let (_, _, term, _) = disambiguate ~disambiguator ~currentProof ast in term in (** tactic AST -> ProofEngineTypes.tactic *) @@ -404,28 +423,28 @@ class proofState | _ -> MatitaTypes.not_implemented "some tactic" in - let shared = new sharedState ~disambiguator ~proof_handler ~console ~dbd () in + let shared = new sharedState ~disambiguator ~currentProof ~console ~dbd () in object (self) inherit interpreterState ~console method evalTactical = function | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> - proof_handler.MatitaTypes.abort_proof (); - Some `Command + currentProof#abort (); + New_state Command | TacticAst.Command (TacticAst.Undo steps) -> - (proof_handler.MatitaTypes.get_proof ())#undo ?steps (); - Some `Proof + currentProof#proof#undo ?steps (); + New_state Proof | TacticAst.Command (TacticAst.Redo steps) -> - (proof_handler.MatitaTypes.get_proof ())#redo ?steps (); - Some `Proof + currentProof#proof#redo ?steps (); + New_state Proof | TacticAst.Command (TacticAst.Qed None) -> - (* TODO Zack this function probably should not simply fail with - * Failure, but rather raise some more meaningful exception *) - if not (proof_handler.MatitaTypes.has_proof ()) then assert false; - let proof = proof_handler.MatitaTypes.get_proof () in + if not (currentProof#onGoing ()) then assert false; + let proof = currentProof#proof in let (uri, metasenv, bo, ty) = proof#proof in let uri = MatitaTypes.unopt_uri uri in + (* TODO Zack this function probably should not simply fail with + * Failure, but rather raise some more meaningful exception *) if metasenv <> [] then failwith "Proof not completed"; let proved_ty,ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph @@ -433,46 +452,35 @@ class proofState let b,ugraph = CicReduction.are_convertible [] proved_ty ty ugraph in - if not b then - failwith "Wrong proof"; - (* TODO Zack [] probably wrong *) - let obj = - Cic.Constant ((UriManager.name_of_uri uri), (Some bo),ty,[]) - in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd - ~owner:(Helm_registry.get "matita.owner") ~uri ~body:(Some bo) ~ty; - proof_handler.MatitaTypes.set_proof None; - (MatitaMathView.proof_viewer_instance ())#unload; - (* TODO Zack a lot more to be done here: - * - save object to disk in xml format - * - register uri to the getter - * - save universe file *) - Some `Command + if not b then failwith "Wrong proof"; + add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph (); + currentProof#abort (); + (match mathViewer with None -> () | Some v -> v#unload ()); + New_state Command | TacticAst.Seq tacticals -> (* TODO Zack check for proof completed at each step? *) List.iter (fun t -> ignore (self#evalTactical t)) tacticals; - Some `Proof + New_state Proof | TacticAst.Tactic tactic_phrase -> let tactic = lookup_tactic tactic_phrase in - (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic; - Some `Proof + currentProof#proof#apply_tactic tactic; + New_state Proof | tactical -> shared#evalTactical tactical end class interpreter ~(disambiguator: MatitaTypes.disambiguator) - ~(proof_handler: MatitaTypes.proof_handler) + ~(currentProof: MatitaTypes.currentProof) ~(console: MatitaTypes.console) + ?mathViewer ~(dbd: Mysql.dbd) () = let commandState = - new commandState ~disambiguator ~proof_handler ~console ~dbd () + new commandState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () in let proofState = - new proofState ~disambiguator ~proof_handler ~console ~dbd () + new proofState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () in object (self) val mutable state = commandState @@ -482,22 +490,20 @@ class interpreter method endOffset = state#endOffset method private updateState = function - | Some `Command -> state <- commandState - | Some `Proof -> state <- proofState - | None -> () - - method evalPhrase s = - let success = - console#wrap_exn (fun () -> self#updateState (state#evalPhrase s)) - in - if success then console#clear (); - success - - method evalAst ast = - let success = - console#wrap_exn (fun () -> self#updateState (state#evalAst ast)) - in - if success then console#clear (); - success + | New_state Command -> (state <- commandState) + | New_state Proof -> (state <- proofState) + | _ -> () + + method private eval f = + let ok () = console#clear (); (true, true) in + match console#wrap_exn f with + | Some (New_state Command) -> (state <- commandState); ok () + | Some (New_state Proof) -> (state <- proofState); ok () + | Some (Echo msg) -> console#echo_message msg; (true, false) + | Some Quiet -> ok () + | None -> (false, false) + + method evalPhrase s = self#eval (fun () -> state#evalPhrase s) + method evalAst ast = self#eval (fun () -> state#evalAst ast) end diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index 96f824861..7886a564a 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -27,8 +27,9 @@ exception Command_error of string class interpreter: disambiguator:MatitaTypes.disambiguator -> - proof_handler:MatitaTypes.proof_handler -> + currentProof:MatitaTypes.currentProof -> console:MatitaTypes.console -> + ?mathViewer:MatitaTypes.mathViewer -> dbd:Mysql.dbd -> unit -> MatitaTypes.interpreter diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 8c38cfc0b..d485ac025 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -172,7 +172,7 @@ class sequent_viewer obj = class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () + ~(sequent_viewer:sequent_viewer) ~set_goal () = let tab_label metano = (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce @@ -277,7 +277,27 @@ let proof_viewer_instance = fun () -> Lazy.force instance let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () + ~(sequent_viewer:sequent_viewer) ~set_goal () = new sequents_viewer ~notebook ~sequent_viewer ~set_goal () +let check_widget = + lazy + (let gui = MatitaGui.instance () in + sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ()) + +class mathViewer = + object + method checkTerm sequent metasenv = + let (metano, context, expr) = sequent in + let widget = Lazy.force check_widget in + let gui = MatitaGui.instance () in + gui#check#checkWin#show (); + gui#main#showCheckMenuItem#set_active true; + widget#load_sequent (sequent :: metasenv) metano + + method unload () = (proof_viewer_instance ())#unload + end + +let mathViewer () = new mathViewer + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 02141cde5..b7a18e920 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -23,6 +23,36 @@ * http://helm.cs.unibo.it/ *) +class type proof_viewer = + object + inherit GMathViewAux.single_selection_math_view + + method load_proof: StatefulProofEngine.proof_status -> unit + end + +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 -> int -> unit + end + +class type sequents_viewer = + object + method reset: unit + method load_sequents: Cic.metasenv -> unit + method goto_sequent: int -> unit (* to be called _after_ load_sequents *) + end + val proof_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -33,11 +63,11 @@ val proof_viewer: ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> - MatitaTypes.proof_viewer + proof_viewer (** singleton proof_viewer instance. * Uses singleton GUI instance *) -val proof_viewer_instance: unit -> MatitaTypes.proof_viewer +val proof_viewer_instance: unit -> proof_viewer val sequent_viewer: ?hadjustment:GData.adjustment -> @@ -49,12 +79,14 @@ val sequent_viewer: ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> - MatitaTypes.sequent_viewer + sequent_viewer val sequents_viewer: notebook:GPack.notebook -> - sequent_viewer:MatitaTypes.sequent_viewer -> + sequent_viewer:sequent_viewer -> set_goal:(int -> unit) -> unit -> - MatitaTypes.sequents_viewer + sequents_viewer + +val mathViewer: unit -> MatitaTypes.mathViewer diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index ca1b4c907..54ebdf6cf 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -106,9 +106,49 @@ class proof ?uri ~typ ~metasenv ~body () = end +class currentProof = + let fail () = failwith "No current proof" in + object (self) + val mutable _proof: MatitaTypes.proof option = None + val mutable observers = [] + val mutable callbacks = [] + + initializer self#connect `Abort (fun () -> _proof <- None; false) + + (** execute all callbacks related to a given event until one of them + * return true or the end of the callback list is reached *) + method private do_callbacks event = + let rec aux = function + | [] -> () + | (event', f) :: tl when event' = event -> if not (f ()) then aux tl + | _ :: tl -> aux tl + in + aux callbacks + + method addObserver o = observers <- o :: observers + + method connect (event:[`Abort|`Quit]) f = + callbacks <- (event, f) :: callbacks + + method onGoing () = _proof <> None + method proof = match _proof with None -> fail () | Some proof -> proof + method start (proof: MatitaTypes.proof) = + List.iter + (fun observer -> + ignore (proof#attach_observer + ~interested_in:StatefulProofEngine.all_events observer)) + observers; + proof#notify; + _proof <- Some proof + method abort () = self#do_callbacks `Abort + method quit () = self#do_callbacks `Quit + end + 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 () +let currentProof () = new currentProof + diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli index 9293e330a..566777fc1 100644 --- a/helm/matita/matitaProof.mli +++ b/helm/matita/matitaProof.mli @@ -35,3 +35,20 @@ val proof: unit -> MatitaTypes.proof + (** current proof handler *) +class currentProof: + object + inherit MatitaTypes.currentProof + + (** add an observer to the current observer list. All observers will be + * attached to each new proof (method "start") created by this object + *) + method addObserver: unit StatefulProofEngine.observer -> unit + + (** connect as the first event handler for a given event (abort or quit). + * If the event handler returns true, handler processing stops, otherwise + * continue with the next handler + *) + method connect: [`Abort|`Quit] -> (unit -> bool) -> unit + end + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 4631fa351..5305ea463 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -23,17 +23,29 @@ * http://helm.cs.unibo.it/ *) +open Printf + exception Not_implemented of string let not_implemented feature = raise (Not_implemented feature) - (** exceptions whose content should be presented to the user *) exception Failure of string let error s = raise (Failure s) let warning s = prerr_endline ("MATITA WARNING:\t" ^ s) let debug_print s = if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s) -exception No_proof (** no current proof is available *) +let explain = function + | StatefulProofEngine.Tactic_failure exn -> + sprintf "Tactic failed: %s"(Printexc.to_string exn) + | StatefulProofEngine.Observer_failures exns -> + String.concat "\n" + (List.map (fun (_, exn) -> Printexc.to_string exn) exns) + | CicTextualParser2.Parse_error (floc, msg) -> + let (x, y) = CicAst.loc_of_floc floc in + sprintf "parse error at character %d-%d: %s" x y msg + | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn) + +exception No_proof exception Cancel exception Unbound_identifier of string @@ -55,13 +67,12 @@ class type parserr = (* "parser" is a keyword :-( *) method parseTactical: char Stream.t -> DisambiguateTypes.tactical end - (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) class type console = object method echo_message : string -> unit method echo_error : string -> unit method clear : unit -> unit - method wrap_exn : (unit -> unit) -> bool + method wrap_exn : 'a. (unit -> 'a) -> 'a option end class type disambiguator = @@ -72,28 +83,19 @@ class type disambiguator = method env: DisambiguateTypes.environment method setEnv: DisambiguateTypes.environment -> unit - (* TODO Zack: as long as matita doesn't support MDI inteface, - * disambiguateTerm will return a single term *) - (** @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 * CicUniv.universe_graph) - (** @param env @see disambiguateTerm above *) + (DisambiguateTypes.environment * Cic.metasenv * Cic.term * + CicUniv.universe_graph) method disambiguateTermAst: ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> DisambiguateTypes.term -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) + (DisambiguateTypes.environment * Cic.metasenv * Cic.term * + CicUniv.universe_graph) - (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All - * AST should be closed hence no context param is permitted on this method - *) method disambiguateTermAsts: ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> @@ -102,69 +104,39 @@ class type disambiguator = CicUniv.universe_graph) end -(* -type sequents_metadata = - (int * (** sequent (meta) index *) - (Cic.annconjecture * (** annotated conjecture *) - (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) - (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) - (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *) - list -type proof_metadata = - Cic.annobj * (** annotated object *) - (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) - (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) - (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *) - (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *) - (Cic.id, Cic.hypothesis) Hashtbl.t (** ids_to_hypotheses *) -type hist_metadata = proof_metadata * sequents_metadata -*) - class type proof = object inherit [unit] StatefulProofEngine.status - (** return a pair of "xml" (as defined in Xml module) representing the * - * current proof type and body, respectively *) method toXml: Xml.token Stream.t * Xml.token Stream.t method toString: string end -type proof_handler = - { get_proof: unit -> proof; (* return current proof or fail *) - set_proof: proof option -> unit; - abort_proof: unit -> unit;(* abort current proof, cleaning up garbage *) - has_proof: unit -> bool; (* check if a current proof is available or not *) - new_proof: proof -> unit; (* as a set_proof but takes care also to register - observers *) - quit: unit -> unit - } - - (** interpreter for toplevel phrases given via console *) -class type interpreter = +class type currentProof = object - method reset: unit (** return the interpreter to the initial state *) - - (** parse a single phrase contained in the input string. Additional - * garbage at the end of the phrase is ignored - * @return true if no exception has been raised by the evaluation, false - * otherwise - *) - method evalPhrase: string -> bool - - (** as above, evaluating a command/tactics AST *) - method evalAst: DisambiguateTypes.tactical -> bool + method onGoing: unit -> bool + method proof: proof + method start: proof -> unit + method abort: unit -> unit + method quit: unit -> unit + end - (** offset from the starting of the last string parser by evalPhrase where - * parsing stop. - * @raise Failure when no offset has been recorded *) - method endOffset: int +type command_outcome = bool * bool +class type interpreter = + object + method endOffset : int + method evalAst : DisambiguateTypes.tactical -> command_outcome + method evalPhrase : string -> command_outcome +(* method evalStream: char Stream.t -> command_outcome *) + method reset : unit end -(** {2 MathML widgets} *) +class type mathViewer = + object + method checkTerm: Cic.conjecture -> Cic.metasenv -> unit + method unload: unit -> unit + end type mml_of_cic_sequent = Cic.metasenv -> Cic.conjecture -> @@ -178,38 +150,6 @@ type mml_of_cic_object = (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document -class type proof_viewer = - object - inherit GMathViewAux.single_selection_math_view - - method load_proof: StatefulProofEngine.proof_status -> unit - end - -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 -> int -> unit - end - -class type sequents_viewer = - object - method reset: unit - method load_sequents: Cic.metasenv -> unit - method goto_sequent: int -> unit (* to be called _after_ load_sequents *) - end - -(** {2 shorthands} *) - type namer = ProofEngineTypes.mk_fresh_name_type type choose_uris_callback = @@ -217,6 +157,9 @@ type choose_uris_callback = ?title:string -> ?msg:string -> ?nonvars_button:bool -> string list -> string list - type choose_interp_callback = (string * string) list list -> int list +let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ = + raise (Failure "ambiguous input") +let mono_interp_callback _ = raise (Failure "ambiguous input") + diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli new file mode 100644 index 000000000..cc91486d6 --- /dev/null +++ b/helm/matita/matitaTypes.mli @@ -0,0 +1,193 @@ +(* 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/ + *) + + (** exceptions whose content should be presented to the user *) +exception Not_implemented of string +exception Failure of string + +val not_implemented : string -> 'a +val error : string -> 'a +val warning : string -> unit +val debug_print : string -> unit + +exception No_proof (** no current proof is available *) +exception Cancel +exception Unbound_identifier of string + + (** @param exn an exception + * @return a string which is meant to be a textual explaination of the + exception understandable by a user *) +val explain: exn -> string + +val unopt_uri : 'a option -> 'a + +class type parserr = + object + method parseTactical : char Stream.t -> DisambiguateTypes.tactical + method parseTerm : char Stream.t -> DisambiguateTypes.term + end + + (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) +class type console = + object + method clear : unit -> unit + method echo_error : string -> unit + method echo_message : string -> unit + method wrap_exn : 'a. (unit -> 'a) -> 'a option + end + +class type disambiguator = + object + method parserr : parserr + method setParserr : parserr -> unit + + method env : DisambiguateTypes.environment + method setEnv : DisambiguateTypes.environment -> unit + + (* TODO Zack: as long as matita doesn't support MDI inteface, + * disambiguateTerm will return a single term *) + (** @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 * + CicUniv.universe_graph + + (** @param env @see disambiguateTerm above *) + method disambiguateTermAst : + ?context:Cic.context -> + ?metasenv:Cic.metasenv -> + ?env:DisambiguateTypes.environment -> + DisambiguateTypes.term -> + DisambiguateTypes.environment * Cic.metasenv * Cic.term * + CicUniv.universe_graph + + (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All + * AST should be closed hence no context param is permitted on this method + *) + method disambiguateTermAsts : + ?metasenv:Cic.metasenv -> + ?env:DisambiguateTypes.environment -> + DisambiguateTypes.term list -> + DisambiguateTypes.environment * Cic.metasenv * Cic.term list * + CicUniv.universe_graph + end + +class type proof = + object + inherit [unit] StatefulProofEngine.status + + (** return a pair of "xml" (as defined in Xml module) representing the * + * current proof type and body, respectively *) + method toXml : Xml.token Stream.t * Xml.token Stream.t + + method toString : string + end + +class type currentProof = + object + method onGoing: unit -> bool (** true if a proof is on going *) + method proof: proof (** @raise Failure "No current proof" *) + method start: proof -> unit (** starts a new proof *) + method abort: unit -> unit (** abort the on going proof *) + method quit: unit -> unit (** quit matita *) + end + + (** first component represents success: true = success, false = failure + * second component represents console action: true = hide, false = keep *) +type command_outcome = bool * bool + + (** interpreter for toplevel phrases given via console *) +class type interpreter = + object + method reset: unit (** return the interpreter to the initial state *) + + (** parse a single phrase contained in the input string. Additional + * garbage at the end of the phrase is ignored + * @return true if no exception has been raised by the evaluation, false + * otherwise + *) + method evalPhrase: string -> command_outcome + + (** as evalPhrase above, but parses a character stream. Only characters + * composing next phrases are consumed *) +(* method evalStream: char Stream.t -> command_outcome *) + + (** as above, evaluating a command/tactics AST *) + method evalAst: DisambiguateTypes.tactical -> command_outcome + + (** offset from the starting of the last string parser by evalPhrase where + * parsing stop. + * @raise Failure when no offset has been recorded *) + method endOffset: int + + end + +(** {2 MathML widgets} *) + +class type mathViewer = + object + method checkTerm: Cic.conjecture -> Cic.metasenv -> unit + method unload: unit -> unit + end + +type mml_of_cic_sequent = + Cic.metasenv -> + Cic.conjecture -> + 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 + +(** {2 shorthands} *) + +type namer = ProofEngineTypes.mk_fresh_name_type + + (** {3 disambiguator callbacks} *) + +type choose_uris_callback = + selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?title:string -> + ?msg:string -> ?nonvars_button:bool -> string list -> string list + +type choose_interp_callback = (string * string) list list -> int list + + (** @raise Failure if called, use if unambiguous input is required *) +val mono_uris_callback: choose_uris_callback + (** @raise Failure if called, use if unambiguous input is required *) +val mono_interp_callback: choose_interp_callback + diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml new file mode 100644 index 000000000..648702490 --- /dev/null +++ b/helm/matita/matitac.ml @@ -0,0 +1,113 @@ +(* 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/ + *) + +open Printf + +open MatitaTypes + +let message s = printf "** MatitaC: %s\n" s; flush stdout +let warn s = eprintf "** MatitaC WARNING: %s\n" s; flush stdout +let error s = eprintf "** MatitaC ERROR: %s\n" s; flush stderr + + (** console which prints on stdout/stderr *) +class tty_console = + object (self) + method clear () = () + method echo_message s = message s + method echo_error s = error s + (* TODO Zack: this method is similar to omonymous method in console, + * factorize it in a common super class *) + method wrap_exn: 'a. (unit -> 'a) -> 'a option = + fun f -> + try + Some (f ()) + with exn -> + self#echo_error (explain exn); + None + end + +(** {2 Initialization} *) + +let arg_spec = [ +(* "-opt", Arg...., "set bla bla bla"; *) +] +let usage = + sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:" + BuildTimeConf.version + +let _ = Helm_registry.load_from "matita.conf.xml" + +let scripts = + let acc = ref [] in + let add_script fname = acc := fname :: !acc in + Arg.parse arg_spec add_script usage; + List.rev !acc + +let parserr = new MatitaDisambiguator.parserr () +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () +let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner") +let disambiguator = + new MatitaDisambiguator.disambiguator ~parserr ~dbd + ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback + () +let console = new tty_console +let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof) +let interpreter = + new MatitaInterpreter.interpreter + ~disambiguator ~currentProof ~console ~dbd () + +let run_script fname = + message (sprintf "execution of %s started." fname); + let script = + let ic = open_in fname in + let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in + close_in ic; + ast + in + let rec aux = function + | [] -> () + | DisambiguateTypes.Comment _ :: tl -> aux tl + | DisambiguateTypes.Command ast :: tl -> + let loc = + match ast with + | TacticAst.LocatedTactical (loc, _) -> loc + | _ -> assert false + in + let (success, _) = interpreter#evalAst ast in + if not success then + error (sprintf "%s: error at %s, aborting." fname + (CicAst.pp_location loc)) + else + aux tl + in + aux script + +let _ = List.iter run_script scripts + -- 2.39.2