1 files changed, 209 insertions, 0 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
new file mode 100644
index 00000000..042ee5c8
--- /dev/null
+++ b/toplevel/whelp.ml4
@@ -0,0 +1,209 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: whelp.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
+
+open Options
+open Pp
+open Util
+open System
+open Names
+open Term
+open Environ
+open Rawterm
+open Libnames
+open Nametab
+open Termops
+open Detyping
+open Constrintern
+open Dischargedhypsmap
+open Command
+open Pfedit
+open Refiner
+open Tacmach
+
+(* Coq interface to the Whelp query engine developed at 
+   the University of Bologna *)
+
+let make_whelp_request req c =
+  "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+
+let b = Buffer.create 16
+
+let url_char c =
+  if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or 
+     '0' <= c & c <= '9' or 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 (string_of_id 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 Idset.empty ref in
+  error ("Definitions of the current session not supported in Whelp: " ^ string_of_qualid qid)
+
+let uri_of_repr_kn ref (mp,dir,l) = 
+  match mp with
+    | MPfile sl ->
+        uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath 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_rawsort = function
+  | RProp Null -> "Prop"
+  | RProp Pos -> "Set"
+  | RType _ -> "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: "^(string_of_id id))
+  | ConstRef cst ->
+      uri_of_repr_kn ref (repr_con cst); url_string ".con"
+  | IndRef (kn,i) -> 
+      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1]
+  | ConstructRef ((kn,i),j) ->
+      uri_of_repr_kn ref (repr_kn 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
+  | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+      get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
+  | RRef (_,(ConstRef cst as ref)) ->
+      get_discharged_hyp_names (sp_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
+  | RVar (_,id) -> url_id id
+  | RRef (_,ref) ->  uri_of_global ref
+  | RHole _ | REvar _ -> url_string "?"
+  | RSort (_,s) -> url_string (whelp_of_rawsort s)
+  | _ -> url_paren (fun () -> match c with
+  | RApp (_,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
+  | RLambda (_,na,ty,c) ->
+      url_string "\\lambda "; url_of_name na; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
+  | RProd (_,Anonymous,ty,c) ->
+      uri_of_constr ty; url_string "\\to "; uri_of_constr c
+  | RProd (_,Name id,ty,c) ->
+      url_string "\\forall "; url_id id; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
+  | RLetIn (_,na,b,c) ->
+      url_string "let "; url_of_name na; url_string "\\def ";
+      uri_of_constr b; url_string " in "; uri_of_constr c
+  | RCast (_,c,_,t) ->
+      uri_of_constr c; url_string ":"; uri_of_constr t
+  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+      error "Whelp does not support pattern-matching and (co-)fixpoint"
+  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+      anomaly "Written w/o parenthesis"
+  | RPatVar _ | RDynamic _ -> 
+      anomaly "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 = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in
+  let _ = run_command (fun x -> x) print_string command in ()
+
+let whelp_constr req c =
+  let c = detype false [whelm_special] [] c in
+  send_whelp req (make_string uri_of_constr c)
+
+let whelp_constr_expr req c =
+  let (sigma,env)= get_current_context () in
+  let _,c = interp_open_constr sigma env c in
+  whelp_constr 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 locate_inductive r =
+  let (loc,qid) = qualid_of_reference r in
+  try match Syntax_def.locate_global qid with
+    | IndRef ind -> ind
+    | _ -> user_err_loc (loc,"",str "Inductive type expected")
+  with Not_found -> error_global_not_found_loc loc qid
+
+let on_goal f =
+  let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
+  f (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 s c
+
+VERNAC ARGUMENT EXTEND whelp_constr_request
+| [ "Match" ] -> [ "match" ]
+| [ "Instance" ] -> [ "instance" ]
+END
+
+VERNAC COMMAND EXTEND Whelp
+| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
+| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] 
+| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
+END
+
+VERNAC COMMAND EXTEND WhelpHint
+| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] 
+| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] 
+END