diff options
102 files changed, 1266 insertions, 1022 deletions
@@ -61,6 +61,26 @@ Coq binaries and process model `coq{proof,tactic,query}worker` are in charge of task-specific and parallel proof checking. +SSReflect + +- The implementation of delayed clear switches in intro patterns + is now simpler to explain: + 1. The immediate effect of a clear switch like {x} is to rename the + variable x to _x_ (i.e. a reserved identifier that cannot be mentioned + explicitly) + 2. The delayed effect of {x} is that _x_ is cleared at the end of the intro + pattern + 3. A clear switch immediately before a view application like {x}/v is + translated to /v{x}. + In particular rule 3 lets one write {x}/v even if v uses the variable x: + indeed the view is executed before the renaming. + +- An empty clear switch is now accepted in intro patterns before a + view application whenever the view is a variable. + One can now write {}/v to mean {v}/v. Remark that {}/x is very similar + to the idiom {}e for the rewrite tactic (the equation e is used for + rewriting and then discarded). + Changes from 8.8.0 to 8.8.1 =========================== @@ -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. - @@ -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 3304b032e..a890f2cef 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -207,7 +207,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) @@ -252,9 +252,10 @@ type recarg = type wf_paths = recarg Rtree.t -type record_body = (Id.t * Constant.t array * projection_body array) option - (* The body is empty for non-primitive records, otherwise we get its - binder name in projections and list of projections if it is primitive. *) +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : constr; @@ -322,7 +323,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** Whether the inductive type has been declared as a record. *) + mind_record : record_info; (** Whether the inductive type has been declared as a record. *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) diff --git a/checker/closure.ml b/checker/closure.ml index b9ae4daa8..2dcc1a984 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -619,7 +619,8 @@ let drop_parameters depth n argstk = let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.mind_record with - | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite -> + | PrimRecord info when mib.mind_finite <> CoFinite -> + let (_, projs, pbs) = info.(snd ind) in (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.mind_nparams in diff --git a/checker/environ.ml b/checker/environ.ml index 3d5fac806..ba1eb0ddb 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -192,11 +192,12 @@ let add_mind kn mib env = (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let new_projections = match mib.mind_record with - | None | Some None -> env.env_globals.env_projections - | Some (Some (id, kns, pbs)) -> - Array.fold_left2 (fun projs kn pb -> - Cmap_env.add kn pb projs) - env.env_globals.env_projections kns pbs + | NotRecord | FakeRecord -> env.env_globals.env_projections + | PrimRecord projs -> + Array.fold_left (fun accu (id, kns, pbs) -> + Array.fold_left2 (fun accu kn pb -> + Cmap_env.add kn pb accu) accu kns pbs) + env.env_globals.env_projections projs in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then 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/subtyping.ml b/checker/subtyping.ml index f4ae02084..6d0d6f6c6 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -9,7 +9,6 @@ (************************************************************************) (*i*) -open CErrors open Util open Names open Cic @@ -126,46 +125,13 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in - check MutInd.equal (fun x -> x.proj_ind); + check eq_ind (fun x -> x.proj_ind); check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); 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 @@ -218,16 +184,19 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (* we check that records and their field names are preserved. *) let record_equal x y = match x, y with - | None, None -> true - | Some None, Some None -> true - | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) -> - Id.equal id1 id2 && - Array.for_all2 Constant.UserOrd.equal p1 p2 && - Array.for_all2 eq_projection_body pb1 pb2 + | NotRecord, NotRecord -> true + | FakeRecord, FakeRecord -> true + | PrimRecord info1, PrimRecord info2 -> + let check (id1, p1, pb1) (id2, p2, pb2) = + Id.equal id1 id2 && + Array.for_all2 Constant.UserOrd.equal p1 p2 && + Array.for_all2 eq_projection_body pb1 pb2 + in + Array.equal check info1 info2 | _, _ -> false in check record_equal (fun mib -> mib.mind_record); - if mib1.mind_record != None then begin + if mib1.mind_record != NotRecord then begin let rec names_prod_letin t = match t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) @@ -251,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/typeops.ml b/checker/typeops.ml index 18f07dc0b..345ee5b8f 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -203,7 +203,7 @@ let judge_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (c, ct) in - assert(MutInd.equal pb.proj_ind (fst ind)); + assert(eq_ind pb.proj_ind ind); let ty = subst_instance_constr u pb.proj_type in substl (c :: List.rev args) ty 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 31e65729b..4f28d6e44 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 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli +MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli *) @@ -225,7 +225,7 @@ let v_cst_def = let v_projbody = v_tuple "projection_body" - [|v_cst;Int;Int;v_constr|] + [|v_ind;Int;Int;v_constr|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] @@ -274,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body" Any|] let v_finite = v_enum "recursivity_kind" 3 -let v_mind_record = Annot ("mind_record", - Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]))) + +let v_record_info = + v_sum "record_info" 2 + [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |] let v_ind_pack_univs = v_sum "abstract_inductive_universes" 0 @@ -283,7 +285,7 @@ let v_ind_pack_univs = let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; - v_mind_record; + v_record_info; v_finite; Int; v_section_ctxt; 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/README.md b/dev/ci/README.md index 08364c897..45176581c 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -86,11 +86,6 @@ We are currently running tests on the following platforms: - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. -GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit -message to bypass CI. Do not use this unless your commit only changes files -that are not compiled (e.g. Markdown files like this one, or files under -[`.github/`](../../.github/)). - You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87d837b38..2ebbf2cc4 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-trunk}" -: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" +: "${coq_dpdgraph_CI_BRANCH:=coq-master}" +: "${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,46 @@ # 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}" ######################################################################## # 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/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/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/doc/critical-bugs b/dev/doc/critical-bugs new file mode 100644 index 000000000..293b01f63 --- /dev/null +++ b/dev/doc/critical-bugs @@ -0,0 +1,226 @@ +Preliminary compilation of critical bugs in stable releases of Coq +================================================================== + WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS + + +To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions) + +Typing constructions + + component: "match" + summary: substitution missing in the body of a let + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin) + found by: Herbelin + exploit: test-suite/success/Case22.v + GH issue number: ? + risk: ? + + component: fixpoint, guard + summary: missing lift in checking guard + introduced: probably from V5.10 + impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4 + impacted development branches: v8.0 ? + impacted coqchk versions: ? + fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras) + found by: Barras + exploit: test-suite/failure/guard.v + GH issue number: none + risk: unprobable by chance + + component: cofixpoint, guard + summary: de Bruijn indice bug in checking guard of nested cofixpoints + introduced: after V6.3.1, before V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport) + found by: Dénès + exploit: ? + GH issue number: none ? + risk: ? + + component: inductive types, elimination principle + summary: de Bruijn indice bug in computing allowed elimination principle + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism) + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès) + found by: Dénès + exploit: see GH#3211 + GH issue number: #3211 + risk: ? + + component: universe subtyping + summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop + introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin) + impacted released versions: V8.2-V8.2pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport) + found by: Georgi Guninski + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Module system + + component: modules, universes + summary: missing universe constraints in typing "with" clause of a module type + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau) + found by: Dénès + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Universes + + component: template polymorphism + summary: issue with two parameters in the same universe level + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), + found by: Barras + exploit: test-suite/failure/inductive4.v + GH issue number: none + risk: unlikely to be activated by chance + +Primitive projections + + component: primitive projections, guard condition + summary: check of guardedness of extra arguments of primitive projections missing + introduced: 6 May 2014, a4043608f, Sozeau + impacted released versions: V8.5-V8.5pl2, + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau) + found by: Sozeau, by analyzing bug report #4876 + exploit: to be done (?) + GH issue number: #4876 + risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?) + + component: primitive projections, guard condition + summary: records based on primitive projections became possibly recursive without the guard condition being updated + introduced: 10 Sep 2014, 6624459e4, Sozeau (?) + impacted released versions: V8.5 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès) + found by: Dénès exploiting bug #4588 + exploit: test-suite/bugs/closed/4588.v + GH issue number: #4588 + risk: ? + +Conversion machines + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: collision between constructors when more than 256 constructors in a type + introduced: V8.1 + impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5 + impacted development branches: none + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport) + found by: Dénès, Pédrot + exploit: test-suite/failure/vm-bug4157.v + GH issue number: #4157 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: wrong universe constraints + introduced: possibly exploitable from V8.1; exploitable at least from V8.5 + impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1 + impacted development branches: unknown for v8.1-v8.4, none from v8.5 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport) + found by: Dénès + exploit: test-suite/bugs/closed/6677.v + GH issue number: #6677 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: missing pops in executing 31bit arithmetic + introduced: V8.5 + impacted released versions: V8.1-V8.4pl5 + impacted development branches: v8.1 (probably) + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès), + found by: Catalin Hritcu + exploit: lost? + GH issue number: ? + risk: + + component: "native" conversion machine (translation to OCaml which compiles to native code) + summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False + introduced: V8.5 + impacted released versions: V8.5-V8.5pl1 + impacted development branches: none + impacted coqchk versions: none (no native computation in coqchk) + fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), + found by: Letouzey, Dénès + exploit: lost? + GH issue number: ? + risk: + +Conflicts with axioms in library + + component: library of real numbers + summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set + introduced: 67c75fa01, 20 Jun 2002 + impacted released versions: 7.3.1, 7.4 + impacted coqchk versions: + fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004 + found by: Herbelin & Werner + exploit: need to find the example again + GH issue number: no + risk: unlikely to be exploited by chance + + component: library of extensional sets, guard condition + summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets + introduced: not a bug per se but an incompatibility discovered late + impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it + impacted coqchk versions: ? + fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès) + found by: Schepler, Dénès, Azevedo de Amorim + exploit: ? + GH issue number: none + risk: unlikely to be exploited by chance (?) + + component: library for axiom of choice and excluded-middle + summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set + introduced: not a bug but a change of intended "model" + impacted released versions: strictly before 8.1 + impacted coqchk versions: ? + fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin + found by: Benjamin Werner + exploit: + GH issue number: none + risk: + +There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1). + +There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical. + +Another non exploitable bug? + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: bug in 31bit arithmetic + introduced: V8.1 + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès) + found by: Dénès, from a bug report by Tahina Ramananandro + exploit: ? + GH issue number: ? + risk: + diff --git a/doc/LICENSE b/doc/LICENSE index c223a4e16..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 @@ -14,33 +14,14 @@ License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. -The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine -Paulin-Mohring. All documents (the LaTeX source and the PostScript, -PDF and html outputs) are copyright (c) INRIA 1999-2006. The material -connected to the Coq Tutorial 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. - 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. -The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre -Castéran and Eduardo Gimenez. All related documents (the LaTeX and -BibTeX sources and the PostScript, PDF and html outputs) are copyright -(c) INRIA 1997-2006. The material connected to the Tutorial on -[Co-]Inductive Types in Coq 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. - ---------------------------------------------------------------------- *Open Publication License* 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 20e4069f4..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,42 +77,35 @@ 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 ================================ This manual does not contain all the documentation the user may need about |Coq|. Various informations can be found in the following documents: -Tutorial - A companion volume to this reference manual, the |Coq| Tutorial, is - aimed at gently introducing new users to developing proofs in |Coq| - without assuming prior knowledge of type theory. In a second step, - the user can read also the tutorial on recursive types (document - `RecTutorial.ps`). - Installation A text file `INSTALL` that comes with the sources explains how to install |Coq|. 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/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ab52c2ce7..6fb73a030 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -623,7 +623,9 @@ where: + In the occurrence switch :token:`occ_switch`, if the first element of the list is a natural, this element should be a number, and not an Ltac variable. The empty list ``{}`` is not interpreted as a valid occurrence - switch. + switch, it is rather used as a flag to signal the intent of the user to + clear the name following it (see :ref:`ssr_rewrite_occ_switch` and + :ref:`introduction_ssr`) The tactic: @@ -1539,7 +1541,7 @@ whose general syntax is :name: => .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term .. prodn:: s_item ::= /= %| // %| //= @@ -1641,6 +1643,11 @@ The view is applied to the top assumption. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. +``/`` :token:`term` + Interprets the top of the stack with the view :token:`term`. + It is equivalent to ``move/term``. The optional flag ``{}`` can + be used to signal that the :token:`term`, when it is a context entry, + has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -3236,6 +3243,7 @@ the equality. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. +.. _ssr_rewrite_occ_switch: Occurrence switches and redex switches `````````````````````````````````````` @@ -3260,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. +An empty occurrence switch ``{}`` is not interpreted as a valid occurrence +switch. It has the effect of clearing the :token:`r_item` (when it is the name +of a context entry). Occurrence selection and repetition ``````````````````````````````````` @@ -5279,7 +5290,7 @@ generalization item see :ref:`structure_ssr` intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term intro item see :ref:`introduction_ssr` diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 82be4791f..1625f6fc8 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -514,6 +514,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami evdref := evd'; ev +(* Safe interface to unification problems *) +type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr + +let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') = + pbty == pbty' && env == env' && + EConstr.eq_constr evd t1 t1' && + EConstr.eq_constr evd t2 t2' + +let add_unification_pb ?(tail=false) pb evd = + let conv_pbs = Evd.conv_pbs evd in + if not (List.exists (eq_unification_pb evd pb) conv_pbs) then + let (pbty,env,t1,t2) = pb in + Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd + else evd + (* This assumes an evar with identity instance and generalizes it over only the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c17f3d168..db638be9e 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -217,6 +217,14 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array -> val compare_constructor_instances : evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map +(** {6 Unification problems} *) +type unification_pb = conv_pb * env * constr * constr + +(** [add_unification_pb ?tail pb sigma] + Add a unification problem [pb] to [sigma], if not already present. + Put it at the end of the list if [tail] is true, by default it is false. *) +val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map + (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) diff --git a/engine/evd.ml b/engine/evd.ml index f56f9662d..714a0b645 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -621,10 +621,11 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = - (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} +let conv_pbs d = d.conv_pbs + let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names diff --git a/engine/evd.mli b/engine/evd.mli index 405fcc403..d166fd804 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -439,7 +439,11 @@ type clbinding = (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * econstr * econstr + +(** The following two functions are for internal use only, + see [Evarutil.add_unification_pb] for a safe interface. *) val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map +val conv_pbs : evar_map -> evar_constraint list val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> diff --git a/interp/declare.ml b/interp/declare.ml index aa737239b..e79cc6079 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,11 +383,14 @@ 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,0) in + let spec,_ = Inductive.lookup_mind_specif env mind in match spec.mind_record with - | Some (Some (_, kns, _)) -> - let projs = Inductiveops.compute_projections env (mind, 0) in + | PrimRecord info -> + let _, kns, _ = info.(0) in + let projs = Inductiveops.compute_projections env mind in Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in let univs = match univs with @@ -410,8 +413,8 @@ let declare_projections univs mind = assert (Constant.equal kn kn') ) kns projs; true, true - | Some None -> true,false - | None -> false,false + | FakeRecord -> true,false + | NotRecord -> false,false (* for initial declaration *) let declare_mind mie = diff --git a/interp/discharge.ml b/interp/discharge.ml index e16a955d9..0e44a8b46 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -111,9 +111,10 @@ let process_inductive info modlist mib = let section_decls' = Context.Named.map discharge section_decls in let (params',inds') = abstract_inductive section_decls' nparamdecls inds in let record = match mib.mind_record with - | Some (Some (id, _, _)) -> Some (Some id) - | Some None -> Some None - | None -> None + | PrimRecord info -> + Some (Some (Array.map pi1 info)) + | FakeRecord -> Some None + | NotRecord -> None in { mind_entry_record = record; mind_entry_finite = mib.mind_finite; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 74618a290..5bf46282f 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -113,7 +113,7 @@ let type_of_global_ref gr = "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record <> None then + if mib.Declarations.mind_record <> Declarations.NotRecord then begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1d8861cbc..1d5142a5c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -587,78 +587,95 @@ let mk_clos_deep clos_fun env t = let mk_clos2 = mk_clos_deep mk_clos (* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = +let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x | FAtom c -> exliftn lfts c | FCast (a,k,b) -> - mkCast (constr_fun lfts a, k, constr_fun lfts b) + mkCast (to_constr lfts a, k, to_constr lfts b) | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op | FCaseT (ci,p,c,ve,env) -> - mkCase (ci, constr_fun lfts (mk_clos env p), - constr_fun lfts c, - Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) - | FFix ((op,(lna,tys,bds)),e) -> + if is_subs_id env && is_lift_id lfts then + mkCase (ci, p, to_constr lfts c, ve) + else + let subs = comp_subs lfts env in + mkCase (ci, subst_constr subs p, + to_constr lfts c, + Array.map (fun b -> subst_constr subs b) ve) + | FFix ((op,(lna,tys,bds)) as fx, e) -> + if is_subs_id e && is_lift_id lfts then + mkFix fx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn n lfts in - mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) - | FCoFix ((op,(lna,tys,bds)),e) -> + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkFix (op, (lna, tys, bds)) + | FCoFix ((op,(lna,tys,bds)) as cfx, e) -> + if is_subs_id e && is_lift_id lfts then + mkCoFix cfx + else let n = Array.length bds in - let ftys = Array.Fun1.map mk_clos e tys in - let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, - Array.Fun1.map constr_fun lfts' fbds)) + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkCoFix (op, (lna, tys, bds)) | FApp (f,ve) -> - mkApp (constr_fun lfts f, - Array.Fun1.map constr_fun lfts ve) + mkApp (to_constr lfts f, + Array.Fun1.map to_constr lfts ve) | FProj (p,c) -> - mkProj (p,constr_fun lfts c) + mkProj (p,to_constr lfts c) - | FLambda _ -> - let (na,ty,bd) = destFLambda mk_clos2 v in - mkLambda (na, constr_fun lfts ty, - constr_fun (el_lift lfts) bd) + | FLambda (len, tys, f, e) -> + if is_subs_id e && is_lift_id lfts then + Term.compose_lam (List.rev tys) f + else + let subs = comp_subs lfts e in + let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in + let f = subst_constr (subs_liftn len subs) f in + Term.compose_lam (List.rev tys) f | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) + mkProd (n, to_constr lfts t, + to_constr (el_lift lfts) c) | FLetIn (n,b,t,f,e) -> - let fc = mk_clos2 (subs_lift e) f in - mkLetIn (n, constr_fun lfts b, - constr_fun lfts t, - constr_fun (el_lift lfts) fc) + let subs = comp_subs (el_lift lfts) (subs_lift e) in + mkLetIn (n, to_constr lfts b, + to_constr lfts t, + subst_constr subs f) | FEvar ((ev,args),env) -> - mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) - | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + let subs = comp_subs lfts env in + mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) + | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FCLOS (t,env) -> - let fr = mk_clos2 env t in - let unfv = update v fr.norm fr.term in - to_constr constr_fun lfts unfv + if is_subs_id env && is_lift_id lfts then t + else + let subs = comp_subs lfts env in + subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and subst_constr subst c = match Constr.kind c with +| Rel i -> + begin match expand_rel i subst with + | Inl (k, lazy v) -> Vars.lift k v + | Inr (m, _) -> mkRel m + end +| _ -> + Constr.map_with_binders Esubst.subs_lift subst_constr subst c + +and comp_subs el s = + Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s + (* This function defines the correspondance between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) -let term_of_fconstr = - let rec term_of_fconstr_lift lfts v = - match v.term with - | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> - Term.compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx - | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift el_id - - +let term_of_fconstr c = to_constr el_id c (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a @@ -803,10 +820,12 @@ let drop_parameters depth n argstk = constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = + let open Declarations in let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (_,projs,pbs)) when + | PrimRecord infos when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = infos.(snd ind) in (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in @@ -817,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') = let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) term = FProj (Projection.make p true, right) }) projs in argss, [Zapp hstack] - | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) + | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 63daa4a7c..f8f98f0ab 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -244,6 +244,6 @@ val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr -val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr +val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) diff --git a/kernel/constr.ml b/kernel/constr.ml index 418229330..e68f906ec 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -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/cooking.ml b/kernel/cooking.ml index 68057b389..c7a84f617 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,16 +126,15 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in - let make c = Projection.make c (Projection.unfolded p) in - match kind p' with - | Const (p',_) -> mkProj (make p', substrec c') - | App (f, args) -> - (match kind f with - | Const (p', _) -> mkProj (make p', substrec c') - | _ -> assert false) - | _ -> assert false + (try + (** No need to expand parameters or universes for projections *) + let map cst = + let _ = Cmap.find cst (fst modlist) in + pop_con cst + in + let p = Projection.map map p in + let c' = substrec c' in + mkProj (p, c') with Not_found -> Constr.map substrec c) | _ -> Constr.map substrec c diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd7d6c9c..58fb5d66b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -50,7 +50,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : MutInd.t; + proj_ind : inductive; proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) @@ -109,13 +109,22 @@ v} *) (** Record information: - If the record is not primitive, then None - Otherwise, we get: + If the type is not a record, then NotRecord + If the type is a non-primitive record, then FakeRecord + If it is a primitive record, for every type in the block, we get: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - - The checked projection bodies. *) + - The checked projection bodies. -type record_body = (Id.t * Constant.t array * projection_body array) option + The kernel does not exploit the difference between [NotRecord] and + [FakeRecord]. It is mostly used by extraction, and should be extruded from + the kernel at some point. +*) + +type record_info = +| NotRecord +| FakeRecord +| PrimRecord of (Id.t * Constant.t array * projection_body array) array type regular_inductive_arity = { mind_user_arity : types; @@ -181,7 +190,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : record_body option; (** The record information *) + mind_record : record_info; (** The record information *) mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1b73096f7..3e6c4858e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -84,7 +84,7 @@ let subst_const_def sub def = match def with | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) let subst_const_proj sub pb = - { pb with proj_ind = subst_mind sub pb.proj_ind; + { pb with proj_ind = subst_ind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; } @@ -208,14 +208,21 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (id, ps, pb as r) = - let ps' = Array.Smart.map (subst_constant sub) ps in - let pb' = Array.Smart.map (subst_const_proj sub) pb in - if ps' == ps && pb' == pb then r +let subst_mind_record sub r = match r with +| NotRecord -> NotRecord +| FakeRecord -> FakeRecord +| PrimRecord infos -> + let map (id, ps, pb as info) = + let ps' = Array.Smart.map (subst_constant sub) ps in + let pb' = Array.Smart.map (subst_const_proj sub) pb in + if ps' == ps && pb' == pb then info else (id, ps', pb') + in + let infos' = Array.Smart.map map infos in + if infos' == infos then r else PrimRecord infos' let subst_mind_body sub mib = - { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; + { mind_record = subst_mind_record sub mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); diff --git a/kernel/entries.ml b/kernel/entries.ml index 3c555f8c7..724ed9ec7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -49,9 +49,9 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : (Id.t option) option; - (** Some (Some id): primitive record with id the binder name of the record - in projections. + mind_entry_record : (Id.t array option) option; + (** Some (Some ids): primitive records with ids the binder name of each + record in their respective projections. Not used by the kernel. Some None: non-primitive record *) mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d6c9117b..0e34a7165 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -515,11 +515,12 @@ let template_polymorphic_pind (ind,u) env = let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_projections = match mind.mind_record with - | None | Some None -> env.env_globals.env_projections - | Some (Some (id, kns, pbs)) -> - Array.fold_left2 (fun projs kn pb -> - Cmap_env.add kn pb projs) - env.env_globals.env_projections kns pbs + | NotRecord | FakeRecord -> env.env_globals.env_projections + | PrimRecord projs -> + Array.fold_left (fun accu (id, kns, pbs) -> + Array.fold_left2 (fun accu kn pb -> + Cmap_env.add kn pb accu) accu kns pbs) + env.env_globals.env_projections projs in let new_globals = { env.env_globals with diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 4b8edf63f..9fc3b11d7 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -134,6 +134,29 @@ let rec exp_rel lams k subs = let expand_rel k subs = exp_rel 0 k subs +let rec subs_map f = function +| ESID _ as s -> s +| CONS (x, s) -> CONS (Array.map f x, subs_map f s) +| SHIFT (n, s) -> SHIFT (n, subs_map f s) +| LIFT (n, s) -> LIFT (n, subs_map f s) + +let rec lift_subst mk_cl s1 s2 = match s1 with +| ELID -> subs_map (fun c -> mk_cl ELID c) s2 +| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2) +| ELLFT (k, s) -> + match s2 with + | CONS(x,s') -> + CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s') + | ESID n -> lift_subst mk_cl s (ESID (n + k)) + | SHIFT(k',s') -> + if k<k' + then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s'))) + else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s') + | LIFT(k',s') -> + if k<k' + then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s')) + else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s') + let rec comp mk_cl s1 s2 = match (s1, s2) with | _, ESID _ -> s1 diff --git a/kernel/esubst.mli b/kernel/esubst.mli index a674c425a..475b64f47 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift val el_lift : lift -> lift val reloc_rel : int -> lift -> int val is_lift_id : lift -> bool + +(** Lift applied to substitution: [lift_subst mk_clos el s] computes a + substitution equivalent to applying el then s. Argument + mk_clos is used when a closure has to be created, i.e. when + el is applied on an element of s. +*) +val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 14f2a3d8f..e63f43849 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -797,15 +797,23 @@ exception UndefinableExpansion build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections ((kn, _ as ind), u) nparamargs params - mind_consnrealdecls mind_consnrealargs paramslet ctx = +let compute_projections (kn, i as ind) mib = + let pkt = mib.mind_packets.(i) in + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx + | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) + 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 that typechecking projections requires just a substitution and not matching with a parameter context. *) let paramsletsubst = (* [Ind inst] is typed in context [params-wo-let] *) - let inst' = rel_list 0 nparamargs in + let inst' = rel_list 0 mib.mind_nparams in (* {params-wo-let |- subst:params] *) let subst = subst_of_rel_context_instance paramslet inst' in (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) @@ -839,7 +847,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) let fterm = mkProj (Projection.make kn false, mkRel 1) in - let body = { proj_ind = fst ind; proj_npars = nparamargs; + let body = { proj_ind = ind; proj_npars = mib.mind_nparams; proj_arg = i; proj_type = projty; } in (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion @@ -932,33 +940,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in - let pkt = packets.(0) in - let isrecord = - match isrecord with - | Some (Some rid) when pkt.mind_kelim == all_sorts - && Array.length pkt.mind_consnames == 1 - && pkt.mind_consnrealargs.(0) > 0 -> - (** The elimination criterion ensures that all projections can be defined. *) - let u = - match aiu with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx - | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) - in - let indsp = ((kn, 0), u) in - let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in - (try - let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in - let kns, projs = - compute_projections indsp nparamargs paramsctxt - pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields - in Some (Some (rid, kns, projs)) - with UndefinableExpansion -> Some None) - | Some _ -> Some None - | None -> None - in - (* Build the mutual inductive *) - { mind_record = isrecord; + let mib = + (* Build the mutual inductive *) + { mind_record = NotRecord; mind_ntypes = ntypes; mind_finite = isfinite; mind_hyps = hyps; @@ -970,6 +954,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r mind_private = prv; mind_typing_flags = Environ.typing_flags env; } + in + let record_info = match isrecord with + | Some (Some rid) -> + let is_record pkt = + pkt.mind_kelim == all_sorts + && Array.length pkt.mind_consnames == 1 + && pkt.mind_consnrealargs.(0) > 0 + in + (** The elimination criterion ensures that all projections can be defined. *) + if Array.for_all is_record packets then + let map i id = + let kn, projs = compute_projections (kn, i) mib in + (id, kn, projs) + in + try PrimRecord (Array.mapi map rid) + with UndefinableExpansion -> FakeRecord + else FakeRecord + | Some None -> FakeRecord + | None -> NotRecord + in + { mib with mind_record = record_info } (************************************************************************) (************************************************************************) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 45228e35e..7c36dac67 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,5 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_projections : pinductive -> - int -> Context.Rel.t -> int array -> int array -> - Context.Rel.t -> Context.Rel.t -> - (Constant.t array * projection_body array) +val compute_projections : inductive -> + mutual_inductive_body -> (Constant.t array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 090acdf16..9130b8778 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -293,8 +293,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (Some _) -> true - | _ -> false + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in 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 8257dc8b8..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 @@ -1965,6 +1969,7 @@ let compile_mind prefix ~interactive mb mind stack = in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in let add_proj j acc pb = + let () = assert (eq_ind ind pb.proj_ind) in let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -1985,12 +1990,14 @@ let compile_mind prefix ~interactive mb mind stack = let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + let gn = Gproj ("", ind, pb.proj_arg) in Glet (gn, mkMLlam [|c_uid|] code) :: acc in let projs = match mb.mind_record with - | None | Some None -> [] - | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + | NotRecord | FakeRecord -> [] + | PrimRecord info -> + let _, _, pbs = info.(i) in + Array.fold_left_i add_proj [] pbs in projs @ constructors @ gtype :: accu :: stack in @@ -2052,7 +2059,7 @@ let compile_deps env sigma prefix ~interactive init t = | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let pb = lookup_projection p env in - let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 0325a00b4..244e5e0dd 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -432,7 +432,6 @@ module Renv = r end -(* What about pattern matching ?*) let is_lazy prefix t = match kind t with | App (f,args) -> @@ -448,7 +447,7 @@ let is_lazy prefix t = with Not_found -> true) | _ -> true end - | LetIn _ -> true + | LetIn _ | Case _ | Proj _ -> true | _ -> false let evar_value sigma ev = sigma.evars_val ev @@ -520,8 +519,7 @@ let rec lambda_of_constr env sigma c = | Proj (p, c) -> let pb = lookup_projection p !global_env in - (** FIXME: handle mutual records *) - let ind = (pb.proj_ind, 0) in + let ind = pb.proj_ind in let prefix = get_mind_prefix !global_env (fst ind) in mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f4af31386..2c61b7a01 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -693,8 +693,8 @@ 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 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8cf588c3e..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 = @@ -226,8 +194,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 else error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x); - if mib1.mind_record <> None then begin + (** FIXME: this check looks nonsense *) + check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x); + if mib1.mind_record <> NotRecord then begin let rec names_prod_letin t = match kind t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) @@ -259,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_typing.ml b/kernel/term_typing.ml index 37bf679c5..bad449731 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -179,36 +179,36 @@ let rec is_nth_suffix n l suf = | _ :: l -> is_nth_suffix (pred n) l suf (* Given the list of signatures of side effects, checks if they match. - * I.e. if they are ordered descendants of the current revstruct *) + * I.e. if they are ordered descendants of the current revstruct. + Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor (sl, curmb) (mb, how_many) = - match curmb with - | None -> None, None - | Some curmb -> + let is_direct_ancestor accu (mb, how_many) = + match accu with + | None -> None + | Some (n, curmb) -> try let mb = CEphemeron.get mb in - match sl with - | None -> sl, None - | Some n -> - if is_nth_suffix how_many mb curmb - then Some (n + how_many), Some mb - else None, None - with CEphemeron.InvalidKey -> None, None in - let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in - sl + if is_nth_suffix how_many mb curmb + then Some (n + how_many, mb) + else None + with CEphemeron.InvalidKey -> None in + let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in + match sl with + | None -> 0 + | Some (n, _) -> n let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in - match sl, kind b with - | (None|Some 0), _ -> b, e, acc - | Some sl, LetIn (n,c,ty,bo) -> - aux (Some (sl-1)) bo + if Int.equal sl 0 then b, e, acc + else match kind b with + | LetIn (n,c,ty,bo) -> + aux (sl - 1) bo (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc) - | Some sl, App(hd,arg) -> + | App(hd,arg) -> begin match kind hd with | Lambda (n,ty,bo) -> - aux (Some (sl-1)) bo + aux (sl - 1) bo (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc) | _ -> assert false end @@ -522,23 +522,24 @@ let export_side_effects mb env c = end in let rec translate_seff sl seff acc env = - match sl, seff with - | _, [] -> List.rev acc, ce - | (None | Some 0), cbs :: rest -> + match seff with + | [] -> List.rev acc, ce + | cbs :: rest -> + if Int.equal sl 0 then let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in - translate_seff sl rest (cbs @ acc) env - | Some sl, cbs :: rest -> + translate_seff 0 rest (cbs @ acc) env + else let cbs_len = List.length cbs in let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> kn, cb, r) cbs in - translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + translate_seff (sl - cbs_len) rest (ecbs @ acc) env in translate_seff trusted seff [] env ;; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 325d5cecd..34ed2afb2 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -301,7 +301,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(MutInd.equal pb.proj_ind (fst ind)); + assert(eq_ind pb.proj_ind ind); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: CList.rev args) ty 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/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3a61c7747..71e09992c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if Option.is_empty mib.mind_record then raise (I Standard); + if mib.mind_record == Declarations.NotRecord then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with @@ -1069,8 +1069,7 @@ let extract_constant env kn cb = | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection env ind in let body = bodies.(pb.Declarations.proj_arg) in mk_typ (EConstr.of_constr body)) @@ -1086,8 +1085,7 @@ let extract_constant env kn cb = | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection env ind in let body = bodies.(pb.Declarations.proj_arg) in mk_def (EConstr.of_constr body)) diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 5571c5420..6ba937a2f 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -88,7 +88,7 @@ type ssripat = | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of ssrview (* /view *) + | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index f929e9430..23cbf49c0 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -417,8 +417,6 @@ let rwcltac cl rdx dir sr gl = then errorstrm Pp.(str "Rewriting impacts evars") else errorstrm Pp.(str "Dependent type error in rewrite of " ++ pr_constr_env (pf_env gl) (project gl) (Term.mkNamedLambda pattern_id (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) - | CErrors.UserError _ as e -> raise e - | e -> anomaly ("cvtac's exception: " ^ Printexc.to_string e); in tclTHEN cvtac' rwtac gl diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2c046190f..7fe2421f9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let cl = EConstr.Unsafe.to_constr cl in try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ @@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in - let gl = pf_merge_uc ucst gl in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 8207bc11e..46fde4115 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -119,13 +119,10 @@ let intro_end = Ssrcommon.tcl0G (isCLR_CONSUME) (** [=> _] *****************************************************************) -let intro_clear ids future_ipats = +let intro_clear ids = Goal.enter begin fun gl -> let _, clear_ids, ren = List.fold_left (fun (used_ids, clear_ids, ren) id -> - if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin - used_ids, id :: clear_ids, ren - end else let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren)) (Tacmach.New.pf_ids_of_hyps gl, [], []) ids @@ -213,22 +210,22 @@ let tclLOG p t = tclUNIT () end -let rec ipat_tac1 future_ipats ipat : unit tactic = +let rec ipat_tac1 ipat : unit tactic = match ipat with - | IPatView l -> - Ssrview.tclIPAT_VIEWS ~views:l - ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats) + | IPatView (clear_if_id,l) -> + Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id + ~conclusion:(fun ~to_clear:clr -> intro_clear clr) | IPatDispatch ipatss -> - tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) [] + tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] | IPatId id -> Ssrcommon.tclINTRO_ID id | IPatCase ipatss -> - tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) - future_ipats ipatss + ipatss | IPatAnon Drop -> intro_drop | IPatAnon One -> Ssrcommon.tclINTRO_ANON @@ -239,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatClear ids -> tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + intro_clear (List.map Ssrcommon.hyp_id ids) | IPatSimpl (Simpl n) -> V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) @@ -256,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatTac t -> t -and ipat_tac future_ipats pl : unit tactic = +and ipat_tac pl : unit tactic = match pl with | [] -> tclUNIT () | pat :: pl -> - Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*> + Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*> isTICK pat <*> - ipat_tac future_ipats pl + ipat_tac pl -and tclIORPAT tac future_ipats = function +and tclIORPAT tac = function | [[]] -> tac - | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p) + | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) let split_at_first_case ipats = let rec loop acc = function @@ -282,12 +279,27 @@ let ssr_exception is_on = function let option_to_list = function None -> [] | Some x -> [x] +(* Simple pass doing {x}/v -> /v{x} *) +let elaborate_ipats l = + let rec elab = function + | [] -> [] + | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest + | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest + | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest + | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest + | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | + IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | + IPatAbstractVars _) as x :: rest -> x :: elab rest + in + elab l + let main ?eqtac ~first_case_is_dispatch ipats = + let ipats = elaborate_ipats ipats in let ip_before, case, ip_after = split_at_first_case ipats in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in - Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) end (* }}} *) @@ -576,7 +588,7 @@ let ssrmovetac = function (tacVIEW_THEN_GRAB view ~conclusion) <*> tclIPAT (IPatClear clr :: ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView view :: IPatClear clr :: ipats) + tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7a1d06fdc..347a1e4e2 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -412,8 +412,8 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] +| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] END (* Old kinds of terms *) @@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView v -> IPatView (List.map map_ast_closure_term v) + | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -646,7 +646,7 @@ let interp_ipat ist gl = | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x | IPatTac _ -> assert false (*internal usage only *) @@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] | [ ssrdocc(occ) "->" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] + | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some [], _ -> [IPatView (true,v)] + | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] @@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] | [ "-/" integer(n) "/" integer (m) "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView v] ] + | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] END @@ -1678,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] +| [ ssrdocc(docc) cpattern(dt) ] -> [ + match docc with + | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") + | _ -> docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 11369228c..8f4b2179e 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -107,7 +107,8 @@ let rec pr_ipat p = | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon One -> str "?" - | IPatView v -> pr_view2 v + | IPatView (false,v) -> pr_view2 v + | IPatView (true,v) -> str"{}" ++ pr_view2 v | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatTac _ -> str "<tac>" diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index faebe3179..3f974ea06 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -67,9 +67,9 @@ end module State : sig (* View storage API *) - val vsINIT : EConstr.t -> unit tactic - val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic - val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic + val vsINIT : EConstr.t * Id.t list -> unit tactic + val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic + val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic val vsASSERT_EMPTY : unit tactic end = struct (* {{{ *) @@ -78,6 +78,7 @@ type vstate = { subject_name : Id.t option; (* top *) (* None if views are being applied to a term *) view : EConstr.t; (* v2 (v1 top) *) + to_clear : Id.t list; } include Ssrcommon.MakeState(struct @@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct let init = None end) -let vsINIT view = tclSET (Some { subject_name = None; view }) +let vsINIT (view, to_clear) = + tclSET (Some { subject_name = None; view; to_clear }) let vsPUSH k = tacUPDATE (fun s -> match s with - | Some { subject_name; view } -> - k view >>= fun view -> - tclUNIT (Some { subject_name; view }) + | Some { subject_name; view; to_clear } -> + k view >>= fun (view, clr) -> + tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr }) | None -> Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in @@ -102,15 +104,15 @@ let vsPUSH k = | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in Ssrcommon.tclINTRO_ID id <*> - k view >>= fun view -> - tclUNIT (Some { subject_name = Some id; view }) + k view >>= fun (view, to_clear) -> + tclUNIT (Some { subject_name = Some id; view; to_clear }) end) let vsCONSUME k = tclGET (fun s -> match s with - | Some { subject_name; view } -> + | Some { subject_name; view; to_clear } -> tclSET None <*> - k subject_name view + k ~name:subject_name view ~to_clear | None -> anomaly "vsCONSUME: empty storage") let vsASSERT_EMPTY = @@ -187,6 +189,16 @@ end * modular, see the 2 functions below that would need to "uncommit" *) let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t +let tclADD_CLEAR_IF_ID (env, ist, t) x = + Ssrprinters.ppdebug (lazy + Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); + let hd, _ = EConstr.decompose_app ist t in + match EConstr.kind ist hd with + | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) + | _ -> tclUNIT (x,[]) + +let tclPAIR p x = tclUNIT (x, p) + (* The ssr heuristic : *) (* Estimate a bound on the number of arguments of a raw constr. *) (* This is not perfect, because the unifier may fail to *) @@ -203,14 +215,15 @@ let guess_max_implicits ist glob = (fun _ -> tclUNIT 5) let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal -> - interp_glob ist glob >>= fun (env, sigma, term) -> + interp_glob ist glob >>= fun (env, sigma, term as ot) -> let term_ty = Retyping.get_type_of env sigma term in let ctx, i = Reductionops.splay_prod env sigma term_ty in let rel_ctx = List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in - if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i - then tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) - else Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i) + then Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + else tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) + >>= tclADD_CLEAR_IF_ID ot end (* There are two ways of "applying" a view to term: *) @@ -221,7 +234,7 @@ end (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) (* Builds v p *) -let interp_view ist v p = +let interp_view ~clear_if_id ist v p = let is_specialize hd = match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in (* We cast the pile of views p into a term p_id *) @@ -230,25 +243,31 @@ let interp_view ist v p = match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> Ssrprinters.ppdebug (lazy Pp.(str "specialize")); - interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr + interp_glob ist (mkGApp p_id rargs) + >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> Ssrprinters.ppdebug (lazy Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE - (pad_to_inductive ist v >>= fun vpad -> + (pad_to_inductive ist v >>= fun (vpad,clr) -> Ssrcommon.tclFIRSTa (List.map - (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)) + (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors) + >>= tclPAIR clr) (fun _ -> guess_max_implicits ist v >>= fun n -> Ssrcommon.tclFIRSTi (fun n -> - interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n) - >>= tclKeepOpenConstr + interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n + >>= fun x -> tclADD_CLEAR_IF_ID x x) + >>= fun (ot,clr) -> + if clear_if_id + then tclKeepOpenConstr ot >>= tclPAIR clr + else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view (ist, v) = +let pile_up_view ~clear_if_id (ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in - State.vsPUSH (fun p -> interp_view ist v p) + State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> @@ -292,7 +311,7 @@ let pose_proof subject_name p = <*> Tactics.New.reduce_after_refine -let rec apply_all_views ending vs s0 = +let rec apply_all_views ~clear_if_id ending vs s0 = match vs with | [] -> ending s0 | v :: vs -> @@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 = | `Tac tac -> Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); ending s0 <*> Tacinterp.eval_tactic tac <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending vs + Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs | `Term v -> Ssrprinters.ppdebug (lazy Pp.(str"..a term")); - pile_up_view v <*> apply_all_views ending vs s0 + pile_up_view ~clear_if_id v <*> + apply_all_views ~clear_if_id ending vs s0 (* Entry points *********************************************************) -let tclIPAT_VIEWS ~views:vs ~conclusion:tac = +let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac = let end_view_application s0 = - State.vsCONSUME (fun name t -> - finalize_view s0 t >>= pose_proof name <*> - tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in + State.vsCONSUME (fun ~name t ~to_clear -> + let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in + finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id end_view_application vs <*> State.vsASSERT_EMPTY end let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac = let ending_tac s0 = - State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in + State.vsCONSUME (fun ~name:_ t ~to_clear:_ -> + finalize_view s0 ~simple_types t >>= tac) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - State.vsINIT subject <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*> + State.vsINIT (subject,[]) <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id:false ending_tac vs <*> State.vsASSERT_EMPTY end diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index be51fe7f9..b128a95da 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -20,9 +20,11 @@ module AdaptorDb : sig end -(* Apply views to the top of the stack (intro pattern) *) +(* Apply views to the top of the stack (intro pattern). If clear_if_id is + * true (default false) then views that happen to be a variable are considered + * as to be cleared (see the to_clear argument to the continuation) *) val tclIPAT_VIEWS : - views:ast_closure_term list -> + views:ast_closure_term list -> ?clear_if_id:bool -> conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index c20e415b4..9d9b1b2e8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -561,8 +561,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when equal u.up_f f -> na - | KpatFixed when equal u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -582,8 +582,8 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> equal u.up_f f - | KpatFixed -> equal u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f @@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false) let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> equal u.up_f - | KpatConst -> equal u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fe49d64c7..23a985dc3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection (snd env) ind in let body = bodies.(pb.Declarations.proj_arg) in let ty = Retyping.get_type_of (snd env) sigma c in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6d08f66c1..a71ef6508 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty i,mkEvar ev else i,Stack.zip evd apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) tF tR else UnifFailure (evd,OccurCheck (fst ev,tR)))]) @@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = + let open Declarations in let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = info.(snd ind) in let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1003f86c5..d599afe69 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == BiFinite - | _ -> true + | PrimRecord _ -> mib.mind_finite == BiFinite + | NotRecord | FakeRecord -> true (* Annotation for cases *) let make_case_info env ind style = @@ -346,8 +346,10 @@ let get_constructors env (ind,params) = let get_projections env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in match mib.mind_record with - | Some (Some (id, projs, pbs)) -> Some projs - | _ -> None + | PrimRecord infos -> + let (_, projs, _) = infos.(snd (fst ind)) in + Some projs + | NotRecord | FakeRecord -> None let make_case_or_project env sigma indf ci pred c branches = let open EConstr in @@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs = build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections env (kn, _ as ind) = +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 @@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) = mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) in let x = match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | Some (Some (id, _, _)) -> Name id + | PrimRecord info-> Name (pi1 (info.(i))) in (** FIXME: handle mutual records *) let pkt = mib.mind_packets.(0) in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 4b8e0e096..7319846fb 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch -let get_proj env ((mind, _n), i) = +let get_proj env ((mind, n), i) = let mib = Environ.lookup_mind mind env in match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let _, projs, _ = info.(n) in Projection.make projs.(i) true let rec nf_val env sigma v typ = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5cf6e4b26..4ba5d2794 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t = let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with - | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> + | Construct (((_, i as ind), j), u) when j == 1 -> + let open Declarations in let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && + let (_, projs, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term = | _ -> false let eta_constructor_app env sigma f l1 term = + let open Declarations in match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let (_, projs, _) = info.(i) in let npars = mib.Declarations.mind_nparams in let pars, l1' = Array.chop npars l1 in let arg = Array.append pars [|term|] in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 5e5d00362..f926e8275 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -246,13 +246,13 @@ let print_type_in_type ref = else [] let print_primitive_record recflag mipv = function - | Some (Some (_, ps,_)) -> + | PrimRecord _ -> let eta = match recflag with | CoFinite | Finite -> str" without eta conversion" | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] - | _ -> [] + | FakeRecord | NotRecord -> [] let print_primitive ref = match ref with diff --git a/printing/printmod.ml b/printing/printmod.ml index be8bc1357..3f95dcfb6 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -217,7 +217,7 @@ let print_record env mind mib udecl = ) let pr_mutual_inductive_body env mind mib udecl = - if mib.mind_record <> None && not !Flags.raw_print then + if mib.mind_record != NotRecord && not !Flags.raw_print then print_record env mind mib udecl else print_mutual_inductive env mind mib udecl diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f34c83ae7..837865e64 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -753,8 +753,8 @@ module New = struct let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with - | None -> true,gl_make_elim - | Some _ -> false,gl_make_case_dep + | NotRecord -> true,gl_make_elim + | FakeRecord | PrimRecord _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) end 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/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/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v new file mode 100644 index 000000000..7a44db2ea --- /dev/null +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -0,0 +1,23 @@ +Require Import ssreflect. + +Axiom v1 : nat -> bool. + +Section Foo. + +Variable v2 : nat -> bool. + +Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. +Proof. +move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. +Check b1 : bool. +Check b2 : bool. +Check b3 : bool. +Check b4 : bool. +Fail Check v3. +Fail Check v4. +Fail Check v5. +Check v2 : nat -> bool. +by []. +Qed. + +End Foo. diff --git a/test-suite/ssr/rew_polyuniv.v b/test-suite/ssr/rew_polyuniv.v new file mode 100644 index 000000000..e2bbbc9ec --- /dev/null +++ b/test-suite/ssr/rew_polyuniv.v @@ -0,0 +1,90 @@ +From Coq Require Import Utf8 Setoid ssreflect. +Set Default Proof Using "Type". + +Local Set Universe Polymorphism. + +(** Telescopes *) +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X → tele) : tele. + +Arguments TeleS {_} _. + +(** The telescope version of Coq's function type *) +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => ∀ x, tele_fun (b x) T + end. + +Notation "TT -t> A" := + (tele_fun TT A) (at level 99, A at level 200, right associativity). + +(** A sigma-like type for an "element" of a telescope, i.e. the data it + takes to get a [T] from a [TT -t> T]. *) +Inductive tele_arg : tele → Type := +| TargO : tele_arg TeleO +(* the [x] is the only relevant data here *) +| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder). + +Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T := + λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T := + match a in tele_arg TT return (TT -t> T) → T with + | TargO => λ t : T, t + | TargS x a => λ f, rec a (f x) + end) TT a f. +Arguments tele_app {!_ _} _ !_ /. + +Coercion tele_arg : tele >-> Sortclass. +Coercion tele_app : tele_fun >-> Funclass. + +(** Inversion lemma for [tele_arg] *) +Lemma tele_arg_inv {TT : tele} (a : TT) : + match TT as TT return TT → Prop with + | TeleO => λ a, a = TargO + | TeleS f => λ a, ∃ x a', a = TargS x a' + end a. +Proof. induction a; eauto. Qed. +Lemma tele_arg_O_inv (a : TeleO) : a = TargO. +Proof. exact (tele_arg_inv a). Qed. +Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) : + ∃ x a', a = TargS x a'. +Proof. exact (tele_arg_inv a). Qed. + +(** Operate below [tele_fun]s with argument telescope [TT]. *) +Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U := + match TT as TT return (TT → U) → TT -t> U with + | TeleO => λ F, F TargO + | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *) + tele_bind (λ a, F (TargS x a)) + end. +Arguments tele_bind {_ !_} _ /. + +(* Show that tele_app ∘ tele_bind is the identity. *) +Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x : + (tele_app (tele_bind f)) x = f x. +Proof. + induction TT as [|X b IH]; simpl in *. + - rewrite (tele_arg_O_inv x). auto. + - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl. + rewrite IH. auto. +Qed. + +(** Notation-compatible telescope mapping *) +(* This adds (tele_app ∘ tele_bind), which is an identity function, around every + binder so that, after simplifying, this matches the way we typically write + notations involving telescopes. *) +Notation "'λ..' x .. y , e" := + (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. ))) + (at level 200, x binder, y binder, right associativity, + format "'[ ' 'λ..' x .. y ']' , e"). + +(* The testcase *) +Lemma test {TA TB : tele} {X} (α' β' γ' : X → Prop) (Φ : TA → TB → Prop) x' : + (forall P Q, ((P /\ Q) = Q) * ((P -> Q) = Q)) -> + ∀ a b, Φ a b = (λ.. x y, β' x' ∧ (γ' x' → Φ x y)) a b. +Proof. +intros cheat a b. +rewrite !tele_app_bind. +by rewrite !cheat. +Qed. diff --git a/test-suite/ssr/set_polyuniv.v b/test-suite/ssr/set_polyuniv.v new file mode 100644 index 000000000..436eeafc7 --- /dev/null +++ b/test-suite/ssr/set_polyuniv.v @@ -0,0 +1,11 @@ +From Coq Require Import ssreflect. +Set Default Proof Using "Type". + +Local Set Universe Polymorphism. + +Axiom foo : Type -> Prop. + +Lemma test : foo nat. +Proof. +set x := foo _. (* key @foo{i} matches @foo{j} *) +Abort. diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/ssr_rew_illtyped.v new file mode 100644 index 000000000..7358068c8 --- /dev/null +++ b/test-suite/ssr/ssr_rew_illtyped.v @@ -0,0 +1,9 @@ +From Coq Require Import ssreflect Setoid. + +Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}. + +Fact anomaly: forall P : SEProp, prop_of P. +Proof. +move=> [P E]. +Fail rewrite E. +Abort. 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 423f20e44..fa6a9adf1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -864,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 = @@ -873,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 940859723..202c9b92f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -292,8 +292,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u if !primitive_flag then let is_primitive = match mib.mind_record with - | Some (Some _) -> true - | Some None | None -> false + | PrimRecord _ -> true + | FakeRecord | NotRecord -> false in if not is_primitive then warn_non_primitive_record (env,indsp); @@ -403,7 +403,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t 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_private = None; @@ -562,12 +562,18 @@ 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 |