← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to toplevel/whelp.ml4

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
toplevel/whelp.ml4
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i camlp4deps: "parsing/grammar.cma" i*)
 
10
 
 
11
(* $Id: whelp.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
 
12
 
 
13
open Flags
 
14
open Pp
 
15
open Util
 
16
open System
 
17
open Names
 
18
open Term
 
19
open Environ
 
20
open Rawterm
 
21
open Libnames
 
22
open Nametab
 
23
open Termops
 
24
open Detyping
 
25
open Constrintern
 
26
open Dischargedhypsmap
 
27
open Command
 
28
open Pfedit
 
29
open Refiner
 
30
open Tacmach
 
31
open Syntax_def
 
32
 
 
33
(* Coq interface to the Whelp query engine developed at 
 
34
   the University of Bologna *)
 
35
 
 
36
let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
 
37
let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
 
38
 
 
39
open Goptions
 
40
 
 
41
let _ =
 
42
  declare_string_option 
 
43
    { optsync  = false;
 
44
      optname  = "Whelp server";
 
45
      optkey   = (SecondaryTable ("Whelp","Server"));
 
46
      optread  = (fun () -> !whelp_server_name);
 
47
      optwrite = (fun s -> whelp_server_name := s) }
 
48
 
 
49
let _ =
 
50
  declare_string_option 
 
51
    { optsync  = false;
 
52
      optname  = "Whelp getter";
 
53
      optkey   = (SecondaryTable ("Whelp","Getter"));
 
54
      optread  = (fun () -> !getter_server_name);
 
55
      optwrite = (fun s -> getter_server_name := s) }
 
56
 
 
57
 
 
58
let make_whelp_request req c =
 
59
  !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&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
 
60
 
 
61
let b = Buffer.create 16
 
62
 
 
63
let url_char c =
 
64
  if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or 
 
65
     '0' <= c & c <= '9' or c ='.'
 
66
  then Buffer.add_char b c
 
67
  else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
 
68
 
 
69
let url_string s = String.iter url_char s
 
70
 
 
71
let rec url_list_with_sep sep f = function
 
72
  | [] -> ()
 
73
  | [a] -> f a
 
74
  | a::l -> f a; url_string sep; url_list_with_sep sep f l 
 
75
 
 
76
let url_id id = url_string (string_of_id id)
 
77
 
 
78
let uri_of_dirpath dir =
 
79
  url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
 
80
 
 
81
let error_whelp_unknown_reference ref =
 
82
  let qid = Nametab.shortest_qualid_of_global Idset.empty ref in
 
83
  errorlabstrm ""
 
84
    (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ 
 
85
     strbrk ", are not supported in Whelp.")
 
86
 
 
87
let uri_of_repr_kn ref (mp,dir,l) = 
 
88
  match mp with
 
89
    | MPfile sl ->
 
90
        uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl)
 
91
    | _ ->
 
92
        error_whelp_unknown_reference ref
 
93
 
 
94
let url_paren f l = url_char '('; f l; url_char ')'
 
95
let url_bracket f l = url_char '['; f l; url_char ']'
 
96
 
 
97
let whelp_of_rawsort = function
 
98
  | RProp Null -> "Prop"
 
99
  | RProp Pos -> "Set"
 
100
  | RType _ -> "Type"
 
101
 
 
102
let uri_int n = Buffer.add_string b (string_of_int n)
 
103
 
 
104
let uri_of_ind_pointer l =
 
105
  url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l
 
106
 
 
107
let uri_of_global ref =
 
108
  match ref with
 
109
  | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".")
 
110
  | ConstRef cst ->
 
111
      uri_of_repr_kn ref (repr_con cst); url_string ".con"
 
112
  | IndRef (kn,i) -> 
 
113
      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1]
 
114
  | ConstructRef ((kn,i),j) ->
 
115
      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j]
 
116
 
 
117
let whelm_special = id_of_string "WHELM_ANON_VAR"
 
118
 
 
119
let url_of_name = function
 
120
  | Name id -> url_id id
 
121
  | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
 
122
 
 
123
let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
 
124
 
 
125
let uri_params f = function
 
126
  | [] -> ()
 
127
  | l -> url_string "\\subst"; 
 
128
         url_bracket (url_list_with_sep ";" (uri_of_binding f)) l
 
129
 
 
130
let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
 
131
 
 
132
let section_parameters = function
 
133
  | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
 
134
      get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
 
135
  | RRef (_,(ConstRef cst as ref)) ->
 
136
      get_discharged_hyp_names (sp_of_global ref)
 
137
  | _ -> []
 
138
 
 
139
let merge vl al =
 
140
  let rec aux acc = function
 
141
  | ([],l) | (_,([] as l)) -> List.rev acc, l
 
142
  | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
 
143
  in aux [] (vl,al)
 
144
 
 
145
let rec uri_of_constr c =
 
146
  match c with
 
147
  | RVar (_,id) -> url_id id
 
148
  | RRef (_,ref) ->  uri_of_global ref
 
149
  | RHole _ | REvar _ -> url_string "?"
 
150
  | RSort (_,s) -> url_string (whelp_of_rawsort s)
 
151
  | _ -> url_paren (fun () -> match c with
 
152
  | RApp (_,f,args) ->
 
153
      let inst,rest = merge (section_parameters f) args in
 
154
      uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
 
155
      url_list_with_sep " " uri_of_constr rest
 
156
  | RLambda (_,na,k,ty,c) ->
 
157
      url_string "\\lambda "; url_of_name na; url_string ":";
 
158
      uri_of_constr ty; url_string "."; uri_of_constr c
 
159
  | RProd (_,Anonymous,k,ty,c) ->
 
160
      uri_of_constr ty; url_string "\\to "; uri_of_constr c
 
161
  | RProd (_,Name id,k,ty,c) ->
 
162
      url_string "\\forall "; url_id id; url_string ":";
 
163
      uri_of_constr ty; url_string "."; uri_of_constr c
 
164
  | RLetIn (_,na,b,c) ->
 
165
      url_string "let "; url_of_name na; url_string "\\def ";
 
166
      uri_of_constr b; url_string " in "; uri_of_constr c
 
167
  | RCast (_,c, CastConv (_,t)) ->
 
168
      uri_of_constr c; url_string ":"; uri_of_constr t
 
169
  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
 
170
      error "Whelp does not support pattern-matching and (co-)fixpoint."
 
171
  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
 
172
      anomaly "Written w/o parenthesis"
 
173
  | RPatVar _ | RDynamic _ -> 
 
174
      anomaly "Found constructors not supported in constr") ()
 
175
 
 
176
let make_string f x = Buffer.reset b; f x; Buffer.contents b
 
177
 
 
178
let send_whelp req s =
 
179
  let url = make_whelp_request req s in
 
180
  let command = subst_command_placeholder browser_cmd_fmt url in
 
181
  let _ = run_command (fun x -> x) print_string command in ()
 
182
 
 
183
let whelp_constr req c =
 
184
  let c = detype false [whelm_special] [] c in
 
185
  send_whelp req (make_string uri_of_constr c)
 
186
 
 
187
let whelp_constr_expr req c =
 
188
  let (sigma,env)= get_current_context () in
 
189
  let _,c = interp_open_constr sigma env c in
 
190
  whelp_constr req c
 
191
 
 
192
let whelp_locate s =
 
193
  send_whelp "locate" s
 
194
 
 
195
let whelp_elim ind = 
 
196
  send_whelp "elim" (make_string uri_of_global (IndRef ind))
 
197
 
 
198
let on_goal f =
 
199
  let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
 
200
  f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
 
201
 
 
202
type whelp_request =
 
203
  | Locate of string
 
204
  | Elim of inductive
 
205
  | Constr of string * constr
 
206
 
 
207
let whelp = function
 
208
  | Locate s -> whelp_locate s
 
209
  | Elim ind -> whelp_elim ind
 
210
  | Constr (s,c) -> whelp_constr s c
 
211
 
 
212
VERNAC ARGUMENT EXTEND whelp_constr_request
 
213
| [ "Match" ] -> [ "match" ]
 
214
| [ "Instance" ] -> [ "instance" ]
 
215
END
 
216
 
 
217
VERNAC COMMAND EXTEND Whelp
 
218
| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
 
219
| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
 
220
| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] 
 
221
| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 
222
END
 
223
 
 
224
VERNAC COMMAND EXTEND WhelpHint
 
225
| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] 
 
226
| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] 
 
227
END