{-  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/>. -}

{- |
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 <paufil@di.uminho.pt>
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 $
            "<TypeChecker.Expr>.<check>: <<TODO>>: 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)