content: -- 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 i spec = do
    putStrLn "Note: CSV format does not output observers."
    interpret' I.CSV i 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 = interpret' 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 i spec = do
    coreSpec <- reify spec
    putStrLn $ I.interpret format (fromIntegral i) coreSpec
  