{-  CAO Compiler
    Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>. -}

{-# LANGUAGE PatternGuards #-}

{-
Module      :  $Header$
Description :  Compiler main module
Copyright   :  (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License     :  GPL

Maintainer  :  Paulo Silva <paufil@di.uminho.pt>
Stability   :  experimental
Portability :  non-portable

-}

module Main.Compiler ( caoComp ) where

import Control.Monad
import Control.Monad.State

import Data.Maybe (fromMaybe)
import System.Directory (doesFileExist, getPermissions, readable, findExecutable) 
import System.FilePath(splitExtension, addExtension, takeFileName)
import System.IO

import Language.CAO.Analysis.CFG
import Language.CAO.Analysis.SSA

import Language.CAO.Common.Error
import Language.CAO.Common.Monad 
import Language.CAO.Common.State
import Language.CAO.Common.Var

import Language.CAO.Parser.Config
import Language.CAO.Parser.Parser ( parseFile )

import Language.CAO.Platform.Specification

import Language.CAO.Syntax
import Language.CAO.Syntax.Tidy

import Language.CAO.Transformation.Expand
import Language.CAO.Transformation.Eval
import Language.CAO.Transformation.Indist
import Language.CAO.Transformation.Simplify
import Language.CAO.Transformation.Target

import qualified Language.CAO.Translation.C as NC
import Language.CAO.Translation.PreC

import Language.CAO.Typechecker ( tcCaoAST )

import Main.Flags
import Main.Dot

_WRONG_MODE :: a
_WRONG_MODE = error "<Main.Compiler>: Panic! unexpected mode!"

caoComp :: Options -> IO ()
caoComp opts@(Comp {}) = do
    -- Check config file
    let cfg_file = config opts
    exists_cfg <- doesFileExist cfg_file
    when (not exists_cfg) $
        error $ "Error: could not find config file: `" ++ cfg_file ++ "'."
    cfg_permissions <- getPermissions cfg_file
    when (not (readable cfg_permissions)) $
        error $ "Error: config file `" ++ cfg_file ++ "' is not readable."
      
    -- Check input file
    let input_file = input opts
        (file, extension) = splitExtension input_file
    when (null input_file) $ error $ "Error: no input file."
    exists_input <- doesFileExist input_file
    when (not exists_input) $
        error $ "Error: could not find input file: `" ++ input_file ++ "'."
    when (extension /= ".cao") $
        error $ "Error: input file format not recognized: `" ++ extension ++"'."
    input_permissions <- getPermissions input_file
    when (not (readable input_permissions)) $
        error $ "Error: input file `" ++ input_file ++ "' is not readable."

    -- Check Yices
    yices <- checkYices

    -- Output file
    let output_file = fromMaybe (addExtension (takeFileName file) ".c") (output opts)

    cfg <- loadConfig cfg_file
    (c_prog, warn) <- runCaoResultWarn $ compile cfg opts yices
    hPutStrLn stderr $ showCaoWarnings warn
    writeFile output_file c_prog
caoComp _
    = _WRONG_MODE

checkYices :: IO (Maybe FilePath)
checkYices = do
    yices <- findExecutable "yices"
    maybe (hPutStrLn stderr "Without Yices some conditions may not be verified correctly") (const (return ())) yices
    return yices
--------------------------------------------------------------------------------
-- Main compilation function:
--    pipeline = parser -> typechecker -> seq expansion
--                             -> eval -> simplify -> optimize -> C
compile :: TranslationSpec -> Options -> Maybe FilePath -> CaoResult String
compile cfg opts yices = do
    let file_name = input opts
    setFileName file_name
    setYices yices
    -- Parse
    parsed_ast <- parseFile file_name
    -- TypeCheck prog
    let mode = runmode opts
    (tc_ast,_) <- tcCaoAST mode parsed_ast
    dump mode (verbose opts) (ddump_tc opts) (dcheck opts) tc_ast
    -- Expand sequences
    seq_exp_ast <- whenOpt (fexpand)
                      (\_ a -> expandSequences a) opts tc_ast
    dump mode (verbose opts) (ddump_expand opts && fexpand opts) (dcheck opts) seq_exp_ast
    -- Eval
    let eval_ast = evalExpr seq_exp_ast
    dump mode (verbose opts) (ddump_eval opts) (dcheck opts) eval_ast
    -- Simplify
    simpl_ast <- simplifyCaoAST (initProcName $ globalTransSpec cfg) eval_ast
    dump mode (verbose opts) (ddump_simpl opts) (dcheck opts) simpl_ast
    -- Optimize
    opt_ast   <- whenOpt optimize
                    optProg opts simpl_ast
    dump mode (verbose opts) (ddump_opt opts) (dcheck opts) opt_ast
    --- Platform dependent ---
    -- Not valid CAO code anymore --
    -- Target
    target_ast <- targetCaoAST cfg opt_ast
    dump mode (verbose opts) (ddump_target opts) (dcheck opts) target_ast
    -- PreC
    prec_ast <- cao2prec cfg target_ast
    dump mode (verbose opts) (ddump_prec opts) (dcheck opts) prec_ast
    -- Cao2C
    NC.cao2c cfg prec_ast

--------------------------------------------------------------------------------
-- Optimization

whenOpt :: Monad m =>
  (Options -> Bool) -> (Options -> a -> m a) -> Options -> a -> m a
whenOpt fm f o a
    | fm o      = f o a
    | otherwise = return a

optProg :: Options -> Prog Var -> CaoResult (Prog Var)
optProg opts prog = do
    -- ToCFG
    let cfg = buildCFG prog
    maybe (return ()) (generateCFG opts cfg)     $ dgen_cfg opts
    -- ToSSA
    ssa_cfg <- mapM toSSA cfg
    maybe (return ()) (generateCFG opts ssa_cfg) $ dgen_ssa opts
    -- SSA back translation
    let back_cfg' = map fromSSA ssa_cfg
    
    -- >> Indistinguishable functions
    back_cfg <- maybe (return back_cfg') (flip (uncurry mkIndistFun) back_cfg') $ findist_fun opts

    -- From CFG
    let opt_ast = toAST back_cfg
    return opt_ast

--------------------------------------------------------------------------------
-- Dump mode

dump :: RunMode -> Bool -> Bool -> Bool -> Prog Var -> CaoResult ()
dump m _ True True = \ ast -> do
    s <- get
    put initialState
    _ <- tcCaoAST m (fmap varName (tidyCaoAST ast))
    put s
    liftIO $ hPutStrLn stderr "Dumped code type checked with success"

dump _ v True False
    = liftIO . hPutStrLn stderr . doDump
    where 
    doDump | v         = showCaoASTDebug
           | otherwise = showCaoAST
dump _ _ False _
    = const $ return ()