Map opaque definitions to bytecode holes.

silene · Apr 9, 2024 · ce0855b · ce0855b
1 parent 7f43b96
commit ce0855b
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 3 deletions.
diff --git a/checker/values.ml b/checker/values.ml
@@ -283,7 +283,7 @@ let v_reloc_info = v_sum "vm_reloc_info" 0 [|
 let v_vm_patches = v_tuple "vm_patches" [|Array v_reloc_info|]
 
 let v_vm_pbody_code index =
-  v_sum "pbody_code" 1 [|
+  v_sum "pbody_code" 2 [|
     [|v_pair index v_vm_patches|];
     [|v_cst|];
   |]

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
@@ -393,6 +393,7 @@ let push_bytecode vmtab code =
     let vmtab, index = Vmlibrary.add code vmtab in
     vmtab, Some (BCdefined (index, patches))
   | Some BCconstant -> vmtab, Some BCconstant
+  | Some BChole -> vmtab, Some BChole
   | Some (BCalias kn) -> vmtab, Some (BCalias kn)
   in
   vmtab, code
@@ -920,7 +921,7 @@ let add_constant l decl senv =
         let nonce = Nonce.create () in
         let future_cst = HandleMap.add i (ctx, senv, nonce) senv.future_cst in
         let senv = { senv with future_cst } in
-        senv, { cb with const_body = OpaqueDef o; const_body_code = Some Vmemitcodes.BCconstant }
+        senv, { cb with const_body = OpaqueDef o; const_body_code = Some Vmemitcodes.BChole }
       | ConstantEntry ce ->
         let cb = Constant_typing.infer_constant ~sec_univs senv.env ce in
         let cb = compile_bytecode senv.env cb in

diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
@@ -942,7 +942,8 @@ let compile ~fail_on_error ?universes env sigma c =
     end
 
 let compile_constant_body ~fail_on_error env univs = function
-  | Undef _ | OpaqueDef _ -> Some BCconstant
+  | Undef _ -> Some BCconstant
+  | OpaqueDef _ -> Some BChole
   | Primitive _ | Symbol _ -> None
   | Def body ->
       let instance_size = UVars.AbstractContext.size (Declareops.universes_context univs) in

diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
@@ -495,13 +495,15 @@ type 'a pbody_code =
   | BCdefined of ('a * patches)
   | BCalias of Names.Constant.t
   | BCconstant
+  | BChole
 
 type body_code = to_patch pbody_code
 
 let subst_body_code s = function
 | BCdefined (x, tp) -> BCdefined (x, subst_patches s tp)
 | BCalias cu -> BCalias (subst_constant s cu)
 | BCconstant -> BCconstant
+| BChole -> BChole
 
 let to_memory fv code =
   let env = {

diff --git a/kernel/vmemitcodes.mli b/kernel/vmemitcodes.mli
@@ -26,6 +26,7 @@ type 'a pbody_code =
   | BCdefined of ('a * patches)
   | BCalias of Constant.t
   | BCconstant
+  | BChole
 
 type body_code = to_patch pbody_code
 

diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
@@ -270,6 +270,7 @@ let rec slot_for_getglobal env sigma kn envcache table =
            set_global v table
         | BCalias kn' -> slot_for_getglobal env sigma kn' envcache table
         | BCconstant -> set_global (val_of_constant kn) table
+        | BChole -> set_global (val_of_atom Ahole) table
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (CEphemeron.create pos);