1 (* Copyright (C) 2004-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
29 let debug_print s = if debug then prerr_endline (Lazy.force s)
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;>
39 <!ELEMENT Hidden EMPTY>
40 <!ELEMENT Goal %term;>
43 exception Getter_failure of string * string
44 exception Parser_failure of string
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
53 (* id, for, params, body, object attributes *)
54 | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm
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 *)
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) *)
79 mutable stack: stack_entry list;
80 mutable xml_parser: XmlPushParser.xml_parser option;
81 mutable filename: string;
85 let string_of_stack ctxt =
86 "[" ^ (String.concat "; "
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)
112 let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2
113 let sort_attrs = List.sort compare_attrs
115 let new_parser_context uri = {
122 let get_parser ctxt =
123 match ctxt.xml_parser with
125 | None -> assert false
127 (** {2 Error handling} *)
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))
134 let attribute_error ctxt tag =
135 parse_error ctxt ("wrong attribute set for " ^ tag)
137 (** {2 Parsing context management} *)
140 (* debug_print (lazy "pop");*)
141 match ctxt.stack with
142 | hd :: tl -> (ctxt.stack <- tl)
146 (* debug_print (lazy "push");*)
147 ctxt.stack <- v :: ctxt.stack
150 (* debug_print (lazy "set_top");*)
151 match ctxt.stack with
152 | _ :: tl -> (ctxt.stack <- v :: tl)
155 (** pop the last tag from the open tags stack returning a pair <tag_name,
158 match ctxt.stack with
159 | Tag (tag, attrs) :: tl ->
162 | _ -> parse_error ctxt "unexpected extra content"
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
167 let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt))
170 let rec aux acc stack =
172 | Cic_term t :: tl -> aux (t :: acc) tl
175 let values, new_stack = aux [] ctxt.stack in
176 ctxt.stack <- new_stack;
179 let pop_class_modifiers ctxt =
180 let rec aux acc stack =
182 | (Cic_term (Cic.ASort _) as m) :: tl
183 | (Obj_field _ as m) :: tl ->
187 let values, new_stack = aux [] ctxt.stack in
188 ctxt.stack <- new_stack;
191 let pop_meta_substs ctxt =
192 let rec aux acc stack =
194 | Meta_subst t :: tl -> aux (t :: acc) tl
197 let values, new_stack = aux [] ctxt.stack in
198 ctxt.stack <- new_stack;
201 let pop_fix_funs ctxt =
202 let rec aux acc stack =
204 | Fix_fun (id, name, index, typ, body) :: tl ->
205 aux ((id, name, index, typ, body) :: acc) tl
208 let values, new_stack = aux [] ctxt.stack in
209 ctxt.stack <- new_stack;
212 let pop_cofix_funs ctxt =
213 let rec aux acc stack =
215 | Cofix_fun (id, name, typ, body) :: tl ->
216 aux ((id, name, typ, body) :: acc) tl
219 let values, new_stack = aux [] ctxt.stack in
220 ctxt.stack <- new_stack;
223 let pop_constructors ctxt =
224 let rec aux acc stack =
226 | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl
229 let values, new_stack = aux [] ctxt.stack in
230 ctxt.stack <- new_stack;
233 let pop_inductive_types ctxt =
234 let rec aux acc stack =
236 | Inductive_type (id, name, ind, arity, ctors) :: tl ->
237 aux ((id, name, ind, arity, ctors) :: acc) tl
240 let values, new_stack = aux [] ctxt.stack in
242 parse_error ctxt "no \"InductiveType\" element found";
243 ctxt.stack <- new_stack;
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, _)) :: _ ->
255 | Arg _ :: tl -> aux tl
256 | _ -> parse_error ctxt "no \"arg\" element found"
258 UriManager.buri_of_uri (aux ctxt.stack)
260 (** backwardly eats the stack building an explicit named substitution from Arg
262 let pop_subst ctxt base_uri =
263 let rec aux acc stack =
265 | Arg (rel_uri, term) :: tl ->
266 let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in
267 aux ((uri, term) :: acc) tl
270 let subst, new_stack = aux [] ctxt.stack in
272 parse_error ctxt "no \"arg\" element found";
273 ctxt.stack <- new_stack;
277 match ctxt.stack with
278 | Cic_term t :: tl ->
281 | _ -> parse_error ctxt "no cic term found"
283 let pop_obj_attributes ctxt =
284 match ctxt.stack with
285 | Cic_attributes attributes :: tl ->
290 (** {2 Auxiliary functions} *)
292 let uri_of_string = UriManager.uri_of_string
294 let uri_list_of_string =
295 let space_RE = Str.regexp " " in
297 List.map uri_of_string (Str.split space_RE s)
299 let sort_of_string ctxt = function
302 | "CProp" -> Cic.CProp
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
306 | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
308 let len = String.length s in
309 if not(len > 5) then parse_error ctxt "sort expected";
310 if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
315 ~id:(int_of_string (String.sub s 5 (len - 5))) ())
317 | Failure "int_of_string"
318 | Invalid_argument _ -> parse_error ctxt "sort expected"
320 let patch_subst ctxt subst = function
321 | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
322 | Cic.AMutInd (id, uri, typeno, _) ->
323 Cic.AMutInd (id, uri, typeno, subst)
324 | Cic.AMutConstruct (id, uri, typeno, consno, _) ->
325 Cic.AMutConstruct (id, uri, typeno, consno, subst)
326 | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst)
329 ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^
332 (** backwardly eats the stack seeking for the first open tag carrying
333 * "helm:exception" attributes. If found return Some of a pair containing
334 * exception name and argument. Return None otherwise *)
335 let find_helm_exception ctxt =
336 let rec aux = function
338 | Tag (_, attrs) :: tl ->
340 let exn = List.assoc "helm:exception" attrs in
342 try List.assoc "helm:exception_arg" attrs with Not_found -> ""
345 with Not_found -> aux tl)
350 (** {2 Push parser callbacks}
351 * each callback needs to be instantiated to a parsing context *)
353 let start_element ctxt tag attrs =
354 (* debug_print (lazy (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs))));*)
355 push ctxt (Tag (tag, attrs))
357 let end_element ctxt tag =
358 (* debug_print (lazy (sprintf "</%s>" tag));*)
359 (* debug_print (lazy (string_of_stack ctxt));*)
360 let attribute_error () = attribute_error ctxt tag in
361 let parse_error = parse_error ctxt in
362 let sort_of_string = sort_of_string ctxt in
366 (match pop_tag_attrs ctxt with
367 | ["binder", binder; "id", id; "idref", idref; "value", value]
368 | ["binder", binder; "id", id; "idref", idref; "sort", _;
370 Cic.ARel (id, idref, int_of_string value, binder)
371 | _ -> attribute_error ()))
374 (match pop_tag_attrs ctxt with
375 | ["id", id; "uri", uri]
376 | ["id", id; "sort", _; "uri", uri] ->
377 Cic.AVar (id, uri_of_string uri, [])
378 | _ -> attribute_error ()))
381 (match pop_tag_attrs ctxt with
382 | ["id", id; "uri", uri]
383 | ["id", id; "sort", _; "uri", uri] ->
384 Cic.AConst (id, uri_of_string uri, [])
385 | _ -> attribute_error ()))
388 (match pop_tag_attrs ctxt with
389 | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort)
390 | _ -> attribute_error ()))
392 let args = pop_cics ctxt in
394 (match pop_tag_attrs ctxt with
396 | ["id", id; "sort", _] -> Cic.AAppl (id, args)
397 | _ -> attribute_error ()))
399 let source = pop_cic ctxt in
401 (match pop_tag_attrs ctxt with
402 | ["binder", binder; "id", id ]
403 | ["binder", binder; "id", id; "type", _] ->
404 Decl (id, Cic.Name binder, source)
406 | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
407 | _ -> attribute_error ())
408 | "def" -> (* same as "decl" above *)
409 let ty = pop_cic ctxt in
410 let source = pop_cic ctxt in
412 (match pop_tag_attrs ctxt with
413 | ["binder", binder; "id", id]
414 | ["binder", binder; "id", id; "sort", _] ->
415 Def (id, Cic.Name binder, source, ty)
417 | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty)
418 | _ -> attribute_error ())
419 | "arity" (* transparent elements (i.e. which contain a CIC) *)
427 let term = pop_cic ctxt in
428 pop ctxt; (* pops start tag matching current end tag (e.g. <arity>) *)
429 push ctxt (Cic_term term)
430 | "substitution" -> (* optional transparent elements (i.e. which _may_
432 set_top ctxt (* replace <substitution> *)
433 (match ctxt.stack with
434 | Cic_term term :: tl ->
436 (Meta_subst (Some term))
437 | _ -> Meta_subst None)
439 let target = pop_cic ctxt in
440 let rec add_decl target = function
441 | Decl (id, binder, source) :: tl ->
442 add_decl (Cic.AProd (id, binder, source, target)) tl
447 let term = add_decl target ctxt.stack in
448 (match pop_tag_attrs ctxt with
451 | _ -> attribute_error ());
452 push ctxt (Cic_term term)
454 let target = pop_cic ctxt in
455 let rec add_decl target = function
456 | Decl (id, binder, source) :: tl ->
457 add_decl (Cic.ALambda (id, binder, source, target)) tl
462 let term = add_decl target ctxt.stack in
463 (match pop_tag_attrs ctxt with
466 | _ -> attribute_error ());
467 push ctxt (Cic_term term)
469 let target = pop_cic ctxt in
470 let rec add_def target = function
471 | Def (id, binder, source, ty) :: tl ->
472 add_def (Cic.ALetIn (id, binder, source, ty, target)) tl
477 let term = add_def target ctxt.stack in
478 (match pop_tag_attrs ctxt with
481 | _ -> attribute_error ());
482 push ctxt (Cic_term term)
484 let typ = pop_cic ctxt in
485 let term = pop_cic ctxt in
487 (match pop_tag_attrs ctxt with
489 | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
490 | _ -> attribute_error ()));
493 (match pop_tag_attrs ctxt with
494 | ["id", id] -> Cic.AImplicit (id, None)
495 | ["annotation", annotation; "id", id] ->
496 let implicit_annotation =
497 match annotation with
498 | "closed" -> `Closed
501 | _ -> parse_error "invalid value for \"annotation\" attribute"
503 Cic.AImplicit (id, Some implicit_annotation)
504 | _ -> attribute_error ()))
506 let meta_substs = pop_meta_substs ctxt in
508 (match pop_tag_attrs ctxt with
509 | ["id", id; "no", no]
510 | ["id", id; "no", no; "sort", _] ->
511 Cic.AMeta (id, int_of_string no, meta_substs)
512 | _ -> attribute_error ()));
515 (match pop_tag_attrs ctxt with
516 | ["id", id; "noType", noType; "uri", uri] ->
517 Cic.AMutInd (id, uri_of_string uri, int_of_string noType, [])
518 | _ -> attribute_error ()));
521 (match pop_tag_attrs ctxt with
522 | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri]
523 | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
525 Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
526 int_of_string noConstr, [])
527 | _ -> attribute_error ()));
529 let body = pop_cic ctxt in
530 let typ = pop_cic ctxt in
532 (match pop_tag_attrs ctxt with
533 | ["id", id; "name", name; "recIndex", recIndex] ->
534 Fix_fun (id, name, int_of_string recIndex, typ, body)
535 | _ -> attribute_error ())
537 let body = pop_cic ctxt in
538 let typ = pop_cic ctxt in
540 (match pop_tag_attrs ctxt with
541 | ["id", id; "name", name] ->
542 Cofix_fun (id, name, typ, body)
543 | _ -> attribute_error ())
545 let fix_funs = pop_fix_funs ctxt in
547 (match pop_tag_attrs ctxt with
548 | ["id", id; "noFun", noFun]
549 | ["id", id; "noFun", noFun; "sort", _] ->
550 Cic.AFix (id, int_of_string noFun, fix_funs)
551 | _ -> attribute_error ()))
553 let cofix_funs = pop_cofix_funs ctxt in
555 (match pop_tag_attrs ctxt with
556 | ["id", id; "noFun", noFun]
557 | ["id", id; "noFun", noFun; "sort", _] ->
558 Cic.ACoFix (id, int_of_string noFun, cofix_funs)
559 | _ -> attribute_error ()))
561 (match pop_cics ctxt with
562 | patternsType :: inductiveTerm :: patterns ->
564 (match pop_tag_attrs ctxt with
565 | ["id", id; "noType", noType; "uriType", uriType]
566 | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
567 Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
568 patternsType, inductiveTerm, patterns)
569 | _ -> attribute_error ()))
570 | _ -> parse_error "invalid \"MUTCASE\" content")
572 let typ = pop_cic ctxt in
574 (match pop_tag_attrs ctxt with
575 | ["name", name] -> Constructor (name, typ)
576 | _ -> attribute_error ())
578 let constructors = pop_constructors ctxt in
579 let arity = pop_cic ctxt in
581 (match pop_tag_attrs ctxt with
582 | ["id", id; "inductive", inductive; "name", name] ->
583 Inductive_type (id, name, bool_of_string inductive, arity,
585 | _ -> attribute_error ())
586 | "InductiveDefinition" ->
587 let inductive_types = pop_inductive_types ctxt in
588 let obj_attributes = pop_obj_attributes ctxt in
590 (match pop_tag_attrs ctxt with
591 | ["id", id; "noParams", noParams; "params", params] ->
592 Cic.AInductiveDefinition (id, inductive_types,
593 uri_list_of_string params, int_of_string noParams, obj_attributes)
594 | _ -> attribute_error ()))
596 let typ = pop_cic ctxt in
597 let obj_attributes = pop_obj_attributes ctxt in
599 (match pop_tag_attrs ctxt with
600 | ["id", id; "name", name; "params", params] ->
601 Cic_constant_type (id, name, uri_list_of_string params, typ,
603 | _ -> attribute_error ())
605 let body = pop_cic ctxt in
606 let obj_attributes = pop_obj_attributes ctxt in
608 (match pop_tag_attrs ctxt with
609 | ["for", for_; "id", id; "params", params] ->
610 Cic_constant_body (id, for_, uri_list_of_string params, body,
612 | _ -> attribute_error ())
614 let typ = pop_cic ctxt in
616 match pop_cics ctxt with
619 | _ -> parse_error "wrong content for \"Variable\""
621 let obj_attributes = pop_obj_attributes ctxt in
623 (match pop_tag_attrs ctxt with
624 | ["id", id; "name", name; "params", params] ->
625 Cic.AVariable (id, name, body, typ, uri_list_of_string params,
627 | _ -> attribute_error ()))
629 let term = pop_cic ctxt in
631 (match pop_tag_attrs ctxt with
632 | ["relUri", relUri] -> Arg (relUri, term)
633 | _ -> attribute_error ())
635 (* explicit named substitution handling: when the end tag of an element
636 * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it
637 * is stored on the stack with no substitutions (i.e. []). When the end
638 * tag of an "instantiate" element is found we patch the term currently
639 * on the stack with the substitution built from "instantiate" children
641 (* XXX inefficiency here: first travels the <arg> elements in order to
642 * find the baseUri, then in order to build the explicit named subst *)
643 let base_uri = find_base_uri ctxt in
644 let subst = pop_subst ctxt base_uri in
645 let term = pop_cic ctxt in
646 (* comment from CicParser3.ml:
647 * CSC: the "id" optional attribute should be parsed and reflected in
648 * Cic.annterm and id = string_of_xml_attr (n#attribute "id") *)
649 (* replace <instantiate> *)
650 set_top ctxt (Cic_term (patch_subst ctxt subst term))
652 let rec aux acc = function (* retrieve object attributes *)
653 | Obj_class c :: tl -> aux (`Class c :: acc) tl
654 | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
655 | Obj_generated :: tl -> aux (`Generated :: acc) tl
658 let obj_attrs, new_stack = aux [] ctxt.stack in
659 ctxt.stack <- new_stack;
660 set_top ctxt (Cic_attributes obj_attrs)
661 | "generated" -> set_top ctxt Obj_generated
664 (match pop_tag_attrs ctxt with
665 | ["name", name] -> Obj_field name
666 | _ -> attribute_error ())
669 (match pop_tag_attrs ctxt with
670 | [ "value", "definition"] -> Obj_flavour `Definition
671 | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
672 | [ "value", "fact"] -> Obj_flavour `Fact
673 | [ "value", "lemma"] -> Obj_flavour `Lemma
674 | [ "value", "remark"] -> Obj_flavour `Remark
675 | [ "value", "theorem"] -> Obj_flavour `Theorem
676 | [ "value", "variant"] -> Obj_flavour `Variant
677 | [ "value", "axiom"] -> Obj_flavour `Axiom
678 | _ -> attribute_error ())
680 let class_modifiers = pop_class_modifiers ctxt in
682 (match pop_tag_attrs ctxt with
683 | ["value", "coercion"] -> Obj_class (`Coercion 0)
684 | ("value", "coercion")::["arity",n]
685 | ("arity",n)::["value", "coercion"] ->
686 let arity = try int_of_string n with Failure _ ->
687 parse_error "\"arity\" must be an integer"
689 Obj_class (`Coercion arity)
690 | ["value", "elim"] ->
691 (match class_modifiers with
692 | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
695 "unexpected extra content for \"elim\" object class")
696 | ["value", "record"] ->
701 (match Str.split (Str.regexp " ") name with
702 | [name] -> name, false, 0
703 | [name;"coercion"] -> name,true,0
704 | [name;"coercion"; n] ->
708 parse_error "int expected after \"coercion\""
713 "wrong \"field\"'s name attribute")
716 "unexpected extra content for \"record\" object class")
719 Obj_class (`Record fields)
720 | ["value", "projection"] -> Obj_class `Projection
721 | ["value", "inversion"] -> Obj_class `InversionPrinciple
722 | _ -> attribute_error ())
724 match find_helm_exception ctxt with
725 | Some (exn, arg) -> raise (Getter_failure (exn, arg))
726 | None -> parse_error (sprintf "unknown element \"%s\"" tag)
728 (** {2 Parser internals} *)
730 let has_gz_suffix fname =
732 let idx = String.rindex fname '.' in
733 let suffix = String.sub fname idx (String.length fname - idx) in
735 with Not_found -> false
737 let parse uri filename =
738 let ctxt = new_parser_context uri in
739 ctxt.filename <- filename;
740 let module P = XmlPushParser in
742 P.default_callbacks with
743 P.start_element = Some (start_element ctxt);
744 P.end_element = Some (end_element ctxt);
746 let xml_parser = P.create_parser callbacks in
747 ctxt.xml_parser <- Some xml_parser;
751 if has_gz_suffix filename then `Gzip_file filename
754 P.parse xml_parser xml_source
756 ctxt.xml_parser <- None;
757 (* ZACK: the above "<- None" is vital for garbage collection. Without it
758 * we keep in memory a circular structure parser -> callbacks -> ctxt ->
759 * parser. I don't know if the ocaml garbage collector is supposed to
760 * collect such structures, but for sure the expat bindings will (orribly)
761 * leak when used in conjunction with such structures *)
763 ctxt.xml_parser <- None; (* ZACK: same comment as above *)
764 (* debug_print (lazy (string_of_stack stack));*)
765 (* assert (List.length ctxt.stack = 1) *)
768 | Failure "int_of_string" -> parse_error ctxt "integer number expected"
769 | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
770 | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
773 | Getter_failure _ as exn ->
776 raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn))
778 (** {2 API implementation} *)
780 let annobj_of_xml uri filename filenamebody =
781 match filenamebody with
783 (match parse uri filename with
784 | Cic_constant_type (id, name, params, typ, obj_attributes) ->
785 Cic.AConstant (id, None, name, None, typ, params, obj_attributes)
787 | _ -> raise (Parser_failure ("no object found in " ^ filename)))
788 | Some filenamebody ->
789 (match parse uri filename, parse uri filenamebody with
790 | Cic_constant_type (type_id, name, params, typ, obj_attributes),
791 Cic_constant_body (body_id, _, _, body, _) ->
792 Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,obj_attributes)
794 raise (Parser_failure (sprintf "no constant found in %s, %s"
795 filename filenamebody)))
797 let obj_of_xml uri filename filenamebody =
798 Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)