[bitc-dev] Re: BitC issues

[Swaroop Sridhar]

Jonathan S. Shapiro wrote:
> Swaroop:
> 
> 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)
> 
> 
> Both
> 
> 	(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?

ex:
type ppage (addr: long, perm: byte)
type vpage (addr: long, perm: byte)

where
((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:

(let prq
   (lambda x
      (if (match x (PAGE y))
         (if (match y[25] (PTE z))
	      z)

instead of

let pqr (lambda x:ppage x[25].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).