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

{- |
Module      :  $Header$
Description :  Expression evaluation.
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

Frequently, source code may contain expressions using constant literals that 
are not in their most evaluated format. For example, in cryptographic 
implementations one often uses container sizes that are the explicit product 
of two constants, to improve the clarity of the code. The expansion phase also 
introduces literals in expressions by replacing the sequence indices by their 
corresponding values. All these expression using literals are amenable to be 
partially evaluated during compilation, thus resulting in simpler and more 
efficient final code.

In this phase, several reductions are performed on expressions containing 
literals accordingly with the rules defined in the operational semantics. In 
many cases, these are quite identical to those defined in the language 
interpreter. The main difference is that the interpreter needs all the values 
fully defined while the evaluator can handle a mixture of defined and undefined 
(variables) values. The evaluation does not give guarantees of completeness: 
there may be some expressions that could be more reduced using more 
sophisticated approaches. However all the reductions have been designed to be 
safe and preserve the semantics of the program.

The following reductions on expressions are performed during this phase:

* Whenever possible, arithmetic expressions on literals are computed. This 
resorts to some extent to commutativity, associativity and distributivity of 
certain operators.

* Whenever possible, boolean expressions on literals are computed.

* Casts of literals are evaluated by converting their value to the target type,
accordingly with the semantics.

* Every nested range access is replaced by an equivalent non-nested range 
access. This evaluation is always safe since the type checker already validated 
the dimensions of the resulting ranges.
For vectors, the following rules are used, where @v@ is a vector and @l@, 
@h@ and @n@ are integer literals:

@
v[l..h][n]        → v[l + n] 
v[l1..h1][l2..h2] → v[l1 + l2..l1 + h2]
@

For matrices, the rules are analogous using a second dimension.


After the evaluation of expressions, when the condition of a conditional or 
iterative statement is a literal, the decision can be statically performed 
without changing the meaning of the original program. Therefore, some 
statements are also reduced:

* The corresponding branch of an if statement is chosen if its condition is 
a literal.

* A while statement is removed if its condition is the false literal.
-}

module Language.CAO.Transformation.Eval ( evalExpr) where

import Language.CAO.Common.Literal
import Language.CAO.Common.SrcLoc
import Language.CAO.Common.Utils
import Language.CAO.Common.Var ( Var )
import Language.CAO.Common.Outputable

import Language.CAO.Semantics.Bool
import Language.CAO.Semantics.Casts
import Language.CAO.Semantics.Integer

import Language.CAO.Syntax
import Language.CAO.Syntax.Utils (isIntLit, isRange, typeOf)

import Language.CAO.Type

-- Consider the fusion with function checkIntExp of CaoTypeChecker
-- A more elaborated version could perform more distributivity laws
-- Can this step be fused with the remaining simplification?
evalExpr :: Prog Var -> Prog Var
evalExpr (Prog defs _) = Prog (map (fmap evalDef) defs) Nothing

evalDef :: Def Var -> Def Var
evalDef (VarDef   vd) = VarDef   $ evalVD  vd
evalDef (FunDef   fd) = FunDef   $ evalFD  fd
evalDef (TyDef    td) = TyDef    $ evalTDF td
evalDef (ConstDef cd) = ConstDef $ evalCD  cd

evalVD :: VarDecl Var -> VarDecl Var
evalVD (VarD n td (Just e)) = VarD n td (Just $ evalLE e)
evalVD (ContD ln td es)     = ContD ln td $ map evalLE es
evalVD vd                   = vd

-- Casts are not allowed inside constant initialization, and the type
-- annotation is never needed. Thus, it is safe to be undefined
evalCD :: ConstDecl Var -> ConstDecl Var
evalCD (ConstD c td (ConstInit e)) = ConstD c td (ConstInit (evalL undefined e))
evalCD cd                          = cd

evalFD :: Fun Var -> Fun Var 
evalFD (Fun n args rt stmts)
    = Fun n (map aux args) 
            (map evalTD rt)
            (concatMap evalLStmt stmts)

    where
    aux (Arg a td)        = Arg a (evalTD td)
    aux (ArgConst a td e) = ArgConst a (evalTD td) e

evalTDF :: TyDef Var -> TyDef Var 
evalTDF (TySynDef   n td)   = TySynDef   n $ evalTD td
evalTDF (StructDecl n flds) = StructDecl n $ map (mapSnd evalTD) flds

evalLTD :: LTyDecl Var -> LTyDecl Var
evalLTD = fmap evalTD

evalTD :: TyDecl Var -> TyDecl Var
evalTD (BitsD s e)          = BitsD s (evalL RInt e)
evalTD (ModD m)             = ModD  $ evalMod m
evalTD (VectorD e td)       = VectorD (evalL RInt e) (evalTD td)
evalTD (MatrixD e1 e2 td)   = MatrixD (evalL RInt e1) (evalL RInt e2) (evalTD td)
evalTD td                   = td

evalMod :: Mod Var -> Mod Var
evalMod (ModNum e)          = ModNum $ evalL Int e
evalMod (ModPol td n p)     = ModPol (evalTD td) n p

evalStmt :: Stmt Var -> [Stmt Var]
evalStmt (CDecl cd)         = [CDecl $ evalCD cd]
evalStmt (VDecl vd)         = [VDecl $ evalVD vd]
evalStmt (Assign lvs es)    = [Assign (map evalLV lvs) (map evalLE es)]
evalStmt (FCallS n es)      = [FCallS n $ map evalLE es]
evalStmt (Ret es)           = [Ret $ map evalLE es]
evalStmt (Ite i t me)       = let
        i'  = evalLE i
        t'  = concatMap evalLStmt t
        me' = fmap (concatMap evalLStmt) me
    in case unTyp $ unLoc i' of
        Lit (BLit True)  -> map unLoc t'
        Lit (BLit False) -> maybe [] (map unLoc) me'
        _                -> [Ite i' t' me']
evalStmt (Seq (SeqIter v s e b r) ss)
  = [Seq (SeqIter v (evalL RInt s)
                    (evalL RInt e)
                    (fmap (evalL RInt) b)
                    r) $ concatMap evalLStmt ss]
evalStmt (While e ss)       = let 
        e' = evalLE e
    in case unTyp $ unLoc e' of
        Lit (BLit False) -> []
        _ -> [While e' (concatMap evalLStmt ss)]
evalStmt s@(Nop _)          = [s]

evalLStmt :: LStmt Var -> [LStmt Var]
evalLStmt (L l s)           = map (L l) $ evalStmt s

evalL :: Type Var -> LExpr Var -> LExpr Var
evalL t = fmap evalE . annL t

evalLE :: TLExpr Var -> TLExpr Var
evalLE (L loc e@(TyE tyann _)) = L loc $ TyE tyann $ evalE e

-- Type annotations are necessary to eval casts
evalE :: TExpr Var -> Expr Var
evalE (TyE _ v@(Var _))                  = v
evalE (TyE _ l@(Lit _))                  = l
evalE (TyE _ (FunCall n es))             = FunCall n      $ map evalLE es
evalE (TyE _ (StructProj e f))           = StructProj (evalLE e) f
evalE (TyE _ (UnaryOp Sym e))            = reduceIntExpr  $ UnaryOp Sym $ evalLE e
evalE (TyE _ (UnaryOp Not e))            = reduceBoolExpr $ UnaryOp Not $ evalLE e
evalE (TyE _ (UnaryOp BNot bs))          = UnaryOp BNot   $ evalLE bs
evalE (TyE _ (BinaryOp (ArithOp o) l r)) = reduceIntExpr  $ 
    BinaryOp (ArithOp o) (evalLE l) (evalLE r)
evalE (TyE _ (BinaryOp (BoolOp o) l r))  = reduceBoolExpr $ 
    BinaryOp (BoolOp o) (evalLE l) (evalLE r)
evalE (TyE _ (BinaryOp op e1 e2))        = BinaryOp op (evalLE e1) (evalLE e2)
evalE (TyE _ (Access e p))               = reduceRanges   $ Access (evalLE e) (evalP p)
evalE (TyE t (Cast b td e))              = 
    case evalLE e of
        -- Needed to evaluate nested casts of literals
        L _ l@(TyE _ (Lit _)) -> convertTo t l
        e'                    -> Cast b (map evalLTD td) e'

evalP :: APat Var -> APat Var
evalP (VectP p)  = VectP $ evalAP p
evalP (MatP l r) = MatP (evalAP l) (evalAP r)

evalAP :: RowAPat Var -> RowAPat Var
evalAP (CElem e)    = CElem $ evalLE e
evalAP (CRange l r) = CRange (evalLE l) (evalLE r)

evalLV :: LVal Var -> LVal Var
evalLV (LVStruct lv fi) = LVStruct (evalLV lv) fi
evalLV (LVCont ty lv p)
    = case reduceLRanges (LVCont ty (evalLV lv) (evalP p)) of
        LVCont ty' lv' p' -> LVCont ty' (evalLV lv') (evalP p')
        _  -> error "<Language.CAO.Transformation.Eval>.\
                       \<evalLV>: Unexpected error in 'reduceLRanges'"
evalLV v@(LVVar _) = v

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

getTLInt :: TLExpr Var -> Either (Integer, SrcLoc, Type Var) (TLExpr Var)
getTLInt (L l (TyE t (Lit (ILit i))))   = Left  (i, l, t)
getTLInt e                              = Right e

getTInt :: TLExpr Var -> Either (Integer, Type Var) (TLExpr Var)
getTInt (unLoc -> TyE t (Lit (ILit i))) = Left  (i, t)
getTInt e                               = Right e

reduceAssoc :: AOp -> (Integer -> Integer) -> TLExpr Var -> TLExpr Var -> Expr Var
reduceAssoc op i (getTInt -> Left (j, _))    (getTInt -> Left (k, _))
    = Lit $ ILit $ i $ fInt op j k
reduceAssoc op i (getTLInt -> Left (j,l, t)) (getTInt -> Right k)
    = BinaryOp (ArithOp op) (L l $ annTyE t $ Lit $ ILit $ i j) k
reduceAssoc op i (getTInt -> Right j)        (getTLInt -> Left (k,l,t))
    = BinaryOp (ArithOp op)  j (L l $ annTyE t $ Lit $ ILit $ i k)
reduceAssoc _ _ _ _
    = error "<Language.CAO.Transformation.Eval>.<reduceAssoc>: Unexpected case"

reduceTimesPlus :: Integer -> TLExpr Var -> TLExpr Var -> Expr Var
reduceTimesPlus i (getTInt -> Left (j, _))    (getTInt -> Left (k, _)) = 
    Lit $ ILit $ i * (j + k)
reduceTimesPlus i (getTLInt -> Left (j, l, t)) (getTInt -> Right k) = 
    BinaryOp (ArithOp Plus) 
        (L l $ annTyE t $ Lit $ ILit $ j `integerTimes` i) 
        (L (getLoc k) $ annTyE t $ 
            BinaryOp (ArithOp Times) (genLoc $ annTyE t $ Lit $ ILit i) k)
reduceTimesPlus i (getTInt -> Right j)       (getTLInt -> Left (k, l, t)) = 
    BinaryOp (ArithOp Plus) 
        (L (getLoc j) $ annTyE t $ 
            BinaryOp (ArithOp Times) (genLoc $ annTyE t $ Lit $ ILit i) j)
        (L l $ annTyE t $ Lit $ ILit $ k `integerTimes` i)
reduceTimesPlus i (getTInt -> Right j)       (getTInt -> Right k) = 
    BinaryOp (ArithOp Plus) 
        (L (getLoc j) $ annTyE tj $ BinaryOp (ArithOp Times) ei j)
        (L (getLoc k) $ annTyE (typeOf k) $ BinaryOp (ArithOp Times) ei k)
    where 
    tj = typeOf j
    ei = genLoc $ annTyE tj $ Lit $ ILit i
reduceTimesPlus e1 e2 e3 = 
    error $ "<Language.CAO.Transformation.Eval>.<reduceTimesPlus>:\
      \ Unexpected case: (" ++ showPpr e1 ++ ") * ((" ++ showPpr e2
                        ++ ") + (" ++ showPpr e3 ++ "))"


reduceIntExpr :: Expr Var -> Expr Var
-- Simple exprs
reduceIntExpr (BinaryOp (ArithOp (fInt   -> op))
                          (getTInt -> Left (b1, _))
                          (getTInt -> Left (b2, _)))
    = Lit $ ILit $ b1 `op` b2
reduceIntExpr (UnaryOp Sym (getTInt -> Left (b1, _)))
    = Lit $ ILit $ negate b1

-- Distributivity of '*'
reduceIntExpr (BinaryOp (ArithOp Times)
                          (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Plus) e1 e2))
                          (getTInt -> Left (e3, _)))
    = reduceTimesPlus e3 e1 e2
reduceIntExpr (BinaryOp (ArithOp Times)
                          (getTInt -> Left (e3, _))
                          (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Plus) e1 e2)))
    = reduceTimesPlus e3 e1 e2

-- Associativity
reduceIntExpr (BinaryOp (ArithOp oop)
                          (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp iop) e1 e2))
                          (getTInt -> Left (e3, _)))
    | isAssoc oop && oop == iop && (isIntLit (unTyp (unLoc e1)) || isIntLit (unTyp (unLoc e2)))
        = reduceAssoc oop (flip (fInt oop) e3) e1 e2
reduceIntExpr (BinaryOp (ArithOp oop)
                          (getTInt -> Left (e3, _))
                          (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp iop) e1 e2)))
    | isAssoc oop && oop == iop && (isIntLit (unTyp (unLoc e1)) || isIntLit (unTyp (unLoc e2)))
        = reduceAssoc oop (fInt oop e3) e1 e2
-- Minus Case
--
-- <FIXME reduceAssoc>
-- reduceAssoc takes advantage also from commutativity, so
-- isAssoc now is True only for associative and commutative ops)
reduceIntExpr
    (BinaryOp (ArithOp Minus)
              (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
                                                    (getTInt -> Left (e1, _))
                                                    (getTInt -> Left (e2, _))))
              (getTInt -> Left (e3, _)))
    = Lit $ ILit (e1 - e2 - e3)
reduceIntExpr
    (BinaryOp (ArithOp Minus)
              (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
                                                    (getTInt -> Right e1)
                                                    (getTLInt -> Left (e2, l, _))))
              (getTInt -> Left (e3, t)))
    = BinaryOp (ArithOp Minus) e1 (L l $ annTyE t $ Lit $ ILit (e2 - e3))
reduceIntExpr
    (BinaryOp (ArithOp Minus)
              (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
                                                    (getTLInt -> Left (e1, l, _))
                                                    (getTInt -> Right e2)))
              (getTInt -> Left (e3, t)))
    = BinaryOp (ArithOp Minus) (L l $ annTyE t $ Lit $ ILit (e1 - e3)) e2 
reduceIntExpr
    (BinaryOp (ArithOp Minus)
              (getTInt -> Left (e3, t))
              (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
                                                    (getTInt -> Right e1)
                                                    (getTLInt -> Left (e2, l, _)))))
    = BinaryOp (ArithOp Minus) (L l $ annTyE t $ Lit $ ILit (e2 + e3)) e1
reduceIntExpr
    (BinaryOp (ArithOp Minus)
              (getTInt -> Left (e3, t))
              (getTInt -> Right (unLoc -> unTyp -> BinaryOp (ArithOp Minus)
                                                    (getTLInt -> Left (e1, l, _))
                                                    (getTInt -> Right e2))))
    = BinaryOp (ArithOp Plus) (L l $ annTyE t $ Lit $ ILit (e3 - e1)) e2
-- </FIXME reduceAssoc>
reduceIntExpr e
    = e


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

getBool :: TLExpr Var -> Maybe Bool
getBool (unLoc -> unTyp -> Lit (BLit b)) = Just b
getBool _                         = Nothing

reduceBoolExpr :: Expr Var -> Expr Var
reduceBoolExpr (BinaryOp (BoolOp (fBool   -> op))
                          (getBool -> Just b1)
                          (getBool -> Just b2))
    = Lit $ BLit $ b1 `op` b2
reduceBoolExpr (UnaryOp Not (getBool -> Just b1))
    = Lit $ BLit $ boolNot b1
reduceBoolExpr e
    = e

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

reduceRanges :: Expr Var -> Expr Var
reduceRanges (Access (unLoc -> (TyE _ (Access e1 p1))) p2) | isRange p1
    = Access e1 $ reducePats p1 p2
reduceRanges e
    = e

-- | Reduce nested ranges in LValues
--
-- Examples: 
-- m[1..5,2..3][3,1] ----->
--  m' =  m[1..5,2..3] : matrix[5,2] of a'
--  m'[3,1] : a'
--  =====> reduces to m[4,3]
--
-- m[1..5,2..3][3 .. 4,1] ----->
--  m' =  m[1..5,2..3] : matrix[5,2] of a'
--  m'[3 .. 4 ,1] : matrix [2, 1] of a'
--  reduces to m[4 .. 5, 3]
--
reduceLRanges :: LVal Var -> LVal Var
reduceLRanges (LVCont ty (LVCont _ lv' p1) p2) | isRange p1
    = LVCont ty lv' (reducePats p1 p2)
reduceLRanges lv
    = lv

reducePats :: APat Var -> APat Var -> APat Var
reducePats (VectP r1) (VectP r2)
    = VectP $ reduceRngs r1 r2
reducePats (MatP r11 r12) (MatP r21 r22)
    = MatP (reduceRngs r11 r21) (reduceRngs r12 r22)
reducePats _ _
    = error $ "<Language.CAO.Transformation.Eval>.\
              \<reducePats>: Unexpected case."

reduceRngs :: RowAPat Var -> RowAPat Var -> RowAPat Var
reduceRngs (CRange e1 _) (CElem ei)
    = CElem $ L (getLoc e1) $ annTyE RInt $ reduceIntExpr $ 
        BinaryOp (ArithOp Plus) e1 ei
reduceRngs (CRange e1 _) (CRange el eh)
    = CRange (L (getLoc e1) $ annTyE RInt $ reduceIntExpr $ 
                BinaryOp (ArithOp Plus) e1 el)
             (L (getLoc e1) $ annTyE RInt $ reduceIntExpr $ 
                BinaryOp (ArithOp Plus) e1 eh)
reduceRngs _ _
    = error $ "<Language.CAO.Transformation.Eval>.\
              \<reduceRngs>: Unexpected case."

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

fInt :: AOp -> Integer -> Integer -> Integer
fInt Plus  = integerPlus
fInt Minus = integerMinus
fInt Times = integerTimes
fInt Power = integerPower
fInt Div   = integerDiv
fInt ModOp = integerMod

isAssoc :: AOp -> Bool
isAssoc Plus  = True
isAssoc Times = True
isAssoc _     = False

fBool :: BOp -> Bool -> Bool -> Bool
fBool   And = boolAnd
fBool   Or  = boolOr
fBool   Xor = boolXor