diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..f94ebc4 --- /dev/null +++ b/.gitignore @@ -0,0 +1,25 @@ +dist +dist-* +cabal-dev +*.o +*.hi +*.chi +*.chs.h +*.dyn_o +*.dyn_hi +.hpc +.hsenv +.cabal-sandbox/ +cabal.sandbox.config +*.prof +*.aux +*.hp +*.eventlog +.stack-work/ +cabal.project.local +cabal.project.local~ +.HTF/ +.ghc.environment.* +copilot-profiling +.DS_Store +.log diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 0000000..e69de29 diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..d4ed5bc --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..f4a93c4 --- /dev/null +++ b/README.md @@ -0,0 +1,34 @@ +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) + +# Copilot: a stream DSL + +The visualizer, which draws Copilot specifications using different graphical +formats. + +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. + +Programs can be interpreted for testing (with the library copilot-interpreter), +or translated C99 code to be incorporated in a project, or as a standalone +application. The C99 backend ensures us that the output is constant in memory +and time, making it suitable for systems with hard realtime requirements. + +## Installation + +Copilot-visualizer can be found on +[Hackage](https://hackage.haskell.org/package/copilot-interpreter). It is +typically only installed as part of the complete Copilot distribution. For +installation instructions, please refer to the [Copilot +website](https://copilot-language.github.io). + +## Further information + +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) + +## License + +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-interpreter/LICENSE). diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-visualizer.cabal b/copilot-visualizer.cabal new file mode 100644 index 0000000..726aa89 --- /dev/null +++ b/copilot-visualizer.cabal @@ -0,0 +1,92 @@ +cabal-version: >=1.10 +name: copilot-visualizer +version: 4.2 +synopsis: Visualizer for Copilot. +description: + Visualizer for 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 tutorial, examples, and other information are available at + . + +author: Ivan Perez, Frank Dedden +license: BSD3 +license-file: LICENSE +maintainer: Ivan Perez +homepage: https://copilot-language.github.io +bug-reports: https://github.com/Copilot-Language/copilot/issues +stability: Experimental +category: Language, Embedded +build-type: Simple +extra-source-files: README.md, CHANGELOG +data-files: data/tikz.latex + data/timeline.html + +x-curation: uncurated + +source-repository head + type: git + location: https://github.com/Copilot-Language/copilot.git + subdir: copilot-visualizer + +executable copilot-live-backend + default-language: Haskell2010 + + main-is: Copilot/Live.hs + + hs-source-dirs: src + + ghc-options: + -Wall + + build-depends: + base >= 4.9 && < 5, + aeson, + directory, + filepath, + hint, + pretty >= 1.0 && < 1.2, + ogma-extra >= 1.6.0 && < 1.7, + + copilot-core >= 4.2 && < 4.3, + copilot-interpreter >= 4.2 && < 4.3, + copilot-visualizer >= 4.2 && < 4.3, + copilot-language, + copilot, + text, + websockets >= 0.12.7 + + other-modules: + + Paths_copilot_visualizer + +library + + default-language: Haskell2010 + + hs-source-dirs: src + + ghc-options: + -Wall + + build-depends: + base >= 4.9 && < 5, + aeson, + directory, + filepath, + pretty >= 1.0 && < 1.2, + ogma-extra >= 1.6.0 && < 1.7, + + copilot-core >= 4.2 && < 4.3, + copilot-interpreter >= 4.2 && < 4.3 + + exposed-modules: + + Copilot.Visualize + + other-modules: + + Paths_copilot_visualizer diff --git a/data/tikz.latex b/data/tikz.latex new file mode 100644 index 0000000..b05f2c1 --- /dev/null +++ b/data/tikz.latex @@ -0,0 +1,37 @@ +{{=<% %>=}} +\documentclass{standalone} +\usepackage{tikz} +\usepackage{tikz-timing} +\usepackage{xcolor} +\definecolor{false}{HTML}{ECD9ED} +\definecolor{true}{HTML}{D9ECED} +\begin{document} +\newcommand{\true}{T} +\newcommand{\false}{F} +\tikzset{ +every picture/.style={ + execute at end picture={ + \path (current bounding box.south west) +(-1,-1) (current bounding box.north east) +(1,1); + } +} +} + +\tikzset{ +timing/.style={x=5ex,y=2ex}, +timing/rowdist=4ex, +timing/dslope=0.1, +x=5ex, +timing/coldist=1ex, +timing/name/.style={font=\sffamily\scriptsize}, +timing/d/text/.style={font=\sffamily\tiny}, +} +\begin{tikztimingtable} +<%#adTraceElems%> +<%teName%> & g<%#teValues%><%#tvIsEmpty%>S<%/tvIsEmpty%><%^tvIsEmpty%><%#teIsBoolean%>[fill=<%tvValue%>]D{\<%tvValue%>}<%/teIsBoolean%><%^teIsBoolean%>D{<%tvValue%>}<%/teIsBoolean%><%/tvIsEmpty%><%/teValues%>\\ +<%/adTraceElems%> +\extracode +\begin{background}[shift={(0.05,0)},help lines] +\vertlines[help lines,opacity=0.3]{-0.3ex,...,<%adLastSample%>} +\end{background} +\end{tikztimingtable} +\end{document} diff --git a/data/timeline.html b/data/timeline.html new file mode 100644 index 0000000..e19cafc --- /dev/null +++ b/data/timeline.html @@ -0,0 +1,255 @@ + + + + + + Copilot Visualizer + + + + + + + +
+ +
+ + + + diff --git a/main.html b/main.html new file mode 100644 index 0000000..2966ad2 --- /dev/null +++ b/main.html @@ -0,0 +1,436 @@ + + + + + + Copilot Visualizer + + + + + + + +
+ +
+
+ + + + + + + +
+ + + + + + + diff --git a/src/Copilot/Live.hs b/src/Copilot/Live.hs new file mode 100644 index 0000000..e4fed16 --- /dev/null +++ b/src/Copilot/Live.hs @@ -0,0 +1,392 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} + +import Control.Concurrent +import Control.Concurrent.MVar +import Control.Exception (handle, SomeException(..), finally) +import Control.Monad +import qualified Copilot.Core as Core +import Copilot.Interpret.Eval +import Copilot.Language hiding (interpret, typeOf) +import qualified Copilot.Language +import qualified Copilot.Visualize as View +import Data.Aeson +import Data.List hiding ((++)) +import Data.Maybe (fromMaybe) +import qualified Data.Text as T +import qualified Data.Type.Equality as DE +import Data.Typeable +import GHC.Generics +import Language.Copilot +import Language.Copilot hiding (interpret, typeOf) +import qualified Language.Haskell.Interpreter as HI +import qualified Language.Haskell.Interpreter.Unsafe as HI +import qualified Network.WebSockets as WS +import Prelude hiding (div, not, (++), (<), (>)) +import qualified Prelude +import System.Directory +import Text.Read + +main :: IO () +main = do + putStrLn "WebSocket server starting on port 9160..." + WS.runServer "127.0.0.1" 9160 app + +makeTraceEval' k spec' = + View.makeTraceEval k spec' (eval Haskell k spec') + +-- * App + +app :: WS.ServerApp +app pending = do + conn <- WS.acceptRequest pending + WS.withPingThread conn 30 (return ()) $ + handle (\(e :: SomeException) -> do putStrLn $ "Something went wrong:" Prelude.++ show e + error $ show e) $ do + spec' <- readSpec spec + + let k = 3 + + specV <- newMVar spec + v <- newMVar (k, spec') + + let a = makeTraceEval' k spec' + samples = encode $ toJSON $ allSamples a + WS.sendTextData conn samples + + loop conn v specV + + where + + loop conn v specV = forever $ do + msg <- WS.receiveData conn + print msg + let pair = readMaybe (T.unpack msg) + print pair + + (k, spec') <- takeMVar v + spec'' <- case (T.unpack msg, pair) of + ("StepUp", _) -> pure spec' + ("StepDown", _) -> pure spec' + (_, Just (AddStream name expr, _)) -> do + spec <- takeMVar specV + let specN = spec Prelude.++ "\n" Prelude.++ + " " Prelude.++ completeExpr + completeExpr = concat [ "observer " + , show name + , " (" + , expr + , ")" + ] + let trace = extractTrace spec' + spec2 <- readSpec specN + putMVar specV specN + let spec3 = updateWithTrace trace spec2 + return spec3 + (_, Just (command, name)) -> apply spec' name command + _ -> pure spec' + + let k' = case T.unpack msg of + "StepUp" -> k + 1 + "StepDown" -> k - 1 + _ -> k + + putMVar v (k', spec'') + + let a = makeTraceEval' k' spec'' + samples = encode $ toJSON $ allSamples a + WS.sendTextData conn samples + +data Data = Data + { adLastSample :: Int + , adTraceElems :: [TraceElem] + } + deriving (Generic) + +instance ToJSON Data + +data TraceElem = TraceElem + { teName :: String + , teIsBoolean :: Bool + , teValues :: [Sample] + } + deriving (Generic) + +instance ToJSON TraceElem + +data Sample = Sample + { time :: Int + , value :: String + , duration :: Float + } + deriving (Generic) + +instance ToJSON Sample + +allSamples :: View.AppData -> Data +allSamples appData = Data + { adLastSample = View.adLastSample appData + , adTraceElems = map toTraceElem (View.adTraceElems appData) + } + +toTraceElem :: View.TraceElem -> TraceElem +toTraceElem te = TraceElem + { teName = View.teName te + , teIsBoolean = View.teIsBoolean te + , teValues = map + (\(i, v) -> Sample i (View.tvValue v) 1) + (zip [0..] (View.teValues te)) + } + +-- * Update specs using commands + +data Command = Up Int + | Down Int + | AddStream String String + | Noop + deriving (Eq, Read, Show) + +apply :: Core.Spec -> String -> Command -> IO Core.Spec +apply spec name (AddStream sName sExpr) = do + putStrLn "Here" + spec' <- addStream sName sExpr + putStrLn "Here 2" + -- 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 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) + } + +updateObserver :: String -> Command -> Core.Observer -> Core.Observer +updateObserver name command (Core.Observer i e ty) = (Core.Observer i e' ty) + where + e' = updateExpr name command e + +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 + +updateExpr :: String -> Command -> Core.Expr a -> Core.Expr a +updateExpr name command e = case e of + (Core.ExternVar ty nameE vs) + | nameE Prelude.== name + -> Core.ExternVar ty nameE (updateValues vs ty command) + | otherwise + -> e + (Core.Op1 op e) -> + Core.Op1 op (updateExpr name command e) + (Core.Op2 op e1 e2) -> + Core.Op2 op (updateExpr name command e1) (updateExpr name command e2) + (Core.Op3 op e1 e2 e3) -> + Core.Op3 + op + (updateExpr name command e1) + (updateExpr name command e2) + (updateExpr name command e3) + _ -> e + +updateUExpr :: String -> Command -> Core.UExpr -> Core.UExpr +updateUExpr name cmd (Core.UExpr ty e) = Core.UExpr ty (updateExpr name cmd e) + +updateStream :: String -> Command -> Core.Stream -> Core.Stream +updateStream name command (Core.Stream i b e ty) = + (Core.Stream i b (updateExpr name command e) ty) + +updateValues :: Maybe [a] -> Type a -> Command -> Maybe [a] +updateValues vsM ty command = + fmap (\vs -> fmap (updateValue command ty) (zip [0..] vs)) vsM + +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 _ _ (ix, a) = a + +-- * Sample spec + +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)" + ] + +spec' :: String -> HI.Interpreter Core.Spec +spec' spec = do + HI.setImportsQ [ ("Prelude", Just "P") + , ("Copilot.Language", Nothing) + , ("Copilot.Language.Spec", Nothing) + , ("Language.Copilot", Nothing) + , ("Data.Functor.Identity", Nothing) + , ("Control.Monad.Writer", Nothing) + ] + + spec' <- HI.interpret spec (HI.as :: Spec) + HI.liftIO $ reify spec' + +readSpec :: String -> IO Core.Spec +readSpec spec = do + r <- HI.runInterpreter (spec' spec) + case r of + Left err -> do putStrLn $ "There was an error, and here it is: " Prelude.++ show err + error $ show err + Right s -> return s + +addStream :: String -> String -> IO (Core.Spec) +addStream name expr = do + r <- HI.runInterpreter (addStream' name expr) + case r of + Left err -> do putStrLn $ "There was an error, and here it is: " Prelude.++ show err + error $ show err + Right spec -> return spec + +-- observe that Interpreter () is an alias for InterpreterT IO () +addStream' :: String -> String -> HI.Interpreter Core.Spec +addStream' name expr = do + HI.setImportsQ [ ("Prelude", Just "P") + , ("Copilot.Language", Nothing) + , ("Copilot.Language.Spec", Nothing) + , ("Language.Copilot", Nothing) + , ("Data.Functor.Identity", Nothing) + , ("Control.Monad.Writer", Nothing) + ] + + -- For debugging purposes only: let completeExpr = "observer \"h1\" (constF 3.0)" + let completeExpr = concat [ "observer " + , show name + , " (" + , expr + , ")" + ] + + -- HI.liftIO $ putStrLn $ "I'm about to interpret " ++ completeExpr + spec <- HI.interpret completeExpr (HI.as :: Spec) + -- HI.liftIO $ putStrLn "completed" + HI.liftIO $ reify spec + +data Trace = Trace + { traceMap :: [ (String, UValues) ] + } + +data UValues = forall a . Typeable a => UValues + { uvType :: Core.Type a + , uvValues :: [ a ] + } + +extractTrace :: Core.Spec -> Trace +extractTrace spec = Trace $ concat $ concat + [ fmap extractTraceStream (Core.specStreams spec) + , fmap extractTraceObserver (Core.specObservers spec) + , fmap extractTraceTrigger (Core.specTriggers spec) + ] + +extractTraceStream :: Core.Stream -> [ (String, UValues) ] +extractTraceStream (Core.Stream _id _buf expr _ty) = + extractTraceExpr expr + +extractTraceObserver :: Core.Observer -> [ (String, UValues) ] +extractTraceObserver (Core.Observer _name expr _ty) = + extractTraceExpr expr + +extractTraceTrigger :: Core.Trigger -> [ (String, UValues) ] +extractTraceTrigger (Core.Trigger _name expr args) = concat $ + extractTraceExpr expr + : fmap extractTraceUExpr args + +extractTraceExpr :: Core.Expr a -> [ (String, UValues) ] +extractTraceExpr (Core.Local _ _ _ expr1 expr2) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + ] +extractTraceExpr (Core.ExternVar ty name values) = + [ (name, UValues ty (fromMaybe [] values)) ] +extractTraceExpr (Core.Op1 _op expr) = + extractTraceExpr expr +extractTraceExpr (Core.Op2 _op expr1 expr2) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + ] +extractTraceExpr (Core.Op3 _op expr1 expr2 expr3) = concat + [ extractTraceExpr expr1 + , extractTraceExpr expr2 + , extractTraceExpr expr3 + ] +extractTraceExpr (Core.Label _ty _lbl expr) = + extractTraceExpr expr +extractTraceExpr _ = [] + +extractTraceUExpr :: Core.UExpr -> [ (String, UValues) ] +extractTraceUExpr (Core.UExpr ty expr) = + extractTraceExpr expr + +updateWithTrace :: Trace -> Core.Spec -> Core.Spec +updateWithTrace trace spec = spec + { Core.specStreams = fmap (updateWithTraceStream trace) (Core.specStreams spec) + , Core.specObservers = fmap (updateWithTraceObserver trace) (Core.specObservers spec) + , Core.specTriggers = fmap (updateWithTraceTrigger trace) (Core.specTriggers spec) + } + +updateWithTraceStream :: Trace -> Core.Stream -> Core.Stream +updateWithTraceStream trace (Core.Stream ident buf expr ty) = + Core.Stream ident buf (updateWithTraceExpr trace expr) ty + +updateWithTraceObserver :: Trace -> Core.Observer -> Core.Observer +updateWithTraceObserver trace (Core.Observer name expr ty) = + Core.Observer name (updateWithTraceExpr trace expr) ty + +updateWithTraceTrigger :: Trace -> Core.Trigger -> Core.Trigger +updateWithTraceTrigger trace (Core.Trigger name expr args) = + Core.Trigger name (updateWithTraceExpr trace expr) (fmap (updateWithTraceUExpr trace) args) + +updateWithTraceExpr :: Trace -> Core.Expr a -> Core.Expr a +updateWithTraceExpr trace (Core.Local ty1 ty2 name expr1 expr2) = + Core.Local ty1 ty2 name (updateWithTraceExpr trace expr1) (updateWithTraceExpr trace expr2) +updateWithTraceExpr trace (Core.ExternVar ty name values) = + Core.ExternVar ty name values' + where + values' | Just (UValues ty2 vals) <- lookup name (traceMap trace) + , Just DE.Refl <- DE.testEquality ty ty2 + = Just vals + | otherwise + = values +updateWithTraceExpr trace (Core.Op1 op expr) = + Core.Op1 op (updateWithTraceExpr trace expr) +updateWithTraceExpr trace (Core.Op2 op expr1 expr2) = + Core.Op2 op (updateWithTraceExpr trace expr1) (updateWithTraceExpr trace expr2) +updateWithTraceExpr trace (Core.Op3 op expr1 expr2 expr3) = + Core.Op3 op + (updateWithTraceExpr trace expr1) + (updateWithTraceExpr trace expr2) + (updateWithTraceExpr trace expr3) +updateWithTraceExpr trace (Core.Label ty lbl expr) = + Core.Label ty lbl (updateWithTraceExpr trace expr) +updateWithTraceExpr trace x = x + +updateWithTraceUExpr :: Trace -> Core.UExpr -> Core.UExpr +updateWithTraceUExpr trace (Core.UExpr ty expr) = + Core.UExpr ty (updateWithTraceExpr trace expr) diff --git a/src/Copilot/Visualize.hs b/src/Copilot/Visualize.hs new file mode 100644 index 0000000..115e96f --- /dev/null +++ b/src/Copilot/Visualize.hs @@ -0,0 +1,170 @@ +-- | Graphical visualization of Copilot specifications. + +{-# LANGUAGE DeriveGeneric #-} + +module Copilot.Visualize + where + +-- External imports +import Data.Aeson +import Data.List +import Data.Maybe ( fromMaybe, isJust, isNothing ) +import GHC.Generics +import System.Directory +import System.Directory.Extra +import System.FilePath +import Text.Printf +import Text.Read + +-- External imports: Copilot +import Copilot.Core +import Copilot.Interpret.Eval + +-- Internal imports +import Paths_copilot_visualizer + +-- | Generate a visualization of a specification for a given number of steps. +makeTrace :: Int -- ^ Number of steps to interpret. + -> Spec -- ^ Specification to interpret. + -> IO () +makeTrace k spec = do + dir <- getDataDir + let f = dir "data" + let subs = toJSON $ makeTraceEval k spec e + copyTemplate f subs "target" + where + e = eval Haskell k spec + +-- | Generate an abstract representation of a trace of a specification +-- interpreted for a given number of steps. +makeTraceEval :: Int + -> Spec + -> ExecTrace + -> AppData +makeTraceEval k spec e = + AppData (observerTEs ++ triggerTEs) (k - 1) + where + observerTEs = map mkTraceElem (interpObserversOpt spec e) + triggerTEs = map mkTraceElem (interpTriggersWithArgs spec e) + +mkTraceElem :: (String, [Maybe Output]) -> TraceElem +mkTraceElem (name, outputs) = TraceElem + { teName = name + , teValues = values + , teIsBoolean = any (isBoolean . tvValue) values + , teIsFloat = any (isFloat . tvValue) values + } + where + values = map mkTraceValue outputs + +mkTraceValue :: Maybe Output -> TraceValue +mkTraceValue x = TraceValue (showValue x) (isNothing x) + +-- * Abstract representation of a trace + +data AppData = AppData + { adTraceElems :: Trace + , adLastSample :: Int + } + deriving (Generic, Show) + +instance ToJSON AppData + +type Trace = [ TraceElem ] + +data TraceElem = TraceElem + { teName :: String + , teIsBoolean :: Bool + , teIsFloat :: Bool + , teValues :: [ TraceValue ] + } + deriving (Generic, Show) + +instance ToJSON TraceElem + +data TraceValue = TraceValue + { tvValue :: String + , tvIsEmpty :: Bool + } + deriving (Generic, Show) + +instance ToJSON TraceValue + +-- * Auxiliary functions + +-- | Compute the list of values associated to observers. +interpObserversOpt :: Spec -> ExecTrace -> [(String, [Maybe Output])] +interpObserversOpt _spec e = + map (\(n, os) -> (n, map Just os)) (interpObservers e) + +-- | Compute the list of values associated to triggers and their arguments. +-- +-- For each trigger, we first include the values of the trigger itself, and +-- then the values of the arguments to the trigger. +interpTriggersWithArgs :: Spec -> ExecTrace -> [(String, [Maybe Output])] +interpTriggersWithArgs spec e = concatMap triggerOutputs (interpTriggers e) + where + -- This function adds one more output for the trigger itself. + triggerOutputs :: (String, [Maybe [Output]]) -> [(String, [Maybe Output])] + triggerOutputs (triggerName, triggerArgs) = + (triggerName, triggerValues) : zip argNames argValues + where + triggerValues = map triggerValue triggerArgs + + -- Value for the trigger at a given time, based on the values of its + -- arguments. + triggerValue :: Maybe [Output] -> Maybe Output + triggerValue Nothing = Just "false" + triggerValue (Just _) = Just "true" + + -- Names and values for the arguments. + argNames = map (\ix -> triggerName ++ "Arg" ++ show ix) [0..] + argValues = transpose (transMaybes numArgs triggerArgs) + numArgs = triggerNumArgs spec triggerName + +-- Number of arguments to a trigger in a spec. +-- +-- PRE: name exists as a trigger in spec. +triggerNumArgs :: Spec -> String -> Int +triggerNumArgs spec name = + case find (\t -> triggerName t == name) (specTriggers spec) of + Nothing -> error "Couldn't find given trigger in spec, should never occur!" + Just t -> length $ triggerArgs t + +-- | True if the input value denotes a boolean value. +isBoolean :: String -> Bool +isBoolean "true" = True +isBoolean "false" = True +isBoolean _ = False + +-- | True if the input value denotes a floating point value. +isFloat :: String -> Bool +isFloat s = + isJust asInt || isJust asFloat + where + asInt :: Maybe Int + asInt = readMaybe s + + asFloat :: Maybe Float + asFloat = readMaybe s + +-- | Show a value. +showValue :: Maybe Output -> String +showValue Nothing = "--" +showValue (Just s) | isFloat s = showValueFloat s + | otherwise = s + +-- | Show a floating point value. +showValueFloat :: Output -> String +showValueFloat = formatFloat . read + where + formatFloat :: Double -> String + formatFloat = printf "%.2g" + +-- | Given a list of maybe lists of known length, this function creates a list +-- of lists, pushing the Maybe's inside. +transMaybes :: Int -> [Maybe [a]] -> [[Maybe a]] +transMaybes = map . transMaybes' + where + transMaybes' argsLength (Just xs) = map Just xs + transMaybes' argsLength Nothing = replicate argsLength Nothing