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