{-  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 PatternGuards #-}

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

After handling constants, the next step is to make the CAO code as close as 
possible to the final C code. In more detail, the following actions are 
performed:
* All CAO native operations are replaced by a call to a function with the 
same name as the respective implementation in the static library. For 
instance, the following CAO code, where 'a', 'b' and 'r' are integer variables

@r := a + b;@

is transformed to

@r := CAO_int_add(a, b);@

In particular, the called name follows the convention: 

@{prefix} {type name} {operation name}(argument list)@

* Accesses to vectors or matrices are replaced by extraction of references. 
Although CAO does not support references, this is completely transparent 
since these are treated as a special kind of variable. For instance, the 
following assignment to a vector v of integers, where n is an integer

@v[0] := n;@

is transformed to

@
def t : REF;
t := CAO_vector_ref(v, 0);
t := CAO_int_assign(n);
@

In the final translation step, the variable t will be translated to a real 
reference.

* Operation and function arguments are handled according to the specification 
of safety, as explained in the previous section. If an operation in specified 
as unsafe, a copy of its arguments is generated. If an operation is argument 
safe, a copy of the argument used as result is generated as in the case 
@a := <op>(a,b)@. This assumes that the compiler does not introduce aliasing 
and that variables can be distinguished by their name. The introduction of 
references described above in not a problem since it always references a 
region of a container and cannot be mixed with other references.
We should notice that the implementation of the init and assign operations in 
the library must be safe. Otherwise, a copy would not solve the problem as 
these are the operations used to copy values. Also, ref operations must be safe 
since extracting a reference should not change its argument.

* Calls to structure fields are replaced by integers accordingly with the 
specification. For instance, let us consider the following structure in CAO:

@
typedef S := struct [
    def n : int;
    def b : bool;
];
@

and that we have the following code:
@
     def i : int;
     i   := s.n;
     s.b := true;
@

The inlining option makes the integer constant to be used directly in the 
selection functions:

@
     c_i := CAO_struct_select(c_s, 0);
     c_t := CAO_bool_init(true);
     c_t50 := CAO_struct_ref(c_s, 1);
     c_t50 := CAO_bool_assign(c_t);
@

In this case, the field n was replaced by 0 and the field b was replaced by 1. 
The global variable option replaces the call by a global variable:

@
     c_i := CAO_struct_select(c_s, c_n);
     c_t52 := CAO_struct_ref(c_s, c_b);
     c_t52 := CAO_bool_assign(c_const_true);
@

which is initialized in the global init procedure:

@
     def init() : void {
       c_n := CAO_int_init(0);
       c_b := CAO_int_init(1);
       c_const_true := CAO_bool_init(true);
}
@

* The specification allows us to determine if values should be returned by 
value or by reference. The language also allows us to return several results 
simultaneously. The chosen mechanism for returning several values or references 
were C structures.

For instance, let us consider the swap function which returns two integer, and 
that integers in this platform are returned by value:

@
     def swap(a : int, b : int) : int, int {
         return b, a;
}
@

In this phase, a structure to return the two integers is generated using CAO 
syntax. However, this will be directly mapped to C structures since it is not 
a user defined CAO structure.

@
typedef sRes55 := struct[def c_sRes55_0 : int;
                              def c_sRes55_1 : int;];
     def c_swap(c_a : int, c_b : int) : sRes55 {
       def c_CAO_t58 : sRes55;
       c_CAO_t58.c_sRes55_0 := CAO_int_assign(c_b);
       c_CAO_t58.c_sRes55_1 := CAO_int_assign(c_a);
       return c_CAO_t58;
}
@

A call to the swap function:

@
     n1, n2 := swap(m1, m2);
@

is transformed to

@
     def c_CAO_t65 : sRes59;
     c_CAO_t65 := c_swap(c_m1, c_m2);
     c_n1 := CAO_int_assign(c_CAO_t65.c_sRes59_0);
     c_n2 := CAO_int_assign(c_CAO_t65.c_sRes59_1);
@

-}

module Language.CAO.Translation.PreC 
    ( cao2prec
    , precStatement 
    , precAssignment
    ) where

import Control.Monad

import Data.List (partition)

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

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

import Language.CAO.Syntax
import Language.CAO.Syntax.Utils (type2TyDecl, typeOf, Typeable)

import Language.CAO.Translation.Names

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

-- This module should:
-- * Replace CAO operations by calls to functions with the same name as in the backend
-- * Handle operation and function arguments accordingly with the specification of safety,
--   making copies whenever necessary
--   *_init and *_assign have to be safe. Otherwise, a copy would not solve the problem.
-- * Distinguish between values returned by value or by reference and create the necessary
--   structure declarations
-- * Replace calls to struct fields by integers
-- * ??? Replace CAO types by backend types???
-- Safe operations by design:
--   *_init
--   *_assign
--   *_ref

--------------------------------------------------------------------------------
-- CaoAST

cao2prec 
    :: CaoMonad m 
    => TranslationSpec -> Prog Var 
    -> m (Prog Var)
cao2prec tspec (Prog defs (Just ip)) = withPreCST $ do
    (defs', fldDefs) <- concatMapAndUnzipM (precDefinition tspec) defs
    -- The init procedure does not return any value, thus it is safe to ignore
    -- the second value of 'precFunc'
    (ip', _) <- precFunc tspec ip 
    return $ Prog defs' (Just (aux fldDefs ip'))
    where
    aux :: [FieldDef] -> Fun Var -> Fun Var
    aux s f = f { funBody = s ++ funBody f } 
cao2prec _ _ = internalError "cao2prec" "No init function"

--------------------------------------------------------------------------------
precDefinition 
    :: CaoMonad m 
    => TranslationSpec -> LDef Var 
    -> m ([LDef Var], [FieldDef])
precDefinition tspec (L l d) = case d of
    VarDef _   -> return (L l d : [], [])
    FunDef fd  -> do
        (fd', structDecl) <- precFunc tspec fd
        return (consMaybe structDecl $ L l (FunDef fd') : [], [])
    TyDef td   -> precTypeDef tspec l td
    ConstDef _ -> return (L l d : [], [])

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

type FieldDef = LStmt Var
type StructResDecl = LDef Var

precTypeDef 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> TyDef Var 
    -> m ([LDef Var], [FieldDef])
precTypeDef tspec l (StructDecl sname lFlds) = liftM (mapFst (L l (TyDef $ TySynDef sname $ TySynD sname) : )) $
    globalOrInlinedField tspec 
    (liftM unzip            $ zipWithSeqM auxGlobal  lFlds)
    (liftM (const ([], [])) $ zipWithSeqM auxInlined lFlds)
    where

    auxGlobal :: CaoMonad m => Integer -> (Located Var, TyDecl Var) -> m (LDef Var, FieldDef)
    auxGlobal fldIndex (nm, _) = do
        nm' <- liftM (L (getLoc nm)) $ freshVar' Global (getSymbol (unLoc nm)) RInt
        let decl = L l $ VarDef $ VarD nm' (type2TyDecl RInt) Nothing 
        assign <- fCallSAux tspec code_init (LVVar nm') [rintLit fldIndex]
        return (decl, genLoc assign)

    auxInlined :: CaoMonad m => Integer -> (Located Var, TyDecl Var) -> m ()
    auxInlined fldIndex (nm, _) = putFieldProj (unLoc nm, fldIndex)

    
precTypeDef _ l t = return ([L l $ TyDef t], [])

--------------------------------------------------------------------------------
precFunc 
    :: CaoMonad m 
    => TranslationSpec -> Fun Var 
    -> m (Fun Var, Maybe StructResDecl)
precFunc tspec (Fun (L loc fn) args _ body) = do
    resetPreCST

    let typ@(FuncSig ta _ c) = varType fn

    (rtype, sdef, rsdef) <- precReturnType tspec typ
    let retD' = map type2TyDecl rtype
        typ'  = FuncSig ta (Tuple rtype) c
        fn'   = L loc $ setType typ' fn
    putFunType fn typ'

    body' <- precBlocks tspec body
    refV  <- getRefVar
    tmpvs <- getTmpVars
    refV' <- mapMaybeM refVarDecl refV

    let body'' = insertTmps body' tmpvs
    
    return (Fun fn' args retD' (consMaybe refV' (consMaybe rsdef body'')), sdef)

    where
    refVarDecl v = do
        t <- freshVar' Global caoRef Bullet
        return $ genLoc $ VDecl $ VarD (genLoc v) (TySynD (genLoc t)) Nothing

    insertTmps bd tmpvs = let
            (dep, noDep)   = partition (isDependent . varType) tmpvs
        in insertAll (map varDecl' noDep) (map varDecl' dep) bd

    varDecl' = genLoc . VDecl . varDecl

    insertAll nodeps deps [] = nodeps ++ deps
    insertAll [] deps (L l (Nop EndIndex)  : sts) = L l (Nop EndIndex) : deps ++ sts
    insertAll _  _ (L _ (Nop EndIndex)  : _) = internalError "insertAll" "Not expected order"
    insertAll nodeps deps (L l (Nop EndConsts) : sts) = L l (Nop EndConsts) : nodeps ++ insertAll [] deps sts
    insertAll nodeps deps (s : sts) = s : insertAll nodeps deps sts

precReturnType 
    :: CaoMonad m 
    => TranslationSpec -> Type Var 
    -> m ([Type Var], Maybe StructResDecl, Maybe ReturnStructDecl)
precReturnType tspec (FuncSig _ (fromTuple -> rtype) _) = do
    (vtyp, rtyp) <- returnByValOrRef tspec rtype
    (vtyp', sdecl, rsdecl) <- precByVal vtyp
    return (consMaybe vtyp' rtyp, sdecl, rsdecl)
    where

    precByVal :: CaoMonad m => [Type Var] -> m (Maybe (Type Var), Maybe StructResDecl, Maybe ReturnStructDecl)
    precByVal [] = return (Nothing, Nothing, Nothing)
    precByVal [t] = valOrRef tspec t 
            (return (Just t, Nothing, Nothing)) -- Single value variable returned directly
            (returnStruct =<< newStructRes [t])
    precByVal typs = returnStruct =<< newStructRes typs

    returnStruct (t, sd) = do
        (fv, sdecl) <- returnStructDecl tspec t
        putRetStruct fv
        return (Just t, Just sd, Just sdecl)
precReturnType _ _ = internalError
    "precReturnType" "Unexpected function type."

--------------------------------------------------------------------------------
-- Handling structs to return results of functions

type ReturnStructDecl = LStmt Var

-- Returns a new struct with a field of each given typ
newStructRes
    :: CaoMonad m
    => [Type Var]
    -> m (Type Var, StructResDecl)
newStructRes typs = do
    uid <- uniqId
    let tname = structRes ++ show uid
        sname = mkGId (mkTvName tname) uid Bullet
    sflds <- zipWithSeqM (newStructField tname sname) typs
    let struct = Struct sname sflds
    return ( struct
           , genLoc $ TyDef $ StructDecl (genLoc sname) 
                (map (mapPair genLoc type2TyDecl) sflds))
    where
    newStructField tname sname n typ = do
        fld <- freshSFld (tname ++ "_" ++ show n) (SField sname typ)
        return (fld, typ)

-- Declares a new struct variable to return results
returnStructDecl
    :: CaoMonad m
    => TranslationSpec -> Type Var
    -> m (Var, ReturnStructDecl)
returnStructDecl tspec typ@(Struct sname _) = do
    (i, sn) <- freshSmb
    let fv = mkCStruct sn i typ (typePrefix tspec) (getSymbol sname)
    let decl = genLoc $ VDecl $ VarD (genLoc fv) (type2TyDecl typ) Nothing
    return (fv, decl)
returnStructDecl _ _ = internalError "returnStructDecl" "Not expected case"


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

precBlocks 
    :: CaoMonad m 
    => TranslationSpec -> [LStmt Var] 
    -> m [LStmt Var]
precBlocks tspec = concatMapM (precStatement tspec)

precStatement 
    :: CaoMonad m 
    => TranslationSpec -> LStmt Var 
    -> m [LStmt Var]
precStatement tspec (L l (VDecl vd)) = 
    liftM (singleton . L l . VDecl) $ precVDecl tspec vd

-- TODO: Constant declaration must be processed because of the change in Target
precStatement tspec (L l (CDecl cd)) = do
    (cd', stmt) <- precCDecl tspec cd
    return (L l (CDecl cd') : stmt)

precStatement tspec (L l (Assign lv [L l' (TyE _ (FunCall (L lf fn) args))])) = do
    Just ftyp <- getFunType fn
    let fn' = L lf $ setType ftyp fn
    (lv', decl, assign) <- precReturnLVal tspec lv ftyp
    (args', stmts) <- safetyCopy tspec lv args
    return $ decl ++ stmts ++ L l (Assign lv' [L l' (annTyE ftyp (FunCall fn' args'))]) : assign

precStatement tspec (L l (Assign [lv] [ex])) =
    precAssignment tspec l lv ex

precStatement _ (L _ (Assign _ _)) = 
    internalError "precStatement" "Unexpected assignment case"

precStatement tspec (L l (FCallS pn ex))  = do
    (ex', stmts) <- safeOrUnsafeDefault tspec
        (return (ex, []))
        (genUnsafeCopy tspec ex)
        (return (ex, [])) --- There is no need to make a copy to make it arg
            -- safe, because there is no result assignment since this is a
            -- procedure
    return $ stmts ++ [ L l $ FCallS pn ex' ]

precStatement tspec (L l (Ret exps)) = do
    precReturn tspec l exps

precStatement tspec (L l (Ite ex ifBlock eBlock)) = do
    ifBlock'    <- precBlocks tspec ifBlock
    eBlock'     <- mapMaybeM (precBlocks tspec) eBlock
    return [ L l $ Ite ex ifBlock' eBlock' ]
        
precStatement tspec (L l (While ex whileBlock)) = do
    whileBlock' <- precBlocks tspec whileBlock
    return [ L l $ While ex whileBlock' ]

precStatement tspec (L l (Seq i seqBlock)) = do
    seqBlock' <- precBlocks tspec seqBlock
    return [ L l $ Seq i seqBlock' ]

precStatement _ (L l (Nop a)) = return [L l (Nop a)]

{-
Note
The translation of 'if' and 'while' statements will use native C support.
Therefore, it is assumed that these operations are safe and do not need 
previous copy of the values.
-}
--------------------------------------------------------------------------------

precReturnLVal 
    :: CaoMonad m 
    => TranslationSpec -> [LVal Var] -> Type Var 
    -> m ([LVal Var], [ReturnStructDecl], [LStmt Var])
precReturnLVal tspec lvs (FuncSig _ (Tuple (ht:_)) _) = do
    (vlv, rlv) <- returnByValOrRef tspec lvs
    if null vlv then return (rlv, [], [])
        else case ht of
            typ@(Struct _ flds) -> do
                (fv, decl) <- returnStructDecl tspec typ
                assign <- zipWithM (aux fv) vlv flds 
                return (LVVar (genLoc fv) : rlv, [decl], assign)
            _ -> return (vlv ++ rlv, [], [])
    where

    aux fv lv (fld, _) = liftM genLoc $ 
        fCallSAux tspec code_init lv [genLoc $ annTyE (varType fld) $ StructProj (genLoc (annTyE (varType fv) (Var fv))) fld]
precReturnLVal _ _ _ = internalError
        "precReturnLVal" "Unexpected case."

precReturn 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> [TLExpr Var] 
    -> m [LStmt Var]
precReturn tspec loc exps = do
    (val, ref) <- returnByValOrRef tspec exps
    (val', stmt) <- precByVal val
    return $ stmt ++ [ L loc $ Ret $ val' `consMaybe` ref ]
    where
    precByVal :: CaoMonad m => [TLExpr Var] -> m (Maybe (TLExpr Var), [LStmt Var])
    precByVal []   = return (Nothing, [])
    precByVal [v]  =
        valOrRef tspec (typeOf v)
            (return (Just v, [])) -- Single value variable returned directly
            (liftM wrap $ precByVal' [v])
    precByVal vals = liftM wrap $ precByVal' vals

    wrap (a, b) = (Just a, b)

    precByVal' :: CaoMonad m => [TLExpr Var] -> m (TLExpr Var, [LStmt Var])
    precByVal' vals = do
        Just fv <- getRetStruct
        let Struct _ flds = varType fv
        block <- zipWithM (\ (fld, _) ex -> do
            sfld <- freshSFld (getSymbol fld) (varType fld)
            case unLoc ex of
                -- Init is safe because it takes constants
                TyE t (Lit l) -> do
                    l' <- precLiteral tspec t l
                    liftM genLoc $ fCallSAux tspec code_init (LVStruct (LVVar (genLoc fv)) sfld) (map (L (getLoc ex) . TyE t . Lit) l')
                -- Assign must be safe, otherwise the system would not be safe
                TyE _ (Var _) -> liftM genLoc $ fCallSAux tspec code_assign (LVStruct (LVVar (genLoc fv)) sfld) [ex]
                _ -> error "Not expected"
            ) flds vals
        return (genLoc $ annTyE (varType fv) $ Var fv, block)

--------------------------------------------------------------------------------
precAssignment 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> LVal Var -> TLExpr Var 
    -> m [LStmt Var]
precAssignment tspec loc lv ex = case lv of
    LVVar (unLoc -> vid)    -> assignSimpleLVal vid 
    LVStruct lv' fld -> do
        fld' <- precField tspec fld
        precSimpleAssign tspec loc lv' [ex, fld']
    LVCont _ lv' (VectP (CElem iexp)) 
        -> precSimpleAssign tspec loc lv' [ex, iexp]
    LVCont _ lv' (VectP (CRange iexp jexp)) 
        -> precRangeAssign tspec loc code_range_set lv' [ex, iexp, jexp]
    LVCont _ lv' (MatP (CElem ce) (CElem re)) 
        -> precSimpleAssign tspec loc lv' [ex, ce, re]
    LVCont _ lv' (MatP (CRange ci cj) (CRange ri rj))
        -> precRangeAssign tspec loc code_range_set lv' [ex, ci, cj, ri, rj]
    LVCont _ lv' (MatP (CRange lre rre) (CElem cole))
        -> precRangeAssign tspec loc code_row_range_set lv' [ex, cole, lre, rre]
    LVCont _ lv' (MatP (CElem rowe) (CRange lce rce))
        -> precRangeAssign tspec loc code_col_range_set lv' [ex, rowe, lce, rce]

    where

    assignSimpleLVal vid = case unLoc ex of
        TyE t (Lit l)         -> do
            l' <- precLiteral tspec t l
            let ex' = map (L (getLoc ex) . TyE t . Lit) l'
            let typ = typeOf ex
            n <- cCall tspec code_init typ
            return $ L loc (Assign [lv] [genLoc $ annTyE typ $ FunCall (genLoc n) ex' ]) : []
            
        TyE _ (Var _)           -> do
            let typ = typeOf ex
            n <- cCall tspec code_assign typ
            return $ L loc (Assign [lv] [genLoc $ annTyE typ $ FunCall (genLoc n) [ex] ]) : []

        TyE td (Cast _ _ ce)  -> assignCast vid td ce
        TyE _ (StructProj s f)  -> do
            f' <- precField tspec f
            assignGeneral vid [s, f']
        _               -> assignGeneral vid (getArgExps ex)

    assignCast vid td ce = do
        let typ = typeOf ce
        n <- liftM (L (getLoc ex)) $ cCastCall tspec typ td
        (ce', stmts) <- safetyCopy' tspec typ code_cast [vid] [ce]
        return $ stmts ++ [ L loc $ Assign [lv] [L (getLoc ex) $ annTyE td $ FunCall n ce'] ]

    assignGeneral vid args = do
        let fcode = codeOf $ unTyp $ unLoc ex
            typ = typeOf $ head args
        n <- cCall tspec fcode typ
        (args', stmts) <- safetyCopy' tspec typ fcode [vid] args
        return $ stmts ++ [ L loc $ Assign [lv] [L (getLoc ex) $ annTyE (typeOf lv) $ FunCall (genLoc n) args' ] ]

{-
Note
Some operations have of the backend must be safe. Otherwise it would not
be possible to ensure the safety of the translation. These operations are:
* initialization       -> code_init
* assignment           -> code_assign
* reference extraction -> code_ref
* global references    -> cGlobalRef
-}

-- Precondition: the list is not empty
precRangeAssign 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> OpCode -> LVal Var -> [TLExpr Var] 
    -> m [LStmt Var]
precRangeAssign tspec loc op lv exps = do
    (root, path) <- precLValue tspec lv
    if null path 
        then simpleLVal root
        else composedLVal root path 
    
    where
    simpleLVal (L rl root) = do
        n1 <- cCall tspec op (typeOf lv)
        (exps'', stmts) <- safetyCopy' tspec (typeOf lv) op [root] exps
        return $ stmts ++
             assign (L rl root) n1 exps'' : []

    composedLVal (L rl root) path = do 
            fv <- getRefVariable
            let n1 = cGlobalRef (typePrefix tspec) -- [See Note]
            n2 <- cCall tspec op (typeOf lv)
            (exps', stmts) <- safeOfUnsafe tspec (typeOf lv) op
                (return (exps, []))
                (genUnsafeCopy tspec exps)
                (return (exps, [])) -- TODO: Is this a bug?
            return $ stmts ++ 
                     assign (genLoc fv) n1 (L rl (annTyE (varType root) (Var root)) : path ) :
                     assign (genLoc fv) n2 exps' : []

    assign l fn exps' = L loc $ Assign [LVVar l] [genLoc $ annTyE (typeOf l) $ FunCall (genLoc fn) exps']

-- Precondition: the list is not empty
precSimpleAssign 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> LVal Var -> [TLExpr Var] 
    -> m [LStmt Var]
precSimpleAssign tspec loc lv exps@(ex:exps') = do
    (root, path) <- precLValue tspec lv
    if null path
        then simpleLVal root
        else composedLVal root path

    where
    simpleLVal (L rl root) = bitsCase (typeOf lv)
        (auxBits rl root)
        (do fv <- getRefVariable
            n1 <- cCall tspec code_ref (typeOf lv) -- [See Note]
            let c1 = assign (genLoc fv) n1 $ L rl (annTyE (varType root) (Var root)) : exps'
            c2 <- auxGen fv
            return $ c1 : c2 : []
        )

    composedLVal (L rl root) path = do
        fv <- getRefVariable
        let n1 = cGlobalRef (typePrefix tspec) -- [See Note]
        bitsCase (typeOf lv)
            (do let c1 = assign (genLoc fv) n1 $ L rl (annTyE (varType root) (Var root)) : path 
                c2 <- auxBits rl fv
                return $ c1 : c2)
            (do let c1 = assign (genLoc fv) n1 $ L rl (annTyE (varType root) (Var root)) : path ++ exps'
                c2 <- auxGen fv
                return $ c1 : c2 : [])

    auxBits rl lv' = do 
        n2 <- cCall tspec code_set (typeOf lv)
        (exps'', stmts) <- safetyCopy' tspec (typeOf lv) code_set [lv'] exps
        return $ stmts ++ assign (L rl lv') n2 exps'' : []

    -- [See Note]
    auxGen fv = do 
        (n2, ex') <- case unLoc ex of
                TyE ty (Lit l) -> do
                    nn <- cCall tspec code_init ty
                    l' <- precLiteral tspec ty l
                    return (nn, map (L (getLoc ex) . TyE ty . Lit) l')
                TyE _ (Var v)   -> do
                    let ty = varType v
                    nn <- cCall tspec code_assign ty
                    return (nn, [ex])
                _ -> error "precGenericAssign"
        return $ assign (genLoc fv) n2 ex'

    assign l fn exs = L loc $ Assign [LVVar l] [genLoc $ annTyE (typeOf l) $ FunCall (genLoc fn) exs]
precSimpleAssign _ _ _ _ = internalError "precSimpleAssign" "Not expected"

--------------------------------------------------------------------------------
-- This function takes as left value and returns its inner variable,
-- together with the complete path from the variable to the value.
precLValue 
    :: CaoMonad m 
    => TranslationSpec -> LVal Var 
    -> m (Located Var, [TLExpr Var])
precLValue _ (LVVar (L l vid)) = return (L l vid, [])
precLValue tspec (LVStruct lv fld) = do
    (e, lres) <- precLValue tspec lv
    fld'      <- precField tspec fld
    return (e, lres ++ [fld'])
precLValue tspec (LVCont _ lv (VectP (CElem iexp))) = do
    (e, lres) <- precLValue tspec lv
    return (e, lres ++ [iexp])
precLValue tspec (LVCont _ lv (MatP (CElem ce) (CElem re))) = do
    (e, lres) <- precLValue tspec lv
    return (e, lres ++ [ce, re])
precLValue _ _ =
    internalError "precLValue" "Not expected case"

--------------------------------------------------------------------------------
-- Only to split literals whenever needed
precVDecl 
    :: CaoMonad m 
    => TranslationSpec -> VarDecl Var 
    -> m (VarDecl Var)
precVDecl tspec (ContD loc typ exps) =
    liftM (ContD loc typ) $ concatMapM aux exps  
    where
    aux (L ll (TyE t (Lit l))) = 
        liftM (map (L ll . TyE t . Lit)) $ precLiteral tspec t l
    aux v = return [v]
precVDecl _ vd = return vd

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

precCDecl
    :: CaoMonad m
    => TranslationSpec -> ConstDecl Var
    -> m (ConstDecl Var, [LStmt Var])
precCDecl tspec (ConstD (L l c) d (ConstInit e)) = do
    stmt <- precAssignment tspec l (LVVar (L l c)) (annL (typeOf c) e) 
    return (ConstD (L l c) d None, stmt)
precCDecl _ cd = return (cd, [])

-------------------------------------------------------------------------------
precField 
    :: CaoMonad m 
    => TranslationSpec -> Var 
    -> m (TLExpr Var)
precField tspec fld = globalOrInlinedField tspec
    (return $ genLoc $ annTyE RInt $ Var $ setType RInt fld)
    (do nfld <- lookupFieldProj fld
        case nfld of
            Just nfld' -> return $ rintLit nfld'
            Nothing -> internalError "precField" "Field of structure not found")
-------------------------------------------------------------------------------
-- Getting the reference variable
getRefVariable :: CaoMonad m => m Var
getRefVariable = getRefVar >>= \mstr ->
  case mstr of
    Nothing -> do
      (i, vn) <- freshSmb
      let refV = mkCRef vn i caoRef
      setRefVar refV
      return refV
    Just refV -> return refV

-------------------------------------------------------------------------------
-- Literals
-- TODO: difference between signed and unsigned bits

-- TODO: Somewhere before this phase, the size of the bit string is being
-- truncated without verification of the overflow.

-- TODO: The chunk size has to be an exact divisor of the size of the type.
-- Otherwise, the is unreliable or unpredicatable.

-- Is the current backend for HIACE handling negative numbers correctly?

-- Integers are signed. Possible sign specification (signed/unsigned platform)?

-- The typechecker verifies the validity (range) of mod and modpol literals
-- We only have to validate statically if the precision of the platform is enough
-- and possibly if the literal has to be split
precLiteral 
    :: CaoMonad m 
    => TranslationSpec -> Type Var -> Literal Var 
    -> m [Literal Var]
-- For boolean literals, it is assumed that literals cannot be split.
-- This should be added to the system documentation.
precLiteral tspec typ l = checkLiteral tspec typ
    (return [l])
    (\ls -> case l of
        -- This ensures that booleans are supported
        BLit _ -> return [l]
        ILit v     -> do
            l' <- checkILit ls v
            return $ map ILit l'
        -- TODO: signed/unsigned bit strings!!
        BSLit s bits -> do
            l' <- checkBSLit ls typ bits
            return $ map (BSLit s) l'
        PLit p   -> do
            l' <- checkPLit ls typ p
            return $ map PLit l')

-------------------------------------------------------------------------------
-- Argument copy

-- Creates a copy of all variables in a list. This is used when the call to a function is 
-- not safe, i.e., it may not preserve the contents of the arguments.
genUnsafeCopy 
    :: CaoMonad m 
    => TranslationSpec -> [TLExpr Var] 
    -> m ([TLExpr Var], [LStmt Var])
genUnsafeCopy tspec = safeCopy (\ _ _ -> True) tspec []

-- Creates a copy of all variables which are in the specified list. This is used when the call to a
-- function is argument safe but it may have problems if a variable is simultaneously argument and
-- result.
genArgSafeCopy 
    :: CaoMonad m 
    => TranslationSpec -> [Var] -> [TLExpr Var] 
    -> m ([TLExpr Var], [LStmt Var])
genArgSafeCopy = safeCopy elem

safeCopy 
    :: CaoMonad m 
    => (Var -> [Var] -> Bool) -> TranslationSpec -> [Var] -> [TLExpr Var] 
    -> m ([TLExpr Var], [LStmt Var])
safeCopy cond tspec lv exps = do
    (e, stmt, vars) <- concatMap3M worker exps
    mapM_ storeTmpVar vars
    return (e, stmt)
    where
    worker :: CaoMonad m => TLExpr Var -> m (TLExpr Var, [LStmt Var], [Var])
    worker ex@(unLoc -> unTyp -> Var v) | cond v lv = do
        let typ = varType v
        n   <- cCall tspec code_assign typ
        (var, decl, vars) <- 
            ifM isDependent workerDepend workerNonDep typ
        return ( genLoc $ annTyE typ $ Var var
               , decl ++ [genLoc $ Assign [LVVar $ genLoc var] [genLoc $ annTyE typ $ FunCall (genLoc n) [ex]]]
               , vars)
    worker e = return (e, [], [])

    workerDepend typ = do
        v <- freshVar Local typ
        return (v, [genLoc $ VDecl $ varDecl v], [])

    workerNonDep typ = do
        var <- freshTmpVar typ
        return (var, [], [var])

    

safetyCopy 
    :: CaoMonad m 
    => TranslationSpec -> [LVal Var] -> [TLExpr Var] 
    -> m ([TLExpr Var], [LStmt Var])
safetyCopy tspec lv ex = safeOrUnsafeDefault tspec
    (return (ex, []))
    (genUnsafeCopy tspec ex)
    (genArgSafeCopy tspec (getVars lv) ex)

safetyCopy' 
    :: CaoMonad m 
    => TranslationSpec -> Type Var -> OpCode -> [Var] -> [TLExpr Var] 
    -> m ([TLExpr Var], [LStmt Var])
safetyCopy' tspec typ fcode lv ex = safeOfUnsafe tspec typ fcode
    (return (ex, []))
    (genUnsafeCopy tspec ex)
    (genArgSafeCopy tspec lv ex)

-------------------------------------------------------------------------------
-- Auxiliary

-- Calls

-- This function was changed to accept a list of expressions since literals can
-- be decomposed is several literal expressions to fit the platform representation
fCallSAux
    :: CaoMonad m 
    => TranslationSpec -> OpCode -> LVal Var -> [TLExpr Var] 
    -> m (Stmt Var)
fCallSAux tspec op lv ex = do
    -- This is the type to choose from the several libraries
    let typ = typeOf $ head ex
    n <- cCall tspec op typ
    return $ Assign [lv] [genLoc $ annTyE typ $ FunCall (genLoc n) ex ] -- TODO: is this type annotation correct?

cCall
    :: CaoMonad m 
    => TranslationSpec -> OpCode -> Type Var 
    -> m Var
cCall tspec op typ = liftM (cFun op typ (callPrefix $ globalTransSpec tspec)) $ typeName tspec typ

cCastCall 
    :: CaoMonad m 
    => TranslationSpec -> Type Var -> Type Var 
    -> m Var
cCastCall tspec typ typD = do
    tname  <- typeName tspec typ
    tnameD <- typeName tspec typD
    return $ cCast typ (callPrefix $ globalTransSpec tspec) tname tnameD

returnByValOrRef 
    :: (CaoMonad m, Typeable a) 
    => TranslationSpec -> [a] 
    -> m ([a], [a])
returnByValOrRef tspec = partitionM byVal
    where
    byVal e = valOrRefFuncReturn tspec (typeOf e) (return True) (return False)

-------------------------------------------------------------------------------
bitsCase :: Type Var -> m a -> m a -> m a
bitsCase typ fb fe = case typ of
    Bits _ _ -> fb
    _        -> fe

getVars :: [LVal Var] -> [Var]
getVars = map aux
    where
    aux (LVVar v) = unLoc v
    aux _ = internalError "getVars" "Not expected case."
-------------------------------------------------------------------------------

getArgExps :: TLExpr Var -> [TLExpr Var]
getArgExps ex = case unTyp $ unLoc ex of
    Lit _ -> [ex]
    StructProj s f -> [s, genLoc $ annTyE (varType f) $ Var f]
    UnaryOp _ e -> [e]
    BinaryOp _ l r ->  [l, r]
    Access e1 (VectP (CElem ei)) -> [e1, ei]
    Access e1 (VectP (CRange ei ej)) -> [e1, ei, ej]
    Access e1 (MatP (CElem ei) (CElem ej)) -> [e1, ei, ej]
    Access e1 (MatP (CRange ei ej) (CRange ek el)) -> [e1, ei, ej, ek, el]
    Access e1 (MatP (CRange ei ej) (CElem cole)) -> [e1, cole, ei, ej]
    Access e1 (MatP (CElem rowe) (CRange ei ej)) -> [e1, rowe, ei, ej]
    _ -> []

-------------------------------------------------------------------------------
moduleName :: String
moduleName = "<Language.CAO.Translation.PreC>"

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

varDecl :: Var -> VarDecl Var
varDecl v = VarD (genLoc v) (type2TyDecl (varType v)) Nothing

rintLit :: Integer -> TLExpr Var
rintLit = genLoc . annTyE RInt . Lit . ILit