--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | An interpreter for Copilot specifications.

{-# LANGUAGE Safe #-}

module Copilot.Core.Interpret
  ( Format (..)
  , interpret
  ) where

import Copilot.Core
import Copilot.Core.Interpret.Eval
import Copilot.Core.Interpret.Render
import Copilot.Core.Type.Show (ShowType(..))

data Format = Table | CSV

-- | Interprets a Copilot specification.
interpret :: Format -> Int -> Spec -> String
interpret :: Format -> Int -> Spec -> String
interpret Format
format Int
k Spec
spec =
  case Format
format of
    Format
Table -> ExecTrace -> String
renderAsTable ExecTrace
e
    Format
CSV   -> ExecTrace -> String
renderAsCSV ExecTrace
e
  where e :: ExecTrace
e = ShowType -> Int -> Spec -> ExecTrace
eval ShowType
Haskell Int
k Spec
spec