BitC as kind-level naturals? How did I miss that! Or is this something
that's coming soon? You can verify a lot of interesting properties with
type-level naturals, so that would be pretty nice to have.
Sandro
On 2010-10-29 1:40 AM, Jonathan S. Shapiro wrote:
> This is a *great* question. We have a paper solution, but none that is
> currently implemented in BitC.
>
> The issue you raise (assuming that I have understood you properly) isn't
> really specific to ring buffers. It actually has two parts:
>
> 1. Parameterizing over array sizes
> 2. Dealing with *dynamically* sized arrays.
>
> The first part is simple: as we introduced the 'nat' kind, arrays will
> fold into the language more naturally, and it will be possible to write
> something like (don't hold me to syntax here):
>
> struct S('len:nat)
> is
> len: 'len
> a: array(char, 'len)
>
> you can then instantiate S(5) or S(6) or ...
> [...]
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
