From: Claudio Sacerdoti Coen Date: Wed, 2 May 2001 14:14:57 +0000 (+0000) Subject: Initial revision X-Git-Tag: v0_1_2~12 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a3551a665bcc68c9e2d4f7a220e4dfabad3fde1;p=helm.git Initial revision --- diff --git a/helm/xmltheory/Coq_v2theoryxml/.depend b/helm/xmltheory/Coq_v2theoryxml/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/helm/xmltheory/Coq_v2theoryxml/Makefile b/helm/xmltheory/Coq_v2theoryxml/Makefile new file mode 100644 index 000000000..1f9fae538 --- /dev/null +++ b/helm/xmltheory/Coq_v2theoryxml/Makefile @@ -0,0 +1,17 @@ +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 diff --git a/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml b/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml new file mode 100644 index 000000000..b1e856e1a --- /dev/null +++ b/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml @@ -0,0 +1,176 @@ +(* 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 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 diff --git a/helm/xmltheory/FakeCoq_vo2xml/README b/helm/xmltheory/FakeCoq_vo2xml/README new file mode 100644 index 000000000..4accfcafc --- /dev/null +++ b/helm/xmltheory/FakeCoq_vo2xml/README @@ -0,0 +1,3 @@ +# 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 diff --git a/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml b/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml new file mode 100755 index 000000000..34e44a0a4 --- /dev/null +++ b/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml @@ -0,0 +1,4 @@ +#!/bin/bash + +BASEDIR=/home/projects/helm/EXPORT/xmltheory +$BASEDIR/Coq_v2theoryxml/coq_v2theoryxml -R $BASEDIR/XmlTheory Bologna.XmlTheory $@ diff --git a/helm/xmltheory/XmlTheory/.depend b/helm/xmltheory/XmlTheory/.depend new file mode 100644 index 000000000..2b814a941 --- /dev/null +++ b/helm/xmltheory/XmlTheory/.depend @@ -0,0 +1,8 @@ +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 diff --git a/helm/xmltheory/XmlTheory/COME_COMPILARE b/helm/xmltheory/XmlTheory/COME_COMPILARE new file mode 100644 index 000000000..f1389cc35 --- /dev/null +++ b/helm/xmltheory/XmlTheory/COME_COMPILARE @@ -0,0 +1,5 @@ +# Settare + +OPT=-byte # Nota: questo andrebbe fatto nel Make, ma un bug di coq_makefile + # lo impedisce +COQTOP=... diff --git a/helm/xmltheory/XmlTheory/Make b/helm/xmltheory/XmlTheory/Make new file mode 100644 index 000000000..a927b6345 --- /dev/null +++ b/helm/xmltheory/XmlTheory/Make @@ -0,0 +1,5 @@ +-R . Bologna.XmlTheory +-I $(COQTOP)/contrib/xml +XmlTheory.v +iXml.ml +xmltheoryentries.ml diff --git a/helm/xmltheory/XmlTheory/Makefile b/helm/xmltheory/XmlTheory/Makefile new file mode 100644 index 000000000..1dc9d35c4 --- /dev/null +++ b/helm/xmltheory/XmlTheory/Makefile @@ -0,0 +1,165 @@ +############################################################################## +## 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 + diff --git a/helm/xmltheory/XmlTheory/README b/helm/xmltheory/XmlTheory/README new file mode 100644 index 000000000..ce4c86c98 --- /dev/null +++ b/helm/xmltheory/XmlTheory/README @@ -0,0 +1,78 @@ +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 >] diff --git a/helm/xmltheory/XmlTheory/XmlTheory.v b/helm/xmltheory/XmlTheory/XmlTheory.v new file mode 100644 index 000000000..54fdf82e6 --- /dev/null +++ b/helm/xmltheory/XmlTheory/XmlTheory.v @@ -0,0 +1,15 @@ +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)]. diff --git a/helm/xmltheory/XmlTheory/iXml.ml b/helm/xmltheory/XmlTheory/iXml.ml new file mode 100644 index 000000000..98fb186d8 --- /dev/null +++ b/helm/xmltheory/XmlTheory/iXml.ml @@ -0,0 +1,53 @@ +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) +;; diff --git a/helm/xmltheory/XmlTheory/iXml.mli b/helm/xmltheory/XmlTheory/iXml.mli new file mode 100644 index 000000000..11fad8202 --- /dev/null +++ b/helm/xmltheory/XmlTheory/iXml.mli @@ -0,0 +1,7 @@ +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 diff --git a/helm/xmltheory/XmlTheory/xmltheoryentries.ml b/helm/xmltheory/XmlTheory/xmltheoryentries.ml new file mode 100644 index 000000000..de3c5030a --- /dev/null +++ b/helm/xmltheory/XmlTheory/xmltheoryentries.ml @@ -0,0 +1,371 @@ +(*********************) +(* 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 = +"\n" ^ +"\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 () + ) +;; diff --git a/helm/xmltheory/maththeory.dtd b/helm/xmltheory/maththeory.dtd new file mode 100644 index 000000000..f010b6500 --- /dev/null +++ b/helm/xmltheory/maththeory.dtd @@ -0,0 +1,78 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +