diff options
| author | Matthieu Sozeau | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-15 18:59:00 +0530 |
| commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
| tree | 38a09851cb687921193b4368a93eed34ccd55a58 /kernel/cemitcodes.ml | |
| parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (diff) | |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2091440447..3c9692a5c6 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of pconstant type patch = reloc_info * int @@ -147,8 +147,8 @@ and slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal id = - enter (Reloc_getglobal id); +and slot_for_getglobal p = + enter (Reloc_getglobal p); out_int 0 @@ -320,7 +320,7 @@ let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> 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)) + | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) let subst_patch s (ri,pos) = match ri with @@ -329,19 +329,19 @@ 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 (fst (subst_con_kn s kn)), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = | BCdefined of to_patch - | BCallias of constant + | BCallias of pconstant | BCconstant let subst_body_code s = function | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias kn -> BCallias (fst (subst_con_kn s kn)) + | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted |