diff options
| -rw-r--r-- | _tags | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 81 | ||||
| -rw-r--r-- | ide/MacOS/default_accel_map | 1 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 1 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 1 | ||||
| -rw-r--r-- | toplevel/whelp.ml4 | 224 | ||||
| -rw-r--r-- | toplevel/whelp.mli | 20 |
9 files changed, 1 insertions, 334 deletions
@@ -24,8 +24,6 @@ ## tags for camlp4 files -"toplevel/whelp.ml4": use_grammar - "parsing/g_constr.ml4": use_compat5 "parsing/g_ltac.ml4": use_compat5 "parsing/g_prim.ml4": use_compat5 @@ -74,4 +72,4 @@ "tools/coqdoc": include "toplevel": include -<plugins/**>: include
\ No newline at end of file +<plugins/**>: include diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 4547c7fd89..32f94abf7a 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -490,87 +490,6 @@ Locate I.Dont.Exist. \SeeAlso Section \ref{LocateSymbol} -\subsection{The {\sc Whelp} searching tool -\label{Whelp}} - -{\sc Whelp} is an experimental searching and browsing tool for the whole {\Coq} -library and the whole set of {\Coq} user contributions. {\sc Whelp} requires a -browser to work. {\sc Whelp} has been developed at the University of Bologna as -part of the HELM\footnote{Hypertextual Electronic Library of Mathematics} and -MoWGLI\footnote{Mathematics on the Web, Get it by Logics and Interfaces} -projects. It can be invoked directly from the {\Coq} toplevel or from -{\CoqIDE}, assuming a graphical environment is also running. The browser to use -can be selected by setting the environment variable {\tt COQREMOTEBROWSER}. If -not explicitly set, it defaults to -\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"! or -\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the underlying -operating system (in the command, the string \verb!%s! serves as metavariable -for the url to open). The Whelp tool relies on a dedicated Whelp server and on -another server called Getter that retrieves formal documents. The default Whelp -server name can be obtained using the command {\tt Test Whelp Server} and the -default Getter can be obtained using the command: {\tt Test Whelp Getter}. The -Whelp server name can be changed using the command: - -\smallskip -\noindent {\tt Set Whelp Server {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}). -\optindex{Whelp Server} -\smallskip - -\noindent The Getter can be changed using the command: -\smallskip - -\noindent {\tt Set Whelp Getter {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}). -\optindex{Whelp Getter} - -\bigskip - -The {\sc Whelp} commands are: - -\subsubsection{\tt Whelp Locate "{\sl reg\_expr}". -\comindex{Whelp Locate}} - -This command opens a browser window and displays the result of seeking -for all names that match the regular expression {\sl reg\_expr} in the -{\Coq} library and user contributions. The regular expression can -contain the special operators are * and ? that respectively stand for -an arbitrary substring and for exactly one character. - -\variant {\tt Whelp Locate {\ident}.}\\ -This is equivalent to {\tt Whelp Locate "{\ident}"}. - -\subsubsection{\tt Whelp Match {\pattern}. -\comindex{Whelp Match}} - -This command opens a browser window and displays the result of seeking -for all statements that match the pattern {\pattern}. Holes in the -pattern are represented by the wildcard character ``\_''. - -\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}} - -This command opens a browser window and displays the result of seeking -for all statements that are instances of the pattern {\pattern}. The -pattern is here assumed to be an universally quantified expression. - -\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}} - -This command opens a browser window and displays the result of seeking -for all statements that have the ``form'' of an elimination scheme -over the type denoted by {\qualid}. - -\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}} - -This command opens a browser window and displays the result of seeking -for all statements that can be instantiated so that to prove the -statement {\term}. - -\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint -{\sl goal}} where {\sl goal} is the current goal to prove. Notice that -{\Coq} does not send the local environment of definitions to the {\sc -Whelp} tool so that it only works on requests strictly based on, only, -definitions of the standard library and user contributions. - \section{Loading files} \Coq\ offers the possibility of loading different diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb124..47612cdf72 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "") -; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "") (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l") ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "") ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3") diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 995c45c5ae..37e38a5464 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,8 +228,6 @@ let state_preserving = [ "Test Printing Synth"; "Test Printing Wildcard"; - "Whelp Hint"; - "Whelp Locate"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index cb05363ddc..4564d620ea 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1171,7 +1171,6 @@ let build_ui () = qitem "About" (Some "<Ctrl><Shift>A"); qitem "Locate" (Some "<Ctrl><Shift>L"); qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); - qitem "Whelp Locate" None; ]; menu tools_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e78c..edfe28b261 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> - <menuitem action='Whelp Locate' /> </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d22524e5ca..bf0f305abd 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -13,7 +13,6 @@ Record Vernacinterp Mltop Vernacentries -Whelp Vernac Usage Coqloop diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 deleted file mode 100644 index daedc30f42..0000000000 --- a/toplevel/whelp.ml4 +++ /dev/null @@ -1,224 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "grammar/grammar.cma" i*) - -open Flags -open Pp -open Errors -open Names -open Term -open Glob_term -open Libnames -open Globnames -open Nametab -open Detyping -open Constrintern -open Dischargedhypsmap -open Pfedit -open Tacmach -open Misctypes - -(* Coq interface to the Whelp query engine developed at - the University of Bologna *) - -let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080" -let getter_server_name = ref "http://mowgli.cs.unibo.it:58081" - -open Goptions - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp server"; - optkey = ["Whelp";"Server"]; - optread = (fun () -> !whelp_server_name); - optwrite = (fun s -> whelp_server_name := s) } - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp getter"; - optkey = ["Whelp";"Getter"]; - optread = (fun () -> !getter_server_name); - optwrite = (fun s -> getter_server_name := s) } - - -let make_whelp_request req c = - !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req - -let b = Buffer.create 16 - -let url_char c = - if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' || - '0' <= c && c <= '9' || c ='.' - then Buffer.add_char b c - else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) - -let url_string s = String.iter url_char s - -let rec url_list_with_sep sep f = function - | [] -> () - | [a] -> f a - | a::l -> f a; url_string sep; url_list_with_sep sep f l - -let url_id id = url_string (Id.to_string id) - -let uri_of_dirpath dir = - url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir) - -let error_whelp_unknown_reference ref = - let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in - errorlabstrm "" - (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ - strbrk ", are not supported in Whelp.") - -let uri_of_repr_kn ref (mp,dir,l) = - match mp with - | MPfile sl -> - uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl) - | _ -> - error_whelp_unknown_reference ref - -let url_paren f l = url_char '('; f l; url_char ')' -let url_bracket f l = url_char '['; f l; url_char ']' - -let whelp_of_glob_sort = function - | GProp -> "Prop" - | GSet -> "Set" - | GType _ -> "Type" - -let uri_int n = Buffer.add_string b (string_of_int n) - -let uri_of_ind_pointer l = - url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l - -let uri_of_global ref = - match ref with - | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".") - | ConstRef cst -> - uri_of_repr_kn ref (repr_con cst); url_string ".con" - | IndRef (kn,i) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1] - | ConstructRef ((kn,i),j) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j] - -let whelm_special = Id.of_string "WHELM_ANON_VAR" - -let url_of_name = function - | Name id -> url_id id - | Anonymous -> url_id whelm_special (* No anon id in Whelp *) - -let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c - -let uri_params f = function - | [] -> () - | l -> url_string "\\subst"; - url_bracket (url_list_with_sep ";" (uri_of_binding f)) l - -let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) - -let section_parameters = function - | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) -> - get_discharged_hyp_names (path_of_global (IndRef(induri,0))) - | GRef (_,(ConstRef cst as ref),_) -> - get_discharged_hyp_names (path_of_global ref) - | _ -> [] - -let merge vl al = - let rec aux acc = function - | ([],l) | (_,([] as l)) -> List.rev acc, l - | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) - in aux [] (vl,al) - -let rec uri_of_constr c = - match c with - | GVar (_,id) -> url_id id - | GRef (_,ref,_) -> uri_of_global ref - | GHole _ | GEvar _ -> url_string "?" - | GSort (_,s) -> url_string (whelp_of_glob_sort s) - | GApp (_,f,args) -> - let inst,rest = merge (section_parameters f) args in - uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; - url_list_with_sep " " uri_of_constr rest - | GLambda (_,na,k,ty,c) -> - url_string "\\lambda "; url_of_name na; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GProd (_,Anonymous,k,ty,c) -> - uri_of_constr ty; url_string "\\to "; uri_of_constr c - | GProd (_,Name id,k,ty,c) -> - url_string "\\forall "; url_id id; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GLetIn (_,na,b,c) -> - url_string "let "; url_of_name na; url_string "\\def "; - uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, (CastConv t|CastVM t|CastNative t)) -> - uri_of_constr c; url_string ":"; uri_of_constr t - | GRec _ | GIf _ | GLetTuple _ | GCases _ -> - error "Whelp does not support pattern-matching and (co-)fixpoint." - | GCast (_,_, CastCoerce) -> - anomaly (Pp.str "Written w/o parenthesis") - | GPatVar _ -> - anomaly (Pp.str "Found constructors not supported in constr") - -let make_string f x = Buffer.reset b; f x; Buffer.contents b - -let send_whelp req s = - let url = make_whelp_request req s in - let command = Util.subst_command_placeholder browser_cmd_fmt url in - let _ = CUnix.run_command ~hook:print_string command in () - -let whelp_constr env sigma req c = - let c = detype false [whelm_special] env sigma c in - send_whelp req (make_string uri_of_constr c) - -let whelp_constr_expr req c = - let (sigma,env)= Lemmas.get_current_context () in - let _,c = interp_open_constr env sigma c in - whelp_constr env sigma req c - -let whelp_locate s = - send_whelp "locate" s - -let whelp_elim ind = - send_whelp "elim" (make_string uri_of_global (IndRef ind)) - -let on_goal f = - let gls = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { gls with Evd.it = List.hd gls.Evd.it } in - f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -let whelp = function - | Locate s -> whelp_locate s - | Elim ind -> whelp_elim ind - | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c - -VERNAC ARGUMENT EXTEND whelp_constr_request -| [ "Match" ] -> [ "match" ] -| [ "Instance" ] -> [ "instance" ] -END - -VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY -| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] -| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] -END - -VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY -| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] -> - [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ] -END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli deleted file mode 100644 index 62272c50ff..0000000000 --- a/toplevel/whelp.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Coq interface to the Whelp query engine developed at - the University of Bologna *) - -open Names -open Term - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -val whelp : whelp_request -> unit |