From 3705200c998538c28d8cd9d3ca557616837daf05 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 13 Oct 2004 08:17:57 +0000 Subject: [PATCH] snapshot, notably history no longer remember annotations: they are computed on the fly --- helm/matita/.depend | 24 +++-- helm/matita/Makefile.in | 1 + helm/matita/buildTimeConf.ml.in | 1 + helm/matita/matita.glade | 36 +++++-- helm/matita/matita.ml | 29 +++--- helm/matita/matitaGeneratedGui.ml | 41 +++++--- helm/matita/matitaGeneratedGui.mli | 25 +++-- helm/matita/matitaGui.ml | 5 +- helm/matita/matitaInterpreter.ml | 60 +++++++++--- helm/matita/matitaMathView.ml | 149 +++++++++++++---------------- helm/matita/matitaMathView.mli | 1 + helm/matita/matitaProof.ml | 26 +++-- helm/matita/matitaTypes.ml | 13 ++- 13 files changed, 241 insertions(+), 170 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index a21785af7..d348338e8 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,5 +1,7 @@ -matitaConsole.cmo: matitaGtkMisc.cmi matitaConsole.cmi -matitaConsole.cmx: matitaGtkMisc.cmx matitaConsole.cmi +matitaCicMisc.cmo: matitaTypes.cmo +matitaCicMisc.cmx: matitaTypes.cmx +matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaConsole.cmi +matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaConsole.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi @@ -10,20 +12,22 @@ matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ matitaGtkMisc.cmi matitaGui.cmi matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ matitaGtkMisc.cmx matitaGui.cmi -matitaInterpreter.cmo: matitaConsole.cmi matitaProof.cmi matitaTypes.cmo \ - matitaInterpreter.cmi -matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \ - matitaInterpreter.cmi -matitaMathView.cmo: matitaTypes.cmo matitaMathView.cmi -matitaMathView.cmx: matitaTypes.cmx matitaMathView.cmi +matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \ + matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi +matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \ + matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi +matitaMathView.cmo: matitaCicMisc.cmo matitaTypes.cmo matitaMathView.cmi +matitaMathView.cmx: matitaCicMisc.cmx matitaTypes.cmx matitaMathView.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaProof.cmi \ matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaProof.cmx \ matitaTypes.cmx -matitaProof.cmo: buildTimeConf.cmo matitaTypes.cmo matitaProof.cmi -matitaProof.cmx: buildTimeConf.cmx matitaTypes.cmx matitaProof.cmi +matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \ + matitaProof.cmi +matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ + matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmx: buildTimeConf.cmx matitaDisambiguator.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index faab87d29..eba88af12 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -15,6 +15,7 @@ CMOS = \ buildTimeConf.cmo \ matitaGeneratedGui.cmo \ matitaTypes.cmo \ + matitaCicMisc.cmo \ matitaGtkMisc.cmo \ matitaConsole.cmo \ matitaGui.cmo \ diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index cef844f0c..249058f8b 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -28,4 +28,5 @@ let version = "0.0.1";; let undo_history_size = 10;; let console_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; +let base_uri = "cic:/matita";; diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 2dab41008..466174ba3 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -93,7 +93,7 @@ - + True gtk-open 1 @@ -114,7 +114,7 @@ - + True gtk-save 1 @@ -134,7 +134,7 @@ True - + True gtk-save-as 1 @@ -161,7 +161,7 @@ - + True gtk-quit 1 @@ -220,6 +220,7 @@ Show Check Window True False + @@ -1227,7 +1228,9 @@ Copyright (C) 2004, - Check + 300 + 200 + Matita: check term GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE False @@ -1240,7 +1243,26 @@ Copyright (C) 2004, GDK_GRAVITY_NORTH_WEST - + + True + True + False + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index bf57dc8d9..fb163aa9c 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -70,40 +70,36 @@ let proof_viewer = MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) () let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = + let set_goal goal = + debug_print (sprintf "Setting goal %d" goal); + if not (has_proof ()) then assert false; + (get_proof ())#set_goal goal + in MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook - ~sequent_viewer () + ~sequent_viewer ~set_goal () let new_proof (proof: MatitaTypes.proof) = let xmldump_observer _ _ = print_endline proof#toString in - let proof_observer _ (status, (proof_metadata, _)) = + let proof_observer _ (status, ()) = debug_print "proof_observer"; - let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - proof_metadata - in let ((uri_opt, _, _, _), _) = status in let uri = MatitaTypes.unopt_uri uri_opt in debug_print "apply transformation"; - let mathml = - ApplyTransformation.mml_of_cic_object - ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types - in - if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml"; - proof_viewer#load_proof mathml proof_metadata; + proof_viewer#load_proof status; debug_print "/proof_observer" in - let sequents_observer _ ((proof, goal_opt), (_, sequents_metadata)) = + let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = sequents_viewer#reset; (match goal_opt with | None -> () | Some goal -> - sequents_viewer#load_sequents sequents_metadata; + sequents_viewer#load_sequents metasenv; sequents_viewer#goto_sequent goal) in ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - sequents_observer); + sequents_observer); ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - proof_observer); + proof_observer); ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events xmldump_observer); proof#notify; @@ -125,6 +121,7 @@ let abort_proof () = 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; diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 17a9268af..943f78ff8 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -36,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) method newMenu = newMenu - val image108 = + val image116 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image108" ~info:"GtkImage" xmldata)) - method image108 = image108 + (Glade.get_widget_msg ~name:"image116" ~info:"GtkImage" xmldata)) + method image116 = image116 val newMenu_menu = new GMenu.menu (GtkMenu.Menu.cast (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) @@ -56,26 +56,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) method openMenuItem = openMenuItem - val image109 = + val image117 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image109" ~info:"GtkImage" xmldata)) - method image109 = image109 + (Glade.get_widget_msg ~name:"image117" ~info:"GtkImage" xmldata)) + method image117 = image117 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image110 = + val image118 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image110" ~info:"GtkImage" xmldata)) - method image110 = image110 + (Glade.get_widget_msg ~name:"image118" ~info:"GtkImage" xmldata)) + method image118 = image118 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image111 = + val image119 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image111" ~info:"GtkImage" xmldata)) - method image111 = image111 + (Glade.get_widget_msg ~name:"image119" ~info:"GtkImage" xmldata)) + method image119 = image119 val separator1 = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) @@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) method quitMenuItem = quitMenuItem - val image112 = + val image120 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image112" ~info:"GtkImage" xmldata)) - method image112 = image112 + (Glade.get_widget_msg ~name:"image120" ~info:"GtkImage" xmldata)) + method image120 = image120 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -526,6 +526,17 @@ class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GWindow.window (GtkWindow.Window.cast (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata)) method checkWin = checkWin + val checkWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"CheckWinEventBox" ~info:"GtkEventBox" xmldata)) + method checkWinEventBox = checkWinEventBox + val scrolledCheck = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata)) + method scrolledCheck = scrolledCheck + method reparent parent = + checkWinEventBox#misc#reparent parent; + toplevel#destroy () method check_widgets () = () end diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 437d85a21..d67a27549 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -13,11 +13,11 @@ class mainWin : val fileMenu_menu : GMenu.menu val helpMenu : GMenu.menu_item val helpMenu_menu : GMenu.menu - val image108 : GMisc.image - val image109 : GMisc.image - val image110 : GMisc.image - val image111 : GMisc.image - val image112 : GMisc.image + val image116 : GMisc.image + val image117 : GMisc.image + val image118 : GMisc.image + val image119 : GMisc.image + val image120 : GMisc.image val mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned @@ -56,11 +56,11 @@ class mainWin : method fileMenu_menu : GMenu.menu method helpMenu : GMenu.menu_item method helpMenu_menu : GMenu.menu - method image108 : GMisc.image - method image109 : GMisc.image - method image110 : GMisc.image - method image111 : GMisc.image - method image112 : GMisc.image + method image116 : GMisc.image + method image117 : GMisc.image + method image118 : GMisc.image + method image119 : GMisc.image + method image120 : GMisc.image method mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned @@ -330,11 +330,16 @@ class checkWin : unit -> object val checkWin : GWindow.window + val checkWinEventBox : GBin.event_box + val scrolledCheck : GBin.scrolled_window val toplevel : GWindow.window val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method checkWin : GWindow.window + method checkWinEventBox : GBin.event_box method check_widgets : unit -> unit + method reparent : GObj.widget -> unit + method scrolledCheck : GBin.scrolled_window method toplevel : GWindow.window method xml : Glade.glade_xml Gtk.obj end diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 70a909a57..212e4e4d9 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -55,7 +55,8 @@ class gui file = let proof = new proofWin ~file () in let check = new checkWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) - [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ] + [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; + check#checkWinEventBox ] in let console = MatitaConsole.console ~evbox:main#consoleEventBox @@ -75,6 +76,8 @@ class gui file = List.iter (fun (key, callback) -> self#addKeyBinding key callback) [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; + GdkKeysyms._F4, + toggle_win ~check:main#showCheckMenuItem check#checkWin; ]; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 45332107f..3e505c28e 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -39,6 +39,9 @@ type state_tag = [ `Command | `Proof ] option exception Command_error of string +let uri name = + UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name) + let canonical_context metano metasenv = try let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in @@ -83,11 +86,10 @@ class virtual interpreterState ~(console: MatitaConsole.console) = method evalPhrase s = self#evalTactical (self#parsePhrase s) end -let check_widget: MatitaTypes.sequents_viewer lazy_t = lazy ( - let gui = MatitaGui.instance () in - let notebook = GPack.notebook ~show:true ~packing:gui#check#checkWin#add () in - let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () in - MatitaMathView.sequents_viewer ~notebook ~sequent_viewer ()) +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 @@ -106,18 +108,17 @@ class sharedState (* do nothing, just for compatibility with coq syntax *) Some `Command | TacticAst.Command (TacticAst.Check term) -> - let dummyno = 1023 in let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in let (context, metasenv) = get_context_and_metasenv proof_handler in - let sequent = (dummyno, context, term) in - let metadata = Cic2acic.asequent_of_sequent metasenv sequent in + let dummyno = CicMkImplicit.new_meta metasenv [] in + let ty = CicTypeChecker.type_of_aux' metasenv context term in + 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#reset; - widget#load_sequents [dummyno, metadata]; - widget#goto_sequent dummyno; + widget#load_sequent (sequent::metasenv) dummyno; None | tactical -> raise (Command_error (TacticAstPp.pp_tactical tactical)) @@ -136,9 +137,14 @@ class commandState method evalTactical = function | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical - | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) -> + | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) -> let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in - let proof = MatitaProof.proof ~typ:expr ~metasenv () in + let uri = + match name_opt with + | None -> None + | Some name -> Some (uri name) + in + let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in proof_handler.MatitaTypes.new_proof proof; Some `Proof | TacticAst.Command TacticAst.Quit -> @@ -194,8 +200,11 @@ class proofState | TacticAst.Transitivity term -> EqualityTactics.transitivity_tac (disambiguate term) | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term) + | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term) | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term) | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term) + | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *) + PrimitiveTactics.elim_intros_simpl_tac (disambiguate term) | TacticAst.ElimType term -> EliminationTactics.elim_type_tac (disambiguate term) | TacticAst.Replace (what, with_what) -> @@ -203,12 +212,10 @@ class proofState ~with_what:(disambiguate with_what) (* (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Absurd | TacticAst.Change of 'term * 'term * 'ident option | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option | TacticAst.Decompose of 'ident * 'ident list | TacticAst.Discriminate of 'ident - | TacticAst.Elim of 'term * 'term option | TacticAst.Fold of reduction_kind * 'term | TacticAst.Injection of 'ident | TacticAst.LetIn of 'term * 'ident @@ -234,6 +241,29 @@ class proofState | TacticAst.Command (TacticAst.Redo steps) -> (proof_handler.MatitaTypes.get_proof ())#redo ?steps (); Some `Proof + | TacticAst.Command (TacticAst.Qed name_opt) -> + (* 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 + (match name_opt with + | None -> () + | Some name -> proof#set_uri (uri name)); + let (uri, metasenv, bo, ty) = proof#proof in + let uri = MatitaTypes.unopt_uri uri in + if metasenv <> [] then failwith "Proof not completed"; + let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in + if not (CicReduction.are_convertible [] proved_ty ty) then + failwith "Wrong proof"; + (* TODO Zack [] probably wrong *) + CicEnvironment.add_type_checked_term uri + (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[])); + proof_handler.MatitaTypes.set_proof None; + (* TODO Zack a lot more to be done here: + * - save object to disk in xml format + * - collect metadata + * - register uri to the getter *) + Some `Command | TacticAst.Seq tacticals -> (* TODO Zack check for proof completed at each step? *) List.iter (fun t -> ignore (self#evalTactical t)) tacticals; diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 46733bf60..4dc34cfa1 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -23,17 +23,9 @@ * http://cs.unibo.it/helm/. *) -(***************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* 29/01/2003 Claudio Sacerdoti Coen *) -(* *) -(* *) -(***************************************************************************) - open Printf +open MatitaCicMisc open MatitaTypes (* List utility functions *) @@ -52,7 +44,38 @@ let list_map_fail f = in aux -(* End of the list utility functions *) +class proof_viewer obj = + object(self) + + inherit GMathViewAux.single_selection_math_view obj + +(* initializer self#set_log_verbosity 3 *) + + val mutable current_infos = None + val mutable current_mathml = None + + method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = + let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = + Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses); + let mathml = + ApplyTransformation.mml_of_cic_object ~explode_all:true + (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types + in + match current_mathml with + | None -> + debug_print "no previous MathML"; + self#load_root ~root:mathml#get_documentElement ; + current_mathml <- Some mathml + | Some current_mathml -> + debug_print "Previous MathML available: xmldiffing ..."; + self#freeze ; + XmlDiff.update_dom ~from:current_mathml mathml ; + self#thaw + end class sequent_viewer obj = object(self) @@ -101,107 +124,78 @@ class sequent_viewer obj = | None -> assert false (* "ERROR: No current term!!!" *) ) selections - method load_sequent (mml:Gdome.document) - (metadata:MatitaTypes.sequents_metadata) sequent_no - = + method load_sequent metasenv metano = +(* let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_hypotheses) - = - try - List.assoc sequent_no metadata - with Not_found -> assert false + ids_to_hypotheses) = + Cic2acic.asequent_of_sequent metasenv conjecture + in +*) + let sequent = CicUtil.lookup_meta metano metasenv in + let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses)) = + ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); - self#load_root ~root:mml#get_documentElement + debug_print "load_sequent: dumping MathML to /tmp/prova"; + ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ()); + self#load_root ~root:mathml#get_documentElement end -class proof_viewer obj = - object(self) - - inherit GMathViewAux.single_selection_math_view obj - -(* initializer self#set_log_verbosity 3 *) - - val mutable current_infos = None - val mutable current_mml = None - - method load_proof (mml:Gdome.document) (metadata:MatitaTypes.proof_metadata) = - let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - metadata - in - current_infos <- - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses); - match current_mml with - | None -> - MatitaTypes.debug_print "no previous MathML"; - self#load_root ~root:mml#get_documentElement ; - current_mml <- Some mml - | Some current_mml' -> - MatitaTypes.debug_print "Previous MathML available: xmldiffing ..."; - self#freeze ; - XmlDiff.update_dom ~from:current_mml' mml ; - self#thaw - end class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) () + ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () = object (self) val mutable pages = 0 val mutable switch_page_callback = None - val mutable mathmls = [] - val mutable metadata = None val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) + val mutable _metasenv = [] method reset = for i = 1 to pages do notebook#remove_page 0 done; pages <- 0; - mathmls <- []; - metadata <- None; page2goal <- []; goal2page <- []; + _metasenv <- []; (match switch_page_callback with | Some id -> GtkSignal.disconnect notebook#as_widget id; switch_page_callback <- None | None -> ()) - method load_sequents (metadata': MatitaTypes.sequents_metadata) = - metadata <- Some metadata'; - let sequents = metadata' in - let sequents_no = List.length sequents in + method load_sequents metasenv = + let sequents_no = List.length metasenv in + _metasenv <- metasenv; debug_print (sprintf "sequents no: %d" sequents_no); pages <- sequents_no; let widget = sequent_viewer#coerce in let page = ref 0 in List.iter - (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) -> + (fun (metano, _, _) -> page2goal <- (!page, metano) :: page2goal; goal2page <- (metano, !page) :: goal2page; + incr page; let tab_label = (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce in - notebook#append_page ~tab_label widget; - let mathml = lazy - (let content_sequent = Cic2content.map_sequent asequent in - let pres_sequent = - Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent - in - let xmlpres = Box.document_of_box pres_sequent in - Xml2Gdome.document_of_xml Misc.domImpl xmlpres) - in - mathmls <- (metano, mathml) :: mathmls) - sequents; - mathmls <- List.rev mathmls; + notebook#append_page ~tab_label widget) + metasenv; switch_page_callback <- (* TODO Zack the "#after" may probably be removed after Luca's fix for * widget not loading documents before being realized *) Some (notebook#connect#after#switch_page ~callback:(fun page -> debug_print "switch_page callback"; - self#render_page page)) + let goal = + try + List.assoc page page2goal + with Not_found -> assert false + in + set_goal goal; + self#render_page goal)) + + method private render_page goal = + sequent_viewer#load_sequent _metasenv goal method goto_sequent goal = let page = @@ -210,14 +204,7 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page page - - method private render_page page = - let metadata = - match metadata with Some metadata -> metadata | None -> assert false - in - let (metano, mathml) = List.nth mathmls page in - sequent_viewer#load_sequent (Lazy.force mathml) metadata metano + self#render_page goal end @@ -240,7 +227,7 @@ let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = [] let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) () + ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () = - new sequents_viewer ~notebook ~sequent_viewer () + new sequents_viewer ~notebook ~sequent_viewer ~set_goal () diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 0ed1a4573..b0ceda45c 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -50,6 +50,7 @@ val sequent_viewer: val sequents_viewer: notebook:GPack.notebook -> sequent_viewer:MatitaTypes.sequent_viewer -> + set_goal:(int -> unit) -> unit -> MatitaTypes.sequents_viewer diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index a6f2988d3..ca1b4c907 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -23,16 +23,16 @@ * http://helm.cs.unibo.it/ *) - (** create a Cic.CurrentProof from a given proof *) -let currentProof (uri, metasenv, bo, ty) = - let uri = MatitaTypes.unopt_uri uri in - (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) +open MatitaCicMisc +let init_metadata _ = () +let compute_metadata _ _ = () + +(* let init_metadata status = let ((_, metasenv, _, _) as proof, _) = status in let proof_object_metadata = (* compute proof annotations *) - Cic2acic.acic_object_of_cic_object (currentProof proof) + Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) in let sequents_metadata = (* compute all sequent annotations from scratch *) List.map @@ -43,9 +43,14 @@ let init_metadata status = (proof_object_metadata, sequents_metadata) let compute_metadata (old_status, old_metadata) new_status = - let ((_, new_metasenv, _, _) as new_proof, _) = new_status in + let ((_, new_metasenv, _, _) as new_proof, goal_opt) = new_status in let proof_object_metadata = (* compute proof annotations *) - Cic2acic.acic_object_of_cic_object (currentProof new_proof) + let obj = + match goal_opt with + | Some _ -> cicCurrentProof new_proof + | None -> cicConstant new_proof + in + Cic2acic.acic_object_of_cic_object obj in let sequents_metadata = (* compute all sequent annotations from scratch *) (** TODO Zack could we reuse some of the annotations from the previous @@ -57,17 +62,18 @@ let compute_metadata (old_status, old_metadata) new_status = new_metasenv in (proof_object_metadata, sequents_metadata) +*) class proof ?uri ~typ ~metasenv ~body () = object (self) - inherit [MatitaTypes.hist_metadata] + inherit [unit] StatefulProofEngine.status ~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv init_metadata compute_metadata () method toXml = - let currentproof = currentProof self#proof in + let currentproof = cicCurrentProof self#proof in let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof in diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index ec02348f7..86e77e7e8 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -77,6 +77,7 @@ class type disambiguator = (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end +(* type sequents_metadata = (int * (** sequent (meta) index *) (Cic.annconjecture * (** annotated conjecture *) @@ -94,10 +95,11 @@ type proof_metadata = (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 [hist_metadata] StatefulProofEngine.status + inherit [unit] StatefulProofEngine.status (** return a pair of "xml" (as defined in Xml module) representing the * * current proof type and body, respectively *) @@ -107,6 +109,7 @@ class type proof = 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 @@ -124,7 +127,7 @@ class type interpreter = (** {2 MathML widgets} *) type mml_of_cic_sequent = - Cic.metasenv -> int * Cic.context * Cic.term -> + Cic.metasenv -> Cic.conjecture -> Gdome.document * ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t * @@ -139,7 +142,7 @@ class type proof_viewer = object inherit GMathViewAux.single_selection_math_view - method load_proof: Gdome.document -> proof_metadata -> unit + method load_proof: StatefulProofEngine.proof_status -> unit end class type sequent_viewer = @@ -155,13 +158,13 @@ class type sequent_viewer = method get_selected_hypotheses: Cic.hypothesis list (** load a sequent and render it into parent widget *) - method load_sequent: Gdome.document -> sequents_metadata -> int -> unit + method load_sequent: Cic.metasenv -> int -> unit end class type sequents_viewer = object method reset: unit - method load_sequents: sequents_metadata -> unit + method load_sequents: Cic.metasenv -> unit method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end -- 2.39.2