application patch Claudio

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 302 insertions, 22 deletions

diff --git a/Makefile b/Makefile
index ca3e3478e..ed249fa76 100644
--- a/Makefile
+++ b/Makefile
@@ -489,7 +489,8 @@ $(CONTRIBVO): states/initial.coq
 contrib: $(CONTRIBVO)
 omega: $(OMEGAVO)
 ring: $(RINGVO)
-xml: $(XMLVO)
+# xml_ instead of xml to avoid conflict with "make xml"
+xml_: $(XMLVO)
 extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
 correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 field: $(FIELDVO)
@@ -509,8 +510,10 @@ COQDEP=bin/coqdep$(EXE)
 COQMAKEFILE=bin/coq_makefile$(EXE)
 GALLINA=bin/gallina$(EXE)
 COQTEX=bin/coq-tex$(EXE)
+COQVO2XML=bin/coq_vo2xml$(EXE)
+RUNCOQVO2XML=coq_vo2xml$(EXE)   # Uses the one in PATH and not the one in bin
 
-tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) dev/top_printers.cmo
+tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) dev/top_printers.cmo
 
 COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo
 
@@ -532,11 +535,16 @@ $(COQMAKEFILE): tools/coq_makefile.ml
 $(COQTEX): tools/coq-tex.ml
 	$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.ml
 
+COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo
+
+$(COQVO2XML): $(COQVO2XMLCMO)
+	$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQVO2XMLCMO)
+
 clean::
 	rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml
 
 archclean::
-	rm -f $(COQDEP) $(GALLINA) $(COQTEX) $(COQMAKEFILE)
+	rm -f $(COQDEP) $(GALLINA) $(COQTEX) $(COQMAKEFILE) $(COQVO2XML)
 
 ###########################################################################
 # minicoq
@@ -555,6 +563,18 @@ archclean::
 	rm -f $(MINICOQ)
 
 ###########################################################################
+# XML
+###########################################################################
+
+# Warning: coq_vo2xml in PATH and not the one in bin is used
+
+.PHONY: xml
+xml: .xml_time_stamp
+.xml_time_stamp: $(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO)
+	$(RUNCOQVO2XML) -boot -byte $(COQINCLUDES) $(?:%.o=%)
+	touch .xml_time_stamp
+
+###########################################################################
 # Installation
 ###########################################################################
 
@@ -581,7 +601,7 @@ install-opt:
 
 install-binaries:
 	$(MKDIR) $(FULLBINDIR)
-	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(FULLBINDIR)
+	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(FULLBINDIR)
 
 LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO)
 
@@ -599,7 +619,7 @@ install-library:
 MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
 	man/coq_makefile.1 man/coqmktop.1 \
-	man/coq-interface.1 man/parser.1
+	man/coq-interface.1 man/parser.1 man/coq_vo2xml.1
 
 install-manpages:
 	$(MKDIR) $(FULLMANDIR)/man1
diff --git a/bin/.cvsignore b/bin/.cvsignore
index 51c25a5f3..39760ace8 100644
--- a/bin/.cvsignore
+++ b/bin/.cvsignore
@@ -10,3 +10,4 @@ coq-tex
 coq-extraction
 coq-interface
 parser
+coq_vo2xml
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 573f4319b..5f23c1d64 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -305,15 +305,16 @@ let print_term inner_types l env csr =
    (* coq coding of terms (the one of the logical framework)              *)
    match T.kind_of_term cstr with
      T.IsRel n  ->
-      (match List.nth l (n - 1) with
-          N.Name id ->
-            X.xml_empty "REL"
-             (add_sort_attribute false
-              ["value",(string_of_int n) ;
-               "binder",(N.string_of_id id) ;
-               "id", next_id])
-        | N.Anonymous -> assert false
-      )
+      let id =
+       match List.nth l (n - 1) with
+          N.Name id   -> id
+        | N.Anonymous -> N.make_ident "_" None
+      in
+       X.xml_empty "REL"
+        (add_sort_attribute false
+          ["value",(string_of_int n) ;
+           "binder",(N.string_of_id id) ;
+           "id", next_id])
    | T.IsVar id ->
       let depth =
        match get_depth_of_var (N.string_of_id id) with
diff --git a/man/coq_vo2xml.1 b/man/coq_vo2xml.1
new file mode 100644
index 000000000..21be67b77
--- /dev/null
+++ b/man/coq_vo2xml.1
@@ -0,0 +1,69 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq_vo2xml \- Exports the content of a Coq module to XML
+
+
+.SH SYNOPSIS
+.B coq_vo2xml
+[
+.B general \ Coq \ options
+]
+[
+.B -image
+.I f
+]
+[
+.B -t
+]
+[
+.B -xml-library-root
+.I d
+]
+.IR module " .\|.\|."
+
+
+.SH DESCRIPTION
+
+.B coq_vo2xml
+is a tool to export the content of a Coq module to XML.
+Because it executes coqtop(1), it recognizes a superset of its options.
+ones:
+.PP
+.B -image
+.IR f
+overrides the coqtop(1) executable with
+.IR f "."
+.PP
+.B -t
+does not remove the temporary file fed to coqtop(1).
+.PP
+.B -xml-library-root
+.IR d
+sets the path to the root of the XML library to
+.IR d ","
+overriding the value of $XML_ROOT_LIBRARY. The root of the XML library
+must be specified, either using the flag or setting the variable.
+.PP
+.IR module \&
+is the name of the module to export. The file module.vo will be searched in the
+Coq path by coqtop(1).
+The compiler produces a whole tree of XML files and directories rooted in the
+specified XML root library.
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Will give you a description of the whole list of options of coq_vo2xml,
+including the ones of coqtop(1).
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coq_makefile (1),
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ead690e50..ce220b54f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -93,6 +93,11 @@ let standard sds =
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
     sds;
   print "\n";
+  print "xml::\n";
+  List.iter
+    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\n")
+    sds;
+  print "\n";
   print "install:\n";
   print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n";
   if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n";
@@ -131,7 +136,7 @@ let implicit () =
     print ".v.tex:\n\t$(COQ2LATEX) $< -latex -o $@\n\n" ;
     print ".v.g.html:\n\t$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@\n\n" ;
     print 
-      ".v.g.tex:\n\t$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@\n\n"
+      ".v.g.tex:\n\t$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@\n\n" ;
   and ml_suffixes =
     if !some_mlfile then 
       [ ".mli" ; ".ml" ; ".cmo" ; ".cmi"; ".cmx" ]
@@ -183,6 +188,7 @@ let variables l =
   print "CAMLLINK=ocamlc\n";
   print "CAMLOPTLINK=ocamlopt\n";
   print "COQDEP=$(COQBIN)coqdep -c\n";
+  print "COQVO2XML=coq_vo2xml\n";
   var_aux l;
   print "\n"
 
@@ -234,7 +240,7 @@ let subdirs l =
   section "Special targets.";
   print ".PHONY: " ;
   print_list " "
-    ("all"::"opt"::"byte"::"archclean"::"clean"::"install"::"depend"::sds);
+    ("all"::"opt"::"byte"::"archclean"::"clean"::"install"::"depend"::"xml"::sds);
   print "\n\n";
   sds
 
@@ -242,17 +248,18 @@ let subdirs l =
 
 let rec other_files suff = function
   | V n :: r -> 
-      let f = (Filename.chop_suffix n "vo") ^ suff in
+      let f = (Filename.chop_suffix n ".vo") ^ suff in
       f :: (other_files suff r)
   | _   :: r -> other_files suff r
   | []       -> []
 
-let gfiles = other_files "g"
-let hfiles = other_files "html"
-let tfiles = other_files "tex"
-let vifiles = other_files "vi"
+let gfiles = other_files ".g"
+let hfiles = other_files ".html"
+let tfiles = other_files ".tex"
+let vifiles = other_files ".vi"
 let gtfiles l = List.map (fun f -> f^".tex") (gfiles l)
 let ghfiles l = List.map (fun f -> f^".html") (gfiles l)
+let vofiles = other_files ".vo"
 
 let all_target l =
   let rec fnames = function
@@ -281,6 +288,11 @@ let all_target l =
     print "\n\n";
     print "gallinahtml: "; print_list "\\\n  " (ghfiles l) ;
     print "\n\n";
+    print "xml:: .xml_time_stamp\n" ;
+    print ".xml_time_stamp: "; print_list "\\\n  " (vofiles l) ;
+     print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n" ;
+     print "\ttouch .xml_time_stamp" ;
+    print "\n\n"
   end
 
 let parse f =
diff --git a/tools/coq_vo2xml.ml b/tools/coq_vo2xml.ml
new file mode 100644
index 000000000..9b47fed03
--- /dev/null
+++ b/tools/coq_vo2xml.ml
@@ -0,0 +1,175 @@
+(* environment *)
+
+let environment = Unix.environment ()
+
+let bindir = ref Coq_config.bindir
+let binary = ref ("coqtop." ^ Coq_config.best)
+let image = ref ""
+let xml_library_root = ref (
+ try
+  Sys.getenv "XML_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_vo2xml 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_vo2xml" ".v" in
+  let args' = 
+    command :: "-batch" :: "-silent" :: 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 Xml.\n" ;
+  Printf.fprintf oc "Require %s.\n" modulename;
+  Printf.fprintf oc "Print XML Module Disk \"%s\" %s.\n" !xml_library_root
+   modulename;
+  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_vo2xml <options> <Coq options> module...\n
+options are:
+  -xml-library-root d   specify the path to the root of the XML library
+                        (overrides $XML_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-library-root" :: v :: rem ->
+        xml_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 ->
+	binary := "coqtop.byte"; parse (cfiles,args) rem
+    | "-opt" :: rem ->
+	binary := "coqtop.opt"; parse (cfiles,args) rem
+    | "-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_vo2xml: too few arguments" ;
+    usage ()
+  end;
+  let coqtopname = 
+    if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
+  in
+  if !xml_library_root = "" then
+   begin
+    prerr_endline "coq_vo2xml: you must either set $XML_LIBRARY_ROOT or use -xml-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/toplevel/usage.mli b/toplevel/usage.mli
index 4322b0c9b..c24ae331a 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -12,7 +12,9 @@
 
 val version : unit -> 'a
 
-(*s Prints the usage on the error output. *)
+(*s Prints the usage on the error output, preceeded by a user-provided message. *)
+val print_usage : string -> unit
 
+(*s Prints the usage on the error output. *)
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit