{-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} -- | -- Copyright : (c) NASA, 2024-2025 -- License : BSD-style (see the LICENSE file in the distribution) -- -- Allow loading Copilot specifications from strings and modifying them live. -- -- An example of a spec that can be passed as argument to the live simulator -- follows: -- -- @ -- spec :: String -- spec = unlines -- [ "let temperature :: Stream Word8" -- , " temperature = extern \"temperature\" (Just [0, 15, 20, 25, 30])" -- , "" -- , " ctemp :: Stream Float" -- , " ctemp = (unsafeCast temperature) * (150.0 / 255.0) - 50.0" -- , "" -- , " trueFalse :: Stream Bool" -- , " trueFalse = [True] ++ not trueFalse" -- , "" -- , "in do trigger \"heaton\" (temperature < 18) [arg ctemp, arg (constI16 1), arg trueFalse]" -- , " trigger \"heatoff\" (temperature > 21) [arg (constI16 1), arg ctemp]" -- , " observer \"temperature\" temperature" -- , " observer \"temperature2\" (temperature + 1)" -- ] -- @ -- -- The imports are predefined. module Copilot.Visualize.Dynamic ( simInit , simStep , SimulationSettings(..) , mkDefaultSimulationSettings , SimData(..) ) where -- External imports import qualified Language.Haskell.Interpreter as HI import Prelude hiding (div, not, (++), (<), (>)) import qualified Prelude -- External imports: Copilot import qualified Copilot.Core as Core import Copilot.Language hiding (interpret, typeOf) import Language.Copilot hiding (interpret, typeOf) -- Internal imports import Copilot.Visualize.TypedTrace -- | Simulation data. data SimData = SimData { simSteps :: Int -- ^ Number of steps to simulate. , simSpec :: Core.Spec -- ^ Copilot spec to simulate. , simString :: String -- ^ Textual representation of Copilot spec. } -- | Initialize a simulation. simInit :: SimulationSettings -> String -> IO SimData simInit simulationSettings spec = do -- Load the spec, and save it so that it doesn't need to be reloaded if it -- doesn't change. let numSteps = simulationSettingsInitialSteps simulationSettings spec' <- readSpec simulationSettings spec let simData = SimData numSteps spec' spec return simData -- | Update the spec based on the input command received. simStep :: SimulationSettings -> SimData -> (Command, String) -> IO SimData simStep _ simData (StepUp, _) = pure simData { simSteps = simSteps simData + 1 } simStep _ simData (StepDown, _) = pure simData { simSteps = simSteps simData + 1 } simStep simulationSettings simData (AddStream name expr, _) = do let specN = concat [ simString simData, "\n", " ", completeExpr] completeExpr = concat [ "observer ", show name, " (", expr, ")" ] let trace = extractTrace $ simSpec simData spec2 <- readSpec simulationSettings specN let spec3 = updateWithTrace trace spec2 pure simData { simSpec = spec3, simString = specN } simStep simulationSettings simData (command, name) = do spec' <- apply simulationSettings (simSpec simData) name command pure simData { simSpec = spec' } -- | Settings used for a simulation. data SimulationSettings = SimulationSettings { simulationSettingsInitialSteps :: Int , simulationSettingsImports :: [(String, Maybe String)] } -- | Default settings that simulates 3 steps and provides default imports of -- the main Copilot modules. mkDefaultSimulationSettings :: SimulationSettings mkDefaultSimulationSettings = SimulationSettings 3 [ ("Control.Monad.Writer", Nothing) , ("Copilot.Language", Nothing) , ("Copilot.Language.Spec", Nothing) , ("Data.Functor.Identity", Nothing) , ("Language.Copilot", Nothing) , ("Prelude", Just "P") ] -- * Commands -- * Load specs from strings -- | Read a specification from a string and reify it. readSpec :: SimulationSettings -> String -> IO Core.Spec readSpec settings spec = do r <- HI.runInterpreter (loadSpec settings spec) case r of Left err -> do putStrLn $ "Error: " Prelude.++ show err error $ show err Right s -> return s -- | Load a spec from a string, adding standard imports. loadSpec :: SimulationSettings -> String -> HI.Interpreter Core.Spec loadSpec settings spec = do HI.setImportsQ (simulationSettingsImports settings) spec' <- HI.interpret spec (HI.as :: Spec) HI.liftIO $ reify spec' -- | Commands to apply to a running simulation. data Command = StepUp | StepDown | Up Int | Down Int | AddStream String String | Noop deriving (Eq, Read, Show) -- | Apply a command to a simulation. apply :: SimulationSettings -> Core.Spec -> String -> Command -> IO Core.Spec apply settings spec _name (AddStream sName sExpr) = do spec' <- addStream settings sName sExpr -- TODO: I need to bring the streams from the other spec too, otherwise the -- streams to include may refer to streams by ID that are in a different -- scope. let observers' = Core.specObservers spec' observers = Core.specObservers spec return $ spec { Core.specObservers = observers Prelude.++ observers' } apply _settings spec name command = pure $ spec { Core.specStreams = map (updateStream name command) (Core.specStreams spec) , Core.specObservers = map (updateObserver name command) (Core.specObservers spec) , Core.specTriggers = map (updateTrigger name command) (Core.specTriggers spec) } -- | Apply a command to an observer. updateObserver :: String -> Command -> Core.Observer -> Core.Observer updateObserver name command (Core.Observer i e ty) = Core.Observer i (updateExpr name command e) ty -- | Apply a command to a trigger. updateTrigger :: String -> Command -> Core.Trigger -> Core.Trigger updateTrigger name command (Core.Trigger i e es) = Core.Trigger i e' es' where e' = updateExpr name command e es' = map (updateUExpr name command) es -- | Apply a command to a core expression. updateExpr :: String -> Command -> Core.Expr a -> Core.Expr a updateExpr name command expr = case expr of Core.ExternVar ty nameE vs | nameE Prelude.== name -> Core.ExternVar ty nameE (updateValues vs ty command) | otherwise -> expr Core.Op1 op expr1 -> Core.Op1 op (updateExpr name command expr1) Core.Op2 op expr1 expr2 -> Core.Op2 op (updateExpr name command expr1) (updateExpr name command expr2) Core.Op3 op expr1 expr2 expr3 -> Core.Op3 op (updateExpr name command expr1) (updateExpr name command expr2) (updateExpr name command expr3) _ -> expr -- | Apply a command to an untyped expression that carries the information -- about the type of the expression as a value (existential). updateUExpr :: String -> Command -> Core.UExpr -> Core.UExpr updateUExpr name cmd (Core.UExpr ty expr) = Core.UExpr ty (updateExpr name cmd expr) -- | Apply a command to a stream. updateStream :: String -> Command -> Core.Stream -> Core.Stream updateStream name command (Core.Stream i buf expr ty) = Core.Stream i buf (updateExpr name command expr) ty -- | Apply a command to a series of typed values, if any. updateValues :: Maybe [a] -> Type a -> Command -> Maybe [a] updateValues vsM ty command = fmap (fmap (updateValue command ty) . zip [0..]) vsM -- | Apply a command to a typed value. updateValue :: Command -> Type a -> (Int, a) -> a updateValue (Up n) Core.Bool (ix, a) = if n Prelude.== ix then Prelude.not a else a updateValue (Down n) Core.Bool (ix, a) = if n Prelude.== ix then Prelude.not a else a updateValue (Up n) Core.Word8 (ix, a) = if n Prelude.== ix then a + 1 else a updateValue (Down n) Core.Word8 (ix, a) = if n Prelude.== ix then a - 1 else a updateValue _ _ (_, a) = a -- * Sample spec -- | Produce a specification from the expression for a stream. addStream :: SimulationSettings -> String -> String -> IO Core.Spec addStream settings name expr = do r <- HI.runInterpreter (addStream' settings name expr) case r of Left err -> do putStrLn $ "Error: " Prelude.++ show err error $ show err Right spec -> return spec -- | Produce a specification from the expression for a stream, in an -- interpreter context. -- -- Observe that Interpreter () is an alias for InterpreterT IO () addStream' :: SimulationSettings -> String -> String -> HI.Interpreter Core.Spec addStream' settings name expr = do HI.setImportsQ (simulationSettingsImports settings) let completeExpr = concat [ "observer ", show name, " (", expr, ")" ] spec <- HI.interpret completeExpr (HI.as :: Spec) HI.liftIO $ reify spec