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; "sort", _;
 353            "value", value] ->
 354             Cic.ARel (id, idref, int_of_string value, binder)
 355         | _ -> attribute_error ()))
 356   | "VAR" ->
 357       push ctxt (Cic_term
 358         (match pop_tag_attrs ctxt with
 359         | ["id", id; "sort", _; "uri", uri] ->
 360             Cic.AVar (id, uri_of_string uri, [])
 361         | _ -> attribute_error ()))
 362   | "CONST" ->
 363       push ctxt (Cic_term
 364         (match pop_tag_attrs ctxt with
 365         | ["id", id; "sort", _; "uri", uri] ->
 366             Cic.AConst (id, uri_of_string uri, [])
 367         | _ -> attribute_error ()))
 368   | "SORT" ->
 369       push ctxt (Cic_term
 370         (match pop_tag_attrs ctxt with
 371         | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort)
 372         | _ -> attribute_error ()))
 373   | "APPLY" ->
 374       let args = pop_cics ctxt in
 375       push ctxt (Cic_term
 376         (match pop_tag_attrs ctxt with
 377         | ["id", id; "sort", _] -> Cic.AAppl (id, args)
 378         | _ -> attribute_error ()))
 379   | "decl" ->
 380       let source = pop_cic ctxt in
 381       push ctxt
 382         (match pop_tag_attrs ctxt with
 383         | ["binder", binder; "id", id; "type", _] ->
 384             Decl (id, Cic.Name binder, source)
 385         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
 386         | _ -> attribute_error ())
 387   | "def" ->  (* same as "decl" above *)
 388       let source = pop_cic ctxt in
 389       push ctxt
 390         (match pop_tag_attrs ctxt with
 391         | ["binder", binder; "id", id; "sort", _] ->
 392             Def (id, Cic.Name binder, source)
 393         | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
 394         | _ -> attribute_error ())
 395   | "arity"           (* transparent elements (i.e. which contain a CIC) *)
 396   | "body"
 397   | "inductiveTerm"
 398   | "pattern"
 399   | "patternsType"
 400   | "target"
 401   | "term"
 402   | "type" ->
 403       let term = pop_cic ctxt in
 404       pop ctxt; (* pops start tag matching current end tag (e.g. <arity>) *)
 405       push ctxt (Cic_term term)
 406   | "substitution" ->   (* optional transparent elements (i.e. which _may_
 407                          * contain a CIC) *)
 408       set_top ctxt  (* replace <substitution> *)
 409         (match ctxt.stack with
 410         | Cic_term term :: tl ->
 411             ctxt.stack <- tl;
 412             (Meta_subst (Some term))
 413         | _ ->  Meta_subst None)
 414   | "PROD" ->
 415       let target = pop_cic ctxt in
 416       let rec add_decl target = function
 417         | Decl (id, binder, source) :: tl ->
 418             add_decl (Cic.AProd (id, binder, source, target)) tl
 419         | tl ->
 420             ctxt.stack <- tl;
 421             target
 422       in
 423       let term = add_decl target ctxt.stack in
 424       (match pop_tag_attrs ctxt with
 425       | ["type", _] -> ()
 426       | _ -> attribute_error ());
 427       push ctxt (Cic_term term)
 428   | "LAMBDA" ->
 429       let target = pop_cic ctxt in
 430       let rec add_decl target = function
 431         | Decl (id, binder, source) :: tl ->
 432             add_decl (Cic.ALambda (id, binder, source, target)) tl
 433         | tl ->
 434             ctxt.stack <- tl;
 435             target
 436       in
 437       let term = add_decl target ctxt.stack in
 438       (match pop_tag_attrs ctxt with
 439       | ["sort", _] -> ()
 440       | _ -> attribute_error ());
 441       push ctxt (Cic_term term)
 442   | "LETIN" ->
 443       let target = pop_cic ctxt in
 444       let rec add_def target = function
 445         | Def (id, binder, source) :: tl ->
 446             add_def (Cic.ALetIn (id, binder, source, target)) tl
 447         | tl ->
 448             ctxt.stack <- tl;
 449             target
 450       in
 451       let term = add_def target ctxt.stack in
 452       (match pop_tag_attrs ctxt with
 453       | ["sort", _] -> ()
 454       | _ -> attribute_error ());
 455       push ctxt (Cic_term term)
 456   | "CAST" ->
 457       let typ = pop_cic ctxt in
 458       let term = pop_cic ctxt in
 459       push ctxt (Cic_term
 460         (match pop_tag_attrs ctxt with
 461         | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
 462         | _ -> attribute_error ()));
 463   | "IMPLICIT" ->
 464       push ctxt (Cic_term
 465         (match pop_tag_attrs ctxt with
 466         | ["id", id] -> Cic.AImplicit (id, None)
 467         | ["annotation", annotation; "id", id] ->
 468             let implicit_annotation =
 469               match annotation with
 470               | "closed" -> `Closed
 471               | "hole" -> `Hole
 472               | "type" -> `Type
 473               | _ -> parse_error "invalid value for \"annotation\" attribute"
 474             in
 475             Cic.AImplicit (id, Some implicit_annotation)
 476         | _ -> attribute_error ()))
 477   | "META" ->
 478       let meta_substs = pop_meta_substs ctxt in
 479       push ctxt (Cic_term
 480         (match pop_tag_attrs ctxt with
 481         | ["id", id; "no", no; "sort", _] ->
 482             Cic.AMeta (id, int_of_string no, meta_substs)
 483         | _ -> attribute_error ()));
 484   | "MUTIND" ->
 485       push ctxt (Cic_term
 486         (match pop_tag_attrs ctxt with
 487         | ["id", id; "noType", noType; "uri", uri] ->
 488             Cic.AMutInd (id, uri_of_string uri, int_of_string noType, [])
 489         | _ -> attribute_error ()));
 490   | "MUTCONSTRUCT" ->
 491       push ctxt (Cic_term
 492         (match pop_tag_attrs ctxt with
 493         | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
 494            "uri", uri] ->
 495             Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
 496               int_of_string noConstr, [])
 497         | _ -> attribute_error ()));
 498   | "FixFunction" ->
 499       let body = pop_cic ctxt in
 500       let typ = pop_cic ctxt in
 501       push ctxt
 502         (match pop_tag_attrs ctxt with
 503         | ["id", id; "name", name; "recIndex", recIndex] ->
 504             Fix_fun (id, name, int_of_string recIndex, typ, body)
 505         | _ -> attribute_error ())
 506   | "CofixFunction" ->
 507       let body = pop_cic ctxt in
 508       let typ = pop_cic ctxt in
 509       push ctxt
 510         (match pop_tag_attrs ctxt with
 511         | ["id", id; "name", name] ->
 512             Cofix_fun (id, name, typ, body)
 513         | _ -> attribute_error ())
 514   | "FIX" ->
 515       let fix_funs = pop_fix_funs ctxt in
 516       push ctxt (Cic_term
 517         (match pop_tag_attrs ctxt with
 518         | ["id", id; "noFun", noFun; "sort", _] ->
 519             Cic.AFix (id, int_of_string noFun, fix_funs)
 520         | _ -> attribute_error ()))
 521   | "COFIX" ->
 522       let cofix_funs = pop_cofix_funs ctxt in
 523       push ctxt (Cic_term
 524         (match pop_tag_attrs ctxt with
 525         | ["id", id; "noFun", noFun; "sort", _] ->
 526             Cic.ACoFix (id, int_of_string noFun, cofix_funs)
 527         | _ -> attribute_error ()))
 528   | "MUTCASE" ->
 529       (match pop_cics ctxt with
 530       | patternsType :: inductiveTerm :: patterns ->
 531           push ctxt (Cic_term
 532             (match pop_tag_attrs ctxt with
 533             | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
 534                 Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
 535                   patternsType, inductiveTerm, patterns)
 536             | _ -> attribute_error ()))
 537       | _ -> parse_error "invalid \"MUTCASE\" content")
 538   | "Constructor" ->
 539       let typ = pop_cic ctxt in
 540       push ctxt
 541         (match pop_tag_attrs ctxt with
 542         | ["name", name] -> Constructor (name, typ)
 543         | _ -> attribute_error ())
 544   | "InductiveType" ->
 545       let constructors = pop_constructors ctxt in
 546       let arity = pop_cic ctxt in
 547       push ctxt
 548         (match pop_tag_attrs ctxt with
 549         | ["id", id; "inductive", inductive; "name", name] ->
 550             Inductive_type (id, name, bool_of_string inductive, arity,
 551               constructors)
 552         | _ -> attribute_error ())
 553   | "InductiveDefinition" ->
 554       let inductive_types = pop_inductive_types ctxt in
 555       let obj_attributes = pop_obj_attributes ctxt in
 556       push ctxt (Cic_obj
 557         (match pop_tag_attrs ctxt with
 558         | ["id", id; "noParams", noParams; "params", params] ->
 559             Cic.AInductiveDefinition (id, inductive_types,
 560               uri_list_of_string params, int_of_string noParams, obj_attributes)
 561         | _ -> attribute_error ()))
 562   | "ConstantType" ->
 563       let typ = pop_cic ctxt in
 564       let obj_attributes = pop_obj_attributes ctxt in
 565       push ctxt
 566         (match pop_tag_attrs ctxt with
 567         | ["id", id; "name", name; "params", params] ->
 568             Cic_constant_type (id, name, uri_list_of_string params, typ,
 569               obj_attributes)
 570         | _ -> attribute_error ())
 571   | "ConstantBody" ->
 572       let body = pop_cic ctxt in
 573       let obj_attributes = pop_obj_attributes ctxt in
 574       push ctxt
 575         (match pop_tag_attrs ctxt with
 576         | ["for", for_; "id", id; "params", params] ->
 577             Cic_constant_body (id, for_, uri_list_of_string params, body,
 578               obj_attributes)
 579         | _ -> attribute_error ())
 580   | "Variable" ->
 581       let typ = pop_cic ctxt in
 582       let body =
 583         match pop_cics ctxt with
 584         | [] -> None
 585         | [t] -> Some t
 586         | _ -> parse_error "wrong content for \"Variable\""
 587       in
 588       let obj_attributes = pop_obj_attributes ctxt in
 589       push ctxt (Cic_obj
 590         (match pop_tag_attrs ctxt with
 591         | ["id", id; "name", name; "params", params] ->
 592             Cic.AVariable (id, name, body, typ, uri_list_of_string params,
 593               obj_attributes)
 594         | _ -> attribute_error ()))
 595   | "arg" ->
 596       let term = pop_cic ctxt in
 597       push ctxt
 598         (match pop_tag_attrs ctxt with
 599         | ["relUri", relUri] -> Arg (relUri, term)
 600         | _ -> attribute_error ())
 601   | "instantiate" ->
 602         (* explicit named substitution handling: when the end tag of an element
 603          * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it
 604          * is stored on the stack with no substitutions (i.e. []). When the end
 605          * tag of an "instantiate" element is found we patch the term currently
 606          * on the stack with the substitution built from "instantiate" children
 607          *)
 608         (* XXX inefficiency here: first travels the <arg> elements in order to
 609          * find the baseUri, then in order to build the explicit named subst *)
 610       let base_uri = find_base_uri ctxt in
 611       let subst = pop_subst ctxt base_uri in
 612       let term = pop_cic ctxt in
 613         (* comment from CicParser3.ml:
 614          * CSC: the "id" optional attribute should be parsed and reflected in
 615          *      Cic.annterm and id = string_of_xml_attr (n#attribute "id") *)
 616         (* replace <instantiate> *)
 617       set_top ctxt (Cic_term (patch_subst ctxt subst term))
 618   | "attributes" ->
 619       let rec aux acc = function  (* retrieve object attributes *)
 620         | Obj_class c :: tl -> aux (`Class c :: acc) tl
 621         | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
 622         | Obj_generated :: tl -> aux (`Generated :: acc) tl
 623         | tl -> acc, tl
 624       in
 625       let obj_attrs, new_stack = aux [] ctxt.stack in
 626       ctxt.stack <- new_stack;
 627       set_top ctxt (Cic_attributes obj_attrs)
 628   | "generated" -> set_top ctxt Obj_generated
 629   | "field" ->
 630       push ctxt
 631         (match pop_tag_attrs ctxt with
 632         | ["name", name] -> Obj_field name
 633         | _ -> attribute_error ())
 634   | "flavour" ->
 635       push ctxt
 636         (match pop_tag_attrs ctxt with
 637         | [ "value", "definition"] -> Obj_flavour `Definition
 638         | [ "value", "fact"] -> Obj_flavour `Fact
 639         | [ "value", "lemma"] -> Obj_flavour `Lemma
 640         | [ "value", "remark"] -> Obj_flavour `Remark
 641         | [ "value", "theorem"] -> Obj_flavour `Theorem
 642         | [ "value", "variant"] -> Obj_flavour `Variant
 643         | _ -> attribute_error ())
 644   | "class" ->
 645       let class_modifiers = pop_class_modifiers ctxt in
 646       push ctxt
 647         (match pop_tag_attrs ctxt with
 648         | ["value", "coercion"] -> Obj_class `Coercion
 649         | ["value", "elim"] ->
 650             (match class_modifiers with
 651             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
 652             | _ ->
 653                 parse_error
 654                   "unexpected extra content for \"elim\" object class")
 655         | ["value", "record"] ->
 656             let fields =
 657               List.map
 658                 (function
 659                   | Obj_field name -> name
 660                   | _ ->
 661                       parse_error
 662                         "unexpected extra content for \"record\" object class")
 663                 class_modifiers
 664             in
 665             Obj_class (`Record fields)
 666         | ["value", "projection"] -> Obj_class `Projection
 667         | _ -> attribute_error ())
 668   | tag ->
 669       match find_helm_exception ctxt with
 670       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
 671       | None -> parse_error (sprintf "unknown element \"%s\"" tag)
 672
 673 (** {2 Parser internals} *)
 674
 675 let has_gz_suffix fname =
 676   try
 677     let idx = String.rindex fname '.' in
 678     let suffix = String.sub fname idx (String.length fname - idx) in
 679     suffix = ".gz"
 680   with Not_found -> false
 681
 682 let parse uri filename =
 683   let ctxt = new_parser_context uri in
 684   ctxt.filename <- filename;
 685   let module P = XmlPushParser in
 686   let callbacks = {
 687     P.default_callbacks with
 688       P.start_element = Some (start_element ctxt);
 689       P.end_element = Some (end_element ctxt);
 690   } in
 691   let xml_parser = P.create_parser callbacks in
 692   ctxt.xml_parser <- Some xml_parser;
 693   try
 694     (try
 695       let xml_source =
 696         if has_gz_suffix filename then `Gzip_file filename
 697         else `File filename
 698       in
 699       P.parse xml_parser xml_source
 700     with exn ->
 701       ctxt.xml_parser <- None;
 702       (* ZACK: the above "<- None" is vital for garbage collection. Without it
 703        * we keep in memory a circular structure parser -> callbacks -> ctxt ->
 704        * parser. I don't know if the ocaml garbage collector is supposed to
 705        * collect such structures, but for sure the expat bindings will (orribly)
 706        * leak when used in conjunction with such structures *)
 707       raise exn);
 708     ctxt.xml_parser <- None; (* ZACK: same comment as above *)
 709 (*    debug_print (lazy (string_of_stack stack));*)
 710     (* assert (List.length ctxt.stack = 1) *)
 711     List.hd ctxt.stack
 712   with
 713   | Failure "int_of_string" -> parse_error ctxt "integer number expected"
 714   | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
 715   | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
 716   | Parser_failure _
 717   | Getter_failure _ as exn ->
 718       raise exn
 719   | exn ->
 720       raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
 721
 722 (** {2 API implementation} *)
 723
 724 let annobj_of_xml uri filename filenamebody =
 725   match filenamebody with
 726   | None ->
 727       (match parse uri filename with
 728       | Cic_constant_type (id, name, params, typ, obj_attributes) ->
 729           Cic.AConstant (id, None, name, None, typ, params, obj_attributes)
 730       | Cic_obj obj -> obj
 731       | _ -> raise (Parser_failure ("no object found in " ^ filename)))
 732   | Some filenamebody ->
 733       (match parse uri filename, parse uri filenamebody with
 734       | Cic_constant_type (type_id, name, params, typ, obj_attributes),
 735         Cic_constant_body (body_id, _, _, body, _) ->
 736           Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[])
 737       | _ ->
 738           raise (Parser_failure (sprintf "no constant found in %s, %s"
 739             filename filenamebody)))
 740
 741 let obj_of_xml uri filename filenamebody =
 742  Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)