]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicParser.ml
rendering from markup to string
[helm.git] / helm / ocaml / cic / cicParser.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 let debug_print = prerr_endline
27
28 open Printf
29
30 (* ZACK TODO element from the DTD still to be handled:
31    <!ELEMENT CurrentProof (Conjecture*,body)>
32    <!ELEMENT Sequent %sequent;>
33    <!ELEMENT Conjecture %sequent;>
34    <!ELEMENT Decl %term;>
35    <!ELEMENT Def %term;>
36    <!ELEMENT Hidden EMPTY>
37    <!ELEMENT Goal %term;>
38 *)
39
40 exception Getter_failure of string * string
41 exception Parser_failure of string
42
43 type stack_entry =
44   | Arg of string * Cic.annterm (* relative uri, term *)
45   (* constants' body and types resides in differne files, thus we can't simple
46    * keep constants in Cic_obj stack entries *)
47   | Cic_attributes of Cic.attribute list
48   | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm
49       * Cic.attribute list
50       (* id, for, params, body, object attributes *)
51   | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm
52       * Cic.attribute list
53       (* id, name, params, type, object attributes *)
54   | Cic_term of Cic.annterm (* term *)
55   | Cic_obj of Cic.annobj   (* object *)
56   | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm
57       (* id, name, type, body *)
58   | Constructor of string * Cic.annterm   (* name, type *)
59   | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
60   | Def of Cic.id * Cic.name * Cic.annterm  (* id, binder, source *)
61   | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
62       (* id, name, ind. index, type, body *)
63   | Inductive_type of string * string * bool * Cic.annterm *
64       (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
65   | Meta_subst of Cic.annterm option
66   | Obj_class of Cic.object_class
67   | Obj_flavour of Cic.object_flavour
68   | Obj_field of string (* field name *)
69   | Obj_generated
70   | Tag of string * (string * string) list  (* tag name, attributes *)
71       (* ZACK TODO add file position to tag stack entry so that when attribute
72        * errors occur, the position of their _start_tag_ could be printed
73        * instead of the current position (usually the end tag) *)
74
75 type ctxt = {
76   mutable stack: stack_entry list;
77   mutable xml_parser: XmlPushParser.xml_parser option;
78   mutable filename: string;
79   uri: UriManager.uri;
80 }
81
82 let string_of_stack ctxt =
83   "[" ^ (String.concat "; "
84     (List.map
85       (function
86       | Arg (reluri, _) -> sprintf "Arg %s" reluri
87       | Cic_attributes _ -> "Cic_attributes"
88       | Cic_constant_body (id, name, _, _, _) ->
89           sprintf "Cic_constant_body %s (id=%s)" name id
90       | Cic_constant_type (id, name, _, _, _) ->
91           sprintf "Cic_constant_type %s (id=%s)" name id
92       | Cic_term _ -> "Cic_term"
93       | Cic_obj _ -> "Cic_obj"
94       | Constructor (name, _) -> "Constructor " ^ name
95       | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
96       | Decl (id, _, _) -> sprintf "Decl (id=%s)" id
97       | Def (id, _, _) -> sprintf "Def (id=%s)" id
98       | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
99       | Inductive_type (id, name, _, _, _) ->
100           sprintf "Inductive_type %s (id=%s)" name id
101       | Meta_subst _ -> "Meta_subst"
102       | Obj_class _ -> "Obj_class"
103       | Obj_flavour _ -> "Obj_flavour"
104       | Obj_field name -> "Obj_field " ^ name
105       | Obj_generated -> "Obj_generated"
106       | Tag (tag, _) -> "Tag " ^ tag)
107       ctxt.stack)) ^ "]"
108
109 let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2
110 let sort_attrs = List.sort compare_attrs
111
112 let new_parser_context uri = {
113   stack = [];
114   xml_parser = None;
115   filename = "-";
116   uri = uri;
117 }
118
119 let get_parser ctxt =
120   match ctxt.xml_parser with
121   | Some p -> p
122   | None -> assert false
123
124 (** {2 Error handling} *)
125
126 let parse_error ctxt msg =
127   let (line, col) = XmlPushParser.get_position (get_parser ctxt) in
128   raise (Parser_failure (sprintf "[%s: line %d, column %d] %s"
129     ctxt.filename line col msg))
130
131 let attribute_error ctxt tag =
132   parse_error ctxt ("wrong attribute set for " ^ tag)
133
134 (** {2 Parsing context management} *)
135
136 let pop ctxt =
137 (*  debug_print "pop";*)
138   match ctxt.stack with
139   | hd :: tl -> (ctxt.stack <- tl)
140   | _ -> assert false
141
142 let push ctxt v =
143 (*  debug_print "push";*)
144   ctxt.stack <- v :: ctxt.stack
145
146 let set_top ctxt v =
147 (*  debug_print "set_top";*)
148   match ctxt.stack with
149   | _ :: tl -> (ctxt.stack <- v :: tl)
150   | _ -> assert false
151
152   (** pop the last tag from the open tags stack returning a pair <tag_name,
153    * attribute_list> *)
154 let pop_tag ctxt =
155   match ctxt.stack with
156   | Tag (tag, attrs) :: tl ->
157       ctxt.stack <- tl;
158       (tag, attrs)
159   | _ -> parse_error ctxt "unexpected extra content"
160
161   (** pop the last tag from the open tags stack returning its attributes.
162    * Attributes are returned as a list of pair <name, value> _sorted_ by
163    * attribute name *)
164 let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt))
165
166 let pop_cics ctxt =
167   let rec aux acc stack =
168     match stack with
169     | Cic_term t :: tl -> aux (t :: acc) tl
170     | tl -> acc, tl
171   in
172   let values, new_stack = aux [] ctxt.stack in
173   ctxt.stack <- new_stack;
174   values
175
176 let pop_class_modifiers ctxt =
177   let rec aux acc stack =
178     match stack with
179     | (Cic_term (Cic.ASort _) as m) :: tl
180     | (Obj_field _ as m) :: tl ->
181         aux (m :: acc) tl
182     | tl -> acc, tl
183   in
184   let values, new_stack = aux [] ctxt.stack in
185   ctxt.stack <- new_stack;
186   values
187
188 let pop_meta_substs ctxt =
189   let rec aux acc stack =
190     match stack with
191     | Meta_subst t :: tl -> aux (t :: acc) tl
192     | tl -> acc, tl
193   in
194   let values, new_stack = aux [] ctxt.stack in
195   ctxt.stack <- new_stack;
196   values
197
198 let pop_fix_funs ctxt =
199   let rec aux acc stack =
200     match stack with
201     | Fix_fun (id, name, index, typ, body) :: tl ->
202         aux ((id, name, index, typ, body) :: acc) tl
203     | tl -> acc, tl
204   in
205   let values, new_stack = aux [] ctxt.stack in
206   ctxt.stack <- new_stack;
207   values
208
209 let pop_cofix_funs ctxt =
210   let rec aux acc stack =
211     match stack with
212     | Cofix_fun (id, name, typ, body) :: tl ->
213         aux ((id, name, typ, body) :: acc) tl
214     | tl -> acc, tl
215   in
216   let values, new_stack = aux [] ctxt.stack in
217   ctxt.stack <- new_stack;
218   values
219
220 let pop_constructors ctxt =
221   let rec aux acc stack =
222     match stack with
223     | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl
224     | tl -> acc, tl
225   in
226   let values, new_stack = aux [] ctxt.stack in
227   ctxt.stack <- new_stack;
228   values
229
230 let pop_inductive_types ctxt =
231   let rec aux acc stack =
232     match stack with
233     | Inductive_type (id, name, ind, arity, ctors) :: tl ->
234         aux ((id, name, ind, arity, ctors) :: acc) tl
235     | tl -> acc, tl
236   in
237   let values, new_stack = aux [] ctxt.stack in
238   if values = [] then
239     parse_error ctxt "no \"InductiveType\" element found";
240   ctxt.stack <- new_stack;
241   values
242
243   (** travels the stack (without popping) for the first term subject of explicit
244    * named substitution and return its URI *)
245 let find_base_uri ctxt =
246   let rec aux = function
247     | Cic_term (Cic.AConst (_, uri, _)) :: _
248     | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _
249     | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _
250     | Cic_term (Cic.AVar (_, uri, _)) :: _ ->
251         uri
252     | Arg _ :: tl -> aux tl
253     | _ -> parse_error ctxt "no \"arg\" element found"
254   in
255   UriManager.buri_of_uri (aux ctxt.stack)
256
257   (** backwardly eats the stack building an explicit named substitution from Arg
258    * stack entries *)
259 let pop_subst ctxt base_uri =
260   let rec aux acc stack =
261     match stack with
262     | Arg (rel_uri, term) :: tl ->
263         let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in
264         aux ((uri, term) :: acc) tl
265     | tl -> acc, tl
266   in
267   let subst, new_stack = aux [] ctxt.stack in
268   if subst = [] then
269     parse_error ctxt "no \"arg\" element found";
270   ctxt.stack <- new_stack;
271   subst
272
273 let pop_cic ctxt =
274   match ctxt.stack with
275   | Cic_term t :: tl ->
276       ctxt.stack <- tl;
277       t
278   | _ -> parse_error ctxt "no cic term found"
279
280 let pop_obj_attributes ctxt =
281   match ctxt.stack with
282   | Cic_attributes attributes :: tl ->
283       ctxt.stack <- tl;
284       attributes
285   | _ -> []
286
287 (** {2 Auxiliary functions} *)
288
289 let uri_of_string = UriManager.uri_of_string
290
291 let uri_list_of_string =
292   let space_RE = Str.regexp " " in
293   fun s ->
294     List.map uri_of_string (Str.split space_RE s)
295
296 let sort_of_string ctxt = function
297   | "Prop" -> Cic.Prop
298   | "Set"  -> Cic.Set
299   | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
300 (*   | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
301   | "CProp" -> Cic.CProp
302   | _ -> parse_error ctxt "sort expected"
303
304 let patch_subst ctxt subst = function
305   | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
306   | Cic.AMutInd (id, uri, typeno, _) ->
307       Cic.AMutInd (id, uri, typeno, subst)
308   | Cic.AMutConstruct (id, uri, typeno, consno, _) ->
309       Cic.AMutConstruct (id, uri, typeno, consno, subst)
310   | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst)
311   | _ ->
312       parse_error ctxt
313         ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^
314         " instantiated")
315
316   (** backwardly eats the stack seeking for the first open tag carrying
317    * "helm:exception" attributes. If found return Some of a pair containing
318    * exception name and argument. Return None otherwise *)
319 let find_helm_exception ctxt =
320   let rec aux = function
321     | [] -> None
322     | Tag (_, attrs) :: tl ->
323         (try
324           let exn = List.assoc "helm:exception" attrs in
325           let arg =
326             try List.assoc "helm:exception_arg" attrs with Not_found -> ""
327           in
328           Some (exn, arg)
329         with Not_found -> aux tl)
330     | _ :: tl -> aux tl
331   in
332   aux ctxt.stack
333
334 (** {2 Push parser callbacks}
335  * each callback needs to be instantiated to a parsing context *)
336
337 let start_element ctxt tag attrs =
338 (*  debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*)
339   push ctxt (Tag (tag, attrs))
340
341 let end_element ctxt tag =
342 (*  debug_print (sprintf "</%s>" tag);*)
343 (*  debug_print (string_of_stack ctxt);*)
344   let attribute_error () = attribute_error ctxt tag in
345   let parse_error = parse_error ctxt in
346   let sort_of_string = sort_of_string ctxt in
347   match tag with
348   | "REL" ->
349       push ctxt (Cic_term
350         (match pop_tag_attrs ctxt with
351         | ["binder", binder; "id", id; "idref", idref; "sort", _;
352            "value", value] ->
353             Cic.ARel (id, idref, int_of_string value, binder)
354         | _ -> attribute_error ()))
355   | "VAR" ->
356       push ctxt (Cic_term
357         (match pop_tag_attrs ctxt with
358         | ["id", id; "sort", _; "uri", uri] ->
359             Cic.AVar (id, uri_of_string uri, [])
360         | _ -> attribute_error ()))
361   | "CONST" ->
362       push ctxt (Cic_term
363         (match pop_tag_attrs ctxt with
364         | ["id", id; "sort", _; "uri", uri] ->
365             Cic.AConst (id, uri_of_string uri, [])
366         | _ -> attribute_error ()))
367   | "SORT" ->
368       push ctxt (Cic_term
369         (match pop_tag_attrs ctxt with
370         | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort)
371         | _ -> attribute_error ()))
372   | "APPLY" ->
373       let args = pop_cics ctxt in
374       push ctxt (Cic_term
375         (match pop_tag_attrs ctxt with
376         | ["id", id; "sort", _] -> Cic.AAppl (id, args)
377         | _ -> attribute_error ()))
378   | "decl" ->
379       let source = pop_cic ctxt in
380       push ctxt
381         (match pop_tag_attrs ctxt with
382         | ["binder", binder; "id", id; "type", _] ->
383             Decl (id, Cic.Name binder, source)
384         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
385         | _ -> attribute_error ())
386   | "def" ->  (* same as "decl" above *)
387       let source = pop_cic ctxt in
388       push ctxt
389         (match pop_tag_attrs ctxt with
390         | ["binder", binder; "id", id; "sort", _] ->
391             Def (id, Cic.Name binder, source)
392         | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
393         | _ -> attribute_error ())
394   | "arity"           (* transparent elements (i.e. which contain a CIC) *)
395   | "body"
396   | "inductiveTerm"
397   | "pattern"
398   | "patternsType"
399   | "target"
400   | "term"
401   | "type" ->
402       let term = pop_cic ctxt in
403       pop ctxt; (* pops start tag matching current end tag (e.g. <arity>) *)
404       push ctxt (Cic_term term)
405   | "substitution" ->   (* optional transparent elements (i.e. which _may_
406                          * contain a CIC) *)
407       set_top ctxt  (* replace <substitution> *)
408         (match ctxt.stack with
409         | Cic_term term :: tl ->
410             ctxt.stack <- tl;
411             (Meta_subst (Some term))
412         | _ ->  Meta_subst None)
413   | "PROD" ->
414       let target = pop_cic ctxt in
415       let rec add_decl target = function
416         | Decl (id, binder, source) :: tl ->
417             add_decl (Cic.AProd (id, binder, source, target)) tl
418         | tl ->
419             ctxt.stack <- tl;
420             target
421       in
422       let term = add_decl target ctxt.stack in
423       (match pop_tag_attrs ctxt with
424       | ["type", _] -> ()
425       | _ -> attribute_error ());
426       push ctxt (Cic_term term)
427   | "LAMBDA" ->
428       let target = pop_cic ctxt in
429       let rec add_decl target = function
430         | Decl (id, binder, source) :: tl ->
431             add_decl (Cic.ALambda (id, binder, source, target)) tl
432         | tl ->
433             ctxt.stack <- tl;
434             target
435       in
436       let term = add_decl target ctxt.stack in
437       (match pop_tag_attrs ctxt with
438       | ["sort", _] -> ()
439       | _ -> attribute_error ());
440       push ctxt (Cic_term term)
441   | "LETIN" ->
442       let target = pop_cic ctxt in
443       let rec add_def target = function
444         | Def (id, binder, source) :: tl ->
445             add_def (Cic.ALetIn (id, binder, source, target)) tl
446         | tl ->
447             ctxt.stack <- tl;
448             target
449       in
450       let term = add_def target ctxt.stack in
451       (match pop_tag_attrs ctxt with
452       | ["sort", _] -> ()
453       | _ -> attribute_error ());
454       push ctxt (Cic_term term)
455   | "CAST" ->
456       let typ = pop_cic ctxt in
457       let term = pop_cic ctxt in
458       push ctxt (Cic_term
459         (match pop_tag_attrs ctxt with
460         | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
461         | _ -> attribute_error ()));
462   | "IMPLICIT" ->
463       push ctxt (Cic_term
464         (match pop_tag_attrs ctxt with
465         | ["id", id] -> Cic.AImplicit (id, None)
466         | ["annotation", annotation; "id", id] ->
467             let implicit_annotation =
468               match annotation with
469               | "closed" -> `Closed
470               | "hole" -> `Hole
471               | "type" -> `Type
472               | _ -> parse_error "invalid value for \"annotation\" attribute"
473             in
474             Cic.AImplicit (id, Some implicit_annotation)
475         | _ -> attribute_error ()))
476   | "META" ->
477       let meta_substs = pop_meta_substs ctxt in
478       push ctxt (Cic_term
479         (match pop_tag_attrs ctxt with
480         | ["id", id; "no", no; "sort", _] ->
481             Cic.AMeta (id, int_of_string no, meta_substs)
482         | _ -> attribute_error ()));
483   | "MUTIND" ->
484       push ctxt (Cic_term
485         (match pop_tag_attrs ctxt with
486         | ["id", id; "noType", noType; "uri", uri] ->
487             Cic.AMutInd (id, uri_of_string uri, int_of_string noType, [])
488         | _ -> attribute_error ()));
489   | "MUTCONSTRUCT" ->
490       push ctxt (Cic_term
491         (match pop_tag_attrs ctxt with
492         | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
493            "uri", uri] ->
494             Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
495               int_of_string noConstr, [])
496         | _ -> attribute_error ()));
497   | "FixFunction" ->
498       let body = pop_cic ctxt in
499       let typ = pop_cic ctxt in
500       push ctxt
501         (match pop_tag_attrs ctxt with
502         | ["id", id; "name", name; "recIndex", recIndex] ->
503             Fix_fun (id, name, int_of_string recIndex, typ, body)
504         | _ -> attribute_error ())
505   | "CofixFunction" ->
506       let body = pop_cic ctxt in
507       let typ = pop_cic ctxt in
508       push ctxt
509         (match pop_tag_attrs ctxt with
510         | ["id", id; "name", name] ->
511             Cofix_fun (id, name, typ, body)
512         | _ -> attribute_error ())
513   | "FIX" ->
514       let fix_funs = pop_fix_funs ctxt in
515       push ctxt (Cic_term
516         (match pop_tag_attrs ctxt with
517         | ["id", id; "noFun", noFun; "sort", _] ->
518             Cic.AFix (id, int_of_string noFun, fix_funs)
519         | _ -> attribute_error ()))
520   | "COFIX" ->
521       let cofix_funs = pop_cofix_funs ctxt in
522       push ctxt (Cic_term
523         (match pop_tag_attrs ctxt with
524         | ["id", id; "noFun", noFun; "sort", _] ->
525             Cic.ACoFix (id, int_of_string noFun, cofix_funs)
526         | _ -> attribute_error ()))
527   | "MUTCASE" ->
528       (match pop_cics ctxt with
529       | patternsType :: inductiveTerm :: patterns ->
530           push ctxt (Cic_term
531             (match pop_tag_attrs ctxt with
532             | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
533                 Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
534                   patternsType, inductiveTerm, patterns)
535             | _ -> attribute_error ()))
536       | _ -> parse_error "invalid \"MUTCASE\" content")
537   | "Constructor" ->
538       let typ = pop_cic ctxt in
539       push ctxt
540         (match pop_tag_attrs ctxt with
541         | ["name", name] -> Constructor (name, typ)
542         | _ -> attribute_error ())
543   | "InductiveType" ->
544       let constructors = pop_constructors ctxt in
545       let arity = pop_cic ctxt in
546       push ctxt
547         (match pop_tag_attrs ctxt with
548         | ["id", id; "inductive", inductive; "name", name] ->
549             Inductive_type (id, name, bool_of_string inductive, arity,
550               constructors)
551         | _ -> attribute_error ())
552   | "InductiveDefinition" ->
553       let inductive_types = pop_inductive_types ctxt in
554       let obj_attributes = pop_obj_attributes ctxt in
555       push ctxt (Cic_obj
556         (match pop_tag_attrs ctxt with
557         | ["id", id; "noParams", noParams; "params", params] ->
558             Cic.AInductiveDefinition (id, inductive_types,
559               uri_list_of_string params, int_of_string noParams, obj_attributes)
560         | _ -> attribute_error ()))
561   | "ConstantType" ->
562       let typ = pop_cic ctxt in
563       let obj_attributes = pop_obj_attributes ctxt in
564       push ctxt
565         (match pop_tag_attrs ctxt with
566         | ["id", id; "name", name; "params", params] ->
567             Cic_constant_type (id, name, uri_list_of_string params, typ,
568               obj_attributes)
569         | _ -> attribute_error ())
570   | "ConstantBody" ->
571       let body = pop_cic ctxt in
572       let obj_attributes = pop_obj_attributes ctxt in
573       push ctxt
574         (match pop_tag_attrs ctxt with
575         | ["for", for_; "id", id; "params", params] ->
576             Cic_constant_body (id, for_, uri_list_of_string params, body,
577               obj_attributes)
578         | _ -> attribute_error ())
579   | "Variable" ->
580       let typ = pop_cic ctxt in
581       let body =
582         match pop_cics ctxt with
583         | [] -> None
584         | [t] -> Some t
585         | _ -> parse_error "wrong content for \"Variable\""
586       in
587       let obj_attributes = pop_obj_attributes ctxt in
588       push ctxt (Cic_obj
589         (match pop_tag_attrs ctxt with
590         | ["id", id; "name", name; "params", params] ->
591             Cic.AVariable (id, name, body, typ, uri_list_of_string params,
592               obj_attributes)
593         | _ -> attribute_error ()))
594   | "arg" ->
595       let term = pop_cic ctxt in
596       push ctxt
597         (match pop_tag_attrs ctxt with
598         | ["relUri", relUri] -> Arg (relUri, term)
599         | _ -> attribute_error ())
600   | "instantiate" ->
601         (* explicit named substitution handling: when the end tag of an element
602          * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it
603          * is stored on the stack with no substitutions (i.e. []). When the end
604          * tag of an "instantiate" element is found we patch the term currently
605          * on the stack with the substitution built from "instantiate" children
606          *)
607         (* XXX inefficiency here: first travels the <arg> elements in order to
608          * find the baseUri, then in order to build the explicit named subst *)
609       let base_uri = find_base_uri ctxt in
610       let subst = pop_subst ctxt base_uri in
611       let term = pop_cic ctxt in
612         (* comment from CicParser3.ml:
613          * CSC: the "id" optional attribute should be parsed and reflected in
614          *      Cic.annterm and id = string_of_xml_attr (n#attribute "id") *)
615         (* replace <instantiate> *)
616       set_top ctxt (Cic_term (patch_subst ctxt subst term))
617   | "attributes" ->
618       let rec aux acc = function  (* retrieve object attributes *)
619         | Obj_class c :: tl -> aux (`Class c :: acc) tl
620         | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
621         | Obj_generated :: tl -> aux (`Generated :: acc) tl
622         | tl -> acc, tl
623       in
624       let obj_attrs, new_stack = aux [] ctxt.stack in
625       ctxt.stack <- new_stack;
626       set_top ctxt (Cic_attributes obj_attrs)
627   | "generated" -> set_top ctxt Obj_generated
628   | "field" ->
629       push ctxt
630         (match pop_tag_attrs ctxt with
631         | ["name", name] -> Obj_field name
632         | _ -> attribute_error ())
633   | "flavour" ->
634       push ctxt 
635         (match pop_tag_attrs ctxt with
636         | [ "value", "definition"] -> Obj_flavour `Definition
637         | [ "value", "fact"] -> Obj_flavour `Fact
638         | [ "value", "lemma"] -> Obj_flavour `Lemma
639         | [ "value", "remark"] -> Obj_flavour `Remark
640         | [ "value", "theorem"] -> Obj_flavour `Theorem
641         | [ "value", "variant"] -> Obj_flavour `Variant
642         | _ -> attribute_error ())
643   | "class" ->
644       let class_modifiers = pop_class_modifiers ctxt in
645       push ctxt
646         (match pop_tag_attrs ctxt with
647         | ["value", "coercion"] -> Obj_class `Coercion
648         | ["value", "elim"] ->
649             (match class_modifiers with
650             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
651             | _ ->
652                 parse_error
653                   "unexpected extra content for \"elim\" object class")
654         | ["value", "record"] ->
655             let fields =
656               List.map
657                 (function
658                   | Obj_field name -> name
659                   | _ ->
660                       parse_error
661                         "unexpected extra content for \"record\" object class")
662                 class_modifiers
663             in
664             Obj_class (`Record fields)
665         | ["value", "projection"] -> Obj_class `Projection
666         | _ -> attribute_error ())
667   | tag ->
668       match find_helm_exception ctxt with
669       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
670       | None -> parse_error (sprintf "unknown element \"%s\"" tag)
671
672 (** {2 Parser internals} *)
673
674 let has_gz_suffix fname =
675   try
676     let idx = String.rindex fname '.' in
677     let suffix = String.sub fname idx (String.length fname - idx) in
678     suffix = ".gz"
679   with Not_found -> false
680
681 let parse uri filename =
682   let ctxt = new_parser_context uri in
683   ctxt.filename <- filename;
684   let module P = XmlPushParser in
685   let callbacks = {
686     P.default_callbacks with
687       P.start_element = Some (start_element ctxt);
688       P.end_element = Some (end_element ctxt);
689   } in
690   let xml_parser = P.create_parser callbacks in
691   ctxt.xml_parser <- Some xml_parser;
692   try
693     (try
694       let xml_source =
695         if has_gz_suffix filename then `Gzip_file filename
696         else `File filename
697       in
698       P.parse xml_parser xml_source
699     with exn ->
700       ctxt.xml_parser <- None;
701       (* ZACK: the above "<- None" is vital for garbage collection. Without it
702        * we keep in memory a circular structure parser -> callbacks -> ctxt ->
703        * parser. I don't know if the ocaml garbage collector is supposed to
704        * collect such structures, but for sure the expat bindings will (orribly)
705        * leak when used in conjunction with such structures *)
706       raise exn);
707     ctxt.xml_parser <- None; (* ZACK: same comment as above *)
708 (*    debug_print (string_of_stack stack);*)
709     (* assert (List.length ctxt.stack = 1) *)
710     List.hd ctxt.stack
711   with
712   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
713   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
714   | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
715   | Parser_failure _
716   | Getter_failure _ as exn ->
717       raise exn
718   | exn ->
719       raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
720
721 (** {2 API implementation} *)
722
723 let annobj_of_xml uri filename filenamebody =
724   match filenamebody with
725   | None ->
726       (match parse uri filename with
727       | Cic_constant_type (id, name, params, typ, obj_attributes) ->
728           Cic.AConstant (id, None, name, None, typ, params, obj_attributes)
729       | Cic_obj obj -> obj
730       | _ -> raise (Parser_failure ("no object found in " ^ filename)))
731   | Some filenamebody ->
732       (match parse uri filename, parse uri filenamebody with
733       | Cic_constant_type (type_id, name, params, typ, obj_attributes),
734         Cic_constant_body (body_id, _, _, body, _) ->
735           Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[])
736       | _ ->
737           raise (Parser_failure (sprintf "no constant found in %s, %s"
738             filename filenamebody)))
739
740 let obj_of_xml uri filename filenamebody =
741  Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)