{-  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 :  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 (<reason>)

-}

module Language.CAO.Typechecker.Constraint (
      Constraint(..)
    , Substitution(..)
    , (.=?=.)
    , (.=?>.)
    , (.=>>.)
    , subst
    , subst'
    , substSqrL
    , substL
    , remove
    , substitution
 ) where

import Language.CAO.Common.Outputable hiding (equals)
import Language.CAO.Common.Var hiding (mrange)

import Language.CAO.Index

import Language.CAO.Type

{- This may be of the form:
 - two types must be equal
 - two types must be coercible
 - a predicate that a type(s) must meet
 - an error to report the failure

 - two level constraints:
    - type constrains are solved and index constraints are generated
    - index constraints are solved
-}

(.=?=.), (.=?>.), (.=>>.) :: Type Var -> Type Var -> Constraint
(.=?=.) t1 t2 = Equal t1 t2
(.=?>.) t1 t2 = Coerces t1 t2
(.=>>.) t1 t2 = Casts t1 t2

data Constraint 
    = Equal (Type Var) (Type Var)
    | Coerces (Type Var) (Type Var)
    | Unifies (Type Var) (Type Var) (Type Var)
    | Casts (Type Var) (Type Var)

    | ToAlgebraic (Type Var) (Type Var)

    | Mult (Type Var) (Type Var) (Type Var)
    | Pow (Type Var) (Type Var)
    | Conc (Type Var) (Type Var) (Type Var)
    | UnifiesL (Type Var) [Type Var]
    | UnifiesC (Type Var) (Type Var) (Type Var)

    | MAccess (Type Var) (Type Var) (Maybe (IExpr Var, IExpr Var))
    | MRange (Type Var) (Type Var) (IExpr Var) (IExpr Var) (IExpr Var) (IExpr Var)
    | MRow (Type Var) (Type Var) (IExpr Var) (IExpr Var) (Maybe (IExpr Var))
    | MCol (Type Var) (Type Var) (IExpr Var) (IExpr Var) (Maybe (IExpr Var))

    | VBAccess (Type Var) (Type Var) (Maybe (IExpr Var))
    | VBRange (Type Var) (Type Var) (IExpr Var) (IExpr Var)

instance Show Constraint where
    show (Equal t1 t2) = showPpr t1 ++ " =?= " ++ showPpr t2
    show (Coerces t1 t2) = showPpr t1 ++ " =?> " ++ showPpr t2
    show (Unifies tu t1 t2) = showPpr t1 ++ " =^^=> " ++ showPpr t2 ++ " = " ++ showPpr tu
    show (Casts t1 t2) = "(" ++ showPpr t1 ++ ")" ++ showPpr t2
    show (Mult tv t1 t2) = showPpr t1 ++ " * " ++ showPpr t2 ++ " = " ++ showPpr tv
    show (Pow t1 t2) = showPpr t1 ++ " = ** " ++ showPpr t2
    show (Conc tv t1 t2) = showPpr t1 ++ " @ " ++ showPpr t2 ++ " = " ++ showPpr tv
    show (UnifiesL tv tlst) = "[" ++ concatMap showPpr tlst ++ "] = " ++ showPpr tv 
    show (UnifiesC tu t1 t2) = showPpr t1 ++ " =^C^=> " ++ showPpr t2 ++ " = " ++ showPpr tu
    show (ToAlgebraic tu t) = "toAlgebraic(" ++ showPpr t ++ ") = " ++ showPpr tu
    show _ = "access"

data Substitution = Subst Int (Type Var)
    deriving Eq

instance Show Substitution where
    show (Subst n t2) = "@" ++ show n ++ " ==> " ++ showPpr t2

substitution :: [Substitution] -> [Constraint] -> [Constraint]
substitution [] c = c
substitution sb c = map (substL sb) c

substL :: [Substitution] -> Constraint -> Constraint
substL sl c = foldr substC c sl

substC :: Substitution -> Constraint -> Constraint
substC s (Equal t1 t2) = Equal (subst s t1) (subst s t2)
substC s (Coerces t1 t2) = Coerces (subst s t1) (subst s t2)
substC s (Unifies tu t1 t2) = Unifies (subst s tu) (subst s t1) (subst s t2)
substC s (Casts t1 t2) = Casts (subst s t1) (subst s t2)
substC s (ToAlgebraic t1 t2) = ToAlgebraic (subst s t1) (subst s t2)
substC s (Mult tu t1 t2) = Mult (subst s tu) (subst s t1) (subst s t2)
substC s (Pow t1 t2) = Pow (subst s t1) (subst s t2)
substC s (Conc tu t1 t2) = Conc (subst s tu) (subst s t1) (subst s t2)
substC s (UnifiesL t1 tlst) = UnifiesL (subst s t1) (map (subst s) tlst)
substC s (UnifiesC tu t1 t2) = UnifiesC (subst s tu) (subst s t1) (subst s t2)
substC s (MAccess t1 t2 mi) = MAccess (subst s t1) (subst s t2) mi
substC s (MRange t1 t2 i1 i2 i3 i4) = MRange (subst s t1) (subst s t2) i1 i2 i3 i4
substC s (MRow t1 t2 i1 i2 mi) = MRow (subst s t1) (subst s t2) i1 i2 mi
substC s (MCol t1 t2 i1 i2 mi) = MCol (subst s t1) (subst s t2) i1 i2 mi
substC s (VBAccess t1 t2 mi) = VBAccess (subst s t1) (subst s t2) mi
substC s (VBRange t1 t2 i1 i2) = VBRange (subst s t1) (subst s t2) i1 i2

subst' :: [Substitution] -> Type Var -> Type Var
subst' s t = foldr subst t s

subst :: Substitution -> Type Var -> Type Var
subst (Subst n' t) (IntVar n) | n == n' = t
subst (Subst n' t) (ModVar n) | n == n' = t
subst (Subst n' t) (TyVar n)  | n == n' = t
subst s (Tuple ts) = Tuple $ map (subst s) ts
subst _ t = t

remove :: TyVarId -> [Substitution] -> [Substitution]
remove tid = filter (\ (Subst n _) -> tid /= n) 

-- (active substitution list) (target substitution list)
substSqrL :: [Substitution] -> [Substitution] -> [Substitution]
substSqrL sbs = map (flip substSqr' sbs)

-- (target substitution) (active substitution list)
substSqr' :: Substitution -> [Substitution] -> Substitution
substSqr' s = foldr substSqr s

-- (active substitution) (target substitution)
substSqr :: Substitution -> Substitution -> Substitution
substSqr sbs (Subst n t) = Subst n (subst sbs t)