{-  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/>. -}

{-
Module      :  $Header$
Description :  The Yices expression 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

-}

module Language.CAO.Translation.Yices 
    ( expr2Y
    , cond2Y
    , type2Y
    ) where

import Math.SMT.Yices.Syntax

import Language.CAO.Index
import Language.CAO.Common.Var
import Language.CAO.Type

cond2Y :: ICond Var -> ExpY
cond2Y ex = case ex of
    IBool b -> LitB b
    IBInd v -> VarE $ getSymbol v
    INot e -> NOT $ cond2Y e
    IAnd e -> AND $ map cond2Y e
    IBoolOp op e1 e2 ->(bOp2Y op) [cond2Y e1, cond2Y e2]
    ILeq e -> (LitI 0) :<= expr2Y e
    IEq e -> (LitI 0) := expr2Y e
        
expr2Y :: IExpr Var -> ExpY
expr2Y ex = case ex of 
    IInt n -> LitI n
    IInd v -> VarE $ getSymbol v
    ISum e -> aux e
    IArith op e1 e2 -> (aOp2Y op) (expr2Y e1) (expr2Y e2)
    ISym e -> LitI (-1) :*: expr2Y e
    where
    aux [e] = expr2Y e
    aux (e:es) = (expr2Y e) :+: aux es
    aux _ = error "<expr2Y>"

aOp2Y :: IAOp -> (ExpY -> ExpY -> ExpY)
aOp2Y IMinus = (:-:)
aOp2Y ITimes = (:*:)
aOp2Y IDiv   = DIV -- TODO: Is this the correct division?
aOp2Y IModOp = MOD
aOp2Y _ = error "aOp2Y"
--Power

bOp2Y :: IBOp -> ([ExpY] -> ExpY)
bOp2Y IOr = OR
bOp2Y _  = error "<bOp2Y>"
-- XOr

type2Y :: Type id -> Maybe TypY
type2Y t = case t of
    Bool -> return $ VarT "bool"
    Int -> return $ VarT "int"
    _ -> Nothing