aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-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/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
18 files changed, 117 insertions, 40 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e6511..29e33d349 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 9cbf4077e..8c5ab0ecb 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 ddbde9d38..0a121dc32 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 1bf493e2c..1590a2141 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 93fd61f02..3271ac145 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 d9998c89e..745ef311b 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 ac46dc583..d5435f0c3 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 2535a64d3..0d9334a50 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 49ab68bea..8fd90ec36 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/term_typing.ml b/kernel/term_typing.ml
index a316b4492..83e566041 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 1c31cc041..a03a67db8 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 d4bf461b3..a822f92eb 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 519035682..d31448ee1 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 dfdc24d48..90aa8000a 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 7959759a3..757599a3c 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 25d17c7c9..a644e3d10 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -3,8 +3,8 @@ Termops
Namegen
Evd
Reductionops
-Vnorm
Inductiveops
+Vnorm
Arguments_renaming
Nativenorm
Retyping
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a56861c68..743bc3b19 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 8198db1b8..af640d7f3 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 01:21:11 +0000