cao-0.1: src/Language/CAO/Translation/Yices.hs

{-
Module      :  $Header$
Description :  The Yices expression translation
Copyright   :  (c) SMART Team / HASLab
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