From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tools/README.coq-tex | 13 + tools/README.emacs | 31 ++ tools/check-v8 | 24 ++ tools/coq-inferior.el | 324 ++++++++++++++++ tools/coq-sl.sty | 37 ++ tools/coq-tex.ml4 | 292 +++++++++++++++ tools/coq.el | 182 +++++++++ tools/coq_makefile.ml4 | 454 +++++++++++++++++++++++ tools/coqdep.ml | 537 +++++++++++++++++++++++++++ tools/coqdep_lexer.mll | 231 ++++++++++++ tools/coqdoc/alpha.ml | 45 +++ tools/coqdoc/alpha.mli | 19 + tools/coqdoc/coqdoc.sty | 58 +++ tools/coqdoc/index.mli | 59 +++ tools/coqdoc/index.mll | 327 +++++++++++++++++ tools/coqdoc/main.ml | 420 +++++++++++++++++++++ tools/coqdoc/output.ml | 812 +++++++++++++++++++++++++++++++++++++++++ tools/coqdoc/output.mli | 92 +++++ tools/coqdoc/pretty.mli | 19 + tools/coqdoc/pretty.mll | 586 +++++++++++++++++++++++++++++ tools/coqdoc/style.css | 23 ++ tools/coqwc.mll | 293 +++++++++++++++ tools/gallina.ml | 66 ++++ tools/gallina_lexer.mll | 128 +++++++ tools/restore-v7 | 9 + tools/translate-v8 | 41 +++ tools/translate_V6-3-1_to_V7-0 | 27 ++ tools/upgrade-v8 | 22 ++ 28 files changed, 5171 insertions(+) create mode 100755 tools/README.coq-tex create mode 100755 tools/README.emacs create mode 100755 tools/check-v8 create mode 100644 tools/coq-inferior.el create mode 100755 tools/coq-sl.sty create mode 100644 tools/coq-tex.ml4 create mode 100644 tools/coq.el create mode 100644 tools/coq_makefile.ml4 create mode 100755 tools/coqdep.ml create mode 100755 tools/coqdep_lexer.mll create mode 100644 tools/coqdoc/alpha.ml create mode 100644 tools/coqdoc/alpha.mli create mode 100644 tools/coqdoc/coqdoc.sty create mode 100644 tools/coqdoc/index.mli create mode 100644 tools/coqdoc/index.mll create mode 100644 tools/coqdoc/main.ml create mode 100644 tools/coqdoc/output.ml create mode 100644 tools/coqdoc/output.mli create mode 100644 tools/coqdoc/pretty.mli create mode 100644 tools/coqdoc/pretty.mll create mode 100644 tools/coqdoc/style.css create mode 100644 tools/coqwc.mll create mode 100644 tools/gallina.ml create mode 100644 tools/gallina_lexer.mll create mode 100755 tools/restore-v7 create mode 100755 tools/translate-v8 create mode 100755 tools/translate_V6-3-1_to_V7-0 create mode 100755 tools/upgrade-v8 (limited to 'tools') diff --git a/tools/README.coq-tex b/tools/README.coq-tex new file mode 100755 index 00000000..5c7606a9 --- /dev/null +++ b/tools/README.coq-tex @@ -0,0 +1,13 @@ +DESCRIPTION. + +The coq-tex filter extracts Coq phrases embedded in LaTeX files, +evaluates them, and insert the outcome of the evaluation after each +phrase. + +The filter is written in Perl, so you'll need Perl version 4 installed +on your machine. + +USAGE. See the manual page (coq-tex.1). + +AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr) + from caml-tex of Xavier Leroy. diff --git a/tools/README.emacs b/tools/README.emacs new file mode 100755 index 00000000..0d27b607 --- /dev/null +++ b/tools/README.emacs @@ -0,0 +1,31 @@ + +DESCRIPTION: + +An emacs mode to help editing Coq vernacular files. + +AUTHOR: + +Jean-Christophe Filliatre (jcfillia@lri.fr), + from the Caml mode of Xavier Leroy. + +CONTENTS: + + coq.el A major mode for editing Coq files in Gnu Emacs + +USAGE: + +Add the following lines to your .emacs file: + +(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + +The Coq major mode is triggered by visiting a file with extension .v, +or manually by M-x coq-mode. It gives you the correct syntax table for +the Coq language, and also a rudimentary indentation facility: + +- pressing TAB at the beginning of a line indents the line like the line above + +- extra TABs increase the indentation level (by 2 spaces by default) + +- M-TAB decreases the indentation level. + diff --git a/tools/check-v8 b/tools/check-v8 new file mode 100755 index 00000000..9dfa0be3 --- /dev/null +++ b/tools/check-v8 @@ -0,0 +1,24 @@ +#!/bin/sh + +echo ------------------ Producing v8 files ------------------------- +if [ -e v8 ]; then rm -r v8; fi +if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi +cp -pr . /tmp/v8.$$ +mv /tmp/v8.$$ v8 +cd v8 +rm description +make clean +make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ + { echo ---- Failed to translate; exit 1; } +echo ------------------ Upgrading v8 files ------------------------- +v8files=`find . -name \*.v8` +for i in $v8files; do + j=`dirname $i`/`basename $i .v8`.v + echo Upgrading $i + mv -u -f $i $j +done +echo ------------------ Recompiling v8 files ----------------------- +make clean +make || { echo ---- Failed to recompile; exit 1; } +make clean # to save disk space +echo ------------------ Translation completed ---------------------- diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el new file mode 100644 index 00000000..d4f96a16 --- /dev/null +++ b/tools/coq-inferior.el @@ -0,0 +1,324 @@ +;;; inferior-coq.el --- Run an inferior Coq process. +;;; +;;; Copyright (C) Marco Maggesi +;;; Time-stamp: "2002-02-28 12:15:04 maggesi" + + +;; Emacs Lisp Archive Entry +;; Filename: inferior-coq.el +;; Version: 1.0 +;; Keywords: process coq +;; Author: Marco Maggesi +;; Maintainer: Marco Maggesi +;; Description: Run an inferior Coq process. +;; URL: http://www.math.unifi.it/~maggesi/ +;; Compatibility: Emacs20, Emacs21, XEmacs21 + +;; This is free software; you can redistribute it and/or modify it under +;; the terms of the GNU General Public License as published by the Free +;; Software Foundation; either version 2, or (at your option) any later +;; version. +;; +;; This is distributed in the hope that it will be useful, but WITHOUT +;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +;; for more details. +;; +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs; see the file COPYING. If not, write to the +;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, +;; MA 02111-1307, USA. + +;;; Commentary: + +;; Coq is a proof assistant (http://coq.inria.fr/). This code run an +;; inferior Coq process and defines functions to send bits of code +;; from other buffers to the inferior process. This is a +;; customisation of comint-mode (see comint.el). For a more complex +;; and full featured Coq interface under Emacs look at Proof General +;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). +;; +;; Written by Marco Maggesi with code heavly +;; borrowed from emacs cmuscheme.el +;; +;; Please send me bug reports, bug fixes, and extensions, so that I can +;; merge them into the master source. + +;;; Installation: + +;; You need to have coq.el already installed (it comes with the +;; standard Coq distribution) in order to use this code. Put this +;; file somewhere in you load-path and add the following lines in your +;; "~/.emacs": +;; +;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +;; (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) +;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) +;; (autoload 'run-coq-other-window "inferior-coq" +;; "Run an inferior Coq process in a new window." t) +;; (autoload 'run-coq-other-frame "inferior-coq" +;; "Run an inferior Coq process in a new frame." t) + +;;; Usage: + +;; Call `M-x "run-coq'. +;; +;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): +;; C-return ('M-x coq-send-line) send the current line. +;; C-c C-r (`M-x coq-send-region') send the current region. +;; C-c C-a (`M-x coq-send-abort') send the command "Abort". +;; C-c C-t (`M-x coq-send-restart') send the command "Restart". +;; C-c C-s (`M-x coq-send-show') send the command "Show". +;; C-c C-u (`M-x coq-send-undo') send the command "Undo". +;; C-c C-v (`M-x coq-check-region') run command "Check" on region. +;; C-c . (`M-x coq-come-here') Restart and send until current point. + +;;; Change Log: + +;; From -0.0 to 1.0 brought into existence. + + +(require 'coq) +(require 'comint) + +(setq coq-program-name "coqtop") + +(defgroup inferior-coq nil + "Run a coq process in a buffer." + :group 'coq) + +(defcustom inferior-coq-mode-hook nil + "*Hook for customising inferior-coq mode." + :type 'hook + :group 'coq) + +(defvar inferior-coq-mode-map + (let ((m (make-sparse-keymap))) + (define-key m "\C-c\C-r" 'coq-send-region) + (define-key m "\C-c\C-a" 'coq-send-abort) + (define-key m "\C-c\C-t" 'coq-send-restart) + (define-key m "\C-c\C-s" 'coq-send-show) + (define-key m "\C-c\C-u" 'coq-send-undo) + (define-key m "\C-c\C-v" 'coq-check-region) + m)) + +;; Install the process communication commands in the coq-mode keymap. +(define-key coq-mode-map [(control return)] 'coq-send-line) +(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) +(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) +(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) +(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) +(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) +(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) +(define-key coq-mode-map "\C-c." 'coq-come-here) + +(defvar coq-buffer) + +(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" + "\ +Major mode for interacting with an inferior Coq process. + +The following commands are available: +\\{inferior-coq-mode-map} + +A Coq process can be fired up with M-x run-coq. + +Customisation: Entry to this mode runs the hooks on comint-mode-hook +and inferior-coq-mode-hook (in that order). + +You can send text to the inferior Coq process from other buffers +containing Coq source. + +Functions and key bindings (Learn more keys with `C-c C-h'): + C-return ('M-x coq-send-line) send the current line. + C-c C-r (`M-x coq-send-region') send the current region. + C-c C-a (`M-x coq-send-abort') send the command \"Abort\". + C-c C-t (`M-x coq-send-restart') send the command \"Restart\". + C-c C-s (`M-x coq-send-show') send the command \"Show\". + C-c C-u (`M-x coq-send-undo') send the command \"Undo\". + C-c C-v (`M-x coq-check-region') run command \"Check\" on region. + C-c . (`M-x coq-come-here') Restart and send until current point. +" + ;; Customise in inferior-coq-mode-hook + (setq comint-prompt-regexp "^[^<]* < *") + (coq-mode-variables) + (setq mode-line-process '(":%s")) + (setq comint-input-filter (function coq-input-filter)) + (setq comint-get-old-input (function coq-get-old-input))) + +(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" + "*Input matching this regexp are not saved on the history list. +Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." + :type 'regexp + :group 'inferior-coq) + +(defun coq-input-filter (str) + "Don't save anything matching `inferior-coq-filter-regexp'." + (not (string-match inferior-coq-filter-regexp str))) + +(defun coq-get-old-input () + "Snarf the sexp ending at point." + (save-excursion + (let ((end (point))) + (backward-sexp) + (buffer-substring (point) end)))) + +(defun coq-args-to-list (string) + (let ((where (string-match "[ \t]" string))) + (cond ((null where) (list string)) + ((not (= where 0)) + (cons (substring string 0 where) + (coq-args-to-list (substring string (+ 1 where) + (length string))))) + (t (let ((pos (string-match "[^ \t]" string))) + (if (null pos) + nil + (coq-args-to-list (substring string pos + (length string))))))))) + +;;;###autoload +(defun run-coq (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +;;;###autoload +(defun run-coq-other-window (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (pop-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +(defun run-coq-other-frame (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer-other-frame "*coq*")) + +(defun switch-to-coq (eob-p) + "Switch to the coq process buffer. +With argument, position cursor at end of buffer." + (interactive "P") + (if (get-buffer coq-buffer) + (pop-to-buffer coq-buffer) + (error "No current process buffer. See variable `coq-buffer'")) + (cond (eob-p + (push-mark) + (goto-char (point-max))))) + +(defun coq-send-region (start end) + "Send the current region to the inferior Coq process." + (interactive "r") + (comint-send-region (coq-proc) start end) + (comint-send-string (coq-proc) "\n")) + +(defun coq-send-line () + "Send the current line to the Coq process." + (interactive) + (save-excursion + (end-of-line) + (let ((end (point))) + (beginning-of-line) + (coq-send-region (point) end))) + (next-line 1)) + +(defun coq-send-abort () + "Send the command \"Abort.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Abort.\n")) + +(defun coq-send-restart () + "Send the command \"Restart.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Restart.\n")) + +(defun coq-send-undo () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Undo.\n")) + +(defun coq-check-region (start end) + "Run the commmand \"Check\" on the current region." + (interactive "r") + (comint-proc-query (coq-proc) + (concat "Check " + (buffer-substring start end) + ".\n"))) + +(defun coq-send-show () + "Send the command \"Show.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Show.\n")) + +(defun coq-come-here () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Reset Initial.\n") + (coq-send-region 1 (point))) + +(defvar coq-buffer nil "*The current coq process buffer.") + +(defun coq-proc () + "Return the current coq process. See variable `coq-buffer'." + (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) + (current-buffer) + coq-buffer)))) + (or proc + (error "No current process. See variable `coq-buffer'")))) + +(defcustom inferior-coq-load-hook nil + "This hook is run when inferior-coq is loaded in. +This is a good place to put keybindings." + :type 'hook + :group 'inferior-coq) + +(run-hooks 'inferior-coq-load-hook) + +(provide 'inferior-coq) diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty new file mode 100755 index 00000000..9f6e5480 --- /dev/null +++ b/tools/coq-sl.sty @@ -0,0 +1,37 @@ +% COQ style option, for use with the coq-latex filter. + +\typeout{Document Style option `coq-sl' <7 Apr 92>.} + +\ifcase\@ptsize + \font\sltt = cmsltt10 +\or \font\sltt = cmsltt10 \@halfmag +\or \font\sltt = cmsltt10 \@magscale1 +\fi + +{\catcode`\^^M=\active % + \gdef\@coqinputline#1^^M{\tt Coq < #1\par} % + \gdef\@coqoutputline#1^^M{\sltt#1\par} } % +\def\@coqblankline{\medskip} +\chardef\@coqbackslash="5C + +\def\coq{ + \bgroup + \flushleft + \parindent 0pt + \parskip 0pt + \let\do\@makeother\dospecials + \catcode`\^^M=\active + \catcode`\\=0 + \catcode`\ \active + \frenchspacing + \@vobeyspaces + \let\?\@coqinputline + \let\:\@coqoutputline + \let\;\@coqblankline + \let\\\@coqbackslash +} + +\def\endcoq{ + \endflushleft + \egroup\noindent +} diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 new file mode 100644 index 00000000..6987d78b --- /dev/null +++ b/tools/coq-tex.ml4 @@ -0,0 +1,292 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () + | _ -> begin + print_string "This program only runs under Unix !\n"; + flush stdout; + exit 1 + end + +let linelen = ref 72 +let output = ref "" +let output_specified = ref false +let image = ref "" +let cut_at_blanks = ref false +let verbose = ref false +let slanted = ref false +let hrule = ref false +let small = ref false + +let coq_prompt = Str.regexp "Coq < " +let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " + +let remove_prompt s = Str.replace_first any_prompt "" s + +(* First pass: extract the Coq phrases to evaluate from [texfile] + * and put them into the file [inputv] *) + +let begin_coq = Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" +let end_coq = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" + +let extract texfile inputv = + let chan_in = open_in texfile in + let chan_out = open_out inputv in + let rec inside () = + let s = input_line chan_in in + if Str.string_match end_coq s 0 then + outside () + else begin + output_string chan_out (s ^ "\n"); + inside () + end + and outside () = + let s = input_line chan_in in + if Str.string_match begin_coq s 0 then + inside () + else + outside () + in + try + output_string chan_out + ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); + outside () + with End_of_file -> + begin close_in chan_in; close_out chan_out end + +(* Second pass: insert the answers of Coq from [coq_output] into the + * TeX file [texfile]. The result goes in file [result]. *) + +let begin_coq_example = + Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" +let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" +let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" +let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" +let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" + +let has_match r s = + try let _ = Str.search_forward r s 0 in true with Not_found -> false + +let percent = Str.regexp "%" +let bang = Str.regexp "!" +let expos = Str.regexp "^" + +let tex_escaped s = + let rec trans = parser + | [< s1 = (parser + | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> + "\\" ^ (String.make 1 c) + | [< ''\\' >] -> "\\char'134" + | [< ''^' >] -> "\\char'136" + | [< ''~' >] -> "\\char'176" + | [< '' ' >] -> "~" + | [< ''<' >] -> "{<}" + | [< ''>' >] -> "{>}" + | [< 'c >] -> String.make 1 c); + s2 = trans >] -> s1 ^ s2 + | [< >] -> "" + in + trans (Stream.of_string s) + +let encapsule sl c_out s = + if sl then + Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) + else + Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) + +let print_block c_out bl = + List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl + +let insert texfile coq_output result = + let c_tex = open_in texfile in + let c_coq = open_in coq_output in + let c_out = open_out result in + (* next_block k : this function reads the next block of Coq output + * removing the k leading prompts. + * it returns the block as a list of string) *) + let last_read = ref "" in + let next_block k = + if !last_read = "" then last_read := input_line c_coq; + (* skip k prompts *) + for i = 1 to k do + last_read := remove_prompt !last_read; + done; + (* read and return the following lines until a prompt is found *) + let rec read_lines () = + let s = input_line c_coq in + if Str.string_match any_prompt s 0 then begin + last_read := s; [] + end else + s :: (read_lines ()) + in + let first = !last_read in first :: (read_lines ()) + in + (* we are just after \end{coq_...} block *) + let rec just_after () = + let s = input_line c_tex in + if Str.string_match begin_coq_example s 0 then begin + inside (Str.matched_group 1 s <> "example*") + (Str.matched_group 1 s <> "example#") 0 false + end + else begin + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n"; + if Str.string_match begin_coq_eval s 0 then + eval 0 + else begin + output_string c_out (s ^ "\n"); + outside () + end + end + (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) + and outside () = + let s = input_line c_tex in + if Str.string_match begin_coq_example s 0 then begin + if !small then output_string c_out "\\begin{small}\n"; + output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + inside (Str.matched_group 1 s <> "example*") + (Str.matched_group 1 s <> "example#") 0 true + end else if Str.string_match begin_coq_eval s 0 then + eval 0 + else begin + output_string c_out (s ^ "\n"); + outside () + end + (* we are inside a \begin{coq_example?} ... \end{coq_example?} block + * show_answers tells what kind of block it is + * k is the number of lines read until now *) + and inside show_answers show_questions k first_block = + let s = input_line c_tex in + if Str.string_match end_coq_example s 0 then begin + just_after () + end else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if (not first_block) & k=0 then output_string c_out "\\medskip\n"; + if show_questions then encapsule false c_out ("Coq < " ^ s); + if has_match dot_end_line s then begin + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions 0 false + end else + inside show_answers show_questions (succ k) first_block + end + (* we are inside a \begin{coq_eval} ... \end{coq_eval} block + * k is the number of lines read until now *) + and eval k = + let s = input_line c_tex in + if Str.string_match end_coq_eval s 0 then + outside () + else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if has_match dot_end_line s then + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + eval 0 + else + eval (succ k) + end + in + try + let _ = next_block 0 in (* to skip the Coq banner *) + let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) + outside () + with End_of_file -> begin + close_in c_tex; + close_in c_coq; + close_out c_out + end + +(* Process of one TeX file *) + +let rm f = try Sys.remove f with _ -> () + +let one_file texfile = + let inputv = Filename.temp_file "coq_tex" ".v" in + let coq_output = Filename.temp_file "coq_tex" ".coq_output"in + let result = + if !output_specified then + !output + else if Filename.check_suffix texfile ".tex" then + (Filename.chop_suffix texfile ".tex") ^ ".v.tex" + else + texfile ^ ".v.tex" + in + try + (* 1. extract Coq phrases *) + extract texfile inputv; + (* 2. run Coq on input *) + let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv + coq_output) + in + (* 3. insert Coq output into original file *) + insert texfile coq_output result; + (* 4. clean up *) + rm inputv; rm coq_output + with e -> begin + rm inputv; rm coq_output; + raise e + end + +(* Parsing of the command line, check of the Coq command and process + * of all the files in the command line, one by one *) + +let files = ref [] + +let parse_cl () = + Arg.parse + [ "-o", Arg.String (fun s -> output_specified := true; output := s), + "output-file Specifiy the resulting LaTeX file"; + "-n", Arg.Int (fun n -> linelen := n), + "line-width Set the line width"; + "-image", Arg.String (fun s -> image := s), + "coq-image Use coq-image as Coq command"; + "-w", Arg.Set cut_at_blanks, + " Try to cut lines at blanks"; + "-v", Arg.Set verbose, + " Verbose mode (show Coq answers on stdout)"; + "-sl", Arg.Set slanted, + " Coq answers in slanted font (only with LaTeX2e)"; + "-hrule", Arg.Set hrule, + " Coq parts are written between 2 horizontal lines"; + "-small", Arg.Set small, + " Coq parts are written in small font" + ] + (fun s -> files := s :: !files) + "coq-tex [options] file ..." + +let main () = + parse_cl (); + if !image = "" then begin + Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; + image := "coqtop" + end; + if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin + Printf.printf "Error: "; + let _ = Sys.command (!image ^ " -batch") in + exit 1 + end else begin + Printf.printf "Your version of coqtop seems OK\n"; + flush stdout + end; + List.iter one_file (List.rev !files) + +let _ = Printexc.catch main () diff --git a/tools/coq.el b/tools/coq.el new file mode 100644 index 00000000..0eb04d8d --- /dev/null +++ b/tools/coq.el @@ -0,0 +1,182 @@ +;; coq.el --- Coq mode editing commands for Emacs +;; +;; Jean-Christophe Filliatre, march 1995 +;; Honteusement pompé de caml.el, Xavier Leroy, july 1993. +;; +;; modified by Marco Maggesi for coq-inferior + +(defvar coq-mode-map nil + "Keymap used in Coq mode.") +(if coq-mode-map + () + (setq coq-mode-map (make-sparse-keymap)) + (define-key coq-mode-map "\t" 'coq-indent-command) + (define-key coq-mode-map "\M-\t" 'coq-unindent-command) + (define-key coq-mode-map "\C-c\C-c" 'compile) +) + +(defvar coq-mode-syntax-table nil + "Syntax table in use in Coq mode buffers.") +(if coq-mode-syntax-table + () + (setq coq-mode-syntax-table (make-syntax-table)) + ; ( is first character of comment start + (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) + ; * is second character of comment start, + ; and first character of comment end + (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) + ; ) is last character of comment end + (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) + ; quote is a string-like delimiter (for character literals) + (modify-syntax-entry ?' "\"" coq-mode-syntax-table) + ; quote is part of words + (modify-syntax-entry ?' "w" coq-mode-syntax-table) +) + +(defvar coq-mode-indentation 2 + "*Indentation for each extra tab in Coq mode.") + +(defun coq-mode-variables () + (set-syntax-table coq-mode-syntax-table) + (make-local-variable 'paragraph-start) + (setq paragraph-start (concat "^$\\|" page-delimiter)) + (make-local-variable 'paragraph-separate) + (setq paragraph-separate paragraph-start) + (make-local-variable 'paragraph-ignore-fill-prefix) + (setq paragraph-ignore-fill-prefix t) + (make-local-variable 'require-final-newline) + (setq require-final-newline t) + (make-local-variable 'comment-start) + (setq comment-start "(* ") + (make-local-variable 'comment-end) + (setq comment-end " *)") + (make-local-variable 'comment-column) + (setq comment-column 40) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip "(\\*+ *") + (make-local-variable 'parse-sexp-ignore-comments) + (setq parse-sexp-ignore-comments nil) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'coq-indent-command)) + +;;; The major mode + +(defun coq-mode () + "Major mode for editing Coq code. +Tab at the beginning of a line indents this line like the line above. +Extra tabs increase the indentation level. +\\{coq-mode-map} +The variable coq-mode-indentation indicates how many spaces are +inserted for each indentation level." + (interactive) + (kill-all-local-variables) + (setq major-mode 'coq-mode) + (setq mode-name "coq") + (use-local-map coq-mode-map) + (coq-mode-variables) + (run-hooks 'coq-mode-hook)) + +;;; Indentation stuff + +(defun coq-in-indentation () + "Tests whether all characters between beginning of line and point +are blanks." + (save-excursion + (skip-chars-backward " \t") + (bolp))) + +(defun coq-indent-command () + "Indent the current line in Coq mode. +When the point is at the beginning of an empty line, indent this line like +the line above. +When the point is at the beginning of an indented line +\(i.e. all characters between beginning of line and point are blanks\), +increase the indentation by one level. +The indentation size is given by the variable coq-mode-indentation. +In all other cases, insert a tabulation (using insert-tab)." + (interactive) + (let* ((begline + (save-excursion + (beginning-of-line) + (point))) + (current-offset + (- (point) begline)) + (previous-indentation + (save-excursion + (if (eq (forward-line -1) 0) (current-indentation) 0)))) + (cond ((and (bolp) + (looking-at "[ \t]*$") + (> previous-indentation 0)) + (indent-to previous-indentation)) + ((coq-in-indentation) + (indent-to (+ current-offset coq-mode-indentation))) + (t + (insert-tab))))) + +(defun coq-unindent-command () + "Decrease indentation by one level in Coq mode. +Works only if the point is at the beginning of an indented line +\(i.e. all characters between beginning of line and point are blanks\). +Does nothing otherwise." + (interactive) + (let* ((begline + (save-excursion + (beginning-of-line) + (point))) + (current-offset + (- (point) begline))) + (if (and (>= current-offset coq-mode-indentation) + (coq-in-indentation)) + (backward-delete-char-untabify coq-mode-indentation)))) + +;;; Hilight + +(cond + (window-system + (setq hilit-mode-enable-list '(not text-mode) + hilit-inhibit-hooks nil + hilit-inhibit-rebinding nil) + + (require 'hilit19) + (setq hilit-quietly t) + (hilit-set-mode-patterns + 'coq-mode + '(;;comments + ("(\\*" "\\*)" comment) + ;;strings + (hilit-string-find ?' string) + ;;directives + ("^[ \t]*\\(AddPath\\|DelPath\\|Add[ \t]+ML[ \t]+Path\\|Declare[ \t]+ML[ \t]+Module\\|Require\\|Export\\|Module\\|Opaque\\|Transparent\\|Section\\|Chapter\\|End\\|Load\\|Print\\|Show\\)[ \t]+[^.]*" nil include) + ("Implicit[ \t]+Arguments[ \t]+\\(On\\|Off\\)[^.]*" nil include) + ;;grammar definitions + ("^[ \t]*Syntax[ \t]+\\(tactic\\|command\\)" nil define) + ("^[ \t]*Syntax[ \t]+\\(tactic\\|command\\)[ \t]*level[ \t]+[0-9]+[ \t]*" nil define) + ("^[ \t]*level[ \t]+[0-9]+[ \t]*:" nil define) + ("^[ \t]*Grammar.*" ":=" define) + ("^[ \t]*Tactic[ \t]+Definition" ":=" define) + ("^[ \t]*Token[^.]*" nil define) + ("^[ \t]*\\(Coercion\\|Class\\|Infix\\)[ \t]+[[A-Za-z0-9$_\\']+" nil define) + ;;declarations + ("^[ \t]*Recursive[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*Syntactic[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*Tactic[ \t]+Definition[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*Inductive[ \t]+\\(Set\\|Prop\\|Type\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*Mutual[ \t]+\\(Inductive\\|CoInductive\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*\\(Inductive\\|CoInductive\\|CoFixpoint\\|Definition\\|Local\\|Fixpoint\\|with\\|Record\\|Correctness\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*\\(Derive\\|Dependant[ \t]+Derive\\)[ \t]+\\(Inversion\\|Inversion_clear\\)[ \t]+[A-Za-z0-9$_\\']+" nil defun) + ("^[ \t]*\\(Variable\\|Parameter\\|Hypothesis\\).*" ":" defun) + ("^[ \t]*\\(Global[ \t]+Variable\\).*" ":" defun) + ("^[ \t]*\\(Realizer[ \t]+Program\\|Realizer\\)" nil defun) + ;;proofs + ("^[ \t]*\\(Lemma\\|Theorem\\|Remark\\|Axiom\\).*" ":" defun) + ("^[ \t]*Proof" nil decl) + ("^[ \t]*\\(Save\\|Qed\\|Defined\\|Hint\\|Immediate\\)[^.]*" nil decl) + ;;keywords + ("[^_]\\<\\(Case\\|Cases\\|case\\|esac\\|of\\|end\\|in\\|Match\\|with\\|Fix\\|let\\|if\\|then\\|else\\)\\>[^_]" 1 keyword) + ("[^_]\\<\\(begin\\|assert\\|invariant\\|variant\\|for\\|while\\|do\\|done\\|state\\)\\>[^_]" 1 keyword) + )) +)) + +;;; coq.el ends here + +(provide 'coq) diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 new file mode 100644 index 00000000..4879e97d --- /dev/null +++ b/tools/coq_makefile.ml4 @@ -0,0 +1,454 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Special of string * string * string (* file, dependencies, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | Include of string + | RInclude of string * string (* -R physicalpath logicalpath *) + +let output_channel = ref stdout +let makefile_name = ref "Makefile" +let make_name = ref "" + +let some_file = ref false +let some_vfile = ref false +let some_mlfile = ref false + +let opt = ref "-opt" +let impredicative_set = ref false + +let print x = output_string !output_channel x +let printf x = Printf.fprintf !output_channel x + +let rec print_list sep = function + | [ x ] -> print x + | x :: l -> print x; print sep; print_list sep l + | [] -> () + +let section s = + let l = String.length s in + let sep = String.make (l+5) '#' + and sep2 = String.make (l+5) ' ' in + String.set sep (l+4) '\n'; + String.set sep2 0 '#'; + String.set sep2 (l+3) '#'; + String.set sep2 (l+4) '\n'; + print sep; + print sep2; + print "# "; print s; print " #\n"; + print sep2; + print sep; + print "\n" + +let usage () = + output_string stderr "Usage summary: + +coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom + command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] + ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + +[file.v]: Coq file to be compiled +[file.ml]: ML file to be compiled +[subdirectory] : subdirectory that should be \"made\" +[-custom command dependencies file]: add target \"file\" with command + \"command\" and dependencies \"dependencies\" +[-I dir]: look for dependencies in \"dir\" +[-R physicalpath logicalpath]: look for dependencies resursively starting from + \"physicalpath\". The logical path associated to the physical path is + \"logicalpath\". +[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" +[-byte]: compile with byte-code version of coq +[-opt]: compile with native-code version of coq +[-impredicative-set]: compile with option -impredicative-set of coq +[-f file]: take the contents of file as arguments +[-o file]: output should go in file file +[-h]: print this usage summary +[--help]: equivalent to [-h]\n"; + exit 1 + +let standard sds = + print "byte:\n"; + print "\t$(MAKE) all \"OPT=\"\n\n"; + print "opt:\n"; + if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; + print "\t$(MAKE) all \"OPT="; print !opt; print "\"\n\n"; + if !some_file then print "include .depend\n\n"; + print ".depend depend:\n"; + if !some_file then begin + print "\trm -f .depend\n"; + print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n"; + print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n"; + end; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") + sds; + print "\n"; + print "install:\n"; + print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; + if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; + if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + sds; + print "\n"; + if !make_name <> "" then begin + printf "%s: %s\n" !makefile_name !make_name; + printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; + printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name; + print "\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + sds; + print "\n"; + end; + print "clean:\n"; + print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n"; + print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") + sds; + print "\n"; + print "archclean:\n"; + print "\trm -f *.cmx *.o\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") + sds; + print "\n"; + print "html:\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) html)\n") + sds; + print "\n" + +let implicit () = + let ml_rules () = + print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + and v_rule () = + print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.g:\n\t$(GALLINA) $<\n\n"; + print ".v.tex:\n\t$(COQDOC) -latex $< -o $@\n\n"; + print ".v.html:\n\t$(COQDOC) -html $< -o $@\n\n"; + print ".v.g.tex:\n\t$(COQDOC) -latex -g $< -o $@\n\n"; + print ".v.g.html:\n\t$(COQDOC) -html -g $< -o $@\n\n" + and ml_suffixes = + if !some_mlfile then + [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ] + else + [] + and v_suffixes = + if !some_vfile then + [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] + else + [] + in + let suffixes = ml_suffixes @ v_suffixes in + if suffixes <> [] then begin + print ".SUFFIXES: "; print_list " " suffixes; + print "\n\n" + end; + if !some_mlfile then ml_rules (); + if !some_vfile then v_rule () + +let variables l = + let rec var_aux = function + | [] -> () + | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r + | _ :: r -> var_aux r + in + section "Variables definitions."; + print "CAMLP4LIB=`camlp4 -where`\n"; +(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) + print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + -I $(COQTOP)/library -I $(COQTOP)/parsing \\ + -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ + -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ + -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\ + -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\ + -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \\ + -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\ + -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\ + -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\ + -I $(CAMLP4LIB)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; + if !opt = "-byte" then + print "override OPT=-byte\n" + else + print "OPT=\n"; + if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "COQC=$(COQBIN)coqc\n"; + print "GALLINA=gallina\n"; + print "COQDOC=coqdoc\n"; + print "CAMLC=ocamlc -c\n"; + print "CAMLOPTC=ocamlopt -c\n"; + print "CAMLLINK=ocamlc\n"; + print "CAMLOPTLINK=ocamlopt\n"; + print "COQDEP=$(COQBIN)coqdep -c\n"; + print "GRAMMARS=grammar.cma\n"; + print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; + print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; + var_aux l; + print "\n" + +let include_dirs l = + let include_aux' includeR = + let rec include_aux = function + | [] -> [] + | Include x :: r -> ("-I " ^ x) :: (include_aux r) + | RInclude (p,l) :: r when includeR -> + let l' = if l = "" then "\"\"" else l in + ("-R " ^ p ^ " " ^ l') :: (include_aux r) + | _ :: r -> include_aux r + in + include_aux + in + let i_ocaml = "-I ." :: (include_aux' false l) in + let i_coq = "-I ." :: (include_aux' true l) in + section "Libraries definition."; + print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n"; + print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n" + +let special l = + let pr_sp (file,dependencies,com) = + print file; print ": "; print dependencies; print "\n"; + print "\t"; print com; print "\n\n" + in + let rec sp_aux = function + | [] -> [] + | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r) + | _ :: r -> sp_aux r + in + let sps = sp_aux l in + if sps <> [] then section "Custom targets."; + List.iter pr_sp sps + +let subdirs l = + let rec subdirs_aux = function + | [] -> [] + | Subdir x :: r -> x :: (subdirs_aux r) + | _ :: r -> subdirs_aux r + and pr_subdir s = + print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" + in + let sds = subdirs_aux l in + if sds <> [] then section "Subdirectories."; + List.iter pr_subdir sds; + section "Special targets."; + print ".PHONY: "; + print_list " " + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" + :: "depend" :: "html" :: sds); + print "\n\n"; + sds + +(* Extract gallina/html filenames (foo.v) from the list of all targets *) + +let rec other_files suff = function + | V n :: r -> + let f = (Filename.chop_suffix n ".vo") ^ suff in + f :: (other_files suff r) + | _ :: r -> + other_files suff r + | [] -> + [] + +let vfiles = other_files ".v" +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 + | ML n :: r -> n :: (fnames r) + | Subdir n :: r -> n :: (fnames r) + | V n :: r -> n :: (fnames r) + | Special (n,_,_) :: r -> n :: (fnames r) + | Include _ :: r -> fnames r + | RInclude _ :: r -> fnames r + | Def _ :: r -> fnames r + | [] -> [] + in + section "Definition of the \"all\" target."; + print "VFILES="; print_list "\\\n " (vfiles l); print "\n"; + print "VOFILES=$(VFILES:.v=.vo)\n"; + print "VIFILES=$(VFILES:.v=.vi)\n"; + print "GFILES=$(VFILES:.v=.g)\n"; + print "HTMLFILES=$(VFILES:.v=.html)\n"; + print "GHTMLFILES=$(VFILES:.v=.g.html)\n"; + print "\n"; + print "all: "; print_list "\\\n " (fnames l); + print "\n\n"; + if !some_vfile then begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(HTMLFILES)\n\n"; + print "gallinahtml: $(GHTMLFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(VFILES)\n"; + print "\t$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "\n\n" + end + +let parse f = + let rec string = parser + | [< '' ' | '\n' | '\t' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(string s) + | [< >] -> "" + and string2 = parser + | [< ''"' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(string2 s) + and skip_comment = parser + | [< ''\n'; s >] -> s + | [< 'c; s >] -> skip_comment s + | [< >] -> [< >] + and args = parser + | [< '' ' | '\n' | '\t'; s >] -> args s + | [< ''#'; s >] -> args (skip_comment s) + | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s + | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) + | [< >] -> [] + in + let c = open_in f in + let res = args (Stream.of_channel c) in + close_in c; + res + +let rec process_cmd_line = function + | [] -> + some_file := !some_file or !some_mlfile or !some_vfile; [] + | ("-h"|"--help") :: _ -> + usage () + | ("-no-opt"|"-byte") :: r -> + opt := "-byte"; process_cmd_line r + | ("-full"|"-opt") :: r -> + opt := "-opt"; process_cmd_line r + | "-impredicative-set" :: r -> + impredicative_set := true; process_cmd_line r + | "-custom" :: com :: dependencies :: file :: r -> + some_file := true; + Special (file,dependencies,com) :: (process_cmd_line r) + | "-I" :: d :: r -> + Include d :: (process_cmd_line r) + | "-R" :: p :: l :: r -> + RInclude (p,l) :: (process_cmd_line r) + | ("-I"|"-custom") :: _ -> + usage () + | "-f" :: file :: r -> + make_name := file; + process_cmd_line ((parse file)@r) + | ["-f"] -> + usage () + | "-o" :: file :: r -> + makefile_name := file; + output_channel := (open_out file); + (process_cmd_line r) + | v :: "=" :: def :: r -> + Def (v,def) :: (process_cmd_line r) + | f :: r -> + if Filename.check_suffix f ".v" then begin + some_vfile := true; + V (f^"o") :: (process_cmd_line r) + end else if Filename.check_suffix f ".ml" then begin + some_mlfile := true; + ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r) + end else + Subdir f :: (process_cmd_line r) + +let banner () = + print +"############################################################################## +## The Calculus of Inductive Constructions ## +## ## +## Projet Coq ## +## ## +## INRIA ENS-CNRS ## +## Rocquencourt Lyon ## +## ## +## Coq V7 ## +## ## +## ## +############################################################################## + +" + +let warning () = + print "# WARNING\n#\n"; + print "# This Makefile has been automagically generated by coq_makefile\n"; + print "# Edit at your own risks !\n"; + print "#\n# END OF WARNING\n\n" + +let print_list l = List.iter (fun x -> print x; print " ") l + +let command_line args = + print "#\n# This Makefile was generated by the command line :\n"; + print "# coq_makefile "; + print_list args; + print "\n#\n\n" + +let directories_deps l = + let print_dep f dep = + if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end + in + let rec iter ((dirs,before) as acc) = function + | [] -> + () + | (Subdir d) :: l -> + print_dep d before; iter (d :: dirs, d :: before) l + | (ML f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (V f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (Special (f,_,_)) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | _ :: l -> + iter acc l + in + iter ([],[]) l + +let do_makefile args = + let l = process_cmd_line args in + banner (); + warning (); + command_line args; + variables l; + include_dirs l; + all_target l; + special l; + let sds = subdirs l in + implicit (); + standard sds; + (* TEST directories_deps l; *) + warning (); + if not (!output_channel == stdout) then close_out !output_channel; + exit 0 + +let main () = + let args = + if Array.length Sys.argv = 1 then usage (); + List.tl (Array.to_list Sys.argv) + in + do_makefile args + +let _ = Printexc.catch main () + diff --git a/tools/coqdep.ml b/tools/coqdep.ml new file mode 100755 index 00000000..ab7cef92 --- /dev/null +++ b/tools/coqdep.ml @@ -0,0 +1,537 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* " else + List.fold_left (/) (List.hd l) (List.tl l) + +let stderr = Pervasives.stderr +let stdout = Pervasives.stdout + +let coqlib = ref Coq_config.coqlib + +let option_c = ref false +let option_D = ref false +let option_w = ref false +let option_i = ref false +let option_sort = ref false + +let suffixe = ref ".vo" +let suffixe_spec = ref ".vi" + +type dir = string option + +(* Files specified on the command line *) +let mlAccu = ref ([] : (string * string * dir) list) +and mliAccu = ref ([] : (string * string * dir) list) +and vAccu = ref ([] : string list) + +(* Queue operations *) +let addQueue q v = q := v :: !q + +let safe_addQueue clq q (k,v) = + try + let v2 = List.assoc k !q in + if v<>v2 then + let rec add_clash = function + (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl + | cl::cltl -> cl::add_clash cltl + | [] -> [(k,[v;v2])] in + clq := add_clash !clq + with Not_found -> addQueue q (k,v) + +(* Files found in the loadpaths *) +let mlKnown = ref ([] : (string * dir) list) +and mliKnown = ref ([] : (string * dir) list) +and vKnown = ref ([] : (string list * string) list) +and coqlibKnown = ref ([] : (string list * string) list) + +let clash_v = ref ([]: (string list * string list) list) + + +let warning_module_notfound f s = + eprintf "*** Warning : in file %s, module " f; + eprintf "%s.v is required and has not been found in loadpath !\n" + (String.concat "." s); + flush stderr + +let warning_notfound f s = + eprintf "*** Warning : in file %s, the file " f; + eprintf "%s.v is required and has not been found !\n" s; + flush stderr + +let warning_clash file dir = + match List.assoc dir !clash_v with + (f1::f2::fl) -> + let f = Filename.basename f1 in + let d1 = Filename.dirname f1 in + let d2 = Filename.dirname f2 in + let dl = List.map Filename.dirname (List.rev fl) in + eprintf + "*** Warning : in file %s, \n required module %s is ambiguous!\n (found %s.v in " + file (String.concat "." dir) f; + List.iter (fun s -> eprintf "%s, " s) dl; + eprintf "%s and %s)\n" d2 d1 + | _ -> assert false + +let safe_assoc verbose file k = + if verbose && List.mem_assoc k !clash_v then warning_clash file k; + List.assoc k !vKnown + + + +let file_name = function + | (s,None) -> file_concat s + | (s,Some ".") -> file_concat s + | (s,Some d) -> d / file_concat s + +let traite_fichier_ML md ext = + try + let chan = open_in (md ^ ext) in + let buf = Lexing.from_channel chan in + let deja_vu = ref [md] in + let a_faire = ref "" in + let a_faire_opt = ref "" in + begin try + while true do + let (Use_module str) = caml_action buf in + if List.mem str !deja_vu then + () + else begin + addQueue deja_vu str; + begin try + let mlidir = List.assoc str !mliKnown in + let filename = file_name ([str],mlidir) in + a_faire := !a_faire ^ " " ^ filename ^ ".cmi"; + with Not_found -> + try + let mldir = List.assoc str !mlKnown in + let filename = file_name ([str],mldir) in + a_faire := !a_faire ^ " " ^ filename ^ ".cmo"; + with Not_found -> () + end; + begin try + let mldir = List.assoc str !mlKnown in + let filename = file_name ([str],mldir) in + a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmx" + with Not_found -> + try + let mlidir = List.assoc str !mliKnown in + let filename = file_name ([str],mlidir) in + a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmi" + with Not_found -> () + end + end + done + with Fin_fichier -> () + end; + close_in chan; + (!a_faire, !a_faire_opt) + with Sys_error _ -> ("","") + +let cut_prefix p s = + let lp = String.length p in + let ls = String.length s in + if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s + +let canonize f = match Sys.os_type with + | "Win32" -> cut_prefix ".\\" f + | _ -> cut_prefix "./" f + +let sort () = + let seen = Hashtbl.create 97 in + let rec loop file = + let file = canonize file in + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + let cin = open_in (file ^ ".v") in + let lb = Lexing.from_channel cin in + try + while true do + match coq_action lb with + | Require (_, s) -> + (try loop (List.assoc s !vKnown) with Not_found -> ()) + | RequireString (_, s) -> loop s + | _ -> () + done + with Fin_fichier -> + close_in cin; + printf "%s%s " file !suffixe + end + in + List.iter loop !vAccu + +let traite_fichier_Coq verbose f = + try + let chan = open_in f in + let buf = Lexing.from_channel chan in + let deja_vu_v = ref ([]: string list list) + and deja_vu_ml = ref ([] : string list) in + try + while true do + let tok = coq_action buf in + match tok with + | Require (spec,str) -> + if not (List.mem str !deja_vu_v) then begin + addQueue deja_vu_v str; + try + let file_str = safe_assoc verbose f str in + printf " %s%s" (canonize file_str) + (if spec then !suffixe_spec else !suffixe) + with Not_found -> + if verbose && not (List.mem_assoc str !coqlibKnown) then + warning_module_notfound f str + end + | RequireString (spec,s) -> + let str = Filename.basename s in + if not (List.mem [str] !deja_vu_v) then begin + addQueue deja_vu_v [str]; + try + let file_str = List.assoc [str] !vKnown in + printf " %s%s" (canonize file_str) + (if spec then !suffixe_spec else !suffixe) + with Not_found -> + begin try let _ = List.assoc [str] !coqlibKnown in () + with Not_found -> warning_notfound f s end + end + | Declare sl -> + List.iter + (fun str -> + if not (List.mem str !deja_vu_ml) then begin + addQueue deja_vu_ml str; + try + let mldir = List.assoc str !mlKnown in + printf " %s.cmo" (file_name ([str],mldir)) + with Not_found -> () + end) + sl + | Load str -> + let str = Filename.basename str in + if not (List.mem [str] !deja_vu_v) then begin + addQueue deja_vu_v [str]; + try + let file_str = List.assoc [str] !vKnown in + printf " %s.v" (canonize file_str) + with Not_found -> () + end + done + with Fin_fichier -> (); + close_in chan + with Sys_error _ -> () + + +let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 + +let mL_dep_list b f = + try + Hashtbl.find dep_tab f + with Not_found -> + let deja_vu = ref ([] : string list) in + try + let chan = open_in f in + let buf = Lexing.from_channel chan in + try + while true do + let (Use_module str) = caml_action buf in + if str = b then begin + eprintf "*** Warning : in file %s the" f; + eprintf " notation %s. is useless !\n" b; + flush stderr + end else + if not (List.mem str !deja_vu) then addQueue deja_vu str + done; [] + with Fin_fichier -> begin + close_in chan; + let rl = List.rev !deja_vu in + Hashtbl.add dep_tab f rl; + rl + end + with Sys_error _ -> [] + +let affiche_Declare f dcl = + printf "\n*** In file %s: \n" f; + printf "Declare ML Module"; + List.iter (fun str -> printf " \"%s\"" str) dcl; + printf ".\n"; + flush stdout + +let warning_Declare f dcl = + eprintf "*** Warning : in file %s, the ML modules" f; + eprintf " declaration should be\n"; + eprintf "*** Declare ML Module"; + List.iter (fun str -> eprintf " \"%s\"" str) dcl; + eprintf ".\n"; + flush stderr + +let traite_Declare f = + let decl_list = ref ([] : string list) in + let rec treat = function + | s :: ll -> + if (List.mem_assoc s !mlKnown) & not (List.mem s !decl_list) then begin + let mldir = List.assoc s !mlKnown in + let fullname = file_name ([s],mldir) in + let depl = mL_dep_list s (fullname ^ ".ml") in + treat depl; + decl_list := s :: !decl_list + end; + treat ll + | [] -> () + in + try + let chan = open_in f in + let buf = Lexing.from_channel chan in + begin try + while true do + let tok = coq_action buf in + (match tok with + | Declare sl -> + decl_list := []; + treat sl; + decl_list := List.rev !decl_list; + if !option_D then + affiche_Declare f !decl_list + else if !decl_list <> sl then + warning_Declare f !decl_list + | _ -> ()) + done + with Fin_fichier -> () end; + close_in chan + with Sys_error _ -> () + +let file_mem (f,_,d) = + let rec loop = function + | (f1,_,d1) :: l -> (f1 = f && d1 = d) || (loop l) + | _ -> false + in + loop + +let mL_dependencies () = + List.iter + (fun ((name,ext,dirname) as pairname) -> + let fullname = file_name ([name],dirname) in + let (dep,dep_opt) = traite_fichier_ML fullname ext in + printf "%s.cmo: %s%s" fullname fullname ext; + if file_mem pairname !mliAccu then printf " %s.cmi" fullname; + printf "%s\n" dep; + printf "%s.cmx: %s%s" fullname fullname ext; + if file_mem pairname !mliAccu then printf " %s.cmi" fullname; + printf "%s\n" dep_opt; + flush stdout) + (List.rev !mlAccu); + List.iter + (fun ((name,ext,dirname) as pairname) -> + let fullname = file_name ([name],dirname) in + let (dep,_) = traite_fichier_ML fullname ext in + printf "%s.cmi: %s%s" fullname fullname ext; + printf "%s\n" dep; + flush stdout) + (List.rev !mliAccu) + +let coq_dependencies () = + List.iter + (fun name -> + printf "%s%s: %s.v" name !suffixe name; + traite_fichier_Coq true (name ^ ".v"); + printf "\n"; + if !option_i then begin + printf "%s%s: %s.v" name !suffixe_spec name; + traite_fichier_Coq false (name ^ ".v"); + printf "\n"; + end; + flush stdout) + (List.rev !vAccu) + +let declare_dependencies () = + List.iter + (fun name -> + traite_Declare (name^".v"); + flush stdout) + (List.rev !vAccu) + +let rec warning_mult suf l = + let tab = Hashtbl.create 151 in + List.iter + (fun (f,d) -> + begin try + let d' = Hashtbl.find tab f in + if (Filename.dirname (file_name ([f],d))) + <> (Filename.dirname (file_name ([f],d'))) then begin + eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf); + flush stderr + end + with Not_found -> () end; + Hashtbl.add tab f d) + l + +(* Gives the list of all the directories under [dir], including [dir] *) +let all_subdirs root_dir log_dir = + let l = ref [(root_dir,[log_dir])] in + let add f = l := f :: !l in + let rec traverse phys_dir dir = + let dirh = handle_unix_error opendir phys_dir in + try + while true do + let f = readdir dirh in + if f <> "." && f <> ".." then + let file = dir@[f] in + let filename = phys_dir/f in + if (stat filename).st_kind = S_DIR then begin + add (filename,file); + traverse filename file + end + done + with End_of_file -> + closedir dirh + in + traverse root_dir [log_dir]; List.rev !l + +let usage () = + eprintf + "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] + ]\n"; + flush stderr; + exit 1 + +let add_coqlib_known dir_name f = + let complete_name = dir_name/f in + let lib_name = Filename.basename dir_name in + match try (stat complete_name).st_kind with _ -> S_BLK with + | S_REG -> + if Filename.check_suffix f ".vo" then + let basename = Filename.chop_suffix f ".vo" in + addQueue coqlibKnown ([basename],complete_name); + addQueue coqlibKnown (["Coq";lib_name;basename],complete_name) + | _ -> () + +let add_coqlib_directory dir_name = + match try (stat dir_name).st_kind with _ -> S_BLK with + | S_DIR -> + (let dir = opendir dir_name in + try + while true do add_coqlib_known dir_name (readdir dir) done + with End_of_file -> closedir dir) + | _ -> () + +let coqdep () = + let lg_command = Array.length Sys.argv in + if lg_command < 2 then usage (); + let rec treat old_dirname old_name = + let name = Filename.basename old_name + and new_dirname = Filename.dirname old_name in + let dirname = + match (old_dirname,new_dirname) with + | (d, ".") -> d + | (None,d) -> Some d + | (Some d1,d2) -> Some (d1/d2) + in + let complete_name = file_name ([name],dirname) in + match try (stat complete_name).st_kind with _ -> S_BLK with + | S_DIR -> + (if name <> "." & name <> ".." then + let dir=opendir complete_name in + let newdirname = + match dirname with + | None -> name + | Some d -> d/name + in + try + while true do treat (Some newdirname) (readdir dir) done + with End_of_file -> closedir dir) + | S_REG -> + if Filename.check_suffix name ".ml" then + let basename = Filename.chop_suffix name ".ml" in + addQueue mlAccu (basename,".ml",dirname) + else if Filename.check_suffix name ".ml4" then + let basename = Filename.chop_suffix name ".ml4" in + addQueue mlAccu (basename,".ml4",dirname) + else if Filename.check_suffix name ".mli" then + let basename = Filename.chop_suffix name ".mli" in + addQueue mliAccu (basename,".mli",dirname) + else if Filename.check_suffix name ".v" then + let basename = Filename.chop_suffix name ".v" in + addQueue vAccu (file_name ([basename], dirname)) + | _ -> () + in + let add_known phys_dir log_dir f = + let complete_name = phys_dir/f in + match try (stat complete_name).st_kind with _ -> S_BLK with + | S_REG -> + if Filename.check_suffix f ".ml" then + let basename = Filename.chop_suffix f ".ml" in + addQueue mlKnown (basename,Some phys_dir) + else if Filename.check_suffix f ".ml4" then + let basename = Filename.chop_suffix f ".ml4" in + addQueue mlKnown (basename,Some phys_dir) + else if Filename.check_suffix f ".mli" then + let basename = Filename.chop_suffix f ".mli" in + addQueue mliKnown (basename,Some phys_dir) + else if Filename.check_suffix f ".v" then + let basename = Filename.chop_suffix f ".v" in + let name = log_dir@[basename] in + let file = phys_dir/basename in + let paths = [name;[basename]] in + List.iter + (fun n -> safe_addQueue clash_v vKnown (n,file)) paths + | _ -> () in + let add_directory (phys_dir, log_dir) = + match try (stat phys_dir).st_kind with _ -> S_BLK with + | S_DIR -> + (let dir = opendir phys_dir in + try + while true do + add_known phys_dir log_dir (readdir dir) done + with End_of_file -> closedir dir) + | _ -> () + in + let add_rec_directory dir_name log_name = + List.iter add_directory (all_subdirs dir_name log_name) + in + let rec parse = function + | "-c" :: ll -> option_c := true; parse ll + | "-D" :: ll -> option_D := true; parse ll + | "-w" :: ll -> option_w := true; parse ll + | "-i" :: ll -> option_i := true; parse ll + | "-sort" :: ll -> option_sort := true; parse ll + | "-I" :: r :: ll -> add_directory (r, []); parse ll + | "-I" :: [] -> usage () + | "-R" :: r :: ln :: ll -> add_rec_directory r ln; parse ll + | "-R" :: ([] | [_]) -> usage () + | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll + | "-coqlib" :: [] -> usage () + | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll + | "-suffix" :: [] -> usage () + | f :: ll -> treat None f; parse ll + | [] -> () + in + add_directory (".", []); + parse (List.tl (Array.to_list Sys.argv)); + List.iter + (fun (s,_) -> add_coqlib_directory s) + (all_subdirs (!coqlib/"theories") "Coq"); + List.iter + (fun (s,_) -> add_coqlib_directory s) + (all_subdirs (!coqlib/"contrib") "Coq"); + mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu); + mlKnown := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu); + warning_mult ".mli" !mliKnown; + warning_mult ".ml" !mlKnown; +(* warning_mult ".v" (List.map (fun (s,d) -> (file_concat s, d)) + !vKnown);*) + if !option_sort then begin sort (); exit 0 end; + if !option_c && not !option_D then mL_dependencies (); + if not !option_D then coq_dependencies (); + if !option_w || !option_D then declare_dependencies () + +let _ = Printexc.catch coqdep () diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll new file mode 100755 index 00000000..4f5f172f --- /dev/null +++ b/tools/coqdep_lexer.mll @@ -0,0 +1,231 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* " | "." | ".." + | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" + | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" + | "-." { caml_action lexbuf } + + | ['!' '?' '~'] + ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * + { caml_action lexbuf } + | ['=' '<' '>' '@' '^' '|' '&' '$'] + ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * + { caml_action lexbuf } + | ['+' '-'] + ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * + { caml_action lexbuf } + | "**" + ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * + { caml_action lexbuf } + | ['*' '/' '%'] + ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * + { caml_action lexbuf } + | eof { raise Fin_fichier } + | _ { caml_action lexbuf } + +and comment = parse + | "(*" (* "*)" *) + { comment_depth := succ !comment_depth; comment lexbuf } + | "*)" + { comment_depth := pred !comment_depth; + if !comment_depth > 0 then comment lexbuf } + | "'" [^ '\\' '\''] "'" + { comment lexbuf } + | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" + { comment lexbuf } + | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" + { comment lexbuf } + | eof + { raise Fin_fichier } + | _ { comment lexbuf } + +and string = parse + | '"' (* '"' *) + { () } + | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * + { string lexbuf } + | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*) + { string lexbuf } + | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] + { string lexbuf } + | eof + { raise Fin_fichier } + | _ + { string lexbuf } + +and load_file = parse + | '"' [^ '"']* '"' (*'"'*) + { let s = lexeme lexbuf in + let f = String.sub s 1 (String.length s - 2) in + skip_to_dot lexbuf; + Load (if check_suffix f ".v" then chop_suffix f ".v" else f) } + | coq_ident + { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s } + | eof + { raise Fin_fichier } + | _ + { load_file lexbuf } + +and skip_to_dot = parse + | dot { () } + | eof { () } + | _ { skip_to_dot lexbuf } + +and opened_file = parse + | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf } + | space+ + { opened_file lexbuf } + | "Implementation" + { opened_file lexbuf } + | "Specification" + { specif := true; opened_file lexbuf } + | coq_ident + { module_name := [Lexing.lexeme lexbuf]; + opened_file_fields lexbuf } + + | '"' [^'"']* '"' { (*'"'*) + let lex = Lexing.lexeme lexbuf in + let str = String.sub lex 1 (String.length lex - 2) in + let str = + if Filename.check_suffix str ".v" then + Filename.chop_suffix str ".v" + else str in + RequireString (!specif, str) } + | eof { raise Fin_fichier } + | _ { opened_file lexbuf } + +and opened_file_fields = parse + | "(*" (* "*)" *) + { comment_depth := 1; comment lexbuf; + opened_file_fields lexbuf } + | space+ + { opened_file_fields lexbuf } + | coq_field + { module_name := + field_name (Lexing.lexeme lexbuf) :: !module_name; + opened_file_fields lexbuf } + | dot { Require (!specif, List.rev !module_name) } + | eof { raise Fin_fichier } + | _ { opened_file_fields lexbuf } + + +and modules = parse + | space+ { modules lexbuf } + | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; + modules lexbuf } + | '"' [^'"']* '"' + { let lex = (Lexing.lexeme lexbuf) in + let str = String.sub lex 1 (String.length lex - 2) in + mllist := str :: !mllist; modules lexbuf } + | _ { (Declare (List.rev !mllist)) } + +and qual_id = parse + | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) } + | eof { raise Fin_fichier } + | _ { caml_action lexbuf } + +and caml_opened_file = parse + | uppercase identchar* + { let lex = (Lexing.lexeme lexbuf) in + let str = String.sub lex 0 (String.length lex) in + (Use_module (String.uncapitalize str)) } + | eof {raise Fin_fichier } + | _ { caml_action lexbuf } + + + diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml new file mode 100644 index 00000000..2418b6e1 --- /dev/null +++ b/tools/coqdoc/alpha.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'A' + | '\199' -> 'C' + | '\200'..'\203' -> 'E' + | '\204'..'\207' -> 'I' + | '\209' -> 'N' + | '\210'..'\214' -> 'O' + | '\217'..'\220' -> 'U' + | '\221' -> 'Y' + | c -> c + +let norm_string s = + let u = String.copy s in + for i = 0 to String.length s - 1 do + u.[i] <- norm_char s.[i] + done; + u + +let compare_char c1 c2 = match norm_char c1, norm_char c2 with + | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2 + | 'A'..'Z', _ -> -1 + | _, 'A'..'Z' -> 1 + | c1, c2 -> compare c1 c2 + +let compare_string s1 s2 = + let n1 = String.length s1 in + let n2 = String.length s2 in + let rec cmp i = + if i == n1 || i == n2 then + n1 - n2 + else + let c = compare_char s1.[i] s2.[i] in + if c == 0 then cmp (succ i) else c + in + cmp 0 diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli new file mode 100644 index 00000000..46409c9a --- /dev/null +++ b/tools/coqdoc/alpha.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* char -> int +val compare_string : string -> string -> int + +(* Alphabetic normalization. *) + +val norm_char : char -> char +val norm_string : string -> string diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty new file mode 100644 index 00000000..7f7aa9aa --- /dev/null +++ b/tools/coqdoc/coqdoc.sty @@ -0,0 +1,58 @@ + +% This is coqdoc.sty, by Jean-Christophe Filliâtre +% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc) +% +% You can modify the following macros to customize the appearance +% of the document. + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{coqdoc}[2002/02/11] + +% Headings + +\usepackage{fancyhdr} +\newcommand{\coqdocleftpageheader}{\thepage\ -- \today} +\newcommand{\coqdocrightpageheader}{\today\ -- \thepage} +\pagestyle{fancyplain} + +%BEGIN LATEX +\plainheadrulewidth 0.4pt +\plainfootrulewidth 0pt +\lhead[\coqdocleftpageheader]{\leftmark} +\rhead[\leftmark]{\coqdocrightpageheader} +\cfoot{} +%END LATEX + +% Hevea puts to much space with \medskip and \bigskip +%HEVEA\renewcommand{\medskip}{} +%HEVEA\renewcommand{\bigskip}{} + +% own name +\newcommand{\coqdoc}{\textsf{coqdoc}} + +% pretty underscores (the package fontenc causes ugly underscores) +%BEGIN LATEX +\def\_{\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em} +%END LATEX + +% macro for typesetting keywords +\newcommand{\coqdockw}[1]{\textsf{#1}} + +% macro for typesetting identifiers +\newcommand{\coqdocid}[1]{\textit{#1}} + +% newline and indentation +%BEGIN LATEX +\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} +\newcommand{\coqdocindent}[1]{\noindent\kern#1} +%END LATEX +%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}
\end{rawhtml}} +%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}} + +% macro for typesetting the title of a module implementation +\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}} + +%HEVEA\newcommand{\lnot}{\coqwkw{not}} +%HEVEA\newcommand{\lor}{\coqwkw{or}} +%HEVEA\newcommand{\land}{\&} + diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli new file mode 100644 index 00000000..60c21387 --- /dev/null +++ b/tools/coqdoc/index.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* loc -> index_entry + +val add_module : coq_module -> unit + +type module_kind = Local | Coqlib | Unknown + +val find_module : coq_module -> module_kind + +(*s Scan identifiers introductions from a file *) + +val scan_file : string -> coq_module -> unit + +(*s Read globalizations from a file (produced by coqc -dump-glob) *) + +val read_glob : string -> unit + +(*s Indexes *) + +type 'a index = { + idx_name : string; + idx_entries : (char * (string * 'a) list) list; + idx_size : int } + +val all_entries : unit -> + (coq_module * entry_type) index * + (entry_type * coq_module index) list + +val map : (string -> 'a -> 'b) -> 'a index -> 'b index + diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll new file mode 100644 index 00000000..799825ad --- /dev/null +++ b/tools/coqdoc/index.mll @@ -0,0 +1,327 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + "", s + +let modules = Hashtbl.create 97 +let local_modules = Hashtbl.create 97 + +let add_module m = + let _,id = split_sp m in + Hashtbl.add modules id m; + Hashtbl.add local_modules m () + +type module_kind = Local | Coqlib | Unknown + +let coq_module m = + String.length m >= 4 && String.sub m 0 4 = "Coq." + +let find_module m = + if Hashtbl.mem local_modules m then + Local + else if coq_module m then + Coqlib + else + Unknown + +let ref_module loc s = + try + let n = String.length s in + let i = String.rindex s ' ' in + let id = String.sub s (i+1) (n-i-1) in + add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id + with Not_found -> + () + +(* Building indexes *) + +type 'a index = { + idx_name : string; + idx_entries : (char * (string * 'a) list) list; + idx_size : int } + +let map f i = + { i with idx_entries = + List.map + (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l)) + i.idx_entries } + +let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2 + +let sort_entries el = + let t = Hashtbl.create 97 in + List.iter + (fun c -> Hashtbl.add t c []) + ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; + 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_']; + List.iter + (fun ((s,_) as e) -> + let c = Alpha.norm_char s.[0] in + let l = try Hashtbl.find t c with Not_found -> [] in + Hashtbl.replace t c (e :: l)) + el; + let res = ref [] in + Hashtbl.iter + (fun c l -> res := (c, List.sort compare_entries l) :: !res) t; + List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res + +let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0 + +let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h [] + +let type_name = function + | Library -> "library" + | Module -> "module" + | Definition -> "definition" + | Inductive -> "inductive" + | Constructor -> "constructor" + | Lemma -> "lemma" + | Variable -> "variable" + | Axiom -> "axiom" + | TacticDefinition -> "tactic" + +let all_entries () = + let gl = ref [] in + let add_g s m t = gl := (s,(m,t)) :: !gl in + let bt = Hashtbl.create 11 in + let add_bt t s m = + let l = try Hashtbl.find bt t with Not_found -> [] in + Hashtbl.replace bt t ((s,m) :: l) + in + let classify (m,_) e = match e with + | Def (s,t) -> add_g s m t; add_bt t s m + | Ref _ | Mod _ -> () + in + Hashtbl.iter classify table; + Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; + { idx_name = "global"; + idx_entries = sort_entries !gl; + idx_size = List.length !gl }, + Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; + idx_entries = sort_entries e; + idx_size = List.length e }) :: l) bt [] + +} + +(*s Shortcuts for regular expressions. *) + +let space = + [' ' '\010' '\013' '\009' '\012'] +let firstchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] +let identchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' + '\'' '0'-'9'] +let ident = + firstchar identchar* + +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" +let end_hide = "(*" space* "end" space+ "hide" space* "*)" + +(*s Indexing entry point. *) + +rule traverse = parse + | "Definition" space + { current_type := Definition; index_ident lexbuf; traverse lexbuf } + | "Tactic" space+ "Definition" space + { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf } + | ("Axiom" | "Parameter") space + { current_type := Axiom; index_ident lexbuf; traverse lexbuf } + | "Fixpoint" space + { current_type := Definition; index_ident lexbuf; fixpoint lexbuf; + traverse lexbuf } + | ("Lemma" | "Theorem") space + { current_type := Lemma; index_ident lexbuf; traverse lexbuf } + | "Inductive" space + { current_type := Inductive; + index_ident lexbuf; inductive lexbuf; traverse lexbuf } + | "Record" space + { current_type := Inductive; index_ident lexbuf; traverse lexbuf } + | "Module" (space+ "Type")? space + { current_type := Module; index_ident lexbuf; traverse lexbuf } +(*i*** + | "Variable" 's'? space + { current_type := Variable; index_idents lexbuf; traverse lexbuf } +***i*) + | "Require" (space+ "Export")? space+ ident + { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf } + | begin_hide + { skip_hide lexbuf; traverse lexbuf } + | "(*" + { comment lexbuf; traverse lexbuf } + | '"' + { string lexbuf; traverse lexbuf } + | eof + { () } + | _ + { traverse lexbuf } + +(*s Index one identifier. *) + +and index_ident = parse + | space+ + { index_ident lexbuf } + | ident + { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) } + | eof + { () } + | _ + { () } + +(*s Index identifiers separated by blanks and/or commas. *) + +and index_idents = parse + | space+ | ',' + { index_idents lexbuf } + | ident + { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf); + index_idents lexbuf } + | eof + { () } + | _ + { skip_until_point lexbuf } + +(*s Index identifiers in an inductive definition (types and constructors). *) + +and inductive = parse + | '|' | ":=" space* '|'? + { current_type := Constructor; index_ident lexbuf; inductive lexbuf } + | "with" space + { current_type := Inductive; index_ident lexbuf; inductive lexbuf } + | '.' + { () } + | eof + { () } + | _ + { inductive lexbuf } + +(*s Index identifiers in a Fixpoint declaration. *) + +and fixpoint = parse + | "with" space + { index_ident lexbuf; fixpoint lexbuf } + | '.' + { () } + | eof + { () } + | _ + { fixpoint lexbuf } + +(*s Skip a possibly nested comment. *) + +and comment = parse + | "*)" { () } + | "(*" { comment lexbuf; comment lexbuf } + | '"' { string lexbuf; comment lexbuf } + | eof { eprintf " *** Unterminated comment while indexing" } + | _ { comment lexbuf } + +(*s Skip a constant string. *) + +and string = parse + | '"' { () } + | eof { eprintf " *** Unterminated string while indexing" } + | _ { string lexbuf } + +(*s Skip everything until the next dot. *) + +and skip_until_point = parse + | '.' { () } + | eof { () } + | _ { skip_until_point lexbuf } + +(*s Skip everything until [(* end hide *)] *) + +and skip_hide = parse + | eof | end_hide { () } + | _ { skip_hide lexbuf } + +{ + + let read_glob f = + let c = open_in f in + let cur_mod = ref "" in + try + while true do + let s = input_line c in + let n = String.length s in + if n > 0 then begin + match s.[0] with + | 'F' -> + cur_mod := String.sub s 1 (n - 1) + | 'R' -> + (try + let i = String.index s ' ' in + let loc = int_of_string (String.sub s 1 (i - 1)) in + let sp = String.sub s (i + 1) (n - i - 1) in + let m',id = split_sp sp in + add_ref !cur_mod loc m' id + with Not_found -> + ()) + | _ -> () + end + done + with End_of_file -> + close_in c + + let scan_file f m = + current_module := m; + let c = open_in f in + let lb = from_channel c in + traverse lb; + close_in c +} diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml new file mode 100644 index 00000000..66d2a993 --- /dev/null +++ b/tools/coqdoc/main.ml @@ -0,0 +1,420 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* on 9 & 10 Mar 2004: + * - handling of absolute filenames (function coq_module) + * - coq_module: chop ./// (arbitrary amount of slashes), not only "./" + * - function chop_prefix not useful anymore. Deleted. + * - correct typo in usage message: "-R" -> "--R" + * - shorten the definition of make_path + * This notice is made to comply with section 2.a of the GPLv2. + * It may be removed or abbreviated as far as I am concerned. + *) + +open Filename +open Printf +open Output +open Pretty + +(*s \textbf{Usage.} Printed on error output. *) + +let usage () = + prerr_endline ""; + prerr_endline "Usage: coqdoc "; + prerr_endline " --html produce a HTML document (default)"; + prerr_endline " --latex produce a LaTeX document"; + prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --dvi output the DVI"; + prerr_endline " --ps output the PostScript"; + prerr_endline " -o write output in file "; + prerr_endline " -d output files into directory "; + prerr_endline " -g (gallina) skip proofs"; + prerr_endline " -s (short) no titles for files"; + prerr_endline " -l light mode (only defs and statements)"; + prerr_endline " -t give a title to the document"; + prerr_endline " --body-only suppress LaTeX/HTML header and trailer"; + prerr_endline " --no-index do not output the index"; + prerr_endline " --multi-index index split in multiple files"; + prerr_endline " --toc output a table of contents"; + prerr_endline " --vernac consider as a .v file"; + prerr_endline " --tex consider as a .tex file"; + prerr_endline " -p insert in LaTeX preamble"; + prerr_endline " --files-from read file names to process in "; + prerr_endline " --quiet quiet mode"; + prerr_endline " --glob-from read Coq globalizations from file "; + prerr_endline " --no-externals no links to Coq standard library"; + prerr_endline " --coqlib set URL for Coq standard library"; + prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline " -R map physical dir to Coq dir"; + prerr_endline " --latin1 set ISO-8859-1 input language"; + prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --charset set HTML charset"; + prerr_endline " --inputenc set LaTeX input encoding"; + prerr_endline ""; + prerr_endline + "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n"; + exit 1 + +(*s \textbf{Banner.} Always printed. Notice that it is printed on error + output, so that when the output of [coqdoc] is redirected this header + is not (unless both standard and error outputs are redirected, of + course). *) + +let banner () = + eprintf "This is coqdoc version %s, compiled on %s\n" + Coq_config.version Coq_config.compile_date; + flush stderr + + +(*s \textbf{Separation of files.} Files given on the command line are + separated according to their type, which is determined by their + suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\ + files have suffix \verb!.tex!. *) + +let check_if_file_exists f = + if not (Sys.file_exists f) then begin + eprintf "\ncoqdoc: %s: no such file\n" f; + exit 1 + end + +let paths = ref [] + +let add_path m l = paths := (m,l) :: !paths + +let exists_dir dir = + try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false + +let add_rec_path f l = + let rec traverse abs rel = + add_path abs rel; + let dirh = Unix.opendir abs in + try + while true do + let f = Unix.readdir dirh in + if f <> "" && f.[0] <> '.' && f <> "CVS" then + let abs' = Filename.concat abs f in + try + if exists_dir abs' then traverse abs' (rel ^ "." ^ f) + with Unix.Unix_error _ -> + () + done + with End_of_file -> + Unix.closedir dirh + in + if exists_dir f then traverse f l + +(* turn A/B/C into A.B.C *) +let make_path = Str.global_replace (Str.regexp "/") ".";; + +let coq_module file = +(* TODO + * LEM: + * We should also remove things like "/./" in the middle of the filename, + * rewrite "/foo/../bar" to "/bar", recognise different paths that lead + * to the same file / directory (via symlinks), etc. The best way to do + * all this would be to use the libc function realpath() on _both_ p and + * file / f before comparing them. + * + * The semantics of realpath() on file symlinks might not be what we + * want... (But it is what we want on directory symlinks.) So, we would + * have to cook up our own version of realpath()? + * + * Do all target platforms have realpath()? + *) + let f = chop_extension file in + (* remove leading ./ and any number of slashes after *) + let f = Str.replace_first (Str.regexp "^\\./+") "" f in + if (Str.string_before f 1) = "/" then + (* f is an absolute path. Prefixes must be matched with the beginning of f, + * not prepended + *) + let rec trypath = function + | [] -> make_path f + | (p, lg) :: r -> + (* make sure p ends with a single '/' + * This guarantees that we don't match a file whose name is + * of the form p ^ "foo". It means we may miss p itself, + * but this does not matter: coqdoc doesn't do anything + * of a directory anyway. *) + let p = (Str.replace_first (Str.regexp "/*$") "/" p) in + let p_quoted = (Str.quote p) in + if (Str.string_match (Str.regexp p_quoted) f 0) then + make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f)) + else + trypath r + in trypath !paths + else (* f is a relative path *) + let rec trypath = function + | [] -> + make_path f + | (p,lg) :: r -> + let p_file = Filename.concat p file in + if Sys.file_exists p_file then + make_path (Filename.concat lg f) + else + trypath r + in trypath !paths;; + +let what_file f = + check_if_file_exists f; + if check_suffix f ".v" || check_suffix f ".g" then + Vernac_file (f, coq_module f) + else if check_suffix f ".tex" then + Latex_file f + else begin + eprintf "\ncoqdoc: don't know what to do with %s\n" f; + exit 1 + end + +(*s \textbf{Reading file names from a file.} + File names may be given + in a file instead of being given on the command + line. [(files_from_file f)] returns the list of file names contained + in the file named [f]. These file names must be separated by spaces, + tabulations or newlines. + *) + +let files_from_file f = + let files_from_channel ch = + let buf = Buffer.create 80 in + let l = ref [] in + try + while true do + match input_char ch with + | ' ' | '\t' | '\n' -> + if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l; + Buffer.clear buf + | c -> + Buffer.add_char buf c + done; [] + with End_of_file -> + List.rev !l + in + try + check_if_file_exists f; + let ch = open_in f in + let l = files_from_channel ch in + close_in ch;l + with Sys_error s -> begin + eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s; + exit 1 + end + +(*s \textbf{Parsing of the command line.} *) + +let output_file = ref "" +let dvi = ref false +let ps = ref false + +let parse () = + let files = ref [] in + let add_file f = files := f :: !files in + let rec parse_rec = function + | [] -> () + + | ("-nopreamble" | "--nopreamble" | "--no-preamble" + | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> + header_trailer := false; parse_rec rem + | ("-p" | "--preamble") :: s :: rem -> + push_in_preamble s; parse_rec rem + | ("-p" | "--preamble") :: [] -> + usage () + | ("-noindex" | "--noindex" | "--no-index") :: rem -> + index := false; parse_rec rem + | ("-multi-index" | "--multi-index") :: rem -> + multi_index := true; parse_rec rem + | ("-toc" | "--toc" | "--table-of-contents") :: rem -> + toc := true; parse_rec rem + | ("-o" | "--output") :: f :: rem -> + output_file := f; parse_rec rem + | ("-o" | "--output") :: [] -> + usage () + | ("-d" | "--directory") :: dir :: rem -> + output_dir := dir; parse_rec rem + | ("-d" | "--directory") :: [] -> + usage () + | ("-s" | "--short") :: rem -> + short := true; parse_rec rem + | ("-l" | "-light" | "--light") :: rem -> + gallina := true; light := true; parse_rec rem + | ("-g" | "-gallina" | "--gallina") :: rem -> + gallina := true; parse_rec rem + | ("-t" | "-title" | "--title") :: s :: rem -> + title := s; parse_rec rem + | ("-t" | "-title" | "--title") :: [] -> + usage () + | ("-latex" | "--latex") :: rem -> + Output.target_language := LaTeX; parse_rec rem + | ("-dvi" | "--dvi") :: rem -> + Output.target_language := LaTeX; dvi := true; parse_rec rem + | ("-ps" | "--ps") :: rem -> + Output.target_language := LaTeX; ps := true; parse_rec rem + | ("-html" | "--html") :: rem -> + Output.target_language := HTML; parse_rec rem + | ("-texmacs" | "--texmacs") :: rem -> + Output.target_language := TeXmacs; parse_rec rem + + | ("-charset" | "--charset") :: s :: rem -> + Output.charset := s; parse_rec rem + | ("-charset" | "--charset") :: [] -> + usage () + | ("-inputenc" | "--inputenc") :: s :: rem -> + Output.inputenc := s; parse_rec rem + | ("-inputenc" | "--inputenc") :: [] -> + usage () + | ("-raw-comments" | "--raw-comments") :: rem -> + Output.raw_comments := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> + Output.set_latin1 (); parse_rec rem + | ("-utf8" | "--utf8") :: rem -> + Output.set_utf8 (); parse_rec rem + + | ("-q" | "-quiet" | "--quiet") :: rem -> + quiet := true; parse_rec rem + + | ("-h" | "-help" | "-?" | "--help") :: rem -> + banner (); usage () + | ("-v" | "-version" | "--version") :: _ -> + banner (); exit 0 + + | ("-vernac-file" | "--vernac-file") :: f :: rem -> + check_if_file_exists f; + add_file (Vernac_file (f, coq_module f)); parse_rec rem + | ("-vernac-file" | "--vernac-file") :: [] -> + usage () + | ("-tex-file" | "--tex-file") :: f :: rem -> + add_file (Latex_file f); parse_rec rem + | ("-tex-file" | "--tex-file") :: [] -> + usage () + | ("-files" | "--files" | "--files-from") :: f :: rem -> + List.iter (fun f -> add_file (what_file f)) (files_from_file f); + parse_rec rem + | ("-files" | "--files") :: [] -> + usage () + + | "-R" :: path :: log :: rem -> + add_path path log; parse_rec rem + | "-R" :: ([] | [_]) -> + usage () + | ("-glob-from" | "--glob-from") :: f :: rem -> + Index.read_glob f; parse_rec rem + | ("-glob-from" | "--glob-from") :: [] -> + usage () + | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> + Output.externals := false; parse_rec rem + | ("--coqlib" | "-coqlib") :: u :: rem -> + Output.coqlib := u; parse_rec rem + | ("--coqlib" | "-coqlib") :: [] -> + usage () + + | f :: rem -> + add_file (what_file f); parse_rec rem + in + parse_rec (List.tl (Array.to_list Sys.argv)); + List.rev !files + + +(*s The following function produces the output. The default output is + the \LaTeX\ document: in that case, we just call [Web.produce_document]. + If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then + we make calls to \verb!latex! or \verb!dvips! accordingly. *) + +let locally dir f x = + let cwd = Sys.getcwd () in + try + Sys.chdir dir; let y = f x in Sys.chdir cwd; y + with e -> + Sys.chdir cwd; raise e + +let clean_temp_files basefile = + let remove f = try Sys.remove f with _ -> () in + remove (basefile ^ ".tex"); + remove (basefile ^ ".log"); + remove (basefile ^ ".aux"); + remove (basefile ^ ".dvi"); + remove (basefile ^ ".ps"); + remove (basefile ^ ".haux"); + remove (basefile ^ ".html") + +let clean_and_exit file res = clean_temp_files file; exit res + +let cat file = + let c = open_in file in + try + while true do print_char (input_char c) done + with End_of_file -> + close_in c + +let copy src dst = + let cin = open_in src + and cout = open_out dst in + try + while true do Pervasives.output_char cout (input_char cin) done + with End_of_file -> + close_in cin; close_out cout + +let produce_output fl = + if not (!dvi || !ps) then begin + if !output_file <> "" then set_out_file !output_file; + produce_document fl + end else begin + let texfile = temp_file "coqdoc" ".tex" in + let basefile = chop_suffix texfile ".tex" in + set_out_file texfile; + produce_document fl; + let command = + let file = basename texfile in + let file = + if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file + in + sprintf "(latex %s && latex %s) 1>&2 %s" file file + (if !quiet then "> /dev/null" else "") + in + let res = locally (dirname texfile) Sys.command command in + if res <> 0 then begin + eprintf "Couldn't run LaTeX successfully\n"; + clean_and_exit basefile res + end; + let dvifile = basefile ^ ".dvi" in + if !dvi then begin + if !output_file <> "" then + (* we cannot use Sys.rename accross file systems *) + copy dvifile !output_file + else + cat dvifile + end; + if !ps then begin + let psfile = + if !output_file <> "" then !output_file else basefile ^ ".ps" + in + let command = + sprintf "dvips %s -o %s %s" dvifile psfile + (if !quiet then "> /dev/null 2>&1" else "") + in + let res = Sys.command command in + if res <> 0 then begin + eprintf "Couldn't run dvips successfully\n"; + clean_and_exit basefile res + end; + if !output_file = "" then cat psfile + end; + clean_temp_files basefile + end + + +(*s \textbf{Main program.} Print the banner, parse the command line, + read the files and then call [produce_document] from module [Web]. *) + +let main () = + let files = parse () in + if not !quiet then banner (); + if List.length files > 0 then produce_output files + +let _ = Printexc.catch main () diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml new file mode 100644 index 00000000..c10f3683 --- /dev/null +++ b/tools/coqdoc/output.ml @@ -0,0 +1,812 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "" then Filename.concat !output_dir f else f in + out_channel := open_out f; + output_is_file := true + +let close () = + if !output_is_file then close_out !out_channel + +let output_char c = Pervasives.output_char !out_channel c + +let output_string s = Pervasives.output_string !out_channel s + +let printf s = Printf.fprintf !out_channel s + +let sprintf = Printf.sprintf + +let dump_file f = + let ch = open_in f in + try + while true do + Pervasives.output_char !out_channel (input_char ch) + done + with End_of_file -> close_in ch + +(*s Options *) + +let header_trailer = ref true +let quiet = ref false +let light = ref false +let short = ref false +let index = ref true +let multi_index = ref false +let toc = ref false +let page_title = ref "" +let title = ref "" +let externals = ref true +let coqlib = ref "http://coq.inria.fr/library/" +let raw_comments = ref false + +let charset = ref "" +let inputenc = ref "" +let latin1 = ref false +let utf8 = ref false + +let set_latin1 () = + charset := "iso-8859-1"; + inputenc := "latin1"; + latin1 := true + +let set_utf8 () = + charset := "utf-8"; + inputenc := "utf8"; + utf8 := true + +(*s Coq keywords *) + +let build_table l = + let h = Hashtbl.create 101 in + List.iter (fun key ->Hashtbl.add h key ()) l; + function s -> try Hashtbl.find h s; true with Not_found -> false + +let is_keyword = + build_table + [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; + "CoInductive"; "Defined"; "Definition"; + "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; + "Hypothesis"; "Hypotheses"; + "Immediate"; "Implicit"; "Import"; "Inductive"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Module"; "Module Type"; "Declare Module"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; + "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; + "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "Unset"; "Variable"; "Variables"; + "Notation"; + (*i (* correctness *) + "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if"; + "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; + "while"; i*) + (*i (* coq terms *) + "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*) + ] + +(*s Current Coq module *) + +let current_module = ref "" + +let set_module m = current_module := m; page_title := m + +(*s Common to both LaTeX and HTML *) + +let item_level = ref 0 + +(*s Customized pretty-print *) + +let token_pp = Hashtbl.create 97 + +let add_printing_token = Hashtbl.replace token_pp + +let find_printing_token tok = + try Hashtbl.find token_pp tok with Not_found -> None, None + +let remove_printing_token = Hashtbl.remove token_pp + +(* predefined pretty-prints *) +let _ = List.iter + (fun (s,l) -> Hashtbl.add token_pp s (Some l, None)) + [ "*" , "\\ensuremath{\\times}"; + "->", "\\ensuremath{\\rightarrow}"; + "->~", "\\ensuremath{\\rightarrow\\lnot}"; + "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; + "<-", "\\ensuremath{\\leftarrow}"; + "<->", "\\ensuremath{\\leftrightarrow}"; + "=>", "\\ensuremath{\\Rightarrow}"; + "<=", "\\ensuremath{\\le}"; + ">=", "\\ensuremath{\\ge}"; + "<>", "\\ensuremath{\\not=}"; + "~", "\\ensuremath{\\lnot}"; + "/\\", "\\ensuremath{\\land}"; + "\\/", "\\ensuremath{\\lor}"; + "|-", "\\ensuremath{\\vdash}"; + "forall", "\\ensuremath{\\forall}"; + "exists", "\\ensuremath{\\exists}"; + ] + +(*s Table of contents *) + +type toc_entry = + | Toc_library of string + | Toc_section of int * (unit -> unit) * string + +let (toc_q : toc_entry Queue.t) = Queue.create () + +let add_toc_entry e = Queue.add e toc_q + +let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r + +(*s LaTeX output *) + +module Latex = struct + + (*s Latex preamble *) + + let (preamble : string Queue.t) = Queue.create () + + let push_in_preamble s = Queue.add s preamble + + let header () = + if !header_trailer then begin + printf "\\documentclass[12pt]{article}\n"; + if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; + printf "\\usepackage[T1]{fontenc}\n"; + printf "\\usepackage{fullpage}\n"; + printf "\\usepackage{coqdoc}\n"; + Queue.iter (fun s -> printf "%s\n" s) preamble; + printf "\\begin{document}\n" + end; + output_string + "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; + output_string + "%% This file has been automatically generated with the command\n"; + output_string "%% "; + Array.iter (fun s -> printf "%s " s) Sys.argv; + printf "\n"; + output_string + "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n" + + let trailer () = + if !header_trailer then begin + printf "\\end{document}\n" + end + + let char c = match c with + | '\\' -> + printf "\\symbol{92}" + | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> + output_char '\\'; output_char c + | '^' | '~' -> + output_char '\\'; output_char c; printf "{}" + | _ -> + output_char c + + let latex_char = output_char + let latex_string = output_string + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = + if not !short then begin + printf "\\coqdocmodule{"; + raw_ident !current_module; + printf "}\n\n" + end + + let start_latex_math () = output_char '$' + + let stop_latex_math () = output_char '$' + + let start_verbatim () = printf "\\begin{verbatim}" + + let stop_verbatim () = printf "\\end{verbatim}\n" + + let indentation n = + if n == 0 then + printf "\\noindent\n" + else + let space = 0.5 *. (float n) in + printf "\\coqdocindent{%2.2fem}\n" space + + let with_latex_printing f tok = + try + (match Hashtbl.find token_pp tok with + | Some s, _ -> output_string s + | _ -> f tok) + with Not_found -> + f tok + + let ident s _ = + if is_keyword s then begin + printf "\\coqdockw{"; raw_ident s; printf "}" + end else begin + printf "\\coqdocid{"; raw_ident s; printf "}" + end + + let ident s l = with_latex_printing (fun s -> ident s l) s + + let symbol = with_latex_printing raw_ident + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n\\begin{itemize}\n\\item "; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n\\end{itemize}\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\\item " + + let stop_item () = reach_item_level 0 + + let start_doc () = printf "\n\n\n\\noindent\n" + + let end_doc () = stop_item (); printf "\n\n\n" + + let start_coq () = () + + let end_coq () = () + + let start_code () = end_doc (); start_coq () + + let end_code () = end_coq (); start_doc () + + let section_kind = function + | 1 -> "\\section{" + | 2 -> "\\subsection{" + | 3 -> "\\subsubsection{" + | 4 -> "\\paragraph{" + | _ -> assert false + + let section lev f = + stop_item (); + output_string (section_kind lev); + f (); + printf "}\n\n" + + let rule () = + printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" + + let paragraph () = stop_item (); printf "\n\n\\medskip\n" + + let line_break () = printf "\\coqdoceol\n" + + let empty_line_of_code () = printf "\n\n\\medskip\n" + + let start_inline_coq () = () + + let end_inline_coq () = () + + let make_index () = () + + let make_toc () = printf "\\tableofcontents\n" + +end + + +(*s HTML output *) + +module Html = struct + + let header () = + if !header_trailer then begin + printf "\n\n"; + if !charset != "" then + printf "" !charset; + printf ""; + printf "%s\n\n\n" !page_title; + printf "\n\n" + end + + let self = "http://www.lri.fr/~filliatr/coqdoc/" + + let trailer () = + if !index && !current_module <> "Index" then + printf "
Index"; + if !header_trailer then begin + printf "
This page has been generated by "; + printf "coqdoc\n" self; + printf "\n" + end + + let start_module () = + if not !short then begin + (* add_toc_entry (Toc_library !current_module); *) + printf "

Library %s

\n\n" !current_module + end + + let indentation n = for i = 1 to n do printf " " done + + let line_break () = printf "
\n" + + let empty_line_of_code () = printf "\n
\n" + + let char = function + | '<' -> printf "<" + | '>' -> printf ">" + | '&' -> printf "&" + | c -> output_char c + + let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + + let latex_char _ = () + let latex_string _ = () + + let html_char = output_char + let html_string = output_string + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = printf "
"
+  let stop_verbatim () = printf "
\n" + + let module_ref m s = + printf "" m; raw_ident s; printf "" + (*i + match find_module m with + | Local -> + printf "" m; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s + i*) + + let ident_ref m s = match find_module m with + | Local -> + printf "" m s; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m s; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s + + let ident s loc = + if is_keyword s then begin + printf ""; + raw_ident s; + printf "" + end else + try + (match Index.find !current_module loc with + | Def _ -> + printf "" s; raw_ident s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,s') when s = s' -> + ident_ref m s + | Mod _ | Ref _ -> + raw_ident s) + with Not_found -> + raw_ident s + + let with_html_printing f tok = + try + (match Hashtbl.find token_pp tok with + | _, Some s -> output_string s + | _ -> f tok) + with Not_found -> + f tok + + let ident s l = with_html_printing (fun s -> ident s l) s + + let symbol = with_html_printing raw_ident + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n
    \n
  • "; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n
    • \n
\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\n
  • " + + let stop_item () = reach_item_level 0 + + let start_coq () = if not !raw_comments then printf "\n" + + let end_coq () = if not !raw_comments then printf "\n" + + let start_doc () = + if not !raw_comments then + printf "\n
    \n" + + let end_doc () = + stop_item (); + if not !raw_comments then printf "\n
    \n" + + let start_code () = end_doc (); start_coq () + + let end_code () = end_coq (); start_doc () + + let start_inline_coq () = printf "" + + let end_inline_coq () = printf "" + + let paragraph () = stop_item (); printf "\n

    \n" + + let section lev f = + let lab = new_label () in + let r = sprintf "%s.html#%s" !current_module lab in + add_toc_entry (Toc_section (lev, f, r)); + stop_item (); + printf "" lab lev; + f (); + printf "\n" lev + + let rule () = printf "
    \n" + + let entry_type = function + | Library -> "library" + | Module -> "module" + | Definition -> "definition" + | Inductive -> "inductive" + | Constructor -> "constructor" + | Lemma -> "lemma" + | Variable -> "variable" + | Axiom -> "axiom" + | TacticDefinition -> "tactic definition" + + (* make a HTML index from a list of triples (name,text,link) *) + let index_ref i c = + let idxc = sprintf "%s_%c" i.idx_name c in + if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc + + let letter_index category idx (c,l) = + if l <> [] then begin + let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in + printf "

    %c %s

    \n" idx c c cat; + List.iter + (fun (id,(text,link)) -> + printf "%s %s
    \n" link id text) l; + printf "

    " + end + + let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries + + let separate_index navig i = + let idx = i.idx_name in + let one_letter ((c,l) as cl) = + set_out_file (sprintf "index_%s_%c.html" idx c); + header (); + navig (); + printf "
    "; + letter_index true idx cl; + if List.length l > 30 then begin printf "
    "; navig () end; + trailer (); + close () + in + List.iter one_letter i.idx_entries + + let format_global_index = + Index.map + (fun s (m,t) -> + if t = Library then + "[library]", m ^ ".html" + else + sprintf "[%s, in %s]" (entry_type t) m m , + sprintf "%s.html#%s" m s) + + let format_bytype_index = function + | Library, idx -> + Index.map (fun id m -> "", m ^ ".html") idx + | (t,idx) -> + Index.map + (fun s m -> + let text = sprintf "[in %s]" m m in + (text, sprintf "%s.html#%s" m s)) idx + + let navig_one_index i = + printf "\n%s Index\n" (String.capitalize i.idx_name); + List.iter + (fun (c,l) -> + if l <> [] then + printf "%c\n" (index_ref i c) c + else + printf "%c\n" c) + i.idx_entries; + let n = i.idx_size in + printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); + printf "\n" + + let navig_index il = + printf "\n"; + List.iter navig_one_index il; + printf "
    \n" + + let make_index () = + if !index then begin + let idxl = + let glob,bt = Index.all_entries () in + format_global_index glob :: + List.map format_bytype_index bt + in + let navig () = navig_index idxl in + set_out_file "index.html"; + current_module := "Index"; + page_title := (if !title <> "" then !title else "Index"); + header (); + if !title <> "" then printf "

    %s

    \n" !title; + navig (); + if !multi_index then begin + trailer (); + close (); + List.iter (separate_index navig) idxl; + end else begin + let one_index i = + if i.idx_size > 0 then begin + printf "
    \n

    %s Index

    \n" (String.capitalize i.idx_name); + all_letters i + end + in + List.iter one_index idxl; + printf "
    "; + navig (); + trailer (); + close () + end; + end + + let make_toc () = + set_out_file "toc.html"; + page_title := (if !title <> "" then !title else "Table of contents"); + header (); + if !title <> "" then printf "

    %s

    \n" !title; + let make_toc_entry = function + | Toc_library m -> + stop_item (); + printf "

    Library %s

    \n" m m + | Toc_section (n, f, r) -> + item n; + printf "" r; f (); printf "\n" + in + Queue.iter make_toc_entry toc_q; + stop_item (); + if !index then printf "

    Index

    "; + trailer (); + close () + +end + + +(*s TeXmacs-aware output *) + +module TeXmacs = struct + + (*s Latex preamble *) + + let in_doc = ref false + + let (preamble : string Queue.t) = + in_doc := false; Queue.create () + + let push_in_preamble s = Queue.add s preamble + + let header () = + output_string + "(*i This file has been automatically generated with the command \n"; + output_string + " "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n" + + let trailer () = () + + let char_true c = match c with + | '\\' -> printf "\\\\" + | '<' -> printf "\\<" + | '|' -> printf "\\|" + | '>' -> printf "\\>" + | _ -> output_char c + + let char c = if !in_doc then char_true c else output_char c + + let latex_char = char_true + let latex_string = String.iter latex_char + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = () + + let start_latex_math () = printf "' + + let start_verbatim () = in_doc := true; printf "<\\verbatim>" + + let stop_verbatim () = in_doc := false; printf "" + + let indentation n = () + + let ident_true s = + if is_keyword s then begin + printf "" + end else begin + raw_ident s + end + + let ident s _ = if !in_doc then ident_true s else raw_ident s + + let symbol_true s = + let ensuremath x = printf ">" x in + match s with + | "*" -> ensuremath "times" + | "->" -> ensuremath "rightarrow" + | "<-" -> ensuremath "leftarrow" + | "<->" ->ensuremath "leftrightarrow" + | "=>" -> ensuremath "Rightarrow" + | "<=" -> ensuremath "le" + | ">=" -> ensuremath "ge" + | "<>" -> ensuremath "noteq" + | "~" -> ensuremath "lnot" + | "/\\" -> ensuremath "land" + | "\\/" -> ensuremath "lor" + | "|-" -> ensuremath "vdash" + | s -> raw_ident s + + let symbol s = if !in_doc then symbol_true s else raw_ident s + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n<\\itemize>\n"; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\n" + + let stop_item () = reach_item_level 0 + + let start_doc () = in_doc := true; printf "(** texmacs: " + + let end_doc () = stop_item (); in_doc := false; printf " *)" + + let start_coq () = () + + let end_coq () = () + + let start_code () = in_doc := true; printf "<\\code>\n" + let end_code () = in_doc := false; printf "\n" + + let section_kind = function + | 1 -> "section" + | 2 -> "subsection" + | 3 -> "subsubsection" + | 4 -> "paragraph" + | _ -> assert false + + let section lev f = + stop_item (); + printf "<"; output_string (section_kind lev); printf "|"; + f (); printf ">\n\n" + + let rule () = + printf "\n\n" + + let paragraph () = stop_item (); printf "\n\n" + + let line_break_true () = printf "" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = printf "" + + let make_index () = () + + let make_toc () = () + +end + +(*s Generic output *) + +let select f1 f2 f3 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x + +let push_in_preamble = Latex.push_in_preamble + +let header = select Latex.header Html.header TeXmacs.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer + +let start_module = + select Latex.start_module Html.start_module TeXmacs.start_module + +let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc + +let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq + +let start_code = select Latex.start_code Html.start_code TeXmacs.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code + +let start_inline_coq = + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq +let end_inline_coq = + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + +let indentation = select Latex.indentation Html.indentation TeXmacs.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break +let empty_line_of_code = select + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + +let section = select Latex.section Html.section TeXmacs.section +let item = select Latex.item Html.item TeXmacs.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule + +let char = select Latex.char Html.char TeXmacs.char +let ident = select Latex.ident Html.ident TeXmacs.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol + +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_string = + select Latex.latex_string Html.latex_string TeXmacs.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char +let html_string = + select Latex.html_string Html.html_string TeXmacs.html_string + +let start_latex_math = + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math +let stop_latex_math = + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + +let start_verbatim = + select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim +let stop_verbatim = + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim +let verbatim_char = + select output_char Html.char TeXmacs.char +let hard_verbatim_char = output_char + +let make_index = select Latex.make_index Html.make_index TeXmacs.make_index +let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli new file mode 100644 index 00000000..2195fa53 --- /dev/null +++ b/tools/coqdoc/output.mli @@ -0,0 +1,92 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val output_dir : string ref +val close : unit -> unit + +val quiet : bool ref +val short : bool ref +val light : bool ref +val header_trailer : bool ref +val index : bool ref +val multi_index : bool ref +val toc : bool ref +val title : string ref +val externals : bool ref +val coqlib : string ref +val raw_comments : bool ref + +val charset : string ref +val inputenc : string ref +val set_latin1 : unit -> unit +val set_utf8 : unit -> unit + +val add_printing_token : string -> string option * string option -> unit +val remove_printing_token : string -> unit + +val set_module : coq_module -> unit + +val header : unit -> unit +val trailer : unit -> unit + +val push_in_preamble : string -> unit + +val dump_file : string -> unit + +val start_module : unit -> unit + +val start_doc : unit -> unit +val end_doc : unit -> unit + +val start_coq : unit -> unit +val end_coq : unit -> unit + +val start_code : unit -> unit +val end_code : unit -> unit + +val start_inline_coq : unit -> unit +val end_inline_coq : unit -> unit + +val indentation : int -> unit +val line_break : unit -> unit +val paragraph : unit -> unit +val empty_line_of_code : unit -> unit + +val section : int -> (unit -> unit) -> unit + +val item : int -> unit + +val rule : unit -> unit + +val char : char -> unit +val ident : string -> loc -> unit +val symbol : string -> unit + +val latex_char : char -> unit +val latex_string : string -> unit +val html_char : char -> unit +val html_string : string -> unit +val verbatim_char : char -> unit +val hard_verbatim_char : char -> unit + +val start_latex_math : unit -> unit +val stop_latex_math : unit -> unit +val start_verbatim : unit -> unit +val stop_verbatim : unit -> unit + +val make_index : unit -> unit +val make_toc : unit -> unit diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli new file mode 100644 index 00000000..07808fe9 --- /dev/null +++ b/tools/coqdoc/pretty.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll new file mode 100644 index 00000000..541939b5 --- /dev/null +++ b/tools/coqdoc/pretty.mll @@ -0,0 +1,586 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* count (c + (8 - (c mod 8))) (i + 1) + | ' ' -> count (c + 1) (i + 1) + | _ -> c + in + count 0 0 + + let count_dashes s = + let c = ref 0 in + for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done; + !c + + let cut_head_tail_spaces s = + let n = String.length s in + let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in + let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in + let l = look_up 0 in + let r = look_dn (n-1) in + if l <= r then String.sub s l (r-l+1) else s + + let sec_title s = + let rec count lev i = + if s.[i] = '*' then + count (succ lev) (succ i) + else + let t = String.sub s i (String.length s - i) in + lev, cut_head_tail_spaces t + in + count 0 (String.index s '*') + + let formatted = ref false + let brackets = ref 0 + + let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + + (* Gallina (skipping proofs). This is a three states automaton. *) + + let gallina = ref false + + type gallina_state = Nothing | AfterDot | Proof + + let gstate = ref AfterDot + + let is_proof = + let t = Hashtbl.create 13 in + List.iter (fun s -> Hashtbl.add t s true) + [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let"; + "Correctness"; "Definition"; "Morphism" ]; + fun s -> try Hashtbl.find t s with Not_found -> false + + let gallina_id id = + if !gstate = AfterDot then + if is_proof id then gstate := Proof else + if id <> "Add" then gstate := Nothing + + let gallina_symbol s = + if !gstate = AfterDot || (!gstate = Proof && s = ":=") then + gstate := Nothing + + let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false + + let gallina_char c = + if c = '.' then + (let skip = !gstate = Proof in gstate := AfterDot; skip) + else + (if !gstate = AfterDot && not (is_space c) then gstate := Nothing; + false) + + (* saving/restoring the PP state *) + + type state = { + st_gallina : bool; + st_light : bool + } + + let state_stack = Stack.create () + + let save_state () = + Stack.push { st_gallina = !gallina; st_light = !light } state_stack + + let restore_state () = + let s = Stack.pop state_stack in + gallina := s.st_gallina; + light := s.st_light + + let without_ref r f x = save_state (); r := false; f x; restore_state () + + let without_gallina = without_ref gallina + + let without_light = without_ref light + + let show_all f = without_gallina (without_light f) + + let begin_show () = save_state (); gallina := false; light := false + let end_show () = restore_state () + + (* Reset the globals *) + + let reset () = + formatted := false; + brackets := 0; + gstate := AfterDot + + (* erasing of Section/End *) + + let section_re = Str.regexp "[ \t]*Section" + let end_re = Str.regexp "[ \t]*End" + let is_section s = Str.string_match section_re s 0 + let is_end s = Str.string_match end_re s 0 + + let sections_to_close = ref 0 + + let section_or_end s = + if is_section s then begin + incr sections_to_close; true + end else if is_end s then begin + if !sections_to_close > 0 then begin + decr sections_to_close; true + end else + false + end else + true + + (* tokens pretty-print *) + + let token_buffer = Buffer.create 1024 + + let token_re = + Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)" + let printing_token_re = + Str.regexp + "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?" + + let add_printing_token toks pps = + try + if Str.string_match token_re toks 0 then + let tok = Str.matched_group 1 toks in + if Str.string_match printing_token_re pps 0 then + let pp = + (try Some (Str.matched_group 3 pps) with _ -> + try Some (Str.matched_group 4 pps) with _ -> None), + (try Some (Str.matched_group 6 pps) with _ -> None) + in + Output.add_printing_token tok pp + with _ -> + () + + let remove_token_re = + Str.regexp + "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)" + + let remove_printing_token toks = + try + if Str.string_match remove_token_re toks 0 then + let tok = Str.matched_group 1 toks in + Output.remove_printing_token tok + with _ -> + () + + let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:=" + let extract_ident s = + assert (String.length s >= 3); + if Str.string_match extract_ident_re s 0 then + Str.matched_group 1 s + else + String.sub s 1 (String.length s - 3) + +} + +(*s Regular expressions *) + +let space = [' ' '\t'] +let space_nl = [' ' '\t' '\n' '\r'] + +let firstchar = + ['A'-'Z' 'a'-'z' '_' + (* iso 8859-1 accents *) + '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | + (* utf-8 latin 1 supplement *) + '\195' ['\128'-'\191'] | + (* utf-8 letterlike symbols *) + '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) +let identchar = + firstchar | ['\'' '0'-'9' '@'] +let identifier = firstchar identchar* + +let symbolchar_no_brackets = + ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' + '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' + '{' '}' '(' ')'] | + (* utf-8 symbols *) + '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ +let symbolchar = symbolchar_no_brackets | '[' | ']' +let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' + +(* tokens with balanced brackets *) +let token_brackets = + ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* + | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ ) + symbolchar_no_brackets* + +let section = "*" | "**" | "***" | "****" + +let item_space = " " + +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n' +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n' +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n' +let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n' +(* +let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" +let end_verb = "(*" space* "end" space+ "verb" space* "*)" +*) + +let coq_command_to_hide = + "Implicit" space | + "Ltac" space | + "Require" space | + "Load" space | + "Hint" space | + "Transparent" space | + "Opaque" space | + ("Declare" space+ ("Morphism" | "Step") space) | + "Section" space | + "Variable" 's'? space | + ("Hypothesis" | "Hypotheses") space | + "End" space | + ("Set" | "Unset") space+ "Printing" space+ "Coercions" space | + "Declare" space+ ("Left" | "Right") space+ "Step" space + +(*s Scanning Coq, at beginning of line *) + +rule coq_bol = parse + | '\n'+ + { empty_line_of_code (); coq_bol lexbuf } + | space* "(**" space_nl + { end_coq (); start_doc (); + let eol = doc_bol lexbuf in + end_doc (); start_coq (); + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Comments" space_nl + { end_coq (); start_doc (); comments lexbuf; end_doc (); + start_coq (); coq lexbuf } + | space* begin_hide + { skip_hide lexbuf; coq_bol lexbuf } + | space* begin_show + { begin_show (); coq_bol lexbuf } + | space* end_show + { end_show (); coq_bol lexbuf } + | space* coq_command_to_hide + { let s = lexeme lexbuf in + if !light && section_or_end s then begin + skip_to_dot lexbuf; + coq_bol lexbuf + end else begin + indentation (count_spaces s); + backtrack lexbuf; + coq lexbuf + end } + | space* "(**" space+ "printing" space+ (identifier | token) space+ + { let tok = lexeme lexbuf in + let s = printing_token lexbuf in + add_printing_token tok s; + coq_bol lexbuf } + | space* "(**" space+ "printing" space+ + { eprintf "warning: bad 'printing' command at character %d\n" + (lexeme_start lexbuf); flush stderr; + ignore (comment lexbuf); + coq_bol lexbuf } + | space* "(**" space+ "remove" space+ "printing" space+ + (identifier | token) space* "*)" + { remove_printing_token (lexeme lexbuf); + coq_bol lexbuf } + | space* "(**" space+ "remove" space+ "printing" space+ + { eprintf "warning: bad 'remove printing' command at character %d\n" + (lexeme_start lexbuf); flush stderr; + ignore (comment lexbuf); + coq_bol lexbuf } + | space* "(*" + { let eol = comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | space+ + { indentation (count_spaces (lexeme lexbuf)); coq lexbuf } + | eof + { () } + | _ + { backtrack lexbuf; indentation 0; coq lexbuf } + +(*s Scanning Coq elsewhere *) + +and coq = parse + | "\n" + { line_break (); coq_bol lexbuf } + | "(**" space_nl + { end_coq (); start_doc (); + let eol = doc_bol lexbuf in + end_doc (); start_coq (); + if eol then coq_bol lexbuf else coq lexbuf } + | "(*" + { let eol = comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | '\n'+ space* "]]" + { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end } + | eof + { () } + | token + { let s = lexeme lexbuf in + if !gallina then gallina_symbol s; + symbol s; + coq lexbuf } + | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module" + (* hack to avoid making Type a keyword *) + { let s = lexeme lexbuf in + if !gallina then gallina_id s; + ident s (lexeme_start lexbuf); coq lexbuf } + | "(" space* identifier space* ":=" + { let id = extract_ident (lexeme lexbuf) in + symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf } + | (identifier '.')* identifier + { let id = lexeme lexbuf in + if !gallina then gallina_id id; + ident id (lexeme_start lexbuf); coq lexbuf } + | _ + { let c = lexeme_char lexbuf 0 in + char c; + if !gallina && gallina_char c then skip_proof lexbuf; + coq lexbuf } + +(*s Scanning documentation, at beginning of line *) + +and doc_bol = parse + | space* "\n" '\n'* + { paragraph (); doc_bol lexbuf } + | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])* + { let lev, s = sec_title (lexeme lexbuf) in + section lev (fun () -> ignore (doc (from_string s))); + doc lexbuf } + | space* '-'+ + { let n = count_dashes (lexeme lexbuf) in + if n >= 4 then rule () else item n; + doc lexbuf } + | "<<" space* + { start_verbatim (); verbatim lexbuf; doc_bol lexbuf } + | eof + { false } + | _ + { backtrack lexbuf; doc lexbuf } + +(*s Scanning documentation elsewhere *) + +and doc = parse + | "\n" + { char '\n'; doc_bol lexbuf } + | "[" + { brackets := 1; + start_inline_coq (); escaped_coq lexbuf; end_inline_coq (); + doc lexbuf } + | "[[" '\n' space* + { formatted := true; start_code (); + indentation (count_spaces (lexeme lexbuf)); + without_gallina coq lexbuf; + end_code (); formatted := false; + doc lexbuf } + | '*'* "*)" space* '\n' + { true } + | '*'* "*)" + { false } + | "$" + { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } + | "$$" + { char '$'; doc lexbuf } + | "%" + { escaped_latex lexbuf; doc lexbuf } + | "%%" + { char '%'; doc lexbuf } + | "#" + { escaped_html lexbuf; doc lexbuf } + | "##" + { char '#'; doc lexbuf } + | eof + { false } + | _ + { char (lexeme_char lexbuf 0); doc lexbuf } + +(*s Various escapings *) + +and escaped_math_latex = parse + | "$" { stop_latex_math () } + | eof { stop_latex_math () } + | _ { latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } + +and escaped_latex = parse + | "%" { () } + | eof { () } + | _ { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } + +and escaped_html = parse + | "#" { () } + | "&#" + { html_char '&'; html_char '#'; escaped_html lexbuf } + | "##" + { html_char '#'; escaped_html lexbuf } + | eof { () } + | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } + +and verbatim = parse + | "\n>>" { verbatim_char '\n'; stop_verbatim () } + | eof { stop_verbatim () } + | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf } + +(*s Coq, inside quotations *) + +and escaped_coq = parse + | "]" + { decr brackets; + if !brackets > 0 then begin char ']'; escaped_coq lexbuf end } + | "[" + { incr brackets; char '['; escaped_coq lexbuf } + | "(*" + { ignore (comment lexbuf); escaped_coq lexbuf } + | "*)" + { (* likely to be a syntax error: we escape *) backtrack lexbuf } + | eof + { () } + | token_brackets + { let s = lexeme lexbuf in + symbol s; + escaped_coq lexbuf } + | (identifier '.')* identifier + { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } + | _ + { char (lexeme_char lexbuf 0); escaped_coq lexbuf } + +(*s Coq "Comments" command. *) + +and comments = parse + | space_nl+ + { char ' '; comments lexbuf } + | '"' [^ '"']* '"' + { let s = lexeme lexbuf in + let s = String.sub s 1 (String.length s - 2) in + ignore (doc (from_string s)); comments lexbuf } + | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+ + { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf } + | "." (space_nl | eof) + { () } + | eof + { () } + | _ + { char (lexeme_char lexbuf 0); comments lexbuf } + +(*s Skip comments *) + +and comment = parse + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "*)" space* '\n'+ { true } + | "*)" { false } + | eof { false } + | _ { comment lexbuf } + +(*s Skip proofs *) + +and skip_proof = parse + | "(*" { ignore (comment lexbuf); skip_proof lexbuf } + | "Save" | "Qed" | "Defined" + | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf } + | "Proof" space* '.' { skip_proof lexbuf } + | identifier { skip_proof lexbuf } (* to avoid keywords within idents *) + | eof { () } + | _ { skip_proof lexbuf } + +and skip_to_dot = parse + | eof | '.' { if !gallina then gstate := AfterDot } + | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf } + | _ { skip_to_dot lexbuf } + +and skip_hide = parse + | eof | end_hide { () } + | _ { skip_hide lexbuf } + +(*s Reading token pretty-print *) + +and printing_token = parse + | "*)" | eof + { let s = Buffer.contents token_buffer in + Buffer.clear token_buffer; + s } + | _ { Buffer.add_string token_buffer (lexeme lexbuf); + printing_token lexbuf } + +(*s Applying the scanners to files *) + +{ + + type file = + | Vernac_file of string * coq_module + | Latex_file of string + + let coq_file f m = + reset (); + Index.scan_file f m; + start_module (); + let c = open_in f in + let lb = from_channel c in + start_coq (); coq_bol lb; end_coq (); + close_in c + + (* LaTeX document *) + + let latex_document l = + let file = function + | Vernac_file (f,m) -> set_module m; coq_file f m + | Latex_file f -> dump_file f + in + header (); + if !toc then make_toc (); + List.iter file l; + trailer (); + close () + + (* HTML document *) + + let html_document l = + let file = function + | Vernac_file (f,m) -> + set_module m; + let hf = m ^ ".html" in + set_out_file hf; + header (); + coq_file f m; + trailer (); + close () + | Latex_file _ -> () + in + List.iter file l; + make_index (); + if !toc then make_toc () + + (* TeXmacs document *) + + let texmacs_document l = + let file = function + | Vernac_file (f,m) -> set_module m; coq_file f m + | Latex_file f -> dump_file f + in + header (); + List.iter file l; + trailer (); + close () + + let index_module = function + | Vernac_file (_,m) -> Index.add_module m + | Latex_file _ -> () + + let produce_document l = + List.iter index_module l; + (match !target_language with + | LaTeX -> latex_document + | HTML -> html_document + | TeXmacs -> texmacs_document) l + +} + diff --git a/tools/coqdoc/style.css b/tools/coqdoc/style.css new file mode 100644 index 00000000..5150bd75 --- /dev/null +++ b/tools/coqdoc/style.css @@ -0,0 +1,23 @@ +a:visited {color : #416DFF; text-decoration : none; } +a:link {color : #416DFF; text-decoration : none; font-weight : bold} +a:hover {color : Red; text-decoration : underline; } +a:active {color : Red; text-decoration : underline; } +.keyword { font-weight : bold ; color : Red } +.keywordsign { color : #C04600 } +.superscript { font-size : 4 } +.subscript { font-size : 4 } +.comment { color : Green } +.constructor { color : Blue } +.string { color : Maroon } +.warning { color : Red ; font-weight : bold } +.info { margin-left : 3em; margin-right : 3em } +.title1 { font-size : 20pt ; background-color : #416DFF } +.title2 { font-size : 20pt ; background-color : #418DFF } +.title3 { font-size : 20pt ; background-color : #41ADFF } +.title4 { font-size : 20pt ; background-color : #41CDFF } +.title5 { font-size : 20pt ; background-color : #41EDFF } +.title6 { font-size : 20pt ; background-color : #41FFFF } +body { background-color : White } +tr { background-color : White } +# .doc { background-color :#aaeeff } +.doc { background-color :#66ff66 } diff --git a/tools/coqwc.mll b/tools/coqwc.mll new file mode 100644 index 00000000..08bf2bcc --- /dev/null +++ b/tools/coqwc.mll @@ -0,0 +1,293 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* printf " %s" f | _ -> ()); + if !percentage then begin + let s = sl + pl + dl in + let p = if s > 0 then 100 * dl / s else 0 in + printf " (%d%%)" p + end; + print_newline () + +let print_file fo = print_line !slines !plines !dlines fo + +let print_totals () = print_line !tslines !tplines !tdlines (Some "total") + +(*i*)}(*i*) + +(*s Shortcuts for regular expressions. The [rcs] regular expression + is used to skip the CVS infos possibly contained in some comments, + in order not to consider it as documentation. *) + +let space = [' ' '\t' '\r'] +let character = + "'" ([^ '\\' '\''] | + '\\' (['\\' '\'' 'n' 't' 'b' 'r'] | ['0'-'9'] ['0'-'9'] ['0'-'9'])) "'" +let rcs_keyword = + "Author" | "Date" | "Header" | "Id" | "Name" | "Locker" | "Log" | + "RCSfile" | "Revision" | "Source" | "State" +let rcs = "\036" rcs_keyword [^ '$']* "\036" +let stars = "(*" '*'* "*)" +let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) +let proof_start = + "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" +let proof_end = + ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.' + +(*s [spec] scans the specification. *) + +rule spec = parse + | "(*" { comment lexbuf; spec lexbuf } + | '"' { let n = string lexbuf in slines := !slines + n; + seen_spec := true; spec lexbuf } + | '\n' { newline (); spec lexbuf } + | space+ | stars + { spec lexbuf } + | proof_start space + { seen_spec := true; spec_to_dot lexbuf; proof lexbuf } + | proof_start '\n' + { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf } + | "Definition" space + { seen_spec := true; definition lexbuf } + | character | _ + { seen_spec := true; spec lexbuf } + | eof { () } + +(*s [spec_to_dot] scans a spec until a dot is reached and returns. *) + +and spec_to_dot = parse + | "(*" { comment lexbuf; spec_to_dot lexbuf } + | '"' { let n = string lexbuf in slines := !slines + n; + seen_spec := true; spec_to_dot lexbuf } + | '\n' { newline (); spec_to_dot lexbuf } + | dot { () } + | space+ | stars + { spec_to_dot lexbuf } + | character | _ + { seen_spec := true; spec_to_dot lexbuf } + | eof { () } + +(*s [definition] scans a definition; passes to [proof] is the body is + absent, and to [spec] otherwise *) + +and definition = parse + | "(*" { comment lexbuf; definition lexbuf } + | '"' { let n = string lexbuf in slines := !slines + n; + seen_spec := true; definition lexbuf } + | '\n' { newline (); definition lexbuf } + | ":=" { seen_spec := true; spec lexbuf } + | dot { proof lexbuf } + | space+ | stars + { definition lexbuf } + | character | _ + { seen_spec := true; definition lexbuf } + | eof { () } + +(*s Scans a proof, then returns to [spec]. *) + +and proof = parse + | "(*" { comment lexbuf; proof lexbuf } + | '"' { let n = string lexbuf in plines := !plines + n; + seen_proof := true; proof lexbuf } + | space+ | stars + { proof lexbuf } + | '\n' { newline (); proof lexbuf } + | "Proof" space* '.' + { seen_proof := true; proof lexbuf } + | "Proof" space + { proof_term lexbuf } + | proof_end + { seen_proof := true; spec lexbuf } + | character | _ + { seen_proof := true; proof lexbuf } + | eof { () } + +and proof_term = parse + | "(*" { comment lexbuf; proof_term lexbuf } + | '"' { let n = string lexbuf in plines := !plines + n; + seen_proof := true; proof_term lexbuf } + | space+ | stars + { proof_term lexbuf } + | '\n' { newline (); proof_term lexbuf } + | dot { spec lexbuf } + | character | _ + { seen_proof := true; proof_term lexbuf } + | eof { () } + +(*s Scans a comment. *) + +and comment = parse + | "(*" { comment lexbuf; comment lexbuf } + | "*)" { () } + | '"' { let n = string lexbuf in dlines := !dlines + n; + seen_comment := true; comment lexbuf } + | '\n' { newline (); comment lexbuf } + | space+ | stars + { comment lexbuf } + | character | _ + { seen_comment := true; comment lexbuf } + | eof { () } + +(*s The entry [string] reads a string until its end and returns the number + of newlines it contains. *) + +and string = parse + | '"' { 0 } + | '\\' ('\\' | 'n' | '"') { string lexbuf } + | '\n' { succ (string lexbuf) } + | _ { string lexbuf } + | eof { 0 } + +(*s The following entry [read_header] is used to skip the possible header at + the beggining of files (unless option \texttt{-e} is specified). + It stops whenever it encounters an empty line or any character outside + a comment. In this last case, it correctly resets the lexer position + on that character (decreasing [lex_curr_pos] by 1). *) + +and read_header = parse + | "(*" { skip_comment lexbuf; skip_until_nl lexbuf; + read_header lexbuf } + | "\n" { () } + | space+ { read_header lexbuf } + | _ { lexbuf.lex_curr_pos <- lexbuf.lex_curr_pos - 1 } + | eof { () } + +and skip_comment = parse + | "*)" { () } + | "(*" { skip_comment lexbuf; skip_comment lexbuf } + | _ { skip_comment lexbuf } + | eof { () } + +and skip_until_nl = parse + | '\n' { () } + | _ { skip_until_nl lexbuf } + | eof { () } + +(*i*){(*i*) + +(*s Processing files and channels. *) + +let process_channel ch = + let lb = Lexing.from_channel ch in + reset_counters (); + if !skip_header then read_header lb; + spec lb + +let process_file f = + try + let ch = open_in f in + process_channel ch; + close_in ch; + print_file (Some f); + update_totals () + with + | Sys_error "Is a directory" -> + flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr + | Sys_error s -> + flush stdout; eprintf "coqwc: %s\n" s; flush stderr + +(*s Parsing of the command line. *) + +let usage () = + prerr_endline "usage: coqwc [options] [files]"; + prerr_endline "Options are:"; + prerr_endline " -p print percentage of comments"; + prerr_endline " -s print only the spec size"; + prerr_endline " -r print only the proof size"; + prerr_endline " -e (everything) do not skip headers"; + exit 1 + +let rec parse = function + | [] -> [] + | ("-h" | "-?" | "-help" | "--help") :: _ -> usage () + | ("-s" | "--spec-only") :: args -> + proof_only := false; spec_only := true; parse args + | ("-r" | "--proof-only") :: args -> + spec_only := false; proof_only := true; parse args + | ("-p" | "--percentage") :: args -> percentage := true; parse args + | ("-e" | "--header") :: args -> skip_header := false; parse args + | f :: args -> f :: (parse args) + +(*s Main program. *) + +let main () = + let files = parse (List.tl (Array.to_list Sys.argv)) in + if not (!spec_only || !proof_only) then + printf " spec proof comments\n"; + match files with + | [] -> process_channel stdin; print_file None + | [f] -> process_file f + | _ -> List.iter process_file files; print_totals () + +let _ = Printexc.catch main () + +(*i*)}(*i*) + + diff --git a/tools/gallina.ml b/tools/gallina.ml new file mode 100644 index 00000000..c997820c --- /dev/null +++ b/tools/gallina.ml @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* begin + flush !chan_out; + close_in chan_in; + if not !option_stdout then close_out !chan_out + end + with Sys_error _ -> + () + +let traite_stdin () = + try + let buf = Lexing.from_channel stdin in + try + while true do Gallina_lexer.action buf done + with Fin_fichier -> + flush !chan_out + with Sys_error _ -> + () + +let gallina () = + let lg_command = Array.length Sys.argv in + if lg_command < 2 then begin + output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; + flush stderr; + exit 1 + end; + let treat = function + | "-" -> option_moins := true + | "-stdout" -> option_stdout := true + | "-nocomments" -> comments := false + | f -> + if Filename.check_suffix f ".v" then + vfiles := (Filename.chop_suffix f ".v") :: !vfiles + in + Array.iter treat Sys.argv; + if !option_moins then + traite_stdin () + else + List.iter traite_fichier !vfiles + +let _ = Printexc.catch gallina () + diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll new file mode 100644 index 00000000..ce9fb950 --- /dev/null +++ b/tools/gallina_lexer.mll @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 0 then comment lexbuf } + | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf)); + comment_depth := pred !comment_depth; + if !comment_depth > 0 then comment lexbuf } + | eof { raise Fin_fichier } + | _ { (if !comments then print (Lexing.lexeme lexbuf)); + comment lexbuf } + +and skip_comment = parse + | "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf } + | "*)" { comment_depth := pred !comment_depth; + if !comment_depth > 0 then skip_comment lexbuf } + | eof { raise Fin_fichier } + | _ { skip_comment lexbuf } + +and body_def = parse + | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () } + | _ { print (Lexing.lexeme lexbuf); body lexbuf } + +and body = parse + | enddot { print ".\n"; skip_proof lexbuf } + | ":=" { print ".\n"; skip_proof lexbuf } + | "(*" { print "(*"; comment_depth := 1; + comment lexbuf; body lexbuf } + | eof { raise Fin_fichier } + | _ { print (Lexing.lexeme lexbuf); body lexbuf } + +and body_pgm = parse + | enddot { print ".\n"; skip_proof lexbuf } + | "(*" { print "(*"; comment_depth := 1; + comment lexbuf; body_pgm lexbuf } + | eof { raise Fin_fichier } + | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf } + +and skip_until_point = parse + | '.' '\n' { () } + | enddot { end_of_line lexbuf } + | "(*" { comment_depth := 1; + skip_comment lexbuf; skip_until_point lexbuf } + | eof { raise Fin_fichier } + | _ { skip_until_point lexbuf } + +and end_of_line = parse + | [' ' '\t' ]* { end_of_line lexbuf } + | '\n' { () } + | eof { raise Fin_fichier } + | _ { print (Lexing.lexeme lexbuf) } + +and skip_proof = parse + | "Save." { end_of_line lexbuf } + | "Save" space + { skip_until_point lexbuf } + | "Qed." { end_of_line lexbuf } + | "Qed" space + { skip_until_point lexbuf } + | "Defined." { end_of_line lexbuf } + | "Defined" space + { skip_until_point lexbuf } + | "Abort." { end_of_line lexbuf } + | "Abort" space + { skip_until_point lexbuf } + | "Proof" space { skip_until_point lexbuf } + | "Proof" [' ' '\t']* '.' { skip_proof lexbuf } + | "(*" { comment_depth := 1; + skip_comment lexbuf; skip_proof lexbuf } + | eof { raise Fin_fichier } + | _ { skip_proof lexbuf } diff --git a/tools/restore-v7 b/tools/restore-v7 new file mode 100755 index 00000000..ab884587 --- /dev/null +++ b/tools/restore-v7 @@ -0,0 +1,9 @@ +#!/bin/sh + +echo Restoring v7 files from directory v7 +v7files=`find v7 -name \*.v` +for i in $v7files; do + j=`echo $i | sed -e "s@^v7/@@"` + echo Restoring $i from v7 + cp -f $i $j +done diff --git a/tools/translate-v8 b/tools/translate-v8 new file mode 100755 index 00000000..7d71bea9 --- /dev/null +++ b/tools/translate-v8 @@ -0,0 +1,41 @@ +#!/bin/sh + +if [ -e v7 ]; then + echo "Warning: v7 directory found, the files are maybe already translated"; + sleep 5; +fi +echo --------- Producing v8 files in the translation directory ------------- +if [ -e v8 ]; then rm -r v8; fi +if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi +cp -pr . /tmp/v7.$$ +cp -pr /tmp/v7.$$ v8 +cd v8 +rm description toto +make clean +make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ + { echo ---- Failed to translate; exit 1; } +echo --------- Upgrading files in the translation directory ---------------- +v8files=`find . -name \*.v8` +for i in $v8files; do + j=`dirname $i`/`basename $i .v8`.v + echo Upgrading $j in the translation directory + mv -u -f $i $j +done +echo --------- Recompiling v8 files in the translation directory ----------- +make clean +make || { echo ---- Failed to recompile; exit 1; } +echo --------- Saving v7 files in directory v7 ----------------------------- +/bin/rm -r ../v7 +mv /tmp/v7.$$ ../v7 +echo Saving v7 files done +echo --------- Upgrading files in current directory ------------------------ +vfiles=`find . -name \*.v` +cd .. +for i in $vfiles; do + echo Upgrading $i in current directory + mv -u -f v8/$i $i +done +echo --------- Translation completed --------------------------------------- +echo Old files are in directory '"v7"' +echo New files are in current directory +echo You can now remove the translation directory '"v8"' diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0 new file mode 100755 index 00000000..10e7f140 --- /dev/null +++ b/tools/translate_V6-3-1_to_V7-0 @@ -0,0 +1,27 @@ +#! /bin/sh + +echo "This shell script performs the following transformations:" +echo "- Insertion of a space after a dot not followed by a separator" +echo "- Insertion of a space between consecutive ~ and < and between" +echo " consecutive | and < assumed to be part of distinct tokens" +echo "- Various renamings of commands as described in document Changes.ps" + +for i in $* + do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \ + -e "s/~ $i.tmp$$ + if diff $i.tmp$$ $i > /dev/null + then + rm $i.tmp$$ + else + echo Le fichier $i a été modifié + mv $i.tmp$$ $i + fi + done +echo diff --git a/tools/upgrade-v8 b/tools/upgrade-v8 new file mode 100755 index 00000000..36d0bf8c --- /dev/null +++ b/tools/upgrade-v8 @@ -0,0 +1,22 @@ +#!/bin/sh + +mv v7 v7.bak + +echo ---------------- Saving v7 files into directory v7 ------------------ +vfiles=`find . -name \*.v` +for i in $vfiles; do + if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi + if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi + echo Saving $i into v7/$i + j=v7/$i + mkdir -p `dirname $j` + mv -u -f $i $j +done + +echo ---------------- Upgrading files with v8 syntax --------------------- +v8files=`find . -name \*.v8` +for i in $v8files; do + j=`dirname $i`/`basename $i .v8`.v + echo Upgrading $i + mv -u -f $i $j +done -- cgit v1.2.3