diff options
56 files changed, 408 insertions, 289 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 956d74c8c1..3a626796a6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -578,6 +578,8 @@ library:ci-bedrock2: name: "$CI_JOB_NAME" paths: - _build_ci + variables: + NJOBS: "1" library:ci-color: extends: .ci-template-flambda diff --git a/META.coq.in b/META.coq.in index 49bdea6d9c..377dbd9b7e 100644 --- a/META.coq.in +++ b/META.coq.in @@ -561,4 +561,19 @@ package "plugins" ( plugin(byte) = "ssreflect_plugin.cmo" plugin(native) = "ssreflect_plugin.cmxs" ) + + package "ltac2" ( + + description = "Coq Ltac2 Plugin" + version = "8.12" + + requires = "coq.plugins.ltac" + directory = "../user-contrib/Ltac2" + + archive(byte) = "ltac2_plugin.cmo" + archive(native) = "ltac2_plugin.cmx" + + plugin(byte) = "ltac2_plugin.cmo" + plugin(native) = "ltac2_plugin.cmxs" + ) ) diff --git a/Makefile.vofiles b/Makefile.vofiles index b6e0cd0a08..fe7ca7c36f 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -31,9 +31,9 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))) -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))) ifdef QUICK GLOBFILES:= diff --git a/dev/base_include b/dev/base_include index 4841db8953..96a867475d 100644 --- a/dev/base_include +++ b/dev/base_include @@ -60,11 +60,11 @@ open Cases open Pattern open Patternops open Cbv -open Classops +open Coercionops open Arguments_renaming open Pretyping open Cbv -open Classops +open Coercionops open Clenv open Clenvtac open Constr_matching @@ -134,7 +134,7 @@ open Tacticals open Tactics open Eqschemes -open Class +open ComCoercion open ComDefinition open Indschemes open Ind_tables diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b1c752ba60..859b3e3166 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -921,69 +921,6 @@ function make_gtk_sourceview3 { build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.11 tar.xz make_arch_pkg_config } -##### FLEXDLL FLEXLINK ##### - -# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.) -# For MinGW it is not even possible to first build an Ocaml without flexlink support, -# Because Makefile.nt doesn't support this. So we have to use a binary flexlink. -# One could of cause do a bootstrap run ... - -# Install flexdll objects - -function install_flexdll { - cp flexdll.h "$PREFIXMINGW/include" - if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then - cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin" - cp flexdll*_mingw.o "$PREFIXOCAML/bin" - elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then - cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin" - cp flexdll*_mingw64.o "$PREFIXOCAML/bin" - else - echo "Unknown target architecture" - return 1 - fi -} - -# Install flexlink - -function install_flexlink { - cp flexlink.exe "/usr/$TARGET_ARCH/bin" - - cp flexlink.exe "$PREFIXOCAML/bin" -} - -# Get binary flexdll flexlink for building OCaml -# An alternative is to first build an OCaml without shared library support and build flexlink with it - -function get_flex_dll_link_bin { - if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then - install_flexdll - install_flexlink - build_post - fi -} - -# Build flexdll and flexlink from sources after building OCaml - -function make_flex_dll_link { - if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then - if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then - # shellcheck disable=SC2086 - log1 make $MAKE_OPT build_mingw flexlink.exe - elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then - # shellcheck disable=SC2086 - log1 make $MAKE_OPT build_mingw64 flexlink.exe - else - echo "Unknown target architecture" - return 1 - fi - install_flexdll - install_flexlink - log2 make clean - build_post - fi -} - ##### LN replacement ##### # Note: this does support symlinks, but symlinks require special user rights on Windows. @@ -1016,39 +953,22 @@ function make_arch_pkg_config { ##### OCAML ##### function make_ocaml { - get_flex_dll_link_bin - if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then - # See README.win32.adoc - cp config/m-nt.h byterun/caml/m.h - cp config/s-nt.h byterun/caml/s.h - if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then - cp config/Makefile.mingw config/Makefile - elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then - cp config/Makefile.mingw64 config/Makefile - else - echo "Unknown target architecture" - return 1 - fi + if build_prep https://github.com/ocaml/ocaml/archive 4.08.1 tar.gz 1 ocaml-4.08.1 ; then + # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc - # Prefix is fixed in make file - replace it with the real one - # TODO: this might not work if PREFIX contains spaces - sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile + # get flexdll sources into folder ./flexdll + get_expand_source_tar https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 flexdll # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder - # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path: - # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml - # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4 - # So we put an explicit path in there - sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile - - # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT - # I verified that 4.02.3 still doesn't support parallel build - log2 make world -f Makefile.nt - log2 make bootstrap -f Makefile.nt - log2 make opt -f Makefile.nt - log2 make opt.opt -f Makefile.nt - log2 make install -f Makefile.nt - # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development + logn configure ./configure --build=i686-pc-cygwin --host="$TARGET_ARCH" --prefix="$PREFIXOCAML" --libdir="$PREFIXOCAML/libocaml" + + log2 make flexdll $MAKE_OPT + # Note the next command might change after 4.09.x to just make + # see https://github.com/ocaml/ocaml/blob/4.09/README.win32.adoc + # compare to https://github.com/ocaml/ocaml/blob/4.10/README.win32.adoc + log2 make world.opt $MAKE_OPT + log2 make flexlink.opt $MAKE_OPT + log2 make install $MAKE_OPT # Move license files and other into into special folder if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then @@ -1065,7 +985,6 @@ function make_ocaml { build_post fi - make_flex_dll_link } ##### OCAML EXTRA TOOLS ##### @@ -1099,7 +1018,7 @@ function make_num { function make_ocamlbuild { make_ocaml - if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then + if build_prep https://github.com/ocaml/ocamlbuild/archive 0.14.0 tar.gz 1 ocamlbuild-0.14.0; then log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib log1 make $MAKE_OPT log2 make install @@ -1112,6 +1031,7 @@ function make_ocamlbuild { function make_findlib { make_ocaml make_ocamlbuild + # Note: latest is 1.8.1 but http://projects.camlcity.org/projects/dl/findlib-1.8.1/doc/README says this is for OCaml 4.09 if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh new file mode 100644 index 0000000000..a95170a455 --- /dev/null +++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then + + elpi_CI_REF=rename-class-files + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + mtac2_CI_REF=rename-class-files + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 67becb251a..2d187f7bae 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -255,6 +255,18 @@ Conversion machines GH issue number: #9925 risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: broken long multiplication primitive integer emulation layer on 32 bits + introduced: e43b176 + impacted released versions: 8.10.0, 8.10.1, 8.10.2 + impacted development branches: 8.11 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 4e176a7 + found by: Soegtrop, Melquiond + exploit: test-suite/bugs/closed/bug_11321.v + GH issue number: #11321 + risk: critical, as any BigN computation on 32-bit architectures is wrong + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f7f2bcdcff..835c20a4f7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -47,7 +47,7 @@ let ppmind kn = pp(MutInd.debug_print kn) let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) -let ppclindex cl = pp(Classops.pr_cl_index cl) +let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) let prrecarg = function diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5a2144f996..133326523b 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Classops.cl_index -> unit +val ppclindex : Coercionops.cl_index -> unit val ppscheme : 'a Ind_tables.scheme_kind -> unit diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst new file mode 100644 index 0000000000..2815f8af8a --- /dev/null +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -0,0 +1,7 @@ +- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles + arbitrary numbers of underscores and takes in a :g:`uconstr`. In + rare cases where users were relying on :tacn:`rapply` inserting + exactly 15 underscores and no more, due to the lemma having a + completely unspecified codomain (and thus allowing for any number of + underscores), the tactic will now instead loop. (`#10760 + <https://github.com/coq/coq/pull/10760>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst new file mode 100644 index 0000000000..2832e6db61 --- /dev/null +++ b/doc/changelog/04-tactics/11288-omega+depr.rst @@ -0,0 +1,6 @@ +- **Removed:** + The undocumented ``omega with`` tactic variant has been removed, + using ``lia`` is the recommended replacement, tho the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11288 <https://github.com/coq/coq/pull/11288>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst new file mode 100644 index 0000000000..25e929e030 --- /dev/null +++ b/doc/changelog/04-tactics/11337-omega-with-depr.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated, + using ``lia`` is the recommended replacement, tho the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst new file mode 100644 index 0000000000..e73be9c642 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst @@ -0,0 +1,5 @@ +- **Changed:** + The :cmd:`Print Canonical Projections` command now can take constants and + prints only the unification rules that involve or are synthesized from given + constants (`#10747 <https://github.com/coq/coq/pull/10747>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bcdf3277ad..1424b4f3e1 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -60,7 +60,7 @@ Nonetheless, the manual has some structure that is explained below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in six +- The second part describes the proof engine. It is divided into several chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -68,8 +68,10 @@ Nonetheless, the manual has some structure that is explained below. proofs, do multiple proofs in parallel is explained in Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them - *tactics*. The language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. Examples of tactics + *tactics*. The legacy language to combine these tactics into complex proof + strategies is given in Chapter :ref:`ltac`. The currently experimental + language that will eventually replace Ltac is presented in + Chapter :ref:`ltac2`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. Finally, the |SSR| proof language is presented in Chapter :ref:`thessreflectprooflanguage`. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8caa289a47..a8d6d2632b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2075,11 +2075,13 @@ in :ref:`canonicalstructures`; here only a simple example is given. This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. -.. cmd:: Print Canonical Projections +.. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. + which it is a projection is indicated. If constants are given as + its arguments, only the unification rules that involve or are + synthesized from simultaneously all given constants will be shown. .. example:: @@ -2089,10 +2091,15 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. coqtop:: all + + Print Canonical Projections nat. + .. note:: - The last line would not show up if the corresponding projection (namely - :g:`Prf_equiv`) were annotated as not canonical, as described above. + The last line in the first example would not show up if the + corresponding projection (namely :g:`Prf_equiv`) were annotated as not + canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index cfdc70d50e..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 878118c48a..53cfb973d4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -688,6 +688,28 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28f4f5aed6..cc0c1e4602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -678,7 +678,7 @@ let remove_one_coercion inctx c = try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (match Classops.hide_coercion r with + (match Coercionops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> (* We skip the coercion *) let l = List.skipn (n - pars) args in diff --git a/interp/notation.ml b/interp/notation.ml index 5dc1658824..93969f3718 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -open Classops +open Coercionops type scope_class = cl_typ diff --git a/interp/notation.mli b/interp/notation.mli index 864e500d56..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option -val scope_class_of_class : Classops.cl_typ -> scope_class +val scope_class_of_class : Coercionops.cl_typ -> scope_class (** Building notation key *) diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index e38389ca13..445166f6af 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -15,8 +15,8 @@ let _ = assert (Sys.word_size = 32) let uint_size = 63 -let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF" -let maxuint31 = Int64.of_string "0x7FFFFFFF" +let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL +let maxuint31 = 0x7FFF_FFFFL let zero = Int64.zero let one = Int64.one @@ -118,27 +118,30 @@ let div21 xh xl y = let div21 xh xl y = if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y - (* exact multiplication *) +(* exact multiplication *) let mulc x y = - let lx = ref (Int64.logand x maxuint31) in - let ly = ref (Int64.logand y maxuint31) in + let lx = Int64.logand x maxuint31 in + let ly = Int64.logand y maxuint31 in let hx = Int64.shift_right x 31 in let hy = Int64.shift_right y 31 in - let hr = ref (Int64.mul hx hy) in - let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in - hr := (Int64.shift_right_logical !hr 1); - lx := Int64.mul !lx hy; - ly := Int64.mul hx !ly; - hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32)); - lr := Int64.add !lr (Int64.shift_left !lx 31); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - if Int64.logand !lr Int64.min_int <> 0L - then Int64.(sub !hr one, mask63 !lr) - else (!hr, !lr) - -let equal x y = mask63 x = mask63 y + (* compute the median products *) + let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in + (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *) + let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in + let hr = Int64.shift_right_logical s 31 in + (* add the outer products *) + let lr = Int64.add (Int64.mul lx ly) lr in + let hr = Int64.add (Int64.mul hx hy) hr in + (* hr fits on 64 bits, since the final result fits on 126 bits *) + (* now x * y = hr * 2^62 + lr and lr < 2^63 *) + let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in + let hr = Int64.shift_right_logical hr 1 in + (* now x * y = hr * 2^63 + lr, but lr might be too large *) + if Int64.logand lr Int64.min_int <> 0L + then Int64.add hr 1L, mask63 lr + else hr, lr + +let equal (x : t) y = x = y let compare x y = Int64.compare x y diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 734dd8ee8a..26afdcb9d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -533,6 +533,7 @@ let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) try EntryDataMap.find tag !camlp5_entries with Not_found -> EntryData.Ex String.Map.empty in + let () = assert (not @@ String.Map.mem name old) in let entries = String.Map.add name e old in camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries in diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 2f26226f4e..4e7482d4af 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,11 +18,11 @@ open Tacticals.New let update_flags ()= let open TransparentState in - let f accu coe = match coe.Classops.coe_value with + let f accu coe = match coe.Coercionops.coe_value with | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } | _ -> accu in - let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in + let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg index 84964a7bd2..7c653b223e 100644 --- a/plugins/omega/g_omega.mlg +++ b/plugins/omega/g_omega.mlg @@ -21,40 +21,9 @@ DECLARE PLUGIN "omega_plugin" { open Ltac_plugin -open Names -open Coq_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in - let tac = Tacenv.interp_ltac kn in - Tacinterp.eval_tactic tac - -let omega_tactic l = - let tacs = List.map - (function - | "nat" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) - (omega_solver) } TACTIC EXTEND omega -| [ "omega" ] -> { omega_tactic [] } +| [ "omega" ] -> { Coq_omega.omega_solver } END - -TACTIC EXTEND omega' -| [ "omega" "with" ne_ident_list(l) ] -> - { omega_tactic (List.map Names.Id.to_string l) } -| [ "omega" "with" "*" ] -> - { Tacticals.New.tclTHEN (eval_tactic "zify") (omega_tactic []) } -END - diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 9f6fe0e651..d8dbf2f3dc 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -370,14 +370,14 @@ let coerce_search_pattern_to_sort hpat = let filter_head, coe_path = try let _, cp = - Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in + Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in warn (); true, cp with _ -> false, [] in let coerce hp coe_index = - let coe_ref = coe_index.Classops.coe_value in + let coe_ref = coe_index.Coercionops.coe_value in try - let n_imps = Option.get (Classops.hide_coercion coe_ref) in + let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with Not_found | Option.IsNone -> errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f0e73bdb29..c980d204ca 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -27,7 +27,7 @@ open EConstr open Vars open Reductionops open Pretype_errors -open Classops +open Coercionops open Evarutil open Evarconv open Evd diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml index 16021b66f8..16021b66f8 100644 --- a/pretyping/classops.ml +++ b/pretyping/coercionops.ml diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli index 9f633843eb..9f633843eb 100644 --- a/pretyping/classops.mli +++ b/pretyping/coercionops.mli diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0364e1b61f..bfdb471c46 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c = (sigma, c) let path_convertible env sigma i p q = - let open Classops in + let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in @@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q = let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false -let _ = Classops.install_path_comparator path_convertible +let _ = Coercionops.install_path_comparator path_convertible diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 7e140f4399..07154d4e03 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -26,7 +26,7 @@ Constr_matching Tacred Typeclasses_errors Typeclasses -Classops +Coercionops Program Coercion Detyping diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5b416a99f9..35e182840b 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -114,7 +114,7 @@ let find_primitive_projection c = (* the effective components of a structure and the projections of the *) (* structure *) -(* Table des definitions "object" : pour chaque object c, +(* Table of "object" definitions: for each object c, c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) @@ -127,16 +127,19 @@ let find_primitive_projection c = that maps the pair (Li,ci) to the following data + o_ORIGIN = c (the constant name which this conversion rule is + synthesized from) o_DEF = c o_TABS = B1...Bk o_INJ = Some n (when ci is a reference to the parameter xi) - o_PARAMS = a1...am - o_NARAMS = m + o_TPARAMS = a1...am + o_NPARAMS = m o_TCOMP = ui1...uir *) type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -224,7 +227,7 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e8b0d771aa..aaba7cc3e5 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,6 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) diff --git a/test-suite/bugs/closed/bug_11321.v b/test-suite/bugs/closed/bug_11321.v new file mode 100644 index 0000000000..ce95280fb1 --- /dev/null +++ b/test-suite/bugs/closed/bug_11321.v @@ -0,0 +1,10 @@ +Require Import Cyclic63. + +Goal False. +Proof. +assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H. + vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63). +generalize (f_equal (zn2z_to_Z wB to_Z) H). +now rewrite mulc_WW_spec. +Fail Qed. +Abort. diff --git a/test-suite/output/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out new file mode 100644 index 0000000000..a4e2251440 --- /dev/null +++ b/test-suite/output/PrintCanonicalProjections.out @@ -0,0 +1,18 @@ +bool <- sort_eq ( bool_eqType ) +bool <- sort_TYPE ( bool_TYPE ) +nat <- sort_eq ( nat_eqType ) +nat <- sort_TYPE ( nat_TYPE ) +prod <- sort_eq ( prod_eqType ) +prod <- sort_TYPE ( prod_TYPE ) +sum <- sort_eq ( sum_eqType ) +sum <- sort_TYPE ( sum_TYPE ) +sum <- sort_TYPE ( sum_TYPE ) +prod <- sort_TYPE ( prod_TYPE ) +nat <- sort_TYPE ( nat_TYPE ) +bool <- sort_TYPE ( bool_TYPE ) +sum <- sort_eq ( sum_eqType ) +prod <- sort_eq ( prod_eqType ) +nat <- sort_eq ( nat_eqType ) +bool <- sort_eq ( bool_eqType ) +bool <- sort_TYPE ( bool_TYPE ) +bool <- sort_eq ( bool_eqType ) diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v new file mode 100644 index 0000000000..808cdffe39 --- /dev/null +++ b/test-suite/output/PrintCanonicalProjections.v @@ -0,0 +1,46 @@ +Record TYPE := Pack_TYPE { sort_TYPE :> Type }. +Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }. + +Definition eq_op (T : eqType) : T -> T -> bool := + match T with Pack_eq _ op => op end. + +Definition bool_eqb b1 b2 := + match b1, b2 with + | false, false => true + | true, true => true + | _, _ => false + end. + +Canonical bool_TYPE := Pack_TYPE bool. +Canonical bool_eqType := Pack_eq bool bool_eqb. + +Canonical nat_TYPE := Pack_TYPE nat. +Canonical nat_eqType := Pack_eq nat Nat.eqb. + +Definition prod_eqb (T U : eqType) (x y : T * U) := + match x, y with + | (x1, x2), (y1, y2) => + andb (eq_op _ x1 y1) (eq_op _ x2 y2) + end. + +Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U). +Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U). + +Definition sum_eqb (T U : eqType) (x y : T + U) := + match x, y with + | inl x, inl y => eq_op _ x y + | inr x, inr y => eq_op _ x y + | _, _ => false + end. + +Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U). +Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U). + +Print Canonical Projections bool. +Print Canonical Projections nat. +Print Canonical Projections prod. +Print Canonical Projections sum. +Print Canonical Projections sort_TYPE. +Print Canonical Projections sort_eq. +Print Canonical Projections sort_TYPE bool. +Print Canonical Projections bool_eqType. diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 470e4f0580..5e0f90d59b 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -90,5 +90,5 @@ Qed. (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. -intros; omega with *. +intros; zify; omega. Qed. diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index 17531064cc..0223255067 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -16,112 +16,112 @@ Open Scope Z_scope. Goal forall a:Z, Z.max a a = a. intros. -omega with *. +zify; omega. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -omega with *. +zify; omega. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -omega with *. +zify; omega. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -omega with *. +zify; omega. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. -intuition; subst; omega. (* pure multiplication: omega alone can't do it *) +intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *) Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -omega with *. +zify; omega. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -omega with *. +zify; omega. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -omega with *. +zify; omega. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -omega with *. +zify; omega. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -omega with *. +zify; omega. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -omega with *. +zify; omega. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -omega with *. +zify; omega. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m*m>=0)%N. intros. -omega with *. +zify; omega. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -omega with *. +zify; omega. Qed. diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v new file mode 100644 index 0000000000..e88ae65e18 --- /dev/null +++ b/test-suite/success/custom_entry.v @@ -0,0 +1,13 @@ +Declare Custom Entry foo. + +Print Custom Grammar foo. + +Notation "[ e ]" := e (e custom foo at level 0). + +Print Custom Grammar foo. + +Notation "1" := O (in custom foo at level 0). + +Print Custom Grammar foo. + +Fail Declare Custom Entry foo. diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v new file mode 100644 index 0000000000..13efd986f0 --- /dev/null +++ b/test-suite/success/rapply.v @@ -0,0 +1,27 @@ +Require Import Coq.Program.Tactics. + +(** We make a version of [rapply] that takes [uconstr]; we do not +currently test what scope [rapply] interprets terms in. *) + +Tactic Notation "urapply" uconstr(p) := rapply p. + +Ltac test n := + (*let __ := match goal with _ => idtac n end in*) + lazymatch n with + | O => let __ := match goal with _ => assert True by urapply I; clear end in + uconstr:(fun _ => I) + | S ?n' + => let lem := test n' in + let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in + uconstr:(fun _ : True => lem) + end. + +Goal True. + assert True by urapply I. + assert True by (unshelve urapply (fun _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ _ => I); try exact I). + clear. + Time let __ := test 50 in idtac. + urapply I. +Qed. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index ba8e4dff6d..c8a100b0e7 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -61,12 +61,12 @@ Ltac destruct_pairs := repeat (destruct_one_pair). Ltac destruct_one_ex := let tac H := let ph := fresh "H" in (destruct H as [H ph]) in - let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in - (destruct H as [H ph ph']) + let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in + (destruct H as [H ph ph']) in let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in - let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in - (destruct H as [H ph ph']) + let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in + (destruct H as [H ph ph']) in match goal with | [H : (ex _) |- _] => tac H @@ -140,7 +140,7 @@ Ltac clear_dups := repeat clear_dup. (** Try to clear everything except some hyp *) -Ltac clear_except hyp := +Ltac clear_except hyp := repeat match goal with [ H : _ |- _ ] => match H with | hyp => fail 1 @@ -173,22 +173,10 @@ Ltac on_application f tac T := (** A variant of [apply] using [refine], doing as much conversion as necessary. *) Ltac rapply p := - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _) || - refine (p _ _ _ _ _) || - refine (p _ _ _ _) || - refine (p _ _ _) || - refine (p _ _) || - refine (p _) || - refine p. + (** before we try to add more underscores, first ensure that adding such underscores is valid *) + (assert_succeeds (idtac; let __ := open_constr:(p _) in idtac); + rapply uconstr:(p _)) + || refine p. (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8a403e5a03..625ffb5a06 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in + let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in () let instance_of_univ_entry = function @@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name | Declare.ImportNeedQualified -> true | Declare.ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in + let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in let inst = instance_of_univ_entry univs in (gr,inst) diff --git a/vernac/class.ml b/vernac/comCoercion.ml index 3c43b125d1..56ab6f289d 100644 --- a/vernac/class.ml +++ b/vernac/comCoercion.ml @@ -18,7 +18,7 @@ open Context open Vars open Termops open Environ -open Classops +open Coercionops open Declare open Libobject @@ -231,7 +231,7 @@ let check_source = function let cache_coercion (_,c) = let env = Global.env () in let sigma = Evd.from_env env in - Classops.declare_coercion env sigma c + Coercionops.declare_coercion env sigma c let open_coercion i o = if Int.equal i 1 then diff --git a/vernac/class.mli b/vernac/comCoercion.mli index 3254d5d981..f98ef4fdd6 100644 --- a/vernac/class.mli +++ b/vernac/comCoercion.mli @@ -9,7 +9,7 @@ (************************************************************************) open Names -open Classops +open Coercionops (** Classes and coercions. *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b603c54026..8de1c69424 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes + List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b65a126f55..07656f9715 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -278,6 +278,10 @@ let find_custom_entry s = try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp) with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".") +let exists_custom_entry s = match find_custom_entry s with +| _ -> true +| exception _ -> false + let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality (* This computes the name of the level where to add a new rule *) diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index f879d51660..6768d24d5c 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -19,4 +19,7 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) val create_custom_entry : local:bool -> string -> unit + +val exists_custom_entry : string -> bool + val locality_of_custom_entry : string -> bool diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 436648c163..69ab0fafe9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram | IDENT "Coercions" -> { PrintCoercions } | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } - | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global + -> { PrintCanonicalConversions qids } | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } diff --git a/vernac/library.ml b/vernac/library.ml index 244424de6b..0f7e7d2aa0 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -430,6 +430,22 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) +let save_library_base f sum lib univs tasks proofs = + let ch = raw_extern_library f in + try + System.marshal_out_segment f ch (sum : seg_sum); + System.marshal_out_segment f ch (lib : seg_lib); + System.marshal_out_segment f ch (univs : seg_univ option); + System.marshal_out_segment f ch (tasks : 'tasks option); + System.marshal_out_segment f ch (proofs : seg_proofs); + close_out ch + with reraise -> + let reraise = CErrors.push reraise in + close_out ch; + Feedback.msg_warning (str "Removed file " ++ str f); + Sys.remove f; + iraise reraise + type ('document,'counters) todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) @@ -454,18 +470,17 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = match todo_proofs with | ProofsTodoNone -> None, None | ProofsTodoSomeEmpty _except -> - None, - Some (Univ.ContextSet.empty,false) + None, Some (Univ.ContextSet.empty,false) | ProofsTodoSome (_except, tasks, rcbackup) -> - let tasks = - List.map Stateid.(fun (r,b) -> + let tasks = + List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b with Not_found -> assert b; { r with uuid = -1 }, b) tasks in - Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false) - in - let sd = { + Some (tasks,rcbackup), + Some (Univ.ContextSet.empty,false) + in + let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); } in @@ -475,36 +490,15 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = } in if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; - (* Open the vo file and write the magic number *) - let f' = f in - let ch = raw_extern_library f' in - try - (* Writing vo payload *) - System.marshal_out_segment f' ch (sd : seg_sum); - System.marshal_out_segment f' ch (md : seg_lib); - System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (tasks : 'tasks option); - System.marshal_out_segment f' ch (opaque_table : seg_proofs); - close_out ch; - (* Writing native code files *) - if output_native_objects then - let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - Nativelib.compile_library dir ast fn - with reraise -> - let reraise = CErrors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in - let () = close_out ch in - let () = Sys.remove f' in - iraise reraise + (* Writing vo payload *) + save_library_base f sd md utab tasks opaque_table; + (* Writing native code files *) + if output_native_objects then + let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in + Nativelib.compile_library dir ast fn let save_library_raw f sum lib univs proofs = - let ch = raw_extern_library f in - System.marshal_out_segment f ch (sum : seg_sum); - System.marshal_out_segment f ch (lib : seg_lib); - System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : 'tasks option); - System.marshal_out_segment f ch (proofs : seg_proofs); - close_out ch + save_library_base f sum lib (Some univs) None proofs module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 35681aed13..222e9eb825 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1654,10 +1654,16 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing (**********************************************************************) (* Declaration of custom entry *) +let warn_custom_entry = + CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing" + (fun s -> + strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.") + let load_custom_entry _ _ = () let open_custom_entry _ (_,(local,s)) = - Egramcoq.create_custom_entry ~local s + if Egramcoq.exists_custom_entry s then warn_custom_entry s + else Egramcoq.create_custom_entry ~local s let cache_custom_entry o = load_custom_entry 1 o; @@ -1677,4 +1683,7 @@ let inCustomEntry : locality_flag * string -> obj = classify_function = classify_custom_entry} let declare_custom_entry local s = - Lib.add_anonymous_leaf (inCustomEntry (local,s)) + if Egramcoq.exists_custom_entry s then + user_err Pp.(str "Custom entry " ++ str s ++ str " already exists") + else + Lib.add_anonymous_leaf (inCustomEntry (local,s)) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 1742027076..a1bd99c237 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function keyword "Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t - | PrintCanonicalConversions -> - keyword "Print Canonical Structures" + | PrintCanonicalConversions qids -> + keyword "Print Canonical Structures" ++ prlist pr_smart_global qids | PrintTypingFlags -> keyword "Print Typing Flags" | PrintTables -> diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index eb7b28f15b..8ced35c3be 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -199,7 +199,7 @@ let print_opacity ref = (*******************) let print_if_is_coercion ref = - if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] (*******************) (* *) @@ -951,7 +951,7 @@ let inspect env sigma depth = (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) -open Classops +open Coercionops let print_coercion_value v = Printer.pr_global v.coe_value @@ -965,7 +965,7 @@ let print_path ((i,j),p) = str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -let _ = Classops.install_path_printer print_path +let _ = Coercionops.install_path_printer print_path let print_graph () = prlist_with_sep fnl print_path (inheritance_graph()) @@ -996,12 +996,26 @@ let print_path_between cls clt = in print_path ((i,j),p) -let print_canonical_projections env sigma = +let print_canonical_projections env sigma grefs = + let match_proj_gref ((x,y),c) gr = + GlobRef.equal x gr || + begin match y with + | Const_cs y -> GlobRef.equal y gr + | _ -> false + end || + match gr with + | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con + | _ -> false + in + let projs = + List.filter (fun p -> List.for_all (match_proj_gref p) grefs) + (canonical_projections ()) + in prlist_with_sep fnl (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") - (canonical_projections ()) + projs (*************************************************************************) diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index dc4280f286..ac41f30c5d 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -52,8 +52,8 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t val print_graph : unit -> Pp.t val print_classes : unit -> 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 +val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t +val print_canonical_projections : env -> Evd.evar_map -> GlobRef.t list -> Pp.t (** Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> Pp.t diff --git a/vernac/record.ml b/vernac/record.ml index ea10e06d02..df9b4a0914 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let refi = GlobRef.ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; if flags.pf_subclass then begin - let cl = Class.class_of_global (GlobRef.IndRef indsp) in - Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl + let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in + ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) @@ -489,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = GlobRef.ConstructRef cstr in - let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in + let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 5226c2ba65..7b4924eaed 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -21,7 +21,7 @@ RecLemmas Library Prettyp Lemmas -Class +ComCoercion Auto_ind_decl Search Indschemes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 439ec61d38..04f3e0d7b2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum = | Some p -> Pfedit.get_goal_context p glnum let cl_of_qualid = function - | FunClass -> Classops.CL_FUN - | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r) + | FunClass -> Coercionops.CL_FUN + | SortClass -> Coercionops.CL_SORT + | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r) let scope_class_of_qualid qid = Notation.scope_class_of_class (cl_of_qualid qid) @@ -524,11 +524,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let vernac_definition_hook ~local ~poly = let open Decls in function | Coercion -> - Some (Class.add_coercion_hook ~poly) + Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> - Some (Class.add_subclass_hook ~poly) + Some (ComCoercion.add_subclass_hook ~poly) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -1034,7 +1034,7 @@ let vernac_coercion ~atts ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target; + ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion ~atts id qids qidt = @@ -1042,7 +1042,7 @@ let vernac_identity_coercion ~atts id qids qidt = let local = enforce_locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local ~poly ~source ~target + ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target (* Type classes *) @@ -1701,7 +1701,9 @@ let vernac_print ~pstate ~atts = | PrintCoercions -> Prettyp.print_coercions () | PrintCoercionPaths (cls,clt) -> Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) - | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma + | PrintCanonicalConversions qids -> + let grefs = List.map Smartlocate.smart_global qids in + Prettyp.print_canonical_projections env sigma grefs | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) | PrintHintGoal -> diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 32ff8b8fb2..1daa244986 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -46,7 +46,7 @@ type printable = | PrintInstances of qualid or_by_notation | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr - | PrintCanonicalConversions + | PrintCanonicalConversions of qualid or_by_notation list | PrintUniverses of bool * qualid list option * string option | PrintHint of qualid or_by_notation | PrintHintGoal |