Redesign concept representation

[snowleopard]

At the moment concepts are represented by a concrete datatype:

-- Abstract concepts
-- * s is the type of states
-- * e is the type of events
data Concept s e = Concept
    {
        initial   :: s -> Bool,
        excited   :: e -> s -> Bool,
        invariant :: s -> Bool
    }

This is later used to define circuit concepts:

-- Circuit primitives
-- Parameter a stands for the alphabet of signals
newtype State a = State (a -> Bool)

data Transition a = Transition
    {
        signal   :: a,
        newValue :: Bool -- Transition x True corresponds to x+
    }

type CircuitConcept a = Concept (State a) (Transition a)

Although this works relatively well now, it is not very flexible. In particular, expressions that combine concepts together cannot be interpreted in different contexts. Consider the following example:

buffer :: Eq a => a -> a -> CircuitConcept a
buffer a b = rise a ~> rise b <> fall a ~> fall b

cElement :: Eq a => a -> a -> a -> CircuitConcept a
cElement a b c = buffer a c <> buffer b c

Given data Signal = X | Y | Z, we can only interpret cElement X Y Z as an expression of type CircuitConcept Signal, which is basically a state graph represented by a collection of Boolean functions.

This is not the only interpretation of interest. In particular, we might want to interpret cElement X Y Z as a compact description of an STG, which could be stored in a .g file for processing by standard tools like petrify or workcraft.

This brings up the following problem: how do we redesign concepts in such a way that cElement and other expressions become polymorphic and the following two interpretations become possible:

deriveFSM :: CircuitConcept c => c a -> FSM a
deriveSTG :: CircuitConcept c => c a -> STG a

The first one should be equivalent to the current interpretation, but the second one should produce an STG datatype instead. The implementation of both of these functions could in fact be as simple as id. Actual work will be done behind the scenes by magic Haskell type inference.

[jrbeaumont]

This is a good point, and it would be useful for us to describe signals as input, output or internal. For FSMs this doesn't make too much of a difference, but for STGs to be useful with tools such as petrify it could do with these distinctions.

This could also be useful with #19 as this is somewhat holding us back with memory concepts. If it possible to define some internal signals for resolving CSC conflicts, for example, and define this, then it can be included when producing an STG, or even a logic implementation.

We have a meeting later this week, in which we can discuss this. But we can meet earlier if possible and discuss this alone, as it is an important point somewhat holding back the development of this concepts tool.

[mvdan]

It's also holding me back for the dotG (STG) generation, so I was going to take a stab at this since I can't do anything else in concepts right now. I would say this is very specific to concepts and could get lengthy, so perhaps it's a good candidate for a quick meeting before Thursday. I'm free whenever. I'll let @snowleopard decide, since he's the busiest.