diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
109 files changed, 1602 insertions, 1248 deletions
@@ -107,8 +107,8 @@ parsing/coqast.cmi: lib/util.cmi kernel/names.cmi library/libnames.cmi \ lib/dyn.cmi parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ - interp/ppextend.cmi kernel/names.cmi interp/genarg.cmi parsing/extend.cmi \ - parsing/coqast.cmi parsing/ast.cmi + parsing/pptactic.cmi interp/ppextend.cmi kernel/names.cmi \ + interp/genarg.cmi parsing/extend.cmi parsing/coqast.cmi parsing/ast.cmi parsing/esyntax.cmi: interp/topconstr.cmi interp/symbols.cmi \ interp/ppextend.cmi lib/pp.cmi parsing/extend.cmi parsing/coqast.cmi \ parsing/ast.cmi @@ -508,10 +508,10 @@ ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi ide/highlight.cmx: ide/ideutils.cmx -ide/ideutils.cmo: ide/utf8_convert.cmo ide/preferences.cmi lib/pp_control.cmi \ - lib/options.cmi config/coq_config.cmi ide/ideutils.cmi -ide/ideutils.cmx: ide/utf8_convert.cmx ide/preferences.cmx lib/pp_control.cmx \ - lib/options.cmx config/coq_config.cmx ide/ideutils.cmi +ide/ideutils.cmo: ide/utf8_convert.cmo lib/system.cmi ide/preferences.cmi \ + lib/pp_control.cmi lib/options.cmi config/coq_config.cmi ide/ideutils.cmi +ide/ideutils.cmx: ide/utf8_convert.cmx lib/system.cmx ide/preferences.cmx \ + lib/pp_control.cmx lib/options.cmx config/coq_config.cmx ide/ideutils.cmi ide/preferences.cmo: lib/util.cmi lib/system.cmi ide/utils/configwin.cmi \ ide/config_lexer.cmo ide/preferences.cmi ide/preferences.cmx: lib/util.cmx lib/system.cmx ide/utils/configwin.cmx \ @@ -703,11 +703,11 @@ kernel/sign.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \ kernel/sign.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \ kernel/sign.cmi kernel/subtyping.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ - kernel/reduction.cmi kernel/names.cmi kernel/modops.cmi \ + kernel/reduction.cmi lib/pp.cmi kernel/names.cmi kernel/modops.cmi \ kernel/inductive.cmi kernel/environ.cmi kernel/declarations.cmi \ kernel/subtyping.cmi kernel/subtyping.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \ - kernel/reduction.cmx kernel/names.cmx kernel/modops.cmx \ + kernel/reduction.cmx lib/pp.cmx kernel/names.cmx kernel/modops.cmx \ kernel/inductive.cmx kernel/environ.cmx kernel/declarations.cmx \ kernel/subtyping.cmi kernel/term.cmo: lib/util.cmi kernel/univ.cmi lib/pp.cmi kernel/names.cmi \ @@ -904,14 +904,14 @@ parsing/coqast.cmx: lib/util.cmx kernel/names.cmx library/libnames.cmx \ lib/hashcons.cmx lib/dyn.cmx parsing/coqast.cmi parsing/egrammar.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo library/summary.cmi \ - interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \ - kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + parsing/pptactic.cmi interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi \ + lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \ parsing/lexer.cmi interp/genarg.cmi parsing/extend.cmi lib/bignat.cmi \ parsing/ast.cmi parsing/egrammar.cmi parsing/egrammar.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx proofs/tacexpr.cmx library/summary.cmx \ - interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \ - kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx \ + lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \ parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx lib/bignat.cmx \ parsing/ast.cmx parsing/egrammar.cmi parsing/esyntax.cmo: lib/util.cmi interp/topconstr.cmi interp/symbols.cmi \ @@ -1488,18 +1488,20 @@ proofs/logic.cmo: lib/util.cmi pretyping/typing.cmi kernel/typeops.cmi \ proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \ pretyping/pretype_errors.cmi lib/pp.cmi lib/options.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ - pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \ - pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ - parsing/coqast.cmi interp/constrextern.cmi proofs/logic.cmi + pretyping/inductiveops.cmi kernel/inductive.cmi kernel/indtypes.cmi \ + library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ + kernel/environ.cmi parsing/coqast.cmi interp/constrextern.cmi \ + proofs/logic.cmi proofs/logic.cmx: lib/util.cmx pretyping/typing.cmx kernel/typeops.cmx \ kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \ kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \ proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \ pretyping/pretype_errors.cmx lib/pp.cmx lib/options.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ - pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \ - pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ - parsing/coqast.cmx interp/constrextern.cmx proofs/logic.cmi + pretyping/inductiveops.cmx kernel/inductive.cmx kernel/indtypes.cmx \ + library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ + kernel/environ.cmx parsing/coqast.cmx interp/constrextern.cmx \ + proofs/logic.cmi proofs/pfedit.cmo: lib/util.cmi pretyping/typing.cmi kernel/term.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi \ kernel/safe_typing.cmi proofs/refiner.cmi proofs/proof_type.cmi \ @@ -1597,9 +1599,10 @@ tactics/auto.cmo: toplevel/vernacexpr.cmo lib/util.cmi pretyping/typing.cmi \ pretyping/matching.cmi proofs/logic.cmi library/library.cmi \ library/libobject.cmi library/libnames.cmi library/lib.cmi \ kernel/inductive.cmi tactics/hipattern.cmi tactics/hiddentac.cmi \ - library/global.cmi pretyping/evd.cmi proofs/evar_refiner.cmi \ - tactics/dhyp.cmi kernel/declarations.cmi interp/constrintern.cmi \ - proofs/clenv.cmi tactics/btermdn.cmi tactics/auto.cmi + library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ + proofs/evar_refiner.cmi tactics/dhyp.cmi kernel/declarations.cmi \ + interp/constrintern.cmi proofs/clenv.cmi tactics/btermdn.cmi \ + tactics/auto.cmi tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \ pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ @@ -1611,9 +1614,10 @@ tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \ pretyping/matching.cmx proofs/logic.cmx library/library.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ kernel/inductive.cmx tactics/hipattern.cmx tactics/hiddentac.cmx \ - library/global.cmx pretyping/evd.cmx proofs/evar_refiner.cmx \ - tactics/dhyp.cmx kernel/declarations.cmx interp/constrintern.cmx \ - proofs/clenv.cmx tactics/btermdn.cmx tactics/auto.cmi + library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ + proofs/evar_refiner.cmx tactics/dhyp.cmx kernel/declarations.cmx \ + interp/constrintern.cmx proofs/clenv.cmx tactics/btermdn.cmx \ + tactics/auto.cmi tactics/autorewrite.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \ @@ -1924,10 +1928,11 @@ tactics/tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi proofs/logic.cmi \ library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ pretyping/indrec.cmi tactics/hipattern.cmi library/global.cmi \ - interp/genarg.cmi pretyping/evd.cmi proofs/evar_refiner.cmi \ - kernel/environ.cmi kernel/entries.cmi library/declare.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \ - interp/constrintern.cmi proofs/clenv.cmi tactics/tactics.cmi + interp/genarg.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ + proofs/evar_refiner.cmi kernel/environ.cmi kernel/entries.cmi \ + library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \ + interp/coqlib.cmi interp/constrintern.cmi proofs/clenv.cmi \ + tactics/tactics.cmi tactics/tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ proofs/tacexpr.cmx kernel/sign.cmx proofs/refiner.cmx \ @@ -1936,10 +1941,11 @@ tactics/tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx proofs/logic.cmx \ library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ pretyping/indrec.cmx tactics/hipattern.cmx library/global.cmx \ - interp/genarg.cmx pretyping/evd.cmx proofs/evar_refiner.cmx \ - kernel/environ.cmx kernel/entries.cmx library/declare.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \ - interp/constrintern.cmx proofs/clenv.cmx tactics/tactics.cmi + interp/genarg.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ + proofs/evar_refiner.cmx kernel/environ.cmx kernel/entries.cmx \ + library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \ + interp/coqlib.cmx interp/constrintern.cmx proofs/clenv.cmx \ + tactics/tactics.cmi tactics/tauto.cmo: lib/util.cmi interp/topconstr.cmi tactics/tactics.cmi \ tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ @@ -2248,7 +2254,7 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \ toplevel/vernacinterp.cmi -translate/ppconstrnew.cmo: lib/util.cmi interp/topconstr.cmi \ +translate/ppconstrnew.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi interp/syntax_def.cmi \ interp/symbols.cmi pretyping/retyping.cmi pretyping/rawterm.cmi \ pretyping/pretyping.cmi interp/ppextend.cmi lib/pp.cmi \ @@ -2257,7 +2263,7 @@ translate/ppconstrnew.cmo: lib/util.cmi interp/topconstr.cmi \ library/global.cmi interp/genarg.cmi pretyping/evd.cmi parsing/coqast.cmi \ interp/constrintern.cmi interp/constrextern.cmi lib/bignat.cmi \ parsing/ast.cmi translate/ppconstrnew.cmi -translate/ppconstrnew.cmx: lib/util.cmx interp/topconstr.cmx \ +translate/ppconstrnew.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \ pretyping/termops.cmx kernel/term.cmx interp/syntax_def.cmx \ interp/symbols.cmx pretyping/retyping.cmx pretyping/rawterm.cmx \ pretyping/pretyping.cmx interp/ppextend.cmx lib/pp.cmx \ @@ -2512,18 +2518,18 @@ contrib/extraction/extract_env.cmx: lib/util.cmx kernel/term.cmx \ contrib/extraction/extract_env.cmi contrib/extraction/extraction.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi contrib/extraction/table.cmi library/summary.cmi \ - kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \ - kernel/reduction.cmi pretyping/recordops.cmi library/nametab.cmi \ - kernel/names.cmi library/nameops.cmi contrib/extraction/mlutil.cmi \ + pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ + pretyping/recordops.cmi library/nametab.cmi kernel/names.cmi \ + library/nameops.cmi contrib/extraction/mlutil.cmi \ contrib/extraction/miniml.cmi library/libnames.cmi \ pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/evd.cmi \ kernel/environ.cmi kernel/declarations.cmi \ contrib/extraction/extraction.cmi contrib/extraction/extraction.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/term.cmx contrib/extraction/table.cmx library/summary.cmx \ - kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \ - kernel/reduction.cmx pretyping/recordops.cmx library/nametab.cmx \ - kernel/names.cmx library/nameops.cmx contrib/extraction/mlutil.cmx \ + pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \ + pretyping/recordops.cmx library/nametab.cmx kernel/names.cmx \ + library/nameops.cmx contrib/extraction/mlutil.cmx \ contrib/extraction/miniml.cmi library/libnames.cmx \ pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/evd.cmx \ kernel/environ.cmx kernel/declarations.cmx \ @@ -1,3 +1,46 @@ +Changes from V8.0pl2 to V8.0pl3 +=============================== + +Tactics + +- The search depth argument of auto can be parameterised in the + Ltac language +- Added entry constr_may_eval for tactic extensions (new syntax) + +Compilation + +- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0. + +Standard library + +- A couple of lemmas of ZArith were renamed. This concerns names + containing O (the letter), which is replaced by 0 (the number). + +Bug fixes + +- Fixes a serious bug in CoqIde. The windows port should be able + to load large libraries (such as Reals) without producing the + "bad file descriptor" error. +- Scope of Ltac variables: global Ltac macros no longer hide goal + hypotheses +- Many fixes concerning extraction: + * fewer useless eta-expansions + * for Ocaml: extraction of records should be ok now. Problem with + type t = M.t in modules fixed. + * in Haskell: improved use of unsafeCoerce, fixed Extract Constant, + function types are now printed. + * important revision of the Scheme extraction: + see http://www.pps.jussieu.fr/~letouzey/scheme +- Fixes a bug in the interpretation of record projections ("bad number + of parameters" error) +- Fixed a bug in the omega tactic +- Fixed a bug in the fold tactic regarding hypotheses ordering +- Pretty-print of universes fixed +- Added an empty level 99 in patterns syntax entry +- "Notation" bug fixes ("only parsing" bug, printing of numerals + arguments of coercions, default spacing for recursive notations + with no terminal separator, "Tactic Notation" printer). + Changes from V8.0pl1 to V8.0pl2 =============================== diff --git a/INSTALL.ide b/INSTALL.ide index d8f1208b..1c1d40c8 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -35,7 +35,7 @@ INSTALLATION 1) You need to install the OCaml stub library lablgtk2. See http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html - The first official release of lablftk2 is here: + The first official release of lablgtk2 is here: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz Note that even if its README requires ocaml > 3.07, it works ok with 3.06. If you are in a hurry just run : diff --git a/INSTALL.win b/INSTALL.win deleted file mode 100644 index f2cddb8a..00000000 --- a/INSTALL.win +++ /dev/null @@ -1,63 +0,0 @@ -***************************************************************** -* INSTALLATION PROCEDURE FOR THE COQ V8 SYSTEM UNDER WINDOWS OS * -***************************************************************** - - The binary distribution consists in a .zip archive file. This .zip contains -long filenames and cannot therefore be unpacked with pkunzip version 2. Use -either Winzip (shareware) or the Windows version of unzip (freeware): - - http://www.winzip.com/ - http://www.winimage.com/zLibDll/ - - Unzipping the distribution creates (among others) the following directories -and files: - - coq\bin\ The command-line tools - coq\lib\ The standard library files - coq\emacs A Coq mode for your Emacs - coq\man\man1 The man pages for the command-line tools - - There are two cases to consider : - -1. You unzip in the root of your drive (say C): -=============================================== - - Hence Coq will be installed in C:\coq - - You must add the C:\coq\bin path to your environment variable PATH. This is -done by adding the following line to your AUTOEXEC.BAT: - - set PATH=%PATH%;C:\coq\bin - - You may also want to specify where Coq has to look for your configuration -file .coqrc (not mandatory), e.g.: - - set HOME=C:\My_Documents\Coq - -2. You unzip in some other place (say D:\My_Dir): -================================================= - - You must add the D:\My_Dir\coq\bin path to your environment variable PATH. -This is done by adding the following line to AUTOEXEC.BAT: - - set PATH=%PATH%;D:\My_Dir\coq\bin - - You must also set the environment variables COQBIN and COQLIB to tell Coq -that binaries and libraries are not in the default place. This is done by -adding the following lines to your AUTOEXEC.BAT: - - set COQBIN=D:\My_Dir\coq\bin - set COQLIB=D:\My_Dir\coq\lib - - You may also want to specify where Coq has to look for your configuration -file .coqrc (not mandatory), e.g.: - - set HOME=C:\My_Documents\Coq - -PROBLEMS: -========= - - If you have any trouble with this installation, please contact: -coq-bugs@pauillac.inria.fr. - - The Coq Team. @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ######################################################################## -# $Id: Makefile,v 1.459.2.13 2005/01/21 17:15:12 herbelin Exp $ +# $Id: Makefile,v 1.459.2.22 2006/01/11 23:18:05 barras Exp $ # Makefile for Coq @@ -80,7 +80,7 @@ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep -DEPFLAGS=$(LOCALINCLUDES) +DEPFLAGS=-slash $(LOCALINCLUDES) OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) @@ -331,7 +331,7 @@ $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ + $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(COQTOP): cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -375,10 +375,6 @@ $(COQC): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) clean:: rm -f scripts/tolink.ml -archclean:: - rm -f $(COQTOPBYTE) $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) - rm -f $(COQTOP) - # we provide targets for each subdirectory lib: $(LIBREP) @@ -534,7 +530,7 @@ COQIDEVO=ide/utf8.vo $(COQIDEVO): states/initial.coq $(BOOTCOQTOP) -compile $* -IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc +IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.ico ide/coq2.ico ide/.coqide-gtk2rc coqide-binaries: coqide-$(HASCOQIDE) coqide-no: @@ -555,35 +551,40 @@ $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide/ide.cmxa $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ + $(HIDE)$(COQMKTOP) -ide -top $(BYTEFLAGS) -o $@ $(COQIDE): cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) ide/%.cmo: ide/%.ml $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< ide/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< -ide/utils/%.cmo: ide/%.ml +ide/utils/%.cmo: ide/utils/%.ml $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< -ide/utils/%.cmi: ide/%.mli +ide/utils/%.cmi: ide/utils/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< -ide/utils/%.cmx: ide/%.ml +ide/utils/%.cmx: ide/utils/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< +# Special target to select between whether lablgtk >= 2.6.0 or not +ide/undo.cmi: ide/undo.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(CAMLP4COMPAT) -intf" -c -intf $< + clean:: rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml @@ -693,8 +694,6 @@ contrib7/interface/Centaur.vo: contrib7/interface/Centaur.v $(INTERFACE) contrib7/interface/AddDad.vo: contrib7/interface/AddDad.v $(INTERFACE) states7/initial.coq $(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $* -clean:: - rm -f bin/parser$(EXE) bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) # install targets install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages @@ -1104,9 +1103,6 @@ clean:: rm -f tools/coqwc.ml rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml -archclean:: - rm -f $(TOOLS) - ########################################################################### # minicoq ########################################################################### @@ -1121,22 +1117,19 @@ $(MINICOQ): $(MINICOQCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) -archclean:: - rm -f $(MINICOQ) - ########################################################################### # Installation ########################################################################### -COQINSTALLPREFIX= - # Can be changed for a local installation (to make packages). - # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). +#COQINSTALLPREFIX= +# Can be changed for a local installation (to make packages). +# You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). -FULLBINDIR=$(COQINSTALLPREFIX)$(BINDIR) -FULLCOQLIB=$(COQINSTALLPREFIX)$(COQLIB) -FULLMANDIR=$(COQINSTALLPREFIX)$(MANDIR) -FULLEMACSLIB=$(COQINSTALLPREFIX)$(EMACSLIB) -FULLCOQDOCDIR=$(COQINSTALLPREFIX)$(COQDOCDIR) +FULLBINDIR=$(BINDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) +FULLCOQLIB=$(COQLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) +FULLMANDIR=$(MANDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) +FULLEMACSLIB=$(EMACSLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) +FULLCOQDOCDIR=$(COQDOCDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) install-coq: install-binaries install-library install-coq-info install-coq8: install-binaries install-library8 install-coq-info @@ -1222,7 +1215,7 @@ install-emacs: install-latex: $(MKDIR) $(FULLCOQDOCDIR) - cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) + cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) ########################################################################### @@ -1453,11 +1446,11 @@ ML4FILES += lib/pp.ml4 \ .ml4.cmx: $(SHOW)'OCAMLOPT4 $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< .ml4.cmo: $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< #.v.vo: # $(BOOTCOQTOP) -compile $* @@ -1473,6 +1466,7 @@ ML4FILES += lib/pp.ml4 \ ########################################################################### archclean:: + -rm -f bin/* rm -f config/*.cmx* config/*.[soa] rm -f lib/*.cmx* lib/*.[soa] rm -f kernel/*.cmx* kernel/*.[soa] @@ -6,7 +6,26 @@ THE COQ V8.0 SYSTEM INSTALLATION. ============= - See the file INSTALL.win for installation procedure. + The windows distribution of Coq consists of an installer that should + perform all installation steps. CoqIde (a GTK interface to Coq) can + be installed. In case the GTK runtime libraries are not installed, + the Coq installer can be set to make a copy of those libraries + within the directory of Coq. + However, if the files are installed but Coq does not work properly, + some steps can be made manually. + Let us assume that the installation dir was c:\coq. The following + environment variables must be set as: + set COQBIN=c:\coq\bin + set COQLIB=c:\coq\lib + On win9x systems, this is achieved by inserting the 2 lines above + in the autoexec.bat file of the system. On other windows systems, + environment variables can be configured via the System application + of the Control Panel. Then select the Advanced tab. + The .bat files in c:\coq should now launch Coq (or CoqIde). + The COQBIN path can also be added to the PATH. This might be a + bad idea if the GTK libraries of Coq's installer were installed + since they might conflict with already installed GTK libraries. + COMPILATION. ============ @@ -15,12 +34,10 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml version 3.06 or later, Visual C++ (needed - for the -custom option of ocaml) and MASM (needed if you want - to produce a native version). + 1- Install ocaml version 3.06 or later (mingw port preferably). 2- Install a complete set of Unix utilities (used by Makefiles). - See: http://sources.redhat.com/cygwin/. + See: http://www.cygwin.com/. 3- Under cygwin, type successively diff --git a/config/Makefile.template b/config/Makefile.template index cd49db89..e75b8bd0 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -24,25 +24,26 @@ LOCAL=LOCALINSTALLATION # LIBDIR=path where the Coq library will reside # MANDIR=path where to install manual pages # EMACSDIR=path where to put Coq's Emacs mode (coq.el) -BINDIR="BINDIRDIRECTORY" -COQLIB="COQLIBDIRECTORY" -MANDIR="MANDIRDIRECTORY" -EMACSLIB="EMACSLIBDIRECTORY" +BINDIR='BINDIRDIRECTORY' +COQLIB='COQLIBDIRECTORY' +MANDIR='MANDIRDIRECTORY' +EMACSLIB='EMACSLIBDIRECTORY' EMACS=EMACSCOMMAND # Path to Coq distribution -COQTOP=COQTOPDIRECTORY +COQTOP='COQTOPDIRECTORY' VERSION=COQVERSION # Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH -CAMLP4BIN=CAMLP4BINDIRECTORY +CAMLP4BIN='CAMLP4BINDIRECTORY' # Ocaml version number CAMLVERSION=CAMLTAG # Camlp4 library directory (avoid CAMLP4LIB used on Windows) CAMLP4O=CAMLP4TOOL -MYCAMLP4LIB=CAMLP4LIBDIRECTORY +CAMLP4COMPAT=CAMLP4COMPATFLAGS +MYCAMLP4LIB='CAMLP4LIBDIRECTORY' # Objective-Caml compile command OCAMLC=BYTECAMLC @@ -86,7 +87,7 @@ EXE=EXECUTEEXTENSION MKDIR=mkdir -p # where to put the coqdoc.sty style file -COQDOCDIR=COQDOCDIRECTORY +COQDOCDIR='COQDOCDIRECTORY' # command to update TeX' kpathsea database #MKTEXLSR=MKTEXLSRCOMMAND diff --git a/config/coq_config.mli b/config/coq_config.mli index 1d88358a..4b780b1f 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq_config.mli,v 1.9.16.1 2004/07/16 19:29:58 herbelin Exp $ i*) +(*i $Id: coq_config.mli,v 1.9.16.2 2006/01/10 17:06:23 barras Exp $ i*) val local : bool (* local use (no installation) *) @@ -26,7 +26,6 @@ val osdeplibs : string (* OS dependant link options for ocamlc *) (* val defined : string list (* options for lib/ocamlpp *) *) val version : string (* version number of Coq *) -val versionsi : string (* version number of Coq\_SearchIsos *) val date : string (* release date *) val compile_date : string (* compile date *) @@ -6,8 +6,8 @@ # ################################## -VERSION=8.0pl2 -DATE="Jan 2005" +VERSION=8.0pl3 +DATE="Jan 2006" # a local which command for sh which () { @@ -30,66 +30,50 @@ coq_profile_flag= best_compiler=opt local=false +src_spec=no +prefix_spec=no bindir_spec=no libdir_spec=no mandir_spec=no emacslib_spec=no -emacs_spec=no +#emacs_spec=no coqdocdir_spec=no reals_opt=no reals=all arch_spec=no coqide_spec=no -COQTOP=`pwd` - - # Parse command-line arguments while : ; do case "$1" in "") break;; - -prefix|--prefix) bindir_spec=yes - bindir=$2/bin - libdir_spec=yes - libdir=$2/lib/coq - mandir_spec=yes - mandir=$2/man - coqdocdir_spec=yes - coqdocdir=$2/share/texmf/tex/latex/misc + -prefix|--prefix) prefix_spec=yes + prefix="$2" shift;; -local|--local) local=true - bindir_spec=yes - bindir=$COQTOP/bin - libdir_spec=yes - libdir=$COQTOP - mandir_spec=yes - mandir=$COQTOP/man - emacslib_spec=yes - emacslib=$COQTOP/tools/emacs - coqdocdir_spec=yes - coqdocdir=$COQTOP/tools/coqdoc reals_opt=yes reals=all;; - -src|--src) COQTOP=$2 + -src|--src) src_spec=yes + COQTOP="$2" shift;; -bindir|--bindir) bindir_spec=yes - bindir=$2 + bindir="$2" shift;; -libdir|--libdir) libdir_spec=yes - libdir=$2 + libdir="$2" shift;; -mandir|--mandir) mandir_spec=yes mandir=$2 shift;; -emacslib|--emacslib) emacslib_spec=yes - emacslib=$2 + emacslib="$2" shift;; - -emacs |--emacs) emacs_spec=yes - emacs=$2 - shift;; +# -emacs |--emacs) emacs_spec=yes +# emacs="$2" +# shift;; -coqdocdir|--coqdocdir) coqdocdir_spec=yes - coqdocdir=$2 + coqdocdir="$2" shift;; -arch|--arch) arch_spec=yes arch=$2 @@ -111,6 +95,11 @@ while : ; do shift done +if [ $prefix_spec = yes -a $local = true ] ; then + echo "Options -prefix and -local are incompatible" + echo "Configure script failed!" + exit 1 +fi # compile date DATEPGM=`which date` @@ -146,125 +135,28 @@ case $arch_spec in yes) ARCH=$arch esac -# bindir, libdir, mandir, etc. - -case $ARCH in - win32) - bindir_def=C:\\coq\\bin - libdir_def=C:\\coq\\lib - mandir_def=C:\\coq\\man - emacslib_def=C:\\coq\\emacs;; - *) - bindir_def=/usr/local/bin - libdir_def=/usr/local/lib/coq - mandir_def=/usr/local/man - emacslib_def=/usr/share/emacs/site-lisp - coqdocdir_def=/usr/share/texmf/tex/latex/misc;; -esac - -emacs_def=emacs - -case $bindir_spec in - no) echo "Where should I install the Coq binaries [$bindir_def] ?" - read BINDIR - - case $BINDIR in - "") BINDIR=$bindir_def;; - *) true;; - esac;; - yes) BINDIR=$bindir;; -esac - -case $libdir_spec in - no) echo "Where should I install the Coq library [$libdir_def] ?" - read LIBDIR - - case $LIBDIR in - "") LIBDIR=$libdir_def;; - *) true;; - esac;; - yes) LIBDIR=$libdir;; -esac - -case $mandir_spec in - no) echo "Where should I install the Coq man pages [$mandir_def] ?" - read MANDIR - - case $MANDIR in - "") MANDIR=$mandir_def;; - *) true;; - esac;; - yes) MANDIR=$mandir;; -esac - -case $emacslib_spec in - no) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?" - read EMACSLIB - - case $EMACSLIB in - "") EMACSLIB=$emacslib_def;; - *) true;; - esac;; - yes) EMACSLIB=$emacslib;; -esac - -case $coqdocdir_spec in - no) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?" - read COQDOCDIR - - case $COQDOCDIR in - "") COQDOCDIR=$coqdocdir_def;; - *) true;; - esac;; - yes) COQDOCDIR=$coqdocdir;; -esac - -case $reals_opt in - no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?" - read reals_ans - - case $reals_ans in - "N"|"n"|"No"|"NO"|"no") - reals=basic;; - *) reals=all;; - esac;; - yes) true;; -esac - -# case $emacs_spec in -# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" -# read EMACS - -# case $EMACS in -# "") EMACS=$emacs_def;; -# *) true;; -# esac;; -# yes) EMACS=$emacs;; -# esac - -# OS dependent libraries +# executable extension case $ARCH in - sun4*) OS=`uname -r` - case $OS in - 5*) OS="Sun Solaris $OS" - OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";; - *) OS="Sun OS $OS" - OSDEPLIBS="-cclib -lunix" - esac;; - alpha) OSDEPLIBS="-cclib -lunix";; - win32) OS="Win32" - OSDEPLIBS="-cclib -lunix";; - *) OSDEPLIBS="-cclib -lunix" + win32) EXE=".exe";; + *) EXE="" esac -# executable extension +# strip command case $ARCH in - win32) EXE=".exe";; - *) EXE="" + win32) + # true -> strip : it exists under cygwin ! + STRIPCOMMAND="strip";; + *) + if [ "$coq_profile_flag" = "-p" ] ; then + STRIPCOMMAND="true" + else + STRIPCOMMAND="strip" + fi esac +######################################### # Objective Caml programs CAMLC=`which $bytecamlc` @@ -293,16 +185,25 @@ CAMLBIN=`dirname "$CAMLC"` CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0) echo "Your version of Objective-Caml is $CAMLVERSION." - echo "You need Objective-Caml 3.06 or later !" + if [ "$CAMLVERSION" = "3.08.0" ] ; then + echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!" + else + echo "You need Objective-Caml 3.06 or later!"; + fi + echo "Configuration script failed!" + exit 1;; + 3.06|3.07*|3.08*) + echo "You have Objective-Caml $CAMLVERSION. Good!";; + ?*) + CAMLP4COMPAT="-loc loc" + echo "You have Objective-Caml $CAMLVERSION. Good!";; + *) + echo "I found the Objective-Caml compiler but cannot find its version number!" + echo "Is it installed properly ?" echo "Configuration script failed!" exit 1;; - ?*) echo "You have Objective-Caml $CAMLVERSION. Good!";; - *) echo "I found the Objective-Caml compiler but cannot find its version number!" - echo "Is it installed properly ?" - echo "Configuration script failed!" - exit 1;; esac CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` @@ -323,20 +224,28 @@ fi # For coqmktop -#CAMLLIB=`"$CAMLC" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' ` CAMLLIB=`"$CAMLC" -where` # Camlp4 (greatly simplified since merged with ocaml) CAMLP4BIN=${CAMLBIN} +CAMLP4LIB=+camlp4 -#case $OS in -# Win32) - CAMLP4LIB=+camlp4 -# ;; -# *) -# CAMLP4LIB=${CAMLLIB}/camlp4 -#esac +# OS dependent libraries + +case $ARCH in + sun4*) OS=`uname -r` + case $OS in + 5*) OS="Sun Solaris $OS" + OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";; + *) OS="Sun OS $OS" + OSDEPLIBS="-cclib -lunix" + esac;; + alpha) OSDEPLIBS="-cclib -lunix";; + win32) OS="Win32" + OSDEPLIBS="-cclib -lunix";; + *) OSDEPLIBS="-cclib -lunix" +esac # lablgtk2 and CoqIDE @@ -349,7 +258,7 @@ if test -x "${CAMLLIB}/lablgtk2" ; then else echo "LablGtk2 found, no native threads: bytecode CoqIde will be available" COQIDE=byte - fi; + fi else echo "LablGtk2 found but too old: CoqIde will not be available" COQIDE=no; @@ -360,30 +269,154 @@ else fi fi +if [ $COQIDE != no ] ; then + if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then + LABLGTKGE26=yes; + else + LABLGTKGE26=no + fi +fi + # Tell on windows if ocaml understands cygwin or windows path formats #"$CAMLC" -o config/giveostype config/giveostype.ml #CAMLOSTYPE=`config/giveostype` #rm config/giveostype -case $ARCH in - win32) - # true -> strip : it exists under cygwin ! - STRIPCOMMAND="strip";; - *) - if [ "$coq_profile_flag" = "-p" ] ; then - STRIPCOMMAND="true" - else - STRIPCOMMAND="strip" - fi -esac - +###################################### # mktexlsr + #MKTEXLSR=`which mktexlsr` #case $MKTEXLSR in # "") MKTEXLSR=true;; #esac +########################################### +# bindir, libdir, mandir, etc. + +canonical_pwd () { +ocaml 2>&1 1>/dev/null <<EOF + prerr_endline(Sys.getcwd());; +EOF +} + +case $src_spec in + no) COQTOP=`canonical_pwd` +esac + +case $ARCH in + win32) + bindir_def='C:\coq\bin' + libdir_def='C:\coq\lib' + mandir_def='C:\coq\man' + emacslib_def='C:\coq\emacs' + coqdocdir_def='C:\coq\latex';; + *) + bindir_def=/usr/local/bin + libdir_def=/usr/local/lib/coq + mandir_def=/usr/local/man + emacslib_def=/usr/share/emacs/site-lisp + coqdocdir_def=/usr/share/texmf/tex/latex/misc;; +esac + +emacs_def=emacs + +case $bindir_spec/$prefix_spec/$local in + yes/*/*) BINDIR=$bindir ;; + */yes/*) BINDIR=$prefix/bin ;; + */*/true) BINDIR=$COQTOP/bin ;; + *) echo "Where should I install the Coq binaries [$bindir_def] ?" + read BINDIR + case $BINDIR in + "") BINDIR=$bindir_def;; + *) true;; + esac;; +esac + +case $libdir_spec/$prefix_spec/$local in + yes/*/*) LIBDIR=$libdir;; + */yes/*) + case $ARCH in + win32) LIBDIR=$prefix ;; + *) LIBDIR=$prefix/lib/coq ;; + esac ;; + */*/true) LIBDIR=$COQTOP ;; + *) echo "Where should I install the Coq library [$libdir_def] ?" + read LIBDIR + case $LIBDIR in + "") LIBDIR=$libdir_def;; + *) true;; + esac;; +esac + +case $mandir_spec/$prefix_spec/$local in + yes/*/*) MANDIR=$mandir;; + */yes/*) MANDIR=$prefix/man ;; + */*/true) MANDIR=$COQTOP/man ;; + *) echo "Where should I install the Coq man pages [$mandir_def] ?" + read MANDIR + case $MANDIR in + "") MANDIR=$mandir_def;; + *) true;; + esac;; +esac + +case $emacslib_spec/$prefix_spec/$local in + yes/*/*) EMACSLIB=$emacslib;; + */yes/*) + case $ARCH in + win32) EMACSLIB=$prefix/emacs ;; + *) EMACSLIB=$prefix/share/emacs/site-lisp ;; + esac ;; + */*/true) EMACSLIB=$COQTOP/tools/emacs ;; + *) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?" + read EMACSLIB + case $EMACSLIB in + "") EMACSLIB=$emacslib_def;; + *) true;; + esac;; +esac + +case $coqdocdir_spec/$prefix_spec/$local in + yes/*/*) COQDOCDIR=$coqdocdir;; + */yes/*) + case $ARCH in + win32) COQDOCDIR=$prefix/latex ;; + *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; + esac ;; + */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; + *) echo "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def] ?" + read COQDOCDIR + case $COQDOCDIR in + "") COQDOCDIR=$coqdocdir_def;; + *) true;; + esac;; +esac + +case $reals_opt in + no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?" + read reals_ans + + case $reals_ans in + "N"|"n"|"No"|"NO"|"no") + reals=basic;; + *) reals=all;; + esac;; + yes) true;; +esac + +# case $emacs_spec in +# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" +# read EMACS + +# case $EMACS in +# "") EMACS=$emacs_def;; +# *) true;; +# esac;; +# yes) EMACS=$emacs;; +# esac + +########################################### # Summary of the configuration echo "" @@ -416,16 +449,19 @@ echo "" # Building the $COQTOP/config/coq_config.ml file ##################################################### -# damned backslashes under M$Windows -case $ARCH in - win32) - CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` - BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` - MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` - EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` - ;; -esac +# An escaped version of a variable +escape_var () { +ocaml 2>&1 1>/dev/null <<EOF + prerr_endline(String.escaped(Sys.getenv"$VAR"));; +EOF +} + +export COQTOP BINDIR LIBDIR CAMLLIB +ESCCOQTOP="`VAR=COQTOP escape_var`" +ESCBINDIR="`VAR=BINDIR escape_var`" +ESCLIBDIR="`VAR=LIBDIR escape_var`" +ESCCAMLLIB="`VAR=CAMLLIB escape_var`" +ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4 mlconfig_file=$COQTOP/config/coq_config.ml rm -f $mlconfig_file @@ -433,16 +469,15 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) let local = $local -let bindir = "$BINDIR" -let coqlib = "$LIBDIR" -let coqtop = "$COQTOP" -let camllib = "$CAMLLIB" -let camlp4lib = "$CAMLP4LIB" +let bindir = "$ESCBINDIR" +let coqlib = "$ESCLIBDIR" +let coqtop = "$ESCCOQTOP" +let camllib = "$ESCCAMLLIB" +let camlp4lib = "$ESCCAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" let osdeplibs = "$OSDEPLIBS" let version = "$VERSION" -let versionsi = "$VERSIONSI" let date = "$DATE" let compile_date = "$COMPILEDATE" let exec_extension = "$EXE" @@ -474,34 +509,45 @@ chmod a-w $mlconfig_file rm -f $COQTOP/config/Makefile -# damned backslashes under M$Windows (bis) +# damned backslashes under M$Windows case $ARCH in win32) - BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` - MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` - EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` + ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` + ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` + ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` ;; + *) + ESCCOQTOP="$COQTOP" + ESCBINDIR="$BINDIR" + ESCLIBDIR="$LIBDIR" + ESCMANDIR="$MANDIR" + ESCEMACSLIB="$EMACSLIB" + ESCCOQDOCDIR="$COQDOCDIR" + ESCCAMLP4BIN="$CAMLP4BIN" ;; esac sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|COQTOPDIRECTORY|$COQTOP|" \ + -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \ -e "s|COQVERSION|$VERSION|" \ - -e "s|BINDIRDIRECTORY|$BINDIR|" \ - -e "s|COQLIBDIRECTORY|$LIBDIR|" \ - -e "s|MANDIRDIRECTORY|$MANDIR|" \ - -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ + -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ + -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ + -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \ + -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \ -e "s|EMACSCOMMAND|$EMACS|" \ - -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \ + -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \ -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \ -e "s|ARCHITECTURE|$ARCH|" \ -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \ -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ - -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \ -e "s|CAMLTAG|$CAMLTAG|" \ - -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ + -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ -e "s|CAMLP4TOOL|$camlp4o|" \ + -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ -e "s|BESTCOMPILER|$best_compiler|" \ @@ -521,22 +567,31 @@ chmod a-w $COQTOP/config/Makefile if test "$coq_debug_flag" = "-g" ; then rm -f $COQTOP/dev/ocamldebug-v7 - if [ "$CAMLP4LIB" = "+camlp4" ] ; then - CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4 - else - CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB - fi sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \ + -e "s|CAMLP4LIBDIRECTORY|$CAMLLIB/camlp4|" \ $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7 chmod a-w,a+x $COQTOP/dev/ocamldebug-v7 fi +################################################## +# Fixing lablgtk types +#################################################### + +if [ "$LABLGTKGE26" = "yes" ] ; then + cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli; +else + cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli +fi + +################################################## +# The end +#################################################### + echo "If anything in the above is wrong, please restart './configure'" echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure,v 1.74.2.7 2005/01/21 17:27:32 herbelin Exp $ +# $Id: configure,v 1.74.2.19 2006/01/13 11:50:07 barras Exp $ diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 53a2631e..8e441613 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml,v 1.51.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*) open Pp open Util @@ -269,11 +269,18 @@ module StdParams = struct (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *) + let unquote s = + if lang () <> Scheme then s + else + let s = String.copy s in + for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; + s + let rec dottify = function | [] -> assert false - | [s] -> s - | s::[""] -> s - | s::l -> (dottify l)^"."^s + | [s] -> unquote s + | s::[""] -> unquote s + | s::l -> (dottify l)^"."^(unquote s) let pp_global mpl r = let ls = get_renamings r in @@ -353,7 +360,7 @@ let preamble prm = match lang () with | Ocaml -> Ocaml.preamble prm | Haskell -> Haskell.preamble prm | Scheme -> Scheme.preamble prm - | Toplevel -> (fun _ _ -> mt ()) + | Toplevel -> (fun _ _ _ -> mt ()) let preamble_sig prm = match lang () with | Ocaml -> Ocaml.preamble_sig prm @@ -374,7 +381,6 @@ let info f = (str ("The file "^f^" has been created by extraction.")) let print_structure_to_file f prm struc = - cons_cofix := Refset.empty; Hashtbl.clear renamings; mod_1st_level := Idmap.empty; modcontents := Gset.empty; @@ -387,9 +393,13 @@ let print_structure_to_file f prm struc = else (create_mono_renamings struc; []) in let print_dummys = - (struct_ast_search MLdummy struc, + (struct_ast_search ((=) MLdummy) struc, struct_type_search Tdummy struc, struct_type_search Tunknown struc) + in + let print_magic = + if lang () <> Haskell then false + else struct_ast_search (function MLmagic _ -> true | _ -> false) struc in (* print the implementation *) let cout = option_app (fun (f,_) -> open_out f) f in @@ -397,7 +407,7 @@ let print_structure_to_file f prm struc = | None -> !Pp_control.std_ft | Some cout -> Pp_control.with_output_to cout in begin try - msg_with ft (preamble prm used_modules print_dummys); + msg_with ft (preamble prm used_modules print_dummys print_magic); msg_with ft (pp_struct struc); option_iter close_out cout; with e -> diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 46bf06dd..6bfe861f 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml,v 1.136.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*) (*i*) open Util @@ -183,15 +183,17 @@ let rec extract_type env db j c args = | (Info, Default) -> (* Standard case: two [extract_type] ... *) let mld = extract_type env' (0::db) j d [] in - if mld = Tdummy then Tdummy + if type_eq (mlt_env env) mld Tdummy then Tdummy else Tarr (extract_type env db 0 t [], mld) | (Info, TypeScheme) when j > 0 -> (* A new type var. *) let mld = extract_type env' (j::db) (j+1) d [] in - if mld = Tdummy then Tdummy else Tarr (Tdummy, mld) + if type_eq (mlt_env env) mld Tdummy then Tdummy + else Tarr (Tdummy, mld) | _ -> let mld = extract_type env' (0::db) j d [] in - if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)) + if type_eq (mlt_env env) mld Tdummy then Tdummy + else Tarr (Tdummy, mld)) | Sort _ -> Tdummy (* The two logical cases. *) | _ when sort_of env (applist (c, args)) = InProp -> Tdummy | Rel n -> @@ -343,38 +345,53 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if List.length l = 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if l = [] then raise (I Standard); + if not mib.mind_record then raise (I Standard); let ip = (kn, 0) in - if is_custom (IndRef ip) then raise (I Standard); - let projs = - try (find_structure ip).s_PROJ - with Not_found -> raise (I Standard); + let r = IndRef ip in + if is_custom r then raise (I Standard); + (* Now we're sure it's a record. *) + (* First, we find its field names. *) + let rec names_prod t = match kind_of_term t with + | Prod(n,_,t) -> n::(names_prod t) + | LetIn(_,_,_,t) -> names_prod t + | Cast(t,_) -> names_prod t + | _ -> [] in - let n = nb_default_params env mip0.mind_nf_arity in - let projs = try List.map out_some projs with _ -> raise (I Standard) in - let is_true_proj kn = - let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in - match kind_of_term body with - | Rel _ -> false - | Case _ -> true - | _ -> assert false + let field_names = + list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + assert (List.length field_names = List.length typ); + let projs = ref KNset.empty in + let mp,d,_ = repr_kn kn in + let rec select_fields l typs = match l,typs with + | [],[] -> [] + | (Name id)::l, typ::typs -> + if type_eq (mlt_env env) Tdummy typ then select_fields l typs + else + let knp = make_kn mp d (label_of_id id) in + if not (List.mem false (type_to_sign (mlt_env env) typ)) then + projs := KNset.add knp !projs; + (ConstRef knp) :: (select_fields l typs) + | Anonymous::l, typ::typs -> + if type_eq (mlt_env env) Tdummy typ then select_fields l typs + else error_record r + | _ -> assert false in - let projs = List.filter is_true_proj projs in - let rec check = function - | [] -> [],[] - | (typ, kn) :: l -> - let l1,l2 = check l in - if type_eq (mlt_env env) Tdummy typ then l1,l2 - else - let r = ConstRef kn in - if List.mem false (type_to_sign (mlt_env env) typ) - then r :: l1, l2 - else r :: l1, r :: l2 - in - add_record kn n (check (List.combine typ projs)); - raise (I Record) + let field_glob = select_fields field_names typ + in + (* Is this record officially declared with its projections ? *) + (* If so, we use this information. *) + begin try + let n = nb_default_params env mip0.mind_nf_arity in + List.iter + (option_iter + (fun kn -> if KNset.mem kn !projs then add_projection n kn)) + (find_structure ip).s_PROJ + with Not_found -> () + end; + Record field_glob with (I info) -> info in - let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in + let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in add_ind kn i; internal_call := KNset.remove kn !internal_call; i @@ -564,7 +581,9 @@ and extract_cst_app env mle mlt kn args = (* Different situations depending of the number of arguments: *) if ls = 0 then put_magic_if magic2 head else if List.mem true s then - if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla)) + if la >= ls || not (List.mem false s) + then + put_magic_if (magic2 && not magic1) (MLapp (head, mla)) else (* Not enough arguments. We complete via eta-expansion. *) let ls' = ls-la in @@ -599,7 +618,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) - let s = List.map ((<>) Tdummy) types in + let s = List.map (type_neq env Tdummy) types in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -614,7 +633,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let head mla = if mi.ind_info = Singleton then put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *) - else put_magic_if magic1 (MLcons (ConstructRef cp, mla)) + else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -670,10 +689,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* The types of the arguments of the corresponding constructor. *) let f t = type_subst_vect metas (type_expand env t) in let l = List.map f oi.ip_types.(i) in + (* the corresponding signature *) + let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in (* Extraction of the branch (in functional form). *) let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) - let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in + let ids,e = case_expunge s e in (ConstructRef (ip,i+1), List.rev ids, e) in if mi.ind_info = Singleton then @@ -687,7 +708,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else (* Standard case: we apply [extract_branch]. *) - MLcase (a, Array.init br_size extract_branch) + MLcase (mi.ind_info, a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) @@ -726,7 +747,7 @@ let extract_std_constant env kn body typ = (* The real type [t']: without head lambdas, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,t' = type_decomp (type_expand env (var2var' t)) in - let s = List.map ((<>) Tdummy) l in + let s = List.map (type_neq env Tdummy) l in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in (* Decomposing the top level lambdas of [body]. *) @@ -836,7 +857,8 @@ let logical_decl = function | Dterm (_,MLdummy,Tdummy) -> true | Dtype (_,[],Tdummy) -> true | Dfix (_,av,tv) -> - (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv) + (array_for_all ((=) MLdummy) av) && + (array_for_all ((=) Tdummy) tv) | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 29c8cd18..3834fe81 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml,v 1.40.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*) (*s Production of Haskell syntax. *) @@ -27,23 +27,41 @@ let keywords = [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; - "as"; "qualified"; "hiding" ; "unit" ] + "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] Idset.empty -let preamble prm used_modules (mldummy,tdummy,tunknown) = +let preamble prm used_modules (mldummy,tdummy,tunknown) magic = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false in + (if not magic then mt () + else + str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++ + str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n") + ++ str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () ++ fnl() ++ str "import qualified Prelude" ++ fnl() ++ prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules ++ fnl () ++ - (if mldummy then + (if not magic then mt () + else str "\ +#ifdef __GLASGOW_HASKELL__ +import qualified GHC.Base +unsafeCoerce = GHC.Base.unsafeCoerce# +#else +-- HUGS +import qualified IOExts +unsafeCoerce = IOExts.unsafeCoerce +#endif") + ++ + fnl() ++ fnl() + ++ + (if not mldummy then mt () + else str "__ = Prelude.error \"Logical or arity value used\"" - ++ fnl () ++ fnl() - else mt()) + ++ fnl () ++ fnl()) let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" @@ -61,27 +79,36 @@ module Make = functor(P : Mlpp_param) -> struct let local_mpl = ref ([] : module_path list) -let pp_global r = P.pp_global !local_mpl r +let pp_global r = + if is_inline_custom r then str (find_custom r) + else P.pp_global !local_mpl r + let empty_env () = [], P.globals() (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) +let kn_sig = + let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in + make_kn specif empty_dirpath (mk_label "sig") + let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global r | Tglob (r,l) -> - pp_par par - (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) + if r = IndRef (kn_sig,0) then + pp_type true vl (List.hd l) + else + pp_par par + (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy -> str "()" | Tunknown -> str "()" | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" - | Tcustom s -> str s in hov 0 (pp_rec par t) @@ -125,16 +152,16 @@ let rec pp_expr par env args = spc () ++ hov 0 pp_a2))) | MLglob r -> apply (pp_global r) - | MLcons (r,[]) -> + | MLcons (_,r,[]) -> assert (args=[]); pp_global r - | MLcons (r,[a]) -> + | MLcons (_,r,[a]) -> assert (args=[]); pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a) - | MLcons (r,args') -> + | MLcons (_,r,args') -> assert (args=[]); pp_par par (pp_global r ++ spc () ++ prlist_with_sep spc (pp_expr true env []) args') - | MLcase (t, pv) -> + | MLcase (_,t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ fnl () ++ str " " ++ pp_pat env pv))) @@ -146,7 +173,8 @@ let rec pp_expr par env args = pp_par par (str "Prelude.error" ++ spc () ++ qs s) | MLdummy -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) - | MLmagic a -> pp_expr par env args a + | MLmagic a -> + pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") and pp_pat env pv = @@ -210,7 +238,7 @@ let pp_one_ind ip pl cv = | [] -> (mt ()) | _ -> (str " " ++ prlist_with_sep - (fun () -> (str " ")) (pp_type true (List.rev pl)) l)) + (fun () -> (str " ")) (pp_type true pl) l)) in str (if cv = [||] then "type " else "data ") ++ pp_global (IndRef ip) ++ str " " ++ @@ -239,6 +267,8 @@ let rec pp_ind first kn i ind = (*s Pretty-printing of a declaration. *) +let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") + let pp_decl mpl = local_mpl := mpl; function @@ -248,21 +278,32 @@ let pp_decl mpl = | Dtype (r, l, t) -> if is_inline_custom r then mt () else - let l = rename_tvars keywords l in - let l' = List.rev l in - hov 2 (str "type " ++ pp_global r ++ spc () ++ - prlist (fun id -> pr_id id ++ str " ") l ++ - str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl () + let l = rename_tvars keywords l in + let st = + try + let ids,s = find_type_custom r in + prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s + with not_found -> + prlist (fun id -> pr_id id ++ str " ") l ++ + if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n" + else str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl () | Dfix (rv, defs,_) -> let ppv = Array.map pp_global rv in prlist_with_sep (fun () -> fnl () ++ fnl ()) (fun (pi,ti) -> pp_function (empty_env ()) pi ti) (List.combine (Array.to_list ppv) (Array.to_list defs)) ++ fnl () ++ fnl () - | Dterm (r, a, _) -> + | Dterm (r, a, t) -> if is_inline_custom r then mt () else - hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ()) + let e = pp_global r in + e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ + if is_custom r then + hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ()) + else + hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ()) let pp_structure_elem mpl = function | (l,SEdecl d) -> pp_decl mpl d diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 4da5db0c..822444bd 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.mli,v 1.15.6.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) open Pp open Names @@ -15,6 +15,6 @@ open Miniml val keywords : Idset.t val preamble : - extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds + extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 866ff847..7c18f9f5 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli,v 1.46.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -35,7 +35,6 @@ type ml_type = | Tdummy | Tunknown | Taxiom - | Tcustom of string and ml_meta = { id : int; mutable contents : ml_type option } @@ -46,7 +45,11 @@ type ml_schema = int * ml_type (*s ML inductive types. *) -type inductive_info = Record | Singleton | Coinductive | Standard +type inductive_info = + | Singleton + | Coinductive + | Standard + | Record of global_reference list (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -79,8 +82,9 @@ type ml_ast = | MLlam of identifier * ml_ast | MLletin of identifier * ml_ast * ml_ast | MLglob of global_reference - | MLcons of global_reference * ml_ast list - | MLcase of ml_ast * (global_reference * identifier list * ml_ast) array + | MLcons of inductive_info * global_reference * ml_ast list + | MLcase of inductive_info * ml_ast * + (global_reference * identifier list * ml_ast) array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index fbe423a7..c01766b0 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml,v 1.104.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*) (*i*) open Pp @@ -117,9 +117,9 @@ let rec mgu = function let needs_magic p = try mgu p; false with Impossible -> true -let put_magic_if b a = if b then MLmagic a else a +let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a -let put_magic p a = if needs_magic p then MLmagic a else a +let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a (*S ML type env. *) @@ -327,11 +327,11 @@ let ast_iter_rel f = | MLrel i -> f (i-n) | MLlam (_,a) -> iter (n+1) a | MLletin (_,a,b) -> iter n a; iter (n+1) b - | MLcase (a,v) -> + | MLcase (_,a,v) -> iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v | MLapp (a,l) -> iter n a; List.iter (iter n) l - | MLcons (_,l) -> List.iter (iter n) l + | MLcons (_,_,l) -> List.iter (iter n) l | MLmagic a -> iter n a | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () in iter 0 @@ -343,10 +343,10 @@ let ast_map_case f (c,ids,a) = (c,ids,f a) let ast_map f = function | MLlam (i,a) -> MLlam (i, f a) | MLletin (i,a,b) -> MLletin (i, f a, f b) - | MLcase (a,v) -> MLcase (f a, Array.map (ast_map_case f) v) + | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v) | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v) | MLapp (a,l) -> MLapp (f a, List.map f l) - | MLcons (c,l) -> MLcons (c, List.map f l) + | MLcons (i,c,l) -> MLcons (i,c, List.map f l) | MLmagic a -> MLmagic (f a) | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a @@ -357,11 +357,11 @@ let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a) let ast_map_lift f n = function | MLlam (i,a) -> MLlam (i, f (n+1) a) | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b) - | MLcase (a,v) -> MLcase (f n a,Array.map (ast_map_lift_case f n) v) + | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v) | MLfix (i,ids,v) -> let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v) | MLapp (a,l) -> MLapp (f n a, List.map (f n) l) - | MLcons (c,l) -> MLcons (c, List.map (f n) l) + | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l) | MLmagic a -> MLmagic (f n a) | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a @@ -372,10 +372,10 @@ let ast_iter_case f (c,ids,a) = f a let ast_iter f = function | MLlam (i,a) -> f a | MLletin (i,a,b) -> f a; f b - | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v + | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v | MLfix (i,ids,v) -> Array.iter f v | MLapp (a,l) -> f a; List.iter f l - | MLcons (c,l) -> List.iter f l + | MLcons (_,c,l) -> List.iter f l | MLmagic a -> f a | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> () @@ -411,7 +411,7 @@ let nb_occur t = nb_occur_k 1 t let nb_occur_match = let rec nb k = function | MLrel i -> if i = k then 1 else 0 - | MLcase(a,v) -> + | MLcase(_,a,v) -> (nb k a) + Array.fold_left (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v @@ -420,7 +420,7 @@ let nb_occur_match = Array.fold_left (fun r a -> r+(nb k a)) 0 v | MLlam (_,a) -> nb (k+1) a | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l - | MLcons (_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l + | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0 in nb 1 @@ -616,7 +616,7 @@ let check_and_generalize (r0,l,c) = if i'<1 then c else if i'>nargs then MLrel (i-nargs+1) else raise Impossible - | MLcons(r,args) when r=r0 && (test_eta_args_lift n nargs args) -> + | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) -> MLrel (n+1) | a -> ast_map_lift genrec n a in genrec 0 c @@ -707,7 +707,7 @@ let rec permut_case_fun br acc = let rec is_iota_gen = function | MLcons _ -> true - | MLcase(_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br + | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br | _ -> false let constructor_index = function @@ -716,15 +716,15 @@ let constructor_index = function let iota_gen br = let rec iota k = function - | MLcons (r,a) -> + | MLcons (i,r,a) -> let (_,ids,c) = br.(constructor_index r) in let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in let c = ast_lift k c in MLapp (c,a) - | MLcase(e,br') -> + | MLcase(i,e,br') -> let new_br = Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br' - in MLcase(e, new_br) + in MLcase(i,e, new_br) | _ -> assert false in iota 0 @@ -741,13 +741,18 @@ let rec simpl o = function simpl o f | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) - | MLcase (e,br) -> + | MLcase (i,e,br) -> let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in - simpl_case o br (simpl o e) - | MLletin(id,c,e) when - (id = dummy_name) || (is_atomic c) || (is_atomic e) || - (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) -> + simpl_case o i br (simpl o e) + | MLletin(id,c,e) -> + let e = (simpl o e) in + if + (id = dummy_name) || (is_atomic c) || (is_atomic e) || + (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) + then simpl o (ast_subst c e) + else + MLletin(id, simpl o c, e) | MLfix(i,ids,c) -> let n = Array.length ids in if ast_occurs_itvl 1 n c.(i) then @@ -770,7 +775,7 @@ and simpl_app o a = function | MLletin (id,e1,e2) when o.opt_let_app -> (* Application of a letin: we push arguments inside *) MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) - | MLcase (e,br) when o.opt_case_app -> + | MLcase (i,e,br) when o.opt_case_app -> (* Application of a case: we push arguments inside *) let br' = Array.map @@ -778,16 +783,16 @@ and simpl_app o a = function let k = List.length l in let a' = List.map (ast_lift k) a in (n, l, simpl o (MLapp (t,a')))) br - in simpl o (MLcase (e,br')) + in simpl o (MLcase (i,e,br')) | (MLdummy | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) -and simpl_case o br e = +and simpl_case o i br e = if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *) simpl o (iota_gen br e) else - try (* Does a term [f] exist such as each branch is [(f e)] ? *) + try (* Does a term [f] exist such that each branch is [(f e)] ? *) if not o.opt_case_idr then raise Impossible; let f = check_generalizable_case o.opt_case_idg br in simpl o (MLapp (MLlam (anonymous,f),[e])) @@ -801,9 +806,9 @@ and simpl_case o br e = then let ids,br = permut_case_fun br [] in let n = List.length ids in - if n <> 0 then named_lams ids (MLcase (ast_lift n e, br)) - else MLcase (e, br) - else MLcase (e,br) + if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br)) + else MLcase (i,e,br) + else MLcase (i,e,br) let rec post_simpl = function | MLletin(_,c,e) when (is_atomic (eta_red c)) -> @@ -1006,8 +1011,8 @@ let optimize_fix a = let rec ml_size = function | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l | MLlam(_,t) -> 1 + ml_size t - | MLcons(_,l) -> ml_size_list l - | MLcase(t,pv) -> + | MLcons(_,_,l) -> ml_size_list l + | MLcase(_,t,pv) -> 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0) | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t @@ -1061,7 +1066,7 @@ let rec non_stricts add cand = function | MLapp (t,l)-> let cand = non_stricts false cand t in List.fold_left (non_stricts false) cand l - | MLcons (_,l) -> + | MLcons (_,_,l) -> List.fold_left (non_stricts false) cand l | MLletin (_,t1,t2) -> let cand = non_stricts false cand t1 in @@ -1071,7 +1076,7 @@ let rec non_stricts add cand = function let cand = lift n cand in let cand = Array.fold_left (non_stricts false) cand f in pop n cand - | MLcase (t,v) -> + | MLcase (_,t,v) -> (* The only interesting case: for a variable to be non-strict, *) (* it is sufficient that it appears non-strict in at least one branch, *) (* so we make an union (in fact a merge). *) diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index feb9e54e..54f0c992 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml,v 1.7.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*) open Names open Declarations @@ -157,6 +157,10 @@ let struct_iter do_decl do_spec s = type do_ref = global_reference -> unit +let record_iter_references do_term = function + | Record l -> List.iter do_term l + | _ -> () + let type_iter_references do_type t = let rec iter = function | Tglob (r,l) -> do_type r; List.iter iter l @@ -169,8 +173,12 @@ let ast_iter_references do_term do_cons do_type a = ast_iter iter a; match a with | MLglob r -> do_term r - | MLcons (r,_) -> do_cons r - | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v + | MLcons (i,r,_) -> + if lang () = Ocaml then record_iter_references do_term i; + do_cons r + | MLcase (i,_,v) as a -> + if lang () = Ocaml then record_iter_references do_term i; + Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () in iter a @@ -180,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind = let packet_iter ip p = do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in - if ind.ind_info = Record then List.iter do_term (find_projections kn); + if lang () = Ocaml then record_iter_references do_term ind.ind_info; Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets let decl_iter_references do_term do_cons do_type = @@ -236,7 +244,7 @@ let struct_get_references_list struc = exception Found let rec ast_search t a = - if t = a then raise Found else ast_iter (ast_search t) a + if t a then raise Found else ast_iter (ast_search t) a let decl_ast_search t = function | Dterm (_,a,_) -> ast_search t a diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index f73e18f7..7f8c4113 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.mli,v 1.2.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*) open Names open Declarations @@ -42,7 +42,7 @@ val add_labels_mp : module_path -> label list -> module_path (*s Functions upon ML modules. *) -val struct_ast_search : ml_ast -> ml_structure -> bool +val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool val struct_type_search : ml_type -> ml_structure -> bool type do_ref = global_reference -> unit diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 707ef94f..ff9cfd21 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml,v 1.100.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*) (*s Production of Ocaml syntax. *) @@ -20,8 +20,6 @@ open Miniml open Mlutil open Modutil -let cons_cofix = ref Refset.empty - (*s Some utility functions. *) let pp_par par st = if par then str "(" ++ st ++ str ")" else st @@ -68,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt () let fnl2 () = fnl () ++ fnl () +let pp_parameters l = + (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) + +let pp_string_parameters l = + (pp_boxed_tuple str l ++ space_if (l<>[])) + (*s Generic renaming issues. *) let rec rename_id id avoid = @@ -126,7 +130,7 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules (mldummy,tdummy,tunknown) = +let preamble _ used_modules (mldummy,tdummy,tunknown) _ = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false @@ -167,22 +171,33 @@ let pp_global r = let empty_env () = [], P.globals () +exception NoRecord + +let find_projections = function Record l -> l | _ -> raise NoRecord + (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) +let kn_sig = + let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in + make_kn specif empty_dirpath (mk_label "sig") + let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) | Tglob (r,[]) -> pp_global r - | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r + | Tglob (r,l) -> + if r = IndRef (kn_sig,0) then + pp_tuple_light pp_rec l + else + pp_tuple_light pp_rec l ++ spc () ++ pp_global r | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy -> str "__" | Tunknown -> str "__" - | Tcustom s -> str s in hov 0 (pp_rec par t) @@ -193,7 +208,7 @@ let rec pp_type par vl t = let expr_needs_par = function | MLlam _ -> true - | MLcase (_,[|_|]) -> false + | MLcase (_,_,[|_|]) -> false | MLcase _ -> true | _ -> false @@ -231,30 +246,32 @@ let rec pp_expr par env args = let record = List.hd args in pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) with _ -> apply (pp_global r)) - | MLcons (r,[]) -> + | MLcons (Coinductive,r,[]) -> assert (args=[]); - if Refset.mem r !cons_cofix then - pp_par par (str "lazy " ++ pp_global r) - else pp_global r - | MLcons (r,args') -> - (try - let projs = find_projections (kn_of_r r) in - pp_record_pat (projs, List.map (pp_expr true env []) args') - with Not_found -> - assert (args=[]); - let tuple = pp_tuple (pp_expr true env []) args' in - if Refset.mem r !cons_cofix then - pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") - else pp_par par (pp_global r ++ spc () ++ tuple)) - | MLcase (t, pv) -> + pp_par par (str "lazy " ++ pp_global r) + | MLcons (Coinductive,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") + | MLcons (_,r,[]) -> + assert (args=[]); + pp_global r + | MLcons (Record projs, r, args') -> + assert (args=[]); + pp_record_pat (projs, List.map (pp_expr true env []) args') + | MLcons (_,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (pp_global r ++ spc () ++ tuple) + | MLcase (i, t, pv) -> let r,_,_ = pv.(0) in - let expr = if Refset.mem r !cons_cofix then + let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else (pp_expr false env [] t) in (try - let projs = find_projections (kn_of_r r) in + let projs = find_projections i in let (_, ids, c) = pv.(0) in let n = List.length ids in match c with @@ -263,17 +280,17 @@ let rec pp_expr par env args = pp_global (List.nth projs (n-i)))) | MLapp (MLrel i, a) when i <= n -> if List.exists (ast_occurs_itvl 1 n) a - then raise Not_found + then raise NoRecord else let ids,env' = push_vars (List.rev ids) env in (pp_apply (pp_expr true env [] t ++ str "." ++ pp_global (List.nth projs (n-i))) par ((List.map (pp_expr true env' []) a) @ args)) - | _ -> raise Not_found - with Not_found -> + | _ -> raise NoRecord + with NoRecord -> if Array.length pv = 1 then - let s1,s2 = pp_one_pat env pv.(0) in + let s1,s2 = pp_one_pat env i pv.(0) in apply (hv 0 (pp_par par' @@ -285,7 +302,7 @@ let rec pp_expr par env args = apply (pp_par par' (v 0 (str "match " ++ expr ++ str " with" ++ - fnl () ++ str " | " ++ pp_pat env pv)))) + fnl () ++ str " | " ++ pp_pat env i pv)))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -307,21 +324,21 @@ and pp_record_pat (projs, args) = (List.combine projs args) ++ str " }" -and pp_one_pat env (r,ids,t) = +and pp_one_pat env i (r,ids,t) = let ids,env' = push_vars (List.rev ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in try - let projs = find_projections (kn_of_r r) in + let projs = find_projections i in pp_record_pat (projs, List.rev_map pr_id ids), expr - with Not_found -> + with NoRecord -> let args = if ids = [] then (mt ()) else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in pp_global r ++ args, expr -and pp_pat env pv = +and pp_pat env i pv = prvect_with_sep (fun () -> (fnl () ++ str " | ")) - (fun x -> let s1,s2 = pp_one_pat env x in + (fun x -> let s1,s2 = pp_one_pat env i x in hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv and pp_function env f t = @@ -331,20 +348,17 @@ and pp_function env f t = let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl) in - let is_not_cofix pv = - let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) - in match t' with - | MLcase(MLrel 1,pv) when is_not_cofix pv -> + | MLcase(i,MLrel 1,pv) when i=Standard -> if is_function pv then (f ++ pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' pv)) + v 0 (str " | " ++ pp_pat env' i pv)) else (f ++ pr_binding (List.rev bl) ++ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' pv)) + v 0 (str " | " ++ pp_pat env' i pv)) | _ -> (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ @@ -384,12 +398,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) = (*s Pretty-printing of inductive types declaration. *) -let pp_parameters l = - (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) - -let pp_string_parameters l = - (pp_boxed_tuple str l ++ space_if (l<>[])) - let pp_one_ind prefix ip pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = @@ -420,9 +428,8 @@ let pp_singleton kn packet = pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -let pp_record kn packet = - let l = List.combine (find_projections kn) packet.ip_types.(0) in - let projs = find_projections kn in +let pp_record kn projs packet = + let l = List.combine projs packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) @@ -466,13 +473,9 @@ let pp_ind co kn ind = let pp_mind kn i = match i.ind_info with | Singleton -> pp_singleton kn i.ind_packets.(0) - | Coinductive -> - let nop _ = () - and add r = cons_cofix := Refset.add r !cons_cofix in - decl_iter_references nop add nop (Dind (kn,i)); - pp_ind true kn i - | Record -> pp_record kn i.ind_packets.(0) - | _ -> pp_ind false kn i + | Coinductive -> pp_ind true kn i + | Record projs -> pp_record kn projs i.ind_packets.(0) + | Standard -> pp_ind false kn i let pp_decl mpl = local_mpl := mpl; @@ -481,6 +484,7 @@ let pp_decl mpl = | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else + let pp_r = pp_global r in let l = rename_tvars keywords l in let ids, def = try let ids,s = find_type_custom r in @@ -490,7 +494,7 @@ let pp_decl mpl = if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" else str "=" ++ spc () ++ pp_type false l t in - hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ + hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ spc () ++ def) | Dterm (r, a, t) -> if is_inline_custom r then failwith "empty phrase" diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 711c15da..5015a50d 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.mli,v 1.26.6.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*) (*s Some utility functions to be reused in module [Haskell]. *) @@ -15,8 +15,6 @@ open Names open Libnames open Miniml -val cons_cofix : Refset.t ref - val pp_par : bool -> std_ppcmds -> std_ppcmds val pp_abst : identifier list -> std_ppcmds val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds @@ -39,10 +37,10 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t val preamble : - extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds + extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds val preamble_sig : - extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds + extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds (*s Production of Ocaml syntax. We export both a functor to be used for extraction in the Coq toplevel and a function to extract some diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 61045304..4a881da2 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml,v 1.9.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*) (*s Production of Scheme syntax. *) @@ -24,17 +24,30 @@ open Ocaml let keywords = List.fold_right (fun s -> Idset.add (id_of_string s)) - [ "define"; "let"; "lambda"; "lambdas"; "match-case"; + [ "define"; "let"; "lambda"; "lambdas"; "match"; "apply"; "car"; "cdr"; "error"; "delay"; "force"; "_"; "__"] Idset.empty -let preamble _ _ (mldummy,_,_) = +let preamble _ _ (mldummy,_,_) _ = + str ";; This extracted scheme code relies on some additional macros" ++ + fnl () ++ + str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++ + fnl () ++ + str "(load \"macros_extr.scm\")" ++ + fnl () ++ fnl () ++ (if mldummy then str "(define __ (lambda (_) __))" ++ fnl () ++ fnl() else mt ()) +let pr_id id = + let s = string_of_id id in + for i = 0 to String.length s - 1 do + if s.[i] = '\'' then s.[i] <- '~' + done; + str s + let paren = pp_par true let pp_abst st = function @@ -43,6 +56,12 @@ let pp_abst st = function | l -> paren (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st) +let pp_apply st _ = function + | [] -> st + | [a] -> hov 2 (paren (st ++ spc () ++ a)) + | args -> hov 2 (paren (str "@ " ++ st ++ + (prlist (fun x -> spc () ++ x) args))) + (*s The pretty-printing functor. *) module Make = functor(P : Mlpp_param) -> struct @@ -63,7 +82,7 @@ let rec pp_expr env args = | MLlam _ as a -> let fl,a' = collect_lams a in let fl,env' = push_vars fl env in - pp_abst (pp_expr env' [] a') (List.rev fl) + apply (pp_abst (pp_expr env' [] a') (List.rev fl)) | MLletin (id,a1,a2) -> let i,env' = push_vars [id] env in apply @@ -77,46 +96,46 @@ let rec pp_expr env args = ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> apply (pp_global r) - | MLcons (r,args') -> + | MLcons (i,r,args') -> assert (args=[]); let st = str "`" ++ paren (pp_global r ++ - (if args' = [] then mt () else (spc () ++ str ",")) ++ - prlist_with_sep - (fun () -> spc () ++ str ",") - (pp_expr env []) args') + (if args' = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args') in - if Refset.mem r !cons_cofix then - paren (str "delay " ++ st) - else st - | MLcase (t, pv) -> - let r,_,_ = pv.(0) in - let e = if Refset.mem r !cons_cofix then - paren (str "force" ++ spc () ++ pp_expr env [] t) - else - pp_expr env [] t - in apply (v 3 (paren - (str "match-case " ++ e ++ fnl () ++ pp_pat env pv))) + if i = Coinductive then paren (str "delay " ++ st) else st + | MLcase (i,t, pv) -> + let e = + if i <> Coinductive then pp_expr env [] t + else paren (str "force" ++ spc () ++ pp_expr env [] t) + in + apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) - paren (str "absurd") + paren (str "error" ++ spc () ++ qs s) | MLdummy -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> pp_expr env args a - | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n") + | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") + +and pp_cons_args env = function + | MLcons (i,r,args) when i<>Coinductive -> + paren (pp_global r ++ + (if args = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args) + | e -> str "," ++ pp_expr env [] e and pp_one_pat env (r,ids,t) = - let pp_arg id = str "?" ++ pr_id id in let ids,env' = push_vars (List.rev ids) env in let args = if ids = [] then mt () - else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids)) + else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) in (pp_global r ++ args), (pp_expr env' [] t) @@ -133,7 +152,8 @@ and pp_fix env j (ids,bl) args = (str "letrec " ++ (v 0 (paren (prvect_with_sep fnl - (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti))) + (fun (fi,ti) -> + paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti))) (array_map2 (fun id b -> (id,b)) ids bl)) ++ fnl () ++ hov 2 (pp_apply (pr_id (ids.(j))) true args)))) @@ -156,8 +176,12 @@ let pp_decl _ = function | Dterm (r, a, _) -> if is_inline_custom r then mt () else - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ - pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () + if is_custom r then + hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + str (find_custom r))) ++ fnl () ++ fnl () + else + hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () let pp_structure_elem mp = function | (l,SEdecl d) -> pp_decl mp d diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 6e689a47..2a828fb9 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.mli,v 1.6.6.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) (*s Some utility functions to be reused in module [Haskell]. *) @@ -17,7 +17,7 @@ open Names val keywords : Idset.t val preamble : - extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds + extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index a65c51a4..9d73d13f 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml,v 1.35.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) open Names open Term @@ -90,17 +90,9 @@ let is_recursor = function (*s Record tables. *) -let records = ref (KNmap.empty : global_reference list KNmap.t) -let init_records () = records := KNmap.empty - let projs = ref (Refmap.empty : int Refmap.t) let init_projs () = projs := Refmap.empty - -let add_record kn n (l1,l2) = - records := KNmap.add kn l1 !records; - projs := List.fold_right (fun r -> Refmap.add r n) l2 !projs - -let find_projections kn = KNmap.find kn !records +let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs let is_projection r = Refmap.mem r !projs let projection_arity r = Refmap.find r !projs @@ -108,7 +100,7 @@ let projection_arity r = Refmap.find r !projs let reset_tables () = init_terms (); init_types (); init_inductives (); init_recursors (); - init_records (); init_projs () + init_projs () (*s Printing. *) @@ -196,6 +188,10 @@ let error_MPfile_as_mod d = err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^ "Extraction cannot currently deal with this situation.\n")) +let error_record r = + err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++ + str "To help extraction, please use an explicit name.") + (*S The Extraction auxiliary commands *) (*s Extraction AutoInline *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 680638e5..6160452a 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli,v 1.25.2.1 2004/07/16 19:30:09 herbelin Exp $ i*) +(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) open Names open Libnames @@ -29,7 +29,7 @@ val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a val error_unqualified_name : string -> string -> 'a val error_MPfile_as_mod : dir_path -> 'a - +val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit @@ -58,9 +58,7 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_record : - kernel_name -> int -> global_reference list * global_reference list -> unit -val find_projections : kernel_name -> global_reference list +val add_projection : int -> kernel_name -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index b358ff39..1500e1ae 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -157,11 +157,9 @@ let rec npatternify ltypes c = | [] -> c | (mv,nme,t)::ltypes' -> let c'= substitterm 0 mv (mkRel 1) c in -(* let _ = prconstr c' in *) let tlift = lift (List.length ltypes') t in let res = npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in -(* let _ = prconstr res in *) res (* fait une application (c m1 m2...mn, où mi est une evar, on rend également @@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs: | u -> let varrels = List.rev (List.map fst lst_vars) in let varnames = List.map snd lst_vars in - let nb_vars = (List.length varnames) in - let nb_eqs = (List.length lst_eqs) in + let nb_vars = List.length varnames in + let nb_eqs = List.length lst_eqs in let eqrels = List.map fst lst_eqs in (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs trouvés dans les let in et les Cases avec ceux trouves dans u (ie mi.mimick). *) (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *) - let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc) in - + let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in + (*c construction du terme: application successive des variables, des egalites et des appels rec, a la variable existentielle correspondant a l'hypothese de recurrence en cours. *) @@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma = sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in princ_proof,levar,lposeq,evararr,absc,parms - (* Do intros [i] times, then do rewrite on all introduced hyps which are called like [heq_prefix], FIX: have another filter than the name. *) let rec iterintro i = @@ -596,12 +593,12 @@ let rec iterintro i = (* (fun hyp gl -> - let _ = print_string ("nthhyp= "^ string_of_int i) in + let _ = prstr ("nthhyp= "^ string_of_int i) in if isConst hyp && ((name_of_const hyp)==heq_prefix) then - let _ = print_string "YES\n" in + let _ = prstr "YES\n" in rewriteLR hyp gl else - let _ = print_string "NO\n" in + let _ = prstr "NO\n" in tclIDTAC gl) *) @@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist = (* Declaration of the functional scheme. *) let declareFunScheme f fname mutflist = - let scheme = - buildFunscheme (constr_of f) - (Array.of_list (List.map constr_of (f::mutflist))) in + let flist = if mutflist=[] then [f] else mutflist in + let fcstrlist = Array.of_list (List.map constr_of flist) in + let scheme = buildFunscheme (constr_of f) fcstrlist in let _ = prstr "Principe:" in let _ = prconstr scheme in let ce = { diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 6e086d95..a125b9a7 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -21,7 +21,7 @@ open Reductionops (*s printing of constr -- debugging *) (* comment this line to see debug msgs *) -let msg x = () ;; let prterm c = str "" +let msg x = () ;; let prterm c = str "" (* uncomment this to see debugging *) let prconstr c = msg (str" " ++ prterm c ++ str"\n") let prlistconstr lc = List.iter prconstr lc @@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs = -(* list of occurrences of a term inside another, no imbricated - occurrence are considered (ie we stop looking inside a termthat is - an occurrence). *) +(* list of occurrences of a term inside another *) +(* Cofix will be wrong, not sure Fix is correct too *) let rec hdMatchSub u t= - if constr_head_match u t then - u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t)) - [] - u) - else - fold_constr (fun l cstr -> l@(hdMatchSub cstr t)) - [] - u + let subres = + match kind_of_term u with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t + | Fix (_,(lna,tl,bl)) -> + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) + [] bl + | LetIn _ -> assert false + (* Correct? *) + | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u + in + if constr_head_match u t then u :: subres else subres + (* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *) let hdMatchSub_cpl u (d,f) = - let res = ref [] in - begin - for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done; - !res - end + let res = ref [] in + begin + for i = d to f do res := hdMatchSub u (mkRel i) @ !res done; + !res + end (* destApplication raises an exception if [t] is not an application *) let exchange_hd_prod subst_hd t = - let (hd,args)= destApplication t in mkApp (subst_hd,args) + let hd,args= destApplication t in mkApp (subst_hd,args) (* substitute t by by_t in head of products inside in_u, reduces each product found *) let rec substit_red prof t by_t in_u = if constr_head_match in_u (lift prof t) then - let _ = prNamedConstr "in_u" in_u in - let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in - let _ = prNamedConstr "xx " x in - let _ = prstr "\n\n" in - x + let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in + x else - map_constr_with_binders succ (fun i u -> substit_red i t by_t u) - prof in_u + map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each reli by tarr.(f-i). *) let exchange_reli_arrayi tarr (d,f) t = let hd,args= destApplication t in let i = destRel hd in - whd_beta (mkApp (tarr.(f-i) ,args)) + let res = whd_beta (mkApp (tarr.(f-i) ,args)) in + res let exchange_reli_arrayi_L tarr (d,f) = List.map (exchange_reli_arrayi tarr (d,f)) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 50f5b947..02dc57de 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -195,6 +195,11 @@ let xlate_int_opt = function | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n) | None -> CT_coerce_NONE_to_INT_OPT CT_none +let xlate_int_or_var_opt_to_int_opt = function + | Some (ArgArg n) -> CT_coerce_INT_to_INT_OPT (CT_int n) + | Some (ArgVar _) -> xlate_error "int_or_var: TODO" + | None -> CT_coerce_NONE_to_INT_OPT CT_none + let tac_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) @@ -1026,12 +1031,12 @@ and xlate_tac = (if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none), (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none)) | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt) - | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt) + | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt) | TacAuto (nopt, None) -> - CT_auto_with (xlate_int_opt nopt, + CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt, CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star) | TacAuto (nopt, Some (id1::idl)) -> - CT_auto_with(xlate_int_opt nopt, + CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt, CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl))) |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) -> @@ -1141,7 +1146,8 @@ and xlate_tac = | TacClearBody([]) -> assert false | TacClearBody(a::l) -> CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l)) - | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b) + | TacDAuto (a, b) -> + CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacNewDestruct(a,b,(c,_)) -> CT_new_destruct (xlate_int_or_constr a, xlate_using b, diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index f2eeb5fe..f0eb1e78 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id: omega.ml,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *) +(* $Id: omega.ml,v 1.7.2.2 2005/02/17 18:25:20 herbelin Exp $ *) open Util open Hashtbl @@ -520,9 +520,11 @@ let rec depend relie_on accu = function depend (e1.id::e2.id::relie_on) (act::accu) l else depend relie_on accu l - | STATE (e,_,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l + | STATE (e,_,o,_,_) -> + if List.mem e.id relie_on then + depend (o.id::relie_on) (act::accu) l + else + depend relie_on accu l | HYP e -> if List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template index 96c53192..1dd625c8 100644 --- a/dev/ocamldebug-v7.template +++ b/dev/ocamldebug-v7.template @@ -2,10 +2,10 @@ # wrap around ocamldebug for Coq -export COQTOP=COQTOPDIRECTORY -export COQLIB=COQLIBDIRECTORY +export COQTOP='COQTOPDIRECTORY' +export COQLIB='COQLIBDIRECTORY' export COQTH=$COQLIB/theories -CAMLBIN=CAMLBINDIRECTORY +CAMLBIN='CAMLBINDIRECTORY' OCAMLDEBUG=$CAMLBIN/ocamldebug export CAMLP4LIB=`$CAMLBIN/camlp4 -where` diff --git a/dev/perf-analysis b/dev/perf-analysis new file mode 100644 index 00000000..4295a573 --- /dev/null +++ b/dev/perf-analysis @@ -0,0 +1,51 @@ +Performance analysis for V8-0-bugfix branch +------------------------------------------- + + Dec 27, 2005: contrib Karatsuba added (~ 24s) + +Dec 1-14, 2005: benchmarking server down + +Nov 29 and Dec 16, 2005: size increase + due to new record flag in inductive for extraction + + Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 24s) + + Aug 1, 2005: contrib Kildall added (~ 64s) + +Jul 26-Aug 2, 2005: bench down + +Jul 14-15, 2005: 4 contribs failed including CoRN + + Jul 7, 2005: adding contrib Fermat4: but not compabible and remove on Jul 8 + + Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 28s) + +Jun 4, 2005: significant time reduction + (e.g. Nijmegen/LinAlg: -15%, Nijmegen/QArith: stable; Nijmegen/CoRN: -1%) + only changes are the removal of an assert checking location and + the pre-definition of level 200 (could it be just a parsing improvement??) + + May 19, 2005: contrib Goodstein and prfx (~ 9s) added + +Apr 30, 2005: evaluation order of atomic tactics changed + (e.g. Nijmegen/CoRN: stable, Nijmegen/QArith: -2%, Nijmegen/LinAlg: +20%) + +Mar 20, 2005: fixed Logic.with_check bug + improved whole V8-0-bugfix bench by 4 % + (e.g. Nijmegen/CoRN: - 7.5 %, Nijmegen/QARITH: - 1.5 %) + +Mar 7-10, 2005: unexplained time reduction + (on Mar 7, changed Ppconstrnew univ printer only) + (note also a server upgrade around Mar 10) + +Feb 17, 2005: fixed omega bug #922 (wrong STATE dependency): + improved whole V8-0-bugfix bench by 2 % + (e.g. Nijmegen/CoRN: - 6.5 %, Nijmegen/QARITH: - 3 %) + +Feb 2, 2005: fixed ltac var interpretation order + + Jan 13, 2005: contrib SumOfTwoSquare added (~ 37s) + +Dec 20-29, 2004: reduced whole V8-0-bugfix due to Berkeley/Godel failure + +Nov 27 - Dec 10, 2004: strong instability diff --git a/ide/coq.ico b/ide/coq.ico Binary files differnew file mode 100644 index 00000000..390065bc --- /dev/null +++ b/ide/coq.ico @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml,v 1.38.2.1 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: coq.ml,v 1.38.2.2 2005/11/16 17:22:38 barras Exp $ *) open Vernac open Vernacexpr @@ -95,10 +95,10 @@ let is_in_coq_path f = let _ = Library.locate_qualified_library (Libnames.make_qualid Names.empty_dirpath (Names.id_of_string base)) in - prerr_endline (f ^ "is in coq path"); + prerr_endline (f ^ " is in coq path"); true with _ -> - prerr_endline (f ^ "is NOT in coq path"); + prerr_endline (f ^ " is NOT in coq path"); false let is_in_proof_mode () = diff --git a/ide/coq2.ico b/ide/coq2.ico Binary files differnew file mode 100755 index 00000000..36964902 --- /dev/null +++ b/ide/coq2.ico diff --git a/ide/coqide.ml b/ide/coqide.ml index 08994010..a8179fb9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml,v 1.99.2.3 2004/10/15 14:50:12 coq Exp $ *) +(* $Id: coqide.ml,v 1.99.2.6 2006/01/06 13:22:36 barras Exp $ *) open Preferences open Vernacexpr @@ -247,50 +247,43 @@ let break () = prerr_endline " ignored (not computing)" end -let full_do_if_not_computing text f x = - ignore - (Thread.create - (async - (fun () -> - if Mutex.try_lock coq_computing - then - begin - prerr_endline ("Launching thread " ^ text); - let w = Blaster_window.blaster_window () in - if not (Mutex.try_lock w#lock) then begin - break (); - let lck = Mutex.create () in - Mutex.lock lck; - prerr_endline "Waiting on blaster..."; - Condition.wait w#blaster_killed lck; - prerr_endline "Waiting on blaster ok"; - Mutex.unlock lck - end else Mutex.unlock w#lock; - let idle = - Glib.Timeout.add ~ms:300 - ~callback:(fun () -> !pulse ();true) in - begin - prerr_endline "Getting lock"; - try - f x; - Glib.Timeout.remove idle; - prerr_endline "Releasing lock"; - Mutex.unlock coq_computing; - with e -> - Glib.Timeout.remove idle; - prerr_endline "Releasing lock (on error)"; - Mutex.unlock coq_computing; - raise e - end - end - else - prerr_endline - "Discarded order (computations are ongoing)")) - ()) - let do_if_not_computing text f x = - ignore (full_do_if_not_computing text f x) - + let threaded_task () = + if Mutex.try_lock coq_computing + then + begin + prerr_endline ("Launching thread " ^ text); + let w = Blaster_window.blaster_window () in + if not (Mutex.try_lock w#lock) then begin + break (); + let lck = Mutex.create () in + Mutex.lock lck; + prerr_endline "Waiting on blaster..."; + Condition.wait w#blaster_killed lck; + prerr_endline "Waiting on blaster ok"; + Mutex.unlock lck + end else Mutex.unlock w#lock; + let idle = + Glib.Timeout.add ~ms:300 + ~callback:(fun () -> async !pulse ();true) in + begin + prerr_endline "Getting lock"; + try + f x; + Glib.Timeout.remove idle; + prerr_endline "Releasing lock"; + Mutex.unlock coq_computing; + with e -> + Glib.Timeout.remove idle; + prerr_endline "Releasing lock (on error)"; + Mutex.unlock coq_computing; + raise e + end + end + else + prerr_endline + "Discarded order (computations are ongoing)" in + ignore (Thread.create threaded_task ()) let add_input_view tv = Vector.append input_views tv @@ -948,27 +941,9 @@ object(self) end method send_to_coq verbosely replace phrase show_output show_error localize = - try - full_goal_done <- false; - prerr_endline "Send_to_coq starting now"; - if replace then begin - let r,info = -(* full_do_if_not_computing "coq eval and replace" *) - Coq.interp_and_replace ("Info " ^ phrase) - in - let msg = read_stdout () in - self#insert_message (if show_output then msg else ""); - - Some r - - end else begin - let r = Some (Coq.interp verbosely phrase) in - let msg = read_stdout () in - self#insert_message (if show_output then msg else ""); - r - end - with e -> - (if show_error then + let display_output msg = + self#insert_message (if show_output then msg else "") in + let display_error e = let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); self#set_message s; @@ -986,8 +961,23 @@ object(self) input_buffer#apply_tag_by_name "error" ~start:starti ~stop:stopi; - input_buffer#place_cursor starti; - )); + input_buffer#place_cursor starti) in + try + full_goal_done <- false; + prerr_endline "Send_to_coq starting now"; + if replace then begin + let r,info = Coq.interp_and_replace ("info " ^ phrase) in + let msg = read_stdout () in + sync display_output msg; + Some r + end else begin + let r = Coq.interp verbosely phrase in + let msg = read_stdout () in + sync display_output msg; + Some r + end + with e -> + if show_error then sync display_error e; None method find_phrase_starting_at (start:GText.iter) = @@ -1068,149 +1058,148 @@ object(self) method process_next_phrase verbosely display_goals do_highlight = - begin - try - self#clear_message; - prerr_endline "process_next_phrase starting now"; - if do_highlight then begin - !push_info "Coq is computing"; - input_view#set_editable false; - end; - begin match (self#find_phrase_starting_at self#get_start_of_input) - with - | None -> + let get_next_phrase () = + self#clear_message; + prerr_endline "process_next_phrase starting now"; + if do_highlight then begin + !push_info "Coq is computing"; + input_view#set_editable false; + end; + match self#find_phrase_starting_at self#get_start_of_input with + | None -> if do_highlight then begin input_view#set_editable true; !pop_info (); - end; false + end; + None | Some(start,stop) -> prerr_endline "process_next_phrase : to_process highlight"; - let b = input_buffer in if do_highlight then begin input_buffer#apply_tag_by_name ~start ~stop "to_process"; prerr_endline "process_next_phrase : to_process applied"; end; prerr_endline "process_next_phrase : getting phrase"; - let phrase = start#get_slice ~stop in - let r = - match self#send_to_coq verbosely false phrase true true true with - | Some ast -> - begin - b#move_mark ~where:stop (`NAME "start_of_input"); - b#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - begin - b#place_cursor stop; - self#recenter_insert - end; - let start_of_phrase_mark = `MARK (b#create_mark start) in - let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase - start_of_phrase_mark - end_of_phrase_mark ast; - if display_goals then self#show_goals; - true - end - | None -> false - in - if do_highlight then begin - b#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true; - !pop_info (); - end; - r; - end - with e -> raise e + Some((start,stop),start#get_slice ~stop) in + let remove_tag (start,stop) = + if do_highlight then begin + input_buffer#remove_tag_by_name ~start ~stop "to_process" ; + input_view#set_editable true; + !pop_info (); + end in + let mark_processed (start,stop) ast = + let b = input_buffer in + b#move_mark ~where:stop (`NAME "start_of_input"); + b#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + begin + b#place_cursor stop; + self#recenter_insert + end; + let start_of_phrase_mark = `MARK (b#create_mark start) in + let end_of_phrase_mark = `MARK (b#create_mark stop) in + push_phrase + start_of_phrase_mark + end_of_phrase_mark ast; + if display_goals then self#show_goals; + remove_tag (start,stop) in + begin + match sync get_next_phrase () with + | None -> false + | Some (loc,phrase) -> + (match self#send_to_coq verbosely false phrase true true true with + | Some ast -> sync (mark_processed loc) ast; true + | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop insertphrase - else input_buffer#insert ~iter:stop ("\n"^insertphrase); - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = `MARK (input_buffer#create_mark start) - in - let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; - self#show_goals; - (*Auto insert save on success... - try (match Coq.get_current_goals () with - | [] -> + let mark_processed ast = + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop insertphrase + else input_buffer#insert ~iter:stop ("\n"^insertphrase); + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast; + self#show_goals; + (*Auto insert save on success... + try (match Coq.get_current_goals () with + | [] -> (match self#send_to_coq "Save.\n" true true true with | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop "Save.\n" - else input_buffer#insert ~iter:stop "\nSave.\n"; - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = `MARK (input_buffer#create_mark start) - in - let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast - end + begin + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop "Save.\n" + else input_buffer#insert ~iter:stop "\nSave.\n"; + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = + `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = + `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast + end | None -> ()) - | _ -> ()) - with _ -> ()*) - true - end - | None -> self#insert_message ("Unsuccessfully tried: "^coqphrase); + | _ -> ()) + with _ -> ()*) in + match self#send_to_coq false false coqphrase show_output show_msg localize with + | Some ast -> sync mark_processed ast; true + | None -> + sync + (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) + (); false method process_until_iter_or_error stop = let stop' = `OFFSET stop#offset in let start = self#get_start_of_input#copy in let start' = `OFFSET start#offset in - input_buffer#apply_tag_by_name - ~start - ~stop - "to_process"; - input_view#set_editable false; + sync (fun _ -> + input_buffer#apply_tag_by_name ~start ~stop "to_process"; + input_view#set_editable false) (); !push_info "Coq is computing"; - process_pending (); +(* process_pending ();*) (try while ((stop#compare self#get_start_of_input>=0) && (self#process_next_phrase false false false)) do Util.check_for_interrupt () done with Sys.Break -> prerr_endline "Interrupted during process_until_iter_or_error"); - self#show_goals; - (* Start and stop might be invalid if an eol was added at eof *) - let start = input_buffer#get_iter start' in - let stop = input_buffer#get_iter stop' in - input_buffer#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true; + sync (fun _ -> + self#show_goals; + (* Start and stop might be invalid if an eol was added at eof *) + let start = input_buffer#get_iter start' in + let stop = input_buffer#get_iter stop' in + input_buffer#remove_tag_by_name ~start ~stop "to_process" ; + input_view#set_editable true) (); !pop_info() method process_until_end_or_error = self#process_until_iter_or_error input_buffer#end_iter method reset_initial = - Stack.iter - (function inf -> - let start = input_buffer#get_iter_at_mark inf.start in - let stop = input_buffer#get_iter_at_mark inf.stop in - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - input_buffer#remove_tag_by_name "processed" ~start ~stop; - input_buffer#delete_mark inf.start; - input_buffer#delete_mark inf.stop; - ) - processed_stack; - Stack.clear processed_stack; - self#clear_message; + sync (fun _ -> + Stack.iter + (function inf -> + let start = input_buffer#get_iter_at_mark inf.start in + let stop = input_buffer#get_iter_at_mark inf.stop in + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + input_buffer#remove_tag_by_name "processed" ~start ~stop; + input_buffer#delete_mark inf.start; + input_buffer#delete_mark inf.stop; + ) + processed_stack; + Stack.clear processed_stack; + self#clear_message) (); Coq.reset_initial () @@ -1260,19 +1249,21 @@ object(self) (match undos with | None -> synchro () | Some n -> try Pfedit.undo n with _ -> synchro ()); - let start = if is_empty () then input_buffer#start_iter - else input_buffer#get_iter_at_mark (top ()).stop - in - prerr_endline "Removing (long) processed tag..."; - input_buffer#remove_tag_by_name - ~start - ~stop:self#get_start_of_input - "processed"; - prerr_endline "Moving (long) start_of_input..."; - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - self#show_goals; - clear_stdout (); - self#clear_message; + sync (fun _ -> + let start = if is_empty () then input_buffer#start_iter + else input_buffer#get_iter_at_mark (top ()).stop + in + prerr_endline "Removing (long) processed tag..."; + input_buffer#remove_tag_by_name + ~start + ~stop:self#get_start_of_input + "processed"; + prerr_endline "Moving (long) start_of_input..."; + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + self#show_goals; + clear_stdout (); + self#clear_message) + (); with _ -> !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. Please restart and report NOW."; @@ -1315,7 +1306,7 @@ Please restart and report NOW."; begin match last_command with | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> begin - try Pfedit.undo 1; ignore (pop ()); update_input () + try Pfedit.undo 1; ignore (pop ()); sync update_input () with _ -> self#backtrack_to_no_lock start end | {ast=_,t;reset_info=Reset (id, {contents=true})} -> @@ -1326,7 +1317,7 @@ Please restart and report NOW."; | VernacEndSegment _ -> reset_to_mod id | _ -> reset_to id); - update_input () + sync update_input () | { ast = _, ( VernacStartTheoremProof _ | VernacGoal _ | VernacDeclareTacticDefinition _ @@ -1340,10 +1331,10 @@ Please restart and report NOW."; prerr_endline "WARNING : found a closed environment"; raise e end); - update_input () + sync update_input () | { ast = (_, a) } when is_state_preserving a -> ignore (pop ()); - update_input () + sync update_input () | _ -> self#backtrack_to_no_lock start end; @@ -1356,7 +1347,6 @@ Please restart and report NOW."; method blaster () = - ignore (Thread.create (fun () -> prerr_endline "Blaster called"; @@ -1375,14 +1365,14 @@ Please restart and report NOW."; ("Goal "^gnb) s (fun () -> try_interptac t') - (fun () -> self#insert_command t'' t'') + (sync(fun () -> self#insert_command t'' t'')) in let set_current_goal (s,t) = c#set "Goal 1" s (fun () -> try_interptac ("progress "^t)) - (fun () -> self#insert_command t t) + (sync(fun () -> self#insert_command t t)) in begin match current_gls with | [] -> () @@ -1405,11 +1395,11 @@ Please restart and report NOW."; ()) method insert_command cp ip = - self#clear_message; + async(fun _ -> self#clear_message)(); ignore (self#insert_this_phrase_on_success true false false cp ip) method tactic_wizard l = - self#clear_message; + async(fun _ -> self#clear_message)(); ignore (List.exists (fun p -> @@ -1742,11 +1732,11 @@ let main files = ~width:!current.window_width ~height:!current.window_height ~title:"CoqIde" () in -(* - let icon_image = Filename.concat lib_ide "coq.ico" in - let icon = GdkPixbuf.from_file icon_image in - w#set_icon (Some icon); -*) + (try + let icon_image = lib_ide_file "coq2.ico" in + let icon = GdkPixbuf.from_file icon_image in + w#set_icon (Some icon) + with _ -> ()); let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in @@ -2064,21 +2054,21 @@ let main files = ignore (get_current_view()).view#clear_undo)); ignore(edit_f#add_separator ()); ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback: - (do_if_not_computing "cut" + (do_if_not_computing "cut" (sync (fun () -> GtkSignal.emit_unit (get_current_view()).view#as_view - GtkText.View.S.cut_clipboard))); + GtkText.View.S.cut_clipboard)))); ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback: (fun () -> GtkSignal.emit_unit (get_current_view()).view#as_view GtkText.View.S.copy_clipboard)); ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback: - (do_if_not_computing "paste" + (do_if_not_computing "paste" (sync (fun () -> try GtkSignal.emit_unit (get_current_view()).view#as_view GtkText.View.S.paste_clipboard - with _ -> prerr_endline "EMIT PASTE FAILED"))); + with _ -> prerr_endline "EMIT PASTE FAILED")))); ignore (edit_f#add_separator ()); @@ -2322,12 +2312,12 @@ let main files = *) ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: - (do_if_not_computing "complete word" + (do_if_not_computing "complete word" (sync (fun () -> ignore ( let av = out_some ((get_current_view()).analyzed_view) in av#complete_at_offset (av#get_insert)#offset - )))); + ))))); ignore(edit_f#add_separator ()); (* external editor *) @@ -2352,7 +2342,7 @@ let main files = (GMain.Timeout.add ~ms:!current.global_auto_revert_delay ~callback: (fun () -> - do_if_not_computing "revert" (fun () -> revert_f ()) (); + do_if_not_computing "revert" (sync revert_f) (); true)) in reset_revert_timer (); (* to enable statup preferences timer *) @@ -2375,7 +2365,7 @@ let main files = (GMain.Timeout.add ~ms:!current.auto_save_delay ~callback: (fun () -> - do_if_not_computing "autosave" (fun () -> auto_save_f ()) (); + do_if_not_computing "autosave" (sync auto_save_f) (); true)) in reset_auto_save_timer (); (* to enable statup preferences timer *) @@ -2444,20 +2434,6 @@ let main files = ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; -(* - add_to_menu_toolbar - "_Forward to" - ~tooltip:"Forward to" - ~key:GdkKeysyms._Right - ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error)) - `GOTO_LAST; - add_to_menu_toolbar - "_Backward to" - ~tooltip:"Backward to" - ~key:GdkKeysyms._Left - ~callback:(do_or_activate (fun a-> a#backtrack_to_insert)) - `GOTO_FIRST; -*) add_to_menu_toolbar "_Go to" ~tooltip:"Go to cursor" @@ -2581,9 +2557,9 @@ let main files = in ignore (factory#add_item menu_text ~callback: - (do_if_not_computing "simple template" + (do_if_not_computing "simple template" (sync (fun () -> let {view = view } = get_current_view () in - ignore (view#buffer#insert_interactive text)))) + ignore (view#buffer#insert_interactive text))))) in List.iter (fun l -> @@ -2616,7 +2592,7 @@ let main files = in let add_complex_template (menu_text, text, offset, len, key) = (* Templates/Lemma *) - let callback = do_if_not_computing "complex template" + let callback = do_if_not_computing "complex template" (sync (fun () -> let {view = view } = get_current_view () in if view#buffer#insert_interactive text then begin @@ -2625,7 +2601,7 @@ let main files = view#buffer#move_mark `INSERT iter; ignore (iter#nocopy#backward_chars len); view#buffer#move_mark `SEL_BOUND iter; - end) + end)) in ignore (templates_factory#add_item menu_text ~callback ?key) in @@ -2695,9 +2671,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in ignore (factory#add_item menu_text ~callback: - (do_if_not_computing "simple template" + (do_if_not_computing "simple template" (sync (fun () -> let {view = view } = get_current_view () in - ignore (view#buffer#insert_interactive text)))) + ignore (view#buffer#insert_interactive text))))) in *) ignore (templates_factory#add_separator ()); @@ -2897,7 +2873,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let detach_menu = configuration_factory#add_item "Detach _Script Window" ~callback: - (do_if_not_computing "detach script window" + (do_if_not_computing "detach script window" (sync (fun () -> let nb = notebook () in if nb#misc#toplevel#get_oid=w#coerce#get_oid then @@ -2910,7 +2886,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); nw#add_accel_group accel_group; nb#misc#reparent nw#coerce end - )) + ))) in let detach_current_view = configuration_factory#add_item @@ -3208,7 +3184,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let _ = tv2#event#connect#motion_notify ~callback: (fun e -> - (do_if_not_computing "motion notify" + (do_if_not_computing "motion notify" (sync (fun e -> let win = match tv2#get_window `WIDGET with | None -> assert false @@ -3231,7 +3207,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); it#as_iter)) tags; false)) e; - false) + false)) in change_font := (fun fd -> @@ -3243,7 +3219,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ); let about (b:GText.buffer) = (try - let image = Filename.concat lib_ide "coq.png" in + let image = lib_ide_file "coq.ico" in let startup_image = GdkPixbuf.from_file image in b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; @@ -3291,7 +3267,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* ignore (faq_m#connect#activate ~callback:(fun () -> - load (Filename.concat lib_ide "FAQ"))); + load (lib_ide_file "FAQ"))); *) resize_window := (fun () -> @@ -3360,7 +3336,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let start () = let files = Coq.init () in ignore_break (); - GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc"); + GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); (try GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc"); with Not_found -> ()); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8ec0e9e4..dc3bcf71 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml,v 1.30.2.1 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: ideutils.ml,v 1.30.2.4 2006/01/06 15:40:37 barras Exp $ *) open Preferences @@ -32,7 +32,12 @@ let prerr_endline s = let prerr_string s = if !debug then (prerr_string s;flush stderr) -let lib_ide = Filename.concat Coq_config.coqlib "ide" +let lib_ide_file f = + let coqlib = + if !Options.boot then Coq_config.coqtop + else + System.getenv_else "COQLIB" Coq_config.coqlib in + Filename.concat (Filename.concat coqlib "ide") f let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT @@ -210,10 +215,15 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) = let find_tag_limits (tag :GText.tag) (it:GText.iter) = (find_tag_start tag it , find_tag_stop tag it) -(* explanations ?? *) +(* explanations: Win32 threads won't work if events are produced + in a thread different from the thread of the Gtk loop. In this + case we must use GtkThread.async to push a callback in the + main thread. Beware that the synchronus version may produce + deadlocks. *) let async = - if Sys.os_type <> "Unix" then GtkThread.async else - (fun x -> x) + if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x) +let sync = + if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x) let stock_to_widget ?(size=`DIALOG) s = let img = GMisc.image () @@ -254,7 +264,7 @@ let browse f url = let url_for_keyword = let ht = Hashtbl.create 97 in begin try - let cin = open_in (Filename.concat lib_ide "index_urls.txt") in + let cin = open_in (lib_ide_file "index_urls.txt") in try while true do let s = input_line cin in try diff --git a/ide/ideutils.mli b/ide/ideutils.mli index d91faff4..cbdaefb9 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli,v 1.6.2.2 2005/01/21 17:21:33 herbelin Exp $ i*) +(*i $Id: ideutils.mli,v 1.6.2.4 2005/11/25 17:18:28 barras Exp $ i*) val async : ('a -> unit) -> 'a -> unit +val sync : ('a -> 'b) -> 'a -> 'b val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int @@ -24,7 +25,7 @@ val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a val is_char_start : char -> bool -val lib_ide : string +val lib_ide_file : string -> string val my_stat : string -> Unix.stats option val prerr_endline : string -> unit diff --git a/ide/undo.ml b/ide/undo.ml index 54449515..6f740667 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: undo.ml,v 1.8.2.1 2004/07/16 19:30:21 herbelin Exp $ *) +(* $Id: undo.ml,v 1.8.2.2 2005/11/16 17:22:39 barras Exp $ *) open GText open Ideutils @@ -18,7 +18,7 @@ let neg act = match act with | Insert (s,i,l) -> Delete (s,i,l) | Delete (s,i,l) -> Insert (s,i,l) -class undoable_view (tv:Gtk.text_view Gtk.obj) = +class undoable_view (tv:[>Gtk.text_view] Gtk.obj) = let undo_lock = ref true in object(self) inherit GText.view tv as super diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli new file mode 100644 index 00000000..d81d08d5 --- /dev/null +++ b/ide/undo_lablgtk_ge26.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: undo_lablgtk_ge26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*) + +(* An undoable view class *) + +class undoable_view : [> Gtk.text_view] Gtk.obj -> +object + inherit GText.view + method undo : bool + method redo : bool + method clear_undo : unit +end + +val undoable_view : + ?buffer:GText.buffer -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + undoable_view + + diff --git a/ide/undo.mli b/ide/undo_lablgtk_lt26.mli index 11613fdb..9c2176b0 100644 --- a/ide/undo.mli +++ b/ide/undo_lablgtk_lt26.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: undo.mli,v 1.4.2.2 2005/01/21 17:21:33 herbelin Exp $ i*) +(*i $Id: undo_lablgtk_lt26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*) (* An undoable view class *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6692dca5..25167865 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml,v 1.85.2.2 2004/07/16 19:30:22 herbelin Exp $ *) +(* $Id: constrextern.ml,v 1.85.2.7 2006/01/05 12:00:35 herbelin Exp $ *) (*i*) open Pp @@ -1333,7 +1333,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function subst in insert_pat_delimiters (make_pat_notation loc ntn l) key) | SynDefRule kn -> - CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn))) + let qid = shortest_qualid_of_syndef vars kn in + CPatAtom (loc,Some (Qualid (loc, qid))) with No_match -> extern_symbol_pattern allscopes vars t rules @@ -1494,21 +1495,38 @@ let rec share_fix_binders n rbl ty def = | _ -> List.rev rbl, ty, def (**********************************************************************) +(* mapping rawterms to numerals (in presence of coercions, choose the *) +(* one with no delimiter if possible) *) + +let extern_possible_numeral scopes r = + try + let (sc,n) = uninterp_numeral r in + match Symbols.availability_of_numeral sc (make_current_scopes scopes) with + | None -> None + | Some key -> Some (insert_delimiters (CNumeral(loc_of_rawconstr r,n)) key) + with No_match -> + None + +let extern_optimal_numeral scopes r r' = + let c = extern_possible_numeral scopes r in + let c' = if r==r' then None else extern_possible_numeral scopes r' in + match c,c' with + | Some n, (Some (CDelimiters _) | None) | _, Some n -> n + | _ -> raise No_match + +(**********************************************************************) (* mapping rawterms to constr_expr *) let rec extern inctx scopes vars r = + let r' = remove_coercions inctx r in try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_numeral (Rawterm.loc_of_rawconstr r) - scopes (Symbols.uninterp_numeral r) + extern_optimal_numeral scopes r r' with No_match -> - - let r = remove_coercions inctx r in - try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_symbol scopes vars r (Symbols.uninterp_notations r) - with No_match -> match r with + extern_symbol scopes vars r' (Symbols.uninterp_notations r') + with No_match -> match r' with | RRef (loc,ref) -> extern_global loc (implicits_of_global_out ref) (extern_reference loc vars ref) @@ -1605,13 +1623,15 @@ let rec extern inctx scopes vars r = | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, - (Some na,option_app (extern_type scopes (add_vname vars na)) typopt), + (option_app (fun _ -> na) typopt, + option_app (extern_type scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (Some na,option_app (extern_type scopes (add_vname vars na)) typopt), + (option_app (fun _ -> na) typopt, + option_app (extern_type scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,blv,tyv,bv) -> @@ -1709,11 +1729,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, extern inctx scopes vars c) -and extern_numeral loc scopes (sc,n) = - match Symbols.availability_of_numeral sc (make_current_scopes scopes) with - | None -> raise No_match - | Some key -> insert_delimiters (CNumeral (loc,n)) key - and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as rule)::rules -> @@ -1745,7 +1760,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subst in insert_delimiters (make_notation loc ntn l) key) | SynDefRule kn -> - CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in + CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in if args = [] then e else (* TODO: compute scopt for the extra args, in case, head is a ref *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 222ea23b..bacdb387 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml,v 1.58.2.6 2004/11/22 14:21:23 herbelin Exp $ *) +(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *) open Pp open Util @@ -621,10 +621,10 @@ let merge_impargs l args = let check_projection isproj nargs r = match (r,isproj) with - | RRef (loc, ref), Some nth -> + | RRef (loc, ref), Some _ -> (try - let n = Recordops.find_projection_nparams ref in - if nargs < nth then + let n = Recordops.find_projection_nparams ref + 1 in + if nargs < n then user_err_loc (loc,"",str "Projection has not enough parameters"); with Not_found -> user_err_loc diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index ef887d88..ceda2b47 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: syntax_def.ml,v 1.6.2.1 2004/07/16 19:30:23 herbelin Exp $ *) +(* $Id: syntax_def.ml,v 1.6.2.2 2006/01/03 20:33:31 herbelin Exp $ *) open Util open Pp @@ -39,10 +39,15 @@ let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) = add_syntax_constant kn c; Nametab.push_syntactic_definition (Nametab.Until i) sp kn; if not onlyparse then + (* Declare it to be used as (long) name *) Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c) -let open_syntax_constant i ((sp,kn),c) = - Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn +let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) = + Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn; + if not onlyparse then + (* Redeclare it to be used as (short) name in case an other (distfix) + notation was declared inbetween *) + Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c) let cache_syntax_constant d = load_syntax_constant 1 d diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8943b0b5..ac2c52cc 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.ml,v 1.31.2.1 2004/07/16 19:30:24 herbelin Exp $ i*) +(*i $Id: declarations.ml,v 1.31.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) (*i*) open Util @@ -104,6 +104,7 @@ type one_inductive_body = { } type mutual_inductive_body = { + mind_record : bool; mind_finite : bool; mind_ntypes : int; mind_hyps : section_context; @@ -139,7 +140,8 @@ let subst_mind_packet sub mbp = } let subst_mind sub mib = - { mind_finite = mib.mind_finite ; + { mind_record = mib.mind_record ; + mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (assert (mib.mind_hyps=[]); []) ; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c670fe9a..6cff3936 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli,v 1.33.2.2 2005/01/21 16:41:49 herbelin Exp $ i*) +(*i $Id: declarations.mli,v 1.33.2.3 2005/11/29 21:40:51 letouzey Exp $ i*) (*i*) open Names @@ -77,6 +77,7 @@ type one_inductive_body = { } type mutual_inductive_body = { + mind_record : bool; mind_finite : bool; mind_ntypes : int; mind_hyps : section_context; diff --git a/kernel/entries.ml b/kernel/entries.ml index d833499e..a3d3d336 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: entries.ml,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*) +(*i $Id: entries.ml,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*) (*i*) open Names @@ -49,6 +49,7 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { + mind_entry_record : bool; mind_entry_finite : bool; mind_entry_inds : one_inductive_entry list } diff --git a/kernel/entries.mli b/kernel/entries.mli index edade51a..e9bc420e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: entries.mli,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*) +(*i $Id: entries.mli,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*) (*i*) open Names @@ -49,6 +49,7 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { + mind_entry_record : bool; mind_entry_finite : bool; mind_entry_inds : one_inductive_entry list } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 88f837aa..0b1d49f5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml,v 1.59.2.1 2004/07/16 19:30:25 herbelin Exp $ *) +(* $Id: indtypes.ml,v 1.59.2.4 2005/12/30 15:58:59 barras Exp $ *) open Util open Names @@ -20,10 +20,14 @@ open Reduction open Typeops open Entries -(* [check_constructors_names id s cl] checks that all the constructors names - appearing in [l] are not present in the set [s], and returns the new set - of names. The name [id] is the name of the current inductive type, used - when reporting the error. *) +(* Same as noccur_between but may perform reductions. + Could be refined more... *) +let weaker_noccur_between env x nvars t = + if noccur_between x nvars t then Some t + else + let t' = whd_betadeltaiota env t in + if noccur_between x nvars t then Some t' + else None (************************************************************************) (* Various well-formedness check for inductive declarations *) @@ -46,6 +50,11 @@ type inductive_error = exception InductiveError of inductive_error +(* [check_constructors_names id s cl] checks that all the constructors names + appearing in [l] are not present in the set [s], and returns the new set + of names. The name [id] is the name of the current inductive type, used + when reporting the error. *) + let check_constructors_names id = let rec check idset = function | [] -> idset @@ -337,9 +346,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); - if not (noccur_between n ntypes b) then - raise (IllFormedInd (LocalNonPos n)); - check_pos (ienv_push_var ienv (na, b, mk_norec)) d + (match weaker_noccur_between env n ntypes b with + None -> raise (IllFormedInd (LocalNonPos n)); + | Some b -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) d) | Rel k -> let (ra,rarg) = try List.nth ra_env (k-1) @@ -481,7 +491,7 @@ let allowed_sorts env issmall isunit = function then logical_sorts else impredicative_sorts else logical_sorts -let build_inductive env env_ar finite inds recargs cst = +let build_inductive env env_ar record finite inds recargs cst = let ntypes = Array.length inds in (* Compute the set of used section variables *) let ids = @@ -527,7 +537,8 @@ let build_inductive env env_ar finite inds recargs cst = } in let packets = array_map2 build_one_packet inds recargs in (* Build the mutual inductive *) - { mind_ntypes = ntypes; + { mind_record = record; + mind_ntypes = ntypes; mind_finite = finite; mind_hyps = hyps; mind_packets = packets; @@ -544,5 +555,6 @@ let check_inductive env mie = (* Then check positivity conditions *) let recargs = check_positivity env_arities inds in (* Build the inductive packets *) - build_inductive env env_arities mie.mind_entry_finite inds recargs cst + build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite + inds recargs cst diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4f180599..0f8c0d54 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml,v 1.76.2.1 2004/07/16 19:30:26 herbelin Exp $ *) +(* $Id: safe_typing.ml,v 1.76.2.2 2005/11/23 14:46:08 barras Exp $ *) open Util open Names @@ -427,11 +427,13 @@ type compiled_library = (* We check that only initial state Require's were performed before [start_library] was called *) +let is_empty senv = + senv.revsign = [] && + senv.modinfo.msid = initial_msid && + senv.modinfo.variant = NONE + let start_library dir senv = - if not (senv.revsign = [] && - senv.modinfo.msid = initial_msid && - senv.modinfo.variant = NONE) - then + if not (is_empty senv) then anomaly "Safe_typing.start_library: environment should be empty"; let dir_path,l = match (repr_dirpath dir) with diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 84b98984..b973fcde 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: safe_typing.mli,v 1.33.2.1 2004/07/16 19:30:26 herbelin Exp $ i*) +(*i $Id: safe_typing.mli,v 1.33.2.2 2005/11/23 14:46:08 barras Exp $ i*) (*i*) open Names @@ -29,6 +29,8 @@ val env_of_safe_env : safe_environment -> Environ.env val empty_environment : safe_environment +val is_empty : safe_environment -> bool + (* Adding and removing local declarations (Local or Variables) *) val push_named_assum : identifier * types -> safe_environment -> diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 825ae8fa..835226fb 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml,v 1.11.2.1 2004/07/16 19:30:26 herbelin Exp $ i*) +(*i $Id: subtyping.ml,v 1.11.2.2 2005/11/29 21:40:52 letouzey Exp $ i*) (*i*) open Util @@ -132,6 +132,34 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = in if kn1 <> kn2 then error () end; + (* we check that records and their field names are preserved. *) + (* To stay compatible, we don't fail but only issue a warning. *) + if mib1.mind_record <> mib2.mind_record then begin + let sid = string_of_id mib1.mind_packets.(0).mind_typename in + Pp.warning + (sid^": record is implemented as an inductive type or conversely.\n"^ + "Beware that extraction cannot handle this situation.\n") + end; + if mib1.mind_record then begin + let rec names_prod_letin t = match kind_of_term t with + | Prod(n,_,t) -> n::(names_prod_letin t) + | LetIn(n,_,_,t) -> n::(names_prod_letin t) + | Cast(t,_) -> names_prod_letin t + | _ -> [] + in + assert (Array.length mib1.mind_packets = 1); + assert (Array.length mib2.mind_packets = 1); + assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); + assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + let fields1 = names_prod_letin mib1.mind_packets.(0).mind_user_lc.(0) + and fields2 = names_prod_letin mib2.mind_packets.(0).mind_user_lc.(0) in + if fields1 <> fields2 then + let sid = string_of_id mib1.mind_packets.(0).mind_typename in + Pp.warning + (sid^": record has different field names in its signature and "^ + "implemantation.\n"^ + "Beware that extraction cannot handle this situation.\n"); + end; (* we first check simple things *) let cst = array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets diff --git a/kernel/univ.ml b/kernel/univ.ml index d46609c8..5e9fbd81 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml,v 1.17.10.1 2004/07/16 19:30:28 herbelin Exp $ *) +(* $Id: univ.ml,v 1.17.10.3 2005/09/08 12:27:46 herbelin Exp $ *) (* Universes are stratified by a partial ordering $\ge$. Let $\~{}$ be the associated equivalence. We also have a strict ordering @@ -57,7 +57,7 @@ let pr_uni = function | Max (gel,gtl) -> str "max(" ++ prlist_with_sep pr_coma pr_uni_level gel ++ - if gel <> [] & gtl <> [] then pr_coma () else mt () ++ + (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++ prlist_with_sep pr_coma (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++ str ")" @@ -69,9 +69,8 @@ let super = function | Variable u -> Max ([],[u]) | Max _ -> - anomaly ("Cannot take the successor of a non variable universes:\n"^ - "you are probably typing a type already known to be the type\n"^ - "of a user-provided term; if you really need this, please report") + anomaly ("Cannot take the successor of a non variable universes\n"^ + "(maybe a bugged tactic)") (* returns the least upper bound of universes u and v. If they are not constrained, then a new universe is created. @@ -412,6 +411,7 @@ let pr_arc = function pr_uni_level u ++ str " " ++ v 0 (prlist_with_sep pr_spc (fun v -> str "> " ++ pr_uni_level v) gt ++ + (if ge <> [] & gt <> [] then spc () else mt ()) ++ prlist_with_sep pr_spc (fun v -> str ">= " ++ pr_uni_level v) ge) ++ fnl () | Equiv (u,v) -> diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 0947f5fb..7ea3ff66 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -20,7 +20,9 @@ let unloc (b,e) = let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in (* Ensure that we unpack a char location that was encoded as a line-col location by make_loc *) +(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954 assert (dummy_loc = (b,e) or make_loc loc = (b,e)); +*) loc end else diff --git a/lib/gmapl.ml b/lib/gmapl.ml index dcb2eb94..5eb4e110 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmapl.ml,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ *) +(* $Id: gmapl.ml,v 1.2.16.2 2006/01/03 20:31:16 herbelin Exp $ *) open Util @@ -21,7 +21,7 @@ let fold = Gmap.fold let add x y m = try let l = Gmap.find x m in - Gmap.add x (if List.mem y l then l else y::l) m + Gmap.add x (y::list_except y l) m with Not_found -> Gmap.add x [y] m diff --git a/lib/system.ml b/lib/system.ml index fd782fe6..9bbcc308 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml,v 1.31.8.1 2004/07/16 19:30:31 herbelin Exp $ *) +(* $Id: system.ml,v 1.31.8.3 2006/01/10 17:06:23 barras Exp $ *) open Pp open Util @@ -22,6 +22,8 @@ let safe_getenv_def var def = flush Pervasives.stdout; def +let getenv_else s dft = try Sys.getenv s with Not_found -> dft + let home = (safe_getenv_def "HOME" ".") let safe_getenv n = safe_getenv_def n ("$"^n) @@ -60,6 +62,34 @@ let glob s = expand_macros true s 0 type physical_path = string type load_path = physical_path list +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + (* All subdirectories, recursively *) let exists_dir dir = diff --git a/lib/system.mli b/lib/system.mli index 86d78b52..dc172b70 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: system.mli,v 1.17.16.1 2004/07/16 19:30:31 herbelin Exp $ i*) +(*i $Id: system.mli,v 1.17.16.3 2006/01/10 17:06:23 barras Exp $ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field @@ -16,6 +16,8 @@ type physical_path = string type load_path = physical_path list +val canonical_path_name : string -> physical_path + val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool val where_in_path : load_path -> string -> physical_path * string @@ -24,7 +26,7 @@ val make_suffix : string -> string -> string val file_readable_p : string -> bool val glob : string -> string - +val getenv_else : string -> string -> string val home : string val exists_dir : string -> bool diff --git a/library/declare.ml b/library/declare.ml index 8b9dfeda..cfa8890a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml,v 1.128.2.1 2004/07/16 19:30:34 herbelin Exp $ *) +(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *) open Pp open Util @@ -271,6 +271,7 @@ let dummy_one_inductive_entry mie = { (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_inductive_entry m = { + mind_entry_record = false; mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds } diff --git a/library/declaremods.ml b/library/declaremods.ml index b968a432..2e8fb0a7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml,v 1.18.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*) open Pp open Util @@ -502,17 +502,17 @@ let end_module id = let dir = fst oldprefix in let msid = msid_of_prefix oldprefix in - let substobjs = try + let substobjs, keep, special = try match res_o with | None -> - empty_subst, mbids, msid, substitute + (empty_subst, mbids, msid, substitute), keep, special | Some (MTEident ln) -> - abstract_substobjs mbids (KNmap.find ln (!modtypetab)) + abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], [] | Some (MTEsig (msid,_)) -> todo "Anonymous signatures not supported"; - empty_subst, mbids, msid, [] + (empty_subst, mbids, msid, []), keep, special | Some (MTEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs mty) + abstract_substobjs mbids (get_modtype_substobjs mty), [], [] | Some (MTEfunsig _) -> anomaly "Funsig cannot be here..." with diff --git a/library/global.ml b/library/global.ml index bfa9335c..8694d7af 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml,v 1.43.2.1 2004/07/16 19:30:35 herbelin Exp $ *) +(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *) open Util open Names @@ -25,6 +25,8 @@ let safe_env () = !global_env let env () = env_of_safe_env !global_env +let env_is_empty () = is_empty !global_env + let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); diff --git a/library/global.mli b/library/global.mli index 1da5965c..007986d1 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli,v 1.40.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: global.mli,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*) (*i*) open Names @@ -32,6 +32,8 @@ val env : unit -> Environ.env val universes : unit -> universes val named_context : unit -> Sign.named_context +val env_is_empty : unit -> bool + (*s Extending env with variables and local definitions *) val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints diff --git a/library/lib.ml b/library/lib.ml index a9f864ef..c46634f4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml,v 1.63.2.3 2004/11/22 14:21:23 herbelin Exp $ *) +(* $Id: lib.ml,v 1.63.2.4 2005/11/04 09:02:38 herbelin Exp $ *) open Pp open Util @@ -555,8 +555,7 @@ let library_part ref = let dir,_ = repr_path sp in match ref with | VarRef id -> - anomaly "TODO"; - extract_dirpath_prefix (sections_depth ()) (cwd ()) + anomaly "library_part not supported on local variables" | _ -> if is_dirpath_prefix_of dir (cwd ()) then (* Not yet (fully) discharged *) diff --git a/library/library.ml b/library/library.ml index cbc8874a..aaed4545 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml,v 1.79.2.2 2004/11/17 14:01:26 herbelin Exp $ *) +(* $Id: library.ml,v 1.79.2.5 2006/01/10 17:06:23 barras Exp $ *) open Pp open Util @@ -29,53 +29,26 @@ let load_path = ref ([],[] : System.physical_path list * logical_path list) let get_load_path () = fst !load_path -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - let find_logical_path phys_dir = - let phys_dir = canonical_path_name phys_dir in + let phys_dir = System.canonical_path_name phys_dir in match list_filter2 (fun p d -> p = phys_dir) !load_path with | _,[dir] -> dir | _,[] -> Nameops.default_root_prefix | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) let remove_path dir = + let dir = System.canonical_path_name dir in load_path := list_filter2 (fun p d -> p <> dir) !load_path let add_load_path_entry (phys_path,coq_path) = - let phys_path = canonical_path_name phys_path in + let phys_path = System.canonical_path_name phys_path in match list_filter2 (fun p d -> p = phys_path) !load_path with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = canonical_path_name Filename.current_dir_name + (phys_path = System.canonical_path_name Filename.current_dir_name && coq_path = Nameops.default_root_prefix) then begin @@ -290,8 +263,8 @@ let (in_import, out_import) = (************************************************************************) (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number7 = 07992 (* V8.0 final old syntax *) -let vo_magic_number8 = 08002 (* V8.0 final new syntax *) +let vo_magic_number7 = 07993 (* V8.0pl3 final old syntax *) +let vo_magic_number8 = 08003 (* V8.0pl3 final new syntax *) let (raw_extern_library7, raw_intern_library7) = System.raw_extern_intern vo_magic_number7 ".vo" @@ -453,13 +426,8 @@ let rec_intern_by_filename_only id f = m.library_name let locate_qualified_library qid = - (* Look if loaded in current environment *) - try - let dir = Nametab.full_name_module qid in - (LibLoaded, dir, library_full_filename dir) - with Not_found -> - (* Look if in loadpath *) try + (* Search library in loadpath *) let dir, base = repr_qualid qid in let loadpath = if repr_dirpath dir = [] then get_load_path () @@ -470,7 +438,12 @@ let locate_qualified_library qid = if loadpath = [] then raise LibUnmappedDir; let name = (string_of_id base)^".vo" in let path, file = System.where_in_path loadpath name in - (LibInPath, extend_dirpath (find_logical_path path) base, file) + let dir = extend_dirpath (find_logical_path path) base in + (* Look if loaded *) + try + (LibLoaded, dir, library_full_filename dir) + with Not_found -> + (LibInPath, dir, file) with Not_found -> raise LibNotFound let rec_intern_qualified_library (loc,qid) = diff --git a/library/nametab.ml b/library/nametab.ml index f009d867..4bd0cb3f 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nametab.ml,v 1.48.2.1 2004/07/16 19:30:36 herbelin Exp $ *) +(* $Id: nametab.ml,v 1.48.2.2 2005/11/21 09:16:27 herbelin Exp $ *) open Util open Pp @@ -472,9 +472,9 @@ let shortest_qualid_of_global ctx ref = let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_syndef kn = +let shortest_qualid_of_syndef ctx kn = let sp = sp_of_syntactic_definition kn in - SpTab.shortest_qualid Idset.empty sp !the_ccitab + SpTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_module mp = let dir = MPmap.find mp !the_modrevtab in diff --git a/library/nametab.mli b/library/nametab.mli index 08a9d1bb..4cea1d40 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli,v 1.43.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) +(*i $Id: nametab.mli,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*) (*i*) open Util @@ -144,7 +144,7 @@ val full_name_module : qualid -> dir_path val sp_of_syntactic_definition : kernel_name -> section_path val shortest_qualid_of_global : Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : kernel_name -> qualid +val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid val dir_of_mp : module_path -> dir_path diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 7a151c1a..09889d40 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml,v 1.48.2.3 2004/11/26 19:37:59 herbelin Exp $ *) +(* $Id: egrammar.ml,v 1.48.2.4 2005/12/23 22:16:46 herbelin Exp $ *) open Pp open Util @@ -30,12 +30,13 @@ type all_grammar_command = | TacticGrammar of (string * (string * grammar_production list) * (Names.dir_path * Tacexpr.raw_tactic_expr)) - list + list * (string * Genarg.argument_type list * + (string * Pptactic.grammar_terminals)) list let subst_all_grammar_command subst = function | Notation _ -> anomaly "Notation not in GRAMMAR summary" | Grammar gc -> Grammar (subst_grammar_command subst gc) - | TacticGrammar g -> TacticGrammar g (* TODO ... *) + | TacticGrammar (g,p) -> TacticGrammar (g,p) (* TODO ... *) let (grammar_state : all_grammar_command list ref) = ref [] @@ -419,7 +420,7 @@ let extend_grammar gram = (match gram with | Notation (_,a) -> extend_constr_notation a | Grammar g -> extend_grammar_rules g - | TacticGrammar l -> add_tactic_entries l); + | TacticGrammar (l,_) -> add_tactic_entries l); grammar_state := gram :: !grammar_state let reset_extend_grammars_v8 () = diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 0009b4b6..ade91453 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli,v 1.14.2.5 2004/11/27 09:25:44 herbelin Exp $ i*) +(*i $Id: egrammar.mli,v 1.14.2.6 2005/12/23 22:16:46 herbelin Exp $ i*) (*i*) open Util @@ -28,7 +28,8 @@ type all_grammar_command = | TacticGrammar of (string * (string * grammar_production list) * (Names.dir_path * Tacexpr.raw_tactic_expr)) - list + list * (string * Genarg.argument_type list * + (string * Pptactic.grammar_terminals)) list val extend_grammar : all_grammar_command -> unit diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index adc26532..fe579e98 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constrnew.ml4,v 1.41.2.2 2004/11/17 12:48:35 herbelin Exp $ *) +(* $Id: g_constrnew.ml4,v 1.41.2.4 2005/09/21 14:47:33 herbelin Exp $ *) open Pcoq open Constr @@ -285,7 +285,9 @@ GEXTEND Gram [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] ; pattern: - [ "10" LEFTA + [ "200" RIGHTA [ ] + | "99" RIGHTA [ ] + | "10" LEFTA [ p = pattern ; lp = LIST1 (pattern LEVEL "0") -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 9c8d1675..7492ac8c 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltacnew.ml4,v 1.22.2.2 2004/07/16 19:30:38 herbelin Exp $ *) +(* $Id: g_ltacnew.ml4,v 1.22.2.3 2005/06/21 15:31:12 herbelin Exp $ *) open Pp open Util @@ -43,7 +43,7 @@ let tactic_expr = Gram.Entry.create "tactic:tactic_expr" if not !Options.v7 then GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr tactic_arg; + GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; tactic_expr: [ "5" LEFTA @@ -108,14 +108,20 @@ GEXTEND Gram | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; may_eval_arg: + [ [ c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + ; + constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrMayEval (ConstrEval (rtc,c)) + ConstrEval (rtc,c) | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrMayEval (ConstrContext (id,c)) + ConstrContext (id,c) | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrMayEval (ConstrTypeOf c) - | IDENT "fresh"; s = OPT STRING -> - TacFreshId s ] ] + ConstrTypeOf c ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> c + | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a1559572..fd64defc 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tactic.ml4,v 1.83.2.4 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: g_tactic.ml4,v 1.83.2.5 2005/05/15 12:47:04 herbelin Exp $ *) open Pp open Ast @@ -306,14 +306,14 @@ GEXTEND Gram (* Automation tactic *) | IDENT "Trivial"; db = hintbases -> TacTrivial db - | IDENT "Auto"; n = OPT natural; db = hintbases -> TacAuto (n, db) + | IDENT "Auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db) | IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n | IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id) | IDENT "DHyp"; id = identref -> TacDestructHyp (false,id) | IDENT "DConcl" -> TacDestructConcl | IDENT "SuperAuto"; l = autoargs -> TacSuperAuto l - | IDENT "Auto"; n = OPT natural; IDENT "Decomp"; p = OPT natural -> + | IDENT "Auto"; n = OPT int_or_var; IDENT "Decomp"; p = OPT natural -> TacDAuto (n, p) (* Context management *) diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 643be98d..5ffd2fd7 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tacticnew.ml4,v 1.35.2.6 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: g_tacticnew.ml4,v 1.35.2.7 2005/05/15 12:47:05 herbelin Exp $ *) open Pp open Ast @@ -340,7 +340,7 @@ GEXTEND Gram (* Automation tactic *) | IDENT "trivial"; db = hintbases -> TacTrivial db - | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db) + | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db) (* Obsolete since V8.0 | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n @@ -349,7 +349,7 @@ GEXTEND Gram | IDENT "dconcl" -> TacDestructConcl | IDENT "superauto"; l = autoargs -> TacSuperAuto l *) - | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural -> + | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural -> TacDAuto (n, p) (* Context management *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index b5ab2387..a8922536 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4,v 1.80.2.3 2005/01/15 14:56:53 herbelin Exp $ i*) +(*i $Id: pcoq.ml4,v 1.80.2.4 2005/06/21 15:31:12 herbelin Exp $ i*) open Pp open Util @@ -379,7 +379,8 @@ module Tactic = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = make_gen_entry utactic rawwit_bindings "bindings" - let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg" +(*v7*) let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg" +(*v8*) let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval" let quantified_hypothesis = make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis" let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 361137f4..15a2c2cc 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli,v 1.63.2.2 2005/01/15 14:56:53 herbelin Exp $ i*) +(*i $Id: pcoq.mli,v 1.63.2.3 2005/06/21 15:31:12 herbelin Exp $ i*) open Util open Names @@ -160,7 +160,8 @@ module Tactic : val castedopenconstr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e - val constrarg : (constr_expr,reference) may_eval Gram.Entry.e +(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e +(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1d7a9428..4103ea00 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *) open Pp open Names @@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) = Hashtbl.add prtac_tab_v7 (s,tags) prods; if for_v8 then Hashtbl.add prtac_tab (s,tags) prods +let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags) + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -536,7 +538,8 @@ and pr_atom1 = function | TacTrivial (Some []) as x -> pr_atom0 x | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db) | TacAuto (None,Some []) as x -> pr_atom0 x - | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAuto (n,db) -> + hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) | TacAutoTDB None as x -> pr_atom0 x | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n) | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id) @@ -546,7 +549,8 @@ and pr_atom1 = function hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2) | TacDAuto (n,p) -> - hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p) + hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ + pr_opt int p) (* Context management *) | TacClear l -> diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index b9cf7401..5c3035ba 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pptactic.mli,v 1.9.2.2 2005/01/21 17:19:37 herbelin Exp $ i*) +(*i $Id: pptactic.mli,v 1.9.2.3 2005/12/23 22:16:46 herbelin Exp $ i*) open Pp open Genarg @@ -46,6 +46,8 @@ type grammar_terminals = string option list val declare_extra_tactic_pprule : bool -> string -> argument_type list * (string * grammar_terminals) -> unit +val exists_extra_tactic_pprule : string -> argument_type list -> bool + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 169eff94..1505745c 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml,v 1.50.2.1 2004/07/16 19:30:40 herbelin Exp $ *) +(* $Id: prettyp.ml,v 1.50.2.2 2005/11/21 09:16:28 herbelin Exp $ *) open Pp open Util @@ -180,8 +180,10 @@ let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in let module N = Nametab in let expand = function - | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref - | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in + | TrueGlobal ref -> + Term ref, N.shortest_qualid_of_global Idset.empty ref + | SyntacticDef kn -> + Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in match List.map expand (N.extended_locate_all qid) with | [] -> let (dir,id) = repr_qualid qid in @@ -329,7 +331,7 @@ let print_constant_with_infos sp = let print_inductive sp = (print_mutual sp) let print_syntactic_def sep kn = - let qid = Nametab.shortest_qualid_of_syndef kn in + let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in let c = Syntax_def.search_syntactic_definition dummy_loc kn in (str (if !Options.v7 then "Syntactic Definition " else "Notation ") ++ pr_qualid qid ++ str sep ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a278e3d5..e8e1830a 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4,v 1.47.2.5 2005/01/15 14:56:54 herbelin Exp $ *) +(* $Id: q_coqast.ml4,v 1.47.2.6 2005/05/15 12:47:05 herbelin Exp $ *) open Util open Names @@ -454,7 +454,7 @@ let rec mlexpr_of_atomic_tactic = function (* Automation tactics *) | Tacexpr.TacAuto (n,l) -> - let n = mlexpr_of_option mlexpr_of_int n in + let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in <:expr< Tacexpr.TacAuto $n$ $l$ >> (* diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 378eee30..4aff508f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *) +(* $Id: cases.ml,v 1.111.2.5 2005/04/29 16:31:03 herbelin Exp $ *) open Util open Names @@ -171,10 +171,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = open Pp let mssg_may_need_inversion () = - str "This pattern-matching is not exhaustive." - -let mssg_this_case_cannot_occur () = - "This pattern-matching is not exhaustive." + str "Found a matching with no clauses on a term unknown to have an empty inductive type" (* Utils *) let make_anonymous_patvars = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f214388f..be78eb2c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml,v 1.38.6.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: coercion.ml,v 1.38.6.2 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Names @@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 = (* appliquer le chemin de coercions p à hj *) let apply_coercion env p hj typ_cl = - if !compter then begin - nbpathc := !nbpathc +1; - nbcoer := !nbcoer + (List.length p) - end; try fst (List.fold_left (fun (ja,typ_cl) i -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 41f63ace..040a185e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml,v 1.75.2.4 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: detyping.ml,v 1.75.2.5 2005/09/06 14:30:41 herbelin Exp $ *) open Pp open Util @@ -446,7 +446,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch = let make_pat x avoid env b ids = if force_wildcard () & noccurn 1 b then PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids - else + else let id = next_name_away_with_default "x" x avoid in PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids in @@ -487,6 +487,6 @@ and detype_binder tenv bk avoid env na ty c = concrete_name (fst tenv) avoid env na c in let r = detype tenv avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r) - | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r) - | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r) + | BProd -> RProd (dummy_loc, na',detype tenv avoid env ty, r) + | BLambda -> RLambda (dummy_loc, na',detype tenv avoid env ty, r) + | BLetIn -> RLetIn (dummy_loc, na',detype tenv avoid env ty, r) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0ee95a0f..2264f82b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *) +(* $Id: evarconv.ml,v 1.44.6.3 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Names @@ -380,21 +380,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = (new_isevar isevars env dloc (substl ks b)) :: ks) [] bs in - if (list_for_all2eq - (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) - us2 us) - & - (list_for_all2eq - (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) - params1 params) - & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) - & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) - then - (*TR*) (if !compter then (nbstruc:=!nbstruc+1; - nbimplstruc:=!nbimplstruc+(List.length ks);true) - else true) - else false - + (list_for_all2eq + (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) + us2 us) + & + (list_for_all2eq + (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) + params1 params) + & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) + & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) + let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2 diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 36df9c8a..bb0e74bb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml,v 1.123.2.3 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: pretyping.ml,v 1.123.2.5 2005/11/29 21:40:52 letouzey Exp $ *) open Pp open Util @@ -162,13 +162,13 @@ let strip_meta id = (* For Grammar v7 compatibility *) let pretype_id loc env (lvar,unbndltacvars) id = let id = strip_meta id in (* May happen in tactics defined by Grammar *) try - List.assoc id lvar - with Not_found -> - try let (n,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = type_app (lift n) typ } with Not_found -> try + List.assoc id lvar + with Not_found -> + try let (_,_,typ) = lookup_named id env in { uj_val = mkVar id; uj_type = typ } with Not_found -> @@ -238,7 +238,6 @@ let rec pretype tycon env isevars lvar = function anomaly "Found a pattern variable in a rawterm to type" | RHole (loc,k) -> - if !compter then nbimpl:=!nbimpl+1; (match tycon with | Some ty -> { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty } @@ -892,7 +891,6 @@ let rec pretype tycon env isevars lvar = function (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *) and pretype_type valcon env isevars lvar = function | RHole loc -> - if !compter then nbimpl:=!nbimpl+1; (match valcon with | Some v -> let s = diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f34d5624..3e73cfee 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml,v 1.26.2.1 2004/07/16 19:30:46 herbelin Exp $ *) +(* $Id: recordops.ml,v 1.26.2.2 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Pp @@ -20,14 +20,6 @@ open Libobject open Library open Classops -let nbimpl = ref 0 -let nbpathc = ref 0 -let nbcoer = ref 0 -let nbstruc = ref 0 -let nbimplstruc = ref 0 - -let compter = ref false - (*s Une structure S est un type inductif non récursif à un seul constructeur (de nom par défaut Build_S) *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 66c1f34d..a458b7b3 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli,v 1.15.2.1 2004/07/16 19:30:46 herbelin Exp $ i*) +(*i $Id: recordops.mli,v 1.15.2.2 2005/11/29 21:40:52 letouzey Exp $ i*) (*i*) open Names @@ -18,13 +18,6 @@ open Libobject open Library (*i*) -val nbimpl : int ref -val nbpathc : int ref -val nbcoer : int ref -val nbstruc : int ref -val nbimplstruc : int ref -val compter : bool ref - type struc_typ = { s_CONST : identifier; s_PARAM : int; diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f225e79f..e8bde1f3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml,v 1.75.2.6 2004/12/29 10:17:10 herbelin Exp $ *) +(* $Id: tacred.ml,v 1.75.2.7 2005/11/02 13:18:43 herbelin Exp $ *) open Pp open Util @@ -204,13 +204,14 @@ let invert_name labs l na0 env sigma ref = function match refi with | None -> None | Some ref -> - match reference_opt_value sigma env ref with + try match reference_opt_value sigma env ref with | None -> None | Some c -> let labs',ccl = decompose_lam c in let _, l' = whd_betalet_stack ccl in let labs' = List.map snd labs' in if labs' = labs & l = l' then Some ref else None + with Not_found (* Undefined ref *) -> None else Some ref | Anonymous -> None (* Actually, should not occur *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 3cc44a0f..cefeb8ae 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *) open Pp open Util @@ -54,7 +54,8 @@ open Pretype_errors let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true + Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) | + Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true | _ -> false let error_cannot_unify (m,n) = @@ -67,16 +68,9 @@ let check = ref false let without_check tac gl = let c = !check in check := false; - let r = tac gl in - check := c; - r + try let r = tac gl in check := c; r with e -> check := c; raise e -let with_check tac gl = - let c = !check in - check := true; - let r = tac gl in - check := c; - r +let with_check = Options.with_option check (************************************************************************) (************************************************************************) @@ -405,9 +399,13 @@ let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id (fun sign (_,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) && - not (option_compare (is_conv env sigma) b c) then - error "convert-hyp rule passed non-converting term"; + if !check && not (is_conv env sigma bt ct) then + (* Just a warning in V8.0bugfix for compatibility *) + msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ + str " (not well-typed in current signature)"); + if !check && not (option_compare (is_conv env sigma) b c) then + msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++ + str " (not well-typed in current signature)"); add_named_decl d sign) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 55f11d52..785e6dd4 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml,v 1.67.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *) open Pp open Util @@ -188,12 +188,8 @@ let lookup_tactic s = (* refiner r is a tactic applying the rule r *) -let bad_subproof () = - anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") - let check_subproof_connection gl spfl = - if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) - then (bad_subproof (); false) else true + list_for_all2eq (fun g pf -> g=pf.goal) gl spfl let abstract_tactic_expr te tacfun gls = let (sgl_sigma,v) = tacfun gls in @@ -778,9 +774,13 @@ let extract_pftreestate pts = (str"Cannot extract from a proof-tree in which we have descended;" ++ spc () ++ str"Please ascend to the root"); let pfterm,subgoals = extract_open_pftreestate pts in - if subgoals <> [] then + let exl = Evd.non_instantiated pts.tpfsigma in + if subgoals <> [] or exl <> [] then errorlabstrm "extract_proof" - (str "Attempt to save an incomplete proof"); + (if subgoals <> [] then + str "Attempt to save an incomplete proof" + else + str "Attempt to save a proof with existential variables still non-instantiated"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env pts.tpfsigma pfterm (*** diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 60a0a937..cd8d34db 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml,v 1.33.2.2 2005/01/21 17:14:09 herbelin Exp $ i*) +(*i $Id: tacexpr.ml,v 1.33.2.3 2005/05/15 12:47:04 herbelin Exp $ i*) open Names open Topconstr @@ -146,12 +146,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Automation tactics *) | TacTrivial of string list option - | TacAuto of int option * string list option + | TacAuto of int or_var option * string list option | TacAutoTDB of int option | TacDestructHyp of (bool * identifier located) | TacDestructConcl | TacSuperAuto of (int option * reference list * bool * bool) - | TacDAuto of int option * int option + | TacDAuto of int or_var option * int option (* Context management *) | TacClear of 'id list diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 78306877..ccb06769 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml,v 1.28.2.1 2004/07/16 19:30:50 herbelin Exp $ *) +(* $Id: coqmktop.ml,v 1.28.2.2 2005/11/04 08:20:57 herbelin Exp $ *) (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the @@ -189,7 +189,7 @@ let parse_args () = coqide := true; parse (op,fl) rem | "-v8" :: rem -> parse (op,fl) rem | "-echo" :: rem -> echo := true ; parse (op,fl) rem - | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' -> + | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> begin match rem' with | a :: rem -> parse (a::o::op,fl) rem diff --git a/tactics/auto.ml b/tactics/auto.ml index b530178e..d7130f35 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml,v 1.63.2.2 2004/12/06 11:25:21 herbelin Exp $ *) +(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *) open Pp open Util @@ -812,7 +812,10 @@ let gen_auto n dbnames = | None -> full_auto n | Some l -> auto n l -let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l) +let inj_or_var = option_app (fun n -> Genarg.ArgArg n) + +let h_auto n l = + Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l) (**************************************************************************) (* The "destructing Auto" from Eduardo *) @@ -839,7 +842,8 @@ let dauto = function | Some n, Some p -> dautomatic p n | None, Some p -> dautomatic p !default_search_depth -let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p)) +let h_dauto (n,p) = + Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p)) (***************************************) (*** A new formulation of Auto *********) diff --git a/tactics/inv.ml b/tactics/inv.ml index 54ce467c..e4bab195 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml,v 1.53.2.1 2004/07/16 19:30:53 herbelin Exp $ *) +(* $Id: inv.ml,v 1.53.2.3 2005/09/08 12:28:00 herbelin Exp $ *) open Pp open Util @@ -135,9 +135,8 @@ let make_inv_predicate env sigma indf realargs id status concl = else make_iterated_tuple env' sigma (ai,ati) (xi,ti) in - let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in let sort = get_sort_of env sigma concl in - let eq_term = find_eq_pattern type_type_rhs sort in + let eq_term = Coqlib.build_coq_eq () in let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist in @@ -191,12 +190,14 @@ let make_inv_predicate env sigma indf realargs id status concl = and introduces generalized hypotheis. Precondition: t=(mkVar id) *) -let rec dependent_hyps id idlist sign = +let rec dependent_hyps id idlist gl = let rec dep_rec =function | [] -> [] - | (id1,_,id1ty as d1)::l -> - if occur_var (Global.env()) id id1ty - then d1 :: dep_rec l + | (id1,_,_)::l -> + (* Update the type of id1: it may have been subject to rewriting *) + let d = pf_get_hyp gl id1 in + if occur_var_in_decl (Global.env()) id d + then d :: dep_rec l else dep_rec l in dep_rec idlist @@ -281,7 +282,7 @@ Nota: with Inversion_clear, only four useless hypotheses *) let generalizeRewriteIntros tac depids id gls = - let dids = dependent_hyps id depids (pf_env gls) in + let dids = dependent_hyps id depids gls in (tclTHENSEQ [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4f8e7d7c..245b5a5b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml,v 1.84.2.8 2005/01/15 14:56:54 herbelin Exp $ *) +(* $Id: tacinterp.ml,v 1.84.2.11 2005/11/04 09:01:27 herbelin Exp $ *) open Constrintern open Closure @@ -440,20 +440,18 @@ let intern_constr_reference strict ist = function let loc,qid = qualid_of_reference r in RRef (loc,locate_reference qid), if strict then None else Some (CRef r) -let intern_reference strict ist = function - | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id) - | r -> - (try Reference (intern_tac_ref ist r) +let intern_reference strict ist r = + (try Reference (intern_tac_ref ist r) + with Not_found -> + (try + ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> - (try - ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) - with Not_found -> - (match r with - | Ident (loc,id) when not strict -> - IntroPattern (IntroIdentifier id) - | _ -> - let (loc,qid) = qualid_of_reference r in - error_global_not_found_loc loc qid))) + (match r with + | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id) + | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id) + | _ -> + let (loc,qid) = qualid_of_reference r in + error_global_not_found_loc loc qid))) let rec intern_intro_pattern lf ist = function | IntroOrAndPattern l -> @@ -668,12 +666,12 @@ let rec intern_atomic lf ist x = (* Automation tactics *) | TacTrivial l -> TacTrivial l - | TacAuto (n,l) -> TacAuto (n,l) + | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) - | TacDAuto (n,p) -> TacDAuto (n,p) + | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p) (* Derived basic tactics *) | TacSimpleInduction (h,ids) -> @@ -1558,8 +1556,7 @@ and interp_match_context ist g lr lmr = | e when is_match_catchable e -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" (str - "No matching clauses for match goal") + errorlabstrm "Tacinterp.apply_match_context" (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Debug On\" for more info)" @@ -1744,12 +1741,12 @@ and interp_atomic ist gl = function (* Automation tactics *) | TacTrivial l -> Auto.h_trivial l - | TacAuto (n, l) -> Auto.h_auto n l + | TacAuto (n, l) -> Auto.h_auto (option_app (interp_int_or_var ist) n) l | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 - | TacDAuto (n,p) -> Auto.h_dauto (n,p) + | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p) (* Derived basic tactics *) | TacSimpleInduction (h,ids) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b6eaf015..2ba09e52 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *) +(* $Id: tactics.ml,v 1.162.2.7 2005/07/13 16:18:57 herbelin Exp $ *) open Pp open Util @@ -220,8 +220,16 @@ let pattern_option l = reduct_option (pattern_occs l) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) +let needs_check = function + (* Expansion is not necessarily well-typed: e.g. expansion of t into x is + not well-typed in [H:(P t); x:=t |- G] because x is defined after H *) + | Fold _ -> true + | _ -> false + let reduce redexp cl goal = - redin_combinator (reduction_of_redexp redexp) cl goal + (if needs_check redexp then with_check else (fun x -> x)) + (redin_combinator (reduction_of_redexp redexp) cl) + goal (* Unfolding occurrences of a constant *) @@ -741,7 +749,7 @@ let letin_tac with_eq name c occs gl = if not (mem_named_context x (pf_hyps gl)) then x else error ("The variable "^(string_of_id x)^" is already declared") in let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in - let t = pf_type_of gl c in + let t = Evarutil.refresh_universes (pf_type_of gl c) in let newcl = mkNamedLetIn id c t ccl in tclTHENLIST [ convert_concl_no_check newcl; diff --git a/test-suite/check b/test-suite/check index 378c8e5d..fdc7b2d6 100755 --- a/test-suite/check +++ b/test-suite/check @@ -84,7 +84,8 @@ test_output() { nbtestsok=`expr $nbtestsok + 1` else echo "Error! (unexpected output)" - fi + fi + rm $tmpoutput done } @@ -106,6 +107,7 @@ test_parser() { echo "Ok" nbtestsok=`expr $nbtestsok + 1` fi + rm $tmpoutput done fi } diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index 5612ea75..84942da1 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -33,7 +33,7 @@ Save. Check (O#O). Locate rel. -Locate M. +Locate Library M. Module N:=Top.M. diff --git a/test-suite/tactics/TestRefine.v b/test-suite/success/TestRefine.v index f752c5bc..ee3d7e3f 100644 --- a/test-suite/tactics/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -182,22 +182,9 @@ Refine (well_founded_induction (fib (pred (pred x0)) ?)) end end). -(********* -Refine (well_founded_induction - nat - lt ? - [_:nat]nat - [x0:nat][fib:(x:nat)(lt x x0)->nat] - Cases x0 of - O => (S O) - | (S O) => (S O) - | (S (S p)) => (plus (fib (pred x0) ?) - (fib (pred (pred x0)) ?)) - end). -***********) Exact lt_wf. -Auto. -Apply lt_trans with m:=(pred x0); Auto. +Auto with arith. +Apply lt_trans with m:=(pred x0); Auto with arith. Save. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 13070bde..6087d3f2 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*) +(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*) Require Import Rbase. Require Import Rfunctions. @@ -489,8 +489,7 @@ elim s; intro. left; apply a. right; apply b. cut (Un_growing (fun n:nat => sum_f_R0 An n)). -intro; set (l1 := sum_f_R0 An N). -fold l1 in r. +intro; set (l1 := sum_f_R0 An N) in r. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. set (N0 := max x N); cut (N0 >= x)%nat. @@ -600,4 +599,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)). do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))). apply Rplus_le_compat_l; apply Hrecn0. apply Rplus_le_compat_l; apply H1. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index a23f53ff..5da14193 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RIneq.v,v 1.23.2.1 2004/07/16 19:31:11 herbelin Exp $ i*) +(*i $Id: RIneq.v,v 1.23.2.2 2005/03/29 15:35:13 herbelin Exp $ i*) (***************************************************************************) (** Basic lemmas for the classical reals numbers *) @@ -1382,7 +1382,7 @@ Qed. (**********) Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. -intros z1 z2 H; apply Zlt_O_minus_lt. +intros z1 z2 H; apply Zlt_0_minus_lt. apply lt_O_IZR. rewrite <- Z_R_minus. exact (Rgt_minus (IZR z2) (IZR z1) H). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 51323ac4..ce33afdb 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt.v,v 1.18.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: RiemannInt.v,v 1.18.2.2 2005/07/13 23:18:52 herbelin Exp $ i*) Require Import Rfunctions. Require Import SeqSeries. @@ -1593,13 +1593,12 @@ Lemma RiemannInt_P17 : intro f; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; - set (phi1 := phi_sequence RinvN pr1); + set (phi1 := phi_sequence RinvN pr1) in u0; set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); apply Rle_cv_lim with (fun N:nat => Rabs (RiemannInt_SF (phi1 N))) (fun N:nat => RiemannInt_SF (phi2 N)). intro; unfold phi2 in |- *; apply StepFun_P34; assumption. -fold phi1 in u0; apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0); try assumption. apply Rcontinuity_abs. @@ -2372,10 +2371,11 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; left; apply (cond_pos (RinvN n)). exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3; intros; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n); - fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n); - fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n); - fold phi2 in H1; assert (H10 : IsStepFun phi3 a b). + rewrite Ropp_0; rewrite Rplus_0_r; + set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *; + set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; + set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; + assert (H10 : IsStepFun phi3 a b). apply StepFun_P44 with c. apply (pre phi3). split; assumption. @@ -2442,7 +2442,7 @@ rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr; replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x)); [ apply Rabs_triang | ring ]. apply Rplus_le_compat. -fold phi3 in H1; apply H1. +apply H1. elim H14; intros; split. replace (Rmin a c) with a. apply Rle_trans with b; try assumption. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 55d4d958..27eb02cd 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) +(*i $Id: Zorder.v,v 1.6.2.3 2005/03/29 15:35:12 herbelin Exp $ i*) (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) @@ -849,12 +849,15 @@ intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *; intros p H; discriminate H. Qed. -Lemma Zmult_lt_O_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m. +Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m. intros a b apos bpos. apply Zgt_lt. apply Zmult_gt_0_compat; try apply Zlt_gt; assumption. Qed. +(* For compatibility *) +Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing). + Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n. Proof. intros x y H1 H2; apply Zmult_le_0_compat; trivial. @@ -958,8 +961,11 @@ intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus; assumption. Qed. -Lemma Zlt_O_minus_lt : forall n m:Z, 0 < n - m -> m < n. +Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n. Proof. intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l; rewrite Zplus_comm; exact H. -Qed.
\ No newline at end of file +Qed. + +(* For compatibility *) +Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing). diff --git a/theories7/Reals/PartSum.v b/theories7/Reals/PartSum.v index ee5fa498..4d28bec8 100644 --- a/theories7/Reals/PartSum.v +++ b/theories7/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) +(*i $Id: PartSum.v,v 1.1.2.2 2005/07/13 23:19:16 herbelin Exp $ i*) Require Rbase. Require Rfunctions. @@ -385,8 +385,7 @@ Elim s; Intro. Left; Apply a. Right; Apply b. Cut (Un_growing [n:nat](sum_f_R0 An n)). -Intro; Pose l1 := (sum_f_R0 An N). -Fold l1 in r. +Intro; LetTac l1 := (sum_f_R0 An N) in r. Unfold Un_cv in H; Cut ``0<l1-l``. Intro; Elim (H ? H2); Intros. Pose N0 := (max x N); Cut (ge N0 x). diff --git a/theories7/Reals/RiemannInt.v b/theories7/Reals/RiemannInt.v index c9301b56..cc537c6d 100644 --- a/theories7/Reals/RiemannInt.v +++ b/theories7/Reals/RiemannInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt.v,v 1.1.2.1 2004/07/16 19:31:34 herbelin Exp $ i*) +(*i $Id: RiemannInt.v,v 1.1.2.2 2005/07/13 23:19:16 herbelin Exp $ i*) Require Rfunctions. Require SeqSeries. @@ -710,9 +710,9 @@ Apply r_Rmult_mult with ``2``; [Unfold Rdiv; Do 2 Rewrite -> (Rmult_sym ``2``); Qed. Lemma RiemannInt_P17 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable [x:R](Rabsolu (f x)) a b)) ``a<=b`` -> ``(Rabsolu (RiemannInt pr1))<=(RiemannInt pr2)``. -Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; Pose phi1 := (phi_sequence RinvN pr1); Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)). +Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; LetTac phi1 := (phi_sequence RinvN pr1) in u0; Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)). Intro; Unfold phi2; Apply StepFun_P34; Assumption. -Fold phi1 in u0; Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption. +Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption. Apply continuity_Rabsolu. Pose phi3 := (phi_sequence RinvN pr2); Assert H0 : (EXT psi3:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((Rabsolu (f t))-((phi3 n) t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr2 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr2 n)). @@ -1139,7 +1139,7 @@ Elim (H ? H4); Clear H; Intros N0 H; Assert H5 : (n:nat)(ge n N0)->``(RinvN n)<e Intros; Replace (pos (RinvN n)) with ``(R_dist (mkposreal (/((INR n)+1)) (RinvN_pos n)) 0)``. Apply H; Assumption. Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply Rabsolu_right; Apply Rle_sym1; Left; Apply (cond_pos (RinvN n)). -Exists N0; Intros; Elim (H1 n); Elim (H2 n); Elim (H3 n); Clear H1 H2 H3; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Pose phi1 := (phi_sequence RinvN pr1 n); Fold phi1 in H8; Pose phi2 := (phi_sequence RinvN pr2 n); Fold phi2 in H3; Pose phi3 := (phi_sequence RinvN pr3 n); Fold phi2 in H1; Assert H10 : (IsStepFun phi3 a b). +Exists N0; Intros; Elim (H1 n); Elim (H2 n); Elim (H3 n); Clear H1 H2 H3; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; LetTac phi1 := (phi_sequence RinvN pr1 n) in H8 Goal; LetTac phi2 := (phi_sequence RinvN pr2 n) in H3 Goal; LetTac phi3 := (phi_sequence RinvN pr3 n) in H1 Goal; Assert H10 : (IsStepFun phi3 a b). Apply StepFun_P44 with c. Apply (pre phi3). Split; Assumption. @@ -1171,7 +1171,7 @@ Apply Rle_compatibility; Apply StepFun_P37; Try Assumption. Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ((f x)-(phi3 x)))+(Rabsolu ((f x)-(phi2 x)))``. Rewrite <- (Rabsolu_Ropp ``(f x)-(phi3 x)``); Rewrite Ropp_distr2; Replace ``(phi3 x)+ -1*(phi2 x)`` with ``((phi3 x)-(f x))+((f x)-(phi2 x))``; [Apply Rabsolu_triang | Ring]. Apply Rplus_le. -Fold phi3 in H1; Apply H1. +Apply H1. Elim H14; Intros; Split. Replace (Rmin a c) with a. Apply Rle_trans with b; Try Assumption. diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 7f7aa9aa..68b9ab26 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -16,8 +16,8 @@ \pagestyle{fancyplain} %BEGIN LATEX -\plainheadrulewidth 0.4pt -\plainfootrulewidth 0pt +\renewcommand{\plainheadrulewidth}{0.4pt} +\renewcommand{\plainfootrulewidth}{0pt} \lhead[\coqdocleftpageheader]{\leftmark} \rhead[\leftmark]{\coqdocrightpageheader} \cfoot{} diff --git a/toplevel/command.ml b/toplevel/command.ml index 3da1c838..10d6a620 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml,v 1.116.2.3 2004/12/31 12:01:16 herbelin Exp $ *) +(* $Id: command.ml,v 1.116.2.4 2005/11/29 21:40:53 letouzey Exp $ *) open Pp open Util @@ -372,7 +372,9 @@ let interp_mutual lparams lnamearconstrs finite = (List.rev arityl) lnamearconstrs in States.unfreeze fs; - notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec } + notations, { mind_entry_record = false; + mind_entry_finite = finite; + mind_entry_inds = mispecvec } with e -> States.unfreeze fs; raise e let declare_mutual_with_eliminations isrecord mie = diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 4a4f7828..4ba8f6c2 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml,v 1.30.2.1 2004/07/16 19:31:47 herbelin Exp $ *) +(* $Id: coqinit.ml,v 1.30.2.4 2006/01/11 23:18:06 barras Exp $ *) open Pp open System @@ -68,16 +68,15 @@ let hm2 s = let n = String.length s in if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s -let getenv_else s dft = try Sys.getenv s with Not_found -> dft - (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = (* developper specific directories to open *) let dev = if Coq_config.local then [ "dev" ] else [] in let coqlib = - if Coq_config.local || !Options.boot then Coq_config.coqtop + if !Options.boot then Coq_config.coqtop (* variable COQLIB overrides the default library *) else getenv_else "COQLIB" Coq_config.coqlib in + let coqlib = canonical_path_name coqlib in (* first user-contrib *) let user_contrib = coqlib/"user-contrib" in if Sys.file_exists user_contrib then @@ -90,6 +89,7 @@ let init_load_path () = (if !Options.v7 then "states7" else "states") :: dev @ vdirs in List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in + let camlp4 = canonical_path_name camlp4 in add_ml_include camlp4; (* then current directory *) Mltop.add_path "." Nameops.default_root_prefix; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 83d240a1..af787460 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml,v 1.72.2.4 2004/09/03 15:05:23 herbelin Exp $ *) +(* $Id: coqtop.ml,v 1.72.2.5 2005/11/23 14:46:09 barras Exp $ *) open Pp open Util @@ -295,7 +295,8 @@ let init is_ide = init_load_path (); inputstate (); engage (); - if not !batch_mode then Declaremods.start_library !toplevel_name; + if not !batch_mode && Global.env_is_empty() then + Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 688885b1..281ff1b6 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml,v 1.81.2.1 2004/07/16 19:31:48 herbelin Exp $ *) +(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *) open Pp open Util @@ -118,6 +118,7 @@ let abstract_inductive sec_sp ids_to_abs hyps inds = let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib = assert (Array.length mib.mind_packets > 0); + let record = mib.mind_record in let finite = mib.mind_finite in let inds = array_map_to_list @@ -153,7 +154,8 @@ let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib = in let indmodifs,cstrmodifs = List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in - ({ mind_entry_finite = finite; + ({ mind_entry_record = record; + mind_entry_finite = finite; mind_entry_inds = inds' }, indmodifs, List.flatten cstrmodifs, diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ca64cda0..4c554209 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml,v 1.105.2.6 2004/11/22 12:41:38 herbelin Exp $ *) +(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *) open Pp open Util @@ -154,12 +154,11 @@ let rec make_tags = function let declare_pprule = function (* Pretty-printing rules only for Grammar (Tactic Notation) *) - | Egrammar.TacticGrammar gl -> - let f (s,(s',l),tac) = - let pp = (make_tags l, (s',List.map make_terminal_status l)) in - Pptactic.declare_extra_tactic_pprule true s pp; - Pptactic.declare_extra_tactic_pprule false s pp in - List.iter f gl + | Egrammar.TacticGrammar (_,pp) -> + let f (s,t,p) = + Pptactic.declare_extra_tactic_pprule true s (t,p); + Pptactic.declare_extra_tactic_pprule false s (t,p) in + List.iter f pp | _ -> () let cache_grammar (_,a) = @@ -199,12 +198,24 @@ let add_grammar_obj univ entryl = (* Tactic notations *) -let locate_tactic_body dir (s,p,e) = (s,p,(dir,e)) +let rec tactic_notation_key = function + | VTerm id :: _ -> id + | _ :: l -> tactic_notation_key l + | [] -> "terminal_free_notation" + +let rec next_key_away key t = + if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t + else key + +let locate_tactic_body dir (s,(s',prods as x),e) = + let tags = make_tags prods in + let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in + (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods)) let add_tactic_grammar g = let dir = Lib.cwd () in - let g = List.map (locate_tactic_body dir) g in - Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar g)) + let pa,pp = List.split (List.map (locate_tactic_body dir) g) in + Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp))) (* Printing grammar entries *) @@ -598,8 +609,12 @@ let make_hunks etyps symbols from = | SProdList (m,sl) :: prods -> let i = list_index m vars in let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in - (* We add NonTerminal for simulation but remove it afterwards *) - let _,sl' = list_sep_last (make NoBreak (sl@[NonTerminal m])) in + let sl' = + (* If no separator: add a break *) + if sl = [] then add_break 1 [] + (* We add NonTerminal for simulation but remove it afterwards *) + else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) + in UnpListMetaVar (i,prec,sl') :: make CanBreak prods | [] -> [] @@ -813,6 +828,10 @@ let pr_level ntn (from,args) = str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ prlist_with_sep pr_coma (pr_arg_level from) args +(* In v8: prec = Some prec8 is for both parsing and printing *) +(* In v7 and translator: + prec is for parsing (None if V8Notation), + prec8 for v8 printing (v7 printing is via ast) *) let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) = try let oldprec, oldprec8 = Symbols.level_of_notation ntn in @@ -869,7 +888,7 @@ let (inSyntaxExtension, outSyntaxExtension) = classify_function = classify_syntax_definition; export_function = export_syntax_definition} -let interp_modifiers = +let interp_modifiers modl = let onlyparsing = ref false in let rec interp assoc level etyps format = function | [] -> @@ -898,10 +917,9 @@ let interp_modifiers = onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> - if format <> None then error "A format is given more than once" - onlyparsing := true; + if format <> None then error "A format is given more than once"; interp assoc level etyps (Some s) l - in interp None None [] None + in interp None None [] None modl let merge_modifiers a n l = (match a with None -> [] | Some a -> [SetAssoc a]) @ @@ -1037,22 +1055,30 @@ let compute_syntax_data forv7 (df,modifiers) = ((onlyparse,recvars,vars, ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df)) +(* Uninterpreted (reserved) notations *) let add_syntax_extension local mv mv8 = + (* from v7: + if mv8 <> None: tells the translator how to print in v8 + if mv <> None: tells how to parse and, how to print in v7 + mv = None = mv8 does not occur + from v8 (mv8 is always None and mv is always Some) + mv tells how to parse and print in v8 + *) let data8 = option_app (compute_syntax_data false) mv8 in let data = option_app (compute_syntax_data !Options.v7) mv in let prec,gram_rule = match data with - | None -> None, None + | None -> None, None (* Case of V8Notation from v7 *) | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) -> Some prec, Some (make_grammar_rule n typs symbols notation None) in match data, data8 with | None, None -> (* Nothing to do: V8Notation while not translating *) () | _, Some d | Some d, None -> - let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in + let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *) let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in let pp_rule = make_pp_rule ppdata in Lib.add_anonymous_leaf (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule))) - + (**********************************************************************) (* Distfix, Infix, Symbols *) @@ -1147,7 +1173,7 @@ let contract_notation ntn = else ntn in aux ntn 0 -let add_notation_in_scope local df c mods omodv8 scope toks = +let add_notation_in_scope local df c mods omodv8 scope = let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')= compute_syntax_data !Options.v7 (df,mods) in (* Declare the parsing and printing rules if not already done *) @@ -1260,7 +1286,7 @@ let add_notation_interpretation df names c sc = add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse false gram_data -let add_notation_in_scope_v8only local df c mv8 scope toks = +let add_notation_in_scope_v8only local df c mv8 scope = let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in let pp_rule = make_pp_rule ppdata in Lib.add_anonymous_leaf @@ -1277,7 +1303,7 @@ let add_notation_v8only local c (df,modifiers) sc = match toks with | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> (* This is a ident to be declared as a rule *) - add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc toks + add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc | _ -> let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in match lev with @@ -1299,12 +1325,16 @@ let add_notation_v8only local c (df,modifiers) sc = if List.for_all (function SetAssoc _ -> false | _ -> true) modifiers then SetAssoc Gramext.NonA :: modifiers else modifiers in - add_notation_in_scope_v8only local df c mods sc toks + add_notation_in_scope_v8only local df c mods sc let is_quoted_ident x = let x' = unquote_notation_token x in x <> x' & try Lexer.check_ident x'; true with _ -> false +(* v7: dfmod=None; mv8=Some: add only v8 printing rule *) +(* dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *) +(* dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *) +(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *) let add_notation local c dfmod mv8 sc = match dfmod with | None -> add_notation_v8only local c (out_some mv8) sc @@ -1313,7 +1343,7 @@ let add_notation local c dfmod mv8 sc = match toks with | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> (* This is a ident to be declared as a rule *) - add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc toks + add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc | _ -> let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in match lev with @@ -1335,11 +1365,11 @@ let add_notation local c dfmod mv8 sc = add_notation_interpretation_core local symbs for_old df a sc onlyparse false gram_data else - add_notation_in_scope local df c modifiers mv8 sc toks + add_notation_in_scope local df c modifiers mv8 sc | Some n -> (* Declare both syntax and interpretation *) let assoc = match assoc with None -> Some Gramext.NonA | a -> a in - add_notation_in_scope local df c modifiers mv8 sc toks + add_notation_in_scope local df c modifiers mv8 sc (* TODO add boxes information in the expression *) @@ -1371,7 +1401,6 @@ let add_distfix local assoc n df r sc = let a = mkAppC (mkRefC r, vars) in let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc - (split_notation_string df) let make_infix_data n assoc modl mv8 = (* Infix defaults to LEFTA in V7 (cf doc) *) @@ -1404,7 +1433,7 @@ let add_infix local (inf,modl) pr mv8 sc = else if n8 = None then error "Needs a level" else let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in - add_notation_in_scope_v8only local df a mv8 sc toks + add_notation_in_scope_v8only local df a mv8 sc else begin let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in (* check the precedence *) @@ -1435,10 +1464,10 @@ let add_infix local (inf,modl) pr mv8 sc = onlyparse false gram_data else let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc toks + add_notation_in_scope local df a mv mv8 sc else let mv,mv8 = make_infix_data n assoc modl mv8 in - add_notation_in_scope local df a mv mv8 sc toks + add_notation_in_scope local df a mv mv8 sc end let standardise_locatable_notation ntn = diff --git a/toplevel/record.ml b/toplevel/record.ml index f703c067..3a10c7e5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml,v 1.52.2.1 2004/07/16 19:31:49 herbelin Exp $ *) +(* $Id: record.ml,v 1.52.2.2 2005/11/29 21:40:53 letouzey Exp $ *) open Pp open Util @@ -226,7 +226,8 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in let mie = - { mind_entry_finite = true; + { mind_entry_record = true; + mind_entry_finite = true; mind_entry_inds = [mie_ind] } in let sp = declare_mutual_with_eliminations true mie in let rsp = (sp,0) in (* This is ind path of idstruc *) diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index f75f767d..381ac2c3 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstrnew.ml,v 1.62.2.4 2004/12/29 10:17:11 herbelin Exp $ *) +(* $Id: ppconstrnew.ml,v 1.62.2.6 2005/03/08 10:13:45 herbelin Exp $ *) (*i*) open Ast @@ -118,7 +118,7 @@ let pr_optc pr = function | None -> mt () | Some x -> pr_sep_com spc pr x -let pr_universe u = str "<univ>" +let pr_universe = Univ.pr_uni let pr_sort = function | RProp Term.Null -> str "Prop" diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 80298c3e..7da30c4e 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptacticnew.ml,v 1.57.2.2 2004/07/16 19:31:52 herbelin Exp $ *) +(* $Id: pptacticnew.ml,v 1.57.2.3 2005/05/15 12:47:03 herbelin Exp $ *) open Pp open Names @@ -587,7 +587,8 @@ and pr_atom1 env = function | TacTrivial (Some []) as x -> pr_atom0 env x | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db) | TacAuto (None,Some []) as x -> pr_atom0 env x - | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAuto (n,db) -> + hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) (* | TacAutoTDB None as x -> pr_atom0 env x | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n) | TacDestructHyp (true,id) -> @@ -599,7 +600,8 @@ and pr_atom1 env = function hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)*) | TacDAuto (n,p) -> - hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p) + hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ + pr_opt int p) (* Context management *) | TacClear l -> diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index bfcbee43..2e921c4e 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernacnew.ml,v 1.95.2.3 2004/10/12 10:10:29 herbelin Exp $ *) +(* $Id: ppvernacnew.ml,v 1.95.2.4 2005/12/23 22:16:56 herbelin Exp $ *) open Pp open Names @@ -48,9 +48,12 @@ let pr_module r = Ident (loc,id_of_string s) | Qualid (loc,qid) -> Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in - let (_,dir,_) = + let dir = try - Library.locate_qualified_library (snd (qualid_of_reference r)) + Nametab.full_name_module (snd (qualid_of_reference r)) + with _ -> + try + pi2 (Library.locate_qualified_library (snd (qualid_of_reference r))) with _ -> errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r) in @@ -1032,7 +1035,7 @@ let rec pr_vernac = function | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern - | VernacLocate loc -> + | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_reference qid | LocateFile f -> str"File" ++ spc() ++ qsnew f |