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