Size of uint8 in memory

I’m trying to understand how all the basic types are are specified, in
order to understand the size of representation.

I have put here the components for uint8, and I want to make sure I
understand these.

My understanding is:

  • typedef uint8_t… ultimately enters uint8_t into the lexicon of types,
    and that it will be the ultimate size in memory, because the code generator
    will generate code with uint8_t

  • abst@ype atstkind_t0yte defines and abstract type, and its main purpose
    is to denote a type that is non boxed

  • typedef tkind_t0ype (tk:tkind) converts the abstract type to a sort
    ’type’ for a non-boxed

  • g0uint_t0pe puts an abstract wrapper around kind_t0ype, but I am not sure
    how it helps

  • typedef g1uint, g1uint0, g1uint1 each add constraints to the previous
    abstract type via its alias

  • sortdef uint8 finally puts uint8 into the system as a sort

  • tkindef uint8_kind creates a kind/type that creates a type that is
    connected to uint8_t so that the compiler can generate a uint8_t

  • uint8_0 passes the uint8_kind int u0uint so that now the compiler knows
    the type is not boxed which I think means u0uint is a constructor of a type
    constructing a type using uint8, which is a uint8_t

  • Finally we have more aliases for uint8 = uint8_1 _0, etc, which I assume
    with uint8 defined multiple times, the compiler must be able to use context
    to figure out which one applies

So I believe that ultimately, if I use uint8, it will generate uint8_t, and
that means addition of numbers resulting in a value larger than sizeof
uint8_t will overflow and wrap, if that is what the C compiler generated
machine code does. Therefore, we can reason about uint8 as if it were a
uint8_t.

Is my understanding of this correct?

Why go from type to abs to type again? I assume that abs is just an alias,
and type is of sort. But this just makes a lot of names and gets confusing.
What is the reason for such a rich vocabulary?

typedef uint8_t atstype_uint8 ;

abstype atstkind_type (tk: tkind)
abst@ype atstkind_t0ype (tk: tkind)
//
typedef
tkind_type (tk:tkind) = atstkind_type (tk)
typedef
tkind_t0ype (tk:tkind) = atstkind_t0ype (tk)

abst@ype
g0uint_t0ype (tk:tkind) = tkind_t0ype (tk)
stadef g0uint = g0uint_t0ype // shorthand
abst@ype
g1uint_int_t0ype (tk:tkind, int) = g0uint (tk)
stadef g1uint = g1uint_int_t0ype // shorthand
//
typedef g1uint (tk:tk) = [i:int] g1uint (tk, i)
typedef g1uint0 (tk:tk) = [i:int | i >= 0] g1uint (tk, i)
typedef g1uint1 (tk:tk) = [i:int | i >= 1] g1uint (tk, i)

sortdef uint8 =
{ i:int | 0 <= i; i < 256 }

tkindef
uint8_kind = "atstype_uint8"
typedef
uint8_0 = g0uint (uint8_kind)
typedef
uint8_1 (i:int) = g1uint (uint8_kind, i)
stadef uint8 = uint8_1 // 2nd-select
stadef uint8 = uint8_0 // 1st-select
stadef uInt8 = [i:nat] uint8_1 (i)

Yes, your understanding is right. The complexity you saw is mostly for supporting templates.------ Original message------From: Mike JonesDate: Fri, Oct 2, 2015 3:08 PMTo: ats-lang-users;Subject:Size of uint8 in memory
I’m trying to understand how all the basic types are are specified, in order to understand the size of representation.
I have put here the components for uint8, and I want to make sure I understand these.
My understanding is:

  • typedef uint8_t… ultimately enters uint8_t into the lexicon of types, and that it will be the ultimate size in memory, because the code generator will generate code with uint8_t
  • abst@ype atstkind_t0yte defines and abstract type, and its main purpose is to denote a type that is non boxed
  • typedef tkind_t0ype (tk:tkind) converts the abstract type to a sort ‘type’ for a non-boxed
  • g0uint_t0pe puts an abstract wrapper around kind_t0ype, but I am not sure how it helps
  • typedef g1uint, g1uint0, g1uint1 each add constraints to the previous abstract type via its alias
  • sortdef uint8 finally puts uint8 into the system as a sort
  • tkindef uint8_kind creates a kind/type that creates a type that is connected to uint8_t so that the compiler can generate a uint8_t
  • uint8_0 passes the uint8_kind int u0uint so that now the compiler knows the type is not boxed which I think means u0uint is a constructor of a type constructing a type using uint8, which is a uint8_t
  • Finally we have more aliases for uint8 = uint8_1 _0, etc, which I assume with uint8 defined multiple times, the compiler must be able to use context to figure out which one applies
    So I believe that ultimately, if I use uint8, it will generate uint8_t, and that means addition of numbers resulting in a value larger than sizeof uint8_t will overflow and wrap, if that is what the C compiler generated machine code does. Therefore, we can reason about uint8 as if it were a uint8_t.
    Is my understanding of this correct?
    Why go from type to abs to type again? I assume that abs is just an alias, and type is of sort. But this just makes a lot of names and gets confusing. What is the reason for such a rich vocabulary?

typedef uint8_t atstype_uint8 ;
abstype atstkind_type (tk: tkind)abst@ype atstkind_t0ype (tk: tkind)//typedeftkind_type (tk:tkind) = atstkind_type (tk)typedeftkind_t0ype (tk:tkind) = atstkind_t0ype (tk)
abst@ypeg0uint_t0ype (tk:tkind) = tkind_t0ype (tk)stadef g0uint = g0uint_t0ype // shorthandabst@ypeg1uint_int_t0ype (tk:tkind, int) = g0uint (tk)stadef g1uint = g1uint_int_t0ype // shorthand//typedef g1uint (tk:tk) = [i:int] g1uint (tk, i)typedef g1uint0 (tk:tk) = [i:int | i >= 0] g1uint (tk, i)typedef g1uint1 (tk:tk) = [i:int | i >= 1] g1uint (tk, i)
sortdef uint8 = { i:int | 0 <= i; i < 256 }
tkindefuint8_kind = "atstype_uint8"typedefuint8_0 = g0uint (uint8_kind)typedefuint8_1 (i:int) = g1uint (uint8_kind, i)stadef uint8 = uint8_1 // 2nd-selectstadef uint8 = uint8_0 // 1st-selectstadef uInt8 = [i:nat] uint8_1 (i)

You received this message because you are subscribed to the Google Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/8455c6a0-e4da-43a5-8465-5c67a0db1867%40googlegroups.com.