diff options
61 files changed, 574 insertions, 389 deletions
diff --git a/.travis.yml b/.travis.yml index 86a2aea668..6273346906 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,11 +82,6 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" - # ppx_tools_versioned requires a specific version findlib - - FINDLIB_VER="" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: @@ -28,6 +28,12 @@ Tactics - The `simple apply` tactic now respects the `Opaque` flag when called from Ltac (`auto` still does not respect it). +- Tactic `constr_eq` now adds universe constraints needed for the + identity to the context (it used to ignore them). New tactic + `constr_eq_strict` checks that the required constraints already hold + without adding new ones. Preexisting tactic `constr_eq_nounivs` can + still be used if you really want to ignore universe constraints. + Tools - Coq_makefile lets one override or extend the following variables from @@ -61,6 +67,7 @@ Changes from 8.8.0 to 8.8.1 Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). +- Fix a critical bug with inlining of polymorphic constants (#7615). Notations diff --git a/checker/check.mllib b/checker/check.mllib index f79ba66e35..139fa765b4 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -3,7 +3,6 @@ Coq_config Analyze Hook Terminal -Canary Hashset Hashcons CSet diff --git a/checker/cic.mli b/checker/cic.mli index 27e2a479f5..3304b032e6 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -128,7 +128,7 @@ type section_context = unit (** {6 Substitutions} *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t @@ -211,8 +211,6 @@ type projection_body = { proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) - proj_eta : constr * constr; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility, the match version *) } type constant_def = @@ -241,7 +239,6 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; } diff --git a/checker/declarations.ml b/checker/declarations.ml index e1d2cf6d1d..a744a02279 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -196,7 +196,12 @@ let subst_con0 sub con u = let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with - | Some t -> con', t + | Some (ctx, t) -> + (** FIXME: we never typecheck the inlined term, so that it could well + be garbage. What environment do we type it in though? The substitution + code should be moot in the checker but it **is** used nonetheless. *) + let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in + con', subst_instance_constr u t | None -> let con'' = match side with | User -> constant_of_delta resolve con' @@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver = let kkey' = if dom then subst_kn subst kkey else kkey in let hint' = match hint with | Equiv kequ -> Equiv (subst_kn_delta subst kequ) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv diff --git a/checker/environ.ml b/checker/environ.ml index 809150cea9..3d5fac8066 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -166,9 +166,6 @@ let evaluable_constant cst env = try let _ = constant_value env (cst, Univ.Instance.empty) in true with Not_found | NotEvaluableConst _ -> false -let is_projection cst env = - (lookup_constant cst env).const_proj - let lookup_projection p env = Cmap_env.find (Projection.constant p) env.env_globals.env_projections diff --git a/checker/environ.mli b/checker/environ.mli index 4a7597249d..acb29d7d2d 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result val constant_value : env -> Constant.t puniverses -> constr val evaluable_constant : Constant.t -> env -> bool -val is_projection : Constant.t -> env -> bool val lookup_projection : Projection.t -> env -> projection_body (* Inductives *) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5c672d04a6..f4ae02084d 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -130,9 +130,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); - check (eq_constr) (fun x -> fst x.proj_eta); - check (eq_constr) (fun x -> snd x.proj_eta); - check (eq_constr) (fun x -> x.proj_body); true + true in let check_inductive_type t1 t2 = diff --git a/checker/values.ml b/checker/values.ml index f7ab95fe2a..31e65729b2 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 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli +MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli *) @@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0, [|[|v_dp|]; [|v_uid|]; [|v_mp;v_id|]|]) -let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|] +let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;Int|] let v_cons = v_tuple "constructor" [|v_ind;Int|] @@ -173,7 +173,7 @@ let v_section_ctxt = v_enum "emptylist" 1 (** kernel/mod_subst *) let v_delta_hint = - v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|] + v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|] let v_resolver = v_tuple "delta_resolver" @@ -225,9 +225,7 @@ let v_cst_def = let v_projbody = v_tuple "projection_body" - [|v_cst;Int;Int;v_constr; - v_tuple "proj_eta" [|v_constr;v_constr|]; - v_constr|] + [|v_cst;Int;Int;v_constr|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] @@ -241,7 +239,6 @@ let v_cb = v_tuple "constant_body" Any; v_const_univs; v_bool; - v_bool; v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) diff --git a/clib/cArray.ml b/clib/cArray.ml index b26dae7298..fc87a74cf6 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -280,7 +280,7 @@ let fold_left2_i f a v1 v2 = let rec fold a n = if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n)) (succ n) in - if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; + if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i"; fold a 0 let fold_left3 f a v1 v2 v3 = @@ -290,7 +290,7 @@ let fold_left3 f a v1 v2 v3 = else fold (f a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then - invalid_arg "Array.fold_left2"; + invalid_arg "Array.fold_left3"; fold a 0 let fold_left4 f a v1 v2 v3 v4 = diff --git a/clib/canary.ml b/clib/canary.ml deleted file mode 100644 index b8b79ed7f3..0000000000 --- a/clib/canary.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t = Obj.t - -let obj = Obj.new_block Obj.closure_tag 0 - (** This is an empty closure block. In the current implementation, it is - sufficient to allow marshalling but forbid equality. Sadly still allows - hash. *) - (** FIXME : use custom blocks somehow. *) - -module type Obj = sig type t end - -module Make(M : Obj) = -struct - type canary = t - type t = (canary * M.t) - - let prj (_, x) = x - let inj x = (obj, x) -end diff --git a/clib/canary.mli b/clib/canary.mli deleted file mode 100644 index d993eabcfd..0000000000 --- a/clib/canary.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t -(** Type of canaries. Canaries are used to ensure that an object does not use - generic operations. *) - -val obj : t -(** Canary. In the current implementation, this object is marshallable, - forbids generic comparison but still allows generic hashes. *) - -module type Obj = sig type t end - -module Make(M : Obj) : -sig - type t - val prj : t -> M.t - val inj : M.t -> t -end -(** Adds a canary to any type. *) diff --git a/clib/clib.mllib b/clib/clib.mllib index c9b4d72fce..afece4074c 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -1,4 +1,3 @@ -Canary CObj CEphemeron diff --git a/clib/hashcons.ml b/clib/hashcons.ml index ec73c6d934..39969ebf75 100644 --- a/clib/hashcons.ml +++ b/clib/hashcons.ml @@ -10,8 +10,6 @@ (* Hash consing of datastructures *) -(* The generic hash-consing functions (does not use Obj) *) - (* [t] is the type of object to hash-cons * [u] is the type of hash-cons functions for the sub-structures * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). @@ -148,41 +146,3 @@ module Hstring = Make( let len = String.length s in hash len s 0 0 end) - -(* Obj.t *) -exception NotEq - -(* From CAMLLIB/caml/mlvalues.h *) -let no_scan_tag = 251 -let tuple_p obj = Obj.is_block obj && (Obj.tag obj < no_scan_tag) - -let comp_obj o1 o2 = - if tuple_p o1 && tuple_p o2 then - let n1 = Obj.size o1 and n2 = Obj.size o2 in - if n1=n2 then - try - for i = 0 to pred n1 do - if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq - done; true - with NotEq -> false - else false - else o1=o2 - -let hash_obj hrec o = - begin - if tuple_p o then - let n = Obj.size o in - for i = 0 to pred n do - Obj.set_field o i (hrec (Obj.field o i)) - done - end; - o - -module Hobj = Make( - struct - type t = Obj.t - type u = (Obj.t -> Obj.t) * unit - let hashcons (hrec,_) = hash_obj hrec - let eq = comp_obj - let hash = Hashtbl.hash - end) diff --git a/clib/hashcons.mli b/clib/hashcons.mli index 3e396ff23c..223dd2a4d2 100644 --- a/clib/hashcons.mli +++ b/clib/hashcons.mli @@ -87,6 +87,3 @@ module Hstring : (S with type t = string and type u = unit) module Hlist (D:HashedType) : (S with type t = D.t list and type u = (D.t list -> D.t list)*(D.t->D.t)) (** Hashconsing of lists. *) - -module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit) -(** Hashconsing of OCaml values. *) diff --git a/dev/ci/README.md b/dev/ci/README.md index 665b3768a4..08364c897a 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -47,16 +47,13 @@ CI. ### Add your development by submitting a pull request -Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at -[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or -[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples); -set the corresponding variables in -[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding -target to [`Makefile.ci`](../../Makefile.ci); add new jobs to -[`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml) and -[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not -hesitate to submit an incomplete pull request if you need help to finish it.** +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **Do not hesitate to submit an incomplete pull request if you need +help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 00d04e6b3d..320ef6ed07 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -140,6 +140,24 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then fi fi +# Sanity check: PR has an outdated version of CI + +BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha') +CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml") + +if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}" +then + warning "This PR didn't run with the latest version of CI." + warning "It is probably a good idea to ask for a rebase." + read -p "Do you want to see the diff? [Y/n] " $QUICK_CONF -r + echo + if [[ ! $REPLY =~ ^[Nn]$ ]] + then + git diff "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}" + fi + ask_confirmation +fi + # Sanity check: CI failed STATUS=$(curl -s "$API/commits/$COMMIT/status") diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e10e16c107..e4d24a1f7e 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -106,7 +106,7 @@ argument. Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation -instance :math`R` if it is covariant on the same argument when the inverse +instance :math:`R` if it is covariant on the same argument when the inverse relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f65400e88c..135c24aed9 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -201,9 +201,9 @@ html_static_path = ['_static'] # The empty string is equivalent to '%b %d, %Y'. #html_last_updated_fmt = None -# If true, SmartyPants will be used to convert quotes and dashes to -# typographically correct entities. -html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there +# FIXME: this could be re-enabled after ensuring that smart quotes are locally +# disabled for all relevant directives +smartquotes = False # Custom sidebar templates, maps document names to template names. #html_sidebars = {} diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ff5d352c99..c21d8d4ec8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1925,74 +1925,75 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the -structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that -`qualid` is declared as a canonical structure using the command - .. cmd:: Canonical Structure @qualid -Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be -solved during the type-checking process, `qualid` is used as a solution. -Otherwise said, `qualid` is canonically used to extend the field |c_i| -into a complete structure built on |c_i|. + This command declares :token:`qualid` as a canonical structure. -Canonical structures are particularly useful when mixed with coercions -and strict implicit arguments. Here is an example. + Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the + structure :g:`struct` of which the fields are |x_1|, …, |x_n|. + Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + solved during the type-checking process, :token:`qualid` is used as a solution. + Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| + into a complete structure built on |c_i|. -.. coqtop:: all + Canonical structures are particularly useful when mixed with coercions + and strict implicit arguments. - Require Import Relations. + .. example:: - Require Import EqNat. + Here is an example. - Set Implicit Arguments. + .. coqtop:: all - Unset Strict Implicit. + Require Import Relations. - Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. + Require Import EqNat. - Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). + Set Implicit Arguments. - Axiom eq_nat_equiv : equivalence nat eq_nat. + Unset Strict Implicit. - Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. + Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. - Canonical Structure nat_setoid. + Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). -Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A`` -and ``B`` can be synthesized in the next statement. + Axiom eq_nat_equiv : equivalence nat eq_nat. -.. coqtop:: all + Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Lemma is_law_S : is_law S. + Canonical Structure nat_setoid. -Remark: If a same field occurs in several canonical structure, then -only the structure declared first as canonical is considered. + Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` + and :g:`B` can be synthesized in the next statement. -.. cmdv:: Canonical Structure @ident := @term : @type + .. coqtop:: all -.. cmdv:: Canonical Structure @ident := @term + Lemma is_law_S : is_law S. -.. cmdv:: Canonical Structure @ident : @type := @term + .. note:: + If a same field occurs in several canonical structures, then + only the structure declared first as canonical is considered. -These are equivalent to a regular definition of `ident` followed by the declaration -``Canonical Structure`` `ident`. + .. cmdv:: Canonical Structure @ident {? : @type } := @term -See also: more examples in user contribution category (Rocq/ALGEBRA). + This is equivalent to a regular definition of :token:`ident` followed by the + declaration :n:`Canonical Structure @ident`. -Print Canonical Projections. -++++++++++++++++++++++++++++ +.. cmd:: Print Canonical Projections -This displays the list of global names that are components of some -canonical structure. For each of them, the canonical structure of -which it is a projection is indicated. For instance, the above example -gives the following output: + This displays the list of global names that are components of some + canonical structure. For each of them, the canonical structure of + which it is a projection is indicated. -.. coqtop:: all + .. example:: + + For instance, the above example gives the following output: + + .. coqtop:: all - Print Canonical Projections. + Print Canonical Projections. Implicit types of variables diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b2009657f..1c554acdb8 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3657,7 +3657,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. coqtop:: reset - From Coq Require Import ssreflect ssrfun ssrbool List. + From Coq Require Import ssreflect ssrfun ssrbool. + From Coq Require Import List. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 29c2f8b815..d0a0d568ea 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise. :name: constr_eq This tactic checks whether its arguments are equal modulo alpha - conversion and casts. + conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. +.. exn:: Not equal (due to universes). + +.. tacn:: constr_eq_strict @term @term + :name: constr_eq_strict + + This tactic checks whether its arguments are equal modulo alpha + conversion, casts and universe constraints. It does not add new + constraints. + +.. exn:: Not equal. +.. exn:: Not equal (due to universes). .. tacn:: unify @term @term :name: unify diff --git a/engine/evd.ml b/engine/evd.ml index 0c9c3a29b2..f56f9662d6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -894,6 +894,9 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' +let check_constraints evd csts = + UGraph.check_constraints csts (UState.ugraph evd.universes) + let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } diff --git a/engine/evd.mli b/engine/evd.mli index c40e925d81..405fcc4037 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -552,6 +552,8 @@ val set_eq_instances : ?flex:bool -> val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool +val check_constraints : evar_map -> Univ.Constraint.t -> bool + val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_subst : evar_map -> UnivSubst.universe_opt_subst diff --git a/interp/declare.ml b/interp/declare.ml index bc2d2068a2..aa737239ba 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -382,17 +382,34 @@ let inInductive : inductive_obj -> obj = discharge_function = discharge_inductive; rebuild_function = infer_inductive_subtyping } -let declare_projections mind = - let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in +let declare_projections univs mind = + let env = Global.env () in + let spec,_ = Inductive.lookup_mind_specif env (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, _)) -> + let projs = Inductiveops.compute_projections env (mind, 0) in + Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in - let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) - in - assert(Constant.equal kn kn')) kns; true,true + let univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + Polymorphic_const_entry ctx + | Cumulative_ind_entry ctx -> + Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + in + let term, types = match univs with + | Monomorphic_const_entry _ -> term, types + | Polymorphic_const_entry ctx -> + let u = Univ.UContext.instance ctx in + Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + in + let entry = definition_entry ~types ~univs term in + let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + assert (Constant.equal kn kn') + ) kns projs; + true, true | Some None -> true,false | None -> false,false @@ -403,7 +420,7 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isrecord,isprim = declare_projections mind in + let isrecord,isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim diff --git a/kernel/constr.ml b/kernel/constr.ml index c11b9ebf46..4182293301 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array -type rec_declaration = Name.t array * constr array * constr array -type fixpoint = (int array * int) * rec_declaration - (* The array of [int]'s tells for each component of the array of - mutual fixpoints the number of lambdas to skip before finding the - recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) - (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is - the recursive argument); - The second component [int] tells which component of the block is - returned *) -type cofixpoint = int * rec_declaration - (* The component [int] tells which component of the block of - cofixpoint is returned *) type types = constr +type rec_declaration = (constr, types) prec_declaration +type fixpoint = (constr, types) pfixpoint +type cofixpoint = (constr, types) pcofixpoint + (*********************) (* Term constructors *) (*********************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 742a13919a..bf7b5e87b5 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) -type rec_declaration = Name.t array * types array * constr array -type fixpoint = (int array * int) * rec_declaration +type ('constr, 'types) prec_declaration = + Name.t array * 'types array * 'constr array +type ('constr, 'types) pfixpoint = + (int array * int) * ('constr, 'types) prec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) + +type ('constr, 'types) pcofixpoint = + int * ('constr, 'types) prec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) + +type rec_declaration = (constr, types) prec_declaration + +type fixpoint = (constr, types) pfixpoint val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] @@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr ... with fn = bn.] *) -type cofixpoint = int * rec_declaration +type cofixpoint = (constr, types) pcofixpoint val mkCoFix : cofixpoint -> constr @@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = Evar.t * 'constr array -type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5783453e66..68057b389f 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } = { cook_body = body; cook_type = typ; - cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0d907f3dea..76c79335f1 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd70c0502..7bd7d6c9ca 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -54,8 +54,6 @@ type projection_body = { proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) - proj_eta : constr * types; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility with VMs only, the match version *) } (* Global declarations (i.e. constants) can be either: *) @@ -87,7 +85,6 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 75c0e5b4cc..1b73096f7f 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -86,7 +86,7 @@ let subst_const_def sub def = match def with let subst_const_proj sub pb = { pb with proj_ind = subst_mind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; - proj_body = subst_const_type sub pb.proj_body } + } let subst_const_body sub cb = assert (List.is_empty cb.const_hyps); (* we're outside sections *) @@ -100,7 +100,6 @@ let subst_const_body sub cb = { const_hyps = []; const_body = body'; const_type = type'; - const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7eb..3c555f8c7b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.Named.t option * types in_constant_universes_entry * inline -type projection_entry = { - proj_entry_ind : MutInd.t; - proj_entry_arg : int } - type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry - | ProjectionEntry of projection_entry (** {6 Modules } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index fb89576dd0..2d6c9117b3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -490,7 +490,7 @@ let lookup_projection cst env = Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - (lookup_constant cst env).const_proj + Cmap_env.mem cst env.env_globals.env_projections (* Mutual Inductives *) let polymorphic_ind (mind,i) env = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 439acd15bf..14f2a3d8f4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -797,16 +797,13 @@ 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 as indu) n x nparamargs params +let compute_projections ((kn, _ as ind), u) nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = 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 indty, paramsletsubst = - (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in - let ty = mkApp (mkIndU indu, inst) in + let paramsletsubst = (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in (* {params-wo-let |- subst:params] *) @@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst in - ty, subst + subst in - let ci = - let print_info = - { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in - { ci_ind = ind; - ci_npar = nparamargs; - ci_cstr_ndecls = mind_consnrealdecls; - ci_cstr_nargs = mind_consnrealargs; - ci_pp_info = print_info } - in - let len = List.length ctx in - let x = Name x in - let compat_body ccl i = - (* [ccl] is defined in context [params;x:indty] *) - (* [ccl'] is defined in context [params;x:indty;x:indty] *) - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 indty, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in - let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in - it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params - in - let projections decl (i, j, kns, pbs, subst, letsubst) = + let projections decl (i, j, kns, pbs, letsubst) = match decl with | LocalDef (na,c,t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] - to [params, x:I |- c(params,proj1 x,..,projj x)] *) - let c1 = substl subst c in - (* From [params, x:I |- subst:field1,..,fieldj] - to [params, x:I |- subst:field1,..,fieldj+1] where [subst] - is represented with instance of field1 last *) - let subst = c1 :: subst in - (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) let c2 = substl letsubst c in (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in - (i, j+1, kns, pbs, subst, letsubst) + (i, j+1, kns, pbs, letsubst) | LocalAssum (na,t) -> match na with | Name id -> @@ -868,21 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let projty = substl letsubst t in (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) - let ty = substl subst t in - let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in - let compat = compat_body ty (j - 1) in - let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in - let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in let body = { proj_ind = fst ind; proj_npars = nparamargs; - proj_arg = i; proj_type = projty; proj_eta = etab, etat; - proj_body = compat } in - (i + 1, j + 1, kn :: kns, body :: pbs, - fterm :: subst, fterm :: letsubst) + proj_arg = i; proj_type = projty; } in + (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, kns, pbs, subst, letsubst) = - List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst) + let (_, _, kns, pbs, letsubst) = + List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev kns), Array.of_list (List.rev pbs) @@ -987,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r (try let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt + compute_projections indsp nparamargs paramsctxt pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields in Some (Some (rid, kns, projs)) with UndefinableExpansion -> Some None) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a38172c2d..45228e35e8 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,7 @@ 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 -> Id.t -> Id.t -> +val compute_projections : pinductive -> int -> Context.Rel.t -> int array -> int array -> Context.Rel.t -> Context.Rel.t -> (Constant.t array * projection_body array) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 0027ebecfc..a47af56ca5 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -24,7 +24,7 @@ open Constr is the term into which we should inline. *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t (* NB: earlier constructor Prefix_equiv of ModPath.t @@ -158,7 +158,7 @@ let find_prefix resolve mp = (** Applying a resolver to a kernel name *) -exception Change_equiv_to_inline of (int * constr) +exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr)) let solve_delta_kn resolve kn = try @@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) = let knu = KerName.make mpu dir l in let knc = if mpu == mpc then knu else KerName.make mpc dir l in match search_delta_inline resolve knu knc with - | Some t -> + | Some (ctx, t) -> (* In case of inlining, discard the canonical part (cf #2608) *) - Constant.make1 knu, t + let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in + Constant.make1 knu, Vars.subst_instance_constr u t | None -> let knc' = progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc @@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver = | Equiv kequ -> (try Equiv (subst_kn_delta subst kequ) with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c)) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index b14d392073..76a1d173b9 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -28,7 +28,7 @@ val add_kn_delta_resolver : KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver diff --git a/kernel/modops.ml b/kernel/modops.ml index 2038171183..22f523a9ae 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + let ctx = Declareops.constant_polymorphic_context constant in + add_inline_delta_resolver kn (lev, Some (ctx, constr)) l with Not_found -> error_no_such_label_sub (Constant.label con) (ModPath.to_string (Constant.modpath con)) diff --git a/kernel/names.ml b/kernel/names.ml index 597061278d..1d2a7c4ce5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ the module system, Aug 2002 *) (* Abstraction over the type of constant for module inlining by Claudio Sacerdoti, Nov 2004 *) -(* Miscellaneous features or improvements by Hugo Herbelin, +(* Miscellaneous features or improvements by Hugo Herbelin, Élie Soubiran, ... *) open Pp @@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath) module KerName = struct type t = { - canary : Canary.t; modpath : ModPath.t; dirpath : DirPath.t; knlabel : Label.t; @@ -372,16 +371,14 @@ module KerName = struct (** Lazily computed hash. If unset, it is set to negative values. *) } - let canary = Canary.obj - type kernel_name = t let make modpath dirpath knlabel = - { modpath; dirpath; knlabel; refhash = -1; canary; } + { modpath; dirpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.dirpath, kn.knlabel) let make2 modpath knlabel = - { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; } + { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; } let modpath kn = kn.modpath let label kn = kn.knlabel @@ -437,7 +434,7 @@ module KerName = struct * (string -> string) let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in - { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } + { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; } let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index db1109e75e..37bf679c51 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } - | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (Some (id, kns, pbs)) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | _ -> assert false - in - let univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Monomorphic_const ctx - | Polymorphic_ind auctx -> Polymorphic_const auctx - | Cumulative_ind acumi -> - Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) - in - let term, typ = pb.proj_eta in - { - Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); - cook_type = typ; - cook_proj = true; - cook_universes = univs; - cook_inline = false; - cook_context = None; - } - let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = @@ -464,7 +434,6 @@ let build_constant_declaration kn env result = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; const_inline_code = result.cook_inline; diff --git a/lib/spawn.ml b/lib/spawn.ml index 63e9e452cb..0652623b74 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -15,14 +15,12 @@ let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () -type req = ReqDie | ReqStats | Hello of int * int -type resp = RespStats of Gc.stat +type req = ReqDie | Hello of int * int module type Control = sig type handle val kill : handle -> unit - val stats : handle -> Gc.stat val wait : handle -> Unix.process_status val unixpid : handle -> int val uid : handle -> string @@ -43,7 +41,6 @@ module type MainLoopModel = sig end (* Common code *) -let assert_ b s = if not b then CErrors.anomaly (Pp.str s) (* According to http://caml.inria.fr/mantis/view.php?id=5325 * you can't use the same socket for both writing and reading (may change @@ -125,14 +122,26 @@ let filter_args args = Array.of_list (aux (Array.to_list args)) let spawn_with_control prefer_sock env prog args = - let control_sock, control_sock_name = mk_socket_channel () in - let extra = [| "-control-channel"; control_sock_name |] in - let args = Array.append extra (filter_args args) in + (* on non-Unix systems we create a control channel *) + let not_Unix = Sys.os_type <> "Unix" in + let args = filter_args args in + let args, control_sock = + if not_Unix then + let control_sock, control_sock_name = mk_socket_channel () in + let extra = [| "-control-channel"; control_sock_name |] in + Array.append extra args, Some control_sock + else + args, None in let (pid, cin, cout, s), is_sock = - if Sys.os_type <> "Unix" || prefer_sock + if not_Unix (* pipes only work well on Unix *) || prefer_sock then spawn_sock env prog args, true else spawn_pipe env prog args, false in - let _, oob_resp, oob_req = accept control_sock in + let oob_resp, oob_req = + if not_Unix then + let _, oob_resp, oob_req = accept (Option.get control_sock) in + Some oob_resp, Some oob_req + else + None, None in pid, oob_resp, oob_req, cin, cout, s, is_sock let output_death_sentence pid oob_req = @@ -146,8 +155,8 @@ module Async(ML : MainLoopModel) = struct type process = { cin : in_channel; cout : out_channel; - oob_resp : in_channel; - oob_req : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; gchan : ML.async_chan; pid : int; mutable watch : ML.watch_id option; @@ -166,11 +175,11 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) = if not alive then prerr_endline "This process is already dead" else begin try Option.iter ML.remove_watch watch; - output_death_sentence (uid p) oob_req; + Option.iter (output_death_sentence (uid p)) oob_req; close_in_noerr cin; close_out_noerr cout; - close_in_noerr oob_resp; - close_out_noerr oob_req; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; p.watch <- None with e -> prerr_endline ("kill: "^Printexc.to_string e) end @@ -199,12 +208,6 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) ); p, cout -let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead."; - output_value oob_req ReqStats; - flush oob_req; - input_value oob_resp - let rec wait p = (* On windows kill is not reliable, so wait may never return. *) if Sys.os_type = "Unix" then @@ -221,8 +224,8 @@ module Sync () = struct type process = { cin : in_channel; cout : out_channel; - oob_resp : in_channel; - oob_req : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; pid : int; mutable alive : bool; } @@ -242,20 +245,14 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try - output_death_sentence (uid p) oob_req; + Option.iter (output_death_sentence (uid p)) oob_req; close_in_noerr cin; close_out_noerr cout; - close_in_noerr oob_resp; - close_out_noerr oob_req; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; with e -> prerr_endline ("kill: "^Printexc.to_string e) end -let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead."; - output_value oob_req ReqStats; - flush oob_req; - let RespStats g = input_value oob_resp in g - let rec wait p = (* On windows kill is not reliable, so wait may never return. *) if Sys.os_type = "Unix" then diff --git a/lib/spawn.mli b/lib/spawn.mli index c7a56349c6..944aa27a7f 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -25,7 +25,6 @@ module type Control = sig type handle val kill : handle -> unit - val stats : handle -> Gc.stat val wait : handle -> Unix.process_status val unixpid : handle -> int @@ -76,6 +75,5 @@ end (* This is exported to separate the Spawned module, that for simplicity assumes * Threads so it is in a separate file *) -type req = ReqDie | ReqStats | Hello of int * int +type req = ReqDie | Hello of int * int val proto_version : int -type resp = RespStats of Gc.stat diff --git a/library/heads.ml b/library/heads.ml index 3d5f6a6ff0..d9d650ac07 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body + if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5aee70194d..3a61c7747d 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,11 +1065,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_typ (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1078,11 +1082,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_def (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f2899ab63c..660e29ca82 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -793,17 +793,12 @@ END (* ********************************************************************* *) -let eq_constr x y = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes env evd x y with - | Some _ -> Proofview.tclUNIT () - | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end - TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] END TACTIC EXTEND constr_eq_nounivs diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index df89d9eac2..5a54c6f05b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - let body = pb.Declarations.proj_body in + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) 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 let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ecec30cfc..11cfd20403 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -414,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) +exception UnsoundRenaming + let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l -let test_id l id = if collide_id l id then raise Not_found +let test_id l id = if collide_id l id then raise UnsoundRenaming let test_na l na = Name.iter (test_id l) na let update_subst na l = @@ -429,8 +431,6 @@ let update_subst na l = else na,l) na (na,l) -exception UnsoundRenaming - let rename_var l id = try let id' = Id.List.assoc id l in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 27b029aade..4ab932723e 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr env 0 f (List.rev cstr.cs_args, recargs) (* Main function *) -let mis_make_indrec env sigma listdepkind mib u = +let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in @@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* Body on make_one_rec *) let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in - if (mis_is_recursive_subset + if force_mutual || (mis_is_recursive_subset (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then @@ -558,7 +558,7 @@ let check_arities env listdepkind = [] listdepkind in true -let build_mutual_induction_scheme env sigma = function +let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in if dep && not (Inductiveops.has_dependent_elim mib) then @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function lrecspec) in let _ = check_arities env listdepkind in - mis_make_indrec env sigma listdepkind mib u + mis_make_indrec env sigma ~force_mutual listdepkind mib u | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index d87a19d282..de9d3a0abf 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive -> (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list + env -> evar_map -> ?force_mutual:bool -> + (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f839d5b983..1003f86c56 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -456,6 +456,110 @@ let build_branch_type env sigma dep p cs = (**************************************************) +(** From a rel context describing the constructor arguments, + 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 open Term in + let mib = Environ.lookup_mind kn env in + let indu = match mib.mind_universes with + | Monomorphic_ind _ -> mkInd ind + | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx) + | Cumulative_ind ctx -> + mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) + in + let x = match mib.mind_record with + | None | Some None -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + | Some (Some (id, _, _)) -> Name id + in + (** FIXME: handle mutual records *) + let pkt = mib.mind_packets.(0) in + let { mind_consnrealargs; mind_consnrealdecls } = pkt in + let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in + let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in + let 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 indty = + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in + let ty = mkApp (indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + ty + in + let ci = + let print_info = + { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in + { ci_ind = ind; + ci_npar = nparamargs; + ci_cstr_ndecls = mind_consnrealdecls; + ci_cstr_nargs = mind_consnrealargs; + ci_pp_info = print_info } + in + let len = List.length ctx in + let compat_body ccl i = + (* [ccl] is defined in context [params;x:indty] *) + (* [ccl'] is defined in context [params;x:indty;x:indty] *) + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 indty, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in + let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in + it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params + in + let projections decl (j, pbs, subst) = + match decl with + | LocalDef (na,c,t) -> + (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) + let c = liftn 1 j c in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (j+1, pbs, subst) + | LocalAssum (na,t) -> + match na with + | Name id -> + let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst t in + let term = mkProj (Projection.make kn true, mkRel 1) in + let fterm = mkProj (Projection.make kn false, mkRel 1) in + let compat = compat_body ty (j - 1) in + let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in + let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in + let body = (etab, etat, compat) in + (j + 1, body :: pbs, fterm :: subst) + | Anonymous -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + in + let (_, pbs, subst) = + List.fold_right projections ctx (1, [], []) + in + Array.rev_of_list pbs + +let legacy_match_projection env ind = + Array.map pi3 (compute_projections env ind) + +let compute_projections ind mib = + let ans = compute_projections ind mib in + Array.map (fun (prj, ty, _) -> (prj, ty)) ans + +(**************************************************) + let extract_mrectype sigma t = let open EConstr in let (t, l) = decompose_app sigma t in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b0d714b03d..aa53f7e67c 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,6 +194,18 @@ val make_case_or_project : val make_default_case_info : env -> case_style -> inductive -> case_info i*) +val compute_projections : Environ.env -> inductive -> (constr * types) array +(** Given a primitive record type, for every field computes the eta-expanded + projection and its type. *) + +val legacy_match_projection : Environ.env -> inductive -> constr array +(** Given a record type, computes the legacy match-based projection of the + projections. + + BEWARE: such terms are ill-typed, and should thus only be used in upper + layers. The kernel will probably badly fail if presented with one of + those. *) + (********************) val type_of_inductive_knowing_conclusion : diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 544175c6d2..ba4cde6d67 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -87,7 +87,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let evd' = if has_typeclass then Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars - ~fail:(not with_evars) clenv.env clenv.evd + ~fail:(not with_evars) ~split:false clenv.env clenv.evd else clenv.evd in if has_resolvable then diff --git a/stm/spawned.ml b/stm/spawned.ml index 3833c8026e..a5d6ea96f9 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -28,13 +28,11 @@ let controller h pr pw = prerr_endline "starting controller thread"; let main () = let ic, oc = open_bin_connection h pr pw in - let rec loop () = + let loop () = try match CThread.thread_friendly_input_value ic with | Hello _ -> prerr_endline "internal protocol error"; exit 1 | ReqDie -> prerr_endline "death sentence received"; exit 0 - | ReqStats -> - output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop () with | e -> prerr_endline ("control channel broken: " ^ Printexc.to_string e); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 770e31fea1..c430edf2e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5034,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac = else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in abstract_subproof ~opaque s gk tac +let constr_eq ~strict x y = + let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in + let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + match EConstr.eq_constr_universes env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + if strict then + if Evd.check_constraints evd csts then Proofview.tclUNIT () + else fail_universes + else + (match Evd.add_constraints evd csts with + | evd -> Proofview.Unsafe.tclEVARS evd + | exception Univ.UniverseInconsistency _ -> + fail_universes) + | None -> fail + end + let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 8d43024507..57f20d2ff2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -409,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - (** {6 Other tactics. } *) +(** Syntactic equality up to universes. With [strict] the universe + constraints must be already true to succeed, without [strict] they + are added to the evar map. *) +val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic + val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v new file mode 100644 index 0000000000..afcdd35fcc --- /dev/null +++ b/test-suite/bugs/closed/7421.v @@ -0,0 +1,39 @@ + + +Universe i j. + +Goal False. +Proof. + Check Type@{i} : Type@{j}. + Fail constr_eq_strict Type@{i} Type@{j}. + assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *) + Fail constr_eq_strict Type@{i} Type@{j}. + + constr_eq Type@{i} Type@{j}. (* <- i=j is retained *) + constr_eq_strict Type@{i} Type@{j}. + Fail Check Type@{i} : Type@{j}. + + Fail constr_eq Prop Set. + Fail constr_eq Prop Type. + + Fail constr_eq_strict Type Type. + constr_eq Type Type. + + constr_eq_strict Set Set. + constr_eq Set Set. + constr_eq Prop Prop. + + let x := constr:(Type) in constr_eq_strict x x. + let x := constr:(Type) in constr_eq x x. + + Fail lazymatch type of prod with + | ?A -> ?B -> _ => constr_eq_strict A B + end. + lazymatch type of prod with + | ?A -> ?B -> _ => constr_eq A B + end. + lazymatch type of prod with + | ?A -> ?B -> ?C => constr_eq A C + end. + +Abort. diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v new file mode 100644 index 0000000000..cd8c4ad7df --- /dev/null +++ b/test-suite/bugs/closed/7615.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +Module Type S. +Parameter Inline T@{i} : Type@{i+1}. +End S. + +Module F (X : S). +Definition X@{j i} : Type@{j} := X.T@{i}. +End F. + +Module M. +Definition T@{i} := Type@{i}. +End M. + +Module N := F(M). + +Require Import Hurkens. + +Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl. diff --git a/test-suite/bugs/closed/7811.v b/test-suite/bugs/closed/7811.v new file mode 100644 index 0000000000..fee330f22d --- /dev/null +++ b/test-suite/bugs/closed/7811.v @@ -0,0 +1,114 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) +(* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *) +(* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3 + coqtop version 8.8.0 (May 2018) *) + +(* This was triggering a "Not_found" at the time of printing/showing the goal *) + +Require Coq.Unicode.Utf8. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing). + +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X -> tele) : tele. + +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => forall x, tele_fun (b x) T + end. + +Inductive tele_arg : tele -> Type := +| TargO : tele_arg TeleO +| TargS {X} {binder} (x : X) : tele_arg (binder x) -> tele_arg (TeleS binder). + +Axiom tele_app : forall {TT : tele} {T} (f : tele_fun TT T), tele_arg TT -> T. + +Coercion tele_arg : tele >-> Sortclass. + +Inductive val := + | LitV + | PairV (v1 v2 : val) + | InjLV (v : val) + | InjRV (v : val). +Axiom coPset : Set. +Axiom atomic_update : forall {PROP : Type} {TA TB : tele}, coPset -> coPset -> (TA -> PROP) -> (TA -> TB -> PROP) -> (TA -> TB -> PROP) -> PROP. +Import Coq.Unicode.Utf8. +Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" := + (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) + (TB:=TeleO) + Eo Ei + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, α) ..) + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, tele_app (TT:=TeleO) β) .. ) + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ) .. ) + ) + (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, + format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope. + +Axiom ident : Set. +Inductive env (A : Type) : Type := Enil : env A | Esnoc : env A → ident → A → env A. +Record envs (PROP : Type) : Type + := Envs { env_spatial : env PROP }. +Axiom positive : Set. +Axiom Qp : Set. +Axiom one : positive. +Goal forall (T : Type) (T0 : forall _ : T, Type) (P : Set) + (u : T) (γs : P) (Q : T0 u) (Φ o : forall _ : val, T0 u) + (stack_content0 : forall (_ : P) (_ : list val), T0 u) + (c c0 : coPset) (l : forall (A : Type) (_ : list A), list A) + (e0 : forall (_ : env (T0 u)) (_ : positive), envs (T0 u)) + (i0 : ident) (o1 : forall (_ : Qp) (_ : val), T0 u) + (b0 : forall _ : env (T0 u), T0 u) (P0 : forall _ : T0 u, Type) + (u0 : forall (_ : T0 u) (_ : T0 u), T0 u), + P0 + (@atomic_update (T0 u) + (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) TeleO c c0 + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (T0 u) (fun (v : val) (q : Qp) => o1 q v)) + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (forall _ : tele_arg TeleO, T0 u) + (fun (v : val) (q : Qp) => @tele_app TeleO (T0 u) (o1 q v))) + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (forall _ : tele_arg TeleO, T0 u) + (fun (x : val) (_ : Qp) => + @tele_app TeleO (T0 u) + (u0 + (b0 + match + e0 + (@Esnoc (T0 u) (@Enil (T0 u)) i0 + (@atomic_update (T0 u) + (@TeleS (list val) (fun _ : list val => TeleO)) TeleO + c c0 + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (T0 u) (fun l0 : list val => stack_content0 γs l0)) + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (forall _ : tele_arg TeleO, T0 u) + (fun l0 : list val => + @tele_app TeleO (T0 u) + (stack_content0 γs (l val l0)))) + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (forall _ : tele_arg TeleO, T0 u) + (fun x1 : list val => + @tele_app TeleO (T0 u) + (u0 Q + (Φ + match x1 return val with + | nil => InjLV LitV + | cons v _ => InjRV v + end)))))) one + return (env (T0 u)) + with + | Envs _ env_spatial0 => env_spatial0 + end) (o x))))) +. + Show. +Abort. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 8d08f5975e..717dc0debe 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -169,7 +169,7 @@ Proof. Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. - Timeout 1 Fail apply _. (* 0.06s *) +Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2deca1e069..e86e108772 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -370,7 +370,7 @@ requested | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) -let do_mutual_induction_scheme lnamedepindsort = +let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort and env0 = Global.env() in let sigma, lrecspec, _ = @@ -388,7 +388,7 @@ let do_mutual_induction_scheme lnamedepindsort = (evd, (indu,dep,sort) :: l, inst)) lnamedepindsort (Evd.from_env env0,[],None) in - let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in + let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma ~force_mutual lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 261c3d8139..ebfc76de9d 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -29,9 +29,13 @@ val declare_congr_scheme : inductive -> unit val declare_rewriting_schemes : inductive -> unit -(** Mutual Minimality/Induction scheme *) +(** Mutual Minimality/Induction scheme. + [force_mutual] forces the construction of eliminators having the same predicates and + methods even if some of the inductives are not recursive. + By default it is [false] and some of the eliminators are defined as simple case analysis. + *) -val do_mutual_induction_scheme : +val do_mutual_induction_scheme : ?force_mutual:bool -> (lident * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) |