{-  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 :  CAO internal type representation.
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

This module constains the definition of data types which represent the
internal representation of CAO types.

-}
module Language.CAO.Type where

{- TODO - Notes:
 - The Eq constraint in Type may have to be droped since syntactic equality is too
 - weak to be used in dependent types
 -
 - The Show instance for expressions may lead to unreadable representations. Using
 - pretty printing may solve this, but read instances may have to be changed to 
 - parsing functions
 -}

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

import Language.CAO.Common.Literal (Sign)
import Language.CAO.Common.Outputable
import Language.CAO.Common.Polynomial

import Language.CAO.Index

--------------------------------------------------------------------------------
-- * Type representation

data Type id
    -- | Arbitrary precision integers. These are mostly used for arithmetic
    --   operation.
    = Int
    -- | Register integers (machine length integers). These are mostly used
    --   for data type sizes, iteration (seq) indexes, access indexes, shift
    --   and rotate.
    | RInt
    -- | Boolean values.
    | Bool
    -- | Bit strings with a sign and a given size.
    | Bits !Sign (IExpr id)
    -- | Modular types with an optional base type, an optional polynomial
    --   variable and a polynomial expression.
    --   Not all combinations are valid. Thus, we may have:
    --   1) @Mod Nothing Nothing ...@
    --   2) ...
    | Mod (Maybe (Type id)) (Maybe id) (Pol id)
    -- | Vectors of a given size and type of elements.
    | Vector (IExpr id) (Type id)
    -- | Matrices with a given dimension and type of elements.
    | Matrix (IExpr id) (IExpr id) (Type id)
    -- | Type synonyms ...
    | TySyn id (Type id)
    -- | Function types: list of argument types, the return type and
    --   a 'Class' classifier (pure, read-only or procedure).
    | FuncSig [Type id] (Type id) (Class id)
    -- | Structure type: ...
    | Struct id [(id, Type id)]
    -- | Struct field type: ...
    | SField id (Type id)
    -- | Polynomial variables??
    | Indet (Type id)
    -- | Tupple of types. Used only internally.
    | Tuple [Type id]
    -- | No type.
    | Bullet
    -- | Type of symbolic constants: constant identifier, an optional invariant
    --   and its type.
    | Index id (Maybe (ICond id)) (Type id)
    -- | Type of generic variables: must not occur after type checking.
    | TyVar !TyVarId
    -- | Type of integer variables
    | IntVar !TyVarId
    -- | Type of unknown modules
    | ModVar !TyVarId
    deriving (Show, Read, Eq, Functor, Foldable, Traversable)

type TyVarId = Int

instance PP id => PP (Type id) where
    ppr = pprType

pprType :: PP id => Type id -> CDoc
pprType Int
    = text "int"
pprType RInt
    = text "register" <+> text "int"
pprType Bool
    = text "bool"
pprType (Bits s i)
    = ppr s <+> text "bits" <> brackets (ppr i)
pprType (Mod Nothing Nothing (Pol []))
    = text "mod" <> brackets (char '*')
pprType (Mod Nothing Nothing (Pol [p]))
    = text "mod" <> brackets (ppr p)
pprType (Mod (Just b) (Just i) p)
    = text "mod" <> brackets (  ppr b <> char '<' <> ppr i
                             <> char '>' <> char '/' <> ppr p)
pprType (Vector i t)
    = text "vector" <> brackets (ppr i) <+> text "of" <+> ppr t
pprType (Matrix r c t)
    = text "matrix" <> ppr [r, c] <+> text "of" <+> ppr t
pprType (TySyn _ t)
    = text "synonym" <+> text "to" <+> ppr t
pprType (FuncSig args ret clas)
    = ppr (Tuple args) <+> text "->" <+> ppr ret <+> braces (ppr clas)
pprType (Struct sn flds)
    = text "struct" <+> ppr sn <+> ifPprDebug (   text "@@Fields="
                                               <> noPprDebug (pprFlds flds)
                                               <> text "@@"
                                              )
pprType (SField fn ty)
    = text "field" <+> text "of" <+> text "struct" <+>
        ppr fn <+> char ':' <+> ppr ty
pprType (Indet ty)
    = text "indeterminate" <+> text "of" <+> ppr ty
pprType (Tuple tys)
    = parens $ pprElems tys
pprType Bullet
    = char '@'
pprType (Index i c t) 
    = ppr t <+> ifPprDebug (   text "forall @@Var=" 
                            <> ppr i <> text "@@Cond=" 
                            <> ppr c
                           )
pprType (TyVar i) 
    = char '@' <> ppr i
pprType (IntVar i) 
    = text "i@" <> ppr i
pprType (ModVar i) 
    = text "mod" <> brackets (char '*' <> ppr i)
pprType _ 
    = text "??"

pprFlds :: PP id => [(id, Type id)] -> CDoc
pprFlds = fsep . punctuate comma . map pprFld

pprFld :: PP id => (id, Type id) -> CDoc
pprFld (n, ty) = ppr n <+> colon <+> ppr ty

--------------------------------------------------------------------------------
-- * Auxiliary definitions

-- | Function classification (pure/read-only/procedure)
--
data Class id 
    -- | Pure functions do not have side-effects. Every call with the same
    --   arguments yields the same result.
    = Pure
    -- | Read-only functions access the global state but do not modify it.
    --   Different calls with the same arguments may yield different results,
    --   but the global values remain unchanged.
    | RO
    -- | Procedures access the global state and modify it as side-effect.
    --   This constructor carries the list of written global variables.
    | Proc [id]
    deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable)

instance PP id => PP (Class id) where
    ppr Pure     =   text "Pure"
    ppr RO       =   text "ReadOnly"
    ppr (Proc n) =   text "Procedure"
                 <+> ifPprDebug (text "#Globals_Written" <> ppr n)