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