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
compile :: Name -> String -> String -> String -> Atom () -> Int -> IO ()
compile name include preCode postCode atom depth = do
r <- elaborate name atom
case r of
Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)
Just (rules, uvs, asserts) -> do
r <- schedule 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 include preCode postCode schedule uvs