From 56925d60207f940ebb88d56981f8cdff41c58247 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 25 Jun 2015 13:56:14 +0200 Subject: Exporting a purely functional interface to bytecode patching. --- kernel/cemitcodes.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9b275cb6c3..37794b5ea6 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -29,11 +29,19 @@ let patch_char4 buff pos c1 c2 c3 c4 = String.unsafe_set buff (pos + 2) c3; String.unsafe_set buff (pos + 3) c4 -let patch_int buff pos n = +let patch 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)) +let patch_int buff patches = + (* 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 = String.copy buff in + let () = List.iter (fun p -> patch buff p) patches in + buff + (* Buffering of bytecode *) let out_buffer = ref(String.create 1024) -- cgit v1.2.3 From 8cb3a606f7c72c32298fe028c9f98e44ea0d378b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 25 Jun 2015 13:48:44 +0200 Subject: Hashcons bytecode generated by the VM. --- kernel/cemitcodes.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 37794b5ea6..4e64ed6976 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -374,6 +374,8 @@ let to_memory (init_code, fun_code, fv) = emit fun_code; let code = String.create !out_position in String.unsafe_blit !out_buffer 0 code 0 !out_position; + (** Later uses of this string are all purely functional *) + let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> (match lbl with -- cgit v1.2.3 From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- kernel/cemitcodes.ml | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9b275cb6c3..2a70d0b1b7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of pconstant + | Reloc_getglobal of Names.constant type patch = reloc_info * int @@ -127,11 +127,11 @@ let slot_for_const c = enter (Reloc_const c); out_int 0 -and slot_for_annot a = +let slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal p = +let slot_for_getglobal p = enter (Reloc_getglobal p); out_int 0 @@ -190,7 +190,7 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q - | Kconst((Const_b0 i)) -> + | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 then out (opCONST0 + i) else (out opCONSTINT; out_int i) @@ -310,7 +310,7 @@ let rec subst_strcst s sc = | Const_sorts _ | Const_b0 _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_patch s (ri,pos) = match ri with @@ -319,7 +319,7 @@ let subst_patch s (ri,pos) = 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_pcon s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -328,12 +328,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) type body_code = | BCdefined of to_patch - | BCalias of pconstant + | BCalias of Names.constant | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of pconstant substituted +| PBCalias of Names.constant substituted | PBCconstant let from_val = function @@ -343,7 +343,7 @@ let from_val = function let force = function | PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCalias cu -> BCalias (force subst_pconstant cu) +| PBCalias cu -> BCalias (force subst_constant cu) | PBCconstant -> BCconstant let subst_to_patch_subst s = function @@ -373,8 +373,3 @@ let to_memory (init_code, fun_code, fv) = | Label_undefined patchlist -> assert (patchlist = []))) !label_table; (code, reloc, fv) - - - - - -- cgit v1.2.3 From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 11:16:24 +0100 Subject: Refine Gregory Malecha's patch on VM and universe polymorphism. - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. --- kernel/cemitcodes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2a70d0b1b7..ef0c9af4ff 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -307,7 +307,7 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | 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) -- cgit v1.2.3 From cbd815a289db52f58235f23f5afba3be49cc8eed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 13:54:18 +0100 Subject: Removing dead code. --- kernel/cemitcodes.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 5ba93eda05..61042ccc17 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -306,8 +306,6 @@ let init () = type emitcodes = string -let copy = String.copy - let length = String.length type to_patch = emitcodes * (patch list) * fv @@ -332,8 +330,6 @@ 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 | BCalias of Names.constant -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/cemitcodes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ef0c9af4ff..57e32684ad 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*