From 99b249b23524cda2d91602ee088fef1a7be253ee Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 16:02:51 +0000 Subject: [PATCH] added contextual menu to act over selected terms work in progress: still bugged wrt the locked mark of matitaScript --- helm/matita/dump_moo.ml | 3 +- helm/matita/matita.ml | 7 +- helm/matita/matitaGui.ml | 33 ++-- helm/matita/matitaGuiTypes.mli | 2 + helm/matita/matitaMathView.ml | 278 ++++++++++++++++++--------------- helm/matita/matitaScript.ml | 18 ++- helm/matita/matitacLib.ml | 8 +- 7 files changed, 197 insertions(+), 152 deletions(-) diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml index 17f24fc0a..25b98f424 100644 --- a/helm/matita/dump_moo.ml +++ b/helm/matita/dump_moo.ml @@ -48,7 +48,8 @@ let _ = let commands = GrafiteMarshal.load_moo ~fname in List.iter (fun cmd -> - printf " %s\n" (GrafiteAstPp.pp_cic_command cmd); flush stdout) + printf " %s\n%!" + (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) cmd)) commands; end) (List.rev !moos) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 1f49c1ac5..0086f6aea 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -139,8 +139,11 @@ let _ = addDebugItem "dump moo to stderr" (fun _ -> let status = (MatitaScript.current ())#status in let moo = status.moo_content_rev in - List.iter (fun cmd -> prerr_endline - (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo)); + List.iter + (fun cmd -> + prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) + cmd)) + (List.rev moo)); addDebugItem "print metasenv goals and stack to stderr" (fun _ -> prerr_endline ("metasenv goals: " ^ String.concat " " diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5aa3d59e9..16712c454 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -548,14 +548,18 @@ class gui () = let tac ast _ = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance - ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) + ~statement:("\n" + ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast))) () in let tac_w_term ast _ = if (MatitaScript.current ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" ^ GrafiteAstPp.pp_tactic ast) + ("\n" + ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ast) in let tbar = main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); @@ -823,24 +827,23 @@ class gui () = (** selections / clipboards handling *) - method private markup_selected = MatitaMathView.has_selection () - method private text_selected = + method markupSelected = MatitaMathView.has_selection () + method private textSelected = (source_buffer#get_iter_at_mark `INSERT)#compare (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 - method private something_selected = - self#markup_selected || self#text_selected - method private markup_stored = MatitaMathView.has_clipboard () - method private text_stored = clipboard#text <> None - method private something_stored = self#markup_stored || self#text_stored + method private somethingSelected = self#markupSelected || self#textSelected + method private markupStored = MatitaMathView.has_clipboard () + method private textStored = clipboard#text <> None + method private somethingStored = self#markupStored || self#textStored - method canCopy = self#something_selected - method canCut = self#text_selected - method canDelete = self#text_selected - method canPaste = self#something_stored - method canPastePattern = self#markup_stored + method canCopy = self#somethingSelected + method canCut = self#textSelected + method canDelete = self#textSelected + method canPaste = self#somethingStored + method canPastePattern = self#markupStored method copy () = - if self#text_selected + if self#textSelected then begin MatitaMathView.empty_clipboard (); source_view#buffer#copy_clipboard clipboard; diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index c68bbc28e..1b9d17cad 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -74,6 +74,8 @@ object method canPaste: bool method canPastePattern: bool + method markupSelected: bool + method copy: unit -> unit method cut: unit -> unit method delete: unit -> unit diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 0feab6121..a7299879a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -137,8 +137,24 @@ let string_of_dom_node node = text#get_data#to_string with GdomeInit.DOMCastException _ -> "") +let name_of_hypothesis = function + | Some (Cic.Name s, _) -> s + | _ -> assert false + +let id_of_node (node: Gdome.element) = + let xref_attr = + node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds in + try + List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) + with Failure _ -> assert false + +type selected_term = + | SelTerm of Cic.term * string option (* term, parent hypothesis (if any) *) + | SelHyp of string * Cic.context (* hypothesis, context *) + class clickableMathView obj = let text_width = 80 in +let dummy_loc = DisambiguateTypes.dummy_floc in object (self) inherit GMathViewAux.multi_selection_math_view obj @@ -162,18 +178,21 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = + let text = + match ctxt#target with + | "PATTERN" -> self#text_of_selection `Pattern + | "TERM" | _ -> self#text_of_selection `Term + in + match text with + | None -> () + | Some s -> ctxt#return s + + method private text_of_selection fmt = match self#get_selections with - | [] -> () - | node :: _ -> -(* eprintf "getting selection with target %s\n%!" ctxt#target; *) - (match ctxt#target with - | "PATTERN" -> - ctxt#return (self#string_of_node ~paste_kind:`Pattern node) - | "TERM" | _ -> - ctxt#return (self#string_of_node ~paste_kind:`Term node)) + | [] -> None + | node :: _ -> Some (self#string_of_node ~paste_kind:fmt node) method private selection_clear_cb sel_event = -(* eprintf "selection clear\n%!"; *) self#remove_selections; (GData.clipboard Gdk.Atom.clipboard)#clear (); false @@ -188,16 +207,56 @@ object (self) self#popup_contextual_menu (GdkEvent.Button.time gdk_button); false + (** @return a pattern structure which contains pretty printed terms *) + method private tactic_text_pattern_of_selection = + match self#get_selections with + | [] -> assert false (* this method is invoked only if there's a sel. *) + | node :: _ -> + let id = id_of_node node in + let cic_info, unsh_sequent = self#get_cic_info id in + match self#get_term_by_id cic_info id with + | SelTerm (t, father_hyp) -> + let sequent = self#sequent_of_id ~paste_kind:`Pattern id in + let text = self#string_of_cic_sequent sequent in + (match father_hyp with + | None -> None, [], Some text + | Some hyp_name -> None, [ hyp_name, text ], None) + | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None + method private popup_contextual_menu time = - let clipboard = GData.clipboard Gdk.Atom.clipboard in let menu = GMenu.menu () in - let copy_menu_item = - GMenu.image_menu_item - ~label:"_Copy" ~stock:`COPY ~packing:menu#append () - in + let add_menu_item ?(menu = menu) ?stock ?label () = + GMenu.image_menu_item ?stock ?label ~packing:menu#append () in + let check = add_menu_item ~label:"Check" () in + let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in + menu#append reductions_menu_item; + let reductions = GMenu.menu () in + reductions_menu_item#set_submenu reductions; + let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in + let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in + let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in + let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in + menu#append (GMenu.separator_item ()); + let copy = add_menu_item ~stock:`COPY () in let gui = get_gui () in - copy_menu_item#misc#set_sensitive gui#canCopy; - connect_menu_item copy_menu_item gui#copy; + List.iter (fun item -> item#misc#set_sensitive gui#canCopy) + [ copy; check; normalize; reduce; simplify; whd ]; + let reduction_action kind () = + let pat = self#tactic_text_pattern_of_selection in + let statement = + let loc = DisambiguateTypes.dummy_floc in + GrafiteAstPp.pp_executable ~term_pp:(fun s -> s) + ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) + (GrafiteAst.Tactical (loc, + GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)), + Some (GrafiteAst.Semicolon loc))) in + HLog.debug ("soon I'll evaluate: " ^ statement); + (MatitaScript.current ())#advance ~statement () in + connect_menu_item copy gui#copy; + connect_menu_item normalize (reduction_action `Normalize); + connect_menu_item reduce (reduction_action `Reduce); + connect_menu_item simplify (reduction_action `Simpl); + connect_menu_item whd (reduction_action `Whd); menu#popup ~button:right_button ~time method private button_release_cb gdk_button = @@ -240,8 +299,7 @@ object (self) List.iter (fun uri -> let menu_item = - GMenu.menu_item ~label:uri ~packing:menu#append () - in + GMenu.menu_item ~label:uri ~packing:menu#append () in connect_menu_item menu_item (fun () -> f uri)) uris; menu#popup ~button ~time) @@ -275,20 +333,36 @@ object (self) method update_font_size = self#set_font_size !current_font_size + (** find a term by id from stored CIC infos @return either `Hyp if the id + * correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a + * term. In the latter case hyp is either None (if the term is a subterm of + * the sequent conclusion) or Some hyp_name if the term belongs to an + * hypothesis *) method private get_term_by_id cic_info id = - let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + let unsh_item, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, _, _ = + cic_info in + let rec find_father_hyp id = + if Hashtbl.mem ids_to_hypotheses id + then Some (name_of_hypothesis (Hashtbl.find ids_to_hypotheses id)) + else + let father_id = + try Hashtbl.find ids_to_father_ids id + with Not_found -> assert false in + match father_id with + | Some id -> find_father_hyp id + | None -> None + in try - `Term (Hashtbl.find ids_to_terms id) + let term = Hashtbl.find ids_to_terms id in + let father_hyp = find_father_hyp id in + SelTerm (term, father_hyp) with Not_found -> try let hyp = Hashtbl.find ids_to_hypotheses id in let _, context, _ = - match unsh_item with - | Some seq -> seq - | None -> assert false - in + match unsh_item with Some seq -> seq | None -> assert false in let context' = MatitaMisc.list_tl_at hyp context in - `Hyp context' + SelHyp (name_of_hypothesis hyp, context') with Not_found -> assert false method private find_obj_conclusion id = @@ -303,94 +377,65 @@ object (self) method private string_of_node ~(paste_kind:paste_kind) node = if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds - then self#string_of_id_node ~paste_kind node + then + let id = id_of_node node in + self#string_of_cic_sequent (self#sequent_of_id ~paste_kind id) else string_of_dom_node node - method private string_of_id_node ~(paste_kind:paste_kind) node = - let get_id (node: Gdome.element) = - let xref_attr = - node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds - in - List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) - in - let id = get_id node in + method private string_of_cic_sequent cic_sequent = let script = MatitaScript.current () in let metasenv = - if script#onGoingProof () then - script#proofMetasenv - else - [] - in - let string_of_cic_sequent cic_sequent = - let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = - Cic2acic.asequent_of_sequent metasenv cic_sequent - in - let _, _, _, annterm = acic_sequent in - let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm - in - let pped_ast = TermContentPres.pp_ast ast in - let markup = CicNotationPres.render ids_to_uris pped_ast in - BoxPp.render_to_string text_width markup - in - let cic_info, unsh_sequent = - match self#cic_info with - | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> - info, unsh_sequent - | Some ((None, _, _, _, _, _) as info) -> - (* building a dummy sequent for obj *) - let t = self#find_obj_conclusion id in -(* HLog.debug (CicPp.ppterm t); *) - info, (~-1, [], t) - | None -> assert false - in - let paste_as_pattern_sequent term unsh_sequent = - match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with - | [context, _] -> - (let context_len = List.length context in - let _, unsh_context, conclusion = unsh_sequent in - try - (match - List.nth unsh_context (List.length unsh_context - context_len - 1) - with - | None -> assert false (* can't select a restricted hyp *) - | Some (name, Cic.Decl ty) -> - let pattern = - ProofEngineHelpers.pattern_of ~term:ty [term] - in -(* HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern); *) - ~-1, [], pattern - | Some (name, Cic.Def (bo, _)) -> - let pattern = - ProofEngineHelpers.pattern_of ~term:bo [term] - in -(* HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern); *) - ~-1, [], pattern) - with Failure _ | Invalid_argument _ -> - let pattern = - ProofEngineHelpers.pattern_of ~term:conclusion [term] - in -(* HLog.debug ("\\vdash " ^ CicPp.ppterm pattern); *) - ~-1, [], pattern) - | _ -> assert false (* since it uses physical equality *) - in - let paste_as_term_sequent term unsh_sequent = - let context' = - match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with - | [context,_] -> context - | _ -> assert false (* since it uses physical equality *) - in - ~-1, context', term - in + if script#onGoingProof () then script#proofMetasenv else [] in + let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = + Cic2acic.asequent_of_sequent metasenv cic_sequent in + let _, _, _, annterm = acic_sequent in + let ast, ids_to_uris = + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in + let pped_ast = TermContentPres.pp_ast ast in + let markup = CicNotationPres.render ids_to_uris pped_ast in + BoxPp.render_to_string text_width markup + + method private pattern_of term context unsh_sequent = + let context_len = List.length context in + let _, unsh_context, conclusion = unsh_sequent in + try + (match + List.nth unsh_context (List.length unsh_context - context_len - 1) + with + | None -> assert false (* can't select a restricted hypothesis *) + | Some (name, Cic.Decl ty) -> + ProofEngineHelpers.pattern_of ~term:ty [term] + | Some (name, Cic.Def (bo, _)) -> + ProofEngineHelpers.pattern_of ~term:bo [term]) + with Failure _ | Invalid_argument _ -> + ProofEngineHelpers.pattern_of ~term:conclusion [term] + + method private get_cic_info id = + match self#cic_info with + | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> info, unsh_sequent + | Some ((None, _, _, _, _, _) as info) -> + let t = self#find_obj_conclusion id in + info, (~-1, [], t) (* dummy sequent for obj *) + | None -> assert false + + method private sequent_of_id ~(paste_kind:paste_kind) id = + let cic_info, unsh_sequent = self#get_cic_info id in let cic_sequent = match self#get_term_by_id cic_info id with - | `Term t -> - (match paste_kind with - | `Term -> paste_as_term_sequent t unsh_sequent - | `Pattern -> paste_as_pattern_sequent t unsh_sequent) - | `Hyp context -> ~-1, context, Cic.Rel 1 - in - string_of_cic_sequent cic_sequent + | SelTerm (t, _father_hyp) -> + let occurrences = + ProofEngineHelpers.locate_in_conjecture t unsh_sequent in + (match occurrences with + | [ context, _t ] -> + (match paste_kind with + | `Term -> ~-1, context, t + | `Pattern -> ~-1, [], self#pattern_of t context unsh_sequent) + | _ -> + HLog.error (sprintf "found %d occurrences while 1 was expected" + (List.length occurrences)); + assert false) (* since it uses physical equality *) + | SelHyp (_name, context) -> ~-1, context, Cic.Rel 1 in + cic_sequent method private string_of_selection ~(paste_kind:paste_kind) = match self#get_selections with @@ -853,7 +898,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadCheck term = failwith "not implemented _loadCheck"; - self#_showMath +(* self#_showMath *) method private egg () = win#mathOrListNotebook#goto_page 2; @@ -1055,20 +1100,3 @@ let paste_clipboard paste_kind = | Some cb -> (try List.assoc paste_kind cb with Not_found -> assert false) -(* let get_selections () = - if (MatitaScript.current ())#onGoingProof () then - let rec aux = - function - | [] -> None - | mv :: tl -> - (match mv#string_of_selections with - | [] -> aux tl - | sels -> Some sels) - in - aux (get_math_views ()) - else - None - -let reset_selections () = - List.iter (fun mv -> mv#remove_selections) (get_math_views ()) *) - diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c14bd7710..a545b65d4 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -229,6 +229,10 @@ let disambiguate_macro_term term status user_goal = match interps with | [_,_,x,_], _ -> x | _ -> assert false + +let pp_eager_statement_ast = + GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in @@ -239,6 +243,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in let dbd = LibraryDb.instance () in + (* XXX use a real CIC -> string pretty printer *) + let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> @@ -254,12 +260,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | TA.WInstance (loc, term) -> let term = disambiguate_macro_term term status user_goal in let l = Whelp.instance ~dbd term in - let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in + let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WLocate (loc, s) -> let l = Whelp.locate ~dbd s in - let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in + let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WElim (loc, term) -> @@ -270,14 +276,14 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | _ -> failwith "Not a MutInd" in let l = Whelp.elim ~dbd uri in - let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in + let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WHint (loc, term) -> let term = disambiguate_macro_term term status user_goal in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in - let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in + let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length (* REAL macro *) @@ -303,9 +309,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = ~disambiguate_command:GrafiteDisambiguate.disambiguate_command status ast in let extra_text = - comment parsed_text ^ - "\n" ^ TAPp.pp_statement ast - in + comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in [ new_status , (extra_text, ast) ], parsed_text_length | _ -> HLog.error diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 1f9dad80f..07d58b395 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -27,6 +27,10 @@ open Printf open GrafiteTypes +let pp_ast_statement = + GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj + (** {2 Initialization} *) let status = ref None @@ -44,9 +48,9 @@ let run_script is eval_function = else (fun status stm -> (* dump_status status; *) - let stm = GrafiteAstPp.pp_statement stm in + let stm = pp_ast_statement stm in let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = + let stm = if String.length stm > 50 then String.sub stm 0 50 ^ " ..." else -- 2.39.2