{- 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 . -}
{-# 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
Stability : experimental
Portability : non-portable ()
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