Thanks to all for the propositions !

I think I need to give a more concrete example to explain my pb and wishes.
Sorry, if this get a bit longish.

So, here's a small example in CAPH, involving a very single actor, performing addition on streams of signed, 8-bit integers :

---------- sizedint.cph -----------

actor foo ()
  in (a:signed<8>, b:signed<8>)
  out (c:signed<8>)
rules
  (a, b) -> c
| (x, y) -> x+y
;

stream i1:signed<8> from "sample1.txt";
stream i2:signed<8> from "sample2.txt";
stream o:signed<8> to "result.txt";

net o = foo (i1,i2);

---------- ------------ -----------

The VHDL code inferred for this example. In particular, the code describing the behavior of the foo actor will contain lines (lots of lines omitted here) :

---------- foo_act.vhd  -----------

entity foo_act is
   port (
    ...
    a: in std_logic_vector(7 downto 0);
    b: in std_logic_vector(7 downto 0);
    c: out std_logic_vector(7 downto 0);
    ...    );
end foo_act;

architecture FSM of foo_act is
   ...
    variable x_v : std_logic_vector(7 downto 0);
    variable y_v : std_logic_vector(7 downto 0);
    ...
    c <= x_v + y_v;
   ...
end FSM;

---------- ------------ -----------

If i replace 8 by 16 in the .cph source code, the generated code will be similar, except that the std_logic_vectors will (correctly) have range "15 downto 0".
The genericity of the "+" operator does the rest.

So far, so good.

But now suppose that the foo actor, instead of using directly the "+" operator calls a user-defined "add" function (which itself uses the "+" operator).

Here's the way to write this in CAPH : 

---------- sizedint.cph -----------

function add (x,y) = x+y : signed<8> * signed<8> -> signed<8>;

actor foo ()
  in (a:signed<8>, b:signed<8>)
  out (c:signed<8>)
rules
  (a, b) -> c
| (x, y) -> add(x,y)
;

stream i1:signed<8> from "sample1.txt";
stream i2:signed<8> from "sample2.txt";
stream o:signed<8> to "result.txt";

net o = foo (i1,i2);

---------- ------------ -----------

Again, this compiles and runs ok, with the an extra VHDL file generated, called sizedint_globals.vhd :

---------- sizedint_globals.vhd -----------

package sizedint_globals is
  function add(x:std_logic_vector(7 downto 0); y:std_logic_vector(7 downto 0)) return std_logic_vector;
end sizedint_globals;

package body sizedint_globals is
  function add(x:std_logic_vector(7 downto 0); y:std_logic_vector(7 downto 0)) return std_logic_vector is
  begin
    return x + y;
  end add;
end sizedint_globals;

---------- ------------ -----------

But now, suppose i now want to write the same program for 16 bit integers (as Oliver rightly points it out, one major advantage of hw programming is the ability to adjust datapath to applications to avoid waste of ressources).
For this, i will have to rewrite 

---------- sizedint.cph -----------

function add (x,y) = x+y : signed<16> * signed<16> -> signed<16>;

actor foo ()
  in (a:signed<16>, b:signed<16>)
  out (c:signed<16>)
rules
  (a, b) -> c
| (x, y) -> add(x,y)
;

stream i1:signed<16> from "sample1.txt";
stream i2:signed<16> from "sample2.txt";
stream o:signed<16> to "result.txt";

net o = foo (i1,i2);

---------- ------------ -----------
 
Of course, changing the type signature for foo and the I/Os is normal (after all, it's what i want).
But I would to like to avoid writing another add function (because i know that, at the VHDL level, my function is generic in size).
So i would like to be able to write sth like :

---------- sizedint.cph -----------

function add (x,y) = x+y : signed<s> * signed<s> -> signed<s>;

...

---------- ------------ -----------

and let the compiler infer, from the context in which add is called the value of s (and generated the right signature and impl in signedint_globals.vhd).

Jocelyn

 Le 27 sept. 11 à 16:13, oliver a écrit :

Hello,


On Tue, Sep 27, 2011 at 10:23:56AM +0200, Jocelyn Sérot wrote:

Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :

Phantom types could be a solution but we must declare a new type for
each possible size, which is cumbersome / annoying.

If you define the type system yourself, you can easily add a family of
type constants `size<n>` (with `n` an integer literal) to the default
environment of the type checker. Then you can define a parametrized
type `type 's sized_int` (or float, etc.) and instantiate it with any
of the size<n>.

Yes. Good point. Thanks for the idea.
IIUC, my add function would be declared as :

val add : 'a sized_int * 'a sized_int -> 'a sized_int

then, with

val x : size16 sized_int
val y : size16 sized_int

the type infered for z in

let z = add (x,y)

will be

z : size16 sized_int

Am i right ?
[...]

Not sure.

Depends on what you want ;-)

What would the type system
yield fopr a type for



val x : size16 sized_int
val y : size16 sized_int

let z = and_msb (x,y)  # AND the MSBs of both input values

z might be 16 Bits, if this is your "natural" int size - but: what is natural on
FPGA's, when you can change your HW at will?
And: if it's "batural", why to declare it?

But ANDing two Bits will result in a 1 Bit result.

Why should z be 16 Bits then?
That would be wasting ressources.

IMHO it does not make sense to derive the type of z from the type of
x and y. It must be derived from the operation or function that is used.


If you use  'a sized_int   then  this would offer you
the possibility also of taking 2 x 16 Bits and get 1 Bit (as in the and_msb()-example)
but of course also to do your

z = add (x,y) with z of 16 Bits, which you looked for.

But is thats a type that can be derived from x and y?

Or is it rather the OPERATION ("add" here), or better: the operation
together with the input values, that fives you the resulting type?

What if you do:

val x : size16 sized_int
val y : size8  sized_int

z = add(x, y)

What type does z no have?

8 Bits? 16 Bits?
Somewhere in between?


AFAIK one of the biggest (or better: THE) advantage of FPGAs/VHDL is:
you can create your "HW" (HW connections) by SW.

So you are not fixed in width, and you can save some bits here and there,
and use them later somewhere else...


And, I doubt, somehow, that what you are talking about is a "type issue".
At least nothing that can be derived from the structure of the inputs
without knowing the operation.

AFAIK you are not constrained to a fixed ALU and databus width,
at least not in a sense as we know it from fixed HW that we normally use
when buying a computer at the store.
(There may be limits of course, depending on the FPGA device in use.)


So, how do you address these issues?

I would say either you also need to define the type of z,
or you need to derive the type from the source of which
your operations/functions are derived.

So: you need more information than what you presented in your questions,
to decide for the resulting type.

Ciao,
  Oliver