{-  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 :  Unification of type when checking expressions.
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.Unification ( solve ) where

import Data.List (partition)

import Language.CAO.Common.Error
import Language.CAO.Common.Polynomial
import Language.CAO.Common.Var hiding (mrange)

import Language.CAO.Index

import Language.CAO.Type
import Language.CAO.Type.Utils
import Language.CAO.Typechecker.Constraint

import Language.CAO.Index.Eval

{-
Invariants:
* Coercions are directed, i.e., the left type coerces to the right type. The left
  type is the actual type while the right type is the expected type.
* Unification is not directed, i.e., left and right types are interchangeable.
* Unification always takes a type variable which will take the type resulting of
  the unification.
* Casts are directed. The left type is the source type and the right type is the
  target type.
* The target type of a cast is always determined, i.e., it is not a type variable.
* After a cast of a type variable, this cannot occur again.
* Leafs (variables and constants) types cannot be unbounded type variables. 
  They are either base types or integer type variables.
* The list of constraints is collected in a post-order traversal of the expression.
  This means that leafs  in the expression are processed 
  before the operators. This as a number of implications:
  - A given type variable only appears in a constraint *after* appearing as a result
    of an unification. This means that unification is a kind of type variable 
    introduction.
  - Since each unification resolves to a type which is not an unbounded variable,
    all the subsequent occurences get replaced. This means that, when processing
    constraints, unbounded variables can only occur as the result of an unification.
  - It is possible that integer type variables are not instantiated. In this case,
    the integer type is assumed.
-}

-- TODO: Missing tuple case
solve :: [Constraint] -> Either (ErrorCode Var) ([Substitution], [ICond Var])
solve [] = return ([], [])
solve (Equal t1 t2              : s)  = solvePat (equals t1 t2) s
solve (Coerces t1 t2            : s)  = solvePat (coerces t1 t2) s
solve (Unifies tv t1 t2         : s)  = solvePat (unifies tv t1 t2) s
solve (UnifiesC tv t1 t2        : s)  = solvePat (unifiesC tv t1 t2) s
solve (Casts t1 t2              : s)  = solvePat (casts t1 t2) s
solve (ToAlgebraic t1 t2        : s)  = solvePat (toAlgebraic t1 t2) s
solve (Mult tv t1 t2            : s)  = solvePat (mult tv t1 t2) s
solve (Pow t1 t2                : s)  = solvePat (power t1 t2) s
solve (Conc tv t1 t2            : s)  = solvePat (conc tv t1 t2) s
solve (UnifiesL tv tlst         : s)  = solvePat (unifiesL tv tlst) s
solve (MAccess t1 t2 mi         : s)  = solvePat (maccess t1 t2 mi) s
solve (MRange t1 t2 i1 i2 i3 i4 : s)  = solvePat (mrange t1 t2 i1 i2 i3 i4) s
solve (MRow t1 t2 i1 i2 mi      : s)  = solvePat (mrow t1 t2 i1 i2 mi) s
solve (MCol t1 t2 i1 i2 mi      : s)  = solvePat (mcol t1 t2 i1 i2 mi) s
solve (VBAccess t1 t2 mi        : s)  = solvePat (vbaccess t1 t2 mi) s
solve (VBRange t1 t2 i1 i2      : s)  = solvePat (vbrange t1 t2 i1 i2) s

solvePat
  :: Either (ErrorCode Var) ([Substitution], [ICond Var])
     -> [Constraint]
     -> Either (ErrorCode Var) ([Substitution], [ICond Var])
solvePat f s = do
    (sbs, c) <- f
    (s', c') <- solve (substitution sbs s)
    let sbs' = substSqrL s' sbs
    return (sbs' ++ s', c ++ c')

skip :: Either (ErrorCode Var) ([Substitution], [ICond Var])
skip = return ([], [])

self :: Type Var -> Substitution
self t@(TyVar n) = Subst n t
self t@(IntVar n) = Subst n t
self t@(ModVar n) = Subst n t
self _ = error "self substitution: not expected"

equals :: Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
equals Bool Bool = skip
equals RInt RInt = skip
equals Int Int = skip
equals (IntVar n1) t2@(IntVar n2)
    | n1 == n2  = skip
    | otherwise = return ([Subst n1 t2, self t2], [])
equals t1@(IntVar n1) t2
    | isInt t2  = return ([Subst n1 t2], []) 
    | otherwise = Left (TypeMismatchException t1 t2 MatchException)
equals t1 t2@(IntVar n2)
    | isInt t1 = return ([Subst n2 t1], [])
    | otherwise = Left (TypeMismatchException t1 t2 MatchException)
equals (Bits s1 n1) (Bits s2 n2) | s1 == s2 = return ([], [n1 .==. n2])
equals (ModVar m1) t2@(ModVar m2)
    | m1 == m2 = skip
    | otherwise = return ([Subst m1 t2, self t2], [])
-- TODO: missing cases for ModVar's
equals (Mod Nothing Nothing (Pol [Mon (CoefI n1) EZero]))
       (Mod Nothing Nothing (Pol [Mon (CoefI n2) EZero])) =
    return ([], [n1 .==. n2])
equals (Mod (Just t1) v1 p1) (Mod (Just t2) v2 p2) | v1 == v2 = do
    (s', c') <- equals t1 t2
    c'' <- eqPol p1 p2
    return (s', c' ++ c'')
equals (Vector i1 t1) (Vector i2 t2) = do
    (s', c') <- equals t1 t2
    return (s', i1 .==. i2 : c')
equals (Matrix i1 j1 t1) (Matrix i2 j2 t2) = do
    (s', c') <- equals t1 t2
    let c = [i1 .==. i2, j1 .==. j2]
    return (s', c ++ c')
equals (Struct s1 _) (Struct s2 _) | s1 == s2 = skip

equals t1 t2 = Left (TypeMismatchException t1 t2 MatchException)

coerces :: Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
coerces Bool Bool = skip
coerces RInt RInt = skip
coerces Int  Int  = skip
-- When two integer type variables are compared:
-- - if they are equal, they can be removed since they add no information
-- - if they are different, one replaces all occurrences of the other
coerces (IntVar n1) t2@(IntVar n2)
    | n1 == n2  = skip
    | otherwise = return ([Subst n1 t2, self t2], [])
-- When a integer type variable is being coerced to another type, the target type
-- can only be an integer (rint or int) type, since integers cannot be coerced to any 
-- other type.
-- - The integer type variable is replaced by the target type in all its occurrences.
-- - Otherwise, the coercion is not possible
coerces t1@(IntVar n1) t2
    | isInt t2  = return ([Subst n1 t2], []) 
    | otherwise = Left (TypeMismatchException t1 t2 MatchException)
-- When a type is being coerced to an integer type variable, the source type can be
-- either a bit string or an integer (rint or int) by the possible coercion rules.
-- - if it is an integer type, this type replaces all occurrences of the variable
-- - if it is a bit string, this implies that the variable type is int, since coercions
--   to rint are not allowed.
coerces t1 (IntVar n2)
    | isInt t1 = return ([Subst n2 t1], [])
    | isBits t1 = return ([Subst n2 Int], [])

-- Index
coerces t1 (Index _ _ t2) = coerces t1 t2
-- Bits to Integers
coerces (Bits _ _) Int = skip
-- Bits
coerces (Bits s1 n1) (Bits s2 n2) | s1 == s2 = return ([], [n1 .==. n2])
-- Mod's
-- What may happen if the base of a Mod is an integer? Should that be possible?
coerces (ModVar m1) t2@(ModVar m2)
    | m1 == m2 = skip
    | otherwise = return ([Subst m1 t2, self t2], [])
coerces (ModVar m1) m2@(Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) =
    return ([Subst m1 m2], [])
coerces (ModVar m1) (Mod (Just t2) _ _) = coerces (ModVar m1) t2
-- TODO: missing cases for ModVar's
--coerces (Mod Nothing Nothing (Pol [])) (Mod {}) = skip
coerces (Mod Nothing Nothing (Pol [Mon (CoefI n1) EZero]))
        (Mod Nothing Nothing (Pol [Mon (CoefI n2) EZero])) =
    return ([], [n1 .==. n2])
coerces (Mod (Just t1) v1 p1) (Mod (Just t2) v2 p2) | v1 == v2 = do
    (s', c') <- coerces t1 t2
    c'' <- eqPol p1 p2
    return (s', c' ++ c'')
coerces t1 (Mod (Just b) _ _) = coerces t1 b
-- Vectors
coerces (Vector i1 t1) (Vector i2 t2) = do
    (s', c') <- coerces t1 t2
    return (s', i1 .==. i2 : c')
-- Matrices
coerces (Matrix i1 j1 t1) (Matrix i2 j2 t2) = do
    (s', c') <- coerces t1 t2
    let c = [i1 .==. i2, j1 .==. j2]
    return (s', c ++ c')

coerces (Struct s1 _) (Struct s2 _) | s1 == s2 = skip

coerces t1 t2 = Left (TypeMismatchException t1 t2 MatchException)

eqPol :: Pol Var -> Pol Var -> Either (ErrorCode Var) [ICond Var]
eqPol (Pol p1) (Pol p2) = eqPolLst p1 p2
    where
    eqPolLst [] [] = return []
    eqPolLst (m1 : mlst1) (m2 : mlst2) = do
        c1 <- eqMon m1 m2
        c2 <- eqPolLst mlst1 mlst2
        return (c1 ++ c2)
    eqPolLst _ _ = Left $ UnknownErr "eqPol: <<TODO>>: eqPolLst"

    eqMon (Mon c1 b1) (Mon c2 b2) = do
        c1' <- eqCoef c1 c2
        _  <- eqBase b1 b2
        return c1'

    eqCoef (CoefI i1) (CoefI i2) = return [i1 .==. i2]
    eqCoef (CoefP pl1) (CoefP pl2) = eqPol pl1 pl2
    eqCoef _ _ = Left $ UnknownErr "eqPol: <<TODO>>: eqCoef"

    eqBase EZero EZero = return []
    eqBase (MExpI v1 e1) (MExpI v2 e2) | v1 == v2 && e1 == e2 = return []
    eqBase _ _ = Left $ UnknownErr "eqPol: <<TODO>>: eqBase"

unifies :: Type Var -> Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
-- Operations on bits imply a coercion to Int. This rule must come
-- before the rest of unification, otherwise, equal bit string types
-- would unify to themselves.
unifies (TyVar tv) (Bits _ _) (Bits _ _) = return ([Subst tv Int], [])

unifies (TyVar tv) t1@(IntVar n1) t2@(IntVar n2) 
    | n1 == n2  = return ([Subst tv t2, self t1, self t2], [])
    | otherwise = return ([Subst n1 t2, Subst tv t2, self t2], [])

-- Unification of an integer type variable with a integer type
-- returns this integer type.
-- Unification of an integer type variable with a bit string
-- returns an integer (the only possible unification)
unifies (TyVar tv) (IntVar n1) t2
    | isInt t2 = return ([Subst n1 t2, Subst tv t2], [])
    | isBits t2 = return ([Subst n1 Int, Subst tv Int], [])
-- Symmetric case of the above
unifies (TyVar tv) t1 (TyVar n2)
    | isInt t1 = return ([Subst n2 t1, Subst tv t1], [])
    | isBits t1 = return ([Subst n2 Int, Subst tv Int], [])

unifies (TyVar tv) t1@(ModVar m1) t2@(ModVar m2)
    | m1 == m2 = return ([Subst tv t2, self t1, self t2], [])
    | otherwise = return ([Subst m1 t2, Subst tv t2, self t2], [])

-- Mod variables
unifies (TyVar tv) (ModVar m1) m2@(Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) =
    return ([Subst m1 m2, Subst tv m2], [])

unifies (TyVar tv) (ModVar m1) (Mod (Just t2) _ _) = unifies (TyVar tv) (ModVar m1) t2

unifies (TyVar tv) m1@(Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) (ModVar m2) =
    return ([Subst m2 m1, Subst tv m1], [])

unifies (TyVar tv)  (Mod (Just t1) _ _) (ModVar m2) = unifies (TyVar tv) (ModVar m2) t1

-- Unification cannot rely on just coercion for the case of vectors
-- and matrices, because of the unification must be propagated 
-- through the structure.
-- Unification of Vectors
unifies (TyVar tv) (Vector i1 t1) (Vector i2 t2) = do
    (sbs, c') <- unifies (TyVar tv) t1 t2
    let tv' = subst' sbs (TyVar tv) -- This can be improved...
        sbs' = Subst tv (Vector i1 tv') : remove tv sbs -- Arbitrary choice since i1 and i2 must be equal
    return (sbs', i1 .==. i2 : c')
-- Unification of Matrices
unifies (TyVar tv) (Matrix i1 j1 t1) (Matrix i2 j2 t2) = do
    (sbs, c') <- unifies (TyVar tv) t1 t2
    let tv' = subst' sbs (TyVar tv) -- This can be improved...
        sbs' = Subst tv (Matrix i1 j1 tv') : remove tv sbs -- Arbitrary choice since i1 and i2 must be equal
        c = i1 .==. i2 : j1 .==. j2 : c'
    return (sbs', c)

unifies (TyVar tv) s@(Struct s1 _) (Struct s2 _) | s1 == s2 =
    return ([Subst tv s], [])
-- General unification case uses coercions
-- TODO: use try/catch??
unifies (TyVar tv) t1 t2 = case coerces t1 t2 of
    Left _ -> case coerces t2 t1 of
        Left _ -> Left (TypeMismatchException t1 t2 UnificationException)
        Right (sbs, c) -> do
            let sbs' = Subst tv (subst' sbs t1) : sbs
            return (sbs', c)
    Right (sbs, c) -> do
            let sbs' = Subst tv (subst' sbs t2) : sbs
            return (sbs', c)
unifies _ t1 t2 = Left (TypeMismatchException t1 t2 UnificationException)

--casts' t1 t2 | isModInt t1   = return $ isIntExt t2 || isModInt t2
casts :: Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
casts RInt Int = skip
casts Int RInt = skip
-- Any integer type variable is castable to an int or rint
-- So, we can assume that the source type is equal to the target type
casts (IntVar n) Int = return ([Subst n Int], [])
casts (IntVar n) RInt = return ([Subst n RInt], [])
-- rint's are not directly castable to bits to avoid errors.
-- This also means that an integer type variable is only castable
-- to bits if it is an int.
casts (IntVar n) (Bits _ _) = return ([Subst n Int], [])
casts Int (Bits _ _) = skip
casts (Bits {}) (Bits {}) = skip
casts (ModVar _) Int = skip
casts (ModVar _) (Bits _ _) = skip
casts (ModVar _) (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) = skip
casts (ModVar _) (Mod (Just _) (Just _) (Pol _)) = skip
casts (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) Int = skip
casts (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) (Bits _ _) = skip -- Possible through int
casts (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) = skip
casts (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) (Mod (Just _) (Just _) (Pol _)) = skip
casts Int (Mod {}) = skip
-- This is only possible when the integer type variable is an Int
casts (IntVar n) (Mod {}) = return ([Subst n Int], [])
casts (Bits _ _) (Mod {}) = skip
{-
casts Int (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) = skip
casts (Bits _ _) (Mod Nothing Nothing (Pol [Mon (CoefI _) EZero])) = skip -- Possible through int
casts Int (Mod (Just bt) (Just v) _) = skip
casts (Bits _ _) (Mod (Just bt) (Just v) _) = skip-}
casts (Vector i1 t1) (Mod (Just bt) (Just _) pol) = do
    (sbs, c) <- casts t1 bt
    return (sbs, i1 .==. IInt (degree pol) : c)
casts (Mod (Just bt) (Just _) pol) (Vector i2 t2) = do
    (sbs, c) <- casts bt t2
    return (sbs, i2 .==. IInt (degree pol) : c)
casts (Matrix i1 j1 t1) (Mod (Just bt) (Just _) pol) = do
    (sbs, c) <- casts t1 bt
    let deg = IInt $ degree pol
        c' = IAnd [i1 .==. IInt 1, j1 .==. deg] .||. IAnd [j1 .==. IInt 1, i1 .==. deg] 
    return (sbs, c' : c)
casts (Mod (Just bt) (Just _) pol) (Matrix i2 j2 t2) = do
    (sbs, c) <- casts bt t2
    let deg = IInt $ degree pol
        c' = IAnd [i2 .==. IInt 1, deg .==. j2] .||. IAnd [j2 .==. IInt 1, deg .==. i2]
    return (sbs, c' : c)
casts (Matrix i1 j1 t1) (Vector i2 t2) = do
    (sbs, c) <- casts t1 t2
    let c' = IAnd [i1 .==. IInt 1, j1 .==. i2] .||. IAnd [j1 .==. IInt 1, i1 .==. i2] 
    return (sbs, c' : c)
casts (Vector i1 t1) (Matrix i2 j2 t2) = do
    (sbs, c) <- casts t1 t2
    let c' = IAnd [i2 .==. IInt 1, i1 .==. j2] .||. IAnd [j2 .==. IInt 1, i1 .==. i2]
    return (sbs, c' : c)
casts (Vector i1 t1) (Vector i2 t2) = do
    (sbs, c) <- casts t1 t2
    return (sbs, i1 .==. i2 : c)
casts (Matrix i1 j1 t1) (Matrix i2 j2 t2) = do
    (sbs, c) <- casts t1 t2
    return (sbs, i1 .==. i2 : j1 .==. j2 : c)
casts (Tuple t1) (Tuple t2) = solve $ zipWith Casts t1 t2

casts t1 t2 = either (const (Left (TypeMismatchException t1 t2 CastException))) Right (coerces t1 t2)

toAlgebraic :: Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
toAlgebraic (TyVar tv) (Bits _ _) = return ([Subst tv Int], [])
toAlgebraic (TyVar tv) t = return ([Subst tv t], [])
toAlgebraic _ _ = Left (UnknownErr "toAlgebraic")

mult :: Type Var -> Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
mult (TyVar tv) (Matrix r1 c1 t1) (Matrix r2 c2 t2) = do
    (sbs, c) <- mult (TyVar tv) t1 t2
    let tv' = subst' sbs (TyVar tv)
        sbs' = Subst tv (Matrix r1 c2 tv') : remove tv sbs
    return (sbs', c ++ [c1 .==. r2])
mult tv@(TyVar _) t1 t2 = unifies tv t1 t2
mult _ t1 t2 = Left (TypeMismatchException t1 t2 UnificationException)

power :: Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
power (TyVar tv) (Matrix r1 c1 t) = do
    (sbs, c) <- power (TyVar tv) t
    let tv' = subst' sbs (TyVar tv)
        sbs' = Subst tv (Matrix r1 c1 tv') : remove tv sbs
    return (sbs', c ++ [r1 .==. c1])
power (TyVar tv) (Bits _ _) = do -- Coercible to Int
    return ([Subst tv Int], [])
power (TyVar tv) t =
    return ([Subst tv t], [])
power t1 t2 = Left (TypeMismatchException t1 t2 UnificationException)

-- This is a particular case for concatenation of vectores and equality. The unification of equal bit strings
-- should be a bit string. In all other cases, bit strings are taken as integers.
-- This may be a result of a poor design...
unifiesC :: Type Var -> Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
unifiesC (TyVar tv) (Bits s1 (IInt n1)) (Bits s2 (IInt n2)) | s1 == s2 && n1 == n2 =
    return ([Subst tv (Bits s1 (IInt n1))], [])
-- TODO: Add the general case for testing bit string sizes with arbitrary case
unifiesC tv t1 t2 = unifies tv t1 t2

conc :: Type Var -> Type Var -> Type Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
conc (TyVar tv) (Bits s1 n1) (Bits s2 n2) | s1 == s2 =
    return ([Subst tv (Bits s1 (evalExpr (ISum [n1, n2])))], [])
conc (TyVar tv) (Vector n1 t1) (Vector n2 t2) = do
    (sbs, c) <- unifiesC (TyVar tv) t1 t2
    let tv' = subst' sbs (TyVar tv)
        sbs' = Subst tv (Vector (evalExpr (ISum [n1, n2])) tv') : remove tv sbs -- TODO: improve this pattern
    return (sbs', c)
conc _ t1 t2 = Left (TypeMismatchException t1 t2 UnificationException)

isModVar :: Type Var -> Bool
isModVar m = case m of
    ModVar _ -> True
    _ -> False

unifiesL :: Type Var -> [Type Var] -> Either (ErrorCode Var) ([Substitution], [ICond Var])
unifiesL _ [] = error "<Unification>.<unifiesL>: not expected empty case"
-- There is nothing to unify
unifiesL (TyVar tv) [t] = return ([Subst tv t], [])
unifiesL (TyVar tv) tlst = 
    let (modvars, tvars) = partition isModVar tlst
    in if null tvars
        then return (sbsLst tv (tail modvars) (head modvars), [])
        else do
            (tu, c) <- aux (TyVar tv) tvars
            let sbs =  sbsLst tv modvars tu
            return (sbs, c)

    where
    sbsLst t modvars tu = Subst t tu : zipWith (\ (ModVar v) -> Subst v) modvars (repeat tu)

    aux _ [t] = return (t, [])
    aux tv' (t:ts) = aux' tv' t ts []
    aux _ _ = error "unifiesL.aux: Not expected case"

    aux' _ tu [] cs = return (tu, cs)
    aux' tv' tu (t:ts) cs = do
        (sbs, c) <- unifies tv' t tu
        let tu' = subst' sbs tv'
        aux' tv' tu' ts (c ++ cs)
unifiesL _ _ = error "<Unification>.<unifiesL>: not expected case"

maccess :: Type Var -> Type Var -> Maybe (IExpr Var, IExpr Var) -> Either (ErrorCode Var) ([Substitution], [ICond Var])
maccess (TyVar tv) (Matrix u v t) mi = return ([Subst tv t], cAccessM u v mi)
maccess _ t2 _ = Left $ WrongTypeException t2 MatrixType

mrange :: Type Var -> Type Var -> IExpr Var -> IExpr Var -> IExpr Var -> IExpr Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
mrange (TyVar tv) (Matrix u v it) i1 i2 i3 i4 =
    return ( [Subst tv (Matrix (cSize i1 i2) (cSize i3 i4) it)]
           , cRange u i1 i2 ++ cRange v i3 i4)
mrange _ t2 _ _ _ _ = Left $ WrongTypeException t2 MatrixType


mrow :: Type Var -> Type Var -> IExpr Var -> IExpr Var -> Maybe (IExpr Var) -> Either (ErrorCode Var) ([Substitution], [ICond Var])
mrow (TyVar tv) (Matrix v u it) i1 i2 mi =
    return ([Subst tv (Matrix (IInt 1) (cSize i1 i2) it)], cRange u i1 i2 ++ cAccess v mi)
mrow _ t2 _ _ _ = Left $ WrongTypeException t2 MatrixType

mcol :: Type Var -> Type Var -> IExpr Var -> IExpr Var -> Maybe (IExpr Var) -> Either (ErrorCode Var) ([Substitution], [ICond Var])
mcol (TyVar tv) (Matrix v u it) i1 i2 mi = do
    return ([Subst tv (Matrix (cSize i1 i2) (IInt 1) it)], cRange v i1 i2 ++ cAccess u mi)
mcol _ t2 _ _ _ = Left $ WrongTypeException t2 MatrixType

vbaccess :: Type Var -> Type Var -> Maybe (IExpr Var) -> Either (ErrorCode Var) ([Substitution], [ICond Var])
vbaccess (TyVar tv) (Bits s k) mi = return ([Subst tv (Bits s (IInt 1))], cAccess k mi)
vbaccess (TyVar tv) (Vector k t) mi = return ([Subst tv t], cAccess k mi)
vbaccess _ t2 _ = Left $ WrongTypeException t2 BitsOrVectorType

vbrange :: Type Var -> Type Var -> IExpr Var -> IExpr Var -> Either (ErrorCode Var) ([Substitution], [ICond Var])
vbrange (TyVar tv) (Bits s k) i1 i2 = 
    return ([Subst tv (Bits s (cSize i1 i2))], cRange k i1 i2)
vbrange (TyVar tv) (Vector k t) i1 i2 =
    return ([Subst tv (Vector (cSize i1 i2) t)], cRange k i1 i2)
vbrange _ t2 _ _ = Left $ WrongTypeException t2 BitsOrVectorType

-----------------------------------
-- TODO: This code is shared with Check.hs
cRange :: IExpr Var -> IExpr Var -> IExpr Var -> [ICond Var]
cRange s i j = [j .<. s, i .<=. j, IInt 0 .<=. i]
cSize :: IExpr Var -> IExpr Var -> IExpr Var 
cSize i j = evalExpr $ ISum [ j, ISym i, IInt 1 ]
cAccessM :: IExpr Var -> IExpr Var -> Maybe (IExpr Var, IExpr Var) -> [ICond Var]
cAccessM _ _ Nothing = []
cAccessM u v (Just (i, j)) = [IInt 0 .<=. i, i .<. u, IInt 0 .<=. j, j .<. v]
cAccess :: IExpr Var -> Maybe (IExpr Var) -> [ICond Var]
cAccess _ Nothing = []
cAccess k (Just i) = [IInt 0 .<=. i, i .<. k]
----------------------------