Any way to get the RDY signal for a method?

[myrfy001]

It would be very useful to have a way to test if a method can be called.

For example, FIFOF interface have notFull/notEmpty methods, which can be used before accessing deq or enq to prevent a rule from blocking. But we can't get the ready signal for arbitrary methods.

If we can get the the ready signal for arbitrary methods, writting an fix priority arbiter will be a lot eaisier with some if statement in an single rule.

[quark17]

There is a function impCondOf in the Prelude, that takes an expression (of any type) and returns the implicit condition of the expression (as Bool). Can you see if that works for you?

For synthesized submodules, it would be safe to call impCondOf(f.enq), but to be safe you should call impCondOf on fully applied expressions, so include the argument to any function or method, like this:

impCondOf(f.enq(x))

That's because, a function doesn't have implicit conditions, it's the return result of the function that has the implicit condition.

I'm also not sure how impCondOf handles conditional method calls. When you call BSC, by default it builds conditions conservatively (not taking into account the condition on method calls), but you can give the flag --aggressive-conditions to have BSC build the conditions aggressively (and there may be attributes to control this in the source, I can't recall if we support that or just intended to). Comments in the BSC source code claim that impCondOf returns the aggressive condition, and does not consult the flag choice. That's something to look into (and file an enhancement request if necessary). If you're just using it on methods of synthesized submodules, then that wouldn't matter.

Oh, I guess it's because -- to use this function -- you will need aggressive conditions. Because if you write something like this:

if (impCondOf(f.enq(x)))
  f.enq(x)
else
  do_something_else;

this code still contains a call to f.enq(x) and will therefore pick up its implicit condition. It is necessary to construct the implicit condition aggressively, for this code to do anything useful.

I also notice that back in 2010 there was a proposal to support unGuard in place of impCondOf. The function unGuard looked like this (in BH/Classic):

unGuard :: (a -> b) -> a -> b -> b
unGuard fn v alt = ...

This primitive would return fn applied to v (with no implicit condition), when the implicit condition is True; and would return alt when the implicit condition is False. I don't recall why this form was proposed, but I think it has to do with wanting to avoid picking up the implicit condition of f.enq(x) when you do choose to call it -- probably so that it could be used in rules marked with the no_implicit_conditions attributes. This was probably back before BSC was using an SMT solver to check these kinds of assertions; BSC was probably looking for constant True as the condition, but was finding an expression that hadn't been fully simplified. With aggressive conditions, the above block of code should produce the implicit condition (assuming that do_something_else has no conditions):

if f.not_full then f.not_full else True

I'm not sure why this would have been a problem for BSC, even before SMT solvers, but also maybe BSC wasn't doing much logic reduction before checking for just the expression True. Certainly now, the SMT solver would notice that it is always satisfied. But I guess the idea with unGuard is that it would (safely) prevent the condition from being picked up in the first place.

So try impCondOf and see if that works for you? If not, we can look at fixing any issues or maybe implementing unGuard, depending on what you run into. (There is a draft implementation for unGuard from 2010, that could be used as a starting point.)

[mieszko]

I think personally I would prefer a simpler version of this:

unguard :: a -> Maybe a

This would naturally turn a Wire into an RWire; also, given that Maybe is a Monad instance, one could write particularly elegant code.

If we also stole

maybe :: b -> (a -> b) -> Maybe a -> b 

from Haskell then you can use maybe alt f ∘ unguard to transform the value inside.

It would be even nicer if we could also do the reverse: that is, have a

guard :: Maybe a -> a

where guard would attach an implicit condition that is true iff the value is a Just.

[quark17]

I think you can write guard like this:

guard m = when (isValid m) (validValue m)

[quark17]

And your unguard could be written from the proposed unGuard as follows:

unguard x = unGuard Just x Nothing

And I think it can also be written currently, as follows:

unguard x = if (impCondOf x) then (Just x) else Nothing

The difference is that the second version would still pick up the implicit condition (but hopefully aggressive conditions would make it do what you want); with unGuard, the condition would not be picked up in the first place.

[mieszko]

hmm but does when work like that?

package Guard(guard) where

guard :: Maybe a -> a
guard m = when (isValid m) (validValue m)

gives me this:

Error: "Guard.bs", line 4, column 10: (P0005)
  Unexpected "when"; expected "\" or "interface"

I also tried this:

guard m = (validValue m) when (isValid m)

also unexpected when.

[quark17]

Ah, when is a keyword in Classic. Try _when_, which is defined in Prelude.bs. That's used to define when in PreludeBSV.bs, which is available in BSV. Sorry, I don't use Classic enough! I also wasn't sure whether you could have a bare Just or needed (\v -> Just v).

[mieszko]

oh cool I didn't know about _when_, i should have looked in Prelude.bs. TIL, thanks!

your unguard indeed works but does in fact require aggressive conditions; would be nice if it didn't. i forget why these are not default anyway.

now if i could just access the values of a module's method inputs elsewhere in the module... unless that works too somehow?

my original point, though, was that in terms of potential inclusion in std libs i would prefer the variant of unguard with Maybe over the one with a HOF, as i think it would result in easier to read code; i realize they can be written in terms of each other.