X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fxmltheory%2FXmlTheory%2Fxmltheoryentries.ml;fp=helm%2Fxmltheory%2FXmlTheory%2Fxmltheoryentries.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=de3c5030aa48c52be619aec421f517a7d7daf19a;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/xmltheory/XmlTheory/xmltheoryentries.ml b/helm/xmltheory/XmlTheory/xmltheoryentries.ml
deleted file mode 100644
index de3c5030a..000000000
--- a/helm/xmltheory/XmlTheory/xmltheoryentries.ml
+++ /dev/null
@@ -1,371 +0,0 @@
-(*********************)
-(* 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 ()
-  )
-;;