(*********************)
(* Utility functions *)
(*********************)

let fail () =
 Pp.warning "XmlTheory: AST not recognized"
;;

(* name is the name of the function to hook *)
(* hook is an hook partial-function to recognize particular inputs *)
let set_hook name hook =
 let module V = Vernacinterp in
  let old = V.vinterp_map name in
   V.vinterp_add name
    (fun l () ->
      old l () ;
      hook l
    )
;;


(*****************************************************)
(* Vernacular administrative commands for the module *)
(*****************************************************)

let header =
"<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ^
"<!DOCTYPE Theory SYSTEM \"http://www.cs.unibo.it/helm/dtd/maththeory.dtd\">\n"
;;

(*Vecchio, ma funzionante
let module V = Vernacinterp in
 V.vinterp_add "XMLTHEORYBEGIN"
  (function
      [V.VARG_STRING curi ; V.VARG_STRING filename] ->
       fun () ->
        IXml.reset_output filename ;
        IXml.output (Xml.xml_cdata header) ;
        IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi]
    | _ -> V.bad_vernac_args "XMLTHEORYBEGIN"
  )
;;
*)

let module V = Vernacinterp in
let module L = Library in
let module S = System in
let module N = Names in
 V.vinterp_add "XMLTHEORYBEGIN"
  (function
      [V.VARG_IDENTIFIER id ; V.VARG_STRING root_dir] ->
       fun () ->
        let s = N.string_of_id id in
         let lpe,_ =
          S.find_file_in_path (L.get_load_path ()) (s^".v")
         in
          let curi = "/" ^ String.concat "/" lpe.S.coq_dirpath in
          let dirname = root_dir ^ curi in
           Unix.system ("mkdir -p " ^ dirname) ;
          let filename = dirname ^ "/" ^ s ^ ".theory" in
           IXml.reset_output filename ;
           IXml.output (Xml.xml_cdata header) ;
           IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi ^ "/" ^ s]
    | _ -> V.bad_vernac_args "XMLTHEORYBEGIN"
  )
;;

let module V = Vernacinterp in
 V.vinterp_add "XMLTHEORYEND"
  (function
      [] ->
       fun () ->
        IXml.close_non_empty_element () ;
        IXml.print_output ()
    | _ -> V.bad_vernac_args "XMLTHEORYEND"
  )
;;


(**********************************************************)
(* All the vernacular commands on which one is interested *)
(* should be overridden here                              *)
(**********************************************************)

let module V = Vernacinterp in
let module N = Names in
let module S = System in
let module L = Library in
 set_hook "Require"
  (function
      [V.VARG_STRING import; V.VARG_STRING specif; V.VARG_IDENTIFIER id] ->
       (* id is the identifier of the module, but we need the absolute *)
       (* identifier as an URI.                                        *)
       (* E.g.: Logic ==> theory:/Coq/Init/Logic.theory                *)
        let name = N.string_of_id id in
         let ({S.coq_dirpath = coq_dirpath},_) = L.module_filename name in
          let uri =
           "theory:/" ^ (String.concat "/" coq_dirpath) ^ "/" ^ name ^ ".theory"
          in
           IXml.output
            (Xml.xml_nempty "vernacular" []
             (Xml.xml_empty
               "Require"
               ["import",import; "specif",specif; "uri",uri]
             )
            )
    | _ -> fail ()
   )
;;

let module V = Vernacinterp in
let module T = Nametab in
let module N = Names in
 set_hook "HintsResolve"
  (function
      (V.VARG_VARGLIST l)::lh ->
        IXml.output
         (Xml.xml_nempty "vernacular" []
          (Xml.xml_nempty
            "HintsResolve" []
            [< Xml.xml_nempty "dbs" []
                (List.fold_right
                  (function
                      (V.VARG_IDENTIFIER x) ->
                        (function i ->
                          [< Xml.xml_empty "db" ["name",N.string_of_id x];
                             i
                          >]
                        )
                    | _ -> Vernacinterp.bad_vernac_args "HintsResolve"
                  )
                l [<>]) ;
               Xml.xml_nempty "hints" []
                (List.fold_right
                  (function
                      (V.VARG_QUALID x) ->
                        (function i ->
                          [< Xml.xml_empty "hint" ["name",T.string_of_qualid x];
                             i
                          >]
                        )
                    | _ -> Vernacinterp.bad_vernac_args "HintsResolve"
                  )
                lh [<>]
                )
            >]
          )
         )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "IMPLICIT_ARGS_ON"
  (function
      [] ->
        IXml.output
         (Xml.xml_nempty "vernacular" []
          (Xml.xml_empty
            "ImplicitArguments"
            ["status","ON"]
          )
         )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "DEFINITION"
  (function
      (* Coq anomaly: a Local definition is a Definition at the syntax *)
      (* level but a Variable at the logical level. Here we have to    *)
      (* recognize the two cases and treat them differently            *)
      (V.VARG_STRING "LOCAL":: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c:: rest) ->
        IXml.output
         (Xml.xml_nempty "VARIABLES" ["as","LOCAL"]
           (Xml.xml_empty
             "VARIABLE"
             ["uri",Names.string_of_id id ^ ".var"]
           )
         )
    | (V.VARG_STRING kind:: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c :: rest) ->
        IXml.output
         (Xml.xml_empty
           "DEFINITION"
           ["uri", Names.string_of_id id ^ ".con" ; "as",kind]
         )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "BeginSection"
  (function
      [V.VARG_IDENTIFIER id] ->
        IXml.open_non_empty_element "SECTION" ["uri", Names.string_of_id id]
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "EndSection"
  (function
      [V.VARG_IDENTIFIER id] ->
        IXml.close_non_empty_element ()
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "StartProof"
  (function
      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
       IXml.output
        (Xml.xml_empty
          "THEOREM"
          ["uri", Names.string_of_id s ^ ".con"; "as",kind]
        )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "MUTUALINDUCTIVE"
  (function
      [V.VARG_STRING f; V.VARG_VARGLIST indl] ->
        (* we need the name of the first inductive defined *)
        (* type in the block to get the URI                *)
        let name =
         match indl with
            (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
          | _ -> assert false
        in
         IXml.output
          (Xml.xml_empty
            "DEFINITION"
            ["uri", Names.string_of_id name ^ ".ind"; "as",f]
          )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "VARIABLE"
  (function
      [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] ->
       (* here we need all the names *)
       let names =
        List.flatten (List.map fst slcl)
       in
        IXml.output
         (Xml.xml_nempty "VARIABLES" ["as",kind]
          (List.fold_right
            (fun name s ->
              [< (Xml.xml_empty
                   "VARIABLE"
                   ["uri",Names.string_of_id name ^ ".var"]
                 ) ; s
              >]
            ) names [<>]
          )
         )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
let module T = Nametab in
let module N = Names in
 set_hook "COERCION"
  (function
      [V.VARG_STRING kind; V.VARG_STRING identity; V.VARG_QUALID qid;
       V.VARG_QUALID qids; V.VARG_QUALID qidt] ->
        (* let's substitute empty strings with non-empty strings *)
        (* to get a stricter DTD                                 *)
        let remove_empty_string s = if s = "" then "UNSPECIFIED" else s in
        let kind     = remove_empty_string kind     in
        let identity = remove_empty_string identity in
         IXml.output
          (Xml.xml_nempty "vernacular" []
           (Xml.xml_empty
             "Coercion"
             ["kind",kind; "identity",identity ; "name",T.string_of_qualid qid ;
              "source",T.string_of_qualid qids;"target",T.string_of_qualid qidt]
           )
          )
    | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "MUTUALRECURSIVE"
  (function
      [V.VARG_VARGLIST lmi] ->
        (* we need the name of the first inductive defined *)
        (* type in the block to get the URI                *)
        let name =
         match lmi with
            (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
          | _ -> assert false
        in
         IXml.output
          (Xml.xml_empty
            "DEFINITION"
            ["uri", Names.string_of_id name ^ ".con" ; "as","Fixpoint"]
          )
     | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "MUTUALCORECURSIVE"
  (function
      [V.VARG_VARGLIST lmi] ->
        (* we need the name of the first inductive defined *)
        (* type in the block to get the URI                *)
        let name =
         match lmi with
            (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
          | _ -> assert false
        in
         IXml.output
          (Xml.xml_empty
            "DEFINITION"
            ["uri", Names.string_of_id name ^ ".con" ; "as","CoFixpoint"]
          )
     | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "RECORD"
  (function
      [V.VARG_STRING coe;
       V.VARG_IDENTIFIER struc;
       V.VARG_BINDERLIST binders;
       V.VARG_CONSTR sort;
       V.VARG_VARGLIST namec;
       V.VARG_VARGLIST cfs] ->
         IXml.output
          (Xml.xml_empty
            "DEFINITION"
            ["uri", Names.string_of_id struc ^ ".ind" ; "as","Record"]
          )
     | _ -> fail ()
  )
;;

let module V = Vernacinterp in
 set_hook "PARAMETER"
  (function
      [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] ->
       (* here we need all the names *)
       let names =
        List.flatten (List.map fst slcl)
       in
        IXml.output
         (Xml.xml_nempty "AXIOMS" ["as",kind]
          (List.fold_right
            (fun name s ->
              [< (Xml.xml_empty
                   "AXIOM"
                   ["uri",Names.string_of_id name ^ ".con"]
                 ) ; s
              >]
            ) names [<>]
          )
         )
    | _ -> fail ()
  )
;;