aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml49
-rw-r--r--kernel/cbytecodes.mli6
-rw-r--r--kernel/cbytegen.ml18
-rw-r--r--kernel/cemitcodes.ml424
-rw-r--r--kernel/cemitcodes.mli14
-rw-r--r--kernel/csymtable.ml63
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/mod_typing.ml27
-rw-r--r--kernel/subtyping.ml9
-rw-r--r--kernel/univ.ml44
-rw-r--r--kernel/univ.mli10
-rw-r--r--kernel/vmvalues.ml11
12 files changed, 373 insertions, 304 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 9febc6449b..6d91c3ec9e 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -45,6 +45,55 @@ type reloc_table = (tag * int) array
type annot_switch =
{ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+let rec eq_structured_constant c1 c2 = match c1, c2 with
+| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_sorts _, _ -> false
+| Const_ind i1, Const_ind i2 -> 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) ->
+ Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2
+| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
+
+let rec hash_structured_constant c =
+ let open Hashset.Combine in
+ match c with
+ | Const_sorts s -> combinesmall 1 (Sorts.hash s)
+ | Const_ind i -> combinesmall 2 (ind_hash i)
+ | 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 5 (combine (Int.hash t) h)
+ | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+ | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
+
+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
+
+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
+
module Label =
struct
type t = int
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 5d37a5840b..bf2e462e83 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -41,6 +41,12 @@ type reloc_table = (tag * int) array
type annot_switch =
{ci : case_info; 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
+
+val eq_annot_switch : annot_switch -> annot_switch -> bool
+val hash_annot_switch : annot_switch -> int
+
module Label :
sig
type t = int
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5dab2932d7..4a34dbcffe 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont =
of the structured constant, while the later (if any) will be applied as
arguments. *)
let open Univ in begin
- let levels = Universe.levels u in
- let global_levels =
- LSet.filter (fun x -> Level.var_index x = None) levels
- in
- let local_levels =
- List.map_filter (fun x -> Level.var_index x)
- (LSet.elements levels)
- in
+ let u,s = Universe.compact u in
(* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
- let uglob =
- LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
- in
- if local_levels = [] then
- compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont
+ if List.is_empty s then
+ compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont
else
let compile_get_univ reloc idx sz cont =
set_max_stack_size sz;
compile_fv_elem reloc (FVuniv_var idx) sz cont
in
comp_app compile_str_cst compile_get_univ reloc
- (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+ (Bstrconst (Const_type u)) (Array.of_list s) sz cont
end
| LetIn(_,xb,_,body) ->
compile_constr reloc xb sz
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index eeea19c12b..856b0b465c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,18 +10,51 @@
machine, Oct 2004 *)
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
+open Names
open Term
open Cbytecodes
open Copcodes
open Mod_subst
+type emitcodes = String.t
+
+external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+
(* Relocation information *)
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
| Reloc_getglobal of Names.Constant.t
-type patch = reloc_info * int
+let eq_reloc_info r1 r2 = match r1, r2 with
+| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
+| Reloc_annot _, _ -> false
+| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2
+| Reloc_const _, _ -> false
+| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
+| Reloc_getglobal _, _ -> false
+
+let hash_reloc_info r =
+ let open Hashset.Combine in
+ match r with
+ | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
+ | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
+ | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+
+module RelocTable = Hashtbl.Make(struct
+ type t = reloc_info
+ let equal = eq_reloc_info
+ let hash = hash_reloc_info
+end)
+
+(** We use arrays for on-disk representation. On 32-bit machines, this means we
+ can only have a maximum amount of about 4.10^6 relocations, which seems
+ quite a lot, but potentially reachable if e.g. compiling big proofs. This
+ would prevent VM computing with these terms on 32-bit architectures. Maybe
+ we should use a more robust data structure? *)
+type patches = {
+ reloc_infos : (reloc_info * int array) array;
+}
let patch_char4 buff pos c1 c2 c3 c4 =
Bytes.unsafe_set buff pos c1;
@@ -29,40 +62,48 @@ let patch_char4 buff pos c1 c2 c3 c4 =
Bytes.unsafe_set buff (pos + 2) c3;
Bytes.unsafe_set buff (pos + 3) c4
-let patch buff (pos, n) =
+let patch1 buff pos n =
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))
-(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
-let patch_int buff patches =
+let patch_int buff reloc =
(* copy code *before* patching because of nested evaluations:
the code we are patching might be called (and thus "concurrently" patched)
and results in wrong results. Side-effects... *)
let buff = Bytes.of_string buff in
- let () = List.iter (fun p -> patch buff p) patches in
- (* Note: we follow the apporach suggested by Gabriel Scherer in
- PR#136 here, and use unsafe as we own buff.
+ let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in
+ let () = CArray.iter iter reloc in
+ buff
- The crux of the question that avoids defining emitcodes just as a
- Byte.t is the call to hcons in to_memory below. Even if disabling
- this optimization has no visible time impact, test data shows
- that the optimization is indeed triggered quite often so we
- choose ugliness over altering the semantics.
-
- Handle with care.
- *)
- Bytes.unsafe_to_string buff
+let patch buff pl f =
+ (** Order seems important here? *)
+ let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
+ let buff = patch_int buff reloc in
+ tcode_of_code buff (Bytes.length buff)
(* Buffering of bytecode *)
-let out_buffer = ref(Bytes.create 1024)
-and out_position = ref 0
+type label_definition =
+ Label_defined of int
+ | Label_undefined of (int * int) list
-let out_word b1 b2 b3 b4 =
- let p = !out_position in
- if p >= Bytes.length !out_buffer then begin
- let len = Bytes.length !out_buffer in
+type env = {
+ mutable out_buffer : Bytes.t;
+ mutable out_position : int;
+ mutable label_table : label_definition array;
+ (* le ieme element de la table = Label_defined n signifie que l'on a
+ deja rencontrer le label i et qu'il est a l'offset n.
+ = Label_undefined l signifie que l'on a
+ pas encore rencontrer ce label, le premier entier indique ou est l'entier
+ a patcher dans la string, le deuxieme son origine *)
+ reloc_info : int list RelocTable.t;
+}
+
+let out_word env b1 b2 b3 b4 =
+ let p = env.out_position in
+ if p >= Bytes.length env.out_buffer then begin
+ let len = Bytes.length env.out_buffer in
let new_len =
if len <= Sys.max_string_length / 2
then 2 * len
@@ -71,260 +112,240 @@ let out_word b1 b2 b3 b4 =
then invalid_arg "String.create" (* Pas la bonne exception .... *)
else Sys.max_string_length in
let new_buffer = Bytes.create new_len in
- Bytes.blit !out_buffer 0 new_buffer 0 len;
- out_buffer := new_buffer
+ Bytes.blit env.out_buffer 0 new_buffer 0 len;
+ env.out_buffer <- new_buffer
end;
- patch_char4 !out_buffer p (Char.unsafe_chr b1)
+ patch_char4 env.out_buffer p (Char.unsafe_chr b1)
(Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
- out_position := p + 4
+ env.out_position <- p + 4
-let out opcode =
- out_word opcode 0 0 0
+let out env opcode =
+ out_word env opcode 0 0 0
-let out_int n =
- out_word n (n asr 8) (n asr 16) (n asr 24)
+let out_int env n =
+ out_word env n (n asr 8) (n asr 16) (n asr 24)
(* Handling of local labels and backpatching *)
-type label_definition =
- Label_defined of int
- | Label_undefined of (int * int) list
-
-let label_table = ref ([| |] : label_definition array)
-(* le ieme element de la table = Label_defined n signifie que l'on a
- deja rencontrer le label i et qu'il est a l'offset n.
- = Label_undefined l signifie que l'on a
- pas encore rencontrer ce label, le premier entier indique ou est l'entier
- a patcher dans la string, le deuxieme son origine *)
-
-let extend_label_table needed =
- let new_size = ref(Array.length !label_table) in
+let extend_label_table env needed =
+ let new_size = ref(Array.length env.label_table) in
while needed >= !new_size do new_size := 2 * !new_size done;
let new_table = Array.make !new_size (Label_undefined []) in
- Array.blit !label_table 0 new_table 0 (Array.length !label_table);
- label_table := new_table
-
-let backpatch (pos, orig) =
- let displ = (!out_position - orig) asr 2 in
- Bytes.set !out_buffer pos @@ Char.unsafe_chr displ;
- Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
- Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
- Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
-
-let define_label lbl =
- if lbl >= Array.length !label_table then extend_label_table lbl;
- match (!label_table).(lbl) with
+ Array.blit env.label_table 0 new_table 0 (Array.length env.label_table);
+ env.label_table <- new_table
+
+let backpatch env (pos, orig) =
+ let displ = (env.out_position - orig) asr 2 in
+ Bytes.set env.out_buffer pos @@ Char.unsafe_chr displ;
+ Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+ Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+ Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
+
+let define_label env lbl =
+ if lbl >= Array.length env.label_table then extend_label_table env lbl;
+ match (env.label_table).(lbl) with
Label_defined _ ->
raise(Failure "CEmitcode.define_label")
| Label_undefined patchlist ->
- List.iter backpatch patchlist;
- (!label_table).(lbl) <- Label_defined !out_position
+ List.iter (fun p -> backpatch env p) patchlist;
+ (env.label_table).(lbl) <- Label_defined env.out_position
-let out_label_with_orig orig lbl =
- if lbl >= Array.length !label_table then extend_label_table lbl;
- match (!label_table).(lbl) with
+let out_label_with_orig env orig lbl =
+ if lbl >= Array.length env.label_table then extend_label_table env lbl;
+ match (env.label_table).(lbl) with
Label_defined def ->
- out_int((def - orig) asr 2)
+ out_int env ((def - orig) asr 2)
| Label_undefined patchlist ->
(* spiwack: patchlist is supposed to be non-empty all the time
thus I commented that out. If there is no problem I suggest
removing it for next release (cur: 8.1) *)
(*if patchlist = [] then *)
- (!label_table).(lbl) <-
- Label_undefined((!out_position, orig) :: patchlist);
- out_int 0
+ (env.label_table).(lbl) <-
+ Label_undefined((env.out_position, orig) :: patchlist);
+ out_int env 0
-let out_label l = out_label_with_orig !out_position l
+let out_label env l = out_label_with_orig env env.out_position l
(* Relocation information *)
-let reloc_info = ref ([] : (reloc_info * int) list)
+let enter env info =
+ let pos = env.out_position in
+ let old = try RelocTable.find env.reloc_info info with Not_found -> [] in
+ RelocTable.replace env.reloc_info info (pos :: old)
-let enter info =
- reloc_info := (info, !out_position) :: !reloc_info
+let slot_for_const env c =
+ enter env (Reloc_const c);
+ out_int env 0
-let slot_for_const c =
- enter (Reloc_const c);
- out_int 0
+let slot_for_annot env a =
+ enter env (Reloc_annot a);
+ out_int env 0
-let slot_for_annot a =
- enter (Reloc_annot a);
- out_int 0
-
-let slot_for_getglobal p =
- enter (Reloc_getglobal p);
- out_int 0
+let slot_for_getglobal env p =
+ enter env (Reloc_getglobal p);
+ out_int env 0
(* Emission of one instruction *)
-let emit_instr = function
- | Klabel lbl -> define_label lbl
+let emit_instr env = function
+ | Klabel lbl -> define_label env lbl
| Kacc n ->
- if n < 8 then out(opACC0 + n) else (out opACC; out_int n)
+ if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n)
| Kenvacc n ->
if n >= 1 && n <= 4
- then out(opENVACC1 + n - 1)
- else (out opENVACC; out_int n)
+ then out env(opENVACC1 + n - 1)
+ else (out env opENVACC; out_int env n)
| Koffsetclosure ofs ->
if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out (opOFFSETCLOSURE0 + ofs / 2)
- else (out opOFFSETCLOSURE; out_int ofs)
+ then out env (opOFFSETCLOSURE0 + ofs / 2)
+ else (out env opOFFSETCLOSURE; out_int env ofs)
| Kpush ->
- out opPUSH
+ out env opPUSH
| Kpop n ->
- out opPOP; out_int n
+ out env opPOP; out_int env n
| Kpush_retaddr lbl ->
- out opPUSH_RETADDR; out_label lbl
+ out env opPUSH_RETADDR; out_label env lbl
| Kapply n ->
- if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n)
+ if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
| Kappterm(n, sz) ->
- if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz)
- else (out opAPPTERM; out_int n; out_int sz)
+ if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
+ else (out env opAPPTERM; out_int env n; out_int env sz)
| Kreturn n ->
- out opRETURN; out_int n
+ out env opRETURN; out_int env n
| Kjump ->
- out opRETURN; out_int 0
+ out env opRETURN; out_int env 0
| Krestart ->
- out opRESTART
+ out env opRESTART
| Kgrab n ->
- out opGRAB; out_int n
+ out env opGRAB; out_int env n
| Kgrabrec(rec_arg) ->
- out opGRABREC; out_int rec_arg
+ out env opGRABREC; out_int env rec_arg
| Kclosure(lbl, n) ->
- out opCLOSURE; out_int n; out_label lbl
+ out env opCLOSURE; out_int env n; out_label env lbl
| Kclosurerec(nfv,init,lbl_types,lbl_bodies) ->
- out opCLOSUREREC;out_int (Array.length lbl_bodies);
- out_int nfv; out_int init;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_types;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_bodies
+ out env opCLOSUREREC;out_int env (Array.length lbl_bodies);
+ out_int env nfv; out_int env init;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_types;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_bodies
| Kclosurecofix(nfv,init,lbl_types,lbl_bodies) ->
- out opCLOSURECOFIX;out_int (Array.length lbl_bodies);
- out_int nfv; out_int init;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_types;
- let org = !out_position in
- Array.iter (out_label_with_orig org) lbl_bodies
+ out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies);
+ out_int env nfv; out_int env init;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_types;
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) lbl_bodies
| Kgetglobal q ->
- out opGETGLOBAL; slot_for_getglobal q
+ out env opGETGLOBAL; slot_for_getglobal env q
| Kconst (Const_b0 i) ->
if i >= 0 && i <= 3
- then out (opCONST0 + i)
- else (out opCONSTINT; out_int i)
+ then out env (opCONST0 + i)
+ else (out env opCONSTINT; out_int env i)
| Kconst c ->
- out opGETGLOBAL; slot_for_const c
+ out env opGETGLOBAL; slot_for_const env c
| Kmakeblock(n, t) ->
if Int.equal n 0 then invalid_arg "emit_instr : block size = 0"
- else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
- else (out opMAKEBLOCK; out_int n; out_int t)
+ else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t)
+ else (out env opMAKEBLOCK; out_int env n; out_int env t)
| Kmakeprod ->
- out opMAKEPROD
+ out env opMAKEPROD
| Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
- out opMAKESWITCHBLOCK;
- out_label typlbl; out_label swlbl;
- slot_for_annot annot;out_int sz
+ out env opMAKESWITCHBLOCK;
+ out_label env typlbl; out_label env swlbl;
+ slot_for_annot env annot;out_int env 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_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
+ out env opSWITCH;
+ out_word env lenc (lenc asr 8) (lenc asr 16) (lenb);
+(* out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
+ let org = env.out_position in
+ Array.iter (out_label_with_orig env org) tbl_const;
+ Array.iter (out_label_with_orig env org) tbl_block
| Kpushfields n ->
- out opPUSHFIELDS;out_int n
+ out env opPUSHFIELDS;out_int env n
| Kfield n ->
- if n <= 1 then out (opGETFIELD0+n)
- else (out opGETFIELD;out_int n)
+ if n <= 1 then out env (opGETFIELD0+n)
+ else (out env opGETFIELD;out_int env n)
| Ksetfield n ->
- if n <= 1 then out (opSETFIELD0+n)
- else (out opSETFIELD;out_int n)
+ if n <= 1 then out env (opSETFIELD0+n)
+ else (out env opSETFIELD;out_int env n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
- | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
- | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size
+ | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p)
+ | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
(* spiwack *)
- | Kbranch lbl -> out opBRANCH; out_label lbl
- | Kaddint31 -> out opADDINT31
- | Kaddcint31 -> out opADDCINT31
- | Kaddcarrycint31 -> out opADDCARRYCINT31
- | Ksubint31 -> out opSUBINT31
- | Ksubcint31 -> out opSUBCINT31
- | Ksubcarrycint31 -> out opSUBCARRYCINT31
- | Kmulint31 -> out opMULINT31
- | Kmulcint31 -> out opMULCINT31
- | Kdiv21int31 -> out opDIV21INT31
- | Kdivint31 -> out opDIVINT31
- | Kaddmuldivint31 -> out opADDMULDIVINT31
- | Kcompareint31 -> out opCOMPAREINT31
- | Khead0int31 -> out opHEAD0INT31
- | Ktail0int31 -> out opTAIL0INT31
- | Kisconst lbl -> out opISCONST; out_label lbl
- | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
- | Kcompint31 -> out opCOMPINT31
- | Kdecompint31 -> out opDECOMPINT31
- | Klorint31 -> out opORINT31
- | Klandint31 -> out opANDINT31
- | Klxorint31 -> out opXORINT31
+ | Kbranch lbl -> out env opBRANCH; out_label env lbl
+ | Kaddint31 -> out env opADDINT31
+ | Kaddcint31 -> out env opADDCINT31
+ | Kaddcarrycint31 -> out env opADDCARRYCINT31
+ | Ksubint31 -> out env opSUBINT31
+ | Ksubcint31 -> out env opSUBCINT31
+ | Ksubcarrycint31 -> out env opSUBCARRYCINT31
+ | Kmulint31 -> out env opMULINT31
+ | Kmulcint31 -> out env opMULCINT31
+ | Kdiv21int31 -> out env opDIV21INT31
+ | Kdivint31 -> out env opDIVINT31
+ | Kaddmuldivint31 -> out env opADDMULDIVINT31
+ | Kcompareint31 -> out env opCOMPAREINT31
+ | Khead0int31 -> out env opHEAD0INT31
+ | Ktail0int31 -> out env opTAIL0INT31
+ | Kisconst lbl -> out env opISCONST; out_label env lbl
+ | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl
+ | Kcompint31 -> out env opCOMPINT31
+ | Kdecompint31 -> out env opDECOMPINT31
+ | Klorint31 -> out env opORINT31
+ | Klandint31 -> out env opANDINT31
+ | Klxorint31 -> out env opXORINT31
(*/spiwack *)
| Kstop ->
- out opSTOP
+ out env opSTOP
(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
-let rec emit insns remaining = match insns with
+let rec emit env insns remaining = match insns with
| [] ->
(match remaining with
[] -> ()
- | (first::rest) -> emit first rest)
+ | (first::rest) -> emit env first rest)
(* Peephole optimizations *)
| Kpush :: Kacc n :: c ->
- if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
- emit c remaining
+ if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n);
+ emit env c remaining
| Kpush :: Kenvacc n :: c ->
if n >= 1 && n <= 4
- then out(opPUSHENVACC1 + n - 1)
- else (out opPUSHENVACC; out_int n);
- emit c remaining
+ then out env(opPUSHENVACC1 + n - 1)
+ else (out env opPUSHENVACC; out_int env n);
+ emit env c remaining
| Kpush :: Koffsetclosure ofs :: c ->
if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
- else (out opPUSHOFFSETCLOSURE; out_int ofs);
- emit c remaining
+ then out env(opPUSHOFFSETCLOSURE0 + ofs / 2)
+ else (out env opPUSHOFFSETCLOSURE; out_int env ofs);
+ emit env c remaining
| Kpush :: Kgetglobal id :: c ->
- out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
+ out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining
| Kpush :: Kconst (Const_b0 i) :: c ->
if i >= 0 && i <= 3
- then out (opPUSHCONST0 + i)
- else (out opPUSHCONSTINT; out_int i);
- emit c remaining
+ then out env (opPUSHCONST0 + i)
+ else (out env opPUSHCONSTINT; out_int env i);
+ emit env c remaining
| Kpush :: Kconst const :: c ->
- out opPUSHGETGLOBAL; slot_for_const const;
- emit c remaining
+ out env opPUSHGETGLOBAL; slot_for_const env const;
+ emit env c remaining
| Kpop n :: Kjump :: c ->
- out opRETURN; out_int n; emit c remaining
+ out env opRETURN; out_int env n; emit env c remaining
| Ksequence(c1,c2)::c ->
- emit c1 (c2::c::remaining)
+ emit env c1 (c2::c::remaining)
(* Default case *)
| instr :: c ->
- emit_instr instr; emit c remaining
+ emit_instr env instr; emit env c remaining
(* Initialization *)
-let init () =
- out_position := 0;
- label_table := Array.make 16 (Label_undefined []);
- reloc_info := []
-
-type emitcodes = String.t
-
-let length = String.length
-
-type to_patch = emitcodes * (patch list) * fv
+type to_patch = emitcodes * patches * fv
(* Substitution *)
let rec subst_strcst s sc =
@@ -334,17 +355,21 @@ let rec subst_strcst s sc =
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
-let subst_patch s (ri,pos) =
+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},pos)
- | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
+ Reloc_annot {a with ci = ci}
+ | Reloc_const sc -> Reloc_const (subst_strcst s sc)
+ | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
+
+let subst_patches subst p =
+ let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
+ { reloc_infos = infos; }
let subst_to_patch s (code,pl,fv) =
- code,List.rev_map (subst_patch s) pl,fv
+ code, subst_patches s pl, fv
type body_code =
| BCdefined of to_patch
@@ -381,16 +406,23 @@ let repr_body_code = function
| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
- init();
- emit init_code [];
- emit fun_code [];
+ let env = {
+ out_buffer = Bytes.create 1024;
+ out_position = 0;
+ label_table = Array.make 16 (Label_undefined []);
+ reloc_info = RelocTable.create 91;
+ } in
+ emit env init_code [];
+ emit env fun_code [];
(** Later uses of this string are all purely functional *)
- let code = Bytes.sub_string !out_buffer 0 !out_position in
+ let code = Bytes.sub_string env.out_buffer 0 env.out_position in
let code = CString.hcons code in
- let reloc = List.rev !reloc_info in
+ let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in
+ let reloc = RelocTable.fold fold env.reloc_info [] in
+ let reloc = { reloc_infos = CArray.of_list reloc } in
Array.iter (fun lbl ->
(match lbl with
Label_defined _ -> assert true
| Label_undefined patchlist ->
- assert (patchlist = []))) !label_table;
+ assert (patchlist = []))) env.label_table;
(code, reloc, fv)
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index fee45aafd8..03920dc1a3 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -6,20 +6,12 @@ type reloc_info =
| Reloc_const of structured_constant
| Reloc_getglobal of Constant.t
-type patch = reloc_info * int
-
-(* A virer *)
-val subst_patch : Mod_subst.substitution -> patch -> patch
-
+type patches
type emitcodes
-val length : emitcodes -> int
-
-val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes
-
-type to_patch = emitcodes * (patch list) * fv
+val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode
-val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
+type to_patch = emitcodes * patches * fv
type body_code =
| BCdefined of to_patch
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 2bbb867cd4..55430a9d81 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -14,7 +14,6 @@
open Util
open Names
-open Constr
open Vmvalues
open Cemitcodes
open Cbytecodes
@@ -25,7 +24,6 @@ open Cbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
-external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
(*******************)
@@ -56,61 +54,12 @@ let set_global v =
(* table pour les structured_constant et les annotations des switchs *)
-let rec eq_structured_constant c1 c2 = match c1, c2 with
-| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> 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) ->
- Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| Const_bn _, _ -> false
-| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
-| Const_univ_level _ , _ -> false
-| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
-| Const_type _ , _ -> false
-
-let rec hash_structured_constant c =
- let open Hashset.Combine in
- match c with
- | Const_sorts s -> combinesmall 1 (Sorts.hash s)
- | Const_ind i -> combinesmall 2 (ind_hash i)
- | 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 5 (combine (Int.hash t) h)
- | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
- | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
-
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
let equal = eq_structured_constant
let hash = hash_structured_constant
end)
-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 &&
- Array.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 &&
- Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
- (asw1.tailcall : bool) == asw2.tailcall
-
-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
-
module AnnotTable = Hashtbl.Make (struct
type t = annot_switch
let equal = eq_annot_switch
@@ -205,15 +154,13 @@ and slot_for_fv env fv =
assert false
and eval_to_patch env (buff,pl,fv) =
- let patch = function
- | Reloc_annot a, pos -> (pos, slot_for_annot a)
- | Reloc_const sc, pos -> (pos, slot_for_str_cst sc)
- | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn)
+ let slots = function
+ | Reloc_annot a -> slot_for_annot a
+ | Reloc_const sc -> slot_for_str_cst sc
+ | Reloc_getglobal kn -> slot_for_getglobal env kn
in
- let patches = List.map_left patch pl in
- let buff = patch_int buff patches in
+ let tc = patch buff pl slots in
let vm_env = Array.map (slot_for_fv env) fv in
- let tc = tcode_of_code buff (length buff) in
eval_tcode tc vm_env
and val_of_constr env c =
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5b9e1a1414..cb7f0ecef3 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -219,7 +219,7 @@ type ('ty,'a) functorize =
type with_declaration =
| WithMod of Id.t list * ModPath.t
- | WithDef of Id.t list * constr Univ.in_universe_context
+ | WithDef of Id.t list * (constr * Univ.AUContext.t option)
type module_alg_expr =
| MEident of ModPath.t
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b7eb481ee3..6b89a1da03 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -73,13 +73,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
any implementations of parameters and opaques terms,
as long as they have the right type *)
let c', univs, ctx' =
- match cb.const_universes with
- | Monomorphic_const _ ->
- (** We do not add the deferred constraints of the body in the
- environment, because they do not appear in the type of the
- definition. Any inconsistency will be raised at a later stage
- when joining the environment. *)
- let env' = Environ.push_context ~strict:true ctx env' in
+ match cb.const_universes, ctx with
+ | Monomorphic_const _, None ->
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
@@ -91,11 +86,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let c' = Mod_subst.force_constr cs in
c, Reduction.infer_conv env' (Environ.universes env') c c'
in
- let ctx = Univ.ContextSet.of_context ctx in
- c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
- | Polymorphic_const uctx ->
- let inst, ctx = Univ.abstract_universes ctx in
- let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
+ c', Monomorphic_const Univ.ContextSet.empty, cst
+ | Polymorphic_const uctx, Some ctx ->
let () =
if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
@@ -116,7 +108,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
in
if not (Univ.Constraint.is_empty cst) then
error_incorrect_with_constraint lab;
- c, Polymorphic_const ctx, Univ.ContextSet.empty
+ c, Polymorphic_const ctx, Univ.Constraint.empty
+ | _ -> error_incorrect_with_constraint lab
in
let def = Def (Mod_subst.from_val c') in
(* let ctx' = Univ.UContext.make (newus, cst) in *)
@@ -225,11 +218,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
let check_with env mp (sign,alg,reso,cst) = function
- |WithDef(idl,c) ->
+ |WithDef(idl, (c, ctx)) ->
let struc = destr_nofunctor sign in
- let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
- NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
+ let struc', c', cst' = check_with_def env struc (idl, (c, ctx)) mp reso in
+ let wd' = WithDef (idl, (c', ctx)) in
+ NoFunctor struc', MEwith (alg,wd'), reso, Univ.ContextSet.add_constraints cst' cst
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d0d5cb1d56..e95d5d2b57 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -118,6 +118,15 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let env = check_polymorphic_instance error env auctx auctx' in
env, Univ.make_abstract_instance auctx'
| Cumulative_ind cumi, Cumulative_ind cumi' ->
+ (** Currently there is no way to control variance of inductive types, but
+ just in case we require that they are in a subtyping relation. *)
+ let () =
+ let v = ACumulativityInfo.variance cumi in
+ let v' = ACumulativityInfo.variance cumi' in
+ if not (Array.for_all2 Variance.check_subtype v' v) then
+ CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++
+ str " is not compatible with the one of " ++ KerName.print kn2)
+ in
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
let env = check_polymorphic_instance error env auctx auctx' in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 080bb7ad48..c42b667492 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -266,7 +266,7 @@ struct
module Expr =
struct
type t = Level.t * int
-
+
(* Hashing of expressions *)
module ExprHash =
struct
@@ -487,7 +487,40 @@ struct
| [] -> cons a l
in
List.fold_right (fun a acc -> aux a acc) u []
-
+
+ (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
+ [p], -1 if not found *)
+ let rec max_var_pred p u =
+ let open Level in
+ match u with
+ | [] -> -1
+ | (v, _) :: u ->
+ match var_index v with
+ | Some i when p i -> max i (max_var_pred p u)
+ | _ -> max_var_pred p u
+
+ let rec remap_var u i j =
+ let open Level in
+ match u with
+ | [] -> []
+ | (v, incr) :: u when var_index v = Some i ->
+ (Level.var j, incr) :: remap_var u i j
+ | _ :: u -> remap_var u i j
+
+ let rec compact u max_var i =
+ if i >= max_var then (u,[]) else
+ let j = max_var_pred (fun j -> j < i) u in
+ if Int.equal i (j+1) then
+ let (u,s) = compact u max_var (i+1) in
+ (u, i :: s)
+ else
+ let (u,s) = compact (remap_var u i j) max_var (i+1) in
+ (u, j+1 :: s)
+
+ let compact u =
+ let max_var = max_var_pred (fun _ -> true) u in
+ compact u max_var 0
+
(* Returns the formal universe that is greater than the universes u and v.
Used to type the products. *)
let sup x y = merge_univs x y
@@ -726,6 +759,13 @@ struct
| Invariant, _ | _, Invariant -> Invariant
| Covariant, Covariant -> Covariant
+ let check_subtype x y = match x, y with
+ | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+ | Irrelevant, Covariant -> false
+ | (Covariant | Invariant), Covariant -> true
+ | (Irrelevant | Covariant), Invariant -> false
+ | Invariant, Invariant -> true
+
let pr = function
| Irrelevant -> str "*"
| Covariant -> str "+"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 77ebf5a11b..74d1bfd3a8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -125,6 +125,13 @@ sig
val for_all : (Level.t * int -> bool) -> t -> bool
val map : (Level.t * int -> 'a) -> t -> 'a list
+
+ (** [compact u] remaps local variables in [u] such that their indices become
+ consecutive. It returns the new universe and the mapping.
+ Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
+ [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+ *)
+ val compact : t -> t * int list
end
type universe = Universe.t
@@ -246,6 +253,9 @@ sig
A'] as opposed to [A' <= A]. *)
type t = Irrelevant | Covariant | Invariant
+ (** [check_subtype x y] holds if variance [y] is also an instance of [x] *)
+ val check_subtype : t -> t -> bool
+
val sup : t -> t -> t
val pr : t -> Pp.t
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec18..2d8a1d9761 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,6 +8,7 @@
open Names
open Sorts
open Cbytecodes
+open Univ
(*******************************************)
(* Initalization of the abstract machine ***)
@@ -189,11 +190,11 @@ let rec whd_accu a stk =
| i when Int.equal i type_atom_tag ->
begin match stk with
| [Zapp args] ->
- let u = ref (Obj.obj (Obj.field at 0)) in
- for i = 0 to nargs args - 1 do
- u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
- done;
- Vsort (Type !u)
+ let args = Array.init (nargs args) (arg args) in
+ let u = Obj.obj (Obj.field at 0) in
+ let inst = Instance.of_array (Array.map uni_lvl_val args) in
+ let u = Univ.subst_instance_universe inst u in
+ Vsort (Type u)
| _ -> assert false
end
| i when i <= max_atom_tag ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 12:58:44 +0000