
bluespec.com Bluespec Forums

View previous topic :: View next topic 
Author 
Message 
tomahawkins
Joined: 14 Dec 2012 Posts: 21

Posted: Sat Mar 30, 2013 11:52 pm Post subject: Recursion with vectors 


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 


SteveA
Joined: 03 May 2007 Posts: 32

Posted: Sun Mar 31, 2013 11:39 am Post subject: polymorphism 


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 , 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 


tomahawkins
Joined: 14 Dec 2012 Posts: 21

Posted: Sun Mar 31, 2013 1:03 pm Post subject: 


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 


SteveA
Joined: 03 May 2007 Posts: 32

Posted: Sun Mar 31, 2013 1:54 pm Post subject: 


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 


quark Site Admin
Joined: 02 Nov 2007 Posts: 499

Posted: Mon Apr 01, 2013 12:29 pm Post subject: Re: Recursion with vectors 


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:
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 ifelse structure. In the last arm of the ifelse 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 ifelse 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 ifexpression 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 


quark Site Admin
Joined: 02 Nov 2007 Posts: 499

Posted: Mon Apr 01, 2013 12:33 pm Post subject: Re: Recursion with vectors 


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 


SteveA
Joined: 03 May 2007 Posts: 32

Posted: Mon Apr 01, 2013 1:47 pm Post subject: 


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 _________________ Steve Allen
Senior Consulting Engineer
Bluespec, Inc 

Back to top 




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

Powered by phpBB © 2001, 2005 phpBB Group
