Implemented bubble function to invert a chosen signal's transitions

[jrbeaumont]

bubble is a concept transformation function which takes a signal and a concept and toggles all of the transitions for that signal, be they cause/effect transitions in a causality, in AND/OR causalities, for the given concept. This acts as a negation on the chosen signal, be it an input or output.

This serves well to provide inverting gates, for example:

bubble c (andGate a b c)
bubble a (orGate a b c)
bubble c (cElement a b c)

These will produce a NAND gate, an OR gate with one inverted input (a), and an inverting output C-element, respectively.

This can also be used in combination, for multiple inversions, e.g:

bubble b (bubble c (andGate a b c))

This will produce a NAND gate with one input (b) inverted.

[snowleopard]

Nice! But I think we should also toggle corresponding initial state bit, as well as the invariant.

[jrbeaumont]

I thought about this, and I agree with invariants in the chosen concept to bubble, but my issue with initial state is that you would have to include the whole concept, i.e. More than just the gate/protocol/concept you wish to bubble. This means that if you want to simply have a NAND gate, but a non-inverting C-element later on using the output of the NAND, it can become confusing, and you toggle every causality in the system.

[snowleopard]

Not sure I understand, can you give an example?

I don't see how the following doesn't work:

nAndGate a b c = bubble c $ andGate a b c

test a b c = bubble c (nAndGate a b c <> initialise0 [a, b, c])

[jrbeaumont]

Well I have just had a thought, and we can toggle all initial states and invariants in the given concept, which can be:

nAndGate a b c = bubble c $ andGate a b c

this will just toggle the causalities for c in the AND gate. Or we can use it as:

wholeSystem x y z = bubble z $ operation x y z <> initialise0 [x, y, z] <> never [rise y, rise z]

which will invert everything that z does.

[snowleopard]

Yes, inverting everything is the idea: it's the same as with dual but only for one signal.

[jrbeaumont]

I will implement it now.

[jrbeaumont]

I have implemented the invariant toggles, but I cannot find a way to invert the initial state for the given signal. The implementation for dual can do it regardless of signal, because it does all initial states. For bubble, I try to use the signal to find the initial state for just this signal, but it does not work, instead throwing compilation errors however I try to do it. I also need to keep the initial states that are not for the given signal as they are.

[snowleopard]

Well, invariant is a function that takes a signal as the input. Try to go this way:

bubbleInvariant :: Eq a => a -> (a -> InitialValue) -> (a -> InitialValue)
bubbleInvariant x f y = ...

[jrbeaumont]

@snowleopard There we go! All works well :)

[snowleopard]

@jrbeaumont Nice! I've added a couple of comments.

[jrbeaumont]

@snowleopard Fixed those issues :)

[jrbeaumont]

Rename done.

[snowleopard]

Thanks! Now merged.