autom4te.cache
matita
matita.opt
+matitac
+matitac.opt
*.cm[aiox]
*.cmxa
*.[ao]
-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
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 \
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
AC_MSG_ERROR(could not find camlp4o)
fi
-FINDLIB_REQUIRES="\
-lablgtk2.glade \
-lablgtkmathview \
+FINDLIB_CREQUIRES="\
pcre \
mysql \
unix \
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)
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)
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
~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;
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 _ =
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
(** {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 _ ->
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)
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;
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 ]
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
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
* 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
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 "# ")
val console :
?prompt:string ->
?phrase_sep:string ->
- ?callback:(string -> bool) ->
+ ?callback:callback ->
?evbox:GBin.event_box ->
paned:GPack.paned ->
* 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
* 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} *)
(** 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.
*)
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
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
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)
(** 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
(** 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 *)
| _ -> 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
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)
()
=
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
(* 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
| _ -> assert false
in
(* TODO ZACK: show URIs to the user *)
- None
+ Quiet
| tactical ->
raise (Command_error (TacticAstPp.pp_tactical tactical))
end
*)
(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
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) =
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
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
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 *)
| _ ->
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
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
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
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
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
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
+
* 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 ->
?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 ->
?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
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
+
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
+
* 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
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 =
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 ->
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 ->
(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 =
?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")
+
--- /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/
+ *)
+
+ (** 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
+
--- /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/
+ *)
+
+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
+
projects / helm.git / commitdiff