diff options
196 files changed, 3305 insertions, 803 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 5be434c8b7..d9136ee24b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,11 +6,23 @@ /.github/ @maximedenes # Secondary maintainer @Zimmi48 +########## Build system ########## + +/Makefile* @gares + +/configure* @ejgallego + +/META.coq.in @ejgallego + +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests @@ -21,8 +33,7 @@ /dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer -/default.nix @Zimmi48 -# Secondary maintainer @vbgl +*.nix @coq/nix-maintainers ########## Documentation ########## @@ -43,6 +54,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -256,6 +268,16 @@ /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 @@ -292,25 +314,6 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes -########## Build system ########## - -/Makefile* @gares - -/configure* @ejgallego - -/META.coq.in @ejgallego - -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes - -# This file belongs to CI -/Makefile.ci @ejgallego -# Secondary maintainer @SkySkimmer - -# This file belongs to the doc -/Makefile.doc @maximedenes -# Secondary maintainer @silene - ########## Test suite ########## /test-suite/Makefile @gares diff --git a/.gitignore b/.gitignore index 0e41d6a778..8fc3c802ad 100644 --- a/.gitignore +++ b/.gitignore @@ -183,3 +183,10 @@ plugins/ssr/ssrvernac.ml # ocaml dev files .merlin META.coq + +# Files automatically generated by Dune. +plugins/*/dune +theories/*/dune +theories/*/*/dune +theories/*/*/*/dune +*.install diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f42d13e4c1..693a0b6bf0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -88,12 +88,25 @@ after_script: - set +e +.dune-template: &dune-template + dependencies: [] + stage: build + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build/ + expire_in: 1 week + script: + - set -e + - make -f Makefile.dune "$DUNE_TARGET" + - set +e + # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that # purpose, we add a spurious dependency `not-a-real-job` that must be # overridden otherwise the CI will fail. -.doc-templare: &doc-template +.doc-template: &doc-template stage: test dependencies: - not-a-real-job @@ -203,6 +216,12 @@ build:edge+flambda: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" +build:egde:dune:dev: + <<: *dune-template + variables: + OPAM_SWITCH: edge + DUNE_TARGET: world + windows64: <<: *windows-template variables: @@ -215,6 +234,12 @@ windows32: except: - /^pr-.*$/ +pkg:dune-release: + <<: *dune-template + stage: test + variables: + OPAM_SWITCH: edge + DUNE_TARGET: release pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git @@ -245,11 +270,23 @@ pkg:nix: paths: - nix-build-coq.drv-0/*/test-suite/logs -documentation: +doc:refman: <<: *doc-template dependencies: - build:base +doc:ml-api: + stage: test + dependencies: + - build:edge + script: + - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" + - make mli-doc source-doc # ml-doc [broken in 4.07.0] + artifacts: + name: "$CI_JOB_NAME" + paths: + - dev/ocamldoc + test-suite:base: <<: *test-suite-template dependencies: diff --git a/.ocamlinit b/.ocamlinit new file mode 100644 index 0000000000..3771334e12 --- /dev/null +++ b/.ocamlinit @@ -0,0 +1 @@ +#rectypes;; @@ -10,6 +10,11 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). +- New command "Declare Scope" to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is + deprecated. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -34,6 +39,10 @@ Tactics - Deprecated the Implicit Tactic family of commands. +- The default program obligation tactic uses a bounded proof search + instead of an unbounded and potentially non-terminating one now + (source of incompatibility). + - The `simple apply` tactic now respects the `Opaque` flag when called from Ltac (`auto` still does not respect it). @@ -48,6 +57,8 @@ Tactics may need to add `Require Import Lra` to your developments. For compatibility, we now define `fourier` as a deprecated alias of `lra`. +- The `romega` tactics have been deprecated; please use `lia` instead. + Focusing - Focusing bracket `{` now supports named goal selectors, @@ -65,6 +76,33 @@ Standard Library - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. +- The scopes `int_scope` and `uint_scope` have been renamed to + `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect + and other packages. They are still delimited by `%int` and `%uint`. + +- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, + and `int31` are no longer available merely by `Require`ing the files + that define the inductives. You must `Import` `Coq.Strings.String`, + `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and + `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use + these notations. Note that passing `-compat 8.8` or issuing + `Require Import Coq.Compat.Coq88` will make these notations + available. Users wishing to port their developments automatically + may download `fix.py` from + <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169> + and run a command like `while true; do make -Okj 2>&1 | + /path/to/fix.py; done` and get a cup of coffee. (This command must + be manually interrupted once the build finishes all the way though. + Note also that this method is not fail-proof; you may have to adjust + some scopes if you were relying on string notations not being + available even when `string_scope` was open.) + +- Numeral syntax for `nat` is no longer available without loading the + entire prelude (`Require Import Coq.Init.Prelude`). This only + impacts users running Coq without the init library (`-nois` or + `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. + Tools - Coq_makefile lets one override or extend the following variables from @@ -98,6 +136,8 @@ Vernacular Commands overwritting the opacity set of the hint database. - Added generic syntax for “attributes”, as in: `#[local] Lemma foo : bar.` +- Added the `Numeral Notation` command for registering decimal numeral + notations for custom types - The `Set SsrHave NoTCResolution` command no longer has special global scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. @@ -177,6 +177,9 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### camldevfiles: $(MERLINFILES) META.coq +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + .merlin: .merlin.in cp -a "$<" "$@" diff --git a/Makefile.build b/Makefile.build index c100eda400..0faa18b059 100644 --- a/Makefile.build +++ b/Makefile.build @@ -317,13 +317,11 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h - sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ - -e '/^}/q' $< $(TOTARGET) +kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh + kernel/byterun/make_jumptbl.sh $< $@ -kernel/copcodes.ml: kernel/byterun/coq_instruct.h - tr -d "\r" < $< | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | \ - awk -f kernel/make-opcodes $(TOTARGET) +kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes + kernel/make_opcodes.sh $< $@ %.o: %.c $(SHOW)'OCAMLC $<' diff --git a/Makefile.common b/Makefile.common index 772561bd70..09457ced7b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,13 +140,12 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo -NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo -OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ - positive_syntax_plugin.cmo n_syntax_plugin.cmo \ - z_syntax_plugin.cmo r_syntax_plugin.cmo \ +SYNTAXCMO:=$(addprefix plugins/syntax/, \ + r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ - string_syntax_plugin.cmo ) + string_syntax_plugin.cmo \ + numeral_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo @@ -156,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ $(QUOTECMO) $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ - $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ + $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) diff --git a/Makefile.doc b/Makefile.doc index 1b1198c1f2..0dcf9daf27 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -218,9 +218,11 @@ ODOCDOTOPTS=-dot -dot-reduce source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf +OCAMLDOC_CAML_FLAGS=-rectypes -I +threads $(MLINCLUDES) + $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\ + $(HIDE)$(OCAMLFIND) ocamldoc -latex $(OCAMLDOC_CAML_FLAGS) \ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' @@ -230,31 +232,31 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css ml-dot: $(MLFILES) - $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \ + $(OCAMLFIND) ocamldoc -dot -dot-reduce $(OCAMLDOC_CAML_FLAGS) \ $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot %_dep.png: %.dot $(DOT) -Tpng $< -o $@ %_types.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -dot-types -o $@ $< -OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ +OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ \ $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) %.dot: | %.mllib.d $(OCAMLDOC_MLLIBD) -ml-doc: +ml-doc: kernel/copcodes.cmi $(SHOW)'OCAMLDOC -html' $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \ $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \ -t "Coq mls documentation" \ -css-style ../style.css @@ -269,7 +271,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(OCAMLDOC_MLLIBD) %.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ $< $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(SHOW)'PDFLATEX $*.tex' diff --git a/Makefile.dune b/Makefile.dune new file mode 100644 index 0000000000..f90f555557 --- /dev/null +++ b/Makefile.dune @@ -0,0 +1,43 @@ +# -*- mode: makefile -*- +# Dune Makefile for Coq + +.PHONY: help voboot states world apidoc + +# use DUNEOPT=--display=short for a more verbose build +# DUNEOPT=--display=short + +BUILD_CONTEXT=_build/default + +help: + @echo "Welcome to Coq's Dune-based build system. Targets are:" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - release: build Coq in release mode" + @echo " - clean: remove build directory and autogenerated files" + @echo " - help: show this message" + +voboot: + dune build $(DUNEOPT) @vodeps + dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d + +states: voboot + dune build $(DUNEOPT) theories/Init/Prelude.vo + +world: voboot + dune build $(DUNEOPT) @install + +release: voboot + dune build $(DUNEOPT) -p coq + +clean: + dune clean + +# Other common dev targets +# +# dune build coq.install +# dune build ide/coqide.install + +# Packaging / OPAM targets: +# +# dune -p coq @install +# dune -p coqide @install diff --git a/checker/dune b/checker/dune new file mode 100644 index 0000000000..d918f853dd --- /dev/null +++ b/checker/dune @@ -0,0 +1,26 @@ +(rule (copy %{project_root}/kernel/names.ml names.ml)) +(rule (copy %{project_root}/kernel/names.mli names.mli)) +(rule (copy %{project_root}/kernel/esubst.ml esubst.ml)) +(rule (copy %{project_root}/kernel/esubst.mli esubst.mli)) + +(library + (name checker) + (public_name coq.checker) + (synopsis "Coq's Standalone Proof Checker") + (modules values analyze names esubst) + (wrapped false) + (libraries coq.lib)) + +(executable + (name main) + (public_name coqchk) + (modules :standard \ votour values analyze names esubst) + (modules_without_implementation cic) + (libraries coq.checker)) + +(executable + (name votour) + (public_name votour) + (modules votour) + (libraries coq.checker)) + diff --git a/clib/cList.mli b/clib/cList.mli index ed468cb977..39d9a5e535 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -289,8 +289,8 @@ sig val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list (** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is - [l1'@l] and [l2] is [l2'@l] and [l] is maximal amongst all such - decompositions*) + [l1'\@l] and [l2] is [l2'\@l] and [l] is maximal amongst all such + decompositions *) (** {6 Association lists} *) diff --git a/clib/dune b/clib/dune new file mode 100644 index 0000000000..689a955ab7 --- /dev/null +++ b/clib/dune @@ -0,0 +1,8 @@ +(library + (name clib) + (synopsis "Coq's Utility Library [general purpose]") + (public_name coq.clib) + (wrapped false) + (modules_without_implementation cSig) + (libraries threads str unix dynlink)) + diff --git a/config/dune b/config/dune new file mode 100644 index 0000000000..30faf1233e --- /dev/null +++ b/config/dune @@ -0,0 +1,13 @@ +(library + (name config) + (synopsis "Coq Configuration Variables") + (public_name coq.config) + (wrapped false)) + +; Dune doesn't use configure's output, but it is still necessary for +; some Coq files to work; will be fixed in the future. +(rule + (targets coq_config.ml) + (mode fallback) + (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run) + (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes)))) diff --git a/coq.opam b/coq.opam new file mode 100644 index 0000000000..7f577dd8be --- /dev/null +++ b/coq.opam @@ -0,0 +1,22 @@ +opam-version: "1.2" +maintainer: "The Coq development team <coqdev@inria.fr>" +authors: "The Coq development team, INRIA, CNRS, and contributors." +homepage: "https://coq.inria.fr/" +bug-reports: "https://github.com/coq/coq/issues" +dev-repo: "https://github.com/coq/coq.git" +license: "LGPL-2.1" + +available: [ ocaml-version >= "4.02.3" ] + +depends: [ + "dune" { build } + "ocamlfind" { build } + "num" + "camlp5" +] + +build: [ + [ "dune" "build" "@vodeps" ] + [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] + [ "dune" "build" "-p" package "-j" jobs ] +] diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 39b4d2ab34..181c43615b 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -81,6 +81,7 @@ type grammar_ext = { type tactic_ext = { tacext_name : string; tacext_level : int option; + tacext_deprecated : code option; tacext_rules : tactic_rule list; } diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 6c6562c204..bfa4e2b57b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -95,6 +95,7 @@ rule extend = parse | "END" { END } | "DECLARE" { DECLARE } | "PLUGIN" { PLUGIN } +| "DEPRECATED" { DEPRECATED } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index fd425ef4ff..a8ed95f5ba 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -181,7 +181,7 @@ let print_fun fmt (vars, body) = in let () = fprintf fmt "fun@ " in let () = List.iter iter vars in - (** FIXME: use Coq locations in the macros *) + (* FIXME: use Coq locations in the macros *) let () = fprintf fmt "loc ->@ @[%s@]" body.code in () @@ -316,10 +316,17 @@ let print_rules fmt rules = fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules let print_ast fmt ext = + let deprecation fmt = + function + | None -> () + | Some { code } -> fprintf fmt "~deprecation:(%s) " code + in let pr fmt () = let level = match ext.tacext_level with None -> 0 | Some i -> i in - fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" - plugin_name ext.tacext_name level print_rules ext.tacext_rules + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a%a" + plugin_name ext.tacext_name level + deprecation ext.tacext_deprecated + print_rules ext.tacext_rules in let () = fprintf fmt "let () = @[%a@]\n" pr () in () diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index baafd633c4..bf435fd247 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -62,7 +62,7 @@ let parse_user_entry s sep = %token <string> IDENT QUALID %token <string> STRING %token <int> INT -%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -108,8 +108,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_level tactic_rules END - { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +| TACTIC EXTEND IDENT tactic_deprecated tactic_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_deprecated = $4; tacext_level = $5; tacext_rules = $6 } } +; + +tactic_deprecated: +| { None } +| DEPRECATED CODE { Some $2 } ; tactic_level: diff --git a/coqpp/dune b/coqpp/dune new file mode 100644 index 0000000000..24b9b9184b --- /dev/null +++ b/coqpp/dune @@ -0,0 +1,8 @@ +(ocamllex coqpp_lex) +(ocamlyacc coqpp_parse) + +(executable + (name coqpp_main) + (public_name coqpp) + (modules coqpp_ast coqpp_lex coqpp_parse coqpp_main) + (modules_without_implementation coqpp_ast)) diff --git a/default.nix b/default.nix index d9317bccaf..6f759f41d1 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz"; - sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j"; + url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; + sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,6 +38,18 @@ with pkgs; with stdenv.lib; +let dune = + overrideDerivation jbuilder (o: { + name = "dune-1.1.1"; + src = fetchFromGitHub { + owner = "ocaml"; + repo = "dune"; + rev = "1.1.1"; + sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; + }; + }); +in + stdenv.mkDerivation rec { name = "coq"; @@ -45,6 +57,7 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python2 time # coq-makefile timing tools + dune ] ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) ++ optional buildIde ocamlPackages.lablgtk @@ -62,8 +75,8 @@ stdenv.mkDerivation rec { ++ [ ocamlPackages.ounit rsync which ] ) ++ optionals shell ( - [ jq curl git gnupg ] # Dependencies of the merging script - ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools + [ jq curl gitFull gnupg ] # Dependencies of the merging script + ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools ); src = @@ -71,7 +84,7 @@ stdenv.mkDerivation rec { else with builtins; filterSource (path: _: - !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.; + !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; prefixKey = "-prefix "; diff --git a/dev/ci/README.md b/dev/ci/README.md index a814e4914e..95892ebe0a 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -136,12 +136,38 @@ 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 can also be downloaded from the GitLab repository. -Currently, available artifacts are: +### 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. -- the Coq documentation, built in the `documentation` job. When submitting - a documentation PR, this can help reviewers checking the rendered result. + 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 + +- 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=doc:refman + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api ### GitLab and Windows @@ -168,6 +194,6 @@ but if you wish to save more time you can skip the job by setting 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.. +it through the web interface. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index d22b9c8f7c..1a9a26843c 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -14,6 +14,6 @@ else COQLIB="$COQBIN/../" fi -( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install ) +( 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/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index abba13428f..b0a2b04121 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -1,5 +1,3 @@ - - HISTORY: ------- @@ -35,13 +33,41 @@ HISTORY: grammar.cma (and q_constr.cmo) directly, no need for a separate subcall to make nor awkward include-failed-and-retry. - ---------------------------------------------------------------------------- +* February - September 2018 (Emilio Jesús Gallego Arias) + + Dune support added. + + The build setup is mostly vanilla for the OCaml part, however the + `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper + that will generate the necessary `dune` files. + + As a developer, you should not have to deal with Dune configuration + files on a regular basis unless adding a new library or plugin. + The vanilla setup declares all the Coq libraries and binaries [we + must respect proper containment/module implementation rules as to + allow packing], and we build custom preprocessors (based on `camlp5` + and `coqpp`) that will process the `ml4`/`mlg` files. + + This suffices to build `coqtop` and `coqide`, all that remains to + handle is `.vo` compilation. + + To teach Dune about the `.vo`, we use a small utility `coq_dune`, + that will generate a `dune` file for each directory in `plugins` and + `theories`. The code is pretty straightforward and declares build + and install rules for each `.v` straight out of `coqdep`. Thus, our + build strategy looks like this: + + 1. Use `dune` to build `coqdep` and `coq_dune`. + 2. Use `coq_dune` to generate `dune` files for each directory with `.v` files. + 3. ? + 4. Profit! [Seriously, at this point Dune has all the information to build Coq] + +--------------------------------------------------------------------------- -This file documents internals of the implementation of the build -system. For what a Coq developer needs to know about the build system, -see build-system.txt . +This file documents internals of the implementation of the make-based +build system. For what a Coq developer needs to know about the build +system, see build-system.txt and build-system.dune.md . .ml4 files ---------- diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md new file mode 100644 index 0000000000..85aaf317ef --- /dev/null +++ b/dev/doc/build-system.dune.md @@ -0,0 +1,103 @@ +This file documents what a Coq developer needs to know about the +Dune-based build system. If you want to enhance the build system +itself (or are curious about its implementation details), see +build-system.dev.txt, and in particular its initial HISTORY section. + +Dune +==== + +Coq can now be built using +[Dune](https://github.com/ocaml/dune). Contrary to other systems, +Dune, doesn't use a global`makefile` but local build files named +`dune` that are later composed to form a global build. + +As a developer, Dune should take care of all OCaml-related build tasks +including library management, merlin files, and link order. You are +are not supposed to modify the `dune` files unless you are adding a +new binary, library, or plugin. + +The current Dune setup also doesn't require a call to `configure`. The +auto-generated configuration files are properly included in the +dependency graph so it will be automatically generated by Dune with +reasonable developer defaults. You can still override the defaults by +manually calling `./configure`, but note that some configure options +such as install paths are not used by Dune. + +Dune uses a separate directory `_build` to store build artifacts; it +will generate an `.install` file so artifacts in the build can be +properly installed by package managers. + +## Targets + +The default dune target is `dune build` (or `dune build @install`), +which will scan all sources in the Coq tree and then build the whole +project, creating an "install" overlay in `_build/install/default`. + +You can build some other target by doing `dune build $TARGET`. + +In order to build a single package, you can do `dune build +$PACKAGE.install`. Dune also provides targets for documentation and +testing, see below. + +## Developer shell + +You can create a developer shell with `dune utop $library`, where +`$library` can be any directory in the current workspace. For example, +`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with +the right libraries already loaded. + +Note that you must invoke the `#rectypes;;` toplevel flag in order to +use Coq libraries. The provided `.ocamlinit` file does this +automatically. + +## Compositionality, developer and release modes. + +By default [in "developer mode"], Dune will compose all the packages +present in the tree and perform a global build. That means that for +example you could drop the `ltac2` folder under `plugins` and get a +build using `ltac2`, that will use the current Coq version. + +This is very useful to develop plugins and Coq libraries as your +plugin will correctly track dependencies and rebuild incrementally as +needed. + +However, it is not always desirable to go this way. For example, the +current Coq source tree contains two packages [Coq and CoqIDE], and in +the OPAM CoqIDE package we don't want to build CoqIDE against the +local copy of Coq. For this purpose, Dune supports the `-p` option, so +`dune build -p coqide` will build CoqIDE against the system-installed +version of Coq libs. + +## Stanzas + +`dune` files contain the so-called "stanzas", that may declare: + +- libraries, +- executables, +- documentation, arbitrary blobs. + +The concrete options for each stanza can be seen in the Dune manual, +but usually the default setup will work well with the current Coq +sources. Note that declaring a library or an executable won't make it +installed by default, for that, you need to provide a "public name". + +## Workspaces and Profiles + +Dune provides support for tree workspaces so the developer can set +global options --- such as flags --- on all packages, or build Coq +with different OPAM switches simultaneously [for example to test +compatibility]; for more information, please refer to the Dune manual. + +## Documentation and test targets + +The documentation and test suite targets for Coq are still not +implemented in Dune. + +## Planned and Advanced features + +Dune supports or will support extra functionality that may result very +useful to Coq, some examples are: + +- Cross-compilation. +- Automatic Generation of OPAM files. +- Multi-directory libraries. diff --git a/doc/README.md b/doc/README.md index 3e70bc443d..47507de52d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -10,7 +10,7 @@ The documentation of the latest released version is available on the Coq web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). Additionally, you can view the documentation for the current master version at -<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. +<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman>. The reference manual is written is reStructuredText and compiled using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst) diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index f7fd4b9146..e507a224c6 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -407,12 +407,11 @@ length, by writing .. coqtop:: in - Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c0c4539564..23cbd76eda 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -325,6 +325,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1e92d01125..f7a431ef29 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,7 +26,9 @@ Description of ``omega`` .. tacv:: romega :name: romega - To be documented. + .. deprecated:: 8.9 + + Use :tacn:`lia` instead. Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 241cdf5eea..62a482096c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1345,8 +1345,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( Value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( Type of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5089a1b3e3..4c0e85bdd4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See :ref:`above <NotationSyntax>` for the syntax of notations including the -possibility to declare them in a given scope. Here is a typical example which -declares the notation for conjunction in the scope ``type_scope``. +.. cmd:: Declare Scope @scope + + This adds a new scope named :n:`@scope`. Note that the initial + state of Coq declares by default the following interpretation scopes: + ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, + ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. + +The syntax to associate a notation to a scope is given +:ref:`above <NotationSyntax>`. Here is a typical example which declares the +notation for conjunction in the scope ``type_scope``. .. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. .. note:: A notation not defined in a scope is called a *lonely* - notation. + notation. No example of lonely notations can be found in the + initial state of Coq though. + Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely interpretations and opening of scopes matters, and not the declaration of interpretations within a scope). -The initial state of Coq declares three interpretation scopes and no -lonely notations. These scopes, in opening order, are ``core_scope``, -``type_scope`` and ``nat_scope``. - .. cmd:: Open Scope @scope The command to add a scope to the interpretation scope stack is @@ -1372,6 +1377,154 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + +Numeral notations +----------------- + +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type. + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: Unexpected term @term while parsing a numeral notation. + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term @term while parsing a numeral notation. + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. + .. _TacticNotation: Tactic Notations diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f448248468..0fa42cadad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v @@ -0,0 +1,11 @@ +(rule + (targets .vfiles.d) + (deps + (source_tree theories) + (source_tree plugins)) + (action (with-stdout-to .vfiles.d (system "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`")))) + +(alias + (name vodeps) + (deps tools/coq_dune.exe .vfiles.d)) + ; (action (run coq_dune .vfiles.d)))) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000000..6ce4ec4717 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 1.1) + +(name coq-devel) diff --git a/dune-workspace b/dune-workspace new file mode 100644 index 0000000000..682631e7dc --- /dev/null +++ b/dune-workspace @@ -0,0 +1,6 @@ +(lang dune 1.1) + +; Add custom flags here. Default developer profile is `dev` +(env + (dev (flags :standard -rectypes -w -9-27-50)) + (release (flags :standard -rectypes))) diff --git a/engine/dune b/engine/dune new file mode 100644 index 0000000000..e2b7ab9c87 --- /dev/null +++ b/engine/dune @@ -0,0 +1,6 @@ +(library + (name engine) + (synopsis "Coq's Tactic Engine") + (public_name coq.engine) + (wrapped false) + (libraries library)) diff --git a/engine/proofview.mli b/engine/proofview.mli index 970bf67732..a9666e4f90 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -532,7 +532,7 @@ module Goal : sig (** Compatibility: avoid if possible *) val goal : t -> Evar.t - val print : t -> Goal.goal Evd.sigma + val print : t -> Evar.t Evd.sigma end diff --git a/grammar/dune b/grammar/dune new file mode 100644 index 0000000000..90847e7fb6 --- /dev/null +++ b/grammar/dune @@ -0,0 +1,41 @@ +(library + (name grammar) + (synopsis "Coq Camlp5 Grammar Extensions for Plugins") + (public_name coq.grammar) + (wrapped false) + (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:grammar.cmxa} -o coqp5))) + +(install + (section bin) + (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/tacextend.mlp b/grammar/tacextend.mlp index 07239e7af0..5943600b7c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -8,6 +8,8 @@ (* * (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 diff --git a/ide/coqide.opam b/ide/coqide.opam new file mode 100644 index 0000000000..1b46efdee2 --- /dev/null +++ b/ide/coqide.opam @@ -0,0 +1,19 @@ +opam-version: "1.2" +maintainer: "The Coq development team <coqdev@inria.fr>" +authors: "The Coq development team, INRIA, CNRS, and contributors." +homepage: "https://coq.inria.fr/" +bug-reports: "https://github.com/coq/coq/issues" +dev-repo: "https://github.com/coq/coq.git" +license: "LGPL-2.1" + +available: [ocaml-version >= "4.02.3"] + +depends: [ + "dune" { build } + "ocamlfind" { build } + "num" + "camlp5" + "coq" +] + +build: [ [ "dune" "build" "-p" package "-j" jobs ] ] diff --git a/ide/dune b/ide/dune new file mode 100644 index 0000000000..bceb981ed0 --- /dev/null +++ b/ide/dune @@ -0,0 +1,21 @@ +(executable + (name idetop) + (public_name coqidetop.opt) + (package coqide) + (modules idetop) + (libraries coq.toplevel coqide.protocol) + (link_flags -linkall)) + +(rule + (targets coqide_main.ml) + (deps (:ml4-file coqide_main.ml4)) + (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + +(executable + (name coqide_main) + (public_name coqide) + (package coqide) + (modules (:standard \ idetop)) + (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol)) + +(ocamllex utf8_convert config_lexer coq_lex) diff --git a/ide/dune-project b/ide/dune-project new file mode 100644 index 0000000000..948dc59000 --- /dev/null +++ b/ide/dune-project @@ -0,0 +1,3 @@ +(lang dune 1.0) + +(name coqide-devel) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 960beb8455..7044263b94 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -71,15 +71,15 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let rmark = `MARK (buf#create_mark buf#start_iter) in (* insert the string, but don't apply diff highlights to white space at the begin/end of line *) let rec insert_str tags s = + let etags = try List.hd !dtags :: tags with hd -> tags in try - let _ = Str.search_forward nl_white_regex s 0 in + let start = Str.search_forward nl_white_regex s 0 in + insert_with_tags buf mark rmark etags (String.sub s 0 start); insert_with_tags buf mark rmark tags (Str.matched_group 1 s); let mend = Str.match_end () in insert_str tags (String.sub s mend (String.length s - mend)) - with Not_found -> begin - let etags = try List.hd !dtags :: tags with hd -> tags in + with Not_found -> insert_with_tags buf mark rmark etags s - end in let rec insert tags = function | PCData s -> insert_str tags s @@ -328,15 +328,18 @@ let coqtop_path () = | None -> try let new_prog = System.get_toplevel_path "coqidetop" in - if Sys.file_exists new_prog then new_prog + (* The file exists or it is to be found by path *) + if Sys.file_exists new_prog || + CString.equal Filename.(basename new_prog) new_prog + then new_prog else let in_macos_bundle = Filename.concat (Filename.dirname new_prog) (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle - else "coqidetop" - with Not_found -> "coqidetop" + else "coqidetop.opt" + with Not_found -> "coqidetop.opt" in file (* In win32, when a command-line is to be executed via cmd.exe diff --git a/ide/protocol/dune b/ide/protocol/dune new file mode 100644 index 0000000000..9ce4559940 --- /dev/null +++ b/ide/protocol/dune @@ -0,0 +1,7 @@ +(library + (name protocol) + (public_name coqide.protocol) + (wrapped false) + (libraries coq.lib)) + +(ocamllex xml_lexer) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 009894fddb..ddc0a5c000 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -531,18 +531,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - let (sc,p) = uninterp_prim_token_ind_pattern ind args in - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> - match availability_of_prim_token p sc scopes with - | None -> raise No_match - | Some key -> - insert_pat_coercion coercion (insert_pat_delimiters (CAst.make @@ CPatPrim p) key) - with No_match -> - try - if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes vars ind args + extern_notation_ind_pattern allscopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in diff --git a/interp/dune b/interp/dune new file mode 100644 index 0000000000..e9ef7ba99a --- /dev/null +++ b/interp/dune @@ -0,0 +1,6 @@ +(library + (name interp) + (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") + (public_name coq.interp) + (wrapped false) + (libraries pretyping)) diff --git a/interp/notation.ml b/interp/notation.ml index 625d072b9f..6b26f66100 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -98,21 +98,40 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) +let warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") + let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope -let check_scope sc = let _ = find_scope sc in () +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () + +let ensure_scope scope = check_scope ~tolerant:true scope + +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -266,16 +285,14 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) - let glob_prim_constr_key c = match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) + | GRef (ref, _) -> Some (canonical_gr ref) | GApp (c, _) -> begin match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) - | _ -> Oth + | GRef (ref, _) -> Some (canonical_gr ref) + | _ -> None end - | _ -> Oth + | _ -> None let glob_constr_keys c = match DAst.get c with | GApp (c, _) -> @@ -303,77 +320,189 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +type prim_token_uid = string -type cases_pattern_status = bool (* true = use prim token in patterns *) +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) +module InnerPrimToken = struct -let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + type interpreter = + | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | StringInterp of (?loc:Loc.t -> string -> glob_constr) -let add_prim_token_interpreter sc interp = - try - let cont = Hashtbl.find prim_token_interpreter_tab sc in - Hashtbl.replace prim_token_interpreter_tab sc (interp cont) - with Not_found -> - let cont = (fun ?loc _p -> raise Not_found) in - Hashtbl.add prim_token_interpreter_tab sc (interp cont) + let interp_eq f f' = match f,f' with + | RawNumInterp f, RawNumInterp f' -> f == f' + | BigNumInterp f, BigNumInterp f' -> f == f' + | StringInterp f, StringInterp f' -> f == f' + | _ -> false -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = - declare_scope sc; - add_prim_token_interpreter sc interp; - List.iter (fun pat -> - prim_token_key_table := KeyMap.add - (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) - patl + let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) -let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) - else Numeral (Bigint.to_string (Bigint.neg n), false) + let do_interp ?loc interp primtok = + match primtok, interp with + | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s) + | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s) + | String s, StringInterp interp -> interp ?loc s + | _ -> raise Not_found -let ofNumeral n s = - if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + type uninterpreter = + | RawNumUninterp of (any_glob_constr -> rawnum option) + | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | StringUninterp of (any_glob_constr -> string option) -let mkString = function -| None -> None -| Some s -> if Unicode.is_utf8 s then Some (String s) else None + let uninterp_eq f f' = match f,f' with + | RawNumUninterp f, RawNumUninterp f' -> f == f' + | BigNumUninterp f, BigNumUninterp f' -> f == f' + | StringUninterp f, StringUninterp f' -> f == f' + | _ -> false -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) + let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + let mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None + + let do_uninterp uninterp g = match uninterp with + | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g) + | BigNumUninterp u -> Option.map mkNumeral (u g) + | StringUninterp u -> mkString (u g) + +end + +(* The following two tables of (un)interpreters will *not* be synchronized. + But their indexes will be checked to be unique *) +let prim_token_interpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) + +let prim_token_uninterpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) + +(* Table from scope_name to backtrack-able informations about interpreters + (in particular interpreter unique id). *) +let prim_token_interp_infos = + ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t) + +(* Table from global_reference to backtrack-able informations about + prim_token uninterpretation (in particular uninterpreter unique id). *) +let prim_token_uninterp_infos = + ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) + +let hashtbl_check_and_set allow_overwrite uid f h eq = + match Hashtbl.find h uid with + | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f + | g when eq f g -> () + | _ -> + user_err ~hdr:"prim_token_interpreter" + (str "Unique identifier " ++ str uid ++ + str " already used to register a numeral or string (un)interpreter.") + +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = + hashtbl_check_and_set + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; + hashtbl_check_and_set + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) + +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) + +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +let cache_prim_token_interpretation (_,infos) = + let sc = infos.pt_scope in + let uid = infos.pt_uid in + check_scope ~tolerant:true sc; + prim_token_interp_infos := + String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; + List.iter (fun r -> prim_token_uninterp_infos := + Refmap.add r (sc,uid,infos.pt_in_match) + !prim_token_uninterp_infos) + infos.pt_refs + +let subst_prim_token_interpretation (subs,infos) = + { infos with + pt_refs = List.map (subst_global_reference subs) infos.pt_refs } + +let classify_prim_token_interpretation infos = + if infos.pt_local then Dispose else Substitute infos + +let inPrimTokenInterp : prim_token_infos -> obj = + declare_object {(default_object "PRIM-TOKEN-INTERP") with + open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + cache_function = cache_prim_token_interpretation; + subst_function = subst_prim_token_interpretation; + classify_function = classify_prim_token_interpretation} + +let enable_prim_token_interpretation infos = + Lib.add_anonymous_leaf (inPrimTokenInterp infos) + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) + +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + +let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_uid = uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } +let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_uid = uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } -let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> match uninterp r with - | None -> None - | Some (n,s) -> Some (Numeral (n,s))), inpat) - -let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = - let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) - -let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p) - (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err ?loc ~hdr:"prim_token_interpreter" - (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + match d with + | [] -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.") + | _ -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -476,9 +605,10 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let pat = interp () in + let interp = Hashtbl.find prim_token_interpreters uid in + let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -649,43 +779,34 @@ let entry_has_ident = function try String.Map.find s !entry_has_ident_map <= n with Not_found -> false let uninterp_prim_token c = - try - let (sc,numpr,_) = - KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match - -let uninterp_prim_token_ind_pattern ind args = - let ref = IndRef ind in - try - let k = RefKey (canonical_gr ref) in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let args' = List.map - (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = DAst.make @@ GRef (ref,None) in - match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + try + let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in + let uninterp = Hashtbl.find prim_token_uninterpreters uid in + match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with + | None -> raise Notation_ops.No_match + | Some n -> (sc,n) + with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - try - let k = cases_pattern_key c in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let na,c = glob_constr_of_closed_cases_pattern c in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (na,sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_constr_of_closed_cases_pattern c with + | exception Not_found -> raise Notation_ops.No_match + | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true - with Not_found -> false in + try + let uid = snd (String.Map.find scope !prim_token_interp_infos) in + let interp = Hashtbl.find prim_token_interpreters uid in + let open InnerPrimToken in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false + with Not_found -> false + in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) @@ -1206,16 +1327,19 @@ let pr_visibility prglob = function let freeze _ = (!scope_map, !scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, + !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,asc,dlm,fkm,clsc,coe,globs,ids) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; scope_class_map := clsc; + prim_token_interp_infos := ptii; + prim_token_uninterp_infos := ptui; entry_coercion_map := coe; entry_has_global_map := globs; entry_has_ident_map := ids @@ -1224,7 +1348,9 @@ let init () = init_scope_map (); delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - scope_class_map := initial_scope_class_map + scope_class_map := initial_scope_class_map; + prim_token_interp_infos := String.Map.empty; + prim_token_uninterp_infos := Refmap.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index c921606484..6e59c0fd70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Bigint open Names open Libnames open Constrexpr @@ -42,6 +41,9 @@ type scopes (** = [scope_name list] *) val declare_scope : scope_name -> unit +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit + val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in @@ -75,24 +77,62 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type cases_pattern_status = bool (** true = use prim token in patterns *) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +(** The unique id string below will be used to refer to a particular + registered interpreter/uninterpreter of numeral or string notation. + Using the same uid for different (un)interpreters will fail. + If at most one interpretation of prim token is used per scope, + then the scope name could be used as unique id. *) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type prim_token_uid = string -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option + +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter + +val register_rawnumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit + +val register_bignumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + +val register_string_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +(** Note: most of the time, the [pt_refs] field above will contain + inductive constructors (e.g. O and S for nat). But it could also be + injection functions such as IZR for reals. *) + +(** Activate a prim token interpretation whose unique id and functions + have already been registered. *) -val declare_rawnumeral_interpreter : scope_name -> required_module -> - rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit +val enable_prim_token_interpretation : prim_token_infos -> unit -val declare_numeral_interpreter : scope_name -> required_module -> - bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) -val declare_string_interpreter : scope_name -> required_module -> - string prim_token_interpreter -> string prim_token_uninterpreter -> unit +val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> + Bigint.bigint prim_token_interpreter -> + glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit +val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> + string prim_token_interpreter -> + glob_constr list * string prim_token_uninterpreter * bool -> unit (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) @@ -110,8 +150,6 @@ val uninterp_prim_token : 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : 'a cases_pattern_g -> Name.t * scope_name * prim_token -val uninterp_prim_token_ind_pattern : - inductive -> cases_pattern list -> scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option diff --git a/kernel/byterun/dune b/kernel/byterun/dune new file mode 100644 index 0000000000..3a714a8a59 --- /dev/null +++ b/kernel/byterun/dune @@ -0,0 +1,10 @@ +(library + (name byterun) + (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") + (public_name coq.vm) + (c_names coq_fix_code coq_memory coq_values coq_interp)) + +(rule + (targets coq_jumptbl.h) + (deps (:h-file coq_instruct.h)) + (action (run ./make_jumptbl.sh %{h-file} %{targets}))) diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh new file mode 100755 index 0000000000..eacd4daac8 --- /dev/null +++ b/kernel/byterun/make_jumptbl.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2} diff --git a/kernel/dune b/kernel/dune new file mode 100644 index 0000000000..011af9c28c --- /dev/null +++ b/kernel/dune @@ -0,0 +1,15 @@ +(library + (name kernel) + (synopsis "The Coq Kernel") + (public_name coq.kernel) + (wrapped false) + (modules_without_implementation cinstr nativeinstr) + (libraries clib config lib byterun)) + +(rule + (targets copcodes.ml) + (deps (:h-file byterun/coq_instruct.h) make-opcodes) + (action (run ./make_opcodes.sh %{h-file} %{targets}))) + +(documentation + (package coq)) diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh new file mode 100755 index 0000000000..bb8aba2f07 --- /dev/null +++ b/kernel/make_opcodes.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +script_dir="$(dirname "$0")" +tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | awk -f "$script_dir"/make-opcodes > "${2}" diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000000..232c208aa6 --- /dev/null +++ b/lib/dune @@ -0,0 +1,7 @@ +(library + (name lib) + (synopsis "Coq's Utility Library [coq-specific]") + (public_name coq.lib) + (wrapped false) + (modules_without_implementation xml_datatype) + (libraries threads coq.clib coq.config)) diff --git a/lib/system.ml b/lib/system.ml index eef65a4e3d..902a4f2506 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -301,8 +301,11 @@ let with_time ~batch f x = Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e +(* We use argv.[0] as we don't want to resolve symlinks *) let get_toplevel_path top = - let dir = Filename.dirname Sys.executable_name in + let open Filename in + let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) + then "" else dirname Sys.argv.(0) ^ dir_sep in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in let eff = if Dynlink.is_native then ".opt" else ".byte" in - dir ^ Filename.dir_sep ^ top ^ eff ^ exe + dir ^ top ^ eff ^ exe diff --git a/library/dune b/library/dune new file mode 100644 index 0000000000..344fad5a75 --- /dev/null +++ b/library/dune @@ -0,0 +1,9 @@ +(library + (name library) + (synopsis "Coq's Loadable Libraries (vo) Support") + (public_name coq.library) + (wrapped false) + (libraries kernel)) + +(documentation + (package coq)) diff --git a/parsing/dune b/parsing/dune new file mode 100644 index 0000000000..b70612a52b --- /dev/null +++ b/parsing/dune @@ -0,0 +1,20 @@ +(library + (name parsing) + (public_name coq.parsing) + (wrapped false) + (libraries proofs)) + +(rule + (targets cLexer.ml) + (deps (:ml4-file cLexer.ml4)) + (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets}))) + +(rule + (targets g_prim.ml) + (deps (:mlg-file g_prim.mlg)) + (action (run coqpp %{mlg-file}))) + +(rule + (targets g_constr.ml) + (deps (:mlg-file g_constr.mlg)) + (action (run coqpp %{mlg-file}))) diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4a2..f1095fc9f1 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,13 +417,13 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega end. Hint Resolve Pos.le_max_r Pos.le_max_l. @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune new file mode 100644 index 0000000000..6a024358c3 --- /dev/null +++ b/plugins/btauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name btauto_plugin) + (public_name coq.plugins.btauto) + (synopsis "Coq's btauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune new file mode 100644 index 0000000000..2a92996d2a --- /dev/null +++ b/plugins/cc/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name cc_plugin) + (public_name coq.plugins.cc) + (synopsis "Coq's congruence closure plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune new file mode 100644 index 0000000000..ba9cd595ce --- /dev/null +++ b/plugins/derive/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name derive_plugin) + (public_name coq.plugins.derive) + (synopsis "Coq's derive plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune new file mode 100644 index 0000000000..037b0d5053 --- /dev/null +++ b/plugins/extraction/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name extraction_plugin) + (public_name coq.plugins.extraction) + (synopsis "Coq's extraction plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune new file mode 100644 index 0000000000..bcbb99d9fc --- /dev/null +++ b/plugins/firstorder/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name ground_plugin) + (public_name coq.plugins.ground) + (synopsis "Coq's first order logic solver plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune new file mode 100644 index 0000000000..8cc76f6f9e --- /dev/null +++ b/plugins/fourier/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name fourier_plugin) + (public_name coq.plugins.fourier) + (synopsis "Coq's fourier plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune new file mode 100644 index 0000000000..002eb28eea --- /dev/null +++ b/plugins/funind/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name recdef_plugin) + (public_name coq.plugins.recdef) + (synopsis "Coq's functional induction plugin") + (libraries coq.plugins.extraction)) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..38600695dc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () @@ -196,9 +199,9 @@ let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () | HypLocation (id,InHyp) -> str "in " ++ pr_id id | HypLocation (id,InHypTypeOnly) -> - str "in (Type of " ++ pr_id id ++ str ")" + str "in (type of " ++ pr_id id ++ str ")" | HypLocation (id,InHypValueOnly) -> - str "in (Value of " ++ pr_id id ++ str ")" + str "in (value of " ++ pr_id id ++ str ")" let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print @@ -217,6 +220,14 @@ let interp_place ist gl p = let subst_place subst pl = pl +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + ARGUMENT EXTEND hloc PRINTED BY pr_place INTERPRETED BY interp_place @@ -231,8 +242,14 @@ ARGUMENT EXTEND hloc | [ "in" ident(id) ] -> [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] + [ warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> + [ warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) ] +| [ "in" "(" "type" "of" ident(id) ")" ] -> + [ HypLocation ((CAst.make id),InHypTypeOnly) ] +| [ "in" "(" "value" "of" ident(id) ")" ] -> [ HypLocation ((CAst.make id),InHypValueOnly) ] END diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune new file mode 100644 index 0000000000..5611f5ba16 --- /dev/null +++ b/plugins/ltac/plugin_base.dune @@ -0,0 +1,13 @@ +(library + (name ltac_plugin) + (public_name coq.plugins.ltac) + (synopsis "Coq's LTAC tactic language") + (modules :standard \ tauto) + (libraries coq.stm)) + +(library + (name tauto_plugin) + (public_name coq.plugins.tauto) + (synopsis "Coq's tauto tactic") + (modules tauto) + (libraries coq.plugins.ltac)) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 0bb9ccb1d8..1f2c722b34 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -144,7 +144,7 @@ let add ~deprecation kn b t = mactab := KNmap.add kn entry !mactab let replace kn path t = - let (path, _, _) = KerName.repr path in + let path = KerName.modpath path in let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune new file mode 100644 index 0000000000..0ae0e6855d --- /dev/null +++ b/plugins/micromega/plugin_base.dune @@ -0,0 +1,7 @@ +(library + (name micromega_plugin) + (public_name coq.plugins.micromega) + ; be careful not to link the executable to the plugin! + (modules (:standard \ csdpcert)) + (synopsis "Coq's micromega plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune new file mode 100644 index 0000000000..9da5b39972 --- /dev/null +++ b/plugins/nsatz/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name nsatz_plugin) + (public_name coq.plugins.nsatz) + (synopsis "Coq's nsatz solver plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune new file mode 100644 index 0000000000..f512501c78 --- /dev/null +++ b/plugins/omega/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name omega_plugin) + (public_name coq.plugins.omega) + (synopsis "Coq's omega plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune new file mode 100644 index 0000000000..323906acb2 --- /dev/null +++ b/plugins/quote/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name quote_plugin) + (public_name coq.plugins.quote) + (synopsis "Coq's quote plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 51b99b9935..da86f4274d 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -8,6 +8,7 @@ *************************************************************************) Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. +Declare Scope Int_scope. Delimit Scope Int_scope with I. (** * Abstract Integers. *) @@ -716,6 +717,7 @@ Inductive term : Set := | Topp : term -> term | Tvar : N -> term. +Declare Scope romega_scope. Bind Scope romega_scope with term. Delimit Scope romega_scope with term. Arguments Tint _%I. diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg index c1ce30027e..ac4f30b1db 100644 --- a/plugins/romega/g_romega.mlg +++ b/plugins/romega/g_romega.mlg @@ -41,14 +41,22 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +let romega_depr = + Vernacinterp.mk_deprecation + ~since:(Some "8.9") + ~note:(Some "Use lia instead.") + () + } TACTIC EXTEND romega +DEPRECATED { romega_depr } | [ "romega" ] -> { romega_tactic false [] } | [ "unsafe_romega" ] -> { romega_tactic true [] } END TACTIC EXTEND romega' +DEPRECATED { romega_depr } | [ "romega" "with" ne_ident_list(l) ] -> { romega_tactic false (List.map Names.Id.to_string l) } | [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune new file mode 100644 index 0000000000..49b0e10edf --- /dev/null +++ b/plugins/romega/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name romega_plugin) + (public_name coq.plugins.romega) + (synopsis "Coq's romega plugin") + (libraries coq.plugins.omega)) diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune new file mode 100644 index 0000000000..233845ae0f --- /dev/null +++ b/plugins/rtauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name rtauto_plugin) + (public_name coq.plugins.rtauto) + (synopsis "Coq's rtauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index d9e32dbbf8..ce115f564f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -19,6 +19,7 @@ Section MakeFieldPol. (* Field elements : R *) Variable R:Type. +Declare Scope R_scope. Bind Scope R_scope with R. Delimit Scope R_scope with ring. Local Open Scope R_scope. @@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth. (* Coefficients : C *) Variable C: Type. +Declare Scope C_scope. Bind Scope C_scope with C. Delimit Scope C_scope with coef. @@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). (* Polynomial expressions : (PExpr C) *) +Declare Scope PE_scope. Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune new file mode 100644 index 0000000000..101246e28f --- /dev/null +++ b/plugins/setoid_ring/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name newring_plugin) + (public_name coq.plugins.setoid_ring) + (synopsis "Coq's setoid ring plugin") + (libraries coq.plugins.quote)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune new file mode 100644 index 0000000000..de9053f1a0 --- /dev/null +++ b/plugins/ssr/plugin_base.dune @@ -0,0 +1,6 @@ +(library + (name ssreflect_plugin) + (public_name coq.plugins.ssreflect) + (synopsis "Coq's ssreflect plugin") + (modules_without_implementation ssrast) + (libraries coq.plugins.ssrmatching)) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune new file mode 100644 index 0000000000..06f67c3774 --- /dev/null +++ b/plugins/ssrmatching/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name ssrmatching_plugin) + (public_name coq.plugins.ssrmatching) + (synopsis "Coq ssrmatching plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + (* Notation to define shortcuts for the "X in t" part of a pattern. *) Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 47a59ba631..5e36fbeb81 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -83,8 +83,18 @@ let make_ascii_string n = let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "char_scope" - (ascii_path,ascii_module) - interp_ascii_string - ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + let sc = "char_scope" in + register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_uid = sc; + pt_required = (ascii_path,ascii_module); + pt_refs = [static_glob_Ascii]; + pt_in_match = true } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 new file mode 100644 index 0000000000..ec14df3baa --- /dev/null +++ b/plugins/syntax/g_numeral.ml4 @@ -0,0 +1,37 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +DECLARE PLUGIN "numeral_notation_plugin" + +open Numeral +open Pp +open Names +open Vernacinterp +open Ltac_plugin +open Stdarg +open Pcoq.Prim + +let pr_numnot_option _ _ _ = function + | Nop -> mt () + | Warning n -> str "(warning after " ++ str n ++ str ")" + | Abstract n -> str "(abstract after " ++ str n ++ str ")" + +ARGUMENT EXTEND numnotoption + PRINTED BY pr_numnot_option +| [ ] -> [ Nop ] +| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] +| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] +END + +VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF + | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] +END diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index f10f98e23b..d3ffe936a9 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) = with Non_closed -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + (* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([DAst.make (GRef (int31_construct, None))], - uninterp_int31, - true) + +let _ = + register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = int31_scope; + pt_uid = int31_scope; + pt_required = (int31_path,int31_module); + pt_refs = [int31_construct]; + pt_in_match = true } diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml deleted file mode 100644 index 0e202be47f..0000000000 --- a/plugins/syntax/n_syntax.ml +++ /dev/null @@ -1,81 +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 Pp -open CErrors -open Names -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "n_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let n_kn = make_kn (make_dir binnums) (Id.of_string "N") -let glob_n = IndRef (n_kn,0) -let path_of_N0 = ((n_kn,0),1) -let path_of_Npos = ((n_kn,0),2) -let glob_N0 = ConstructRef path_of_N0 -let glob_Npos = ConstructRef path_of_Npos - -let n_path = make_path binnums "N" - -let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ - if not (Bigint.equal n zero) then - GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) - else - GRef(glob_N0, None) - -let error_negative ?loc = - user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") - -let n_of_int ?loc n = - if is_pos_or_zero n then n_of_binnat ?loc true n - else error_negative ?loc - -(**********************************************************************) -(* Printing N via scopes *) -(**********************************************************************) - -let bignat_of_n n = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a - | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - ) n - -let uninterp_n (AnyGlobConstr p) = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnums) - n_of_int - ([DAst.make @@ GRef (glob_N0, None); - DAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack deleted file mode 100644 index 4c56645f07..0000000000 --- a/plugins/syntax/n_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -N_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml deleted file mode 100644 index e158e0b516..0000000000 --- a/plugins/syntax/nat_syntax.ml +++ /dev/null @@ -1,85 +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) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "nat_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* This file defines the printer for natural numbers in [nat] *) - -(*i*) -open Pp -open CErrors -open Names -open Glob_term -open Bigint -open Coqlib -(*i*) - -(**********************************************************************) -(* Parsing via scopes *) -(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) - -let threshold = of_int 5000 - -let warn_large_nat = - CWarnings.create ~name:"large-nat" ~category:"numbers" - (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed).") - -let nat_of_int ?loc n = - if is_pos_or_zero n then begin - if less_than threshold n then warn_large_nat (); - let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in - let rec mk_nat acc n = - if n <> zero then - mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) - else - acc - in - mk_nat ref_O n - end - else - user_err ?loc ~hdr:"nat_of_int" - (str "Cannot interpret a negative number as a number of type nat") - -(************************************************************************) -(* Printing via scopes *) - -exception Non_closed_number - -let rec int_of_nat x = DAst.with_val (function - | GApp (r, [a]) -> - begin match DAst.get r with - | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a) - | _ -> raise Non_closed_number - end - | GRef (z,_) when GlobRef.equal z glob_O -> zero - | _ -> raise Non_closed_number - ) x - -let uninterp_nat (AnyGlobConstr p) = - try - Some (int_of_nat p) - with - Non_closed_number -> None - -(************************************************************************) -(* Declare the primitive parsers and printers *) - -let _ = - Notation.declare_numeral_interpreter "nat_scope" - (nat_path,datatypes_module_name) - nat_of_int - ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack deleted file mode 100644 index 39bdd62f47..0000000000 --- a/plugins/syntax/nat_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Nat_syntax diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml new file mode 100644 index 0000000000..fee93593d0 --- /dev/null +++ b/plugins/syntax/numeral.ml @@ -0,0 +1,478 @@ +(************************************************************************) +(* * 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 Pp +open Util +open Names +open Libnames +open Globnames +open Constrexpr +open Constrexpr_ops +open Constr + +(** * Numeral notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotANumber + +let warn_large_num = + CWarnings.create ~name:"large-number" ~category:"numbers" + (fun ty -> + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed).") + +let warn_abstract_large_num = + CWarnings.create ~name:"abstract-large-number" ~category:"numbers" + (fun (ty,f) -> + strbrk "To avoid stack overflow, large numbers in " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") + +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ + strbrk "option type.") + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: only used to decide when a + number is considered as large (see warnings above). *) + +exception Comp of int + +let rec rawnum_compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - rawnum_compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Pervasives.compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + +(***********************************************************************) + +(** ** Conversion between Coq [Decimal.int] and internal raw string *) + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) + +let digit_of_char c = + assert ('0' <= c && c <= '9'); + Char.code c - Char.code '0' + 2 + +let char_of_digit n = + assert (2<=n && n<=11); + Char.chr (n-2 + Char.code '0') + +let coquint_of_rawnum uint str = + let nil = mkConstruct (uint,1) in + let rec do_chars s i acc = + if i < 0 then acc + else + let dg = mkConstruct (uint, digit_of_char s.[i]) in + do_chars s (i-1) (mkApp(dg,[|acc|])) + in + do_chars str (String.length str - 1) nil + +let coqint_of_rawnum inds (str,sign) = + let uint = coquint_of_rawnum inds.uint str in + mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + +let rawnum_of_coquint c = + let rec of_uint_loop c buf = + match Constr.kind c with + | Construct ((_,1), _) (* Nil *) -> () + | App (c, [|a|]) -> + (match Constr.kind c with + | Construct ((_,n), _) (* D0 to D9 *) -> + let () = Buffer.add_char buf (char_of_digit n) in + of_uint_loop a buf + | _ -> raise NotANumber) + | _ -> raise NotANumber + in + let buf = Buffer.create 64 in + let () = of_uint_loop c buf in + if Int.equal (Buffer.length buf) 0 then + (* To avoid ambiguities between Nil and (D0 Nil), we choose + to not display Nil alone as "0" *) + raise NotANumber + else Buffer.contents buf + +let rawnum_of_coqint c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) + | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | _ -> raise NotANumber) + | _ -> raise NotANumber + + +(***********************************************************************) + +(** ** Conversion between Coq [Z] and internal bigint *) + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +(** First, [positive] from/to bigint *) + +let rec pos_of_bigint posty n = + match Bigint.div2_with_rest n with + | (q, false) -> + let c = mkConstruct (posty, 2) in (* xO *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) when not (Bigint.equal q Bigint.zero) -> + let c = mkConstruct (posty, 1) in (* xI *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) -> + mkConstruct (posty, 3) (* xH *) + +let rec bigint_of_pos c = match Constr.kind c with + | Construct ((_, 3), _) -> (* xH *) Bigint.one + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) + | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | n -> assert false (* no other constructor of type positive *) + end + | x -> raise NotANumber + end + | x -> raise NotANumber + +(** Now, [Z] from/to bigint *) + +let z_of_bigint { z_ty; pos_ty } n = + if Bigint.equal n Bigint.zero then + mkConstruct (z_ty, 1) (* Z0 *) + else + let (s, n) = + if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) + else (3, Bigint.neg n) (* Zneg *) + in + let c = mkConstruct (z_ty, s) in + mkApp (c, [| pos_of_bigint pos_ty n |]) + +let bigint_of_z z = match Constr.kind z with + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 2 -> (* Zpos *) bigint_of_pos d + | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | n -> assert false (* no other constructor of type Z *) + end + | _ -> raise NotANumber + end + | _ -> raise NotANumber + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotANumber + +let rec glob_of_constr ?loc c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc c in + let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (strbrk "Unexpected term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (strbrk "Unexpected non-option term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotANumber + +let big2raw n = + if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) + else (Bigint.to_string (Bigint.neg n), false) + +let raw2big (n,s) = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +let interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + warn_large_num o.num_ty + | _ -> () + end; + let c = match fst o.to_kind with + | Int int_ty -> coqint_of_rawnum int_ty n + | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + warn_abstract_large_num (o.num_ty,o.to_ty); + glob_of_constr ?loc (mkApp (to_ty,[|c|])) + | _ -> + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc res + | Option -> interp_option o.num_ty ?loc res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + match fst o.of_kind with + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) + +(* Here we only register the interp and uninterp functions + for a particular Numeral Notation (determined by a unique + string). The actual activation of the notation will be done + later (cf. Notation.enable_prim_token_interpretation). + This registration of interp/uninterp must be added in the + libstack, otherwise this won't work through a Require. *) + +let load_numeral_notation _ (_, (uid,opts)) = + Notation.register_rawnumeral_interpretation + ~allow_overwrite:true uid (interp opts, uninterp opts) + +let cache_numeral_notation x = load_numeral_notation 1 x + +(* TODO: substitution ? + TODO: uid pas stable par substitution dans opts + *) + +let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = + Libobject.declare_object { + (Libobject.default_object "NUMERAL NOTATION") with + Libobject.cache_function = cache_numeral_notation; + Libobject.load_function = load_numeral_notation } + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" +let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" +let q_int = qualid_of_string "Coq.Init.Decimal.int" +let q_uint = qualid_of_string "Coq.Init.Decimal.uint" +let q_option = qualid_of_string "Coq.Init.Datatypes.option" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_ind q = + try unsafe_locate_ind q + with Not_found -> Nametab.error_global_not_found q + +let locate_z () = + try + Some { z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_positive } + with Not_found -> None + +let locate_int () = + { uint = locate_ind q_uint; + int = locate_ind q_int } + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty loadZ = + CErrors.user_err + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let type_error_of g ty loadZ = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let vernac_numeral_notation local ty f g scope opts = + let int_ty = locate_int () in + let z_pos_ty = locate_z () in + let tyc = Smartlocate.global_inductive_with_alias ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in + let cty = mkRefC ty in + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let cZ = cref q_z in + let cint = cref q_int in + let cuint = cref q_uint in + let coption = cref q_option in + let opt r = app coption r in + let constructors = get_constructors tyc in + (* Check the type of f *) + let to_kind = + if has_type f (arrow cint cty) then Int int_ty, Direct + else if has_type f (arrow cint (opt cty)) then Int int_ty, Option + else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct + else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type f (arrow cZ cty) then Z z_pos_ty, Direct + else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option + else type_error_to f ty false + | None -> type_error_to f ty true + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty cint) then Int int_ty, Direct + else if has_type g (arrow cty (opt cint)) then Int int_ty, Option + else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct + else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type g (arrow cty cZ) then Z z_pos_ty, Direct + else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option + else type_error_of g ty false + | None -> type_error_of g ty true + in + let o = { to_kind; to_ty; of_kind; of_ty; + num_ty = ty; + warning = opts } + in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); + (* TODO: un hash suffit-il ? *) + let uid = Marshal.to_string o [] in + let i = Notation.( + { pt_local = local; + pt_scope = scope; + pt_uid = uid; + pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_refs = constructors; + pt_in_match = true }) + in + Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); + Notation.enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli new file mode 100644 index 0000000000..83ede6f48f --- /dev/null +++ b/plugins/syntax/numeral.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* * 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 Libnames +open Constrexpr +open Vernacexpr + +(** * Numeral notation *) + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack new file mode 100644 index 0000000000..f4d9cae3ff --- /dev/null +++ b/plugins/syntax/numeral_notation_plugin.mlpack @@ -0,0 +1,2 @@ +Numeral +G_numeral diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune new file mode 100644 index 0000000000..bfdd480fe9 --- /dev/null +++ b/plugins/syntax/plugin_base.dune @@ -0,0 +1,35 @@ +(library + (name numeral_notation_plugin) + (public_name coq.plugins.numeral_notation) + (synopsis "Coq numeral notation plugin") + (modules g_numeral numeral) + (libraries coq.plugins.ltac)) + +(library + (name r_syntax_plugin) + (public_name coq.plugins.r_syntax) + (synopsis "Coq syntax plugin: reals") + (modules r_syntax) + (libraries coq.vernac)) + +(library + (name ascii_syntax_plugin) + (public_name coq.plugins.ascii_syntax) + (synopsis "Coq syntax plugin: ASCII") + (modules ascii_syntax) + (libraries coq.vernac)) + +(library + (name string_syntax_plugin) + (public_name coq.plugins.string_syntax) + (synopsis "Coq syntax plugin: strings") + (modules string_syntax) + (libraries coq.plugins.ascii_syntax)) + +(library + (name int31_syntax_plugin) + (public_name coq.plugins.int31_syntax) + (synopsis "Coq syntax plugin: int31") + (modules int31_syntax) + (libraries coq.vernac)) + diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 0c82e47445..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,101 +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 Pp -open CErrors -open Util -open Names -open Bigint - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "positive_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_number - -(**********************************************************************) -(* Parsing positive via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -let positive_path = make_path binnums "positive" - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") -let glob_positive = IndRef (positive_kn,0) -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH - -let pos_of_bignat ?loc x = - let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack deleted file mode 100644 index ac8f3c425c..0000000000 --- a/plugins/syntax/positive_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Positive_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 94aa143350..04946c158b 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) = with Non_closed_number -> None -let _ = Notation.declare_numeral_interpreter "R_scope" - (r_path,["Coq";"Reals";"Rdefinitions"]) - r_of_int - ([DAst.make @@ GRef (glob_IZR, None)], - uninterp_r, - false) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let r_scope = "R_scope" + +let _ = + register_bignumeral_interpretation r_scope (r_of_int,uninterp_r); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = r_scope; + pt_uid = r_scope; + pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); + pt_refs = [glob_IZR]; + pt_in_match = false } diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c22869f4d6..640bcfde91 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_uid = sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml deleted file mode 100644 index 2534162e36..0000000000 --- a/plugins/syntax/z_syntax.ml +++ /dev/null @@ -1,78 +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 Names -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "z_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let z_path = make_path binnums "Z" -let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") -let glob_z = IndRef (z_kn,0) -let path_of_ZERO = ((z_kn,0),1) -let path_of_POS = ((z_kn,0),2) -let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = ConstructRef path_of_ZERO -let glob_POS = ConstructRef path_of_POS -let glob_NEG = ConstructRef path_of_NEG - -let z_of_int ?loc n = - if not (Bigint.equal n zero) then - let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) - else - DAst.make ?loc @@ GRef(glob_ZERO, None) - -(**********************************************************************) -(* Printing Z via scopes *) -(**********************************************************************) - -let bigint_of_z z = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero - | _ -> raise Non_closed_number - ) z - -let uninterp_z (AnyGlobConstr p) = - try - Some (bigint_of_z p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for Z *) - -let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binnums) - z_of_int - ([DAst.make @@ GRef (glob_ZERO, None); - DAst.make @@ GRef (glob_POS, None); - DAst.make @@ GRef (glob_NEG, None)], - uninterp_z, - true) diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack deleted file mode 100644 index 411260c04c..0000000000 --- a/plugins/syntax/z_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Z_syntax diff --git a/plugins/xml/README b/plugins/xml/README deleted file mode 100644 index 3128189929..0000000000 --- a/plugins/xml/README +++ /dev/null @@ -1,4 +0,0 @@ -The xml export plugin for Coq has been removed from the sources. -A backward compatible plug-in will be provided as a third-party plugin. -For more informations, contact -Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>. diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 542fb5456c..332ecd2c91 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -16,7 +16,6 @@ open Constr open Libnames open Globnames open Nametab -open Environ open Libobject open Mod_subst @@ -118,6 +117,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -131,12 +133,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -316,16 +319,16 @@ let lookup_pattern_path_between env (s,t) = (* rajouter une coercion dans le graphe *) -let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = - ref (fun _ _ _ -> str "<a class path>") +let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path env sigma x = !path_printer env sigma x +let print_path x = !path_printer x -let message_ambig env sigma l = +let message_ambig l = str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l + prlist_with_sep fnl print_path l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -339,7 +342,7 @@ let different_class_params i = | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false -let add_coercion_in_graph env sigma (ic,source,target) = +let add_coercion_in_graph (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -381,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig env sigma !ambig_paths) + Feedback.msg_info (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -426,7 +429,7 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion env sigma (_, c) = +let cache_coercion (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in @@ -439,15 +442,22 @@ let cache_coercion env sigma (_, c) = coe_param = c.coercion_params; } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph env sigma (xf,is,it) + add_coercion_in_graph (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + cache_coercion o + +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -492,8 +502,8 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn - ); + set_coercion_in_scope objn; + cache_coercion objn); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } @@ -553,3 +563,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..7c4842c8ae 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -99,7 +99,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) @@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option + +val is_coercion_in_scope : GlobRef.t -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5e3821edf1..e15c00f7dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -363,12 +363,20 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +let warn_coercion_not_in_scope = + CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated" + Pp.(fun r -> str "Coercion used but not in scope: " ++ + Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use " + ++ str "this coercion, please Import the module that contains it.") + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> + if not (is_coercion_in_scope i.coe_value) then + warn_coercion_not_in_scope i.coe_value; let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in @@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/dune b/pretyping/dune new file mode 100644 index 0000000000..6609b4e328 --- /dev/null +++ b/pretyping/dune @@ -0,0 +1,6 @@ +(library + (name pretyping) + (synopsis "Coq's Type Inference Component (Pretyper)") + (public_name coq.pretyping) + (wrapped false) + (libraries camlp5.gramlib engine)) diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index eb283a0220..be79b8b07d 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FEvar ((_,args),e) -> let variances = infer_stack infos variances stk in infer_vect infos variances (Array.map (mk_clos e) args) - | FRel _ -> variances + | FRel _ -> infer_stack infos variances stk | FFlex fl -> let variances = infer_table_key infos variances fl in infer_stack infos variances stk diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3b9a8e6a1d..a315376aca 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,9 +68,7 @@ type t = { } let get_extra env sigma = - let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) diff --git a/printing/dune b/printing/dune new file mode 100644 index 0000000000..3392342165 --- /dev/null +++ b/printing/dune @@ -0,0 +1,6 @@ +(library + (name printing) + (synopsis "Coq's Term Pretty Printing Library") + (public_name coq.printing) + (wrapped false) + (libraries parsing proofs)) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1810cc6588..9ed985195f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -902,28 +902,28 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = Printer.pr_global v.coe_value +let print_coercion_value v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path env sigma ((i,j),p) = +let print_path ((i,j),p) = hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j let _ = Classops.install_path_printer print_path -let print_graph env sigma = - prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) +let print_graph () = + prlist_with_sep fnl print_path (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) -let print_coercions env sigma = - pr_sequence (print_coercion_value env sigma) (coercions()) +let print_coercions () = + pr_sequence print_coercion_value (coercions()) let index_of_class cl = try @@ -932,7 +932,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between env sigma cls clt = +let print_path_between cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -943,7 +943,7 @@ let print_path_between env sigma cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path env sigma ((i,j),p) + print_path ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 1668bce297..58606db019 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +39,10 @@ val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : env -> evar_map -> Pp.t +val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/proofs/dune b/proofs/dune new file mode 100644 index 0000000000..679c45f6bf --- /dev/null +++ b/proofs/dune @@ -0,0 +1,6 @@ +(library + (name proofs) + (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") + (public_name coq.proofs) + (wrapped false) + (libraries interp)) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 678c3ea3f7..d971c28a26 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in - let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - cb, status, Evd.evar_universe_context univs' + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + cb, status, univs let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the diff --git a/stm/dune b/stm/dune new file mode 100644 index 0000000000..c369bd00fb --- /dev/null +++ b/stm/dune @@ -0,0 +1,6 @@ +(library + (name stm) + (synopsis "Coq's Document Manager and Proof Checking Scheduler") + (public_name coq.stm) + (wrapped false) + (libraries vernac)) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2170477938..85babd922b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -168,7 +168,8 @@ let classify_vernac e = | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ diff --git a/tactics/dune b/tactics/dune new file mode 100644 index 0000000000..908dde5253 --- /dev/null +++ b/tactics/dune @@ -0,0 +1,6 @@ +(library + (name tactics) + (synopsis "Coq's Core Tactics [ML implementation]") + (public_name coq.tactics) + (wrapped false) + (libraries printing)) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d02c3ca6e..d536204ec3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -125,7 +125,7 @@ let unsafe_intro env store decl b = let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - (sigma, mkNamedLambda_or_LetIn decl ev) + (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev) end let introduction id = diff --git a/test-suite/Makefile b/test-suite/Makefile index b8aac8b6f8..f5ec80bcfc 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ - prerequisite/bind_univs.v.log + prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \ + prerequisite/module_bug7192.v.log ####################################################################### # Phony targets diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), diff --git a/test-suite/bugs/closed/7795.v b/test-suite/bugs/closed/7795.v new file mode 100644 index 0000000000..5db0f81cc5 --- /dev/null +++ b/test-suite/bugs/closed/7795.v @@ -0,0 +1,65 @@ + + +Definition fwd (b: bool) A (e2: A): A. Admitted. + +Ltac destruct_refinement_aux T := + let m := fresh "mres" in + let r := fresh "r" in + let P := fresh "P" in + pose T as m; + destruct m as [ r P ]. + +Ltac destruct_refinement := + match goal with + | |- context[proj1_sig ?T] => destruct_refinement_aux T + end. + +Ltac t_base := discriminate || destruct_refinement. + + +Inductive List (T: Type) := +| Cons_construct: T -> List T -> List T +| Nil_construct: List T. + +Definition t (T: Type): List T. Admitted. +Definition size (T: Type) (src: List T): nat. Admitted. +Definition filter1_rt1_type (T: Type): Type := { res: List T | false = true }. +Definition filter1 (T: Type): filter1_rt1_type T. Admitted. + +Definition hh_1: + forall T : Type, + (forall (T0 : Type), + False -> filter1_rt1_type T0) -> + False. +Admitted. + +Definition hh_2: + forall (T : Type), + filter1_rt1_type T -> + filter1_rt1_type T. +Admitted. + +Definition hh: + forall (T : Type) (f1 : forall (T0 : Type), False -> filter1_rt1_type T0), + fwd + (Nat.leb + (size T + (fwd false (List T) + (fwd false (List T) + (proj1_sig + (hh_2 T + (f1 T (hh_1 T f1))))))) 0) bool + false = true. +Admitted. + +Set Program Mode. (* removing this line prevents the bug *) +Obligation Tactic := repeat t_base. + +Goal + forall T (h17: T), + filter1 T = + exist + _ + (Nil_construct T) + (hh T (fun (T : Type) (_ : False) => filter1 T)). +Abort. diff --git a/test-suite/bugs/closed/7967.v b/test-suite/bugs/closed/7967.v new file mode 100644 index 0000000000..2c8855fd54 --- /dev/null +++ b/test-suite/bugs/closed/7967.v @@ -0,0 +1,2 @@ +Set Universe Polymorphism. +Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v new file mode 100644 index 0000000000..0350be9c06 --- /dev/null +++ b/test-suite/bugs/closed/8288.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Set Polymorphic Inductive Cumulativity. + +Inductive foo := C : (forall A : Type -> Type, A Type) -> foo. +(* anomaly invalid subtyping relation *) diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v new file mode 100644 index 0000000000..07986b0df3 --- /dev/null +++ b/test-suite/interactive/PrimNotation.v @@ -0,0 +1,64 @@ +(* Until recently, the Notation.declare_numeral_notation wasn't synchronized + w.r.t. backtracking. This should be ok now. + This test is pretty artificial (we must declare Z_scope for this to work). +*) + +Delimit Scope Z_scope with Z. +Open Scope Z_scope. +Check let v := 0 in v : nat. +(* let v := 0 in v : nat : nat *) +Require BinInt. +Check let v := 0 in v : BinNums.Z. +(* let v := 0 in v : BinNums.Z : BinNums.Z *) +Back 2. +Check let v := 0 in v : nat. +(* Expected answer: let v := 0 in v : nat : nat *) +(* Used to fail with: +Error: Cannot interpret in Z_scope without requiring first module BinNums. +*) + +Local Set Universe Polymorphism. +Delimit Scope punit_scope with punit. +Delimit Scope pcunit_scope with pcunit. +Delimit Scope int_scope with int. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Module A. + NonCumulative Inductive punit@{u} : Type@{u} := ptt. + Cumulative Inductive pcunit@{u} : Type@{u} := pctt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition to_pcunit : Decimal.int -> option pcunit + := fun v => match v with 0%int => Some pctt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. + Back 2. + Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Check let v := 0%punit in v : pcunit. +End A. +Reset A. +Local Unset Universe Polymorphism. +Module A. + Inductive punit : Set := ptt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. +End A. +Local Set Universe Polymorphism. +Inductive punit@{u} : Type@{u} := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. +Back 6. (* check backtracking of registering universe polymorphic constants *) +Local Unset Universe Polymorphism. +Inductive punit : Set := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index bd9240476f..b67ac4f0df 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -10,6 +10,8 @@ Arguments Nat.sub !n !m. About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. Delimit Scope foo_scope with F. Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. About pf. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -76,6 +76,7 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. +Declare Scope znat_scope. Delimit Scope znat_scope with znat. Open Scope znat_scope. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 34f44cd246..3f4d5ef58c 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -20,3 +20,5 @@ Axioms: M.foo : False Closed under the global context Closed under the global context +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index ea1ab63786..3d4dfe603d 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -137,3 +137,13 @@ Module F (X : T). End F. End SUBMODULES. + +(* Testing a variant of #7192 across files *) +(* This was missing in the original fix to #7192 *) +Require Import module_bug7192. +Print Assumptions M7192.D.f. + +(* Testing reporting assumptions from modules in files *) +(* A regression introduced in the original fix to #7192 was missing implementations *) +Require Import module_bug8416. +Print Assumptions M8416.f. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 6f41b2fcf9..926114a1e1 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -48,6 +48,12 @@ Type@{Top.17} -> Type@{v} -> Type@{u} (* u Top.17 v |= *) foo is universe polymorphic +Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) + = Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) Monomorphic mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) @@ -149,24 +155,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i} -(* i Top.44 Top.45 |= *) +axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} +(* i Top.48 Top.49 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i} -(* i Top.44 Top.45 |= *) +axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} +(* i Top.48 Top.49 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.47} -> Type@{axbar'.i} +axfoo' : Type@{Top.51} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.47} -> Type@{axbar'.i} +axbar' : Type@{Top.51} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index c6efc240a6..f806a9f4f7 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -30,6 +30,11 @@ Unset Strict Universe Declaration. order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. + +Check Type@{i} -> Type@{j}. + +Eval cbv in Type@{i} -> Type@{j}. + Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) diff --git a/test-suite/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v new file mode 100644 index 0000000000..82cfe560af --- /dev/null +++ b/test-suite/prerequisite/module_bug7192.v @@ -0,0 +1,9 @@ +(* Variant of #7192 to be tested in a file requiring this file *) +(* #7192 is about Print Assumptions not entering implementation of submodules *) + +Definition a := True. +Module Type B. Axiom f : Prop. End B. +Module Type C. Declare Module D : B. End C. +Module M7192: C. + Module D <: B. Definition f := a. End D. +End M7192. diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v new file mode 100644 index 0000000000..70f43d132a --- /dev/null +++ b/test-suite/prerequisite/module_bug8416.v @@ -0,0 +1,2 @@ +Module Type A. Axiom f : True. End A. +Module M8416 : A. Definition f := I. End M8416. diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 0000000000..e2045900d5 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v new file mode 100644 index 0000000000..288c9d1da0 --- /dev/null +++ b/test-suite/success/CompatCurrentFlag.v @@ -0,0 +1,3 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that the current compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v new file mode 100644 index 0000000000..b7bbc505b4 --- /dev/null +++ b/test-suite/success/CompatOldFlag.v @@ -0,0 +1,5 @@ +(* -*- coq-prog-args: ("-compat" "8.6") -*- *) +(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. +Import Coq.Compat.Coq86. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v new file mode 100644 index 0000000000..9cfe60390f --- /dev/null +++ b/test-suite/success/CompatPreviousFlag.v @@ -0,0 +1,4 @@ +(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..47ef381270 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,302 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. + Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) +End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. + Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Numeral Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. + End with_var. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. + End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. +End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_uint 0. + Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Decimal.uint) := tt. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test11. + (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) + Inductive unit11 := tt11. + Delimit Scope unit11_scope with unit11. + Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. + Qed. +End Test11. + +Module Test12. + (* Test for numeral notations on context variables *) + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + + Numeral Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Numeral Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test that [Local Numeral Notation]s do not escape modules + nor sections. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Fail Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14''_scope. + Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. +End Test14. + +Module Test15. + (** Test module include *) + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Numeral Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Global Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. +End Test16. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66a82008d8..42af3583d4 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -757,6 +757,8 @@ Qed. with lazy behavior (for vm_compute) *) (*****************************************) +Declare Scope lazy_bool_scope. + Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : lazy_bool_scope. Notation "a ||| b" := (if a then true else b) diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index 03e611f549..c376efef2e 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : crelation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 09b35ca75d..97510578ae 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -87,6 +87,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5217aedb88..516ea12099 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : relation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1858ba76ae..001b7dfdfd 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -88,6 +88,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 2ab3af2029..86a3a88be9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -357,6 +357,8 @@ Definition predicate_implication {l : Tlist} := (** Notations for pointwise equivalence and implication of predicates. *) +Declare Scope predicate_scope. + Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 4142af05d2..578425bfb5 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,3 +9,17 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.8 *) +(** In Coq 8.9, prim token notations follow [Import] rather than + [Require]. So we make all of the relevant notations accessible in + compatibility mode. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Int31. +Declare ML Module "string_syntax_plugin". +Declare ML Module "ascii_syntax_plugin". +Declare ML Module "r_syntax_plugin". +Declare ML Module "int31_syntax_plugin". +Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. +Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope. +Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 3485b9c68d..b0d1824827 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -25,6 +25,7 @@ Unset Strict Implicit. (** Notations and helper lemma about pairs *) +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 3452967821..c0db8646c7 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -27,7 +27,7 @@ *) -Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia. Set Implicit Arguments. Unset Strict Implicit. @@ -39,7 +39,7 @@ Import Raw.Proofs. Local Open Scope pair_scope. Local Open Scope Int_scope. -Ltac omega_max := i2z_refl; romega with Z. +Ltac omega_max := i2z_refl; lia. Section Elt. Variable elt : Type. @@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: end. Proof. intros; unfold cardinal_e_2; simpl; - abstract (do 2 rewrite cons_cardinal_e; romega with * ). + abstract (do 2 rewrite cons_cardinal_e; lia ). Defined. Definition Cmp c := diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 05b741f0ac..76c39f275d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,7 +12,6 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. -Declare ML Module "nat_syntax_plugin". (********************************************************************) (** * Datatypes with zero and one element *) @@ -38,8 +37,8 @@ Inductive bool : Set := Add Printing If bool. +Declare Scope bool_scope. Delimit Scope bool_scope with bool. - Bind Scope bool_scope with bool. (** Basic boolean operators *) @@ -137,6 +136,7 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. Arguments S _%nat. @@ -229,10 +229,13 @@ Inductive list (A : Type) : Type := Arguments nil {A}. Arguments cons {A} a l. -Infix "::" := cons (at level 60, right associativity) : list_scope. + +Declare Scope list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. +Infix "::" := cons (at level 60, right associativity) : list_scope. + Local Open Scope list_scope. Definition length (A : Type) : list A -> nat := diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b07..537400fb05 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,10 +42,13 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). -Delimit Scope uint_scope with uint. -Bind Scope uint_scope with uint. -Delimit Scope int_scope with int. -Bind Scope int_scope with int. +Declare Scope dec_uint_scope. +Delimit Scope dec_uint_scope with uint. +Bind Scope dec_uint_scope with uint. + +Declare Scope dec_int_scope. +Delimit Scope dec_int_scope with int. +Bind Scope dec_int_scope with int. (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, @@ -161,3 +164,9 @@ with succ_double d := end. End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index ad1bc717c4..eb4ba0e5e6 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -24,6 +24,10 @@ Definition t := nat. (** ** Constants *) +Local Notation "0" := O. +Local Notation "1" := (S O). +Local Notation "2" := (S (S O)). + Definition zero := 0. Definition one := 1. Definition two := 2. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 72073bb4f6..8f8e639187 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -108,13 +108,17 @@ End IfNotations. (** Scopes *) -Delimit Scope type_scope with type. -Delimit Scope function_scope with function. +Declare Scope core_scope. Delimit Scope core_scope with core. -Bind Scope type_scope with Sortclass. +Declare Scope function_scope. +Delimit Scope function_scope with function. Bind Scope function_scope with Funclass. +Declare Scope type_scope. +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. + Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index d5322d0945..65e5e76a22 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -31,6 +31,7 @@ Require Import Logic. Require Coq.Init.Nat. Open Scope nat_scope. +Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 802f18c0f2..6d98bcb34a 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,9 +19,24 @@ Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. -(* Initially available plugins - (+ nat_syntax_plugin loaded in Datatypes) *) +(* Some initially available plugins. See also: + - ltac_plugin (in Notations) + - tauto_plugin (in Tauto). +*) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%dec_uint_scope. +Arguments Nat.of_int d%dec_int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : dec_uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : dec_int_scope. + +(* Parsing / printing of [nat] numbers *) +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6afba29a0..db8857df64 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -697,7 +697,7 @@ End Choice_lemmas. Section Dependent_choice_lemmas. - Variables X : Set. + Variable X : Set. Variable R : X -> X -> Prop. Lemma dependent_choice : diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index b966f217aa..aec88f93bf 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -340,6 +340,8 @@ Functional Scheme union_ind := Induction for union Sort Prop. (** Notations and helper lemma about pairs and triples *) +Declare Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5abc7..bd27f94abd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 5de75537cb..be12fffaaf 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -13,6 +13,10 @@ Require Import BinPos. Local Open Scope N_scope. +Local Notation "0" := N0. +Local Notation "1" := (Npos 1). +Local Notation "2" := (Npos 2). + (**********************************************************************) (** * Binary natural numbers, definitions of operations *) (**********************************************************************) @@ -398,4 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. + +(** Re-export the notation for those who just [Import NatIntDef] *) +Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 0000000000..c7e3999691 --- /dev/null +++ b/theories/Numbers/AltBinNotations.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** * Alternative Binary Numeral Notations *) + +(** Faster but less safe parsers and printers of [positive], [N], [Z]. *) + +(** By default, literals in types [positive], [N], [Z] are parsed and + printed via the [Numeral Notation] command, by conversion from/to + the [Decimal.int] representation. When working with numbers with + thousands of digits and more, conversion from/to [Decimal.int] can + become significantly slow. If that becomes a problem for your + development, this file provides some alternative [Numeral + Notation] commmands that use [Z] as bridge type. To enable these + commands, just be sure to [Require] this file after other files + defining numeral notations. + + Note: up to Coq 8.8, literals in types [positive], [N], [Z] were + parsed and printed using a native ML library of arbitrary + precision integers named bigint.ml. From 8.9, the default is to + parse and print using a Coq library converting sequences of + digits, hence reducing the amount of ML code to trust. But this + method is slower. This file then gives access to the legacy + method, trading efficiency against a larger ML trust base relying + on bigint.ml. *) + +Require Import BinNums. + +(** [positive] *) + +Definition pos_of_z z := + match z with + | Zpos p => Some p + | _ => None + end. + +Definition pos_to_z p := Zpos p. + +Numeral Notation positive pos_of_z pos_to_z : positive_scope. + +(** [N] *) + +Definition n_of_z z := + match z with + | Z0 => Some N0 + | Zpos p => Some (Npos p) + | Zneg _ => None + end. + +Definition n_to_z n := + match n with + | N0 => Z0 + | Npos p => Zpos p + end. + +Numeral Notation N n_of_z n_to_z : N_scope. + +(** [Z] *) + +Definition z_of_z (z:Z) := z. + +Numeral Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index d5eb4f2681..7b6740e94b 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,21 +12,18 @@ Set Implicit Arguments. -Declare ML Module "positive_syntax_plugin". -Declare ML Module "n_syntax_plugin". -Declare ML Module "z_syntax_plugin". - (** [positive] is a datatype representing the strictly positive integers in a binary way. Starting from 1 (represented by [xH]), one can add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). - Numbers in [positive] can also be denoted using a decimal notation; - e.g. [6%positive] abbreviates [xO (xI xH)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive | xO : positive -> positive | xH : positive. +Declare Scope positive_scope. Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. Arguments xO _%positive. @@ -34,13 +31,14 @@ Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. - Numbers in [N] can also be denoted using a decimal notation; - e.g. [6%N] abbreviates [Npos (xO (xI xH))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N | Npos : positive -> N. +Declare Scope N_scope. Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. @@ -49,14 +47,15 @@ Arguments Npos _%positive. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number (whose opposite is stored as a [positive] value). - Numbers in [Z] can also be denoted using a decimal notation; - e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z. +Declare Scope Z_scope. Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279d4..4a1f24b95e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -21,9 +21,7 @@ Require Import Znumtheory. Require Import Zgcd_alt. Require Import Zpow_facts. Require Import CyclicAxioms. -Require Import ROmega. - -Declare ML Module "int31_syntax_plugin". +Require Import Lia. Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -128,7 +126,7 @@ Section Basics. Lemma nshiftl_S_tail : forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. - Proof. + Proof. intros n; elim n; simpl; intros; now f_equal. Qed. @@ -1239,7 +1237,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq. destruct Z.compare; intros; @@ -1263,7 +1261,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y+1) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq. destruct Z.compare; intros; @@ -1301,8 +1299,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y) 0). rewrite <- (Z_mod_plus_full (X-Y) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq. destruct Z.compare; intros; @@ -1320,8 +1318,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y-1) 0). rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq. destruct Z.compare; intros; @@ -1358,7 +1356,7 @@ Section Int31_Specs. change [|1|] with 1; change [|0|] with 0. rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB). rewrite Zminus_mod_idemp_l. - rewrite Zmod_small; generalize (phi_bounded x); romega. + rewrite Zmod_small; generalize (phi_bounded x); lia. Qed. Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 9f8da831d8..77ab624ca5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -48,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31. Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d7f25a6613..a70ecd19d8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem - [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ] + [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ] The outcome of the modulo function is hence always positive. This corresponds to convention "E" in the following paper: @@ -46,6 +46,7 @@ Module ZEuclidProp (** We put notations in a scope, to avoid warnings about redefinitions of notations *) + Declare Scope euclid. Infix "/" := D.div : euclid. Infix "mod" := D.modulo : euclid. Local Open Scope euclid. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 3d0c005fd1..acebfcf1d2 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -220,8 +220,10 @@ End NZDomainProp. Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. + +Declare Scope ofnat. Local Open Scope ofnat. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. Lemma ofnat_zero : [O] == 0. Proof. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 000d895e10..dcaae1606d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. + Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. Infix "*" := Pos.mul : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 070314746a..7f30733559 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation positive of_int to_uint : positive_scope. + End Pos. + +(** Re-export the notation for those who just [Import BinPosDef] *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f55093ed48..c2316689fc 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) := Hint Unfold compose. +Declare Scope program_scope. + Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bc83881849..edbae6534a 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -326,7 +326,7 @@ Ltac program_solve_wf := Create HintDb program discriminated. -Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf. +Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 78c36dc7d1..c51cacac68 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -20,12 +20,13 @@ Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) (x ident, y ident, at level 10) : type_scope. +Declare Scope program_scope. +Delimit Scope program_scope with prg. + (** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _) : program_scope. -Delimit Scope program_scope with prg. - (** Abbreviation for first projection and hiding of proofs of subset objects. *) Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 35706e7fa2..139c4bf432 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -18,6 +18,7 @@ Require Export Morphisms Setoid Bool. Record Q : Set := Qmake {Qnum : Z; Qden : positive}. +Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 1510a7b825..81c318138e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec. Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. +Declare Scope Qc_scope. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 36ac738ca6..9f8039ec9d 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -28,6 +28,7 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x. Definition comp f1 f2 (x:R) : R := f1 (f2 x). Definition inv_fct f (x:R) : R := / f x. +Declare Scope Rfun_scope. Delimit Scope Rfun_scope with F. Arguments plus_fct (f1 f2)%F x%R. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 6019d4faf1..a2818371e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,6 +14,7 @@ Require Export ZArith_base. Require Export Rdefinitions. +Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 857b4ec33b..932fcddaf5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,12 +12,15 @@ (** Definitions for the axiomatization *) (*********************************************************) -Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. -(* Declare Scope positive_scope with Key R *) +(* Declare primitive numeral notations for Scope R_scope *) +Declare Scope R_scope. +Declare ML Module "r_syntax_plugin". + +(* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 31a7fb8ad6..3f676c1888 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,7 +13,6 @@ Adapted to Coq V8 by the Coq Development Team *) Require Import Bool BinPos BinNat PeanoNat Nnat. -Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin". Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). +Declare Scope char_scope. +Declare ML Module "ascii_syntax_plugin". Delimit Scope char_scope with char. Bind Scope char_scope with ascii. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index be9a10c6dc..b27474ef25 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,7 +15,6 @@ Require Import Arith. Require Import Ascii. Require Import Bool. -Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) @@ -25,6 +24,8 @@ Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. +Declare Scope string_scope. +Declare ML Module "string_syntax_plugin". Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 87df6b479d..60c64d306b 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType'). Module OrderTac := OT_to_OrderTac O. Ltac order := OrderTac.order. + Declare Scope order. Notation "x <= y" := (~lt y x) : order. Infix "?=" := compare (at level 70, no associativity) : order. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index ba3e411091..390ca78c0e 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -305,6 +305,7 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni End VECTORLIST. Module VectorNotations. +Declare Scope vector_scope. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b57e..a11d491a8b 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b90c..8cb62622db 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -635,4 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. + +(** Re-export the notation for those who just [Import BinIntDef] *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 2f3bf9a32a..1e35370d29 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -17,6 +17,7 @@ *) Require Import BinInt. +Declare Scope Int_scope. Delimit Scope Int_scope with I. Local Open Scope Int_scope. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index e93ebb1ad5..0c9aca2657 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. +Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. @@ -129,33 +129,33 @@ Qed. Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. @@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - - romega with *. - - romega with *. - - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - lia. + - lia. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } - destruct r; simpl Z.sgn in *; romega with *. + destruct r; simpl Z.sgn in *; lia. Qed. Theorem Zquot_mod_unique_full a b q r : @@ -185,7 +185,7 @@ Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. - romega with *. + lia. rewrite <- H1; apply Z.quot_rem'. rewrite <- (Z.opp_involutive a). @@ -193,7 +193,7 @@ Proof. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. - romega with *. + lia. Qed. Theorem Zquot_unique_full a b q r : diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml new file mode 100644 index 0000000000..ab60920fbc --- /dev/null +++ b/tools/coq_dune.ml @@ -0,0 +1,307 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + *) + +(* coq_dune: generate dune build rules for .vo files *) +(* *) +(* At some point this file will become a Dune plugin, so it is very *) +(* important that this file can be bootstrapped with: *) +(* *) +(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) + +open Format + +(* Keeping this file self-contained as it is a "bootstrap" utility *) +(* Is OCaml missing these basic functions in the stdlib? *) +module Aux = struct + + let option_iter f o = match o with + | Some x -> f x + | None -> () + + let option_cata d f o = match o with + | Some x -> f x + | None -> d + + let list_compare f = let rec lc x y = match x, y with + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r + in lc + + let rec pp_list pp sep fmt l = match l with + | [] -> () + | [l] -> fprintf fmt "%a" pp l + | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs + + let rec pmap f l = match l with + | [] -> [] + | x :: xs -> + begin match f x with + | None -> pmap f xs + | Some r -> r :: pmap f xs + end + + let sep fmt () = fprintf fmt "@;" + + module DirOrd = struct + type t = string list + let compare = list_compare String.compare + end + + module DirMap = Map.Make(DirOrd) + + (* Functions available in newer OCaml versions *) + (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) + module Legacy = struct + + (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) + let dirmap_update key f map = + match begin + try f (Some (DirMap.find key map)) + with Not_found -> f None + end with + | None -> DirMap.remove key map + | Some x -> DirMap.add key x map + + (* Available in OCaml >= 4.04 *) + let split_on_char sep s = + let open String in + let r = ref [] in + let j = ref (length s) in + for i = length s - 1 downto 0 do + if unsafe_get s i = sep then begin + r := sub s (i + 1) (!j - i - 1) :: !r; + j := i + end + done; + sub s 0 !j :: !r + + (* Available in OCaml >= 4.04 *) + let is_dir_sep = match Sys.os_type with + | "Win32" -> fun s i -> s.[i] = '\\' + | _ -> fun s i -> s.[i] = '/' + + let extension_len name = + let rec check i0 i = + if i < 0 || is_dir_sep name i then 0 + else if name.[i] = '.' then check i0 (i - 1) + else String.length name - i0 + in + let rec search_dot i = + if i < 0 || is_dir_sep name i then 0 + else if name.[i] = '.' then check i (i - 1) + else search_dot (i - 1) + in + search_dot (String.length name - 1) + + let remove_extension name = + let l = extension_len name in + if l = 0 then name else String.sub name 0 (String.length name - l) + + end + + let add_map_list key elem map = + (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) + Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map + +end + +open Aux + +(* Once this is a Dune plugin the flags will be taken from the env *) +module Options = struct + + type flag = { + enabled : bool; + cmd : string; + } + + let all_opts = + [ { enabled = false; cmd = "-debug"; } + ; { enabled = false; cmd = "-native_compiler"; } + ] + + let build_coq_flags () = + let popt o = if o.enabled then Some o.cmd else None in + String.concat " " @@ pmap popt all_opts +end + +type vodep = { + target: string; + deps : string list; +} + +type ldep = | VO of vodep | ML4 of string | MLG of string +type ddir = ldep list DirMap.t + +(* Filter `.vio` etc... *) +let filter_no_vo = + List.filter (fun f -> Filename.check_suffix f ".vo") + +(* We could have coqdep to output dune files directly *) + +(* Fix once we move to OCaml >= 4.06.0 *) +let list_init len f = + let rec init_aux i n f = + if i >= n then [] + else let r = f i in r :: init_aux (i+1) n f + in init_aux 0 len f + +let gen_sub n = + (* Move to List.init once we can depend on OCaml >= 4.06.0 *) + String.concat "/" (list_init n (fun _ -> "..")) ^ "/" + +let pp_rule fmt targets deps action = + (* Special printing of the first rule *) + let ppl = pp_list pp_print_string sep in + let pp_deps fmt l = match l with + | [] -> + () + | x :: xs -> + fprintf fmt "(:pp-file %s)%a" x sep (); + pp_list pp_print_string sep fmt xs + in + fprintf fmt + "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" + ppl targets pp_deps deps pp_print_string action + +(* Generate the dune rule: *) +let pp_vo_dep dir fmt vo = + let depth = List.length dir in + let sdir = gen_sub depth in + (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) + let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", ["theories/Init/Prelude.vo"] in + (* Coq flags *) + let cflag = Options.build_coq_flags () in + (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) + let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in + (* The source file is also corrected as we will call coqtop from the top dir *) + let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in + (* The final build rule *) + let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in + pp_rule fmt [vo.target] deps action + +let pp_ml4_dep _dir fmt ml = + let target = Legacy.(remove_extension ml) ^ ".ml" in + let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in + pp_rule fmt [target] [ml] ml4_rule + +let pp_mlg_dep _dir fmt ml = + let target = Legacy.(remove_extension ml) ^ ".ml" in + let ml4_rule = "(run coqpp %{pp-file})" in + pp_rule fmt [target] [ml] ml4_rule + +let pp_dep dir fmt oo = match oo with + | VO vo -> pp_vo_dep dir fmt vo + | ML4 f -> pp_ml4_dep dir fmt f + | MLG f -> pp_mlg_dep dir fmt f + +let out_install fmt dir ff = + let itarget = String.concat "/" dir in + let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in + let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (itarget^"/"^tg) in + fprintf fmt "(install@\n @[(section lib)@\n(files @[%a@])@])@\n" + (pp_list pp_ispec sep) ff + +(* For each directory, we must record two things, the build rules and + the install specification. *) +let record_dune d ff = + let sd = String.concat "/" d in + if Sys.file_exists sd && Sys.is_directory sd then + let out = open_out (sd^"/dune") in + let fmt = formatter_of_out_channel out in + if List.nth d 0 = "plugins" then + fprintf fmt "(include plugin_base.dune)@\n"; + out_install fmt d ff; + List.iter (pp_dep d fmt) ff; + fprintf fmt "%!"; + close_out out + else + eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd + +(* File Scanning *) +let choose_ml4g_form f = + if Filename.check_suffix f ".ml4" then ML4 f + else MLG f + +let scan_mlg4 m d = + let dir = ["plugins"; d] in + let m = DirMap.add dir [] m in + let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg")) + Array.(to_list @@ readdir String.(concat "/" dir))) in + List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 + +let scan_plugins m = + let dirs = Sys.(List.filter (fun f -> is_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in + List.fold_left scan_mlg4 m dirs + +(* Process .vfiles.d and generate a skeleton for the dune file *) +let parse_coqdep_line l = + match Str.(split (regexp ":") l) with + | [targets;deps] -> + let targets = Str.(split (regexp "[ \t]+") targets) in + let deps = Str.(split (regexp "[ \t]+") deps) in + let targets = filter_no_vo targets in + begin match targets with + | [target] -> + let dir, target = Filename.(dirname target, basename target) in + Some (Legacy.split_on_char '/' dir, VO { target; deps; }) + (* Otherwise a vio file, we ignore *) + | _ -> None + end + (* Strange rule, we ignore *) + | _ -> None + +let rec read_vfiles ic map = + try + let rule = parse_coqdep_line (input_line ic) in + (* Add vo_entry to its corresponding map entry *) + let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in + read_vfiles ic map + with End_of_file -> map + +let out_map map = + DirMap.iter record_dune map + +let exec_ifile f = + match Array.length Sys.argv with + | 1 -> f stdin + | 2 -> + let ic = open_in Sys.argv.(1) in + (try f ic with _ -> close_in ic) + | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 + +let _ = + exec_ifile (fun ic -> + let map = scan_plugins DirMap.empty in + let map = read_vfiles ic map in + out_map map) diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000..2ba0e3fe8a --- /dev/null +++ b/tools/dune @@ -0,0 +1,31 @@ +(executable + (name coqc) + (public_name coqc) + (modules coqc) + (libraries coq.toplevel)) + +(executable + (name coq_makefile) + (public_name coq_makefile) + (modules coq_makefile) + (libraries coq.lib)) + +(executable + (name coqdep) + (public_name coqdep) + (modules coqdep_lexer coqdep_common coqdep) + (libraries coq.lib)) + +(ocamllex coqdep_lexer) + +(executable + (name coq_tex) + (public_name coq_tex) + (modules coq_tex) + (libraries str)) + +(executable + (name coq_dune) + (public_name coq_dune) + (modules coq_dune) + (libraries str)) diff --git a/topbin/dune b/topbin/dune new file mode 100644 index 0000000000..e89f6c4b13 --- /dev/null +++ b/topbin/dune @@ -0,0 +1,25 @@ +(executable + (name coqtop_bin) + (public_name coqtop) + (package coq) + (modules coqtop_bin) + (libraries coq.toplevel) + (link_flags -linkall)) + +(executable + (name coqtop_byte_bin) + (public_name coqtop.byte) + (package coq) + (modules coqtop_byte_bin) + (libraries compiler-libs.toplevel coq.toplevel) + (modes byte) + (link_flags -linkall)) + +; Workers +(executables + (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin) + (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt) + (package coq) + (modules :standard \ coqtop_byte_bin coqtop_bin) + (libraries coq.toplevel) + (link_flags -linkall)) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 113ba3684c..98a28bb2b6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -154,7 +154,7 @@ let add_compat_require opts v = match v with | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false) | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) - | Flags.Current -> opts + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq88" None (Some false) let set_batch_mode opts = Flags.quiet := true; diff --git a/toplevel/dune b/toplevel/dune new file mode 100644 index 0000000000..f51e50aaa3 --- /dev/null +++ b/toplevel/dune @@ -0,0 +1,13 @@ +(library + (name toplevel) + (public_name coq.toplevel) + (synopsis "Coq's Interactive Shell [terminal-based]") + (wrapped false) + (libraries num coq.stm)) +; Coqlevel provides the `Num` library to plugins, we could also use +; -linkall in the plugins file, to be discussed. + +(rule + (targets g_toplevel.ml) + (deps (:mlg-file g_toplevel.mlg)) + (action (run coqpp %{mlg-file}))) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 765f962e99..e5d2382e46 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with - | MPfile _ -> raise Not_found + | MPfile _ -> Global.lookup_module mp | MPbound _ -> assert false | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index ad1ffa35a1..716c40dbff 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -326,6 +326,15 @@ let check_param = function | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") +let restrict_inductive_universes sigma ctx_params arities constructors = + let merge_universes_of_constr c = + Univ.LSet.union (EConstr.universes_of_constr sigma (EConstr.of_constr c)) in + let uvars = Univ.LSet.empty in + let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in + let uvars = List.fold_right merge_universes_of_constr arities uvars in + let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in + Evd.restrict_universe_context sigma uvars + let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; @@ -400,6 +409,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly let arities = List.map nf arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in + let sigma = restrict_inductive_universes sigma ctx_params arities constructors in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; diff --git a/vernac/dune b/vernac/dune new file mode 100644 index 0000000000..45b567d631 --- /dev/null +++ b/vernac/dune @@ -0,0 +1,16 @@ +(library + (name vernac) + (synopsis "Coq's Vernacular Language") + (public_name coq.vernac) + (wrapped false) + (libraries tactics parsing)) + +(rule + (targets g_proofs.ml) + (deps (:mlg-file g_proofs.mlg)) + (action (run coqpp %{mlg-file}))) + +(rule + (targets g_vernac.ml) + (deps (:mlg-file g_vernac.mlg)) + (action (run coqpp %{mlg-file}))) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74516e320c..44c0159d1b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram info = hint_info -> { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + (* Should be in syntax, but camlp5 would not factorize *) + | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> + { VernacDeclareScope sc } + (* System directory *) | IDENT "Pwd" -> { VernacChdir None } | IDENT "Cd" -> { VernacChdir None } @@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> { VernacSyntaxExtension (false, (s,l)) } - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) + (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order + to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; only_parsing: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d66a121437..2e5e11bb09 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1306,8 +1306,18 @@ type notation_obj = { notobj_notation : notation * notation_location; } -let load_notation _ (_, nobj) = - Option.iter Notation.declare_scope nobj.notobj_scope +let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = + (* When the default shall be to require that a scope already exists *) + (* the call to ensure_scope will have to be removed *) + if silently_define_scope_if_undefined then + (* Don't warn if the scope is not defined: *) + (* there was already a warning at "cache" time *) + Option.iter Notation.declare_scope nobj.notobj_scope + else + Option.iter Notation.ensure_scope nobj.notobj_scope + +let load_notation = + load_notation_common true let open_notation i (_, nobj) = let scope = nobj.notobj_scope in @@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) = end let cache_notation o = - load_notation 1 o; + load_notation_common false 1 o; open_notation 1 o let subst_notation (subst, nobj) = @@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = add_notation local env c (df,modifiers) sc (**********************************************************************) -(* Delimiters and classes bound to scopes *) +(* Scopes, delimiters and classes bound to scopes *) type scope_command = - | ScopeDelim of string + | ScopeDeclare + | ScopeDelimAdd of string + | ScopeDelimRemove | ScopeClasses of scope_class list - | ScopeRemove - -let load_scope_command _ (_,(scope,dlm)) = - Notation.declare_scope scope -let open_scope_command i (_,(scope,o)) = +let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) = + let declare_scope_if_needed = + if silently_define_scope_if_undefined then Notation.declare_scope + else Notation.ensure_scope in + match o with + | ScopeDeclare -> Notation.declare_scope scope + (* When the default shall be to require that a scope already exists *) + (* the call to declare_scope_if_needed will have to be removed below *) + | ScopeDelimAdd dlm -> declare_scope_if_needed scope + | ScopeDelimRemove -> declare_scope_if_needed scope + | ScopeClasses cl -> declare_scope_if_needed scope + +let load_scope_command = + load_scope_command_common true + +let open_scope_command i (_,(local,scope,o)) = if Int.equal i 1 then match o with - | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeDeclare -> () + | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm + | ScopeDelimRemove -> Notation.remove_delimiters scope | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl - | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = - load_scope_command 1 o; + load_scope_command_common false 1 o; open_scope_command 1 o -let subst_scope_command (subst,(scope,o as x)) = match o with +let subst_scope_command (subst,(local,scope,o as x)) = match o with | ScopeClasses cl -> let cl' = List.map_filter (subst_scope_class subst) cl in let cl' = if List.for_all2eq (==) cl cl' then cl else cl' in - scope, ScopeClasses cl' + local, scope, ScopeClasses cl' | _ -> x -let inScopeCommand : scope_name * scope_command -> obj = +let classify_scope_command (local, _, _ as o) = + if local then Dispose else Substitute o + +let inScopeCommand : locality_flag * scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj)} + classify_function = classify_scope_command} + +let declare_scope local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare)) -let add_delimiters scope key = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let add_delimiters local scope key = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key)) -let remove_delimiters scope = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) +let remove_delimiters local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove)) -let add_class_scope scope cl = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) +let add_class_scope local scope cl = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 73bee7121b..38dbdf7e41 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr -> val add_notation_extra_printing_rule : string -> string -> string -> unit -(** Declaring delimiter keys and default scopes *) +(** Declaring scopes, delimiter keys and default scopes *) -val add_delimiters : scope_name -> string -> unit -val remove_delimiters : scope_name -> unit -val add_class_scope : scope_name -> scope_class list -> unit +val declare_scope : locality_flag -> scope_name -> unit +val add_delimiters : locality_flag -> scope_name -> string -> unit +val remove_delimiters : locality_flag -> scope_name -> unit +val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 93e4e89a12..63e9e4fe49 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -635,6 +635,10 @@ open Pputils keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) + | VernacDeclareScope sc -> + return ( + keyword "Declare Scope" ++ spc () ++ str sc + ) | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e1c9712135..681dce3ca3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -403,17 +403,24 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension atts infix l = +let vernac_syntax_extension ~atts infix l = let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l -let vernac_delimiters sc = function - | Some lr -> Metasyntax.add_delimiters sc lr - | None -> Metasyntax.remove_delimiters sc +let vernac_declare_scope ~atts sc = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_scope local sc -let vernac_bind_scope sc cll = - Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) +let vernac_delimiters ~atts sc action = + let local = enforce_module_locality atts.locality in + match action with + | Some lr -> Metasyntax.add_delimiters local sc lr + | None -> Metasyntax.remove_delimiters local sc + +let vernac_bind_scope ~atts sc cll = + let local = enforce_module_locality atts.locality in + Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll) let vernac_open_close_scope ~atts (b,s) = let local = enforce_section_locality atts.locality in @@ -1692,36 +1699,37 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in - let sigma', c = interp_open_constr env sigma rc in - let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in - Evarconv.check_problems_are_solved env sigma'; - let sigma' = Evd.minimize_universes sigma' in - let uctx = Evd.universe_context_set sigma' in - let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in + let sigma, c = interp_open_constr env sigma rc in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Evarconv.check_problems_are_solved env sigma; + let sigma = Evd.minimize_universes sigma in + let uctx = Evd.universe_context_set sigma in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma env) in let j = - if Evarutil.has_undefined_evars sigma' c then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) + if Evarutil.has_undefined_evars sigma c then + Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c) else - let c = EConstr.to_constr sigma' c in + let c = EConstr.to_constr sigma c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in - match redexp with + let pp = match redexp with | None -> - let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in + let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in - let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in - print_judgment env sigma' j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx_set sigma uctx + let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in + print_judgment env sigma j ++ + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l | Some r -> - let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in + let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in let (_, c) = redfun env evm c in c in - print_eval redfun env sigma' rc j + print_eval redfun env sigma rc j + in + pp ++ Printer.pr_universe_ctx_set sigma uctx let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in @@ -1801,13 +1809,13 @@ let vernac_print ~atts env sigma = | PrintName (qid,udecl) -> dump_global qid; print_name env sigma qid udecl - | PrintGraph -> Prettyp.print_graph env sigma + | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() | PrintInstances c -> Prettyp.print_instances (smart_global c) - | PrintCoercions -> Prettyp.print_coercions env sigma + | PrintCoercions -> Prettyp.print_coercions () | PrintCoercionPaths (cls,clt) -> - Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -2092,9 +2100,10 @@ let interp ?proof ~atts ~st c = (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - vernac_syntax_extension atts infix sl - | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr - | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl + vernac_syntax_extension ~atts infix sl + | VernacDeclareScope sc -> vernac_declare_scope ~atts sc + | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr + | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> @@ -2231,6 +2240,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _ | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8fb74e6d78..11b2a7d802 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -325,6 +325,7 @@ type nonrec vernac_expr = (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name + | VernacDeclareScope of scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of (lstring * syntax_modifier list) * |