aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml5
-rw-r--r--Makefile.ci1
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-coqtail.sh8
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile7
-rw-r--r--dev/vm_printers.ml5
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst6
-rw-r--r--kernel/byterun/coq_interp.c2
-rw-r--r--kernel/byterun/coq_values.h1
-rw-r--r--kernel/cPrimitives.mli1
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cemitcodes.ml8
-rw-r--r--kernel/primred.ml77
-rw-r--r--kernel/primred.mli7
-rw-r--r--kernel/term_typing.ml16
-rw-r--r--kernel/vmvalues.ml20
-rw-r--r--kernel/vmvalues.mli3
-rw-r--r--pretyping/vnorm.ml26
-rw-r--r--test-suite/arithmetic/primitive.v12
-rw-r--r--test-suite/success/primitive.v69
-rw-r--r--test-suite/success/sprop.v4
-rw-r--r--test-suite/success/unfold.v70
-rw-r--r--vernac/comPrimitive.ml8
-rw-r--r--vernac/himsg.ml25
24 files changed, 291 insertions, 99 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ec8fe23171..32b05ec746 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
- CACHEKEY: "bionic_coq-V2020-05-24-V1"
+ CACHEKEY: "bionic_coq-V2020-07-21-V38"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
@@ -726,6 +726,9 @@ library:ci-coqprime:
- build:edge+flambda
- plugin:ci-bignums
+library:ci-coqtail:
+ extends: .ci-template
+
library:ci-coquelicot:
extends: .ci-template
diff --git a/Makefile.ci b/Makefile.ci
index 77d8bda671..85e4b965f9 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS= \
ci-color \
ci-compcert \
ci-coq_dpdgraph \
+ ci-coqtail \
ci-coquelicot \
ci-corn \
ci-cross_crypto \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4973cbb478..2725e6b56c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -380,3 +380,10 @@
: "${sf_CI_REF:=master}"
: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
+
+########################################################################
+# Coqtail
+########################################################################
+: "${coqtail_CI_REF:=master}"
+: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}"
+: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh
new file mode 100755
index 0000000000..b8b5c6c724
--- /dev/null
+++ b/dev/ci/ci-coqtail.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coqtail
+
+( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8c5696f4f9..7570b17095 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-24-V1"
+# CACHEKEY: "bionic_coq-V2020-07-21-V38"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -17,9 +17,10 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
# Dependencies of source-doc and coq-makefile
texlive-science tipa
-# More dependencies of the sphinx doc
+# More dependencies of the sphinx doc, pytest for coqtail
RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
- antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2
+ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \
+ pytest==5.4.3
# We need to install OPAM 2.0 manually for now.
RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index aa650fbdc8..ac4972ed0d 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,6 +1,5 @@
open Format
open Term
-open Constr
open Names
open Cemitcodes
open Vmvalues
@@ -8,9 +7,7 @@ open Vmvalues
let ppripos (ri,pos) =
(match ri with
| Reloc_annot a ->
- let sp,i = a.ci.ci_ind in
- print_string
- ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+ print_string "switch\n"
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fcd5ecc070..18149a690a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1786,13 +1786,13 @@ Tactic notations allow customizing the syntax of tactics.
* - ``reference``
- :token:`qualid`
- - a global reference of term
- - :tacn:`unfold`
+ - a qualified identifier
+ - name of an |Ltac|-defined tactic
* - ``smart_global``
- :token:`reference`
- a global reference of term
- - :tacn:`with_strategy`
+ - :tacn:`unfold`, :tacn:`with_strategy`
* - ``constr``
- :token:`term`
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9921208e04..15cc451ea8 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1187,7 +1187,7 @@ value coq_interprete
if (sz == 0) accu = Atom(0);
else {
Alloc_small(accu, sz, Default_tag);
- if (Field(*sp, 2) == Val_true) {
+ if (Is_tailrec_switch(*sp)) {
for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
}else{
for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 86ae6295fd..a19f9b56c1 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -32,6 +32,7 @@
#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#define Is_double(v) (Tag_val(v) == Double_tag)
+#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
/* coq array */
#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 5e5fad9f04..41b3bff465 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -128,6 +128,7 @@ val prim_ind_to_string : 'a prim_ind -> string
(** Can raise [Not_found] *)
val op_or_type_of_string : string -> op_or_type
+
val op_or_type_to_string : op_or_type -> string
val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7bff377238..bacc308e1f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont =
done;
let annot =
- {ci = ci; rtbl = rtbl; tailcall = is_tailcall;
+ {rtbl = rtbl; tailcall = is_tailcall;
max_stack_size = !max_stack_size - sz}
in
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6b4daabf0c..ed475dca7e 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -13,7 +13,6 @@
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
open Names
-open Constr
open Vmvalues
open Cbytecodes
open Copcodes
@@ -424,12 +423,11 @@ let subst_strcst s sc =
| Const_float _ -> sc
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
+let subst_annot _ (a : annot_switch) = a
+
let subst_reloc s ri =
match ri with
- | Reloc_annot a ->
- let (kn,i) = a.ci.ci_ind in
- let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
- Reloc_annot {a with ci = ci}
+ | Reloc_annot a -> Reloc_annot (subst_annot s a)
| Reloc_const sc -> Reloc_const (subst_strcst s sc)
| Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
| Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 10a8da8813..90eeeb9be7 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -5,62 +5,71 @@ open Retroknowledge
open Environ
open CErrors
-let add_retroknowledge env action =
+type _ action_kind =
+ | IncompatTypes : _ prim_type -> Constant.t action_kind
+ | IncompatInd : _ prim_ind -> inductive action_kind
+
+type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
+
+let check_same_types typ c1 c2 =
+ if not (Constant.equal c1 c2)
+ then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
+
+let check_same_inds ind i1 i2 =
+ if not (eq_ind i1 i2)
+ then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
+
+let add_retroknowledge retro action =
match action with
- | Register_type(PT_int63,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_int63 with
- | None -> { retro with retro_int63 = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
- | Register_type(PT_float64,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_float64 with
- | None -> { retro with retro_float64 = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
- | Register_type(PT_array,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_array with
- | None -> { retro with retro_array = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
+ | Register_type(typ,c) ->
+ begin match typ with
+ | PT_int63 ->
+ (match retro.retro_int63 with
+ | None -> { retro with retro_int63 = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+
+ | PT_float64 ->
+ (match retro.retro_float64 with
+ | None -> { retro with retro_float64 = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+
+ | PT_array ->
+ (match retro.retro_array with
+ | None -> { retro with retro_array = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+ end
+
| Register_ind(pit,ind) ->
- let retro = env.retroknowledge in
- let retro =
- match pit with
+ begin match pit with
| PIT_bool ->
let r =
match retro.retro_bool with
| None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_bool = Some r }
| PIT_carry ->
let r =
match retro.retro_carry with
| None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_carry = Some r }
| PIT_pair ->
let r =
match retro.retro_pair with
| None -> (ind,1)
- | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in
+ | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_pair = Some r }
| PIT_cmp ->
let r =
match retro.retro_cmp with
| None -> ((ind,1), (ind,2), (ind,3))
- | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_cmp = Some r }
| PIT_f_cmp ->
let r =
match retro.retro_f_cmp with
| None -> ((ind,1), (ind,2), (ind,3), (ind,4))
- | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_f_cmp = Some r }
| PIT_f_class ->
let r =
@@ -69,10 +78,12 @@ let add_retroknowledge env action =
(ind,5), (ind,6), (ind,7), (ind,8),
(ind,9))
| Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
- assert (eq_ind ind ind'); t in
+ check_same_inds pit ind ind'; t in
{ retro with retro_f_class = Some r }
- in
- set_retroknowledge env retro
+ end
+
+let add_retroknowledge env action =
+ set_retroknowledge env (add_retroknowledge env.retroknowledge action)
let get_int_type env =
match env.retroknowledge.retro_int63 with
diff --git a/kernel/primred.mli b/kernel/primred.mli
index 1bfaffaa44..6e9d4e297e 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -2,6 +2,13 @@ open Names
open Environ
(** {5 Reduction of primitives} *)
+type _ action_kind =
+ | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind
+ | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind
+
+type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
+
+(** May raise [IncomtibleDeclarations] *)
val add_retroknowledge : env -> Retroknowledge.action -> env
val get_int_type : env -> Constant.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 04e7a81697..48567aa564 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
univs, typ
| Some (typ,Monomorphic_entry uctx) ->
- assert (AUContext.is_empty auctx);
+ assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *)
let env = push_context_set ~strict:true uctx env in
let u = Instance.empty in
let typ =
@@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
Monomorphic uctx, typ
| Some (typ,Polymorphic_entry (unames,uctx)) ->
- assert (not (AUContext.is_empty auctx));
- (* push_context will check that the universes aren't repeated in the instance
- so comparing the sizes works *)
- assert (AUContext.size auctx = UContext.size uctx);
- (* No polymorphic primitive uses constraints currently *)
- assert (Constraint.is_empty (UContext.constraints uctx));
+ assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *)
+ (* [push_context] will check that the universes aren't repeated in
+ the instance so comparing the sizes works. No polymorphic
+ primitive uses constraints currently. *)
+ if not (AUContext.size auctx = UContext.size uctx
+ && Constraint.is_empty (UContext.constraints uctx))
+ then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++
+ str (op_or_type_to_string p));
let env = push_context ~strict:false uctx env in
(* Now we know that uctx matches the auctx *)
let typ = (Typeops.infer_type env typ).utj_val in
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index ec429d5f9e..de604176cb 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
open Univ
-open Constr
(********************************************)
(* Initialization of the abstract machine ***)
@@ -61,8 +60,9 @@ type structured_constant =
type reloc_table = (tag * int) array
+(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *)
type annot_switch =
- {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+ { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
let rec eq_structured_values v1 v2 =
v1 == v2 ||
@@ -123,22 +123,16 @@ let hash_structured_constant c =
| Const_float f -> combinesmall 7 (Float64.hash f)
let eq_annot_switch asw1 asw2 =
- let eq_ci ci1 ci2 =
- eq_ind ci1.ci_ind ci2.ci_ind &&
- Int.equal ci1.ci_npar ci2.ci_npar &&
- CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
- in
let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
- eq_ci asw1.ci asw2.ci &&
CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
- (asw1.tailcall : bool) == asw2.tailcall
+ (asw1.tailcall : bool) == asw2.tailcall &&
+ Int.equal asw1.max_stack_size asw2.max_stack_size
let hash_annot_switch asw =
let open Hashset.Combine in
- let h1 = Constr.case_info_hash asw.ci in
- let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
- let h3 = if asw.tailcall then 1 else 0 in
- combine3 h1 h2 h3
+ let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+ let h2 = if asw.tailcall then 1 else 0 in
+ combine3 h1 h2 asw.max_stack_size
let pp_sort s =
let open Sorts in
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f4070a02a3..f6efd49cfc 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Constr
(** Values *)
@@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t
type reloc_table = (tag * int) array
type annot_switch =
- {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+ { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
val eq_structured_constant : structured_constant -> structured_constant -> bool
val hash_structured_constant : structured_constant -> int
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 854a5ff63d..e5fa9bada1 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -262,19 +262,14 @@ and nf_stk ?from:(from=0) env sigma c t stk =
nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk
| Zswitch sw :: stk ->
assert (from = 0) ;
- let ci = sw.sw_annot.Vmvalues.ci in
let ((mind,_ as ind), u), allargs = find_rectype_a env t in
- let iv = if Typeops.should_invert_case env ci then
- CaseInvert {univs=u; args=allargs}
- else NoInvert
- in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
let params,realargs = Util.Array.chop nparams allargs in
let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
- let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
+ let p, relevance = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env sigma ind mib mip u params p in
(* calcul des branches *)
@@ -286,6 +281,11 @@ and nf_stk ?from:(from=0) env sigma c t stk =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs c in
+ let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
+ let iv = if Typeops.should_invert_case env ci then
+ CaseInvert {univs=u; args=allargs}
+ else NoInvert
+ in
nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;
@@ -296,17 +296,17 @@ and nf_stk ?from:(from=0) env sigma c t stk =
and nf_predicate env sigma ind mip params v pT =
match kind (whd_allnolet env pT) with
| LetIn (name,b,t,pT) ->
- let body =
+ let body, rel =
nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
- mkLetIn (name,b,t,body)
+ mkLetIn (name,b,t,body), rel
| Prod (name,dom,codom) -> begin
match whd_val v with
| Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
- let body =
+ let body, rel =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
- mkLambda(name,dom,body)
+ mkLambda(name,dom,body), rel
| _ -> assert false
end
| _ ->
@@ -321,8 +321,10 @@ and nf_predicate env sigma ind mip params v pT =
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let r = Inductive.relevance_of_inductive env (fst ind) in
let name = make_annot name r in
- let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
- mkLambda(name,dom,body)
+ let env = push_rel (LocalAssum (name,dom)) env in
+ let body = nf_vtype env sigma vb in
+ let rel = Retyping.relevance_of_type env sigma (EConstr.of_constr body) in
+ mkLambda(name,dom,body), rel
| _ -> assert false
and nf_args env sigma vargs ?from:(f=0) t =
diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v
deleted file mode 100644
index f62f6109e1..0000000000
--- a/test-suite/arithmetic/primitive.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Section S.
- Variable A : Type.
- Fail Primitive int : let x := A in Set := #int63_type.
- Fail Primitive add := #int63_add.
-End S.
-
-(* [Primitive] should be forbidden in sections, otherwise its type after cooking
-will be incorrect:
-
-Check int.
-
-*)
diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v
new file mode 100644
index 0000000000..b2d02a0c49
--- /dev/null
+++ b/test-suite/success/primitive.v
@@ -0,0 +1,69 @@
+(* This file mostly tests for the error paths in declaring primitives.
+ Successes are tested in the various test-suite/primitive/* directories *)
+
+(* [Primitive] should be forbidden in sections, otherwise its type
+after cooking will be incorrect. *)
+Section S.
+ Variable A : Type.
+ Fail Primitive int : let x := A in Set := #int63_type.
+ Fail Primitive int := #int63_type. (* we fail even if section variable not used *)
+End S.
+Section S.
+ Fail Primitive int := #int63_type. (* we fail even if no section variables *)
+End S.
+
+(* can't declare primitives with nonsense types *)
+Fail Primitive xx : nat := #int63_type.
+
+(* non-cumulative conversion *)
+Fail Primitive xx : Type := #int63_type.
+
+(* check evars *)
+Fail Primitive xx : let x := _ in Set := #int63_type.
+
+(* explicit type is unified with expected type, not just converted
+
+ extra universes are OK for monomorphic primitives (even though
+ their usefulness is questionable, there's no difference compared
+ with predeclaring them)
+ *)
+Primitive xx : let x := Type in _ := #int63_type.
+
+(* double declaration *)
+Fail Primitive yy := #int63_type.
+
+Module DoubleCarry.
+ (* XXX maybe should be an output test: this is the case where the new
+ declaration is already in the nametab so can be nicely printed *)
+ Module M.
+ Variant carry (A : Type) :=
+ | C0 : A -> carry A
+ | C1 : A -> carry A.
+
+ Register carry as kernel.ind_carry.
+ End M.
+
+ Module N.
+ Variant carry (A : Type) :=
+ | C0 : A -> carry A
+ | C1 : A -> carry A.
+
+ Fail Register carry as kernel.ind_carry.
+ End N.
+End DoubleCarry.
+
+(* univ polymorphic primitives *)
+
+(* universe count must be as expected *)
+Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type.
+
+(* use a phantom universe to ensure we check conversion not just the universe count *)
+Fail Primitive array@{u} : Set -> Set := #array_type.
+
+(* no constraints allowed! *)
+Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type.
+
+(* unification works for polymorphic primitives too (although universe
+ counts mean it's not enough) *)
+Fail Primitive array : let x := Type in _ -> Type := #array_type.
+Primitive array : _ -> Type := #array_type.
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index d3e2749088..3a6dfb1e11 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -171,6 +171,10 @@ End sFix.
Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
+(* Check that VM/native properly keep the relevance of the predicate in the case info
+ (bad-relevance warning as error otherwise) *)
+Definition vm_rebuild_case := Eval vm_compute in eq_sind.
+
Require Import ssreflect.
Goal forall T : SProp, T -> True.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 7af09585d0..712cb6a135 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -15,6 +15,7 @@ Goal EQ nat 0 0.
Hint Unfold EQ.
auto.
Qed.
+End toto.
(* Check regular failure when statically existing ref does not exist
any longer at run time *)
@@ -23,4 +24,71 @@ Goal let x := 0 in True.
intro x.
Fail (clear x; unfold x).
Abort.
-End toto.
+
+(* Static analysis of unfold *)
+
+Module A.
+
+Opaque id.
+Ltac f := unfold id.
+Goal id 0 = 0.
+Fail f.
+Transparent id.
+f.
+Abort.
+
+End A.
+
+Module B.
+
+Module Type T. Axiom n : nat. End T.
+
+Module F(X:T).
+Ltac f := unfold X.n.
+End F.
+
+Module M. Definition n := 0. End M.
+Module N := F M.
+Goal match M.n with 0 => 0 | S _ => 1 end = 0.
+N.f.
+match goal with |- 0=0 => idtac end.
+Abort.
+
+End B.
+
+Module C.
+
+(* We reject inductive types and constructors *)
+
+Fail Ltac g := unfold nat.
+Fail Ltac g := unfold S.
+
+End C.
+
+Module D.
+
+(* In interactive mode, we delay the interpretation of short names *)
+
+Notation x := Nat.add.
+
+Goal let x := 0 in x = 0+0.
+unfold x.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let x := 0 in x = 0+0.
+intro; unfold x. (* dynamic binding (but is it really the most natural?) *)
+match goal with |- 0 = 0+0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+unfold fst.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+intro; unfold fst. (* dynamic binding *)
+match goal with |- 0 = Datatypes.fst (0,0) => idtac end.
+Abort.
+
+End D.
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index 110dcdc98a..eaa5271a73 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt =
Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
env evd typ
in
- let evd = Evarconv.unify_delay env evd typ expected_typ in
+ let evd = try Evarconv.unify_delay env evd typ expected_typ
+ with Evarconv.UnableToUnify (evd,e) as exn ->
+ let _, info = Exninfo.capture exn in
+ Exninfo.iraise (Pretype_errors.(
+ PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info))
+ in
+ Pretyping.check_evars_are_solved ~program_mode:false env evd;
let evd = Evd.minimize_universes evd in
let uvars = EConstr.universes_of_constr evd typ in
let evd = Evd.restrict_universe_context evd uvars in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f9ecf10d1b..762c95fffe 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1252,6 +1252,29 @@ let explain_inductive_error = function
error_large_non_prop_inductive_not_in_type ()
| MissingConstraints csts -> error_inductive_missing_constraints csts
+(* Primitive errors *)
+
+let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) =
+ let open Primred in
+ let env = Global.env() in
+ (* The newer constant/inductive (either coming from Primitive or a
+ Require) may be absent from the nametab as the error got raised
+ while adding it to the safe_env. In that case we can't use
+ nametab printing.
+
+ There are still cases where the constant/inductive is added
+ separately from its retroknowledge (using Register), so we still
+ try nametab based printing. *)
+ match act with
+ | IncompatTypes typ ->
+ let px = try pr_constant env x with Not_found -> Constant.print x in
+ str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_type_to_string typ) ++
+ str ": " ++ pr_constant env y ++ str " is already declared."
+ | IncompatInd ind ->
+ let px = try pr_inductive env x with Not_found -> MutInd.print (fst x) in
+ str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_ind_to_string ind) ++
+ str ": " ++ pr_inductive env y ++ str " is already declared."
+
(* Recursion schemes errors *)
let explain_recursion_scheme_error env = function
@@ -1386,6 +1409,8 @@ let rec vernac_interp_error_handler = function
explain_typeclass_error env sigma te
| InductiveError e ->
explain_inductive_error e
+ | Primred.IncompatibleDeclarations (act,x,y) ->
+ explain_incompatible_prim_declarations act x y
| Modops.ModuleTypingError e ->
explain_module_error e
| Modintern.ModuleInternalizationError e ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 20:30:51 +0000