{- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc. -} -- | This module implements two interpreters, which may be used to simulated or -- executed 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 Safe #-} {-# LANGUAGE GADTs, FlexibleInstances #-} module Copilot.Language.Interpret ( csv , interpret ) where import qualified Copilot.Core.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 Spec coreSpec <- Spec -> IO Spec forall a. Spec' a -> IO Spec reify Spec spec String -> IO () putStrLn (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ Format -> Int -> Spec -> String I.interpret Format format (Integer -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral Integer i) Spec coreSpec --------------------------------------------------------------------------------