diff options
176 files changed, 1649 insertions, 2147 deletions
diff --git a/CHANGES.md b/CHANGES.md index 5ff90b5123..1f88b77b51 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -120,6 +120,10 @@ Universes - Added `Print Universes Subgraph` variant of `Print Universes`. Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` +- Added private universes for opaque polymorphic constants, see doc + for the "Private Polymorphic Universes" option (and Unset it to get + the previous behaviour). + Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. @@ -86,6 +86,7 @@ list of persons and groups: J.-P. Jouannaud, S. Lescuyer, A. Miquel, J.-F. Monin, P.-Y. Strub the Foundations Group (Radboud University, Nijmegen, The Netherlands), Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), + L. Lee (https://orcid.org/0000-0002-7128-9257, 2018), INRIA-Gallium project, the CS dept at Yale, the CIS dept at U. Penn, the CSE dept at Harvard, the CS dept at Princeton, the CS dept at MIT diff --git a/appveyor.yml b/appveyor.yml index c9c6bc0684..7420856214 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -2,8 +2,7 @@ version: '{branch}~{build}' clone_depth: 10 cache: - - C:\cygwin64 -> dev\ci\appveyor.bat - - C:\cygwin64\home\appveyor\.opam -> dev\ci\appveyor.sh + - C:\cygwin64 -> dev\ci\appveyor.bat, dev\ci\appveyor.sh platform: - x64 diff --git a/checker/check.ml b/checker/check.ml index e3a4bda8ec..30437e8bd0 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -136,36 +136,9 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p let find_logical_path phys_dir = - let phys_dir = canonical_path_name phys_dir in + let phys_dir = CUnix.canonical_path_name phys_dir in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir @@ -180,14 +153,14 @@ let add_load_path (phys_path,coq_path) = if !Flags.debug then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); - let phys_path = canonical_path_name phys_path in + let phys_path = CUnix.canonical_path_name phys_path in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_path) physical logical with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = canonical_path_name Filename.current_dir_name + (phys_path = CUnix.canonical_path_name Filename.current_dir_name && coq_path = default_root_prefix) then begin diff --git a/checker/checker.ml b/checker/checker.ml index 346ae5fffb..da6a61de1c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -138,13 +138,16 @@ let set_debug () = Flags.debug := true let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet -let engage = Safe_typing.set_engagement (!impredicative_set) -let disable_compilers senv = +let indices_matter = ref false + +let make_senv () = + let senv = Safe_typing.empty_environment in + let senv = Safe_typing.set_engagement !impredicative_set senv in + let senv = Safe_typing.set_indices_matter !indices_matter senv in let senv = Safe_typing.set_VM false senv in Safe_typing.set_native_compiler false senv - let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list @@ -318,6 +321,9 @@ let parse_args argv = | "-impredicative-set" :: rem -> set_impredicative_set (); parse rem + | "-indices-matter" :: rem -> + indices_matter:=true; parse rem + | "-coqlib" :: s :: rem -> if not (exists_dir s) then fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; @@ -377,8 +383,7 @@ let init_with_argv argv = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); - let senv = Safe_typing.empty_environment in - disable_compilers (engage senv) + make_senv () with e -> fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 77f4cea0c6..b83fe831bb 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -19,7 +19,13 @@ let check_constant_declaration env kn cb = | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in - true, push_context ~strict:false ctx env + let env = push_context ~strict:false ctx env in + true, env + in + let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with + | None, _ -> env' + | Some local, (OpaqueDef _, true) -> push_subgraph local env' + | Some _, _ -> assert false in let ty = cb.const_type in let _ = infer_type env' ty in diff --git a/checker/values.ml b/checker/values.ml index 0de8a3e03f..dcb2bca81a 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -217,7 +217,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] @@ -227,6 +227,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; + Opt v_context_set; v_bool; v_typing_flags|] diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d52bd39d72..8d728b5b51 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -146,16 +146,16 @@ let print_local fmt ext = fprintf fmt "in@ " let print_position fmt pos = match pos with -| First -> fprintf fmt "Extend.First" -| Last -> fprintf fmt "Extend.Last" -| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s -| After s -> fprintf fmt "Extend.After@ \"%s\"" s -| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s +| First -> fprintf fmt "Gramlib.Gramext.First" +| Last -> fprintf fmt "Gramlib.Gramext.Last" +| Before s -> fprintf fmt "Gramlib.Gramext.Before@ \"%s\"" s +| After s -> fprintf fmt "Gramlib.Gramext.After@ \"%s\"" s +| Level s -> fprintf fmt "Gramlib.Gramext.Level@ \"%s\"" s let print_assoc fmt = function -| LeftA -> fprintf fmt "Extend.LeftA" -| RightA -> fprintf fmt "Extend.RightA" -| NonA -> fprintf fmt "Extend.NonA" +| LeftA -> fprintf fmt "Gramlib.Gramext.LeftA" +| RightA -> fprintf fmt "Gramlib.Gramext.RightA" +| NonA -> fprintf fmt "Gramlib.Gramext.NonA" let is_token s = match string_split s with | [s] -> is_uident s diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d0b5f4be47..b202635714 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1905,6 +1905,9 @@ function make_addon_quickchick { function make_addons { # Note: ':' is the empty command, which does not produce any output : > "/build/filelists/addon_dependencies.nsh" + : > "/build/filelists/addon_strings.nsh" + : > "/build/filelists/addon_descriptions.nsh" + : > "/build/filelists/addon_sections.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index abeb039c0e..cda369fb1b 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,14 +2,15 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c +APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c -wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH -eval "$(opam config env)" +opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" opam install -y num ocamlfind ounit +# Full regular Coq Build cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 918d289ae2..386a3de204 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -39,6 +39,10 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\ IF "%WINDOWS%" == "enabled_all_addons" (
SET EXTRA_ADDONS=^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
-addon=mathcomp ^
-addon=menhir ^
-addon=menhirlib ^
@@ -56,10 +60,6 @@ IF "%WINDOWS%" == "enabled_all_addons" ( call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon=bignums ^
- -addon=equations ^
- -addon=ltac2 ^
- -addon=mtac2 ^
%EXTRA_ADDONS% ^
-make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md new file mode 100644 index 0000000000..1685b084e9 --- /dev/null +++ b/dev/ci/nix/README.md @@ -0,0 +1,19 @@ +# Working on third-party developments with *this* version of Coq + +Aim: getting an environment suitable for working on a third-party development +using the current version of Coq (i.e., built from the current state of this +repository). + +Dive into such an environment, for the project `example` by running, from the +root of this repository: + + ./dev/ci/nix/shell example + +This will build Coq and the other dependencies of the `example` project, then +open a shell with all these dependencies available (e.g., `coqtop` is in path). + +Additionally, three environment variables are set, to abstract over the +build-system of that project: `configure`, `make`, and `clean`. Therefore, after +changing the working directory to the root of the sources of that project, the +contents of these variables can be evaluated to respectively set-up, build, and +clean the project. diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix index f10afd5680..093c262cde 100644 --- a/dev/ci/nix/unicoq.nix +++ b/dev/ci/nix/unicoq.nix @@ -1,11 +1,8 @@ -{ stdenv, fetchzip, coq }: +{ stdenv, coq }: stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; - src = fetchzip { - url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz"; - sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il"; - }; + src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh new file mode 100644 index 0000000000..482792d7cd --- /dev/null +++ b/dev/ci/user-overlays/08850-poly-local-univs.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then + formal_topology_CI_REF=poly-local-univs + formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology + + paramcoq_CI_REF=poly-local-univs + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh new file mode 100644 index 0000000000..2df8affd14 --- /dev/null +++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then + + elpi_CI_REF=ltac+remove_aliases + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/doc/about-hints b/dev/doc/about-hints deleted file mode 100644 index 95712c3cf9..0000000000 --- a/dev/doc/about-hints +++ /dev/null @@ -1,454 +0,0 @@ -An investigation of how ZArith lemmas could be classified in different -automation classes - -- Reversible lemmas relating operators (to be declared as hints but - needing precedences) -- Equivalent notions (one has to be considered as primitive and the - other rewritten into the canonical one) -- Isomorphisms between structure (one structure has to be considered - as more primitive than the other for a give operator) -- Irreversible simplifications (to be declared with precedences) -- Reversible bottom-up simplifications (to be used in hypotheses) -- Irreversible bottom-up simplifications (to be used in hypotheses - with precedences) -- Rewriting rules (relevant for autorewrite, or for an improved auto) - -Note: this analysis, made in 2001, was previously stored in -theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating -the standard library. - -(**********************************************************************) -(** * Reversible lemmas relating operators *) -(** Probably to be declared as hints but need to define precedences *) - -(** ** Conversion between comparisons/predicates and arithmetic operators *) - -(** Lemmas ending by eq *) -(** -<< -Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` -Zabs_eq: (x:Z)`0 <= x`->`|x| = x` -Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` -Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` -Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` -Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` -Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` -Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` -Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` -Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` -Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` ->> -*) - -(** ** Conversion between nat comparisons and Z comparisons *) - -(** Lemmas ending by eq *) -(** -<< -inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` ->> -*) - -(** ** Conversion between comparisons *) - -(** Lemmas ending by Zge *) -(** -<< -not_Zlt: (x,y:Z)~`x < y`->`x >= y` -Zle_ge: (m,n:Z)`m <= n`->`n >= m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` -not_Zle: (x,y:Z)~`x <= y`->`x > y` -Zlt_gt: (m,n:Z)`m < n`->`n > m` -Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -not_Zge: (x,y:Z)~`x >= y`->`x < y` -Zgt_lt: (m,n:Z)`m > n`->`n < m` -Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` -not_Zgt: (x,y:Z)~`x > y`->`x <= y` -Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` -Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` -Zge_le: (m,n:Z)`m >= n`->`n <= m` -Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` -Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` -Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` -Zle_refl: (n,m:Z)`n = m`->`n <= m` ->> -*) - -(** ** Irreversible simplification involving several comparaisons *) -(** useful with clear precedences *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` -Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` ->> -*) - -(** ** What is decreasing here ? *) - -(** Lemmas ending by eq *) -(** -<< -Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` ->> -*) - -(**********************************************************************) -(** * Useful Bottom-up lemmas *) - -(** ** Bottom-up simplification: should be used *) - -(** Lemmas ending by eq *) -(** -<< -Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` -Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` -Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` -Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` -Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` -Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` -Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` -Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` ->> -*) - -(** Lemmas ending by Zle *) -(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` -Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` -Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) - -(** ** Bottom-up irreversible (syntactic) simplification *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` ->> -*) - -(** ** Other unclearly simplifying lemmas *) - -(** Lemmas ending by Zeq *) -(** -<< -Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` ->> -*) - -(* Lemmas ending by Zgt *) -(** -<< -Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` ->> -*) - -(* Lemmas ending by Zlt *) -(** -<< -pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` ->> -*) - -(* Lemmas ending by Zle *) -(** -<< -Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` -OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` ->> -*) - - -(**********************************************************************) -(** * Irreversible lemmas with meta-variables *) -(** To be used by EAuto *) - -(* Hints Immediate *) -(** Lemmas ending by eq *) -(** -<< -Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` -Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` -Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` -Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` -Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` -Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` ->> -*) - - -(**********************************************************************) -(** * Unclear or too specific lemmas *) -(** Not to be used ? *) - -(** ** Irreversible and too specific (not enough regular) *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` -Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` -OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` -OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` ->> -*) - -(** ** Expansion and too specific ? *) - -(** Lemmas ending by Zge *) -(** -<< -Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` -Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` -Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` ->> -*) - -(** ** Reversible but too specific ? *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` ->> -*) - -(**********************************************************************) -(** * Lemmas to be used as rewrite rules *) -(** but can also be used as hints *) - -(** Left-to-right simplification lemmas (a symbol disappears) *) - -(** -<< -Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) -Zmin_n_n: (n:Z)`(Zmin n n) = n` -Zmult_1_n: (n:Z)`1*n = n` -Zmult_n_1: (n:Z)`n*1 = n` -Zminus_plus: (n,m:Z)`n+m-n = m` -Zle_plus_minus: (n,m:Z)`n+(m-n) = m` -Zopp_Zopp: (x:Z)`(-(-x)) = x` -Zero_left: (x:Z)`0+x = x` -Zero_right: (x:Z)`x+0 = x` -Zplus_inverse_r: (x:Z)`x+(-x) = 0` -Zplus_inverse_l: (x:Z)`(-x)+x = 0` -Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` -Zmult_one: (x:Z)`1*x = x` -Zero_mult_left: (x:Z)`0*x = 0` -Zero_mult_right: (x:Z)`x*0 = 0` -Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` ->> -*) - -(** Right-to-left simplification lemmas (a symbol disappears) *) - -(** -<< -Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` -Zs_pred: (n:Z)`n = (Zs (Zpred n))` -Zplus_n_O: (n:Z)`n = n+0` -Zmult_n_O: (n:Z)`0 = n*0` -Zminus_n_O: (n:Z)`n = n-0` -Zminus_n_n: (n:Z)`0 = n-n` -Zred_factor6: (x:Z)`x = x+0` -Zred_factor0: (x:Z)`x = x*1` ->> -*) - -(** Unclear orientation (no symbol disappears) *) - -(** -<< -Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` -Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` -Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` -Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` -Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` -Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` -Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` -Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` -Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` -Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` -Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` -Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` -Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` -Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` -Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` -Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` -Zplus_sym: (x,y:Z)`x+y = y+x` -Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` -Zmult_sym: (x,y:Z)`x*y = y*x` -Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` -Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` -Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` -Zopp_one: (x:Z)`(-x) = x*(-1)` -Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` -Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` -Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` -Zred_factor1: (x:Z)`x+x = x*2` -Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` -Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` -Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` -Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` -Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` ->> -*) - -(** nat <-> Z *) -(** -<< -inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` -inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` -inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` -inj_minus1: - (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` -inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` ->> -*) - -(** Too specific ? *) -(** -<< -Zred_factor5: (x,y:Z)`x*0+y = y` ->> -*) diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd deleted file mode 100644 index cc33efd483..0000000000 --- a/dev/doc/cic.dtd +++ /dev/null @@ -1,231 +0,0 @@ -<?xml encoding="ISO-8859-1"?> - -<!-- DTD FOR CIC OBJECTS: --> - -<!-- CIC term declaration --> - -<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| - LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> - -<!-- CIC sorts --> - -<!ENTITY % sort '(Prop|Set|Type)'> - -<!-- CIC sequents --> - -<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> - -<!-- CIC objects: --> - -<!ELEMENT ConstantType %term;> -<!ATTLIST ConstantType - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT ConstantBody %term;> -<!ATTLIST ConstantBody - for CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT CurrentProof (Conjecture*,body)> -<!ATTLIST CurrentProof - of CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT InductiveDefinition (InductiveType+)> -<!ATTLIST InductiveDefinition - noParams NMTOKEN #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Variable (body?,type)> -<!ATTLIST Variable - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Sequent %sequent;> -<!ATTLIST Sequent - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!-- Elements used in CIC objects, which are not terms: --> - -<!ELEMENT InductiveType (arity,Constructor*)> -<!ATTLIST InductiveType - name CDATA #REQUIRED - inductive (true|false) #REQUIRED> - -<!ELEMENT Conjecture %sequent;> -<!ATTLIST Conjecture - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Constructor %term;> -<!ATTLIST Constructor - name CDATA #REQUIRED> - -<!ELEMENT Decl %term;> -<!ATTLIST Decl - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Def %term;> -<!ATTLIST Def - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Hidden EMPTY> -<!ATTLIST Hidden - id ID #REQUIRED> - -<!ELEMENT Goal %term;> - -<!-- CIC terms: --> - -<!ELEMENT LAMBDA (decl*,target)> -<!ATTLIST LAMBDA - sort %sort; #REQUIRED> - -<!ELEMENT LETIN (def*,target)> -<!ATTLIST LETIN - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT PROD (decl*,target)> -<!ATTLIST PROD - type %sort; #REQUIRED> - -<!ELEMENT CAST (term,type)> -<!ATTLIST CAST - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT REL EMPTY> -<!ATTLIST REL - value NMTOKEN #REQUIRED - binder CDATA #REQUIRED - id ID #REQUIRED - idref IDREF #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT SORT EMPTY> -<!ATTLIST SORT - value CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT APPLY (%term;)+> -<!ATTLIST APPLY - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT VAR EMPTY> -<!ATTLIST VAR - relUri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- The substitutions are ordered by increasing de Bruijn --> -<!-- index. An empty substitution means that that index is --> -<!-- not accessible. --> -<!ELEMENT META (substitution*)> -<!ATTLIST META - no NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT IMPLICIT EMPTY> -<!ATTLIST IMPLICIT - id ID #REQUIRED> - -<!ELEMENT CONST EMPTY> -<!ATTLIST CONST - uri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTIND EMPTY> -<!ATTLIST MUTIND - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT MUTCONSTRUCT EMPTY> -<!ATTLIST MUTCONSTRUCT - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - noConstr NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> -<!ATTLIST MUTCASE - uriType CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT FIX (FixFunction+)> -<!ATTLIST FIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT COFIX (CofixFunction+)> -<!ATTLIST COFIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- Elements used in CIC terms: --> - -<!ELEMENT FixFunction (type,body)> -<!ATTLIST FixFunction - name CDATA #REQUIRED - recIndex NMTOKEN #REQUIRED> - -<!ELEMENT CofixFunction (type,body)> -<!ATTLIST CofixFunction - name CDATA #REQUIRED> - -<!ELEMENT substitution ((%term;)?)> - -<!-- Explicit named substitutions: --> - -<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)> -<!ATTLIST instantiate - id ID #IMPLIED> - -<!-- Sintactic sugar for CIC terms and for CIC objects: --> - -<!ELEMENT arg %term;> -<!ATTLIST arg - relUri CDATA #REQUIRED> - -<!ELEMENT decl %term;> -<!ATTLIST decl - id ID #REQUIRED - type %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT def %term;> -<!ATTLIST def - id ID #REQUIRED - sort %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT target %term;> - -<!ELEMENT term %term;> - -<!ELEMENT type %term;> - -<!ELEMENT arity %term;> - -<!ELEMENT patternsType %term;> - -<!ELEMENT inductiveTerm %term;> - -<!ELEMENT pattern %term;> - -<!ELEMENT body %term;> diff --git a/dev/doc/minicoq.tex b/dev/doc/minicoq.tex deleted file mode 100644 index a34b03a491..0000000000 --- a/dev/doc/minicoq.tex +++ /dev/null @@ -1,98 +0,0 @@ -\documentclass{article} - -\usepackage{fullpage} -\input{./macros.tex} -\newcommand{\minicoq}{\textsf{minicoq}} -\newcommand{\nonterm}[1]{\textit{#1}} -\newcommand{\terminal}[1]{\textsf{#1}} -\newcommand{\listzero}{\textit{LIST$_0$}} -\newcommand{\listun}{\textit{LIST$_1$}} -\newcommand{\sep}{\textit{SEP}} - -\title{Minicoq: a type-checker for the pure \\ - Calculus of Inductive Constructions} - - -\begin{document} - -\maketitle - -\section{Introduction} - -\minicoq\ is a minimal toplevel for the \Coq\ kernel. - - -\section{Grammar of terms} - -The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - term & ::= & identifier \\ - & $|$ & \terminal{Rel} integer \\ - & $|$ & \terminal{Set} \\ - & $|$ & \terminal{Prop} \\ - & $|$ & \terminal{Type} \\ - & $|$ & \terminal{Const} identifier \\ - & $|$ & \terminal{Ind} identifier integer \\ - & $|$ & \terminal{Construct} identifier integer integer \\ - & $|$ & \terminal{[} name \terminal{:} term - \terminal{]} term \\ - & $|$ & \terminal{(} name \terminal{:} term - \terminal{)} term \\ - & $|$ & term \verb!->! term \\ - & $|$ & \terminal{(} \listun\ term \terminal{)} \\ - & $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\ - & $|$ & \verb!<! term \verb!>! \terminal{Case} - term \terminal{of} \listzero\ term \terminal{end} - \\[1em] - name & ::= & \verb!_! \\ - & $|$ & identifier - \end{tabular} - \end{center} - \hrulefill - \caption{Grammar of terms} - \label{fig:terms} -\end{figure} - -\section{Commands} -The grammar of \minicoq's commands are given in -Figure~\ref{fig:commands}. All commands end with a dot. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\ - & $|$ & \terminal{Definition} identifier \terminal{:} term - \terminal{:=} term. \\ - & $|$ & \terminal{Parameter} identifier \terminal{:} term. \\ - & $|$ & \terminal{Variable} identifier \terminal{:} term. \\ - & $|$ & \terminal{Inductive} \terminal{[} \listzero\ param - \terminal{]} \listun\ inductive \sep\ - \terminal{with}. \\ - & $|$ & \terminal{Check} term. - \\[1em] - param & ::= & identifier - \\[1em] - inductive & ::= & identifier \terminal{:} term \terminal{:=} - \listzero\ constructor \sep\ \terminal{$|$} - \\[1em] - constructor & ::= & identifier \terminal{:} term - \end{tabular} - \end{center} - \hrulefill - \caption{Commands} - \label{fig:commands} -\end{figure} - - -\end{document} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/dev/doc/transition-V5.10-V6 b/dev/doc/transition-V5.10-V6 deleted file mode 100644 index df7b65dd8b..0000000000 --- a/dev/doc/transition-V5.10-V6 +++ /dev/null @@ -1,5 +0,0 @@ -The V5.10 archive has been created with cvs in February 1995 by -Jean-Christophe Filliâtre. It was moved to archive V6 in March 1996. -At this occasion, the contrib directory (user-contributions) were -moved to a separate directory and some theories (like ALGEBRA) moved -to the user-contributions directory too. diff --git a/dev/doc/transition-V6-V7 b/dev/doc/transition-V6-V7 deleted file mode 100644 index e477c9ff9d..0000000000 --- a/dev/doc/transition-V6-V7 +++ /dev/null @@ -1,8 +0,0 @@ -The V6 archive has been created in March 1996 with files from the -former V5.10 archive and has been abandoned in 2000. - -A new archive named V7 has been created in August 1999 by -Jean-Christophe Filliâtre with a new architecture placing the -type-checking at the kernel of Coq. This new architecture came with a -"cleaner" organization of files, a uniform indentation style, uniform -headers, etc. diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4287702b3a..b90a53220d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -20,13 +20,12 @@ open Univ open Environ open Printer open Constr -open Goptions open Genarg open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true -let _ = set_bool_option_value ["Printing";"Matching"] false +let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c8fb4bd00e..789890eab5 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -285,19 +285,21 @@ Activating the Printing of Coercions Classes as Records ------------------ +.. index:: :> (coercion) + We allow the definition of *Structures with Inheritance* (or classes as records) by extending the existing :cmd:`Record` macro. Its new syntax is: .. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` + The first identifier :token:`ident` is the name of the defined record and + :token:`sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be :n:`Build_@ident` if not given). + The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform + field type. Note that the fields always verify the uniform inheritance condition. If the optional ``>`` is given before the record name, then the constructor name is automatically declared as a coercion from the class of the last field type to the record name diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index cc8870e2e4..e153c7cbe2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -102,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern matching if a return or in clause is specified. Likewise, the +pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -118,8 +118,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in: else S (pred n). The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not -produce an equality, contrary to the let pattern construct :g:`let ’(x1, -..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for example: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 15a55d9e72..98dfcb2373 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -228,6 +228,8 @@ mechanism if available, as shown in the example. Substructures ~~~~~~~~~~~~~ +.. index:: :> (substructure) + Substructures are components of a class which are instances of a class themselves. They often arise when using classes for logical properties, e.g.: @@ -260,6 +262,12 @@ preorder can be used instead. This is very similar to the coercion mechanism of ``Structure`` declarations. The implementation simply declares each projection as an instance. +.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class + + Using this ``:>`` syntax with a right-hand-side that is not itself a Class + has no effect (apart from emitting this warning). In particular, is does not + declare a coercion. + One can also declare existing objects or structure projections using the Existing Instance command to achieve the same effect. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 99b883d23c..04aedd0cf6 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -443,3 +443,60 @@ underscore or by omitting the annotation to a polymorphic definition. semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been defined. This is meant mainly for debugging purposes. + +.. flag:: Private Polymorphic Universes + + This option, on by default, removes universes which appear only in + the body of an opaque polymorphic definition from the definition's + universe arguments. As such, no value needs to be provided for + these universes when instanciating the definition. Universe + constraints are automatically adjusted. + + Consider the following definition: + + .. coqtop:: all + + Lemma foo@{i} : Type@{i}. + Proof. exact Type. Qed. + Print foo. + + The universe :g:`Top.xxx` for the :g:`Type` in the body cannot be accessed, we + only care that one exists for any instantiation of the universes + appearing in the type of :g:`foo`. This is guaranteed when the + transitive constraint ``Set <= Top.xxx < i`` is verified. Then when + using the constant we don't need to put a value for the inner + universe: + + .. coqtop:: all + + Check foo@{_}. + + and when not looking at the body we don't mention the private + universe: + + .. coqtop:: all + + About foo. + + To recover the same behaviour with regard to universes as + :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + be unset: + + .. coqtop:: all + + Unset Private Polymorphic Universes. + + Lemma bar : Type. Proof. exact Type. Qed. + About bar. + Fail Check bar@{_}. + Check bar@{_ _}. + + Note that named universes are always public. + + .. coqtop:: all + + Set Private Polymorphic Universes. + Unset Strict Universe Declaration. + + Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. + About baz. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 65df89da6c..1c53f5981d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1380,147 +1380,147 @@ Numeral notations .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. :name: Numeral Notation - This command allows the user to customize the way numeral literals - are parsed and printed. + 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: + 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` + * :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: + 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` + * :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. + 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). + .. 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. + 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). + .. 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. + 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 + .. 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. + 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)}. + .. 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. + 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)}. + .. 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. + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @type is not an inductive type. + .. exn:: @type is not an inductive type. - Numeral notations can only be declared for inductive types with no - arguments. + Numeral notations can only be declared for inductive types with no + arguments. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. 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. + 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. + .. 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. + 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. + .. 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. + 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. + 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]). + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`Numeral Notation` must be a single - identifier. + The type passed to :cmd:`Numeral Notation` must be a single + identifier. - .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`Numeral Notation` must be single - identifiers. + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. - .. exn:: The reference @ident was not found in the current environment. + .. exn:: The reference @ident was not found in the current environment. - Identifiers passed to :cmd:`Numeral Notation` must exist in the - global 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. + .. 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. + 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). + .. 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`. + 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. + .. 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. + 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 + For example - .. coqtop:: all + .. coqtop:: all - Check 90000. + Check 90000. - .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + .. 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. + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: diff --git a/engine/namegen.ml b/engine/namegen.ml index db72dc8ec3..a67ff6965b 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -208,25 +208,18 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (* Introduce a mode where auto-generated names are mangled to test dependence of scripts on auto-generated names *) -let mangle_names = ref false - -let _ = Goptions.( - declare_bool_option - { optdepr = false; - optname = "mangle auto-generated names"; - optkey = ["Mangle";"Names"]; - optread = (fun () -> !mangle_names); - optwrite = (:=) mangle_names; }) +let get_mangle_names = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"mangle auto-generated names" + ~key:["Mangle";"Names"] + ~value:false let mangle_names_prefix = ref (Id.of_string "_0") -let set_prefix x = mangle_names_prefix := forget_subscript x -let set_mangle_names_mode x = begin - set_prefix x; - mangle_names := true - end +let set_prefix x = mangle_names_prefix := forget_subscript x -let _ = Goptions.( +let () = Goptions.( declare_string_option { optdepr = false; optname = "mangled names prefix"; @@ -238,7 +231,7 @@ let _ = Goptions.( with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) end }) -let mangle_id id = if !mangle_names then !mangle_names_prefix else id +let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/namegen.mli b/engine/namegen.mli index a53c3a0d1f..3722cbed24 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed : val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t - -val set_mangle_names_mode : Id.t -> unit -(** Turn on mangled names mode and with the given prefix. - @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/uState.ml b/engine/uState.ml index 5747ae2ad4..6aecc368e6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -441,11 +441,13 @@ let restrict_universe_context (univs, csts) keep = if LSet.is_empty removed then univs, csts else let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in - let g = UGraph.empty_universes in - let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.initial_universes in + let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in let g = UGraph.merge_constraints csts g in - let allkept = LSet.diff allunivs removed in + let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in + let csts = Constraint.filter (fun (l,d,r) -> + not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -575,25 +577,33 @@ let add_global_univ uctx u = uctx_universes = univs } let make_flexible_variable ctx ~algebraic u = - let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if algebraic then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - let has_upper_constraint () = - Univ.Constraint.exists - (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) - (Univ.ContextSet.constraints cstrs) - in - if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) - then Univ.LSet.add u avars else avars - else avars - in - {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'} + let open Univ in + let {uctx_local = cstrs; uctx_univ_variables = uvars; + uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in + assert (try LMap.find u uvars == None with Not_found -> true); + match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with + | Some v -> + let uvars' = LMap.add u (Some (Universe.make v)) uvars in + { ctx with uctx_univ_variables = uvars'; } + | None -> + let uvars' = LMap.add u None uvars in + let avars' = + if algebraic then + let uu = Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v + in + let has_upper_constraint () = + Constraint.exists + (fun (l,d,r) -> d == Lt && Level.equal l u) + (ContextSet.constraints cstrs) + in + if not (LMap.exists substu_not_alg uvars || has_upper_constraint ()) + then LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} let make_nonalgebraic_variable ctx u = { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } diff --git a/engine/univMinim.ml b/engine/univMinim.ml index f10e6d2ec1..e20055b133 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -12,17 +12,12 @@ open Univ open UnivSubst (* To disallow minimization to Set *) -let set_minimization = ref true -let is_set_minimization () = !set_minimization - -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = is_set_minimization; - optwrite = (:=) set_minimization }) - +let get_set_minimization = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"minimization to Set" + ~key:["Universe";"Minimization";"ToSet"] + ~value:true (** Simplification *) @@ -278,7 +273,7 @@ let normalize_context_set g ctx us algs weak = let smallles, csts = Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts in - let smallles = if is_set_minimization () + let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles else Constraint.empty in diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 43a70ca13b..c35c4bd18e 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -55,8 +55,6 @@ type position = | Like of string | Level of string -let warning_verbose = ref true - let rec derive_eps = function Slist0 _ -> true @@ -96,7 +94,7 @@ let is_before s1 s2 = | Stoken _, _ -> true | _ -> false -let insert_tree entry_name gsymbols action tree = +let insert_tree ~warning entry_name gsymbols action tree = let rec insert symbols tree = match symbols with s :: sl -> insert_in_tree s sl tree @@ -105,14 +103,16 @@ let insert_tree entry_name gsymbols action tree = Node {node = s; son = son; brother = bro} -> Node {node = s; son = son; brother = insert [] bro} | LocAct (old_action, action_list) -> - if !warning_verbose then - begin - eprintf "<W> Grammar extension: "; - if entry_name <> "" then eprintf "in [%s], " entry_name; - eprintf "some rule has been masked\n"; - flush stderr - end; - LocAct (action, old_action :: action_list) + begin match warning with + | None -> () + | Some warn_fn -> + let msg = + "<W> Grammar extension: " ^ + (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ + "some rule has been masked" in + warn_fn msg + end; + LocAct (action, old_action :: action_list) | DeadEnd -> LocAct (action, []) and insert_in_tree s sl tree = match try_insert s sl tree with @@ -141,10 +141,10 @@ let insert_tree entry_name gsymbols action tree = in insert gsymbols tree -let srules rl = +let srules ~warning rl = let t = List.fold_left - (fun tree (symbols, action) -> insert_tree "" symbols action tree) + (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) DeadEnd rl in Stree t @@ -175,15 +175,15 @@ and token_exists_in_symbol f = | Stree t -> token_exists_in_tree f t | Snterm _ | Snterml (_, _) | Snext | Sself -> false -let insert_level entry_name e1 symbols action slev = +let insert_level ~warning entry_name e1 symbols action slev = match e1 with true -> {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree entry_name symbols action slev.lsuffix; + lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix; lprefix = slev.lprefix} | false -> {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree entry_name symbols action slev.lprefix} + lprefix = insert_tree ~warning entry_name symbols action slev.lprefix} let empty_lev lname assoc = let assoc = @@ -193,27 +193,33 @@ let empty_lev lname assoc = in {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev lev n lname assoc = +let change_lev ~warning lev n lname assoc = let a = match assoc with None -> lev.assoc | Some a -> - if a <> lev.assoc && !warning_verbose then - begin - eprintf "<W> Changing associativity of level \"%s\"\n" n; - flush stderr - end; + if a <> lev.assoc then + begin + match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Changing associativity of level \""^n^"\"") + end; a in begin match lname with Some n -> - if lname <> lev.lname && !warning_verbose then - begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end + if lname <> lev.lname then + begin match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Level label \""^n^"\" ignored") + end; | None -> () end; {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} -let get_level entry position levs = +let get_level ~warning entry position levs = match position with Some First -> [], empty_lev, levs | Some Last -> levs, empty_lev, [] @@ -226,7 +232,7 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if is_level_labelled n lev then [], change_lev lev n, levs + if is_level_labelled n lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in @@ -268,14 +274,14 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if token_exists_in_level f lev then [], change_lev lev n, levs + if token_exists_in_level f lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in get levs | None -> match levs with - lev :: levs -> [], change_lev lev "<top>", levs + lev :: levs -> [], change_lev ~warning lev "<top>", levs | [] -> [], empty_lev, [] let rec check_gram entry = @@ -347,7 +353,7 @@ let insert_tokens gram symbols = in List.iter insert symbols -let levels_of_rules entry position rules = +let levels_of_rules ~warning entry position rules = let elev = match entry.edesc with Dlevels elev -> elev @@ -358,7 +364,7 @@ let levels_of_rules entry position rules = in if rules = [] then elev else - let (levs1, make_lev, levs2) = get_level entry position elev in + let (levs1, make_lev, levs2) = get_level ~warning entry position elev in let (levs, _) = List.fold_left (fun (levs, make_lev) (lname, assoc, level) -> @@ -370,7 +376,7 @@ let levels_of_rules entry position rules = List.iter (check_gram entry) symbols; let (e1, symbols) = get_initial entry symbols in insert_tokens entry.egram symbols; - insert_level entry.ename e1 symbols action lev) + insert_level ~warning entry.ename e1 symbols action lev) lev level in lev :: levs, empty_lev) diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index 8361e21645..ecb95ec61b 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -53,15 +53,14 @@ type position = | Like of string | Level of string -val levels_of_rules : +val levels_of_rules : warning:(string -> unit) option -> 'te g_entry -> position option -> (string option * g_assoc option * ('te g_symbol list * g_action) list) list -> 'te g_level list -val srules : ('te g_symbol list * g_action) list -> 'te g_symbol + +val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : 'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list - -val warning_verbose : bool ref diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index dfce26a33a..285c14ec62 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -755,9 +755,9 @@ let init_entry_functions entry = let f = continue_parser_of_entry entry in entry.econtinue <- f; f lev bp a strm) -let extend_entry entry position rules = +let extend_entry ~warning entry position rules = try - let elev = Gramext.levels_of_rules entry position rules in + let elev = Gramext.levels_of_rules ~warning entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry with Plexing.Error s -> Printf.eprintf "Lexer initialization error:\n- %s\n" s; @@ -841,8 +841,6 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () -let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer - (* Functorial interface *) module type GLexerType = sig type te val lexer : te Plexing.lexer end @@ -881,7 +879,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -889,10 +887,9 @@ module type S = val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> @@ -945,7 +942,7 @@ module GMake (L : GLexerType) = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t) + let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t) let r_stop = [] let r_next r s = r @ [s] let production @@ -953,15 +950,12 @@ module GMake (L : GLexerType) = Obj.magic p module Unsafe = struct - let gram_reinit = gram_reinit gram let clear_entry = clear_entry end - let extend = extend_entry - let safe_extend e pos + let safe_extend ~warning e pos (r : (string option * Gramext.g_assoc option * Obj.t ty_production list) list) = - extend e pos (Obj.magic r) - let delete_rule e r = delete_rule (Entry.obj e) r - let safe_delete_rule = delete_rule + extend_entry ~warning e pos (Obj.magic r) + let safe_delete_rule e r = delete_rule (Entry.obj e) r end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 1e14e557bc..0c585a7c0d 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -53,7 +53,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -62,10 +62,9 @@ module type S = module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 8c4649fc39..0793a1cc1c 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -37,9 +37,8 @@ let reroute_stdout_stderr () = Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr -(* We also provide specific kill and interrupt functions. *) +(* We also provide a specific interrupt function. *) -external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c index c09bf37dee..f430c9f2b6 100644 --- a/ide/ide_win32_stubs.c +++ b/ide/ide_win32_stubs.c @@ -4,22 +4,6 @@ #include <caml/memory.h> #include <windows.h> -/* Win32 emulation of kill -9 */ - -/* The pid returned by Unix.create_process is actually a pseudo-pid, - made via a cast of the obtained HANDLE, (cf. win32unix/createprocess.c - in the sources of ocaml). Since we're still in the caller process, - we simply cast back to get an handle... - The 0 is the exit code we want for the terminated process. -*/ - -CAMLprim value win32_kill(value pseudopid) { - CAMLparam1(pseudopid); - TerminateProcess((HANDLE)(Long_val(pseudopid)), 0); - CAMLreturn(Val_unit); -} - - /* Win32 emulation of a kill -2 (SIGINT) */ /* This code rely of the fact that coqide is now without initial console. diff --git a/ide/idetop.ml b/ide/idetop.ml index 8cb02190e6..a2b85041e8 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -537,5 +537,5 @@ let islave_init ~opts extra_args = let () = let open Coqtop in - let custom = { init = islave_init; run = loop; } in + let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in start_coq custom diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d5f0b7bff6..3a4969a3ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -604,15 +604,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" (str "This expression should be coercible to a pattern.")) c -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - (** Local universe and constraint declarations. *) let interp_univ_constraints env evd cstrs = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9e83bde8b2..7f14eb4583 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -127,9 +127,6 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation - (** For cases pattern parsing errors *) val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -(** Placeholder for global option, should be moved to a parameter *) -val asymmetric_patterns : bool ref - (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 70ce6cef19..25f2526f74 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -193,17 +193,12 @@ let without_specific_symbols l = (* Control printing of records *) (* Set Record Printing flag *) -let record_print = ref true - -let _ = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "record printing"; - optkey = ["Printing";"Records"]; - optread = (fun () -> !record_print); - optwrite = (fun b -> record_print := b) } - +let get_record_print = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"record printing" + ~key:["Printing";"Records"] + ~value:true let is_record indsp = try @@ -431,7 +426,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in - if !asymmetric_patterns then + if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -469,7 +464,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -489,7 +484,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns then l2 + let l2' = if Constrintern.get_asymmetric_patterns () then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args @@ -824,7 +819,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !record_print then + else if not (get_record_print ()) then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 02db8f6aab..6313f2d7ba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1488,6 +1488,12 @@ let is_non_zero_pat c = match c with | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p) | _ -> false +let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"no parameters in constructors" + ~key:["Asymmetric";"Patterns"] + ~value:false + let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) @@ -1562,7 +1568,7 @@ let drop_notations_pattern looked_for genv = | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = - if !asymmetric_patterns then pl else + if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with @@ -1684,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv ntnvars aliases' p | RCPatCstr (head, expl_pl, pl) -> - if !asymmetric_patterns then + if get_asymmetric_patterns () then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 147a903fe2..035e4bc644 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -197,3 +197,6 @@ val parsing_explicit : bool ref (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(** Placeholder for global option, should be moved to a parameter *) +val get_asymmetric_patterns : unit -> bool diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 7e73609996..1f61bcae2e 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -300,7 +300,7 @@ and fterm = | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * fconstr + | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr @@ -584,9 +584,12 @@ let rec to_constr lfts v = let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in let f = subst_constr (subs_liftn len subs) f in Term.compose_lam (List.rev tys) f - | FProd (n,t,c) -> - mkProd (n, to_constr lfts t, - to_constr (el_lift lfts) c) + | FProd (n, t, c, e) -> + if is_subs_id e && is_lift_id lfts then + mkProd (n, to_constr lfts t, c) + else + let subs' = comp_subs lfts e in + mkProd (n, to_constr lfts t, subst_constr (subs_lift subs') c) | FLetIn (n,b,t,f,e) -> let subs = comp_subs (el_lift lfts) (subs_lift e) in mkLetIn (n, to_constr lfts b, @@ -869,7 +872,7 @@ and knht info e t stk = | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk | Prod (n, t, c) -> - { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk + { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk | LetIn (n,b,t,c) -> { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk @@ -992,8 +995,8 @@ and norm_head info tab m = | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) - | FProd(na,dom,rng) -> - mkProd(na, kl info tab dom, kl info tab rng) + | FProd(na,dom,rng,e) -> + mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng)) | FCoFix((n,(na,tys,bds)),e) -> let ftys = Array.Fun1.map mk_clos e tys in let fbds = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index b6c87b3732..c2d53eed47 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -114,7 +114,7 @@ type fterm = | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * fconstr + | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr diff --git a/kernel/cooking.ml b/kernel/cooking.ml index b39aed01e8..f4b4834d98 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -158,6 +158,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } @@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 = else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in - let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in + let substf = Univ.make_instance_subst subst in + let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = @@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in + let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints + (Univ.make_instance_subst usubst))) + cb.const_private_poly_univs + in { cook_body = body; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; } diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 6ebe691b83..7ff4b657d3 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,6 +21,7 @@ type result = { cook_body : constant_def; cook_type : types; cook_universes : constant_universes; + cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; } diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c1b38b4156..016b63be09 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -61,13 +61,27 @@ type constant_universes = of a constant are tracked in their {!constant_body} so that they can be displayed to the user. *) type typing_flags = { - check_guarded : bool; (** If [false] then fixed points and co-fixed - points are assumed to be total. *) - check_universes : bool; (** If [false] universe constraints are not checked *) - conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) - share_reduction : bool; (** Use by-need reduction algorithm *) - enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *) - enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *) + check_guarded : bool; + (** If [false] then fixed points and co-fixed points are assumed to + be total. *) + + check_universes : bool; + (** If [false] universe constraints are not checked *) + + conv_oracle : Conv_oracle.oracle; + (** Unfolding strategies for conversion *) + + share_reduction : bool; + (** Use by-need reduction algorithm *) + + enable_VM : bool; + (** If [false], all VM conversions fall back to interpreted ones *) + + enable_native_compiler : bool; + (** If [false], all native conversions fall back to VM ones *) + + indices_matter: bool; + (** The universe of an inductive type must be above that of its indices. *) } (* some contraints are in constant_constraints, some other may be in @@ -78,6 +92,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; + const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3ed599c538..707c46048b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -24,6 +24,7 @@ let safe_flags oracle = { share_reduction = true; enable_VM = true; enable_native_compiler = true; + indices_matter = true; } (** {6 Arities } *) @@ -101,6 +102,7 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; + const_private_poly_univs = cb.const_private_poly_univs; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -126,14 +128,20 @@ let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> Monomorphic_const (Univ.hcons_universe_context_set ctx) - | Polymorphic_const ctx -> + | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) +let hcons_const_private_univs = function + | None -> None + | Some univs -> Some (Univ.hcons_universe_context_set univs) + let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; - const_universes = hcons_const_universes cb.const_universes } + const_universes = hcons_const_universes cb.const_universes; + const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; + } (** {6 Inductive types } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 019c0a6819..38a428d9a1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -241,6 +241,8 @@ let is_impredicative_set env = let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded +let indices_matter env = env.env_typing_flags.indices_matter + let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context @@ -380,6 +382,18 @@ let add_universes_set strict ctx g = let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env +let push_subgraph (levels,csts) env = + let add_subgraph g = + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = UGraph.merge_constraints csts newg in + (if not (Univ.Constraint.is_empty csts) then + let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in + (if not (UGraph.check_constraints restricted g) then + CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints."))); + newg + in + map_universes add_subgraph env + let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } @@ -389,6 +403,7 @@ let same_flags { check_guarded; check_universes; conv_oracle; + indices_matter; share_reduction; enable_VM; enable_native_compiler; @@ -396,6 +411,7 @@ let same_flags { check_guarded == alt.check_guarded && check_universes == alt.check_universes && conv_oracle == alt.conv_oracle && + indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && enable_native_compiler == alt.enable_native_compiler diff --git a/kernel/environ.mli b/kernel/environ.mli index c285f907fc..8a2efb2477 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -96,6 +96,7 @@ val typing_flags : env -> typing_flags val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool +val indices_matter : env -> bool (** is the local context empty *) val empty_context : env -> bool @@ -268,6 +269,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env +val push_subgraph : Univ.ContextSet.t -> env -> env +(** [push_subgraph univs env] adds the universes and constraints in + [univs] to [env] as [push_context_set ~strict:false univs env], and + also checks that they do not imply new transitive constraints + between pre-existing universes in [env]. *) + val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 20c90bc05a..a4a02791b4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -35,14 +35,6 @@ env_ar_par = env_ar + declaration of parameters nmr = ongoing computation of recursive parameters *) -(* Tell if indices (aka real arguments) contribute to size of inductive type *) -(* If yes, this is compatible with the univalent model *) - -let indices_matter = ref false - -let enforce_indices_matter () = indices_matter := true -let is_indices_matter () = !indices_matter - (* [weaker_noccur_between env n nvars t] (defined above), checks that no de Bruijn indices between [n] and [n+nvars] occur in [t]. If some such occurrences are found, then reduction is performed @@ -303,7 +295,7 @@ let typecheck_inductive env mie = let inflev = (* The level of the inductive includes levels of indices if in indices_matter mode *) - if !indices_matter + if indices_matter env then Some (cumulate_arity_large_levels env_params sign) else None in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index a827c17683..840e23ed69 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -50,8 +50,3 @@ val check_positivity : chkpos:bool -> (** The following function does checks on inductive declarations. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body - -(** The following enforces a system compatible with the univalent model *) - -val enforce_indices_matter : unit -> unit -val is_indices_matter : unit -> bool diff --git a/kernel/modops.ml b/kernel/modops.ml index 0dde1c7e75..f43dbd88f9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver = | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with - const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index fbb481424f..97cd4c00d7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -438,14 +438,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv - | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> + | (FProd (_, c1, c2, e), FProd (_, c'1, c'2, e')) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv + ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 83d890b628..df9e253135 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -196,6 +196,9 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_indices_matter indices_matter senv = + set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv + let set_share_reduction b senv = let flags = Environ.typing_flags senv.env in set_typing_flags { flags with share_reduction = b } senv @@ -609,7 +612,7 @@ let inline_side_effects env body side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _auctx -> + | Polymorphic_const _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 7af773e3bc..57b01f15e3 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,6 +136,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 +val set_indices_matter : bool -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 val set_share_reduction : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 35fa871b4e..f9fdbdd68e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; + cook_private_univs = None; cook_inline = false; cook_context = ctx; } @@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = Monomorphic_const univs; + cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let body, ctx', _ = handle env body side_eff in body, Univ.ContextSet.union ctx ctx' in - let env, usubst, univs = match c.const_entry_universes with + let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx + env, Univ.empty_level_subst, Monomorphic_const ctx, None | Polymorphic_const_entry (nas, uctx) -> - (** Ensure not to generate internal constraints in polymorphic mode. - The only way for this to happen would be that either the body - contained deferred universes, or that it contains monomorphic - side-effects. The first property is ruled out by upper layers, - and the second one is ensured by the fact we currently - unconditionally export side-effects from polymorphic definitions, - i.e. [trust] is always [Pure]. *) - let () = assert (Univ.ContextSet.is_empty ctx) in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - env, sbst, Polymorphic_const auctx + let env, local = + if opaque then + push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) + else + if Univ.ContextSet.is_empty ctx then env, None + else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + in + env, sbst, Polymorphic_const auctx, local in let j = infer env body in let typ = match typ with @@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -277,6 +281,7 @@ let build_constant_declaration _kn env result = const_type = typ; const_body_code = tps; const_universes = univs; + const_private_poly_univs = result.cook_private_univs; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c8fd83c8a9..c9acd168e8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -151,28 +151,41 @@ let type_of_abstraction _env name var ty = let make_judgev c t = Array.map2 make_judge c t +let rec check_empty_stack = function +| [] -> true +| CClosure.Zupdate _ :: s -> check_empty_stack s +| _ -> false + let type_of_apply env func funt argsv argstv = + let open CClosure in let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - + let infos = create_clos_infos all env in + let tab = create_tab () in + let rec apply_rec i typ = + if Int.equal i len then term_of_fconstr typ + else + let typ, stk = whd_stack infos tab typ [] in + (** The return stack is known to be empty *) + let () = assert (check_empty_stack stk) in + match fterm_of typ with + | FProd (_, c1, c2, e) -> + let arg = argsv.(i) in + let argt = argstv.(i) in + let c1 = term_of_fconstr c1 in + begin match conv_leq false env argt c1 with + | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2) + | exception NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv) + end | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv) + in + apply_rec 0 (inject funt) (* Type of product *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9083156745..afdc8f1511 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -866,6 +866,23 @@ let constraints_for ~kept g = arc.ltle csts) kept csts +let domain g = LMap.domain g.entries + +let choose p g u = + let exception Found of Level.t in + let ru = (repr g u).univ in + if p ru then Some ru + else + try LMap.iter (fun v -> function + | Canonical _ -> () (* we already tried [p ru] *) + | Equiv v' -> + let rv = (repr g v').univ in + if rv == ru && p v then raise (Found v) + (* NB: we could also try [p v'] but it will come up in the + rest of the iteration regardless. *) + ) g.entries; None + with Found v -> Some v + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index a2cc5b3116..4dbfac5c73 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -73,12 +73,19 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option +(** [choose p g u] picks a universe verifying [p] and equal + to [u] in [g]. *) + (** [constraints_for ~kept g] returns the constraints about the universes [kept] in [g] up to transitivity. eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) val constraints_for : kept:LSet.t -> t -> Constraint.t +val domain : t -> LSet.t +(** Known universes *) + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/lib/flags.ml b/lib/flags.ml index 3aef5a7b2c..ae4d337ded 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -123,8 +123,5 @@ let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) let output_native_objects = ref false -(* Print the mod uid associated to a vo file by the native compiler *) -let print_mod_uid = ref false - let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index e282d4ca8c..d883cf1e30 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,8 +119,6 @@ val default_inline_level : int (** When producing vo objects, also compile the native-code version *) val output_native_objects : bool ref -(** Print the mod uid associated to a vo file by the native compiler *) -val print_mod_uid : bool ref - +(** Global profile_ltac flag *) val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/library/global.ml b/library/global.ml index 4ea5969a6f..67b00cf411 100644 --- a/library/global.ml +++ b/library/global.ml @@ -88,6 +88,7 @@ let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) diff --git a/library/global.mli b/library/global.mli index 01ee695c49..40962e21af 100644 --- a/library/global.mli +++ b/library/global.mli @@ -29,6 +29,7 @@ val named_context : unit -> Constr.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit +val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit val typing_flags : unit -> Declarations.typing_flags diff --git a/library/goptions.ml b/library/goptions.ml index 154b863fa1..98efb512ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -276,10 +276,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab; - write - -type 'a write_function = 'a -> unit + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab let declare_int_option = declare_option @@ -302,6 +299,18 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + (* 3- User accessible commands *) (* Setting values of options *) @@ -425,6 +434,3 @@ let print_tables () = (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () - - - diff --git a/library/goptions.mli b/library/goptions.mli index 3d7df18fed..b91553bf3c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,17 +122,18 @@ type 'a option_sig = { (** The [preprocess] function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value. *) -type 'a write_function = 'a -> unit - val declare_int_option : ?preprocess:(int option -> int option) -> - int option option_sig -> int option write_function + int option option_sig -> unit val declare_bool_option : ?preprocess:(bool -> bool) -> - bool option_sig -> bool write_function + bool option_sig -> unit val declare_string_option: ?preprocess:(string -> string) -> - string option_sig -> string write_function + string option_sig -> unit val declare_stringopt_option: ?preprocess:(string option -> string option) -> - string option option_sig -> string option write_function + string option option_sig -> unit +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 5caeab535a..050ed49622 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -14,17 +14,8 @@ type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e type side = Left | Right -type gram_assoc = NonA | RightA | LeftA - -type gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type production_position = - | BorderProd of side * gram_assoc option + | BorderProd of side * Gramlib.Gramext.g_assoc option | InternalProd type production_level = @@ -116,11 +107,11 @@ type 'a production_rule = type 'a single_extend_statement = string option * (** Level *) - gram_assoc option * + Gramlib.Gramext.g_assoc option * (** Associativity *) 'a production_rule list (** Symbol list with the interpretation function *) type 'a extend_statement = - gram_position option * + Gramlib.Gramext.position option * 'a single_extend_statement list diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index d8c08803b6..fc5feba58b 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -32,7 +32,7 @@ type grammar_constr_prod_item = type one_notation_grammar = { notgram_level : level; - notgram_assoc : Extend.gram_assoc option; + notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; } diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 170df6ad09..816a02a6aa 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,8 +14,6 @@ open Extend open Genarg open Gramlib -let uncurry f (x,y) = f x y - (** Location Utils *) let ploc_file_of_coq_file = function | Loc.ToplevelInput -> "" @@ -82,7 +80,6 @@ module type S = end *) - type 'a entry = 'a Entry.e type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable @@ -91,12 +88,10 @@ module type S = val comment_state : coq_parsable -> ((int * int) * string) list -end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct +end with type 'a Entry.e = 'a Extend.entry = struct include Grammar.GMake(CLexer) - type 'a entry = 'a Entry.e - type coq_parsable = parsable * CLexer.lexer_state ref let coq_parsable ?(file=Loc.ToplevelInput) c = @@ -146,20 +141,6 @@ struct end -let warning_verbose = Gramext.warning_verbose - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - module Symbols : sig val stoken : Tok.t -> ('s, string) G.ty_symbol val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol @@ -184,12 +165,6 @@ end = struct let slist1sep x y = G.s_list1sep x y false end -let camlp5_verbosity silent f x = - let a = !warning_verbose in - warning_verbose := silent; - f x; - warning_verbose := a - (** Grammar extensions *) (** NB: [extend_statement = @@ -218,7 +193,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol | Anext -> G.s_next | Aentry e -> G.s_nterm e | Aentryl (e, n) -> G.s_nterml e n -| Arules rs -> G.s_rules (List.map symbol_of_rules rs) +| Arules rs -> + let warning msg = Feedback.msg_warning Pp.(str msg) in + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function | Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) @@ -240,10 +217,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> a any_productio AnyProduction (symb, cast act) let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + (lvl, assoc, List.map of_coq_production_rule rule) let of_coq_extend_statement (pos, st) = - (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (pos, List.map of_coq_single_extend_statement st) let fix_extend_statement (pos, st) = let fix_single_extend_statement (lvl, assoc, rules) = @@ -253,19 +230,19 @@ let fix_extend_statement (pos, st) = (pos, List.map fix_single_extend_statement st) (** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () -module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end +module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) - | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind (** The list of extensions *) @@ -282,13 +259,12 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let a = of_coq_assoc a in - let ext = of_coq_position ext in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in - (G.safe_extend e) (Some ext) [Some lev,Some a,[]] + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -296,15 +272,15 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let ext = fix_extend_statement ext in - let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in + let pos, ext = fix_extend_statement ext in + let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - let ext = fix_extend_statement (of_coq_extend_statement ext) in - camlp5_verbosity false (uncurry (G.safe_extend e)) ext + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -352,14 +328,16 @@ let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in let act = fun _ x loc -> x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = G.r_next G.r_stop (G.s_nterm en) in let act = fun x loc -> f x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e (* Parse a string, does NOT check if the entire string was read @@ -489,7 +467,8 @@ let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in - let () = G.safe_extend entry None ext in + let warning msg = Feedback.msg_warning Pp.(str msg) in + let () = G.safe_extend ~warning:(Some warning) entry None ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -542,7 +521,7 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty @@ -574,7 +553,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e64c614149..69ba57d516 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -26,7 +26,7 @@ sig end module Entry : sig - type 'a t = 'a Grammar.GMake(CLexer).Entry.e + type 'a t = 'a Extend.entry val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit @@ -110,10 +110,6 @@ end *) -(** Temporarily activate camlp5 verbosity *) - -val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit - (** Parse a string *) val parse_string : 'a Entry.t -> string -> 'a @@ -202,7 +198,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) val grammar_extend : 'a Entry.t -> gram_reinit option -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index a6f432b5bd..575d964158 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -33,7 +33,7 @@ let print_constr t = let debug x = if !cc_verbose then Feedback.msg_debug (x ()) -let _= +let () = let gdopt= { optdepr=false; optname="Congruence Verbose"; @@ -61,7 +61,7 @@ module ST=struct type t = {toterm: int IntPairTable.t; tosign: (int * int) IntTable.t} - let empty ()= + let empty () = {toterm=IntPairTable.create init_size; tosign=IntTable.create init_size} @@ -321,7 +321,7 @@ let compress_path uf i j = uf.map.(j).cpath<-i let rec find_aux uf visited i= let j = uf.map.(i).cpath in - if j<0 then let _ = List.iter (compress_path uf i) visited in i else + if j<0 then let () = List.iter (compress_path uf i) visited in i else find_aux uf (i::visited) j let find uf i= find_aux uf [] i diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f6eea3c5c4..16890ea260 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -500,7 +500,7 @@ let info_file f = let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in - let _ = declare_bool_option + let () = declare_bool_option {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; @@ -572,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n let optims () = !opt_flag_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} -let _ = declare_int_option +let () = declare_int_option { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; @@ -593,7 +593,7 @@ let _ = declare_int_option let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; @@ -605,7 +605,7 @@ let _ = declare_bool_option let file_comment_ref = ref "" let file_comment () = !file_comment_ref -let _ = declare_string_option +let () = declare_string_option {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index a212d13453..37fc81ee38 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -33,7 +33,7 @@ DECLARE PLUGIN "ground_plugin" let ground_depth=ref 3 -let _= +let ()= let gdopt= { optdepr=false; optname="Firstorder Depth"; @@ -47,7 +47,7 @@ let _= declare_int_option gdopt -let _= +let ()= let congruence_depth=ref 100 in let gdopt= { optdepr=true; (* noop *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1cf952576d..5ba9735690 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,7 +322,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b68b34ca35..c864bfe9f7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -375,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig = optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } -let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true @@ -388,7 +388,7 @@ let function_debug_sig = optwrite = (fun b -> function_debug := b) } -let _ = declare_bool_option function_debug_sig +let () = declare_bool_option function_debug_sig let do_observe () = !function_debug @@ -406,7 +406,7 @@ let strict_tcc_sig = optwrite = (fun b -> strict_tcc := b) } -let _ = declare_bool_option strict_tcc_sig +let () = declare_bool_option strict_tcc_sig exception Building_graph of exn diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fa70235975..0509d6ae71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Genintern open Tacexpr open Names open Constrexpr @@ -28,22 +29,22 @@ val wit_natural : int Genarg.uniform_genarg_type val wit_glob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lglob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lconstr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val wit_casted_constr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val glob : constr_expr Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 7fb9a19a0c..4576562634 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -14,4 +14,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) -val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic +val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 338839ee96..d9b19c1ae6 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -373,7 +373,7 @@ open Libnames let print_info_trace = ref None -let _ = declare_int_option { +let () = declare_int_option { optdepr = false; optname = "print info trace"; optkey = ["Info" ; "Level"]; diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index f7375a0f01..31fb1c9abf 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -16,6 +16,7 @@ open Names open Locus open Constrexpr open Glob_term +open Genintern open Geninterp open Extraargs open Tacmach @@ -37,8 +38,8 @@ DECLARE PLUGIN "ltac_plugin" { type constr_expr_with_bindings = constr_expr with_bindings -type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings -type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings +type glob_constr_with_bindings = glob_constr_and_expr with_bindings +type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = let _, env = Pfedit.get_current_context () in @@ -70,7 +71,7 @@ END { type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 50cfb6d004..55e58187b0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -26,6 +26,7 @@ open Pputils open Ppconstr open Printer +open Genintern open Tacexpr open Tacarg open Tactics diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6c09e447a5..0ab9e501bc 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -17,6 +17,7 @@ open Names open Environ open Constrexpr open Notation_gram +open Genintern open Tacexpr open Tactypes diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3eb049dbab..ae4b53325f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -446,7 +446,7 @@ let do_print_results_at_close () = let _ = Declaremods.append_end_library_hook do_print_results_at_close -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 4f46e78c71..2457b265f0 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -13,6 +13,7 @@ open Environ open EConstr open Constrexpr open Evd +open Genintern open Tactypes open Tacexpr open Tacinterp diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bdb0be03cf..0c7096a4de 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,6 +11,7 @@ open Genarg open EConstr open Constrexpr +open Genintern open Tactypes open Tacexpr diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d2ae92f6ce..b04c3b9f4e 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -53,7 +53,7 @@ val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ac2d88dec2..2aee809eb6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -119,7 +119,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 9435d0b911..2bd21f9d7a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -93,19 +93,8 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +268,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 1527724420..0c27f3bfe2 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -92,20 +92,8 @@ type ml_tactic_entry = { } (** Composite types *) - -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +267,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 178f6af71d..978ad4dd24 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,6 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr +open Genintern open Tactypes (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cb3a0aaed9..c4d8072ba5 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2039,7 +2039,7 @@ let _ = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -2048,7 +2048,7 @@ let _ = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index f9883e4441..d9c80bb835 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } +open Genintern + val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index d406686c56..4487604dca 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,6 +11,7 @@ open Tacexpr open Mod_subst open Genarg +open Genintern open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 877d4ee758..99b9e881f6 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -89,7 +89,7 @@ let batch = ref false open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Ltac batch debug"; diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 175341df09..91e8510b92 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 0722c68783..457c4e0b9a 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -35,7 +35,7 @@ val match_term : Environ.env -> Evd.evar_map -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic (** [match_goal env sigma hyps concl rules] matches the goal @@ -48,5 +48,5 @@ val match_goal: Evd.evar_map -> EConstr.named_context -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 561bfc5d7c..19256e054d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,7 +65,7 @@ let assoc_flags ist : tauto_flags = let negation_unfolding = ref true open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "unfolding of not in intuition"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 402e8b91e6..d4bafe773f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -51,7 +51,7 @@ let get_lra_option () = -let _ = +let () = let int_opt l vref = { @@ -89,11 +89,11 @@ let _ = optwrite = (fun x -> Certificate.dump_file := x) } in - let _ = declare_bool_option solver_opt in - let _ = declare_stringopt_option dump_file_opt in - let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let _ = declare_bool_option lia_enum_opt in + let () = declare_bool_option solver_opt in + let () = declare_stringopt_option dump_file_opt in + let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in + let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in + let () = declare_bool_option lia_enum_opt in () diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d8adb17710..dff25b3a42 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -64,7 +64,7 @@ let write f x = f:=x open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega system time displaying flag"; @@ -72,7 +72,7 @@ let _ = optread = read display_system_flag; optwrite = write display_system_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega action display flag"; @@ -80,7 +80,7 @@ let _ = optread = read display_action_flag; optwrite = write display_action_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega old style flag"; @@ -88,7 +88,7 @@ let _ = optread = read old_style_flag; optwrite = write old_style_flag } -let _ = +let () = declare_bool_option { optdepr = true; optname = "Omega automatic reset of generated names"; @@ -96,7 +96,7 @@ let _ = optread = read reset_flag; optwrite = write reset_flag } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Omega takes advantage of context variables with body"; diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3de5923968..aab1e47555 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -54,7 +54,7 @@ let opt_pruning= optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} -let _ = declare_bool_option opt_pruning +let () = declare_bool_option opt_pruning type form= Atom of int diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 840a05e02b..e66fa10d5b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -236,7 +236,7 @@ let opt_verbose= optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} -let _ = declare_bool_option opt_verbose +let () = declare_bool_option opt_verbose let check = ref false @@ -247,7 +247,7 @@ let opt_check= optread=(fun () -> !check); optwrite=(fun b -> check:=b)} -let _ = declare_bool_option opt_check +let () = declare_bool_option opt_check open Pp @@ -255,7 +255,7 @@ let rtauto_tac gls= Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; let gamma={next=1;env=[]} in let gl=pf_concl gls in - let _= + let () = if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in @@ -267,7 +267,7 @@ let rtauto_tac gls= | Tactic_debug.DebugOn 0 -> Search.debug_depth_first | _ -> Search.depth_first in - let _ = + let () = begin reset_info (); if !verbose then @@ -279,7 +279,7 @@ let rtauto_tac gls= with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -287,7 +287,7 @@ let rtauto_tac gls= Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in - let _ = step_count := 0; node_count := 0 in + let () = step_count := 0; node_count := 0 in let main = mkApp (force node_count l_Reflect, [|build_env gamma; build_form formula; @@ -295,7 +295,7 @@ let rtauto_tac gls= let term= applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -314,7 +314,7 @@ let rtauto_tac gls= else Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in - let _ = + let () = if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then Feedback.msg_info (str "Internal tactic executed in " ++ diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index a786b9953d..bb8a0faf2e 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -47,7 +47,7 @@ type ssrdocc = ssrclear option * ssrocc (* OLD ssr terms *) type ssrtermkind = char (* FIXME, make algebraic *) -type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr +type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e25c93bf0a..824827e90c 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -146,7 +146,7 @@ val interp_refine : val interp_open_constr : Tacinterp.interp_sign -> Goal.goal Evd.sigma -> - Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) + Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : Goal.goal Evd.sigma -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 22475fef34..490e8fbdbc 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -32,13 +32,13 @@ open Tacticals open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect 1.3 compatibility flag"; - Goptions.optkey = ["SsrOldRewriteGoalsOrder"]; - Goptions.optread = (fun _ -> !ssroldreworder); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssroldreworder := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect 1.3 compatibility flag"; + optkey = ["SsrOldRewriteGoalsOrder"]; + optread = (fun _ -> !ssroldreworder); + optdepr = false; + optwrite = (fun b -> ssroldreworder := b) }) (** The "simpl" tactic *) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f67cf20e49..8cebe62e16 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -66,14 +66,14 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let _ = - Goptions.declare_bool_option - { Goptions.optname = "have type classes"; - Goptions.optkey = ["SsrHave";"NoTCResolution"]; - Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); - } +let () = + Goptions.(declare_bool_option + { optname = "have type classes"; + optkey = ["SsrHave";"NoTCResolution"]; + optread = (fun _ -> !ssrhaveNOtcresolution); + optdepr = false; + optwrite = (fun b -> ssrhaveNOtcresolution := b); + }) open Constrexpr diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 2dff0cc84f..c9221ef758 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -576,6 +576,8 @@ END { +type ssrfwdview = ast_closure_term list + let pr_ssrfwdview _ _ _ = pr_view2 } @@ -637,6 +639,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) +type ssripatrep = ssripat let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat let pr_ssripat _ _ _ = pr_ipat @@ -1605,14 +1608,14 @@ let old_tac = V82.tactic let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect identifiers"; - Goptions.optkey = ["SsrIdents"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ssr_reserved_ids); - Goptions.optwrite = (fun b -> ssr_reserved_ids := b) - } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect identifiers"; + optkey = ["SsrIdents"]; + optdepr = false; + optread = (fun _ -> !ssr_reserved_ids); + optwrite = (fun b -> ssr_reserved_ids := b) + }) let is_ssr_reserved s = let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_' @@ -1933,6 +1936,7 @@ END (* argument *) { +type ssreqid = ssripatrep option let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt () let pr_ssreqid _ _ _ = pr_eqid @@ -1987,10 +1991,12 @@ END (* the entry point parses only non-empty arguments to avoid conflicts *) (* with the basic Coq tactics. *) -(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) - { +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) + let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats @@ -2355,13 +2361,13 @@ END let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect rewrite"; - Goptions.optkey = ["SsrRewrite"]; - Goptions.optread = (fun _ -> !ssr_rw_syntax); - Goptions.optdepr = false; - Goptions.optwrite = (fun b -> ssr_rw_syntax := b) } +let () = + Goptions.(declare_bool_option + { optname = "ssreflect rewrite"; + optkey = ["SsrRewrite"]; + optread = (fun _ -> !ssr_rw_syntax); + optdepr = false; + optwrite = (fun b -> ssr_rw_syntax := b) }) let lbrace = Char.chr 123 (** Workaround to a limitation of coqpp *) diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 862a93765d..a2cbd3c9c8 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -28,10 +28,22 @@ open Ssrmatching open Ssrast open Ssrequality +type ssrfwdview = ast_closure_term list +type ssreqid = ssripat option +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +val wit_ssripatrep : ssripat Genarg.uniform_genarg_type +val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type val wit_ssrclauses : clauses Genarg.uniform_genarg_type val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type val wit_ssrhavefwdwbinders : - (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type + (Tacexpr.raw_tactic_expr fwdbinders, + Tacexpr.glob_tactic_expr fwdbinders, + Tacinterp.Value.t fwdbinders) Genarg.genarg_type +val wit_ssrhintarg : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 824666ba9c..8bf4816e99 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -119,13 +119,13 @@ and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat (* 0 cost pp function. Active only if Debug Ssreflect is Set *) let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let _ = - Goptions.declare_bool_option - { Goptions.optname = "ssreflect debugging"; - Goptions.optkey = ["Debug";"Ssreflect"]; - Goptions.optdepr = false; - Goptions.optread = (fun _ -> !ppdebug_ref == ssr_pp); - Goptions.optwrite = (fun b -> +let () = + Goptions.(declare_bool_option + { optname = "ssreflect debugging"; + optkey = ["Debug";"Ssreflect"]; + optdepr = false; + optread = (fun _ -> !ppdebug_ref == ssr_pp); + optwrite = (fun b -> Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) } + if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) let ppdebug s = !ppdebug_ref s diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 8cb0a8b463..6497b6ff98 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -896,7 +896,7 @@ let interp_rpattern s = function let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG let cpattern_of_term (c, t) ist = c, t, Some ist diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 93a8c48435..8672c55767 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -5,9 +5,7 @@ open Goal open Environ open Evd open Constr - -open Ltac_plugin -open Tacexpr +open Genintern (** ******** Small Scale Reflection pattern matching facilities ************* *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e02fb33276..fe67f5767b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -995,7 +995,7 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let use_unit_judge env evd = let j, ctx = coq_unit_judge !!env in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible evd ctx in evd', j let add_assert_false_case pb tomatch = @@ -2037,7 +2037,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = | None -> (* No type constraint: we first create a generic evar type constraint *) let src = (loc, Evar_kinds.CasesType false) in - let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible_alg ~src in + let sigma, (t, _) = Evarutil.new_type_evar !!env sigma univ_flexible ~src in sigma, t in (* First strategy: we build an "inversion" predicate, also replacing the *) (* dependencies with existential variables *) @@ -2061,7 +2061,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = | Some rtntyp -> (* We extract the signature of the arity *) let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in - let sigma, newt = new_sort_variable univ_flexible_alg sigma in + let sigma, newt = new_sort_variable univ_flexible sigma in let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl, building_arsign] diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5061aeff88..f8289f558c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -183,14 +183,11 @@ let cofixp_reducible flgs _ stk = else false -let debug_cbv = ref false -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "cbv visited constants display"; - Goptions.optkey = ["Debug";"Cbv"]; - Goptions.optread = (fun () -> !debug_cbv); - Goptions.optwrite = (fun a -> debug_cbv:=a); -} +let get_debug_cbv = Goptions.declare_bool_option_and_ref + ~depr:false + ~value:false + ~name:"cbv visited constants display" + ~key:["Debug";"Cbv"] let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp @@ -325,14 +322,14 @@ and norm_head_ref k info env stack normt = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 2c2a8fe49e..f18040accb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,16 +398,12 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic import of coercions"; - optkey = ["Automatic";"Coercions";"Import"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } +let get_automatically_import_coercions = + Goptions.declare_bool_option_and_ref + ~depr:true (* Remove in 8.8 *) + ~name:"automatic import of coercions" + ~key:["Automatic";"Coercions";"Import"] + ~value:false let cache_coercion (_, c) = let () = add_class c.coercion_source in @@ -425,7 +421,7 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if !automatically_import_coercions then + if get_automatically_import_coercions () then cache_coercion o let set_coercion_in_scope (_, c) = @@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) = let open_coercion i o = if Int.equal i 1 then begin set_coercion_in_scope o; - if not !automatically_import_coercions then + if not (get_automatically_import_coercions ()) then cache_coercion o end diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e21c2fda85..4d1d405bd7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -33,16 +33,12 @@ open Evd open Termops open Globnames -let use_typeclasses_for_conversion = ref true - -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "use typeclass resolution during conversion"; - optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; - optread = (fun () -> !use_typeclasses_for_conversion); - optwrite = (fun b -> use_typeclasses_for_conversion := b) } - ) +let get_use_typeclasses_for_conversion = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"use typeclass resolution during conversion" + ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] + ~value:true (* Typing operations dealing with coercions *) exception NoCoercion @@ -183,7 +179,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) with UnableToUnify _ -> let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in - let _ = + let () = try evdref := the_conv_x_leq env eqT eqT' !evdref with UnableToUnify _ -> raise NoSubtacCoercion in @@ -424,7 +420,7 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env evd j with | NoCoercion when not resolve_tc - || not !use_typeclasses_for_conversion -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j) | NoCoercion -> try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) @@ -534,7 +530,7 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with - | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> + | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 072ac9deed..33ced6d6e0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -138,7 +138,7 @@ open Goptions let wildcard_value = ref true let force_wildcard () = !wildcard_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; @@ -148,7 +148,7 @@ let _ = declare_bool_option let synth_type_value = ref true let synthetize_type () = !synth_type_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; @@ -158,7 +158,7 @@ let _ = declare_bool_option let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; @@ -168,7 +168,7 @@ let _ = declare_bool_option let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; @@ -178,7 +178,7 @@ let _ = declare_bool_option let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value -let _ = declare_bool_option +let () = declare_bool_option { optdepr = false; optname = "backwards-compatible printing of primitive projections"; optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; @@ -257,8 +257,7 @@ let lookup_index_as_renamed env sigma t n = let print_factorize_match_patterns = ref true -let _ = - let open Goptions in +let () = declare_bool_option { optdepr = false; optname = "factorization of \"match\" patterns in printing"; @@ -268,8 +267,7 @@ let _ = let print_allow_match_default_clause = ref true -let _ = - let open Goptions in +let () = declare_bool_option { optdepr = false; optname = "possible use of \"match\" default pattern in printing"; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f370ad7ae2..6c268de3b3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -33,14 +33,14 @@ type unify_fun = TransparentState.t -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states sent to Evarconv unification"; - Goptions.optkey = ["Debug";"Unification"]; - Goptions.optread = (fun () -> !debug_unification); - Goptions.optwrite = (fun a -> debug_unification:=a); -} + optkey = ["Debug";"Unification"]; + optread = (fun () -> !debug_unification); + optwrite = (fun a -> debug_unification:=a); +}) (*******************************************) (* Functions to deal with impossible cases *) diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 9762d0f1d9..e46d03b743 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -110,9 +110,9 @@ let rec infer_fterm cv_pb infos variances hd stk = let (_,ty,bd) = destFLambda mk_clos hd in let variances = infer_fterm CONV infos variances ty [] in infer_fterm CONV infos variances bd [] - | FProd (_,dom,codom) -> + | FProd (_,dom,codom,e) -> let variances = infer_fterm CONV infos variances dom [] in - infer_fterm cv_pb infos variances codom [] + infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) [] | FInd (ind, u) -> let variances = if Instance.is_empty u then variances diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index abf52d2893..f5e48bcd39 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,16 +105,12 @@ let search_guard ?loc env possible_indexes fixdefs = (* To force universe name declaration before use *) -let strict_universe_declarations = ref true -let is_strict_universe_declarations () = !strict_universe_declarations - -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "strict universe declaration"; - optkey = ["Strict";"Universe";"Declaration"]; - optread = is_strict_universe_declarations; - optwrite = (:=) strict_universe_declarations }) +let is_strict_universe_declarations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"strict universe declaration" + ~key:["Strict";"Universe";"Declaration"] + ~value:true (** Miscellaneous interpretation functions *) diff --git a/pretyping/program.ml b/pretyping/program.ml index bbabbefdc3..7e38c09189 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -75,7 +75,7 @@ let is_program_cases () = !program_cases open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "preferred transparency of Program obligations"; @@ -83,7 +83,7 @@ let _ = optread = get_proofs_transparency; optwrite = set_proofs_transparency; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "program cases"; @@ -91,7 +91,7 @@ let _ = optread = (fun () -> !program_cases); optwrite = (:=) program_cases } -let _ = +let () = declare_bool_option { optdepr = false; optname = "program generalized coercion"; diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e632976ae5..a57ee6e292 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,14 +29,14 @@ exception Elimconst their parameters in its stack. *) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Generate weak constraints between Irrelevant universes"; - Goptions.optkey = ["Cumulativity";"Weak";"Constraints"]; - Goptions.optread = (fun () -> not !UState.drop_weak_constraints); - Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a); -} + optkey = ["Cumulativity";"Weak";"Constraints"]; + optread = (fun () -> not !UState.drop_weak_constraints); + optwrite = (fun a -> UState.drop_weak_constraints:=not a); +}) (** Support for reduction effects *) @@ -830,14 +830,14 @@ let fix_recarg ((recindices,bodynum),_) stack = *) let debug_RAKAM = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states of the Reductionops abstract machine"; - Goptions.optkey = ["Debug";"RAKAM"]; - Goptions.optread = (fun () -> !debug_RAKAM); - Goptions.optwrite = (fun a -> debug_RAKAM:=a); -} + optkey = ["Debug";"RAKAM"]; + optread = (fun () -> !debug_RAKAM); + optwrite = (fun a -> debug_RAKAM:=a); +}) let equal_stacks sigma (x, l) (y, l') = let f_equal x y = eq_constr sigma x y in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4aea2c3db9..d732544c5c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,19 +31,12 @@ type 'a hint_info_gen = type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen -let typeclasses_unique_solutions = ref false -let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d -let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions - -open Goptions - -let _ = - declare_bool_option - { optdepr = false; - optname = "check that typeclasses proof search returns unique solutions"; - optkey = ["Typeclasses";"Unique";"Solutions"]; - optread = get_typeclasses_unique_solutions; - optwrite = set_typeclasses_unique_solutions; } +let get_typeclasses_unique_solutions = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"check that typeclasses proof search returns unique solutions" + ~key:["Typeclasses";"Unique";"Solutions"] + ~value:false let (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -434,28 +427,40 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance info local glob = +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) info local glob = let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) glob) - | None -> () + | None -> if warn then warning_not_a_class (glob, ty) let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs - (* * interface functions *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8bdac0a575..d00195678b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info option -> bool -> GlobRef.t -> unit +(** Declares the given global reference as an instance of its type. + Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — + when said type is not a registered type class. *) +val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8c1aae26ae..094fcd923e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,25 +43,25 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Unification is keyed"; - Goptions.optkey = ["Keyed";"Unification"]; - Goptions.optread = (fun () -> !keyed_unification); - Goptions.optwrite = (fun a -> keyed_unification:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Unification is keyed"; + optkey = ["Keyed";"Unification"]; + optread = (fun () -> !keyed_unification); + optwrite = (fun a -> keyed_unification:=a); +}) let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Print states sent to tactic unification"; - Goptions.optkey = ["Debug";"Tactic";"Unification"]; - Goptions.optread = (fun () -> !debug_unification); - Goptions.optwrite = (fun a -> debug_unification:=a); -} + optkey = ["Debug";"Tactic";"Unification"]; + optread = (fun () -> !debug_unification); + optwrite = (fun a -> debug_unification:=a); +}) (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 712eb21ee6..f9f4d7f7f8 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -96,8 +96,9 @@ let print_ref reduce ref udecl = then Printer.pr_universe_instance sigma inst else mt () in + let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) (********************************) (** Printing implicit arguments *) @@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs) + Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ diff --git a/printing/printer.ml b/printing/printer.ml index 4840577cbf..2bbda279bd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -34,7 +34,7 @@ let should_unfoc() = !enable_unfocused_goal_printing let should_gname() = !enable_goal_names_printing -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -45,7 +45,7 @@ let _ = (* This is set on by proofgeneral proof-tree mode. But may be used for other purposes *) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -55,7 +55,7 @@ let _ = optwrite = (fun b -> enable_goal_tags_printing:=b) } -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -140,10 +140,10 @@ let pr_cases_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) -let _ = Termops.Internal.set_print_constr +let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) -let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" +let pr_in_comment x = str "(* " ++ x ++ str " *)" (** Term printers resilient to [Nametab] errors *) @@ -199,42 +199,43 @@ let safe_pr_constr_env = safe_gen pr_constr_env let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c + fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) else mt() let pr_universe_ctx sigma ?variance c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) else mt() -let pr_abstract_universe_ctx sigma ?variance c = - if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c +let pr_abstract_universe_ctx sigma ?variance c ~priv = + let open Univ in + let priv = Option.default Univ.ContextSet.empty priv in + let has_priv = not (ContextSet.is_empty priv) in + if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then + let prlev u = Termops.pr_evd_level sigma u in + let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in + let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in + fnl()++pr_in_comment (pub ++ priv) else mt() -let pr_constant_universes sigma = function +let pr_constant_universes sigma ~priv = function | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx - | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx + | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv let pr_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi)) else mt() let pr_abstract_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi)) else mt() @@ -430,7 +431,7 @@ let pr_context_limit_compact ?n env sigma = (* If [None], no limit *) let print_hyps_limit = ref (None : int option) -let _ = +let () = let open Goptions in declare_int_option { optdepr = false; @@ -638,7 +639,7 @@ let print_evar_constraints gl sigma = let should_print_dependent_evars = ref false -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; diff --git a/printing/printer.mli b/printing/printer.mli index cefc005c74..b0232ec4ac 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -87,10 +87,10 @@ val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t -val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> - Univ.AUContext.t -> Pp.t +val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> Declarations.constant_universes -> Pp.t +val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index 2c3ab46670..a8d7b0c1a8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -41,7 +41,7 @@ type short = OnlyNames | WithContents let short = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "short module printing"; @@ -310,7 +310,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx) + Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs) | SFBmind mib -> match extent with | WithContents -> diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index cc1bcc66ae..3e2093db4a 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -52,7 +52,7 @@ let write_diffs_option = function | "removed" -> diff_option := `REMOVED | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".") -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "show diffs in proofs"; diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index 65a94a2c60..cef3fd3f5e 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -53,7 +53,7 @@ let parse_goal_selector = function with Failure _ -> CErrors.user_err Pp.(str err_msg) end -let _ = let open Goptions in +let () = let open Goptions in declare_string_option { optdepr = false; optname = "default goal selector" ; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 81122e6858..886a62cb89 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -16,18 +16,18 @@ open Environ open Evd let use_unification_heuristics_ref = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Solve unification constraints at every \".\""; - Goptions.optkey = ["Solve";"Unification";"Constraints"]; - Goptions.optread = (fun () -> !use_unification_heuristics_ref); - Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Solve unification constraints at every \".\""; + optkey = ["Solve";"Unification";"Constraints"]; + optread = (fun () -> !use_unification_heuristics_ref); + optwrite = (fun a -> use_unification_heuristics_ref:=a); +}) let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end @@ -138,7 +138,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo try let status = by tac in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in match entries with | [entry] -> discard_current (); diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index ed8df29d7b..2ca4f0afb4 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -176,7 +176,7 @@ end (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "bullet behavior"; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cb4b5759dc..095aa36f03 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -53,7 +53,7 @@ let default_proof_mode = ref (find_proof_mode "No") let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; @@ -128,13 +128,13 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -272,12 +272,12 @@ let get_used_variables () = (cur_pstate ()).section_vars let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Proof using Clear Unused"; - Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; - Goptions.optread = (fun () -> !proof_using_auto_clear); - Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Proof using Clear Unused"; + optkey = ["Proof";"Using";"Clear";"Unused"]; + optread = (fun () -> !proof_using_auto_clear); + optwrite = (fun b -> proof_using_auto_clear := b) }) let set_used_variables l = let open Context.Named.Declaration in @@ -318,10 +318,23 @@ let get_open_goals () = type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t -let close_proof ~keep_body_ucst_separate ?feedback_id ~now +let private_poly_univs = + let b = ref true in + let _ = Goptions.(declare_bool_option { + optdepr = false; + optname = "use private polymorphic universes for Qed constants"; + optkey = ["Private";"Polymorphic";"Universes"]; + optread = (fun () -> !b); + optwrite = ((:=) b); + }) + in + fun () -> !b + +let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = let { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in + let opaque = match opaque with Opaque -> true | Transparent -> false in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in @@ -358,6 +371,16 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) + else if poly && opaque && private_poly_univs () then + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let universes = UState.restrict universes used_univs in + let typus = UState.restrict universes used_univs_typ in + let udecl = UState.check_univ_decl ~poly typus universe_decl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + (udecl, typ), ((body, ubody), eff) else (* Since the proof is computed now, we can simply have 1 set of constraints in which we merge the ones for the body and the ones @@ -394,7 +417,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_feedback = feedback_id; const_entry_type = Some typ; const_entry_inline_code = false; - const_entry_opaque = true; + const_entry_opaque = opaque; const_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl initial_goals in @@ -425,10 +448,10 @@ let return_proof ?(allow_partial=false) () = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~feedback_id proof = - close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof -let close_proof ~keep_body_ucst_separate fix_exn = - close_proof ~keep_body_ucst_separate ~now:true +let close_future_proof ~opaque ~feedback_id proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof +let close_proof ~opaque ~keep_body_ucst_separate fix_exn = + close_proof ~opaque ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ())) (** Gets the current terminator without checking that the proof has @@ -467,7 +490,7 @@ let update_global_env () = (p, ()))) (* XXX: Bullet hook, should be really moved elsewhere *) -let _ = +let () = let hook n = try let prf = give_me_the_proof () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e3808bc36d..d9c32cf9d5 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -86,7 +86,7 @@ val update_global_env : unit -> unit (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -97,7 +97,7 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) val return_proof : ?allow_partial:bool -> unit -> closed_proof_output -val close_future_proof : feedback_id:Stateid.t -> +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> closed_proof_output Future.computation -> closed_proof (** Gets the current terminator without checking that the proof has diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 0981584bb5..6658c37f41 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -54,14 +54,14 @@ let strong_cbn flags = strong_with_flags whd_cbn flags let simplIsCbn = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Plug the simpl tactic to the new cbn mechanism"; - Goptions.optkey = ["SimplIsCbn"]; - Goptions.optread = (fun () -> !simplIsCbn); - Goptions.optwrite = (fun a -> simplIsCbn:=a); -} + optkey = ["SimplIsCbn"]; + optread = (fun () -> !simplIsCbn); + optwrite = (fun a -> simplIsCbn:=a); +}) let set_strategy_one ref l = let k = diff --git a/stm/stm.ml b/stm/stm.ml index 9359ab15e2..94405924b7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -27,6 +27,9 @@ open Feedback open Vernacexpr open Vernacextend +let is_vtkeep = function VtKeep _ -> true | _ -> false +let get_vtkeep = function VtKeep x -> x | _ -> assert false + module AsyncOpts = struct type cache = Force @@ -41,7 +44,6 @@ module AsyncOpts = struct async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; @@ -58,7 +60,6 @@ module AsyncOpts = struct async_proofs_mode = APoff; async_proofs_private_flags = None; - async_proofs_full = false; async_proofs_never_reopen_branch = false; async_proofs_tac_error_resilience = `Only [ "curly" ]; @@ -1439,11 +1440,14 @@ end = struct (* {{{ *) let perspective = ref [] let set_perspective l = perspective := l + let is_inside_perspective st = true + (* This code is now disabled. If an IDE needs this feature, make it accessible again. + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st + *) + let task_match age t = match age, t with - | Fresh, BuildProof { t_states } -> - not !cur_opt.async_proofs_full || - List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states + | Fresh, BuildProof { t_states } -> is_inside_perspective t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1479,8 +1483,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !cur_opt.async_proofs_full || t_drop - then `Stay(t_states,[States t_states]) + if t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> @@ -1532,12 +1535,13 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> + let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) Vernacstate.unfreeze_interp_state st; let pobject, _ = - Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in + Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in @@ -1545,7 +1549,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1680,9 +1684,10 @@ end = struct (* {{{ *) (* The original terminator, a hook, has not been saved in the .vio*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + (Lemmas.mk_hook (fun _ _ -> ()))); + let opaque = Proof_global.Opaque in let proof = - Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; @@ -1695,7 +1700,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); `OK proof end with e -> @@ -2121,8 +2126,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create - (if !cur_opt.async_proofs_full then 1 else 0)) + let init () = queue := Some (TaskQueue.create 0) end (* }}} *) @@ -2145,7 +2149,6 @@ let async_policy () = let delegate name = get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !cur_opt.async_proofs_full let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); @@ -2252,8 +2255,7 @@ let collect_proof keep cur hd brkind id = else let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc - else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) + else if (is_vtkeep keep) && (not(State.is_cached_and_valid id)) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2440,9 +2442,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (block_start, nodes, name, delegate) -> (fun () -> - assert(keep == VtKeep || keep == VtKeepAsAxiom); - let drop_pt = keep == VtKeepAsAxiom in + | `ASync (block_start, nodes, name, delegate) -> (fun () -> + let keep' = get_vtkeep keep in + let drop_pt = keep' == VtKeepAxiom in let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; VCS.create_proof_task_box nodes ~qed:id ~block_start; @@ -2450,11 +2452,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); - if okeep != keep then + if okeep <> keep then msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " - ^(if keep == VtKeep then "not check " else "reject ") - ^"the "^(if keep == VtKeep then "new" else "incomplete") + ^(if not drop_pt then "not check " else "reject ") + ^"the "^(if not drop_pt then "new" else "incomplete") ^" proof. Reprocess the command declaring " ^"the proof's statement to avoid that.")); let fp, cancel = @@ -2477,8 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (fp, cancel); + let opaque = match keep' with + | VtKeepAxiom | VtKeepOpaque -> + Proof_global.Opaque (* Admitted -> Opaque should be OK. *) + | VtKeepDefined -> Proof_global.Transparent + in let proof = - Proof_global.close_future_proof ~feedback_id:id fp in + Proof_global.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state `No in @@ -2502,15 +2509,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let proof = match keep with | VtDrop -> None - | VtKeepAsAxiom -> + | VtKeep VtKeepAxiom -> let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None - | VtKeep -> - Some(Proof_global.close_proof + | VtKeep opaque -> + let opaque = let open Proof_global in match opaque with + | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent + | VtKeepAxiom -> assert false + in + Some(Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - if keep != VtKeepAsAxiom then + if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in let st = Vernacstate.freeze_interp_state `No in @@ -2632,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = name by looking at the load path! *) List.iter Mltop.add_coq_path iload_path; + Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; + begin match doc_type with | Interactive ln -> let dp = match ln with | TopLogical dp -> dp | TopPhysical f -> dirpath_of_file f in - Safe_typing.allow_delayed_constants := true; Declaremods.start_library dp | VoDoc f -> @@ -2649,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = set_compilation_hints f | VioDoc f -> - Safe_typing.allow_delayed_constants := true; let ldir = dirpath_of_file f in check_coq_overwriting ldir; let () = Flags.verbosely Declaremods.start_library ldir in @@ -2714,7 +2725,7 @@ let rec join_admitted_proofs id = if Stateid.equal id Stateid.initial then () else let view = VCS.visit id in match view.step with - | `Qed ({ keep = VtKeepAsAxiom; fproof = Some (fp,_) },_) -> + | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) -> ignore(Future.force fp); join_admitted_proofs view.next | _ -> join_admitted_proofs view.next @@ -2827,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok -let allow_nested_proofs = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Nested Proofs Allowed"; - Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; - Goptions.optread = (fun () -> !allow_nested_proofs); - Goptions.optwrite = (fun b -> allow_nested_proofs := b) } +let get_allow_nested_proofs = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Nested Proofs Allowed" + ~key:Vernac_classifier.stm_allow_nested_proofs_option_name + ~value:false let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2855,11 +2865,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = - if !cur_opt.async_proofs_full then `QueryQueue (ref false) - else if VCS.is_vio_doc () && - VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) - then `SkipQueue + if VCS.is_vio_doc () && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque (Vernacprop.under_control x.expr) + then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2867,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> - if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) @@ -3192,8 +3201,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !cur_opt.async_proofs_full then - Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try diff --git a/stm/stm.mli b/stm/stm.mli index 0c0e19ce5c..b6071fa56b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -16,7 +16,9 @@ open Names module AsyncOpts : sig type cache = Force - type async_proofs = APoff | APonLazy | APon + type async_proofs = APoff + | APonLazy (* Delays proof checking, but does it in master *) + | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { @@ -27,7 +29,6 @@ module AsyncOpts : sig async_proofs_mode : async_proofs; async_proofs_private_flags : string option; - async_proofs_full : bool; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 526858bd73..44d07279fc 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -26,8 +26,8 @@ let string_of_vernac_type = function | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" - | VtQed VtKeep -> "Qed(keep)" - | VtQed VtKeepAsAxiom -> "Qed(admitted)" + | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" + | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" | VtProofStep { parallel; proof_block_detection } -> "ProofStep " ^ string_of_parallel parallel ^ @@ -43,6 +43,10 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w +let vtkeep_of_opaque = let open Proof_global in function + | Opaque -> VtKeepOpaque + | Transparent -> VtKeepDefined + let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -65,8 +69,9 @@ let classify_vernac e = VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater - | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater - | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater + | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater + | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater + | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ | VernacCheckMayEval _ -> VtQuery, VtLater diff --git a/tactics/auto.ml b/tactics/auto.ml index 81e487b77d..441fb68acc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -172,15 +172,14 @@ let global_info_trivial = ref false let global_info_auto = ref false let add_option ls refe = - let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = String.concat " " ls; - Goptions.optkey = ls; - Goptions.optread = (fun () -> !refe); - Goptions.optwrite = (:=) refe } - in () - -let _ = + Goptions.(declare_bool_option + { optdepr = false; + optname = String.concat " " ls; + optkey = ls; + optread = (fun () -> !refe); + optwrite = (:=) refe }) + +let () = add_option ["Debug";"Trivial"] global_debug_trivial; add_option ["Debug";"Auto"] global_debug_auto; add_option ["Info";"Trivial"] global_info_trivial; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5959dd54b1..719d552def 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -80,7 +80,7 @@ let get_typeclasses_depth () = !typeclasses_depth open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "do typeclass search avoiding eta-expansions " ^ @@ -89,7 +89,7 @@ let _ = optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "during typeclass resolution, solve instances according to their dependency order"; @@ -97,7 +97,7 @@ let _ = optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "use iterative deepening strategy"; @@ -105,7 +105,7 @@ let _ = optread = get_typeclasses_iterative_deepening; optwrite = set_typeclasses_iterative_deepening; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "compat"; @@ -113,7 +113,7 @@ let _ = optread = get_typeclasses_filtered_unification; optwrite = set_typeclasses_filtered_unification; } -let set_typeclasses_debug = +let () = declare_bool_option { optdepr = false; optname = "debug output for typeclasses proof search"; @@ -121,7 +121,7 @@ let set_typeclasses_debug = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } -let _ = +let () = declare_bool_option { optdepr = false; optname = "debug output for typeclasses proof search"; @@ -129,7 +129,7 @@ let _ = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } -let _ = +let () = declare_int_option { optdepr = false; optname = "verbosity of debug output for typeclasses proof search"; @@ -137,7 +137,7 @@ let _ = optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } -let set_typeclasses_depth = +let () = declare_int_option { optdepr = false; optname = "depth for typeclasses proof search"; @@ -1126,7 +1126,7 @@ let solve_inst env evd filter unique split fail = end in sigma -let _ = +let () = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = @@ -1151,7 +1151,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = end in (sigma, term) -let _ = +let () = Hook.set Typeclasses.solve_one_instance_hook (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index b8adb792e8..3019fc0231 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -329,21 +329,21 @@ module Search = Explore.Make(SearchProblem) let global_debug_eauto = ref false let global_info_eauto = ref false -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Debug Eauto"; - Goptions.optkey = ["Debug";"Eauto"]; - Goptions.optread = (fun () -> !global_debug_eauto); - Goptions.optwrite = (:=) global_debug_eauto } - -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Info Eauto"; - Goptions.optkey = ["Info";"Eauto"]; - Goptions.optread = (fun () -> !global_info_eauto); - Goptions.optwrite = (:=) global_info_eauto } +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "Debug Eauto"; + optkey = ["Debug";"Eauto"]; + optread = (fun () -> !global_debug_eauto); + optwrite = (:=) global_debug_eauto }) + +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "Info Eauto"; + optkey = ["Info";"Eauto"]; + optread = (fun () -> !global_info_eauto); + optwrite = (:=) global_info_eauto }) let mk_eauto_dbg d = if d == Debug || !global_debug_eauto then Debug diff --git a/tactics/equality.ml b/tactics/equality.ml index b8967775bf..bdc95941b2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -69,7 +69,7 @@ let use_injection_in_context = function | None -> !injection_in_context | Some flags -> flags.injection_in_context -let _ = +let () = declare_bool_option { optdepr = false; optname = "injection in context"; @@ -714,7 +714,7 @@ exception DiscrFound of let keep_proof_equalities_for_injection = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "injection on prop arguments"; @@ -1501,7 +1501,7 @@ let intro_decomp_eq tac data (c, t) = decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl end -let _ = declare_intro_decomp_eq intro_decomp_eq +let () = declare_intro_decomp_eq intro_decomp_eq (* [subst_tuple_term dep_pair B] @@ -1666,7 +1666,7 @@ user = raise user error specific to rewrite let regular_subst_tactic = ref true -let _ = +let () = declare_bool_option { optdepr = false; optname = "more regular behavior of tactic subst"; @@ -1911,8 +1911,8 @@ let replace_term dir_opt c = (* Declare rewriting tactic for intro patterns "<-" and "->" *) -let _ = +let () = let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in Hook.set Tactics.general_rewrite_clause gmr -let _ = Hook.set Tactics.subst_one subst_one +let () = Hook.set Tactics.subst_one subst_one diff --git a/tactics/hints.ml b/tactics/hints.ml index e64e08dbde..77479f9efa 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -194,14 +194,14 @@ let write_warn_hint = function | "Strict" -> warn_hint := `STRICT | _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") -let _ = - Goptions.declare_string_option - { Goptions.optdepr = false; - Goptions.optname = "behavior of non-imported hints"; - Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; - Goptions.optread = read_warn_hint; - Goptions.optwrite = write_warn_hint; - } +let () = + Goptions.(declare_string_option + { optdepr = false; + optname = "behavior of non-imported hints"; + optkey = ["Loose"; "Hint"; "Behavior"]; + optread = read_warn_hint; + optwrite = write_warn_hint; + }) let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0beafb7e31..b3ea13cf4f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -61,7 +61,7 @@ let clear_hyp_by_default = ref false let use_clear_hyp_by_default () = !clear_hyp_by_default -let _ = +let () = declare_bool_option { optdepr = false; optname = "default clearing of hypotheses after use"; @@ -77,7 +77,7 @@ let universal_lemma_under_conjunctions = ref false let accept_universal_lemma_under_conjunctions () = !universal_lemma_under_conjunctions -let _ = +let () = declare_bool_option { optdepr = false; optname = "trivial unification in tactics applying under conjunctions"; @@ -96,7 +96,7 @@ let bracketing_last_or_and_intro_pattern = ref true let use_bracketing_last_or_and_intro_pattern () = !bracketing_last_or_and_intro_pattern -let _ = +let () = declare_bool_option { optdepr = false; optname = "bracketing last or-and introduction pattern"; @@ -4548,7 +4548,7 @@ let induction_gen_l isrec with_evars elim names lc = match EConstr.kind sigma c with | Var id when not (mem_named_context_val id (Global.named_context_val ())) && not with_evars -> - let _ = newlc:= id::!newlc in + let () = newlc:= id::!newlc in atomize_list l' | _ -> @@ -4561,7 +4561,7 @@ let induction_gen_l isrec with_evars elim names lc = let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in - let _ = newlc:=id::!newlc in + let () = newlc:=id::!newlc in Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v new file mode 100644 index 0000000000..c1fdd04a65 --- /dev/null +++ b/test-suite/bugs/closed/bug_9014.v @@ -0,0 +1,19 @@ +(* A type, not a class *) +Variant T := mkT. + +(* In records, :> declares a coercion *) +Record R := { t_of_r :> T }. +Check forall r : R, r = r :> T. + +(* A class *) +Class A := { p : Prop }. +(* A sub-class *) +Class B := { a_of_b :> A ; t_of_b :> T }. +(* The sub-instance is automatically inferred due to :> for a_of_b *) +Check forall b : B, p. +(* No coercion is introduced by :> in t_of_b *) +Fail Check forall b : B, b = b :> T. + +(* Using :> when the RHS is not a class produces a “not-a-class” warning. *) +Set Warnings "+not-a-class". +Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index d2116d2183..95daa1bb0c 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -2,7 +2,7 @@ Definition T := nat. Definition le := le. -Hint Unfold le. +Hint Unfold le : core. Lemma le_refl : forall n : nat, le n n. auto. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index d76b307914..339f798240 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -165,19 +165,13 @@ Module binders. exact A. Defined. - Definition nomoreu@{i j | i < j +} (A : Type@{i}) : Type@{j}. - pose(foo:=Type). - exact A. - Fail Defined. - Abort. - - Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. - pose(foo:=Type). - exact A. - Defined. + Polymorphic Lemma hidden_strict_type : Type. + Proof. + exact Type. + Qed. + Check hidden_strict_type@{_}. + Fail Check hidden_strict_type@{Set}. - Check moreu@{_ _ _ _}. - Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A. (* By default constraints are extensible *) diff --git a/test-suite/success/private_univs.v b/test-suite/success/private_univs.v new file mode 100644 index 0000000000..5c30b33435 --- /dev/null +++ b/test-suite/success/private_univs.v @@ -0,0 +1,50 @@ +Set Universe Polymorphism. Set Printing Universes. + +Definition internal_defined@{i j | i < j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). (* 1 universe for the let body + 1 for the type *) + exact A. + Fail Defined. +Abort. + +Definition internal_defined@{i j +} (A : Type@{i}) : Type@{j}. +pose(foo:=Type). +exact A. +Defined. +Check internal_defined@{_ _ _ _}. + +Module M. +Lemma internal_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. +Qed. +Check internal_qed@{_ _}. +End M. +Include M. +(* be careful to remove const_private_univs in Include! will be coqchk'd *) + +Unset Strict Universe Declaration. +Lemma private_transitivity@{i j} (A:Type@{i}) : Type@{j}. +Proof. + pose (bar := Type : Type@{j}). + pose (foo := Type@{i} : bar). + exact bar. +Qed. + +Definition private_transitivity'@{i j|i < j} := private_transitivity@{i j}. +Fail Definition dummy@{i j|j <= i +} := private_transitivity@{i j}. + +Unset Private Polymorphic Universes. +Lemma internal_noprivate_qed@{i j|i<=j} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. + Fail Qed. +Abort. + +Lemma internal_noprivate_qed@{i j +} (A:Type@{i}) : Type@{j}. +Proof. + pose (foo := Type). + exact A. +Qed. +Check internal_noprivate_qed@{_ _ _ _}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 49b9e4c951..81a087b525 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -10,3 +10,5 @@ (** Compatibility file for making Coq act similar to Coq v8.9 *) Local Set Warnings "-deprecated". + +Unset Private Polymorphic Universes. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d5241e622c..af9050da29 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2250,6 +2250,32 @@ Section Exists_Forall. End One_predicate. + Theorem Forall_inv_tail + : forall (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs. + Proof. + intros P x0 xs H. + apply Forall_forall with (l := xs). + assert (H0 : forall x : A, In x (x0 :: xs) -> P x). + apply Forall_forall with (P := P) (l := x0 :: xs). + exact H. + assert (H1 : forall (x : A) (H2 : In x xs), P x). + intros x H2. + apply (H0 x). + right. + exact H2. + intros x H2. + apply (H1 x H2). + Qed. + + Theorem Exists_impl + : forall (P Q : A -> Prop), (forall x : A, P x -> Q x) -> forall xs : list A, Exists P xs -> Exists Q xs. + Proof. + intros P Q H xs H0. + induction H0. + apply (Exists_cons_hd Q x l (H x H0)). + apply (Exists_cons_tl x IHExists). + Qed. + Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : Forall (fun x => ~ P x) l <-> ~(Exists P l). Proof. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 60c64d306b..1fb0a37e16 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -77,7 +77,7 @@ End CompareFacts. (** * Properties of [OrderedTypeFull] *) -Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml new file mode 100644 index 0000000000..b248b87880 --- /dev/null +++ b/toplevel/ccompile.ml @@ -0,0 +1,225 @@ +(************************************************************************) +(* * 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 Coqargs + +let fatal_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +(******************************************************************************) +(* Interactive Load File Simulation *) +(******************************************************************************) +let load_vernacular opts ~state = + List.fold_left + (fun state (f_in, echo) -> + let s = Loadpath.locate_file f_in in + (* Should make the beautify logic clearer *) + let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in + if !Flags.beautify + then Flags.with_option Flags.beautify_file load_vernac f_in + else load_vernac s + ) state (List.rev opts.load_vernacular_list) + +let load_init_vernaculars opts ~state = + let state = + if opts.load_rcfile then + Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + state + end in + + load_vernacular opts ~state + +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + +let ensure_ext ext f = + if Filename.check_suffix f ext then f + else begin + warn_file_no_extension (f,ext); + f ^ ext + end + +let chop_extension f = + try Filename.chop_extension f with _ -> f + +let ensure_bname src tgt = + let src, tgt = Filename.basename src, Filename.basename tgt in + let src, tgt = chop_extension src, chop_extension tgt in + if src <> tgt then + fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) + +let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt + +let ensure_v v = ensure ".v" v v +let ensure_vo v vo = ensure ".vo" v vo +let ensure_vio v vio = ensure ".vio" v vio + +let ensure_exists f = + if not (Sys.file_exists f) then + fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) + +(* Compile a vernac file *) +let compile opts ~echo ~f_in ~f_out = + let open Vernac.State in + let check_pending_proofs () = + let pfs = Proof_global.get_all_proof_names () in + if not (CList.is_empty pfs) then + fatal_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") + in + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + match opts.compilation_mode with + | BuildVo -> + Flags.record_aux_file := true; + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + let long_f_dot_vo = + match f_out with + | None -> long_f_dot_v ^ "o" + | Some f -> ensure_vo long_f_dot_v f in + + let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) + Stm.new_doc + Stm.{ doc_type = VoDoc long_f_dot_vo; + iload_path; require_libs; stm_options; + } in + let state = { doc; sid; proof = None; time = opts.time } in + let state = load_init_vernaculars opts ~state in + let ldir = Stm.get_ldir ~doc:state.doc in + Aux_file.(start_aux_file + ~aux_file:(aux_file_name_for long_f_dot_vo) + ~v_file:long_f_dot_v); + Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; + Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); + let wall_clock1 = Unix.gettimeofday () in + let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in + let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in + let _doc = Stm.join ~doc:state.doc in + let wall_clock2 = Unix.gettimeofday () in + check_pending_proofs (); + Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + Aux_file.record_in_aux_at "vo_compile_time" + (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); + Aux_file.stop_aux_file (); + Dumpglob.end_dump_glob () + + | BuildVio -> + Flags.record_aux_file := false; + Dumpglob.noglob (); + + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + + let long_f_dot_vio = + match f_out with + | None -> long_f_dot_v ^ "io" + | Some f -> ensure_vio long_f_dot_v f in + + (* We need to disable error resiliency, otherwise some errors + will be ignored in batch mode. c.f. #6707 + + This is not necessary in the vo case as it fully checks the + document anyways. *) + let stm_options = let open Stm.AsyncOpts in + { stm_options with + async_proofs_mode = APon; + async_proofs_n_workers = 0; + async_proofs_cmd_error_resilience = false; + async_proofs_tac_error_resilience = `None; + } in + + let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) + Stm.new_doc + Stm.{ doc_type = VioDoc long_f_dot_vio; + iload_path; require_libs; stm_options; + } in + + let state = { doc; sid; proof = None; time = opts.time } in + let state = load_init_vernaculars opts ~state in + let ldir = Stm.get_ldir ~doc:state.doc in + let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in + let doc = Stm.finish ~doc:state.doc in + check_pending_proofs (); + let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + Stm.reset_task_queue () + + | Vio2Vo -> + let open Filename in + Flags.record_aux_file := false; + Dumpglob.noglob (); + let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in + let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in + let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in + Library.save_library_raw lfdv sum lib univs proofs + +let compile opts ~echo ~f_in ~f_out = + ignore(CoqworkmgrApi.get 1); + compile opts ~echo ~f_in ~f_out; + CoqworkmgrApi.giveback 1 + +let compile_file opts (f_in, echo) = + let f_out = opts.compilation_output_name in + if !Flags.beautify then + Flags.with_option Flags.beautify_file + (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in + else + compile opts ~echo ~f_in ~f_out + +let compile_files opts = + let compile_list = List.rev opts.compile_list in + List.iter (compile_file opts) compile_list + +(******************************************************************************) +(* VIO Dispatching *) +(******************************************************************************) +let check_vio_tasks opts = + let rc = + List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) + true (List.rev opts.vio_tasks) in + if not rc then fatal_error Pp.(str "VIO Task Check failed") + +(* vio files *) +let schedule_vio opts = + if opts.vio_checking then + Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files + else + Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files + +let do_vio opts = + (* We must initialize the loadpath here as the vio scheduling + process happens outside of the STM *) + if opts.vio_files <> [] || opts.vio_tasks <> [] then + let iload_path = build_load_path opts in + List.iter Mltop.add_coq_path iload_path; + + (* Vio compile pass *) + if opts.vio_files <> [] then schedule_vio opts; + (* Vio task pass *) + if opts.vio_tasks <> [] then check_vio_tasks opts diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli new file mode 100644 index 0000000000..757c91c408 --- /dev/null +++ b/toplevel/ccompile.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** [load_init_vernaculars opts ~state] Load vernaculars from + the init (rc) file *) +val load_init_vernaculars : Coqargs.coq_cmdopts -> state:Vernac.State.t-> Vernac.State.t + +(** [compile_files opts] compile files specified in [opts] *) +val compile_files : Coqargs.coq_cmdopts -> unit + +(** [do_vio opts] process [.vio] files in [opts] *) +val do_vio : Coqargs.coq_cmdopts -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 15411d55d0..6c4ea9afa1 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -40,8 +40,8 @@ type coq_cmdopts = { load_rcfile : bool; rcfile : string option; - ml_includes : string list; - vo_includes : (string * Names.DirPath.t * bool) list; + ml_includes : Mltop.coq_path list; + vo_includes : Mltop.coq_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -64,6 +64,7 @@ type coq_cmdopts = { color : color; impredicative_set : Declarations.set_predicativity; + indices_matter : bool; enable_VM : bool; enable_native_compiler : bool; stm_flags : Stm.AsyncOpts.stm_opt; @@ -90,7 +91,7 @@ type coq_cmdopts = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let init_args = { +let default_opts = { load_init = true; load_rcfile = true; @@ -118,6 +119,7 @@ let init_args = { color = `AUTO; impredicative_set = Declarations.PredicativeSet; + indices_matter = false; enable_VM = true; enable_native_compiler = Coq_config.native_compiler; stm_flags = Stm.AsyncOpts.default_opts; @@ -137,6 +139,8 @@ let init_args = { print_emacs = false; + (* Quiet / verbosity options should be here *) + inputstate = None; outputstate = None; } @@ -145,11 +149,14 @@ let init_args = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - { opts with ml_includes = s :: opts.ml_includes } + Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } -let add_vo_include opts d p implicit = - let p = Libnames.dirpath_of_string p in - { opts with vo_includes = (d, p, implicit) :: opts.vo_includes } +let add_vo_include opts unix_path coq_path implicit = + let open Mltop in + let coq_path = Libnames.dirpath_of_string coq_path in + { opts with vo_includes = { + recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.vo_includes } let add_vo_require opts d p export = { opts with vo_requires = (d, p, export) :: opts.vo_requires } @@ -161,6 +168,7 @@ let add_compat_require opts v = | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) let set_batch_mode opts = + (* XXX: This should be in the argument record *) Flags.quiet := true; System.trust_file_cache := true; { opts with batch_mode = true } @@ -276,11 +284,6 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 -let get_identifier opt s = - try Names.Id.of_string s - with CErrors.UserError _ -> - prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 - let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -320,7 +323,7 @@ let usage batch = else Usage.print_usage_coqtop () (* Main parsing routine *) -let parse_args arglist : coq_cmdopts * string list = +let parse_args init_opts arglist : coq_cmdopts * string list = let args = ref arglist in let extras = ref [] in let rec parse oval = match !args with @@ -473,7 +476,9 @@ let parse_args arglist : coq_cmdopts * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 @@ -538,10 +543,6 @@ let parse_args arglist : coq_cmdopts * string list = (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - { oval with stm_flags = { oval.stm_flags with - Stm.AsyncOpts.async_proofs_full = true; - }} |"-async-proofs-never-reopen-branch" -> { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true @@ -565,7 +566,7 @@ let parse_args arglist : coq_cmdopts * string list = |"-filteropts" -> { oval with filter_opts = true } |"-impredicative-set" -> { oval with impredicative_set = Declarations.ImpredicativeSet } - |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval + |"-indices-matter" -> { oval with indices_matter = true } |"-m"|"--memory" -> { oval with memory_stat = true } |"-noinit"|"-nois" -> { oval with load_init = false } |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } @@ -595,5 +596,21 @@ let parse_args arglist : coq_cmdopts * string list = parse noval in try - parse init_args + parse init_opts with any -> fatal_error any + +(******************************************************************************) +(* Startup LoadPath and Modules *) +(******************************************************************************) +(* prelude_data == From Coq Require Export Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some false + +let require_libs opts = + if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires + +let cmdline_load_path opts = + List.rev opts.vo_includes @ List.(rev opts.ml_includes) + +let build_load_path opts = + Coqinit.libs_init_load_path ~load_init:opts.load_init @ + cmdline_load_path opts diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index b709788dde..e645b0c126 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -19,8 +19,8 @@ type coq_cmdopts = { load_rcfile : bool; rcfile : string option; - ml_includes : string list; - vo_includes : (string * Names.DirPath.t * bool) list; + ml_includes : Mltop.coq_path list; + vo_includes : Mltop.coq_path list; vo_requires : (string * string option * bool option) list; (* Fuse these two? Currently, [batch_mode] is only used to @@ -43,6 +43,7 @@ type coq_cmdopts = { color : color; impredicative_set : Declarations.set_predicativity; + indices_matter : bool; enable_VM : bool; enable_native_compiler : bool; stm_flags : Stm.AsyncOpts.stm_opt; @@ -62,10 +63,18 @@ type coq_cmdopts = { print_emacs : bool; + (* Quiet / verbosity options should be here *) + inputstate : string option; outputstate : string option; } -val parse_args : string list -> coq_cmdopts * string list +(* Default options *) +val default_opts : coq_cmdopts + +val parse_args : coq_cmdopts -> string list -> coq_cmdopts * string list val exitcode : coq_cmdopts -> int + +val require_libs : coq_cmdopts -> (string * string option * bool option) list +val build_load_path : coq_cmdopts -> Mltop.coq_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 66af7f7cdf..edef741ca6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -64,67 +64,11 @@ let outputstate opts = States.extern_state fname) opts.outputstate (******************************************************************************) -(* Interactive Load File Simulation *) -(******************************************************************************) -let load_vernacular opts ~state = - List.fold_left - (fun state (f_in, echo) -> - let s = Loadpath.locate_file f_in in - (* Should make the beautify logic clearer *) - let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in - if !Flags.beautify - then Flags.with_option Flags.beautify_file load_vernac f_in - else load_vernac s - ) state (List.rev opts.load_vernacular_list) - -let load_init_vernaculars opts ~state = - let state = - if opts.load_rcfile then - Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () - else begin - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - state - end in - - load_vernacular opts ~state - -(******************************************************************************) -(* Startup LoadPath and Modules *) -(******************************************************************************) -(* prelude_data == From Coq Require Export Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some false - -let require_libs opts = - if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires - -let cmdline_load_path opts = - let open Mltop in - (* loadpaths given by options -Q and -R *) - List.map - (fun (unix_path, coq_path, implicit) -> - { recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) - (List.rev opts.vo_includes) @ - - (* additional ml directories, given with option -I *) - List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes) - -let build_load_path opts = - Coqinit.libs_init_load_path ~load_init:opts.load_init @ - cmdline_load_path opts - -(******************************************************************************) (* Fatal Errors *) (******************************************************************************) (** Prints info which is either an error or an anomaly and then exits with the appropriate error code *) -let fatal_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - let fatal_error_exn exn = Topfmt.(in_phase ~phase:Initialization print_err_exn exn); flush_all (); @@ -134,187 +78,6 @@ let fatal_error_exn exn = exit exit_code (******************************************************************************) -(* File Compilation *) -(******************************************************************************) -let warn_file_no_extension = - CWarnings.create ~name:"file-no-extension" ~category:"filesystem" - (fun (f,ext) -> - str "File \"" ++ str f ++ - strbrk "\" has been implicitly expanded to \"" ++ - str f ++ str ext ++ str "\"") - -let ensure_ext ext f = - if Filename.check_suffix f ext then f - else begin - warn_file_no_extension (f,ext); - f ^ ext - end - -let chop_extension f = - try Filename.chop_extension f with _ -> f - -let ensure_bname src tgt = - let src, tgt = Filename.basename src, Filename.basename tgt in - let src, tgt = chop_extension src, chop_extension tgt in - if src <> tgt then - fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ - str "Source: " ++ str src ++ fnl () ++ - str "Target: " ++ str tgt) - -let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt - -let ensure_v v = ensure ".v" v v -let ensure_vo v vo = ensure ".vo" v vo -let ensure_vio v vio = ensure ".vio" v vio - -let ensure_exists f = - if not (Sys.file_exists f) then - fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -(* Compile a vernac file *) -let compile opts ~echo ~f_in ~f_out = - let open Vernac.State in - let check_pending_proofs () = - let pfs = Proof_global.get_all_proof_names () in - if not (CList.is_empty pfs) then - fatal_error (str "There are pending proofs: " - ++ (pfs - |> List.rev - |> prlist_with_sep pr_comma Names.Id.print) - ++ str ".") - in - let iload_path = build_load_path opts in - let require_libs = require_libs opts in - let stm_options = opts.stm_flags in - match opts.compilation_mode with - | BuildVo -> - Flags.record_aux_file := true; - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - let long_f_dot_vo = - match f_out with - | None -> long_f_dot_v ^ "o" - | Some f -> ensure_vo long_f_dot_v f in - - let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) - Stm.new_doc - Stm.{ doc_type = VoDoc long_f_dot_vo; - iload_path; require_libs; stm_options; - } in - - let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in - let ldir = Stm.get_ldir ~doc:state.doc in - Aux_file.(start_aux_file - ~aux_file:(aux_file_name_for long_f_dot_vo) - ~v_file:long_f_dot_v); - Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; - Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); - let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in - let _doc = Stm.join ~doc:state.doc in - let wall_clock2 = Unix.gettimeofday () in - check_pending_proofs (); - Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); - Aux_file.record_in_aux_at "vo_compile_time" - (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - Aux_file.stop_aux_file (); - Dumpglob.end_dump_glob () - - | BuildVio -> - Flags.record_aux_file := false; - Dumpglob.noglob (); - - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - - let long_f_dot_vio = - match f_out with - | None -> long_f_dot_v ^ "io" - | Some f -> ensure_vio long_f_dot_v f in - - (* We need to disable error resiliency, otherwise some errors - will be ignored in batch mode. c.f. #6707 - - This is not necessary in the vo case as it fully checks the - document anyways. *) - let stm_options = let open Stm.AsyncOpts in - { stm_options with - async_proofs_cmd_error_resilience = false; - async_proofs_tac_error_resilience = `None; - } in - - let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) - Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_vio; - iload_path; require_libs; stm_options; - } in - - let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in - let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in - let doc = Stm.finish ~doc:state.doc in - check_pending_proofs (); - let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in - Stm.reset_task_queue () - - | Vio2Vo -> - let open Filename in - Flags.record_aux_file := false; - Dumpglob.noglob (); - let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in - let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in - let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in - Library.save_library_raw lfdv sum lib univs proofs - -let compile opts ~echo ~f_in ~f_out = - ignore(CoqworkmgrApi.get 1); - compile opts ~echo ~f_in ~f_out; - CoqworkmgrApi.giveback 1 - -let compile_file opts (f_in, echo) = - let f_out = opts.compilation_output_name in - if !Flags.beautify then - Flags.with_option Flags.beautify_file - (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in - else - compile opts ~echo ~f_in ~f_out - -let compile_files opts = - let compile_list = List.rev opts.compile_list in - List.iter (compile_file opts) compile_list - -(******************************************************************************) -(* VIO Dispatching *) -(******************************************************************************) -let check_vio_tasks opts = - let rc = - List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) - true (List.rev opts.vio_tasks) in - if not rc then fatal_error Pp.(str "VIO Task Check failed") - -(* vio files *) -let schedule_vio opts = - if opts.vio_checking then - Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files - else - Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files - -let do_vio opts = - (* We must initialize the loadpath here as the vio scheduling - process happens outside of the STM *) - if opts.vio_files <> [] || opts.vio_tasks <> [] then - let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; - - (* Vio compile pass *) - if opts.vio_files <> [] then schedule_vio opts; - (* Vio task pass *) - if opts.vio_tasks <> [] then check_vio_tasks opts - - -(******************************************************************************) (* Color Options *) (******************************************************************************) let init_color opts = @@ -385,7 +148,7 @@ let init_gc () = Gc.space_overhead = 120} (** Main init routine *) -let init_toplevel custom_init arglist = +let init_toplevel init_opts custom_init arglist = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) @@ -401,7 +164,7 @@ let init_toplevel custom_init arglist = *) let res = begin try - let opts,extras = parse_args arglist in + let opts,extras = parse_args init_opts arglist in memory_stat := opts.memory_stat; (* If we have been spawned by the Spawn module, this has to be done @@ -435,6 +198,7 @@ let init_toplevel custom_init arglist = Flags.if_verbose print_header (); Mltop.init_known_plugins (); Global.set_engagement opts.impredicative_set; + Global.set_indices_matter opts.indices_matter; Global.set_VM opts.enable_VM; Global.set_native_compiler opts.enable_native_compiler; @@ -470,13 +234,13 @@ let init_toplevel custom_init arglist = iload_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.time } in - Some (load_init_vernaculars opts ~state), opts + Some (Ccompile.load_init_vernaculars opts ~state), opts (* Non interactive: we perform a sequence of compilation steps *) end else begin - compile_files opts; + Ccompile.compile_files opts; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) - do_vio opts; + Ccompile.do_vio opts; (* Allow the user to output an arbitrary state *) outputstate opts; None, opts @@ -488,20 +252,25 @@ let init_toplevel custom_init arglist = Feedback.del_feeder init_feeder; res -type custom_toplevel = { - init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list; - run : opts:coq_cmdopts -> state:Vernac.State.t -> unit; -} +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } let coqtop_init ~opts extra = init_color opts; CoqworkmgrApi.(init !async_proofs_worker_priority); opts, extra -let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; } +let coqtop_toplevel = + { init = coqtop_init + ; run = Coqloop.loop + ; opts = Coqargs.default_opts + } let start_coq custom = - match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with + match init_toplevel custom.opts custom.init (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) | Some state, opts when not opts.batch_mode -> custom.run ~opts ~state; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 641448f10a..c95d0aca55 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,10 +12,13 @@ [init] is used to do custom command line argument parsing. [run] launches a custom toplevel. *) -type custom_toplevel = { - init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list; - run : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit; -} +open Coqargs + +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } val coqtop_toplevel : custom_toplevel diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 597173e5f5..732744eb42 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -4,5 +4,6 @@ Coqinit Coqargs G_toplevel Coqloop +Ccompile Coqtop WorkerLoop diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index ee6d5e8843..e4e9a87365 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -23,6 +23,7 @@ let arg_init init ~opts extra_args = let start ~init ~loop = let open Coqtop in let custom = { + opts = Coqargs.default_opts; init = arg_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in diff --git a/vernac/attributes.ml b/vernac/attributes.ml index bc0b0310b3..75ca027332 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -162,7 +162,7 @@ let universe_transform ~warn_unqualified : unit attribute = let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] let is_universe_polymorphism = let b = ref false in - let _ = let open Goptions in + let () = let open Goptions in declare_bool_option { optdepr = false; optname = "universe polymorphism"; diff --git a/vernac/classes.ml b/vernac/classes.ml index 95e46b252b..7d6bd1ca64 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -30,13 +30,13 @@ open Entries let refine_instance = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "definition of instances by refining"; - Goptions.optkey = ["Refine";"Instance";"Mode"]; - Goptions.optread = (fun () -> !refine_instance); - Goptions.optwrite = (fun b -> refine_instance := b) -} +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "definition of instances by refining"; + optkey = ["Refine";"Instance";"Mode"]; + optread = (fun () -> !refine_instance); + optwrite = (fun b -> refine_instance := b) +}) let typeclasses_db = "typeclass_instances" @@ -44,7 +44,7 @@ let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) -let _ = +let () = Hook.set Typeclasses.add_instance_hint_hook (fun inst path local info poly -> let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 4cdc60216e..4b8371f5c3 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -26,7 +26,7 @@ open Entries let axiom_into_instance = ref false -let _ = +let () = let open Goptions in declare_bool_option { optdepr = true; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index fbfa997555..8b9cf7d269 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -37,7 +37,7 @@ module RelDecl = Context.Rel.Declaration let should_auto_template = let open Goptions in let auto = ref true in - let _ = declare_bool_option + let () = declare_bool_option { optdepr = false; optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; @@ -266,7 +266,7 @@ let inductive_levels env evd poly arities inds = in let minlev = (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + if indices_matter env && List.length ctx > 0 then ( let ilev = sign_level env evd ctx in Univ.sup ilev minlev) else minlev diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 16101396cf..43abc0a200 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -33,24 +33,24 @@ open Pcoq let constr_level = string_of_int let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,false; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 9,Gramlib.Gramext.RightA,false; + 8,Gramlib.Gramext.RightA,true; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,true; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_constr_levels = (default_levels, default_pattern_levels) @@ -70,28 +70,28 @@ let save_levels levels custom lev = (* first LeftA, then RightA and NoneA together *) let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false + | Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false + | Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false | _ -> true let create_assoc = function - | None -> Extend.RightA + | None -> Gramlib.Gramext.RightA | Some a -> a let error_level_assoc p current expected = let open Pp in let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in + | Gramlib.Gramext.LeftA -> str "left" + | Gramlib.Gramext.RightA -> str "right" + | Gramlib.Gramext.NonA -> str "non" in user_err (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ pr_assoc expected ++ str " associative.") let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) + | None -> Gramlib.Gramext.First + | Some lev -> Gramlib.Gramext.After (constr_level lev) let find_position_gen current ensure assoc lev = match lev with @@ -121,13 +121,13 @@ let find_position_gen current ensure assoc lev = updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - updated, (Some (Extend.Level (constr_level n)), None, None, !init) + updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) end with (* Nothing has changed *) Exit -> (* Just inherit the existing associativity and name (None) *) - current, (Some (Extend.Level (constr_level n)), None, None, None) + current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) let rec list_mem_assoc_triple x = function | [] -> false @@ -186,15 +186,18 @@ let find_position accu custom forpat assoc level = (* Binding constr entry keys to entries *) (* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp5_assoc = function - | Some NonA | Some RightA -> RightA - | None | Some LeftA -> LeftA - -let assoc_eq al ar = match al, ar with -| NonA, NonA -| RightA, RightA -| LeftA, LeftA -> true -| _, _ -> false +let camlp5_assoc = + let open Gramlib.Gramext in function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = + let open Gramlib.Gramext in + match al, ar with + | NonA, NonA + | RightA, RightA + | LeftA, LeftA -> true + | _, _ -> false (* [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of @@ -204,7 +207,7 @@ let assoc_eq al ar = match al, ar with Some None = NEXT Some (Some (n,cur)) = constr LEVEL n s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function +let adjust_level assoc from = let open Gramlib.Gramext in function (* Associativity is None means force the level *) | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) (* Compute production name on the right side *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index e3f6a87541..22528a607f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1175,9 +1175,9 @@ GRAMMAR EXTEND Gram | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) } | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural -> { SetCustomEntry (x,Some n) } - | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA } - | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA } - | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA } + | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA } + | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA } + | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA } | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting } | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing } | IDENT "compat"; s = STRING -> diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c1343fb592..9bd095aa52 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -44,7 +44,7 @@ open Context.Rel.Declaration (* Flags governing automatic synthesis of schemes *) let elim_flag = ref true -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of induction schemes"; @@ -53,7 +53,7 @@ let _ = optwrite = (fun b -> elim_flag := b) } let bifinite_elim_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of induction schemes for non-recursive types"; @@ -62,7 +62,7 @@ let _ = optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of case analysis schemes"; @@ -71,7 +71,7 @@ let _ = optwrite = (fun b -> case_flag := b) } let eq_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of boolean equality"; @@ -82,7 +82,7 @@ let _ = let is_eq_flag () = !eq_flag let eq_dec_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "automatic declaration of decidable equality"; @@ -91,7 +91,7 @@ let _ = optwrite = (fun b -> eq_dec_flag := b) } let rewriting_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname ="automatic declaration of rewriting schemes for equality types"; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2443c5d12a..28e80a74aa 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -311,7 +311,7 @@ let universe_proof_terminator compute_guard hook = | Transparent -> false, true | Opaque -> true, false in - let const = {const with const_entry_opaque = is_opaque} in + assert (is_opaque == const.const_entry_opaque); let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in @@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook = let keep_admitted_vars = ref true -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -498,13 +498,13 @@ let save_proof ?proof = function Admitted(id,k,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe - | Vernacexpr.Proved (is_opaque,idopt) -> + | Vernacexpr.Proved (opaque,idopt) -> let (proof_obj,terminator) = match proof with | None -> - Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Proof_global.discard_current (); - Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) + Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5ab877fae2..82434afbbd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -287,7 +287,7 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = function +let prec_assoc = let open Gramlib.Gramext in function | RightA -> (L,E) | LeftA -> (E,L) | NonA -> (L,L) @@ -685,7 +685,7 @@ let border = function | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a | _ -> None -let recompute_assoc typs = +let recompute_assoc typs = let open Gramlib.Gramext in match border typs, border (List.rev typs) with | Some LeftA, Some RightA -> assert false | Some LeftA, _ -> Some LeftA @@ -802,7 +802,7 @@ let inSyntaxExtension : syntax_extension_obj -> obj = module NotationMods = struct type notation_modifier = { - assoc : gram_assoc option; + assoc : Gramlib.Gramext.g_assoc option; level : int option; custom : notation_entry; etyps : (Id.t * simple_constr_prod_entry_key) list; @@ -1230,7 +1230,7 @@ let compute_syntax_data local df modifiers = let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); - let assoc = Option.append mods.assoc (Some NonA) in + let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in let _ = check_useless_entry_types recvars mainvars mods.etyps in let _ = check_binder_type recvars mods.etyps in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 8baf391c70..4926b8c3e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -337,32 +337,20 @@ let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) (* true = hide obligations *) -let hide_obligations = ref false +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Hidding of Program obligations" + ~key:["Hide";"Obligations"] + ~value:false -let set_hide_obligations = (:=) hide_obligations -let get_hide_obligations () = !hide_obligations -open Goptions -let _ = - declare_bool_option - { optdepr = false; - optname = "Hiding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } - -let shrink_obligations = ref true - -let set_shrink_obligations = (:=) shrink_obligations -let get_shrink_obligations () = !shrink_obligations - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "Shrinking of Program obligations"; - optkey = ["Shrink";"Obligations"]; - optread = get_shrink_obligations; - optwrite = set_shrink_obligations; } +let get_shrink_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true (* remove in 8.8 *) + ~name:"Shrinking of Program obligations" + ~key:["Shrink";"Obligations"] + ~value:true let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) @@ -893,7 +881,7 @@ let obligation_terminator name num guard hook auto pf = let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in - let _ = obls.(num) <- obl in + let () = obls.(num) <- obl in let prg_ctx = if pi2 (prg.prg_kind) then (* Polymorphic *) (** We merge the new universes and constraints of the @@ -949,7 +937,7 @@ in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in let () = if transparent then add_hint true prg cst in let obls = Array.copy obls in - let _ = obls.(num) <- obl in + let () = obls.(num) <- obl in let prg = { prg with prg_ctx = ctx' } in let () = try ignore (update_obls prg obls (pred rem)) @@ -1045,7 +1033,7 @@ and solve_prg_obligations prg ?oblset tac = (fun i -> Int.Set.mem i !set) in let prgref = ref prg in - let _ = + let () = Array.iteri (fun i x -> if p i then match solve_obligation_by_tac !prgref obls' i tac with @@ -1132,7 +1120,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in + let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2ddd210365..e7c1e29beb 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -380,7 +380,7 @@ open Pputils let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) - let pr_syntax_modifier = function + let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ pr_opt pr_constr_as_binder_kind bko diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 3e2bd98720..526845084a 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -137,13 +137,13 @@ let suggest_common env ppid used ids_typ skip = let suggest_proof_using = ref false -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "suggest Proof using"; - Goptions.optkey = ["Suggest";"Proof";"Using"]; - Goptions.optread = (fun () -> !suggest_proof_using); - Goptions.optwrite = ((:=) suggest_proof_using) } +let () = + Goptions.(declare_bool_option + { optdepr = false; + optname = "suggest Proof using"; + optkey = ["Suggest";"Proof";"Using"]; + optread = (fun () -> !suggest_proof_using); + optwrite = ((:=) suggest_proof_using) }) let suggest_constant env kn = if !suggest_proof_using @@ -172,13 +172,13 @@ let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) -let _ = - Goptions.declare_stringopt_option - { Goptions.optdepr = false; - Goptions.optname = "default value for Proof using"; - Goptions.optkey = ["Default";"Proof";"Using"]; - Goptions.optread = (fun () -> Option.map using_to_string !value); - Goptions.optwrite = (fun b -> value := Option.map using_from_string b); - } +let () = + Goptions.(declare_stringopt_option + { optdepr = false; + optname = "default value for Proof using"; + optkey = ["Default";"Proof";"Using"]; + optread = (fun () -> Option.map using_to_string !value); + optwrite = (fun b -> value := Option.map using_from_string b); + }) let get_default_proof_using () = !value diff --git a/vernac/record.ml b/vernac/record.ml index 7bdf6a973f..f6dbcb5291 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -36,7 +36,7 @@ module RelDecl = Context.Rel.Declaration (** Flag governing use of primitive projections. Disabled by default. *) let primitive_flag = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "use of primitive projections"; @@ -45,7 +45,7 @@ let _ = optwrite = (fun b -> primitive_flag := b) } let typeclasses_strict = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "strict typeclass resolution"; @@ -54,7 +54,7 @@ let _ = optwrite = (fun b -> typeclasses_strict := b); } let typeclasses_unique = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "unique typeclass instances"; @@ -103,7 +103,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in - let _ = + let () = let error bk {CAst.loc; v=name} = match bk, name with | Default _, Anonymous -> @@ -458,7 +458,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum ubinders univs id idbuild paramimpls params arity +let declare_class def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records = in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum ubinders univs id.CAst.v idbuild + declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a78329ad1d..a157e01fc1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let uniform_inductive_parameters = ref false +let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Uniform inductive parameters" + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false let should_treat_as_uniform () = - if !uniform_inductive_parameters + if get_uniform_inductive_parameters () then ComInductive.UniformParameters else ComInductive.NonUniformParameters @@ -1409,7 +1414,7 @@ let vernac_generalizable ~local = let local = Option.default true local in Implicit_quantifiers.declare_generalizable ~local -let _ = +let () = declare_bool_option { optdepr = false; optname = "silent"; @@ -1417,7 +1422,7 @@ let _ = optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments"; @@ -1425,7 +1430,7 @@ let _ = optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "strict implicit arguments"; @@ -1433,7 +1438,7 @@ let _ = optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "strong strict implicit arguments"; @@ -1441,7 +1446,7 @@ let _ = optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "contextual implicit arguments"; @@ -1449,7 +1454,7 @@ let _ = optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit status of reversible patterns"; @@ -1457,7 +1462,7 @@ let _ = optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "maximal insertion of implicit"; @@ -1465,7 +1470,7 @@ let _ = optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } -let _ = +let () = declare_bool_option { optdepr = false; optname = "coercion printing"; @@ -1473,7 +1478,7 @@ let _ = optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "printing of existential variable instances"; @@ -1481,7 +1486,7 @@ let _ = optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments printing"; @@ -1489,7 +1494,7 @@ let _ = optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "implicit arguments defensive printing"; @@ -1497,7 +1502,7 @@ let _ = optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "projection printing using dot notation"; @@ -1505,7 +1510,7 @@ let _ = optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "notations printing"; @@ -1513,7 +1518,7 @@ let _ = optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "raw printing"; @@ -1521,7 +1526,7 @@ let _ = optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "use of the program extension"; @@ -1529,7 +1534,7 @@ let _ = optread = (fun () -> !Flags.program_mode); optwrite = (fun b -> Flags.program_mode:=b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "Polymorphic inductive cumulativity"; @@ -1537,15 +1542,7 @@ let _ = optread = Flags.is_polymorphic_inductive_cumulativity; optwrite = Flags.make_polymorphic_inductive_cumulativity } -let _ = - declare_bool_option - { optdepr = false; - optname = "Uniform inductive parameters"; - optkey = ["Uniform"; "Inductive"; "Parameters"]; - optread = (fun () -> !uniform_inductive_parameters); - optwrite = (fun b -> uniform_inductive_parameters := b) } - -let _ = +let () = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -1555,7 +1552,7 @@ let _ = let lev = Option.default Flags.default_inline_level o in Flags.set_inline_level lev) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "kernel term sharing"; @@ -1563,7 +1560,7 @@ let _ = optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); optwrite = Global.set_share_reduction } -let _ = +let () = declare_bool_option { optdepr = false; optname = "display compact goal contexts"; @@ -1571,7 +1568,7 @@ let _ = optread = (fun () -> Printer.get_compact_context()); optwrite = (fun b -> Printer.set_compact_context b) } -let _ = +let () = declare_int_option { optdepr = false; optname = "the printing depth"; @@ -1579,7 +1576,7 @@ let _ = optread = Topfmt.get_depth_boxes; optwrite = Topfmt.set_depth_boxes } -let _ = +let () = declare_int_option { optdepr = false; optname = "the printing width"; @@ -1587,7 +1584,7 @@ let _ = optread = Topfmt.get_margin; optwrite = Topfmt.set_margin } -let _ = +let () = declare_bool_option { optdepr = false; optname = "printing of universes"; @@ -1595,7 +1592,7 @@ let _ = optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } -let _ = +let () = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; @@ -1603,7 +1600,7 @@ let _ = optread = (fun () -> !Cbytegen.dump_bytecode); optwrite = (:=) Cbytegen.dump_bytecode } -let _ = +let () = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; @@ -1611,7 +1608,7 @@ let _ = optread = (fun () -> !Clambda.dump_lambda); optwrite = (:=) Clambda.dump_lambda } -let _ = +let () = declare_bool_option { optdepr = false; optname = "explicitly parsing implicit arguments"; @@ -1619,7 +1616,7 @@ let _ = optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } -let _ = +let () = declare_string_option ~preprocess:CWarnings.normalize_flags_string { optdepr = false; optname = "warnings display"; @@ -1627,7 +1624,7 @@ let _ = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let _ = +let () = declare_string_option { optdepr = false; optname = "native_compute profiler output"; @@ -1635,7 +1632,7 @@ let _ = optread = Nativenorm.get_profile_filename; optwrite = Nativenorm.set_profile_filename } -let _ = +let () = declare_bool_option { optdepr = false; optname = "enable native compute profiling"; @@ -1933,7 +1930,7 @@ let interp_search_about_item env sigma = *) let search_output_name_only = ref false -let _ = +let () = declare_bool_option { optdepr = false; optname = "output-name-only search"; @@ -2303,13 +2300,13 @@ let interp ?proof ~atts ~st c = let default_timeout = ref None -let _ = - Goptions.declare_int_option - { Goptions.optdepr = false; - Goptions.optname = "the default timeout"; - Goptions.optkey = ["Default";"Timeout"]; - Goptions.optread = (fun () -> !default_timeout); - Goptions.optwrite = ((:=) default_timeout) } +let () = + declare_int_option + { optdepr = false; + optname = "the default timeout"; + optkey = ["Default";"Timeout"]; + optread = (fun () -> !default_timeout); + optwrite = ((:=) default_timeout) } (** When interpreting a command, the current timeout is initially the default one, but may be modified locally by a Timeout command. *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 122005e011..1e6c40c829 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,7 +167,7 @@ type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option | SetLevel of int | SetCustomEntry of string * int option - | SetAssoc of Extend.gram_assoc + | SetAssoc of Gramlib.Gramext.g_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 35f26cab4d..2541f73582 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -12,6 +12,10 @@ open Util open Pp open CErrors +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -33,7 +37,6 @@ type vernac_type = (* To be removed *) | VtMeta | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 7feaccd9a3..8b07be8b16 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -27,6 +27,11 @@ considered safe to delegate to a worker. *) + +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -48,7 +53,6 @@ type vernac_type = (* To be removed *) | VtMeta | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = |