diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
| commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
| tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 | |
| parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) | |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
75 files changed, 1223 insertions, 1337 deletions
diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index 1de1655d..00000000 --- a/.dir-locals.el +++ /dev/null @@ -1,8 +0,0 @@ -((nil . ((eval . (setq default-directory (locate-dominating-file - buffer-file-name - ".dir-locals.el") - tags-file-name (concat default-directory - "TAGS") - camldebug-command-name (concat - default-directory "dev/ocamldebug-coq") -)))))
\ No newline at end of file diff --git a/.gitignore b/.gitignore deleted file mode 100644 index e0be678c..00000000 --- a/.gitignore +++ /dev/null @@ -1,185 +0,0 @@ -*.glob -*.d -*.d.raw -*.vo -*.cm* -*.annot -*.spit -*.spot -*.o -*.a -*.log -*.aux -*.dvi -*.blg -*.bbl -*.idx -*.ilg -*.toc -*.atoc -*.comidx -*.comind -*.erridx -*.errind -*.haux -*.hcomind -*.herrind -*.hind -*.htacind -*.htoc -*.ind -*.lof -*.tacidx -*.tacind -*.v.tex -*.v.pdf -*.v.ps -*.v.html -*.stamp -revision -TAGS -.DS_Store -.pc -bin/ -_build -plugins/*/*_mod.ml -myocamlbuild_config.ml -config/Makefile -config/coq_config.ml -dev/ocamldebug-coq -plugins/micromega/csdpcert -kernel/byterun/dllcoqrun.so -states/initial.coq -coqdoc.sty -test-suite/lia.cache -test-suite/trace -test-suite/misc/universes/all_stdlib.v -test-suite/misc/universes/universes.txt - -# documentation - -doc/faq/html/ -doc/refman/csdp.cache -doc/refman/trace -doc/refman/Reference-Manual.pdf -doc/refman/Reference-Manual.ps -doc/refman/Reference-Manual.html -doc/refman/Reference-Manual.out -doc/refman/Reference-Manual.sh -doc/refman/cover.html -doc/refman/styles.hva -doc/common/version.tex -doc/refman/coqide-queries.eps -doc/refman/coqide.eps -doc/refman/euclid.ml -doc/refman/euclid.mli -doc/refman/heapsort.ml -doc/refman/heapsort.mli -doc/refman/html/ -doc/stdlib/Library.out -doc/stdlib/Library.pdf -doc/stdlib/Library.ps -doc/stdlib/Library.coqdoc.tex -doc/stdlib/FullLibrary.pdf -doc/stdlib/FullLibrary.ps -doc/stdlib/FullLibrary.coqdoc.tex -doc/stdlib/html/ -doc/stdlib/index-body.html -doc/stdlib/index-list.html -doc/RecTutorial/RecTutorial.html -doc/RecTutorial/RecTutorial.pdf -doc/RecTutorial/RecTutorial.ps -dev/doc/naming-conventions.pdf - -# .mll files - -dev/ocamlweb-doc/lex.ml -ide/coq_lex.ml -ide/config_lexer.ml -ide/utf8_convert.ml -ide/highlight.ml -plugins/dp/dp_zenon.ml -tools/gallina_lexer.ml -tools/coqwc.ml -tools/coqdep_lexer.ml -tools/coqdoc/cpretty.ml -lib/xml_lexer.ml - -# .mly files - -ide/config_parser.ml -ide/config_parser.mli - -# .ml4 files - -ide/project_file.ml -lib/pp.ml -lib/compat.ml -parsing/g_xml.ml -parsing/g_prim.ml -parsing/q_util.ml -parsing/tacextend.ml -parsing/q_constr.ml -parsing/g_vernac.ml -parsing/pcoq.ml -parsing/g_constr.ml -parsing/g_ltac.ml -parsing/vernacextend.ml -parsing/g_tactic.ml -parsing/argextend.ml -parsing/g_decl_mode.ml -parsing/q_coqast.ml -parsing/g_proofs.ml -parsing/lexer.ml -plugins/xml/proofTree2Xml.ml -plugins/xml/acic2Xml.ml -plugins/xml/xml.ml -plugins/xml/dumptree.ml -plugins/xml/xmlentries.ml -plugins/extraction/g_extraction.ml -plugins/rtauto/g_rtauto.ml -plugins/romega/g_romega.ml -plugins/setoid_ring/newring.ml -plugins/firstorder/g_ground.ml -plugins/dp/g_dp.ml -plugins/cc/g_congruence.ml -plugins/ring/g_ring.ml -plugins/field/field.ml -plugins/funind/g_indfun.ml -plugins/omega/g_omega.ml -plugins/quote/g_quote.ml -plugins/nsatz/nsatz.ml -plugins/micromega/g_micromega.ml -plugins/subtac/g_subtac.ml -plugins/fourier/g_fourier.ml -plugins/decl_mode/g_decl_mode.ml -tactics/tauto.ml -tactics/eauto.ml -tactics/hipattern.ml -tactics/class_tactics.ml -tactics/rewrite.ml -tactics/eqdecide.ml -tactics/extratactics.ml -tactics/extraargs.ml -tools/coq_tex.ml -toplevel/mltop.ml -toplevel/whelp.ml -ide/coqide_main.ml -ide/coqide_main_opt.ml - -# other auto-generated files - -ide/undo.mli -toplevel/mltop.optml -toplevel/mltop.byteml -kernel/byterun/coq_jumptbl.h -kernel/copcodes.ml -scripts/tolink.ml -theories/Numbers/Natural/BigN/NMake_gen.v -ide/index_urls.txt - -# mlis documentation - -dev/ocamldoc/html/ -dev/ocamldoc/coq.* -dev/ocamldoc/ocamldoc.sty @@ -1,3 +1,35 @@ +Changes from V8.4 to V8.4pl1 +============================ + +Bug fixes + +- Solved bugs : + #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921 + #2930 #2941 #2878 +- Partially fixed bug : #2904 +- Various fixes concerning coq_makefile + +Optimizations + +- "Union by rank" optimization for universes contributed by J.H. Jourdan + and G. Sherrer (see union-find-and-coq-universes on gagallium blog). + +Libraries + +- Internal organisation of some modular libraries have slightly changed + due to bug #2904 (GenericMinMax, OrdersTac) +- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml + (cf bug #2878). + +Coqide + +- Improved shutdown of coqtop processes spawned by coqide + (in particular added a missing close_on_exec primitive before forking). +- On windows, launching coqide with the -debug option now produces + a log file in the user's temporary directory. The location of this + log file is displayed in the "About" message. + + Changes from V8.4beta2 to V8.4 ============================== @@ -155,10 +155,6 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt compiler instead of ocamlopt). Makes compilation faster (recommended). --nowarnings - Disable the Objective Caml compiler warnings. This option has no - effect on the result of the compilation. - -browser <command> Use <command> to open an URL in a browser. %s must appear in <command>, and will be replaced by the URL. diff --git a/Makefile.build b/Makefile.build index fe99f3b0..8d3045cc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -84,15 +84,14 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB) OCAMLC += $(CAMLFLAGS) OCAMLOPT += $(CAMLFLAGS) -BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) -OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) -COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +BAREBYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) +BAREOPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +BYTEFLAGS=$(MLINCLUDES) $(BAREBYTEFLAGS) +OPTFLAGS=$(MLINCLUDES) $(BAREOPTFLAGS) DEPFLAGS= -slash $(LOCALINCLUDES) define bestocaml @@ -194,6 +193,16 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### +## In Win32, cygwin provides an emulation of ln -s, but this emulation +## won't work outside of cygwin shell (i.e. typically in a Sys.command). +## So we just forget about it, and do a simple copy. + +ifeq ($(ARCH),win32) +LN:=cp -f +else +LN:=ln -sf +endif + .PHONY: coqbinaries coq coqlib coqlight states coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} @@ -208,15 +217,15 @@ states:: states/initial.coq $(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -opt $(BAREOPTFLAGS) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -top $(BAREBYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) - cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) + cd bin && $(LN) coqtop.$(BEST)$(EXE) coqtop$(EXE) LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) @@ -233,7 +242,7 @@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) - cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) + cd bin && $(LN) coqchk.$(BEST)$(EXE) coqchk$(EXE) # coqmktop @@ -247,7 +256,7 @@ $(COQMKTOPOPT): $(COQMKTOPCMO:.cmo=.cmx) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) - cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE) + cd bin && $(LN) coqmktop.$(BEST)$(EXE) coqmktop$(EXE) scripts/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ @@ -267,7 +276,7 @@ $(COQCOPT): $(COQCCMO:.cmo=.cmx) | $(COQTOPOPT) $(STRIP) $@ $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) - cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) + cd bin && $(LN) coqc.$(BEST)$(EXE) coqc$(EXE) # target for libraries @@ -320,8 +329,8 @@ coqide-files: $(IDEFILES) $(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\ - gtkThread.cmx str.cmxa $(LINKIDEOPT) + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \ + lablgtk.cmxa $(IDEOPTFLAGS) gtkThread.cmx str.cmxa $(LINKIDEOPT) $(STRIP) $@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) @@ -330,7 +339,7 @@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) $(COQIDE): - cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) + cd bin && $(LN) coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) # install targets @@ -346,14 +355,14 @@ install-ide-byte: $(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) - cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) + cd $(FULLBINDIR) && $(LN) coqide.byte$(EXE) coqide$(EXE) install-ide-opt: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \ $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) - cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) + cd $(FULLBINDIR) && $(LN) coqide.opt$(EXE) coqide$(EXE) install-ide-files: $(MKDIR) $(FULLDATADIR) @@ -604,12 +613,12 @@ install-binaries:: install-$(BEST) install-tools install-byte:: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE) + cd $(FULLBINDIR); $(LN) coqtop.byte$(EXE) coqtop$(EXE); $(LN) coqchk.byte$(EXE) coqchk$(EXE) install-opt:: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE) + cd $(FULLBINDIR); $(LN) coqtop.opt$(EXE) coqtop$(EXE); $(LN) coqchk.opt$(EXE) coqchk$(EXE) install-tools:: $(MKDIR) $(FULLBINDIR) @@ -633,7 +642,9 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib +ifneq ($(COQRUNBYTEFLAGS),"-custom") $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif $(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) diff --git a/Makefile.common b/Makefile.common index c5969d17..444a7ee5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -119,8 +119,8 @@ HEVEA:=hevea HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple -export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): -COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small +export TEXINPUTS:=$(HEVEALIB): +COQTEXOPTS:=-boot -n 72 -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex diff --git a/Makefile.doc b/Makefile.doc index 685887f5..31a0675c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -53,10 +53,10 @@ rectutorial: doc/RecTutorial/RecTutorial.html \ ifdef QUICK %.v.tex: %.tex - (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) + $(COQTEX) $(COQTEXOPTS) $< else %.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO) - (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) + $(COQTEX) $(COQTEXOPTS) $< endif %.ps: %.dvi @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme <opaque>) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - @@ -12,12 +12,14 @@ check_config() { [ -L $MYCFG ] || ln -sf $CFG $MYCFG } -ocb() { $OCAMLBUILD $FLAGS $*; } +# NB: we exec ocamlbuild and run ocb last for a correct exit code + +ocb() { exec $OCAMLBUILD $FLAGS $*; } rule() { check_config case $1 in - clean) ocb -clean && rm -rf bin/* && rm -f $MYCFG;; + clean) rm -rf bin/* $MYCFG && ocb -clean;; all) ocb coq.otarget;; win32) ocb coq-win32.otarget;; *) ocb $1;; @@ -6,7 +6,7 @@ # ################################## -VERSION=8.4 +VERSION=8.4pl1 VOMAGIC=08400 STATEMAGIC=58400 DATE=`LC_ALL=C LANG=C date +"%B %Y"` @@ -35,37 +35,36 @@ usage () { printf "\tSet installation directory to <dir>\n" echo "-local" printf "\tSet installation directory to the current source tree\n" - echo "-coqrunbyteflags" + echo "-coqrunbyteflags <flags>" printf "\tSet link flags for VM-dependent bytecode (coqtop)\n" - echo "-coqtoolsbyteflags" + echo "-coqtoolsbyteflags <flags>" printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n" echo "-custom" printf "\tGenerate all bytecode executables with -custom (not recommended)\n" - echo "-src" + echo "-src <dir>" printf "\tSpecifies the source directory\n" - echo "-bindir" - echo "-libdir" - echo "-configdir" - echo "-datadir" - echo "-mandir" - echo "-docdir" + echo "-bindir <dir>" + echo "-libdir <dir>" + echo "-configdir <dir>" + echo "-datadir <dir>" + echo "-mandir <dir>" + echo "-docdir <dir>" printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n" - echo "-emacslib" - echo "-emacs" + echo "-emacslib <dir>" printf "\tSpecifies where emacs files are to be installed\n" - echo "-coqdocdir" + echo "-coqdocdir <dir>" printf "\tSpecifies where Coqdoc style files are to be installed\n" - echo "-camldir" + echo "-camldir <dir>" printf "\tSpecifies the path to the OCaml library\n" - echo "-lablgtkdir" + echo "-lablgtkdir <dir>" printf "\tSpecifies the path to the Lablgtk library\n" echo "-usecamlp5" printf "\tSpecifies to use camlp5 instead of camlp4\n" echo "-usecamlp4" printf "\tSpecifies to use camlp4 instead of camlp5\n" - echo "-camlp5dir" + echo "-camlp5dir <dir>" printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n" - echo "-arch" + echo "-arch <arch>" printf "\tSpecifies the architecture\n" echo "-opt" printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n" @@ -163,8 +162,7 @@ while : ; do -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes coqtoolsbyteflags="$2" shift;; - -custom|--custom) custom_spec=yes - shift;; + -custom|--custom) custom_spec=yes;; -src|--src) src_spec=yes COQSRC="$2" shift;; @@ -191,6 +189,7 @@ while : ; do shift;; -emacs |--emacs) emacs_spec=yes emacs="$2" + printf "Warning: obsolete -emacs option\n" shift;; -coqdocdir|--coqdocdir) coqdocdir_spec=yes coqdocdir="$2" @@ -595,16 +594,13 @@ fi # OS dependent libraries OSDEPLIBS="-cclib -lunix" -case $ARCH,$CYGWIN in +case $ARCH in sun4*) OS=`uname -r` case $OS in 5*) OS="Sun Solaris $OS" OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";; *) OS="Sun OS $OS" esac;; - win32,yes) OS="Win32 (Cygwin)" - cflags="-mno-cygwin $cflags";; - win32,*) OS="Win32 (MinGW)";; esac # lablgtk2 and CoqIDE @@ -627,14 +623,30 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then else case $lablgtkdir_spec in no) - if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then - lablgtkdir_spec=yes - elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then + if lablgtkdirtmp=$(ocamlfind query lablgtk2 2> /dev/null); then + if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then + lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" + lablgtkdir=$lablgtkdirtmp + LABLGTKLIB=$lablgtkdir # Pour le message utilisateur + else + echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)." + fi + fi + if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.mli" -a -f "${CAMLLIB}/glib.mli" ]; then + lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory" lablgtkdir=${CAMLLIB}/lablgtk2 + LABLGTKLIB=+lablgtk2 # Pour le message utilisateur fi;; yes) - if [ ! -f "$lablgtkdir/glib.mli" ]; then - echo "Incorrect LablGtk2 library (glib.mli not found)." + if [ ! -d "$lablgtkdir" ]; then + echo "$lablgtkdir is not a valid directory." + echo "Configuration script failed!" + exit 1 + elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then + lablgtkdirfoundmsg="LablGtk2 directory found" + LABLGTKLIB=$lablgtkdir # Pour le message utilisateur + else + echo "Headers missing in LablGtk2 library (glib.cmi/glib.mli not found)." echo "Configuration script failed!" exit 1 fi;; @@ -643,22 +655,20 @@ else echo "LablGtk2 not found: CoqIde will not be available." COQIDE=no elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then - echo "LablGtk2 found but too old: CoqIde will not be available." + echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available." COQIDE=no; elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then - echo "LablGtk2 found, bytecode CoqIde will be used as requested." + echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested." COQIDE=byte elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then - echo "LablGtk2 found, no native threads: bytecode CoqIde will be available." + echo "$lablgtkdirfoundmsg, no native threads: bytecode CoqIde will be available." COQIDE=byte else - echo "LablGtk2 found, native threads: native CoqIde will be available." + echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available." COQIDE=opt - if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration; + if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null); then - cflags=$cflags" `pkg-config --cflags gtk-mac-integration`" - IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"' - IDEARCHFILE=ide/ide_mac_stubs.o + IDEARCHFLAGS=lablgtkosx.cmxa IDEARCHDEF=QUARTZ elif [ "$ARCH" = "win32" ]; then @@ -671,15 +681,13 @@ fi case $COQIDE in byte|opt) - case $lablgtkdir_spec in - no) LABLGTKLIB=+lablgtk2 # Pour le message - LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile - yes) LABLGTKLIB=$lablgtkdir # Pour le message - LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile - esac;; - no) LABLGTKINCLUDES="";; + LABLGTKINCLUDES="-I $LABLGTKLIB";; + no) + LABLGTKINCLUDES="";; esac +[ x$lablgtkosxdir = x ] || LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir" + # strip command case $ARCH in diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html index 138c3025..ff38ba8a 100644 --- a/doc/common/styles/html/coqremote/footer.html +++ b/doc/common/styles/html/coqremote/footer.html @@ -1,45 +1,34 @@ -<div id="sidebarWrapper"> -<div id="sidebar"> - -<div class="block"> -<h2 class="title">Navigation</h2> -<div class="content"> - -<ul class="menu"> - -<li class="leaf">Standard Library - <ul class="menu"> - <li><a href="index.html">Table of contents</a></li> - <li><a href="genindex.html">Index</a></li> - </ul> -</li> - -</ul> - -</div> -</div> - -</div> -</div> - - -</div> - -</div> - -<div id="footer"> -<div id="nav-footer"> - <ul class="links-menu-footer"> - <li><a href="mailto:webmaster_@_www.lix.polytechnique.fr">webmaster</a></li> - <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li> - <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li> - </ul> - -</div> -</div> + <div id="sidebarWrapper"> + <div id="sidebar"> + <div class="block"> + <h2 class="title">Navigation</h2> + <div class="content"> + <ul class="menu"> + <li class="leaf">Standard Library + <ul class="menu"> + <li><a href="index.html">Table of contents</a></li> + <li><a href="genindex.html">Index</a></li> + </ul> + </li> + </ul> + </div> + </div> + </div> + </div> + + </div> + + <div id="footer"> + <div id="nav-footer"> + <ul class="links-menu-footer"> + <li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li> + </ul> + </div> + </div> </div> </body> </html> - diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html index afcdbe73..891fb328 100644 --- a/doc/common/styles/html/coqremote/header.html +++ b/doc/common/styles/html/coqremote/header.html @@ -6,44 +6,40 @@ <title>Standard Library | The Coq Proof Assistant</title> <link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/node/node.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/defaults.css";</style> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/system.css";</style> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/user/user.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/style.css";</style> -<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/coqdoc.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> </head> <body> <div id="container"> -<div id="headertop"> -<div id="nav"> - <ul class="links-menu"> - <li><a href="http://www.lix.polytechnique.fr/coq/" class="active">Home</a></li> - - <li><a href="http://www.lix.polytechnique.fr/coq/about-coq" title="More about coq">About Coq</a></li> - <li><a href="http://www.lix.polytechnique.fr/coq/download">Get Coq</a></li> - <li><a href="http://www.lix.polytechnique.fr/coq/documentation">Documentation</a></li> - <li><a href="http://www.lix.polytechnique.fr/coq/community">Community</a></li> - </ul> -</div> -</div> - -<div id="header"> - -<div id="logoWrapper"> - -<div id="logo"><a href="http://www.lix.polytechnique.fr/coq/" title="Home"><img src="http://www.lix.polytechnique.fr/coq/files/barron_logo.png" alt="Home" /></a> -</div> -<div id="siteName"><a href="http://www.lix.polytechnique.fr/coq/" title="Home">The Coq Proof Assistant</a> -</div> - -</div> -</div> - -<div id="content"> + <div id="headertop"> + <div id="nav"> + <ul class="links-menu"> + <li><a href="http://coq.inria.fr/" class="active">Home</a></li> + <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> + <li><a href="http://coq.inria.fr/download">Get Coq</a></li> + <li><a href="http://coq.inria.fr/documentation">Documentation</a></li> + <li><a href="http://coq.inria.fr/community">Community</a></li> + </ul> + </div> + </div> + + <div id="header"> + <div id="logoWrapper"> + <div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a> + </div> + <div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a> + </div> + </div> + </div> + + <div id="content"> @@ -191,11 +191,29 @@ let coqtop_zombies () = Note: we use Unix.stderr in Unix.create_process to get debug messages from the coqtop's Ide_slave loop. + + NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r) + in coqtop. We do this indirectly via [Unix.set_close_on_exec]. + This way, coqide has the only remaining copies of these descriptors, + and closing them later will have visible effects in coqtop. Cf man 7 pipe : + + - If all file descriptors referring to the write end of a pipe have been + closed, then an attempt to read(2) from the pipe will see end-of-file + (read(2) will return 0). + - If all file descriptors referring to the read end of a pipe have been + closed, then a write(2) will cause a SIGPIPE signal to be generated for + the calling process. If the calling process is ignoring this signal, + then write(2) fails with the error EPIPE. + + Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be + closed in coqide. *) let open_process_pid prog args = let (ide2top_r,ide2top_w) = Unix.pipe () in let (top2ide_r,top2ide_w) = Unix.pipe () in + Unix.set_close_on_exec ide2top_w; + Unix.set_close_on_exec top2ide_r; let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in assert (pid <> 0); Unix.close ide2top_r; @@ -250,7 +268,7 @@ let eval_call coqtop (c:'a Ide_intf.call) = Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c); flush coqtop.cin; let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in - (Ide_intf.to_answer xml : 'a Interface.value) + (Ide_intf.to_answer xml c : 'a Interface.value) let interp coqtop ?(raw=false) ?(verbose=true) s = eval_call coqtop (Ide_intf.interp (raw,verbose,s)) diff --git a/ide/coqide.ml b/ide/coqide.ml index 1bd490ab..07de4daf 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -41,14 +41,9 @@ object val mutable read_only : bool val mutable filename : string option val mutable stats : Unix.stats option - val mutable detached_views : GWindow.window list method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b method set_auto_complete : bool -> unit - method kill_detached_views : unit -> unit - method add_detached_view : GWindow.window -> unit - method remove_detached_view : GWindow.window -> unit - method filename : string option method stats : Unix.stats option method update_stats : unit @@ -104,7 +99,10 @@ type viewable_script = } let kill_session s = - s.analyzed_view#kill_detached_views (); + (* To close the detached views of this script, we call manually + [destroy] on it, triggering some callbacks in [detach_view]. + In a more modern lablgtk, rather use the page-removed signal ? *) + s.script#destroy (); Coq.kill_coqtop !(s.toplvl) let build_session s = @@ -442,6 +440,7 @@ let remove_tags (buffer:GText.buffer) from upto = Tags.Script.proof_decl; Tags.Script.qed ] (** Cut a part of the buffer in sentences and tag them. + Invariant: either this slice ends the buffer, or it ends with ".". May raise [Coq_lex.Unterminated] when the zone ends with an unterminated sentence. *) @@ -480,14 +479,18 @@ let is_char s c = s#char = Char.code c (** Search backward the first character of a sentence, starting at [iter] and going at most up to [soi] (meant to be the end of the locked zone). - Raise [Not_found] when no proper sentence start has been found, - in particular when the final "." of the locked zone is followed - by a non-blank character outside the locked zone. This non-blank - character will be signaled as erroneous in [tag_on_insert] below. *) + Raise [StartError] when no proper sentence start has been found. + A character following a ending "." is considered as a sentence start + only if this character is a blank. In particular, when a final "." + at the end of the locked zone isn't followed by a blank, then this + non-blank character will be signaled as erroneous in [tag_on_insert] below. +*) + +exception StartError let grab_sentence_start (iter:GText.iter) soi = let cond iter = - if iter#compare soi < 0 then raise Not_found; + if iter#compare soi < 0 then raise StartError; let prev = iter#backward_char in is_sentence_end prev && (not (is_char prev '.') || @@ -509,42 +512,35 @@ let rec grab_ending_dot (start:GText.iter) = (** Retag a zone that has been edited *) -let tag_on_insert = - (* possible race condition here : editing two buffers with a timedelta smaller - * than 1.5s might break the error recovery mechanism. *) - let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *) - fun buffer -> - try - (* the start of the non-locked zone *) - let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in - (* the inserted zone is between [prev_insert] and [insert] *) - let insert = buffer#get_iter_at_mark `INSERT in - let prev_insert = buffer#get_iter_at_mark (`NAME "prev_insert") in - (* [prev_insert] is normally always before [insert] even when deleting. - Let's check this nonetheless *) - let prev_insert = - if insert#compare prev_insert < 0 then insert else prev_insert - in - let start = grab_sentence_start prev_insert soi in - (** The status of "{" "}" as sentence delimiters is too fragile. - We retag up to the next "." instead. *) - let stop = grab_ending_dot insert in - let skip_curr = ref true in (* shall the callback be skipped ? by default yes*) - (!skip_last) := true; (* skip the previously created callback *) - skip_last := skip_curr; - try split_slice_lax buffer start stop - with Coq_lex.Unterminated -> - skip_curr := false; - let callback () = - if not !skip_curr then begin - try split_slice_lax buffer start buffer#end_iter - with Coq_lex.Unterminated -> () - end; false - in - ignore (Glib.Timeout.add ~ms:1500 ~callback) - with Not_found -> - let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in - buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char +let tag_on_insert buffer = + (* the start of the non-locked zone *) + let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in + (* the inserted zone is between [prev_insert] and [insert] *) + let insert = buffer#get_iter_at_mark `INSERT in + let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in + (* [prev] is normally always before [insert] even when deleting. + Let's check this nonetheless *) + let prev, insert = + if insert#compare prev < 0 then insert, prev else prev, insert + in + try + let start = grab_sentence_start prev soi in + (** The status of "{" "}" as sentence delimiters is too fragile. + We retag up to the next "." instead. *) + let stop = grab_ending_dot insert in + try split_slice_lax buffer start stop + with Coq_lex.Unterminated -> + (* This shouldn't happen frequently. Either: + - we are at eof, with indeed an unfinished sentence. + - we have just inserted an opening of comment or string. + - the inserted text ends with a "." that interacts with the "." + found by [grab_ending_dot] to form a non-ending "..". + In any case, we retag up to eof, since this isn't that costly. *) + if not stop#is_end then + try split_slice_lax buffer start buffer#end_iter + with Coq_lex.Unterminated -> () + with StartError -> + buffer#apply_tag Tags.Script.error ~start:soi ~stop:soi#forward_char let force_retag buffer = try split_slice_lax buffer buffer#start_iter buffer#end_iter @@ -591,7 +587,6 @@ object(self) val mutable stats = None val mutable last_modification_time = 0. val mutable last_auto_save_time = 0. - val mutable detached_views = [] val mutable find_forward_instead_of_backward = false val mutable auto_complete_on = !current.auto_complete @@ -606,14 +601,6 @@ object(self) let y = f x in self#set_auto_complete old; y - method add_detached_view (w:GWindow.window) = - detached_views <- w::detached_views - method remove_detached_view (w:GWindow.window) = - detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views - - method kill_detached_views () = - List.iter (fun w -> w#destroy ()) detached_views; - detached_views <- [] method filename = filename method stats = stats @@ -820,7 +807,7 @@ object(self) begin let menu_callback = if !current.contextual_menus_on_goal then (fun s () -> ignore (self#insert_this_phrase_on_success - true true false ("progress "^s) s)) + true true false ("progress "^s) s)) else (fun _ _ -> ()) in try @@ -1007,6 +994,7 @@ object(self) if stop#starts_line then input_buffer#insert ~iter:stop insertphrase else input_buffer#insert ~iter:stop ("\n"^insertphrase); + tag_on_insert input_buffer; let start = self#get_start_of_input in input_buffer#move_mark ~where:stop (`NAME "start_of_input"); input_buffer#apply_tag (safety_tag safe) ~start ~stop; @@ -1231,7 +1219,7 @@ object(self) (List.exists (fun p -> self#insert_this_phrase_on_success true false false - ("progress "^p^".\n") (p^".\n")) l) + ("progress "^p^".") (p^".")) l) method active_keypress_handler k = let state = GdkEvent.Key.state k in @@ -1382,23 +1370,15 @@ object(self) ); ignore (input_buffer#connect#begin_user_action ~callback:(fun () -> - let here = input_buffer#get_iter_at_mark `INSERT in - input_buffer#move_mark (`NAME "prev_insert") here - ) + let where = self#get_insert in + input_buffer#move_mark (`NAME "prev_insert") ~where; + let start = self#get_start_of_input in + let stop = input_buffer#end_iter in + input_buffer#remove_tag Tags.Script.error ~start ~stop) ); ignore (input_buffer#connect#end_user_action ~callback:(fun () -> last_modification_time <- Unix.time (); - let r = input_view#visible_rect in - let stop = - input_view#get_iter_at_location - ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r) - ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r) - in - input_buffer#remove_tag - Tags.Script.error - ~start:self#get_start_of_input - ~stop; tag_on_insert input_buffer ) ); @@ -1795,6 +1775,8 @@ let forbid_quit_to_save () = end else false) +let logfile = ref None + let main files = (* Main window *) @@ -2354,7 +2336,7 @@ let main files = let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s) ~accel:(!current.modifier_for_tactics^sc) ~callback:(do_if_active (fun a -> a#insert_command - ("progress "^s^".\n") (s^".\n"))) in + ("progress "^s^".") (s^"."))) in let query_callback command _ = let word = get_current_word () in if not (word = "") then @@ -2381,6 +2363,24 @@ let main files = |Some ac -> GAction.add_action name ~label ~callback ~accel:(!current.modifier_for_templates^ac) |None -> GAction.add_action name ~label ~callback ?accel:None in + let detach_view _ = + (* Open a separate window containing the current buffer *) + let trm = session_notebook#current_term in + let w = GWindow.window ~show:true + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~position:`CENTER + ~title:(if trm.filename = "" then "*scratch*" else trm.filename) + () + in + let sb = GBin.scrolled_window ~packing:w#add () + in + let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add () + in + nv#misc#modify_font !current.text_font; + (* If the buffer in the main window is closed, destroy this detached view *) + ignore (trm.script#connect#destroy ~callback:w#destroy) + in GAction.add_actions file_actions [ GAction.add_action "File" ~label:"_File"; GAction.add_action "New" ~callback:new_f ~stock:`NEW; @@ -2568,33 +2568,7 @@ let main files = ]; GAction.add_actions windows_actions [ GAction.add_action "Windows" ~label:"_Windows"; - GAction.add_action "Detach View" ~label:"Detach _View" - ~callback:(fun _ -> do_if_not_computing "detach view" - (function {script=v;analyzed_view=av} -> - let w = GWindow.window ~show:true - ~width:(!current.window_width*2/3) - ~height:(!current.window_height*2/3) - ~position:`CENTER - ~title:(match av#filename with - | None -> "*Unnamed*" - | Some f -> f) - () - in - let sb = GBin.scrolled_window - ~packing:w#add () - in - let nv = GText.view - ~buffer:v#buffer - ~packing:sb#add - () - in - nv#misc#modify_font - !current.text_font; - ignore (w#connect#destroy - ~callback: - (fun () -> av#remove_detached_view w)); - av#add_detached_view w) - [session_notebook#current_term]); + GAction.add_action "Detach View" ~label:"Detach _View" ~callback:detach_view ]; GAction.add_actions help_actions [ GAction.add_action "Help" ~label:"_Help"; @@ -2846,12 +2820,17 @@ let main files = \n-------------------\ \n" in + let display_log_file (b:GText.buffer) = + if !debug then + let file = match !logfile with None -> "stderr" | Some f -> f in + b#insert ("Debug mode is on, log file is "^file) + in let initial_about (b:GText.buffer) = let initial_string = "Welcome to CoqIDE, an Integrated Development Environment for Coq\n" in let coq_version = Coq.short_version () in - b#insert ~iter:b#start_iter "\n\n"; + display_log_file b; if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version); if Glib.Utf8.validate initial_string then @@ -2881,8 +2860,8 @@ let main files = then b#insert about_full_string; let coq_version = Coq.version () in if Glib.Utf8.validate coq_version - then b#insert coq_version - + then b#insert coq_version; + display_log_file b; in (* Remove default pango menu for textviews *) w#show (); diff --git a/ide/coqide.mli b/ide/coqide.mli index 18df1f6a..44de77f7 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -12,6 +12,9 @@ no /bin/sh when using create_process instead of open_process. *) val sup_args : string list ref +(** In debug mode under win32, messages are written to a log file *) +val logfile : string option ref + (** Filter the argv from coqide specific options, and set Minilib.coqtop_path accordingly *) val read_coqide_args : string list -> string list diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index f5138311..ebcecc17 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -6,18 +6,37 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -IFDEF QUARTZ THEN -external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit - = "caml_gtk_mac_init" +let _ = Coqide.ignore_break () +let _ = GtkMain.Main.init () -external gtk_mac_ready : ([> Gtk.widget ] as 'a) Gtk.obj -> ([> Gtk.widget ] as 'a) Gtk.obj -> - ([> Gtk.widget ] as 'a) Gtk.obj -> unit - = "caml_gtk_mac_ready" -END +(* We handle Gtk warning messages ourselves : + - on win32, we don't want them to end on a non-existing console + - we display critical messages via pop-ups *) -let initmac () = IFDEF QUARTZ THEN gtk_mac_init Coqide.do_load Coqide.forbid_quit_to_save ELSE () END +let catch_gtk_messages () = + let all_levels = + [`FLAG_RECURSION;`FLAG_FATAL;`ERROR;`CRITICAL;`WARNING; + `MESSAGE;`INFO;`DEBUG] + in + let handler ~level msg = + let header = "Coqide internal error: " in + let level_is tag = (level land Glib.Message.log_level tag) <> 0 in + if level_is `ERROR then + let () = GToolbox.message_box ~title:"Error" (header ^ msg) in + Coqide.crash_save 1 + else if level_is `CRITICAL then + GToolbox.message_box ~title:"Error" (header ^ msg) + else if level_is `DEBUG || Sys.os_type = "Win32" then + Ideutils.prerr_endline msg (* no-op unless in debug mode *) + else + Printf.eprintf "%s\n" msg + in + let catch domain = + ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler) + in + List.iter catch ["GLib";"Gtk";"Gdk";"Pango"] -let macready x y z = IFDEF QUARTZ THEN gtk_mac_ready x#as_widget y#as_widget z#as_widget ELSE () END +let () = catch_gtk_messages () (* On win32, we add the directory of coqide to the PATH at launch-time (this used to be done in a .bat script). *) @@ -33,12 +52,18 @@ let set_win32_path () = *) let reroute_stdout_stderr () = + (* We anticipate a bit the argument parsing and look for -debug *) + let debug = List.mem "-debug" (Array.to_list Sys.argv) in + Ideutils.debug := debug; let out_descr = - if !Ideutils.debug then - Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log")) + if debug then + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + Unix.descr_of_out_channel chan else snd (Unix.pipe ()) in + Unix.set_close_on_exec out_descr; Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr @@ -64,10 +89,17 @@ let () = reroute_stdout_stderr () END +IFDEF QUARTZ THEN + let osx = GosxApplication.osxapplication () + + let _ = + osx#connect#ns_application_open_file ~callback:(fun x -> Coqide.do_load x; true) in + let _ = + osx#connect#ns_application_block_termination ~callback:Coqide.forbid_quit_to_save in + () +END + let () = - Coqide.ignore_break (); - ignore (GtkMain.Main.init ()); - initmac () ; (try let gtkrcdir = List.find (fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc")) @@ -82,13 +114,6 @@ let () = end; (* GtkData.AccelGroup.set_default_mod_mask (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*) - ignore ( - Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL; - `WARNING;`CRITICAL] - (fun ~level msg -> - if level land Glib.Message.log_level `WARNING <> 0 - then Printf.eprintf "Warning: %s\n" msg - else failwith ("Coqide internal error: " ^ msg))); let argl = Array.to_list Sys.argv in let argl = Coqide.read_coqide_args argl in let files = Coq.filter_coq_opts (List.tl argl) in @@ -96,9 +121,18 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ()); - macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs") - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt"); + if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ()) + +IFDEF QUARTZ THEN + let () = + GtkosxApplication.Application.set_menu_bar osx#as_osxapplication (GtkMenu.MenuShell.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) in + let () = + GtkosxApplication.Application.insert_app_menu_item osx#as_osxapplication (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 in + let () = + GtkosxApplication.Application.set_help_menu osx#as_osxapplication (Some (GtkMenu.MenuItem.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) in + osx#ready () +END + while true do try GtkThread.main () diff --git a/ide/ide_mac_stubs.c b/ide/ide_mac_stubs.c deleted file mode 100644 index 2aeb2bf4..00000000 --- a/ide/ide_mac_stubs.c +++ /dev/null @@ -1,85 +0,0 @@ -#include <caml/mlvalues.h> -#include <caml/alloc.h> -#include <caml/memory.h> -#include <caml/callback.h> -#include <caml/fail.h> - -#include <gtk/gtk.h> -#include <lablgtk2/wrappers.h> -#include <lablgtk2/ml_glib.h> -#include <lablgtk2/ml_gobject.h> -#include <gtkmacintegration/gtkosxapplication.h> - -GtkOSXApplication *theApp; -value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item; - -static void osx_accel_map_foreach_lcb(gpointer data,const gchar *accel_path, - guint accel_key, GdkModifierType accel_mods, - gboolean changed) { - if (accel_mods & GDK_CONTROL_MASK) { - accel_mods |= GDK_META_MASK; - accel_mods &= (accel_mods & GDK_MOD1_MASK) ? ~GDK_MOD1_MASK : ~GDK_CONTROL_MASK; - if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) { - g_print("could not change accelerator %s\n",accel_path); - } - } - if (accel_mods & GDK_MOD1_MASK) { - accel_mods &= ~ GDK_MOD1_MASK; - accel_mods |= GDK_CONTROL_MASK; - if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) { - g_print("could not change accelerator %s\n",accel_path); - } - } -} - -static gboolean deal_with_open(GtkOSXApplication *app, gchar *path, gpointer user_data) -{ - CAMLparam0(); - CAMLlocal2(string_path, res); - string_path = caml_copy_string(path); - res = caml_callback_exn(open_file_fun,string_path); - gboolean truc = !(Is_exception_result(res)); - CAMLreturnT(gboolean, truc); -} - -static gboolean deal_with_quit(GtkOSXApplication *app, gpointer user_data) -{ - CAMLparam0(); - CAMLlocal1(res); - res = caml_callback_exn(forbid_quit_fun,Val_unit); - gboolean truc = (Bool_val(res))||((Is_exception_result(res))); - CAMLreturnT(gboolean, truc); -} - -CAMLprim value caml_gtk_mac_init(value open_file_the_fun, value forbid_quit_the_fun) -{ - CAMLparam2(open_file_the_fun,forbid_quit_the_fun); - open_file_fun = open_file_the_fun; - caml_register_generational_global_root(&open_file_fun); - forbid_quit_fun = forbid_quit_the_fun; - caml_register_generational_global_root(&forbid_quit_fun); - theApp = g_object_new(GTK_TYPE_OSX_APPLICATION, NULL); - g_signal_connect(theApp, "NSApplicationOpenFile", G_CALLBACK(deal_with_open), NULL); - g_signal_connect(theApp, "NSApplicationBlockTermination", G_CALLBACK(deal_with_quit), NULL); - CAMLreturn (Val_unit); -} - -CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about) -{ - GtkOSXApplicationMenuGroup * pref_grp, * about_grp; - CAMLparam3(menubar,prefs,about); - themenubar = menubar; - pref_item = prefs; - about_item = about; - caml_register_generational_global_root(&themenubar); - caml_register_generational_global_root(&pref_item); - caml_register_generational_global_root(&about_item); - /* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/ - gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar)); - gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1); - gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2); - gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3); - gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4); - gtk_osxapplication_ready(theApp); - CAMLreturn(Val_unit); -} diff --git a/ide/preferences.ml b/ide/preferences.ml index 17216b92..2fb5023f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -35,6 +35,10 @@ let mod_to_str (m:Gdk.Tags.modifier) = | `MOD5 -> "<Mod5>" | `CONTROL -> "<Control>" | `SHIFT -> "<Shift>" + | `HYPER -> "<Hyper>" + | `META -> "<Meta>" + | `RELEASE -> "" + | `SUPER -> "<Super>" | `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> "" let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml index 57939266..905c3485 100644 --- a/ide/utils/okey.ml +++ b/ide/utils/okey.ml @@ -47,6 +47,10 @@ let int_of_modifier = function | `BUTTON3 -> 1024 | `BUTTON4 -> 2048 | `BUTTON5 -> 4096 + | `HYPER -> 1 lsl 22 + | `META -> 1 lsl 20 + | `RELEASE -> 1 lsl 30 + | `SUPER -> 1 lsl 21 let print_modifier l = List.iter @@ -65,7 +69,11 @@ let print_modifier l = | `BUTTON2 -> "B2" | `BUTTON3 -> "B3" | `BUTTON4 -> "B4" - | `BUTTON5 -> "B5") + | `BUTTON5 -> "B5" + | `HYPER -> "HYPER" + | `META -> "META" + | `RELEASE -> "" + | `SUPER -> "SUPER") m)^" ") ) l; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19e1fef5..20b9c2a3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -250,7 +250,9 @@ and check_same_fix_binder bl1 bl2 = check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2) | _ -> failwith "not same binder") bl1 bl2 -let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false +let is_same_type c d = + try let () = check_same_type c d in true + with Failure _ | Invalid_argument _ -> false (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -374,11 +376,12 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | (keyrule,pat,n as _rule)::rules -> try match t,n with - | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or - n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams -> + | PatCstr (loc,(ind,_),l,na), n when (n = Some 0 or n = None or + n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams) + && (match keyrule with SynDefRule _ -> true | _ -> false) -> (* Abbreviation for the constructor name only *) (match keyrule with - | NotationRule (sc,ntn) -> raise No_match + | NotationRule _ -> assert false | SynDefRule kn -> let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 45df005c..81e4501a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1411,7 +1411,8 @@ let internalize sigma globalenv env allow_patvar lvar c = | None -> [], None in let na = match tm', na with - | GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id + | GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) -> + loc,Name id | GRef (loc, VarRef id), None -> loc,Name id | _, None -> dummy_loc,Anonymous | _, Some (loc,na) -> loc,na in diff --git a/kernel/univ.ml b/kernel/univ.ml index 6aeb7390..028eaeb4 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -125,9 +125,12 @@ let sup u v = (* Comparison on this type is pointer equality *) type canonical_arc = - { univ: UniverseLevel.t; lt: UniverseLevel.t list; le: UniverseLevel.t list } + { univ: UniverseLevel.t; + lt: UniverseLevel.t list; + le: UniverseLevel.t list; + rank: int } -let terminal u = {univ=u; lt=[]; le=[]} +let terminal u = {univ=u; lt=[]; le=[]; rank=0} (* A UniverseLevel.t is either an alias for another one, or a canonical one, for which we know the universes that are above *) @@ -405,24 +408,46 @@ let setleq_if (g,arcu) v = (* we assume compare(u,v) = LE *) (* merge u v forces u ~ v with repr u as canonical repr *) let merge g arcu arcv = - match between g arcu arcv with - | arcu::v -> (* arcu is chosen as canonical and all others (v) are *) - (* redirected to it *) - let redirect (g,w,w') arcv = - let g' = enter_equiv_arc arcv.univ arcu.univ g in - (g',list_unionq arcv.lt w,arcv.le@w') - in - let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g_arcu = (g',arcu) in - let g_arcu = List.fold_left setlt_if g_arcu w in - let g_arcu = List.fold_left setleq_if g_arcu w' in - fst g_arcu - | [] -> anomaly "Univ.between" + (* we find the arc with the biggest rank, and we redirect all others to it *) + let arcu, g, v = + let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = + if arc.rank >= max_rank + then (arc.rank, max_rank, arc, best_arc::rest) + else (max_rank, old_max_rank, best_arc, arc::rest) + in + match between g arcu arcv with + | [] -> anomaly "Univ.between" + | arc::rest -> + let (max_rank, old_max_rank, best_arc, rest) = + List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in + if max_rank > old_max_rank then best_arc, g, rest + else begin + (* one redirected node also has max_rank *) + let arcu = {best_arc with rank = max_rank + 1} in + arcu, enter_arc arcu g, rest + end + in + let redirect (g,w,w') arcv = + let g' = enter_equiv_arc arcv.univ arcu.univ g in + (g',list_unionq arcv.lt w,arcv.le@w') + in + let (g',w,w') = List.fold_left redirect (g,[],[]) v in + let g_arcu = (g',arcu) in + let g_arcu = List.fold_left setlt_if g_arcu w in + let g_arcu = List.fold_left setleq_if g_arcu w' in + fst g_arcu (* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *) (* we assume compare(u,v) = compare(v,u) = NLE *) (* merge_disc u v forces u ~ v with repr u as canonical repr *) -let merge_disc g arcu arcv = +let merge_disc g arc1 arc2 = + let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in + let arcu, g = + if arc1.rank <> arc2.rank then arcu, g + else + let arcu = {arcu with rank = succ arcu.rank} in + arcu, enter_arc arcu g + in let g' = enter_equiv_arc arcv.univ arcu.univ g in let g_arcu = (g',arcu) in let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in @@ -563,7 +588,7 @@ let normalize_universes g = in let canonicalize u = function | Equiv _ -> Equiv (repr u) - | Canonical {univ=v; lt=lt; le=le} -> + | Canonical {univ=v; lt=lt; le=le; rank=rank} -> assert (u == v); (* avoid duplicates and self-loops *) let lt = lrepr lt and le = lrepr le in @@ -575,6 +600,7 @@ let normalize_universes g = univ = v; lt = UniverseLSet.elements lt; le = UniverseLSet.elements le; + rank = rank } in UniverseLMap.mapi canonicalize g @@ -632,7 +658,8 @@ let bellman_ford bottom g = let node = Canonical { univ = bottom; lt = []; - le = UniverseLSet.elements vertices + le = UniverseLSet.elements vertices; + rank = 0 } in UniverseLMap.add bottom node g in let rec iter count accu = @@ -692,12 +719,12 @@ let sort_universes orig = | false, true -> push res v | false, false -> res end - | Canonical {univ=v; lt=lt; le=le} -> + | Canonical {univ=v; lt=lt; le=le; rank=r} -> assert (u == v); if filter u then let lt = List.filter filter lt in let le = List.filter filter le in - UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le}) res + UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res else let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in @@ -717,7 +744,8 @@ let sort_universes orig = let g = UniverseLMap.add u (Canonical { univ = u; le = []; - lt = [types.(i+1)] + lt = [types.(i+1)]; + rank = 1 }) g in aux (i+1) g else g in aux 0 g diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index bf931d75..19bab4f6 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -42,6 +42,7 @@ type error_msg = | AttributeValueExpected | EndOfTagExpected of string | EOFExpected + | Empty type error = error_msg * error_pos @@ -117,13 +118,13 @@ let rec read_node s = | Xml_lexer.PCData s -> PCData s | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, []) | Xml_lexer.Tag (tag, attr, false) -> - let elements = read_elems ~tag s in + let elements = read_elems tag s in Element (tag, attr, canonicalize elements) | t -> push t s; raise NoMoreData and - read_elems ?tag s = + read_elems tag s = let elems = ref [] in (try while true do @@ -137,12 +138,8 @@ and with NoMoreData -> ()); match pop s with - | Xml_lexer.Endtag s when Some s = tag -> List.rev !elems - | Xml_lexer.Eof when tag = None -> List.rev !elems - | t -> - match tag with - | None -> raise (Internal_error EOFExpected) - | Some s -> raise (Internal_error (EndOfTagExpected s)) + | Xml_lexer.Endtag s when s = tag -> List.rev !elems + | t -> raise (Internal_error (EndOfTagExpected tag)) let rec read_xml s = let node = read_node s in @@ -162,24 +159,25 @@ let convert = function | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity +let error_of_exn stk = function + | NoMoreData when Stack.pop stk = Xml_lexer.Eof -> Empty + | NoMoreData -> NodeExpected + | Internal_error e -> e + | Xml_lexer.Error e -> convert e + | e -> raise e + let do_parse xparser source = + let stk = Stack.create() in try Xml_lexer.init source; - let s = { source = source; xparser = xparser; stack = Stack.create(); } in + let s = { source = source; xparser = xparser; stack = stk } in let x = read_xml s in if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected); Xml_lexer.close source; x - with - | NoMoreData -> - Xml_lexer.close source; - raise (!xml_error NodeExpected source) - | Internal_error e -> - Xml_lexer.close source; - raise (!xml_error e source) - | Xml_lexer.Error e -> - Xml_lexer.close source; - raise (!xml_error (convert e) source) + with e -> + Xml_lexer.close source; + raise (!xml_error (error_of_exn stk e) source) let parse p = function | SChannel ch -> do_parse p (Lexing.from_channel ch) @@ -208,6 +206,7 @@ let error_msg = function | AttributeValueExpected -> "Attribute value expected" | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag | EOFExpected -> "End of file expected" + | Empty -> "Empty" let error (msg,pos) = if pos.emin = pos.emax then diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index e3e7ac4d..cc9bcd33 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -59,6 +59,7 @@ type error_msg = | AttributeValueExpected | EndOfTagExpected of string | EOFExpected + | Empty type error = error_msg * error_pos diff --git a/myocamlbuild.ml b/myocamlbuild.ml index c866356a..184985b5 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -422,9 +422,9 @@ let extra_rules () = begin if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) in if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-o";Px fo]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]); rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-o";Px fb]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]); in (** Coq files dependencies *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3720eb20..17ef9f85 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -260,7 +260,14 @@ let rec pr_generic prc prlc prtac prpat x = let rec tacarg_using_rule_token pr_gen = function | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al) + | None :: l, a :: al -> + let print_it = + match genarg_tag a with + | OptArgType _ -> fold_opt (fun _ -> true) false a + | _ -> true + in + let r = tacarg_using_rule_token pr_gen (l,al) in + if print_it then pr_gen a :: r else r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" @@ -423,7 +430,7 @@ let pr_clauses default_is_concl pr_id = function (if occs = no_occurrences_expr then mt () else pr_with_occurrences (fun () -> str" |- *") (occs,()))) -let pr_orient b = if b then mt () else str " <-" +let pr_orient b = if b then mt () else str "<- " let pr_multi = function | Precisely 1 -> mt () @@ -806,17 +813,17 @@ and pr_atom1 = function (* Equivalence relations *) | TacReflexivity as x -> pr_atom0 x - | TacSymmetry cls -> str "symmetry " ++ pr_clauses (Some true) pr_ident cls + | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c | TacTransitivity None -> str "etransitivity" (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - hov 1 (str (with_evars ev "rewrite") ++ + hov 1 (str (with_evars ev "rewrite") ++ spc () ++ prlist_with_sep (fun () -> str ","++spc()) (fun (b,m,c) -> - pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) + pr_orient b ++ pr_multi m ++ pr_with_bindings c) l ++ pr_clauses (Some true) pr_ident cl ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index fd134899..956ece79 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -14,6 +14,10 @@ Require Import ExtrOcamlBasic. (** Disclaimer: trying to obtain efficient certified programs by extracting [nat] into [int] is definitively *not* a good idea: + - This is just a syntactic adaptation, many things can go wrong, + such as name captures (e.g. if you have a constant named "int" + in your development, or a module named "Pervasives"). See bug #2878. + - Since [int] is bounded while [nat] is (theoretically) infinite, you have to make sure by yourself that your program will not manipulate numbers greater than [max_int]. Otherwise you should @@ -34,17 +38,17 @@ Require Import ExtrOcamlBasic. (** Mapping of [nat] into [int]. The last string corresponds to a [nat_case], see documentation of [Extract Inductive]. *) -Extract Inductive nat => int [ "0" "succ" ] +Extract Inductive nat => int [ "0" "Pervasives.succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". (** Efficient (but uncertified) versions for usual [nat] functions *) Extract Constant plus => "(+)". -Extract Constant pred => "fun n -> max 0 (n-1)". -Extract Constant minus => "fun n m -> max 0 (n-m)". +Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)". +Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)". Extract Constant mult => "( * )". -Extract Inlined Constant max => max. -Extract Inlined Constant min => min. +Extract Inlined Constant max => "Pervasives.max". +Extract Inlined Constant min => "Pervasives.min". (*Extract Inlined Constant nat_beq => "(=)".*) Extract Inlined Constant EqNat.beq_nat => "(=)". Extract Inlined Constant EqNat.eq_nat_decide => "(=)". diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index c8c40e73..ab634329 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -34,12 +34,12 @@ Extract Inductive N => int [ "0" "" ] (** Efficient (but uncertified) versions for usual functions *) Extract Constant Pos.add => "(+)". -Extract Constant Pos.succ => "succ". -Extract Constant Pos.pred => "fun n -> max 1 (n-1)". -Extract Constant Pos.sub => "fun n m -> max 1 (n-m)". +Extract Constant Pos.succ => "Pervasives.succ". +Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)". +Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)". Extract Constant Pos.mul => "( * )". -Extract Constant Pos.min => "min". -Extract Constant Pos.max => "max". +Extract Constant Pos.min => "Pervasives.min". +Extract Constant Pos.max => "Pervasives.max". Extract Constant Pos.compare => "fun x y -> if x=y then Eq else if x<y then Lt else Gt". Extract Constant Pos.compare_cont => @@ -47,12 +47,12 @@ Extract Constant Pos.compare_cont => Extract Constant N.add => "(+)". -Extract Constant N.succ => "succ". -Extract Constant N.pred => "fun n -> max 0 (n-1)". -Extract Constant N.sub => "fun n m -> max 0 (n-m)". +Extract Constant N.succ => "Pervasives.succ". +Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)". +Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)". Extract Constant N.mul => "( * )". -Extract Constant N.min => "min". -Extract Constant N.max => "max". +Extract Constant N.min => "Pervasives.min". +Extract Constant N.max => "Pervasives.max". Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b". Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b". Extract Constant N.compare => @@ -60,19 +60,19 @@ Extract Constant N.compare => Extract Constant Z.add => "(+)". -Extract Constant Z.succ => "succ". -Extract Constant Z.pred => "pred". +Extract Constant Z.succ => "Pervasives.succ". +Extract Constant Z.pred => "Pervasives.pred". Extract Constant Z.sub => "(-)". Extract Constant Z.mul => "( * )". Extract Constant Z.opp => "(~-)". -Extract Constant Z.abs => "abs". -Extract Constant Z.min => "min". -Extract Constant Z.max => "max". +Extract Constant Z.abs => "Pervasives.abs". +Extract Constant Z.min => "Pervasives.min". +Extract Constant Z.max => "Pervasives.max". Extract Constant Z.compare => "fun x y -> if x=y then Eq else if x<y then Lt else Gt". Extract Constant Z.of_N => "fun p -> p". -Extract Constant Z.abs_N => "abs". +Extract Constant Z.abs_N => "Pervasives.abs". (** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e76c6919..0a17453c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -130,7 +130,7 @@ let rec nb_default_params env c = (* Enriching a signature with implicit information *) -let sign_with_implicits r s = +let sign_with_implicits r s nb_params = let implicits = implicits_of_global r in let rec add_impl i = function | [] -> [] @@ -139,7 +139,7 @@ let sign_with_implicits r s = if sign = Keep && List.mem i implicits then Kill Kother else sign in sign' :: add_impl (succ i) s in - add_impl 1 s + add_impl (1+nb_params) s (* Enriching a exception message *) @@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args = let head = put_magic_if magic1 (MLglob (ConstRef kn)) in (* Now, the extraction of the arguments. *) let s_full = type2signature env (snd schema) in - let s_full = sign_with_implicits (ConstRef kn) s_full in + let s_full = sign_with_implicits (ConstRef kn) s_full 0 in let s = sign_no_final_keeps s_full in let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) let mla = make_mlargs env mle s args metas in let mla = - if not magic1 then + if magic1 || lang () <> Ocaml then mla + else try + (* for better optimisations later, we discard dependent args + of projections and replace them by fake args that will be + removed during final pretty-print. *) let l,l' = list_chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla with _ -> mla - else mla in (* For strict languages, purely logical signatures with at least one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left @@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) let s = List.map (type2sign env) types in - let s = sign_with_implicits (ConstructRef cp) s in + let s = sign_with_implicits (ConstructRef cp) s params_nb in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let l = List.map f oi.ip_types.(i) in (* the corresponding signature *) let s = List.map (type2sign env) oi.ip_types.(i) in - let s = sign_with_implicits r s in + let s = sign_with_implicits r s mi.ind_nparams 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. *) @@ -876,7 +879,7 @@ let extract_std_constant env kn body typ = let l,t' = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s in + let s = sign_with_implicits (ConstRef kn) s 0 in (* Decomposing the top level lambdas of [body]. If there isn't enough, it's ok, as long as remaining args aren't to be pruned (and initial lambdas aren't to be all @@ -923,6 +926,19 @@ let extract_std_constant env kn body typ = in trm, type_expunge_from_sign env s t +(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) +let extract_axiom env kn typ = + reset_meta_count (); + (* The short type [t] (i.e. possibly with abbreviations). *) + let t = snd (record_constant_type env kn (Some typ)) in + (* The real type [t']: without head products, expanded, *) + (* and with [Tvar] translated to [Tvar'] (not instantiable). *) + let l,_ = type_decomp (expand env (var2var' t)) in + let s = List.map (type2sign env) l in + (* Check for user-declared implicit information *) + let s = sign_with_implicits (ConstRef kn) s 0 in + type_expunge_from_sign env s t + let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in let types = Array.make n (Tdummy Kother) @@ -959,8 +975,8 @@ let extract_constant env kn cb = in Dtype (r, vl, t) in let mk_ax () = - let t = snd (record_constant_type env kn (Some typ)) in - Dterm (r, MLaxiom, type_expunge env t) + let t = extract_axiom env kn typ in + Dterm (r, MLaxiom, t) in let mk_def c = let e,t = extract_std_constant env kn c typ in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 257e1c1c..bd997d2d 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -26,9 +26,9 @@ let rec msid_of_mt = function (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) -let se_iter do_decl do_spec = +let se_iter do_decl do_spec do_mp = let rec mt_iter = function - | MTident _ -> () + | MTident mp -> do_mp mp | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in @@ -38,7 +38,12 @@ let se_iter do_decl do_spec = in let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) - | MTwith (mt,_)->mt_iter mt + | MTwith (mt,ML_With_module(idl,mp))-> + let mp_mt = msid_of_mt mt in + let mp_w = + List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl + in + mt_iter mt; do_mp mp_w; do_mp mp | MTsig (_, sign) -> List.iter spec_iter sign and spec_iter = function | (_,Spec s) -> do_spec s @@ -51,15 +56,16 @@ let se_iter do_decl do_spec = me_iter m.ml_mod_expr; mt_iter m.ml_mod_type | (_,SEmodtype m) -> mt_iter m and me_iter = function - | MEident _ -> () + | MEident mp -> do_mp mp | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt | MEapply (me,me') -> me_iter me; me_iter me' | MEstruct (msid, sel) -> List.iter se_iter sel in se_iter -let struct_iter do_decl do_spec s = - List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s +let struct_iter do_decl do_spec do_mp s = + List.iter + (function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) @@ -141,7 +147,7 @@ let decl_ast_search f = function | _ -> () let struct_ast_search f s = - try struct_iter (decl_ast_search f) (fun _ -> ()) s; false + try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false with Found -> true let rec type_search f = function @@ -165,7 +171,9 @@ let spec_type_search f = function | Sval (_,u) -> type_search f u let struct_type_search f s = - try struct_iter (decl_type_search f) (spec_type_search f) s; false + try + struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s; + false with Found -> true @@ -247,34 +255,32 @@ let dfix_to_mlfix rv av i = let c = Array.map (subst 0) av in MLfix(i, ids, c) +(* [optim_se] applies the [normalize] function everywhere and does the + inlining of code. The inlined functions are kept for the moment in + order to preserve the global interface, later [depcheck_se] will get + rid of them if possible *) + let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - if top && i && not (library ()) && not (List.mem r to_appear) - then optim_se top to_appear s lse - else - let d = match optimize_fix a with - | MLfix (0, _, [|c|]) -> - Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) - | a -> Dterm (r, a, t) - in (l,SEdecl d) :: (optim_se top to_appear s lse) + let d = match optimize_fix a with + | MLfix (0, _, [|c|]) -> + Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) + | a -> Dterm (r, a, t) + in + (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in - let all = ref true in (* This fake body ensures that no fixpoint will be auto-inlined. *) let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s - else all := false done; - if !all && top && not (library ()) - && (array_for_all (fun r -> not (List.mem r to_appear)) rv) - then optim_se top to_appear s lse - else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} in (l,SEmodule m) :: (optim_se top to_appear s lse) @@ -289,7 +295,7 @@ and optim_me to_appear s = function (* After these optimisations, some dependencies may not be needed anymore. For non-library extraction, we recompute a minimal set of dependencies - for first-level objects *) + for first-level definitions (no module pruning yet). *) exception NoDepCheck @@ -362,7 +368,7 @@ let rec depcheck_se = function end | t :: se -> let se' = depcheck_se se in - se_iter compute_deps_decl compute_deps_spec t; + se_iter compute_deps_decl compute_deps_spec add_needed_mp t; t :: se' let rec depcheck_struct = function @@ -370,7 +376,7 @@ let rec depcheck_struct = function | (mp,lse)::struc -> let struc' = depcheck_struct struc in let lse' = depcheck_se lse in - (mp,lse')::struc' + if lse' = [] then struc' else (mp,lse')::struc' let check_implicits = function | MLexn s -> @@ -389,9 +395,9 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in ignore (struct_ast_search check_implicits opt_struc); - if library () then opt_struc + if library () then + List.filter (fun (_,lse) -> lse<>[]) opt_struc else begin reset_needed (); List.iter add_needed (fst to_appear); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c88c6669..43b08840 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -308,13 +308,14 @@ let build_constructors_of_type ind' argl = (Global.env ()) construct in - let argl = - if argl = [] - then + let argl = match argl with + | None -> Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) + (Array.init cst_narg (fun _ -> mkGHole ()) ) - else argl + | Some l -> + Array.to_list + (Array.init npar (fun _ -> mkGHole ()))@l in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) @@ -653,7 +654,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind [] in + let case_pats = build_constructors_of_type ind None in assert (Array.length case_pats = 2); let brl = list_map_i @@ -669,12 +670,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GLetTuple(_,nal,_,b,e) -> begin let nal_as_glob_constr = - List.map + Some (List.map (function Name id -> mkGVar id | Anonymous -> mkGHole () ) - nal + nal) in let b_as_constr = Pretyping.Default.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 11d9a071..ab424c22 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -14,14 +14,14 @@ Delimit Scope Int_scope with I. Module Type Int. - Parameter int : Set. + Parameter t : Set. - Parameter zero : int. - Parameter one : int. - Parameter plus : int -> int -> int. - Parameter opp : int -> int. - Parameter minus : int -> int -> int. - Parameter mult : int -> int -> int. + Parameter zero : t. + Parameter one : t. + Parameter plus : t -> t -> t. + Parameter opp : t -> t. + Parameter minus : t -> t -> t. + Parameter mult : t -> t -> t. Notation "0" := zero : Int_scope. Notation "1" := one : Int_scope. @@ -33,14 +33,14 @@ Module Type Int. Open Scope Int_scope. (* First, int is a ring: *) - Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int). + Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t). (* int should also be ordered: *) - Parameter le : int -> int -> Prop. - Parameter lt : int -> int -> Prop. - Parameter ge : int -> int -> Prop. - Parameter gt : int -> int -> Prop. + Parameter le : t -> t -> Prop. + Parameter lt : t -> t -> Prop. + Parameter ge : t -> t -> Prop. + Parameter gt : t -> t -> Prop. Notation "x <= y" := (le x y): Int_scope. Notation "x < y" := (lt x y) : Int_scope. Notation "x >= y" := (ge x y) : Int_scope. @@ -61,7 +61,7 @@ Module Type Int. forall i j k, 0 < k -> i < j -> k*i<k*j. (* We should have a way to decide the equality and the order*) - Parameter compare : int -> int -> comparison. + Parameter compare : t -> t -> comparison. Infix "?=" := compare (at level 70, no associativity) : Int_scope. Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j. Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j. @@ -83,7 +83,7 @@ Module Z_as_Int <: Int. Open Scope Z_scope. - Definition int := Z. + Definition t := Z. Definition zero := 0. Definition one := 1. Definition plus := Z.add. @@ -91,7 +91,7 @@ Module Z_as_Int <: Int. Definition minus := Z.sub. Definition mult := Z.mul. - Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int). + Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t). Proof. constructor. exact Z.add_0_l. @@ -138,6 +138,7 @@ End Z_as_Int. Module IntProperties (I:Int). Import I. + Local Notation int := I.t. (* Primo, some consequences of being a ring theory... *) @@ -827,6 +828,7 @@ Module IntOmega (I:Int). Import I. Module IP:=IntProperties(I). Import IP. +Local Notation int := I.t. (* \subsubsection{Definition of reified integer expressions} Terms are either: @@ -1037,20 +1039,16 @@ Close Scope romega_scope. Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2. Proof. - simple induction t1; intros until t2; case t2; simpl in *; - try (intros; discriminate; fail); - [ intros; elim beq_true with (1 := H); trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 H3; elim H with (1 := H3); trivial - | intros; elim beq_nat_true with (1 := H); trivial ]. + induction t1; destruct t2; simpl in *; try discriminate; + (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal; + auto using beq_true, beq_nat_true. +Qed. + +Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true. +Proof. + induction t0; simpl in *; try (apply andb_true_iff; split); trivial. + - now apply beq_iff. + - now apply beq_nat_true_iff. Qed. Ltac trivial_case := unfold not; intros; discriminate. @@ -1058,31 +1056,7 @@ Ltac trivial_case := unfold not; intros; discriminate. Theorem eq_term_false : forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. Proof. - simple induction t1; - [ intros z t2; case t2; try trivial_case; simpl; unfold not; - intros; elim beq_false with (1 := H); simplify_eq H0; - auto - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3; - unfold not; intro H4; elim H1 with (1 := H3); - simplify_eq H4; auto - | intros n t2; case t2; try trivial_case; simpl; unfold not; - intros; elim beq_nat_false with (1 := H); simplify_eq H0; - auto ]. + intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H. Qed. (* \subsubsection{Tactiques pour éliminer ces tests} @@ -1919,9 +1893,9 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := end end. -Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). +Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace). Proof. - simple induction t; simpl; + simple induction trace; simpl; [ exact reduce_stable | intros stp l H; case stp; [ apply compose_term_stable; @@ -2093,11 +2067,8 @@ Definition constant_not_nul (i : nat) (h : hyps) := Theorem constant_not_nul_valid : forall i : nat, valid_hyps (constant_not_nul i). Proof. - unfold valid_hyps, constant_not_nul; intros; - generalize (nth_valid ep e i lp); Simplify; simpl. - - elim_beq i1 i0; auto; simpl; intros H1 H2; - elim H1; symmetry ; auto. + unfold valid_hyps, constant_not_nul; intros i ep e lp H. + generalize (nth_valid ep e i lp H); Simplify. Qed. (* \paragraph{[O_CONSTANT_NEG]} *) @@ -2131,12 +2102,12 @@ Definition not_exact_divide (k1 k2 : int) (body : term) end. Theorem not_exact_divide_valid : - forall (k1 k2 : int) (body : term) (t i : nat), - valid_hyps (not_exact_divide k1 k2 body t i). + forall (k1 k2 : int) (body : term) (t0 i : nat), + valid_hyps (not_exact_divide k1 k2 body t0 i). Proof. unfold valid_hyps, not_exact_divide; intros; generalize (nth_valid ep e i lp); Simplify. - rewrite (scalar_norm_add_stable t e), <-H1. + rewrite (scalar_norm_add_stable t0 e), <-H1. do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. absurd (interp_term e body * k1 + k2 = 0); [ now apply OMEGA4 | symmetry; auto ]. @@ -2509,9 +2480,9 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := execute_omega cont (apply_oper_2 i1 i2 (state m s) l) end. -Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). +Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). Proof. - simple induction t; simpl; + simple induction tr; simpl; [ unfold valid_list_hyps; simpl; intros; left; apply (constant_not_nul_valid n ep e lp H) | unfold valid_list_hyps; simpl; intros; left; @@ -2522,7 +2493,7 @@ Proof. (apply_oper_1_valid m (divide_and_approx k1 k2 body n) (divide_and_approx_valid k1 k2 body n) ep e lp H) | unfold valid_list_hyps; simpl; intros; left; - apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H) + apply (not_exact_divide_valid _ _ _ _ _ ep e lp H) | unfold valid_list_hyps, valid_hyps; intros k body n t' Ht' m ep e lp H; apply Ht'; apply @@ -2618,10 +2589,10 @@ Qed. (* \subsubsection{Exécution de la trace} *) Theorem execute_goal : - forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps), - interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l. + forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps), + interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l. Proof. - intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). + intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H). Qed. @@ -2936,13 +2907,13 @@ Proof. | intro; apply ne_left_2; assumption ] | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s); simpl; intro H1; - [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1; + [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1; rewrite plus_permute; rewrite plus_opp_r; rewrite plus_0_r; trivial - | apply (fun a b => plus_le_reg_r a b (- interp_term e t)); + | apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); rewrite plus_opp_r; assumption | rewrite ge_le_iff; - apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); + apply (fun a b => plus_le_reg_r a b (- interp_term e t1)); rewrite plus_opp_r; assumption | rewrite gt_lt_iff; apply lt_left_inv; assumption | apply lt_left_inv; assumption diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 6a5878b3..dfcc8526 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -663,6 +663,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) let admit_obligations n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in + let obls = Array.copy obls in Array.iteri (fun i x -> match x.obl_body with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1819dc52..38355cf1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1763,7 +1763,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length arsign) t in + let pred2 = lift (List.length (List.flatten arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 69ff2af9..a74e4cb4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -389,6 +389,8 @@ let rec detype (isgoal:bool) avoid env t = with _ -> GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) + | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> + detype isgoal avoid env c1 | Cast (c1,k,c2) -> GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fa29243a..b0248a84 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -135,15 +135,20 @@ let whd_head_evar_stack sigma c = let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c) -let noccur_evar evd evk c = - let rec occur_rec c = match kind_of_term c with - | Evar (evk',_ as ev') -> +let noccur_evar env evd evk c = + let rec occur_rec k c = match kind_of_term c with + | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec c - | None -> if evk = evk' then raise Occur) - | _ -> iter_constr occur_rec c + | Some c -> occur_rec k c + | None -> + if evk = evk' then raise Occur else Array.iter (occur_rec k) args') + | Rel i when i > k -> + (match pi2 (Environ.lookup_rel (i-k) env) with + | None -> () + | Some b -> occur_rec k (lift i b)) + | _ -> iter_constr_with_binders succ occur_rec k c in - try occur_rec c; true with Occur -> false + try occur_rec 0 c; true with Occur -> false let normalize_evar evd ev = match kind_of_term (whd_evar evd (mkEvar ev)) with @@ -741,7 +746,8 @@ let is_unification_pattern_meta env nb m l t = None let is_unification_pattern_evar env evd (evk,args) l t = - if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then + if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t + then let args = remove_instance_local_defs evd evk (Array.to_list args) in let n = List.length args in match find_unification_pattern_args env (args @ l) t with @@ -1112,10 +1118,11 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ | Not_found -> CannotInvert | NotUnique -> Invertible NoUniqueProjection -let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = +let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in match res with - | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) -> + | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c) + -> CannotInvert | _ -> res @@ -1153,10 +1160,11 @@ let extract_candidates sols = let filter_of_projection = function Invertible _ -> true | _ -> false -let invert_invertible_arg evd aliases k (evk,argsv) args' = +let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in - let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in + let projs = + array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in Array.of_list (extract_unique_projections projs) (* Redefines an evar with a smaller context (i.e. it may depend on less @@ -1364,12 +1372,14 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t = let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= let filter1 = - restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1) + restrict_upon_filter evd evk1 (noccur_evar env evd evk2) + (Array.to_list argsv1) in let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in let filter2 = - restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2) + restrict_upon_filter evd evk2 (noccur_evar env evd evk1) + (Array.to_list argsv2) in let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in @@ -1389,7 +1399,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 try let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in - evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1) + evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1) with | EvarSolvedWhileRestricting (evd,ev1) -> raise (EvarSolvedOnTheFly (evd,ev1)) @@ -1585,7 +1595,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev' ev in + let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in evdref := evd; body with diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 24c5ba5b..8e4b211f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function | GHole (loc,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr) -> PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) + | _ -> raise Not_found + +let rec cases_pattern_of_glob_constr na = function + | GVar (loc,id) when na<>Anonymous -> + (* Unable to manage the presence of both an alias and a variable *) + raise Not_found + | GVar (loc,id) -> PatVar (loc,Name id) + | GHole (loc,_) -> PatVar (loc,na) + | GRef (loc,ConstructRef cstr) -> + PatCstr (loc,cstr,[],na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) | _ -> raise Not_found (* Turn a closed cases pattern into a glob_constr *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 665491e7..22aacb29 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -42,6 +42,11 @@ let e_type_judgment env evdref j = evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j +let e_assumption_of_judgment env evdref j = + try (e_type_judgment env evdref j).utj_val + with TypeError _ -> + error_assumption env j + let e_judge_of_apply env evdref funj argjv = let rec apply_rec n typ = function | [] -> @@ -150,7 +155,7 @@ let rec execute env evdref cstr = | Evar ev -> let ty = Evd.existential_type !evdref ev in let jty = execute env evdref (whd_evar !evdref ty) in - let jty = assumption_of_judgment env jty in + let jty = e_assumption_of_judgment env evdref jty in { uj_val = cstr; uj_type = jty } | Rel n -> @@ -243,7 +248,7 @@ let rec execute env evdref cstr = and execute_recdef env evdref (names,lar,vdef) = let larj = execute_array env evdref lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lara = Array.map (e_assumption_of_judgment env evdref) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c92c183d..63cdb378 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -198,11 +198,18 @@ type unify_flags = { (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *) modulo_delta : Names.transparent_state; - (* This controls which constant are unfoldable; this is on for apply *) + (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; + (* This controls whether unfoldability is different when trying to unify *) + (* several instances of the same metavariable *) + (* Typical situation is when we give a pattern to be matched *) + (* syntactically against a subterm but we want the metas of the *) + (* pattern to be modulo convertibility *) + check_applied_meta_types : bool; (* This controls whether meta's applied to arguments have their *) (* type unified with the type of their instance *) @@ -240,12 +247,13 @@ type unify_flags = { } (* Default flag for unifying a type against a type (e.g. apply) *) -(* We set all conversion flags *) +(* We set all conversion flags (no flag should be modified anymore) *) let default_unify_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; @@ -258,24 +266,22 @@ let default_unify_flags = { (* in fact useless when not used in w_unify_to_subterm_list *) } +let set_merge_flags flags = + match flags.modulo_delta_in_merge with + | None -> flags + | Some ts -> + { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts } + (* Default flag for the "simple apply" version of unification of a *) (* type against a type (e.g. apply) *) (* We set only the flags available at the time the new "apply" extends *) (* out of "simple apply" *) -let default_no_delta_unify_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let default_no_delta_unify_flags = { default_unify_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = false } (* Default flags for looking for subterms in elimination tactics *) @@ -283,36 +289,16 @@ let default_no_delta_unify_flags = { (* allow_K) because only closed terms are involved in *) (* induction/destruct/case/elim and w_unify_to_subterm_list does not *) (* call w_unify for induction/destruct/case/elim (13/6/2011) *) -let elim_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; - modulo_delta = full_transparent_state; - modulo_delta_types = full_transparent_state; - check_applied_meta_types = true; - resolve_evars = false; - use_pattern_unification = true; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; +let elim_flags = { default_unify_flags with restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; - modulo_eta = true; allow_K_in_toplevel_higher_order_unification = true } -let elim_no_delta_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = true; +let elim_no_delta_flags = { elim_flags with modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; - use_meta_bound_pattern_unification = true; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = false; - modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = true } let set_no_head_reduction flags = @@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) = if Evd.is_defined evd evk then let v = Evd.existential_value evd ev in let (evd,metas',evars'') = - unify_0 curenv evd CONV flags rhs v in + unify_0 curenv evd CONV (set_merge_flags flags) rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin (* This can make rhs' ill-typed if metas are *) @@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) = let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = - unify_0 sp_env evd' CUMUL flags + unify_0 sp_env evd' CUMUL (set_merge_flags flags) (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' diff --git a/pretyping/unification.mli b/pretyping/unification.mli index e3fd46af..1ec5c1a2 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -15,6 +15,7 @@ type unify_flags = { use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; check_applied_meta_types : bool; resolve_evars : bool; use_pattern_unification : bool; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ca8fd6ae..d18ee73f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -105,6 +105,7 @@ let fail_quick_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = false; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5e314069..45e4a84e 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -62,9 +62,12 @@ let get_undo _ = None let start_proof id str hyps c ?init_tac ?compute_guard hook = let goals = [ (Global.env_of_context hyps , c) ] in - let init_tac = Option.map Proofview.V82.tactic init_tac in Proof_global.start_proof id str goals ?compute_guard hook; - try Option.iter Proof_global.run_tactic init_tac + let tac = match init_tac with + | Some tac -> Proofview.V82.tactic tac + | None -> Proofview.tclUNIT () + in + try Proof_global.run_tactic tac with e -> Proof_global.discard_current (); raise e let restart_proof () = undo_todepth 1 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c8bf689b..5bc77457 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -63,16 +63,18 @@ let no_start = ref false let is_ocaml4 = Coq_config.caml_version.[0] <> '3' +(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"), + we only need to include directories mentionned in the temp main ml file + below (for accessing the corresponding .cmi). *) + let src_dirs = - [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] + [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]; ] let includes () = - (if !Flags.boot then [] (* the include flags are given on the cmdline *) - else - let coqlib = Envars.coqlib () in - let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in - let camlp4incl = ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] in - List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs camlp4incl) + let coqlib = if !Flags.boot then "." else Envars.coqlib () in + let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in + (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs []) + @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) (* Transform bytecode object file names in native object file names *) @@ -242,8 +244,7 @@ let declare_loading_string () = (* create a temporary main file to link *) let create_tmp_main_file modules = - let main_name = Filename.temp_file "coqmain" ".ml" in - let oc = open_out main_name in + let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in try (* Add the pre-linked modules *) output_string oc "List.iter Mltop.add_known_module [\""; @@ -290,10 +291,10 @@ let main () = [] in (* the list of the loaded modules *) - let main_file = Filename.quote (create_tmp_main_file modules) in + let main_file = create_tmp_main_file modules in try - let args = - options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in + let args = options @ includes () @ copts @ tolink @ dynlink in + let args = args @ [ Filename.quote main_file ] in (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *) let args = if !top then args @ [ "topstart.cmo" ] else args in (* Now, with the .cma, we MUST use the -linkall option *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 041bb44b..f7d63dcd 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1020,6 +1020,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = true; use_pattern_unification = false; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e8ef545d..cf4a267f 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -77,6 +77,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = true; diff --git a/tactics/equality.ml b/tactics/equality.ml index 241a8bd2..a352355b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -87,6 +87,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -155,6 +156,7 @@ let rewrite_conv_closed_unif_flags = { Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = false; Unification.use_pattern_unification = true; diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index d3403a18..613779c2 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -194,7 +194,7 @@ let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" | Some l,_ -> str "in" ++ - Util.prlist (fun id -> spc () ++ pr_id id) l ++ + spc () ++ Util.prlist_with_sep Util.pr_comma pr_id l ++ match concl with | true -> spc () ++ str "|-" ++ spc () ++ str "*" | _ -> mt () diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 8a1b5996..47e3b7ca 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -151,8 +151,9 @@ let match_with_disjunction ?(strict=false) t = | Ind ind -> let car = mis_constr_nargs ind in let (mib,mip) = Global.lookup_inductive ind in - if array_for_all (fun ar -> ar = 1) car && - not (mis_is_recursive (ind,mib,mip)) + if array_for_all (fun ar -> ar = 1) car + && not (mis_is_recursive (ind,mib,mip)) + && (mip.mind_nrealargs = 0) then if strict then if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index dbe61817..b90a911a 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -294,6 +294,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -305,11 +306,12 @@ let rewrite_unif_flags = { Unification.allow_K_in_toplevel_higher_order_unification = true } -let rewrite2_unif_flags = +let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = conv_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -327,6 +329,7 @@ let general_rewrite_unif_flags () = Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ff53bfe8..12292196 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1690,6 +1690,7 @@ let default_matching_flags sigma = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = Some full_transparent_state; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = false; diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index beba8df9..66307236 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -127,3 +127,12 @@ Identifier 'foo' now a keyword : nat fun _ : nat => 9 : nat -> nat +Identifier 'ONE' now a keyword +fun (x : nat) (p : x = x) => match p with + | ONE => ONE + end = p + : forall x : nat, x = x -> Prop +fun (x : nat) (p : x = x) => match p with + | 1 => 1 + end = p + : forall x : nat, x = x -> Prop diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 52f499ab..612b5325 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -262,3 +262,16 @@ Notation "'foo' n" := (S n) (at level 50): nat_scope. Check (foo 9). Check (fun _ : nat => 9). + +(* Checking parsing and printing of numerical and non-numerical notations for eq_refl *) + +(* This notation was not correctly printed until Pierre B.'s + improvements to the interpretation of patterns *) + +Notation "'ONE'" := eq_refl. +Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. + +(* This one used to failed at parsing until now *) + +Notation "1" := eq_refl. +Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index f445ca8e..c9a3c08e 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1865,3 +1865,9 @@ Type (fun n => match n with | Z0 => true | _ => false end). + +(* Check that types with unknown sort, as A below, are not fatal to + the pattern-matching compilation *) + +Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := + match p with eq_refl => u end. diff --git a/test-suite/success/set.v b/test-suite/success/set.v index 23019275..8116e897 100644 --- a/test-suite/success/set.v +++ b/test-suite/success/set.v @@ -1,8 +1,19 @@ +(* This used to fail in 8.0pl1 *) + Goal forall n, n+n=0->0=n+n. intros. - -(* This used to fail in 8.0pl1 *) set n in * |-. +Abort. + +(* This works from 8.4pl1, since merging of different instances of the + same metavariable in a pattern is done modulo conversion *) + +Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). + +Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H. +intros. +set (f _ _). +Abort. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 980cfeac..c68216e6 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -35,6 +35,7 @@ Module Raw (Import I:Int)(X: OrderedType). Local Open Scope pair_scope. Local Open Scope lazy_bool_scope. Local Open Scope Int_scope. +Local Notation int := I.t. Definition key := X.t. Hint Transparent key. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 1e66e2b5..db12ee31 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -44,6 +44,7 @@ Local Unset Case Analysis Schemes. Module Ops (Import I:Int)(X:OrderedType) <: MSetInterface.Ops X. Local Open Scope Int_scope. +Local Notation int := I.t. (** ** Generic trees instantiated with integer height *) diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 37074aba..5582438b 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -147,18 +147,14 @@ Definition lt_total := lt_trichotomy. Definition le_lteq := lt_eq_cases. Module Private_OrderTac. -Module Elts <: TotalOrder. - Definition t := t. - Definition eq := eq. - Definition lt := lt. - Definition le := le. +Module IsTotal. Definition eq_equiv := eq_equiv. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. Definition lt_total := lt_total. Definition le_lteq := le_lteq. -End Elts. -Module Tac := !MakeOrderTac Elts. +End IsTotal. +Module Tac := !MakeOrderTac NZ IsTotal. End Private_OrderTac. Ltac order := Private_OrderTac.Tac.order. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 3b2a372e..a2bc5e26 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -42,6 +42,7 @@ Module BigQ <: QType <: OrderedTypeFull <: TotalOrder. Bind Scope bigQ_scope with t t_. Include !QProperties <+ HasEqBool2Dec <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. + Ltac order := Private_Tac.order. End BigQ. (** Notations about [BigQ] *) @@ -144,8 +145,7 @@ End TestField. (** [BigQ] can also benefit from an "order" tactic *) -Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ. -Ltac bigQ_order := BigQ_Order.order. +Ltac bigQ_order := BigQ.order. Section TestOrder. Let test : forall x y : bigQ, x<=y -> y<=x -> x==y. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 4747cfe1..be585871 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1486,6 +1486,8 @@ Qed. Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Ltac order := Private_Tac.order. + (** Minimum, maximum and constant one *) Lemma max_1_l n : max 1 n = n. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 5583142f..ffd0649a 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -40,34 +40,34 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. Definition max := gmax O.compare. Definition min := gmin O.compare. - Lemma ge_not_lt : forall x y, y<=x -> x<y -> False. + Lemma ge_not_lt x y : y<=x -> x<y -> False. Proof. - intros x y H H'. + intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. transitivity y; auto. rewrite H in H'; auto. Qed. - Lemma max_l : forall x y, y<=x -> max x y == x. + Lemma max_l x y : y<=x -> max x y == x. Proof. intros. unfold max, gmax. case compare_spec; auto with relations. intros; elim (ge_not_lt x y); auto. Qed. - Lemma max_r : forall x y, x<=y -> max x y == y. + Lemma max_r x y : x<=y -> max x y == y. Proof. intros. unfold max, gmax. case compare_spec; auto with relations. intros; elim (ge_not_lt y x); auto. Qed. - Lemma min_l : forall x y, x<=y -> min x y == x. + Lemma min_l x y : x<=y -> min x y == x. Proof. intros. unfold min, gmin. case compare_spec; auto with relations. intros; elim (ge_not_lt y x); auto. Qed. - Lemma min_r : forall x y, y<=x -> min x y == y. + Lemma min_r x y : y<=x -> min x y == y. Proof. intros. unfold min, gmin. case compare_spec; auto with relations. intros; elim (ge_not_lt x y); auto. @@ -76,31 +76,30 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. End GenericMinMax. -(** ** Consequences of the minimalist interface: facts about [max]. *) +(** ** Consequences of the minimalist interface: facts about [max] and [min]. *) -Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O). - Module Import Private_Tac := !MakeOrderTac O. +Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). + Module Import Private_Tac := !MakeOrderTac O O. (** An alternative caracterisation of [max], equivalent to [max_l /\ max_r] *) -Lemma max_spec : forall n m, - (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). +Lemma max_spec n m : + (n < m /\ max n m == m) \/ (m <= n /\ max n m == n). Proof. - intros n m. destruct (lt_total n m); [left|right]. - split; auto. apply max_r. rewrite le_lteq; auto. - assert (m <= n) by (rewrite le_lteq; intuition). - split; auto. apply max_l; auto. + - split; auto. apply max_r. rewrite le_lteq; auto. + - assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. now apply max_l. Qed. (** A more symmetric version of [max_spec], based only on [le]. Beware that left and right alternatives overlap. *) -Lemma max_spec_le : forall n m, +Lemma max_spec_le n m : (n <= m /\ max n m == m) \/ (m <= n /\ max n m == n). Proof. - intros. destruct (max_spec n m); [left|right]; intuition; order. + destruct (max_spec n m); [left|right]; intuition; order. Qed. Instance : Proper (eq==>eq==>iff) le. @@ -108,25 +107,24 @@ Proof. repeat red. intuition order. Qed. Instance max_compat : Proper (eq==>eq==>eq) max. Proof. -intros x x' Hx y y' Hy. -assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). -set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. -rewrite <- Hx, <- Hy in *. -destruct (lt_total x y); intuition order. + intros x x' Hx y y' Hy. + assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). + set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. + rewrite <- Hx, <- Hy in *. + destruct (lt_total x y); intuition order. Qed. - (** A function satisfying the same specification is equal to [max]. *) -Lemma max_unicity : forall n m p, - ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. +Lemma max_unicity n m p : + ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m. Proof. - intros. assert (Hm := max_spec n m). + assert (Hm := max_spec n m). destruct (lt_total n m); intuition; order. Qed. -Lemma max_unicity_ext : forall f, - (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) -> +Lemma max_unicity_ext f : + (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) -> (forall n m, f n m == max n m). Proof. intros. apply max_unicity; auto. @@ -134,12 +132,12 @@ Qed. (** [max] commutes with monotone functions. *) -Lemma max_mono: forall f, +Lemma max_mono f : (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, max (f x) (f y) == f (max x y). Proof. - intros f Eqf Lef x y. + intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. assert (f x <= f y) by (apply Lef; order). order. @@ -148,239 +146,232 @@ Qed. (** *** Semi-lattice algebraic properties of [max] *) -Lemma max_id : forall n, max n n == n. +Lemma max_id n : max n n == n. Proof. - intros. destruct (max_spec n n); intuition. + apply max_l; order. Qed. Notation max_idempotent := max_id (only parsing). -Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p. +Lemma max_assoc m n p : max m (max n p) == max (max m n) p. Proof. - intros. - destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. - destruct (max_spec m p); intuition; order. order. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order. - destruct (max_spec m p); intuition; order. + destruct (max_spec n p) as [(H,E)|(H,E)]; rewrite E; + destruct (max_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. + - apply max_r; order. + - symmetry. apply max_l; order. Qed. -Lemma max_comm : forall n m, max n m == max m n. +Lemma max_comm n m : max n m == max m n. Proof. - intros. - destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. - destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order. + destruct (max_spec m n) as [(H,E)|(H,E)]; rewrite E; + (apply max_r || apply max_l); order. Qed. +Ltac solve_max := + match goal with |- context [max ?n ?m] => + destruct (max_spec n m); intuition; order + end. + (** *** Least-upper bound properties of [max] *) -Lemma le_max_l : forall n m, n <= max n m. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma le_max_l n m : n <= max n m. +Proof. solve_max. Qed. -Lemma le_max_r : forall n m, m <= max n m. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma le_max_r n m : m <= max n m. +Proof. solve_max. Qed. -Lemma max_l_iff : forall n m, max n m == n <-> m <= n. -Proof. - split. intro H; rewrite <- H. apply le_max_r. apply max_l. -Qed. +Lemma max_l_iff n m : max n m == n <-> m <= n. +Proof. solve_max. Qed. -Lemma max_r_iff : forall n m, max n m == m <-> n <= m. -Proof. - split. intro H; rewrite <- H. apply le_max_l. apply max_r. -Qed. +Lemma max_r_iff n m : max n m == m <-> n <= m. +Proof. solve_max. Qed. -Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m. +Lemma max_le n m p : p <= max n m -> p <= n \/ p <= m. Proof. - intros n m p H; destruct (max_spec n m); - [right|left]; intuition; order. + destruct (max_spec n m); [right|left]; intuition; order. Qed. -Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m. -Proof. - intros. split. apply max_le. - destruct (max_spec n m); intuition; order. -Qed. +Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m. +Proof. split. apply max_le. solve_max. Qed. -Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m. +Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m. Proof. - intros. destruct (max_spec n m); intuition; + destruct (max_spec n m); intuition; order || (right; order) || (left; order). Qed. -Lemma max_lub_l : forall n m p, max n m <= p -> n <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_l n m p : max n m <= p -> n <= p. +Proof. solve_max. Qed. -Lemma max_lub_r : forall n m p, max n m <= p -> m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_r n m p : max n m <= p -> m <= p. +Proof. solve_max. Qed. -Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub n m p : n <= p -> m <= p -> max n m <= p. +Proof. solve_max. Qed. -Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_iff n m p : max n m <= p <-> n <= p /\ m <= p. +Proof. solve_max. Qed. -Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_lt n m p : n < p -> m < p -> max n m < p. +Proof. solve_max. Qed. -Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p. -Proof. - intros; destruct (max_spec n m); intuition; order. -Qed. +Lemma max_lub_lt_iff n m p : max n m < p <-> n < p /\ m < p. +Proof. solve_max. Qed. -Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m. -Proof. - intros. - destruct (max_spec p n) as [(LT,E)|(LE,E)]; rewrite E. - assert (LE' := le_max_r p m). order. - apply le_max_l. -Qed. +Lemma max_le_compat_l n m p : n <= m -> max p n <= max p m. +Proof. intros. apply max_lub_iff. solve_max. Qed. -Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p. -Proof. - intros. rewrite (max_comm n p), (max_comm m p). - auto using max_le_compat_l. -Qed. +Lemma max_le_compat_r n m p : n <= m -> max n p <= max m p. +Proof. intros. apply max_lub_iff. solve_max. Qed. -Lemma max_le_compat : forall n m p q, n <= m -> p <= q -> - max n p <= max m q. +Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q. Proof. - intros n m p q Hnm Hpq. + intros Hnm Hpq. assert (LE := max_le_compat_l _ _ m Hpq). assert (LE' := max_le_compat_r _ _ p Hnm). order. Qed. -End MaxLogicalProperties. - - -(** ** Properties concernant [min], then both [min] and [max]. +(** Properties of [min] *) - To avoid too much code duplication, we exploit that [min] can be - seen as a [max] of the reversed order. -*) +Lemma min_spec n m : + (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). +Proof. + destruct (lt_total n m); [left|right]. + - split; auto. apply min_l. rewrite le_lteq; auto. + - assert (m <= n) by (rewrite le_lteq; intuition). + split; auto. now apply min_r. +Qed. -Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). - Include MaxLogicalProperties O M. - Import Private_Tac. - - Module Import Private_Rev. - Module ORev := TotalOrderRev O. - Module MRev <: HasMax ORev. - Definition max x y := M.min y x. - Definition max_l x y := M.min_r y x. - Definition max_r x y := M.min_l y x. - End MRev. - Module MPRev := MaxLogicalProperties ORev MRev. - End Private_Rev. +Lemma min_spec_le n m : + (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m). +Proof. + destruct (min_spec n m); [left|right]; intuition; order. +Qed. Instance min_compat : Proper (eq==>eq==>eq) min. -Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed. +Proof. +intros x x' Hx y y' Hy. +assert (H1 := min_spec x y). assert (H2 := min_spec x' y'). +set (m := min x y) in *; set (m' := min x' y') in *; clearbody m m'. +rewrite <- Hx, <- Hy in *. +destruct (lt_total x y); intuition order. +Qed. -Lemma min_spec : forall n m, - (n < m /\ min n m == n) \/ (m <= n /\ min n m == m). -Proof. intros. exact (MPRev.max_spec m n). Qed. +Lemma min_unicity n m p : + ((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m. +Proof. + assert (Hm := min_spec n m). + destruct (lt_total n m); intuition; order. +Qed. -Lemma min_spec_le : forall n m, - (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m). -Proof. intros. exact (MPRev.max_spec_le m n). Qed. +Lemma min_unicity_ext f : + (forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) -> + (forall n m, f n m == min n m). +Proof. + intros. apply min_unicity; auto. +Qed. -Lemma min_mono: forall f, +Lemma min_mono f : (Proper (eq ==> eq) f) -> (Proper (le ==> le) f) -> forall x y, min (f x) (f y) == f (min x y). Proof. - intros. apply MPRev.max_mono; auto. compute in *; eauto. + intros Eqf Lef x y. + destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; + destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. + assert (f x <= f y) by (apply Lef; order). order. + assert (f y <= f x) by (apply Lef; order). order. Qed. -Lemma min_unicity : forall n m p, - ((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m. -Proof. intros n m p. apply MPRev.max_unicity. Qed. - -Lemma min_unicity_ext : forall f, - (forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) -> - (forall n m, f n m == min n m). -Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed. - -Lemma min_id : forall n, min n n == n. -Proof. intros. exact (MPRev.max_id n). Qed. +Lemma min_id n : min n n == n. +Proof. + apply min_l; order. +Qed. Notation min_idempotent := min_id (only parsing). -Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p. -Proof. intros. symmetry; apply MPRev.max_assoc. Qed. +Lemma min_assoc m n p : min m (min n p) == min (min m n) p. +Proof. + destruct (min_spec n p) as [(H,E)|(H,E)]; rewrite E; + destruct (min_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy. + - symmetry. apply min_l; order. + - apply min_r; order. +Qed. -Lemma min_comm : forall n m, min n m == min m n. -Proof. intros. exact (MPRev.max_comm m n). Qed. +Lemma min_comm n m : min n m == min m n. +Proof. + destruct (min_spec m n) as [(H,E)|(H,E)]; rewrite E; + (apply min_r || apply min_l); order. +Qed. -Lemma le_min_r : forall n m, min n m <= m. -Proof. intros. exact (MPRev.le_max_l m n). Qed. +Ltac solve_min := + match goal with |- context [min ?n ?m] => + destruct (min_spec n m); intuition; order + end. -Lemma le_min_l : forall n m, min n m <= n. -Proof. intros. exact (MPRev.le_max_r m n). Qed. +Lemma le_min_r n m : min n m <= m. +Proof. solve_min. Qed. -Lemma min_l_iff : forall n m, min n m == n <-> n <= m. -Proof. intros n m. exact (MPRev.max_r_iff m n). Qed. +Lemma le_min_l n m : min n m <= n. +Proof. solve_min. Qed. -Lemma min_r_iff : forall n m, min n m == m <-> m <= n. -Proof. intros n m. exact (MPRev.max_l_iff m n). Qed. +Lemma min_l_iff n m : min n m == n <-> n <= m. +Proof. solve_min. Qed. -Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p. -Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed. +Lemma min_r_iff n m : min n m == m <-> m <= n. +Proof. solve_min. Qed. -Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p. -Proof. intros n m p. rewrite (MPRev.max_le_iff m n p); intuition. Qed. +Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p. +Proof. + destruct (min_spec n m); [left|right]; intuition; order. +Qed. + +Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p. +Proof. split. apply min_le. solve_min. Qed. -Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p. -Proof. intros n m p. rewrite (MPRev.max_lt_iff m n p); intuition. Qed. +Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p. +Proof. + destruct (min_spec n m); intuition; + order || (right; order) || (left; order). +Qed. -Lemma min_glb_l : forall n m p, p <= min n m -> p <= n. -Proof. intros n m. exact (MPRev.max_lub_r m n). Qed. +Lemma min_glb_l n m p : p <= min n m -> p <= n. +Proof. solve_min. Qed. -Lemma min_glb_r : forall n m p, p <= min n m -> p <= m. -Proof. intros n m. exact (MPRev.max_lub_l m n). Qed. +Lemma min_glb_r n m p : p <= min n m -> p <= m. +Proof. solve_min. Qed. -Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m. -Proof. intros. apply MPRev.max_lub; auto. Qed. +Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m. +Proof. solve_min. Qed. -Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m. -Proof. intros. rewrite (MPRev.max_lub_iff m n p); intuition. Qed. +Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m. +Proof. solve_min. Qed. -Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m. -Proof. intros. apply MPRev.max_lub_lt; auto. Qed. +Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m. +Proof. solve_min. Qed. -Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m. -Proof. intros. rewrite (MPRev.max_lub_lt_iff m n p); intuition. Qed. +Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m. +Proof. solve_min. Qed. -Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m. -Proof. intros n m. exact (MPRev.max_le_compat_r m n). Qed. +Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m. +Proof. intros. apply min_glb_iff. solve_min. Qed. -Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p. -Proof. intros n m. exact (MPRev.max_le_compat_l m n). Qed. +Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p. +Proof. intros. apply min_glb_iff. solve_min. Qed. -Lemma min_le_compat : forall n m p q, n <= m -> p <= q -> +Lemma min_le_compat n m p q : n <= m -> p <= q -> min n p <= min m q. -Proof. intros. apply MPRev.max_le_compat; auto. Qed. - +Proof. + intros Hnm Hpq. + assert (LE := min_le_compat_l _ _ m Hpq). + assert (LE' := min_le_compat_r _ _ p Hnm). + order. +Qed. (** *** Combined properties of min and max *) -Lemma min_max_absorption : forall n m, max n (min n m) == n. +Lemma min_max_absorption n m : max n (min n m) == n. Proof. intros. destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E. @@ -388,7 +379,7 @@ Proof. destruct (max_spec n m); intuition; order. Qed. -Lemma max_min_absorption : forall n m, min n (max n m) == n. +Lemma max_min_absorption n m : min n (max n m) == n. Proof. intros. destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. @@ -398,35 +389,35 @@ Qed. (** Distributivity *) -Lemma max_min_distr : forall n m p, +Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p). Proof. - intros. symmetry. apply min_mono. + symmetry. apply min_mono. eauto with *. repeat red; intros. apply max_le_compat_l; auto. Qed. -Lemma min_max_distr : forall n m p, +Lemma min_max_distr n m p : min n (max m p) == max (min n m) (min n p). Proof. - intros. symmetry. apply max_mono. + symmetry. apply max_mono. eauto with *. repeat red; intros. apply min_le_compat_l; auto. Qed. (** Modularity *) -Lemma max_min_modular : forall n m p, +Lemma max_min_modular n m p : max n (min m (max n p)) == min (max n m) (max n p). Proof. - intros. rewrite <- max_min_distr. + rewrite <- max_min_distr. destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. rewrite 2 max_l; try order. rewrite min_le_iff; auto. rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed. -Lemma min_max_modular : forall n m p, +Lemma min_max_modular n m p : min n (max m (min n p)) == max (min n m) (min n p). Proof. intros. rewrite <- min_max_distr. @@ -438,7 +429,7 @@ Qed. (** Disassociativity *) -Lemma max_min_disassoc : forall n m p, +Lemma max_min_disassoc n m p : min n (max m p) <= max (min n m) p. Proof. intros. rewrite min_max_distr. @@ -447,24 +438,24 @@ Qed. (** Anti-monotonicity swaps the role of [min] and [max] *) -Lemma max_min_antimono : forall f, +Lemma max_min_antimono f : Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, max (f x) (f y) == f (min x y). Proof. - intros f Eqf Lef x y. + intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. assert (f y <= f x) by (apply Lef; order). order. assert (f x <= f y) by (apply Lef; order). order. Qed. -Lemma min_max_antimono : forall f, +Lemma min_max_antimono f : Proper (eq==>eq) f -> Proper (le==>inverse le) f -> forall x y, min (f x) (f y) == f (max x y). Proof. - intros f Eqf Lef x y. + intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. assert (f y <= f x) by (apply Lef; order). order. @@ -480,11 +471,11 @@ Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). (** Induction principles for [max]. *) -Lemma max_case_strong : forall n m (P:t -> Type), +Lemma max_case_strong n m (P:t -> Type) : (forall x y, x==y -> P x -> P y) -> (m<=n -> P n) -> (n<=m -> P m) -> P (max n m). Proof. -intros n m P Compat Hl Hr. +intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. assert (n<=m) by (rewrite le_lteq; auto). apply (Compat m), Hr; auto. symmetry; apply max_r; auto. @@ -494,26 +485,26 @@ assert (m<=n) by (rewrite le_lteq; auto). apply (Compat n), Hl; auto. symmetry; apply max_l; auto. Defined. -Lemma max_case : forall n m (P:t -> Type), +Lemma max_case n m (P:t -> Type) : (forall x y, x == y -> P x -> P y) -> P n -> P m -> P (max n m). Proof. intros. apply max_case_strong; auto. Defined. (** [max] returns one of its arguments. *) -Lemma max_dec : forall n m, {max n m == n} + {max n m == m}. +Lemma max_dec n m : {max n m == n} + {max n m == m}. Proof. - intros n m. apply max_case; auto with relations. + apply max_case; auto with relations. intros x y H [E|E]; [left|right]; rewrite <-H; auto. Defined. (** Idem for [min] *) -Lemma min_case_strong : forall n m (P:O.t -> Type), +Lemma min_case_strong n m (P:O.t -> Type) : (forall x y, x == y -> P x -> P y) -> (n<=m -> P n) -> (m<=n -> P m) -> P (min n m). Proof. -intros n m P Compat Hl Hr. +intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. assert (n<=m) by (rewrite le_lteq; auto). apply (Compat n), Hl; auto. symmetry; apply min_l; auto. @@ -523,12 +514,12 @@ assert (m<=n) by (rewrite le_lteq; auto). apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined. -Lemma min_case : forall n m (P:O.t -> Type), +Lemma min_case n m (P:O.t -> Type) : (forall x y, x == y -> P x -> P y) -> P n -> P m -> P (min n m). Proof. intros. apply min_case_strong; auto. Defined. -Lemma min_dec : forall n m, {min n m == n} + {min n m == m}. +Lemma min_dec n m : {min n m == n} + {min n m == m}. Proof. intros. apply min_case; auto with relations. intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations. @@ -558,19 +549,19 @@ Module UsualMinMaxLogicalProperties Include MinMaxLogicalProperties O M. - Lemma max_monotone : forall f, Proper (le ==> le) f -> + Lemma max_monotone f : Proper (le ==> le) f -> forall x y, max (f x) (f y) = f (max x y). Proof. intros; apply max_mono; auto. congruence. Qed. - Lemma min_monotone : forall f, Proper (le ==> le) f -> + Lemma min_monotone f : Proper (le ==> le) f -> forall x y, min (f x) (f y) = f (min x y). Proof. intros; apply min_mono; auto. congruence. Qed. - Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f -> + Lemma min_max_antimonotone f : Proper (le ==> inverse le) f -> forall x y, min (f x) (f y) = f (max x y). Proof. intros; apply min_max_antimono; auto. congruence. Qed. - Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f -> + Lemma max_min_antimonotone f : Proper (le ==> inverse le) f -> forall x y, max (f x) (f y) = f (min x y). Proof. intros; apply max_min_antimono; auto. congruence. Qed. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index f84cdf32..75578195 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -108,19 +108,21 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. Proof. intros; destruct (compare x y); auto. Qed. - Module OrderElts <: Orders.TotalOrder. - Definition t := t. - Definition eq := eq. - Definition lt := lt. - Definition le x y := lt x y \/ eq x y. - Definition eq_equiv := eq_equiv. - Definition lt_strorder := lt_strorder. - Definition lt_compat := lt_compat. - Definition lt_total := lt_total. - Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. - Proof. unfold le; intuition. Qed. - End OrderElts. - Module OrderTac := !MakeOrderTac OrderElts. + Module TO. + Definition t := t. + Definition eq := eq. + Definition lt := lt. + Definition le x y := lt x y \/ eq x y. + End TO. + Module IsTO. + Definition eq_equiv := eq_equiv. + Definition lt_strorder := lt_strorder. + Definition lt_compat := lt_compat. + Definition lt_total := lt_total. + Lemma le_lteq x y : TO.le x y <-> lt x y \/ eq x y. + Proof. reflexivity. Qed. + End IsTO. + Module OrderTac := !MakeOrderTac TO IsTO. Ltac order := OrderTac.order. Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 66a672c9..68ffc379 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -40,16 +40,26 @@ Definition trans_ord o o' := Local Infix "+" := trans_ord. -(** ** The requirements of the tactic : [TotalOrder]. +(** ** The tactic requirements : a total order - [TotalOrder] contains an equivalence [eq], - a strict order [lt] total and compatible with [eq], and - a larger order [le] synonym for [lt\/eq]. + We need : + - an equivalence [eq], + - a strict order [lt] total and compatible with [eq], + - a larger order [le] synonym for [lt\/eq]. + + This used to be provided here via a [TotalOrder], but + for technical reasons related to extraction, we now ask + for two sperate parts: relations in a [EqLtLe] + properties in + [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder] *) +Module Type IsTotalOrder (O:EqLtLe) := + IsEq O <+ IsStrOrder O <+ LeIsLtEq O <+ LtIsTotal O. + (** ** Properties that will be used by the [order] tactic *) -Module OrderFacts(Import O:TotalOrder'). +Module OrderFacts (Import O:EqLtLe)(P:IsTotalOrder O). +Include EqLtLeNotation O. (** Reflexivity rules *) @@ -57,7 +67,7 @@ Lemma eq_refl : forall x, x==x. Proof. reflexivity. Qed. Lemma le_refl : forall x, x<=x. -Proof. intros; rewrite le_lteq; right; reflexivity. Qed. +Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed. Lemma lt_irrefl : forall x, ~ x<x. Proof. intros; apply StrictOrder_Irreflexive. Qed. @@ -69,7 +79,7 @@ Proof. auto with *. Qed. Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y. Proof. - intros x y; rewrite 2 le_lteq. intuition. + intros x y; rewrite 2 P.le_lteq. intuition. elim (StrictOrder_Irreflexive x); transitivity y; auto. Qed. @@ -90,7 +100,7 @@ Local Notation "#" := interp_ord. Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition; +destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. @@ -114,19 +124,19 @@ Proof. eauto using eq_trans, eq_sym. Qed. Lemma not_neq_eq : forall x y, ~~x==y -> x==y. Proof. -intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto; +intros x y H. destruct (P.lt_total x y) as [H'|[H'|H']]; auto; destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto. Qed. Lemma not_ge_lt : forall x y, ~y<=x -> x<y. Proof. -intros x y H. destruct (lt_total x y); auto. -destruct H. rewrite le_lteq. intuition. +intros x y H. destruct (P.lt_total x y); auto. +destruct H. rewrite P.le_lteq. intuition. Qed. Lemma not_gt_le : forall x y, ~y<x -> x<=y. Proof. -intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition. +intros x y H. rewrite P.le_lteq. generalize (P.lt_total x y); intuition. Qed. Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y. @@ -138,9 +148,9 @@ End OrderFacts. (** ** [MakeOrderTac] : The functor providing the order tactic. *) -Module MakeOrderTac (Import O:TotalOrder'). - -Include OrderFacts O. +Module MakeOrderTac (Import O:EqLtLe)(P:IsTotalOrder O). +Include OrderFacts O P. +Include EqLtLeNotation O. (** order_eq : replace x by y in all (in)equations hyps thanks to equality EQ (where eq has been hidden in order to avoid @@ -257,37 +267,10 @@ End MakeOrderTac. Module OTF_to_OrderTac (OTF:OrderedTypeFull). Module TO := OTF_to_TotalOrder OTF. - Include !MakeOrderTac TO. + Include !MakeOrderTac OTF TO. End OTF_to_OrderTac. Module OT_to_OrderTac (OT:OrderedType). Module OTF := OT_to_Full OT. Include !OTF_to_OrderTac OTF. End OT_to_OrderTac. - -Module TotalOrderRev (O:TotalOrder) <: TotalOrder. - -Definition t := O.t. -Definition eq := O.eq. -Definition lt := flip O.lt. -Definition le := flip O.le. -Include EqLtLeNotation. - -(* No Instance syntax to avoid saturating the Equivalence tables *) -Definition eq_equiv := O.eq_equiv. - -Instance lt_strorder: StrictOrder lt. -Proof. unfold lt; auto with *. Qed. -Instance lt_compat : Proper (eq==>eq==>iff) lt. -Proof. unfold lt; auto with *. Qed. - -Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. -Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. - -Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. -Proof. - intros x y; unfold lt, eq, flip. - generalize (O.lt_total x y); intuition. -Qed. - -End TotalOrderRev. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 384c046f..99ecd150 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -25,9 +25,6 @@ Module Type Int. Parameter t : Set. Bind Scope Int_scope with t. - (** For compatibility *) - Definition int := t. - Parameter i2z : t -> Z. Parameter _0 : t. @@ -362,7 +359,6 @@ End MoreInt. Module Z_as_Int <: Int. Local Open Scope Z_scope. Definition t := Z. - Definition int := t. Definition _0 := 0. Definition _1 := 1. Definition _2 := 2. @@ -375,7 +371,7 @@ Module Z_as_Int <: Int. Definition gt_le_dec := Z_gt_le_dec. Definition ge_lt_dec := Z_ge_lt_dec. Definition eq_dec := Z.eq_dec. - Definition i2z : int -> Z := fun n => n. + Definition i2z : t -> Z := fun n => n. Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index eedbf422..6f0071a4 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -222,7 +222,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\n"; end; print "install:"; - if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; + if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; print "\n"; if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; if (not_empty cmofiles) then @@ -291,18 +291,18 @@ let implicit () = print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.ml4.d: %.ml4\n"; - print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.ml.d: %.ml\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let cmxs_rules () = + print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in let mllib_rules () = print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; print "%.mllib.d: %.mllib\n"; print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let mlpack_rules () = @@ -411,7 +411,7 @@ let parameters () = print "# DSTROOT to specify a prefix to install path.\n\n"; print "# Here is a hack to make $(eval $(shell works:\n"; print "define donewline\n\n\nendef\n"; - print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\\n' '@'; })))\n"; + print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n" let include_dirs (inc_i,inc_r) = @@ -543,14 +543,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; classify_files_by_root "CMXSFILES" (l1@l2) inc; end; - print "\n"; + print "ifeq '$(HASNATDYNLINK)' 'true'\n"; + print "HASNATDYNLINK_OR_EMPTY := yes\n"; + print "else\n"; + print "HASNATDYNLINK_OR_EMPTY :=\n"; + print "endif\n\n"; section "Definition of the toplevel targets."; print "all: "; if !some_vfile then print "$(VOFILES) "; if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; if !some_mllibfile then print "$(CMAFILES) "; if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile - then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; + then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; print_list "\\\n " other_targets; print "\n\n"; if !some_mlifile then begin diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml index 1a9b9c73..350b59aa 100644 --- a/tools/coq_tex.ml4 +++ b/tools/coq_tex.ml @@ -13,15 +13,6 @@ * Perl isn't as portable as it pretends to be, and is quite difficult * to read and maintain... Let us rewrite the stuff in Caml! *) -let _ = - match Sys.os_type with - | "Unix" -> () - | _ -> begin - print_string "This program only runs under Unix !\n"; - flush stdout; - exit 1 - end - let linelen = ref 72 let output = ref "" let output_specified = ref false @@ -31,6 +22,7 @@ let verbose = ref false let slanted = ref false let hrule = ref false let small = ref false +let boot = ref false let coq_prompt = Str.regexp "Coq < " let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " @@ -86,21 +78,23 @@ let bang = Str.regexp "!" let expos = Str.regexp "^" let tex_escaped s = - let rec trans = parser - | [< s1 = (parser - | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> - "\\" ^ (String.make 1 c) - | [< ''\\' >] -> "{\\char'134}" - | [< ''^' >] -> "{\\char'136}" - | [< ''~' >] -> "{\\char'176}" - | [< '' ' >] -> "~" - | [< ''<' >] -> "{<}" - | [< ''>' >] -> "{>}" - | [< 'c >] -> String.make 1 c); - s2 = trans >] -> s1 ^ s2 - | [< >] -> "" + let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in + let adapt_delim = function + | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "\\" -> "{\\char'134}" + | "^" -> "{\\char'136}" + | "~" -> "{\\char'176}" + | " " -> "~" + | "<" -> "{<}" + | ">" -> "{>}" + | _ -> assert false + in + let adapt = function + | Str.Text s -> s + | Str.Delim s -> adapt_delim s in - trans (Stream.of_string s) + String.concat "" (List.map adapt (Str.full_split delims s)) let encapsule sl c_out s = if sl then @@ -196,11 +190,11 @@ let insert texfile coq_output result = else begin if !verbose then Printf.printf "Coq < %s\n" s; if has_match dot_end_line s then - let bl = next_block (succ k) in + let bl = next_block (succ k) in if !verbose then List.iter print_endline bl; eval 0 else - eval (succ k) + eval (succ k) end in try @@ -266,18 +260,29 @@ let parse_cl () = "-hrule", Arg.Set hrule, " Coq parts are written between 2 horizontal lines"; "-small", Arg.Set small, - " Coq parts are written in small font" + " Coq parts are written in small font"; + "-boot", Arg.Set boot, + " Launch coqtop with the -boot option" ] (fun s -> files := s :: !files) "coq-tex [options] file ..." +let find_coqtop () = + let prog = Sys.executable_name in + try + let size = String.length prog in + let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in + (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7)) + with Not_found -> begin + Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; + "coqtop" + end + let main () = parse_cl (); - if !image = "" then begin - Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; - image := "coqtop" - end; - if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin + if !image = "" then image := Filename.quote (find_coqtop ()); + if !boot then image := !image ^ " -boot"; + if Sys.command (!image ^ " -batch -silent") <> 0 then begin Printf.printf "Error: "; let _ = Sys.command (!image ^ " -batch") in exit 1 diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c929e559..4977a94c 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -288,7 +288,7 @@ let canonize f = | (f,_) :: _ -> escape f | _ -> escape f -let traite_fichier_Coq verbose f = +let rec traite_fichier_Coq verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in @@ -347,7 +347,9 @@ let traite_fichier_Coq verbose f = addQueue deja_vu_v [str]; try let file_str = Hashtbl.find vKnown [str] in - printf " %s.v" (canonize file_str) + let canon = canonize file_str in + printf " %s.v" canon; + traite_fichier_Coq true (canon ^ ".v") with Not_found -> () end | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index d319ce72..14447b06 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -35,17 +35,18 @@ type entry_type = type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string let current_type : entry_type ref = ref Library let current_library = ref "" (** refers to the file being parsed *) -(** [deftable] stores only definitions and is used to interpolate idents - inside comments, which are not globalized otherwise. *) - +(** [deftable] stores only definitions and is used to build the index *) let deftable = Hashtbl.create 97 +(** [byidtable] is used to interpolate idents inside comments, which are not + globalized otherwise. *) +let byidtable = Hashtbl.create 97 + (** [reftable] stores references and definitions *) let reftable = Hashtbl.create 97 @@ -59,25 +60,25 @@ let full_ident sp id = else "" let add_def loc1 loc2 ty sp id = + let fullid = full_ident sp id in + let def = Def (fullid, ty) in for loc = loc1 to loc2 do - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) + Hashtbl.add reftable (!current_library, loc) def done; - Hashtbl.add deftable id (Def (full_ident sp id, ty)) + Hashtbl.add deftable !current_library (fullid, ty); + Hashtbl.add byidtable id (!current_library, fullid, ty) let add_ref m loc m' sp id ty = + let fullid = full_ident sp id in if Hashtbl.mem reftable (m, loc) then () - else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty)); let idx = if id = "<>" then m' else id in - if Hashtbl.mem deftable idx then () - else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty)) - -let add_mod m loc m' id = - Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable m (Mod (m', id)) + if Hashtbl.mem byidtable idx then () + else Hashtbl.add byidtable idx (m', fullid, ty) let find m l = Hashtbl.find reftable (m, l) -let find_string m s = Hashtbl.find deftable s +let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (*s Manipulating path prefixes *) @@ -289,10 +290,7 @@ let all_entries () = let l = try Hashtbl.find bt t with Not_found -> [] in Hashtbl.replace bt t ((s,m) :: l) in - let classify m e = match e with - | Def (s,t) -> add_g s m t; add_bt t s m - | Ref _ | Mod _ -> () - in + let classify m (s,t) = (add_g s m t; add_bt t s m) in Hashtbl.iter classify deftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 8c658a90..0f62a086 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -34,10 +34,11 @@ val type_name : entry_type -> string type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string +(* Find what symbol coqtop said is located at loc in the source file *) val find : coq_module -> loc -> index_entry +(* Find what data is referred to by some string in some coq module *) val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cd33528a..0dc86bc8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -126,9 +126,12 @@ let initialize_texmacs () = let token_tree_texmacs = ref (initialize_texmacs ()) +let token_tree_latex = ref Tokens.empty_ttree +let token_tree_html = ref Tokens.empty_ttree + let initialize_tex_html () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.fold_right (fun (s,l,l') (tt,tt') -> + let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') -> (Tokens.ttree_add tt s l, match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; @@ -151,10 +154,9 @@ let initialize_tex_html () = "Î ", "\\ensuremath{\\Pi}", if_utf8 "Î "; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; (* "fun", "\\ensuremath{\\lambda}" ? *) - ] (Tokens.empty_ttree,Tokens.empty_ttree) - -let token_tree_latex = ref (fst (initialize_tex_html ())) -let token_tree_html = ref (snd (initialize_tex_html ())) + ] (Tokens.empty_ttree,Tokens.empty_ttree) in + token_tree_latex := tree_latex; + token_tree_html := tree_html let add_printing_token s (t1,t2) = (match t1 with None -> () | Some t1 -> @@ -325,9 +327,6 @@ module Latex = struct let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let module_ref m s = - printf "\\coqdocmodule{%s}{%s}" m (escaped s) - let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with @@ -356,12 +355,8 @@ module Latex = struct let reference s = function | Def (fullid,typ) -> defref (get_module false) fullid typ s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,typ) -> ident_ref m fullid typ s - | Mod _ -> - printf "\\coqdocvar{%s}" (escaped s) (*s The sublexer buffers symbol characters and attached uninterpreted ident and try to apply special translation such as, @@ -389,6 +384,7 @@ module Latex = struct last_was_in := false let initialize () = + initialize_tex_html (); Tokens.token_tree := token_tree_latex; Tokens.outfun := output_sublexer_string @@ -534,10 +530,7 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -545,12 +538,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - printf "<hr/>This page has been generated by "; - printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; - printf "</div>\n\n</div>\n\n</body>\n</html>" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; + printf "<hr/>This page has been generated by "; + printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; + printf "</div>\n\n</div>\n\n</body>\n</html>" + end let start_module () = let ln = !lib_name in @@ -620,15 +615,6 @@ module Html = struct | Some n -> n | None -> addr) - let module_ref m s = - match find_module m with - | Local -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External m when !externals -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External _ | Unknown -> - output_string s - let ident_ref m fid typ s = match find_module m with | Local -> @@ -645,12 +631,8 @@ module Html = struct | Def (fullid,ty) -> printf "<a name=\"%s\">" fullid; printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s - | Mod _ -> - printf "<span class=\"id\" type=\"mod\">%s</span>" s let output_sublexer_string doescape issymbchar tag s = let s = if doescape then escaped s else s in @@ -667,6 +649,7 @@ module Html = struct Tokens.output_tagged_symbol_char tag c let initialize () = + initialize_tex_html(); Tokens.token_tree := token_tree_html; Tokens.outfun := output_sublexer_string diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 1e889639..22a36ede 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -21,7 +21,7 @@ let eval_call (call:'a Ide_intf.call) = Xml_utils.print_xml (snd !coqtop) xml_query; flush (snd !coqtop); let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in - let res = Ide_intf.to_answer xml_answer in + let res = Ide_intf.to_answer xml_answer call in prerr_endline (Ide_intf.pr_full_value call res); match res with Interface.Fail _ -> exit 1 | _ -> () diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 0df24c7a..28f97dc8 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -45,7 +45,7 @@ type handler = { evars : unit -> evar list option; hints : unit -> (hint list * hint) option; status : unit -> status; - search : search_flags -> search_answer list; + search : search_flags -> string coq_object list; get_options : unit -> (option_name * option_state) list; set_options : (option_name * option_value) list -> unit; inloadpath : string -> bool; @@ -63,7 +63,7 @@ let goals : goals option call = Goal let evars : evar list option call = Evars let hints : (hint list * hint) option call = Hints let status : status call = Status -let search flags : search_answer list call = Search flags +let search flags : string coq_object list call = Search flags let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s @@ -81,7 +81,7 @@ let abstract_eval_call handler c = | Evars -> Obj.magic (handler.evars () : evar list option) | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) | Status -> Obj.magic (handler.status () : status) - | Search flags -> Obj.magic (handler.search flags : search_answer list) + | Search flags -> Obj.magic (handler.search flags : string coq_object list) | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) | SetOptions opts -> Obj.magic (handler.set_options opts : unit) | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) @@ -130,6 +130,12 @@ let bool_arg tag b = if b then [tag, ""] else [] (** Base types *) +let of_unit () = Element ("unit", [], []) + +let to_unit = function + | Element ("unit", [], []) -> () + | _ -> raise Marshal_error + let of_bool b = if b then constructor "bool" "true" [] else constructor "bool" "false" [] @@ -166,7 +172,8 @@ let to_string = function let of_int i = Element ("int", [], [PCData (string_of_int i)]) let to_int = function -| Element ("int", [], [PCData s]) -> int_of_string s +| Element ("int", [], [PCData s]) -> + (try int_of_string s with Failure _ -> raise Marshal_error) | _ -> raise Marshal_error let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) @@ -232,20 +239,20 @@ let to_search_constraint xml = do_match xml "search_constraint" | "include_blacklist" -> Include_Blacklist | _ -> raise Marshal_error) -let of_search_answer ans = - let path = of_list of_string ans.search_answer_full_path in - let name = of_string ans.search_answer_base_name in - let tpe = of_string ans.search_answer_type in - Element ("search_answer", [], [path; name; tpe]) - -let to_search_answer = function -| Element ("search_answer", [], [path; name; tpe]) -> - let path = to_list to_string path in - let name = to_string name in - let tpe = to_string tpe in { - search_answer_full_path = path; - search_answer_base_name = name; - search_answer_type = tpe; +let of_coq_object f ans = + let prefix = of_list of_string ans.coq_object_prefix in + let qualid = of_list of_string ans.coq_object_qualid in + let obj = f ans.coq_object_object in + Element ("coq_object", [], [prefix; qualid; obj]) + +let to_coq_object f = function +| Element ("coq_object", [], [prefix; qualid; obj]) -> + let prefix = to_list to_string prefix in + let qualid = to_list to_string qualid in + let obj = f obj in { + coq_object_prefix = prefix; + coq_object_qualid = qualid; + coq_object_object = obj; } | _ -> raise Marshal_error @@ -412,51 +419,74 @@ let to_coq_info = function } | _ -> raise Marshal_error -let of_hints = - let of_hint = of_list (of_pair of_string of_string) in - of_option (of_pair (of_list of_hint) of_hint) - -let of_answer (q : 'a call) (r : 'a value) = - let convert = match q with - | Interp _ -> Obj.magic (of_string : string -> xml) - | Rewind _ -> Obj.magic (of_int : int -> xml) - | Goal -> Obj.magic (of_option of_goals : goals option -> xml) - | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) - | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) - | Status -> Obj.magic (of_status : status -> xml) - | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml) - | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) - | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) - | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) - | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) - | Quit -> Obj.magic (fun _ -> Element ("unit", [], [])) - | About -> Obj.magic (of_coq_info : coq_info -> xml) +(** Conversions between ['a value] and xml answers + + When decoding an xml answer, we dynamically check that it is compatible + with the original call. For that we now rely on the fact that all + sub-fonctions [to_xxx : xml -> xxx] check that the current xml element + is "xxx", and raise [Marshal_error] if anything goes wrong. +*) + +type value_type = + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + +let hint = List (Pair (String, String)) +let option_name = List String + +let expected_answer_type = function + | Interp _ -> String + | Rewind _ -> Int + | Goal -> Option Goals + | Evars -> Option (List Evar) + | Hints -> Option (Pair (List hint, hint)) + | Status -> State + | Search _ -> List (Coq_object String) + | GetOptions -> List (Pair (option_name, Option_state)) + | SetOptions _ -> Unit + | InLoadPath _ -> Bool + | MkCases _ -> List (List String) + | Quit -> Unit + | About -> Coq_info + +let of_answer (q : 'a call) (r : 'a value) : xml = + let rec convert ty : 'a -> xml = match ty with + | Unit -> Obj.magic of_unit + | Bool -> Obj.magic of_bool + | String -> Obj.magic of_string + | Int -> Obj.magic of_int + | State -> Obj.magic of_status + | Option_state -> Obj.magic of_option_state + | Coq_info -> Obj.magic of_coq_info + | Goals -> Obj.magic of_goals + | Evar -> Obj.magic of_evar + | List t -> Obj.magic (of_list (convert t)) + | Option t -> Obj.magic (of_option (convert t)) + | Coq_object t -> Obj.magic (of_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) in - of_value convert r - -let to_answer xml = - let rec convert elt = match elt with - | Element (tpe, attrs, l) -> - begin match tpe with - | "unit" -> Obj.magic () - | "string" -> Obj.magic (to_string elt : string) - | "int" -> Obj.magic (to_int elt : int) - | "status" -> Obj.magic (to_status elt : status) - | "bool" -> Obj.magic (to_bool elt : bool) - | "list" -> Obj.magic (to_list convert elt : 'a list) - | "option" -> Obj.magic (to_option convert elt : 'a option) - | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) - | "goals" -> Obj.magic (to_goals elt : goals) - | "evar" -> Obj.magic (to_evar elt : evar) - | "option_value" -> Obj.magic (to_option_value elt : option_value) - | "option_state" -> Obj.magic (to_option_state elt : option_state) - | "coq_info" -> Obj.magic (to_coq_info elt : coq_info) - | "search_answer" -> Obj.magic (to_search_answer elt : search_answer) - | _ -> raise Marshal_error - end - | _ -> raise Marshal_error + of_value (convert (expected_answer_type q)) r + +let to_answer xml (c : 'a call) : 'a value = + let rec convert ty : xml -> 'a = match ty with + | Unit -> Obj.magic to_unit + | Bool -> Obj.magic to_bool + | String -> Obj.magic to_string + | Int -> Obj.magic to_int + | State -> Obj.magic to_status + | Option_state -> Obj.magic to_option_state + | Coq_info -> Obj.magic to_coq_info + | Goals -> Obj.magic to_goals + | Evar -> Obj.magic to_evar + | List t -> Obj.magic (to_list (convert t)) + | Option t -> Obj.magic (to_option (convert t)) + | Coq_object t -> Obj.magic (to_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) in - to_value convert xml + to_value (convert (expected_answer_type c)) xml (** * Debug printing *) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 26c6b671..7d0685b1 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -77,7 +77,7 @@ type handler = { evars : unit -> evar list option; hints : unit -> (hint list * hint) option; status : unit -> status; - search : search_flags -> search_answer list; + search : search_flags -> string coq_object list; get_options : unit -> (option_name * option_state) list; set_options : (option_name * option_value) list -> unit; inloadpath : string -> bool; @@ -104,7 +104,7 @@ val of_call : 'a call -> xml val to_call : xml -> 'a call val of_answer : 'a call -> 'a value -> xml -val to_answer : xml -> 'a value +val to_answer : xml -> 'a call -> 'a value (** * Debug printing *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 681eec0d..d67b272e 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -127,25 +127,25 @@ let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.string_of_id id in let type_s = string_of_ppcmds (pr_ltype_env env ast) in [ - ("clear "^id_s),("clear "^id_s^".\n"); - ("apply "^id_s),("apply "^id_s^".\n"); - ("exact "^id_s),("exact "^id_s^".\n"); - ("generalize "^id_s),("generalize "^id_s^".\n"); - ("absurd <"^id_s^">"),("absurd "^type_s^".\n") + ("clear "^id_s),("clear "^id_s^"."); + ("apply "^id_s),("apply "^id_s^"."); + ("exact "^id_s),("exact "^id_s^"."); + ("generalize "^id_s),("generalize "^id_s^"."); + ("absurd <"^id_s^">"),("absurd "^type_s^".") ] @ [ - ("discriminate "^id_s),("discriminate "^id_s^".\n"); - ("injection "^id_s),("injection "^id_s^".\n") + ("discriminate "^id_s),("discriminate "^id_s^"."); + ("injection "^id_s),("injection "^id_s^".") ] @ [ - ("rewrite "^id_s),("rewrite "^id_s^".\n"); - ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") + ("rewrite "^id_s),("rewrite "^id_s^"."); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".") ] @ [ - ("elim "^id_s), ("elim "^id_s^".\n"); - ("inversion "^id_s), ("inversion "^id_s^".\n"); - ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") + ("elim "^id_s), ("elim "^id_s^"."); + ("inversion "^id_s), ("inversion "^id_s^"."); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".") ] let concl_next_tac sigma concl = - let expand s = (s,s^".\n") in + let expand s = (s,s^".") in List.map expand ([ "intro"; "intros"; @@ -312,16 +312,26 @@ let search flags = in let ans = ref [] in let print_function ref env constr = - let name = Names.string_of_id (Nametab.basename_of_global ref) in - let make_path = Names.string_of_id in - let path = - List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref)) - in - let answer = { - Interface.search_answer_full_path = path; - Interface.search_answer_base_name = name; - Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr); - } in + let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in + let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in + let (shortpath, basename) = Libnames.repr_qualid qualid in + let shortpath = repr_dirpath shortpath in + (* [shortpath] is a suffix of [fullpath] and we're looking for the missing + prefix *) + let rec prefix full short accu = match full, short with + | _, [] -> + let full = List.rev_map string_of_id full in + (full, accu) + | _ :: full, m :: short -> + prefix full short (string_of_id m :: accu) + | _ -> assert false + in + let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in + let answer = { + Interface.coq_object_prefix = prefix; + Interface.coq_object_qualid = qualid; + Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr); + } in ans := answer :: !ans; in let () = Search.gen_filtered_search filter_function print_function in @@ -432,6 +442,9 @@ let loop () = let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in Ide_intf.of_answer q r with + | Xml_parser.Error (Xml_parser.Empty, _) -> + pr_debug ("End of input, exiting"); + exit 0 | Xml_parser.Error (err, loc) -> let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in fail msg diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 39fb2a0e..7b4312a3 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -86,10 +86,14 @@ type search_constraint = the flag should be negated. *) type search_flags = (search_constraint * bool) list -type search_answer = { - search_answer_full_path : string list; - search_answer_base_name : string; - search_answer_type : string; +(** A named object in Coq. [coq_object_qualid] is the shortest path defined for + the user. [coq_object_prefix] is the missing part to recover the fully + qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid]. + [coq_object_object] is the actual content of the object. *) +type 'a coq_object = { + coq_object_prefix : string list; + coq_object_qualid : string list; + coq_object_object : 'a; } type coq_info = { diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fe6bf7db..6618b695 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -208,7 +208,7 @@ let show_match id = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in msg (v 1 (str "match # with" ++ fnl () ++ - prlist_with_sep fnl pr_branch patterns ++ fnl ())) + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) (* "Print" commands *) |