+(*********************)
+(* 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 ()
+ )
+;;