{-  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 DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}

{- |
Module      :  $Header$
Description :  Index language
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 (<reason>)

In CAO, sizes of types, accesses to vectors or matrices can depend on
symbolic constants. The language of these expressions is treated independently
of the language of CAO expressions. This module describes how these are
handled, dividing them in two types: one for conditions and invariants
over the symbolic constants and other for the expressions themselves.
--}

module Language.CAO.Index 
    ( ICond(..)
    , IExpr(..)
    , IAOp(..)
    , IBOp(..)
    , (.-.)
    , (.*.)
    , (.**.)
    , (./.)
    , (.%.) 
    , (.==.)
    , (./=.)
    , (.<.)
    , (.<=.)
    , (.>.)
    , (.>=.)
    , (.||.)
    , (.^^.)
    ) where

import Data.Foldable ( Foldable )
import Data.Traversable ( Traversable )

import Language.CAO.Common.Operator
import Language.CAO.Common.Outputable

-- TODO: Some modules use Indexes but they do not reduce them to the canonical form
--------------------------------------------------------------------------------
-- * Index conditions
-- TODO: Implication to decide validity?
-- | The conditions are expressed as boolean values and expressions over them.
data ICond id
    -- | Boolean literal
    = IBool !Bool
    -- | Boolean variable
    | IBInd !id
    -- | Boolean negation (not)
    | INot (ICond id)
    -- | Boolean conjunction. The list must be non-empty.
    | IAnd [ICond id]
    -- | Boolean binary operations.
    | IBoolOp IBOp (ICond id) (ICond id)
    -- | Non-negative operator on expressions. 
    -- This has the meaning of @0 <= expr@
    | ILeq (IExpr id)
    -- | Test of equality with 0 (@expr == 0@).
    | IEq (IExpr id)
    deriving (Eq, Read, Show, Functor, Foldable, Traversable)

instance PP id => PP (ICond id) where
    ppr = pprICond

pprICond :: PP id => ICond id -> CDoc
pprICond (IBool b) 
    = text $ show b
pprICond (IBInd b) 
    = ppr b
pprICond ctx@(INot e) 
    = char '!' <> pprParens_ e ctx
pprICond (IAnd l) 
    = parens (cat (punctuate (text " && ") (map ppr l)))
pprICond ctx@(IBoolOp op l r) 
    = pprParensL_ l ctx <+> ppr op <+> pprParensR_ r ctx
pprICond ctx@(ILeq r) 
    = integer 0 <+> text "<=" <+> pprParensR_ r ctx
pprICond ctx@(IEq r) 
    = integer 0 <+> text "="  <+> pprParensR_ r ctx

instance Operator (ICond id) where
    isSimple (IBool _)      = True
    isSimple (IBInd _)      = True
    isSimple _              = False
    
    assoc (IAnd _)          = ALeft
    assoc (IBoolOp op _ _)  = assoc op
    assoc _                 = NoAssoc

    fixity (INot _)         = Prefix
    fixity (IAnd _)         = Infix
    fixity (IBoolOp op _ _) = fixity op
    fixity (IEq _)          = Infix
    fixity (ILeq _)         = Infix
    fixity _                = Nofix

    prec (IBool _)          = 200
    prec (IBInd _)          = 200
    prec (INot _)           = 180
    prec (IAnd _)           = 60
    prec (IBoolOp op _ _)   = prec op
    prec (IEq _)            = 110
    prec (ILeq _)           = 120

-- | Boolean binary operations
data IBOp 
    = IOr  -- ^ Boolean disjunction
    | IXor -- ^ Boolean exclusive disjunction
    deriving (Eq, Read, Show)

instance PP IBOp where
  ppr = pprIBOp

pprIBOp :: IBOp -> CDoc
pprIBOp IOr  = text "||"
pprIBOp IXor = text "^^"
    
instance Operator IBOp where
    isSimple _  = False
    assoc _     = ALeft
    fixity _    = Infix

    prec IOr    = 40
    prec IXor   = 50

-- * Index expressions
-- | Index expressions. Normal form: ...
data IExpr id
    -- | Integer literals
    = IInt !Integer
    -- | Index variables
    | IInd !id
    -- | Arithmetic sum
    | ISum [IExpr id]
    -- | Binary arithmetic operators
    | IArith IAOp (IExpr id) (IExpr id)
    -- | Symmetric
    | ISym (IExpr id)
    deriving (Eq, Read, Show, Functor, Foldable, Traversable)

instance PP id => PP (IExpr id) where
    ppr = pprExpr

pprExpr :: PP id => IExpr id -> CDoc
pprExpr (IInt n)            = integer n
pprExpr (IInd i)            = ppr i
pprExpr (ISum l)            = parens (cat (punctuate (text " + ") (map ppr l)))
pprExpr ctx@(IArith op l r) = pprParensL_ l ctx <+> ppr op <+> pprParensR_ r ctx
pprExpr ctx@(ISym e)        = parens $ char '-' <> pprParens_ e ctx

instance Operator (IExpr id) where
    isSimple (IInt _)      = True
    isSimple (IInd _)      = True
    isSimple _             = False

    assoc (ISum _)         = ALeft
    assoc (IArith op _ _)  = assoc op
    assoc _                = NoAssoc

    fixity (ISum _)        = Infix
    fixity (IArith op _ _) = fixity op
    fixity (ISym _)        = Prefix
    fixity _               = Nofix

    prec (IInt _)          = 200
    prec (IInd _)          = 200
    prec (ISum _)          = 140
    prec (IArith op _ _)   = prec op
    prec (ISym _)          = 180

-- | Binary arithmetic operators
data IAOp 
    = IMinus -- ^ Substraction
    | ITimes -- ^ Multiplication
    | IPower -- ^ Exponentiation
    | IDiv   -- ^ Whole division
    | IModOp -- ^ Remainer of whole division
    deriving (Eq, Read, Show)

instance PP IAOp where
    ppr = pprIAOp

pprIAOp :: IAOp -> CDoc
pprIAOp IMinus = char '-'
pprIAOp ITimes = char '*'
pprIAOp IPower = text "**"
pprIAOp IDiv   = char '/'
pprIAOp IModOp = char '%'

instance Operator IAOp where
    isSimple _   = False

    assoc ITimes = ALeft
    assoc _      = NoAssoc

    fixity _     = Infix

    prec IMinus  = 140
    prec ITimes  = 150
    prec IDiv    = 150
    prec IModOp  = 150
    prec IPower  = 160

--------------------------------------------------------------------------------
-- * Syntactic sugar

(.-.), (.*.), (.**.), (./.), (.%.) :: IExpr id -> IExpr id -> IExpr id
(.-.)  = IArith IMinus
(.*.)  = IArith ITimes
(.**.) = IArith IPower
(./.)  = IArith IDiv
(.%.)  = IArith IModOp

(.==.), (./=.), (.<.), (.<=.), (.>.), (.>=.) :: IExpr id -> IExpr id -> ICond id
(.==.) e1 e2 = IEq (IArith IMinus e1 e2)
(./=.) e1 e2 = INot (e1 .==. e2)
(.<.)  e1 e2 = ILeq $ ISum [e2, ISym e1, IInt (-1)]
(.<=.) e1 e2 = ILeq $ ISum [e2, ISym e1] 
(.>.)  = flip (.<.)
(.>=.) = flip (.<=.)

(.||.), (.^^.) :: ICond id -> ICond id -> ICond id
(.||.) = IBoolOp IOr
(.^^.) = IBoolOp IXor