bluespec.com Forum Index bluespec.com
Bluespec Forums
 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister 
 ProfileProfile   Log in to check your private messagesLog in to check your private messages   Log inLog in 

Recursion with vectors

 
Post new topic   Reply to topic    bluespec.com Forum Index -> Tools: BSC (Bluespec Compiler)
View previous topic :: View next topic  
Author Message
tomahawkins



Joined: 14 Dec 2012
Posts: 21

PostPosted: Sat Mar 30, 2013 11:52 pm    Post subject: Recursion with vectors Reply with quote

I'm struggling with numeric types with recursive functions. I want to build a function that sums up all pairs of bytes in a byte vector:

Code:

typedef Bit#(8) Byte;
typedef Vector#(n, Byte) ByteVector#(numeric type n);

function Bit#(16) sum16(ByteVector#(n) a);
  if (valueof(n) == 0)
    return 0;
  else if (valueof(n) == 1)
    return {a[0], 8'b0};
  else
    return {a[0], a[1]} + sum16(tail(tail(a)));
endfunction


But the compiler complains:

Code:

Error: "CRCTest.bsv", line 8, column 19: (T0030)
  The provisos for this expression are too general.
  Given type:
    function Bit#(16) f(Utils::ByteVector#(n) x1)
  The following provisos are needed:
    Add#(1, a__, b__)
      Introduced at the following locations:
   "CRCTest.bsv", line 14, column 33
    Add#(1, b__, n)
      Introduced at the following locations:
   "CRCTest.bsv", line 14, column 38
  The type variables are from the following positions:
    "a__" at "CRCTest.bsv", line 14, column 27
    "b__" at "CRCTest.bsv", line 14, column 33


What provisos do I need to add to help the type checker along?

-Tom
Back to top
View user's profile Send private message
SteveA



Joined: 03 May 2007
Posts: 32

PostPosted: Sun Mar 31, 2013 11:39 am    Post subject: polymorphism Reply with quote

Read the examples on this page, section 11, on polymorphism:

http://bluespec.com/SmallExamples/index.html

The compiler has told you, fortunately, what privisos are needed with these lines:

Add#(1, a__, b__)
Add#(1, b__, n)


But a common issue is that the variables mentioned by the error message with the __ in them (ie a__ and b__) are just made up internal names.. This will be consistent for this compiler run, meaning you could literally cut and paste these into your provisos list for the function (functions can have provisos also Wink, but if you get another error later, these internal variables are not likely to be the same as the previously mentioned a__..

As a result, I tend to create my own variable names, that I won't use, but they are different than the internal names so they don't overlap with future compiles.. IE

Add#(1, unusedA, unusedB)
Add#(1, unusedB, n)

And the error message tells you which line has the requirement for the requested provisos.. If n is a static variable (compile time elaborated), then different values of n might mean different provisos are needed.. Be sure to test build a few cases with different values of n...

_________________
Steve Allen
Senior Consulting Engineer
Bluespec, Inc
Back to top
View user's profile Send private message
tomahawkins



Joined: 14 Dec 2012
Posts: 21

PostPosted: Sun Mar 31, 2013 1:03 pm    Post subject: Reply with quote

Without any provisos in this function:

Code:

function Bit#(16) sum16(ByteVector#(n) a);
  if (valueof(n) == 0)
    return 0;
  else if (valueof(n) == 1)
    return {a[0], 8'b0};
  else begin
    return {a[0], a[1]} + sum16(tail(tail(a)));
  end
endfunction


...BSC tells me to add these:

Code:

Add#(1, a__, b__)
Add#(1, b__, n)


When I add these provisos, BSC tells me to add more:

Code:

Add#(1, c__, a__)
Add#(1, d__, c__)


And when I add these new provisos, again, BSC tells me to add more:

Code:

Add#(1, e__, f__)
Add#(1, f__, d__)


I'm not sure how to break this loop.

It would help to see how some of the recursive Vector functions are implemented in the standard library. Are these available somewhere? I see nothing but *.bo files in the distribution.

-Tom
Back to top
View user's profile Send private message
SteveA



Joined: 03 May 2007
Posts: 32

PostPosted: Sun Mar 31, 2013 1:54 pm    Post subject: Reply with quote

Ah right... I'm not the expert with BSV and recurse, but I think this does the same (if you are desperate for a solution)

function Bit#(16) sum16(ByteVector#(n) invec) provisos(
Div#(n, 2, m),
Add#(1, a__, m) // must be at least one for this to work
);
function Bit#(16) func1( Byte a, Byte b ) = return { a, b };
function Bit#(16) func2( Byte a ) = return { a, 8'b0 };
Vector#(m,Bit#(16)) vx = mapPairs( func1, func2, invec );
return fold( \+ , vx );
endfunction

recursion wise, I suspect it has to do with the actually act of recursion creating several calls and needing a tighter definition of the provisos (without using {}).. Often it helps to explicitly call out variable types used (rather than let the compiler infer them).. I'll fiddle with it later today when I have some more time...

_________________
Steve Allen
Senior Consulting Engineer
Bluespec, Inc
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Mon Apr 01, 2013 12:29 pm    Post subject: Re: Recursion with vectors Reply with quote

I suspect that what you should do is convert the Vector to a List (which does not have the length in its type) and then call a recursive "sum16" function on the List. Perhaps like this:
Code:
function Bit#(16) sum16(ByteVector#(n) a);
  List#(Byte) bs = toList(a);
  return sum16List(bs);
endfunction

function Bit#(16) sum16List(List#(Byte) bs);
  Integer len = length(bs);
  if (len == 0)
    return 0;
  else if (len == 1)
    return {bs[0], 8'b0};
  else
    return {bs[0], bs[1]} + sum16List(List::tail(List::tail(bs)));
endfunction


For a discussion of the problem and some other possible solutions, have a look at this comment on a similar forum post: http://bluespec.com/forum/viewtopic.php?p=1076#1076.

In your example, the provisos are required because you used the function "tail" in your code. In order to take the "tail" of a Vector, the length has to be at least 1. The way that this is expressed as a proviso is:
Code:
Add#(1, j, length)

This is saying that, there's some length "j" to which you can add 1 to get the length of the Vector; and since numeric types can be 0 but not negative (so "j" can be 0 but not negative), this guarantees that the Vector length is at least 1.

But since you used "tail" twice, that means that you are taking the tail of the resulting Vector of length "j" (from the first call to "tail"), so "j" also must be at least 1. So you have two provisos:
Code:
Add#(1, j, length)
Add#(1, k, j)

The names are called "a__", "b__", etc in the error message (instead of "j" and "k") because that's how BSC picks names for new variables that are mentioned in the code (and so they don't have names that you gave them).

The problem is that your function has an if-else structure. In the last arm of the if-else tree, you have called "tail" twice, which introduces provisos. But provisos are a static requirement; there is no way to say that the provisos only apply if the last if-else arm is taken; the proviso becomes a requirement for all arms.

Or, to put it another way: The types of the two arms of an if-expression are required to be the same -- if one arm is returning Bit#(16) then the other arm also has to return Bit#(16) -- and this includes the provisos, because provisos are part of the type.

So, because one arm requires the Vector length to be at least 2, the entire function has to require that. And this is where the problem comes when you try to recurse: Not only does "length" need to be at least 2, but when you take the tail twice and recursively call "sum16" on a Vector of length "k", the provisos of "sum16" require that "k" also be at least 2. There's no way to get to the base case.

So, that forum post explains several ways to get around the issue:

(1) When you recursively call the function, don't call it on a smaller length ("k"), always call it on the original length; that way, you're not introducing new provisos when you recursively call the function.

(2) Use a typeclass. I said that you can't conditionally pick the provisos, but typeclasses are the one exception.

(3) Or don't introduce the provisos in the first place, by converting the Vector to a type, like List, that doesn't have the length as part of its type. (And so calls to "tail" do not introduce any provisos.)
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Mon Apr 01, 2013 12:33 pm    Post subject: Re: Recursion with vectors Reply with quote

Steve, of course, provided a 4th option, which is not to write a recursive function at all, but to use Vector functions from the library (like "mapPairs" and "fold") which will do the iteration over the Vector for you.
Back to top
View user's profile Send private message
SteveA



Joined: 03 May 2007
Posts: 32

PostPosted: Mon Apr 01, 2013 1:47 pm    Post subject: Reply with quote

Excellent, Jacob! For some reason I always use Vector (must be the die hard old school hardware guy inside of me).. This is a great reason to become more familiar with List Smile
_________________
Steve Allen
Senior Consulting Engineer
Bluespec, Inc
Back to top
View user's profile Send private message
Display posts from previous:   
Post new topic   Reply to topic    bluespec.com Forum Index -> Tools: BSC (Bluespec Compiler) All times are GMT - 4 Hours
Page 1 of 1

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You can attach files in this forum
You can download files in this forum
bluespec.com topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group
Protected by Anti-Spam ACP