diff options
120 files changed, 1270 insertions, 1197 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 971a281ea..4e159ebdc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -306,6 +306,9 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" +ci-bedrock2: + <<: *ci-template + ci-bignums: <<: *ci-template @@ -1,6 +1,10 @@ Changes from 8.8.2 to 8.9+beta1 =============================== +Kernel + +- Mutually defined records are now supported. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -88,6 +92,8 @@ Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). - Fix a critical bug with inlining of polymorphic constants (#7615). +- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was + present since 8.5. Notations @@ -1,6 +1,6 @@ - INSTALLATION PROCEDURES FOR THE COQ V8.8 SYSTEM - ----------------------------------------------- + INSTALLATION PROCEDURE + ---------------------- WHAT DO YOU NEED ? @@ -27,11 +27,14 @@ WHAT DO YOU NEED ? port install coq - To compile Coq V8.8 yourself, you need: + To compile Coq yourself, you need: - OCaml version 4.02.3 or later (available at https://ocaml.org/) + - The Num package, which used to be part of the OCaml standard library, + if you are using an OCaml version >= 4.06.0 + - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) @@ -42,20 +45,24 @@ WHAT DO YOU NEED ? - a C compiler - - for Coqide, the Lablgtk development files, and the GTK libraries - including gtksourceview, see INSTALL.ide for more details + - for CoqIDE, the lablgtk development files (version >= 2.18.3), + and the GTK 2.x libraries including gtksourceview2. - Note that camlp5 and lablgtk should be properly registered with + Note that num, camlp5 and lablgtk should be properly registered with findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. - Opam (https://opam.ocaml.org/) is recommended to install ocaml and + Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam install ocamlfind camlp5 lablgtk-extras + $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview should get you a reasonable OCaml environment to compile Coq. + Nix users can also get all the required dependencies by running: + + $ nix-shell + Advanced users may want to experiment with the OCaml Flambda compiler as way to improve the performance of Coq. In order to profit from Flambda, a special build of the OCaml compiler that has @@ -76,7 +83,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler installed on your +1- Check that you have the OCaml compiler installed on your computer and that "ocamlc" (or, better, its native code version "ocamlc.opt") lies in a directory which is present in your $PATH environment variable. At the time of writing this sentence, all @@ -183,11 +190,6 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). make install Of course, you may need superuser rights to do that. - To use the Coq emacs mode you also need to put the following lines - in you .emacs file: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) 7- Optionally, you could build the bytecode version of Coq via: @@ -258,8 +260,6 @@ THE AVAILABLE COMMANDS. directory, or read online on http://coq.inria.fr/doc/) and in the corresponding manual pages. - There is also a tutorial and a FAQ; see http://coq.inria.fr/getting-started - COMPILING FOR DIFFERENT ARCHITECTURES. ====================================== diff --git a/INSTALL.doc b/INSTALL.doc deleted file mode 100644 index 13e6440d0..000000000 --- a/INSTALL.doc +++ /dev/null @@ -1,91 +0,0 @@ - The Coq documentation - ===================== - -The Coq documentation includes - -- A Reference Manual -- A document presenting the Coq standard library - -The reference manual is written is reStructuredText and compiled -using Sphinx (see `doc/sphinx/README.rst`) to learn more. - -The documentation for the standard library is generated from -the `.v` source files using coqdoc. - -Prerequisite ------------- - -To produce all the documents, the following tools are needed: - - - latex (latex2e) - - pdflatex - - dvips - - makeindex - - Python 3 - - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - - sphinx_rtd_theme - - pexpect - - beautifulsoup4 - - Antlr4 runtime for Python 3 - - -Under recent Debian based operating systems (Debian 10 "Buster", -Ubuntu 18.04, ...) a working set of packages for compiling the -documentation for Coq is: - - texlive-latex-extra texlive-fonts-recommended python3-sphinx - python3-pexpect python3-sphinx-rtd-theme python3-bs4 - python3-sphinxcontrib.bibtex python3-pip - -Then, install the Python3 Antlr4 package: - - pip3 install antlr4-python3-runtime - -Nix users should get the correct development environment to build the -HTML documentation from Coq's `default.nix`. [Note Nix setup doesn't -include the LaTeX packages needed to build the full documentation.] - -If you are in an older/different distribution you can install the -Python packages required to build the user manual using python3-pip: - - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex - -Compilation ------------ - -To produce all documentation about Coq, just run: - - ./configure (if you hadn't already) - make doc - - -Alternatively, you can use some specific targets: - - make doc-ps - to produce all PostScript documents - - make doc-pdf - to produce all PDF documents - - make doc-html - to produce all html documents - - make sphinx - to produce the HTML version of the reference manual - - make stdlib - to produce all formats of the Coq standard library - - -Also note the "-with-doc yes" option of ./configure to enable the -build of the documentation as part of the default make target. - - -Installation ------------- - -To install all produced documents, do: - - make DOCDIR=/some/directory/for/documentation install-doc - -DOCDIR defaults to /usr/share/doc/coq diff --git a/INSTALL.ide b/INSTALL.ide deleted file mode 100644 index c4da84048..000000000 --- a/INSTALL.ide +++ /dev/null @@ -1,123 +0,0 @@ - CoqIde Installation procedure - -CoqIde is a graphical interface to perform interactive proofs. -You should be able to do everything you do in coqtop inside CoqIde -excepted dropping to the ML toplevel. - - -DISTRIBUTION PACKAGES - -Your POSIX operating system may already contain precompiled packages -for Coq, including CoqIde, or a ready-to-compile... If the version -provided there suits you, follow the usual procedure for your -operating system. - -E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do: - aptitude install coqide -On Gentoo GNU/Linux, do: - USE=ide emerge sci-mathematics/coq - -Else, read the rest of this document to compile your own CoqIde. - - -COMPILATION REQUIREMENTS - -- OCaml >= 4.02.3 with native threads support. -- make world must succeed. -- The graphical toolkit GTK+ 2.x. See http://www.gtk.org. - The official supported version is at least 2.24.x. - You may still compile CoqIde with older versions and use all features. - Run - - pkg-config --modversion gtk+-2.0 - - to check your version. - Do not forget to install the development headers packages. - - On Debian, installing lablgtk2 (see below) will automatically - install GTK+. (But "aptitude install libgtk2.0-dev" will - install GTK+ 2.x, should you need to force it for one reason - or another.) -- The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. - You need at least version 2.18.3. - - Your distribution may contain precompiled packages. For example, for - Debian, run - - aptitude install liblablgtksourceview2-ocaml-dev - - for Mandriva, run - - urpmi ocaml-lablgtk-devel - - If it does not, see http://lablgtk.forge.ocamlcore.org/ - - The basic command installing lablgtk2 from the source package is: - - ./configure && make world && make install - - You must have write access to the OCaml standard library path. - If this fails, read the README. - - -INSTALLATION - -0) For optimal performance, OCaml must support native threads (aka pthreads). - If this not the case, this means that Coq computations will be slow and - "make ide" will fail. Use "make bin/coqide.byte" instead. To fix this - problem, just recompile OCaml from source and configure OCaml with: - - "./configure --with-pthreads". - - In case you install over an existing copy of OCaml, you should better - empty the OCaml installation directory. - -1) Go into your Coq source directory and, as usual, configure with: - - ./configure - - This should detect the ability of making CoqIde; check in the - report printed by configure that ability to build CoqIde is detected. - - Then compile with - - make world - - and install with - - make install - - In case you are upgrading from an old version you may need to run - - make clean-ide - -2) You may now run bin/coqide - - -NOTES - -There are three configuration files located in your $(XDG_CONFIG_HOME)/coq -dir (defaulting to $HOME/.config/coq). - -- coqiderc is generated by coqide itself. It may be edited by hand or - by using the Preference menu from coqide. It will be generated the first time - you save your the preferences in Coqide. - -- coqide.keys is a standard Gtk2 accelerator dump. You may edit this file - to change the default shortcuts for the menus. - -Read ide/FAQ for more informations. - - -TROUBLESHOOTING - -- Problem with automatic templates - - Some users may experiment problems with unwanted automatic - templates while using Coqide. This is due to a change in the - modifiers keys available through GTK. The straightest way to get - rid of the problem is to edit by hand your coqiderc (either - /home/<user>/.config/coq/coqiderc under Linux, or - C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows) - and replace any occurrence of MOD4 by MOD1. - diff --git a/Makefile.ci b/Makefile.ci index 7f63157fa..fce16906c 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -8,7 +8,8 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## -CI_TARGETS=ci-bignums \ +CI_TARGETS=ci-bedrock2 \ + ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ @@ -18,7 +18,9 @@ or refer to the [`INSTALL` file](INSTALL) for the procedure to install from sour ## Documentation -The sources of the documentation can be found in directory [`doc`](doc). The +The sources of the documentation can be found in directory [`doc`](doc). +See [`doc/README.md`](/doc/README.md) to learn more about the documentation, +in particular how to build it. The documentation of the last released version is available on the Coq web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). See also [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), diff --git a/checker/cic.mli b/checker/cic.mli index a890f2cef..4846a9af8 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -33,11 +33,10 @@ open Names (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type sorts = - | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) + | Prop + | Set + | Type of Univ.universe (** {6 The sorts family of CCI. } *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 916934a81..bcb71fe55 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t = (* Prop and Set are small *) let is_small_sort = function - | Prop _ -> true + | Prop | Set -> true | _ -> false let is_logic_sort = function -| Prop Null -> true +| Prop -> true | _ -> false (* [infos] is a sequence of pair [islogic,issmall] for each type in @@ -186,10 +186,10 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, ImpredicativeSet -> () - | Prop Pos, _ -> + | Set, ImpredicativeSet -> () + | Set, _ -> if not small then failwith "impredicative Set inductive type" - | Prop Null,_ -> () + | Prop,_ -> () let sort_of_ind = function diff --git a/checker/inductive.ml b/checker/inductive.ml index e1c6b135d..b1edec556 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -101,7 +101,7 @@ let instantiate_params full t u args sign = substl subs ty let full_inductive_instantiate mib u params sign = - let dummy = Prop Null in + let dummy = Prop in let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) @@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> Univ.type0m_univ -| Prop Pos -> Univ.type0_univ +| Prop -> Univ.type0m_univ +| Set -> Univ.type0_univ (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) (* in the domain or add [u |-> sup x su] if [u] is already mapped *) @@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts = let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) - if Univ.is_type0m_univ level then Prop Null + if Univ.is_type0m_univ level then Prop (* Non singleton type not containing types are interpretable in Set *) - else if Univ.is_type0_univ level then Prop Pos + else if Univ.is_type0_univ level then Set (* This is a Type with constraints *) else Type level in @@ -226,8 +226,8 @@ let type_of_inductive env mip = (* The max of an array of universes *) let cumulate_constructor_univ u = function - | Prop Null -> u - | Prop Pos -> Univ.sup Univ.type0_univ u + | Prop -> u + | Set -> Univ.sup Univ.type0_univ u | Type u' -> Univ.sup u u' let max_inductive_sort = diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ca9581167..6b2af71f3 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -2,7 +2,6 @@ open Pp open Util open Names open Cic -open Term open Reduction open Typeops open Indtypes @@ -13,17 +12,6 @@ open Environ (** {6 Checking constants } *) -let refresh_arity ar = - let ctxt, hd = decompose_prod_assum ar in - match hd with - Sort (Type u) when not (Univ.is_univ_variable u) -> - let ul = Univ.Level.make DirPath.empty 1 in - let u' = Univ.Universe.make ul in - let cst = Univ.enforce_leq u u' Univ.empty_constraint in - let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in - mkArity (ctxt,Prop Null), ctx - | _ -> ar, Univ.ContextSet.empty - let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); (** Locally set the oracle for further typechecking *) @@ -37,18 +25,13 @@ let check_constant_declaration env kn cb = let ctx = Univ.AUContext.repr auctx in push_context ~strict:false ctx env in - let envty, ty = - let ty = cb.const_type in - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in - envty, ty - in - let () = + let ty = cb.const_type in + let _ = infer_type env' ty in + let () = match body_of_constant cb with | Some bd -> - let j = infer envty bd in - conv_leq envty j ty + let j = infer env' bd in + conv_leq env' j ty | None -> () in let env = diff --git a/checker/print.ml b/checker/print.ml index fc9cd687e..247c811f8 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -57,8 +57,8 @@ let print_pure_constr fmt csr = fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c and pp_sort fmt = function - | Prop(Pos) -> pp_print_string fmt "Set" - | Prop(Null) -> pp_print_string fmt "Prop" + | Set -> pp_print_string fmt "Set" + | Prop -> pp_print_string fmt "Prop" | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) and pp_name fmt = function diff --git a/checker/reduction.ml b/checker/reduction.ml index 4e508dc77..16c701213 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -210,29 +210,26 @@ let convert_constructors let sort_cmp env univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible - | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible - | (Prop c1, Type u) -> + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) | Set, Type _ -> + if not (pb = CUMUL) then raise NotConvertible + | Type u1, Type u2 -> + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with - CUMUL -> () - | _ -> raise NotConvertible) - | (Type u1, Type u2) -> - (** FIXME: handle type-in-type option here *) - if (* snd (engagement env) == StratifiedType && *) - not - (match pb with - | CONV -> Univ.check_eq univ u1 u2 - | CUMUL -> Univ.check_leq univ u1 u2) - then begin - if !Flags.debug then begin - let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( - str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ) - end; - raise NotConvertible - end - | (_, _) -> raise NotConvertible + | CONV -> Univ.check_eq univ u1 u2 + | CUMUL -> Univ.check_leq univ u1 u2) + then begin + if !Flags.debug then begin + let op = match pb with CONV -> "=" | CUMUL -> "<=" in + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) + end; + raise NotConvertible + end + | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible let rec no_arg_available = function | [] -> true diff --git a/checker/subtyping.ml b/checker/subtyping.ml index a22af4e0f..6d0d6f6c6 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -9,7 +9,6 @@ (************************************************************************) (*i*) -open CErrors open Util open Names open Cic @@ -132,40 +131,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (eq_constr) (fun x -> x.proj_type); true in - let check_inductive_type t1 t2 = - - (* Due to template polymorphism, the conclusions of - t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. - - By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U - |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each - universe in the conclusion of t1 has an bounding universe in - the conclusion of t2, so that we don't need to check the - subtyping of the conclusions of t1 and t2. - - Even if we'd like to recheck it, the inference of constraints - is not designed to deal with algebraic constraints of the form - max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy - to recheck it (in short, we would need the actual graph of - constraints as input while type checking is currently designed - to output a set of constraints instead) *) - - (* So we cheat and replace the subtyping problem on algebraic - constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) - (that we know are necessary true) by trivial constraints that - the constraint generator knows how to deal with *) - - let (ctx1,s1) = dest_arity env t1 in - let (ctx2,s2) = dest_arity env t2 in - let s1,s2 = - match s1, s2 with - | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null - | (Prop _, Type _) | (Type _,Prop _) -> error () - | _ -> (s1, s2) in - check_conv conv_leq env - (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) - in + let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in let check_packet p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -254,52 +220,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (Univ.is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (Univ.is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - error () - with UserError _ (* "not an arity" *) -> - error () end - | _ -> t1,t2 - else - (t1,t2) in - check_conv conv_leq env t1 t2 - in + let check_type env t1 t2 = check_conv conv_leq env t1 t2 in match info1 with | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in diff --git a/checker/term.ml b/checker/term.ml index 509634bdb..d84491b38 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -20,15 +20,15 @@ open Cic (* Sorts. *) let family_of_sort = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type _ -> InType let family_equal = (==) let sort_of_univ u = - if Univ.is_type0m_univ u then Prop Null - else if Univ.is_type0_univ u then Prop Pos + if Univ.is_type0m_univ u then Prop + else if Univ.is_type0_univ u then Set else Type u (********************************************************************) @@ -356,15 +356,11 @@ let rec isArity c = (* alpha conversion : ignore print names and casts *) let compare_sorts s1 s2 = match s1, s2 with -| Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> true - | Pos, Null -> false - | Null, Pos -> false - end +| Prop, Prop | Set, Set -> true | Type u1, Type u2 -> Univ.Universe.equal u1 u2 -| Prop _, Type _ -> false -| Type _, Prop _ -> false +| Prop, Set | Set, Prop -> false +| (Prop | Set), Type _ -> false +| Type _, (Prop | Set) -> false let eq_puniverses f (c1,u1) (c2,u2) = Univ.Instance.equal u1 u2 && f c1 c2 diff --git a/checker/typeops.ml b/checker/typeops.ml index 345ee5b8f..19ede4b9a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | _, Prop -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | (Prop | Set), Set -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | Type u1, Set -> if engagement env = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Univ.sup u1 Univ.type0_univ) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2) + | Set, Type u2 -> Type (Univ.sup Univ.type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | Prop, Type _ -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Univ.sup u1 u2) + | Type u1, Type u2 -> Type (Univ.sup u1 u2) (* Type of a type cast *) @@ -239,7 +239,7 @@ let type_fixpoint env lna lar lbody vdefj = let rec execute env cstr = match cstr with (* Atomic terms *) - | Sort (Prop _) -> judge_of_prop + | Sort (Prop | Set) -> judge_of_prop | Sort (Type u) -> judge_of_type u diff --git a/checker/univ.ml b/checker/univ.ml index 15673736f..e50e883ad 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -190,13 +190,6 @@ struct (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) - let leq (u,n) (v,n') = - let cmp = Level.compare u v in - if Int.equal cmp 0 then n <= n' - else if n <= n' then - (Level.is_prop u && Level.is_small v) - else false - let successor (u,n) = if Level.is_prop u then type1 else (u, n + 1) @@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -let constraint_add_leq v u c = - (* We just discard trivial constraints like u<=u *) - if Expr.equal v u then c - else - match v, u with - | (x,n), (y,m) -> - let j = m - n in - if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then - Constraint.add (x,Lt,y) c - else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then - if Level.equal x y then (* u+(k+1) <= u *) - raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") - else if j = 0 then - Constraint.add (x,Le,y) c - else (* j >= 1 *) (* m = n + k, u <= v+k *) - if Level.equal x y then c (* u <= u+k, trivial *) - else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") - -let check_univ_leq_one u v = Universe.exists (Expr.leq u) v - -let check_univ_leq u v = - Universe.for_all (fun u -> check_univ_leq_one u v) u - -let enforce_leq u v c = - match v with - | [v] -> - List.fold_right (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable.") - -let enforce_leq u v c = - if check_univ_leq u v then c - else enforce_leq u v c - let check_constraint g (l,d,r) = match d with | Eq -> check_equal g l r diff --git a/checker/univ.mli b/checker/univ.mli index 6cd3b3638..3b29b158f 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -val enforce_leq : universe constraint_function - (** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given diff --git a/checker/values.ml b/checker/values.ml index 4f28d6e44..88cdb644d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli +MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli *) @@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] diff --git a/clib/cList.ml b/clib/cList.ml index 2b627f745..de42886dc 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -122,6 +122,7 @@ sig val duplicates : 'a eq -> 'a list -> 'a list val uniquize : 'a list -> 'a list val sort_uniquize : 'a cmp -> 'a list -> 'a list + val min : 'a cmp -> 'a list -> 'a val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list val combinations : 'a list list -> 'a list list @@ -971,6 +972,15 @@ let rec uniquize_sorted cmp = function let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l) +let min cmp l = + let rec aux cur = function + | [] -> cur + | x :: l -> if cmp x cur < 0 then aux x l else aux cur l + in + match l with + | x :: l -> aux x l + | [] -> raise Not_found + let rec duplicates cmp = function | [] -> [] | x :: l -> diff --git a/clib/cList.mli b/clib/cList.mli index 13e069e94..42fae5ed3 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -376,6 +376,11 @@ sig (** Return a sorted version of a list without duplicates according to some comparison function. *) + val min : 'a cmp -> 'a list -> 'a + (** Return minimum element according to some comparison function. + + @raise Not_found on an empty list. *) + (** {6 Cartesian product} *) val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index f960ff008..5af0fcff3 100644..100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -255,6 +255,7 @@ IF NOT "%~0" == "" ( IF NOT EXIST %SETUP% ( ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html. + ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option. GOTO :EOF ) @@ -385,7 +386,6 @@ IF "%RUNSETUP%"=="Y" ( MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" ) - IF NOT "%CYGWIN_QUIET%" == "Y" ( REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it. REM This is not required with the -cygquiet=Y and the resulting --no-admin option. @@ -396,6 +396,12 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ========== +REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear +REM HOME (otherwise we get to the home directory of the other installation) +REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user) +SET "HOME=" +SET "PROFILEREAD=" + copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 508dcf5fb..a4e60744f 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -118,6 +118,9 @@ mkdir -p "$PREFIX/bin" mkdir -p "$PREFIXCOQ/bin" mkdir -p "$PREFIXOCAML/bin" +# This is required for building addons and plugins +export COQBIN=$RESULT_INSTALLDIR_CFMT/bin/ + ###################### Copy Cygwin Setup Info ##################### # Copy Cygwin repo ini file and installed files db to tarballs folder. @@ -1128,14 +1131,12 @@ function copy_coq_license { install -D doc/LICENSE "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt" install -D LICENSE "$PREFIXCOQ/license_readme/coq/License.txt" install -D plugins/micromega/LICENSE.sos "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt" - install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true - install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true - install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true + # FIXME: this is not the micromega license + # It only applies to code that was copied into one single file! + install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" - install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" - install -D INSTALL.ide "$PREFIXCOQ/license_readme/coq/InstallIde.txt" + install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" fi } @@ -1211,6 +1212,10 @@ function make_coq { # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean + # Copy these files somewhere the plugin builds can find them + cp dev/ci/ci-basic-overlay.sh /build/ + cp -r dev/ci/user-overlays /build/ + build_post fi } @@ -1378,8 +1383,16 @@ function make_coq_installer { ###################### ADDONS ##################### +# The bignums library +# Provides BigN, BigZ, BigQ that used to be part of Coq standard library + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then + bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_BRANCH" | cut -f 1) + if [[ "$bignums_SHA" == "" ]]; then + # $bignums_CI_BRANCH must have been a tag and not a branch + bignums_SHA="$bignums_CI_BRANCH" + fi + if build_prep "${bignums_CI_GITURL}/archive" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1388,7 +1401,54 @@ function make_addon_bignums { fi } +# Ltac-2 plugin +# A new (experimental) tactic language + +function make_addon_ltac2 { + ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_BRANCH" | cut -f 1) + if [[ "$ltac2_SHA" == "" ]]; then + # $ltac2_CI_BRANCH must have been a tag and not a branch + ltac2_SHA="$ltac2_CI_BRANCH" + fi + if build_prep "${ltac2_CI_GITURL}/archive" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then + log1 make all + log2 make install + build_post + fi +} + +# Equations plugin +# A function definition plugin + +function make_addon_equations { + Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_BRANCH" | cut -f 1) + if [[ "$Equations_SHA" == "" ]]; then + # $Equations_CI_BRANCH must have been a tag and not a branch + Equations_SHA="$Equations_CI_BRANCH" + fi + if build_prep "${Equations_CI_GITURL}/archive" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then + # Note: PATH is autmatically saved/restored by build_prep / build_post + PATH=$COQBIN:$PATH + logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile + log1 make + log2 make install + build_post + fi +} + function make_addons { + if [ -n "${GITLAB_CI}" ]; then + export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi + fi + . /build/ci-basic-overlay.sh + for overlay in /build/user-overlays/*.sh; do + . "$overlay" + done + for addon in $COQ_ADDONS; do "make_addon_$addon" done diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 3807ff90c..28321d13e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -10,123 +10,123 @@ # MathComp ######################################################################## : "${mathcomp_CI_BRANCH:=master}" -: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" : "${oddorder_CI_BRANCH:=master}" -: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" ######################################################################## # UniMath ######################################################################## : "${UniMath_CI_BRANCH:=master}" -: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" +: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" ######################################################################## # Unicoq + Mtac2 ######################################################################## : "${unicoq_CI_BRANCH:=master}" -: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" +: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" : "${mtac2_CI_BRANCH:=master-sync}" -: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}" +: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" ######################################################################## # Mathclasses + Corn ######################################################################## : "${math_classes_CI_BRANCH:=master}" -: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}" +: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes}" : "${Corn_CI_BRANCH:=master}" -: "${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}" +: "${Corn_CI_GITURL:=https://github.com/c-corn/corn}" ######################################################################## # Iris ######################################################################## : "${stdpp_CI_BRANCH:=master}" -: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" : "${Iris_CI_BRANCH:=master}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" : "${lambdaRust_CI_BRANCH:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" ######################################################################## # HoTT ######################################################################## : "${HoTT_CI_BRANCH:=master}" -: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}" +: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" ######################################################################## # Ltac2 ######################################################################## : "${ltac2_CI_BRANCH:=master}" -: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}" +: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" ######################################################################## # GeoCoq ######################################################################## : "${GeoCoq_CI_BRANCH:=master}" -: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}" +: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" ######################################################################## # Flocq ######################################################################## : "${Flocq_CI_BRANCH:=master}" -: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}" +: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" ######################################################################## # Coquelicot ######################################################################## : "${Coquelicot_CI_BRANCH:=master}" -: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}" +: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" ######################################################################## # CompCert ######################################################################## : "${CompCert_CI_BRANCH:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}" +: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" ######################################################################## # VST ######################################################################## : "${VST_CI_BRANCH:=master}" -: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}" +: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" ######################################################################## # cross-crypto ######################################################################## : "${cross_crypto_CI_BRANCH:=master}" -: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}" +: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" ######################################################################## # fiat_parsers ######################################################################## : "${fiat_parsers_CI_BRANCH:=master}" -: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}" +: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" ######################################################################## # fiat_crypto ######################################################################## : "${fiat_crypto_CI_BRANCH:=master}" -: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}" +: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" ######################################################################## # formal-topology ######################################################################## : "${formal_topology_CI_BRANCH:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}" +: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" ######################################################################## # coq-dpdgraph ######################################################################## : "${coq_dpdgraph_CI_BRANCH:=coq-master}" -: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" +: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" ######################################################################## # CoLoR ######################################################################## : "${CoLoR_CI_BRANCH:=master}" -: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}" +: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" ######################################################################## # SF @@ -139,46 +139,52 @@ # TLC ######################################################################## : "${tlc_CI_BRANCH:=master}" -: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}" +: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## : "${bignums_CI_BRANCH:=master}" -: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}" +: "${bignums_CI_GITURL:=https://github.com/coq/bignums}" + +######################################################################## +# bedrock2 +######################################################################## +: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" ######################################################################## # Equations ######################################################################## : "${Equations_CI_BRANCH:=master}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" +: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" ######################################################################## # Elpi ######################################################################## : "${Elpi_CI_BRANCH:=coq-master}" -: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" +: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" ######################################################################## # fcsl-pcm ######################################################################## : "${fcsl_pcm_CI_BRANCH:=master}" -: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" +: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" ######################################################################## # pidetop ######################################################################## : "${pidetop_CI_BRANCH:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" ######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_BRANCH:=master}" -: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" ######################################################################## # quickchick ######################################################################## : "${quickchick_CI_BRANCH:=master}" -: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh new file mode 100755 index 000000000..447076e09 --- /dev/null +++ b/dev/ci/ci-bedrock2.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" + +git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" +( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) + +( cd "${bedrock2_CI_DIR}" && make ) diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 70278e6d0..973319de6 100644 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -28,7 +28,7 @@ if exist %DESTCOQ%\ rd /s /q %DESTCOQ% 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 -make=N ^ + -addon="bignums ltac2 equations" -make=N ^ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit diff --git a/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh b/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh deleted file mode 100644 index 9d96b6d4c..000000000 --- a/dev/ci/user-overlays/00664-herbelin-master+change-for-coq-pr664-compatibility.sh +++ /dev/null @@ -1,4 +0,0 @@ - if [ "$CI_PULL_REQUEST" = "664" ] || [ "$CI_BRANCH" = "trunk+fix-5500-too-weak-test-return-clause" ]; then - fiat_parsers_CI_BRANCH=master+change-for-coq-pr664-compatibility - fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat -fi diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index e9ba11414..e6a2c4460 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -2,5 +2,5 @@ if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi diff --git a/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh deleted file mode 100644 index f4cb71cf1..000000000 --- a/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then - - # ltac2_CI_BRANCH=econstr+more_fix - # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=evar+strict_to_constr - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh deleted file mode 100644 index b22ab3630..000000000 --- a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ - [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then - - pidetop_CI_BRANCH=stm+top - pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git - -fi diff --git a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh deleted file mode 100644 index cf2af9ae9..000000000 --- a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6960" ] || [ "$CI_BRANCH" = "ltac+tacdepr" ]; then - - # Equations_CI_BRANCH=ssr+correct_packing - # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_BRANCH=ltac+tacdepr - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - # Elpi_CI_BRANCH=ssr+correct_packing - # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh deleted file mode 100644 index e6c48d10a..000000000 --- a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then - Equations_CI_BRANCH=unification-returns-option - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07136-evar-map-econstr.sh b/dev/ci/user-overlays/07136-evar-map-econstr.sh deleted file mode 100644 index 06aa62726..000000000 --- a/dev/ci/user-overlays/07136-evar-map-econstr.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7136" ] || [ "$CI_BRANCH" = "evar-map-econstr" ]; then - Equations_CI_BRANCH=8.9+alpha - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git - - Elpi_CI_BRANCH=coq-7136 - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh deleted file mode 100644 index 7e554684e..000000000 --- a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then - - # Equations_CI_BRANCH=ssr+correct_packing - # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - # ltac2_CI_BRANCH=ssr+correct_packing - # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Elpi_CI_BRANCH=api+vernac_expr_iso - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh deleted file mode 100644 index ea9cd8ee0..000000000 --- a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh +++ /dev/null @@ -1,21 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then - - # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 - # - # equations - # ltac2 - - # The below developments should instead use a backwards compatible fix. - # - # color - # iris-lambda-rust - # math-classes - # formal-topology - - ltac2_CI_BRANCH=tactics+push_fix_naming_out - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=tactics+push_fix_naming_out - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh deleted file mode 100644 index 517088a24..000000000 --- a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then - - ltac2_CI_BRANCH=fast-constr-match-no-context - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - -fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh deleted file mode 100644 index 6939ead2b..000000000 --- a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then - - # this branch contains a commit not present on coq-master that triggers - # the universe restriction bug #7472 - Elpi_CI_BRANCH=overlay-7495 - Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh deleted file mode 100644 index 115f29f1e..000000000 --- a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh +++ /dev/null @@ -1,14 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then - - _OVERLAY_BRANCH=vernac+move_parser - - Equations_CI_BRANCH="$_OVERLAY_BRANCH" - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_BRANCH="$_OVERLAY_BRANCH" - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - mtac2_CI_BRANCH="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh deleted file mode 100644 index b4f716139..000000000 --- a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=misctypes+bye2 - -if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then - - Equations_CI_BRANCH="$_OVERLAY_BRANCH" - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh deleted file mode 100644 index f7811cd6f..000000000 --- a/dev/ci/user-overlays/07797-rm-reference.sh +++ /dev/null @@ -1,20 +0,0 @@ -_OVERLAY_BRANCH=rm-reference - -if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then - - Equations_CI_BRANCH="$_OVERLAY_BRANCH" - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git - - ltac2_CI_BRANCH="fix-7797" - ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git - - quickchick_CI_BRANCH="$_OVERLAY_BRANCH" - quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git - - coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH" - coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git - - Elpi_CI_BRANCH="$_OVERLAY_BRANCH" - Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/07863-rm-sorts-contents.sh b/dev/ci/user-overlays/07863-rm-sorts-contents.sh new file mode 100644 index 000000000..374a61484 --- /dev/null +++ b/dev/ci/user-overlays/07863-rm-sorts-contents.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7863" ] || [ "$CI_BRANCH" = "rm-sorts-contents" ]; then + Elpi_CI_BRANCH=fix-sorts-contents + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/07906-univs-of-constr.sh b/dev/ci/user-overlays/07906-univs-of-constr.sh new file mode 100644 index 000000000..071665087 --- /dev/null +++ b/dev/ci/user-overlays/07906-univs-of-constr.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7906" ] || [ "$CI_BRANCH" = "univs-of-constr-noseff" ]; then + Equations_CI_BRANCH=fix-univs-of-constr + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git + + Elpi_CI_BRANCH=fix-universes-of-constr + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 41212568d..11e4d9ae0 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -24,7 +24,7 @@ Example: `00669-maximedenes-ssr-merge.sh` containing if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 844ad9188..811abd67f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -301,8 +301,8 @@ let constr_display csr = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ()) and sort_display = function - | Prop(Pos) -> "Prop(Pos)" - | Prop(Null) -> "Prop(Null)" + | Set -> "Set" + | Prop -> "Prop" | Type u -> univ_display u; "Type("^(string_of_int !cnt)^")" @@ -423,8 +423,8 @@ let print_pure_constr csr = Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u) and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> open_hbox(); print_string "Type("; pp (pr_uni u); print_string ")"; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 7589e5348..c8385da61 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -26,8 +26,8 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> print_string "Type" diff --git a/doc/LICENSE b/doc/LICENSE index c9f574afb..3789d9104 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,7 +2,7 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font +copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 @@ -18,7 +18,7 @@ The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and the PostScript, PDF and html outputs) are copyright (c) INRIA -1999-2006. The material connected to the Standard Library is +1999-2018. The material connected to the Standard Library is distributed under the terms of the Lesser General Public License version 2.1 or later. diff --git a/doc/README.md b/doc/README.md new file mode 100644 index 000000000..6c6e1f01f --- /dev/null +++ b/doc/README.md @@ -0,0 +1,102 @@ +The Coq documentation +===================== + +The Coq documentation includes + +- A Reference Manual +- A document presenting the Coq standard library + +The documentation of the latest released version is available on the Coq +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). + +Additionnally, you can view the documentation for the current master version at +<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. + +The reference manual is written is reStructuredText and compiled +using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst) +to learn more about the format that is used. + +The documentation for the standard library is generated from +the `.v` source files using coqdoc. + +Dependencies +------------ + +### HTML documentation + +To produce the complete documentation in HTML, you will need Coq dependencies +listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based +reference manual requires Python 3, and the following Python packages: + + sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + +You can install them using `pip3 install` or using your distribution's package +manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) you can use: + + apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ + python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +Then, install the missing Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +HTML documentation from Coq's [`default.nix`](../default.nix) (note this +doesn't include the LaTeX packages needed to build the full documentation). + +### Other formats + +To produce the documentation in PDF and PostScript formats, the following +additional tools are required: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex + +Install them using your package manager. E.g. on Debian / Ubuntu: + + apt install texlive-latex-extra texlive-fonts-recommended + +Compilation +----------- + +To produce all documentation about Coq in all formats, just run: + + ./configure # (if you hadn't already) + make doc + + +Alternatively, you can use some specific targets: + +- `make doc-ps` + to produce all PostScript documents + +- `make doc-pdf` + to produce all PDF documents + +- `make doc-html` + to produce all HTML documents + +- `make sphinx` + to produce the HTML version of the reference manual + +- `make stdlib` + to produce all formats of the Coq standard library + + +Also note the `-with-doc yes` option of `./configure` to enable the +build of the documentation as part of the default make target. + + +Installation +------------ + +To install all produced documents, do: + + make install-doc + +This will install the documentation in `/usr/share/doc/coq` unless you +specify another value through the `-docdir` option of `./configure` or the +`DOCDIR` environment variable. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 6c7258f9c..68b5b9d6f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -296,6 +296,10 @@ Variants: This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined. + .. warn:: @ident is already declared as a typeclass + + This command has no effect when used on a typeclass. + .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } The :cmd:`Instance` command is used to declare a type class instance named diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3e988709c..3574bf675 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} +@InProceedings{Pit16, + Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, + Author = {Pit-Claudel, Clément and Courtieu, Pierre}, + Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, + Year = {2016}, + Month = jan, + Doi = {10.5281/zenodo.44331}, } @Book{RC95, diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index f3ae49381..baf2e0d98 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -84,3 +84,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected. + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bc72877b6..c7bc69db4 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -28,37 +28,35 @@ programs called *tactics*. All services of the |Coq| proof assistant are accessible by interpretation of a command language called *the vernacular*. -Coq has an interactive mode in which commands are interpreted as the +Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file. -- The interactive mode may be used as a debugging mode in which the - user can develop his theories and proofs step by step, backtracking - if needed and so on. The interactive mode is run with the `coqtop` - command from the operating system (which we shall assume to be some - variety of UNIX in the rest of this document). +- In interactive mode, users can develop their theories and proofs step by + step, and query the system for available theorems and definitions. The + interactive mode is generally run with the help of an IDE, such + as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, + Emacs with Proof-General :cite:`Asp00` [#PG]_, + or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). + The `coqtop` read-eval-print-loop can also be used directly, for debugging + purposes. - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the `coqc` - command from the operating system. + command. -These two modes are documented in Chapter :ref:`thecoqcommands`. - -Other modes of interaction with |Coq| are possible: through an emacs shell -window, an emacs generic user-interface for proof assistant (Proof -General :cite:`ProofGeneral`) or through a customized -interface (PCoq :cite:`Pcoq`). These facilities are not -documented here. There is also a |Coq| Integrated Development Environment -described in :ref:`coqintegrateddevelopmentenvironment`. +.. seealso:: :ref:`thecoqcommands`. How to read this book ===================== -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. +This is a Reference Manual, so it is not made for a continuous reading. +We recommend using the various indexes to quickly locate the documentation +you are looking for. There is a global index, and a number of specific indexes +for tactics, vernacular commands, and error messages and warnings. +Nonetheless, the manual has some structure that is explained below. - The first part describes the specification language, |Gallina|. Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete @@ -68,7 +66,7 @@ below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in five +- The second part describes the proof engine. It is divided in six chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -79,24 +77,24 @@ below. *tactics*. The language to combine these tactics into complex proof strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. + Finally, the |SSR| proof language is presented in + Chapter :ref:`thessreflectprooflanguage`. -- The third part describes how to extend the syntax of |Coq|. It - corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. +- The third part describes how to extend the syntax of |Coq| in + Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define + new induction principles in Chapter :ref:`proofschemes`. - In the fourth part more practical tools are documented. First in Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and `coqtop` (interactive mode) with their options is described. Then, in Chapter :ref:`utilities`, various utilities that come with the |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes the |Coq| integrated development environment. + describes CoqIDE. - The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list. -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error messages. - List of additional documentation ================================ @@ -109,5 +107,5 @@ Installation The |Coq| standard library A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is given - in the additional document `Library.ps`. + (including only the specifications, the proofs are removed) is + available at https://coq.inria.fr/stdlib/. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c21d8d4ec..294ac5799 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -23,8 +23,9 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. + record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive + record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` @@ -167,12 +168,13 @@ and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` In each case, `term` is the object projected and the other arguments are the parameters of the inductive type. + .. note:: Records defined with the ``Record`` keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - A *caveat*, however, is that records cannot appear in mutually inductive - (or co-inductive) definitions. + Definition of mutal inductive or co-inductive records are also allowed, as long + as all of the types in the block are records. .. note:: Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 6810626ad..005ef1635 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr env sigma c = +let universes_of_constr sigma c = let open Univ in - let open Declarations in let rec aux s c = match kind sigma c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9d3e782b..913825a9f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1625f6fc8..0c044f20d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -426,10 +426,6 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter ?src candidates = - let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - Evd.declare_future_goal evk' evd, evk' - let new_pure_evar_full evd evi = let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in @@ -547,11 +543,33 @@ let generalize_evar_over_rels sigma (ev,args) = type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential +| NoCandidatesLeft of Evar.t exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option exception Depends of Id.t +let set_of_evctx l = + List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l + +let filter_effective_candidates evd evi filter candidates = + let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in + List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates + +let restrict_evar evd evk filter ?src candidates = + let evar_info = Evd.find_undefined evd evk in + let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in + match candidates with + | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) + | _ -> + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in + (** Mark new evar as future goal, removing previous one, + circumventing Proofview.advance but making Proof.run_tactic catch these. *) + let future_goals = Evd.save_future_goals evd in + let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in + let evd = Evd.restore_future_goals evd future_goals in + (Evd.declare_future_goal evk' evd, evk') + let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of @@ -621,7 +639,9 @@ let rec check_and_clear_in_constr env evdref err ids global c = let origfilter = Evd.evar_filter evi in let filter = Evd.Filter.apply_subfilter origfilter filter in let evd = !evdref in - let (evd,_) = restrict_evar evd evk filter None in + let candidates = Evd.evar_candidates evi in + let candidates = Option.map (List.map EConstr.of_constr) candidates in + let (evd,_) = restrict_evar evd evk filter candidates in evdref := evd; Evd.existential_value0 !evdref ev diff --git a/engine/evarutil.mli b/engine/evarutil.mli index db638be9e..8ce1b625f 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -65,9 +65,6 @@ val new_type_evar : val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val restrict_evar : evar_map -> Evar.t -> Filter.t -> - ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t - (** Polymorphic constants *) val new_global : evar_map -> GlobRef.t -> evar_map * constr @@ -231,9 +228,18 @@ raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential +| NoCandidatesLeft of Evar.t exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option +(** Restrict an undefined evar according to a (sub)filter and candidates. + The evar will be defined if there is only one candidate left, +@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates + into an empty list. *) + +val restrict_evar : evar_map -> Evar.t -> Filter.t -> + ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t + val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> Id.Set.t -> evar_map * named_context_val * types diff --git a/engine/evd.ml b/engine/evd.ml index 714a0b645..761ae7983 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -171,6 +171,8 @@ let evar_context evi = named_context_of_val evi.evar_hyps let evar_filtered_context evi = Filter.filter_list (evar_filter evi) (evar_context evi) +let evar_candidates evi = evi.evar_candidates + let evar_hyps evi = evi.evar_hyps let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with @@ -620,6 +622,7 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } +(* TODO: make unique *) let add_conv_pb ?(tail=false) pb d = if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -852,7 +855,7 @@ let normalize_universe_instance evd l = let normalize_sort evars s = match s with - | Prop _ -> s + | Prop | Set -> s | Type u -> let u' = normalize_universe evars u in if u' == u then s else Type u' diff --git a/engine/evd.mli b/engine/evd.mli index d166fd804..64db70451 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -113,6 +113,7 @@ val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body +val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t val evar_env : evar_info -> env val evar_filtered_env : evar_info -> env @@ -243,7 +244,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) + possibly limiting the instances to a set of candidates (candidates + are filtered according to the filter) *) val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) diff --git a/engine/namegen.ml b/engine/namegen.ml index 23c691139..978f33b68 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -137,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *) s ^ Unicode.lowercase_first_char s' let sort_hdchar = function - | Prop(_) -> "P" - | Type(_) -> "T" + | Prop -> "P" + | Set -> "S" + | Type _ -> "T" let hdchar env sigma c = let rec hdrec k c = diff --git a/engine/termops.ml b/engine/termops.ml index 2db2e07bf..2b179c43b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -25,8 +25,8 @@ module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) let print_sort = function - | Prop Pos -> (str "Set") - | Prop Null -> (str "Prop") + | Set -> (str "Set") + | Prop -> (str "Prop") | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function @@ -1162,15 +1162,14 @@ let is_template_polymorphic env sigma f = let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb == Reduction.CUMUL - | (Type u1, Type u2) -> true - | _ -> false + | Prop, Prop | Set, Set | Type _, Type _ -> true + | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL + | Set, Prop | Type _, Prop | Type _, Set -> false let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Null -> true + | Prop -> true | _ -> false end | Cast (c,_,_) -> is_Prop sigma c @@ -1179,7 +1178,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with let rec is_Set sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Pos -> true + | Set -> true | _ -> false end | Cast (c,_,_) -> is_Set sigma c diff --git a/engine/univops.ml b/engine/univops.ml index 3fd518490..7f9672f82 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -11,24 +11,13 @@ open Univ open Constr -let universes_of_constr env c = - let open Declarations in - let rec aux s c = +let universes_of_constr c = + let rec aux s c = match kind c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s diff --git a/engine/univops.mli b/engine/univops.mli index 0b37ab975..57a53597b 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -11,8 +11,8 @@ open Constr open Univ -(** The universes of monomorphic constants appear. *) -val universes_of_constr : Environ.env -> constr -> LSet.t +(** Return the set of all universes appearing in [constr]. *) +val universes_of_constr : constr -> LSet.t (** [restrict_universe_context (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b3088ee28..9be562d3e 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -103,7 +103,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat else [] in proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); - insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); + insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) @@ -128,7 +128,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle (Some Tags.Proof.goal))); - ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) + ignore(proof#scroll_to_mark `INSERT) let rec flatten = function | [] -> [] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e217b2cd..18d6c1a5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) diff --git a/interp/declare.ml b/interp/declare.ml index e79cc6079..fcb62ac8c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,13 +383,12 @@ let inInductive : inductive_obj -> obj = rebuild_function = infer_inductive_subtyping } let declare_projections univs mind = - (** FIXME: handle mutual records *) - let mind = (mind, 0) in let env = Global.env () in - let spec,_ = Inductive.lookup_mind_specif env mind in - match spec.mind_record with - | PrimRecord info -> - let _, kns, _ = info.(0) in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter i (_, kns, _) = + let mind = (mind, i) in let projs = Inductiveops.compute_projections env mind in Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in @@ -411,10 +410,12 @@ let declare_projections univs mind = let entry = definition_entry ~types ~univs term in let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in assert (Constant.equal kn kn') - ) kns projs; - true, true - | FakeRecord -> true,false - | NotRecord -> false,false + ) kns projs + in + let () = Array.iteri iter info in + true, true + | FakeRecord -> true, false + | NotRecord -> false, false (* for initial declaration *) let declare_mind mie = diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 521f540d2..3095ce148 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -217,6 +217,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) @@ -235,8 +236,8 @@ open Util let pp_sort s = let open Sorts in match s with - | Prop Null -> str "Prop" - | Prop Pos -> str "Set" + | Prop -> str "Prop" + | Set -> str "Set" | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 238edc0af..de21401b3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -159,6 +159,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7a27a3d20..6677db2fd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -112,8 +112,9 @@ let push_fv d e = { let fv r = !(r.in_env) -let empty_comp_env ?(univs=0) ()= - { nb_uni_stack = univs; +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -148,7 +149,8 @@ let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun ?(univs=0) arity = - { nb_uni_stack = univs ; + { arity; + nb_uni_stack = univs ; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; @@ -159,7 +161,8 @@ let comp_env_fun ?(univs=0) arity = let comp_env_fix_type rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -173,7 +176,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -183,7 +187,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -197,7 +202,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -249,8 +255,15 @@ let pos_rel i r sz = Kenvacc(r.offset + pos) let pos_universe_var i r sz = - if i < r.nb_uni_stack then - Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) else let env = !(r.in_env) in let db = FVuniv_var i in @@ -498,7 +511,7 @@ let rec compile_lam env cenv lam sz cont = else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont - | Lsort (Sorts.Prop _ as s) -> + | Lsort (Sorts.Prop | Sorts.Set as s) -> compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes diff --git a/kernel/constr.ml b/kernel/constr.ml index 418229330..45812b5a1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -130,8 +130,8 @@ let mkProp = Sort Sorts.prop let mkSet = Sort Sorts.set let mkType u = Sort (Sorts.Type u) let mkSort = function - | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *) - | Sorts.Prop Sorts.Pos -> mkSet + | Sorts.Prop -> mkProp (* Easy sharing *) + | Sorts.Set -> mkSet | s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) @@ -260,17 +260,17 @@ let isSort c = match kind c with | _ -> false let rec isprop c = match kind c with - | Sort (Sorts.Prop _) -> true + | Sort (Sorts.Prop | Sorts.Set) -> true | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind c with - | Sort (Sorts.Prop Sorts.Null) -> true + | Sort Sorts.Prop -> true | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind c with - | Sort (Sorts.Prop Sorts.Pos) -> true + | Sort Sorts.Set -> true | Cast (c,_,_) -> is_Set c | _ -> false @@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if UGraph.check_leq univs u1 u2 then true else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in + cstrs := Univ.Constraint.union c !cstrs; + true + with Univ.UniverseInconsistency _ -> false) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9130b8778..584c1af03 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -130,11 +130,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = let open Sorts in function -| Type u -> u -| Prop Null -> Universe.type0m -| Prop Pos -> Universe.type0 - (* Template polymorphism *) (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) @@ -168,7 +163,7 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in + let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) @@ -236,8 +231,8 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop Null -> u - | Prop Pos -> Universe.sup Universe.type0 u + | Prop -> u + | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' let max_inductive_sort = diff --git a/kernel/modops.ml b/kernel/modops.ml index 22f523a9a..02bab581a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,7 +47,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/modops.mli b/kernel/modops.mli index ac76d28cf..8e7e618fc 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -106,7 +106,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6821fc980..74d12f3cd 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -71,6 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -86,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index da4413a0a..3901cb9ce 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -116,7 +116,7 @@ let mk_ind_accu ind u = let mk_sort_accu s u = let open Sorts in match s with - | Prop _ -> mk_accu (Asort s) + | Prop | Set -> mk_accu (Asort s) | Type s -> let u = Univ.Instance.of_array u in let s = Univ.subst_instance_universe u s in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f4af31386..3228a155f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -649,23 +649,19 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in if not (type_in_type env) then + let check_pb u0 u1 = + match pb with + | CUMUL -> check_leq univs u0 u1 + | CONV -> check_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible + | Set, Prop -> raise NotConvertible + | Set, Type u -> check_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> check_pb u Univ.type0_univ + | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -693,30 +689,27 @@ let infer_eq (univs, cstrs as cuniv) u u' = let infer_leq (univs, cstrs as cuniv) u u' = if UGraph.check_leq univs u u' then cuniv else - let cstrs' = Univ.enforce_leq u u' cstrs in - univs, cstrs' + let cstrs', _ = UGraph.enforce_leq_alg u u' univs in + univs, Univ.Constraint.union cstrs cstrs' let infer_cmp_universes env pb s0 s1 univs = - let open Sorts in - if type_in_type env then univs + if type_in_type env + then univs else + let open Sorts in + let infer_pb u0 u1 = + match pb with + | CUMUL -> infer_leq univs u0 u1 + | CONV -> infer_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) + | Prop, Prop | Set, Set -> univs + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs + | Set, Prop -> raise NotConvertible + | Set, Type u -> infer_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> infer_pb u Univ.type0_univ + | Type u0, Type u1 -> infer_pb u0 u1 let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = diff --git a/kernel/sorts.ml b/kernel/sorts.ml index daeb90be7..a7bb08f5b 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -10,22 +10,21 @@ open Univ -type contents = Pos | Null - type family = InProp | InSet | InType type t = - | Prop of contents (* proposition types *) + | Prop + | Set | Type of Universe.t -let prop = Prop Null -let set = Prop Pos +let prop = Prop +let set = Set let type1 = Type type1_univ let univ_of_sort = function | Type u -> u - | Prop Pos -> Universe.type0 - | Prop Null -> Universe.type0m + | Set -> Universe.type0 + | Prop -> Universe.type0m let sort_of_univ u = if is_type0m_univ u then prop @@ -34,36 +33,34 @@ let sort_of_univ u = let compare s1 s2 = if s1 == s2 then 0 else - match s1, s2 with - | Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> 0 - | Pos, Null -> -1 - | Null, Pos -> 1 - end - | Type u1, Type u2 -> Universe.compare u1 u2 - | Prop _, Type _ -> -1 - | Type _, Prop _ -> 1 + match s1, s2 with + | Prop, Prop -> 0 + | Prop, _ -> -1 + | Set, Prop -> 1 + | Set, Set -> 0 + | Set, _ -> -1 + | Type u1, Type u2 -> Universe.compare u1 u2 + | Type _, _ -> -1 let equal s1 s2 = Int.equal (compare s1 s2) 0 let is_prop = function - | Prop Null -> true + | Prop -> true | Type u when Universe.equal Universe.type0m u -> true | _ -> false let is_set = function - | Prop Pos -> true + | Set -> true | Type u when Universe.equal Universe.type0 u -> true | _ -> false let is_small = function - | Prop _ -> true + | Prop | Set -> true | Type u -> is_small_univ u let family = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type u when is_type0m_univ u -> InProp | Type u when is_type0_univ u -> InSet | Type _ -> InType @@ -73,15 +70,11 @@ let family_equal = (==) open Hashset.Combine let hash = function -| Prop p -> - let h = match p with - | Pos -> 0 - | Null -> 1 - in - combinesmall 1 h -| Type u -> - let h = Univ.Universe.hash u in - combinesmall 2 h + | Prop -> combinesmall 1 0 + | Set -> combinesmall 1 1 + | Type u -> + let h = Univ.Universe.hash u in + combinesmall 2 h module List = struct let mem = List.memq @@ -101,7 +94,7 @@ module Hsorts = if u' == u then c else Type u' | s -> s let eq s1 s2 = match (s1,s2) with - | (Prop c1, Prop c2) -> c1 == c2 + | Prop, Prop | Set, Set -> true | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 1bbde2608..cac6229b9 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,12 @@ (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type family = InProp | InSet | InType type t = -| Prop of contents (** Prop and Set *) -| Type of Univ.Universe.t (** Type *) + | Prop + | Set + | Type of Univ.Universe.t val set : t val prop : t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 13701d489..1e58f5c24 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -17,7 +17,6 @@ open Names open Univ open Util -open Term open Constr open Declarations open Declareops @@ -138,39 +137,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = - - (* Due to template polymorphism, the conclusions of - t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. - - By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U - |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each - universe in the conclusion of t1 has an bounding universe in - the conclusion of t2, so that we don't need to check the - subtyping of the conclusions of t1 and t2. - - Even if we'd like to recheck it, the inference of constraints - is not designed to deal with algebraic constraints of the form - max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy - to recheck it (in short, we would need the actual graph of - constraints as input while type checking is currently designed - to output a set of constraints instead) *) - - (* So we cheat and replace the subtyping problem on algebraic - constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) - (that we know are necessary true) by trivial constraints that - the constraint generator knows how to deal with *) - - let (ctx1,s1) = dest_arity env t1 in - let (ctx2,s2) = dest_arity env t2 in - let s1,s2 = - match s1, s2 with - | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop - | (Prop _, Type _) | (Type _,Prop _) -> - error (NotConvertibleInductiveField name) - | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 in let check_packet cst p1 p2 = @@ -260,53 +228,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = - let err = NotConvertibleTypeField (env, t1, t2) in - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - error NoTypeConstraintExpected - with NotArity -> - error err end - | _ -> - t1,t2 - else - (t1,t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly infer_conv_leq env t1 t2 in match info1 with | Constant cb1 -> diff --git a/kernel/term.ml b/kernel/term.ml index b44e038e9..81e344e73 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -16,14 +16,11 @@ open Vars open Constr (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/term.mli b/kernel/term.mli index f651d1a58..4d340399d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -190,13 +190,10 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 34ed2afb2..7c0057696 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -69,7 +69,7 @@ let type_of_type u = mkType uu let type_of_sort = function - | Prop c -> type1 + | Prop | Set -> type1 | Type u -> type_of_type u (*s Type of a de Bruijn index. *) @@ -178,11 +178,11 @@ let type_of_apply env func funt argsv argstv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | ((Prop | Set), Set) -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | (Type u1, Set) -> if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -190,9 +190,9 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (Universe.sup u1 u2) @@ -481,10 +481,6 @@ let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 let judge_of_type u = make_judge (mkType u) (type_of_type u) -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 546f2d2b4..3b2abc777 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -43,7 +43,6 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : Sorts.contents -> unsafe_judgment val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4a9467de5..bc624ba56 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -747,6 +747,45 @@ let check_constraint g (l,d,r) = let check_constraints c g = Constraint.for_all (check_constraint g) c +let leq_expr (u,m) (v,n) = + let d = match m - n with + | 1 -> Lt + | diff -> assert (diff <= 0); Le + in + (u,d,v) + +let enforce_leq_alg u v g = + let enforce_one (u,v) = function + | Inr _ as orig -> orig + | Inl (cstrs,g) as orig -> + if check_smaller_expr g u v then orig + else + (let c = leq_expr u v in + match enforce_constraint c g with + | g -> Inl (Constraint.add c cstrs,g) + | exception (UniverseInconsistency _ as e) -> Inr e) + in + (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *) + let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in + let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in + (* We pick a best constraint: smallest number of constraints, not an error if possible. *) + let order x y = match x, y with + | Inr _, Inr _ -> 0 + | Inl _, Inr _ -> -1 + | Inr _, Inl _ -> 1 + | Inl (c,_), Inl (c',_) -> + Int.compare (Constraint.cardinal c) (Constraint.cardinal c') + in + match List.min order c with + | Inl x -> x + | Inr e -> raise e + +(* sanity check wrapper *) +let enforce_leq_alg u v g = + let _,g as cg = enforce_leq_alg u v g in + assert (check_leq g u v); + cg + (* Normalization *) (** [normalize_universes g] returns a graph where all edges point diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e6dd629e4..8c2d877b0 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool +(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *) +val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t + (** Adds a universe to the graph, ensuring it is >= or > Set. @raise AlreadyDeclared if the level is already declared in the graph. *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 9782312ca..311477dac 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -666,7 +666,7 @@ let constraint_add_leq v u c = else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -674,12 +674,7 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - let rec aux acc v = - match v with - | v :: l -> - aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l - | [] -> acc - in aux c v + List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v let enforce_leq u v c = if check_univ_leq u v then c diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml index 61eb1dafd..c2bcd73ff 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml @@ -90,30 +90,50 @@ let rec post_canonize f = exception Parsing_error of string -let rec parse_string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string s) - | [< >] -> "" -and parse_string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise (Parsing_error "unterminated string") -and parse_skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> parse_skip_comment s - | [< >] -> [< >] -and parse_args = parser - | [< '' ' | '\n' | '\t'; s >] -> parse_args s - | [< ''#'; s >] -> parse_args (parse_skip_comment s) - | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s - | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) - | [< >] -> [] +let buffer buf = + let ans = Buffer.contents buf in + let () = Buffer.clear buf in + ans + +let rec parse_string buf s = match Stream.next s with +| ' ' | '\n' | '\t' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string buf s +| exception Stream.Failure -> buffer buf + +and parse_string2 buf s = match Stream.next s with +| '"' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string2 buf s +| exception Stream.Failure -> raise (Parsing_error "unterminated string") + +and parse_skip_comment s = match Stream.next s with +| '\n' -> () +| _ -> parse_skip_comment s +| exception Stream.Failure -> () + +and parse_args buf accu s = match Stream.next s with +| ' ' | '\n' | '\t' -> parse_args buf accu s +| '#' -> + let () = parse_skip_comment s in + parse_args buf accu s +| '"' -> + let str = parse_string2 buf s in + parse_args buf (str :: accu) s +| c -> + let () = Buffer.add_char buf c in + let str = parse_string buf s in + parse_args buf (str :: accu) s +| exception Stream.Failure -> accu let parse f = let c = open_in f in - let res = parse_args (Stream.of_channel c) in + let buf = Buffer.create 64 in + let res = parse_args buf [] (Stream.of_channel c) in close_in c; - res + List.rev res ;; (* Copy from minisys.ml, since we don't see that file here *) @@ -143,7 +163,7 @@ let process_cmd_line orig_dir proj args = error "Use \"-install none\" instead of \"-no-install\"" | "-custom" :: _ -> error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\"" - + | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> @@ -189,7 +209,7 @@ let process_cmd_line orig_dir proj args = error "Output file must be in the current directory"; if proj.makefile <> None then error "Option -o given more than once"; - aux { proj with makefile = Some file } r + aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4c6156a38..4a691e442 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -130,8 +130,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index cc9c2046d..84baea964 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,11 +199,12 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 84b29a0bf..e4d17f250 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -148,8 +148,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let env = Global.env () in - let vars = Univops.universes_of_constr env c in + let vars = Univops.universes_of_constr c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bf9e37aa7..5c4cbefad 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) match (EConstr.kind !evdref x, EConstr.kind !evdref y) with | Sort s, Sort s' -> (match ESorts.kind !evdref s, ESorts.kind !evdref s' with - | Prop x, Prop y when x == y -> None - | Prop _, Type _ -> None + | Prop, Prop | Set, Set -> None + | (Prop | Set), Type _ -> None | Type x, Type y when Univ.Universe.equal x y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2bc603a90..d7118efd7 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels let open Glob_term in begin match ps, ESorts.kind sigma s with - | GProp, Prop Null -> subst - | GSet, Prop Pos -> subst + | GProp, Prop -> subst + | GSet, Set -> subst | GType _, Type _ -> subst | _ -> raise PatternMatchingFailure end diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 23a985dc3..d0de2f8c0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -597,8 +597,8 @@ let detype_universe sigma u = Univ.Universe.map fn u let detype_sort sigma = function - | Prop Null -> GProp - | Prop Pos -> GSet + | Prop -> GProp + | Set -> GSet | Type u -> GType (if !print_universes diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 8afb9b942..3f5d186d4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) - | Prop Pos when refreshset && not direction -> + | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d599afe69..efb205182 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -465,22 +465,21 @@ let build_branch_type env sigma dep p cs = let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in - let indu = match mib.mind_universes with - | Monomorphic_ind _ -> mkInd ind - | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx) - | Cumulative_ind ctx -> - mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Instance.empty + | Polymorphic_ind auctx -> make_abstract_instance auctx + | Cumulative_ind acumi -> + make_abstract_instance (ACumulativityInfo.univ_context acumi) in let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") | PrimRecord info-> Name (pi1 (info.(i))) in - (** FIXME: handle mutual records *) - let pkt = mib.mind_packets.(0) in - let { mind_consnrealargs; mind_consnrealdecls } = pkt in + let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in - let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in + let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in + let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so @@ -489,6 +488,7 @@ let compute_projections env (kn, i as ind) = let indty = (* [ty] = [Ind inst] is typed in context [params] *) let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in + let indu = mkIndU (ind, u) in let ty = mkApp (indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) ty @@ -498,8 +498,8 @@ let compute_projections env (kn, i as ind) = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in { ci_ind = ind; ci_npar = nparamargs; - ci_cstr_ndecls = mind_consnrealdecls; - ci_cstr_nargs = mind_consnrealargs; + ci_cstr_ndecls = pkt.mind_consnrealdecls; + ci_cstr_nargs = pkt.mind_consnrealargs; ci_pp_info = print_info } in let len = List.length ctx in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 622a8e982..685aa400b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -150,8 +150,8 @@ let pattern_of_constr env sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop Null) -> PSort GProp - | Sort (Prop Pos) -> PSort GSet + | Sort Prop -> PSort GProp + | Sort Set -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 746a68b21..7e43c5e41 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> Sorts.type1 + | Prop | Set -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with - | _, (Prop Null as s) -> s - | Prop _, (Prop Pos as s) -> s - | Type _, (Prop Pos as s) when is_impredicative_set env -> s - | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ) - | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) - | Prop Null, (Type _ as s) -> s - | Type u1, Type u2 -> Type (Univ.sup u1 u2)) + let dom = sort_of env t in + let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in + Typeops.sort_of_product env dom rang | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cf34ac016..a66ecaaac 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -241,10 +241,6 @@ let judge_of_set = { uj_val = EConstr.mkSet; uj_type = EConstr.mkSort Sorts.type1 } -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_type u = let uu = Univ.Universe.super u in { uj_val = EConstr.mkType u; @@ -333,10 +329,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with - | Prop c -> - sigma, judge_of_prop_contents c - | Type u -> - sigma, judge_of_type u + | Prop -> sigma, judge_of_prop + | Set -> sigma, judge_of_set + | Type u -> sigma, judge_of_type u end | Proj (p, c) -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3120c97b5..47c9c51ee 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let env = Global.env () in - let used_univs_body = Univops.universes_of_constr env body in - let used_univs_typ = Univops.universes_of_constr env typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 773fc1520..9c5fdcd1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -477,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index 91c577405..0e3921570 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -942,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the diff --git a/tactics/hints.ml b/tactics/hints.ml index 85ff02824..d28d4848c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -828,38 +828,48 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in - match EConstr.kind sigma cty with - | Prod _ -> - let sigma' = Evd.merge_context_set univ_flexible sigma ctx in - let ce = mk_clenv_from_env env sigma' None (c,cty) in - let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in - let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry" in - let nmiss = List.length (clenv_missing ce) in - let secvars = secvars_of_constr env sigma c in - let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in - let pat = match info.hint_pattern with - | Some p -> snd p | None -> pat - in - if Int.equal nmiss 0 then - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; - secvars; - code = with_uid (Res_pf(c,cty,ctx)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then - Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++ - str " will only be used by eauto"); - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) - end - | _ -> failwith "make_apply_entry" + match EConstr.kind sigma cty with + | Prod _ -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let c' = clenv_type (* ~reduce:false *) ce in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry" in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let secvars = secvars_of_constr env sigma c in + let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in + let pat = match info.hint_pattern with + | Some p -> snd p | None -> pat + in + if Int.equal nmiss 0 then + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; + secvars; + code = with_uid (Res_pf(c,cty,ctx)); }) + else begin + if not eapply then failwith "make_apply_entry"; + if verbose then begin + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + end; + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (ERes_pf(c,cty,ctx)); }) + end + | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose c is a constr diff --git a/tactics/inv.ml b/tactics/inv.ml index 755494c2d..e467eacd9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c430edf2e..928530744 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -212,6 +212,9 @@ let clear_dependency_msg env sigma id err inglobal = str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_clear_dependency env sigma id err inglobal = user_err (clear_dependency_msg env sigma id err inglobal) @@ -228,6 +231,9 @@ let replacing_dependency_msg env sigma id err inglobal = str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_replacing_dependency env sigma id err inglobal = user_err (replacing_dependency_msg env sigma id err inglobal) diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v new file mode 100644 index 000000000..5326c0fbb --- /dev/null +++ b/test-suite/bugs/closed/5012.v @@ -0,0 +1,17 @@ +Class Foo := { foo : Set }. + +Axiom admit : forall {T}, T. + +Global Instance Foo0 : Foo + := {| foo := admit |}. + +Global Instance Foo1 : Foo + := { foo := admit }. + +Existing Class Foo. + +Global Instance Foo2 : Foo + := { foo := admit }. (* Error: Unbound method name foo of class Foo. *) + +Set Warnings "+already-existing-class". +Fail Existing Class Foo. diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v new file mode 100644 index 000000000..a20ad1b4d --- /dev/null +++ b/test-suite/bugs/closed/5696.v @@ -0,0 +1,5 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e) +..)) (at level 200, x binder, y binder, e at level 220). +Check (var2 a = 1; a). diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v new file mode 100644 index 000000000..42bdb076b --- /dev/null +++ b/test-suite/bugs/closed/7695.v @@ -0,0 +1,20 @@ +Require Import Hurkens. + +Universes i j k. +Module Type T. + Parameter T1 : Type@{i+1}. + Parameter e : Type@{j} = T1 : Type@{k}. +End T. + +Module M. + Definition T1 := Type@{j}. + Definition e : Type@{j} = T1 : Type@{k} := eq_refl. +End M. + +Module F (A:T). + Definition bad := TypeNeqSmallType.paradox _ A.e. +End F. + +Set Printing Universes. +Fail Module X := F M. +(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *) diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 000000000..216290123 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v new file mode 100644 index 000000000..55c7ee99a --- /dev/null +++ b/test-suite/bugs/closed/7903.v @@ -0,0 +1,4 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). +Check bar x (x + x). diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v new file mode 100644 index 000000000..77529733b --- /dev/null +++ b/test-suite/success/mutual_record.v @@ -0,0 +1,57 @@ +Module M0. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M0. + +Module M1. + +Set Primitive Projections. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M1. + +Module M2. + +Set Primitive Projections. + +CoInductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M2. diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v new file mode 100644 index 000000000..8a1544c8e --- /dev/null +++ b/test-suite/success/vm_records.v @@ -0,0 +1,40 @@ +Set Primitive Projections. + +Module M. + +CoInductive foo := Foo { + foo0 : foo; + foo1 : bar; +} +with bar := Bar { + bar0 : foo; + bar1 : bar; +}. + +CoFixpoint f : foo := Foo f g +with g : bar := Bar f g. + +Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)). +Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g). + +End M. + +Module N. + +Inductive foo := Foo { + foo0 : option foo; + foo1 : list bar; +} +with bar := Bar { + bar0 : option bar; + bar1 : list foo; +}. + +Definition f_0 := Foo None nil. +Definition g_0 := Bar None nil. + +Definition f := Foo (Some f_0) (cons g_0 nil). + +Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil). + +End N. diff --git a/vernac/classes.ml b/vernac/classes.ml index 382d18b09..26d105ecf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let env = Global.env () in - let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) - (Univops.universes_of_constr env term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a8ac52846..750ed35cb 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -163,7 +163,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in uvars, (coe,t,imps)) Univ.LSet.empty l in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index f55c852c0..a8d794642 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt = let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = - Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) + Univ.LSet.union uvars (universes_of_constr evd (of_constr c)) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1d1cc62de..37258c2d4 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let env = Global.env () in - let vars = Univops.universes_of_constr env (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 6057c05f5..0387b32ba 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly = else sigma let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) + u = Prop || (is_impredicative_set env && u = Set) let interp_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in @@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds = let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> - if a = Prop Null then None + if a = Prop then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = @@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds = (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du + Evd.set_leq_sort env evd Set du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du + Evd.set_eq_sort env evd Prop du else evd else Evd.set_eq_sort env evd (Type cu) du in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5d671ef52..534e58f9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -871,9 +871,6 @@ let explain_not_match_error = function pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" | CumulativeStatusExpected b -> let status b = if b then str"cumulative" else str"non-cumulative" in str "a " ++ status b ++ str" declaration was expected, but a " ++ diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1ab24b670..fa6a9adf1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -480,10 +480,9 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let env = Global.env () in let uvars = Univ.LSet.union - (Univops.universes_of_constr env typ) - (Univops.universes_of_constr env body) in + (Univops.universes_of_constr typ) + (Univops.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -865,7 +864,7 @@ let obligation_terminator name num guard hook auto pf = else UState.union prg.prg_ctx ctx in let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in let prg_ctx = @@ -874,10 +873,12 @@ let obligation_terminator name num guard hook auto pf = polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx else - (** The first obligation declares the univs of the constant, + (** The first obligation, if defined, + declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - UState.make (Global.universes ()) + if defined then UState.make (Global.universes ()) + else ctx in let prg = { prg with prg_ctx } in try diff --git a/vernac/record.ml b/vernac/record.ml index a97a1662e..7a8ce7d25 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -100,7 +100,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id poly pl t ps nots fs = +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 _ = @@ -117,7 +117,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in - let sigma, typ, sort, template = match t with + let fold (sigma, template) (_, t, _, _) = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = @@ -132,28 +132,36 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match Evd.is_sort_variable sigma s' with | Some l -> let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in - sigma, s, s', true + (sigma, template), (s, s') | None -> - sigma, s, s', false - else sigma, s, s', false) + (sigma, false), (s, s') + else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in let sigma, s = Evd.new_sort_variable uvarkind sigma in - sigma, EConstr.mkSort s, s, true + (sigma, template), (EConstr.mkSort s, s) in - let arity = EConstr.it_mkProd_or_LetIn typ newps in - let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in + let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in + let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in + let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in + let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in let assums = List.filter is_local_assum newps in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params,(finite != Declarations.BiFinite)) in - let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in - let env2,sigma,impls,newfs,data = - interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) + let impls_env = + let params = List.map (RelDecl.get_name %> Name.get_id) assums in + let ty = Inductive (params, (finite != Declarations.BiFinite)) in + let ids = List.map (fun (id, _, _, _) -> id) records in + let imps = List.map (fun _ -> imps) arities in + compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps in + let fold sigma (_, _, nots, fs) arity = + let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in + (sigma, (impls, newfs)) + in + let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in - let sigma, typ = + let fold sigma (typ, sort) (_, newfs) = let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || (Sorts.is_set sort && is_impredicative_set env0)) then @@ -164,20 +172,24 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in + let (sigma, typs) = List.fold_left2_map fold sigma typs data in let sigma = Evd.minimize_universes sigma in - let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in - let typ = EConstr.to_constr sigma typ in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - List.iter (iter_constr ce) (List.rev newps); + let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let () = List.iter (iter_constr ce) (List.rev newps) in + let map (impls, newfs) typ = + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let typ = EConstr.to_constr sigma typ in List.iter (iter_constr ce) (List.rev newfs); - ubinders, univs, typ, template, imps, newps, impls, newfs + (typ, impls, newfs) + in + let ans = List.map2 map data typs in + ubinders, univs, template, newps, imps, ans let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -261,9 +273,10 @@ let subst_projection fid l c = raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' -let instantiate_possibly_recursive_type indu paramdecls fields = +let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in - Termops.substl_rel_context (subst@[mkIndU indu]) fields + let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in + Termops.substl_rel_context (subst @ subst') fields let warn_non_primitive_record = CWarnings.create ~name:"non-primitive-record" ~category:"record" @@ -281,12 +294,11 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u | Monomorphic_const_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in - let fields = instantiate_possibly_recursive_type indu paramdecls fields in + let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = if !primitive_flag then @@ -374,12 +386,9 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u open Typeclasses -let declare_structure finite ubinders univs id idbuild paramimpls params arity template - fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = - let nparams = List.length params and nfields = List.length fields in - let args = Context.Rel.to_extended_list mkRel nfields params in - let ind = applist (mkRel (1+nparams+nfields), args) in - let type_constructor = it_mkProd_or_LetIn ind fields in + +let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = + let nparams = List.length params in let template, ctx = match univs with | Monomorphic_ind_entry ctx -> @@ -389,37 +398,51 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t | Cumulative_ind_entry cumi -> false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in - let binder_name = + let binder_name = match name with - | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + | None -> + let map (id, _, _, _, _, _, _) = + Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + in + Array.map_of_list map record_data | Some n -> n in - let mie_ind = + let ntypes = List.length record_data in + let mk_block i (id, idbuild, arity, _, fields, _, _) = + let nfields = List.length fields in + let args = Context.Rel.to_extended_list mkRel nfields params in + let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in + let type_constructor = it_mkProd_or_LetIn ind fields in { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in + let blocks = List.mapi mk_block record_data in let mie = { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = Some (if !primitive_flag then Some [|binder_name|] else None); + mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; - mind_entry_inds = [mie_ind]; + mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; } in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in - let rsp = (kn,0) in (* This is ind path of idstruc *) - let cstr = (rsp,1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in - let build = ConstructRef cstr in - let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in - let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - rsp + let impls = List.map (fun _ -> paramimpls, []) record_data in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in + let map i (_, _, _, fieldimpls, fields, is_coe, coers) = + let rsp = (kn, i) in (* This is ind path of idstruc *) + let cstr = (rsp, 1) in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in + let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in + let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in + let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in + rsp + in + List.mapi map record_data let implicits_of_context ctx = List.map_i (fun i name -> @@ -431,22 +454,22 @@ let implicits_of_context ctx = 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities = + template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let len = List.length params in let impls = implicits_of_context params in List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls in - let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in - let impl, projs = + let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in + let data = match fields with | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in - let cst = Declare.declare_constant (snd id) + let cst = Declare.declare_constant id (DefinitionEntry class_entry, IsDefinition Definition) in let cstu = (cst, match univs with @@ -473,7 +496,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in - cref, [Name proj_name, sub, Some proj_cst] + [cref, [Name proj_name, sub, Some proj_cst]] | _ -> let univs = match univs with @@ -485,18 +508,21 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls - params arity template fieldimpls fields - ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) - in + let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in + let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls + params template ~kind:Method ~name:[|binder_name|] record_data + in let coers = List.map2 (fun coe pri -> Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) - (List.rev fields) coers (Recordops.lookup_projections ind) - in IndRef ind, l + let map ind = + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l + in + List.map map inds in let ctx_context = List.map (fun decl -> @@ -517,16 +543,19 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry _ -> Univ.AUContext.empty, ctx_context, fields in - let k = - { cl_univs = univs; - cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; - cl_context = ctx_context; - cl_props = fields; - cl_projs = projs } - in + let map (impl, projs) = + let k = + { cl_univs = univs; + cl_impl = impl; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in add_class k; impl + in + List.map map data let add_constant_class cst = @@ -562,48 +591,87 @@ let add_inductive_class ind = cl_unique = !typeclasses_unique } in add_class k +let warn_already_existing_class = + CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g -> + Printer.pr_global g ++ str " is already declared as a typeclass.") + let declare_existing_class g = - match g with - | ConstRef x -> add_constant_class x - | IndRef x -> add_inductive_class x - | _ -> user_err ~hdr:"declare_existing_class" - (Pp.str"Unsupported class type, only constants and inductives are allowed") + if Typeclasses.is_class g then warn_already_existing_class g + else + match g with + | ConstRef x -> add_constant_class x + | IndRef x -> add_inductive_class x + | _ -> user_err ~hdr:"declare_existing_class" + (Pp.str"Unsupported class type, only constants and inductives are allowed") open Vernacexpr -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a - list telling if the corresponding fields must me declared as coercions - or subinstances. *) -let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) = - let cfs,notations = List.split cfs in - let cfs,priorities = List.split cfs in - let coers,fs = List.split cfs in - let extract_name acc = function +let check_unique_names records = + let extract_name acc (((_, bnd), _), _) = match bnd with Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in - let allnames = idstruc::(List.fold_left extract_name [] fs) in - let () = match List.duplicates Id.equal allnames with + let allnames = + List.fold_left (fun acc (_, id, _, _, cfs, _, _) -> + id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records + in + match List.duplicates Id.equal allnames with | [] -> () | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id)) - in + +let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - user_err Pp.(str "Priorities only allowed for type class substructures"); - (* Now, younger decl in params and fields is on top *) - let pl, univs, arity, template, implpars, params, implfs, fields = + let has_priority (_, _, _, _, cfs, _, _) = + List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs + in + if isnot_class && List.exists has_priority records then + user_err Pp.(str "Priorities only allowed for type class substructures") + +let extract_record_data records = + let map (is_coe, id, _, _, cfs, idbuild, s) = + let fs = List.map (fun (((_, f), _), _) -> f) cfs in + id.CAst.v, s, List.map snd cfs, fs + in + let data = List.map map records in + let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in + let ps = match pss with + | [] -> CErrors.anomaly (str "Empty record block") + | ps :: rem -> + let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in + let () = + if not (List.for_all (eq_local_binders ps) rem) then + user_err (str "Parameters should be syntactically the \ + same for each inductive type.") + in + ps + in + (** FIXME: Same issue as #7754 *) + let _, _, pl, _, _, _, _ = List.hd records in + pl, ps, data + +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances. *) +let definition_structure kind cum poly finite records = + let () = check_unique_names records in + let () = check_priorities kind records in + let pl, ps, data = extract_record_data records in + let pl, univs, template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities + let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + | [r], [d] -> r, d + | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") + 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 pl univs id.CAst.v idbuild + implpars params arity template implfs fields coers priorities | _ -> - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits - (succ (List.length params)) impls) implfs - in + let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in + let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let univs = match univs with | Polymorphic_const_entry univs -> @@ -614,7 +682,11 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure finite pl univs idstruc - idbuild implpars params arity template implfs - fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind + let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) = + let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in + id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe + in + let data = List.map2 map data records in + let inds = declare_structure finite pl univs implpars params template data in + List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index b2c039f0b..7cf7da1e2 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,9 +26,14 @@ val declare_projections : (Name.t * bool) list * Constant.t option list val definition_structure : - inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> + Declarations.recursivity_kind -> + (coercion_flag * + Names.lident * + universe_decl_expr option * + local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> GlobRef.t + Id.t * constr_expr option) list -> + GlobRef.t list val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 479482095..43c974846 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -539,25 +539,36 @@ 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 vernac_record cum k poly finite struc binders sort nameopt cfs = +let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let const = match nameopt with - | None -> add_prefix "Build_" (fst (snd struc)).v - | Some ({v=id} as lid) -> - Dumpglob.dump_definition lid false "constr"; id in - if Dumpglob.dump () then ( - Dumpglob.dump_definition (fst (snd struc)) false "rec"; - List.iter (fun (((_, x), _), _) -> - match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) + let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let const = match nameopt with + | None -> add_prefix "Build_" id.v + | Some lid -> + let () = Dumpglob.dump_definition lid false "constr" in + lid.v + in + let () = + if Dumpglob.dump () then + let () = Dumpglob.dump_definition id false "rec" in + let iter (((_, x), _), _) = match x with + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + Dumpglob.dump_definition (make ?loc id) false "proj" + | _ -> () + in + List.iter iter cfs + in + coe, id, pl, binders, cfs, const, sort + in + let records = List.map map records in + ignore(Record.definition_structure k is_cumulative poly finite records) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = + let open Pp in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -567,35 +578,85 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function + | ((_ , _ , _ , _, RecordDecl _), _) -> true + | _ -> false + in + let is_constructor = function + | ((_ , _ , _ , _, Constructors _), _) -> true + | _ -> false + in + let is_defclass = match indl with + | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + | _ -> None + in + if Option.has_some is_defclass then + (** Definitional class case *) + let (id, bl, c, l) = Option.get is_defclass in + let (coe, (lid, ce)) = l in + let coe' = if coe then Some true else None in + let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in + vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + else if List.for_all is_record indl then + (** Mutual record case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_where ((_, _, _, _, _), wh) = match wh with + | [] -> () + | _ :: _ -> + user_err (str "where clause not supported for records") + in + let () = List.iter check_where indl in + let unpack ((id, bl, c, _, decl), _) = match decl with + | RecordDecl (oc, fs) -> + (id, bl, c, oc, fs) + | Constructors _ -> assert false (** ruled out above *) + in + let ((_, _, _, kind, _), _) = List.hd indl in + let kind = match kind with Class _ -> Class false | _ -> kind in + let recordl = List.map unpack indl in + vernac_record cum kind atts.polymorphic finite recordl + else if List.for_all is_constructor indl then + (** Mutual inductive case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | (Record | Structure) -> + user_err (str "The Record keyword is for types defined using the syntax { ... }.") + | Class _ -> + user_err (str "Inductive classes not supported") + | Variant | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_name ((na, _, _, _, _), _) = match na with + | (true, _) -> + user_err (str "Variant types do not handle the \"> Name\" \ + syntax, which is reserved for records. Use the \":>\" \ + syntax on constructors instead.") + | _ -> () + in + let () = List.iter check_name indl in + let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + | Constructors l -> (id, bl, c, l), ntn + | RecordDecl _ -> assert false (* ruled out above *) + in + let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + else + user_err (str "Mixed record-inductive definitions are not allowed") +(* + match indl with - | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") - | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - user_err Pp.(str "The Variant keyword does not support syntax { ... }.") - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record cum (match b with Class _ -> Class false | _ -> b) - atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] - | [ ( _ , _, _, Class _, Constructors _), [] ] -> - user_err Pp.(str "Inductive classes not supported") - | [ ( id , bl , c , Class _, _), _ :: _ ] -> - user_err Pp.(str "where clause not supported for classes") - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - user_err Pp.(str "where clause not supported for (co)inductive records") - | _ -> let unpack = function - | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn - | ( (true,_),_,_,_,Constructors _),_ -> - user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") - | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") - in - let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + *) let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in |