{-  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 ViewPatterns #-}
{-# LANGUAGE FlexibleContexts #-}

{- |
Module      :  $Header$
Description :  CAO to C translation.
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

CAO to C translation.

Flexible contexts may be dropped.
-}

module Language.CAO.Translation.C (
    cao2c
 ) where

import Control.Monad
import Data.List (intercalate, genericLength, partition)
import qualified Data.Set as Set
import Language.C.Syntax
import Language.C
import Text.PrettyPrint

import Language.CAO.Common.Error
import Language.CAO.Common.Fresh
import Language.CAO.Common.Literal
import Language.CAO.Common.Monad
import Language.CAO.Common.Outputable
import Language.CAO.Common.Polynomial
import Language.CAO.Common.SrcLoc
import Language.CAO.Common.State
import Language.CAO.Common.Utils
import Language.CAO.Common.Var

import Language.CAO.Index

import Language.CAO.Platform.Naming
import Language.CAO.Platform.Query
import Language.CAO.Platform.Specification

import Language.CAO.Semantics.Bits

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

import Language.CAO.Translation.Names
import Language.CAO.Translation.C.Wrappers

import Language.CAO.Type
import Language.CAO.Type.Utils

{-
- The representation of Boolean must be compatible with C integers, or, if a
pointer is used, this must be castable to integers.
-}
--------------------------------------------------------------------------------
------------------------------------- Prog -------------------------------------
-- Top level translation function
cao2c 
    :: CaoMonad m 
    => TranslationSpec -> Prog Var 
    -> m String
cao2c tspec ast = withCST $ do
    cprog <- mapProg tspec $ tidyCaoAST ast
    fnm <- getFileName
    let header = moduleHeader fnm tspec
    return $ header ++ render (pretty cprog)


-- Precondition:
-- The list of definitions is not empty.
mapProg 
    :: CaoMonad m 
    => TranslationSpec -> Prog Var 
    -> m CTranslUnit'
mapProg tspec (Prog defs (Just ip)) = do 
    let gvars = filter isGlobalVar $ Set.toList $ bvs defs
    defs' <- concatMapM (mapDefinition tspec) defs
    ip'   <- initProc tspec ip gvars
    disp  <- disposeProc tspec gvars
    return $ CTranslUnit' (defs' ++ ip' : disp : []) undefNode
mapProg _ _ = internalError "mapProg" "Init procedure not found"

--------------------------------------------------------------------------------
-- Init precedure
initProc 
    :: CaoMonad m 
    => TranslationSpec -> Fun Var -> [Var] 
    -> m CExtDecl'
initProc tspec f = liftM (CED . CFDefExt) . mapInit tspec f 

-- Init procedure generation:
-- Gets the body of the init procedure and the list of global variables
mapInit 
    :: CaoMonad m 
    => TranslationSpec -> Fun Var -> [Var] 
    -> m CFunDef
mapInit tspec (Fun fn _ _ body) gvs = do
    resetCST
    let (gc, gvs') = partition indVar gvs
        gvs'' = map varDecl gvs'
        body''' = mergeDecls gc gvs'' body
    body' <- mapStatements tspec body'''
    disp <- disposeAlloc tspec
    let body'' = body' ++ disp 
    return $ cProc tspec (getSymbol $ unLoc fn) body''
    where
    varDecl v = genLoc $ VDecl $ VarD (genLoc v) undefined Nothing

    mergeDecls gc vs b = insertConstDecls gc (insertVarDecls vs b)

    -- XXX: This is not very efficient...
    insertConstDecls [] b = b
    insertConstDecls (v:vs) b = insertConstDecls vs (insertConst v b)

    insertConst v (L l (Nop EndConsts):slst) = varDecl v : L l (Nop EndConsts) : slst
    insertConst v (s@(L _ (Assign [LVVar (L _ a)] [L _ (TyE _ (FunCall _ _))])):slst)
        | v == a = varDecl v : s : slst
    insertConst v (s:slst) = s : insertConst v slst
    insertConst _ _ = internalError "insertConst" "Not expected case"

    insertVarDecls vs [] = vs
    insertVarDecls vs (L l (Nop EndAux): slst) = (L l $ Nop EndAux) : vs ++ slst
    insertVarDecls vs (s:slst) = s : insertVarDecls vs slst

--------------------------------------------------------------------------------
-- Dispose procedure

disposeProc 
    :: CaoMonad m 
    => TranslationSpec -> [Var] 
    -> m CExtDecl'
disposeProc tspec =
    liftM (CED . CFDefExt . cProc tspec (disposeName tspec))
        . disposeVars tspec

-- Gets the allocated variables and disposes them
disposeAlloc
    :: CaoMonad m
    => TranslationSpec
    -> m [CBlockItem]
disposeAlloc tspec = getAllocVars >>= disposeVars tspec

disposeAllAlloc
    :: CaoMonad m
    => TranslationSpec
    -> m [CBlockItem]
disposeAllAlloc tspec = getAllAllocVars >>= disposeVars tspec

disposeVars 
    :: CaoMonad m 
    => TranslationSpec -> [Var] 
    -> m [CBlockItem]
disposeVars tspec = concatMapM $ \ v -> let
        typ = typeOf v
    in autoOrAlloc tspec typ
        (return [])
        (do tname <- typeName tspec typ
            let fcall = fCall tspec tname code_dispose
            return $ cFuncCallStmt fcall (cVar' v : []) : []
        )

--------------------------------------------------------------------------------
-- Definitions

mapDefinition 
    :: CaoMonad m 
    => TranslationSpec -> LDef Var 
    -> m [CExtDecl']
mapDefinition tspec d = case unLoc d of
    VarDef vd   -> liftM (singleton . declOrMacro) $ mapVarDefinition tspec vd
    ConstDef cd -> liftM (singleton . declOrMacro) $ mapConstDefinition tspec cd
    FunDef fd   -> liftM (singleton . CED . CFDefExt) $ mapFunc tspec fd
    TyDef  td   -> mapTypeDef tspec td

--------------------------------------------------------------------------------
-- Constants

mapConstDefinition 
    :: CaoMonad m 
    => TranslationSpec -> ConstDecl Var 
    -> m (Either CDecl CBlockItem)
mapConstDefinition tspec (ConstD (unLoc -> n) _ _) = mapVar tspec n
mapConstDefinition _ _ = internalError "<mapConstDefinition>" "Not expected case."
    
--------------------------------------------------------------------------------
-- Variables

mapVarDefinition 
    :: CaoMonad m 
    => TranslationSpec -> VarDecl Var 
    -> m (Either CDecl CBlockItem)
mapVarDefinition tspec (VarD (unLoc -> n)  _ Nothing) = mapVar tspec n
mapVarDefinition _ _ = 
    internalError "mapVarDefinition" "Not expected case."

-- Preconditions:
-- 1 - Simplification removes all initializations and multiple declarations
--     in the global setting, so they are not expected as arguments of this
--     function.
-- 2 - Variable/constant initialization is provided elsewhere, namely in the
--     'init' function.
mapVar :: CaoMonad m 
    => TranslationSpec -> Var 
    -> m (Either CDecl CBlockItem)
mapVar tspec n = 
    varOrMacroDecl tspec tn auxVar auxMacro
    where 
    tn = varType n
    auxVar = liftM (Left . cVarDecl (getSymbol n) . tPrefix tspec) $ typeName tspec tn
    auxMacro = valOrRefOpMacroReturn tspec tn code_decl
        (caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapVarDefinition>:\
             \ Not expecting macro variable declaration returning a value")
        (do typ       <- typeName tspec tn
            (p, _)    <- extractParams' tspec tn -- TODO: Verify what happens with global mod variables
            let fdcall = fCall tspec typ code_decl
            return $ Right $ cFuncCallStmt fdcall (cVar' n : p))

--------------------------------------------------------------------------------
----------------------------------------- Func ---------------------------------

mapFunc 
    :: CaoMonad m 
    => TranslationSpec -> Fun Var 
    -> m CFunDef
mapFunc tspec (Fun (L _ fn) args _ body) = do
    let FuncSig _ rtype _  = varType fn
        rtype' = fromTuple rtype
    resetCST
    body'       <- mapBlocks tspec body

    tmpvs       <- getTmpVars
    decls       <- concatMapM (mapVarDecl tspec . varDecl) tmpvs

    args'       <- mapM (mapArg tspec) args
    (cr, rargs) <- mapReturnType tspec rtype'

    let exitFunc = if null rtype' then cReturn caoOk : [] else []
        body''   = decls <<+> (body' <+>> exitFunc)
    return $ cFuncDefinition (getSymbol fn) (rargs ++ args') (tPrefix tspec cr) body''

    where
    varDecl v = VarD (genLoc v) (type2TyDecl (varType v)) Nothing

mapReturnType 
    :: CaoMonad m 
    => TranslationSpec -> [Type Var] 
    -> m (String, [CDecl])
mapReturnType _ [] = return (caoRes, [])
mapReturnType tspec tps@(t:tl) = do
    (t', tl') <- if isStruct t && aux t
                    then return (getSymbol $ getStructName t, tl) 
                    else valOrRefFuncReturn tspec t (liftM (split id (const tl)) $ typeName tspec t) (return (caoRes, tps))
    tl'' <- zipWithSeqM byReference tl'
    return (t', tl'')

    where 

    -- [See note]
    byReference n ty = do
        let retArg = retArgId ++ show n
        (_, ty') <- mapType tspec ty
        valOrRef tspec ty (return $ cPointerDecl retArg) (return $ cParamDecl retArg) `apM` ty'

    aux (Struct sname _) = varType sname == Bullet -- HACK
    aux _ = False
            
--------------------------------------------------------------------------------

mapArg 
    :: CaoMonad m 
    => TranslationSpec -> Arg Var 
    -> m CDecl
mapArg tspec (Arg (L _ an) td)        = cArgs tspec (getSymbol an) td $ varType an
mapArg tspec (ArgConst (L _ an) td _) = cArgs tspec (getSymbol an) td $ varType an

--------------------------------------------------------------------------------
--------------------------------------- TypeDef --------------------------------

mapTypeDef 
    :: CaoMonad m 
    => TranslationSpec -> TyDef Var 
    -> m [CExtDecl']
mapTypeDef tspec td = case td of
    TySynDef sn _ -> do
        let nm = getSymbol $ unLoc sn
        (tname, typ) <- mapType tspec $ synType $ varType $ unLoc sn -- TODO: HACK: get a more elegante way to deal with type synonyms
        if nm == tname then return [] 
            else return [CED $ CDeclExt $ cTypedefDecl (tPrefix tspec nm) typ]
    StructDecl sname lFields -> do
        let tname = tPrefix tspec $ getSymbol (unLoc sname)
        lFields' <- mapM (aux . fst) lFields
        return [ CStructExt tname (tname ++ "_struct") lFields' ]
    where
    aux :: CaoMonad m => Located Var -> m CDecl'
    aux v = do
        let typ = sfType $ varType $ unLoc v
            fldName = getSymbol $ unLoc v
        tname <- typeName tspec typ
        varOrMacroDecl tspec typ
            (declD fldName tname)
            (declM fldName tname typ)

    declD fn tn = return $ cParamDecl' fn (cType (tPrefix tspec tn))
    declM fn tn typ = valOrRefOpMacroReturn tspec typ code_decl
        (caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapTypeDef>:\
             \ Not expecting macro variable declaration returning a value")
        (do (p, _) <- extractParams' tspec typ
            let ffldcall = fCall tspec tn code_decl
            return $ CFld $ cFuncCallStmt ffldcall (cVar fn : p))

--------------------------------------------------------------------------------
--------------------------------------- TypeDecl -------------------------------

mapType 
    :: CaoMonad m 
    => TranslationSpec -> Type Var 
    -> m (String, CDeclSpec)
mapType tspec t = case t of
    TySyn v _ -> return (getSymbol v, cType (tPrefix tspec $ getSymbol v))
    _         -> do
        nm <- typeName tspec t
        return (nm, cType (tPrefix tspec nm))

--------------------------------------------------------------------------------
-------------------------------------- Statement -------------------------------

{-
The copy of values to ensure safeness may require types which are dependent
on the sequence index (this only happens with sequences which were translated
to while loops). Thus, they cannot be handled like ordinary variables and
taken outside the loop (done in PreC module), so they are initialized and
dealocked in the body of the loop to ensure dependencies.

Since PreC declares those variables 'in place', this means that C scope rules
applies and we have to dealock them in the exit of any kind of block 
(while, if, function)
-}

-- Maps a block of CAO statements into a block of C statements
mapBlocks 
    :: CaoMonad m 
    => TranslationSpec -> [LStmt Var]
    -> m CStat
mapBlocks tspec stmt = allocScope $ do
  stmt' <- mapStatements tspec stmt
  iDisp <- if isReturn $ unLoc $ last stmt then return [] else disposeAlloc tspec
  return $ CCompound [] (stmt' ++ iDisp) undefNode

mapStatements
    :: CaoMonad m 
    => TranslationSpec -> [LStmt Var]
    -> m [CBlockItem]
mapStatements tspec = concatMapM (mapStatement tspec . unLoc)

mapStatement 
    :: CaoMonad m 
    => TranslationSpec -> Stmt Var 
    -> m [CBlockItem]

mapStatement tspec (VDecl vd) = mapVarDecl tspec vd

mapStatement tspec (Language.CAO.Syntax.CDecl cd) = mapConstDecl tspec cd

mapStatement tspec (Assign lv [unLoc -> unTyp -> FunCall fn args]) = 
    mapFunCall tspec lv fn args

mapStatement _     (Assign _ _) =
    internalError "mapStatement" "Unexpected assignment case"

mapStatement tspec (FCallS  pn ex)  = do
    liftM singleton $ mapFCallS tspec pn ex

mapStatement tspec (Ret re) = mapReturn tspec re

mapStatement tspec (Ite ex ifBlock elseBlock) = do
    cond <- mapExp tspec ex
    let ex' = typeOf ex
    cond'     <- valOrRef tspec ex' (return id) (return cPointedExpr) `apM` cond
    ifBlock'  <- mapBlocks tspec ifBlock
    elseBlock' <- mapMaybeM (mapBlocks tspec) elseBlock
    return [ CBlockStmt (CIf cond' ifBlock' elseBlock' undefNode) ]

mapStatement tspec (While ex whileBlock) = do
    cond  <- mapExp tspec ex
    let ex' = typeOf ex
    cond' <- valOrRef tspec ex' (return id) (return cPointedExpr) `apM` cond
    whileBlock' <- mapBlocks tspec whileBlock
    return [ CBlockStmt (CWhile cond' whileBlock' False undefNode) ]

mapStatement _ (Nop _) = return []
mapStatement _ _ = internalError "mapStatement" "Not expected!"

--------------------------------------------------------------------------------
{-
Note

If the type is declared as a reference there is nothing left to do
If the type is declared as a value, then a pointer is being used,
thus we have to deference it
-}
{-
Return can be of the form:
* struct, ref1, ref2, ...
* constant, ref1, ref2, ...
* variable, ref1, ref2, ...
* ref1, ref2, ...
-}
mapReturn 
    :: CaoMonad m 
    => TranslationSpec -> [TLExpr Var] 
    -> m [CBlockItem]
mapReturn tspec [] = disposeAllAlloc tspec
mapReturn tspec exps@(expr:el) = do
    e' <- mapExp tspec expr
    (e'', el') <- if isCStructExpr $ unTyp $ unLoc expr
        then return (e', el)
        else valOrRefFuncReturn tspec (typeOf expr) (return (e', el)) (return (cVar caoOk, exps))
    assign <- zipWithSeqM byReference el'
    disp   <- disposeAllAlloc tspec
    return $ assign ++ disp ++ [ cReturnExpr e'' ]

    where
    byReference n ex = do
        let op = if isLit (unTyp $ unLoc ex) then code_init else code_assign
            typ = typeOf ex
        tname <- typeName tspec typ
        let fop = fCall tspec tname op
        ex'  <- mapExp tspec ex
        -- [See note]
        retArg <- valOrRef tspec typ (return cIndirection) (return id) `apM` cVar (retArgId ++ show n)
        opReturnKind' tspec typ op
            (return $ cAssignStmt retArg (cFuncCall fop [ex']))
            (return $ cFuncCallStmt fop [retArg, ex'])
            (do (p, _) <- composedCase typ
                return $ cAssignStmt retArg (cFuncCall fop (ex' : p)))
            (do (p, _) <- composedCase typ
                return $ cFuncCallStmt fop (retArg : ex' : p))

    composedCase typ = if isComposed typ then extractParams' tspec typ else return ([], [])

--------------------------------------------------------------------------------
-- Procedure calls

mapFCallS 
    :: CaoMonad m 
    => TranslationSpec -> Var -> [TLExpr Var] 
    -> m CBlockItem
mapFCallS tspec pn = liftM (cFuncCallStmt (getSymbol pn)) . mapExps tspec

--------------------------------------------------------------------------------
-- Function calls
mapFunCall 
    :: CaoMonad m 
    => TranslationSpec -> [LVal Var] -> Located Var -> [TLExpr Var] 
    -> m [CBlockItem]
-- Particular case when a global refrence extraction has to be called from the
-- static library
mapFunCall tspec lv (unLoc -> fn) ex@(e:_) | isCGlobalRef fn = do
    e' : exps' <- mapExps tspec ex
    (_, constArray) <- freshSmb
    tname <- typeName tspec RInt
    ccode <- cTypeCodeRedux tspec (typeOf e)
    let lv' = mapLVal (head lv) -- TODO: verify that lv has only one value by pattern matching
        len = genericLength exps'
        cdecl = cTypeArrayDecl constArray (tPrefix tspec tname) exps'
    return [cdecl,  cFuncCallStmt (getSymbol fn) [ cExprAddr lv', e', cCharExpr ccode, cVar constArray, cIntExpr len] ]

-- Call to a function of the static library
mapFunCall tspec lv (unLoc -> fn) ex | isCFunction fn = do
    ex' <- mapExps tspec ex
    let typ = varType fn
    opReturnKind' tspec typ (getOpName fn)
        (do lv' <- auxFR lv -- OFuncReturn
            return [ cAssignStmt lv' (cFuncCall (getSymbol fn) ex' )])
        (do lv' <- auxFA lv -- OFuncRef   
            return [ cFuncCallStmt (getSymbol fn) (lv' : ex') ])
        (do lv' <- auxFR lv -- OMacroReturn
            (p, d) <- composedCase typ
            return $ d ++ [ cAssignStmt lv' (cFuncCall (getSymbol fn) (ex' ++ p) )])
        (do lv' <- auxM1 typ lv -- OMacroRef
            (p, d) <- composedCase typ
            return $ d ++ [ cFuncCallStmt (getSymbol fn) (lv' ++ ex' ++ p) ])
    where
    composedCase typ = if isComposed typ && (isCAssign fn || isCComp fn) then extractParams' tspec typ else return ([], [])

    auxFR = return . mapLVal . head
{-
Note:

A macro "returns" a value in a different way than a function.
For instance, in macro(a, b) we can:
- make it return a value
#define macro(a,b) a+b
v = macro(a,b)
- return the value by 'a' (we call this by "reference", although this is not
completely correct):
#define macro(a,b) a=b
macro(v,b)

Thus, what we pass as "return" argument depends on if the type is used by value
or by reference.
However, there is a special case: when we have a reference to a type used by
value. In this case, we have to cast it to a pointer to the type and the use 
an indirection to pass a value.

-}
    auxM1 :: CaoMonad m => Type Var -> [LVal Var] -> m [CExpr]
    auxM1 tp [LVVar (unLoc -> v)] 
        | isCRef v = do
            tname <- typeName tspec tp
            valOrRef tspec tp (return $ singleton . cIndirection)  (return singleton) `apM` cPointerCast (tPrefix tspec tname) (cVar' v)
        | otherwise = return [cVar' v]
    auxM1 _ [LVStruct (LVVar (unLoc -> v)) fld] = return [mapProj v fld]
    auxM1 _ _ = caoError defSrcLoc $ mkUnknownErr $ "Not expected function call result"


    auxFA [LVVar (unLoc -> v)] = case varType v of
        Bullet -> (return $ cVar $ getSymbol v)
        t -> valOrRef tspec t
            (return $ cExprAddr $ cVar $ getSymbol v)
            (return $ cVar $ getSymbol v)
    auxFA [LVStruct (LVVar (unLoc -> v)) fld] = case varType v of
        Bullet -> 
            (return $ mapProj v fld)
        t -> valOrRef tspec t
            (return $ cExprAddr $ mapProj v fld)
            (return $ mapProj v fld)
    auxFA _ = caoError defSrcLoc $ mkUnknownErr $ "Not expected function call result"

-- TODO: Left values were tested againt Bullet type. This is a HACK and was
-- removed. However, some code that dependend on this hack may fail.

-- Call to a function
mapFunCall tspec lv (unLoc -> fn) args = do
    ex' <- mapExps tspec args
    (lv', re) <- auxLV lv
    let call = cFuncCall (getSymbol fn) (re ++ ex')
    return $ singleton $ maybe (cExprStmt call) (flip cAssignStmt call) lv'
    where

    auxLV :: CaoMonad m => [LVal Var] -> m (Maybe CExpr, [CExpr])
    auxLV (r:rt) = do
        (r', rt') <- if isCStruct' r
            then return (Just $ mapLVal r, rt)
            else valOrRefFuncReturn tspec (typeOf r) (return (Just $ mapLVal r, rt)) (return (Nothing, r:rt))
        rt'' <- mapM auxFA rt'
        return (r', rt'')
    auxLV _ = caoError defSrcLoc $ mkUnknownErr $ "Not expected function call result"

    auxFA :: CaoMonad m => LVal Var -> m CExpr
    auxFA l = valOrRef tspec (typeOf l) (return cExprAddr) (return id) `apM` mapLVal l
--------------------------------------------------------------------------------
-- Constant declaration
mapConstDecl 
    :: CaoMonad m 
    => TranslationSpec -> ConstDecl Var 
    -> m [CBlockItem]
mapConstDecl tspec c = case c of
    ConstD (unLoc -> n) _ _ -> varMemory tspec n >> constDeclaration tspec n
    _ -> caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapConstDecl>:\
        \ precondition violation:\n" ++ showPpr c
    
constDeclaration 
    :: CaoMonad m 
    => TranslationSpec -> Var 
    -> m [CBlockItem]
constDeclaration tspec v = varOrMacroDecl tspec (varType v) auxVar auxMac
    -- TODO: This definitions are equal to varDeclaration
    where
    auxVar = do
        decl <- if isGlobalVar v then return [] else liftM (singleton . cVarDeclStmt (getSymbol v) . tPrefix tspec) . cTypeName tspec $ v
        alloc <- autoOrAlloc tspec (varType v) (return []) (do
            typ <- cTypeName tspec v
            (args, d) <- extractParams tspec v
            (targs, decl') <- cTypeCodeArgs tspec (typeOf v)
            let fcall = fCall tspec typ code_decl
                n = cVar' v
            valOrRefOpReturn tspec (varType v) code_decl
                (return (decl' ++ d ++ [ cAssignStmt n $ cFuncCall fcall $ args ++ targs ]))
                (return (decl' ++ d ++ [ cFuncCallStmt fcall (cExprAddr n : args ++ targs) ])))
        return $ decl ++ alloc
    auxMac = do
        tname <- cTypeName tspec v
        (p, d) <- extractParams tspec v
        let n = cVar' v
            fdcall = fCall tspec tname code_decl
        decl <- if isGlobalVar v then return [] else valOrRefOpMacroReturn tspec (varType v) code_decl
            (caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapVarDefinition>:\
                 \ Not expecting macro variable declaration returning a value")
            (return [ cFuncCallStmt fdcall (n : p) ])
        let ficall = fCall tspec tname code_init_def
        vini  <- valOrRefOpMacroReturn tspec (varType v) code_init_def
            (return [ cAssignStmt n $ cFuncCall ficall p ])
            (return [ cFuncCallStmt ficall (n : p) ])
        return (d ++ decl ++ vini)

--------------------------------------------------------------------------------
-- Variable declaration
mapVarDecl 
    :: CaoMonad m 
    => TranslationSpec -> VarDecl Var 
    -> m [CBlockItem]
mapVarDecl tspec v = case v of
    VarD (unLoc -> n) _ Nothing  -> varMemory tspec n >> varDeclaration tspec n
    ContD (unLoc -> n) _ e       -> varMemory tspec n >> varDeclInit tspec n e
    _ -> caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapVarDecl>:\
        \ precondition violation:\n" ++ showPpr v

varDeclaration 
    :: CaoMonad m 
    => TranslationSpec -> Var 
    -> m [CBlockItem]
varDeclaration tspec v 
    | isCRef v = return [ cVarDeclStmt (getSymbol v) (tPrefix tspec caoRef) ]
    | isCStruct v = return [ cVarDeclStmt (getSymbol v) (tPrefix tspec (getTName v)) ]
    | otherwise = varOrMacroDecl tspec (varType v) auxVar auxMacro
    where
    auxVar = do
        decl <- if isGlobalVar v then return [] else liftM (singleton . cVarDeclStmt (getSymbol v) . tPrefix tspec) . cTypeName tspec $ v
        alloc <- autoOrAlloc tspec (varType v) (return []) (do
            typ <- cTypeName tspec v
            (args, d) <- extractParams tspec v
            (targs, decl') <- cTypeCodeArgs tspec (typeOf v)
            let fcall = fCall tspec typ code_decl
                n = cVar' v
            valOrRefOpReturn tspec (varType v) code_decl
                (return (decl' ++ d ++ [ cAssignStmt n $ cFuncCall fcall $ args ++ targs ]))
                (return (decl' ++ d ++ [ cFuncCallStmt fcall (cExprAddr n : args ++ targs) ])))
        return $ decl ++ alloc
    auxMacro = do
        tname <- cTypeName tspec v
        (p, d) <- extractParams tspec v
        let n = cVar' v
            fdcall = fCall tspec tname code_decl
        decl <- if isGlobalVar v then return [] else valOrRefOpMacroReturn tspec (varType v) code_decl
            (caoError defSrcLoc $ mkUnknownErr $ "<CaoToC.h>.<mapVarDefinition>:\
                 \ Not expecting macro variable declaration returning a value")
            (return [ cFuncCallStmt fdcall (n : p) ])
        let ficall = fCall tspec tname code_init_def
        vini  <- valOrRefOpMacroReturn tspec (varType v) code_init_def
            (return [ cAssignStmt n $ cFuncCall ficall p ])
            (return [ cFuncCallStmt ficall (n : p) ])
        return (d ++ decl ++ vini)

varDeclInit 
    :: CaoMonad m 
    => TranslationSpec -> Var -> [TLExpr Var] 
    -> m [CBlockItem]
varDeclInit tspec v exps = do
    let typ = varType v
        intyp = head $ innerType typ
    (_, constArray) <- freshSmb
    tname <- typeName tspec typ
    vdecl <- varDeclaration tspec v
    exps' <- mapExps tspec exps
    cdecl <- autoOrAlloc tspec intyp
        (return $ cIntArrayDecl constArray exps')
        (return $ cCharArrayDecl constArray exps')
    let fcall = fCall tspec tname code_init
    adecl <- opReturnKind' tspec typ code_init
        (return [ cAssignStmt (cVar' v) $ cFuncCall fcall [cVar constArray] ])
        (return [ cFuncCallStmt fcall [cVar' v, cVar constArray ] ])
        (do (p, d) <- extractParams' tspec typ
            return $ d ++ [ cAssignStmt (cVar' v) $ cFuncCall fcall $ [cVar constArray] ++ p])
        (do (p, d) <- extractParams' tspec typ
            return $ d ++ [ cFuncCallStmt fcall $ [cVar' v, cVar constArray] ++ p])
    
    return $ cdecl : vdecl ++ adecl

--------------------------------------------------------------------------------
-------------------------------------------- Exp -------------------------------

mapExps 
    :: CaoMonad m 
    => TranslationSpec -> [TLExpr Var] 
    -> m [CExpr]
mapExps tspec = mapM (mapExp tspec)

mapExp 
    :: CaoMonad m 
    => TranslationSpec -> TLExpr Var 
    -> m CExpr
mapExp tspec e = case unTyp $ unLoc e of
    Lit l                                    -> mapLiteral tspec (typeOf e) l
    Var v                                    -> return $ cVar' v
    StructProj (unLoc -> unTyp -> Var v) fld -> return $ mapProj v fld
    _               -> internalError
        "mapExp" "Not expected case"

--------------------------------------------------------------------------------
-- Left values

mapLVal 
    :: LVal Var 
    -> CExpr
mapLVal (LVVar (unLoc -> v)) = cVar' v
mapLVal (LVStruct (LVVar (unLoc -> v)) fld) = mapProj v fld
mapLVal _ = internalError "mapLVal" "Not expected case."

mapProj :: Var -> Var -> CExpr
mapProj v fld = CMember (cVar' v) (internalIdent (getSymbol fld)) False undefNode 

--------------------------------------------------------------------------------
------------------------------ Literals ----------------------------------------

mapLiteral 
    :: CaoMonad m 
    => TranslationSpec -> Type Var -> Literal Var 
    -> m CExpr
mapLiteral tspec i l = case l of
    BLit b   -> let
            b' = mapBoolLiteral b
        in autoOrAlloc tspec i
            (return $ cIntExpr b')
            (return $ cStringExpr $ show b')
    ILit v          ->
        autoOrAlloc tspec i 
            (return $ cIntExpr v) 
            (return $ cStringExpr $ show v)
    BSLit s bits      -> let
            v = mapBitString s bits
        in autoOrAlloc tspec i 
            (return $ cIntExpr v) 
            (return $ cStringExpr $ show v)
    PLit p   ->
        autoOrAlloc tspec i 
            (return $ cIntExpr $ mapSimplePolynomial p)
            (return $ cStringExpr $ showMonomials $ mapPolynomial p)

mapBoolLiteral :: Bool -> Integer
mapBoolLiteral b = if b then cTrueValue else cFalseValue

mapBitString :: Sign -> [Bool] -> Integer
mapBitString s bs = case s of
    U -> ubitsToInteger bs 
    S -> sbitsToInteger bs

--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
----------------------------- Polynomial ---------------------------------------

mapPolynomial :: Pol Var -> [IExpr Var]
mapPolynomial p = case p of
    Pol [Mon (CoefI i) EZero] -> [i]
    Pol mlst                  -> mapMonomials mlst

mapSimplePolynomial :: Pol Var -> Integer
mapSimplePolynomial p = case p of
    Pol [Mon (CoefI (IInt i)) EZero] -> i
    Pol [Mon (CoefI _) EZero] -> internalError "mapSimplePolynomial" "<<TODO>>: non literal"
    Pol _                     -> internalError "mapSimplePolynomial" "Unexpected polynomial literal"

--------------------------------------------------------------------------------
----------------------------- Monomials ----------------------------------------

showMonomials :: [IExpr Var] -> String
showMonomials = intercalate ";" . map (show . getInteger)

getInteger :: IExpr Var -> Integer
getInteger (IInt n) = n
getInteger _ = internalError "getInteger" "Not expected non-literal"

mapMonomials :: [Mon Var] -> [IExpr Var]
mapMonomials lm = case lm of
    [] -> error "<CaoToC.h>.<mapMonomials>: precondition violation: empty list"
    Mon (CoefP _) _: _ -> error $ "<CaoToC.h>.<mapMonomials>:\n"
                                    ++ concatMap showPpr lm
    Mon (CoefI _) _: _ ->
        uncurry mapMonomial $ split (getMonExp . head) id lm
        -- Invariant: The list of monomials is ordered by decresing degree

mapMonomial :: Integer -> [Mon Var] -> [IExpr Var]
mapMonomial 0 [] = IInt 0 : []
mapMonomial 0 (Mon (CoefI i) _ : _) = i : []
mapMonomial n [] = IInt 0 : mapMonomial (n-1) []
mapMonomial n ml@(Mon (CoefI _) EZero : _) = IInt 0 : mapMonomial (n-1) ml
mapMonomial n ml@(Mon (CoefI icoef) (MExpI _ n'): mlst)
    | n == n'   = icoef  : mapMonomial (n-1) mlst
    | otherwise = IInt 0 : mapMonomial (n-1) ml
mapMonomial _ _ = internalError "mapMonomial" "Not expected case"

--------------------------------------------------------------------------------
--

varMemory :: CaoMonad m => TranslationSpec -> Var -> m ()
varMemory tspec v
    | isCStruct v || isCRef v || isGlobalVar v = return ()
    | otherwise = autoOrAlloc tspec (varType v) (return ()) (storeAllocVar v)

-- Wrapper for creating C declarations from pairs string/type
cArgs :: CaoMonad m =>
    TranslationSpec -> String -> TyDecl Var -> Type Var -> m CDecl
cArgs tspec nm (TySynD n) _ = 
    return $ cParamDecl nm $ cType (tPrefix tspec $ getSymbol (unLoc n))
cArgs tspec nm _ typ          = liftM (cParamDecl nm . snd) (mapType tspec typ)

--------------------------------------------------------------------------------
-- Auxiliary functions

cVar' :: Var -> CExpr
cVar' = cVar . getSymbol

mapIndex :: IExpr Var -> CExpr
mapIndex (IInt n) = cIntExpr n
mapIndex (IInd v) = cVar' v
mapIndex _ = internalError "mapIndex" "Not expected index."

--------------------------------------------------------------------------------

cTypeCodeArgs :: CaoMonad m => TranslationSpec -> Type Var -> m ([CExpr], [CBlockItem])
cTypeCodeArgs tspec i 
    | isSimpleType i = return ([], [])
    | otherwise = do
        let i' = innerType i
        ctc <- concatMapM (cTypeCode tspec) i'
        (ilst, d) <- concatMapAndUnzipM (cTypeParams tspec) i'
        (param, decl) <- if null ilst
            then return ([ cIntExpr 0 ], [])
            else do
                (_, paramArray) <- freshSmb
                let decl = cPointerArrayDecl paramArray ilst
                return ([ cVar paramArray ], [decl])
        return (cStringExpr ctc : param, d ++ decl)

---------------------------------------- CAOType -------------------------------

cTypeCode :: CaoMonad m => TranslationSpec -> Type Var -> m String
cTypeCode tspec = cTypeCode'
    where
    cTypeCode' :: CaoMonad m => Type Var -> m String
    cTypeCode' t = do
        c <- codes tspec t 
        c' <- case t of
          Int  -> return []
          RInt -> return []
          Bool -> return []
          Bits _ _ -> return []
          Mod Nothing Nothing (Pol [Mon (CoefI _) EZero]) -> return []
          Mod (Just b) _ _ ->
              if isModInt b
                  then return []
                  else caoError defSrcLoc $ NestedModpolErr t
          Vector _ t'   -> cTypeCode' t'
          Matrix _ _ t' -> cTypeCode' t'
          Struct _ flds -> concatMapM (cTypeCode' . snd) flds
          _ -> caoError defSrcLoc $ NotSupportedTypeErr t
        return $ c ++ c'

cTypeParams :: CaoMonad m => TranslationSpec -> Type Var -> m ([CExpr], [CBlockItem])
cTypeParams tspec = worker
    where
    worker :: CaoMonad m => Type Var -> m ([CExpr], [CBlockItem])
    worker t = do
        i <- cTypeCode' t
        concatMap2M aux i

    aux [] = return (cIntExpr 0, [])
    aux [IInd v] = do
        v' <- valOrRef tspec (varType v) (return cExprAddr) (return id)
            `apM` cVar' v
        return (v', [])
    aux [IInt n] = do
        (_, paramArray) <- freshSmb
        ctc <- typeName tspec RInt
        let decl = cTypeArrayDecl paramArray (tPrefix tspec ctc) [ cIntExpr n ]
        return ( cVar paramArray, [decl] )
    aux [i, j] = do
        (_, paramArray) <- freshSmb
        ctc <- typeName tspec RInt
        let a = mapIndex i : mapIndex j : []
            decl = cTypeArrayDecl paramArray (tPrefix tspec ctc) a
        return ( cVar paramArray, [decl])

    aux _ = internalError "cTypeCode.aux" "Not expected value"

    cTypeCode' :: CaoMonad m => Type Var -> m [[IExpr Var]]
    cTypeCode' t =
        case t of
          Int  -> return [[]]
          RInt -> return [[]]
          Bool -> return [[]]
          Bits _ n -> return [[n]]
          Mod Nothing Nothing (Pol [Mon (CoefI m) EZero]) -> return [[m]]
          Mod (Just b) _ _ ->
              if isModInt b
                  then return [[]]
                  else caoError defSrcLoc $ NestedModpolErr t
          Vector n t'   -> do
              ilst <- cTypeCode' t'
              return ([n] : ilst)
          Matrix n m t' -> do
              ilst <- cTypeCode' t'
              return ([n , m] : ilst)
          Struct _ flds -> do
              liftM ([IInt $ genericLength flds] : ) $ concatMapM (cTypeCode' . snd) flds
          _ -> caoError defSrcLoc $ NotSupportedTypeErr t

extractParams :: CaoMonad m => TranslationSpec -> Var -> m ([CExpr], [CBlockItem])
extractParams tspec = extractParams' tspec . varType

extractParams' :: CaoMonad m => TranslationSpec -> Type Var -> m ([CExpr], [CBlockItem])
extractParams' tspec i = case i of
    Bits _ m          ->
        return (mapIndex m : [], [])
    Vector m _        -> do
        return (mapIndex m : [], [])
    Matrix m n _      -> do
        return (mapIndex m : mapIndex n : [], [])
    Mod Nothing Nothing (Pol [Mon (CoefI m) EZero]) -> do
        return (mapIndex m : [], [])
    Mod (Just (Mod Nothing Nothing (Pol [Mon (CoefI m) EZero]))) (Just _) pol
                    -> polyParams tspec m pol
    Mod (Just _) (Just _) _
                    -> caoError defSrcLoc $ NestedModpolErr i
    Struct _ flds     -> return ([cIntExpr $ genericLength flds], [])
    _                 -> return ([], [])

polyParams :: CaoMonad m => TranslationSpec -> IExpr Var -> Pol Var -> m ([CExpr], [CBlockItem])
polyParams tspec m pol =  do
    (_, paramArray) <- freshSmb
    ctc <- typeName tspec Int
    let m' = mapIndex m
        pol' = map mapIndex (mapPolynomial pol)
        decl = cTypeArrayDecl paramArray (tPrefix tspec ctc) pol'
    return ([ dg (degree pol), m', cVar paramArray ], [decl])
    --return ([ cIntExpr (degree pol), m', cVar paramArray ], [decl])

    where
    -- XXX: This should be improved since it may not work in all cases
    dg n = cVar $ "c_const_int_" ++ show n

--------------------------------------------------------------------------------
isComposed :: Type Var -> Bool
isComposed t = isVector t || isMatrix t
  
cTypeCodeRedux :: CaoMonad m => TranslationSpec -> Type Var -> m Char
cTypeCodeRedux tspec = liftM head . codes tspec

isCStruct' :: LVal Var -> Bool
isCStruct' (LVVar (unLoc -> v)) = isCStruct v
isCStruct' (LVStruct (LVVar (unLoc -> v)) _) = isCStruct v
isCStruct' _ = error "Not expected function call result"

isCStructExpr :: Expr Var -> Bool
isCStructExpr (Var e) = isCStruct e
isCStructExpr _ = False

-- Translation of type names
cTypeName :: CaoMonad m => TranslationSpec -> Var -> m String
cTypeName tspec = typeName tspec . varType

cProc :: TranslationSpec -> String -> [CBlockItem] -> CFunDef
cProc tspec name body = cFuncDefinition name [] (tPrefix tspec caoRes) $
    CCompound [] (body ++ cReturn caoOk : []) undefNode 

tPrefix :: TranslationSpec -> String -> String
tPrefix tspec = ((typePrefix tspec ++ "_") ++)

moduleName :: String
moduleName = "<Language.CAO.Translation.C>"

internalError :: String -> String -> a
internalError funcName msg = error $
    moduleName ++ ".<" ++ funcName ++ ">: " ++ msg