From 642e20a0135126586603ffb539f0d1c1428f1502 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 9 Feb 2005 15:07:37 +0000 Subject: [PATCH] added script support a la coqide --- helm/matita/.depend | 13 +- helm/matita/Makefile.in | 3 +- helm/matita/matita.ml | 95 ++++++-------- helm/matita/matitaInterpreter.ml | 56 +++++--- helm/matita/matitaScript.ml | 212 +++++++++++++++++++++++++++++++ helm/matita/matitaScript.mli | 45 +++++++ helm/matita/matitaTypes.ml | 14 +- helm/matita/matitaTypes.mli | 24 +++- 8 files changed, 376 insertions(+), 86 deletions(-) create mode 100644 helm/matita/matitaScript.ml create mode 100644 helm/matita/matitaScript.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index be6811b19..dd0b23972 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -34,16 +34,20 @@ matitaMathView.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx \ buildTimeConf.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ - matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \ +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaProof.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \ matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \ - matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaProof.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaProof.cmo: matitaTypes.cmi matitaMisc.cmi matitaCicMisc.cmi \ buildTimeConf.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaMisc.cmx matitaCicMisc.cmx \ buildTimeConf.cmx matitaProof.cmi +matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaMathView.cmi \ + matitaGui.cmi matitaScript.cmi +matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaMathView.cmx \ + matitaGui.cmx matitaScript.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi matitaCicMisc.cmi: matitaTypes.cmi @@ -54,3 +58,4 @@ matitaGui.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaConsole.cmi matitaInterpreter.cmi: matitaTypes.cmi matitaMathView.cmi: matitaTypes.cmi matitaProof.cmi: matitaTypes.cmi +matitaScript.cmi: matitaTypes.cmi matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 0ca62ff70..90a8a2a41 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -29,7 +29,8 @@ CMOS = \ matitaProof.cmo \ matitaDisambiguator.cmo \ matitaMathView.cmo \ - matitaInterpreter.cmo + matitaInterpreter.cmo \ + matitaScript.cmo # objects for matitac (batch compiler) CCMOS = \ buildTimeConf.cmo \ diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 4b9d9e1f6..e6eff09fe 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -41,10 +41,11 @@ let _ = ignore (GMain.Main.init ()) let gui = MatitaGui.instance () +let disambiguator = MatitaDisambiguator.instance () let _ = (* set disambiguator callbacks *) - let disambiguator = MatitaDisambiguator.instance () in disambiguator#setChooseUris (interactive_user_uri_choice ~gui); disambiguator#setChooseInterp (interactive_interp_choice ~gui) + let _ = (* environment trust *) CicEnvironment.set_trust (let trust = Helm_registry.get_bool "matita.environment_trust" in @@ -52,15 +53,8 @@ let _ = (* environment trust *) let currentProof = MatitaProof.instance () - -let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () -let sequents_viewer = - let 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 sequent_viewer = MatitaMathView.sequent_viewer_instance () +let sequents_viewer = MatitaMathView.sequents_viewer_instance () let _ = (* attach observers to proof status *) let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = @@ -86,6 +80,7 @@ let _ = (* attach observers to proof status *) let interpreter = let mathViewer = MatitaMathView.mathViewer () in MatitaInterpreter.interpreter ~console:gui#console ~mathViewer () +let script = MatitaScript.script ~interpreter let _ = let href_callback uri = let term = CicAst.Uri (uri, None) in @@ -93,53 +88,37 @@ let _ = in sequent_viewer#set_href_callback (Some href_callback) -(** {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 - let (success, hide) = - interpreter#evalPhrase - (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()) +let console_callback s = + let module A = TacticAst in + let rec strip_locations = function + | A.LocatedTactical (loc, tac) -> strip_locations tac + | tac -> tac in - if success then - gui#lockScript (locked_iter#offset + interpreter#endOffset) - -let script_jump _ = - let buf = gui#script#scriptTextView#buffer in - let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in - let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in - let len = String.length raw_text in - let rec parse offset = - if offset < len then begin - let (success, hide) = - interpreter#evalPhrase (String.sub raw_text offset (len - offset)) - in - if success then begin - let new_offset = interpreter#endOffset + offset in - gui#lockScript (new_offset + locked_iter#offset); - parse new_offset - end else - raise Exit - end + let needed_by_script ast = + prerr_endline (TacticAstPp.pp_tactical ast); + match strip_locations ast with + | A.Tactic _ + | A.Command + (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) -> + true + | _ -> false in - try - parse 0 - with Exit -> () + let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in + if needed_by_script ast then + script#advance ast + else + interpreter#evalAst ast -let script_back _ = not_implemented "script_back" - -let load_script fname = - gui#script#scriptTextView#buffer#set_text (input_file fname); - gui#script#scriptWin#show (); - gui#main#showScriptMenuItem#set_active true +let console_callback s = + match gui#console#wrap_exn (fun () -> console_callback s) with + | None -> (false, false) + | Some outcome -> outcome (** {2 GUI callbacks} *) let _ = gui#setQuitCallback currentProof#quit; - gui#setPhraseCallback interpreter#evalPhrase; + gui#setPhraseCallback console_callback; gui#main#debugMenu#misc#hide (); ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> gui#console#clear (); @@ -147,19 +126,21 @@ let _ = ignore (gui#main#openMenuItem#connect#activate (fun _ -> match gui#chooseFile () with | None -> () - | Some f when is_proof_script f -> load_script f + | Some f when is_proof_script f -> + ignore (gui#console#wrap_exn (fun () -> script#loadFrom f)) | Some f -> gui#console#echo_error (sprintf "Don't know what to do with file: %s\nUnrecognized file format." f))); ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> ignore (MatitaMathView.cicBrowser ()))); - connect_button gui#script#scriptWinForwardButton script_forward; - connect_button gui#script#scriptWinBackButton script_back; - connect_button gui#script#scriptWinJumpButton script_jump; let module A = TacticAst in let hole = CicAst.UserInput in - let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in + let tac ast _ = + let ast = A.Tactic ast in + ignore (interpreter#evalAst ast); + ignore (script#advance ast) + in let tac_w_term ast _ = (* gui#console#clear (); *) gui#console#show ~msg:(TacticAstPp.pp_tactic ast) (); @@ -212,11 +193,7 @@ let _ = (** *) let _ = -(* - (try - load_script Sys.argv.(1) - with Invalid_argument _ -> ()); -*) + (try script#loadFrom Sys.argv.(1) with Invalid_argument _ -> ()); if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) Helm_registry.set "matita.mode" "cicbrowser"; let browser = MatitaMathView.cicBrowser () in diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 4d3137d55..96b765c70 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -63,7 +63,8 @@ let split_obj = function class virtual interpreterState = (* static values, shared by all states inheriting this class *) let loc = ref None in - let history = ref [] in + let last_item = ref None in + let evalAstCallback = ref None in fun ~(console: #MatitaTypes.console) -> object (self) @@ -74,34 +75,37 @@ class virtual interpreterState = (** eval a toplevel phrase in the current state and return the new state *) method parsePhrase s = - match CicTextualParser2.parse_tactical s with + match disambiguator#parserr#parseTactical s with | (TacticAst.LocatedTactical (loc', tac)) as tactical -> loc := Some loc'; - (match tac with (* update interpreter history *) - | TacticAst.Command (TacticAst.Qed None) -> - history := `Qed :: !history - | TacticAst.Command (TacticAst.Theorem (_, Some name, _, None)) -> - history := `Theorem name :: !history - | TacticAst.Command (TacticAst.Qed _) - | TacticAst.Command (TacticAst.Theorem _) -> assert false - | _ -> history := `Tactic :: !history); tactical | _ -> assert false method virtual evalTactical: (CicAst.term, string) TacticAst.tactical -> outcome + method private _evalTactical ast = + self#setLastItem None; + let res = self#evalTactical ast in + (match !evalAstCallback with Some f -> f ast | None -> ()); + res + method evalPhrase s = debug_print (sprintf "evaluating '%s'" s); - self#evalTactical (self#parsePhrase (Stream.of_string s)) + self#_evalTactical (self#parsePhrase (Stream.of_string s)) - method evalAst ast = self#evalTactical ast + method evalAst ast = self#_evalTactical ast method endOffset = match !loc with | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum | None -> failwith "MatitaInterpreter: no offset recorded" + method lastItem: script_item option = !last_item + method private setLastItem item = last_item := item + + method setEvalAstCallback f = evalAstCallback := Some f + end (** Implements phrases that should be accepted in all states *) @@ -380,6 +384,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () = let uri = UriManager.uri_of_string (qualify name ^ ".con") in let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in currentProof#start proof; + self#setLastItem (Some `Theorem); New_state Proof | TacticAst.Command (TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) -> @@ -399,6 +404,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () = let body = CicMetaSubst.apply_subst subst body_cic in let ty = CicMetaSubst.apply_subst subst type_cic in add_constant_to_world ~console ~dbd ~uri ~body ~ty ~ugraph (); + self#setLastItem (Some (`Def uri)); Quiet | TacticAst.Command (TacticAst.Inductive (params, indTypes)) -> @@ -412,6 +418,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () = in add_inductive_def_to_world ~console ~dbd ~uri ~indTypes ~params ~leftno ~ugraph (); + self#setLastItem (Some (`Inductive uri)); Quiet | TacticAst.Command TacticAst.Quit -> currentProof#quit (); @@ -471,8 +478,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () = UriManager.uri_of_string (base ^ xp) | Cic.Appl (he::_) -> uri_of_term he | t -> - prerr_endline ("Fallisco a estrarre la uri di " ^ - (CicPp.ppterm t)); + error ("can't extract uri from " ^ (CicPp.ppterm t)); assert false in let ty_src,ty_tgt = extract_last_two_p coer_ty in @@ -605,14 +611,21 @@ class proofState ~(console: #MatitaTypes.console) ?mathViewer () = add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph (); currentProof#abort (); console#echo_message (sprintf "%s defined" suri); + self#setLastItem (Some (`Qed uri)); New_state Command | TacticAst.Seq tacticals -> - (* TODO Zack check for proof completed at each step? *) + (* TODO ZACK check for proof completed at each step? *) + (* TODO ZACK code completely broken here: we must build logic level + * tacticals instead of iterating interpreter evaluation *) + if (List.length tacticals > 1) then + warning "tacticals are broken: see matitaInterpreter.ml"; List.iter (fun t -> ignore (self#evalTactical t)) tacticals; + self#setLastItem (Some `Tactic); New_state Proof | TacticAst.Tactic tactic_phrase -> let tactic = self#lookup_tactic tactic_phrase in currentProof#proof#apply_tactic tactic; + self#setLastItem (Some `Tactic); New_state Proof | tactical -> shared#evalTactical tactical end @@ -623,9 +636,10 @@ class interpreter ~(console: #MatitaTypes.console) ?mathViewer () = object (self) val mutable state = commandState - method reset = state <- commandState - - method endOffset = state#endOffset + method setState (tag: [`Proof | `Command]) = + match tag with + | `Proof -> (state <- proofState) + | `Command -> (state <- commandState) method private updateState = function | New_state Command -> (state <- commandState) @@ -643,6 +657,12 @@ class interpreter ~(console: #MatitaTypes.console) ?mathViewer () = method evalPhrase s = self#eval (fun () -> state#evalPhrase s) method evalAst ast = self#eval (fun () -> state#evalAst ast) + + (** {2 methods delegated to current state} *) + + method endOffset = state#endOffset + method lastItem = state#lastItem + method setEvalAstCallback = state#setEvalAstCallback end let interpreter ~(console: #MatitaTypes.console) ?mathViewer () = diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml new file mode 100644 index 000000000..acb73fb54 --- /dev/null +++ b/helm/matita/matitaScript.ml @@ -0,0 +1,212 @@ +(* Copyright (C) 2005, 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 + +exception Script_failure of string + +let remove_constant_from_world ~dbd ~uri = + CicEnvironment.remove_obj uri; + MetadataDb.unindex ~dbd ~uri; + let uri = UriManager.string_of_uri uri in + List.iter + (* TODO ZACK remove xml files from disk *) + (fun suffix -> Http_getter.unregister (uri ^ suffix)) + [""; ".body"; ".types"] + +let remove_inductive_def_from_world ~dbd ~uri = + remove_constant_from_world ~dbd ~uri; + let uri = UriManager.string_of_uri uri in + Http_getter.unregister uri; + List.iter + (fun suffix -> + let uri = + Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri + in + remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri)) + ["ind"; "rec"; "rect"] + +let is_empty = + let rex = Pcre.regexp "^\\s*$" in + fun s -> + Pcre.pmatch ~rex s + +class script ~(interpreter:MatitaTypes.interpreter) () = + let gui = MatitaGui.instance () in + let script = gui#script in + let buf = script#scriptTextView#buffer in + let dbd = MatitaMisc.dbd_instance () in + let rec undo_item = function + | None -> () + | Some item -> + (match item with + | `Tactic -> + let res = + interpreter#evalAst (TacticAst.Command (TacticAst.Undo None)) + in + assert (fst res) + | `Theorem -> + interpreter#setState `Command; + (MatitaMathView.sequents_viewer_instance ())#reset + | `Qed uri + | `Def uri -> remove_constant_from_world ~dbd ~uri + | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri) + in + object (self) + initializer + let console = (MatitaGui.instance ())#console in + let w f () = ignore (console#wrap_exn (fun () -> f ())) in + ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); + ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom)); + ignore (gui#script#scriptWinForwardButton#connect#clicked + (w self#forward)); + ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back)); + ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); + ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump)) + + val mutable items = [] + + (** {3 text buffer locking} *) + + (** text mark and tag representing locked part of a script *) + val locked_mark = + buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter + val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] + + (** lock script text view from the beginning to the given offset (in UTF-8 + * characters) *) + method private lockScript offset = + let mark = `MARK locked_mark in + buf#move_mark mark ~where:(buf#get_iter_at_char offset); + buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter; + buf#apply_tag locked_tag ~start:buf#start_iter + ~stop:(buf#get_iter_at_mark mark) + + method win = gui#script + + method loadFrom fname = + buf#set_text (MatitaMisc.input_file fname); + gui#script#scriptWin#show (); + gui#main#showScriptMenuItem#set_active true + + method advance tactical = + let text = "\n" ^ TacticAstPp.pp_tactical tactical in + buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text; + let res = self#_forward () in + if not (fst res) then begin + let locked_iter = buf#get_iter_at_mark (`NAME "locked") in + buf#delete ~start:locked_iter + ~stop:(locked_iter#forward_chars (String.length text)); + end; + res + + (** {3 script progress} *) + + method private jump () = + let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in + let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in + let rec forward_until_cursor () = + prerr_endline "forward_until_cursor"; + (* go forward until locked > cursor (or forward fails) *) + let success = + try + fst (self#_forward ~stop:cursor_iter ()) + with + | Script_failure _ | CicTextualParser2.Parse_error _ -> false + in + if success && (locked_iter ())#compare cursor_iter < 0 then + forward_until_cursor () + in + let rec back_until_cursor () = (* go backward until locked < cursor *) + prerr_endline "back_until_cursor"; + let res = self#back () in + if (locked_iter ())#compare cursor_iter > 0 then + back_until_cursor () + in + let cmp = (locked_iter ())#compare cursor_iter in + if cmp < 0 then (* locked < cursor *) + (prerr_endline "locked < cursor"; forward_until_cursor ()) + else if cmp > 0 then (* locked > cursor *) + (prerr_endline "locked > cursor"; back_until_cursor ()) + else (* cursor = locked *) + () + + method private top () = + try while true do self#back () done with Script_failure _ -> () + + method private bottom () = + try + while true do + let res = self#_forward () in + if not (fst res) then raise (Script_failure "error") + done + with Script_failure _ -> () + + method private _forward ?(stop = buf#end_iter) () = + let locked_iter = buf#get_iter_at_mark (`NAME "locked") in + let (success, hide) as res = + let text = buf#get_text ~start:locked_iter ~stop () in + if is_empty text then + raise (Script_failure "at bottom") + else + interpreter#evalPhrase text + in + if success then begin + let old_offset = locked_iter#offset in + let new_offset = old_offset + interpreter#endOffset in + self#lockScript new_offset; + items <- (interpreter#lastItem, old_offset) :: items + end; + res + + method private forward () = ignore (self#_forward ()) + + method private back () = + (* clean history backward until the first theorem, return offset before + * it and remaning history *) + let rec flush_theorem = function + | (Some `Theorem, offset) :: tl -> offset, tl + | _ :: tl -> flush_theorem tl + | [] -> assert false + in + match items with + | [] -> raise (Script_failure "at top") + | (item, last_offset) :: tl -> + undo_item item; + let (last_offset, tl) = + (* if undoing a qed, go back before corresponding theorem *) + match item with + | Some (`Qed _) -> flush_theorem tl + | _ -> last_offset, tl + in + items <- tl; + self#lockScript last_offset + + end + +let script ~interpreter = new script ~interpreter () + diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli new file mode 100644 index 000000000..cdcb5a544 --- /dev/null +++ b/helm/matita/matitaScript.mli @@ -0,0 +1,45 @@ +(* Copyright (C) 2005, 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/ + *) + + (** script failures (e.g. going before the beginning or after the end of the + * script) *) +exception Script_failure of string + +class type script = + object + (** script window used by this script *) + method win: MatitaGeneratedGui.scriptWin + + (** fill text buffer reading a script from a file *) + method loadFrom: string -> unit + + (** adds a tactical at current script execution point and execute it. Used + * when the user uses buttons or console instead of directly editing the + * script *) + method advance: DisambiguateTypes.tactical -> MatitaTypes.command_outcome + end + +val script: interpreter:MatitaTypes.interpreter -> script + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 8f59d3fc9..a9e74bf5f 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -137,13 +137,23 @@ class type currentProof = type command_outcome = bool * bool +type script_item = + [ `Tactic + | `Theorem + | `Qed of UriManager.uri + | `Def of UriManager.uri + | `Inductive of UriManager.uri + ] + 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 + method endOffset : int + method lastItem: script_item option + method setState: [`Proof | `Command] -> unit + method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit end type term_source = diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index 99e69f6e1..538b4b324 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -146,11 +146,18 @@ class type currentProof = * second component represents console action: true = hide, false = keep *) type command_outcome = bool * bool + (** schematic representation of items scripts are made of *) +type script_item = + [ `Tactic (** action on proof status *) + | `Theorem (** start of proof, to be proved *) + | `Qed of UriManager.uri (** end of proof, successfull *) + | `Def of UriManager.uri (** constant with body *) + | `Inductive of UriManager.uri (** inductive definition *) + ] + (** 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 @@ -165,11 +172,24 @@ class type interpreter = (** as above, evaluating a command/tactics AST *) method evalAst: DisambiguateTypes.tactical -> command_outcome + (** {3 callbacks} *) + + method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit + + (** {3 stateful methods} + * bookkeeping of last interpreted phrase *) + (** 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 + (** last item parsed *) + method lastItem: script_item option + + (** change internal interpreter state *) + method setState: [`Proof | `Command] -> unit + end (** {2 MathML widgets} *) -- 2.39.2