From d46411c038cccb932638fd9d131c5d858c80ac5e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 Oct 2010 14:35:36 +0000 Subject: [PATCH] =?utf8?q?-=20parser:=20"whelp=20...=C3=82"removed=20-=20i?= =?utf8?q?nterface:=20whelp=20bar=20removed=20-=20interface:=20whelp=20and?= =?utf8?q?=20dependency=20graphs=20removed?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- matita/components/grafite/grafiteAst.ml | 6 -- matita/components/grafite/grafiteAstPp.ml | 6 -- .../grafite_parser/grafiteDisambiguate.ml | 13 --- .../grafite_parser/grafiteParser.ml | 10 --- matita/matita/matita.glade | 67 --------------- matita/matita/matitaMathView.ml | 81 +----------------- matita/matita/matitaScript.ml | 83 +------------------ matita/matita/matitaTypes.ml | 15 ---- matita/matita/matitaTypes.mli | 3 - 9 files changed, 3 insertions(+), 281 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 9ea33c2de..5adc2e91b 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -184,12 +184,6 @@ type inline_param = IPPrefix of string (* undocumented *) | IPCR (* detect convertible rewriting *) type ('term,'lazy_term) macro = - (* Whelp's stuff *) - | WHint of loc * 'term - | WMatch of loc * 'term - | WInstance of loc * 'term - | WLocate of loc * string - | WElim of loc * 'term (* real macros *) | Eval of loc * 'lazy_term reduction * 'term | Check of loc * 'term diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 5f89df9d6..5ba1b649d 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -345,12 +345,6 @@ let pp_macro ~term_pp ~lazy_term_pp = in let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in function - (* Whelp *) - | WInstance (_, term) -> "whelp instance " ^ term_pp term - | WHint (_, t) -> "whelp hint " ^ term_pp t - | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\"" - | WElim (_, t) -> "whelp elim " ^ term_pp t - | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) | Eval (_, kind, term) -> Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term) diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index 7510c1cc5..cfb85d239 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -892,18 +892,6 @@ let disambiguate_macro let disambiguate_reduction_kind = disambiguate_reduction_kind text prefix_len lexicon_status_ref in match macro with - | GrafiteAst.WMatch (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.WMatch (loc,term) - | GrafiteAst.WInstance (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.WInstance (loc,term) - | GrafiteAst.WElim (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.WElim (loc,term) - | GrafiteAst.WHint (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.WHint (loc,term) | GrafiteAst.Check (loc,term) -> let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Check (loc,term) @@ -916,6 +904,5 @@ let disambiguate_macro disambiguate_auto_params disambiguate_term metasenv context params in metasenv, GrafiteAst.AutoInteractive (loc, params) | GrafiteAst.Hint _ - | GrafiteAst.WLocate _ | GrafiteAst.Inline _ as macro -> metasenv,macro diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 941bb2218..3a0edb7ac 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -730,16 +730,6 @@ EXTEND if rew = None then G.Hint (loc, false) else G.Hint (loc,true) | IDENT "auto"; params = auto_params -> G.AutoInteractive (loc,params) - | [ IDENT "whelp"; "match" ] ; t = term -> - G.WMatch (loc,t) - | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> - G.WInstance (loc,t) - | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> - G.WLocate (loc,id) - | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> - G.WElim (loc, t) - | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> - G.WHint (loc,t) ] ]; alias_spec: [ diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade index 5c343f0af..0934b8102 100644 --- a/matita/matita/matita.glade +++ b/matita/matita/matita.glade @@ -86,22 +86,6 @@ True - - - True - View the graph of objects on which the current one depends on - (Direct) Dependencies - True - - - - - True - View the graph of objects which depends on the current one - (Inverse) Dependencies - True - - True @@ -265,57 +249,6 @@ 1 - - - True - 3 - 6 - - - True - gtk-missing-image - - - False - - - - - True - True - * - - - 1 - - - - - True - - - True - - - - - - False - False - - - - - False - 2 - - - - - False - 2 - - True diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 3364b55f3..770d2a83a 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -1010,35 +1010,16 @@ type term_source = class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = - let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" in let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in - let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in - let whelp_query_RE = Pcre.regexp - "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" - in - let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in - let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in let gui = get_gui () in let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in - let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in - let combo,_ = GEdit.combo_box_text ~strings:queries () in - let activate_combo_query input q = - let q' = String.lowercase q in - let rec aux i = function - | [] -> failwith ("Whelp query '" ^ q ^ "' not found") - | h::_ when String.lowercase h = q' -> i - | _::tl -> aux (i+1) tl - in - win#queryInputText#set_text input; - combo#set_active (aux 0 queries); - in let searchText = GSourceView2.source_view ~auto_indent:false ~editable:false () in @@ -1062,15 +1043,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(win#entrySearch#connect#activate ~callback); ignore(win#buttonSearch#connect#clicked ~callback); in - let set_whelp_query txt = - let query, arg = - try - let q = Pcre.extract ~rex:whelp_query_RE txt in - q.(1), q.(3) - with Not_found -> failwith "Malformed Whelp query" - in - activate_combo_query arg query; - in let toplevel = win#toplevel in let mathView = cicMathView ~packing:win#scrolledBrowser#add () in let fail message = @@ -1151,25 +1123,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val dep_contextual_menu = GMenu.menu () initializer - activate_combo_query "" "locate"; - win#whelpBarComboVbox#add combo#coerce; - let start_query () = - let query = - try - String.lowercase (List.nth queries combo#active) - with Not_found -> assert false in - let input = win#queryInputText#text in - let statement = - if query = "locate" then - "whelp " ^ query ^ " \"" ^ input ^ "\"." - else - "whelp " ^ query ^ " (" ^ input ^ ")." - in - (MatitaScript.current ())#advance ~statement () - in - ignore(win#queryInputText#connect#activate ~callback:start_query); - ignore(combo#connect#changed ~callback:start_query); - win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png"); win#mathOrListNotebook#set_show_tabs false; win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; @@ -1208,14 +1161,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | button when button = right_button -> dep_contextual_menu#popup ~button ~time | _ -> ()); - connect_menu_item win#depGraphMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Metadata (`Deps (`Fwd, uri))) - | None -> ()); - connect_menu_item win#invDepGraphMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Metadata (`Deps (`Back, uri))) - | None -> ()); connect_menu_item win#browserCloseMenuItem (fun () -> let my_id = Oo.id self in cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; @@ -1262,8 +1207,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** @return None if no object uri can be built from the current entry *) method private currentCicUri = match current_entry with - | `Uri uri - | `Metadata (`Deps (_, uri)) -> Some uri + | `Uri uri -> Some uri | _ -> None val model = @@ -1348,15 +1292,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors - | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> - self#dependencies dir uri () | `Uri uri -> self#_loadUriManagerUri uri | `NRef nref -> self#_loadNReference nref - | `Univs uri -> self#_loadUnivs uri - | `Whelp (query, results) -> - set_whelp_query query; - self#_loadList (List.map (fun r -> "obj", - UriManager.string_of_uri r) results)); + | `Univs uri -> self#_loadUnivs uri); self#setEntry entry end) @@ -1557,14 +1495,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = - let parse_metadata s = - let subs = Pcre.extract ~rex:metadata_RE s in - let uri = UriManager.uri_of_string ("cic:/" ^ subs.(3)) in - match subs.(1), subs.(2) with - | "deps", "forward" -> `Deps (`Fwd, uri) - | "deps", "backward" -> `Deps (`Back, uri) - | _ -> assert false - in let txt = HExtlib.trim_blanks txt in (* (* ZACK: what the heck? *) let fix_uri txt = @@ -1572,17 +1502,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (UriManager.strip_xpointer (UriManager.uri_of_string txt)) in *) - if is_whelp txt then begin - set_whelp_query txt; - (MatitaScript.current ())#advance ~statement:(txt ^ ".") () - end else begin let entry = match txt with | txt when is_uri txt -> `Uri (UriManager.uri_of_string ((*fix_uri*) txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) - | txt when is_metadata txt -> `Metadata (parse_metadata txt) - | "hbugs:/tutors/" -> `HBugs `Tutors | txt -> (try MatitaTypes.entry_of_string txt @@ -1592,7 +1516,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_load entry; self#_historyAdd entry - end (** {2 methods accessing underlying GtkMathView} *) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 1e63cc3d1..552d4907a 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -433,90 +433,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in let dbd = LibraryDb.instance () in - let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in match mac with - (* WHELP's stuff *) - | TA.WMatch (loc, term) -> - let l = Whelp.match_term ~dbd term in - let entry = `Whelp (pp_macro [] [] mac, l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], "", parsed_text_length - | TA.WInstance (loc, term) -> - let l = Whelp.instance ~dbd term in - let entry = `Whelp (pp_macro [] [] mac, 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 (pp_macro [] [] mac, l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], "", parsed_text_length - | TA.WElim (loc, term) -> - let uri = - match term with - | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None - | _ -> failwith "Not a MutInd" - in - let l = Whelp.elim ~dbd uri in - let entry = `Whelp (pp_macro [] [] mac, l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], "", parsed_text_length - | TA.WHint (loc, term) -> - let _subst = [] in - let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in - let l = List.map fst (MQ.experimental_hint ~dbd s) in - let entry = `Whelp (pp_macro [] [] mac, l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], "", parsed_text_length (* REAL macro *) - | TA.Hint (loc, rewrite) -> - let user_goal' = - match user_goal with - Some n -> n - | None -> raise NoUnfinishedProof - in - let proof = GrafiteTypes.get_current_proof grafite_status in - let proof_status = proof,user_goal' in - if rewrite then - let l = MQ.equations_for_goal ~dbd proof_status in - let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in - let entry = - `Whelp (pp_macro [] [] (TA.WHint(loc, Cic.Implicit None)), l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], "", parsed_text_length - else - let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in - let selected = guistuff.urichooser l in - (match selected with - | [] -> [], "", parsed_text_length - | [uri] -> - let suri = UriManager.string_of_uri uri in - let ast loc = - TA.Executable (loc, (TA.Tactic (loc, - Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))), - TA.Dot loc))) in - let text = - comment parsed_text ^ "\n" ^ - pp_eager_statement_ast (ast HExtlib.dummy_floc) - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - in - let text_len = MatitaGtkMisc.utf8_string_length text in - let loc = HExtlib.floc_of_loc (0,text_len) in - let statement = `Ast (GrafiteParser.LSome (ast loc),text) in - let res,_,_parsed_text_len = - eval_statement include_paths buffer guistuff - grafite_status user_goal script statement - in - (* we need to replace all the parsed_text *) - res,"",String.length parsed_text - | _ -> - HLog.error - "The result of the urichooser should be only 1 uri, not:\n"; - List.iter ( - fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") - ) selected; - assert false) + | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false | TA.Eval (_, kind, term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in let context = diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index 30e64892c..e295b9c0f 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -48,11 +48,8 @@ type mathViewer_entry = | `Cic of Cic.term * Cic.metasenv | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string (* "directory" in cic uris namespace *) - | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) - | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri (* cic object uri *) | `NRef of NReference.reference (* cic object uri *) - | `Whelp of string * UriManager.uri list (* query and results *) | `Univs of UriManager.uri ] @@ -69,20 +66,8 @@ let string_of_entry = function | `Cic (_, _) -> "term:" | `NCic (_, _, _, _) -> "nterm:" | `Dir uri -> uri - | `HBugs `Tutors -> "hbugs:/tutors/" - | `Metadata meta -> - "metadata:/" ^ - (match meta with - | `Deps (dir, uri) -> - "deps/" ^ - let suri = - let suri = UriManager.string_of_uri uri in - let len = String.length suri in - String.sub suri 4 (len - 4) in (* strip "cic:" prefix *) - (match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri) | `Uri uri -> UriManager.string_of_uri uri | `NRef nref -> NReference.string_of_reference nref - | `Whelp (query, _) -> query | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri let entry_of_string = function diff --git a/matita/matita/matitaTypes.mli b/matita/matita/matitaTypes.mli index 6d672a123..ec3048f67 100644 --- a/matita/matita/matitaTypes.mli +++ b/matita/matita/matitaTypes.mli @@ -34,11 +34,8 @@ type mathViewer_entry = | `Cic of Cic.term * Cic.metasenv | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string - | `HBugs of [ `Tutors ] - | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] | `Uri of UriManager.uri | `NRef of NReference.reference - | `Whelp of string * UriManager.uri list | `Univs of UriManager.uri ] -- 2.39.2