aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES9
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_instruct.h1
-rw-r--r--kernel/byterun/coq_interp.c28
-rw-r--r--kernel/byterun/coq_values.h9
-rw-r--r--kernel/cbytecodes.ml6
-rw-r--r--kernel/cbytecodes.mli3
-rw-r--r--kernel/cbytegen.ml14
-rw-r--r--kernel/cemitcodes.ml1
-rw-r--r--kernel/csymtable.ml7
-rw-r--r--kernel/declarations.mli6
-rw-r--r--kernel/nativeconv.ml22
-rw-r--r--kernel/term_typing.ml20
-rw-r--r--kernel/vconv.ml17
-rw-r--r--kernel/vm.ml22
-rw-r--r--kernel/vm.mli1
-rw-r--r--pretyping/inductiveops.ml9
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/pretyping.mllib2
-rw-r--r--pretyping/retyping.ml9
-rw-r--r--pretyping/vnorm.ml4
-rw-r--r--test-suite/bugs/closed/4203.v19
-rw-r--r--tools/coqdep.ml37
-rw-r--r--tools/coqdep_common.ml68
-rw-r--r--tools/coqdep_common.mli2
-rw-r--r--tools/coqdep_lexer.mli2
-rw-r--r--tools/coqdep_lexer.mll11
27 files changed, 231 insertions, 102 deletions
diff --git a/CHANGES b/CHANGES
index 9172195960..050d3e999f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,10 +163,11 @@ Specification Language
- Constructors in pattern-matching patterns now respect the same rules
regarding implicit arguments than in applicative position. The old
behavior can be recovered by the command "Set Asymmetric
- Patterns". As a side effect, Much more notations can be used in
- patterns. Considering that the pattern language is rich enough like
- that, definitions are now always forbidden in patterns. (source of
- incompatibilities for definitions that delta-reduce to a constructor)
+ Patterns". As a side effect, notations for constructors explicitly
+ mentioning non-implicit parameters can now be used in patterns.
+ Considering that the pattern language is already rich enough, binding
+ local definitions is however now forbidden in patterns (source of
+ incompatibilities for local definitions that delta-reduce to a constructor).
- Type inference algorithm now granting opacity of constants. This might also
affect behavior of tactics (source of incompatibilities, solvable by
re-declaring transparent constants which were set opaque).
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e65113..29e33d349b 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
arity[BRANCH]=arity[ISCONST]= 1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[ARECONST]=2;
+ arity[ARECONST]=arity[PROJ]=2;
/* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077e2..8c5ab0ecbd 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
SWITCH, PUSHFIELDS,
GETFIELD0, GETFIELD1, GETFIELD,
SETFIELD0, SETFIELD1, SETFIELD,
+ PROJ,
CONST0, CONST1, CONST2, CONST3, CONSTINT,
PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ddbde9d385..0a121dc32e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -878,8 +878,32 @@ value coq_interprete
caml_modify(&Field(accu, *pc),*sp);
sp++; pc++;
Next;
- }
-
+ }
+
+
+ Instruct(PROJ){
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
+ /* Skip over the index of projected field */
+ pc++;
+ /* Save the argument on the stack */
+ *--sp = accu;
+ /* Create atom */
+ Alloc_small(accu, 2, ATOM_PROJ_TAG);
+ Field(accu, 0) = Field(coq_global_data, *pc);
+ Field(accu, 1) = sp[0];
+ sp[0] = accu;
+ /* Create accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = *sp++;
+ } else {
+ accu = Field(accu, *pc++);
+ }
+ pc++;
+ Next;
+ }
+
/* Integer constants */
Instruct(CONST0){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2c0..1590a2141d 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -22,10 +22,11 @@
#define ATOM_ID_TAG 0
#define ATOM_IDDEF_TAG 1
#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 93fd61f02a..3271ac1458 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -31,6 +31,7 @@ let last_variant_tag = 245
type structured_constant =
| Const_sorts of sorts
| Const_ind of pinductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -81,6 +82,8 @@ type instruction =
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (* index of the projected argument,
+ name of projection *)
(* spiwack: instructions concerning integers *)
| Kbranch of Label.t (* jump to label *)
| Kaddint31 (* adds the int31 in the accu
@@ -167,6 +170,7 @@ let pp_sort s =
let rec pp_struct_const = function
| Const_sorts s -> pp_sort s
| Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+ | Const_proj p -> Constant.print p
| Const_b0 i -> int i
| Const_bn (i,t) ->
int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
@@ -228,6 +232,8 @@ let rec pp_instr i =
| Kbranch lbl -> str "branch " ++ pp_lbl lbl
+ | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+
| Kaddint31 -> str "addint31"
| Kaddcint31 -> str "addcint31"
| Kaddcarrycint31 -> str "addcarrycint31"
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index d9998c89e8..745ef311b0 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -25,6 +25,7 @@ val last_variant_tag : tag
type structured_constant =
| Const_sorts of sorts
| Const_ind of pinductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
@@ -72,6 +73,8 @@ type instruction =
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (** index of the projected argument,
+ name of projection *)
(** spiwack: instructions concerning integers *)
| Kbranch of Label.t (** jump to label, is it needed ? *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index ac46dc5833..d5435f0c37 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -540,14 +540,12 @@ let rec compile_constr reloc c sz cont =
match kind_of_term c with
| Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
| Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
- | Proj (p,c) ->
- (* compile_const reloc p [|c|] sz cont *)
- let kn = Projection.constant p in
- let cb = lookup_constant kn !global_env in
- (* TODO: better representation of projections *)
- let pb = Option.get cb.const_proj in
- let args = Array.make pb.proj_npars mkProp in
- compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+ | Proj (p,c) ->
+ let kn = Projection.constant p in
+ let cb = lookup_constant kn !global_env in
+ let pb = Option.get cb.const_proj in
+ let n = pb.proj_arg in
+ compile_constr reloc c sz (Kproj (n,kn) :: cont)
| Cast(c,_,_) -> compile_constr reloc c sz cont
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d3c..0d9334a50c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -225,6 +225,7 @@ let emit_instr = function
if n <= 1 then out (opSETFIELD0+n)
else (out opSETFIELD;out_int n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+ | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
(* spiwack *)
| Kbranch lbl -> out opBRANCH; out_label lbl
| Kaddint31 -> out opADDINT31
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 49ab68beae..8fd90ec364 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -60,6 +60,8 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts _, _ -> false
| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_b0 _, _ -> false
| Const_bn (t1, a1), Const_bn (t2, a2) ->
@@ -71,11 +73,12 @@ let rec hash_structured_constant c =
match c with
| Const_sorts s -> combinesmall 1 (Sorts.hash s)
| Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
- | Const_b0 t -> combinesmall 3 (Int.hash t)
+ | Const_proj p -> combinesmall 3 (Constant.hash p)
+ | Const_b0 t -> combinesmall 4 (Int.hash t)
| Const_bn (t, a) ->
let fold h c = combine h (hash_structured_constant c) in
let h = Array.fold_left fold 0 a in
- combinesmall 4 (combine (Int.hash t) h)
+ combinesmall 5 (combine (Int.hash t) h)
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3f0..c1c19a757c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -142,12 +142,10 @@ type one_inductive_body = {
mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
mind_consnrealargs : int array;
- (** Number of expected proper arguments of the constructors (w/o params)
- (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
- (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 1f8bfc984f..d0aa96fd15 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -20,11 +20,15 @@ let rec conv_val env pb lvl cu v1 v2 =
if v1 == v2 then ()
else
match kind_of_value v1, kind_of_value v2 with
- | Vaccu k1, Vaccu k2 ->
- conv_accu env pb lvl cu k1 k2
| Vfun f1, Vfun f2 ->
let v = mk_rel_accu lvl in
conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+ | Vfun f1, _ ->
+ conv_val env CONV lvl cu v1 (fun x -> v2 x)
+ | _, Vfun f2 ->
+ conv_val env CONV lvl cu (fun x -> v1 x) v2
+ | Vaccu k1, Vaccu k2 ->
+ conv_accu env pb lvl cu k1 k2
| Vconst i1, Vconst i2 ->
if not (Int.equal i1 i2) then raise NotConvertible
| Vblock b1, Vblock b2 ->
@@ -40,11 +44,7 @@ let rec conv_val env pb lvl cu v1 v2 =
aux lvl max b1 b2 (i+1) cu)
in
aux lvl (n1-1) b1 b2 0 cu
- | Vfun f1, _ ->
- conv_val env CONV lvl cu v1 (fun x -> v2 x)
- | _, Vfun f2 ->
- conv_val env CONV lvl cu (fun x -> v1 x) v2
- | _, _ -> raise NotConvertible
+ | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
and conv_accu env pb lvl cu k1 k2 =
let n1 = accu_nargs k1 in
@@ -60,6 +60,7 @@ and conv_atom env pb lvl a1 a2 cu =
if a1 == a2 then ()
else
match a1, a2 with
+ | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
| Arel i1, Arel i2 ->
if not (Int.equal i1 i2) then raise NotConvertible
| Aind ind1, Aind ind2 ->
@@ -104,7 +105,12 @@ and conv_atom env pb lvl a1 a2 cu =
conv_val env CONV lvl cu d1 d2;
let v = mk_rel_accu lvl in
conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
- | _, _ -> raise NotConvertible
+ | Aproj(p1,ac1), Aproj(p2,ac2) ->
+ if not (Constant.equal p1 p2) then raise NotConvertible
+ else conv_accu env CONV lvl cu ac1 ac2
+ | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+ | Aproj _, _ -> raise NotConvertible
(* Precondition length t1 = length f1 = length f2 = length t2 *)
and conv_fix env lvl t1 f1 t2 f2 cu =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492b..83e566041f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
match proj with
| None -> compile_constant_body env def
| Some pb ->
- compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+ (* The compilation of primitive projections is a bit tricky, because
+ they refer to themselves (the body of p looks like fun c =>
+ Proj(p,c)). We break the cycle by building an ad-hoc compilation
+ environment. A cleaner solution would be that kernel projections are
+ simply Proj(i,c) with i an int and c a constr, but we would have to
+ get rid of the compatibility layer. *)
+ let cb =
+ { const_hyps = hyps;
+ const_body = def;
+ const_type = typ;
+ const_proj = proj;
+ const_body_code = None;
+ const_polymorphic = poly;
+ const_universes = univs;
+ const_inline_code = inline_code }
+ in
+ let env = add_constant kn cb env in
+ compile_constant_body env def
in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
@@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
const_universes = univs;
const_inline_code = inline_code }
-
(*s Global and local constant declaration. *)
let translate_constant env kn ce =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc0414..a03a67db8b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
match z1, z2 with
| Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
| Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2)
- | Zswitch _, Zswitch _ -> true
- | _ , _ -> false
+ | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+ | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
let rec compare_stack stk1 stk2 =
match stk1, stk2 with
@@ -81,7 +81,10 @@ and conv_whd env pb k whd1 whd2 cu =
conv_whd env pb k whd1 (force_whd v stk) cu
| Vatom_stk(Aiddef(_,v),stk), _ ->
conv_whd env pb k (force_whd v stk) whd2 cu
- | _, _ -> raise NotConvertible
+
+ | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
+ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
and conv_atom env pb k a1 stk1 a2 stk2 cu =
match a1, a2 with
@@ -110,7 +113,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
| _, Aiddef(ik2,v2) ->
conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
- | _, _ -> raise NotConvertible
+ | Aind _, _ | Aid _, _ -> raise NotConvertible
and conv_stack env k stk1 stk2 cu =
match stk1, stk2 with
@@ -131,7 +134,11 @@ and conv_stack env k stk1 stk2 cu =
done;
conv_stack env k stk1 stk2 !rcu
else raise NotConvertible
- | _, _ -> raise NotConvertible
+ | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+ if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+ else raise NotConvertible
+ | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+ | Zproj _ :: _, _ -> raise NotConvertible
and conv_fun env pb k f1 f2 cu =
if f1 == f2 then cu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b39..a822f92eb3 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -127,10 +127,11 @@ type vswitch = {
(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *)
-(* -- 3_[accu|fix_app] : a fixpoint blocked by an accu *)
-(* -- 4_[accu|vswitch] : a match blocked by an accu *)
-(* -- 5_[fcofix] : a cofix function *)
-(* -- 6_[fcofix|val] : a cofix function, val represent the value *)
+(* -- 3_[accu|proj name] : a projection blocked by an accu *)
+(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *)
+(* -- 5_[accu|vswitch] : a match blocked by an accu *)
+(* -- 6_[fcofix] : a cofix function *)
+(* -- 7_[fcofix|val] : a cofix function, val represent the value *)
(* of the function applied to arg1 ... argn *)
(* The [arguments] type, which is abstracted as an array, represents : *)
(* tag[ _ | _ |v1|... | vn] *)
@@ -149,6 +150,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix*arguments (* Possibly empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list
@@ -176,15 +178,18 @@ let rec whd_accu a stk =
match Obj.tag at with
| i when i <= 2 ->
Vatom_stk(Obj.magic at, stk)
- | 3 (* fix_app tag *) ->
+ | 3 (* proj tag *) ->
+ let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+ whd_accu (Obj.field at 1) (zproj :: stk)
+ | 4 (* fix_app tag *) ->
let fa = Obj.field at 1 in
let zfix =
Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
whd_accu (Obj.field at 0) (zfix :: stk)
- | 4 (* switch tag *) ->
+ | 5 (* switch tag *) ->
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
whd_accu (Obj.field at 0) (zswitch :: stk)
- | 5 (* cofix_tag *) ->
+ | 6 (* cofix_tag *) ->
let vcfx = Obj.obj (Obj.field at 0) in
let to_up = Obj.obj a in
begin match stk with
@@ -192,7 +197,7 @@ let rec whd_accu a stk =
| [Zapp args] -> Vcofix(vcfx, to_up, Some args)
| _ -> assert false
end
- | 6 (* cofix_evaluated_tag *) ->
+ | 7 (* cofix_evaluated_tag *) ->
let vcofix = Obj.obj (Obj.field at 0) in
let res = Obj.obj a in
begin match stk with
@@ -289,6 +294,7 @@ let rec obj_of_str_const str =
match str with
| Const_sorts s -> Obj.repr (Vsort s)
| Const_ind ind -> obj_of_atom (Aind ind)
+ | Const_proj p -> Obj.repr p
| Const_b0 tag -> Obj.repr tag
| Const_bn(tag, args) ->
let len = Array.length args in
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5190356828..d31448ee13 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -34,6 +34,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix * arguments (** might be empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d480..90aa8000a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -584,6 +584,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
env evdref scl ar.template_level (ctx,ar.template_param_levels) in
!evdref, mkArity (List.rev ctx,scl)
+let type_of_projection_knowing_arg env sigma p c ty =
+ let IndType(pars,realargs) =
+ try find_rectype env sigma ty
+ with Not_found ->
+ raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
+ in
+ let (_,u), pars = dest_ind_family pars in
+ substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+
(***********************************************)
(* Guard condition *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a3f..757599a3ce 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,6 +126,8 @@ val allowed_sorts : env -> inductive -> sorts_family list
(** Primitive projections *)
val projection_nparams : projection -> int
val projection_nparams_env : env -> projection -> int
+val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
+ constr -> types -> types
(** Extract information from an inductive family *)
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 436f61d7b6..b59589bda2 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,7 +1,7 @@
Locusops
Reductionops
-Vnorm
Inductiveops
+Vnorm
Arguments_renaming
Nativenorm
Retyping
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a56861c683..743bc3b19b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -127,13 +127,8 @@ let retype ?(polyprop=true) sigma =
strip_outer_cast
(subst_type env sigma (type_of env f) (Array.to_list args))
| Proj (p,c) ->
- let Inductiveops.IndType(pars,realargs) =
- let ty = type_of env c in
- try Inductiveops.find_rectype env sigma ty
- with Not_found -> retype_error BadRecursiveType
- in
- let (_,u), pars = dest_ind_family pars in
- substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+ let ty = type_of env c in
+ Inductiveops.type_of_projection_knowing_arg env sigma p c ty
| Cast (c,_, t) -> t
| Sort _ | Prod _ -> mkSort (sort_of env cstr)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8198db1b8a..af640d7f34 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -216,6 +216,10 @@ and nf_stk env c t stk =
let tcase = build_case_type dep p realargs c in
let ci = case_info sw in
nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+ | Zproj p :: stk ->
+ let p' = Projection.make p true in
+ let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
+ nf_stk env (mkProj(p',c)) ty stk
and nf_predicate env ind mip params v pT =
match whd_val v, kind_of_term pT with
diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v
new file mode 100644
index 0000000000..076a3c3d68
--- /dev/null
+++ b/test-suite/bugs/closed/4203.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record ops {T:Type} := { is_ok : T -> Prop; constant : T }.
+Arguments ops : clear implicits.
+
+Record ops_ok {T} (Ops:ops T) := { constant_ok : is_ok Ops (constant Ops) }.
+
+Definition nat_ops : ops nat := {| is_ok := fun n => n = 1; constant := 1 |}.
+Definition nat_ops_ok : ops_ok nat_ops.
+Proof.
+ split. cbn. apply eq_refl.
+Qed.
+
+Definition t := Eval lazy in constant_ok nat_ops nat_ops_ok.
+Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok.
+Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok.
+
+Check (eq_refl t : t = t').
+Check (eq_refl t : t = t''). \ No newline at end of file
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f1a3131dd8..397ccd8a25 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -56,11 +56,12 @@ let sort () =
try
while true do
match coq_action lb with
- | Require sl ->
+ | Require (from, sl) ->
List.iter
(fun s ->
- try loop (Hashtbl.find vKnown s)
- with Not_found -> ())
+ match search_v_known ?from s with
+ | None -> ()
+ | Some f -> loop f)
sl
| _ -> ()
done
@@ -299,16 +300,15 @@ module DAG = DAG(struct type t = string let compare = compare end)
(** TODO: we should share this code with Coqdep_common *)
let treat_coq_file chan =
let buf = Lexing.from_channel chan in
- let deja_vu_v = ref ([]: string list list)
+ let deja_vu_v = ref ([]: (string list option * string list) list)
and deja_vu_ml = ref ([] : string list) in
- let mark_v_done acc str =
- let seen = List.mem str !deja_vu_v in
+ let mark_v_done from acc str =
+ let seen = List.mem (from, str) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v str in
- try
- let file_str = Hashtbl.find vKnown str in
- (canonize file_str, !suffixe) :: acc
- with Not_found -> acc
+ let () = addQueue deja_vu_v (from, str) in
+ match search_v_known ?from str with
+ | None -> acc
+ | Some file_str -> (canonize file_str, !suffixe) :: acc
else acc
in
let rec loop acc =
@@ -317,8 +317,8 @@ let treat_coq_file chan =
| None -> acc
| Some action ->
let acc = match action with
- | Require strl ->
- List.fold_left mark_v_done acc strl
+ | Require (from, strl) ->
+ List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
| Declare sl ->
let declare suff dir s =
let base = file_name s dir in
@@ -340,13 +340,12 @@ let treat_coq_file chan =
List.fold_left decl acc sl
| Load str ->
let str = Filename.basename str in
- let seen = List.mem [str] !deja_vu_v in
+ let seen = List.mem (None, [str]) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v [str] in
- try
- let file_str = Hashtbl.find vKnown [str] in
- (canonize file_str, ".v") :: acc
- with Not_found -> acc
+ let () = addQueue deja_vu_v (None, [str]) in
+ match search_v_known [str] with
+ | None -> acc
+ | Some file_str -> (canonize file_str, ".v") :: acc
else acc
| AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 38e454aefb..879da6c588 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -72,9 +72,9 @@ let vAccu = ref ([] : (string * string) list)
let addQueue q v = q := v :: !q
-let safe_hash_add cmp clq q (k,v) =
+let safe_hash_add cmp clq q (k, (v, b)) =
try
- let v2 = Hashtbl.find q k in
+ let (v2, _) = Hashtbl.find q k in
if not (cmp v v2) then
let rec add_clash = function
(k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
@@ -82,8 +82,8 @@ let safe_hash_add cmp clq q (k,v) =
| [] -> [(k,[v;v2])] in
clq := add_clash !clq;
(* overwrite previous bindings, as coqc does *)
- Hashtbl.add q k v
- with Not_found -> Hashtbl.add q k v
+ Hashtbl.add q k (v, b)
+ with Not_found -> Hashtbl.add q k (v, b)
(** Files found in the loadpaths.
For the ML files, the string is the basename without extension.
@@ -112,9 +112,37 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
let add_mllib_known, _, search_mllib_known = mkknown ()
let add_mlpack_known, _, search_mlpack_known = mkknown ()
-let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
+let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
+(** The associated boolean is true if this is a root path. *)
let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
+let get_prefix p l =
+ let rec drop_prefix_rec = function
+ | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl)
+ | ([], tl) -> Some tl
+ | _ -> None
+ in
+ drop_prefix_rec (p, l)
+
+exception Found of string
+
+let search_v_known ?from s = match from with
+| None -> fst (Hashtbl.find vKnown s)
+| Some from ->
+ let iter logpath (phys_dir, root) =
+ if root then match get_prefix from logpath with
+ | None -> ()
+ | Some rem ->
+ match get_prefix (List.rev s) (List.rev rem) with
+ | None -> ()
+ | Some _ -> raise (Found phys_dir)
+ in
+ try Hashtbl.iter iter vKnown; raise Not_found
+ with Found s -> s
+
+let search_v_known ?from s =
+ try Some (search_v_known ?from s) with Not_found -> None
+
let clash_v = ref ([]: (string list * string list) list)
let error_cannot_parse s (i,j) =
@@ -153,9 +181,11 @@ let warning_cannot_open_dir dir =
eprintf "*** Warning: cannot open %s\n" dir;
flush stderr
-let safe_assoc verbose file k =
+let safe_assoc from verbose file k =
if verbose && List.mem_assoc k !clash_v then warning_clash file k;
- Hashtbl.find vKnown k
+ match search_v_known ?from k with
+ | None -> raise Not_found
+ | Some path -> path
let absolute_dir dir =
let current = Sys.getcwd () in
@@ -299,18 +329,18 @@ let rec traite_fichier_Coq suffixe verbose f =
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
- let deja_vu_v = ref ([]: string list list)
+ let deja_vu_v = ref ([]: (string list option * string list) list)
and deja_vu_ml = ref ([] : string list) in
try
while true do
let tok = coq_action buf in
match tok with
- | Require strl ->
+ | Require (from, strl) ->
List.iter (fun str ->
- if not (List.mem str !deja_vu_v) then begin
- addQueue deja_vu_v str;
+ if not (List.mem (from, str) !deja_vu_v) then begin
+ addQueue deja_vu_v (from, str);
try
- let file_str = safe_assoc verbose f str in
+ let file_str = safe_assoc from verbose f str in
printf " %s%s" (canonize file_str) suffixe
with Not_found ->
if verbose && not (Hashtbl.mem coqlibKnown str) then
@@ -339,10 +369,10 @@ let rec traite_fichier_Coq suffixe verbose f =
in List.iter decl sl
| Load str ->
let str = Filename.basename str in
- if not (List.mem [str] !deja_vu_v) then begin
- addQueue deja_vu_v [str];
+ if not (List.mem (None, [str]) !deja_vu_v) then begin
+ addQueue deja_vu_v (None, [str]);
try
- let file_str = Hashtbl.find vKnown [str] in
+ let (file_str, _) = Hashtbl.find vKnown [str] in
let canon = canonize file_str in
printf " %s.v" canon;
traite_fichier_Coq suffixe true (canon ^ ".v")
@@ -431,9 +461,11 @@ let add_known recur phys_dir log_dir f =
| (basename,".v") ->
let name = log_dir@[basename] in
let file = phys_dir//basename in
- let paths = if recur then suffixes name else [name] in
- List.iter
- (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+ let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+ if recur then
+ let paths = List.tl (suffixes name) in
+ let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
+ List.iter iter paths
| (basename,".vo") when not(!option_boot) ->
let name = log_dir@[basename] in
let paths = if recur then suffixes name else [name] in
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 3ac602183f..dcd69ebdb7 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -29,7 +29,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit
val search_mli_known : string -> dir option
val add_mllib_known : string -> dir -> string -> unit
val search_mllib_known : string -> dir option
-val vKnown : (string list, string) Hashtbl.t
+val search_v_known : ?from:string list -> string list -> string option
val coqlibKnown : (string list, unit) Hashtbl.t
val file_name : string -> string option -> string
val escape : string -> string
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index c7b9c9a0a8..84c9ba798b 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -11,7 +11,7 @@ type mL_token = Use_module of string
type qualid = string list
type coq_token =
- Require of qualid list
+ Require of qualid option * qualid list
| Declare of string list
| Load of string
| AddLoadPath of string
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 5692e5b45f..291bc55fbe 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -16,7 +16,7 @@
type qualid = string list
type coq_token =
- | Require of qualid list
+ | Require of qualid option * qualid list
| Declare of string list
| Load of string
| AddLoadPath of string
@@ -270,12 +270,9 @@ and require_file = parse
module_names := [coq_qual_id_tail lexbuf];
let qid = coq_qual_id_list lexbuf in
parse_dot lexbuf;
- match !from_pre_ident with
- None ->
- Require qid
- | Some from ->
- (from_pre_ident := None ;
- Require (List.map (fun x -> from @ x) qid)) }
+ let from = !from_pre_ident in
+ from_pre_ident := None;
+ Require (from, qid) }
| eof
{ syntax_error lexbuf }
| _
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:53:43 +0000