Examples wishlist

[j-hui]

Starting this meta-issue/thread as a place to collect examples which we want to be able to implement in our language.

[j-hui]

One-shot and its variations:

Basic one-shot:

oneShot :: SSMTime -> Bool -> Ref () -> Ref Bool -> SSM ()
oneShot delay low i o = while True $ do
  wait [i]
  o <~ not low
  after delay, o <~ low

---

A more type-generic version that acts more like a functor, mapping over values of the input reference:

oneShotMap :: SSMTime -> Exp b -> (Exp a -> Exp b) -> Ref a -> Ref b -> SSM ()
oneShotMap delay low f i o = while True $ do
  wait [i]
  o <~ f (deref i)
  after delay, o <~ low

We can redefine oneShot using oneShotMap:

oneShot delay low = oneShotMap delay low (const $ not low)

For the following variations, I'll use the type-specific version for brevity.

---

The above implementation will issue an additional instantaneous assignment if it receives two consecutive input signals before it is able to reset the output signal. While the additional assignment may seem redundant, it has the effect of waking up waiting processes (though with no change in value). That may or may not be desirable. This implementation ensures that only alternating assignments are made:

oneShot' :: SSMTime -> Exp Bool -> Ref () -> Ref Bool -> SSM ()
oneShot' delay low i o = while True $ do
  wait [i]
  when (deref o != low) $ o <~ not low
  after delay, o <~ low -- extends scheduled shut-off time

Note that if the scheduled o <~ low update takes place at the exact same time that input is received on i, o will be assigned to twice in the same instant, with different values.

---

Meahwhile, if we wanted to imitate the behavior of the one-shot circuit shown here, we need to make a few changes. First, the input needs to be a Ref Bool as well, to remain faithful to the circuit analogy. We only respond to rising edges. We also need to ignore repeated assignments of the same value. Secondly, we need to make sure that once we've received a rising edge input, we ignore subsequent input until we've written low value.

oneShotW :: SSMTime -> Exp Bool -> Ref Bool -> Ref Bool -> SSM ()
oneShotW delay low i o = while True $ do
  -- wait until i <~ true
  while True $ do
    wait [i]
    when (deref i) $ break

  -- raise o
  o <~ not low

  -- set alarm
  wake <- var ()
  after delay, wake <~ ()
  wait [wake]

  -- reset o
  o <~ low

Note that here we use an internal alarm rather than waiting on o, because we can't assume we are the only process writing to o. This inadvertently solves another issue: in the previous examples, we mixed instananeous assignments with delayed assignments to o, such that all processes would see the delayed o <~ low assignment, but only processes of lower priority would see the instananeous o <~ not low assignment, creating an odd asymmetry that leads to unexpected behavior. For instance, if o is an output LED with a higher priorirty output handler, the output handler would never turn on the LED, but will receive low signals to o that could clobber other concurrent signals.

The implementation of oneShotW is such that we only ever use instanenous assignment on o, so that only lower priority processes will be able to see writes by oneShotW to o. A high priority output handler still wouldn't be able to receive output to the LED, but at least the output handler is uniformly deaf to both o <~ not low and o <~ low.

---

The fact that oneShotW uses instantaneous assignment precludes the use of high priority output handlers for o that can only evaluate delayed updates. We can adjust the implementations of oneShotW and oneShot' to only use delayed assignment, parametrized by some small latency that is used in place of the instananeous assignment:

oneShotW_ :: SSMTime -> SSMTime -> Exp Bool -> Ref Bool -> Ref Bool -> SSM ()
oneShotW_ latency delay low i o = while True $ do
  -- wait until i <~ true
  while True $ do
    wait [i]
    when (deref i) $ break

  -- raise o
  after latency, o <~ not low

  -- set alarm
  wake <- var ()
  after delay, wake <~ ()
  wait [wake]

  -- reset o
  after latency, o <~ low

oneShot'_ :: SSMTime -> SSMTime -> Exp Bool -> Ref () -> Ref Bool -> SSM ()
oneShot'_ latency delay low i o = while True $ do
  wait [i]
  when (deref o != low) $ after latency, o <~ not low
  after (latency + delay), o <~ low

[j-hui]

On second thought, closing this in favor of continuing the thread in #19 .