components/cic/cicParser.ml

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