ArduinoBasic.idr

||| A Straightforward translation of the
||| [ArduinoML](https://github.com/mosser/ArduinoML-kernel) use case
||| with a bit of syntax extension for a smooth DSL experience
module ArduinoBasic

import Data.Union

namespace model

  data SIGNAL = LOW | HIGH

  record Sensor where
    constructor MkSensor
    name : String
    pin : Integer

  record Actuator where
    constructor MkActuator
    name : String
    pin : Integer

  Brick : Type
  Brick = Union [Sensor, Actuator]

  record Action where
    constructor MkAction
    actuator : Actuator
    value : SIGNAL

  mutual

    record State where
      constructor MkState
      name : String
      transition : Transition
      actions : List Action

    record Transition where
      constructor MkTransition
      sensor : Sensor
      value : SIGNAL
      next : State

  record App where
    constructor MkApp
    name : String
    initial : State
    states : List State
    bricks : List Brick

namespace lang

  syntax when [s] is [sig] goto [t] = MkTransition s sig t
  syntax set [a] to [v] = MkAction a v
  syntax state [x] startsWith [as] and [t] = MkState x t as
  syntax app [x] withStates [ss] andBricks [bs] startsAs [s] = MkApp x s ss bs

namespace sample

  button : Sensor
  button = MkSensor "button" 9

  light : Actuator
  light = MkActuator "light" 12

  mutual

    offline : State
    offline = state "offline" startsWith [ set light to LOW ]
                and when button is HIGH goto online


    online : State
    online = state "online" startsWith [ set light to HIGH ]
                and when button is HIGH goto offline

  switchApp : App
  switchApp = app "Switch" withStates [offline, online]
                           andBricks [member button, member light]
                           startsAs offline