From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- tools/coq-tex.ml4 | 2 +- tools/coq_makefile.ml4 | 439 +++++++++++++++++++++++++--------------------- tools/coqdep.ml | 396 +++++++++++++++++++---------------------- tools/coqdep_lexer.mll | 4 +- tools/coqdoc/cdglobals.ml | 8 +- tools/coqdoc/coqdoc.sty | 126 +++++++++++-- tools/coqdoc/index.mli | 18 +- tools/coqdoc/index.mll | 145 ++++++++++----- tools/coqdoc/main.ml | 391 +++++++++++++++++++++-------------------- tools/coqdoc/output.ml | 193 ++++++++++++++------ tools/coqdoc/pretty.mll | 319 +++++++++++++++++++-------------- tools/coqwc.mll | 2 +- 12 files changed, 1190 insertions(+), 853 deletions(-) (limited to 'tools') diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 index d55901b9..4c11725c 100644 --- a/tools/coq-tex.ml4 +++ b/tools/coq-tex.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq-tex.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *) +(* $Id: coq-tex.ml4 9532 2007-01-24 16:04:29Z bgregoir $ *) (* coq-tex * JCF, 16/1/98 diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index b6af3abc..77dbcc47 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) +(* $Id: coq_makefile.ml4 11136 2008-06-18 10:41:34Z herbelin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -81,21 +81,10 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom let standard sds sps = print "byte:\n"; - print "\t$(MAKE) all \"OPT=\"\n\n"; + print "\t$(MAKE) all \"OPT:=-byte\"\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) $(VFILES) *.ml *.mli >.depend\n"; - print "\t$(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend\n"; - end; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") - sds; - print "\n"; + print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n"; print "install:\n"; print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n"; @@ -116,7 +105,11 @@ let standard sds sps = end; print "clean:\n"; print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n"; - print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; + print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ + $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; + if !some_mlfile then + print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; + print "\t- rm -rf html\n"; List.iter (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n") sps; @@ -129,44 +122,32 @@ let standard sds sps = 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" + print "\n\n" + +let includes () = + if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; + if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\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"; + print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.ml.d: %.ml\n"; + print "\t$(CAMLBIN)ocamldep -slash $(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 - [] + print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.g: %.v\n\t$(GALLINA) $<\n\n"; + print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n"; + print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n"; + print "%.v.d: %.v\n"; + print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" 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 () + if !some_mlfile then ml_rules (); + if !some_vfile then v_rule () let variables l = let rec var_aux = function @@ -174,71 +155,122 @@ let variables l = | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r | _ :: r -> var_aux r in - section "Variables definitions."; - print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n"; - print "CAMLP4=`basename $CAMLP4LIB`\n"; - print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + section "Variables definitions."; + print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n"; + print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; + if Coq_config.local then + (print "COQSRC:=$(COQTOP)\n"; + print "COQSRCLIBS:=-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)/proofs -I $(COQTOP)/tactics \\ + -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\ + -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\ + -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\ + -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\ -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=$(COQBIN)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_macro.cmo q_MLast.cmo\n"; - print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; - var_aux l; - print "\n" + -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\ + -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\ + -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\ + -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\ + -I $(CAMLP4LIB)\n") + else + (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n"; + print "COQSRCLIBS:=-I $(COQSRC)\n"); + print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n"; + if !opt = "-byte" then + print "override OPT:=-byte\n" + else + print "OPT:=\n"; + if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; + (* Coq executables and relative variables *) + print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "COQC:=$(COQBIN)coqc\n"; + print "COQDEP:=$(COQBIN)coqdep -c\n"; + print "GALLINA:=$(COQBIN)gallina\n"; + print "COQDOC:=$(COQBIN)coqdoc\n"; + (* Caml executables and relative variables *) + printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n"; + printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n"; + printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n"; + printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n"; + print "GRAMMARS:=grammar.cma\n"; + print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; + + (if Coq_config.local then + print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n" + else + print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"); + var_aux l; + print "\n" + +let absolute_dir dir = + let current = Sys.getcwd () in + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' + +let is_prefix dir1 dir2 = + let l1 = String.length dir1 in + let l2 = String.length dir2 in + dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') + +let is_included dir = function + | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir) + | Include dir' -> absolute_dir dir = absolute_dir dir' + | _ -> false + +let dir_of_target t = + match t with + | RInclude (dir,_) -> dir + | Include dir -> dir + | _ -> assert false 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 + let rec split_includes l = + match l with + | [] -> [], [] + | Include _ as i :: rem -> + let ri, rr = split_includes rem in + (i :: ri), rr + | RInclude _ as r :: rem -> + let ri, rr = split_includes rem in + ri, (r :: rr) + | _ :: rem -> split_includes rem + in + let rec parse_includes l = + match l with + | [] -> [] + | Include x :: rem -> ("-I " ^ x) :: parse_includes rem + | RInclude (p,l) :: rem -> + let l' = if l = "" then "\"\"" else l in + ("-R " ^ p ^ " " ^ l') :: parse_includes rem + | _ :: rem -> parse_includes rem 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 l' = if List.exists (is_included ".") l then l else Include "." :: l in + let inc_i, inc_r = split_includes l' in + let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in + let str_i = parse_includes inc_i in + let str_i' = parse_includes inc_i' in + let str_r = parse_includes inc_r in + section "Libraries definition."; + print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n"; + print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; + print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n" let rec special = function | [] -> [] | Special (file,deps,com) :: r -> (file,deps,com) :: (special r) | _ :: r -> special r - + let custom sps = let pr_sp (file,dependencies,com) = print file; print ": "; print dependencies; print "\n"; print "\t"; print com; print "\n\n" in - if sps <> [] then section "Custom targets."; - List.iter pr_sp sps + if sps <> [] then section "Custom targets."; + List.iter pr_sp sps let subdirs l = let rec subdirs_aux = function @@ -249,69 +281,69 @@ let subdirs l = 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 + 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 - | [] -> [] + let rec parse_arguments l = + match l with + | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o) + | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o) + | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o) + | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o) + | Include _ :: r -> parse_arguments r + | RInclude _ :: r -> parse_arguments r + | Def _ :: r -> parse_arguments 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 + vfiles, mlfiles, other_targets = parse_arguments l + in + section "Definition of the \"all\" target."; + if !some_vfile then + begin + print "VFILES:="; print_list "\\\n " vfiles; print "\n"; + print "VOFILES:=$(VFILES:.v=.vo)\n"; + print "GLOBFILES:=$(VFILES:.v=.glob)\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" + end; + if !some_mlfile then + begin + print "MLFILES:="; print_list "\\\n " mlfiles; print "\n"; + print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; + end; + print "\nall: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile then print "$(CMOFILES) "; + print_list "\\\n " other_targets; print "\n"; + if !some_vfile then + begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir html\n"; + print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir html\n"; + print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "\n\n" + end + let parse f = let rec string = parser | [< '' ' | '\n' | '\t' >] -> "" @@ -333,8 +365,8 @@ let parse f = in let c = open_in f in let res = args (Stream.of_channel c) in - close_in c; - res + close_in c; + res let rec process_cmd_line = function | [] -> @@ -348,8 +380,16 @@ let rec process_cmd_line = function | "-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) + let check_dep f = + if Filename.check_suffix f ".v" then + some_vfile := true + else if Filename.check_suffix f ".ml" then + some_mlfile := true + else + () + in + List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); + Special (file,dependencies,com) :: (process_cmd_line r) | "-I" :: d :: r -> Include d :: (process_cmd_line r) | "-R" :: p :: l :: r -> @@ -369,45 +409,39 @@ let rec process_cmd_line = function 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) + some_vfile := true; + V f :: (process_cmd_line r) + end else if Filename.check_suffix f ".ml" then begin + some_mlfile := true; + ML f :: (process_cmd_line r) end else - Subdir f :: (process_cmd_line r) - + Subdir f :: (process_cmd_line r) + let banner () = print -"############################################################################## -## The Calculus of Inductive Constructions ## -## ## -## Projet Coq ## -## ## -## INRIA ENS-CNRS ## -## Rocquencourt Lyon ## -## ## -## Coq V7 ## -## ## -## ## -############################################################################## +"########################################################################## +## v # The Coq Proof Assistant ## +## 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 @@ -426,32 +460,33 @@ let directories_deps l = | _ :: l -> iter acc l in - iter ([],[]) l + 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; - let sps = special l in - custom sps; - let sds = subdirs l in - implicit (); - standard sds sps; - (* TEST directories_deps l; *) - warning (); - if not (!output_channel == stdout) then close_out !output_channel; - exit 0 - + banner (); + warning (); + command_line args; + include_dirs l; + variables l; + all_target l; + let sps = special l in + custom sps; + let sds = subdirs l in + implicit (); + standard sds sps; + (* TEST directories_deps l; *) + includes (); + 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 - + do_makefile args + let _ = Printexc.catch main () diff --git a/tools/coqdep.ml b/tools/coqdep.ml index e787cdb3..dc80476b 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 10196 2007-10-08 13:50:39Z notin $ *) +(* $Id: coqdep.ml 10746 2008-04-03 15:45:25Z notin $ *) open Printf open Coqdep_lexer @@ -22,9 +22,9 @@ let option_D = ref false let option_w = ref false let option_i = ref false let option_sort = ref false +let option_glob = ref false let option_slash = ref false - -let directories_added = ref false +let option_boot = ref false let suffixe = ref ".vo" let suffixe_spec = ref ".vi" @@ -41,6 +41,12 @@ let file_concat l = if l=[] then "" else List.fold_left (//) (List.hd l) (List.tl l) +let make_ml_module_name filename = + (* Computes a ML Module name from its physical name *) + let fn = try Filename.chop_extension filename with _ -> filename in + let bn = Filename.basename fn in + String.capitalize bn + (* Files specified on the command line *) let mlAccu = ref ([] : (string * string * dir) list) and mliAccu = ref ([] : (string * string * dir) list) @@ -49,28 +55,29 @@ and vAccu = ref ([] : (string * string) list) (* Queue operations *) let addQueue q v = q := v :: !q -let safe_addQueue clq q (k,v) = +let safe_hash_add clq q (k,v) = try - let v2 = List.assoc k !q in + let v2 = Hashtbl.find q k 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) + with Not_found -> Hashtbl.add 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 mlKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t) +let mliKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t) +let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t) +let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) let clash_v = ref ([]: (string list * string list) list) let warning_module_notfound f s = - eprintf "*** Warning : in file %s, module " f; + eprintf "*** Warning : in file %s, library " f; eprintf "%s.v is required and has not been found in loadpath !\n" (String.concat "." s); flush stderr @@ -88,7 +95,7 @@ let warning_clash file dir = 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 " + "*** Warning : in file %s, \n required library %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 @@ -96,15 +103,14 @@ let warning_clash file dir = let safe_assoc verbose file k = if verbose && List.mem_assoc k !clash_v then warning_clash file k; - List.assoc k !vKnown - + Hashtbl.find vKnown k let absolute_dir dir = let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' let absolute_file_name basename odir = let dir = match odir with Some dir -> dir | None -> "." in @@ -130,23 +136,23 @@ let traite_fichier_ML md ext = else begin addQueue deja_vu str; begin try - let mlidir = List.assoc str !mliKnown in + let mlidir = Hashtbl.find mliKnown str 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 mldir = Hashtbl.find mlKnown str 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 mldir = Hashtbl.find mlKnown str 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 mlidir = Hashtbl.find mliKnown str in let filename = file_name ([str],mlidir) in a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmi" with Not_found -> () @@ -184,7 +190,7 @@ let sort () = | Require (_, sl) -> List.iter (fun s -> - try loop (List.assoc s !vKnown) + try loop (Hashtbl.find vKnown s) with Not_found -> ()) sl | RequireString (_, s) -> loop s @@ -216,7 +222,7 @@ let traite_fichier_Coq verbose f = 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 + if verbose && not (Hashtbl.mem coqlibKnown str) then warning_module_notfound f str end) strl | RequireString (spec,s) -> @@ -224,30 +230,31 @@ let traite_fichier_Coq verbose f = if not (List.mem [str] !deja_vu_v) then begin addQueue deja_vu_v [str]; try - let file_str = List.assoc [str] !vKnown in + let file_str = Hashtbl.find vKnown [str] 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 + if not (Hashtbl.mem coqlibKnown [str]) then + warning_notfound f s 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) + let s = make_ml_module_name str in + if not (List.mem s !deja_vu_ml) then begin + addQueue deja_vu_ml s; + try + let mldir = Hashtbl.find mlKnown s in + printf " %s.cmo" (file_name ([String.uncapitalize s],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 + let file_str = Hashtbl.find vKnown [str] in printf " %s.v" (canonize file_str) with Not_found -> () end @@ -304,36 +311,37 @@ 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 + let s' = make_ml_module_name s in + if (Hashtbl.mem mlKnown s') & not (List.mem s' !decl_list) then begin + let mldir = Hashtbl.find mlKnown s in + let fullname = file_name ([(String.uncapitalize 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 _ -> () + 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 @@ -367,11 +375,12 @@ let mL_dependencies () = let coq_dependencies () = List.iter (fun (name,_) -> - printf "%s%s: %s.v" name !suffixe name; + let glob = if !option_glob then " "^name^".glob" else "" in + printf "%s%s%s: %s.v" name !suffixe glob name; traite_fichier_Coq true (name ^ ".v"); printf "\n"; if !option_i then begin - printf "%s%s: %s.v" name !suffixe_spec name; + printf "%s%s%s: %s.v" name !suffixe_spec glob name; traite_fichier_Coq false (name ^ ".v"); printf "\n"; end; @@ -387,8 +396,8 @@ let declare_dependencies () = let rec warning_mult suf l = let tab = Hashtbl.create 151 in - List.iter - (fun (f,d) -> + Hashtbl.iter + (fun f d -> begin try let d' = Hashtbl.find tab f in if (Filename.dirname (file_name ([f],d))) @@ -400,163 +409,128 @@ let rec warning_mult suf l = 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] [-R dir coqdir] [-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 +let add_coqlib_known phys_dir log_dir f = + if Filename.check_suffix f ".vo" then + let basename = Filename.chop_suffix f ".vo" in + let name = log_dir@[basename] in + Hashtbl.add coqlibKnown [basename] (); + Hashtbl.add coqlibKnown name () + +let add_known phys_dir log_dir f = + if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then + let basename = make_ml_module_name f in + Hashtbl.add mlKnown 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_hash_add clash_v vKnown (n,file)) paths + +(* Visits all the directories under [dir], including [dir], + or just [dir] if [recur=false] *) + +let rec add_directory recur add_file phys_dir log_dir = + let dirh = opendir phys_dir in + try + while true do + let f = readdir dirh in + (* we avoid . .. and all hidden files and subdirs (e.g. .svn) *) + if f.[0] <> '.' then + let phys_f = phys_dir//f in + match try (stat phys_f).st_kind with _ -> S_BLK with + | S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f]) + | S_REG -> add_file phys_dir log_dir f + | _ -> () + done + with End_of_file -> closedir dirh + +let add_dir add_file phys_dir log_dir = + try add_directory false add_file phys_dir log_dir with Unix_error _ -> () + +let add_rec_dir add_file phys_dir log_dir = + handle_unix_error (add_directory true add_file phys_dir) log_dir + +let rec treat_file 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.[0] <> '.' then + let dir=opendir complete_name in + let newdirname = + match dirname with + | None -> name + | Some d -> d//name + in + try + while true do treat_file (Some newdirname) (readdir dir) done + with End_of_file -> closedir dir) | 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) + 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 + let name = file_name ([basename],dirname) in + addQueue vAccu (name, absolute_file_name basename dirname) | _ -> () -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 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 + | "-boot" :: ll -> option_boot := true; parse ll + | "-sort" :: ll -> option_sort := true; parse ll + | "-glob" :: ll -> option_glob := true; parse ll + | "-I" :: r :: ll -> add_dir add_known r []; parse ll + | "-I" :: [] -> usage () + | "-R" :: r :: ln :: ll -> add_rec_dir add_known 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 () + | "-slash" :: ll -> option_slash := true; parse ll + | f :: ll -> treat_file None f; parse ll + | [] -> () 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 - let name = file_name ([basename],dirname) in - addQueue vAccu (name, absolute_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) = - directories_added := true; - 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 () - | "-slash" :: ll -> option_slash := true; parse ll - | f :: ll -> treat None f; parse ll - | [] -> () - in - if not !directories_added then add_directory (".", []); + if Array.length Sys.argv < 2 then usage (); 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"); - add_coqlib_directory (!coqlib//"user-contrib"); - 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_boot then begin + add_rec_dir add_known "theories" ["Coq"]; + add_rec_dir add_known "contrib" ["Coq"] + end else begin + add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"]; + add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"]; + add_dir add_coqlib_known (!coqlib//"user-contrib") [] + end; + List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu; + List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu; + warning_mult ".mli" mliKnown; + warning_mult ".ml" mlKnown; 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 (); diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8ecab3b4..cc9f2175 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqdep_lexer.mll 8737 2006-04-26 21:55:21Z herbelin $ i*) +(*i $Id: coqdep_lexer.mll 10721 2008-03-26 14:40:30Z notin $ i*) { @@ -215,7 +215,7 @@ and modules = parse | '"' [^'"']* '"' { let lex = (Lexing.lexeme lexbuf) in let str = String.sub lex 1 (String.length lex - 2) in - mllist := str :: !mllist; modules lexbuf } + mllist := str :: !mllist; modules lexbuf} | _ { (Declare (List.rev !mllist)) } and qual_id = parse diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 8a774876..44b9bd3c 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -26,14 +26,18 @@ let out_to = ref MultFiles let out_channel = ref stdout let open_out_file f = - let f = if !output_dir <> "" then Filename.concat !output_dir f else f in + let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in out_channel := open_out f let close_out_file () = close_out !out_channel let header_trailer = ref true -let quiet = ref false +let header_file = ref "" +let header_file_spec = ref false +let footer_file = ref "" +let footer_file_spec = ref false +let quiet = ref true let light = ref false let gallina = ref false let short = ref false diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 2c07b9fc..d31314c5 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -8,20 +8,20 @@ \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{coqdoc}[2002/02/11] -% Headings -\usepackage{fancyhdr} -\newcommand{\coqdocleftpageheader}{\thepage\ -- \today} -\newcommand{\coqdocrightpageheader}{\today\ -- \thepage} -\pagestyle{fancyplain} +% % Headings +% \usepackage{fancyhdr} +% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today} +% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage} +% \pagestyle{fancyplain} -%BEGIN LATEX -\headsep 8mm -\renewcommand{\plainheadrulewidth}{0.4pt} -\renewcommand{\plainfootrulewidth}{0pt} -\lhead[\coqdocleftpageheader]{\leftmark} -\rhead[\leftmark]{\coqdocrightpageheader} -\cfoot{} -%END LATEX +% %BEGIN LATEX +% \headsep 8mm +% \renewcommand{\plainheadrulewidth}{0.4pt} +% \renewcommand{\plainfootrulewidth}{0pt} +% \lhead[\coqdocleftpageheader]{\leftmark} +% \rhead[\leftmark]{\coqdocrightpageheader} +% \cfoot{} +% %END LATEX % Hevea puts to much space with \medskip and \bigskip %HEVEA\renewcommand{\medskip}{} @@ -36,11 +36,27 @@ %END LATEX % macro for typesetting keywords -\newcommand{\coqdockw}[1]{\textsf{#1}} +\newcommand{\coqdockw}[1]{\texttt{#1}} -% macro for typesetting identifiers +% macro for typesetting variable identifiers \newcommand{\coqdocid}[1]{\textit{#1}} +% macro for typesetting constant identifiers +\newcommand{\coqdoccst}[1]{\textsf{#1}} + +% macro for typesetting module identifiers +\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}} + +% macro for typesetting module constant identifiers (e.g. Parameters in +% module types) +\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}} + +% macro for typesetting inductive type identifiers +\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}} + +% macro for typesetting constructor identifiers +\newcommand{\coqdocconstr}[1]{\textsf{#1}} + % newline and indentation %BEGIN LATEX \newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} @@ -52,6 +68,86 @@ % macro for typesetting the title of a module implementation \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } +\usepackage{ifpdf} +\ifpdf + \usepackage[pdftex]{hyperref} + \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} + \usepackage[all]{hypcap} + + \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}} + \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}} + \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}} + \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection + \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}} +\else + \newcommand{\coqdef}[3]{#3} + \newcommand{\coqref}[2]{#2} + \newcommand{\identref}[2]{\textsf {#2}} + \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}} +\fi +\usepackage{xr} + +%\usepackage{color} +%\usepackage{multind} +%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} + + + +\newcommand{\coqdocvar}[1]{{\textit{#1}}} +\newcommand{\coqdoctac}[1]{{\texttt{#1}}} + + +\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} +%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} +\newcommand{\coqvariable}[2]{\coqdocid{#2}} + +\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}} +\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}} + +\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} + +\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}} + +%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}} + +\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}} +\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}} + +\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}} + %HEVEA\newcommand{\lnot}{\coqwkw{not}} %HEVEA\newcommand{\lor}{\coqwkw{or}} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 4b53d6ff..1da8ebd7 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*) +(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*) open Cdglobals @@ -19,13 +19,23 @@ type entry_type = | Inductive | Constructor | Lemma + | Record + | Projection + | Instance + | Class + | Method | Variable | Axiom | TacticDefinition + | Abbreviation + | Notation + | Section + +val type_name : entry_type -> string type index_entry = | Def of string * entry_type - | Ref of coq_module * string + | Ref of coq_module * string * entry_type | Mod of coq_module * string val find : coq_module -> loc -> index_entry @@ -42,7 +52,7 @@ val scan_file : string -> coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> unit +val read_glob : string -> coq_module (*s Indexes *) @@ -51,6 +61,8 @@ type 'a index = { idx_entries : (char * (string * 'a) list) list; idx_size : int } +val current_library : string ref + val all_entries : unit -> (coq_module * entry_type) index * (entry_type * coq_module index) list diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 5b281b8b..fc2090dc 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* "<>" then + if id <> "<>" then + sp ^ "." ^ id + else sp + else if id <> "<>" + then id + else "" + +let add_def loc ty sp id = + Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) +let add_ref m loc m' sp id ty = + Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty)) + let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id)) let find m l = Hashtbl.find table (m, l) - (*s Manipulating path prefixes *) type stack = string list @@ -99,14 +118,15 @@ let make_fullid id = else id + (* Coq modules *) let split_sp s = try let i = String.rindex s '.' in - String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1) - with Not_found -> - "", s + String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1) + with + Not_found -> "", s let modules = Hashtbl.create 97 let local_modules = Hashtbl.create 97 @@ -118,8 +138,7 @@ let add_module m = type module_kind = Local | Coqlib | Unknown -let coq_module m = - String.length m >= 4 && String.sub m 0 4 = "Coq." +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 @@ -129,14 +148,6 @@ let find_module m = 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_library (loc+i+1) (Hashtbl.find modules id) id - with Not_found -> - () (* Building indexes *) @@ -181,10 +192,18 @@ let type_name = function | Inductive -> "inductive" | Constructor -> "constructor" | Lemma -> "lemma" + | Record -> "record" + | Projection -> "projection" + | Instance -> "instance" + | Class -> "class" + | Method -> "method" | Variable -> "variable" | Axiom -> "axiom" | TacticDefinition -> "tactic" - + | Abbreviation -> "abbreviation" + | Notation -> "notation" + | Section -> "section" + let all_entries () = let gl = ref [] in let add_g s m t = gl := (s,(m,t)) :: !gl in @@ -209,6 +228,8 @@ let all_entries () = } (*s Shortcuts for regular expressions. *) +let digit = ['0'-'9'] +let num = digit+ let space = [' ' '\010' '\013' '\009' '\012'] @@ -225,16 +246,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)" (*s Indexing entry point. *) rule traverse = parse - | "Definition" space + | ("Program" space+)? "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 + | ("Program" space+)? "Fixpoint" space { current_type := Definition; index_ident lexbuf; fixpoint lexbuf; traverse lexbuf } - | ("Lemma" | "Theorem") space + | ("Program" space+)? ("Lemma" | "Theorem") space + { current_type := Lemma; index_ident lexbuf; traverse lexbuf } + | "Obligation" space num ("of" ident)? { current_type := Lemma; index_ident lexbuf; traverse lexbuf } | "Inductive" space { current_type := Inductive; @@ -247,8 +270,8 @@ rule traverse = parse | "Variable" 's'? space { current_type := Variable; index_idents lexbuf; traverse lexbuf } ***i*) - | "Require" (space+ ("Export"|"Import"))? space+ ident - { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf } + | "Require" (space+ ("Export"|"Import"))? + { module_refs lexbuf; traverse lexbuf } | "End" space+ { end_ident lexbuf; traverse lexbuf } | begin_hide @@ -277,7 +300,7 @@ and index_ident = parse | Lemma -> make_fullid id | _ -> id in - add_def (lexeme_start lexbuf) !current_type fullid } + add_def (lexeme_start lexbuf) !current_type "" fullid } | eof { () } | _ @@ -289,7 +312,7 @@ and index_idents = parse | space+ | ',' { index_idents lexbuf } | ident - { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf); + { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf); index_idents lexbuf } | eof { () } @@ -369,14 +392,52 @@ and module_ident = parse { () } | ident { let id = lexeme lexbuf in - begin_module id; add_def (lexeme_start lexbuf) !current_type id } + begin_module id; add_def (lexeme_start lexbuf) !current_type "" id } | eof { () } | _ { () } +(*s parse module names *) + +and module_refs = parse + | space+ + { module_refs lexbuf } + | ident + { let id = lexeme lexbuf in + (try + add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id + with + Not_found -> () + ); + module_refs lexbuf } + | eof + { () } + | _ + { () } + { - + let type_of_string = function + | "def" | "coe" | "subclass" | "canonstruc" + | "ex" | "scheme" -> Definition + | "prf" | "thm" -> Lemma + | "ind" | "coind" -> Inductive + | "constr" -> Constructor + | "rec" | "corec" -> Record + | "proj" -> Projection + | "class" -> Class + | "meth" -> Method + | "inst" -> Instance + | "var" -> Variable + | "defax" | "prfax" | "ax" -> Axiom + | "syndef" -> Abbreviation + | "not" -> Notation + | "lib" -> Library + | "mod" | "modtype" -> Module + | "tac" -> TacticDefinition + | "sec" -> Section + | s -> raise (Invalid_argument ("type_of_string:" ^ s)) + let read_glob f = let c = open_in f in let cur_mod = ref "" in @@ -387,22 +448,22 @@ and module_ident = parse if n > 0 then begin match s.[0] with | 'F' -> - cur_mod := String.sub s 1 (n - 1) + cur_mod := String.sub s 1 (n - 1); + current_library := !cur_mod | 'R' -> (try - let i = String.index s ' ' in - let j = String.index_from s (i+1) ' ' in - let loc = int_of_string (String.sub s 1 (i - 1)) in - let lib_dp = String.sub s (i + 1) (j - i - 1) in - let full_id = String.sub s (j + 1) (n - j - 1) in - add_ref !cur_mod loc lib_dp full_id - with Not_found -> - ()) - | _ -> () + Scanf.sscanf s "R%d %s %s %s %s" + (fun loc lib_dp sp id ty -> + add_ref !cur_mod loc lib_dp sp id (type_of_string ty)) + with _ -> ()) + | _ -> + try Scanf.sscanf s "%s %d %s %s" + (fun ty loc sp id -> add_def loc (type_of_string ty) sp id) + with Scanf.Scan_failure _ -> () end - done + done; assert false with End_of_file -> - close_in c + close_in c; !cur_mod let scan_file f m = init_stack (); current_library := m; diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 18a44a44..7111187f 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -19,50 +20,53 @@ *) open Cdglobals -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 " --stdout write output to stdout"; - 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 " --coqlib_path set the path where Coq files are installed"; - 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 " --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 " --pdf output the Pdf"; + prerr_endline " --stdout write output to stdout"; + 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 " --with-header prepend as html reader"; + prerr_endline " --with-footer append as html footer"; + 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 (default)"; + prerr_endline " --verbose verbose mode"; + 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 " --coqlib_path set the path where Coq files are installed"; + 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 ""; exit 1 +let obsolete s = + eprintf "Warning: option %s is now obsolete; please update your scripts\n" s + (*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 @@ -74,7 +78,7 @@ let banner () = flush stderr let target_full_name f = - match !target_language with + match !Cdglobals.target_language with | HTML -> f ^ ".html" | _ -> f ^ ".tex" @@ -88,95 +92,70 @@ let check_if_file_exists f = eprintf "\ncoqdoc: %s: no such file\n" f; exit 1 end - + + +(*s Manipulations of paths and path aliases *) + +let normalize_path p = + (* We use the Unix subsystem to normalize a physical path (relative + or absolute) and get rid of symbolic links, relative links (like + ./ or ../ in the middle of the path; it's tricky but it + works... *) + (* Rq: Sys.getcwd () returns paths without '/' at the end *) + let orig = Sys.getcwd () in + Sys.chdir p; + let res = Sys.getcwd () in + Sys.chdir orig; + res + +let normalize_filename f = + let basename = Filename.basename f in + let dirname = Filename.dirname f in + Filename.concat (normalize_path dirname) basename + +(* [paths] maps a physical path to a name *) let paths = ref [] -let add_path m l = paths := (m,l) :: !paths +let add_path dir name = + (* if dir is relative we add both the relative and absolute name *) + let p = normalize_path dir in + paths := (p,name) :: !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 name_of_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 coq_module filename = + let bfname = Filename.chop_extension filename in + let nfname = normalize_filename bfname in + let rec change_prefix map f = + match map with + | [] -> + (* There is no prefix alias; + we just cut the name wrt current working directory *) + let cwd = Sys.getcwd () in + let exp = Str.regexp (Str.quote (cwd ^ "/")) in + if (Str.string_match exp f 0) then + name_of_path (Str.replace_first exp "" f) + else + name_of_path f + | (p, name) :: rem -> + let expp = Str.regexp (Str.quote p) in + if (Str.string_match expp f 0) then + let newp = Str.replace_first expp name f in + name_of_path newp + else + change_prefix rem f + in + change_prefix !paths nfname let what_file f = check_if_file_exists f; - if check_suffix f ".v" || check_suffix f ".g" then + if Filename.check_suffix f ".v" || Filename.check_suffix f ".g" then Vernac_file (f, coq_module f) - else if check_suffix f ".tex" then + else if Filename.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 + else + (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1) (*s \textbf{Reading file names from a file.} * File names may be given @@ -214,9 +193,9 @@ let files_from_file f = (*s \textbf{Parsing of the command line.} *) -let output_file = ref "" let dvi = ref false let ps = ref false +let pdf = ref false let parse () = let files = ref [] in @@ -227,8 +206,16 @@ let parse () = | ("-nopreamble" | "--nopreamble" | "--no-preamble" | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> header_trailer := false; parse_rec rem + | ("-with-header" | "--with-header") :: f ::rem -> + header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem + | ("-with-header" | "--with-header") :: [] -> + usage () + | ("-with-footer" | "--with-footer") :: f ::rem -> + header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem + | ("-with-footer" | "--with-footer") :: [] -> + usage () | ("-p" | "--preamble") :: s :: rem -> - push_in_preamble s; parse_rec rem + Output.push_in_preamble s; parse_rec rem | ("-p" | "--preamble") :: [] -> usage () | ("-noindex" | "--noindex" | "--no-index") :: rem -> @@ -259,6 +246,8 @@ let parse () = usage () | ("-latex" | "--latex") :: rem -> Cdglobals.target_language := LaTeX; parse_rec rem + | ("-pdf" | "--pdf") :: rem -> + Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem | ("-dvi" | "--dvi") :: rem -> Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem | ("-ps" | "--ps") :: rem -> @@ -284,10 +273,12 @@ let parse () = | ("-q" | "-quiet" | "--quiet") :: rem -> quiet := true; parse_rec rem + | ("-v" | "-verbose" | "--verbose") :: rem -> + quiet := false; parse_rec rem | ("-h" | "-help" | "-?" | "--help") :: rem -> banner (); usage () - | ("-v" | "-version" | "--version") :: _ -> + | ("-V" | "-version" | "--version") :: _ -> banner (); exit 0 | ("-vernac-file" | "--vernac-file") :: f :: rem -> @@ -309,7 +300,7 @@ let parse () = | "-R" :: ([] | [_]) -> usage () | ("-glob-from" | "--glob-from") :: f :: rem -> - Index.read_glob f; parse_rec rem + obsolete "glob-from"; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> @@ -332,7 +323,7 @@ let parse () = (*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. *) + we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *) let locally dir f x = let cwd = Sys.getcwd () in @@ -346,8 +337,10 @@ let clean_temp_files basefile = remove (basefile ^ ".tex"); remove (basefile ^ ".log"); remove (basefile ^ ".aux"); + remove (basefile ^ ".toc"); remove (basefile ^ ".dvi"); remove (basefile ^ ".ps"); + remove (basefile ^ ".pdf"); remove (basefile ^ ".haux"); remove (basefile ^ ".html") @@ -370,70 +363,81 @@ let copy src dst = (*s Functions for generating output files *) - + let gen_one_file l = let file = function | Vernac_file (f,m) -> - set_module m; coq_file f m + Output.set_module m; Pretty.coq_file f m | Latex_file _ -> () in - if (!header_trailer) then header (); - if !toc then make_toc (); + if (!header_trailer) then Output.header (); + if !toc then Output.make_toc (); List.iter file l; - if !index then make_index(); - if (!header_trailer) then trailer () + if !index then Output.make_index(); + if (!header_trailer) then Output.trailer () let gen_mult_files l = let file = function | Vernac_file (f,m) -> - set_module m; + Output.set_module m; let hf = target_full_name m in open_out_file hf; - if (!header_trailer) then header (); - if !toc then make_toc (); - coq_file f m; - if (!header_trailer) then trailer (); + if (!header_trailer) then Output.header (); + Pretty.coq_file f m; + if (!header_trailer) then Output.trailer (); close_out_file() | Latex_file _ -> () in List.iter file l; if (!index && !target_language=HTML) then begin - if (!multi_index) then make_multi_index (); + if (!multi_index) then Output.make_multi_index (); open_out_file "index.html"; page_title := (if !title <> "" then !title else "Index"); - if (!header_trailer) then header (); - make_index (); - if (!header_trailer) then trailer (); + if (!header_trailer) then Output.header (); + Output.make_index (); + if (!header_trailer) then Output.trailer (); close_out_file() end; if (!toc && !target_language=HTML) then begin open_out_file "toc.html"; page_title := (if !title <> "" then !title else "Table of contents"); - if (!header_trailer) then header (); + if (!header_trailer) then Output.header (); if !title <> "" then printf "

%s

\n" !title; - make_toc (); - if (!header_trailer) then trailer (); + Output.make_toc (); + if (!header_trailer) then Output.trailer (); close_out_file() end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) +let read_glob x = + match x with + | Vernac_file (f,m) -> + let glob = (Filename.chop_extension f) ^ ".glob" in + (try + Vernac_file (f, Index.read_glob glob) + with _ -> + eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + x) + | Latex_file _ -> x let index_module = function - | Vernac_file (_,m) -> Index.add_module m + | Vernac_file (f,m) -> + Index.add_module m | Latex_file _ -> () let produce_document l = - List.iter index_module l; (if !target_language=HTML then let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in copy src dst); (if !target_language=LaTeX then - let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in - let dst = if !output_dir <> "" then - Filename.concat !output_dir "coqdoc.sty" - else "coqdoc.sty" in - copy src dst); + let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in + let dst = if !output_dir <> "" then + Filename.concat !output_dir "coqdoc.sty" + else "coqdoc.sty" in + copy src dst); + let l = List.map read_glob l in + List.iter index_module l; match !out_to with | StdOut -> Cdglobals.out_channel := stdout; @@ -446,51 +450,64 @@ let produce_document l = gen_mult_files l let produce_output fl = - if not (!dvi || !ps) then begin + if not (!dvi || !ps || !pdf) then produce_document fl - end else begin - let texfile = temp_file "coqdoc" ".tex" in - let basefile = chop_suffix texfile ".tex" in - open_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 + else + begin + let texfile = Filename.temp_file "coqdoc" ".tex" in + let basefile = Filename.chop_suffix texfile ".tex" in + let final_out_to = !out_to in + out_to := File texfile; + output_dir := (Filename.dirname texfile); + produce_document fl; + + let latexexe = if !pdf then "pdflatex" else "latex" in + let latexcmd = + let file = Filename.basename texfile in + let file = + if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file + in + sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "") 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 + let res = locally (Filename.dirname texfile) Sys.command latexcmd 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 + match final_out_to with + | MultFiles | StdOut -> cat dvifile + | File f -> copy dvifile f end; - if !output_file = "" then cat psfile - end; - clean_temp_files basefile - end + let pdffile = basefile ^ ".pdf" in + if !pdf then + begin + match final_out_to with + | MultFiles | StdOut -> cat pdffile + | File f -> copy pdffile f + end; + if !ps then begin + let psfile = 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; + match final_out_to with + | MultFiles | StdOut -> cat psfile + | File f -> copy psfile f + end; + + clean_temp_files basefile + end (*s \textbf{Main program.} Print the banner, parse the command line, diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d0bc6c2..93414f22 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Hashtbl.add token_pp s (Some l, None)) [ "*" , "\\ensuremath{\\times}"; + "|", "\\ensuremath{|}"; "->", "\\ensuremath{\\rightarrow}"; "->~", "\\ensuremath{\\rightarrow\\lnot}"; "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; @@ -153,6 +171,12 @@ module Latex = struct | _ -> output_char c + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + let latex_char = output_char let latex_string = output_string @@ -162,9 +186,14 @@ module Latex = struct let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + let label_ident s = + for i = 0 to String.length s - 1 do label_char s.[i] done + let start_module () = if not !short then begin - printf "\\coqdocmodule{"; + printf "\\coqlibrary{"; + label_ident !current_module; + printf "}{"; raw_ident !current_module; printf "}\n\n" end @@ -192,11 +221,53 @@ module Latex = struct with Not_found -> f tok - let ident s _ = + let module_ref m s = + printf "\\moduleid{%s}{" 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 fid typ s = + let id = if fid <> "" then (m ^ "." ^ fid) else m in + match find_module m with + | Local -> + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" + | Coqlib when !externals -> + let _m = Filename.concat !coqlib m in + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" + | Coqlib | Unknown -> + raw_ident s + + let defref m id ty s = + printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin - printf "\\coqdocid{"; raw_ident s; printf "}" + begin + try + (match Index.find !current_module loc with + | Def (fullid,typ) -> + defref !current_module fullid typ s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid,typ) -> + ident_ref m fullid typ s + | Mod _ -> + printf "\\coqdocid{"; raw_ident s; printf "}") + with Not_found -> + if is_tactic s then begin + printf "\\coqdoctac{"; raw_ident s; printf "}" + end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end + end end let ident s l = with_latex_printing (fun s -> ident s l) s @@ -271,31 +342,51 @@ end module Html = struct let header () = - if !header_trailer then begin - printf "\n"; - printf "\n\n"; - printf "\n" !charset; - printf "\n"; - printf "%s\n\n\n" !page_title; - printf "\n\n
\n\n
\n
\n\n"; - printf "
\n\n" - end + if !header_trailer then + if !header_file_spec then + let cin = Pervasives.open_in !header_file in + try + while true do + let s = Pervasives.input_line cin in + printf "%s\n" s + done + with End_of_file -> Pervasives.close_in cin + else + begin + printf "\n"; + printf "\n\n"; + printf "\n" !charset; + printf "\n"; + printf "%s\n\n\n" !page_title; + printf "\n\n
\n\n
\n
\n\n"; + printf "
\n\n" + end let self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then printf "
\n\n
\n
Index"; - if !header_trailer then begin - printf "
This page has been generated by "; - printf "coqdoc\n" self; - printf "
\n\n
\n\n\n" - end + if !header_trailer then + if !footer_file_spec then + let cin = Pervasives.open_in !footer_file in + try + while true do + let s = Pervasives.input_line cin in + printf "%s\n" s + done + with End_of_file -> Pervasives.close_in cin + else + begin + printf "
This page has been generated by "; + printf "coqdoc\n" self; + printf "
\n\n
\n\n\n" + end let start_module () = if not !short then begin - (* add_toc_entry (Toc_library !current_module); *) + add_toc_entry (Toc_library !current_module); printf "

Library %s

\n\n" !current_module end @@ -338,14 +429,15 @@ module Html = struct raw_ident s i*) - let ident_ref m fid s = match find_module m with - | Local -> - printf "" m fid; raw_ident s; printf "" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "" m fid; raw_ident s; printf "" - | Coqlib | Unknown -> - raw_ident s + let ident_ref m fid s = + match find_module m with + | Local -> + printf "" m fid; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m fid; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s let ident s loc = if is_keyword s then begin @@ -360,9 +452,9 @@ module Html = struct printf "" fullid; raw_ident s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid) -> + | Ref (m,fullid,ty) -> ident_ref m fullid s - | Mod _ | Ref _ -> + | Mod _ -> raw_ident s) with Not_found -> raw_ident s @@ -429,17 +521,6 @@ module Html = struct 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 @@ -465,7 +546,7 @@ module Html = struct if t = Library then "[library]", m ^ ".html" else - sprintf "[%s, in %s]" (entry_type t) m m , + sprintf "[%s, in %s]" (type_name t) m m , sprintf "%s.html#%s" m s) let format_bytype_index = function @@ -548,8 +629,8 @@ module Html = struct item n; printf "" r; f (); printf "\n" in - Queue.iter make_toc_entry toc_q; - stop_item (); + Queue.iter make_toc_entry toc_q; + stop_item (); end diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index e16c7979..8be3e0b0 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* count (c + (8 - (c mod 8))) (i + 1) | ' ' -> count (c + 1) (i + 1) - | _ -> c + | _ -> c,i in - count 0 0 + count 0 0 let count_dashes s = let c = ref 0 in @@ -52,6 +49,11 @@ in count 0 (String.index s '*') + let strip_eol s = + let eol = s.[String.length s - 1] = '\n' in + (eol, if eol then String.sub s 1 (String.length s - 1) else s) + + let formatted = ref false let brackets = ref 0 @@ -69,22 +71,22 @@ let state_stack = Stack.create () let save_state () = - Stack.push { st_gallina = !gallina; st_light = !light } state_stack + Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack let restore_state () = let s = Stack.pop state_stack in - gallina := s.st_gallina; - light := s.st_light + Cdglobals.gallina := s.st_gallina; + Cdglobals.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_gallina = without_ref Cdglobals.gallina - let without_light = without_ref light + let without_light = without_ref Cdglobals.light let show_all f = without_gallina (without_light f) - let begin_show () = save_state (); gallina := false; light := false + let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () (* Reset the globals *) @@ -163,15 +165,20 @@ let space = [' ' '\t'] let space_nl = [' ' '\t' '\n' '\r'] +let nl = "\r\n" | '\n' let firstchar = ['A'-'Z' 'a'-'z' '_' (* iso 8859-1 accents *) '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | + '\194' '\185' | (* utf-8 latin 1 supplement *) '\195' ['\128'-'\191'] | (* utf-8 letterlike symbols *) - '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) + '\206' ['\177'-'\183'] | + '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) + | '\129' [ '\176'-'\187' ] (* superscripts *) + | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) let identchar = firstchar | ['\'' '0'-'9' '@' ] let id = firstchar identchar* @@ -186,8 +193,9 @@ let symbolchar_no_brackets = (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ let symbolchar = symbolchar_no_brackets | '[' | ']' +let token_no_brackets = symbolchar_no_brackets+ let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' - +let printing_token = (token | id)+ let thm_token = "Theorem" @@ -202,6 +210,7 @@ let thm_token = let def_token = "Definition" | "Let" + | "Class" | "SubClass" | "Example" | "Local" @@ -209,11 +218,10 @@ let def_token = | "CoFixpoint" | "Record" | "Structure" + | "Instance" | "Scheme" | "Inductive" | "CoInductive" - | "Program" space+ "Definition" - | "Program" space+ "Fixpoint" let decl_token = "Hypothesis" @@ -224,6 +232,8 @@ let decl_token = let gallina_ext = "Module" + | "Include" space+ "Type" + | "Include" | "Declare" space+ "Module" | "Transparent" | "Opaque" @@ -235,6 +245,11 @@ let gallina_ext = | "Infix" | "Tactic" space+ "Notation" | "Reserved" space+ "Notation" + | "Section" + | "Context" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" let commands = "Pwd" @@ -254,6 +269,12 @@ let commands = | "Check" | "Type" + | "Section" + | "Chapter" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -261,6 +282,12 @@ let extraction = let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction +let prog_kw = + "Program" space+ gallina_kw + | "Obligation" + | "Obligations" + | "Solve" + let gallina_kw_to_hide = "Implicit" | "Ltac" @@ -275,11 +302,6 @@ let gallina_kw_to_hide = | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | "Section" - | "Chapter" - | "Variable" 's'? - | ("Hypothesis" | "Hypotheses") - | "End" | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" @@ -294,10 +316,10 @@ 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_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl +let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl (* let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" @@ -308,16 +330,16 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" (*s Scanning Coq, at beginning of line *) rule coq_bol = parse - | space* '\n'+ - { empty_line_of_code (); coq_bol lexbuf } + | space* nl+ + { Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl - { end_coq (); start_doc (); + { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); + Output.end_doc (); Output.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 } + { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); + Output.start_coq (); coq lexbuf } | space* begin_hide { skip_hide lexbuf; coq_bol lexbuf } | space* begin_show @@ -326,28 +348,38 @@ rule coq_bol = parse { end_show (); coq_bol lexbuf } | space* gallina_kw_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 - let nbsp = count_spaces s in - indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + if !Cdglobals.light && section_or_end s then + let eol = skip_to_dot lexbuf in + if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf + else + begin + let nbsp,isp = count_spaces s in + Output.indentation nbsp; + let s = String.sub s isp (String.length s - isp) in + Output.ident s (lexeme_start lexbuf + isp); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | space* gallina_kw { let s = lexeme lexbuf in - let nbsp = count_spaces s in - let s = String.sub s nbsp (String.length s - nbsp) in - indentation nbsp; - ident s (lexeme_start lexbuf + nbsp); + let nbsp,isp = count_spaces s in + let s = String.sub s isp (String.length s - isp) in + Output.indentation nbsp; + Output.ident s (lexeme_start lexbuf + isp); let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space* "(**" space+ "printing" space+ (identifier | token) space+ + | space* prog_kw + { let s = lexeme lexbuf in + let nbsp,isp = count_spaces s in + Output.indentation nbsp; + let s = String.sub s isp (String.length s - isp) in + Output.ident s (lexeme_start lexbuf + isp); + let eol= body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + + | space* "(**" space+ "printing" space+ printing_token space+ { let tok = lexeme lexbuf in - let s = printing_token lexbuf in + let s = printing_token_body lexbuf in add_printing_token tok s; coq_bol lexbuf } | space* "(**" space+ "printing" space+ @@ -366,13 +398,13 @@ rule coq_bol = parse coq_bol lexbuf } | space* "(*" { let eol = comment lexbuf in - if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf } + if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ { let eol = - if not !gallina then - begin backtrack lexbuf; indentation 0; body_bol lexbuf end + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end else skip_to_dot lexbuf in @@ -381,141 +413,148 @@ rule coq_bol = parse (*s Scanning Coq elsewhere *) and coq = parse - | "\n" - { line_break(); coq_bol lexbuf } + | nl + { Output.line_break(); coq_bol lexbuf } | "(**" space_nl - { end_coq (); start_doc (); + { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); + Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } | "(*" { let eol = comment lexbuf in - if eol then begin line_break(); coq_bol lexbuf end + if eol then begin Output.line_break(); coq_bol lexbuf end else coq lexbuf } - | '\n'+ space* "]]" - { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end } + | nl+ space* "]]" + { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end } | eof { () } | gallina_kw_to_hide { let s = lexeme lexbuf in - if !light && section_or_end s then + if !Cdglobals.light && section_or_end s then begin let eol = skip_to_dot lexbuf in if eol then coq_bol lexbuf else coq lexbuf end else begin - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } | gallina_kw { let s = lexeme lexbuf in - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space+ { char ' '; coq lexbuf } + | prog_kw + { let s = lexeme lexbuf in + Output.ident s (lexeme_start lexbuf); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | space+ { Output.char ' '; coq lexbuf } | eof { () } - | _ { let eol = - if not !gallina then - begin backtrack lexbuf; indentation 0; body lexbuf end + | _ { let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body lexbuf end else - skip_to_dot lexbuf + let eol = skip_to_dot lexbuf in + if eol then Output.line_break (); eol in if eol then coq_bol lexbuf else 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 } + | space* nl+ + { Output.paragraph (); doc_bol lexbuf } + | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? + { let eol, lex = strip_eol (lexeme lexbuf) in + let lev, s = sec_title lex in + Output.section lev (fun () -> ignore (doc (from_string s))); + if eol then doc_bol lexbuf else doc lexbuf } + | space* '-'+ + { let n = count_dashes (lexeme lexbuf) in + if n >= 4 then Output.rule () else Output.item n; + doc lexbuf } + | "<<" space* + { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } | eof - { false } + { true } | _ { backtrack lexbuf; doc lexbuf } (*s Scanning documentation elsewhere *) and doc = parse - | "\n" - { char '\n'; doc_bol lexbuf } + | nl + { Output.char '\n'; doc_bol lexbuf } | "[" { brackets := 1; - start_inline_coq (); escaped_coq lexbuf; end_inline_coq (); + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); doc lexbuf } - | "[[" '\n' space* - { formatted := true; line_break (); start_inline_coq (); - indentation (count_spaces (lexeme lexbuf)); + | "[[" nl space* + { formatted := true; Output.line_break (); Output.start_inline_coq (); + Output.indentation (fst (count_spaces (lexeme lexbuf))); let eol = body_bol lexbuf in - end_inline_coq (); formatted := false; + Output.end_inline_coq (); formatted := false; if eol then doc_bol lexbuf else doc lexbuf} - | '*'* "*)" space* '\n' + | '*'* "*)" space* nl { true } | '*'* "*)" { false } | "$" - { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } + { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } | "$$" - { char '$'; doc lexbuf } + { Output.char '$'; doc lexbuf } | "%" { escaped_latex lexbuf; doc lexbuf } | "%%" - { char '%'; doc lexbuf } + { Output.char '%'; doc lexbuf } | "#" { escaped_html lexbuf; doc lexbuf } | "##" - { char '#'; doc lexbuf } + { Output.char '#'; doc lexbuf } | eof { false } | _ - { char (lexeme_char lexbuf 0); doc lexbuf } + { Output.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 } + | "$" { Output.stop_latex_math () } + | eof { Output.stop_latex_math () } + | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } and escaped_latex = parse | "%" { () } | eof { () } - | _ { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } + | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } and escaped_html = parse | "#" { () } | "&#" - { html_char '&'; html_char '#'; escaped_html lexbuf } + { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf } | "##" - { html_char '#'; escaped_html lexbuf } + { Output.html_char '#'; escaped_html lexbuf } | eof { () } - | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } + | _ { Output.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 } + | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () } + | eof { Output.stop_verbatim () } + | _ { Output.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 } + if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end } | "[" - { incr brackets; char '['; escaped_coq lexbuf } + { incr brackets; Output.char '['; escaped_coq lexbuf } | "(*" { ignore (comment lexbuf); escaped_coq lexbuf } | "*)" @@ -524,18 +563,18 @@ and escaped_coq = parse { () } | token_brackets { let s = lexeme lexbuf in - symbol s; + Output.symbol s; escaped_coq lexbuf } | (identifier '.')* identifier - { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } + { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } | _ - { char (lexeme_char lexbuf 0); escaped_coq lexbuf } + { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf } (*s Coq "Comments" command. *) and comments = parse | space_nl+ - { char ' '; comments lexbuf } + { Output.char ' '; comments lexbuf } | '"' [^ '"']* '"' { let s = lexeme lexbuf in let s = String.sub s 1 (String.length s - 2) in @@ -547,61 +586,79 @@ and comments = parse | eof { () } | _ - { char (lexeme_char lexbuf 0); comments lexbuf } + { Output.char (lexeme_char lexbuf 0); comments lexbuf } (*s Skip comments *) and comment = parse - | "(*" { ignore (comment lexbuf); comment lexbuf } - | "*)" space* '\n'+ { true } + | "(*" { comment lexbuf } + | "*)" space* nl { true } | "*)" { false } | eof { false } | _ { comment lexbuf } and skip_to_dot = parse - | '.' space* '\n' { true } + | '.' space* nl { true } | eof | '.' space+ { false} | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf } | _ { skip_to_dot lexbuf } and body_bol = parse | space+ - { indentation (count_spaces (lexeme lexbuf)); body lexbuf } + { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } | _ { backtrack lexbuf; body lexbuf } and body = parse - | '\n' {line_break(); body_bol lexbuf} - | '\n'+ space* "]]" - { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true } + | nl {Output.line_break(); body_bol lexbuf} + | nl+ space* "]]" + { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true } | eof { false } - | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true } - | '.' space+ { char '.'; char ' '; false } + | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true } + | '.' space+ { Output.char '.'; Output.char ' '; false } + | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf } | "(*" { let eol = comment lexbuf in - if eol then begin line_break(); body_bol lexbuf end else body lexbuf } + if eol + then begin Output.line_break(); body_bol lexbuf end + else body lexbuf } | identifier { let s = lexeme lexbuf in - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); body lexbuf } - | token + | token_no_brackets { let s = lexeme lexbuf in - symbol s; body lexbuf } + Output.symbol s; body lexbuf } | _ { let c = lexeme_char lexbuf 0 in - char c; + Output.char c; body lexbuf } +and notation_bol = parse + | space+ + { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf } + | _ { backtrack lexbuf; notation lexbuf } + +and notation = parse + | nl { Output.line_break(); notation_bol lexbuf } + | '"' { Output.char '"'; false } + | token + { let s = lexeme lexbuf in + Output.symbol s; notation lexbuf } + | _ { let c = lexeme_char lexbuf 0 in + Output.char c; + notation lexbuf } + and skip_hide = parse | eof | end_hide { () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) -and printing_token = parse +and printing_token_body = parse | "*)" | eof { let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } | _ { Buffer.add_string token_buffer (lexeme lexbuf); - printing_token lexbuf } + printing_token_body lexbuf } (*s Applying the scanners to files *) @@ -609,11 +666,11 @@ and printing_token = parse let coq_file f m = reset (); - Index.scan_file f m; - start_module (); + Index.current_library := m; + Output.start_module (); let c = open_in f in let lb = from_channel c in - start_coq (); coq_bol lb; end_coq (); + Output.start_coq (); coq_bol lb; Output.end_coq (); close_in c } diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 0ce172ea..81fe06cd 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -9,7 +9,7 @@ (* coqwc - counts the lines of spec, proof and comments in Coq sources * Copyright (C) 2003 Jean-Christophe Filliâtre *) -(*i $Id: coqwc.mll 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: coqwc.mll 9691 2007-03-08 15:29:27Z msozeau $ i*) (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. It assumes the files to be lexically well-formed. *) -- cgit v1.2.3