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

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

The first phase of the translation mostly handles constant literals according 
to the specification. This introduces additional variables when the 
specification is not 'inlined' or 'mixed'. When 'inlined' is required but it is
not possible to accomplish (variables are used) the translation fails. The 
following cases are considered:

* Constants as operands to CAO operations.

* Constants in function calls and return statements.

* Indices in accesses to vectors, matrices or bit strings.

* Indices in shift, rotate and exponentiation operations.

* When inlining is not possible, the initialization of vectors or matrices is 
expanded to a position by position assignment. This requires the introduction 
of additional indices to access the positions of the container.

Moreover, this phase also performs the following tasks:

* When not using sequence expansion, @seq@ statements are translated to an 
equivalent @while@ loop.

* Creates a global init procedure if one does not already exist.

* Introduces the initialization of additional global constants in the init 
procedure.

-}

module Language.CAO.Transformation.Target (
    targetCaoAST
 ) where

import Control.Applicative ( (<$>) )
import Control.Monad

import Language.CAO.Common.Error
import Language.CAO.Common.Fresh
import Language.CAO.Common.Literal
import Language.CAO.Common.Monad
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.Syntax
import Language.CAO.Syntax.Utils(isAscSeq, isLit, type2TyDecl, typeOf)

import Language.CAO.Translation.Names()

import Language.CAO.Type
import Language.CAO.Type.Utils(innerType)

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

targetCaoAST 
    :: CaoMonad m 
    => TranslationSpec -> Prog Var 
    -> m (Prog Var)
targetCaoAST tspec (Prog defs ip) = withTargetST $ do
    defs' <- concatMapM (targetDefinition tspec) defs
    ip'   <- mapMaybeM (targetFunc tspec) ip
    cs    <- allConsts
    cs'   <- mapM aux cs
    let cdecls = map (genLoc . VarDef . varDecl . fst) cs'
        ip''   = updateInitDecls tspec ip' cs'
    return $ Prog (cdecls ++ defs') (Just ip'')

    where
    aux :: CaoMonad m => (Var, Literal Var) -> m (Var, Literal Var)
    aux (v, l) = do
        v' <- constIndVar tspec v
        return (v', l)

{-
Note 1:
Constants have to come first, before indexes. Why?
[EndConsts]
-}
updateInitDecls 
    :: TranslationSpec -> Maybe (Fun Var) -> [(Var, Literal Var)] 
    -> Fun Var
updateInitDecls tspec ip vars = case ip of
    Just f ->
        f { funBody = gConsts ++ (genLoc $ Nop EndConsts) : (funBody f) }
    Nothing -> let 
            fName = globalInit (initProcName $ globalTransSpec tspec) []
        in Fun (genLoc fName) [] [] $ gConsts ++ 
            genLoc (Nop EndConsts) : 
            genLoc (Nop EndIndex) : 
            genLoc (Nop EndAux) : []
    where
    gConsts = map initGlobalConsts vars
    initGlobalConsts (v, l) = genLoc $ Assign 
        [LVVar (genLoc v)] [genLoc $ annTyE (varType v) $ Lit l]

--------------------------------------------------------------------------------
-- Definition

targetDefinition 
    :: CaoMonad m
    => TranslationSpec -> LDef Var 
    -> m [LDef Var]
targetDefinition tspec (L l d) = liftM (map (L l)) $ targetDef tspec d

targetDef 
    :: CaoMonad m
    => TranslationSpec -> Def Var 
    -> m [Def Var]
targetDef tspec (VarDef vd) = 
    -- In global variable declarations, the 'simplify' stage ensures that the declaration with
    -- initialization of container variables is always removed and replaced with the 
    -- VarD _ Nothing case. Thus, the second return value of 'targetVarDeclarations' can
    -- be safely ignored.
    liftM (map VarDef . fst) $ targetVarDeclaration tspec vd
targetDef tspec (FunDef f) =
    liftM (singleton . FunDef) $ targetFunc tspec f
targetDef _ d@(TyDef _) = 
    return [d]
targetDef tspec (ConstDef cd) = 
    liftM (map ConstDef . fst) $ targetConstDeclaration tspec cd

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

{-
Note 2:
The state of the module stores ...
-}
targetFunc 
    :: CaoMonad m 
    => TranslationSpec -> Fun Var 
    -> m (Fun Var)
targetFunc tspec (Fun (L loc fn) args rtype body) = do
    resetTargetST -- [See Note 2]
    args' <- mapM aux args
    fn'   <- constIndVar tspec fn
    body' <- targetStatements tspec body
    tmpvs <- getTmpVars
    let vars = map (genLoc . VDecl . varDecl) tmpvs
        body'' = vars ++ genLoc (Nop EndConsts) : body'
    return (Fun (L loc fn') args' rtype body'')

    where
    aux (Arg (L l v) t) = do
        v' <- constIndVar tspec v
        return (Arg (L l v') t)
    aux (ArgConst (L l v) t e) = do
        v' <- constIndVar tspec v
        return (ArgConst (L l v') t e)
   
--------------------------------------------------------------------------------
-- Statement

targetStatements 
    :: CaoMonad m 
    => TranslationSpec -> [LStmt Var] 
    -> m [LStmt Var]
targetStatements tspec = 
    concatMapM (uncurry (targetStmt tspec) . split getLoc unLoc)

targetStmt 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> Stmt Var 
    -> m [LStmt Var]
targetStmt tspec l (VDecl vd) = do
    (vd', stmts) <- targetVarDeclaration tspec vd
    return (map (L l . VDecl) vd' ++ stmts)
targetStmt tspec l (CDecl cd) = do
    (cd', stmts) <- targetConstDeclaration tspec cd
    return (map (L l . CDecl) cd' ++ stmts)

targetStmt tspec l (Assign lv' e') =
    case (lv', e') of
        (lv:[], e:[]) -> targetAssignment tspec l lv e
        (_:_:_, e:[]) -> targetTupleAssignment tspec lv' e
        _             -> internalError 
            "targetStmt" "Unexpected case in assignment"

targetStmt tspec l (FCallS fid exps) = do
    (exps', stmts) <- targetExps tspec "<procedure call>" exps
    fid' <- constIndVar tspec fid
    return (stmts ++ L l (FCallS fid' exps') : [])
targetStmt tspec l (Ret exps) = do
    -- Initialy, this was leaving the expressions unchanged. However, this may cause inconsistency
    -- when returning values, with calls to '_init' in platforms which use constants as global
    -- variables.
    (exps', stmts) <- targetExps tspec "<return>" exps
    return (stmts ++ L l (Ret exps') : [])
targetStmt tspec l (Ite i t e) = do
    -- The condition of an 'if' statement is always a variable
    t'      <- targetStatements tspec t
    e'      <- mapMaybeM (targetStatements tspec) e
    return $ L l (Ite i t' e') : []

targetStmt tspec l (While cond wstms) = do
    -- The condition of a 'while' is a variable or the constant 'true'.
    -- This will be treated as a special case because referenced constants can
    -- cause problems in the translation.
    wstms' <- targetStatements tspec wstms
    return $ L l (While cond wstms') : []

-- The sequence statement is transformed in an equivalent while loop.
-- Pre-condition: the bounds and increment values can only be variables or
-- literals
targetStmt tspec l (Seq i@(SeqIter v start end b _) sstms) = do
    let -- c = defaultOperands $ globalTransSpec tspec
        -- The bound variable is only implicitly declared in the sequence
        -- Now, we have to declare it explicitly.
        vd     = genLoc $ VDecl $ varDecl v 
        -- Initialization with starting value
        init_v = genLoc $ Assign (LVVar (genLoc v) : []) (annL RInt start : [])
        -- Condition: sequence iteration always uses register integers.
        -- TODO: what about constants??? They must be processed by target
        cond   = genLoc $ annTyE Bool $ BinaryOp (CmpOp RInt cmpOp) 
                    (genLoc $ annTyE RInt (Var v)) 
                    (annL RInt end) 
        cmpOp  = if isAscSeq i then Leq else Geq
        -- Increment value
        b'     = maybe (rintLit 1) (annL RInt) b
        -- Incrementing the bound variable. The operations are always
        -- on register integers.
        step   = genLoc $ Assign 
                    [LVVar $ genLoc v] 
                    [genLoc $ annTyE RInt $ BinaryOp (ArithOp Plus) 
                        (genLoc $ annTyE RInt $ Var v) 
                        b']
    sstms' <- targetStatements tspec sstms
    -- NEW seq translation
    cond_v <- freshTmpVar Bool
    storeTmpVar cond_v
    -- Condition
    let condStmt = genLoc $ Assign [LVVar $ genLoc cond_v] [cond]
    return $ vd 
           : init_v 
           : condStmt 
           : L l (While (genLoc $ annTyE Bool $ Var cond_v) 
                    (sstms' ++ step : condStmt : [])) 
           : []

targetStmt _ l (Nop a) = return [L l $ Nop a]
    
    
--------------------------------------------------------------------------------
{-
Note:

The first idea was to use the kind of operand of '_init' (fInitCall)
However, this is not correct because '_init' must ALWAYS get a literal
constant. Therefore, the correct way is to use the default value of the
platform. If this is 'inline', the literal constants are left and
the assignment will be replaced by an '_init' in the following steps.
If this is 'vars_*' instead, the constant is replaced by a variable
and an '_assign' operation is introduced in the following steps.

-}
-- Precondition: |lv| = 1  |e| = 1
targetAssignment 
    :: CaoMonad m 
    => TranslationSpec -> SrcLoc -> LVal Var -> TLExpr Var 
    -> m [LStmt Var]

-- [See Note ?]
targetAssignment tspec l lv@(LVVar _) le@(unLoc -> unTyp -> Lit _) = do
    (lv', _) <- targetLValue tspec lv
    (e', stmts) <- targetExpChoiceGeneral tspec "<constant assign>" le
    return (stmts ++ [L l $  Assign [lv'] [e']])
targetAssignment tspec l lv@(LVVar _) e = do
    (lv', _) <- targetLValue tspec lv
    (e', stmts) <- targetExp tspec e
    return (stmts ++ [L l $  Assign [lv'] [e']])
targetAssignment tspec l lv le@(unLoc -> TyE _ (Lit _)) = do
    -- Unlike the previous case of assignment of a literal constant, here
    -- the operation will be always an assignment. Moreover, we have to
    -- distinguish the left value case and the assignment case.
    (lv', stmts1) <- targetLValue tspec lv
    (e',stmts2)   <- targetExpChoice tspec code_assign le
    return (stmts1 ++ stmts2 ++ [L l $ Assign [lv'] [e']])
targetAssignment tspec l lv (L loc (TyE _ (Var v))) = do
    (lv', stmts) <- targetLValue tspec lv
    v' <- constIndTVar tspec v
    return (stmts ++ [L l $ Assign [lv'] [L loc v']])
targetAssignment _ _ _ _ = 
    internalError "targetAssignment" "not expected case"

-- Precondition: |lvs| > 1 |e| = 1
-- Precondition: it is assumed that 'lvs' only contains variables
targetTupleAssignment 
    :: CaoMonad m 
    => TranslationSpec -> [LVal Var] -> TLExpr Var 
    -> m [LStmt Var]
targetTupleAssignment tspec lvs e = do
    (e', stmts) <- targetExp tspec e
    -- Assuming that we have only 'LVVar' in the list
    lvs' <- mapM (liftM fst . targetLValue tspec) lvs
    return $ stmts ++ [genLoc $ Assign lvs' [e']]

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

targetLValue 
    :: CaoMonad m 
    => TranslationSpec -> LVal Var 
    -> m (LVal Var, [LStmt Var])
targetLValue tspec (LVVar (L l v)) = do
    v' <- constIndVar tspec v
    return (LVVar (L l v'), [])
targetLValue tspec (LVStruct lv fld) = do
    (lv', stmts) <- targetLValue tspec lv
    return (LVStruct lv' fld, stmts)
targetLValue tspec (LVCont ty lv p) = do
    ty' <- constIndType tspec ty
    (lv', stmts1)  <- targetLValue tspec lv
    return (LVCont ty' lv' p, stmts1)

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

targetConstDeclaration 
    :: CaoMonad m
    => TranslationSpec -> ConstDecl Var 
    -> m ([ConstDecl Var], [LStmt Var])
targetConstDeclaration tspec (ConstD (L l c) d e) = do
    (e'', stmts) <- case e of
        ConstInit e' -> liftM (mapFst (ConstInit . unTypL)) $ 
            targetExp tspec (annL (typeOf c) e')
        _            -> return (e, [])
    return ([ConstD (L l c) d e''], stmts)
targetConstDeclaration _ _ = internalError 
    "<targetConstDeclaration" "Not expected multiple constant declarations"


targetVarDeclaration 
    :: CaoMonad m
    => TranslationSpec -> VarDecl Var 
    -> m ( [VarDecl Var]
         , [LStmt Var])
targetVarDeclaration tspec (VarD (L l v) d Nothing) = do
    t <- constIndType tspec $ varType v
    return ([VarD (L l (setType t v)) d Nothing], [])
targetVarDeclaration tspec c@(ContD (L l v) d ex) = do
    ci <- operandKind tspec (varType v) code_init -- TODO: Verify this!! Before this was indexKind
    t' <- constIndType tspec (varType v)
    let v' = setType t' v
    case ci of
        GlobalV -> do
            ini <- zipWithSeqM auxGlobal ex
            return ([VarD (L l v') d Nothing], ini)
        LocalV  -> do
            ini <- zipWithSeqM auxLocal ex
            return ([VarD (L l v') d Nothing], ini)
        Inlined -> if all (isLit . unTyp . unLoc) ex
            then return ([], [genLoc $ VDecl c])
            else caoError l $ NotSupportedVar (operName code_init) (varType v)
        Mixed   -> return ([], [genLoc $ VDecl c]) -- This maintains the order since there may be dependencies

        where

        -- TODO: Replace these types
        auxGlobal n e@(unLoc -> unTyp -> Lit _) = do
            ind <- arrayIndex (L l v) n
            e' <- introGlobalLitVar tspec e
            return $ genLoc $ Assign [ind] [e']
        auxGlobal n e@(unLoc -> unTyp -> Var _) = do
            ind <- arrayIndex (L l v) n
            return $ genLoc $ Assign [ind] [e]
        auxGlobal _ _ = internalError
            "targetVarDeclaration" "Not expected case"

        -- This does not really require the introduction of additional variables.
        -- The assignment will always result in the use a call to an _init function
        -- during the translation
        auxLocal n e = do
            ind <- arrayIndex (L l v) n
            return $ genLoc $ Assign [ind] [e]
    

targetVarDeclaration _ _ = internalError 
    "targetVarDeclaration" "Not expected case"

arrayIndex 
    :: CaoMonad m 
    => Located Var -> Integer 
    -> m (LVal Var)
arrayIndex v n = case typ of
    Vector _ _ -> do
        let e = rintLit n
        return $ LVCont (head $ innerType typ) (LVVar v) $ VectP $ CElem e
    Matrix _ (IInt m) _ -> do
        let (i, j) = divMod n m
            ei = rintLit i
            ej = rintLit j
        return $ LVCont (head $ innerType typ) (LVVar v) $ MatP (CElem ei) (CElem ej)
    Matrix _ _ _ -> internalError "arrayIndex" "<<TODO>>: not literal"
    _ -> internalError
        "arrayIndex" "Unexpected container type"
    where
    typ = varType (unLoc v)

--------------------------------------------------------------------------------
-- Expression

targetExps 
    :: CaoMonad m 
    => TranslationSpec -> String
    -> [TLExpr Var] -> m ( [TLExpr Var]
                         , [LStmt Var]
                         )
targetExps tspec nm = concatMap2M (targetExpChoiceGeneral tspec nm)

targetExp 
    :: CaoMonad m 
    => TranslationSpec -> TLExpr Var 
    -> m (TLExpr Var, [LStmt Var])
targetExp tspec (L l e) = do
    (e', as) <- tagExp tspec e
    return (L l e', as)

tagExp 
    :: CaoMonad m 
    => TranslationSpec -> TExpr Var 
    -> m (TExpr Var, [LStmt Var])
tagExp tspec (TyE typ l@(Lit _)) = do
    typ' <- constIndType tspec typ
    return (annTyE typ' l, [])
tagExp tspec (TyE _ (Var   v)) = do
    v' <- constIndTVar tspec v
    return (v', [])
tagExp tspec (TyE _ (FunCall (L l f) es)) = do
    f' <- constIndVar tspec f
    (es', stmts) <- targetExps tspec "<function call>" es
    return (annTyE (typeOf f') $ FunCall (L l f') es', stmts)
tagExp tspec (TyE t e@(StructProj ea n)) = do
    (ea', stmts) <- targetExpChoice tspec (codeOf e) ea
    return (TyE t $ StructProj ea' n, stmts) -- TODO: need to process t
-- TODO: replace codeOf with a more specific function
tagExp tspec (TyE t eu@(UnaryOp op e)) = do
    (e', ss) <- targetExpChoice tspec (codeOf eu) e
    return (TyE t $ UnaryOp op e', ss)
tagExp tspec (TyE t e@(BinaryOp (BitsSROp op) l r)) = do
    (l', ss)  <- targetExpChoice tspec (codeOf e) l
    return (TyE t $ BinaryOp (BitsSROp op) l' r, ss)
tagExp tspec (TyE t e@(BinaryOp op l r)) = do
    ((l', r'), ss) <- targetBinaryExp tspec (codeOf e) l r
    return (TyE t (BinaryOp op l' r'), ss)
tagExp tspec (TyE ty ae@(Access e p)) = do
    (e', ss1) <- targetExpChoice tspec (codeOf ae) e
    ty' <- constIndType tspec ty
    return (annTyE ty' (Access e' p), ss1)
tagExp tspec (TyE ty (Cast b td (L l (unTyp -> (Var v))))) = do
    -- The first version used the kind of operand of operation 'fCastName'.
    -- However, this operation must always receive a variable, since all
    -- literal constants casts were already evaluated statically. Using
    -- the kind of operand causes problems if the user specifies 'inlined'
    -- which will cause the compilation to fail because a constant was
    -- expected
    ty' <- constIndType tspec ty
    tv  <- constIndTVar tspec v
    return (annTyE ty' $ Cast b td (L l tv), [])
tagExp _ _  = internalError "tagExp" "Not expected expression"


targetBinaryExp 
    :: CaoMonad m 
    => TranslationSpec -> OpCode -> TLExpr Var -> TLExpr Var
    -> m ((TLExpr Var, TLExpr Var), [LStmt Var])
targetBinaryExp tspec op l r = do
    c <- operandKind tspec (typeOf l) op
    let opn = operName op
    (l', stmts1) <- targetExpChoice' tspec c opn l
    (r', stmts2) <- targetExpChoice' tspec c opn r
    return ((l', r'), stmts1 ++ stmts2)

--------------------------------------------------------------------------------
-- Exp choice

{-
Note:
It is here that happens all the magic!
-}

targetExpChoiceGeneral
    :: CaoMonad m
    => TranslationSpec -> OpName -> TLExpr Var 
    -> m (TLExpr Var, [LStmt Var])
targetExpChoiceGeneral tspec op e = do
    c <- operandKindGeneral tspec (typeOf e)
    targetExpChoice' tspec c op e

targetExpChoice
    :: CaoMonad m
    => TranslationSpec -> OpCode -> TLExpr Var 
    -> m (TLExpr Var, [LStmt Var])
targetExpChoice tspec op e = do
    c <- operandKind tspec (typeOf e) op
    targetExpChoice' tspec c (operName op) e

targetExpChoice'
    :: CaoMonad m
    => TranslationSpec -> Consts -> OpName -> TLExpr Var 
    -> m (TLExpr Var, [LStmt Var])
targetExpChoice' tspec c _ e@(L loc (TyE t l@(Lit _))) = case c of
    GlobalV -> liftM (split id (const [])) $ introGlobalLitVar tspec e
    LocalV  -> introLocalLitVar tspec e
    _ -> do
        t' <- constIndType tspec t
        return (L loc (annTyE t' l), [])
targetExpChoice' tspec c op (L l (unTyp -> (Var v))) = case c of
    Inlined -> caoError l $ NotSupportedVar op $ varType v
    _       -> do
        v' <- constIndTVar tspec v
        return (L l v', [])
targetExpChoice' _ _ _ _ = internalError
    "targetExpChoice'" "Not expected case"

{-
Gets a literal and returns:
* A new variable with the same type
* The declarations of the variable
* The assignment of the literal to the new variable (definition)
-}
introLocalLitVar 
    :: CaoMonad m 
    => TranslationSpec -> TLExpr Var 
    -> m (TLExpr Var, [LStmt Var])
introLocalLitVar tspec (L loc (TyE typ l@(Lit _))) = do
    typ' <- constIndType tspec typ
    tv   <- freshVar Local typ' -- TODO: consider using tmpvar
    let decl   = genLoc $ VDecl $ varDecl tv
        assign = genLoc $ Assign [LVVar (genLoc tv)] [L loc (annTyE typ' l)]
    return (genLoc $ annTyE typ' $ Var tv, decl : assign : [])
introLocalLitVar _ _ = internalError 
    "introLocalLitVar" "Getting something that is not a literal"

{-
The function returns a variable which denotes the constant value.
HOW??? getConst?
-}
introGlobalLitVar 
    :: CaoMonad m 
    => TranslationSpec -> TLExpr Var 
    -> m (TLExpr Var)
introGlobalLitVar tspec (L loc (TyE t (Lit l))) = do
    v  <- getConst t l
    t' <- constIndType tspec t
    return (L loc $ annTyE t' $ Var (setType t' v))
introGlobalLitVar _ _ = internalError "introGlobalLitVar" "not expected case"


--------------------------------------------------------------------------------
-- Constanst in type declarations

constIndVar :: CaoMonad m => TranslationSpec -> Var -> m Var
constIndVar tspec v = do
    t <- constIndType tspec $ varType v
    return (setType t v)

constIndTVar :: CaoMonad m => TranslationSpec -> Var -> m (TExpr Var)
constIndTVar tspec v = do
    t <- constIndType tspec $ varType v
    return $ annTyE t $ Var (setType t v)

-- TODO: what if an inner type requires it?
constIndType 
    :: CaoMonad m 
    => TranslationSpec -> Type Var 
    -> m (Type Var)
constIndType _ Bullet = return Bullet
constIndType tspec (Tuple tlst) = do
    t <- mapM (constIndType tspec) tlst
    return (Tuple t)
constIndType tspec (FuncSig ta tr c) = do
    ta' <- mapM (constIndType tspec) ta
    tr' <- constIndType tspec tr
    return (FuncSig ta' tr' c)
constIndType tspec typ = constIndType' tspec GlobalV typ {-do
    c <- operandKind tspec typ fDeclCall
    case c of
        GlobalV -> constIndType' c typ
        LocalV -> error "<targetIndChoice>: Not supported local vars"
        _ -> return typ-}

constIndType' :: CaoMonad m => TranslationSpec -> Consts -> Type Var -> m (Type Var)
constIndType' tspec c typ = case typ of
    Vector n t -> do
         t' <- indType tspec c t
         return (Vector n t')
    Matrix n m t -> do
         t' <- indType tspec c t
         return (Matrix n m t')
    Struct s tlst -> do
        fldtys' <- mapM (\(v,sf) -> (v,) <$> indType tspec c sf) tlst
        let tct = Struct newvar tlst'
            newvar = setType tct s
            tlst'  = map (\(v, ty) -> (setType (SField newvar ty) v, ty)) fldtys'
        return tct
    Mod Nothing Nothing (Pol [Mon (CoefI _) EZero]) -> indType tspec c typ
    Mod (Just (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero]))) (Just _) p@(Pol _) -> polDegree p >> indType tspec c typ
    TySyn v t -> do
        t' <- indType tspec c t
        let tct = TySyn newvar t'
            newvar = setType tct v
        return tct
    _ -> return typ

polDegree :: CaoMonad m => Pol id -> m ()
polDegree (Pol ((Mon _ (MExpI _ e)):_)) = getConst Int (ILit e) >> return ()
polDegree _ = internalError "polDegree" "Not expected case"

indType 
    :: CaoMonad m 
    => TranslationSpec -> Consts -> Type Var 
    -> m (Type Var)
indType _ _ Bullet = return Bullet
indType _ _ Int = return Int
indType _ _ RInt = return RInt
indType _ _ Bool = return Bool
indType _ c (Bits s sz) = do
    sz' <- targetIndChoice c sz
    return (Bits s sz')
indType tspec _ m'@(Mod Nothing Nothing (Pol [Mon (CoefI m) EZero])) = case m of
    IInt n -> do
        if existsModWithBase tspec n then return m' else do
            v <- getConst Int (ILit n)
            return (Mod Nothing Nothing (Pol [Mon (CoefI (IInd v)) EZero]))
    _ -> return m'
indType tspec c (Mod (Just im@(Mod Nothing Nothing (Pol [Mon (CoefI _) EZero]))) (Just i) p@(Pol pol)) = do
        polDegree p
        im' <- indType tspec c im
        pol' <- mapM aux pol
        return (Mod (Just im') (Just i) (Pol pol'))
    where
    aux m@(Mon co e) = case co of
        CoefI (IInt n) -> do
            v <- getConst Int (ILit n)
            return (Mon (CoefI (IInd v)) e)
        CoefI _ -> return m
        CoefP _ -> error "<constIndType'>: Polynomial extension"
indType _ _ (Mod _ _ _) = error "<indType><<TODO>>: Mod"
indType tspec c (Vector n t) = do
    n' <- targetIndChoice c n
    t' <- indType tspec c t
    return (Vector n' t')
indType tspec c (Matrix n m t) = do
    n' <- targetIndChoice c n
    m' <- targetIndChoice c m
    t' <- indType tspec c t
    return (Matrix n' m' t')
indType _ _ (SField _ _) = error "<<TODO>><indType>: SField"
indType tspec c (TySyn v t) = do
    t' <- indType tspec c t
    let tct = TySyn newvar t'
        newvar = setType tct v
    return tct
indType tspec c (Struct s flds) = do
    fldtys' <- zip (map fst flds) <$> mapM indFld flds
    let tct     = Struct newvar flds'
        newvar  = setType tct s
        flds'   = map (\(v, ty) -> (setType (SField newvar ty) v, ty)) fldtys'
    return tct
  where indFld (_, sf) = indType tspec c sf
indType tspec c (Tuple l) = liftM Tuple $ mapM (indType tspec c) l
indType _ _ _ = error "<indType><<TODO>>: other type"

{-
Precondition: It expected that simplification has left only constants and
index variables in index expressions.
-}
targetIndChoice 
    :: CaoMonad m 
    => Consts -> IExpr Var 
    -> m (IExpr Var)
targetIndChoice c e@(IInt n) = case c of
    GlobalV -> do
        v <- getConst RInt (ILit n)
        return (IInd v)
    LocalV -> internalError "targetIndChoice" "Not supported local vars"
    Inlined -> return e
    Mixed   -> return e
targetIndChoice c e@(IInd _) = case c of
    Inlined -> caoError defSrcLoc $ mkUnknownErr $
        "<Language.CAO.Transformation.Target>.\
            \<targetIndChoice>: not expected case"
    _ -> return e
targetIndChoice _ _ = internalError
    "targetIndChoice" "not expected composed expression"

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

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

moduleName :: String
moduleName = "<Language.CAO.Transformation.Target>"

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

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