diff options
153 files changed, 1108 insertions, 2053 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 512a9c99eb..98fe2546b5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -96,16 +96,11 @@ /engine/uState.* @SkySkimmer # Secondary maintainer @mattam82 -########## Grammar macros ########## - -/grammar/ @ppedrot -# Secondary maintainer @maximedenes - ########## CoqIDE ########## /ide/ @ppedrot /test-suite/ide/ @ppedrot -# Secondary maintainer @gares +# Secondary maintainers @gares @herbelin ########## Interpretation ########## @@ -132,8 +127,9 @@ ########## Parser ########## -/parsing/ @herbelin -# Secondary maintainer @mattam82 +/coqpp/ @coq/parsing-maintainers +/gramlib/ @coq/parsing-maintainers +/parsing/ @coq/parsing-maintainers ########## Plugins ########## @@ -166,15 +162,11 @@ /plugins/setoid_ring/ @amahboubi # Secondary maintainer @bgregoir -/plugins/ssrmatching/ @gares -# Secondary maintainer @maximedenes +/plugins/ssrmatching/ @coq/ssreflect-maintainers +/plugins/ssr/ @coq/ssreflect-maintainers +/test-suite/ssr/ @coq/ssreflect-maintainers -/plugins/ssr/ @gares -/test-suite/ssr/ @gares -# Secondary maintainer @maximedenes - -/plugins/syntax/ @ppedrot -# Secondary maintainer @maximedenes +/plugins/syntax/ @coq/parsing-maintainers /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin @@ -274,16 +266,6 @@ /theories/Vectors/ @herbelin -########## Dune ########## - -/.ocamlinit @ejgallego -/Makefile.dune @ejgallego -/tools/coq_dune* @ejgallego -/dune* @ejgallego -/coq.opam @ejgallego -/ide/coqide.opam @ejgallego -# Secondary maintainer @Zimmi48 - ########## Tools ########## /tools/coqdoc/ @silene @@ -320,6 +302,8 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes +/vernac/metasyntax.* @coq/parsing-maintainers + ########## Test suite ########## /test-suite/Makefile @gares @@ -358,3 +342,10 @@ /dev/tools/update-compat.py @JasonGross /test-suite/tools/update-compat/ @JasonGross # Secondary maintainer @Zimmi48 + +########## Dune ########## + +/.ocamlinit @ejgallego +*dune* @ejgallego +*.opam @ejgallego +# Secondary maintainer @Zimmi48 diff --git a/.gitignore b/.gitignore index e513837445..da675309e5 100644 --- a/.gitignore +++ b/.gitignore @@ -165,6 +165,9 @@ user-contrib plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml +# gramlib__pack +gramlib__pack + # ocaml dev files .merlin META.coq diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ea7eccb47f..45597851ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-10-30-V1" + CACHEKEY: "bionic_coq-V2018-11-08-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -436,9 +436,6 @@ ci-mtac2: ci-paramcoq: <<: *ci-template -ci-pidetop: - <<: *ci-template - ci-plugin_tutorial: <<: *ci-template diff --git a/.merlin.in b/.merlin.in index 404a7e7935..db7259dd6f 100644 --- a/.merlin.in +++ b/.merlin.in @@ -40,6 +40,8 @@ S API B API S ide B ide +S gramlib__pack +B gramlib__pack S tools B tools @@ -51,4 +53,4 @@ B dev S plugins/** B plugins/** -PKG threads.posix camlp5 +PKG threads.posix diff --git a/.travis.yml b/.travis.yml index 6f625b1c75..02b94f4a8e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,6 @@ env: - NJOBS=2 - COMPILER="4.07.0" - DUNE_VER=".1.2.1" - - CAMLP5_VER=".7.06" - FINDLIB_VER=".1.8.0" - LABLGTK="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" @@ -56,7 +55,7 @@ matrix: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list - - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} + - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM} - opam list - if: NOT (type = pull_request) @@ -81,7 +80,7 @@ matrix: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list - - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} + - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM} - opam list before_deploy: - dev/build/osx/make-macos-dmg.sh diff --git a/CHANGES.md b/CHANGES.md index 9a38b18a25..5ff90b5123 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,20 @@ Changes from 8.9 to 8.10 ======================== +OCaml and dependencies + +- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + INSTALL file for more information on dependencies. + +- Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a + fork of the core parsing library that Coq uses, which is a small + subset of the whole Camlp5 distribution. In particular, this subset + doesn't depend on the OCaml AST, allowing easier compilation and + testing on experimental OCaml versions. + + The Coq developers would like to thank Daniel de Rauglaudre for many + years of continued support. + Coqide - CoqIDE now properly sets the module name for a given file based on @@ -13,11 +27,6 @@ Coqtop proper -R/-Q options. For example, given -R Foo foolib using -topfile foolib/bar.v will set the module name to Foo.Bar. -OCaml - -- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the - INSTALL file for more information on dependencies. - Specification language, type inference - Fixing a missing check in interpreting instances of existential @@ -111,6 +120,10 @@ Universes - Added `Print Universes Subgraph` variant of `Print Universes`. Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` +Misc + +- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -39,9 +39,6 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 7.03) - (available at https://camlp5.github.io/) - - GNU Make version 3.81 or later - a C compiler @@ -49,14 +46,14 @@ WHAT DO YOU NEED ? - for CoqIDE, the lablgtk development files (version >= 2.18.5), and the GTK 2.x libraries including gtksourceview2. - Note that num, camlp5 and lablgtk should be properly registered with + Note that num and lablgtk should be properly registered with findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview + $ opam install num ocamlfind lablgtk conf-gtksourceview should get you a reasonable OCaml environment to compile Coq. @@ -96,19 +93,14 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). bigger), you will also need the "ocamlopt" (or its native code version "ocamlopt.opt") command. -2- Check that you have Camlp5 installed on your computer and that the - command "camlp5" lies in a directory which is present in your $PATH - environment variable path. (You need Camlp5 in both bytecode and - native versions if your platform supports it). - -3- The uncompression and un-tarring of the distribution file gave birth +2- The uncompression and un-tarring of the distribution file gave birth to a directory named "coq-8.xx". You can rename this directory and put it wherever you want. Just keep in mind that you will need some spare space during the compilation (reckon on about 300 Mb of disk space for the whole system in native-code compilation). Once installed, the binaries take about 30 Mb, and the library about 200 Mb. -4- First you need to configure the system. It is done automatically with +3- First you need to configure the system. It is done automatically with the command: ./configure <options> @@ -171,7 +163,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). c.f. https://caml.inria.fr/mantis/view.php?id=7630 -5- Still in the root directory, do +4- Still in the root directory, do make @@ -183,7 +175,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). it is recommended to compile in parallel, via make -jN where N is your number of cores. -6- You can now install the Coq system. Executables, libraries, manual pages +5- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at configuration time (step 3). Just do @@ -192,7 +184,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). Of course, you may need superuser rights to do that. -7- Optionally, you could build the bytecode version of Coq via: +6- Optionally, you could build the bytecode version of Coq via: make byte @@ -204,7 +196,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml toplevel accessible via the Drop command. -8- You can now clean all the sources. (You can even erase them.) +7- You can now clean all the sources. (You can even erase them.) make clean diff --git a/META.coq.in b/META.coq.in index 16928587cb..181887bc3d 100644 --- a/META.coq.in +++ b/META.coq.in @@ -4,19 +4,7 @@ description = "The Coq Proof Assistant Plugin API" version = "8.10" directory = "" -requires = "camlp5" - -package "grammar" ( - - description = "Coq Camlp5 Grammar Extensions for Plugins" - version = "8.10" - - requires = "camlp5.gramlib" - directory = "grammar" - - archive(byte) = "grammar.cma" - archive(native) = "grammar.cmxa" -) +requires = "" package "config" ( @@ -153,12 +141,24 @@ package "proofs" ( ) +package "gramlib" ( + + description = "Coq Grammar Engine" + version = "8.10" + + requires = "" + directory = "gramlib__pack" + + archive(byte) = "gramlib.cma" + archive(native) = "gramlib.cmxa" +) + package "parsing" ( description = "Coq Parsing Engine" version = "8.10" - requires = "camlp5.gramlib, coq.proofs" + requires = "coq.gramlib, coq.proofs" directory = "parsing" archive(byte) = "parsing.cma" @@ -94,6 +94,10 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENMLGFILES:= $(MLGFILES:.mlg=.ml) +# GRAMFILES must be in linking order +export GRAMFILES=$(addprefix gramlib__pack/gramlib__,Ploc Plexing Gramext Grammar) +export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) +export GENGRAMFILES := $(GRAMMLFILES) gramlib__pack/gramlib.ml export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) @@ -121,7 +125,6 @@ help: @echo " make clean" @echo "or make archclean" @echo "For make to be verbose, add VERBOSE=1" - @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo @echo "Bytecode compilation is now a separate target:" @echo " make byte" @@ -190,12 +193,16 @@ META.coq: META.coq.in .PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean -clean: objclean cruftclean depclean docclean camldevfilesclean +clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean objclean: archclean indepclean +.PHONY: gramlibclean +gramlibclean: + rm -rf gramlib__pack/ + cruftclean: mlgclean find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + rm -f gmon.out core @@ -284,7 +291,7 @@ KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ - $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma + gramlib__pack/gramlib.cma gramlib__pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) alienclean: diff --git a/Makefile.build b/Makefile.build index ee856aae8e..8e4b63c364 100644 --- a/Makefile.build +++ b/Makefile.build @@ -22,10 +22,6 @@ # set this variable to 1 (or any non-empty value): VERBOSE ?= -# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files -# will be generated in a human-readable format rather than in a binary format. -READABLE_ML4 ?= - # When non-empty, a time command is performed at each .v compilation. # To collect compilation timings of .v and import them in a spreadsheet, # you could hence consider: make TIMED=1 2> timings.csv @@ -199,14 +195,14 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP5LIB) +MLINCLUDES=$(LOCALINCLUDES) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) -DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol) +DEPFLAGS=$(LOCALINCLUDES) -map gramlib__pack/gramlib.ml $(if $(filter plugins/%,$@),, -I ide -I ide/protocol) # On MacOS, the binaries are signed, except our private ones ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) @@ -253,20 +249,9 @@ define ocamlbyte $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^ endef -# Camlp5 settings - -CAMLP5DEPS:=grammar/grammar.cma -CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) - -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -# XXX unused but should be used for mlp files - # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads -# We do not repeat the dependencies already in SYSMOD here -P4CMA:=gramlib.cma - ########################################################################### # Infrastructure for the rest of the Makefile ########################################################################### @@ -336,70 +321,15 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/ $(SHOW)'CCDEP $<' $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) -########################################################################### -# grammar/grammar.cma -########################################################################### - -## In this part, we compile grammar/grammar.cma -## without relying on .d dependency files, for bootstraping the creation -## and inclusion of these .d files - -## Explicit dependencies for grammar stuff - -GRAMBASEDEPS := grammar/q_util.cmi -GRAMCMO := grammar/q_util.cmo \ - grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) -grammar/argextend.cmo : $(GRAMBASEDEPS) -grammar/q_util.cmo : $(GRAMBASEDEPS) -grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo -grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ - grammar/argextend.cmo - coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo -## Ocaml compiler with the right options and -I for grammar - -GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ - -I $(MYCAMLP5LIB) -I grammar - -## Specific rules for grammar.cma - -grammar/grammar.cma : $(GRAMCMO) - $(SHOW)'Testing $@' - @touch grammar/test.mlp - $(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test - @rm -f grammar/test.* grammar/test - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) $^ -linkall -a -o $@ - $(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) -I coqpp $^ -linkall -o $@ - -## Support of Camlp5 and Camlp5 - -COMPATCMO:= -GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -GRAMPP:=$(CAMLP5O) -I $(MYCAMLP5LIB) $(GRAMP4USE) $(CAMLP5COMPAT) -impl - -## Rules for standard .mlp and .mli files in grammar/ - -grammar/%.cmo: grammar/%.mlp | $(COMPATCMO) - $(SHOW)'OCAMLC -c -pp $<' - $(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $< - -grammar/%.cmo: grammar/%.ml | $(COMPATCMO) - $(SHOW)'OCAMLC -c -pp $<' - $(HIDE)$(GRAMC) -c $< - -grammar/%.cmi: grammar/%.mli - $(SHOW)'OCAMLC -c $<' - $(HIDE)$(GRAMC) -c $< - + $(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@ ########################################################################### # Main targets (coqtop.opt, coqtop.byte) @@ -407,7 +337,7 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) $(GRAMMARCMA) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target @@ -418,7 +348,7 @@ $(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST)) bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ $(STRIP_HIDE) $@ $(CODESIGN_HIDE) $@ @@ -427,7 +357,7 @@ bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMO) $(BYTEFLAGS) $< -o $@ COQTOP_BYTE=topbin/coqtop_byte_bin.ml @@ -438,7 +368,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + $(SYSMOD) -package compiler-libs.toplevel \ $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@ # For coqc @@ -612,7 +542,7 @@ VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m validate: $(CHICKEN) | $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot -debug $(VALIDOPTS) $(ALLMODS) + $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' @@ -630,15 +560,40 @@ test-suite: world byte $(ALLSTDLIB).v # Default rules for compiling ML code ########################################################################### -# Target for libraries .cma and .cmxa +gramlib__pack: + mkdir -p $@ -# The dependency over the .mllib is somewhat artificial, since -# ocamlc -a won't use this file, hence the $(filter-out ...) below. -# But this ensures that the .cm(x)a is rebuilt when needed, -# (especially when removing a module in the .mllib). -# We used to have a "order-only" dependency over .mllib.d here, -# but the -include mechanism should already ensure that we have -# up-to-date dependencies. +# gramlib.ml contents +gramlib__pack/gramlib.ml: | gramlib__pack + echo " \ +module Ploc = Gramlib__Ploc \ +module Plexing = Gramlib__Plexing \ +module Gramext = Gramlib__Gramext \ +module Grammar = Gramlib__Grammar" > $@ + +gramlib__pack/gramlib__P%: gramlib/p% | gramlib__pack + cp -a $< $@ + sed -e "1i # 1 \"$<\"" -i $@ +gramlib__pack/gramlib__G%: gramlib/g% | gramlib__pack + cp -a $< $@ + sed -e "1i # 1 \"$<\"" -i $@ + +# Specific rules for gramlib to pack it Dune / OCaml 4.08 style +GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) + +gramlib__pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49 +gramlib__pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49 + +gramlib__pack/gramlib.%: COND_OPENFLAGS= +gramlib__pack/gramlib__%: COND_OPENFLAGS=-open Gramlib + +gramlib__pack/gramlib.cma: $(GRAMOBJS) gramlib__pack/gramlib.cmo + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^ + +gramlib__pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib__pack/gramlib.cmx + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^ # Specific rule for kernel.cma, with $(VMBYTEFLAGS). # This helps loading dllcoqrun.so during an ocamldebug @@ -651,6 +606,16 @@ kernel/kernel.cmxa: kernel/kernel.mllib $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^) +# Target for libraries .cma and .cmxa + +# The dependency over the .mllib is somewhat artificial, since +# ocamlc -a won't use this file, hence the $(filter-out ...) below. +# But this ensures that the .cm(x)a is rebuilt when needed, +# (especially when removing a module in the .mllib). +# We used to have a "order-only" dependency over .mllib.d here, +# but the -include mechanism should already ensure that we have +# up-to-date dependencies. + %.cma: %.mllib $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) @@ -672,11 +637,14 @@ kernel/kernel.cmxa: kernel/kernel.mllib COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,) COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,) +# For module packing +COND_OPENFLAGS= + COND_BYTEFLAGS= \ - $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) + $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_OPENFLAGS) COND_OPTFLAGS= \ - $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) + $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_OPENFLAGS) plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' @@ -780,12 +748,13 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack -MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) -MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) +MAINMLFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES)) +MAINMLLIBFILES := $(filter-out gramlib__pack/% checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) -$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) +$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(GENGRAMFILES) $(SHOW)'OCAMLDEP MLFILES MLIFILES' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(MAINMLFILES) $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) -passrest $(MAINMLFILES) -open Gramlib $(GRAMMLFILES) $(TOTARGET) +#NB: -passrest is needed to avoid ocamlfind reordering the -open Gramlib $(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) $(SHOW)'OCAMLLIBDEP MLLIBFILES MLPACKFILES' diff --git a/Makefile.ci b/Makefile.ci index 88ea64974a..d0b87fc58b 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-pidetop \ ci-plugin_tutorial \ ci-quickchick \ ci-sf \ diff --git a/Makefile.common b/Makefile.common index f2a11ee4b4..ca2cb8fee6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -91,7 +91,7 @@ MKDIR:=install -d CORESRCDIRS:=\ coqpp \ config clib lib kernel kernel/byterun library \ - engine pretyping interp proofs parsing printing \ + engine pretyping interp proofs gramlib__pack parsing printing \ tactics vernac stm toplevel PLUGINDIRS:=\ @@ -119,11 +119,10 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + gramlib__pack/gramlib.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma -GRAMMARCMA:=grammar/grammar.cma - ########################################################################### # plugins object files ########################################################################### diff --git a/Makefile.ide b/Makefile.ide index 39af1f8545..cae77ee348 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -147,7 +147,7 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ $(STRIP_HIDE) $@ $(CODESIGN_HIDE) $@ @@ -156,7 +156,7 @@ $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib \ + $(SYSMOD) \ $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@ #################### diff --git a/Makefile.install b/Makefile.install index be6fe54933..8233807e03 100644 --- a/Makefile.install +++ b/Makefile.install @@ -93,7 +93,7 @@ install-tools: INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ - $(PLUGINS:.cmo=.cmi) + $(PLUGINS:.cmo=.cmi) gramlib__pack/gramlib.cmi INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \ configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \ diff --git a/checker/dune b/checker/dune index 3ab4f50d13..ee427d26c5 100644 --- a/checker/dune +++ b/checker/dune @@ -1,26 +1,3 @@ -(copy_files# - %{project_root}/kernel/{names,esubst,declarations,environ,constr,term,univ,evar,sorts,uGraph,context}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{mod_subst,vars,opaqueproof,conv_oracle,reduction,typeops,inductive,indtypes,declareops,type_errors}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{modops,mod_typing,}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{cClosure,cPrimitives,csymtable,vconv,vm,uint31,cemitcodes,vmvalues,cbytecodes,cinstr,retroknowledge,copcodes}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{cbytegen,clambda,nativeinstr,nativevalues,nativeconv,nativecode,nativelib,nativelibrary,nativelambda}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking,transparentState}.ml{,i}) - -; VM stuff - -(copy_files# - %{project_root}/kernel/byterun/{*.c,*.h}) - ; Careful with bug https://github.com/ocaml/odoc/issues/148 ; ; If we don't pack checker we will have a problem here due to @@ -30,10 +7,8 @@ (public_name coq.checklib) (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) - (modules_without_implementation cinstr nativeinstr) - (c_names coq_fix_code coq_memory coq_values coq_interp) (wrapped true) - (libraries coq.lib)) + (libraries coq.kernel)) (executable (name coqchk) diff --git a/checker/include b/checker/include index da0346359b..3ffc301724 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp5";; #load "unix.cma";; #load"threads.cma";; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ed617d73c2..77f4cea0c6 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -3,7 +3,6 @@ open Util open Names open Reduction open Typeops -open Subtyping open Declarations open Environ @@ -65,17 +64,17 @@ let rec check_module env mp mb = check_signature env mb.mod_type mb.mod_mp mb.mod_delta in let optsign = match mb.mod_expr with - |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta) + |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta) |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta) |Abstract|FullStruct -> None in match optsign with |None -> () - |Some sign -> - let mtb1 = mk_mtb mp sign mb.mod_delta + |Some (sign,delta) -> + let mtb1 = mk_mtb mp sign delta and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in let env = Modops.add_module_type mp mtb1 env in - let cu = check_subtypes env mtb1 mtb2 in + let cu = Subtyping.check_subtypes env mtb1 mtb2 in if not (Environ.check_constraints cu env) then CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); @@ -103,15 +102,17 @@ and check_structure_field env mp lab res = function and check_mexpr env mse mp_mse res = match mse with | MEident mp -> let mb = lookup_module mp env in - (Modops.strengthen_and_subst_mb mb mp_mse false).mod_type + let mb = Modops.strengthen_and_subst_mb mb mp_mse false in + mb.mod_type, mb.mod_delta | MEapply (f,mp) -> - let sign = check_mexpr env f mp_mse res in + let sign, delta = check_mexpr env f mp_mse res in let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mtb = Modops.module_type_of_module (lookup_module mp env) in - let cu = check_subtypes env mtb farg_b in + let cu = Subtyping.check_subtypes env mtb farg_b in if not (Environ.check_constraints cu env) then CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); - Modops.subst_signature (Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver) fbody_b + let subst = Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver in + Modops.subst_signature subst fbody_b, Mod_subst.subst_codom_delta_resolver subst delta | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation") @@ -119,8 +120,8 @@ and check_mexpression env sign mp_mse res = match sign with | MoreFunctor (arg_id, mtb, body) -> check_module_type env mtb; let env' = Modops.add_module_type (MPbound arg_id) mtb env in - let body = check_mexpression env' body mp_mse res in - MoreFunctor(arg_id,mtb,body) + let body, delta = check_mexpression env' body mp_mse res in + MoreFunctor(arg_id,mtb,body), delta | NoFunctor me -> check_mexpr env me mp_mse res and check_signature env sign mp_mse res = match sign with diff --git a/checker/validate.ml b/checker/validate.ml index c214409a2c..b85944f94f 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -143,10 +143,8 @@ let validate debug v x = let o = Obj.repr x in try val_gen v mt_ec o with ValidObjError(msg,ctx,obj) -> - if debug then begin + (if debug then let ctx = List.rev_map print_frame ctx in - print_endline ("Validation failed: "^msg); print_endline ("Context: "^String.concat"/"ctx); - pr_obj obj - end; - failwith "vo structure validation failed" + pr_obj obj); + failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") diff --git a/checker/values.ml b/checker/values.ml index e21acd8179..0de8a3e03f 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -10,28 +10,15 @@ (** Abstract representations of values in a vo *) -(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! +(** NB: This needs updating when the types in declarations.ml and + their dependencies are changed. *) -To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli -with a copy we maintain here: - -MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli - -*) - -(** We reify here the types of values present in a vo (see cic.mli), +(** We reify here the types of values present in a vo. in order to validate its structure. Maybe this reification could become automatically generated someday ? - - [Any] stands for a value that we won't check, - - [Fail] means a value that shouldn't be there at all, - - [Tuple] provides a name and sub-values in this block - - [Sum] provides a name, a number of constant constructors, - and sub-values at each position of each possible constructed - variant - - [List] and [Opt] could have been defined via [Sum], but - having them here helps defining some recursive values below - - [Annot] is a no-op, just there for improving debug messages *) + See values.mli for the meaning of each constructor. +*) type value = | Any @@ -45,6 +32,7 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref let fix (f : value -> value) : value = diff --git a/checker/values.mli b/checker/values.mli index 1b1437a469..616b69907f 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -10,17 +10,36 @@ type value = | Any + (** A value that we won't check, *) + | Fail of string + (** A value that shouldn't be there at all, *) + | Tuple of string * value array + (** A debug name and sub-values in this block *) + | Sum of string * int * value array array + (** A debug name, a number of constant constructors, and sub-values + at each position of each possible constructed variant *) + | Array of value | List of value | Opt of value | Int | String + (** Builtin Ocaml types. *) + | Annot of string * value + (** Adds a debug note to the inner value *) + | Dyn + (** Coq's Dyn.t *) + | Proxy of value ref + (** Same as the inner value, used to define recursive types *) + +(** NB: List and Opt have their own constructors to make it easy to + define eg [let rec foo = List foo]. *) val v_univopaques : value val v_libsum : value diff --git a/config/coq_config.mli b/config/coq_config.mli index 22d8c49fd1..33acceb1f0 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -25,11 +25,6 @@ val docdirsuffix : string (* doc directory relative to installation prefix *) val ocamlfind : string -val camlp5o : string (* name of the camlp5o executable *) -val camlp5bin : string (* base directory for camlp5 binaries *) -val camlp5lib : string (* where is the library of camlp5 *) -val camlp5compat : string (* compatibility argument to camlp5 *) - val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *) val arch : string (* architecture *) diff --git a/configure.ml b/configure.ml index 47f7633ae8..ec765acc15 100644 --- a/configure.ml +++ b/configure.ml @@ -4,6 +4,7 @@ (**********************************) + (** This file should be run via: ocaml configure.ml <opts> You could also use our wrapper ./configure <opts> *) @@ -188,34 +189,6 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false -(** Choose a command among a list of candidates - (command name, mandatory arguments, arguments for this test). - Chooses the first one whose execution outputs a non-empty (first) line. - Dies with message [msg] if none is found. *) - -let select_command msg candidates = - let rec search = function - | [] -> die msg - | (p, x, y) :: tl -> - if fst (tryrun p (x @ y)) <> "" - then List.fold_left (Printf.sprintf "%s %s") p x - else search tl - in search candidates - -(** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it - a quoted path to camlp5o via -pp. So we only quote camlp5o on not - Windows, and warn on Windows if the path contains spaces *) -let contains_suspicious_characters str = - List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t'] - -let win_aware_quote_executable str = - if not (os_type_win32 || os_type_cygwin) then - sprintf "%S" str - else - let _ = if contains_suspicious_characters str then - warn "The string %S contains suspicious characters; ocamlfind might fail" str in - Str.global_replace (Str.regexp "\\\\") "/" str - (** * Date *) (** The short one is displayed when starting coqtop, @@ -254,7 +227,6 @@ type preferences = { coqdocdir : string option; ocamlfindcmd : string option; lablgtkdir : string option; - camlp5dir : string option; arch : string option; natdynlink : bool; coqide : ide option; @@ -292,7 +264,6 @@ let default = { coqdocdir = None; ocamlfindcmd = None; lablgtkdir = None; - camlp5dir = None; arch = None; natdynlink = true; coqide = None; @@ -399,8 +370,6 @@ let args_options = Arg.align [ "<dir> Specifies the ocamlfind command to use"; "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }), "<dir> Specifies the path to the Lablgtk library"; - "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }), - "<dir> Specifies where is the Camlp5 library and tells to use it"; "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }), "<flags> Specifies additional flags to be passed to the flambda optimizing compiler"; "-arch", arg_string_option (fun p arch -> { p with arch }), @@ -580,8 +549,6 @@ let camlbin, caml_version, camllib, findlib_version = then reset_caml_top camlexec (camlbin / "ocaml") in camlbin, caml_version, camllib, findlib_version -let camlp5compat = "-loc loc" - (** Caml version as a list of string, e.g. ["4";"00";"1"] *) let caml_version_list = numeric_prefix_list caml_version @@ -660,76 +627,12 @@ let caml_flags = let coq_caml_flags = coq_warn_error -(** * Camlp5 configuration *) - -(* Convention: we use camldir as a prioritary location for camlp5, if given *) -(* i.e., in the case of camlp5, we search for a copy of camlp5o which *) -(* answers the right camlp5 lib dir *) - -let strip_slash dir = - let n = String.length dir in - if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir - -let which_camlp5o_for camlp5lib = - let camlp5o = Filename.concat camlbin "camlp5o" in - let camlp5lib = strip_slash camlp5lib in - if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else - let camlp5o = which "camlp5o" in - if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else - die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) - -let which_camlp5 base = - let file = Filename.concat camlbin base in - if is_executable file then file else which base - -(* TODO: camlp5dir should rather be the *binary* location, just as camldir *) -(* TODO: remove the late attempts at finding gramlib.cma *) - -let check_camlp5 testcma = match !prefs.camlp5dir with - | Some dir -> - if Sys.file_exists (dir/testcma) then - let camlp5o = - try which_camlp5o_for dir - with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in - dir, camlp5o - else - let msg = - sprintf "Cannot find camlp5 libraries in '%s' (%s not found)." - dir testcma - in die msg - | None -> - try - let camlp5o = which_camlp5 "camlp5o" in - let dir,_ = tryrun camlp5o ["-where"] in - dir, camlp5o - with Not_found -> - die "No Camlp5 installation found." - -let check_camlp5_version camlp5o = - let version_line, _ = run ~err:StdOut camlp5o ["-v"] in - let version = List.nth (string_split ' ' version_line) 2 in - match numeric_prefix_list version with - | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> - cprintf "You have Camlp5 %s. Good!" version; version - | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" - -let config_camlp5 () = - let camlp5mod = "gramlib" in - let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in - let camlp5_version = check_camlp5_version camlp5o in - camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version - -let camlp5o, camlp5bindir, fullcamlp5libdir, - camlp5mod, camlp5_version = config_camlp5 () - let shorten_camllib s = if starts_with s (camllib^"/") then let l = String.length camllib + 1 in "+" ^ String.sub s l (String.length s - l) else s -let camlp5libdir = shorten_camllib fullcamlp5libdir - (** * Native compiler *) let msg_byteonly = @@ -738,9 +641,6 @@ let msg_byteonly = let msg_no_ocamlopt () = warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly -let msg_no_camlp5_cmxa () = - warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly - let msg_no_dynlink_cmxa () = warn "Cannot find native-code dynlink library.\n%s" msg_byteonly; cprintf "For building a native-code Coq, you may try to first"; @@ -751,8 +651,6 @@ let check_native () = let () = if !prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found - else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) - then let () = msg_no_camlp5_cmxa () in raise Not_found else if fst (tryrun camlexec.find ["query";"dynlink"]) = "" then let () = msg_no_dynlink_cmxa () in raise Not_found else @@ -771,7 +669,6 @@ let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt" let natdynlinkflag = if hasnatdynlink then "true" else "false" - (** * OS dependent libraries *) let operating_system = @@ -1111,9 +1008,6 @@ let print_summary () = pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); pr " OCaml flambda flags : %s\n" (String.concat " " !prefs.flambda_flags); - pr " Camlp5 version : %s\n" camlp5_version; - pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); - pr " Camlp5 library in : %s\n" (esc camlp5libdir); if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then @@ -1153,7 +1047,6 @@ let write_dbg_wrapper f = pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n"; pr "export COQTOP=%S\n" coqtop; pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug"); - pr "CAMLP5LIB=%S\n\n" camlp5libdir; pr ". $COQTOP/dev/ocamldebug-coq.run\n"; close_out o; Unix.chmod f 0o555 @@ -1185,10 +1078,6 @@ let write_configml f = pr_p "datadirsuffix" datadirsuffix; pr_p "docdirsuffix" docdirsuffix; pr_s "ocamlfind" camlexec.find; - pr_s "camlp5o" camlp5o; - pr_s "camlp5bin" camlp5bindir; - pr_s "camlp5lib" camlp5libdir; - pr_s "camlp5compat" camlp5compat; pr_s "caml_flags" caml_flags; pr_s "version" coq_version; pr_s "caml_version" caml_version; @@ -1212,7 +1101,7 @@ let write_configml f = pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; - "engine"; "pretyping"; "interp"; "parsing"; "proofs"; + "engine"; "pretyping"; "interp"; "gramlib__pack"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" @@ -1295,11 +1184,6 @@ let write_makefile f = pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag; pr "# Compilation profile flag\n"; pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag; - pr "# Camlp5 : flavor, binaries, libraries ...\n"; - pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n"; - pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o); - pr "CAMLP5COMPAT=%s\n" camlp5compat; - pr "MYCAMLP5LIB=%S\n\n" camlp5libdir; pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; @@ -22,7 +22,6 @@ depends: [ "ocaml" { >= "4.05.0" } "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.03" } ] build-env: [ diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 8da4c6db13..d52bd39d72 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -139,7 +139,7 @@ let print_local fmt ext = match locals with | [] -> () | e :: locals -> - let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in + let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in let () = List.iter iter locals in @@ -277,16 +277,16 @@ let print_rule fmt r = let pr_prd fmt prd = print_list fmt print_prod prd in fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) -let print_entry fmt gram e = +let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ " - gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ " + e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = let () = fprintf fmt "let _ = @[" in let () = fprintf fmt "@[<v>%a@]" print_local ext in - let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in + let () = List.iter (fun e -> print_entry fmt e) ext.gramext_entries in let () = fprintf fmt "()@]@\n" in () diff --git a/default.nix b/default.nix index 7c8113c9ab..eeab388cb4 100644 --- a/default.nix +++ b/default.nix @@ -48,7 +48,7 @@ stdenv.mkDerivation rec { python2 time # coq-makefile timing tools dune ] - ++ (with ocamlPackages; [ ocaml findlib camlp5 num ]) + ++ (with ocamlPackages; [ ocaml findlib num ]) ++ optional buildIde ocamlPackages.lablgtk ++ optionals buildDoc [ # Sphinx doc dependencies @@ -67,6 +67,7 @@ stdenv.mkDerivation rec { ++ optionals shell ( [ jq curl gitFull gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools + ++ [ graphviz ] # Useful for STM debugging ); src = diff --git a/dev/base_include b/dev/base_include index 0e12b57b36..48feeec147 100644 --- a/dev/base_include +++ b/dev/base_include @@ -8,6 +8,7 @@ #directory "toplevel";; #directory "library";; #directory "kernel";; +#directory "gramlib";; #directory "engine";; #directory "pretyping";; #directory "lib";; @@ -18,8 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp5";; (* Gramext is found in top_printers.ml *) - #use "top_printers.ml";; #use "vm_printers.ml";; @@ -135,7 +134,6 @@ open Pfedit open Proof open Proof_using open Proof_global -open Proof_type open Redexpr open Refiner open Tacmach diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 0dcabc0b97..d0b5f4be47 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1076,7 +1076,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_camlp5 + # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1386,7 +1386,7 @@ function make_coq { make_ocaml make_num make_findlib - make_camlp5 + # make_camlp5 make_lablgtk if case $COQ_VERSION in diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md new file mode 100644 index 0000000000..6ca3aa2981 --- /dev/null +++ b/dev/ci/README-developers.md @@ -0,0 +1,165 @@ +Information for developers about the CI system +---------------------------------------------- + +When you submit a pull request (PR) on the Coq GitHub repository, this will +automatically launch a battery of CI tests. The PR will not be integrated +unless these tests pass. + +We are currently running tests on the following platforms: + +- GitLab CI is the main CI platform. It tests the compilation of Coq, + of the documentation, and of CoqIDE on Linux with several versions + of OCaml and with warnings as errors; it runs the test-suite and + tests the compilation of several external developments. + +- Travis CI is used to test the compilation of Coq and run the test-suite on + macOS. It also runs a linter that checks whitespace discipline. A + [pre-commit hook](../tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline without pain. + +- AppVeyor is used to test the compilation of Coq and run the test-suite on + Windows. + +You can anticipate the results of most of these tests prior to submitting your +PR by running GitLab CI on your private branches. To do so follow these steps: + +1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). +2. Click on "New Project". +3. Choose "CI / CD for external repository" then click on "GitHub". +4. Find your fork of the Coq repository and click on "Connect". +5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). +6. You are encouraged to go to the CI / CD general settings and increase the + timeout from 1h to 2h for better reliability. + +Now everytime you push (including force-push unless you changed the default +GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and +CI will be run. You will receive an e-mail with a report of the failures if +there are some. + +You can also run one CI target locally (using `make ci-somedev`). + +See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite. + +### Breaking changes + +When your PR breaks an external project we test in our CI, you must +prepare a patch (or ask someone to prepare a patch) to fix the +project. There is experimental support for an improved workflow, see +[the next section](#experimental-automatic-overlay-creation-and-building), below +are the steps to manually prepare a patch: + +1. Fork the external project, create a new branch, push a commit adapting + the project to your changes. +2. Test your pull request with your adapted version of the external project by + adding an overlay file to your pull request (cf. + [`dev/ci/user-overlays/README.md`](user-overlays/README.md)). +3. Fixes to external libraries (pure Coq projects) *must* be backward + compatible (i.e. they should also work with the development version of Coq, + and the latest stable version). This will allow you to open a PR on the + external project repository to have your changes merged *before* your PR on + Coq can be integrated. + + On the other hand, patches to plugins (projects linking to the Coq ML API) + can very rarely be made backward compatible and plugins we test will + generally have a dedicated branch per Coq version. + You can still open a pull request but the merging will be requested by the + developer who merges the PR on Coq. There are plans to improve this, cf. + [#6724](https://github.com/coq/coq/issues/6724). + +Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. + +### Experimental automatic overlay creation and building + +If you break external projects that are hosted on GitHub, you can use +the `create-overlays.sh` script to automatically perform most of the +above steps. In order to do so, call the script as: +``` +./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac +``` +replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR +number. The script will: + +- checkout the contributions and prepare the branch/remote so you can + just commit the fixes and push, +- add the corresponding overlay file in `dev/ci/user-overlays`. + +For problems related to ML-plugins, if you use `dune build` to build +Coq, it will actually be aware of the broken contributions and perform +a global build. This is very convenient when using `merlin` as you +will get a coherent view of all the broken plugins, with full +incremental cross-project rebuild. + +Advanced GitLab CI information +------------------------------ + +GitLab CI is set up to use the "build artifact" feature to avoid +rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` +and `make install` is run, then the `_install_ci` directory +persists to and is used by the next jobs. + +### Artifacts + +Build artifacts from GitLab can be linked / downloaded in a systematic +way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts) +for more information. For example, to access the documentation of the +`master` branch, you can do: + +https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + +Browsing artifacts is also possible: +https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +Above, you can replace `master` and `job` by the desired GitLab branch and job name. + +Currently available artifacts are: + +- the Coq executables and stdlib, in four copies varying in + architecture and OCaml version used to build Coq: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + + Additionally, an experimental Dune build is provided: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: + + + Coq's Reference Manual [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + + Coq's Standard Library Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc + +### GitLab and Windows + +If your repository has access to runners tagged `windows`, setting the +secret variable `WINDOWS` to `enabled` will add jobs building Windows +versions of Coq (32bit and 64bit). + +If the secret variable `WINDOWS` is set to `enabled_all_addons`, +an extended set of addons will be added to the Windows installer. +This leads to a considerable runtime in CI so this is not enabled +by default for pipelines for pull requests. + +The Windows jobs are enabled on Coq's repository, where pipelines for +pull requests run. + +### GitLab and Docker + +System and opam packages are installed in a Docker image. The image is +automatically built and uploaded to your GitLab registry, and is +loaded by subsequent jobs. + +**IMPORTANT**: When updating Coq's CI docker image, you must modify +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) +and [`Dockerfile`](docker/bionic_coq/Dockerfile) + +The Docker building job reuses the uploaded image if it is available, +but if you wish to save more time you can skip the job by setting +`SKIP_DOCKER` to `true`. + +This means you will need to change its value when the Docker image +needs to be updated. You can do so for a single pipeline by starting +it through the web interface. + +See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md new file mode 100644 index 0000000000..01769aeddb --- /dev/null +++ b/dev/ci/README-users.md @@ -0,0 +1,85 @@ +Information for external library / Coq plugin authors +----------------------------------------------------- + +You are encouraged to consider submitting your development for addition to +Coq's CI. This means that: + +- Any time that a proposed change is breaking your development, Coq developers + will send you patches to adapt it or, at the very least, will work with you + to see how to adapt it. + +On the condition that: + +- At the time of the submission, your development works with Coq's + `master` branch. + +- Your development is publicly available in a git repository and we can easily + send patches to you (e.g. through pull / merge requests). + +- You react in a timely manner to discuss / integrate those patches. + +- You do not push, to the branches that we test, commits that haven't been + first tested to compile with the corresponding branch(es) of Coq. + + For that, we recommend setting a CI system for you development, see + [supported CI images for Coq](#supported-ci-images-for-coq) below. + +- You maintain a reasonable build time for your development, or you provide + a "lite" target that we can use. + +In case you forget to comply with these last three conditions, we would reach +out to you and give you a 30-day grace period during which your development +would be moved into our "allow failure" category. At the end of the grace +period, in the absence of progress, the development would be removed from our +CI. + +### Timely merging of overlays + +A pitfall of the current CI setup is that when a breaking change is +merged in Coq upstream, CI for your contrib will be broken until you +merge the corresponding pull request with the fix for your contribution. + +As of today, you have to worry about synchronizing with Coq upstream +every once in a while; we hope we will improve this in the future by +using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is +to give merge permissions to someone from the Coq team as to help with +these kind of merges. + +### Add your development by submitting a pull request + +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **Do not hesitate to submit an incomplete pull request if you need +help to finish it.** + +You may also be interested in having your development tested in our +performance benchmark. Currently this is done by providing an OPAM package +in https://github.com/coq/opam-coq-archive and opening an issue at +https://github.com/coq/coq-bench/issues. + +### Recommended branching policy. + +It is sometimes the case that you will need to maintain a branch of +your development for particular Coq versions. This is in fact very +likely if your development includes a Coq ML plugin. + +We thus recommend a branching convention that mirrors Coq's branching +policy. Then, you would have a `master` branch that follows Coq's +`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so +on. + +This convention will be supported by tools in the future to make some +developer commands work more seamlessly. + +### Supported CI images for Coq + +The Coq developers and contributors provide official Docker and Nix +images for testing against Coq master. Using these images is highly +recommended: + +- For Docker, see: https://github.com/coq-community/docker-coq +- For Nix, see the setup at + https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix diff --git a/dev/ci/README.md b/dev/ci/README.md index 7ed90f524c..afbfab3ac6 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -6,213 +6,15 @@ breakage on our Continuous Integration (CI) platforms *before* integration, so as to ensure better robustness and catch problems as early as possible. These tests include the compilation of several external libraries / plugins. -This document contains information for both external library / plugin authors, -who might be interested in having their development tested, and for Coq -developers / contributors, who must ensure that they don't break these -external developments accidentally. +This README is split into two specific documents: -*Remark:* the CI policy outlined in this document is susceptible to evolve and -specific accommodations are of course possible. +- [README-users.md](./README-users.md) which contains information for + authors of external libraries and plugins who might be interested in + having their development tested in our CI system. -Information for external library / plugin authors -------------------------------------------------- +- [README-developers.md](./README-developers.md) for Coq developers / + contributors, who must ensure that they don't break these external + developments accidentally. -You are encouraged to consider submitting your development for addition to -our CI. This means that: - -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. - -On the condition that: - -- At the time of the submission, your development works with Coq's - `master` branch. - -- Your development is publicly available in a git repository and we can easily - send patches to you (e.g. through pull / merge requests). - -- You react in a timely manner to discuss / integrate those patches. - -- You do not push, to the branches that we test, commits that haven't been - first tested to compile with the corresponding branch(es) of Coq. - -- You maintain a reasonable build time for your development, or you provide - a "lite" target that we can use. - -In case you forget to comply with these last three conditions, we would reach -out to you and give you a 30-day grace period during which your development -would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our -CI. - -### Add your development by submitting a pull request - -Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding -variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the -corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to -[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. -Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an -example. **Do not hesitate to submit an incomplete pull request if you need -help to finish it.** - -You may also be interested in having your development tested in our -performance benchmark. Currently this is done by providing an OPAM package -in https://github.com/coq/opam-coq-archive and opening an issue at -https://github.com/coq/coq-bench/issues. - -### Recommended branching policy. - -It is sometimes the case that you will need to maintain a branch of -your development for particular Coq versions. This is in fact very -likely if your development includes a Coq ML plugin. - -We thus recommend a branching convention that mirrors Coq's branching -policy. Then, you would have a `master` branch that follows Coq's -`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so -on. - -This convention will be supported by tools in the future to make some -developer commands work more seamlessly. - -Information for developers --------------------------- - -When you submit a pull request (PR) on Coq GitHub repository, this will -automatically launch a battery of CI tests. The PR will not be integrated -unless these tests pass. - -We are currently running tests on the following platforms: - -- GitLab CI is the main CI platform. It tests the compilation of Coq, of the - documentation, and of CoqIDE on Linux with several versions of OCaml / - camlp5, and with warnings as errors; it runs the test-suite and tests the - compilation of several external developments. - -- Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. It also runs a linter that checks whitespace discipline. A - [pre-commit hook](../tools/pre-commit) is automatically installed by - `./configure`. It should allow complying with this discipline without pain. - -- AppVeyor is used to test the compilation of Coq and run the test-suite on - Windows. - -You can anticipate the results of most of these tests prior to submitting your -PR by running GitLab CI on your private branches. To do so follow these steps: - -1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). -2. Click on "New Project". -3. Choose "CI / CD for external repository" then click on "GitHub". -4. Find your fork of the Coq repository and click on "Connect". -5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). -6. You are encouraged to go to the CI / CD general settings and increase the - timeout from 1h to 2h for better reliability. - -Now everytime you push (including force-push unless you changed the default -GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and -CI will be run. You will receive an e-mail with a report of the failures if -there are some. - -You can also run one CI target locally (using `make ci-somedev`). - -See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite. - -### Breaking changes - -When your PR breaks an external project we test in our CI, you must prepare a -patch (or ask someone to prepare a patch) to fix the project: - -1. Fork the external project, create a new branch, push a commit adapting - the project to your changes. -2. Test your pull request with your adapted version of the external project by - adding an overlay file to your pull request (cf. - [`dev/ci/user-overlays/README.md`](user-overlays/README.md)). -3. Fixes to external libraries (pure Coq projects) *must* be backward - compatible (i.e. they should also work with the development version of Coq, - and the latest stable version). This will allow you to open a PR on the - external project repository to have your changes merged *before* your PR on - Coq can be integrated. - - On the other hand, patches to plugins (projects linking to the Coq ML API) - can very rarely be made backward compatible and plugins we test will - generally have a dedicated branch per Coq version. - You can still open a pull request but the merging will be requested by the - developer who merges the PR on Coq. There are plans to improve this, cf. - [#6724](https://github.com/coq/coq/issues/6724). - -Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. - -Advanced GitLab CI information ------------------------------- - -GitLab CI is set up to use the "build artifact" feature to avoid -rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` -and `make install` is run, then the `_install_ci` directory -persists to and is used by the next jobs. - -### Artifacts - -Build artifacts from GitLab can be linked / downloaded in a systematic -way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts) -for more information. For example, to access the documentation of the -`master` branch, you can do: - -https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman - -Browsing artifacts is also possible: -https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base - -Above, you can replace `master` and `job` by the desired GitLab branch and job name. - -Currently available artifacts are: - -- the Coq executables and stdlib, in four copies varying in - architecture and OCaml version used to build Coq: - https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base - - Additionally, an experimental Dune build is provided: - https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev - -- the Coq documentation, built in the `doc:*` jobs. When submitting - a documentation PR, this can help reviewers checking the rendered result: - - + Coq's Reference Manual [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman - + Coq's Standard Library Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base - + Coq's ML API Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc - -### GitLab and Windows - -If your repository has access to runners tagged `windows`, setting the -secret variable `WINDOWS` to `enabled` will add jobs building Windows -versions of Coq (32bit and 64bit). - -If the secret variable `WINDOWS` is set to `enabled_all_addons`, -an extended set of addons will be added to the Windows installer. -This leads to a considerable runtime in CI so this is not enabled -by default for pipelines for pull requests. - -The Windows jobs are enabled on Coq's repository, where pipelines for -pull requests run. - -### GitLab and Docker - -System and opam packages are installed in a Docker image. The image is -automatically built and uploaded to your GitLab registry, and is -loaded by subsequent jobs. - -**IMPORTANT**: When updating Coq's CI docker image, you must modify -the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) -and [`Dockerfile`](docker/bionic_coq/Dockerfile) - -The Docker building job reuses the uploaded image if it is available, -but if you wish to save more time you can skip the job by setting -`SKIP_DOCKER` to `true`. - -This means you will need to change its value when the Docker image -needs to be updated. You can do so for a single pipeline by starting -it through the web interface. - -See also [`docker/README.md`](docker/README.md). +*Remark:* the CI policy outlined in these documents is susceptible to +evolve and specific accommodations are of course possible. diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 84fec71f7a..abeb039c0e 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -10,6 +10,6 @@ bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y num ocamlfind camlp5 ounit +opam install -y num ocamlfind ounit cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4d5834eeb6..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,13 +215,6 @@ : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## -# pidetop -######################################################################## -: "${pidetop_CI_REF:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" -: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" - -######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh deleted file mode 100755 index 1a9a26843c..0000000000 --- a/dev/ci/ci-pidetop.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download pidetop - -# Travis / Gitlab have different filesystem layout due to use of -# `-local`. We need to improve this divergence but if we use Dune this -# "local" oddity goes away automatically so not bothering... -if [ -d "$COQBIN/../lib/coq" ]; then - COQLIB="$COQBIN/../lib/coq/" -else - COQLIB="$COQBIN/../" -fi - -( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) - -echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4ddb582414..3fc6dce4e5 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-30-V1" +# CACHEKEY: "bionic_coq-V2018-11-08-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,29 +41,27 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.03" \ - COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" +ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" # base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER + opam install $BASE_OPAM # EDGE switch ENV COMPILER_EDGE="4.07.1" \ - CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM RUN opam clean -a -c diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh new file mode 100644 index 0000000000..e74e53fa40 --- /dev/null +++ b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then + plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg + plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials +fi diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh new file mode 100644 index 0000000000..d7130cc67a --- /dev/null +++ b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then + + elpi_CI_REF=use_coq_gramlib + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh new file mode 100644 index 0000000000..c8bea0c868 --- /dev/null +++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then + + equations_CI_REF=legacy_proof_eng_clean + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh new file mode 100644 index 0000000000..14e7c0d7f0 --- /dev/null +++ b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then + + equations_CI_REF=camlp5-safe-api-strikes-back + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + ltac2_CI_REF=camlp5-safe-api-strikes-back + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/doc/README.md b/dev/doc/README.md index 223cf6286e..c764455aed 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -16,7 +16,6 @@ $ opam init --comp <latest-ocaml-version> ~/.bashrc and ~/.ocamlinit files. $ source ~/.bashrc -$ opam install camlp5 # needed if you want to build "coqide" target diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 30a2967259..acb0d80c18 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,15 @@ ## Changes between Coq 8.9 and Coq 8.10 +### ML4 Pre Processing + +- Support for `.ml4` files, processed by camlp5 has been removed in + favor of `.mlg` files processed by `coqpp`. + + Porting is usually straightforward, and involves renaming the + `file.ml4` file to `file.mlg` and adding a few brackets. + + See "Transitioning away from Camlp5" below for update instructions. + ### ML API General deprecation diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 764d482957..e5e4f740bd 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V -Proof_type.tactic +Proofview.V82.tac TODO: check with Hugo @@ -10,7 +10,7 @@ (rule (targets dune-dbg) (deps dune-dbg.in - ../checker/main.bc + ../checker/coqchk.bc ../topbin/coqtop_byte_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 3f3df23fe1..80ad0500e0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,7 +3,7 @@ # Run in a proper install dune env. case $1 in checker) - exe=_build/default/checker/main.bc + exe=_build/default/checker/coqchk.bc ;; *) exe=_build/default/topbin/coqtop_byte_bin.bc diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index d330f517be..707c7f07ce 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -8,14 +8,13 @@ # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ + -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index 314ac07e68..41392be5d7 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -75,4 +75,4 @@ done # End the file; copy to overlays folder. echo "fi" >> $OVERLAY_FILE PR_NUMBER=$(printf '%05d' "$PR_NUMBER") -mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-$OVERLAY_BRANCH.sh +mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-${OVERLAY_BRANCH///}.sh diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 320ef6ed07..5fd8a3b7d9 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -202,9 +202,8 @@ info "merging" git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e # TODO: improve this check -if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then - warning "this PR may have overlays (sorry the check is not perfect)" - warning "if it has overlays please check the following:" +if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then + warning "this PR has overlays, please check the following:" warning "- each overlay has a corresponding open PR on the upstream repo" warning "- after merging please notify the upstream they can merge the PR" fi diff --git a/dev/top_printers.mli b/dev/top_printers.mli index eaa12ff702..5eac3e2b9c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit val ppgoalgoal : Goal.goal -> unit -val ppgoal : Proof_type.goal Evd.sigma -> unit +val ppgoal : Goal.goal Evd.sigma -> unit (* also print evar map *) -val ppgoalsigma : Proof_type.goal Evd.sigma -> unit +val ppgoalsigma : Goal.goal Evd.sigma -> unit val pphintdb : Hints.Hint_db.t -> unit val ppproofview : Proofview.proofview -> unit diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c0a57763b9..5d219ebd0d 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,7 +35,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. The tactics solve propositional formulas parameterized by atomic -arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. +arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. The syntax of the formulas is the following: .. productionlist:: `F` @@ -46,8 +46,8 @@ The syntax of the formulas is the following: where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the operators :math:`−, +, ×` are respectively subtraction, addition, and product; :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. -For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of -rationals ==. +For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of +rationals ``==``. For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the @@ -58,7 +58,7 @@ following expressions: c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`. -This includes integer constants written using the decimal notation, *i.e.*, c%R. +This includes integer constants written using the decimal notation, *i.e.*, ``c%R``. *Positivstellensatz* refutations @@ -94,7 +94,7 @@ general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and For each conjunct :math:`C_i`, the tactic calls an oracle which searches for :math:`-1` within the cone. Upon success, the oracle returns a *cone -expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) +expression* that is normalized by the :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. `lra`: a decision procedure for linear real and rational arithmetic @@ -245,11 +245,11 @@ proof by abstracting monomials by variables. As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` (polynomial hypotheses are printed in bold). By construction, this expression -belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we +belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with - the `zify` tactic. + the ``zify`` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/engine/eConstr.ml b/engine/eConstr.ml index cfc4bea85f..96f1ce5e60 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -296,6 +296,8 @@ let decompose_prod_n_assum sigma n c = let existential_type = Evd.existential_type +let lift n c = of_constr (Vars.lift n (unsafe_to_constr c)) + let map_under_context f n c = let f c = unsafe_to_constr (f (of_constr c)) in of_constr (Constr.map_under_context f n (unsafe_to_constr c)) @@ -306,137 +308,21 @@ let map_return_predicate f ci p = let f c = unsafe_to_constr (f (of_constr c)) in of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p)) -let map_gen userview sigma f c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (b,k,t) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkCast (b', k, t') - | Prod (na,t,b) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkProd (na, t', b') - | Lambda (na,t,b) -> - let b' = f b in - let t' = f t in - if b'==b && t' == t then c - else mkLambda (na, t', b') - | LetIn (na,b,t,k) -> - let b' = f b in - let t' = f t in - let k' = f k in - if b'==b && t' == t && k'==k then c - else mkLetIn (na, b', t', k') - | App (b,l) -> - let b' = f b in - let l' = Array.Smart.map f l in - if b'==b && l'==l then c - else mkApp (b', l') - | Proj (p,t) -> - let t' = f t in - if t' == t then c - else mkProj (p, t') - | Evar (e,l) -> - let l' = Array.Smart.map f l in - if l'==l then c - else mkEvar (e, l') - | Case (ci,p,b,bl) when userview -> - let b' = f b in - let p' = map_return_predicate f ci p in - let bl' = map_branches f ci bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') - | Case (ci,p,b,bl) -> - let b' = f b in - let p' = f p in - let bl' = Array.Smart.map f bl in - if b'==b && p'==p && bl'==bl then c - else mkCase (ci, p', b', bl') - | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map f tl in - let bl' = Array.Smart.map f bl in - if tl'==tl && bl'==bl then c - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map f tl in - let bl' = Array.Smart.map f bl in - if tl'==tl && bl'==bl then c - else mkCoFix (ln,(lna,tl',bl')) - -let map_user_view = map_gen true -let map = map_gen false - -let map_with_binders sigma g f l c0 = match kind sigma c0 with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c0 - | Cast (c, k, t) -> - let c' = f l c in - let t' = f l t in - if c' == c && t' == t then c0 - else mkCast (c', k, t') - | Prod (na, t, c) -> - let t' = f l t in - let c' = f (g l) c in - if t' == t && c' == c then c0 - else mkProd (na, t', c') - | Lambda (na, t, c) -> - let t' = f l t in - let c' = f (g l) c in - if t' == t && c' == c then c0 - else mkLambda (na, t', c') - | LetIn (na, b, t, c) -> - let b' = f l b in - let t' = f l t in - let c' = f (g l) c in - if b' == b && t' == t && c' == c then c0 - else mkLetIn (na, b', t', c') - | App (c, al) -> - let c' = f l c in - let al' = Array.Fun1.Smart.map f l al in - if c' == c && al' == al then c0 - else mkApp (c', al') - | Proj (p, t) -> - let t' = f l t in - if t' == t then c0 - else mkProj (p, t') - | Evar (e, al) -> - let al' = Array.Fun1.Smart.map f l al in - if al' == al then c0 - else mkEvar (e, al') - | Case (ci, p, c, bl) -> - let p' = f l p in - let c' = f l c in - let bl' = Array.Fun1.Smart.map f l bl in - if p' == p && c' == c && bl' == bl then c0 - else mkCase (ci, p', c', bl') - | Fix (ln, (lna, tl, bl)) -> - let tl' = Array.Fun1.Smart.map f l tl in - let l' = iterate g (Array.length tl) l in - let bl' = Array.Fun1.Smart.map f l' bl in - if tl' == tl && bl' == bl then c0 - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.Fun1.Smart.map f l tl in - let l' = iterate g (Array.length tl) l in - let bl' = Array.Fun1.Smart.map f l' bl in - mkCoFix (ln,(lna,tl',bl')) - -let iter sigma f c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_,t) -> f c; f t - | Prod (_,t,c) -> f t; f c - | Lambda (_,t,c) -> f t; f c - | LetIn (_,b,t,c) -> f b; f t; f c - | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c - | Evar (_,l) -> Array.iter f l - | Case (_,p,c,bl) -> f p; f c; Array.iter f bl - | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl - | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl +let map_user_view sigma f c = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c))) + +let map sigma f c = + let f c = unsafe_to_constr (f (of_constr c)) in + of_constr (Constr.map f (unsafe_to_constr (whd_evar sigma c))) + +let map_with_binders sigma g f l c = + let f l c = unsafe_to_constr (f l (of_constr c)) in + of_constr (Constr.map_with_binders g f l (unsafe_to_constr (whd_evar sigma c))) + +let iter sigma f c = + let f c = f (of_constr c) in + Constr.iter f (unsafe_to_constr (whd_evar sigma c)) let iter_with_full_binders sigma g f n c = let open Context.Rel.Declaration in @@ -453,31 +339,20 @@ let iter_with_full_binders sigma g f n c = | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in Array.iter (f n') bl | CoFix (_,(lna,tl,bl)) -> Array.iter (f n) tl; - let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in + let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in Array.iter (f n') bl let iter_with_binders sigma g f n c = - iter_with_full_binders sigma (fun _ acc -> g acc) f n c + let f l c = f l (of_constr c) in + Constr.iter_with_binders g f n (unsafe_to_constr (whd_evar sigma c)) -let fold sigma f acc c = match kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_,t) -> f (f acc c) t - | Prod (_,t,c) -> f (f acc t) c - | Lambda (_,t,c) -> f (f acc t) c - | LetIn (_,b,t,c) -> f (f (f acc b) t) c - | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c - | Evar (_,l) -> Array.fold_left f acc l - | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> - Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl +let fold sigma f acc c = + let f acc c = f acc (of_constr c) in + Constr.fold f acc (unsafe_to_constr (whd_evar sigma c)) let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 @@ -712,7 +587,7 @@ let to_rel_decl = unsafe_to_rel_decl type substl = t list (** Operations that commute with evar-normalization *) -let lift n c = of_constr (Vars.lift n (to_constr c)) +let lift = lift let liftn n m c = of_constr (Vars.liftn n m (to_constr c)) let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c)) diff --git a/engine/termops.ml b/engine/termops.ml index ada6311067..98300764df 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -721,18 +721,16 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let bl' = Array.map (f l) bl in if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else mkCase (ci, p', c', bl') - | Fix (ln,(lna,tl,bl)) -> + | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> + | CoFix(ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in + let l' = fold_rec_types g fx l in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -759,34 +757,17 @@ let fold_constr_with_full_binders sigma g f n acc c = Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = - fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_constr_with_binders g f n acc c (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders sigma g f l c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_, t) -> f l c; f l t - | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c - | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c - | App (c,args) -> f l c; Array.iter (f l) args - | Proj (p,c) -> f l c - | Evar (_,args) -> Array.iter (f l) args - | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl - | Fix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl - | CoFix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl +let iter_constr_with_full_binders = EConstr.iter_with_full_binders (***************************) (* occurs check functions *) diff --git a/engine/termops.mli b/engine/termops.mli index 6c3d4fa612..eef8452e64 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -88,6 +88,7 @@ val iter_constr_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."] (**********************************************************************) diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 72468b540e..43a70ca13b 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -149,8 +149,6 @@ let srules rl = in Stree t -external action : 'a -> g_action = "%identity" - let is_level_labelled n lev = match lev.lname with Some n1 -> n = n1 diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index e888508277..8361e21645 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -59,7 +59,6 @@ val levels_of_rules : list -> 'te g_level list val srules : ('te g_symbol list * g_action) list -> 'te g_symbol -external action : 'a -> g_action = "%identity" val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : diff --git a/gramlib/gramlib.mllib b/gramlib/gramlib.mllib new file mode 100644 index 0000000000..4c915b2b05 --- /dev/null +++ b/gramlib/gramlib.mllib @@ -0,0 +1,4 @@ +Ploc +Plexing +Gramext +Grammar diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 1ce0136c1d..dfce26a33a 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -5,6 +5,8 @@ open Gramext open Format +external gramext_action : 'a -> g_action = "%identity" + let rec flatten_tree = function DeadEnd -> [] @@ -350,7 +352,7 @@ let top_tree entry = | LocAct (_, _) | DeadEnd -> raise Stream.Failure let skip_if_empty bp p strm = - if Stream.count strm == bp then Gramext.action (fun a -> p strm) + if Stream.count strm == bp then gramext_action (fun a -> p strm) else raise Stream.Failure let continue entry bp a s son p1 (strm__ : _ Stream.t) = @@ -359,7 +361,7 @@ let continue entry bp a s son p1 (strm__ : _ Stream.t) = try p1 strm__ with Stream.Failure -> raise (Stream.Error (tree_failed entry a s son)) in - Gramext.action (fun _ -> app act a) + gramext_action (fun _ -> app act a) let do_recover parser_of_tree entry nlevn alevn bp a s son (strm__ : _ Stream.t) = @@ -861,7 +863,6 @@ module type S = val of_parser : string -> (te Stream.t -> 'a) -> 'a e val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit - external obj : 'a e -> te Gramext.g_entry = "%identity" end type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule @@ -891,18 +892,11 @@ module type S = val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val extend : - 'a Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * - (te Gramext.g_symbol list * Gramext.g_action) list) - list -> - unit val safe_extend : 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> unit - val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 1c5fcb7bbf..1e14e557bc 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -35,7 +35,6 @@ module type S = val of_parser : string -> (te Stream.t -> 'a) -> 'a e val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit - external obj : 'a e -> te Gramext.g_entry = "%identity" end type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule @@ -66,18 +65,11 @@ module type S = val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val extend : - 'a Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * - (te Gramext.g_symbol list * Gramext.g_action) list) - list -> - unit val safe_extend : 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> unit - val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit end (** Signature type of the functor [Grammar.GMake]. The types and diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp deleted file mode 100644 index 715b8cd23f..0000000000 --- a/grammar/argextend.mlp +++ /dev/null @@ -1,221 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Q_util - -let loc = Ploc.dummy - -IFDEF STRICT THEN - let ploc_vala x = Ploc.VaVal x -ELSE - let ploc_vala x = x -END - -let declare_str_items loc l = - MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *) - -let declare_arg loc s e = - declare_str_items loc [ - <:str_item< value ($lid:"wit_"^s$, $lid:s$) = $e$ >>; - (** Prevent the unused variable warning *) - <:str_item< value _ = ($lid:"wit_"^s$, $lid:s$) >>; - ] - -let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> - -let rec make_wit loc = function - | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> mk_extraarg loc s - -let is_self s = function -| ExtraArgType s' -> s = s' -| _ -> false - -let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> -let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> -let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> - -let make_act loc act pil = - let rec make = function - | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >> - | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> - | ExtTerminal _ :: tl -> - <:expr< (fun _ -> $make tl$) >> in - make (List.rev pil) - -let make_prod_item self = function - | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (Uentry e, _) when e = self -> <:expr< Extend.Aself >> - | ExtNonTerminal (g, _) -> - let base s = <:expr< $lid:s$ >> in - mlexpr_of_prod_entry_key base g - -let rec make_prod self = function -| [] -> <:expr< Extend.Stop >> -| item :: prods -> <:expr< Extend.Next $make_prod self prods$ $make_prod_item self item$ >> - -let make_rule loc self (prods,act) = - <:expr< Extend.Rule $make_prod self (List.rev prods)$ $make_act loc act prods$ >> - -let is_ident x = function -| <:expr< $lid:s$ >> -> (s : string) = x -| _ -> false - -let make_extend loc self cl = match cl with -| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> - (** Special handling of identity arguments by not redeclaring an entry *) - <:expr< Vernacextend.Arg_alias $lid:e$ >> -| _ -> - <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> - -let warning_deprecated prefix s = function -| None -> () -| Some _ -> - Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \ - Use [TYPED AS] instead.\n%!" prefix s - -let get_type s = function -| None -> None -| Some typ -> - if is_self s typ then - let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in - None - else Some typ - -let declare_tactic_argument loc s (typ, f, g, h) cl = - let se = mlexpr_of_string s in - let typ, pr = match typ with - | `Uniform (typ, pr) -> - let typ = get_type s typ in - typ, <:expr< ($lid:pr$, $lid:pr$, $lid:pr$) >> - | `Specialized (a, rpr, c, gpr, e, tpr) -> - let () = warning_deprecated "RAW_" s a in - let () = warning_deprecated "GLOB_" s c in - let typ = get_type s e in - typ, <:expr< ($lid:rpr$, $lid:gpr$, $lid:tpr$) >> - in - let glob = match g, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, $lid:f$ ist v)) >> - | None, Some typ -> - <:expr< Tacentries.ArgInternWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, v)) >> - in - let interp = match f, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgInterpLegacy $lid:f$ >> - | None, Some typ -> - <:expr< Tacentries.ArgInterpWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgInterpRet >> - in - let subst = match h, typ with - | Some f, (None | Some _) -> - <:expr< Tacentries.ArgSubstFun $lid:f$ >> - | None, Some typ -> - <:expr< Tacentries.ArgSubstWit $make_wit loc typ$ >> - | None, None -> - <:expr< Tacentries.ArgSubstFun (fun s v -> v) >> - in - let dyn = mlexpr_of_option (fun typ -> <:expr< Geninterp.val_tag $make_topwit loc typ$ >>) typ in - declare_arg loc s <:expr< Tacentries.argument_extend ~{ name = $se$ } { - Tacentries.arg_parsing = $make_extend loc s cl$; - Tacentries.arg_tag = $dyn$; - Tacentries.arg_intern = $glob$; - Tacentries.arg_subst = $subst$; - Tacentries.arg_interp = $interp$; - Tacentries.arg_printer = $pr$ - } >> - -let declare_vernac_argument loc s pr cl = - let se = mlexpr_of_string s in - let pr_rules = match pr with - | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >> - | Some pr -> <:expr< $lid:pr$ >> in - declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } { - Vernacextend.arg_printer = $pr_rules$; - Vernacextend.arg_parsing = $make_extend loc s cl$ - } >> - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "ARGUMENT"; "EXTEND"; s = entry_name; - header = argextend_header; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_tactic_argument loc s header l - | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name; - pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; - OPT "|"; l = LIST1 argrule SEP "|"; - "END" -> - declare_vernac_argument loc s pr l ] ] - ; - argextend_specialized: - [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ]; - "RAW_PRINTED"; "BY"; rawpr = LIDENT; - globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ]; - "GLOB_PRINTED"; "BY"; globpr = LIDENT -> - (rawtyp, rawpr, globtyp, globpr) ] ] - ; - argextend_header: - [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ]; - "PRINTED"; "BY"; pr = LIDENT; - f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; - g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; - h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; - special = OPT argextend_specialized -> - let repr = match special with - | None -> `Uniform (typ, pr) - | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr) - in - (repr, f, g, h) ] ] - ; - argtype: - [ "2" - [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] - | "1" - [ e = argtype; LIDENT "list" -> ListArgType e - | e = argtype; LIDENT "option" -> OptArgType e ] - | "0" - [ e = LIDENT -> - let e = parse_user_entry e "" in - type_of_user_symbol e - | "("; e = argtype; ")" -> e ] ] - ; - argrule: - [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] - ; - genarg: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> ExtTerminal s - ] ] - ; - entry_name: - [ [ s = LIDENT -> s - | UIDENT -> failwith "Argument entry names must be lowercase" - ] ] - ; - END diff --git a/grammar/dune b/grammar/dune deleted file mode 100644 index 78df2826d6..0000000000 --- a/grammar/dune +++ /dev/null @@ -1,41 +0,0 @@ -(library - (name grammar5) - (synopsis "Coq Camlp5 Grammar Extensions for Plugins") - (public_name coq.grammar) - (flags (:standard -w -58)) - (libraries camlp5)) - -; Custom camlp5! This is a net speedup, and a preparation for using -; Dune's preprocessor abilities. -(rule - (targets coqmlp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5))) - -(rule - (targets coqp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5))) - -(install - (section bin) - (package coq) - (files coqp5 coqmlp5)) - -(rule - (targets q_util.ml) - (deps (:mlp-file q_util.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets argextend.ml) - (deps (:mlp-file argextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets tacextend.ml) - (deps (:mlp-file tacextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) - -(rule - (targets vernacextend.ml) - (deps (:mlp-file vernacextend.mlp)) - (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets}))) diff --git a/grammar/q_util.mli b/grammar/q_util.mli deleted file mode 100644 index b163100fc3..0000000000 --- a/grammar/q_util.mli +++ /dev/null @@ -1,54 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type argument_type = -| ListArgType of argument_type -| OptArgType of argument_type -| PairArgType of argument_type * argument_type -| ExtraArgType of string - -type user_symbol = -| Ulist1 of user_symbol -| Ulist1sep of user_symbol * string -| Ulist0 of user_symbol -| Ulist0sep of user_symbol * string -| Uopt of user_symbol -| Uentry of string -| Uentryl of string * int - -type extend_token = -| ExtTerminal of string -| ExtNonTerminal of user_symbol * string option - -val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr - -val mlexpr_of_pair : - ('a -> MLast.expr) -> ('b -> MLast.expr) - -> 'a * 'b -> MLast.expr - -val mlexpr_of_bool : bool -> MLast.expr - -val mlexpr_of_int : int -> MLast.expr - -val mlexpr_of_string : string -> MLast.expr - -val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr - -val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr - -val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr - -val type_of_user_symbol : user_symbol -> argument_type - -val parse_user_entry : string -> string -> user_symbol - -val mlexpr_of_symbol : user_symbol -> MLast.expr - -val binders_of_tokens : MLast.expr -> extend_token list -> MLast.expr diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp deleted file mode 100644 index a2007d258c..0000000000 --- a/grammar/q_util.mlp +++ /dev/null @@ -1,150 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* This file defines standard combinators to build ml expressions *) - -type argument_type = -| ListArgType of argument_type -| OptArgType of argument_type -| PairArgType of argument_type * argument_type -| ExtraArgType of string - -type user_symbol = -| Ulist1 of user_symbol -| Ulist1sep of user_symbol * string -| Ulist0 of user_symbol -| Ulist0sep of user_symbol * string -| Uopt of user_symbol -| Uentry of string -| Uentryl of string * int - -type extend_token = -| ExtTerminal of string -| ExtNonTerminal of user_symbol * string option - -let mlexpr_of_list f l = - List.fold_right - (fun e1 e2 -> - let e1 = f e1 in - let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - l (let loc = Ploc.dummy in <:expr< [] >>) - -let mlexpr_of_pair m1 m2 (a1,a2) = - let e1 = m1 a1 and e2 = m2 a2 in - let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< ($e1$, $e2$) >> - -(* We don't give location for tactic quotation! *) -let loc = Ploc.dummy - - -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - -let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> - -let mlexpr_of_string s = <:expr< $str:s$ >> - -let mlexpr_of_option f = function - | None -> <:expr< None >> - | Some e -> <:expr< Some $f e$ >> - -let mlexpr_of_name f = function - | None -> <:expr< Names.Name.Anonymous >> - | Some e -> <:expr< Names.Name.Name $f e$ >> - -let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> - -let rec mlexpr_of_prod_entry_key f = function - | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Extend.Aentry ($f e$) >> - | Uentryl (e, l) -> - (** Keep in sync with Pcoq! *) - assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> - else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >> - -let rec type_of_user_symbol = function -| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> - ListArgType (type_of_user_symbol s) -| Uopt s -> - OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> ExtraArgType e - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := c = d; - incr i - done; - !break - -let check_separator sep = - if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep." - -let rec parse_user_entry s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) "" in - check_separator sep; - Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) "" in - Ulist1sep (entry, sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) "" in - check_separator sep; - Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) "" in - Ulist0sep (entry, sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) "" in - check_separator sep; - Uopt entry - else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in - check_separator sep; - Uentryl ("tactic", n) - else - let s = match s with "hyp" -> "var" | _ -> s in - check_separator sep; - Uentry s - -let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> -| Uentry e -> - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> -| Uentryl (e, l) -> - assert (e = "tactic"); - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> - -let rec binders_of_tokens e = function -| [] -> e -| ExtNonTerminal(_,None) :: cl -> <:expr< fun _ -> $binders_of_tokens e cl$ >> -| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_tokens e cl$ >> -| ExtTerminal _ :: cl -> binders_of_tokens e cl diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp deleted file mode 100644 index a093f78388..0000000000 --- a/grammar/tacextend.mlp +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** WARNING: this file is deprecated; consider modifying coqpp instead. *) - -(** Implementation of the TACTIC EXTEND macro. *) - -open Q_util -open Argextend - -let plugin_name = <:expr< __coq_plugin_name >> - -let rec mlexpr_of_clause = function -| [] -> <:expr< TyNil >> -| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, _) :: cl -> - <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "TACTIC"; "EXTEND"; s = tac_name; - depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ]; - level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; - OPT "|"; l = LIST1 tacrule SEP "|"; - "END" -> - let level = match level with Some i -> int_of_string i | None -> 0 in - let level = mlexpr_of_int level in - let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in - let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in - declare_str_items loc [ <:str_item< Tacentries.tactic_extend - $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation = - $depr$ } $l$ >> ] ] ] - ; - tacrule: - [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> - let e = <:expr< fun ist -> $e$ >> in - <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >> - ] ] - ; - - tacargs: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - let () = if s = "" then failwith "Empty terminal." in - ExtTerminal s - ] ] - ; - tac_name: - [ [ s = LIDENT -> s - | s = UIDENT -> s - ] ] - ; - END diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp deleted file mode 100644 index d44eeef670..0000000000 --- a/grammar/vernacextend.mlp +++ /dev/null @@ -1,115 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Implementation of the VERNAC EXTEND macro. *) - -open Q_util -open Argextend - -type rule = { - r_patt : extend_token list; - (** The remaining tokens of the parsing rule *) - r_class : MLast.expr option; - (** An optional classifier for the STM *) - r_branch : MLast.expr; - (** The action performed by this rule. *) - r_depr : bool; - (** Whether this entry is deprecated *) -} - -let rec mlexpr_of_clause = function -| [] -> <:expr< Vernacextend.TyNil >> -| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, id) :: cl -> - <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -let make_rule r = - let ty = mlexpr_of_clause r.r_patt in - let cmd = binders_of_tokens r.r_branch r.r_patt in - let make_classifier c = binders_of_tokens c r.r_patt in - let classif = mlexpr_of_option make_classifier r.r_class in - <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> - -let declare_command loc s c nt cl = - let se = mlexpr_of_string s in - let c = mlexpr_of_option (fun x -> x) c in - let rules = mlexpr_of_list make_rule cl in - declare_str_items loc - [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr<None>> l - | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 fun_rule SEP "|"; - "END" -> - declare_command loc s c <:expr<None>> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s c <:expr<Some $lid:nt$>> l - | "DECLARE"; "PLUGIN"; name = STRING -> - declare_str_items loc [ - <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; - ] - ] ] - ; - classification: - [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> - | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> - | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> Vernac_classifier.classify_as_query >> - ] ] - ; - deprecation: - [ [ -> false | "DEPRECATED" -> true ] ] - ; - rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in - { r_patt = l; r_class = c; r_branch = b; r_depr = d; } - ] ] - ; - (** The [OPT "-"] argument serves no purpose nowadays, it is left here for - backward compatibility. *) - fun_rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - { r_patt = l; r_class = c; r_branch = e; r_depr = d; } - ] ] - ; - classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ] - ; - args: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - ExtTerminal s - ] ] - ; - END -;; diff --git a/ide/idetop.ml b/ide/idetop.ml index 8a221a93e9..8cb02190e6 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -212,25 +212,20 @@ let goals () = if Proof_diffs.show_diffs () then begin let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in let diff_goal_map = Proof_diffs.make_goal_map oldp newp in - let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) - try Evar.Map.find ng diff_goal_map with Not_found -> ng - in let process_goal_diffs nsigma ng = let open Evd in - let og = map_goal_for_diff ng in let og_s = match oldp with | Some oldp -> let (_,_,_,_,osigma) = Proof.proof oldp in - Some { it = og; sigma = osigma } + (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } + with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)")) | None -> None in let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } in - try - Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs)) - with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) + Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs)) end else Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) with Proof_global.NoCurrentProof -> None;; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 838ef40545..70ce6cef19 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -716,20 +716,20 @@ let rec flatten_application c = match DAst.get c with (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = - try - let (sc,n) = uninterp_prim_token r in - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> - match availability_of_prim_token n sc scopes with - | None -> None - | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)) - with No_match -> - None - -let extern_optimal_prim_token scopes r r' = - let c = extern_possible_prim_token scopes r in - let c' = if r==r' then None else extern_possible_prim_token scopes r' in + let (sc,n) = uninterp_prim_token r in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> + match availability_of_prim_token n sc scopes with + | None -> raise No_match + | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + +let extern_possible extern r = + try Some (extern r) with No_match -> None + +let extern_optimal extern r r' = + let c = extern_possible extern r in + let c' = if r==r' then None else extern_possible extern r' in match c,c' with | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match @@ -769,12 +769,14 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal_prim_token scopes r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_optimal + (fun r -> extern_notation scopes vars r (uninterp_notations r)) + r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with diff --git a/interp/impargs.ml b/interp/impargs.ml index d8582d856e..d024a9e808 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -19,7 +19,6 @@ open Decl_kinds open Lib open Libobject open EConstr -open Termops open Reductionops open Constrexpr open Namegen @@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc acc.(i) <- update pos rig acc.(i) | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Proj (p,c) when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Evar _ -> () | _ -> - iter_constr_with_full_binders sigma push_lift (frec rig) ed c + iter_with_full_binders sigma push_lift (frec rig) ed c in let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc diff --git a/kernel/constr.ml b/kernel/constr.ml index 704e6de6b8..8e5d15dd2d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -452,27 +452,6 @@ let fold f acc c = match kind c with | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl -let fold_with_full_binders g f n acc c = - let open Context.Rel.Declaration in - match kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (_,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - (* [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) @@ -534,12 +513,12 @@ let fold_constr_with_binders g f n acc c = | Proj (_p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in + | Fix (_,(_,tl,bl)) -> + let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in + | CoFix (_,(_,tl,bl)) -> + let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -799,6 +778,49 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) +(*********************) +(* Lifting *) +(*********************) + +(* The generic lifting function *) +let rec exliftn el c = + let open Esubst in + match kind c with + | Rel i -> mkRel(reloc_rel i el) + | _ -> map_with_binders el_lift exliftn el c + +(* Lifting the binding depth across k bindings *) + +let liftn n k c = + let open Esubst in + match el_liftn (pred k) (el_shft n el_id) with + | ELID -> c + | el -> exliftn el c + +let lift n = liftn n 1 + +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + + type 'univs instance_compare_fn = GlobRef.t -> int -> 'univs -> 'univs -> bool diff --git a/kernel/constr.mli b/kernel/constr.mli index 1be1f63ff7..f2cedcdabb 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -383,6 +383,17 @@ type rel_context = rel_declaration list type named_context = named_declaration list type compacted_context = compacted_declaration list +(** {6 Relocation and substitution } *) + +(** [exliftn el c] lifts [c] with lifting [el] *) +val exliftn : Esubst.lift -> constr -> constr + +(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *) +val liftn : int -> int -> constr -> constr + +(** [lift n c] lifts by [n] the positive indexes in [c] *) +val lift : int -> constr -> constr + (** {6 Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)} *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 2464df799e..83d890b628 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -498,7 +498,7 @@ type generic_name = | M (** name already known, cf the mod_mp field *) | MT (** name already known, cf the mod_mp field *) -let add_field ((l,sfb) as field) gn senv = +let add_field ?(is_include=false) ((l,sfb) as field) gn senv = let mlabs,olabs = match sfb with | SFBmind mib -> let l = labels_of_mib mib in @@ -508,8 +508,18 @@ let add_field ((l,sfb) as field) gn senv = | SFBmodule _ | SFBmodtype _ -> check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty) in - let cst = constraints_of_sfb senv.env sfb in - let senv = add_constraints_list cst senv in + let senv = + if is_include then + (* Universes and constraints were added when the included module + was defined eg in [Include F X.] (one of the trickier + versions of Include) the constraints on the fields are + exactly those of the fields of F which was defined + separately. *) + senv + else + let cst = constraints_of_sfb senv.env sfb in + add_constraints_list cst senv + in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env @@ -1049,7 +1059,7 @@ let add_include me is_module inl senv = | SFBmodule _ -> M | SFBmodtype _ -> MT in - add_field field new_name senv + add_field ~is_include:true field new_name senv in resolver, List.fold_left add senv str diff --git a/kernel/vars.ml b/kernel/vars.ml index 7380a860dd..f9c576ca4a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Esubst module RelDecl = Context.Rel.Declaration @@ -80,19 +79,9 @@ let noccur_with_meta n m term = (* Lifting *) (*********************) -(* The generic lifting function *) -let rec exliftn el c = match Constr.kind c with - | Constr.Rel i -> Constr.mkRel(reloc_rel i el) - | _ -> Constr.map_with_binders el_lift exliftn el c - -(* Lifting the binding depth across k bindings *) - -let liftn n k c = - match el_liftn (pred k) (el_shft n el_id) with - | ELID -> c - | el -> exliftn el c - -let lift n = liftn n 1 +let exliftn = Constr.exliftn +let liftn = Constr.liftn +let lift = Constr.lift (*********************) (* Substituting *) diff --git a/lib/envars.ml b/lib/envars.ml index 724a3dddc7..b5036e7340 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -177,10 +177,6 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; - fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name Coq_config.camlp5bin; - fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name Coq_config.camlp5lib; - fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml index 7b4b1eab73..a485bf31c0 100644 --- a/lib/pp_diff.ml +++ b/lib/pp_diff.ml @@ -86,7 +86,7 @@ let shorten_diff_span dtype diff_list = if (get_variant !src) = dtype then begin if (lt !dst !src) then dst := !src; - while (lt !dst len) && (get_variant !dst) <> `Common do + while (lt !dst len) && (get_variant !dst) = dtype do dst := !dst + incr; done; if (lt !dst len) && (get_str !src) = (get_str !dst) then begin diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 619718f723..d81ee475b5 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -11,6 +11,7 @@ open Pp open Util open Tok +open Gramlib (** Location utilities *) let ploc_file_of_coq_file = function diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index e4aa8debc1..c0ebdd45ef 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -40,7 +40,7 @@ where tok_text : pattern -> string; tok_comm : mutable option (list location) } *) -include Grammar.GLexerType with type te = Tok.t +include Gramlib.Grammar.GLexerType with type te = Tok.t module Error : sig type t diff --git a/parsing/dune b/parsing/dune index 0669e3a3c2..e91740650f 100644 --- a/parsing/dune +++ b/parsing/dune @@ -2,7 +2,6 @@ (name parsing) (public_name coq.parsing) (wrapped false) - (flags :standard -open Gramlib) (libraries coq.gramlib proofs)) (rule diff --git a/parsing/extend.ml b/parsing/extend.ml index 6fe2956643..5caeab535a 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -10,7 +10,7 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Grammar.GMake(CLexer).Entry.e +type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e type side = Left | Right diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index e25f7aa54f..b3ae24e941 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -81,7 +81,7 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let lpar_id_coloneq = - Gram.Entry.of_parser "test_lpar_id_coloneq" + Pcoq.Entry.of_parser "test_lpar_id_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -96,7 +96,7 @@ let lpar_id_coloneq = | _ -> err ()) let impl_ident_head = - Gram.Entry.of_parser "impl_ident_head" + Pcoq.Entry.of_parser "impl_ident_head" (fun strm -> match stream_nth 0 strm with | KEYWORD "{" -> @@ -109,7 +109,7 @@ let impl_ident_head = | _ -> err ()) let name_colon = - Gram.Entry.of_parser "name_colon" + Pcoq.Entry.of_parser "name_colon" (fun strm -> match stream_nth 0 strm with | IDENT s -> diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index dfb788907e..6247a12640 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -13,7 +13,6 @@ open Names open Libnames -open Pcoq open Pcoq.Prim let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index d4aa598fd8..170df6ad09 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -12,8 +12,8 @@ open CErrors open Util open Extend open Genarg +open Gramlib -let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) @@ -83,13 +83,9 @@ module type S = *) type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable - val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -100,9 +96,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct include Grammar.GMake(CLexer) type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action type coq_parsable = parsable * CLexer.lexer_state ref @@ -113,7 +106,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct state := CLexer.get_lexer_state (); (a,state) - let action = Gramext.action let entry_create = Entry.create let entry_parse e (p,state) = @@ -148,6 +140,9 @@ struct let create = G.Entry.create let parse = G.entry_parse let print = G.Entry.print + let of_parser = G.Entry.of_parser + let name = G.Entry.name + let parse_token_stream = G.Entry.parse_token_stream end @@ -166,16 +161,9 @@ let of_coq_position = function | Extend.Level s -> Gramext.Level s module Symbols : sig - val stoken : Tok.t -> G.symbol - val sself : G.symbol - val snext : G.symbol - val slist0 : G.symbol -> G.symbol - val slist0sep : G.symbol * G.symbol -> G.symbol - val slist1 : G.symbol -> G.symbol - val slist1sep : G.symbol * G.symbol -> G.symbol - val sopt : G.symbol -> G.symbol - val snterml : G.internal_entry * string -> G.symbol - val snterm : G.internal_entry -> G.symbol + val stoken : Tok.t -> ('s, string) G.ty_symbol + val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol + val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol end = struct let stoken tok = @@ -190,19 +178,10 @@ end = struct | Tok.BULLET s -> "BULLET", s | Tok.EOI -> "EOI", "" in - Gramext.Stoken pattern - - let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) - let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) - - let snterml (x, y) = Gramext.Snterml (x, y) - let snterm x = Gramext.Snterm x - let sself = Gramext.Sself - let snext = Gramext.Snext - let slist0 x = Gramext.Slist0 x - let slist1 x = Gramext.Slist1 x - let sopt x = Gramext.Sopt x + G.s_token pattern + let slist0sep x y = G.s_list0sep x y false + let slist1sep x y = G.s_list1sep x y false end let camlp5_verbosity silent f x = @@ -224,40 +203,41 @@ let camlp5_verbosity silent f x = (** Binding general entry keys to symbol *) -let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function -| Stop -> fun f -> G.action (fun loc -> f (!@ loc)) -| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) - -let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function - | Atoken t -> Symbols.stoken t - | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) - | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) - | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) - | Aself -> Symbols.sself - | Anext -> Symbols.snext - | Aentry e -> - Symbols.snterm (G.Entry.obj e) - | Aentryl (e, n) -> - Symbols.snterml (G.Entry.obj e, n) - | Arules rs -> - Gramext.srules (List.map symbol_of_rules rs) - -and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function -| Stop -> fun accu -> accu -| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) - -and symbol_of_rules : type a. a Extend.rules -> _ = function +type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function +| Atoken t -> Symbols.stoken t +| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s) +| Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) +| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s) +| Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) +| Aopt s -> G.s_opt (symbol_of_prod_entry_key s) +| Aself -> G.s_self +| Anext -> G.s_next +| Aentry e -> G.s_nterm e +| Aentryl (e, n) -> G.s_nterml e n +| Arules rs -> G.s_rules (List.map symbol_of_rules rs) + +and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function +| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) +| Next (r, s) -> + let Casted (r, cast) = symbol_of_rule r in + Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x))) + +and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function | Rules (r, act) -> - let symb = symbol_of_rule r.norec_rule [] in - let act = of_coq_action r.norec_rule act in - (symb, act) + let Casted (symb, cast) = symbol_of_rule r.norec_rule in + G.production (symb, cast act) + +(** FIXME: This is a hack around a deficient camlp5 API *) +type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production -let of_coq_production_rule : type a. a Extend.production_rule -> _ = function -| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) +let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function +| Rule (toks, act) -> + let Casted (symb, cast) = symbol_of_rule toks in + AnyProduction (symb, cast act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) @@ -265,6 +245,13 @@ let of_coq_single_extend_statement (lvl, assoc, rule) = let of_coq_extend_statement (pos, st) = (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) +let fix_extend_statement (pos, st) = + let fix_single_extend_statement (lvl, assoc, rules) = + let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in + (lvl, assoc, List.map fix_production_rule rules) + in + (pos, List.map fix_single_extend_statement st) + (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position @@ -291,7 +278,7 @@ let camlp5_entries = ref EntryDataMap.empty let grammar_delete e reinit (pos,rls) = List.iter (fun (n,ass,lev) -> - List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) + List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) (List.rev rls); match reinit with | Some (a,ext) -> @@ -301,7 +288,7 @@ let grammar_delete e reinit (pos,rls) = | Some (Gramext.Level n) -> n | _ -> assert false in - (G.extend e) (Some ext) [Some lev,Some a,[]] + (G.safe_extend e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -309,13 +296,15 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in + let ext = fix_extend_statement ext in + let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) + let ext = fix_extend_statement (of_coq_extend_statement ext) in + camlp5_verbosity false (uncurry (G.safe_extend e)) ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -323,25 +312,6 @@ let grammar_extend_sync e reinit ext = module Gram = struct include G - let extend e = - curry - (fun ext -> - camlp5_state := - (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> uncurry (G.extend e) ext))) - :: !camlp5_state; - uncurry (G.extend e) ext) - let delete_rule e pil = - (* spiwack: if you use load an ML module which contains GDELETE_RULE - in a section, God kills a kitty. As it would corrupt remove_grammars. - There does not seem to be a good way to undo a delete rule. As deleting - takes fewer arguments than extending. The production rule isn't returned - by delete_rule. If we could retrieve the necessary information, then - ByEXTEND provides just the framework we need to allow this in section. - I'm not entirely sure it makes sense, but at least it would be more correct. - *) - G.delete_rule e pil - let gram_extend e ext = grammar_extend e None ext end (** Remove extensions @@ -380,16 +350,16 @@ let make_rule r = [None, None, r] let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in - let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in - let act = Gram.action (fun _ x loc -> x) in - uncurry (Gram.extend e) (None, make_rule [symbs, act]); + let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in + let act = fun _ x loc -> x in + Gram.safe_extend e None (make_rule [G.production (symbs, act)]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in - let symbs = [Symbols.snterm (Gram.Entry.obj en)] in - let act = Gram.action (fun x loc -> f x) in - uncurry (Gram.extend e) (None, make_rule [symbs, act]); + let symbs = G.r_next G.r_stop (G.s_nterm en) in + let act = fun x loc -> f x in + Gram.safe_extend e None (make_rule [G.production (symbs, act)]); e (* Parse a string, does NOT check if the entire string was read @@ -516,10 +486,10 @@ module Module = end let epsilon_value f e = - let r = Rule (Next (Stop, e), fun x _ -> f x) in - let ext = of_coq_extend_statement (None, [None, None, [r]]) in + let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in + let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in - let () = uncurry (G.extend entry) ext in + let () = G.safe_extend entry None ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c05229d576..e64c614149 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,20 +13,10 @@ open Extend open Genarg open Constrexpr open Libnames +open Gramlib (** The parser of Coq *) -(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE. - We only have it here to work with Camlp5. Handwritten grammar extensions - should use the safe [Pcoq.grammar_extend] function below. *) -module Gram : sig - - include Grammar.S with type te = Tok.t - - val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit - -end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e - module Parsable : sig type t @@ -40,6 +30,9 @@ module Entry : sig val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit + val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t + val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a + val name : 'a t -> string end (** The parser of Coq is built from three kinds of rule declarations: diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 92fa94d6dc..ef1d1af199 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -131,8 +131,7 @@ let finish_proof dynamic_infos g = g -let refine c = - Tacmach.refine c +let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) let thin l = Proofview.V82.of_tactic (Tactics.clear l) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 7e707b423a..8f0440a2a4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -145,7 +145,6 @@ END { -module Gram = Pcoq.Gram module Vernac = Pvernac.Vernac_ module Tactic = Pltac diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 9f583234d8..002eb28eea 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -2,5 +2,4 @@ (name recdef_plugin) (public_name coq.plugins.recdef) (synopsis "Coq's functional induction plugin") - (flags :standard -open Gramlib) (libraries coq.plugins.extraction)) diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index c4c4e51ecc..156ee94a66 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -332,7 +332,7 @@ END let local_test_lpar_id_colon = let err () = raise Stream.Failure in - Pcoq.Gram.Entry.of_parser "lpar_id_colon" + Pcoq.Entry.of_parser "lpar_id_colon" (fun strm -> match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index bd8a097154..338839ee96 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -70,7 +70,7 @@ let _ = (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" + Pcoq.Entry.of_parser "test_bracket_ident" (fun strm -> match stream_nth 0 strm with | KEYWORD "[" -> diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index e29f78af5b..ef18dd6cdc 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -45,7 +45,6 @@ let with_tac f tac = * Subtac. These entries are named Subtac.<foo> *) -module Gram = Pcoq.Gram module Tactic = Pltac open Pcoq diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2596bc22f2..f7375a0f01 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -226,8 +226,6 @@ let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer -open Pcoq - } GRAMMAR EXTEND Gram diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 0ce0fbd0cd..46ea3819ac 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -39,7 +39,7 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = - Gram.Entry.of_parser "lpar_id_coloneq" + Pcoq.Entry.of_parser "lpar_id_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -53,7 +53,7 @@ let test_lpar_id_coloneq = (* Hack to recognize "(x)" *) let test_lpar_id_rpar = - Gram.Entry.of_parser "lpar_id_coloneq" + Pcoq.Entry.of_parser "lpar_id_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -67,7 +67,7 @@ let test_lpar_id_rpar = (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = - Gram.Entry.of_parser "test_lpar_idnum_coloneq" + Pcoq.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> match stream_nth 0 strm with | KEYWORD "(" -> @@ -84,7 +84,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Gram.Entry.of_parser "lpar_id_colon" + Pcoq.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with @@ -108,7 +108,7 @@ let check_for_coloneq = | _ -> err ()) let lookup_at_as_comma = - Gram.Entry.of_parser "lookup_at_as_comma" + Pcoq.Entry.of_parser "lookup_at_as_comma" (fun strm -> match stream_nth 0 strm with | KEYWORD (","|"at"|"as") -> () diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune index 1b31655310..5611f5ba16 100644 --- a/plugins/ltac/plugin_base.dune +++ b/plugins/ltac/plugin_base.dune @@ -3,7 +3,6 @@ (public_name coq.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (flags :standard -open Gramlib) (libraries coq.stm)) (library diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 188d5de7de..ac2d88dec2 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -697,7 +697,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 79f9e093fb..309db539d0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -125,7 +125,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index fa58a1c39a..efc4a2c743 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); - Tacmach.refine_no_check t gl + Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in @@ -1092,8 +1092,8 @@ let tclDO n tac = let _, info = CErrors.push e in let e' = CErrors.UserError (l, prefix i ++ s) in Util.iraise (e', info) - | Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> + raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e92489e568..e25c93bf0a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm val mk_ast_closure_term : [ `None | `Parens | `DoubleParens | `At ] -> Constrexpr.constr_expr -> ast_closure_term -val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal +val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index d09b81593e..2c9ec3a7cf 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -398,13 +398,13 @@ let revtoptac n0 gl = let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl + Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl let equality_inj l b id c gl = let msg = ref "" in try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with - | Ploc.Exc(_,CErrors.UserError (_,s)) + | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s)) | CErrors.UserError (_,s) when msg := Pp.string_of_ppcmds s; !msg = "Not a projectable equality but a discriminable one." || diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7c91860228..2dff0cc84f 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -268,16 +268,16 @@ let negate_parser f x = | Some _ -> raise Stream.Failure let test_not_ssrslashnum = - Pcoq.Gram.Entry.of_parser + Pcoq.Entry.of_parser "test_not_ssrslashnum" (negate_parser test_ssrslashnum10) let test_ssrslashnum00 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 let test_ssrslashnum10 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 + Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 let test_ssrslashnum11 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 + Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 let test_ssrslashnum01 = - Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 } @@ -470,7 +470,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "@" -> xWithAt | _ -> xNoFlag -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind (* New kinds of terms *) @@ -481,7 +481,7 @@ let input_term_annotation strm = | Tok.KEYWORD "@" :: _ -> `At | _ -> `None let term_annotation = - Gram.Entry.of_parser "term_annotation" input_term_annotation + Pcoq.Entry.of_parser "term_annotation" input_term_annotation (* terms *) @@ -800,7 +800,7 @@ let reject_ssrhid strm = | _ -> ()) | _ -> () -let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid +let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid } @@ -961,7 +961,7 @@ let accept_ssrfwdid strm = | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm | _ -> raise Stream.Failure -let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid +let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid } @@ -1540,7 +1540,7 @@ let accept_ssrseqvar strm = accept_before_syms_or_ids ["["] ["first";"last"] strm | _ -> raise Stream.Failure -let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar +let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar let swaptacarg (loc, b) = (b, []), Some (TacId []) @@ -1628,7 +1628,7 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) +let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ()) } @@ -1955,7 +1955,7 @@ let accept_ssreqid strm = accept_before_syms [":"] strm | _ -> raise Stream.Failure -let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid +let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid } @@ -2373,7 +2373,7 @@ let test_ssr_rw_syntax = match Util.stream_nth 0 strm with | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in - Gram.Entry.of_parser "test_ssr_rw_syntax" test + Pcoq.Entry.of_parser "test_ssr_rw_syntax" test } @@ -2583,7 +2583,7 @@ let accept_idcomma strm = | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm | _ -> raise Stream.Failure -let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma +let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma } diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 3f0794fdd4..4ddaeb49fd 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -11,7 +11,6 @@ { open Ltac_plugin -open Pcoq open Pcoq.Constr open Ssrmatching open Ssrmatching.Internal @@ -69,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind } diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune index 1450a94de1..06f67c3774 100644 --- a/plugins/ssrmatching/plugin_base.dune +++ b/plugins/ssrmatching/plugin_base.dune @@ -2,5 +2,4 @@ (name ssrmatching_plugin) (public_name coq.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") - (flags :standard -open Gramlib) (libraries coq.plugins.ltac)) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 63b7e1783e..93a8c48435 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -230,7 +230,7 @@ sig val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern - val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern + val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern val pr_rpattern : rpattern -> Pp.t val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern @@ -238,7 +238,7 @@ sig val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern - val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern + val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern val pr_ssrterm : cpattern -> Pp.t end diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 14358dd02a..10d8451947 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -759,6 +759,6 @@ let control_only_guard env sigma c = in let rec iter env c = check_fix_cofix env c; - iter_constr_with_full_binders sigma EConstr.push_rel iter env c + EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c in iter env c diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8c57fc2375..abf52d2893 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -215,7 +215,7 @@ type frozen = (** Proper partition of the evar map as described above. *) let frozen_and_pending_holes (sigma, sigma') = - let undefined0 = Evd.undefined_map sigma in + let undefined0 = Option.cata Evd.undefined_map Evar.Map.empty sigma in (** Fast path when the undefined evars where not modified *) if undefined0 == Evd.undefined_map sigma' then FrozenId undefined0 @@ -306,8 +306,8 @@ let check_evars_are_solved env sigma frozen = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars ?hook flags env sigma init_sigma = - let frozen = frozen_and_pending_holes (init_sigma, sigma) in +let solve_remaining_evars ?hook flags env ?initial sigma = + let frozen = frozen_and_pending_holes (initial, sigma) in let sigma = if flags.use_typeclasses then apply_typeclasses env sigma frozen false @@ -324,12 +324,12 @@ let solve_remaining_evars ?hook flags env sigma init_sigma = if flags.fail_evar then check_evars_are_solved env sigma frozen; sigma -let check_evars_are_solved env current_sigma init_sigma = - let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in +let check_evars_are_solved env ?initial current_sigma = + let frozen = frozen_and_pending_holes (initial, current_sigma) in check_evars_are_solved env current_sigma frozen -let process_inference_flags flags env initial_sigma (sigma,c,cty) = - let sigma = solve_remaining_evars flags env sigma initial_sigma in +let process_inference_flags flags env initial (sigma,c,cty) = + let sigma = solve_remaining_evars flags env ~initial sigma in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c,cty diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2eaa77b822..59e6c00037 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -95,13 +95,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> - env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map + env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit + env -> ?initial:evar_map -> (* current map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 490d58fa52..8c1aae26ae 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1530,7 +1530,7 @@ let indirectly_dependent sigma c d decls = List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = - let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in + let sigma = Pretyping.solve_remaining_evars flags env current_sigma ~initial:pending in (sigma, nf_evar sigma c) let default_matching_core_flags sigma = diff --git a/printing/dune b/printing/dune index 837ac48009..3392342165 100644 --- a/printing/dune +++ b/printing/dune @@ -2,6 +2,5 @@ (name printing) (synopsis "Coq's Term Pretty Printing Library") (public_name coq.printing) - (flags :standard -open Gramlib) (wrapped false) (libraries parsing proofs)) diff --git a/printing/printer.ml b/printing/printer.ml index 831008a957..4840577cbf 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -685,10 +685,6 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | None -> GoalMap.empty in - let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) - try GoalMap.find ng diff_goal_map with Not_found -> ng - in - (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -724,7 +720,12 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map let get_ogs g = match os_map with - | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma } + | Some (osigma, _) -> + (* if Not_found, returning None treats the goal as new and it will be highlighted; + returning Some { it = g; sigma = sigma } will compare the new goal + to itself and it won't be highlighted *) + (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma } + with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)")) | None -> None in let rec pr_rec n = function diff --git a/printing/printer.mli b/printing/printer.mli index 785f452a7b..cefc005c74 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -13,7 +13,6 @@ open Constr open Environ open Pattern open Evd -open Proof_type open Glob_term open Ltac_pretype @@ -144,7 +143,7 @@ val pr_transparent_state : TransparentState.t -> Pp.t records containing the goal and sigma for, respectively, the new and old proof steps, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t +val pr_goal : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t (** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals] prints the goals in [goals] followed by the goals in [unfocused] in a compact form @@ -161,17 +160,17 @@ val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> there are non-instantiated existential variables. [stack] is used to print summary info on unfocused goals. *) -val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map - -> seeds:goal list -> shelf:goal list -> stack:int list - -> unfocused: goal list -> goals:goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list + -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t -val pr_subgoal : int -> evar_map -> goal list -> Pp.t +val pr_subgoal : int -> evar_map -> Goal.goal list -> Pp.t (** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion, [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t +val pr_concl : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t (** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop. The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their @@ -182,7 +181,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 0b630b39b5..cc1bcc66ae 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -88,7 +88,7 @@ let tokenize_string s = let st = CLexer.get_lexer_state () in try let istr = Stream.of_string s in - let lex = CLexer.lexer.Plexing.tok_func istr in + let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in let toks = stream_tok [] (fst lex) in CLexer.set_lexer_state st; toks @@ -214,26 +214,22 @@ module CDC = Context.Compacted.Declaration let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) = let open CDC in function - | LocalAssum(idl, tm) -> (idl, None, tm) - | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);; + | LocalAssum(idl, tm) -> (idl, None, EConstr.of_constr tm) + | LocalDef(idl,tdef,tm) -> (idl, Some (EConstr.of_constr tdef), EConstr.of_constr tm);; (* XXX: Very unfortunately we cannot use the Proofview interface as Proof is still using the "legacy" one. *) -let process_goal_concl sigma g : Constr.t * Environ.env = +let process_goal_concl sigma g : EConstr.t * Environ.env = let env = Goal.V82.env sigma g in let ty = Goal.V82.concl sigma g in - let ty = EConstr.to_constr sigma ty in (ty, env) -let process_goal sigma g : Constr.t reified_goal = +let process_goal sigma g : EConstr.t reified_goal = let env = Goal.V82.env sigma g in - let hyps = Goal.V82.hyps sigma g in let ty = Goal.V82.concl sigma g in let name = Goal.uid g in - (* There is a Constr/Econstr mess here... *) - let ty = EConstr.to_constr sigma ty in (* compaction is usually desired [eg for better display] *) - let hyps = Termops.compact_named_context (Environ.named_context_of_val hyps) in + let hyps = Termops.compact_named_context (Environ.named_context env) in let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; @@ -241,13 +237,15 @@ let pr_letype_core goal_concl_style env sigma t = Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t) let pp_of_type env sigma ty = - pr_letype_core true env sigma EConstr.(of_constr ty) + pr_letype_core true env sigma ty let pr_leconstr_core goal_concl_style env sigma t = Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t) let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) +let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c + let diff_concl ?og_s nsigma ng = let open Evd in let o_concl_pp = match og_s with @@ -291,8 +289,8 @@ let goal_info goal sigma = line_idents := idents :: !line_idents; let mid = match body with | Some c -> - let pb = pr_lconstr_env env sigma c in - let pb = if Constr.isCast c then surround pb else pb in + let pb = pr_lconstr_env_econstr env sigma c in + let pb = if EConstr.isCast sigma c then surround pb else pb in str " := " ++ pb | None -> mt() in let ts = pp_of_type env sigma ty in @@ -409,7 +407,7 @@ let match_goals ot nt = match exp, exp2 with | Some expa, Some expb -> constr_expr ogname expa expb | None, None -> () - | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)") + | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)") in let local_binder_expr ogname exp exp2 = match exp, exp2 with @@ -421,7 +419,7 @@ let match_goals ot nt = | CLocalPattern p, CLocalPattern p2 -> let (p,ty), (p2,ty2) = p.v,p2.v in constr_expr_opt ogname ty ty2 - | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)") + | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)") in let recursion_order_expr ogname exp exp2 = match exp, exp2 with @@ -431,7 +429,7 @@ let match_goals ot nt = | CMeasureRec (m,r), CMeasureRec (m2,r2) -> constr_expr ogname m m2; constr_expr_opt ogname r r2 - | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)") + | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)") in let fix_expr ogname exp exp2 = let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in @@ -515,7 +513,7 @@ let match_goals ot nt = | CastNative a, CastNative a2 -> constr_expr ogname a a2 | CastCoerce, CastCoerce -> () - | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)")) + | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)")) | CNotation (ntn,args), CNotation (ntn2,args2) -> constr_notation_substitution ogname args args2 | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) -> @@ -523,7 +521,7 @@ let match_goals ot nt = | CPrim p, CPrim p2 -> () | CDelimiters (key,e), CDelimiters (key2,e2) -> constr_expr ogname e e2 - | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)") + | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)") end in @@ -563,9 +561,8 @@ let db_goal_map op np ng_to_og = Printf.printf "\n" [@@@ocaml.warning "+32"] -(* Create a map from new goals to old goals for proof diff. The map only - has entries for new goals that are not the same as the corresponding old - goal; there are no entries for unchanged goals. +(* Create a map from new goals to old goals for proof diff. New goals + that are evars not appearing in the proof will not have a mapping. It proceeds as follows: 1. Find the goal ids that were removed from the old proof and that were @@ -583,7 +580,7 @@ let db_goal_map op np ng_to_og = the removed goal. - if there are more than 2 removals and more than one addition, call match_goals to get a map between old and new evar names, then use this - to create the map from new goal ids to old goal ids for the differing goals. + to create the map from new goal ids to old goal ids. *) let make_goal_map_i op np = let ng_to_og = ref GoalMap.empty in @@ -598,6 +595,9 @@ let make_goal_map_i op np = let add_gs = diff ngs ogs in let num_adds = cardinal add_gs in + (* add common goals *) + Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x x !ng_to_og) (inter ogs ngs); + if num_rems = 0 then !ng_to_og (* proofs are the same *) else if num_adds = 0 then @@ -616,17 +616,16 @@ let make_goal_map_i op np = List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) (Goal.Set.elements rem_gs); - try - let (_,_,_,_,nsigma) = Proof.proof np in - let get_og ng = - let nevar = goal_to_evar ng nsigma in - let oevar = StringMap.find nevar nevar_to_oevar in - let og = StringMap.find oevar !oevar_to_og in - og - in - Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs; - !ng_to_og - with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)") + let (_,_,_,_,nsigma) = Proof.proof np in + let get_og ng = + let nevar = goal_to_evar ng nsigma in + let oevar = StringMap.find nevar nevar_to_oevar in + let og = StringMap.find oevar !oevar_to_og in + og + in + Goal.Set.iter (fun ng -> + try ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og with Not_found -> ()) add_gs; + !ng_to_og end let make_goal_map op np = diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 832393e15f..ce9ee5ae6f 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,7 +16,6 @@ val write_diffs_option : string -> unit val show_diffs : unit -> bool open Evd -open Proof_type open Environ open Constr @@ -31,7 +30,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t +val diff_goal_ide : Goal.goal sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t (** Computes the diff between two goals @@ -43,7 +42,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t +val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list @@ -53,7 +52,7 @@ val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.cons val pr_lconstr_env : env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) -val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t +val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t (** Generates a map from [np] to [op] that maps changed goals to their prior forms. The map doesn't include entries for unchanged goals; unchanged goals @@ -61,7 +60,7 @@ will have the same goal id in both versions. [op] and [np] must be from the same proof document and [op] must be for a state before [np]. *) -val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t +val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c7703b52c7..4720328893 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,6 @@ open EConstr open Refiner open Logic open Reduction -open Tacmach open Clenv (* This function put casts around metavariables whose type could not be @@ -79,7 +78,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl end let clenv_pose_dependent_evars ?(with_evars=false) clenv = diff --git a/proofs/logic.ml b/proofs/logic.ml index f9e2edd888..15ba0a704f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -20,7 +20,6 @@ open Environ open Reductionops open Inductiveops open Typing -open Proof_type open Type_errors open Retyping @@ -585,12 +584,15 @@ let convert_hyp check sign sigma d = let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - match r with - (* Logical rules *) - | Refine c -> - let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables env sigma c; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) + let cl = EConstr.Unsafe.to_constr cl in + check_meta_variables env sigma r; + let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in + let sgl = List.rev sgl in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in + (sgl, sigma) + +let prim_refiner ~check r sigma goal = + if check then + with_check (prim_refiner r sigma) goal + else + prim_refiner r sigma goal diff --git a/proofs/logic.mli b/proofs/logic.mli index 2cad278e10..f99076db23 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -13,27 +13,20 @@ open Names open Constr open Evd -open Proof_type -(** This suppresses check done in [prim_refiner] for the tactic given in - argument; works by side-effect *) - -val with_check : tactic -> tactic - -(** [without_check] respectively means:\\ - [Intro]: no check that the name does not exist\\ - [Intro_after]: no check that the name does not exist and that variables in +(** [check] respectively means:\\ + [Intro]: check that the name does not exist\\ + [Intro_after]: check that the name does not exist and that variables in its type does not escape their scope\\ - [Intro_replacing]: no check that the name does not exist and that + [Intro_replacing]: check that the name does not exist and that variables in its type does not escape their scope\\ [Convert_hyp]: - no check that the name exist and that its type is convertible\\ + check that the name exist and that its type is convertible\\ *) (** The primitive refiner. *) -val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map - +val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map (** {6 Refiner errors. } *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 76a9a9f4c8..6c13c4946a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -504,4 +504,6 @@ let all_goals p = let set = add goals Goal.Set.empty in let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in let set = add shelf set in - add given_up set + let set = add given_up set in + let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in + add bgoals set diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index 149f30c673..0000000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Legacy proof engine. Do not use in newly written code. *) - -open Evd -open Constr - -(** This module defines the structure of proof tree and the tactic type. So, it - is used by [Proof_tree] and [Refiner] *) - -type prim_rule = - | Refine of constr - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index f9bb2c3d60..dbd5be23ab 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_type Refine Proof Logic diff --git a/proofs/refiner.ml b/proofs/refiner.ml index be32aadd91..bce227dabb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,9 +12,10 @@ open Pp open CErrors open Util open Evd -open Proof_type open Logic +type tactic = Proofview.V82.tac + module NamedDecl = Context.Named.Declaration let sig_it x = x.it @@ -25,16 +26,16 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let refiner pr goal_sigma = - let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in +let refiner ~check pr goal_sigma = + let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in { it = sgl; sigma = sigma'; } (* Profiling refiner *) -let refiner = +let refiner ~check = if Flags.profile then let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key refiner - else refiner + CProfile.profile2 refiner_key (refiner ~check) + else refiner ~check (*********************) (* Tacticals *) @@ -178,9 +179,9 @@ let tclPROGRESS tac ptree = NOTE: some tactics delete hypothesis and reuse names (induction, destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) - :Proof_type.goal list Evd.sigma = + : Goal.goal list Evd.sigma = let oldhyps = pf_hyps goal in - let rslt:Proof_type.goal list Evd.sigma = tac goal in + let rslt:Goal.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 30af6d8e1a..52cbf7658b 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -11,18 +11,18 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Proof_type open EConstr (** The refiner (handles primitive rules and high-level tactics). *) +type tactic = Proofview.V82.tac val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map -val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_env : Goal.goal sigma -> Environ.env +val pf_hyps : Goal.goal sigma -> named_context -val refiner : rule -> tactic +val refiner : check:bool -> Constr.t -> tactic (** {6 Tacticals. } *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 231a8fe266..64d7630d55 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -17,9 +17,7 @@ open Evd open Typing open Redexpr open Tacred -open Proof_type open Logic -open Refiner open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -30,7 +28,7 @@ let re_sig it gc = { it = it; sigma = gc; } (* Operations for handling terms under a local typing context *) (**************************************************************) -type tactic = Proof_type.tactic +type tactic = Proofview.V82.tac let sig_it = Refiner.sig_it let project = Refiner.project @@ -103,20 +101,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -(********************************************) -(* Definition of the most primitive tactics *) -(********************************************) - -let refiner = refiner - -let refine_no_check c gl = - let c = EConstr.Unsafe.to_constr c in - refiner (Refine c) gl - -(* Versions with consistency checks *) - -let refine c = with_check (refine_no_check c) - (* Pretty-printers *) open Pp diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 14c83a6802..ef6a1544e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,85 +12,78 @@ open Names open Constr open Environ open EConstr -open Proof_type open Redexpr open Locus (** Operations for handling terms under a local typing context. *) open Evd -type tactic = Proof_type.tactic;; + +type tactic = Proofview.V82.tac val sig_it : 'a sigma -> 'a -val project : goal sigma -> evar_map +val project : Goal.goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val pf_concl : goal sigma -> types -val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context -(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) -val pf_hyps_types : goal sigma -> (Id.t * types) list -val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration -val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> evar_map * constr -val pf_unsafe_type_of : goal sigma -> constr -> types -val pf_type_of : goal sigma -> constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> constr -> types +val pf_concl : Goal.goal sigma -> types +val pf_env : Goal.goal sigma -> env +val pf_hyps : Goal.goal sigma -> named_context +(*i val pf_untyped_hyps : Goal.goal sigma -> (Id.t * constr) list i*) +val pf_hyps_types : Goal.goal sigma -> (Id.t * types) list +val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t +val pf_last_hyp : Goal.goal sigma -> named_declaration +val pf_ids_of_hyps : Goal.goal sigma -> Id.t list +val pf_global : Goal.goal sigma -> Id.t -> evar_map * constr +val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +val pf_type_of : Goal.goal sigma -> constr -> evar_map * types +val pf_hnf_type_of : Goal.goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration -val pf_get_hyp_typ : goal sigma -> Id.t -> types +val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration +val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types -val pf_get_new_id : Id.t -> goal sigma -> Id.t +val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr +val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr -val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a +val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> - goal sigma -> 'a -> goal sigma * 'b + Goal.goal sigma -> 'a -> Goal.goal sigma * 'b val pf_reduce : (env -> evar_map -> constr -> constr) -> - goal sigma -> constr -> constr + Goal.goal sigma -> constr -> constr val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> - goal sigma -> constr -> evar_map * constr - -val pf_whd_all : goal sigma -> constr -> constr -val pf_hnf_constr : goal sigma -> constr -> constr -val pf_nf : goal sigma -> constr -> constr -val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_compute : goal sigma -> constr -> constr + Goal.goal sigma -> constr -> evar_map * constr + +val pf_whd_all : Goal.goal sigma -> constr -> constr +val pf_hnf_constr : Goal.goal sigma -> constr -> constr +val pf_nf : Goal.goal sigma -> constr -> constr +val pf_nf_betaiota : Goal.goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_compute : Goal.goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> constr -> constr - -val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : goal sigma -> constr -> constr -> bool - -(** {6 The most primitive tactics. } *) - -val refiner : rule -> tactic -val refine_no_check : constr -> tactic + -> Goal.goal sigma -> constr -> constr -(** {6 The most primitive tactics with consistency and type checking } *) - -val refine : constr -> tactic +val pf_const_value : Goal.goal sigma -> pconstant -> constr +val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) -val pr_gls : goal sigma -> Pp.t -val pr_glls : goal list sigma -> Pp.t +val pr_gls : Goal.goal sigma -> Pp.t +val pr_glls : Goal.goal list sigma -> Pp.t [@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t + (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a val project : Proofview.Goal.t -> Evd.evar_map val pf_env : Proofview.Goal.t -> Environ.env diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 63ef4f850f..b8adb792e8 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -15,7 +15,6 @@ open Names open Constr open Termops open EConstr -open Proof_type open Tacticals open Tacmach open Evd @@ -203,7 +202,7 @@ let find_first_goal gls = type search_state = { priority : int; depth : int; (*r depth of search before failing *) - tacres : goal list sigma; + tacres : Goal.goal list sigma; last_tactic : Pp.t Lazy.t; dblist : hint_db list; localdb : hint_db list; diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e161d88824..5aa2f42de1 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -26,7 +26,7 @@ val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list -> val eauto_with_bases : ?debug:debug -> bool * int -> - delayed_open_constr list -> hint_db list -> Proof_type.tactic + delayed_open_constr list -> hint_db list -> Proofview.V82.tac val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 969f539d1f..b8967775bf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1028,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1354,8 +1354,8 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Proofview.V82.tactic (Tacmach.refine - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) ])] with Exit -> Proofview.tclUNIT () @@ -1400,7 +1400,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (Tacmach.refine pf)]) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f2cf915fe3..224cd68cf9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -26,6 +26,8 @@ module NamedDecl = Context.Named.Declaration (* Tacticals re-exported from the Refiner module *) (************************************************************************) +type tactic = Proofview.V82.tac + let tclIDTAC = Refiner.tclIDTAC let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE let tclORELSE0 = Refiner.tclORELSE0 diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cc15469d0e..2947e44f7a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -12,12 +12,13 @@ open Names open Constr open EConstr open Evd -open Proof_type open Locus open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) +type tactic = Proofview.V82.tac + val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic @@ -65,20 +66,20 @@ val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic val onNLastDecls : int -> (named_context -> tactic) -> tactic -val lastHypId : goal sigma -> Id.t -val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> named_declaration -val nLastHypsId : int -> goal sigma -> Id.t list -val nLastHyps : int -> goal sigma -> constr list -val nLastDecls : int -> goal sigma -> named_context +val lastHypId : Goal.goal sigma -> Id.t +val lastHyp : Goal.goal sigma -> constr +val lastDecl : Goal.goal sigma -> named_declaration +val nLastHypsId : int -> Goal.goal sigma -> Id.t list +val nLastHyps : int -> Goal.goal sigma -> constr list +val nLastDecls : int -> Goal.goal sigma -> named_context -val afterHyp : Id.t -> goal sigma -> named_context +val afterHyp : Id.t -> Goal.goal sigma -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic -val onHyps : (goal sigma -> named_context) -> +val onHyps : (Goal.goal sigma -> named_context) -> (named_context -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -127,11 +128,11 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis val compute_induction_names : bool list array -> or_and_intro_pattern option -> intro_patterns array -val elimination_sort_of_goal : goal sigma -> Sorts.family -val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family -val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family +val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family +val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family +val elimination_sort_of_clause : Id.t option -> Goal.goal sigma -> Sorts.family -val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic +val pf_with_evars : (Goal.goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 349cfce205..0beafb7e31 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -142,7 +142,6 @@ let introduction id = | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end -let refine = Tacmach.refine let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = @@ -1300,7 +1299,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) if not with_evars && occur_meta clenv.evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in - let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in + let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN @@ -1624,7 +1623,7 @@ let descend_in_conjunctions avoid tac (err, info) c = | Some (p,pt) -> Tacticals.New.tclTHENS (assert_before_gen false (NamingAvoid avoid) pt) - [Proofview.V82.tactic (refine p); + [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p)); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end))) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 4e91a9a728..75b5caaa36 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -12,7 +12,6 @@ open Names open Constr open EConstr open Environ -open Proof_type open Evd open Clenv open Redexpr @@ -50,8 +49,8 @@ val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t -val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t -val find_intro_names : rel_context -> goal sigma -> Id.t list +val fresh_id : Id.Set.t -> Id.t -> Goal.goal sigma -> Id.t +val find_intro_names : rel_context -> Goal.goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic diff --git a/test-suite/coqchk/bug_8937.v b/test-suite/coqchk/bug_8937.v new file mode 100644 index 0000000000..5b326e389b --- /dev/null +++ b/test-suite/coqchk/bug_8937.v @@ -0,0 +1,21 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + +Unset Elimination Schemes. +Module Type S. + +Inductive foo : Prop :=. +Definition bar (x:foo) : Prop := match x with end. + +End S. + +Module M. + +Inductive foo : Prop :=. +Definition bar (x:foo) : Prop := match x with end. + +End M. + +Module MS : S := M. + +Module F (Z:S) := Z. +Module MS' : S := F M. diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh new file mode 100755 index 0000000000..96bdee2fc2 --- /dev/null +++ b/test-suite/misc/quick-include.sh @@ -0,0 +1,5 @@ +#!/bin/sh +set -e + +$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v +$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v diff --git a/test-suite/misc/quick-include/file1.v b/test-suite/misc/quick-include/file1.v new file mode 100644 index 0000000000..fa48e240cb --- /dev/null +++ b/test-suite/misc/quick-include/file1.v @@ -0,0 +1,18 @@ + +Module Type E. End E. + +Module M. + Lemma x : True. + Proof. trivial. Qed. +End M. + + +Module Type T. + Lemma x : True. + Proof. trivial. Qed. +End T. + +Module F(A:E). + Lemma x : True. + Proof. trivial. Qed. +End F. diff --git a/test-suite/misc/quick-include/file2.v b/test-suite/misc/quick-include/file2.v new file mode 100644 index 0000000000..ab10dfd8de --- /dev/null +++ b/test-suite/misc/quick-include/file2.v @@ -0,0 +1,6 @@ + +From QuickInclude Require file1. + +Module M. Include file1.M. End M. +Module T. Include file1.T. End T. +Module F. Include file1.F. End F. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 46784d1897..d25ad5dca8 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -17,3 +17,7 @@ end : Expr -> Expr [(1 + 1)] : Expr +Let "x" e1 e2 + : expr +Let "x" e1 e2 + : expr diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 6bdbf1bed5..7800e91ee5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -70,3 +70,27 @@ Notation "( x )" := x (in custom expr at level 0, x at level 2). Check [1 + 1]. End C. + +(* An example of interaction between coercion and notations from + Robbert Krebbers. *) + +Require Import String. + +Module D. + +Inductive expr := + | Var : string -> expr + | Lam : string -> expr -> expr + | App : expr -> expr -> expr. + +Notation Let x e1 e2 := (App (Lam x e2) e1). + +Parameter e1 e2 : expr. + +Check (Let "x" e1 e2). + +Coercion App : expr >-> Funclass. + +Check (Let "x" e1 e2). + +End D. diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 526cefec44..7f9e6cc6e0 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -71,6 +71,13 @@ let _ = add_test "tokenize_string examples" t open Pp +(* example that was failing from #8922 *) +let t () = + Proof_diffs.write_diffs_option "removed"; + ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1"); + Proof_diffs.write_diffs_option "on" +let _ = add_test "shorten_diff_span failure from #8922" t + (* note pp_to_string concatenates adjacent strings, could become one token, e.g. str " a" ++ str "b " will give a token "ab" *) (* checks background is present and correct *) diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v index dc1397aff2..5e031efa85 100644 --- a/theories/Compat/Coq87.v +++ b/theories/Compat/Coq87.v @@ -9,6 +9,8 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.7 *) +Local Set Warnings "-deprecated". + Require Export Coq.Compat.Coq88. (* In 8.7, omega wasn't taking advantage of local abbreviations, diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 0aab64e4c4..989072940a 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,6 +9,8 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.8 *) +Local Set Warnings "-deprecated". + Require Export Coq.Compat.Coq89. (** In Coq 8.9, prim token notations follow [Import] rather than diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index d25671887f..49b9e4c951 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -9,3 +9,4 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.9 *) +Local Set Warnings "-deprecated". diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 92cc820483..b673225e40 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -20,7 +20,6 @@ include @CONF_FILE@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) -ML4FILES := $(COQMF_ML4FILES) MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) @@ -37,10 +36,6 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP5O := $(COQMF_CAMLP5O) -CAMLP5BIN := $(COQMF_CAMLP5BIN) -CAMLP5LIB := $(COQMF_CAMLP5LIB) -CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -99,7 +94,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str +CAMLDONTLINK=unix,str # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -192,22 +187,11 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) -ifeq (,$(CAMLLIB)) -PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") -else -PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif - ifneq (,$(TIMING)) TIMING_ARG=-time ifeq (after,$(TIMING)) @@ -774,10 +758,6 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 7c28ef24d4..15411d55d0 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -9,7 +9,7 @@ (************************************************************************) let fatal_error exn = - Topfmt.print_err_exn Topfmt.ParsingCommandLine exn; + Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn); let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index cbc5c124c8..5cf2157044 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -150,10 +150,11 @@ let print_highlight_location ib loc = let valid_buffer_loc ib loc = let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e + (* Toplevel error explanation. *) -let error_info_for_buffer ?loc phase buf = +let error_info_for_buffer ?loc buf = match loc with - | None -> Topfmt.pr_phase ?loc phase + | None -> Topfmt.pr_phase ?loc () | Some loc -> let fname = loc.Loc.fname in (* We are in the toplevel *) @@ -161,17 +162,17 @@ let error_info_for_buffer ?loc phase buf = | Loc.ToplevelInput -> let nloc = adjust_loc_buf buf loc in if valid_buffer_loc buf loc then - match Topfmt.pr_phase ~loc:nloc phase with + match Topfmt.pr_phase ~loc:nloc () with | None -> None | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc) (* in the toplevel, but not a valid buffer *) - else Topfmt.pr_phase ~loc phase + else Topfmt.pr_phase ~loc () (* we are in batch mode, don't adjust location *) - | Loc.InFile _ -> Topfmt.pr_phase ~loc phase + | Loc.InFile _ -> Topfmt.pr_phase ~loc () (* Actual printing routine *) -let print_error_for_buffer ?loc phase lvl msg buf = - let pre_hdr = error_info_for_buffer ?loc phase buf in +let print_error_for_buffer ?loc lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc buf in if !print_emacs then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg @@ -245,7 +246,7 @@ let parse_to_dot = | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in - Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -255,7 +256,7 @@ let rec discard_to_dot () = try Pcoq.Entry.parse parse_to_dot top_buffer.tokens with - | Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot () + | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () @@ -281,7 +282,7 @@ let extract_default_loc loc doc_id sid : Loc.t option = with _ -> loc (** Coqloop Console feedback handler *) -let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in +let coqloop_feed (fb : Feedback.feedback) = let open Feedback in match fb.contents with | Processed -> () | Incomplete -> () @@ -300,9 +301,9 @@ let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) | Message (Warning,loc,msg) -> let loc = extract_default_loc loc fb.doc_id fb.span_id in - TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer + TopErr.print_error_for_buffer ?loc Warning msg top_buffer | Message (lvl,loc,msg) -> - TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer + TopErr.print_error_for_buffer ?loc lvl msg top_buffer (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -362,7 +363,7 @@ let top_goal_print ~doc c oldp newp = let (e, info) = CErrors.push exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer (* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = @@ -404,7 +405,7 @@ let rec vernac_loop ~state = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer; + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; vernac_loop ~state let rec loop ~state = @@ -430,7 +431,7 @@ let loop ~opts ~state = let open Coqargs in print_emacs := opts.print_emacs; (* We initialize the console only if we run the toploop_run *) - let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in + let tl_feed = Feedback.add_feeder coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index b11f13d3cb..7d03484412 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -27,7 +27,7 @@ val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) -val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit +val coqloop_feed : Feedback.feedback -> unit (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 66469ff0b9..66af7f7cdf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,15 +30,6 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -(* Feedback received in the init stage, this is different as the STM - will not be generally be initialized, thus stateid, etc... may be - bogus. For now we just print to the console too *) -let coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization - -let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude - -let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile - let memory_stat = ref false let print_memory_stat () = begin (* -m|--memory from the command-line *) @@ -86,16 +77,11 @@ let load_vernacular opts ~state = else load_vernac s ) state (List.rev opts.load_vernacular_list) -let load_init_vernaculars cur_feeder opts ~state = +let load_init_vernaculars opts ~state = let state = - if opts.load_rcfile then begin - Feedback.del_feeder !cur_feeder; - let rc_feeder = Feedback.add_feeder coqtop_rcfile_feed in - let state = Coqinit.load_rcfile ~rcfile:opts.rcfile ~state in - Feedback.del_feeder rc_feeder; - cur_feeder := Feedback.add_feeder coqtop_init_feed; - state - end + if opts.load_rcfile then + Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -140,7 +126,7 @@ let fatal_error msg = exit 1 let fatal_error_exn exn = - Topfmt.print_err_exn Topfmt.Initialization exn; + Topfmt.(in_phase ~phase:Initialization print_err_exn exn); flush_all (); let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 @@ -186,7 +172,7 @@ let ensure_exists f = fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile cur_feeder opts ~echo ~f_in ~f_out = +let compile opts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in @@ -210,18 +196,14 @@ let compile cur_feeder opts ~echo ~f_in ~f_out = | None -> long_f_dot_v ^ "o" | Some f -> ensure_vo long_f_dot_v f in - Feedback.del_feeder !cur_feeder; - let doc_feeder = Feedback.add_feeder coqtop_doc_feed in - let doc, sid = - Stm.(new_doc - { doc_type = VoDoc long_f_dot_vo; - iload_path; require_libs; stm_options; - }) in - Feedback.del_feeder doc_feeder; - cur_feeder := Feedback.add_feeder coqtop_init_feed; + let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) + Stm.new_doc + Stm.{ doc_type = VoDoc long_f_dot_vo; + iload_path; require_libs; stm_options; + } in let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars cur_feeder opts ~state in + let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -262,18 +244,14 @@ let compile cur_feeder opts ~echo ~f_in ~f_out = async_proofs_tac_error_resilience = `None; } in - Feedback.del_feeder !cur_feeder; - let doc_feeder = Feedback.add_feeder coqtop_doc_feed in - let doc, sid = - Stm.(new_doc - { doc_type = VioDoc long_f_dot_vio; - iload_path; require_libs; stm_options; - }) in - Feedback.del_feeder doc_feeder; - cur_feeder := Feedback.add_feeder coqtop_init_feed; + let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) + Stm.new_doc + Stm.{ doc_type = VioDoc long_f_dot_vio; + iload_path; require_libs; stm_options; + } in let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars cur_feeder opts ~state in + let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in @@ -290,22 +268,22 @@ let compile cur_feeder opts ~echo ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile cur_feeder opts ~echo ~f_in ~f_out = +let compile opts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile cur_feeder opts ~echo ~f_in ~f_out; + compile opts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file cur_feeder opts (f_in, echo) = +let compile_file opts (f_in, echo) = let f_out = opts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in + (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in else - compile cur_feeder opts ~echo ~f_in ~f_out + compile opts ~echo ~f_in ~f_out -let compile_files cur_feeder opts = +let compile_files opts = let compile_list = List.rev opts.compile_list in - List.iter (compile_file cur_feeder opts) compile_list + List.iter (compile_file opts) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -414,7 +392,8 @@ let init_toplevel custom_init arglist = CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in + let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in + Lib.init(); (* Coq's init process, phase 2: @@ -485,20 +464,16 @@ let init_toplevel custom_init arglist = let require_libs = require_libs opts in let stm_options = opts.stm_flags in let open Vernac.State in - Feedback.del_feeder !init_feeder; - let doc_feeder = Feedback.add_feeder coqtop_doc_feed in - let doc, sid = - Stm.(new_doc - { doc_type = Interactive opts.toplevel_name; - iload_path; require_libs; stm_options; - }) in - Feedback.del_feeder doc_feeder; - init_feeder := Feedback.add_feeder coqtop_init_feed; + let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) + Stm.new_doc + Stm.{ doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + } in let state = { doc; sid; proof = None; time = opts.time } in - Some (load_init_vernaculars init_feeder opts ~state), opts + Some (load_init_vernaculars opts ~state), opts (* Non interactive: we perform a sequence of compilation steps *) end else begin - compile_files init_feeder opts; + compile_files opts; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) do_vio opts; @@ -510,7 +485,7 @@ let init_toplevel custom_init arglist = flush_all(); fatal_error_exn any end in - Feedback.del_feeder !init_feeder; + Feedback.del_feeder init_feeder; res type custom_toplevel = { diff --git a/toplevel/dune b/toplevel/dune index c2f9cd662e..f51e50aaa3 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,7 +3,6 @@ (public_name coq.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) - (flags :standard -open Gramlib) (libraries num coq.stm)) ; Coqlevel provides the `Num` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8707121306..4cdc60216e 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -29,7 +29,7 @@ let axiom_into_instance = ref false let _ = let open Goptions in declare_bool_option - { optdepr = false; + { optdepr = true; optname = "automatically declare axioms whose type is a typeclass as instances"; optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; optread = (fun _ -> !axiom_into_instance); @@ -156,7 +156,7 @@ let do_assumptions kind nl l = ((sigma,env,ienv),((is_coe,idl),t,imps))) (sigma,env,empty_internalization_env) l in - let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in + let sigma = solve_remaining_evars all_and_fail_flags env sigma in (* The universe constraints come from the whole telescope. *) let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 472411ac3a..9c80f1d2f5 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -87,8 +87,7 @@ let interp_definition pl bl poly red_option c ctypopt = let check_definition (ce, evd, _, imps) = let env = Global.env () in - let empty_sigma = Evd.from_env env in - check_evars_are_solved env evd empty_sigma; + check_evars_are_solved env evd; ce let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a9c499b192..274c99107f 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -239,7 +239,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = end let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) = - check_evars_are_solved env evd (Evd.from_env env); + check_evars_are_solved env evd; let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index f405c4d5a9..fbfa997555 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -402,7 +402,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in + let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in diff --git a/vernac/dune b/vernac/dune index 4673251002..45b567d631 100644 --- a/vernac/dune +++ b/vernac/dune @@ -3,7 +3,6 @@ (synopsis "Coq's Vernacular Language") (public_name coq.vernac) (wrapped false) - (flags :standard -open Gramlib) (libraries tactics parsing)) (rule diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index e6803443b3..befb4d7ccf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -29,7 +29,7 @@ exception EvaluatedError of Pp.t * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3cdf81ced0..e3f6a87541 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -474,7 +474,7 @@ END { let only_starredidentrefs = - Gram.Entry.of_parser "test_only_starredidentrefs" + Pcoq.Entry.of_parser "test_only_starredidentrefs" (fun strm -> let rec aux n = match Util.stream_nth n strm with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index de020926f6..2443c5d12a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -421,7 +421,7 @@ let start_proof_com ?inference_hook kind thms hook = let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in let hook = inference_hook in - let evd = solve_remaining_evars ?hook flags env evd Evd.empty in + let evd = solve_remaining_evars ?hook flags env evd in let ids = List.map RelDecl.get_name ctx in check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 2e5e11bb09..5ab877fae2 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -58,7 +58,7 @@ let pr_registered_grammar name = | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") | Some entries -> let pr_one (Pcoq.AnyEntry e) = - str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ + str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e in prlist pr_one entries diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 4761e4bbc2..f26e0d0885 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -41,8 +41,8 @@ module Vernac_ = let command_entry_ref = ref noedit_mode let command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm) + Pcoq.Entry.of_parser "command_entry" + (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm) end diff --git a/vernac/record.ml b/vernac/record.ml index ac84003266..7bdf6a973f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -160,7 +160,7 @@ let typecheck_params_and_fields finite def poly pl ps records = in let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in let fold sigma (typ, sort) (_, newfs) = let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index f842ca5ead..4bf76dae51 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -335,6 +335,20 @@ type execution_phase = | LoadingRcFile | InteractiveLoop +let default_phase = ref InteractiveLoop + +let in_phase ~phase f x = + let op = !default_phase in + default_phase := phase; + try + let res = f x in + default_phase := op; + res + with exn -> + let iexn = Backtrace.add_backtrace exn in + default_phase := op; + Util.iraise iexn + let pr_loc loc = let fname = loc.Loc.fname in match fname with @@ -347,8 +361,8 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":") -let pr_phase ?loc phase = - match phase, loc with +let pr_phase ?loc () = + match !default_phase, loc with | LoadingRcFile, loc -> (* For when all errors go through feedback: str "While loading rcfile:" ++ @@ -363,10 +377,10 @@ let pr_phase ?loc phase = (* Note: interactive messages such as "foo is defined" are not located *) None -let print_err_exn phase any = +let print_err_exn any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let pre_hdr = pr_phase ?loc phase in + let pre_hdr = pr_phase ?loc () in let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ?pre_hdr Feedback.Error msg diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 73dcb0064b..0ddf474970 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -61,9 +61,11 @@ type execution_phase = | LoadingRcFile | InteractiveLoop +val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b + val pr_loc : Loc.t -> Pp.t -val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option -val print_err_exn : execution_phase -> exn -> unit +val pr_phase : ?loc:Loc.t -> unit -> Pp.t option +val print_err_exn : exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 3a321ecdb4..35f26cab4d 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -190,7 +190,7 @@ let vernac_extend ~command ?classifier ?entry ext = | None -> let e = match entry with | None -> "COMMAND" - | Some e -> Pcoq.Gram.Entry.name e + | Some e -> Pcoq.Entry.name e in let msg = Printf.sprintf "\ Vernac entry \"%s\" misses a classifier. \ |