-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Sketch programming with Copilot
--   
--   This extends Copilot with a FRP-like interface which can be used to
--   implement simple standalone programs (sketches) for embedded boards.
--   
--   It is used by arduino-copilot and zephyr-copilot.
--   
--   Copilot is a stream (i.e., infinite lists) domain-specific language
--   (DSL) in Haskell that compiles into embedded C. Copilot contains an
--   interpreter, multiple back-end compilers, and other verification
--   tools. <a>https://copilot-language.github.io/</a>
@package sketch-frp-copilot
@version 1.0.11

module Sketch.FRP.Copilot.Types

-- | A value that changes over time.
--   
--   This is implemented as a <a>Stream</a> in the Copilot DSL. Copilot
--   provides many operations on streams, for example <a>&amp;&amp;</a> to
--   combine two streams of Bools.
--   
--   For documentation on using the Copilot DSL, see
--   <a>https://copilot-language.github.io/</a>
type Behavior t = Stream t

-- | A Behavior with an additional phantom type <tt>p</tt>.
--   
--   The Compilot DSL only lets a Stream contain basic C types, a
--   limitation that <a>Behavior</a> also has. When more type safely is
--   needed, this can be used.
data TypedBehavior (p :: k) t
TypedBehavior :: Behavior t -> TypedBehavior (p :: k) t

-- | A discrete event, that occurs at particular points in time.
data Event (p :: k) v
Event :: v -> Stream Bool -> Event (p :: k) v

-- | A sketch, implemented using Copilot.
--   
--   It's best to think of the <tt>Sketch</tt> as a description of the
--   state of the board at any point in time.
--   
--   Under the hood, the <tt>Sketch</tt> is run in a loop. On each
--   iteration, it first reads inputs and then updates outputs as needed.
--   
--   While it is a monad, a Sketch's outputs are not updated in any
--   particular order, because Copilot does not guarantee any order.
--   
--   This is a generalized Sketch that can operate on any type of context.
newtype GenSketch ctx t
GenSketch :: WriterT [(TriggerLimit -> Spec, TriggerLimit -> GenFramework ctx)] (State UniqueIds) t -> GenSketch ctx t
class Ord ctx => Context ctx

-- | Things that can have a <a>Behavior</a> or <a>Event</a> output to them.
class Output ctx o t

-- | Connect a <a>Behavior</a> or <a>Event</a> to an <a>Output</a>
--   
--   <pre>
--   led =: blinking
--   </pre>
--   
--   When a <a>Behavior</a> is used, its current value is written on each
--   iteration of the <tt>Sketch</tt>.
--   
--   For example, this constantly turns on the LED, even though it will
--   already be on after the first iteration, because <a>true</a> is a
--   <a>Behavior</a> (that is always True).
--   
--   <pre>
--   led =: true
--   </pre>
--   
--   To avoid unncessary work being done, you can use an <a>Event</a>
--   instead. Then the write only happens at the points in time when the
--   <a>Event</a> occurs. To turn a <a>Behavior</a> into an <a>Event</a>,
--   use <a>@:</a>
--   
--   So to make the LED only be turned on in the first iteration, and allow
--   it to remain on thereafter without doing extra work:
--   
--   <pre>
--   led =: true @: firstIteration
--   </pre>
(=:) :: Output ctx o t => o -> t -> GenSketch ctx ()
infixr 1 =:
class Input ctx o t

-- | The list is input to use when simulating the Sketch.
input' :: Input ctx o t => o -> [t] -> GenSketch ctx (Behavior t)

-- | The framework of a sketch.
--   
--   This is a generalized Framework that can operate on any type of
--   context.
data GenFramework ctx
Framework :: [CChunk] -> [CChunk] -> [CChunk] -> Map ctx (Set PinMode) -> [CChunk] -> GenFramework ctx

-- | Things that come before the C code generated by Copilot.
[defines] :: GenFramework ctx -> [CChunk]

-- | Things to do at setup, not including configuring pins.
[setups] :: GenFramework ctx -> [CChunk]

-- | Things to do at setup, before the setups.
[earlySetups] :: GenFramework ctx -> [CChunk]

-- | How pins are used.
[pinmodes] :: GenFramework ctx -> Map ctx (Set PinMode)

-- | Things to run in <tt>loop</tt>.
[loops] :: GenFramework ctx -> [CChunk]
newtype UniqueIds
UniqueIds :: Map String Integer -> UniqueIds
newtype UniqueId
UniqueId :: Integer -> UniqueId
data TriggerLimit
TriggerLimit :: Behavior Bool -> TriggerLimit
NoTriggerLimit :: TriggerLimit
data PinMode
InputMode :: PinMode
InputPullupMode :: PinMode
OutputMode :: PinMode

-- | A line of C code.
newtype CLine
CLine :: String -> CLine
[fromCLine] :: CLine -> String

-- | A chunk of C code. Identical chunks get deduplicated.
newtype CChunk
CChunk :: [CLine] -> CChunk

-- | This type family is open, so it can be extended when adding other data
--   types to the IsBehavior class.
type family BehaviorToEvent a
class IsBehavior behavior

-- | Generate an Event, from some type of behavior, that only occurs when
--   the <a>Behavior</a> Bool is True.
(@:) :: IsBehavior behavior => behavior -> Behavior Bool -> BehaviorToEvent behavior
data PinCapabilities
DigitalIO :: PinCapabilities
AnalogInput :: PinCapabilities
PWM :: PinCapabilities
type family IsDigitalIOPin (t :: [PinCapabilities])
type family IsAnalogInputPin (t :: [PinCapabilities])
type family IsPWMPin (t :: [PinCapabilities])
type family HasPinCapability (c :: t) (list :: [t]) :: Bool
type family SameCapability (a :: PinCapabilities) (b :: PinCapabilities) :: Bool
instance GHC.Internal.Base.Applicative (Sketch.FRP.Copilot.Types.GenSketch ctx)
instance GHC.Classes.Eq Sketch.FRP.Copilot.Types.CChunk
instance GHC.Classes.Eq Sketch.FRP.Copilot.Types.CLine
instance GHC.Classes.Eq Sketch.FRP.Copilot.Types.PinCapabilities
instance GHC.Classes.Eq Sketch.FRP.Copilot.Types.PinMode
instance GHC.Internal.Base.Functor (Sketch.FRP.Copilot.Types.GenSketch ctx)
instance Sketch.FRP.Copilot.Types.IsBehavior (Sketch.FRP.Copilot.Types.Behavior v)
instance forall k (p :: k) v. Sketch.FRP.Copilot.Types.IsBehavior (Sketch.FRP.Copilot.Types.TypedBehavior p v)
instance GHC.Internal.Base.Monad (Sketch.FRP.Copilot.Types.GenSketch ctx)
instance Control.Monad.State.Class.MonadState Sketch.FRP.Copilot.Types.UniqueIds (Sketch.FRP.Copilot.Types.GenSketch ctx)
instance Control.Monad.Writer.Class.MonadWriter [(Sketch.FRP.Copilot.Types.TriggerLimit -> Copilot.Language.Spec.Spec, Sketch.FRP.Copilot.Types.TriggerLimit -> Sketch.FRP.Copilot.Types.GenFramework ctx)] (Sketch.FRP.Copilot.Types.GenSketch ctx)
instance GHC.Internal.Base.Monoid Sketch.FRP.Copilot.Types.CChunk
instance Sketch.FRP.Copilot.Types.Context ctx => GHC.Internal.Base.Monoid (Sketch.FRP.Copilot.Types.GenFramework ctx)
instance GHC.Internal.Base.Monoid (Sketch.FRP.Copilot.Types.GenSketch ctx ())
instance GHC.Internal.Base.Monoid Sketch.FRP.Copilot.Types.TriggerLimit
instance GHC.Classes.Ord Sketch.FRP.Copilot.Types.CChunk
instance GHC.Classes.Ord Sketch.FRP.Copilot.Types.CLine
instance GHC.Classes.Ord Sketch.FRP.Copilot.Types.PinCapabilities
instance GHC.Classes.Ord Sketch.FRP.Copilot.Types.PinMode
instance Sketch.FRP.Copilot.Types.Output ctx o (Sketch.FRP.Copilot.Types.Event () (Copilot.Language.Stream.Stream v)) => Sketch.FRP.Copilot.Types.Output ctx o (Sketch.FRP.Copilot.Types.Behavior v)
instance forall k ctx o (p :: k) v. Sketch.FRP.Copilot.Types.Output ctx o (Sketch.FRP.Copilot.Types.Event p (Copilot.Language.Stream.Stream v)) => Sketch.FRP.Copilot.Types.Output ctx o (Sketch.FRP.Copilot.Types.TypedBehavior p v)
instance GHC.Internal.Base.Semigroup Sketch.FRP.Copilot.Types.CChunk
instance Sketch.FRP.Copilot.Types.Context ctx => GHC.Internal.Base.Semigroup (Sketch.FRP.Copilot.Types.GenFramework ctx)
instance GHC.Internal.Base.Semigroup (Sketch.FRP.Copilot.Types.GenSketch ctx t)
instance GHC.Internal.Base.Semigroup Sketch.FRP.Copilot.Types.TriggerLimit
instance GHC.Internal.Show.Show Sketch.FRP.Copilot.Types.CChunk
instance GHC.Internal.Show.Show Sketch.FRP.Copilot.Types.CLine
instance GHC.Internal.Show.Show Sketch.FRP.Copilot.Types.PinCapabilities
instance GHC.Internal.Show.Show Sketch.FRP.Copilot.Types.PinMode

module Sketch.FRP.Copilot.Internals
getTriggerLimit :: TriggerLimit -> Behavior Bool
addTriggerLimit :: TriggerLimit -> Behavior Bool -> Behavior Bool

-- | Gets a unique id.
getUniqueId :: String -> GenSketch ctx UniqueId

-- | Generates a unique name.
uniqueName :: String -> UniqueId -> String
uniqueName' :: String -> UniqueId -> String

-- | Use to create an empty framework.
--   
--   It helps to specify the type of context to use:
--   
--   <pre>
--   (emptyFramework @Arduino) { ... }
--   </pre>
emptyFramework :: Context ctx => GenFramework ctx
mkCChunk :: [CLine] -> [CChunk]

-- | Copilot only supports calling a trigger with a given name once per
--   Spec; the generated C code will fail to build if the same name is used
--   in two triggers. This generates a unique alias that can be used in a
--   trigger.
defineTriggerAlias :: String -> GenFramework ctx -> GenSketch ctx (GenFramework ctx, String)
defineTriggerAlias' :: String -> String -> GenFramework ctx -> GenSketch ctx (GenFramework ctx, String)
data MkInputSource ctx t
InputSource :: [CChunk] -> [CChunk] -> Map ctx PinMode -> [CChunk] -> Stream t -> MkInputSource ctx t

-- | Added to the <a>Framework</a>'s <a>defines</a>, this typically defines
--   a C variable.
[defineVar] :: MkInputSource ctx t -> [CChunk]

-- | How to set up the input, not including pin mode.
[setupInput] :: MkInputSource ctx t -> [CChunk]

-- | How pins are used by the input.
[inputPinmode] :: MkInputSource ctx t -> Map ctx PinMode

-- | How to read a value from the input, this typically reads a value into
--   a C variable.
[readInput] :: MkInputSource ctx t -> [CChunk]

-- | How to use Copilot's extern to access the input values.
[inputStream] :: MkInputSource ctx t -> Stream t
mkInput :: MkInputSource ctx t -> GenSketch ctx (Behavior t)
evalSketch :: Context ctx => GenSketch ctx a -> (Maybe Spec, GenFramework ctx)

-- | Extracts a copilot <a>Spec</a> from a <tt>Sketch</tt>.
--   
--   This can be useful to intergrate with other libraries such as
--   copilot-theorem.
sketchSpec :: Context ctx => GenSketch ctx a -> Spec

module Sketch.FRP.Copilot

-- | Use this to make a LED blink on and off.
--   
--   On each iteration of the <tt>Sketch</tt>, this changes to the opposite
--   of its previous value.
--   
--   This is implemented using Copilot's <a>clk</a>, so to get other
--   blinking behaviors, just pick different numbers, or use Copilot
--   <a>Stream</a> combinators.
--   
--   <pre>
--   blinking = clk (period 2) (phase 1)
--   </pre>
blinking :: Behavior Bool

-- | True on the first iteration of the <tt>Sketch</tt>, and False
--   thereafter.
firstIteration :: Behavior Bool

-- | Use this to make an event occur 1 time out of n.
--   
--   This is implemented using Copilot's <a>clk</a>:
--   
--   <pre>
--   frequency = clk (period n) (phase 1)
--   </pre>
frequency :: Integer -> Behavior Bool

-- | Schedule when to perform different Sketches.
scheduleB :: (Typed t, Eq t, Context ctx) => Behavior t -> [(t, GenSketch ctx ())] -> GenSketch ctx ()

-- | Apply a Copilot DSL function to a <a>TypedBehavior</a>.
liftB :: (Behavior a -> Behavior r) -> TypedBehavior t a -> Behavior r

-- | Apply a Copilot DSL function to two <a>TypedBehavior</a>s.
liftB2 :: (Behavior a -> Behavior b -> Behavior r) -> TypedBehavior t a -> TypedBehavior t b -> Behavior r

-- | Limit the effects of a <tt>Sketch</tt> to times when a <a>Behavior</a>
--   <a>Bool</a> is True.
--   
--   When applied to <a>=:</a>, this does the same thing as <a>@:</a> but
--   without the FRP style conversion the input <a>Behavior</a> into an
--   <a>Event</a>. So <a>@:</a> is generally better to use than this.
--   
--   But, this can also be applied to <a>input</a>, to limit how often
--   input gets read. Useful to avoid performing slow input operations on
--   every iteration of a Sketch.
--   
--   <pre>
--   v &lt;- whenB (frequency 10) $ input pin12
--   </pre>
--   
--   (It's best to think of the value returned by that as an Event, but
--   it's currently represented as a Behavior, since the Copilot DSL cannot
--   operate on Events.)
whenB :: Context ctx => Behavior Bool -> GenSketch ctx t -> GenSketch ctx t
class IfThenElse (t :: Type -> Type) a

-- | This allows "if then else" expressions to be written that choose
--   between two Streams, or Behaviors, or TypedBehaviors, or Sketches,
--   when the RebindableSyntax language extension is enabled.
--   
--   <pre>
--   {-# LANGUAGE RebindableSyntax #-}
--   buttonpressed &lt;- input pin3
--   if buttonpressed then ... else ...
--   </pre>
ifThenElse :: IfThenElse t a => Behavior Bool -> t a -> t a -> t a

-- | Use this to read a value from a component of the board.
--   
--   For example, to read a digital value from pin12 and turn on the led
--   when the pin is high:
--   
--   <pre>
--   buttonpressed &lt;- input pin12
--   led =: buttonpressed
--   </pre>
--   
--   Some pins support multiple types of reads, for example a pin may
--   support a digital read (<a>Bool</a>), and an analog to digital
--   converter read (<tt>ADC</tt>). In such cases you may need to specify
--   the type of data to read:
--   
--   <pre>
--   v &lt;- input a0 :: Sketch (Behavior ADC)
--   </pre>
input :: Input ctx o t => o -> GenSketch ctx (Behavior t)

-- | A stream of milliseconds.
data MilliSeconds
MilliSeconds :: Stream Word32 -> MilliSeconds

-- | A stream of microseconds.
data MicroSeconds
MicroSeconds :: Stream Word32 -> MicroSeconds
data Delay
Delay :: Delay

-- | Use this to add a delay between each iteration of the <tt>Sketch</tt>.
--   A <tt>Sketch</tt> with no delay will run as fast as the hardware can
--   run it.
--   
--   <pre>
--   delay := MilliSeconds (constant 100)
--   </pre>
delay :: Delay
instance (Sketch.FRP.Copilot.Types.Context ctx, Copilot.Core.Type.Typed a) => Sketch.FRP.Copilot.IfThenElse (Sketch.FRP.Copilot.Types.GenSketch ctx) (Sketch.FRP.Copilot.Types.Behavior a)
instance Sketch.FRP.Copilot.Types.Context ctx => Sketch.FRP.Copilot.IfThenElse (Sketch.FRP.Copilot.Types.GenSketch ctx) ()
instance Copilot.Core.Type.Typed a => Sketch.FRP.Copilot.IfThenElse Copilot.Language.Stream.Stream a
instance Copilot.Core.Type.Typed a => Sketch.FRP.Copilot.IfThenElse (Sketch.FRP.Copilot.Types.TypedBehavior p) a
