{- 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 . -}
{- |
Module : $Header$
Description : Checks constraints over types
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
-}
module Language.CAO.Typechecker.Expr
( Constraint(..)
, Substitution
, (.=?=.)
, (.=?>.)
, (.=>>.)
, check
, TypePred(..)
, subst'
, checkAlgebraic
) where
import Control.Monad
import Language.CAO.Common.Error
import Language.CAO.Common.Monad
import Language.CAO.Common.Var
import Language.CAO.Typechecker.Constraint
import Language.CAO.Typechecker.Solver
import Language.CAO.Typechecker.Unification
import Language.CAO.Type
import Language.CAO.Type.Utils
check :: CaoMonad m => [Constraint] -> [TypePred] -> m [Substitution]
check cnst tpred = case solve cnst of
Right (s, c) -> do
let s' = checkSubst s
evalCond s' tpred
v <- valid' c
unless v $ tcError (UnknownErr $
".: <>: condition: " ++ show c :: ErrorCode Var)
return s'
Left err -> tcError err
data TypePred
= Algebraic (Type Var)
| AlgebraicExt (Type Var)
| FuncReturn (Type Var) (Type Var) -- Is this necessary in expressions?
| MatrixT (Type Var)
| BitsOrVector (Type Var)
| BitsT (Type Var)
| ModT (Type Var)
| IntOrMod (Type Var)
deriving Show
checkSubst :: [Substitution] -> [Substitution]
checkSubst = map worker
where
worker (Subst t (IntVar _)) = Subst t Int
worker s = s
evalCond :: CaoMonad m => [Substitution] -> [TypePred] -> m ()
evalCond sbs = mapM_ aux
where
aux (Algebraic t) = checkAlgebraic $ subst' sbs t
aux (AlgebraicExt t) = let t' = subst' sbs t
in unless (isAlgebraic t' || isBits t') $ tcError (WrongTypeException t' AlgebraicType)
aux (FuncReturn t1 rt) = let t1' = subst' sbs t1; rt' = subst' sbs rt
in unless (not (isNil t1') || isNil rt') $ tcError (FuncReturnErr :: ErrorCode Var)
aux (MatrixT t) = let t' = subst' sbs t
in unless (isMatrix t') $ tcError (WrongTypeException t' MatrixType)
aux (BitsOrVector t) = let t' = subst' sbs t
in unless (isBits t' || isVector t') $ tcError (WrongTypeException t' BitsOrVectorType)
aux (BitsT t) = let t' = subst' sbs t
in unless (isBits t') $ tcError (WrongTypeException t' BitsType )
aux (ModT t) = let t' = subst' sbs t
in unless (isMod t') $ tcError (WrongTypeException t' ModType )
aux (IntOrMod t) = let t' = subst' sbs t
in unless (isMod t' || isInt t') $ tcError (WrongTypeException t' IntOrModType )
checkAlgebraic :: CaoMonad m => Type Var -> m ()
checkAlgebraic t = unless (isAlgebraic t) $ tcError (WrongTypeException t AlgebraicType)