[bitc-dev] Re: BitC issues
swaroop at cs.jhu.edu
Fri Dec 17 15:35:00 EST 2004
Jonathan S. Shapiro wrote:
> These notes should go to bitc-dev at coyotos.org
Sorry, I somehow forgot the mailing list altogether.
>>1) Consider the following example:
>>(datatype t1 (N int))
>>(datatype t2 (N int))
> This is illegal. The second datatype is a syntax error.
> The reason is that the *first* datatype binds the symbol N as an
> indentifier in the scope containing the datatype declaration. Because
> this identifier is bound, the second datatype is redefining a bound
> identifier, which is illegal.
This probably is illegal according to current BitC grammar. But, I think
the the top level definition of an expression language should be a let*
(sequential binding). In this case, the second definition should
'overrule' the first.
>>However if there was a way to declare new types, then
>>type pte (addr: long, perm: char)
>>type page (vector pte 1024)
> (typealias pte (addr : long, perm: char))
> (typealias page (vector pte 1024))
> are legal. See section 2.5.1 and section 2.5.3. By the way, I am fairly
> certain that you want 'byte', not 'char'.
I know this. However, my question was: Do we want a facility to declare
new type-names that DO NOT unify, WITHOUT having to use constructors?
type ppage (addr: long, perm: byte)
type vpage (addr: long, perm: byte)
((lambda x: ppage <do-something>) (y: vpage)) DOES NOT typecheck.
This is different from
typealias ppage (addr: long, perm: byte)
typealias vpage (addr: long, perm: byte)
I know that this can be done using datatypes. My only concern is about
the programmer, who has to write:
(if (match x (PAGE y))
(if (match y (PTE z))
let pqr (lambda x:ppage x.addr)
Another question about language implementation:
Does the specification require that the vectors and tuples be packed, or
is the compiler free to pad extra bytes for alignment? I think we need
both kinds of data structures for correctness and efficiency (unless we
want to do manual alignment).
More information about the bitc-dev