diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 16:07:25 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | a91518d0b07b9a2cd7d9381044c20365771ec382 (patch) | |
| tree | b5abacb47818522d18533aecbcb7114ca0ca6b6a /pretyping | |
| parent | b0f3857eca168ee5d843e86b7678ac3d5375b07c (diff) | |
Readback for int31 values from native compiler.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index af7a99320..b635229cf 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -70,8 +70,15 @@ let type_constructor mind mib typ params = let construct_of_constr_notnative const env tag (mind, _ as ind) allargs = let mib,mip = lookup_mind_specif env ind in let nparams = mib.mind_nparams in - let i = invert_tag const tag mip.mind_reloc_tbl in let params = Array.sub allargs 0 nparams in + try + if const then + let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in + retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + else + raise Not_found + with Not_found -> + let i = invert_tag const tag mip.mind_reloc_tbl in let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in (mkApp(mkConstruct(ind,i), params), ctyp) |