Index.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{- |
Module      :  $Header$
Description :  Index language
Copyright   :  (c) SMART Team / HASLab
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