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