Typespecs Encoding in Core Erlang

Question

I am trying to understand how Erlang typespecs are encoded in Core Erlang and would like to find some information.

I consulted the Core Erlang specification, but as far as I can tell, typespecs are not discussed. This tutorial and paper do not refer to typespecs either.

Compiling the following Erlang module, simple.erl,

-module(simple).

-export([double/1, wrap/1]).

-type datum() :: integer() | float() | atom(). 

-spec double(integer() | float()) -> float().
double(A) -> A * 2.0.

-spec wrap(A)-> {a, A} when A :: datum().
wrap(A) -> {a, A}.

to Core Erlang (erlc +to_core simple.erl) yields the following:

module 'simple' 
    ['double'/1, 'wrap'/1]

attributes [
    'type' =
        [{'datum',{'type',{5,18},'union',[{'type',{5,18},'integer',[]}|[{'type',{5,30},'float',[]}|[{'type',{5,40},'atom',[]}]]]},[]}],
    'spec' =
        [{{'double',1},[{'type',{7,13},'fun',[{'type',{7,13},'product',[{'type',{7,14},'union',[{'type',{7,14},'integer',[]}|[{'type',{7,26},'float',[]}]]}]}|[{'type',{7,38},'float',[]}]]}]}],
    'spec' =
        [{{'wrap',1},[{'type',{10,11},'bounded_fun',[{'type',{10,11},'fun',[{'type',{10,11},'product',[{'var',{10,12},'a'}]}|[{'type',{10,17},'tuple',[{'atom',{10,18},'a'}|[{'var',{10,21},'a'}]]}]]}|[[{'type',{10,29},'constraint',[{'atom',{10,29},'is_subtype'}|[[{'var',{10,29},'a'}|[{'user_type',{10,34},'datum',[]}]]]]}]]]}]}]
    ]

'double'/1 =
    fun (_0) -> call 'erlang':'*'(_0, 2.00000000000000000000e+00)

'wrap'/1 =
    fun (_0) -> {'a', _0}
end

The user-defined datum() type is encoded as the key-value pair 'type' = [...] in the attributes list, as are the typespecs for double/1 and wrap/1. Is there any existing specification for translating Erlang typespecs into such an encoding?