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
(************************************************************************)
9
(*i camlp4use: "pa_extend.cmo" i*)
11
(* $Id: g_xml.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
26
(* Generic xml parser without raw data *)
28
type attribute = string * (loc * string)
29
type xml = XmlTag of loc * string * attribute list * xml list
31
let check_tags loc otag ctag =
33
user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
34
str "does not match open xml tag " ++ str otag ++ str ".")
36
let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e)
42
[ [ x = xml; EOI -> x ] ]
45
[ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
46
"<"; "/"; ctag = IDENT; ">" ->
47
check_tags loc otag ctag;
48
XmlTag (loc,ctag,attrs,l)
49
| "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
50
XmlTag (loc,tag,attrs,[])
54
[ [ name = IDENT; "="; data = STRING -> (name, (loc, data)) ] ]
60
let error_expect_one_argument loc =
61
user_err_loc (loc,"",str "wrong number of arguments (expect one).")
63
let error_expect_no_argument loc =
64
user_err_loc (loc,"",str "wrong number of arguments (expect none).")
66
(* Interpreting attributes *)
70
with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
72
let interp_xml_attr_qualid = function
73
| "uri", s -> qualid_of_string s
74
| _ -> error "Ill-formed xml attribute"
76
let get_xml_attr s al =
78
with Not_found -> error ("No attribute "^s)
80
(* Interpreting specific attributes *)
82
let ident_of_cdata (loc,a) = id_of_string a
85
let n = String.index s ':' in
86
let p = String.index s '.' in
87
let s = String.sub s (n+2) (p-n-2) in
88
for i=0 to String.length s - 1 do if s.[i]='/' then s.[i]<-'.' done;
91
let constant_of_cdata (loc,a) = Nametab.locate_constant (uri_of_data a)
93
let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a)
95
let inductive_of_cdata a = match global_of_cdata a with
97
| _ -> anomaly "XML parser: not an inductive"
99
let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
101
let sort_of_cdata (loc,a) = match a with
102
| "Prop" -> RProp Null
104
| "Type" -> RType None
105
| _ -> user_err_loc (loc,"",str "sort expected.")
107
let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
109
let get_xml_inductive_kn al =
110
inductive_of_cdata (* uriType apparent synonym of uri *)
111
(try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
113
let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
115
let get_xml_inductive al =
116
(get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al))
118
let get_xml_constructor al =
119
(get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
121
let get_xml_binder al =
122
try Name (ident_of_cdata (List.assoc "binder" al))
123
with Not_found -> Anonymous
125
let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
127
let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
129
let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
131
let get_xml_no al = nmtoken (get_xml_attr "no" al)
133
(* A leak in the xml dtd: arities of constructor need to know global env *)
135
let compute_branches_lengths ind =
136
let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
137
mip.Declarations.mind_consnrealdecls
139
let compute_inductive_nargs ind =
140
Inductiveops.inductive_nargs (Global.env()) ind
142
(* Interpreting constr as a rawconstr *)
144
let rec interp_xml_constr = function
145
| XmlTag (loc,"REL",al,[]) ->
146
RVar (loc, get_xml_ident al)
147
| XmlTag (loc,"VAR",al,[]) ->
148
error "XML parser: unable to interp free variables"
149
| XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
150
let body,decls = list_sep_last xl in
151
let ctx = List.map interp_xml_decl decls in
152
List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b))
153
ctx (interp_xml_target body)
154
| XmlTag (loc,"PROD",al,(_::_ as xl)) ->
155
let body,decls = list_sep_last xl in
156
let ctx = List.map interp_xml_decl decls in
157
List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b))
158
ctx (interp_xml_target body)
159
| XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
160
let body,defs = list_sep_last xl in
161
let ctx = List.map interp_xml_def defs in
162
List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b))
163
ctx (interp_xml_target body)
164
| XmlTag (loc,"APPLY",_,x::xl) ->
165
RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
166
| XmlTag (loc,"instantiate",_,
167
(XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
168
RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
169
| XmlTag (loc,"META",al,xl) ->
170
REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
171
| XmlTag (loc,"CONST",al,[]) ->
172
RRef (loc, ConstRef (get_xml_constant al))
173
| XmlTag (loc,"MUTCASE",al,x::y::yl) ->
174
let ind = get_xml_inductive al in
175
let p = interp_xml_patternsType x in
176
let tm = interp_xml_inductiveTerm y in
177
let brs = List.map interp_xml_pattern yl in
178
let brns = Array.to_list (compute_branches_lengths ind) in
179
let mat = simple_cases_matrix_of_branches ind brns brs in
180
let nparams,n = compute_inductive_nargs ind in
181
let nal,rtn = return_type_of_predicate ind nparams n p in
182
RCases (loc,RegularStyle,rtn,[tm,nal],mat)
183
| XmlTag (loc,"MUTIND",al,[]) ->
184
RRef (loc, IndRef (get_xml_inductive al))
185
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
186
RRef (loc, ConstructRef (get_xml_constructor al))
187
| XmlTag (loc,"FIX",al,xl) ->
188
let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
189
let ln,lc,lt = list_split3 lnct in
190
let lctx = List.map (fun _ -> []) ln in
191
RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
192
| XmlTag (loc,"COFIX",al,xl) ->
193
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
194
RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
195
| XmlTag (loc,"CAST",al,[x1;x2]) ->
196
RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
197
| XmlTag (loc,"SORT",al,[]) ->
198
RSort (loc, get_xml_sort al)
199
| XmlTag (loc,s,_,_) ->
200
user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
202
and interp_xml_tag s = function
203
| XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl)
204
| XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
205
str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
207
and interp_xml_constr_alias s x =
208
match interp_xml_tag s x with
209
| (_,_,[x]) -> interp_xml_constr x
210
| (loc,_,_) -> error_expect_one_argument loc
212
and interp_xml_term x = interp_xml_constr_alias "term" x
213
and interp_xml_type x = interp_xml_constr_alias "type" x
214
and interp_xml_target x = interp_xml_constr_alias "target" x
215
and interp_xml_body x = interp_xml_constr_alias "body" x
216
and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
217
and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
218
and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
219
and interp_xml_arg x = interp_xml_constr_alias "arg" x
220
and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
221
(* no support for empty substitution from official dtd *)
223
and interp_xml_decl_alias s x =
224
match interp_xml_tag s x with
225
| (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
226
| (loc,_,_) -> error_expect_one_argument loc
228
and interp_xml_def x = interp_xml_decl_alias "def" x
229
and interp_xml_decl x = interp_xml_decl_alias "decl" x
231
and interp_xml_recursionOrder x =
232
let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
233
let (locs, s) = get_xml_attr "type" al in
236
(match l with [] -> RStructRec
237
| _ -> error_expect_no_argument loc)
240
[c] -> RWfRec (interp_xml_type c)
241
| _ -> error_expect_one_argument loc)
244
[c] -> RMeasureRec (interp_xml_type c)
245
| _ -> error_expect_one_argument loc)
247
user_err_loc (locs,"",str "Invalid recursion order.")
249
and interp_xml_FixFunction x =
250
match interp_xml_tag "FixFunction" x with
251
| (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
252
((Some (nmtoken (get_xml_attr "recIndex" al)),
253
interp_xml_recursionOrder x1),
254
(get_xml_name al, interp_xml_type x2, interp_xml_body x3))
255
| (loc,al,[x1;x2]) ->
256
((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
257
(get_xml_name al, interp_xml_type x1, interp_xml_body x2))
259
error_expect_one_argument loc
261
and interp_xml_CoFixFunction x =
262
match interp_xml_tag "CoFixFunction" x with
263
| (loc,al,[x1;x2]) ->
264
(get_xml_name al, interp_xml_type x1, interp_xml_body x2)
266
error_expect_one_argument loc
268
(* Interpreting tactic argument *)
270
let rec interp_xml_tactic_arg = function
271
| XmlTag (loc,"TERM",[],[x]) ->
272
ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
273
| XmlTag (loc,"CALL",al,xl) ->
274
let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
275
TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
276
| XmlTag (loc,s,_,_) ->
277
user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
279
let parse_tactic_arg ch =
280
interp_xml_tactic_arg
281
(Pcoq.Gram.Entry.parse xml_eoi
282
(Pcoq.Gram.parsable (Stream.of_channel ch)))
added
removed
parsing/g_xml.ml4
