-- | Atom compilation.
module Language.Atom.Compile
  ( compile
  ) where

import Control.Monad.State hiding (join)
import Data.Maybe
import System.Exit
import System.IO

import Language.Atom.Code
import Language.Atom.Scheduling
import Language.Atom.Elaboration
import Language.Atom.Language hiding (Atom)
import Language.Atom.Verify ()

-- | Compiles an atom description to C.
compile :: Name -> Atom () -> IO ()
compile name atom = do
  r <- elaborate name atom
  case r of
    Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)
    Just (rules, uvs, _) -> do
      r <- schedule name rules
      case r of
        Nothing -> putStrLn "ERROR: Rule scheduling failed." >> exitWith (ExitFailure 1)
        Just schedule -> do
          {-
          when (depth > 0) $ do
            putStrLn $ "Starting bounded model checking with depth " ++ show depth ++ "..."
            v <- mapM (verify depth schedule uvs) asserts 
            when (not $ and v) $ putStrLn "ERROR: Verification failed." >> exitWith (ExitFailure 1)
          -}
          putStrLn "Starting code generation..."
          hFlush stdout
          writeC name schedule uvs