-- 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