cao-0.1: src/Language/CAO/Typechecker/Unification.hs
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-
Module : $Header$
Description : Unification of type when checking expressions.
Copyright : (c) SMART Team / HASLab
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]
----------------------------