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


-- | Interpreter for Copilot.
--   
--   Interpreter 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
--   <a>https://copilot-language.github.io</a>.
@package copilot-interpreter
@version 3.19


-- | A tagless interpreter for Copilot specifications.
module Copilot.Interpret.Eval

-- | An environment that contains an association between (stream or extern)
--   names and their values.
type Env nm = [(nm, Dynamic)]

-- | The simulation output is defined as a string. Different backends may
--   choose to format their results differently.
type Output = String

-- | An execution trace, containing the traces associated to each
--   individual monitor trigger and observer.
data ExecTrace
ExecTrace :: [(String, [Maybe [Output]])] -> [(String, [Output])] -> ExecTrace

-- | Map from trigger names to their optional output, which is a list of
--   strings representing their values. The output may be <a>Nothing</a> if
--   the guard for the trigger was false. The order is important, since we
--   compare the arg lists between the interpreter and backends.
[interpTriggers] :: ExecTrace -> [(String, [Maybe [Output]])]

-- | Map from observer names to their outputs.
[interpObservers] :: ExecTrace -> [(String, [Output])]

-- | Evaluate a specification for a number of steps.
eval :: ShowType -> Int -> Spec -> ExecTrace

-- | Target language for showing a typed value. Used to adapt the
--   representation of booleans.
data ShowType
C :: ShowType
Haskell :: ShowType
instance GHC.Show.Show Copilot.Interpret.Eval.ExecTrace
instance GHC.Show.Show Copilot.Interpret.Eval.InterpException
instance GHC.Exception.Type.Exception Copilot.Interpret.Eval.InterpException


-- | An interpreter for Copilot specifications.
module Copilot.Interpret

-- | Output format for the results of a Copilot spec interpretation.
data Format
Table :: Format
CSV :: Format

-- | Interpret a Copilot specification.
interpret :: Format -> Int -> Spec -> String