aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/closure.ml11
-rw-r--r--checker/closure.mli4
-rw-r--r--checker/declarations.ml13
-rw-r--r--checker/environ.ml4
-rw-r--r--checker/environ.mli2
-rw-r--r--checker/print.ml2
-rw-r--r--checker/reduction.ml6
-rw-r--r--checker/term.ml2
-rw-r--r--checker/values.ml11
-rw-r--r--test-suite/coqchk/primproj.v2
11 files changed, 34 insertions, 25 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index e875e40f0..d75af7654 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
| Case of case_info * constr * constr * constr array
| Fix of constr pfixpoint
| CoFix of constr pcofixpoint
- | Proj of constant * constr
+ | Proj of projection * constr
type existential = constr pexistential
type rec_declaration = constr prec_declaration
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683fa..c6cc2185d 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * constant
+ | Zproj of int * int * projection
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
let (depth, args, s) = strip_update_shift_app m s in
(** Try to drop the params, might fail on partially applied constructors. *)
let argss = try_drop_parameters depth pars args in
- let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
- term = FProj (p, right) }) projs in
+ let hstack =
+ Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+ term = FProj (Projection.make p false, right) }) projs in
argss, [Zapp hstack]
| _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
@@ -738,7 +739,7 @@ let rec knh info m stk =
| FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
- if red_set info.i_flags (fCONST p) then
+ if red_set info.i_flags (fCONST (Projection.constant p)) then
(let pb = lookup_projection p (info.i_env) in
knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
:: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250d..376e9fef7 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * constant
+ | Zproj of int * int * projection
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475f..36e6a7cab 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
let func = map_kn f f' in
match c with
| Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
- | Proj (kn,t) ->
- let kn' =
- try fst (f' kn Univ.Instance.empty)
- with No_subst -> kn
+ | Proj (p,t) ->
+ let p' =
+ Projection.map (fun kn ->
+ try fst (f' kn Univ.Instance.empty)
+ with No_subst -> kn) p
in
let t' = func t in
- if kn' == kn && t' == t then c
- else Proj (kn', t')
+ if p' == p && t' == t then c
+ else Proj (p', t')
| Ind ((kn,i),u) ->
let kn' = f kn in
if kn'==kn then c else Ind ((kn',i),u)
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc712..c0f366000 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -147,8 +147,8 @@ let evaluable_constant cst env =
let is_projection cst env =
not (Option.is_empty (lookup_constant cst env).const_proj)
-let lookup_projection cst env =
- match (lookup_constant cst env).const_proj with
+let lookup_projection p env =
+ match (lookup_constant (Projection.constant p) env).const_proj with
| Some pb -> pb
| None -> anomaly ("lookup_projection: constant is not a projection")
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b127..22fe7d8f1 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -51,7 +51,7 @@ val constant_value : env -> constant puniverses -> constr
val evaluable_constant : constant -> env -> bool
val is_projection : constant -> env -> bool
-val lookup_projection : constant -> env -> projection_body
+val lookup_projection : projection -> env -> projection_body
(* Inductives *)
val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff77..7624fd325 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
done
in print_string"{"; print_fix (); print_string"}"
| Proj (p, c) ->
- print_string "Proj("; sp_con_display p; print_string ",";
+ print_string "Proj("; sp_con_display (Projection.constant p); print_string ",";
box_display c; print_string ")"
and box_display c = open_hovbox 1; term_display c; close_box()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28fdb130e..58f0f894f 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of Names.constant * lift
+ | Zlproj of Names.projection * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (Names.eq_con_chk c1 c2) then
+ if not (Names.eq_con_chk
+ (Names.Projection.constant c1)
+ (Names.Projection.constant c2)) then
raise NotConvertible
| (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
diff --git a/checker/term.ml b/checker/term.ml
index 93540276b..430be4951 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
- | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+ | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
| _ -> false
let rec eq_constr m n =
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d..46b66adc4 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
*)
@@ -126,6 +126,7 @@ let v_caseinfo =
v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
let rec v_constr =
Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
[|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
[|v_fix|]; (* Fix *)
[|v_cofix|]; (* CoFix *)
- [|v_cst;v_constr|] (* Proj *)
+ [|v_proj;v_constr|] (* Proj *)
|])
and v_prec = Tuple ("prec_declaration",
@@ -205,8 +206,10 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_projbody =
- v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
- v_constr|]
+ v_tuple "projection_body"
+ [|v_cst;Int;Int;v_constr;
+ v_tuple "proj_eta" [|v_constr;v_constr|];
+ v_constr|]
let v_cb = v_tuple "constant_body"
[|v_section_ctxt;
diff --git a/test-suite/coqchk/primproj.v b/test-suite/coqchk/primproj.v
new file mode 100644
index 000000000..04d0a2b6f
--- /dev/null
+++ b/test-suite/coqchk/primproj.v
@@ -0,0 +1,2 @@
+Set Primitive Projections.
+Record foo (T : Type) := { bar : T}.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 15:18:50 +0000