    -- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc.

    -- | This module implements two interpreters, which may be used to simulate or
    -- execute Copilot specifications on a computer to understand their behavior to
    -- debug possible errors.
    --
    -- The interpreters included vary in how the present the results to the user.
    -- One of them uses a format (csv) that may be more machine-readable, while the
    -- other uses a format that may be easier for humans to read.

    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs             #-}
    {-# LANGUAGE Safe              #-}

    module Copilot.Language.Interpret
      ( csv
      , interpret
      ) where

    import qualified Copilot.Interpret as I

    import Copilot.Language.Spec (Spec)
    import Copilot.Language.Reify

    -- | Simulate a number of steps of a given specification, printing the results
    -- in a table in comma-separated value (CSV) format.
    csv :: Integer -> Spec -> IO ()
    csv :: Integer -> Spec -> IO ()
    csv Integer
    i Spec
    spec = do
      String -> IO ()
    putStrLn String
    "Note: CSV format does not output observers."
      Format -> Integer -> Spec -> IO ()
    interpret' Format
    I.CSV Integer
    i Spec
    spec

    -- | Simulate a number of steps of a given specification, printing the results
    -- in a table in readable format.
    --
    -- Compared to 'csv', this function is slower but the output may be more
    -- readable.
    interpret :: Integer -> Spec -> IO ()
    interpret :: Integer -> Spec -> IO ()
    interpret = Format -> Integer -> Spec -> IO ()
    interpret' Format
    I.Table

    -- | Simulate a number of steps of a given specification, printing the results
    -- in the format specified.
    interpret' :: I.Format -> Integer -> Spec -> IO ()
    interpret' :: Format -> Integer -> Spec -> IO ()
    interpret' Format
    format Integer
    i Spec
    spec = do
      coreSpec <- Spec -> IO Spec
    forall a. Spec' a -> IO Spec
    reify Spec
    spec
      putStrLn $ I.interpret format (fromIntegral i) coreSpec