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