(* Copyright (C) 2004-2005, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)

open Printf

(* ZACK TODO element from the DTD still to be handled:
   <!ELEMENT CurrentProof (Conjecture*,body)>
   <!ELEMENT Sequent %sequent;>
   <!ELEMENT Conjecture %sequent;>
   <!ELEMENT Decl %term;>
   <!ELEMENT Def %term;>
   <!ELEMENT Hidden EMPTY>
   <!ELEMENT Goal %term;>
*)

exception Getter_failure of string * string
exception Parser_failure of string

type stack_entry =
  | Arg of string * Cic.annterm (* relative uri, term *)
  (* constants' body and types resides in differne files, thus we can't simple
   * keep constants in Cic_obj stack entries *)
  | Cic_attributes of Cic.attribute list
  | Cic_constant_body of string * string * UriManager.uri list * Cic.annterm
      * Cic.attribute list
      (* id, for, params, body, object attributes *)
  | Cic_constant_type of string * string * UriManager.uri list * Cic.annterm
      * Cic.attribute list
      (* id, name, params, type, object attributes *)
  | Cic_term of Cic.annterm (* term *)
  | Cic_obj of Cic.annobj   (* object *)
  | Cofix_fun of Cic.id * string * Cic.annterm * Cic.annterm
      (* id, name, type, body *)
  | Constructor of string * Cic.annterm   (* name, type *)
  | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
  | Def of Cic.id * Cic.name * Cic.annterm  (* id, binder, source *)
  | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
      (* id, name, ind. index, type, body *)
  | Inductive_type of string * string * bool * Cic.annterm *
      (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
  | Meta_subst of Cic.annterm option
  | Obj_class of Cic.object_class
  | Obj_flavour of Cic.object_flavour
  | Obj_field of string (* field name *)
  | Obj_generated
  | Tag of string * (string * string) list  (* tag name, attributes *)
      (* ZACK TODO add file position to tag stack entry so that when attribute
       * errors occur, the position of their _start_tag_ could be printed
       * instead of the current position (usually the end tag) *)

type ctxt = {
  mutable stack: stack_entry list;
  mutable xml_parser: XmlPushParser.xml_parser option;
  mutable filename: string;
  uri: UriManager.uri;
}

let string_of_stack ctxt =
  "[" ^ (String.concat "; "
    (List.map
      (function
      | Arg (reluri, _) -> sprintf "Arg %s" reluri
      | Cic_attributes _ -> "Cic_attributes"
      | Cic_constant_body (id, name, _, _, _) ->
          sprintf "Cic_constant_body %s (id=%s)" name id
      | Cic_constant_type (id, name, _, _, _) ->
          sprintf "Cic_constant_type %s (id=%s)" name id
      | Cic_term _ -> "Cic_term"
      | Cic_obj _ -> "Cic_obj"
      | Constructor (name, _) -> "Constructor " ^ name
      | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
      | Decl (id, _, _) -> sprintf "Decl (id=%s)" id
      | Def (id, _, _) -> sprintf "Def (id=%s)" id
      | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
      | Inductive_type (id, name, _, _, _) ->
          sprintf "Inductive_type %s (id=%s)" name id
      | Meta_subst _ -> "Meta_subst"
      | Obj_class _ -> "Obj_class"
      | Obj_flavour _ -> "Obj_flavour"
      | Obj_field name -> "Obj_field " ^ name
      | Obj_generated -> "Obj_generated"
      | Tag (tag, _) -> "Tag " ^ tag)
      ctxt.stack)) ^ "]"

let compare_attrs (a1, v1) (a2, v2) = Pervasives.compare a1 a2
let sort_attrs = List.sort compare_attrs

let new_parser_context uri = {
  stack = [];
  xml_parser = None;
  filename = "-";
  uri = uri;
}

let get_parser ctxt =
  match ctxt.xml_parser with
  | Some p -> p
  | None -> assert false

(** {2 Error handling} *)

let parse_error ctxt msg =
  let (line, col) = XmlPushParser.get_position (get_parser ctxt) in
  raise (Parser_failure (sprintf "[%s: line %d, column %d] %s"
    ctxt.filename line col msg))

let attribute_error ctxt tag =
  parse_error ctxt ("wrong attribute set for " ^ tag)

(** {2 Parsing context management} *)

let pop ctxt =
(*  debug_print (lazy "pop");*)
  match ctxt.stack with
  | hd :: tl -> (ctxt.stack <- tl)
  | _ -> assert false

let push ctxt v =
(*  debug_print (lazy "push");*)
  ctxt.stack <- v :: ctxt.stack

let set_top ctxt v =
(*  debug_print (lazy "set_top");*)
  match ctxt.stack with
  | _ :: tl -> (ctxt.stack <- v :: tl)
  | _ -> assert false

  (** pop the last tag from the open tags stack returning a pair <tag_name,
   * attribute_list> *)
let pop_tag ctxt =
  match ctxt.stack with
  | Tag (tag, attrs) :: tl ->
      ctxt.stack <- tl;
      (tag, attrs)
  | _ -> parse_error ctxt "unexpected extra content"

  (** pop the last tag from the open tags stack returning its attributes.
   * Attributes are returned as a list of pair <name, value> _sorted_ by
   * attribute name *)
let pop_tag_attrs ctxt = sort_attrs (snd (pop_tag ctxt))

let pop_cics ctxt =
  let rec aux acc stack =
    match stack with
    | Cic_term t :: tl -> aux (t :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_class_modifiers ctxt =
  let rec aux acc stack =
    match stack with
    | (Cic_term (Cic.ASort _) as m) :: tl
    | (Obj_field _ as m) :: tl ->
        aux (m :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_meta_substs ctxt =
  let rec aux acc stack =
    match stack with
    | Meta_subst t :: tl -> aux (t :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_fix_funs ctxt =
  let rec aux acc stack =
    match stack with
    | Fix_fun (id, name, index, typ, body) :: tl ->
        aux ((id, name, index, typ, body) :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_cofix_funs ctxt =
  let rec aux acc stack =
    match stack with
    | Cofix_fun (id, name, typ, body) :: tl ->
        aux ((id, name, typ, body) :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_constructors ctxt =
  let rec aux acc stack =
    match stack with
    | Constructor (name, t) :: tl -> aux ((name, t) :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  ctxt.stack <- new_stack;
  values

let pop_inductive_types ctxt =
  let rec aux acc stack =
    match stack with
    | Inductive_type (id, name, ind, arity, ctors) :: tl ->
        aux ((id, name, ind, arity, ctors) :: acc) tl
    | tl -> acc, tl
  in
  let values, new_stack = aux [] ctxt.stack in
  if values = [] then
    parse_error ctxt "no \"InductiveType\" element found";
  ctxt.stack <- new_stack;
  values

  (** travels the stack (without popping) for the first term subject of explicit
   * named substitution and return its URI *)
let find_base_uri ctxt =
  let rec aux = function
    | Cic_term (Cic.AConst (_, uri, _)) :: _
    | Cic_term (Cic.AMutInd (_, uri, _, _)) :: _
    | Cic_term (Cic.AMutConstruct (_, uri, _, _, _)) :: _
    | Cic_term (Cic.AVar (_, uri, _)) :: _ ->
        uri
    | Arg _ :: tl -> aux tl
    | _ -> parse_error ctxt "no \"arg\" element found"
  in
  UriManager.buri_of_uri (aux ctxt.stack)

  (** backwardly eats the stack building an explicit named substitution from Arg
   * stack entries *)
let pop_subst ctxt base_uri =
  let rec aux acc stack =
    match stack with
    | Arg (rel_uri, term) :: tl ->
        let uri = UriManager.uri_of_string (base_uri ^ "/" ^ rel_uri) in
        aux ((uri, term) :: acc) tl
    | tl -> acc, tl
  in
  let subst, new_stack = aux [] ctxt.stack in
  if subst = [] then
    parse_error ctxt "no \"arg\" element found";
  ctxt.stack <- new_stack;
  subst

let pop_cic ctxt =
  match ctxt.stack with
  | Cic_term t :: tl ->
      ctxt.stack <- tl;
      t
  | _ -> parse_error ctxt "no cic term found"

let pop_obj_attributes ctxt =
  match ctxt.stack with
  | Cic_attributes attributes :: tl ->
      ctxt.stack <- tl;
      attributes
  | _ -> []

(** {2 Auxiliary functions} *)

let uri_of_string = UriManager.uri_of_string

let uri_list_of_string =
  let space_RE = Str.regexp " " in
  fun s ->
    List.map uri_of_string (Str.split space_RE s)

let sort_of_string ctxt = function
  | "Prop" -> Cic.Prop
  | "Set"  -> Cic.Set
  | "CProp" -> Cic.CProp
  (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
   * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION 
   * IS FIXED *)
  | "Type" ->  Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
  | s ->
      let len = String.length s in
      if not(len > 5) then parse_error ctxt "sort expected";
      if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
      try 
        Cic.Type 
          (CicUniv.fresh 
            ~uri:ctxt.uri 
            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
      with
      | Failure "int_of_string" 
      | Invalid_argument _ -> parse_error ctxt "sort expected" 

let patch_subst ctxt subst = function
  | Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
  | Cic.AMutInd (id, uri, typeno, _) ->
      Cic.AMutInd (id, uri, typeno, subst)
  | Cic.AMutConstruct (id, uri, typeno, consno, _) ->
      Cic.AMutConstruct (id, uri, typeno, consno, subst)
  | Cic.AVar (id, uri, _) -> Cic.AVar (id, uri, subst)
  | _ ->
      parse_error ctxt
        ("only \"CONST\", \"VAR\", \"MUTIND\", and \"MUTCONSTRUCT\" can be" ^
        " instantiated")

  (** backwardly eats the stack seeking for the first open tag carrying
   * "helm:exception" attributes. If found return Some of a pair containing
   * exception name and argument. Return None otherwise *)
let find_helm_exception ctxt =
  let rec aux = function
    | [] -> None
    | Tag (_, attrs) :: tl ->
        (try
          let exn = List.assoc "helm:exception" attrs in
          let arg =
            try List.assoc "helm:exception_arg" attrs with Not_found -> ""
          in
          Some (exn, arg)
        with Not_found -> aux tl)
    | _ :: tl -> aux tl
  in
  aux ctxt.stack

(** {2 Push parser callbacks}
 * each callback needs to be instantiated to a parsing context *)

let start_element ctxt tag attrs =
(*  debug_print (lazy (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs))));*)
  push ctxt (Tag (tag, attrs))

let end_element ctxt tag =
(*  debug_print (lazy (sprintf "</%s>" tag));*)
(*  debug_print (lazy (string_of_stack ctxt));*)
  let attribute_error () = attribute_error ctxt tag in
  let parse_error = parse_error ctxt in
  let sort_of_string = sort_of_string ctxt in
  match tag with
  | "REL" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["binder", binder; "id", id; "idref", idref; "value", value]
        | ["binder", binder; "id", id; "idref", idref; "sort", _;
           "value", value] ->
            Cic.ARel (id, idref, int_of_string value, binder)
        | _ -> attribute_error ()))
  | "VAR" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "uri", uri]
        | ["id", id; "sort", _; "uri", uri] ->
            Cic.AVar (id, uri_of_string uri, [])
        | _ -> attribute_error ()))
  | "CONST" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "uri", uri]
        | ["id", id; "sort", _; "uri", uri] ->
            Cic.AConst (id, uri_of_string uri, [])
        | _ -> attribute_error ()))
  | "SORT" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "value", sort] -> Cic.ASort (id, sort_of_string sort)
        | _ -> attribute_error ()))
  | "APPLY" ->
      let args = pop_cics ctxt in
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id ]
        | ["id", id; "sort", _] -> Cic.AAppl (id, args)
        | _ -> attribute_error ()))
  | "decl" ->
      let source = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["binder", binder; "id", id ]
        | ["binder", binder; "id", id; "type", _] ->
            Decl (id, Cic.Name binder, source)
        | ["id", id]
        | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
        | _ -> attribute_error ())
  | "def" ->  (* same as "decl" above *)
      let source = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["binder", binder; "id", id]
        | ["binder", binder; "id", id; "sort", _] ->
            Def (id, Cic.Name binder, source)
        | ["id", id]
        | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
        | _ -> attribute_error ())
  | "arity"           (* transparent elements (i.e. which contain a CIC) *)
  | "body"
  | "inductiveTerm"
  | "pattern"
  | "patternsType"
  | "target"
  | "term"
  | "type" ->
      let term = pop_cic ctxt in
      pop ctxt; (* pops start tag matching current end tag (e.g. <arity>) *)
      push ctxt (Cic_term term)
  | "substitution" ->   (* optional transparent elements (i.e. which _may_
                         * contain a CIC) *)
      set_top ctxt  (* replace <substitution> *)
        (match ctxt.stack with
        | Cic_term term :: tl ->
            ctxt.stack <- tl;
            (Meta_subst (Some term))
        | _ ->  Meta_subst None)
  | "PROD" ->
      let target = pop_cic ctxt in
      let rec add_decl target = function
        | Decl (id, binder, source) :: tl ->
            add_decl (Cic.AProd (id, binder, source, target)) tl
        | tl ->
            ctxt.stack <- tl;
            target
      in
      let term = add_decl target ctxt.stack in
      (match pop_tag_attrs ctxt with
        []
      | ["type", _] -> ()
      | _ -> attribute_error ());
      push ctxt (Cic_term term)
  | "LAMBDA" ->
      let target = pop_cic ctxt in
      let rec add_decl target = function
        | Decl (id, binder, source) :: tl ->
            add_decl (Cic.ALambda (id, binder, source, target)) tl
        | tl ->
            ctxt.stack <- tl;
            target
      in
      let term = add_decl target ctxt.stack in
      (match pop_tag_attrs ctxt with
        []
      | ["sort", _] -> ()
      | _ -> attribute_error ());
      push ctxt (Cic_term term)
  | "LETIN" ->
      let target = pop_cic ctxt in
      let rec add_def target = function
        | Def (id, binder, source) :: tl ->
            add_def (Cic.ALetIn (id, binder, source, target)) tl
        | tl ->
            ctxt.stack <- tl;
            target
      in
      let term = add_def target ctxt.stack in
      (match pop_tag_attrs ctxt with
        []
      | ["sort", _] -> ()
      | _ -> attribute_error ());
      push ctxt (Cic_term term)
  | "CAST" ->
      let typ = pop_cic ctxt in
      let term = pop_cic ctxt in
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
          ["id", id]
        | ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
        | _ -> attribute_error ()));
  | "IMPLICIT" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id] -> Cic.AImplicit (id, None)
        | ["annotation", annotation; "id", id] ->
            let implicit_annotation =
              match annotation with
              | "closed" -> `Closed
              | "hole" -> `Hole
              | "type" -> `Type
              | _ -> parse_error "invalid value for \"annotation\" attribute"
            in
            Cic.AImplicit (id, Some implicit_annotation)
        | _ -> attribute_error ()))
  | "META" ->
      let meta_substs = pop_meta_substs ctxt in
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "no", no]
        | ["id", id; "no", no; "sort", _] ->
            Cic.AMeta (id, int_of_string no, meta_substs)
        | _ -> attribute_error ()));
  | "MUTIND" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "noType", noType; "uri", uri] ->
            Cic.AMutInd (id, uri_of_string uri, int_of_string noType, [])
        | _ -> attribute_error ()));
  | "MUTCONSTRUCT" ->
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri]
        | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
           "uri", uri] ->
            Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
              int_of_string noConstr, [])
        | _ -> attribute_error ()));
  | "FixFunction" ->
      let body = pop_cic ctxt in
      let typ = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["id", id; "name", name; "recIndex", recIndex] ->
            Fix_fun (id, name, int_of_string recIndex, typ, body)
        | _ -> attribute_error ())
  | "CofixFunction" ->
      let body = pop_cic ctxt in
      let typ = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["id", id; "name", name] ->
            Cofix_fun (id, name, typ, body)
        | _ -> attribute_error ())
  | "FIX" ->
      let fix_funs = pop_fix_funs ctxt in
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "noFun", noFun]
        | ["id", id; "noFun", noFun; "sort", _] ->
            Cic.AFix (id, int_of_string noFun, fix_funs)
        | _ -> attribute_error ()))
  | "COFIX" ->
      let cofix_funs = pop_cofix_funs ctxt in
      push ctxt (Cic_term
        (match pop_tag_attrs ctxt with
        | ["id", id; "noFun", noFun]
        | ["id", id; "noFun", noFun; "sort", _] ->
            Cic.ACoFix (id, int_of_string noFun, cofix_funs)
        | _ -> attribute_error ()))
  | "MUTCASE" ->
      (match pop_cics ctxt with
      | patternsType :: inductiveTerm :: patterns ->
          push ctxt (Cic_term
            (match pop_tag_attrs ctxt with
            | ["id", id; "noType", noType; "uriType", uriType]
            | ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
                Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
                  patternsType, inductiveTerm, patterns)
            | _ -> attribute_error ()))
      | _ -> parse_error "invalid \"MUTCASE\" content")
  | "Constructor" ->
      let typ = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["name", name] -> Constructor (name, typ)
        | _ -> attribute_error ())
  | "InductiveType" ->
      let constructors = pop_constructors ctxt in
      let arity = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["id", id; "inductive", inductive; "name", name] ->
            Inductive_type (id, name, bool_of_string inductive, arity,
              constructors)
        | _ -> attribute_error ())
  | "InductiveDefinition" ->
      let inductive_types = pop_inductive_types ctxt in
      let obj_attributes = pop_obj_attributes ctxt in
      push ctxt (Cic_obj
        (match pop_tag_attrs ctxt with
        | ["id", id; "noParams", noParams; "params", params] ->
            Cic.AInductiveDefinition (id, inductive_types,
              uri_list_of_string params, int_of_string noParams, obj_attributes)
        | _ -> attribute_error ()))
  | "ConstantType" ->
      let typ = pop_cic ctxt in
      let obj_attributes = pop_obj_attributes ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["id", id; "name", name; "params", params] ->
            Cic_constant_type (id, name, uri_list_of_string params, typ,
              obj_attributes)
        | _ -> attribute_error ())
  | "ConstantBody" ->
      let body = pop_cic ctxt in
      let obj_attributes = pop_obj_attributes ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["for", for_; "id", id; "params", params] ->
            Cic_constant_body (id, for_, uri_list_of_string params, body,
              obj_attributes)
        | _ -> attribute_error ())
  | "Variable" ->
      let typ = pop_cic ctxt in
      let body =
        match pop_cics ctxt with
        | [] -> None
        | [t] -> Some t
        | _ -> parse_error "wrong content for \"Variable\""
      in
      let obj_attributes = pop_obj_attributes ctxt in
      push ctxt (Cic_obj
        (match pop_tag_attrs ctxt with
        | ["id", id; "name", name; "params", params] ->
            Cic.AVariable (id, name, body, typ, uri_list_of_string params,
              obj_attributes)
        | _ -> attribute_error ()))
  | "arg" ->
      let term = pop_cic ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["relUri", relUri] -> Arg (relUri, term)
        | _ -> attribute_error ())
  | "instantiate" ->
        (* explicit named substitution handling: when the end tag of an element
         * subject of exlicit named subst (MUTIND, MUTCONSTRUCT, CONST, VAR) it
         * is stored on the stack with no substitutions (i.e. []). When the end
         * tag of an "instantiate" element is found we patch the term currently
         * on the stack with the substitution built from "instantiate" children
         *)
        (* XXX inefficiency here: first travels the <arg> elements in order to
         * find the baseUri, then in order to build the explicit named subst *)
      let base_uri = find_base_uri ctxt in
      let subst = pop_subst ctxt base_uri in
      let term = pop_cic ctxt in
        (* comment from CicParser3.ml:
         * CSC: the "id" optional attribute should be parsed and reflected in
         *      Cic.annterm and id = string_of_xml_attr (n#attribute "id") *)
        (* replace <instantiate> *)
      set_top ctxt (Cic_term (patch_subst ctxt subst term))
  | "attributes" ->
      let rec aux acc = function  (* retrieve object attributes *)
        | Obj_class c :: tl -> aux (`Class c :: acc) tl
        | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
        | Obj_generated :: tl -> aux (`Generated :: acc) tl
        | tl -> acc, tl
      in
      let obj_attrs, new_stack = aux [] ctxt.stack in
      ctxt.stack <- new_stack;
      set_top ctxt (Cic_attributes obj_attrs)
  | "generated" -> set_top ctxt Obj_generated
  | "field" ->
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["name", name] -> Obj_field name
        | _ -> attribute_error ())
  | "flavour" ->
      push ctxt 
        (match pop_tag_attrs ctxt with
        | [ "value", "definition"] -> Obj_flavour `Definition
        | [ "value", "fact"] -> Obj_flavour `Fact
        | [ "value", "lemma"] -> Obj_flavour `Lemma
        | [ "value", "remark"] -> Obj_flavour `Remark
        | [ "value", "theorem"] -> Obj_flavour `Theorem
        | [ "value", "variant"] -> Obj_flavour `Variant
        | _ -> attribute_error ())
  | "class" ->
      let class_modifiers = pop_class_modifiers ctxt in
      push ctxt
        (match pop_tag_attrs ctxt with
        | ["value", "coercion"] -> Obj_class `Coercion
        | ["value", "elim"] ->
            (match class_modifiers with
            | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
            | _ ->
                parse_error
                  "unexpected extra content for \"elim\" object class")
        | ["value", "record"] ->
            let fields =
              List.map
                (function
                  | Obj_field name -> name
                  | _ ->
                      parse_error
                        "unexpected extra content for \"record\" object class")
                class_modifiers
            in
            Obj_class (`Record fields)
        | ["value", "projection"] -> Obj_class `Projection
        | _ -> attribute_error ())
  | tag ->
      match find_helm_exception ctxt with
      | Some (exn, arg) -> raise (Getter_failure (exn, arg))
      | None -> parse_error (sprintf "unknown element \"%s\"" tag)

(** {2 Parser internals} *)

let has_gz_suffix fname =
  try
    let idx = String.rindex fname '.' in
    let suffix = String.sub fname idx (String.length fname - idx) in
    suffix = ".gz"
  with Not_found -> false

let parse uri filename =
  let ctxt = new_parser_context uri in
  ctxt.filename <- filename;
  let module P = XmlPushParser in
  let callbacks = {
    P.default_callbacks with
      P.start_element = Some (start_element ctxt);
      P.end_element = Some (end_element ctxt);
  } in
  let xml_parser = P.create_parser callbacks in
  ctxt.xml_parser <- Some xml_parser;
  try
    (try
      let xml_source =
        if has_gz_suffix filename then `Gzip_file filename
        else `File filename
      in
      P.parse xml_parser xml_source
    with exn ->
      ctxt.xml_parser <- None;
      (* ZACK: the above "<- None" is vital for garbage collection. Without it
       * we keep in memory a circular structure parser -> callbacks -> ctxt ->
       * parser. I don't know if the ocaml garbage collector is supposed to
       * collect such structures, but for sure the expat bindings will (orribly)
       * leak when used in conjunction with such structures *)
      raise exn);
    ctxt.xml_parser <- None; (* ZACK: same comment as above *)
(*    debug_print (lazy (string_of_stack stack));*)
    (* assert (List.length ctxt.stack = 1) *)
    List.hd ctxt.stack
  with
  | Failure "int_of_string" -> parse_error ctxt "integer number expected"
  | Invalid_argument "bool_of_string" -> parse_error ctxt "boolean expected"
  | P.Parse_error msg -> parse_error ctxt ("parse error: " ^ msg)
  | Parser_failure _
  | Getter_failure _ as exn ->
      raise exn
  | exn ->
      raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))

(** {2 API implementation} *)

let annobj_of_xml uri filename filenamebody =
  match filenamebody with
  | None ->
      (match parse uri filename with
      | Cic_constant_type (id, name, params, typ, obj_attributes) ->
          Cic.AConstant (id, None, name, None, typ, params, obj_attributes)
      | Cic_obj obj -> obj
      | _ -> raise (Parser_failure ("no object found in " ^ filename)))
  | Some filenamebody ->
      (match parse uri filename, parse uri filenamebody with
      | Cic_constant_type (type_id, name, params, typ, obj_attributes),
        Cic_constant_body (body_id, _, _, body, _) ->
          Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[])
      | _ ->
          raise (Parser_failure (sprintf "no constant found in %s, %s"
            filename filenamebody)))

let obj_of_xml uri filename filenamebody =
 Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)