Implementations of concepts and transformations discussed in #83

[snowleopard]

@jrbeaumont I think the current version of enable is too strict: not only it restricts the behaviour of outputs, it can also prevent inputs from firing, which is probably undesirable.

Perhaps, it would be a more useful function if it can be used in a more targeted way, for example by applying it only to specified output (or a set of outputs): enable e [q, nq] $ srLatch s r q nq. Imagine applying it to all signals in this case -- this would mean inputs can never fire!

It is similar to bubble/bubbles in the sense that it is commutative. But it is idempotent (enabling twice is the same as enabling once), whereas bubble is an involution, i.e. it's a self-inverse (inverting an input twice is a no-op).

[jrbeaumont]

@snowleopard: I didn't think of this! Thank you for pointing it out. Targeting it to specific signals would be a much better idea, or if possible, aiming it only at output/internal signals. However, this is much more difficult to do, as we cannot guarantee that the interface concepts will be included in the concept which is passed into enable.

p.s. idempotent and involution are fantastic words :)

[jrbeaumont]

@snowleopard I have made some changes, let me know what you think.

[snowleopard]

Wait. The new enable t s c can probably be implemented simply as c <> (t ~> rise s <> t ~> fall s). What do you think?

[snowleopard]

Which brings me to another useful variant of enable, which we can call sync. It can be implemented similarly: sync x y c = c <> (rise x ~> rise y <> fall x ~> fall y).

Simplifying even further: sync x y c = c <> buffer x y.

Now you can express meElement as sync r1 g1 $ sync r2 g2 $ mutex g1 g2 :)

It doesn't look like a major step forward, but I think it's a fairly flexible higher-order transformation that can make some specifications easier to understand.

[snowleopard]

I realised there is a subtle difference between the current implementation and the one I proposed above.

Currently, enable t s mempty == mempty.

In the above proposal, enable t s mempty = t ~> rise s <> t ~> fall s.

I'm unsure which one is preferable.

@jrbeaumont Any thoughts?

[jrbeaumont]

An enable for a single output can be done, it makes more sense to have it this way, but I would like to have enables like you said, for symmetry.

Wait. The new enable t s c can probably be implemented simply as c <> (t ~> rise s <> t ~> fall s).

This makes a lot more sense. An output will have constraints on both rise and fall transitions, so it only makes sense to generalise it, and make it more efficient, and ensure that the enable signal applies to both of it's transitions.

Sync seems interesting, I am not sure I quite understand it's use in this example. It seems to just replace buffer, but not use standard <> operator. Is it an idea to synchronise signals?

As far as for mempty, I am also unsure. I think ideally, if someone is to use enable on it's own, it should produce a result, it could be seen as a buffer in some cases, i.e. s indicates the polarity of t, so it is identifiable whether the circuit is enabled.

[jrbeaumont]

I have changed enable, and added enables and sync

[jrbeaumont]

The clearer srLatch implementation has been added.

[snowleopard]

@jrbeaumont Thanks, looks good!