+++ /dev/null
-(*********************)
-(* 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 ()
- )
-;;
projects / helm.git / blobdiff