aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c4
-rw-r--r--kernel/byterun/coq_interp.c4
-rw-r--r--kernel/cbytecodes.ml3
-rw-r--r--kernel/cbytecodes.mli1
-rw-r--r--kernel/cbytegen.ml130
-rw-r--r--kernel/cbytegen.mli8
-rw-r--r--kernel/cemitcodes.ml89
-rw-r--r--kernel/csymtable.ml23
-rw-r--r--kernel/declarations.mli6
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/indtypes.ml10
-rw-r--r--kernel/mod_typing.ml2
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/nativelambda.ml9
-rw-r--r--kernel/term_typing.ml12
-rw-r--r--kernel/vconv.ml3
-rw-r--r--kernel/vm.ml18
-rw-r--r--kernel/vm.mli2
20 files changed, 211 insertions, 121 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 52dc49bf8e..1be3e65113 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) {
uint32_t i, sizes, const_size, block_size;
COPY32(q,p); p++;
sizes=*q++;
- const_size = sizes & 0xFFFF;
- block_size = sizes >> 16;
+ const_size = sizes & 0xFFFFFF;
+ block_size = sizes >> 24;
sizes = const_size + block_size;
for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
} else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d74affdea9..0ab9f89ffa 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -791,12 +791,12 @@ value coq_interprete
Instruct(SWITCH) {
uint32_t sizes = *pc++;
print_instr("SWITCH");
- print_int(sizes & 0xFFFF);
+ print_int(sizes & 0xFFFFFF);
if (Is_block(accu)) {
long index = Tag_val(accu);
print_instr("block");
print_int(index);
- pc += pc[(sizes & 0xFFFF) + index];
+ pc += pc[(sizes & 0xFFFFFF) + index];
} else {
long index = Long_val(accu);
print_instr("constant");
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ae679027d6..700de50200 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,6 +24,9 @@ let fix_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6
+(* It could be greate if OCaml export this value,
+ So fixme if this occur in a new version of OCaml *)
+let last_variant_tag = 245
type structured_constant =
| Const_sorts of sorts
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index b65268f722..fbb40ffd1f 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -20,6 +20,7 @@ val fix_tag : tag
val switch_tag : tag
val cofix_tag : tag
val cofix_evaluated_tag : tag
+val last_variant_tag : tag
type structured_constant =
| Const_sorts of sorts
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 3b0c93b322..07fab06a42 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -329,13 +329,50 @@ let init_fun_code () = fun_code := []
(* Compilation of constructors and inductive types *)
+
+(* Limitation due to OCaml's representation of non-constant
+ constructors: limited to 245 + 1 (0 tag) cases. *)
+
+exception TooLargeInductive of Id.t
+
+let max_nb_const = 0x1000000
+let max_nb_block = 0x1000000 + last_variant_tag - 1
+
+let str_max_constructors =
+ Format.sprintf
+ " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
+
+let check_compilable ib =
+
+ if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then
+ raise (TooLargeInductive ib.mind_typename)
+
+(* Inv: arity > 0 *)
+
+let const_bn tag args =
+ if tag < last_variant_tag then Const_bn(tag, args)
+ else
+ Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
+
+
+let code_makeblock arity tag cont =
+ if tag < last_variant_tag then
+ Kmakeblock(arity, tag) :: cont
+ else
+ Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) ::
+ Kmakeblock(arity+1, last_variant_tag) :: cont
+
(* Inv : nparam + arity > 0 *)
let code_construct tag nparams arity cont =
let f_cont =
add_pop nparams
(if Int.equal arity 0 then
[Kconst (Const_b0 tag); Kreturn 0]
- else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
+ else if tag < last_variant_tag then
+ [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
+ else
+ [Kconst (Const_b0 (tag - last_variant_tag));
+ Kmakeblock(arity+1, last_variant_tag); Kreturn 0])
in
let lbl = Label.create() in
fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
@@ -345,7 +382,6 @@ let get_strcst = function
| Bstrconst sc -> sc
| _ -> raise Not_found
-
let rec str_const c =
match kind_of_term c with
| Sort s -> Bstrconst (Const_sorts s)
@@ -357,7 +393,8 @@ let rec str_const c =
begin
let oib = lookup_mind kn !global_env in
let oip = oib.mind_packets.(j) in
- let num,arity = oip.mind_reloc_tbl.(i-1) in
+ let () = check_compilable oip in
+ let tag,arity = oip.mind_reloc_tbl.(i-1) in
let nparams = oib.mind_nparams in
if Int.equal (nparams + arity) (Array.length args) then
(* spiwack: *)
@@ -399,15 +436,15 @@ let rec str_const c =
with Not_found ->
(* 3/ if no special behavior is available, then the compiler
falls back to the normal behavior *)
- if Int.equal arity 0 then Bstrconst(Const_b0 num)
+ if Int.equal arity 0 then Bstrconst(Const_b0 tag)
else
let rargs = Array.sub args nparams arity in
let b_args = Array.map str_const rargs in
try
let sc_args = Array.map get_strcst b_args in
- Bstrconst(Const_bn(num, sc_args))
+ Bstrconst(const_bn tag sc_args)
with Not_found ->
- Bmakeblock(num,b_args)
+ Bmakeblock(tag,b_args)
else
let b_args = Array.map str_const args in
(* spiwack: tries first to apply the run-time compilation
@@ -418,7 +455,7 @@ let rec str_const c =
f),
b_args)
with Not_found ->
- Bconstruct_app(num, nparams, arity, b_args)
+ Bconstruct_app(tag, nparams, arity, b_args)
end
| _ -> Bconstr c
end
@@ -435,6 +472,7 @@ let rec str_const c =
with Not_found ->
let oib = lookup_mind kn !global_env in
let oip = oib.mind_packets.(j) in
+ let () = check_compilable oip in
let num,arity = oip.mind_reloc_tbl.(i-1) in
let nparams = oib.mind_nparams in
if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
@@ -489,9 +527,12 @@ let rec compile_fv reloc l sz cont =
let rec get_allias env (kn,u as p) =
let cb = lookup_constant kn env in
let tps = cb.const_body_code in
- (match Cemitcodes.force tps with
- | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
- | _ -> p)
+ match tps with
+ | None -> p
+ | Some tps ->
+ (match Cemitcodes.force tps with
+ | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+ | _ -> p)
(* Compiling expressions *)
@@ -607,9 +648,14 @@ let rec compile_constr reloc c sz cont =
let ind = ci.ci_ind in
let mib = lookup_mind (fst ind) !global_env in
let oib = mib.mind_packets.(snd ind) in
+ let () = check_compilable oib in
let tbl = oib.mind_reloc_tbl in
let lbl_consts = Array.make oib.mind_nb_constant Label.no in
- let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in
+ let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+ let nblock = min nallblock (last_variant_tag + 1) in
+ let lbl_blocks = Array.make nblock Label.no in
+ let neblock = max 0 (nallblock - last_variant_tag) in
+ let lbl_eblocks = Array.make neblock Label.no in
let branch1,cont = make_branch cont in
(* Compiling return type *)
let lbl_typ,fcode =
@@ -629,6 +675,15 @@ let rec compile_constr reloc c sz cont =
in
lbl_blocks.(0) <- lbl_accu;
let c = ref code_accu in
+ (* perform the extra match if needed (to many block constructors) *)
+ if neblock <> 0 then begin
+ let lbl_b, code_b =
+ label_code (
+ Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
+ lbl_blocks.(last_variant_tag) <- lbl_b;
+ c := code_b
+ end;
+
(* Compiling regular constructor branches *)
for i = 0 to Array.length tbl - 1 do
let tag, arity = tbl.(i) in
@@ -640,22 +695,24 @@ let rec compile_constr reloc c sz cont =
else
let args, body = decompose_lam branchs.(i) in
let nargs = List.length args in
- let lbl_b,code_b =
- label_code(
- if Int.equal nargs arity then
- Kpushfields arity ::
+
+ let code_b =
+ if Int.equal nargs arity then
compile_constr (push_param arity sz_b reloc)
body (sz_b+arity) (add_pop arity (branch :: !c))
else
let sz_appterm = if is_tailcall then sz_b + arity else arity in
- Kpushfields arity ::
compile_constr reloc branchs.(i) (sz_b+arity)
- (Kappterm(arity,sz_appterm) :: !c))
- in
- lbl_blocks.(tag) <- lbl_b;
+ (Kappterm(arity,sz_appterm) :: !c) in
+ let code_b =
+ if tag < last_variant_tag then Kpushfields arity :: code_b
+ else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in
+ let lbl_b,code_b = label_code code_b in
+ if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
+ else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
c := code_b
done;
- c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
+ c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
let code_sw =
match branch1 with
(* spiwack : branch1 can't be a lbl anymore it's a Branch instead
@@ -677,9 +734,10 @@ and compile_str_cst reloc sc sz cont =
| Bstrconst sc -> Kconst sc :: cont
| Bmakeblock(tag,args) ->
let nargs = Array.length args in
- comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
+ comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont)
| Bconstruct_app(tag,nparams,arity,args) ->
- if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
+ if Int.equal (Array.length args) 0 then
+ code_construct tag nparams arity cont
else
comp_app
(fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -706,13 +764,14 @@ and compile_const =
Kgetglobal (get_allias !global_env (kn,u)) :: cont)
compile_constr reloc () args sz cont
-let compile env c =
+let compile fail_on_error env c =
set_global_env env;
init_fun_code ();
Label.reset_label_counter ();
let reloc = empty_comp_env () in
- let init_code = compile_constr reloc c 0 [Kstop] in
- let fv = List.rev (!(reloc.in_env).fv_rev) in
+ try
+ let init_code = compile_constr reloc c 0 [Kstop] in
+ let fv = List.rev (!(reloc.in_env).fv_rev) in
(* draw_instr init_code;
draw_instr !fun_code;
Format.print_string "fv = ";
@@ -722,21 +781,26 @@ let compile env c =
| FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format
.print_string "\n";
Format.print_flush(); *)
- init_code,!fun_code, Array.of_list fv
-
-let compile_constant_body env = function
- | Undef _ | OpaqueDef _ -> BCconstant
+ Some (init_code,!fun_code, Array.of_list fv)
+ with TooLargeInductive tname ->
+ let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+ (Pp.(fn
+ (str "Cannot compile code for virtual machine as it uses inductive " ++
+ Id.print tname ++ str str_max_constructors));
+ None)
+
+let compile_constant_body fail_on_error env = function
+ | Undef _ | OpaqueDef _ -> Some BCconstant
| Def sb ->
let body = Mod_subst.force_constr sb in
match kind_of_term body with
| Const (kn',u) ->
(* we use the canonical name of the constant*)
let con= constant_of_kn (canonical_con kn') in
- BCallias (get_allias env (con,u))
+ Some (BCallias (get_allias env (con,u)))
| _ ->
- let res = compile env body in
- let to_patch = to_memory res in
- BCdefined to_patch
+ let res = compile fail_on_error env body in
+ Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 8fb6601a93..1128f0d0b7 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -5,10 +5,12 @@ open Declarations
open Pre_env
-val compile : env -> constr -> bytecodes * bytecodes * fv
- (** init, fun, fv *)
+val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
+ env -> constr -> (bytecodes * bytecodes * fv) option
+(** init, fun, fv *)
-val compile_constant_body : env -> constant_def -> body_code
+val compile_constant_body : bool ->
+ env -> constant_def -> body_code option
(** Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 9ecae2b36f..2535a64d3c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -23,34 +23,22 @@ type reloc_info =
type patch = reloc_info * int
+let patch_char4 buff pos c1 c2 c3 c4 =
+ String.unsafe_set buff pos c1;
+ String.unsafe_set buff (pos + 1) c2;
+ String.unsafe_set buff (pos + 2) c3;
+ String.unsafe_set buff (pos + 3) c4
+
let patch_int buff pos n =
- String.unsafe_set buff pos (Char.unsafe_chr n);
- String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
- String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
- String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
-
+ patch_char4 buff pos
+ (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16))
+ (Char.unsafe_chr (n asr 24))
(* Buffering of bytecode *)
let out_buffer = ref(String.create 1024)
and out_position = ref 0
-(*
-let out_word b1 b2 b3 b4 =
- let p = !out_position in
- if p >= String.length !out_buffer then begin
- let len = String.length !out_buffer in
- let new_buffer = String.create (2 * len) in
- String.blit !out_buffer 0 new_buffer 0 len;
- out_buffer := new_buffer
- end;
- String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
- String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
- String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
- String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
- out_position := p + 4
-*)
-
let out_word b1 b2 b3 b4 =
let p = !out_position in
if p >= String.length !out_buffer then begin
@@ -66,13 +54,10 @@ let out_word b1 b2 b3 b4 =
String.blit !out_buffer 0 new_buffer 0 len;
out_buffer := new_buffer
end;
- String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
- String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
- String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
- String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+ patch_char4 !out_buffer p (Char.unsafe_chr b1)
+ (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
out_position := p + 4
-
let out opcode =
out_word opcode 0 0 0
@@ -101,7 +86,7 @@ let extend_label_table needed =
let backpatch (pos, orig) =
let displ = (!out_position - orig) asr 2 in
- !out_buffer.[pos] <- Char.unsafe_chr displ;
+ !out_buffer.[pos] <- Char.unsafe_chr displ;
!out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
!out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
!out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
@@ -222,8 +207,12 @@ let emit_instr = function
out_label typlbl; out_label swlbl;
slot_for_annot annot;out_int sz
| Kswitch (tbl_const, tbl_block) ->
+ let lenb = Array.length tbl_block in
+ let lenc = Array.length tbl_const in
+ assert (lenb < 0x100 && lenc < 0x1000000);
out opSWITCH;
- out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+ out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
+(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
let org = !out_position in
Array.iter (out_label_with_orig org) tbl_const;
Array.iter (out_label_with_orig org) tbl_block
@@ -333,25 +322,41 @@ let subst_patch s (ri,pos) =
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
+let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
+
type body_code =
| BCdefined of to_patch
| BCallias of pconstant
| BCconstant
-let subst_body_code s = function
- | BCdefined tp -> BCdefined (subst_to_patch s tp)
- | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
- | BCconstant -> BCconstant
-
-type to_patch_substituted = body_code substituted
-
-let from_val = from_val
-
-let force = force subst_body_code
-
-let subst_to_patch_subst = subst_substituted
-
-let repr_body_code = repr_substituted
+type to_patch_substituted =
+| PBCdefined of to_patch substituted
+| PBCallias of pconstant substituted
+| PBCconstant
+
+let from_val = function
+| BCdefined tp -> PBCdefined (from_val tp)
+| BCallias cu -> PBCallias (from_val cu)
+| BCconstant -> PBCconstant
+
+let force = function
+| PBCdefined tp -> BCdefined (force subst_to_patch tp)
+| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCconstant -> BCconstant
+
+let subst_to_patch_subst s = function
+| PBCdefined tp -> PBCdefined (subst_substituted s tp)
+| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCconstant -> PBCconstant
+
+let repr_body_code = function
+| PBCdefined tp ->
+ let (s, tp) = repr_substituted tp in
+ (s, BCdefined tp)
+| PBCallias cu ->
+ let (s, cu) = repr_substituted cu in
+ (s, BCallias cu)
+| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
init();
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index ed8b0a6d1d..b29f06c652 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) =
with NotEvaluated ->
(* Pp.msgnl(str"not yet evaluated");*)
let pos =
- match Cemitcodes.force cb.const_body_code with
- | BCdefined(code,pl,fv) ->
- if Univ.Instance.is_empty u then
- let v = eval_to_patch env (code,pl,fv) in
- set_global v
- else set_global (val_of_constant (kn,u))
- | BCallias kn' -> slot_for_getglobal env kn'
- | BCconstant -> set_global (val_of_constant (kn,u)) in
+ match cb.const_body_code with
+ | None -> set_global (val_of_constant (kn,u))
+ | Some code ->
+ match Cemitcodes.force code with
+ | BCdefined(code,pl,fv) ->
+ if Univ.Instance.is_empty u then
+ let v = eval_to_patch env (code,pl,fv) in
+ set_global v
+ else set_global (val_of_constant (kn,u))
+ | BCallias kn' -> slot_for_getglobal env kn'
+ | BCconstant -> set_global (val_of_constant (kn,u)) in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (Ephemeron.create pos);
pos
@@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) =
and val_of_constr env c =
let (_,fun_code,_ as ccfv) =
- try compile env c
+ try match compile true env c with
+ | Some v -> v
+ | None -> assert false
with reraise ->
let reraise = Errors.push reraise in
let () = print_string "can not compile \n" in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index cef920c6a5..27c1c3f3f0 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -70,7 +70,7 @@ type constant_body = {
const_hyps : Context.section_context; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
- const_body_code : Cemitcodes.to_patch_substituted;
+ const_body_code : Cemitcodes.to_patch_substituted option;
const_polymorphic : bool; (** Is it polymorphic or not *)
const_universes : constant_universes;
const_proj : projection_body option;
@@ -139,7 +139,7 @@ type one_inductive_body = {
mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
- mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
+ 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)
@@ -172,7 +172,7 @@ type mutual_inductive_body = {
mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *)
- mind_nparams : int; (** Number of expected parameters *)
+ mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 48a6098eee..a7051d5c13 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -129,7 +129,7 @@ let subst_const_body sub cb =
const_type = type';
const_proj = proj';
const_body_code =
- Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+ Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_polymorphic = cb.const_polymorphic;
const_universes = cb.const_universes;
const_inline_code = cb.const_inline_code }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0ebff440a1..a79abbb7e8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -473,7 +473,7 @@ type unsafe_type_judgment = {
(*s Compilation of global declaration *)
-let compile_constant_body = Cbytegen.compile_constant_body
+let compile_constant_body = Cbytegen.compile_constant_body false
exception Hyp_not_found
diff --git a/kernel/environ.mli b/kernel/environ.mli
index de960ecccf..ede356e699 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -253,7 +253,7 @@ type unsafe_type_judgment = {
(** {6 Compilation of global declaration } *)
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code
+val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
exception Hyp_not_found
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 799471c68a..6b909824ba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -346,7 +346,7 @@ let typecheck_inductive env mie =
in
(id,cn,lc,(sign,arity)))
inds
- in (env_arities, params, inds)
+ in (env_arities, env_ar_par, params, inds)
(************************************************************************)
(************************************************************************)
@@ -366,9 +366,8 @@ exception IllFormedInd of ill_formed_ind
let mind_extract_params = decompose_prod_n_assum
-let explain_ind_err id ntyp env0 nbpar c nargs err =
+let explain_ind_err id ntyp env nbpar c nargs err =
let (lpar,c') = mind_extract_params nbpar c in
- let env = push_rel_context lpar env0 in
match err with
| LocalNonPos kt ->
raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
@@ -486,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
| Rel k ->
(try let (ra,rarg) = List.nth ra_env (k-1) in
+ let largs = List.map (whd_betadeltaiota env) largs in
let nmr1 =
(match ra with
Mrec _ -> compute_rec_par ienv hyps nmr largs
@@ -822,9 +822,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let check_inductive env kn mie =
(* First type-check the inductive definition *)
- let (env_ar, params, inds) = typecheck_inductive env mie in
+ let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
(* Then check positivity conditions *)
- let (nmr,recargs) = check_positivity kn env_ar params inds in
+ let (nmr,recargs) = check_positivity kn env_ar_par params inds in
(* Build the inductive packets *)
build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
mie.mind_entry_universes
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 99d353aae6..26dd45f5f3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -97,7 +97,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let cb' =
{ cb with
const_body = def;
- const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
+ const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
const_universes = ctx' }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d8f319fa79..d52fe611c0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver =
in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) }
+ const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 543397df53..383f810295 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -375,9 +375,12 @@ let makeblock env cn u tag args =
let rec get_allias env (kn, u as p) =
let tps = (lookup_constant kn env).const_body_code in
- match Cemitcodes.force tps with
- | Cemitcodes.BCallias kn' -> get_allias env kn'
- | _ -> p
+ match tps with
+ | None -> p
+ | Some tps ->
+ match Cemitcodes.force tps with
+ | Cemitcodes.BCallias kn' -> get_allias env kn'
+ | _ -> p
(*i Global environment *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b54511e402..a316b4492b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -245,12 +245,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
let tps =
(* FIXME: incompleteness of the bytecode vm: we compile polymorphic
constants like opaque definitions. *)
- if poly then Cemitcodes.from_val Cemitcodes.BCconstant
+ if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
else
- match proj with
- | None -> Cemitcodes.from_val (compile_constant_body env def)
- | Some pb ->
- Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
+ let res =
+ match proj with
+ | None -> compile_constant_body env def
+ | Some pb ->
+ compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+ in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 29315b0a90..1c31cc0414 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -64,8 +64,9 @@ and conv_whd env pb k whd1 whd2 cu =
| Vconstr_const i1, Vconstr_const i2 ->
if Int.equal i1 i2 then cu else raise NotConvertible
| Vconstr_block b1, Vconstr_block b2 ->
+ let tag1 = btag b1 and tag2 = btag b2 in
let sz = bsize b1 in
- if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
+ if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
let rcu = ref cu in
for i = 0 to sz - 1 do
rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 2cc1efe431..d4bf461b39 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -79,7 +79,7 @@ type vprod
type vfun
type vfix
type vcofix
-type vblock
+type vblock
type arguments
type vm_env
@@ -224,10 +224,9 @@ let whd_val : values -> whd =
| 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
| 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
| _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
- else Vconstr_block(Obj.obj o)
-
-
-
+ else
+ Vconstr_block(Obj.obj o)
+
(************************************************)
(* Abstrct machine ******************************)
(************************************************)
@@ -518,8 +517,13 @@ let type_of_switch sw =
let branch_arg k (tag,arity) =
if Int.equal arity 0 then ((Obj.magic tag):values)
else
- let b = Obj.new_block tag arity in
- for i = 0 to arity - 1 do
+ let b, ofs =
+ if tag < last_variant_tag then Obj.new_block tag arity, 0
+ else
+ let b = Obj.new_block last_variant_tag (arity+1) in
+ Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+ b,1 in
+ for i = ofs to ofs + arity - 1 do
Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
done;
val_of_obj b
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 295ea83c49..5190356828 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -94,7 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array
(** Block *)
-val btag : vblock -> int
+val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> values
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:41:55 +0000