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