{-  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 :  Decision procedures for constraints
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.Solver
  ( valid
  , valid'
  ) where

import Control.Monad

import Language.CAO.Common.Error
import Language.CAO.Common.Monad
import Language.CAO.Common.State
import Language.CAO.Common.Var
import Language.CAO.Index
import Language.CAO.Index.Eval

import Language.CAO.Typechecker.SMT

valid :: CaoMonad m => [ICond Var] -> ErrorCode Var -> m ()
valid i e = do
    r <- validEval $ IAnd i
    unless r $ tcError e 

valid' :: CaoMonad m => [ICond Var] -> m Bool
valid' i = validEval $ IAnd i

validEval :: CaoMonad m => ICond Var -> m Bool
validEval c = case evalCond c of
    IBool b -> return b
    IAnd i -> do
        hyp <- getHypothesis
        case fromHyp hyp i of
            IBool b -> return b
            r -> checkValidity (IAnd hyp) r
    _ -> error $ "<validEval>: unexpected canonical form."

fromHyp :: [ICond Var] -> [ICond Var] -> ICond Var
fromHyp hyp cond = let
        cond' = filter (not . checkHyp hyp) cond
    in if null cond' then IBool True else IAnd cond'

    where

    checkHyp :: [ICond Var] -> ICond Var -> Bool
    checkHyp hyp' c = any (exactHyp c) hyp'

    exactHyp :: ICond Var -> ICond Var -> Bool
-- C, a |= a
    exactHyp c h
        | c == h = True
-- C, 0 <= a |= 0 <= b  <==  |= a <= b'
    exactHyp (ILeq b) (ILeq a) = let
            (n,  c,  i) = decompose b
            (n', c', i') = decompose a 
        in if i == i' 
            then if evalBool [c .<. IInt 0, c' .<. IInt 0]
                then evalBool [(n .*. c') .<=. (n' .*. c)]
                else if evalBool [c .>. IInt 0, c' .>. IInt 0]
                    then evalBool [(n' .*. c) .<=. (n .*. c')]
                    else evalBool [a .<=. b]
            else evalBool [a .<=. b]

    exactHyp c (IAnd l) = checkHyp l c
    exactHyp _ _ = False

evalBool :: [ICond Var] -> Bool
evalBool = toBool . evalCond . IAnd
toBool :: ICond Var -> Bool
toBool (IBool b) = b
toBool _ = False 

-- (Term, Coeficient, Variable)
decompose :: IExpr Var -> (IExpr Var, IExpr Var, IExpr Var)
decompose (ISum [IInt n, IArith ITimes c i]) = (IInt n, c, i)
decompose (ISum [IInt n, i])                 = (IInt n, IInt 1, i)
decompose (ISum [IArith ITimes c i])         = (IInt 0, c, i)
decompose (IArith ITimes c i)                = (IInt 0, c, i)
decompose i                                  = (IInt 0, IInt 1, i)