diff options
57 files changed, 838 insertions, 319 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 =========================== 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/subtyping.ml b/checker/subtyping.ml index f4ae02084..a22af4e0f 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -126,7 +126,7 @@ 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); @@ -218,16 +218,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) 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/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/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87d837b38..3807ff90c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -119,7 +119,7 @@ ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" +: "${coq_dpdgraph_CI_BRANCH:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" ######################################################################## 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..c9f574afb 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -14,15 +14,6 @@ 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 @@ -31,16 +22,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA 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/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 20e4069f4..bc72877b6 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -103,13 +103,6 @@ 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|. 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/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/nativecode.ml b/kernel/nativecode.ml index 8257dc8b8..6821fc980 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1965,6 +1965,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 +1986,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 +2055,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/subtyping.ml b/kernel/subtyping.ml index 8cf588c3e..13701d489 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -226,8 +226,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) 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/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/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/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/vernac/record.ml b/vernac/record.ml index 940859723..a97a1662e 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; |