--- /dev/null
+COQTOP=/home/projects/helm/EXPORT/V7
+OCAMLC=ocamlc -I $(COQTOP)/config -I $(COQTOP)/toplevel
+
+COQV2THEORYXMLOBJS= \
+ $(COQTOP)/config/coq_config.cmo \
+ $(COQTOP)/toplevel/usage.cmo \
+ coq_v2theoryxml.cmo
+
+coq_v2theoryxml: $(COQV2THEORYXMLOBJS)
+ $(OCAMLC) -o $@ unix.cma $(COQV2THEORYXMLOBJS)
+
+coq_v2theoryxml.cmo: coq_v2theoryxml.ml
+ $(OCAMLC) -c $<
+
+.PHONY: clean
+clean:
+ rm -f coq_v2theoryxml *.cmo *.cmi
--- /dev/null
+(* environment *)
+
+let environment = Unix.environment ()
+
+let bindir = ref Coq_config.bindir
+let binary = "coqtop.byte"
+let image = ref ""
+let xml_theory_library_root = ref (
+ try
+ Sys.getenv "XML_THEORY_LIBRARY_ROOT"
+ with Not_found -> ""
+)
+
+(* the $COQBIN environment variable has priority over the Coq_config value *)
+let _ =
+ try
+ let c = Sys.getenv "COQBIN" in
+ if c <> "" then bindir := c
+ with Not_found -> ()
+
+(* coq_v2theoryxml options *)
+
+let keep = ref false
+
+(* Verifies that a string do not contains others caracters than letters,
+ digits, or `_` *)
+
+let check_module_name s =
+ let err () =
+ output_string stderr
+ "Modules names must only contain letters, digits, or underscores\n";
+ output_string stderr
+ "and must begin with a letter\n";
+ exit 1
+ in
+ match String.get s 0 with
+ | 'a' .. 'z' | 'A' .. 'Z' ->
+ for i = 1 to (String.length s)-1 do
+ match String.get s i with
+ | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> ()
+ | _ -> err ()
+ done
+ | _ -> err ()
+
+ (* compilation of a file [file] with command [command] and args [args] *)
+
+let compile command args file =
+ let dirname = Filename.dirname file in
+ let basename = Filename.basename file in
+ let modulename =
+ if Filename.check_suffix basename ".vo" then
+ Filename.chop_suffix basename ".vo"
+ else
+ basename
+ in
+ check_module_name modulename;
+ let tmpfile = Filename.temp_file "coq_v2theoryxml" ".v" in
+ let args' =
+ command :: "-batch" :: "-silent" :: "-is" :: "barestate" :: args
+ @ ["-load-vernac-source"; tmpfile] in
+ let devnull =
+ if Sys.os_type = "Unix" then
+ Unix.openfile "/dev/null" [] 0o777
+ else
+ Unix.stdin
+ in
+ let oc = open_out tmpfile in
+ Printf.fprintf oc "Require XmlTheory.\n" ;
+ Printf.fprintf oc "XmlTheory Begin %s \"%s\".\n" modulename
+ !xml_theory_library_root ;
+ Printf.fprintf oc "Load %s.\n" modulename;
+ Printf.fprintf oc "XmlTheory End.\n" ;
+ flush oc;
+ close_out oc;
+ try
+ let pid =
+ Unix.create_process_env command
+ (Array.of_list args') environment devnull Unix.stdout Unix.stderr in
+ let status = Unix.waitpid [] pid in
+ if not !keep then Sys.remove tmpfile ;
+ match status with
+ | _, Unix.WEXITED 0 -> ()
+ | _, Unix.WEXITED 127 ->
+ Printf.printf "Cannot execute %s\n" command;
+ exit 1
+ | _, Unix.WEXITED c -> exit c
+ | _ -> exit 1
+ with _ ->
+ if not !keep then Sys.remove tmpfile; exit 1
+
+(* parsing of the command line
+ *
+ * special treatment for -bindir and -i.
+ * other options are passed to coqtop *)
+
+let usage () =
+ Usage.print_usage
+ "Usage: coq_v2theoryxml <options> <Coq options> module...\n
+options are:
+ -xml-theory-library-root d specify the path to the root of the XML library
+ (overrides $XML_THEORY_LIBRARY_ROOT)
+ -image f specify an alternative executable for Coq
+ -t keep temporary files\n\n" ;
+ flush stderr ;
+ exit 1
+
+let parse_args () =
+ let rec parse (cfiles,args) = function
+ | [] ->
+ List.rev cfiles, List.rev args
+ | "-xml-theory-library-root" :: v :: rem ->
+ xml_theory_library_root := v ; parse (cfiles,args) rem
+ | "-t" :: rem ->
+ keep := true ; parse (cfiles,args) rem
+ | "-boot" :: rem ->
+ bindir:= Filename.concat Coq_config.coqtop "bin";
+ parse (cfiles, "-boot"::args) rem
+ | "-bindir" :: d :: rem ->
+ bindir := d ; parse (cfiles,args) rem
+ | "-bindir" :: [] ->
+ usage ()
+ | "-byte" :: rem ->
+ parse (cfiles,args) rem
+ | "-opt" :: rem ->
+ raise (Failure "To load ML modules, only -byte is allowed")
+ | "-image" :: f :: rem ->
+ image := f; parse (cfiles,args) rem
+ | "-image" :: [] ->
+ usage ()
+ | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+ | ("-libdir"|"-outputstate"|"-I"|"-include"
+ |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object"
+ |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
+ |"-init-file" as o) :: rem ->
+ begin
+ match rem with
+ | s :: rem' -> parse (cfiles,s::o::args) rem'
+ | [] -> usage ()
+ end
+ | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
+ | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
+ |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
+ |"-silent"|"-m" as o) :: rem ->
+ parse (cfiles,o::args) rem
+ | ("-v"|"--version") :: _ ->
+ Usage.version ()
+ | "-where" :: _ ->
+ print_endline Coq_config.coqlib; exit 0
+ | f :: rem -> parse (f::cfiles,args) rem
+ in
+ parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+(* main: we parse the command line, define the command to compile files
+ * and then call the compilation on each file *)
+
+let main () =
+ let cfiles, args = parse_args () in
+ if cfiles = [] then begin
+ prerr_endline "coq_v2theoryxml: too few arguments" ;
+ usage ()
+ end;
+ let coqtopname =
+ if !image <> "" then !image else Filename.concat !bindir (binary ^ Coq_config.exec_extension)
+ in
+ if !xml_theory_library_root = "" then
+ begin
+ prerr_endline "coq_v2theoryxml: you must either set $XML_THEORY_LIBRARY_ROOT or use -xml-theory-library-root";
+ usage ()
+ end
+ else
+ List.iter (compile coqtopname args) cfiles ;
+ prerr_endline
+ ("\nWARNING: all the URIs in the generated XML files are broken." ^
+ "\n See the README in the XML contrib to learn how to fix them.\n")
+
+let _ = Printexc.print main (); exit 0
--- /dev/null
+# This coq_vo2xml must be put in PATH before the real coq_vo2xml.
+# It's aim is to run coq_v2theoryxml instead of coq_vo2xml
+# Remember to set $XML_THEORY_LIBRARY_ROOT before starting this coq_vo2xml
--- /dev/null
+#!/bin/bash
+
+BASEDIR=/home/projects/helm/EXPORT/xmltheory
+$BASEDIR/Coq_v2theoryxml/coq_v2theoryxml -R $BASEDIR/XmlTheory Bologna.XmlTheory $@
--- /dev/null
+xmltheoryentries.cmo: xmltheoryentries.ml iXml.cmi
+xmltheoryentries.cmx: xmltheoryentries.ml iXml.cmx
+iXml.cmo: iXml.ml iXml.cmi
+iXml.cmx: iXml.ml iXml.cmi
+iXml.cmi: iXml.mli
+XmlTheory.vo: XmlTheory.v iXml.cmo xmltheoryentries.cmo
+XmlTheory.vi: XmlTheory.v iXml.cmo xmltheoryentries.cmo
+XmlTheory.html: XmlTheory.v iXml.cmo xmltheoryentries.cmo
--- /dev/null
+# Settare
+
+OPT=-byte # Nota: questo andrebbe fatto nel Make, ma un bug di coq_makefile
+ # lo impedisce
+COQTOP=...
--- /dev/null
+-R . Bologna.XmlTheory
+-I $(COQTOP)/contrib/xml
+XmlTheory.v
+iXml.ml
+xmltheoryentries.ml
--- /dev/null
+##############################################################################
+## The Calculus of Inductive Constructions ##
+## ##
+## Projet Coq ##
+## ##
+## INRIA ENS-CNRS ##
+## Rocquencourt Lyon ##
+## ##
+## Coq V7 ##
+## ##
+## ##
+##############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f Make -o Makefile
+#
+
+##########################
+# #
+# Variables definitions. #
+# #
+##########################
+
+CAMLP4LIB=`camlp4 -where`
+MAKE=make "COQBIN=$(COQBIN)" "OPT=$(OPT)"
+COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
+ -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
+ -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
+ -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
+ZFLAGS=$(OCAMLLIBS) $(COQSRC)
+COQFLAGS=-q $(OPT) $(COQLIBS)
+COQC=$(COQBIN)coqc
+COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(COQLIBS)
+GALLINA=gallina
+COQ2HTML=coq2html
+COQ2LATEX=coq2latex
+CAMLC=ocamlc -c
+CAMLOPTC=ocamlopt -c
+CAMLLINK=ocamlc
+CAMLOPTLINK=ocamlopt
+COQDEP=$(COQBIN)coqdep -c
+COQVO2XML=coq_vo2xml
+
+#########################
+# #
+# Libraries definition. #
+# #
+#########################
+
+OCAMLLIBS=-I .\
+ -I $(COQTOP)/contrib/xml
+COQLIBS=-I .\
+ -R . Bologna.XmlTheory\
+ -I $(COQTOP)/contrib/xml
+
+###################################
+# #
+# Definition of the "all" target. #
+# #
+###################################
+
+all: XmlTheory.vo\
+ iXml.cmo\
+ xmltheoryentries.cmo
+
+spec: XmlTheory.vi
+
+gallina: XmlTheory.g
+
+html: XmlTheory.html
+
+tex: XmlTheory.tex
+
+gallinatex: XmlTheory.g.tex
+
+gallinahtml: XmlTheory.g.html
+
+xml: .xml_time_stamp
+.xml_time_stamp: XmlTheory.vo
+ $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
+ touch .xml_time_stamp
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+.PHONY: all opt byte archclean clean install depend xml
+
+.SUFFIXES: .mli .ml .cmo .cmi .cmx .v .vo .vi .g .html .tex .g.tex .g.html
+
+.mli.cmi:
+ $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+.ml.cmo:
+ $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+.ml.cmx:
+ $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
+
+.v.vo:
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+.v.vi:
+ $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+.v.g:
+ $(GALLINA) $<
+
+.v.html:
+ $(COQ2HTML) $<
+
+.v.tex:
+ $(COQ2LATEX) $< -latex -o $@
+
+.v.g.html:
+ $(GALLINA) -stdout $< | $(COQ2HTML) -f > $@
+
+.v.g.tex:
+ $(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@
+
+byte:
+ $(MAKE) all "OPT="
+
+opt:
+ $(MAKE) all "OPT=-opt"
+
+include .depend
+
+depend:
+ rm .depend
+ $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
+ $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
+
+install:
+ @if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
+ cp -f *.vo $(TARGETDIR)
+ cp -f *.cmo $(TARGETDIR)
+
+Makefile: Make
+ mv -f Makefile Makefile.bak
+ $(COQBIN)coq_makefile -f Make -o Makefile
+
+clean:
+ rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
+
+archclean:
+ rm -f *.cmx *.o
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
--- /dev/null
+Here we show the procedure to follow to add the recognition of
+a new syntactical form.
+
+Form to recognize in the model:
+
+Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}.
+
+1. cd V7 ; grep "Lemma" */*.ml4
+ the result should be one or a few files. In this case the
+ only file is parsing/g_vernac.ml4. In the case of many files,
+ only one is the good one.
+2. open the file and search for Lemma:
+ thm_tok:
+ [ [ "Theorem" -> <:ast< "THEOREM" >>
+ | IDENT "Lemma" -> <:ast< "LEMMA" >>
+ | IDENT "Fact" -> <:ast< "FACT" >>
+ | IDENT "Remark" -> <:ast< "REMARK" >>
+ | IDENT "Decl" -> <:ast< "DECL" >> ] ]
+
+ so a Lemma is mapped into an ast of phylum thm_tok.
+ Let's search for thm_tok. Many occurrences are found,
+ but the only one that matches the form to recognize is
+
+ gallina:
+ (* Definition, Goal *)
+ [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
+ <:ast< (StartProof $thm $id $c) >>
+
+ So the ast created is tagged StartProof
+3. grep "StartProof" */*.ml (usually toplevel/...)
+ Open the file and search for StartProof.
+ This is found:
+ let _ =
+ add "StartProof"
+ (function
+ | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
+ ...
+4. edit xmltheoryentries.ml and copy the entry for another rule,
+ substituting StartProof as the parameter for set_hook and
+ using the above match (with V. added where appropriate) after function:
+
+let module V = Vernacinterp in
+ set_hook "StartProof"
+ (function
+ [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
+ ???
+ | _ -> fail ()
+ )
+;;
+
+ Finally, write OCaml code to print to XML the availables interesting
+ infos. In our case the code becomes
+
+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 ()
+ )
+;;
+
+ IXml.output should always be present and the code inside
+ (that is simply XML written in OCaml form) should be changed.
+ The syntax is
+ Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"]
+ to create an empty element name with attributes att1 ... attn.
+ To create a non-empty element, use
+ Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"]
+ stream
+ where stream is an OCaml stream of other XML elements, as:
+ * another Xml.xml_nempty
+ * an Xml.xml_empty
+ * [< stream1 ; ... ; streamk >]
--- /dev/null
+Declare ML Module "iXml" "xmltheoryentries".
+
+(*Vecchio, ma funzionante
+Grammar vernac vernac : ast :=
+ xml_theory_begin [ "XmlTheory" "Begin" stringarg($s) stringarg($f) "." ] ->
+ [(XMLTHEORYBEGIN $s $f)]
+| xml_theory_end [ "XmlTheory" "End" "." ] ->
+ [(XMLTHEORYEND)].
+*)
+
+Grammar vernac vernac : ast :=
+ xml_theory_begin [ "XmlTheory" "Begin" identarg($s) stringarg($f) "." ] ->
+ [(XMLTHEORYBEGIN $s $f)]
+| xml_theory_end [ "XmlTheory" "End" "." ] ->
+ [(XMLTHEORYEND)].
--- /dev/null
+exception NoOpenNonEmptyElements
+
+type sectionTree =
+ Leaf of Xml.token Stream.t
+ | Node of string * (string * string) list * sectionTree list ref
+;;
+
+let rec token_stream_of_section_tree_list =
+ function
+ he::tl ->
+ [< token_stream_of_section_tree_list tl; token_stream_of_section_tree he >]
+ | [] -> [<>]
+and token_stream_of_section_tree =
+ function
+ Leaf t -> [< t >]
+ | Node (elem_name, attr_list, section_tree) ->
+ Xml.xml_nempty elem_name attr_list
+ (token_stream_of_section_tree_list !section_tree)
+;;
+
+let section_stack = ref [];;
+let xmloutput = ref (ref []);;
+let filename = ref "";;
+
+let reset_output fname =
+ filename := fname ;
+ xmloutput := ref [] ;
+ section_stack := []
+;;
+
+let output n =
+ let xmloutput = !xmloutput in
+ xmloutput := (Leaf n) :: !xmloutput
+;;
+
+let open_non_empty_element elem_name attr_list =
+ let newxmloutput = ref [] in
+ !xmloutput := (Node (elem_name, attr_list, newxmloutput)) :: !(!xmloutput) ;
+ section_stack := !xmloutput :: !section_stack ;
+ xmloutput := newxmloutput
+;;
+
+let close_non_empty_element () =
+ match !section_stack with
+ oldxmloutput::oldsection_stack ->
+ xmloutput := oldxmloutput ;
+ section_stack := oldsection_stack
+ | _ -> raise NoOpenNonEmptyElements
+;;
+
+let print_output () =
+ Xml.pp (token_stream_of_section_tree_list !(!xmloutput)) (Some !filename)
+;;
--- /dev/null
+exception NoOpenNonEmptyElements
+
+val reset_output : string -> unit
+val output : Xml.token Stream.t -> unit
+val open_non_empty_element : string -> (string * string) list -> unit
+val close_non_empty_element : unit -> unit
+val print_output : unit -> unit
--- /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 ()
+ )
+;;
--- /dev/null
+<?xml encoding="ISO-8859-1"?>
+
+<!--*****************************************************************-->
+<!-- DTD FOR THEORY OBJECTS AT LEVEL OF CIC XML FILES: -->
+<!-- First draft: May 10 2000, Claudio Sacerdoti Coen, Irene Schena -->
+<!-- Revised: February 2001, Claudio Sacerdoti Coen -->
+<!-- Revised: May 01 2001, Claudio Sacerdoti Coen -->
+<!--*****************************************************************-->
+
+<!ENTITY % mathstructure '(AXIOMS|DEFINITION|THEOREM|VARIABLES|SECTION|vernacular)*'>
+
+<!ELEMENT Theory (%mathstructure;)>
+<!ATTLIST Theory
+ uri CDATA #REQUIRED>
+
+<!ELEMENT AXIOMS (AXIOM*)>
+<!ATTLIST AXIOMS
+ as (AXIOM|PARAMETER|PARAMETERS) #REQUIRED>
+
+<!ELEMENT AXIOM EMPTY>
+<!ATTLIST AXIOM
+ uri CDATA #REQUIRED>
+
+<!ELEMENT DEFINITION EMPTY>
+<!ATTLIST DEFINITION
+ uri CDATA #REQUIRED
+ as (DEFINITION|Inductive|CoInductive|Fixpoint|CoFixpoint|Record) #REQUIRED>
+
+<!ELEMENT THEOREM EMPTY>
+<!ATTLIST THEOREM
+ uri CDATA #REQUIRED
+ as (THEOREM|LEMMA|FACT|REMARK|DECL) #REQUIRED>
+
+<!ELEMENT VARIABLES (VARIABLE*)>
+<!ATTLIST VARIABLES
+ as (VARIABLE|VARIABLES|HYPOTHESIS|HYPOTHESES|LOCAL) #REQUIRED>
+
+<!ELEMENT VARIABLE EMPTY>
+<!ATTLIST VARIABLE
+ uri CDATA #REQUIRED>
+
+<!ELEMENT SECTION (%mathstructure;)>
+<!ATTLIST SECTION
+ uri CDATA #REQUIRED>
+
+<!ELEMENT vernacular (Require|ImplicitArguments|Coercion|HintsResolve)>
+
+<!ELEMENT Require EMPTY>
+<!ATTLIST Require
+ import (EXPORT|IMPORT) #REQUIRED
+ specif (UNSPECIFIED|IMPLEMENTATION|SPECIFICATION) #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT ImplicitArguments (EMPTY)>
+<!ATTLIST ImplicitArguments
+ status (ON) #REQUIRED>
+
+<!ELEMENT Coercion EMPTY>
+<!ATTLIST Coercion
+ kind (LOCAL|UNSPECIFIED) #REQUIRED
+ identity (IDENTITY|UNSPECIFIED) #REQUIRED
+ name CDATA #REQUIRED
+ source CDATA #REQUIRED
+ target CDATA #REQUIRED>
+
+<!ELEMENT HintsResolve (dbs,hints)>
+
+<!ELEMENT dbs (db*)>
+
+<!ELEMENT db (EMPTY)>
+<!ATTLIST db
+ name CDATA #REQUIRED>
+
+<!ELEMENT hints (hint*)>
+
+<!ELEMENT hint (EMPTY)>
+<!ATTLIST hint
+ name CDATA #REQUIRED>
projects / helm.git / commitdiff