{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}

-- | The type checker checks whether the program is type-consistent.
module Futhark.IR.TypeCheck
  ( -- * Interface
    checkProg,
    TypeError (..),
    ErrorCase (..),

    -- * Extensionality
    TypeM,
    bad,
    context,
    Checkable (..),
    CheckableOp (..),
    lookupVar,
    lookupAliases,
    checkOpWith,

    -- * Checkers
    require,
    requireI,
    requirePrimExp,
    checkSubExp,
    checkCerts,
    checkExp,
    checkStms,
    checkStm,
    checkType,
    checkExtType,
    matchExtPat,
    matchExtBranchType,
    argType,
    noArgAliases,
    checkArg,
    checkSOACArrayArgs,
    checkLambda,
    checkBody,
    consume,
    binding,
    alternative,
  )
where

import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Parallel.Strategies
import Data.List (find, intercalate, isPrefixOf, sort)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Analysis.PrimExp
import Futhark.Construct (instantiateShapes)
import Futhark.IR.Aliases hiding (lookupAliases)
import Futhark.Util
import Futhark.Util.Pretty (Pretty, align, indent, ppr, prettyDoc, text, (<+>), (</>))

-- | Information about an error during type checking.  The 'Show'
-- instance for this type produces a human-readable description.
data ErrorCase rep
  = TypeError String
  | UnexpectedType (Exp rep) Type [Type]
  | ReturnTypeError Name [ExtType] [ExtType]
  | DupDefinitionError Name
  | DupParamError Name VName
  | DupPatError VName
  | InvalidPatError (Pat (LetDec (Aliases rep))) [ExtType] (Maybe String)
  | UnknownVariableError VName
  | UnknownFunctionError Name
  | ParameterMismatch (Maybe Name) [Type] [Type]
  | SlicingError Int Int
  | BadAnnotation String Type Type
  | ReturnAliased Name VName
  | UniqueReturnAliased Name
  | NotAnArray VName Type
  | PermutationError [Int] Int (Maybe VName)

instance Checkable rep => Show (ErrorCase rep) where
  show :: ErrorCase rep -> String
show (TypeError String
msg) =
    String
"Type error:\n" forall a. [a] -> [a] -> [a]
++ String
msg
  show (UnexpectedType Exp rep
e Type
_ []) =
    String
"Type of expression\n"
      forall a. [a] -> [a] -> [a]
++ Int -> Doc -> String
prettyDoc Int
160 (Int -> Doc -> Doc
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
ppr Exp rep
e)
      forall a. [a] -> [a] -> [a]
++ String
"\ncannot have any type - possibly a bug in the type checker."
  show (UnexpectedType Exp rep
e Type
t [Type]
ts) =
    String
"Type of expression\n"
      forall a. [a] -> [a] -> [a]
++ Int -> Doc -> String
prettyDoc Int
160 (Int -> Doc -> Doc
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
ppr Exp rep
e)
      forall a. [a] -> [a] -> [a]
++ String
"\nmust be one of "
      forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> String
pretty [Type]
ts)
      forall a. [a] -> [a] -> [a]
++ String
", but is "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
t
      forall a. [a] -> [a] -> [a]
++ String
"."
  show (ReturnTypeError Name
fname [ExtType]
rettype [ExtType]
bodytype) =
    String
"Declaration of function "
      forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      forall a. [a] -> [a] -> [a]
++ String
" declares return type\n  "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple [ExtType]
rettype
      forall a. [a] -> [a] -> [a]
++ String
"\nBut body has type\n  "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple [ExtType]
bodytype
  show (DupDefinitionError Name
name) =
    String
"Duplicate definition of function " forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
name forall a. [a] -> [a] -> [a]
++ String
""
  show (DupParamError Name
funname VName
paramname) =
    String
"Parameter "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
paramname
      forall a. [a] -> [a] -> [a]
++ String
" mentioned multiple times in argument list of function "
      forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
funname
      forall a. [a] -> [a] -> [a]
++ String
"."
  show (DupPatError VName
name) =
    String
"Variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
name forall a. [a] -> [a] -> [a]
++ String
" bound twice in pattern."
  show (InvalidPatError Pat (LetDec (Aliases rep))
pat [ExtType]
t Maybe String
desc) =
    String
"Pat\n"
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Pat (LetDec (Aliases rep))
pat
      forall a. [a] -> [a] -> [a]
++ String
"\ncannot match value of type\n"
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTupleLines [ExtType]
t
      forall a. [a] -> [a] -> [a]
++ String
end
    where
      end :: String
end = case Maybe String
desc of
        Maybe String
Nothing -> String
"."
        Just String
desc' -> String
":\n" forall a. [a] -> [a] -> [a]
++ String
desc'
  show (UnknownVariableError VName
name) =
    String
"Use of unknown variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
name forall a. [a] -> [a] -> [a]
++ String
"."
  show (UnknownFunctionError Name
fname) =
    String
"Call of unknown function " forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname forall a. [a] -> [a] -> [a]
++ String
"."
  show (ParameterMismatch Maybe Name
fname [Type]
expected [Type]
got) =
    String
"In call of "
      forall a. [a] -> [a] -> [a]
++ String
fname'
      forall a. [a] -> [a] -> [a]
++ String
":\n"
      forall a. [a] -> [a] -> [a]
++ String
"expecting "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
nexpected
      forall a. [a] -> [a] -> [a]
++ String
" arguments of type(s)\n"
      forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> String
pretty [Type]
expected)
      forall a. [a] -> [a] -> [a]
++ String
"\nGot "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
ngot
      forall a. [a] -> [a] -> [a]
++ String
" arguments of types\n"
      forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> String
pretty [Type]
got)
    where
      nexpected :: Int
nexpected = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
expected
      ngot :: Int
ngot = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
got
      fname' :: String
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"anonymous function" ((String
"function " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameToString) Maybe Name
fname
  show (SlicingError Int
dims Int
got) =
    forall a. Show a => a -> String
show Int
got forall a. [a] -> [a] -> [a]
++ String
" indices given, but type of indexee has " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
dims forall a. [a] -> [a] -> [a]
++ String
" dimension(s)."
  show (BadAnnotation String
desc Type
expected Type
got) =
    String
"Annotation of \""
      forall a. [a] -> [a] -> [a]
++ String
desc
      forall a. [a] -> [a] -> [a]
++ String
"\" type of expression is "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
expected
      forall a. [a] -> [a] -> [a]
++ String
", but derived to be "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
got
      forall a. [a] -> [a] -> [a]
++ String
"."
  show (ReturnAliased Name
fname VName
name) =
    String
"Unique return value of function "
      forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      forall a. [a] -> [a] -> [a]
++ String
" is aliased to "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
name
      forall a. [a] -> [a] -> [a]
++ String
", which is not consumed."
  show (UniqueReturnAliased Name
fname) =
    String
"A unique tuple element of return value of function "
      forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      forall a. [a] -> [a] -> [a]
++ String
" is aliased to some other tuple component."
  show (NotAnArray VName
e Type
t) =
    String
"The expression "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
e
      forall a. [a] -> [a] -> [a]
++ String
" is expected to be an array, but is "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
t
      forall a. [a] -> [a] -> [a]
++ String
"."
  show (PermutationError [Int]
perm Int
rank Maybe VName
name) =
    String
"The permutation ("
      forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Int]
perm)
      forall a. [a] -> [a] -> [a]
++ String
") is not valid for array "
      forall a. [a] -> [a] -> [a]
++ String
name'
      forall a. [a] -> [a] -> [a]
++ String
"of rank "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
rank
      forall a. [a] -> [a] -> [a]
++ String
"."
    where
      name' :: String
name' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((forall a. [a] -> [a] -> [a]
++ String
" ") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
pretty) Maybe VName
name

-- | A type error.
data TypeError rep = Error [String] (ErrorCase rep)

instance Checkable rep => Show (TypeError rep) where
  show :: TypeError rep -> String
show (Error [] ErrorCase rep
err) =
    forall a. Show a => a -> String
show ErrorCase rep
err
  show (Error [String]
msgs ErrorCase rep
err) =
    forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
msgs forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ErrorCase rep
err

-- | A tuple of a return type and a list of parameters, possibly
-- named.
type FunBinding rep = ([RetType (Aliases rep)], [FParam (Aliases rep)])

type VarBinding rep = NameInfo (Aliases rep)

data Usage
  = Consumed
  | Observed
  deriving (Usage -> Usage -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Usage -> Usage -> Bool
$c/= :: Usage -> Usage -> Bool
== :: Usage -> Usage -> Bool
$c== :: Usage -> Usage -> Bool
Eq, Eq Usage
Usage -> Usage -> Bool
Usage -> Usage -> Ordering
Usage -> Usage -> Usage
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Usage -> Usage -> Usage
$cmin :: Usage -> Usage -> Usage
max :: Usage -> Usage -> Usage
$cmax :: Usage -> Usage -> Usage
>= :: Usage -> Usage -> Bool
$c>= :: Usage -> Usage -> Bool
> :: Usage -> Usage -> Bool
$c> :: Usage -> Usage -> Bool
<= :: Usage -> Usage -> Bool
$c<= :: Usage -> Usage -> Bool
< :: Usage -> Usage -> Bool
$c< :: Usage -> Usage -> Bool
compare :: Usage -> Usage -> Ordering
$ccompare :: Usage -> Usage -> Ordering
Ord, Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> Usage -> ShowS
Show)

data Occurence = Occurence
  { Occurence -> Names
observed :: Names,
    Occurence -> Names
consumed :: Names
  }
  deriving (Occurence -> Occurence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Occurence -> Occurence -> Bool
$c/= :: Occurence -> Occurence -> Bool
== :: Occurence -> Occurence -> Bool
$c== :: Occurence -> Occurence -> Bool
Eq, Int -> Occurence -> ShowS
[Occurence] -> ShowS
Occurence -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Occurence] -> ShowS
$cshowList :: [Occurence] -> ShowS
show :: Occurence -> String
$cshow :: Occurence -> String
showsPrec :: Int -> Occurence -> ShowS
$cshowsPrec :: Int -> Occurence -> ShowS
Show)

observation :: Names -> Occurence
observation :: Names -> Occurence
observation = forall a b c. (a -> b -> c) -> b -> a -> c
flip Names -> Names -> Occurence
Occurence forall a. Monoid a => a
mempty

consumption :: Names -> Occurence
consumption :: Names -> Occurence
consumption = Names -> Names -> Occurence
Occurence forall a. Monoid a => a
mempty

nullOccurence :: Occurence -> Bool
nullOccurence :: Occurence -> Bool
nullOccurence Occurence
occ = Occurence -> Names
observed Occurence
occ forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty Bool -> Bool -> Bool
&& Occurence -> Names
consumed Occurence
occ forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty

type Occurences = [Occurence]

allConsumed :: Occurences -> Names
allConsumed :: [Occurence] -> Names
allConsumed = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
consumed

seqOccurences :: Occurences -> Occurences -> Occurences
seqOccurences :: [Occurence] -> [Occurence] -> [Occurence]
seqOccurences [Occurence]
occurs1 [Occurence]
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) (forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Occurence
filt [Occurence]
occurs1) forall a. [a] -> [a] -> [a]
++ [Occurence]
occurs2
  where
    filt :: Occurence -> Occurence
filt Occurence
occ =
      Occurence
occ {observed :: Names
observed = Occurence -> Names
observed Occurence
occ Names -> Names -> Names
`namesSubtract` Names
postcons}
    postcons :: Names
postcons = [Occurence] -> Names
allConsumed [Occurence]
occurs2

altOccurences :: Occurences -> Occurences -> Occurences
altOccurences :: [Occurence] -> [Occurence] -> [Occurence]
altOccurences [Occurence]
occurs1 [Occurence]
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) (forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Occurence
filt [Occurence]
occurs1) forall a. [a] -> [a] -> [a]
++ [Occurence]
occurs2
  where
    filt :: Occurence -> Occurence
filt Occurence
occ =
      Occurence
occ
        { consumed :: Names
consumed = Occurence -> Names
consumed Occurence
occ Names -> Names -> Names
`namesSubtract` Names
postcons,
          observed :: Names
observed = Occurence -> Names
observed Occurence
occ Names -> Names -> Names
`namesSubtract` Names
postcons
        }
    postcons :: Names
postcons = [Occurence] -> Names
allConsumed [Occurence]
occurs2

unOccur :: Names -> Occurences -> Occurences
unOccur :: Names -> [Occurence] -> [Occurence]
unOccur Names
to_be_removed = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Occurence
unOccur'
  where
    unOccur' :: Occurence -> Occurence
unOccur' Occurence
occ =
      Occurence
occ
        { observed :: Names
observed = Occurence -> Names
observed Occurence
occ Names -> Names -> Names
`namesSubtract` Names
to_be_removed,
          consumed :: Names
consumed = Occurence -> Names
consumed Occurence
occ Names -> Names -> Names
`namesSubtract` Names
to_be_removed
        }

-- | The 'Consumption' data structure is used to keep track of which
-- variables have been consumed, as well as whether a violation has been detected.
data Consumption
  = ConsumptionError String
  | Consumption Occurences
  deriving (Int -> Consumption -> ShowS
[Consumption] -> ShowS
Consumption -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Consumption] -> ShowS
$cshowList :: [Consumption] -> ShowS
show :: Consumption -> String
$cshow :: Consumption -> String
showsPrec :: Int -> Consumption -> ShowS
$cshowsPrec :: Int -> Consumption -> ShowS
Show)

instance Semigroup Consumption where
  ConsumptionError String
e <> :: Consumption -> Consumption -> Consumption
<> Consumption
_ = String -> Consumption
ConsumptionError String
e
  Consumption
_ <> ConsumptionError String
e = String -> Consumption
ConsumptionError String
e
  Consumption [Occurence]
o1 <> Consumption [Occurence]
o2
    | VName
v : [VName]
_ <- Names -> [VName]
namesToList forall a b. (a -> b) -> a -> b
$ Names
consumed_in_o1 Names -> Names -> Names
`namesIntersection` Names
used_in_o2 =
        String -> Consumption
ConsumptionError forall a b. (a -> b) -> a -> b
$ String
"Variable " forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> String
pretty VName
v forall a. Semigroup a => a -> a -> a
<> String
" referenced after being consumed."
    | Bool
otherwise =
        [Occurence] -> Consumption
Consumption forall a b. (a -> b) -> a -> b
$ [Occurence]
o1 [Occurence] -> [Occurence] -> [Occurence]
`seqOccurences` [Occurence]
o2
    where
      consumed_in_o1 :: Names
consumed_in_o1 = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
consumed [Occurence]
o1
      used_in_o2 :: Names
used_in_o2 = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
consumed [Occurence]
o2 forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
observed [Occurence]
o2

instance Monoid Consumption where
  mempty :: Consumption
mempty = [Occurence] -> Consumption
Consumption forall a. Monoid a => a
mempty

-- | The environment contains a variable table and a function table.
-- Type checking happens with access to this environment.  The
-- function table is only initialised at the very beginning, but the
-- variable table will be extended during type-checking when
-- let-expressions are encountered.
data Env rep = Env
  { forall rep. Env rep -> Map VName (VarBinding rep)
envVtable :: M.Map VName (VarBinding rep),
    forall rep. Env rep -> Map Name (FunBinding rep)
envFtable :: M.Map Name (FunBinding rep),
    forall rep. Env rep -> OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp :: OpWithAliases (Op rep) -> TypeM rep (),
    forall rep. Env rep -> [String]
envContext :: [String]
  }

data TState = TState
  { TState -> Names
stateNames :: Names,
    TState -> Consumption
stateCons :: Consumption
  }

-- | The type checker runs in this monad.
newtype TypeM rep a
  = TypeM (ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a)
  deriving
    ( forall {rep}. Applicative (TypeM rep)
forall a. a -> TypeM rep a
forall rep a. a -> TypeM rep a
forall a b. TypeM rep a -> TypeM rep b -> TypeM rep b
forall a b. TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b
forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep b
forall rep a b. TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TypeM rep a
$creturn :: forall rep a. a -> TypeM rep a
>> :: forall a b. TypeM rep a -> TypeM rep b -> TypeM rep b
$c>> :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep b
>>= :: forall a b. TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b
$c>>= :: forall rep a b. TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b
Monad,
      forall a b. a -> TypeM rep b -> TypeM rep a
forall a b. (a -> b) -> TypeM rep a -> TypeM rep b
forall rep a b. a -> TypeM rep b -> TypeM rep a
forall rep a b. (a -> b) -> TypeM rep a -> TypeM rep b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TypeM rep b -> TypeM rep a
$c<$ :: forall rep a b. a -> TypeM rep b -> TypeM rep a
fmap :: forall a b. (a -> b) -> TypeM rep a -> TypeM rep b
$cfmap :: forall rep a b. (a -> b) -> TypeM rep a -> TypeM rep b
Functor,
      forall rep. Functor (TypeM rep)
forall a. a -> TypeM rep a
forall rep a. a -> TypeM rep a
forall a b. TypeM rep a -> TypeM rep b -> TypeM rep a
forall a b. TypeM rep a -> TypeM rep b -> TypeM rep b
forall a b. TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b
forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep a
forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep b
forall rep a b. TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b
forall a b c.
(a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c
forall rep a b c.
(a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TypeM rep a -> TypeM rep b -> TypeM rep a
$c<* :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep a
*> :: forall a b. TypeM rep a -> TypeM rep b -> TypeM rep b
$c*> :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep b
liftA2 :: forall a b c.
(a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c
$cliftA2 :: forall rep a b c.
(a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c
<*> :: forall a b. TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b
$c<*> :: forall rep a b. TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b
pure :: forall a. a -> TypeM rep a
$cpure :: forall rep a. a -> TypeM rep a
Applicative,
      MonadReader (Env rep),
      MonadState TState
    )

instance
  Checkable rep =>
  HasScope (Aliases rep) (TypeM rep)
  where
  lookupType :: VName -> TypeM rep Type
lookupType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. Typed t => t -> Type
typeOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar
  askScope :: TypeM rep (Scope (Aliases rep))
askScope = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a} {b}. (a, b) -> Maybe (a, b)
varType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. Env rep -> Map VName (VarBinding rep)
envVtable
    where
      varType :: (a, b) -> Maybe (a, b)
varType (a
name, b
dec) = forall a. a -> Maybe a
Just (a
name, b
dec)

runTypeM ::
  Env rep ->
  TypeM rep a ->
  Either (TypeError rep) a
runTypeM :: forall rep a. Env rep -> TypeM rep a -> Either (TypeError rep) a
runTypeM Env rep
env (TypeM ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a
m) =
  forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a
m Env rep
env) (Names -> Consumption -> TState
TState forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)

-- | Signal a type error.
bad :: ErrorCase rep -> TypeM rep a
bad :: forall rep a. ErrorCase rep -> TypeM rep a
bad ErrorCase rep
e = do
  [String]
messages <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall rep. Env rep -> [String]
envContext
  forall rep a.
ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a
-> TypeM rep a
TypeM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall rep. [String] -> ErrorCase rep -> TypeError rep
Error (forall a. [a] -> [a]
reverse [String]
messages) ErrorCase rep
e

tell :: Consumption -> TypeM rep ()
tell :: forall rep. Consumption -> TypeM rep ()
tell Consumption
cons = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = TState -> Consumption
stateCons TState
s forall a. Semigroup a => a -> a -> a
<> Consumption
cons}

-- | Add information about what is being type-checked to the current
-- context.  Liberal use of this combinator makes it easier to track
-- type errors, as the strings are added to type errors signalled via
-- 'bad'.
context ::
  String ->
  TypeM rep a ->
  TypeM rep a
context :: forall rep a. String -> TypeM rep a -> TypeM rep a
context String
s = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \Env rep
env -> Env rep
env {envContext :: [String]
envContext = String
s forall a. a -> [a] -> [a]
: forall rep. Env rep -> [String]
envContext Env rep
env}

message ::
  Pretty a =>
  String ->
  a ->
  String
message :: forall a. Pretty a => String -> a -> String
message String
s a
x =
  Int -> Doc -> String
prettyDoc Int
80 forall a b. (a -> b) -> a -> b
$
    String -> Doc
text String
s Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr a
x)

-- | Mark a name as bound.  If the name has been bound previously in
-- the program, report a type error.
bound :: VName -> TypeM rep ()
bound :: forall rep. VName -> TypeM rep ()
bound VName
name = do
  Bool
already_seen <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ VName -> Names -> Bool
nameIn VName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. TState -> Names
stateNames
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
already_seen forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        String
"Name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
name forall a. [a] -> [a] -> [a]
++ String
" bound twice"
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateNames :: Names
stateNames = VName -> Names
oneName VName
name forall a. Semigroup a => a -> a -> a
<> TState -> Names
stateNames TState
s}

occur :: Occurences -> TypeM rep ()
occur :: forall rep. [Occurence] -> TypeM rep ()
occur = forall rep. Consumption -> TypeM rep ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Occurence] -> Consumption
Consumption forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence)

-- | Proclaim that we have made read-only use of the given variable.
-- No-op unless the variable is array-typed.
observe ::
  Checkable rep =>
  VName ->
  TypeM rep ()
observe :: forall rep. Checkable rep => VName -> TypeM rep ()
observe VName
name = do
  NameInfo (Aliases rep)
dec <- forall rep. VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar VName
name
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall shape u. TypeBase shape u -> Bool
primType forall a b. (a -> b) -> a -> b
$ forall t. Typed t => t -> Type
typeOf NameInfo (Aliases rep)
dec) forall a b. (a -> b) -> a -> b
$
    forall rep. [Occurence] -> TypeM rep ()
occur [Names -> Occurence
observation forall a b. (a -> b) -> a -> b
$ VName -> Names
oneName VName
name forall a. Semigroup a => a -> a -> a
<> forall rep. NameInfo (Aliases rep) -> Names
aliases NameInfo (Aliases rep)
dec]

-- | Proclaim that we have written to the given variables.
consume :: Checkable rep => Names -> TypeM rep ()
consume :: forall rep. Checkable rep => Names -> TypeM rep ()
consume Names
als = do
  Scope (Aliases rep)
scope <- forall rep (m :: * -> *). HasScope rep m => m (Scope rep)
askScope
  let isArray :: VName -> Bool
isArray = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall shape u. TypeBase shape u -> Bool
primType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Typed t => t -> Type
typeOf) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Scope (Aliases rep)
scope)
  forall rep. [Occurence] -> TypeM rep ()
occur [Names -> Occurence
consumption forall a b. (a -> b) -> a -> b
$ [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
isArray forall a b. (a -> b) -> a -> b
$ Names -> [VName]
namesToList Names
als]

collectOccurences :: TypeM rep a -> TypeM rep (a, Occurences)
collectOccurences :: forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m = do
  Consumption
old <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TState -> Consumption
stateCons
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = forall a. Monoid a => a
mempty}
  a
x <- TypeM rep a
m
  Consumption
new <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TState -> Consumption
stateCons
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = Consumption
old}
  [Occurence]
o <- forall rep. Consumption -> TypeM rep [Occurence]
checkConsumption Consumption
new
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, [Occurence]
o)

checkOpWith ::
  (OpWithAliases (Op rep) -> TypeM rep ()) ->
  TypeM rep a ->
  TypeM rep a
checkOpWith :: forall rep a.
(OpWithAliases (Op rep) -> TypeM rep ())
-> TypeM rep a -> TypeM rep a
checkOpWith OpWithAliases (Op rep) -> TypeM rep ()
checker = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \Env rep
env -> Env rep
env {envCheckOp :: OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp = OpWithAliases (Op rep) -> TypeM rep ()
checker}

checkConsumption :: Consumption -> TypeM rep Occurences
checkConsumption :: forall rep. Consumption -> TypeM rep [Occurence]
checkConsumption (ConsumptionError String
e) = forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. String -> ErrorCase rep
TypeError String
e
checkConsumption (Consumption [Occurence]
os) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [Occurence]
os

-- | Type check two mutually control flow branches.  Think @if@.  This
-- interacts with consumption checking, as it is OK for an array to be
-- consumed in both branches.
alternative :: TypeM rep a -> TypeM rep b -> TypeM rep (a, b)
alternative :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep (a, b)
alternative TypeM rep a
m1 TypeM rep b
m2 = do
  (a
x, [Occurence]
os1) <- forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m1
  (b
y, [Occurence]
os2) <- forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep b
m2
  forall rep. Consumption -> TypeM rep ()
tell forall a b. (a -> b) -> a -> b
$ [Occurence] -> Consumption
Consumption forall a b. (a -> b) -> a -> b
$ [Occurence]
os1 [Occurence] -> [Occurence] -> [Occurence]
`altOccurences` [Occurence]
os2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, b
y)

-- | Permit consumption of only the specified names.  If one of these
-- names is consumed, the consumption will be rewritten to be a
-- consumption of the corresponding alias set.  Consumption of
-- anything else will result in a type error.
consumeOnlyParams :: [(VName, Names)] -> TypeM rep a -> TypeM rep a
consumeOnlyParams :: forall rep a. [(VName, Names)] -> TypeM rep a -> TypeM rep a
consumeOnlyParams [(VName, Names)]
consumable TypeM rep a
m = do
  (a
x, [Occurence]
os) <- forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m
  forall rep. Consumption -> TypeM rep ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Occurence] -> Consumption
Consumption forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Occurence -> TypeM rep Occurence
inspect [Occurence]
os
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  where
    inspect :: Occurence -> TypeM rep Occurence
inspect Occurence
o = do
      Names
new_consumed <- forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TypeM rep Names
wasConsumed (Names -> [VName]
namesToList forall a b. (a -> b) -> a -> b
$ Occurence -> Names
consumed Occurence
o)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Occurence
o {consumed :: Names
consumed = Names
new_consumed}
    wasConsumed :: VName -> TypeM rep Names
wasConsumed VName
v
      | Just Names
als <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v [(VName, Names)]
consumable = forall (f :: * -> *) a. Applicative f => a -> f a
pure Names
als
      | Bool
otherwise =
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
            [ forall a. Pretty a => a -> String
pretty VName
v forall a. [a] -> [a] -> [a]
++ String
" was invalidly consumed.",
              String
what forall a. [a] -> [a] -> [a]
++ String
" can be consumed here."
            ]
    what :: String
what
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(VName, Names)]
consumable = String
"Nothing"
      | Bool
otherwise = String
"Only " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => a -> String
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(VName, Names)]
consumable)

-- | Given the immediate aliases, compute the full transitive alias
-- set (including the immediate aliases).
expandAliases :: Names -> Env rep -> Names
expandAliases :: forall rep. Names -> Env rep -> Names
expandAliases Names
names Env rep
env = Names
names forall a. Semigroup a => a -> a -> a
<> Names
aliasesOfAliases
  where
    aliasesOfAliases :: Names
aliasesOfAliases = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map VName -> Names
look forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> [VName]
namesToList forall a b. (a -> b) -> a -> b
$ Names
names
    look :: VName -> Names
look VName
k = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k forall a b. (a -> b) -> a -> b
$ forall rep. Env rep -> Map VName (VarBinding rep)
envVtable Env rep
env of
      Just (LetName (VarAliases
als, LetDec rep
_)) -> VarAliases -> Names
unAliases VarAliases
als
      Maybe (VarBinding rep)
_ -> forall a. Monoid a => a
mempty

binding ::
  Checkable rep =>
  Scope (Aliases rep) ->
  TypeM rep a ->
  TypeM rep a
binding :: forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding Scope (Aliases rep)
stms = TypeM rep a -> TypeM rep a
check forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Env rep -> Scope (Aliases rep) -> Env rep
`bindVars` Scope (Aliases rep)
stms)
  where
    bindVars :: Env rep -> Scope (Aliases rep) -> Env rep
bindVars = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
M.foldlWithKey' forall {rep}.
Typed (LetDec rep) =>
Env rep -> VName -> NameInfo (Aliases rep) -> Env rep
bindVar
    boundnames :: [VName]
boundnames = forall k a. Map k a -> [k]
M.keys Scope (Aliases rep)
stms

    bindVar :: Env rep -> VName -> NameInfo (Aliases rep) -> Env rep
bindVar Env rep
env VName
name (LetName (AliasDec Names
als, LetDec rep
dec)) =
      let als' :: Names
als'
            | forall shape u. TypeBase shape u -> Bool
primType (forall t. Typed t => t -> Type
typeOf LetDec rep
dec) = forall a. Monoid a => a
mempty
            | Bool
otherwise = forall rep. Names -> Env rep -> Names
expandAliases Names
als Env rep
env
       in Env rep
env
            { envVtable :: Map VName (NameInfo (Aliases rep))
envVtable =
                forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name (forall rep. LetDec rep -> NameInfo rep
LetName (Names -> VarAliases
AliasDec Names
als', LetDec rep
dec)) forall a b. (a -> b) -> a -> b
$ forall rep. Env rep -> Map VName (VarBinding rep)
envVtable Env rep
env
            }
    bindVar Env rep
env VName
name NameInfo (Aliases rep)
dec =
      Env rep
env {envVtable :: Map VName (NameInfo (Aliases rep))
envVtable = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name NameInfo (Aliases rep)
dec forall a b. (a -> b) -> a -> b
$ forall rep. Env rep -> Map VName (VarBinding rep)
envVtable Env rep
env}

    -- Check whether the bound variables have been used correctly
    -- within their scope.
    check :: TypeM rep a -> TypeM rep a
check TypeM rep a
m = do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. VName -> TypeM rep ()
bound forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Scope (Aliases rep)
stms
      (a
a, [Occurence]
os) <- forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m
      forall rep. Consumption -> TypeM rep ()
tell forall a b. (a -> b) -> a -> b
$ [Occurence] -> Consumption
Consumption forall a b. (a -> b) -> a -> b
$ Names -> [Occurence] -> [Occurence]
unOccur ([VName] -> Names
namesFromList [VName]
boundnames) [Occurence]
os
      forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

lookupVar :: VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar :: forall rep. VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar VName
name = do
  Maybe (NameInfo (Aliases rep))
stm <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. Env rep -> Map VName (VarBinding rep)
envVtable
  case Maybe (NameInfo (Aliases rep))
stm of
    Maybe (NameInfo (Aliases rep))
Nothing -> forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. VName -> ErrorCase rep
UnknownVariableError VName
name
    Just NameInfo (Aliases rep)
dec -> forall (f :: * -> *) a. Applicative f => a -> f a
pure NameInfo (Aliases rep)
dec

lookupAliases :: Checkable rep => VName -> TypeM rep Names
lookupAliases :: forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
name = do
  NameInfo (Aliases rep)
info <- forall rep. VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar VName
name
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    if forall shape u. TypeBase shape u -> Bool
primType forall a b. (a -> b) -> a -> b
$ forall t. Typed t => t -> Type
typeOf NameInfo (Aliases rep)
info
      then forall a. Monoid a => a
mempty
      else VName -> Names
oneName VName
name forall a. Semigroup a => a -> a -> a
<> forall rep. NameInfo (Aliases rep) -> Names
aliases NameInfo (Aliases rep)
info

aliases :: NameInfo (Aliases rep) -> Names
aliases :: forall rep. NameInfo (Aliases rep) -> Names
aliases (LetName (VarAliases
als, LetDec rep
_)) = VarAliases -> Names
unAliases VarAliases
als
aliases NameInfo (Aliases rep)
_ = forall a. Monoid a => a
mempty

subExpAliasesM :: Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM :: forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM Constant {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
subExpAliasesM (Var VName
v) = forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
v

lookupFun ::
  Checkable rep =>
  Name ->
  [SubExp] ->
  TypeM rep ([RetType rep], [DeclType])
lookupFun :: forall rep.
Checkable rep =>
Name -> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
lookupFun Name
fname [SubExp]
args = do
  Maybe ([RetType rep], [Param (FParamInfo rep)])
stm <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
fname forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. Env rep -> Map Name (FunBinding rep)
envFtable
  case Maybe ([RetType rep], [Param (FParamInfo rep)])
stm of
    Maybe ([RetType rep], [Param (FParamInfo rep)])
Nothing -> forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Name -> ErrorCase rep
UnknownFunctionError Name
fname
    Just ([RetType rep]
ftype, [Param (FParamInfo rep)]
params) -> do
      [Type]
argts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t (m :: * -> *). HasScope t m => SubExp -> m Type
subExpType [SubExp]
args
      case forall rt dec.
(IsRetType rt, Typed dec) =>
[rt] -> [Param dec] -> [(SubExp, Type)] -> Maybe [rt]
applyRetType [RetType rep]
ftype [Param (FParamInfo rep)]
params forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [SubExp]
args [Type]
argts of
        Maybe [RetType rep]
Nothing ->
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Maybe Name -> [Type] -> [Type] -> ErrorCase rep
ParameterMismatch (forall a. a -> Maybe a
Just Name
fname) (forall a b. (a -> b) -> [a] -> [b]
map forall dec. Typed dec => Param dec -> Type
paramType [Param (FParamInfo rep)]
params) [Type]
argts
        Just [RetType rep]
rt ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ([RetType rep]
rt, forall a b. (a -> b) -> [a] -> [b]
map forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo rep)]
params)

-- | @checkAnnotation loc s t1 t2@ checks if @t2@ is equal to
-- @t1@.  If not, a 'BadAnnotation' is raised.
checkAnnotation ::
  String ->
  Type ->
  Type ->
  TypeM rep ()
checkAnnotation :: forall rep. String -> Type -> Type -> TypeM rep ()
checkAnnotation String
desc Type
t1 Type
t2
  | Type
t2 forall a. Eq a => a -> a -> Bool
== Type
t1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise = forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. String -> Type -> Type -> ErrorCase rep
BadAnnotation String
desc Type
t1 Type
t2

-- | @require ts se@ causes a '(TypeError vn)' if the type of @se@ is
-- not a subtype of one of the types in @ts@.
require :: Checkable rep => [Type] -> SubExp -> TypeM rep ()
require :: forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [Type]
ts SubExp
se = do
  Type
t <- forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
se
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
ts) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Exp rep -> Type -> [Type] -> ErrorCase rep
UnexpectedType (forall rep. BasicOp -> Exp rep
BasicOp forall a b. (a -> b) -> a -> b
$ SubExp -> BasicOp
SubExp SubExp
se) Type
t [Type]
ts

-- | Variant of 'require' working on variable names.
requireI :: Checkable rep => [Type] -> VName -> TypeM rep ()
requireI :: forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [Type]
ts VName
ident = forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [Type]
ts forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
ident

checkArrIdent ::
  Checkable rep =>
  VName ->
  TypeM rep (Shape, PrimType)
checkArrIdent :: forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
v = do
  Type
t <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
v
  case Type
t of
    Array PrimType
pt Shape
shape NoUniqueness
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Shape
shape, PrimType
pt)
    Type
_ -> forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. VName -> Type -> ErrorCase rep
NotAnArray VName
v Type
t

checkAccIdent ::
  Checkable rep =>
  VName ->
  TypeM rep (Shape, [Type])
checkAccIdent :: forall rep. Checkable rep => VName -> TypeM rep (Shape, [Type])
checkAccIdent VName
v = do
  Type
t <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
v
  case Type
t of
    Acc VName
_ Shape
ispace [Type]
ts NoUniqueness
_ ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Shape
ispace, [Type]
ts)
    Type
_ ->
      forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        forall a. Pretty a => a -> String
pretty VName
v
          forall a. [a] -> [a] -> [a]
++ String
" should be an accumulator but is of type "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
t

checkOpaques :: OpaqueTypes -> Either (TypeError rep) ()
checkOpaques :: forall rep. OpaqueTypes -> Either (TypeError rep) ()
checkOpaques (OpaqueTypes [(String, OpaqueType)]
types) = forall {rep}.
[String] -> [(String, OpaqueType)] -> Either (TypeError rep) ()
descend [] [(String, OpaqueType)]
types
  where
    descend :: [String] -> [(String, OpaqueType)] -> Either (TypeError rep) ()
descend [String]
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    descend [String]
known ((String
name, OpaqueType
t) : [(String, OpaqueType)]
ts) = do
      forall {t :: * -> *} {rep}.
Foldable t =>
t String -> OpaqueType -> Either (TypeError rep) ()
check [String]
known OpaqueType
t
      [String] -> [(String, OpaqueType)] -> Either (TypeError rep) ()
descend (String
name forall a. a -> [a] -> [a]
: [String]
known) [(String, OpaqueType)]
ts
    check :: t String -> OpaqueType -> Either (TypeError rep) ()
check t String
known (OpaqueRecord [(Name, EntryPointType)]
fs) =
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {t :: * -> *} {rep}.
Foldable t =>
t String -> EntryPointType -> Either (TypeError rep) ()
checkEntryPointType t String
known forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Name, EntryPointType)]
fs
    check t String
_ (OpaqueType [ValueType]
_) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkEntryPointType :: t String -> EntryPointType -> Either (TypeError rep) ()
checkEntryPointType t String
known (TypeOpaque String
s) =
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t String
known) forall a b. (a -> b) -> a -> b
$
        forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. [String] -> ErrorCase rep -> TypeError rep
Error [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
          String
"Opaque not defined before first use: " forall a. Semigroup a => a -> a -> a
<> String
s
    checkEntryPointType t String
_ (TypeTransparent ValueType
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Type check a program containing arbitrary type information,
-- yielding either a type error or a program with complete type
-- information.
checkProg ::
  Checkable rep =>
  Prog (Aliases rep) ->
  Either (TypeError rep) ()
checkProg :: forall rep.
Checkable rep =>
Prog (Aliases rep) -> Either (TypeError rep) ()
checkProg (Prog OpaqueTypes
opaques Stms (Aliases rep)
consts [FunDef (Aliases rep)]
funs) = do
  forall rep. OpaqueTypes -> Either (TypeError rep) ()
checkOpaques OpaqueTypes
opaques
  let typeenv :: Env rep
typeenv =
        Env
          { envVtable :: Map VName (VarBinding rep)
envVtable = forall k a. Map k a
M.empty,
            envFtable :: Map Name (FunBinding rep)
envFtable = forall a. Monoid a => a
mempty,
            envContext :: [String]
envContext = [],
            envCheckOp :: OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp = forall rep.
CheckableOp rep =>
OpWithAliases (Op rep) -> TypeM rep ()
checkOp
          }
  let const_names :: [VName]
const_names = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall dec. Pat dec -> [VName]
patNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. Stm rep -> Pat (LetDec rep)
stmPat) Stms (Aliases rep)
consts
      onFunction :: Map Name ([RetType rep], [Param (FParamInfo rep)])
-> Map VName (VarBinding rep)
-> FunDef (Aliases rep)
-> Either (TypeError rep) ()
onFunction Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable Map VName (VarBinding rep)
vtable FunDef (Aliases rep)
fun = forall rep a. Env rep -> TypeM rep a -> Either (TypeError rep) a
runTypeM Env rep
typeenv forall a b. (a -> b) -> a -> b
$ do
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateNames :: Names
stateNames = [VName] -> Names
namesFromList [VName]
const_names}
        forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env rep
env -> Env rep
env {envFtable :: Map Name (FunBinding rep)
envFtable = Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable, envVtable :: Map VName (VarBinding rep)
envVtable = Map VName (VarBinding rep)
vtable}) forall a b. (a -> b) -> a -> b
$
          forall rep. Checkable rep => FunDef (Aliases rep) -> TypeM rep ()
checkFun FunDef (Aliases rep)
fun
  Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable <-
    forall rep a. Env rep -> TypeM rep a -> Either (TypeError rep) a
runTypeM Env rep
typeenv TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
buildFtable
  Map VName (VarBinding rep)
vtable <-
    forall rep a. Env rep -> TypeM rep a -> Either (TypeError rep) a
runTypeM Env rep
typeenv {envFtable :: Map Name (FunBinding rep)
envFtable = Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable} forall a b. (a -> b) -> a -> b
$ forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
consts forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall rep. Env rep -> Map VName (VarBinding rep)
envVtable
  forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap forall a. Strategy a
rpar (Map Name ([RetType rep], [Param (FParamInfo rep)])
-> Map VName (VarBinding rep)
-> FunDef (Aliases rep)
-> Either (TypeError rep) ()
onFunction Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable Map VName (VarBinding rep)
vtable) [FunDef (Aliases rep)]
funs
  where
    buildFtable :: TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
buildFtable = do
      Map Name ([RetType rep], [Param (FParamInfo rep)])
table <- forall rep. Checkable rep => TypeM rep (Map Name (FunBinding rep))
initialFtable
      forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {rep} {rep}.
Map Name ([RetType rep], [Param (FParamInfo rep)])
-> FunDef rep
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
expand Map Name ([RetType rep], [Param (FParamInfo rep)])
table [FunDef (Aliases rep)]
funs
    expand :: Map Name ([RetType rep], [Param (FParamInfo rep)])
-> FunDef rep
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
expand Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable (FunDef Maybe EntryPoint
_ Attrs
_ Name
name [RetType rep]
ret [Param (FParamInfo rep)]
params Body rep
_)
      | forall k a. Ord k => k -> Map k a -> Bool
M.member Name
name Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable =
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Name -> ErrorCase rep
DupDefinitionError Name
name
      | Bool
otherwise =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
name ([RetType rep]
ret, [Param (FParamInfo rep)]
params) Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable

initialFtable ::
  Checkable rep =>
  TypeM rep (M.Map Name (FunBinding rep))
initialFtable :: forall rep. Checkable rep => TypeM rep (Map Name (FunBinding rep))
initialFtable = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t :: * -> *} {rep} {a} {a}.
(Traversable t, Checkable rep, IsRetType a) =>
(a, (PrimType, t PrimType))
-> TypeM rep (a, ([a], t (Param (FParamInfo rep))))
addBuiltin forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map Name (PrimType, [PrimType])
builtInFunctions
  where
    addBuiltin :: (a, (PrimType, t PrimType))
-> TypeM rep (a, ([a], t (Param (FParamInfo rep))))
addBuiltin (a
fname, (PrimType
t, t PrimType
ts)) = do
      t (Param (FParamInfo rep))
ps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep.
Checkable rep =>
VName -> PrimType -> TypeM rep (FParam (Aliases rep))
primFParam VName
name) t PrimType
ts
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
fname, ([forall rt. IsRetType rt => PrimType -> rt
primRetType PrimType
t], t (Param (FParamInfo rep))
ps))
    name :: VName
name = Name -> Int -> VName
VName (String -> Name
nameFromString String
"x") Int
0

checkFun ::
  Checkable rep =>
  FunDef (Aliases rep) ->
  TypeM rep ()
checkFun :: forall rep. Checkable rep => FunDef (Aliases rep) -> TypeM rep ()
checkFun (FunDef Maybe EntryPoint
_ Attrs
_ Name
fname [RetType (Aliases rep)]
rettype [FParam (Aliases rep)]
params Body (Aliases rep)
body) =
  forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"In function " forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname)
    forall a b. (a -> b) -> a -> b
$ forall rep.
Checkable rep =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
checkFun'
      ( Name
fname,
        forall a b. (a -> b) -> [a] -> [b]
map forall t. DeclExtTyped t => t -> DeclExtType
declExtTypeOf [RetType (Aliases rep)]
rettype,
        forall rep. [FParam rep] -> [(VName, NameInfo (Aliases rep))]
funParamsToNameInfos [FParam (Aliases rep)]
params
      )
      (forall a. a -> Maybe a
Just [(VName, Names)]
consumable)
    forall a b. (a -> b) -> a -> b
$ do
      forall rep. Checkable rep => [FParam rep] -> TypeM rep ()
checkFunParams [FParam (Aliases rep)]
params
      forall rep. Checkable rep => [RetType rep] -> TypeM rep ()
checkRetType [RetType (Aliases rep)]
rettype
      forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking function body" forall a b. (a -> b) -> a -> b
$ forall rep.
Checkable rep =>
[RetType rep] -> Body (Aliases rep) -> TypeM rep [Names]
checkFunBody [RetType (Aliases rep)]
rettype Body (Aliases rep)
body
  where
    consumable :: [(VName, Names)]
consumable =
      [ (forall dec. Param dec -> VName
paramName Param (FParamInfo rep)
param, forall a. Monoid a => a
mempty)
        | Param (FParamInfo rep)
param <- [FParam (Aliases rep)]
params,
          forall shape. TypeBase shape Uniqueness -> Bool
unique forall a b. (a -> b) -> a -> b
$ forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType Param (FParamInfo rep)
param
      ]

funParamsToNameInfos ::
  [FParam rep] ->
  [(VName, NameInfo (Aliases rep))]
funParamsToNameInfos :: forall rep. [FParam rep] -> [(VName, NameInfo (Aliases rep))]
funParamsToNameInfos = forall a b. (a -> b) -> [a] -> [b]
map forall {rep}. Param (FParamInfo rep) -> (VName, NameInfo rep)
nameTypeAndDec
  where
    nameTypeAndDec :: Param (FParamInfo rep) -> (VName, NameInfo rep)
nameTypeAndDec Param (FParamInfo rep)
fparam =
      ( forall dec. Param dec -> VName
paramName Param (FParamInfo rep)
fparam,
        forall rep. FParamInfo rep -> NameInfo rep
FParamName forall a b. (a -> b) -> a -> b
$ forall dec. Param dec -> dec
paramDec Param (FParamInfo rep)
fparam
      )

checkFunParams ::
  Checkable rep =>
  [FParam rep] ->
  TypeM rep ()
checkFunParams :: forall rep. Checkable rep => [FParam rep] -> TypeM rep ()
checkFunParams = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a b. (a -> b) -> a -> b
$ \Param (FParamInfo rep)
param ->
  forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"In function parameter " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Param (FParamInfo rep)
param) forall a b. (a -> b) -> a -> b
$
    forall rep.
Checkable rep =>
VName -> FParamInfo rep -> TypeM rep ()
checkFParamDec (forall dec. Param dec -> VName
paramName Param (FParamInfo rep)
param) (forall dec. Param dec -> dec
paramDec Param (FParamInfo rep)
param)

checkLambdaParams ::
  Checkable rep =>
  [LParam rep] ->
  TypeM rep ()
checkLambdaParams :: forall rep. Checkable rep => [LParam rep] -> TypeM rep ()
checkLambdaParams = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a b. (a -> b) -> a -> b
$ \Param (LParamInfo rep)
param ->
  forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"In lambda parameter " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Param (LParamInfo rep)
param) forall a b. (a -> b) -> a -> b
$
    forall rep.
Checkable rep =>
VName -> LParamInfo rep -> TypeM rep ()
checkLParamDec (forall dec. Param dec -> VName
paramName Param (LParamInfo rep)
param) (forall dec. Param dec -> dec
paramDec Param (LParamInfo rep)
param)

checkFun' ::
  Checkable rep =>
  ( Name,
    [DeclExtType],
    [(VName, NameInfo (Aliases rep))]
  ) ->
  Maybe [(VName, Names)] ->
  TypeM rep [Names] ->
  TypeM rep ()
checkFun' :: forall rep.
Checkable rep =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
checkFun' (Name
fname, [DeclExtType]
rettype, [(VName, NameInfo (Aliases rep))]
params) Maybe [(VName, Names)]
consumable TypeM rep [Names]
check = do
  TypeM rep ()
checkNoDuplicateParams
  forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, NameInfo (Aliases rep))]
params) forall a b. (a -> b) -> a -> b
$
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall rep a. [(VName, Names)] -> TypeM rep a -> TypeM rep a
consumeOnlyParams Maybe [(VName, Names)]
consumable forall a b. (a -> b) -> a -> b
$ do
      [Names]
body_aliases <- TypeM rep [Names]
check
      Scope (Aliases rep)
scope <- forall rep (m :: * -> *). HasScope rep m => m (Scope rep)
askScope
      let isArray :: VName -> Bool
isArray = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. Ord a => a -> a -> Bool
> Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Typed t => t -> Type
typeOf) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Scope (Aliases rep)
scope)
      forall rep a. String -> TypeM rep a -> TypeM rep a
context
        ( String
"When checking the body aliases: "
            forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty (forall a b. (a -> b) -> [a] -> [b]
map Names -> [VName]
namesToList [Names]
body_aliases)
        )
        forall a b. (a -> b) -> a -> b
$ [Names] -> TypeM rep ()
checkReturnAlias
        forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([VName] -> Names
namesFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
isArray forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> [VName]
namesToList) [Names]
body_aliases
  where
    param_names :: [VName]
param_names = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(VName, NameInfo (Aliases rep))]
params

    checkNoDuplicateParams :: TypeM rep ()
checkNoDuplicateParams = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ [VName] -> VName -> TypeM rep [VName]
expand [] [VName]
param_names

    expand :: [VName] -> VName -> TypeM rep [VName]
expand [VName]
seen VName
pname
      | Just VName
_ <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall a. Eq a => a -> a -> Bool
== VName
pname) [VName]
seen =
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Name -> VName -> ErrorCase rep
DupParamError Name
fname VName
pname
      | Bool
otherwise =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ VName
pname forall a. a -> [a] -> [a]
: [VName]
seen
    checkReturnAlias :: [Names] -> TypeM rep ()
checkReturnAlias =
      forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ Set (VName, Uniqueness)
-> (Uniqueness, Names) -> TypeM rep (Set (VName, Uniqueness))
checkReturnAlias' forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {shape} {b}.
[TypeBase shape Uniqueness] -> [b] -> [(Uniqueness, b)]
returnAliasing [DeclExtType]
rettype

    checkReturnAlias' :: Set (VName, Uniqueness)
-> (Uniqueness, Names) -> TypeM rep (Set (VName, Uniqueness))
checkReturnAlias' Set (VName, Uniqueness)
seen (Uniqueness
Unique, Names
names)
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map forall a b. (a, b) -> a
fst Set (VName, Uniqueness)
seen) forall a b. (a -> b) -> a -> b
$ Names -> [VName]
namesToList Names
names =
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Name -> ErrorCase rep
UniqueReturnAliased Name
fname
      | Bool
otherwise = do
          forall rep. Checkable rep => Names -> TypeM rep ()
consume Names
names
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set (VName, Uniqueness)
seen forall a. Semigroup a => a -> a -> a
<> forall {t}. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Unique Names
names
    checkReturnAlias' Set (VName, Uniqueness)
seen (Uniqueness
Nonunique, Names
names)
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` Set (VName, Uniqueness)
seen) forall a b. (a -> b) -> a -> b
$ forall {t}. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Unique Names
names =
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. Name -> ErrorCase rep
UniqueReturnAliased Name
fname
      | Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set (VName, Uniqueness)
seen forall a. Semigroup a => a -> a -> a
<> forall {t}. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Nonunique Names
names

    tag :: t -> Names -> Set (VName, t)
tag t
u = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (,t
u) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> [VName]
namesToList

    returnAliasing :: [TypeBase shape Uniqueness] -> [b] -> [(Uniqueness, b)]
returnAliasing [TypeBase shape Uniqueness]
expected [b]
got =
      forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$
        forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness [TypeBase shape Uniqueness]
expected) forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Uniqueness
Nonunique) forall a b. (a -> b) -> a -> b
$
          forall a. [a] -> [a]
reverse [b]
got

checkSubExp :: Checkable rep => SubExp -> TypeM rep Type
checkSubExp :: forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp (Constant PrimValue
val) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall shape u. PrimType -> TypeBase shape u
Prim forall a b. (a -> b) -> a -> b
$ PrimValue -> PrimType
primValueType PrimValue
val
checkSubExp (Var VName
ident) = forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"In subexp " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
ident) forall a b. (a -> b) -> a -> b
$ do
  forall rep. Checkable rep => VName -> TypeM rep ()
observe VName
ident
  forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
ident

checkCerts :: Checkable rep => Certs -> TypeM rep ()
checkCerts :: forall rep. Checkable rep => Certs -> TypeM rep ()
checkCerts (Certs [VName]
cs) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit]) [VName]
cs

checkSubExpRes :: Checkable rep => SubExpRes -> TypeM rep Type
checkSubExpRes :: forall rep. Checkable rep => SubExpRes -> TypeM rep Type
checkSubExpRes (SubExpRes Certs
cs SubExp
se) = do
  forall rep. Checkable rep => Certs -> TypeM rep ()
checkCerts Certs
cs
  forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
se

checkStms ::
  Checkable rep =>
  Stms (Aliases rep) ->
  TypeM rep a ->
  TypeM rep a
checkStms :: forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
origstms TypeM rep a
m = [Stm (Aliases rep)] -> TypeM rep a
delve forall a b. (a -> b) -> a -> b
$ forall rep. Stms rep -> [Stm rep]
stmsToList Stms (Aliases rep)
origstms
  where
    delve :: [Stm (Aliases rep)] -> TypeM rep a
delve (stm :: Stm (Aliases rep)
stm@(Let Pat (LetDec (Aliases rep))
pat StmAux (ExpDec (Aliases rep))
_ Exp (Aliases rep)
e) : [Stm (Aliases rep)]
stms) = do
      forall rep a. String -> TypeM rep a -> TypeM rep a
context (forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$ Doc
"In expression of statement" Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr Pat (LetDec (Aliases rep))
pat)) forall a b. (a -> b) -> a -> b
$
        forall rep. Checkable rep => Exp (Aliases rep) -> TypeM rep ()
checkExp Exp (Aliases rep)
e
      forall rep a.
Checkable rep =>
Stm (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStm Stm (Aliases rep)
stm forall a b. (a -> b) -> a -> b
$
        [Stm (Aliases rep)] -> TypeM rep a
delve [Stm (Aliases rep)]
stms
    delve [] =
      TypeM rep a
m

checkResult ::
  Checkable rep =>
  Result ->
  TypeM rep ()
checkResult :: forall rep. Checkable rep => Result -> TypeM rep ()
checkResult = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => SubExpRes -> TypeM rep Type
checkSubExpRes

checkFunBody ::
  Checkable rep =>
  [RetType rep] ->
  Body (Aliases rep) ->
  TypeM rep [Names]
checkFunBody :: forall rep.
Checkable rep =>
[RetType rep] -> Body (Aliases rep) -> TypeM rep [Names]
checkFunBody [RetType rep]
rt (Body (BodyAliasing
_, BodyDec rep
rep) Stms (Aliases rep)
stms Result
res) = do
  forall rep. Checkable rep => BodyDec rep -> TypeM rep ()
checkBodyDec BodyDec rep
rep
  forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
stms forall a b. (a -> b) -> a -> b
$ do
    forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking body result" forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => Result -> TypeM rep ()
checkResult Result
res
    forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When matching declared return type to result of body" forall a b. (a -> b) -> a -> b
$
      forall rep.
Checkable rep =>
[RetType rep] -> Result -> TypeM rep ()
matchReturnType [RetType rep]
rt Result
res
    forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpRes -> SubExp
resSubExp) Result
res
  where
    bound_here :: Names
bound_here = [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stms (Aliases rep)
stms

checkLambdaBody ::
  Checkable rep =>
  [Type] ->
  Body (Aliases rep) ->
  TypeM rep [Names]
checkLambdaBody :: forall rep.
Checkable rep =>
[Type] -> Body (Aliases rep) -> TypeM rep [Names]
checkLambdaBody [Type]
ret (Body (BodyAliasing
_, BodyDec rep
rep) Stms (Aliases rep)
stms Result
res) = do
  forall rep. Checkable rep => BodyDec rep -> TypeM rep ()
checkBodyDec BodyDec rep
rep
  forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
stms forall a b. (a -> b) -> a -> b
$ do
    forall rep. Checkable rep => [Type] -> Result -> TypeM rep ()
checkLambdaResult [Type]
ret Result
res
    forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpRes -> SubExp
resSubExp) Result
res
  where
    bound_here :: Names
bound_here = [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stms (Aliases rep)
stms

checkLambdaResult ::
  Checkable rep =>
  [Type] ->
  Result ->
  TypeM rep ()
checkLambdaResult :: forall rep. Checkable rep => [Type] -> Result -> TypeM rep ()
checkLambdaResult [Type]
ts Result
es
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length Result
es =
      forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        String
"Lambda has return type "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple [Type]
ts
          forall a. [a] -> [a] -> [a]
++ String
" describing "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
          forall a. [a] -> [a] -> [a]
++ String
" values, but body returns "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length Result
es)
          forall a. [a] -> [a] -> [a]
++ String
" values: "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple Result
es
  | Bool
otherwise = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts Result
es) forall a b. (a -> b) -> a -> b
$ \(Type
t, SubExpRes
e) -> do
      Type
et <- forall rep. Checkable rep => SubExpRes -> TypeM rep Type
checkSubExpRes SubExpRes
e
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
et forall a. Eq a => a -> a -> Bool
== Type
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        String
"Subexpression "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty SubExpRes
e
          forall a. [a] -> [a] -> [a]
++ String
" has type "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
et
          forall a. [a] -> [a] -> [a]
++ String
" but expected "
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
t

checkBody ::
  Checkable rep =>
  Body (Aliases rep) ->
  TypeM rep [Names]
checkBody :: forall rep.
Checkable rep =>
Body (Aliases rep) -> TypeM rep [Names]
checkBody (Body (BodyAliasing
_, BodyDec rep
rep) Stms (Aliases rep)
stms Result
res) = do
  forall rep. Checkable rep => BodyDec rep -> TypeM rep ()
checkBodyDec BodyDec rep
rep
  forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
stms forall a b. (a -> b) -> a -> b
$ do
    forall rep. Checkable rep => Result -> TypeM rep ()
checkResult Result
res
    forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpRes -> SubExp
resSubExp) Result
res
  where
    bound_here :: Names
bound_here = [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stms (Aliases rep)
stms

checkBasicOp :: Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp :: forall rep. Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp (SubExp SubExp
es) =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
es
checkBasicOp (Opaque OpaqueOp
_ SubExp
es) =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
es
checkBasicOp (ArrayLit [] Type
_) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkBasicOp (ArrayLit (SubExp
e : [SubExp]
es') Type
t) = do
  let check :: Type -> SubExp -> TypeM rep ()
check Type
elemt SubExp
eleme = do
        Type
elemet <- forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
eleme
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
elemet forall a. Eq a => a -> a -> Bool
== Type
elemt) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
          forall a. Pretty a => a -> String
pretty Type
elemet
            forall a. [a] -> [a] -> [a]
++ String
" is not of expected type "
            forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
elemt
            forall a. [a] -> [a] -> [a]
++ String
"."
  Type
et <- forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
e

  -- Compare that type with the one given for the array literal.
  forall rep. String -> Type -> Type -> TypeM rep ()
checkAnnotation String
"array-element" Type
t Type
et

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {rep}. Checkable rep => Type -> SubExp -> TypeM rep ()
check Type
et) [SubExp]
es'
checkBasicOp (UnOp UnOp
op SubExp
e) = forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim forall a b. (a -> b) -> a -> b
$ UnOp -> PrimType
unOpType UnOp
op] SubExp
e
checkBasicOp (BinOp BinOp
op SubExp
e1 SubExp
e2) = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (BinOp -> PrimType
binOpType BinOp
op) SubExp
e1 SubExp
e2
checkBasicOp (CmpOp CmpOp
op SubExp
e1 SubExp
e2) = forall rep.
Checkable rep =>
CmpOp -> SubExp -> SubExp -> TypeM rep ()
checkCmpOp CmpOp
op SubExp
e1 SubExp
e2
checkBasicOp (ConvOp ConvOp
op SubExp
e) = forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ ConvOp -> (PrimType, PrimType)
convOpType ConvOp
op] SubExp
e
checkBasicOp (Index VName
ident (Slice [DimIndex SubExp]
idxes)) = do
  Type
vt <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
ident
  forall rep. Checkable rep => VName -> TypeM rep ()
observe VName
ident
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
vt forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [DimIndex SubExp]
idxes) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Int -> Int -> ErrorCase rep
SlicingError (forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
vt) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [DimIndex SubExp]
idxes)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => DimIndex SubExp -> TypeM rep ()
checkDimIndex [DimIndex SubExp]
idxes
checkBasicOp (Update Safety
_ VName
src (Slice [DimIndex SubExp]
idxes) SubExp
se) = do
  (Shape
src_shape, PrimType
src_pt) <- forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
src
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. ArrayShape a => a -> Int
shapeRank Shape
src_shape forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [DimIndex SubExp]
idxes) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Int -> Int -> ErrorCase rep
SlicingError (forall a. ArrayShape a => a -> Int
shapeRank Shape
src_shape) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [DimIndex SubExp]
idxes)

  Names
se_aliases <- forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM SubExp
se
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
src VName -> Names -> Bool
`nameIn` Names
se_aliases) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. String -> ErrorCase rep
TypeError String
"The target of an Update must not alias the value to be written."

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => DimIndex SubExp -> TypeM rep ()
checkDimIndex [DimIndex SubExp]
idxes
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u_unused u.
ArrayShape shape =>
TypeBase shape u_unused -> shape -> u -> TypeBase shape u
arrayOf (forall shape u. PrimType -> TypeBase shape u
Prim PrimType
src_pt) (forall d. [d] -> ShapeBase d
Shape (forall d. Slice d -> [d]
sliceDims (forall d. [DimIndex d] -> Slice d
Slice [DimIndex SubExp]
idxes))) NoUniqueness
NoUniqueness] SubExp
se
  forall rep. Checkable rep => Names -> TypeM rep ()
consume forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
src
checkBasicOp (FlatIndex VName
ident FlatSlice SubExp
slice) = do
  Type
vt <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
ident
  forall rep. Checkable rep => VName -> TypeM rep ()
observe VName
ident
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
vt forall a. Eq a => a -> a -> Bool
/= Int
1) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Int -> Int -> ErrorCase rep
SlicingError (forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
vt) Int
1
  forall rep. Checkable rep => FlatSlice SubExp -> TypeM rep ()
checkFlatSlice FlatSlice SubExp
slice
checkBasicOp (FlatUpdate VName
src FlatSlice SubExp
slice VName
v) = do
  (Shape
src_shape, PrimType
src_pt) <- forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
src
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. ArrayShape a => a -> Int
shapeRank Shape
src_shape forall a. Eq a => a -> a -> Bool
/= Int
1) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Int -> Int -> ErrorCase rep
SlicingError (forall a. ArrayShape a => a -> Int
shapeRank Shape
src_shape) Int
1

  Names
v_aliases <- forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
v
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
src VName -> Names -> Bool
`nameIn` Names
v_aliases) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. String -> ErrorCase rep
TypeError String
"The target of an Update must not alias the value to be written."

  forall rep. Checkable rep => FlatSlice SubExp -> TypeM rep ()
checkFlatSlice FlatSlice SubExp
slice
  forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [forall shape u_unused u.
ArrayShape shape =>
TypeBase shape u_unused -> shape -> u -> TypeBase shape u
arrayOf (forall shape u. PrimType -> TypeBase shape u
Prim PrimType
src_pt) (forall d. [d] -> ShapeBase d
Shape (forall d. FlatSlice d -> [d]
flatSliceDims FlatSlice SubExp
slice)) NoUniqueness
NoUniqueness] VName
v
  forall rep. Checkable rep => Names -> TypeM rep ()
consume forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
src
checkBasicOp (Iota SubExp
e SubExp
x SubExp
s IntType
et) = do
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
e
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
et] SubExp
x
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
et] SubExp
s
checkBasicOp (Replicate (Shape [SubExp]
dims) SubExp
valexp) = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
dims
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
valexp
checkBasicOp (Scratch PrimType
_ [SubExp]
shape) =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp [SubExp]
shape
checkBasicOp (Reshape ReshapeKind
k Shape
newshape VName
arrexp) = do
  Int
rank <- forall a. ArrayShape a => a -> Int
shapeRank forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
arrexp
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) forall a b. (a -> b) -> a -> b
$ forall d. ShapeBase d -> [d]
shapeDims Shape
newshape
  case ReshapeKind
k of
    ReshapeKind
ReshapeCoerce ->
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. ArrayShape a => a -> Int
shapeRank Shape
newshape forall a. Eq a => a -> a -> Bool
/= Int
rank) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
        forall rep. String -> ErrorCase rep
TypeError String
"Coercion changes rank of array."
    ReshapeKind
ReshapeArbitrary ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkBasicOp (Rearrange [Int]
perm VName
arr) = do
  Type
arrt <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
  let rank :: Int
rank = forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
arrt
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
perm forall a. Eq a => a -> a -> Bool
/= Int
rank Bool -> Bool -> Bool
|| forall a. Ord a => [a] -> [a]
sort [Int]
perm forall a. Eq a => a -> a -> Bool
/= [Int
0 .. Int
rank forall a. Num a => a -> a -> a
- Int
1]) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. [Int] -> Int -> Maybe VName -> ErrorCase rep
PermutationError [Int]
perm Int
rank forall a b. (a -> b) -> a -> b
$
        forall a. a -> Maybe a
Just VName
arr
checkBasicOp (Rotate [SubExp]
rots VName
arr) = do
  Type
arrt <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
  let rank :: Int
rank = forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
arrt
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
rots
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
rots forall a. Eq a => a -> a -> Bool
/= Int
rank) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        String
"Cannot rotate "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
rots)
          forall a. [a] -> [a] -> [a]
++ String
" dimensions of "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
rank
          forall a. [a] -> [a] -> [a]
++ String
"-dimensional array."
checkBasicOp (Concat Int
i (VName
arr1exp :| [VName]
arr2exps) SubExp
ressize) = do
  [SubExp]
arr1_dims <- forall d. ShapeBase d -> [d]
shapeDims forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
arr1exp
  [[SubExp]]
arr2s_dims <- forall a b. (a -> b) -> [a] -> [b]
map (forall d. ShapeBase d -> [d]
shapeDims forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent [VName]
arr2exps
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
== forall a. Int -> Int -> [a] -> [a]
dropAt Int
i Int
1 [SubExp]
arr1_dims) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> Int -> [a] -> [a]
dropAt Int
i Int
1) [[SubExp]]
arr2s_dims) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. String -> ErrorCase rep
TypeError String
"Types of arguments to concat do not match."
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
ressize
checkBasicOp (Copy VName
e) =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => VName -> TypeM rep (Shape, PrimType)
checkArrIdent VName
e
checkBasicOp (Manifest [Int]
perm VName
arr) =
  forall rep. Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp forall a b. (a -> b) -> a -> b
$ [Int] -> VName -> BasicOp
Rearrange [Int]
perm VName
arr -- Basically same thing!
checkBasicOp (Assert SubExp
e (ErrorMsg [ErrorMsgPart SubExp]
parts) (SrcLoc, [SrcLoc])
_) = do
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool] SubExp
e
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {rep}. Checkable rep => ErrorMsgPart SubExp -> TypeM rep ()
checkPart [ErrorMsgPart SubExp]
parts
  where
    checkPart :: ErrorMsgPart SubExp -> TypeM rep ()
checkPart ErrorString {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkPart (ErrorVal PrimType
t SubExp
x) = forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
x
checkBasicOp (UpdateAcc VName
acc [SubExp]
is [SubExp]
ses) = do
  (Shape
shape, [Type]
ts) <- forall rep. Checkable rep => VName -> TypeM rep (Shape, [Type])
checkAccIdent VName
acc

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
ses forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
    String
"Accumulator requires "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
      forall a. [a] -> [a] -> [a]
++ String
" values, but "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
ses)
      forall a. [a] -> [a] -> [a]
++ String
" provided."

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
is forall a. Eq a => a -> a -> Bool
== forall a. ArrayShape a => a -> Int
shapeRank Shape
shape) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
      String
"Accumulator requires "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. ArrayShape a => a -> Int
shapeRank Shape
shape)
        forall a. [a] -> [a] -> [a]
++ String
" indices, but "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
is)
        forall a. [a] -> [a] -> [a]
++ String
" provided."

  forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure [Type]
ts) [SubExp]
ses
  forall rep. Checkable rep => Names -> TypeM rep ()
consume forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
acc

matchLoopResultExt ::
  Checkable rep =>
  [Param DeclType] ->
  Result ->
  TypeM rep ()
matchLoopResultExt :: forall rep.
Checkable rep =>
[Param DeclType] -> Result -> TypeM rep ()
matchLoopResultExt [Param DeclType]
merge Result
loopres = do
  let rettype_ext :: [ExtType]
rettype_ext =
        [VName] -> [ExtType] -> [ExtType]
existentialiseExtTypes (forall a b. (a -> b) -> [a] -> [b]
map forall dec. Param dec -> VName
paramName [Param DeclType]
merge) forall a b. (a -> b) -> a -> b
$
          forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes forall a b. (a -> b) -> a -> b
$
            forall a b. (a -> b) -> [a] -> [b]
map forall t. Typed t => t -> Type
typeOf [Param DeclType]
merge

  [Type]
bodyt <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t (m :: * -> *). HasScope t m => SubExpRes -> m Type
subExpResType Result
loopres

  case forall (m :: * -> *) u.
Monad m =>
(Int -> m SubExp) -> [TypeBase ExtShape u] -> m [TypeBase Shape u]
instantiateShapes (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SubExpRes -> SubExp
resSubExp forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall int a. Integral int => int -> [a] -> Maybe a
`maybeNth` Result
loopres)) [ExtType]
rettype_ext of
    Maybe [Type]
Nothing ->
      forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
        forall rep. Name -> [ExtType] -> [ExtType] -> ErrorCase rep
ReturnTypeError
          (String -> Name
nameFromString String
"<loop body>")
          [ExtType]
rettype_ext
          (forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes [Type]
bodyt)
    Just [Type]
rettype' ->
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
bodyt forall u shape.
(Ord u, ArrayShape shape) =>
[TypeBase shape u] -> [TypeBase shape u] -> Bool
`subtypesOf` [Type]
rettype') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
        forall rep. Name -> [ExtType] -> [ExtType] -> ErrorCase rep
ReturnTypeError
          (String -> Name
nameFromString String
"<loop body>")
          (forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes [Type]
rettype')
          (forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes [Type]
bodyt)

checkExp ::
  Checkable rep =>
  Exp (Aliases rep) ->
  TypeM rep ()
checkExp :: forall rep. Checkable rep => Exp (Aliases rep) -> TypeM rep ()
checkExp (BasicOp BasicOp
op) = forall rep. Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp BasicOp
op
checkExp (Match [SubExp]
ses [Case (Body (Aliases rep))]
cases Body (Aliases rep)
def_case MatchDec (BranchType (Aliases rep))
info) = do
  [Type]
ses_ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp [SubExp]
ses
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> Case (Body (Aliases rep)) -> TypeM rep ()
checkCase [Type]
ses_ts) [Case (Body (Aliases rep))]
cases
  Body (Aliases rep) -> TypeM rep ()
checkCaseBody Body (Aliases rep)
def_case
  where
    checkVal :: TypeBase shape u -> Maybe PrimValue -> Bool
checkVal TypeBase shape u
t (Just PrimValue
v) = forall shape u. PrimType -> TypeBase shape u
Prim (PrimValue -> PrimType
primValueType PrimValue
v) forall a. Eq a => a -> a -> Bool
== TypeBase shape u
t
    checkVal TypeBase shape u
_ Maybe PrimValue
Nothing = Bool
True
    checkCase :: [Type] -> Case (Body (Aliases rep)) -> TypeM rep ()
checkCase [Type]
ses_ts (Case [Maybe PrimValue]
vs Body (Aliases rep)
body) = do
      let ok :: Bool
ok = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe PrimValue]
vs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ses_ts Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {u} {shape}.
(Eq u, Eq shape) =>
TypeBase shape u -> Maybe PrimValue -> Bool
checkVal [Type]
ses_ts [Maybe PrimValue]
vs)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$
        Doc
"Scrutinee"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => [a] -> Doc
ppTuple' [SubExp]
ses)
          Doc -> Doc -> Doc
</> Doc
"cannot match pattern"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => [a] -> Doc
ppTuple' [Maybe PrimValue]
vs)
      forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"in body of case " forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => [a] -> String
prettyTuple [Maybe PrimValue]
vs) forall a b. (a -> b) -> a -> b
$ Body (Aliases rep) -> TypeM rep ()
checkCaseBody Body (Aliases rep)
body
    checkCaseBody :: Body (Aliases rep) -> TypeM rep ()
checkCaseBody = forall rep.
Checkable rep =>
[BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
matchBranchType (forall rt. MatchDec rt -> [rt]
matchReturns MatchDec (BranchType (Aliases rep))
info)
checkExp (Apply Name
fname [(SubExp, Diet)]
args [RetType (Aliases rep)]
rettype_annot (Safety, SrcLoc, [SrcLoc])
_) = do
  ([RetType rep]
rettype_derived, [DeclType]
paramtypes) <- forall rep.
Checkable rep =>
Name -> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
lookupFun Name
fname forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(SubExp, Diet)]
args
  [Arg]
argflows <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(SubExp, Diet)]
args
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([RetType rep]
rettype_derived forall a. Eq a => a -> a -> Bool
/= [RetType (Aliases rep)]
rettype_annot) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$
      Doc
"Expected apply result type:"
        Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr [RetType rep]
rettype_derived)
        Doc -> Doc -> Doc
</> Doc
"But annotation is:"
        Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr [RetType (Aliases rep)]
rettype_annot)
  forall rep. [DeclType] -> [Arg] -> TypeM rep ()
consumeArgs [DeclType]
paramtypes [Arg]
argflows
checkExp (DoLoop [(FParam (Aliases rep), SubExp)]
merge LoopForm (Aliases rep)
form Body (Aliases rep)
loopbody) = do
  let ([Param (FParamInfo rep)]
mergepat, [SubExp]
mergeexps) = forall a b. [(a, b)] -> ([a], [b])
unzip [(FParam (Aliases rep), SubExp)]
merge
  [Arg]
mergeargs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg [SubExp]
mergeexps

  TypeM rep ()
checkLoopArgs

  forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding (forall rep a. Scoped rep a => a -> Scope rep
scopeOf LoopForm (Aliases rep)
form) forall a b. (a -> b) -> a -> b
$ do
    [(VName, Names)]
form_consumable <- [Arg] -> LoopForm (Aliases rep) -> TypeM rep [(VName, Names)]
checkForm [Arg]
mergeargs LoopForm (Aliases rep)
form

    let rettype :: [DeclType]
rettype = forall a b. (a -> b) -> [a] -> [b]
map forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo rep)]
mergepat
        consumable :: [(VName, Names)]
consumable =
          [ (forall dec. Param dec -> VName
paramName Param (FParamInfo rep)
param, forall a. Monoid a => a
mempty)
            | Param (FParamInfo rep)
param <- [Param (FParamInfo rep)]
mergepat,
              forall shape. TypeBase shape Uniqueness -> Bool
unique forall a b. (a -> b) -> a -> b
$ forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType Param (FParamInfo rep)
param
          ]
            forall a. [a] -> [a] -> [a]
++ [(VName, Names)]
form_consumable

    forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"Inside the loop body"
      forall a b. (a -> b) -> a -> b
$ forall rep.
Checkable rep =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
checkFun'
        ( String -> Name
nameFromString String
"<loop body>",
          forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes [DeclType]
rettype,
          forall rep. [FParam rep] -> [(VName, NameInfo (Aliases rep))]
funParamsToNameInfos [Param (FParamInfo rep)]
mergepat
        )
        (forall a. a -> Maybe a
Just [(VName, Names)]
consumable)
      forall a b. (a -> b) -> a -> b
$ do
        forall rep. Checkable rep => [FParam rep] -> TypeM rep ()
checkFunParams [Param (FParamInfo rep)]
mergepat
        forall rep. Checkable rep => BodyDec rep -> TypeM rep ()
checkBodyDec forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall rep. Body rep -> BodyDec rep
bodyDec Body (Aliases rep)
loopbody

        forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms (forall rep. Body rep -> Stms rep
bodyStms Body (Aliases rep)
loopbody) forall a b. (a -> b) -> a -> b
$ do
          forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"In loop body result" forall a b. (a -> b) -> a -> b
$
            forall rep. Checkable rep => Result -> TypeM rep ()
checkResult forall a b. (a -> b) -> a -> b
$
              forall rep. Body rep -> Result
bodyResult Body (Aliases rep)
loopbody

          forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When matching result of body with loop parameters" forall a b. (a -> b) -> a -> b
$
            forall rep.
Checkable rep =>
[FParam (Aliases rep)] -> Result -> TypeM rep ()
matchLoopResult (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(FParam (Aliases rep), SubExp)]
merge) forall a b. (a -> b) -> a -> b
$
              forall rep. Body rep -> Result
bodyResult Body (Aliases rep)
loopbody

          let bound_here :: Names
bound_here =
                [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall rep a. Scoped rep a => a -> Scope rep
scopeOf forall a b. (a -> b) -> a -> b
$ forall rep. Body rep -> Stms rep
bodyStms Body (Aliases rep)
loopbody
          forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpRes -> SubExp
resSubExp) (forall rep. Body rep -> Result
bodyResult Body (Aliases rep)
loopbody)
  where
    checkLoopVar :: (Param (LParamInfo rep), VName) -> TypeM rep (VName, Names)
checkLoopVar (Param (LParamInfo rep)
p, VName
a) = do
      Type
a_t <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
a
      forall rep. Checkable rep => VName -> TypeM rep ()
observe VName
a
      case forall u. Int -> TypeBase Shape u -> Maybe (TypeBase Shape u)
peelArray Int
1 Type
a_t of
        Just Type
a_t_r -> do
          forall rep.
Checkable rep =>
VName -> LParamInfo rep -> TypeM rep ()
checkLParamDec (forall dec. Param dec -> VName
paramName Param (LParamInfo rep)
p) forall a b. (a -> b) -> a -> b
$ forall dec. Param dec -> dec
paramDec Param (LParamInfo rep)
p
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
a_t_r forall u shape.
(Ord u, ArrayShape shape) =>
TypeBase shape u -> TypeBase shape u -> Bool
`subtypeOf` forall t. Typed t => t -> Type
typeOf (forall dec. Param dec -> dec
paramDec Param (LParamInfo rep)
p)) forall a b. (a -> b) -> a -> b
$
            forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
              String
"Loop parameter "
                forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Param (LParamInfo rep)
p
                forall a. [a] -> [a] -> [a]
++ String
" not valid for element of "
                forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
a
                forall a. [a] -> [a] -> [a]
++ String
", which has row type "
                forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
a_t_r
          Names
als <- forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
a
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall dec. Param dec -> VName
paramName Param (LParamInfo rep)
p, Names
als)
        Maybe Type
_ ->
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
            String
"Cannot loop over "
              forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
a
              forall a. [a] -> [a] -> [a]
++ String
" of type "
              forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty Type
a_t
    checkForm :: [Arg] -> LoopForm (Aliases rep) -> TypeM rep [(VName, Names)]
checkForm [Arg]
mergeargs (ForLoop VName
loopvar IntType
it SubExp
boundexp [(LParam (Aliases rep), VName)]
loopvars) = do
      Param (FParamInfo rep)
iparam <- forall rep.
Checkable rep =>
VName -> PrimType -> TypeM rep (FParam (Aliases rep))
primFParam VName
loopvar forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
it
      let mergepat :: [Param (FParamInfo rep)]
mergepat = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(FParam (Aliases rep), SubExp)]
merge
          funparams :: [Param (FParamInfo rep)]
funparams = Param (FParamInfo rep)
iparam forall a. a -> [a] -> [a]
: [Param (FParamInfo rep)]
mergepat
          paramts :: [DeclType]
paramts = forall a b. (a -> b) -> [a] -> [b]
map forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo rep)]
funparams

      [(VName, Names)]
consumable <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {rep}.
Checkable rep =>
(Param (LParamInfo rep), VName) -> TypeM rep (VName, Names)
checkLoopVar [(LParam (Aliases rep), VName)]
loopvars
      Arg
boundarg <- forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg SubExp
boundexp
      forall rep. Maybe Name -> [DeclType] -> [Arg] -> TypeM rep ()
checkFuncall forall a. Maybe a
Nothing [DeclType]
paramts forall a b. (a -> b) -> a -> b
$ Arg
boundarg forall a. a -> [a] -> [a]
: [Arg]
mergeargs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [(VName, Names)]
consumable
    checkForm [Arg]
mergeargs (WhileLoop VName
cond) = do
      case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
== VName
cond) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dec. Param dec -> VName
paramName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(FParam (Aliases rep), SubExp)]
merge of
        Just (Param (FParamInfo rep)
condparam, SubExp
_) ->
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dec. Typed dec => Param dec -> Type
paramType Param (FParamInfo rep)
condparam forall a. Eq a => a -> a -> Bool
== forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool) forall a b. (a -> b) -> a -> b
$
            forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
              String
"Conditional '"
                forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
cond
                forall a. [a] -> [a] -> [a]
++ String
"' of while-loop is not boolean, but "
                forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty (forall dec. Typed dec => Param dec -> Type
paramType Param (FParamInfo rep)
condparam)
                forall a. [a] -> [a] -> [a]
++ String
"."
        Maybe (Param (FParamInfo rep), SubExp)
Nothing ->
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
            forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
              String
"Conditional '" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
cond forall a. [a] -> [a] -> [a]
++ String
"' of while-loop is not a merge variable."
      let mergepat :: [Param (FParamInfo rep)]
mergepat = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(FParam (Aliases rep), SubExp)]
merge
          funparams :: [Param (FParamInfo rep)]
funparams = [Param (FParamInfo rep)]
mergepat
          paramts :: [DeclType]
paramts = forall a b. (a -> b) -> [a] -> [b]
map forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo rep)]
funparams
      forall rep. Maybe Name -> [DeclType] -> [Arg] -> TypeM rep ()
checkFuncall forall a. Maybe a
Nothing [DeclType]
paramts [Arg]
mergeargs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

    checkLoopArgs :: TypeM rep ()
checkLoopArgs = do
      let ([Param (FParamInfo rep)]
params, [SubExp]
args) = forall a b. [(a, b)] -> ([a], [b])
unzip [(FParam (Aliases rep), SubExp)]
merge

      [Type]
argtypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t (m :: * -> *). HasScope t m => SubExp -> m Type
subExpType [SubExp]
args

      let expected :: [Type]
expected = forall t. Typed t => [VName] -> [t] -> [SubExp] -> [Type]
expectedTypes (forall a b. (a -> b) -> [a] -> [b]
map forall dec. Param dec -> VName
paramName [Param (FParamInfo rep)]
params) [Param (FParamInfo rep)]
params [SubExp]
args
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
expected forall a. Eq a => a -> a -> Bool
== [Type]
argtypes) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$
        Doc
"Loop parameters"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => [a] -> Doc
ppTuple' [Param (FParamInfo rep)]
params)
          Doc -> Doc -> Doc
</> Doc
"cannot accept initial values"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => [a] -> Doc
ppTuple' [SubExp]
args)
          Doc -> Doc -> Doc
</> Doc
"of types"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => [a] -> Doc
ppTuple' [Type]
argtypes)
checkExp (WithAcc [WithAccInput (Aliases rep)]
inputs Lambda (Aliases rep)
lam) = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall rep. Lambda rep -> [LParam rep]
lambdaParams Lambda (Aliases rep)
lam) forall a. Eq a => a -> a -> Bool
== Int
2 forall a. Num a => a -> a -> a
* Int
num_accs) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
      forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall rep. Lambda rep -> [LParam rep]
lambdaParams Lambda (Aliases rep)
lam))
        forall a. [a] -> [a] -> [a]
++ String
" parameters, but "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
num_accs
        forall a. [a] -> [a] -> [a]
++ String
" accumulators."

  let cert_params :: [Param (LParamInfo rep)]
cert_params = forall a. Int -> [a] -> [a]
take Int
num_accs forall a b. (a -> b) -> a -> b
$ forall rep. Lambda rep -> [LParam rep]
lambdaParams Lambda (Aliases rep)
lam
  [Arg]
acc_args <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [WithAccInput (Aliases rep)]
inputs [Param (LParamInfo rep)]
cert_params) forall a b. (a -> b) -> a -> b
$ \((Shape
shape, [VName]
arrs, Maybe (Lambda (Aliases rep), [SubExp])
op), Param (LParamInfo rep)
p) -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) (forall d. ShapeBase d -> [d]
shapeDims Shape
shape)
    [Type]
elem_ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VName]
arrs forall a b. (a -> b) -> a -> b
$ \VName
arr -> do
      Type
arr_t <- forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall d. ShapeBase d -> [d]
shapeDims Shape
shape forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` forall u. TypeBase Shape u -> [SubExp]
arrayDims Type
arr_t) forall a b. (a -> b) -> a -> b
$
        forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
          forall a. Pretty a => a -> String
pretty VName
arr forall a. Semigroup a => a -> a -> a
<> String
" is not an array of outer shape " forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> String
pretty Shape
shape
      forall rep. Checkable rep => Names -> TypeM rep ()
consume forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
arr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall u. Int -> TypeBase Shape u -> TypeBase Shape u
stripArray (forall a. ArrayShape a => a -> Int
shapeRank Shape
shape) Type
arr_t

    case Maybe (Lambda (Aliases rep), [SubExp])
op of
      Just (Lambda (Aliases rep)
op_lam, [SubExp]
nes) -> do
        let mkArrArg :: a -> (a, b)
mkArrArg a
t = (a
t, forall a. Monoid a => a
mempty)
        [Type]
nes_ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp [SubExp]
nes
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
nes_ts forall a. Eq a => a -> a -> Bool
== forall rep. Lambda rep -> [Type]
lambdaReturnType Lambda (Aliases rep)
op_lam) forall a b. (a -> b) -> a -> b
$
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
            forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
              [String] -> String
unlines
                [ String
"Accumulator operator return type: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty (forall rep. Lambda rep -> [Type]
lambdaReturnType Lambda (Aliases rep)
op_lam),
                  String
"Type of neutral elements: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty [Type]
nes_ts
                ]
        forall rep.
Checkable rep =>
Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkLambda Lambda (Aliases rep)
op_lam forall a b. (a -> b) -> a -> b
$
          forall a. Int -> a -> [a]
replicate (forall a. ArrayShape a => a -> Int
shapeRank Shape
shape) (forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64, forall a. Monoid a => a
mempty)
            forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall {b} {a}. Monoid b => a -> (a, b)
mkArrArg ([Type]
elem_ts forall a. [a] -> [a] -> [a]
++ [Type]
elem_ts)
      Maybe (Lambda (Aliases rep), [SubExp])
Nothing ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall shape u. VName -> Shape -> [Type] -> u -> TypeBase shape u
Acc (forall dec. Param dec -> VName
paramName Param (LParamInfo rep)
p) Shape
shape [Type]
elem_ts NoUniqueness
NoUniqueness, forall a. Monoid a => a
mempty)

  forall rep.
Checkable rep =>
Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkAnyLambda Bool
False Lambda (Aliases rep)
lam forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
num_accs (forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit, forall a. Monoid a => a
mempty) forall a. [a] -> [a] -> [a]
++ [Arg]
acc_args
  where
    num_accs :: Int
num_accs = forall (t :: * -> *) a. Foldable t => t a -> Int
length [WithAccInput (Aliases rep)]
inputs
checkExp (Op Op (Aliases rep)
op) = do
  OpWithAliases (Op rep) -> TypeM rep ()
checker <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall rep. Env rep -> OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp
  OpWithAliases (Op rep) -> TypeM rep ()
checker Op (Aliases rep)
op

checkSOACArrayArgs ::
  Checkable rep =>
  SubExp ->
  [VName] ->
  TypeM rep [Arg]
checkSOACArrayArgs :: forall rep. Checkable rep => SubExp -> [VName] -> TypeM rep [Arg]
checkSOACArrayArgs SubExp
width = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TypeM rep Arg
checkSOACArrayArg
  where
    checkSOACArrayArg :: VName -> TypeM rep Arg
checkSOACArrayArg VName
v = do
      (Type
t, Names
als) <- forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
v
      case Type
t of
        Acc {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type
t, Names
als)
        Array {} -> do
          let argSize :: SubExp
argSize = forall u. Int -> TypeBase Shape u -> SubExp
arraySize Int
0 Type
t
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SubExp
argSize forall a. Eq a => a -> a -> Bool
== SubExp
width) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
            String
"SOAC argument "
              forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
v
              forall a. [a] -> [a] -> [a]
++ String
" has outer size "
              forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty SubExp
argSize
              forall a. [a] -> [a] -> [a]
++ String
", but width of SOAC is "
              forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty SubExp
width
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall u. TypeBase Shape u -> TypeBase Shape u
rowType Type
t, Names
als)
        Type
_ ->
          forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
            String
"SOAC argument " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
v forall a. [a] -> [a] -> [a]
++ String
" is not an array"

checkType ::
  Checkable rep =>
  TypeBase Shape u ->
  TypeM rep ()
checkType :: forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType (Mem (ScalarSpace [SubExp]
d PrimType
_)) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
d
checkType (Acc VName
cert Shape
shape [Type]
ts u
_) = do
  forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit] VName
cert
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) forall a b. (a -> b) -> a -> b
$ forall d. ShapeBase d -> [d]
shapeDims Shape
shape
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType [Type]
ts
checkType TypeBase Shape u
t = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Shape u -> [SubExp]
arrayDims TypeBase Shape u
t

checkExtType ::
  Checkable rep =>
  TypeBase ExtShape u ->
  TypeM rep ()
checkExtType :: forall rep u. Checkable rep => TypeBase ExtShape u -> TypeM rep ()
checkExtType = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {rep}. Checkable rep => Ext SubExp -> TypeM rep ()
checkExtDim forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall d. ShapeBase d -> [d]
shapeDims forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall shape u. ArrayShape shape => TypeBase shape u -> shape
arrayShape
  where
    checkExtDim :: Ext SubExp -> TypeM rep ()
checkExtDim (Free SubExp
se) = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
se
    checkExtDim (Ext Int
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

checkCmpOp ::
  Checkable rep =>
  CmpOp ->
  SubExp ->
  SubExp ->
  TypeM rep ()
checkCmpOp :: forall rep.
Checkable rep =>
CmpOp -> SubExp -> SubExp -> TypeM rep ()
checkCmpOp (CmpEq PrimType
t) SubExp
x SubExp
y = do
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
x
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
y
checkCmpOp (CmpUlt IntType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (IntType -> PrimType
IntType IntType
t) SubExp
x SubExp
y
checkCmpOp (CmpUle IntType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (IntType -> PrimType
IntType IntType
t) SubExp
x SubExp
y
checkCmpOp (CmpSlt IntType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (IntType -> PrimType
IntType IntType
t) SubExp
x SubExp
y
checkCmpOp (CmpSle IntType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (IntType -> PrimType
IntType IntType
t) SubExp
x SubExp
y
checkCmpOp (FCmpLt FloatType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (FloatType -> PrimType
FloatType FloatType
t) SubExp
x SubExp
y
checkCmpOp (FCmpLe FloatType
t) SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs (FloatType -> PrimType
FloatType FloatType
t) SubExp
x SubExp
y
checkCmpOp CmpOp
CmpLlt SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs PrimType
Bool SubExp
x SubExp
y
checkCmpOp CmpOp
CmpLle SubExp
x SubExp
y = forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs PrimType
Bool SubExp
x SubExp
y

checkBinOpArgs ::
  Checkable rep =>
  PrimType ->
  SubExp ->
  SubExp ->
  TypeM rep ()
checkBinOpArgs :: forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs PrimType
t SubExp
e1 SubExp
e2 = do
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
e1
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
e2

checkPatElem ::
  Checkable rep =>
  PatElem (LetDec rep) ->
  TypeM rep ()
checkPatElem :: forall rep. Checkable rep => PatElem (LetDec rep) -> TypeM rep ()
checkPatElem (PatElem VName
name LetDec rep
dec) =
  forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"When checking pattern element " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty VName
name) forall a b. (a -> b) -> a -> b
$
    forall rep. Checkable rep => VName -> LetDec rep -> TypeM rep ()
checkLetBoundDec VName
name LetDec rep
dec

checkFlatDimIndex ::
  Checkable rep =>
  FlatDimIndex SubExp ->
  TypeM rep ()
checkFlatDimIndex :: forall rep. Checkable rep => FlatDimIndex SubExp -> TypeM rep ()
checkFlatDimIndex (FlatDimIndex SubExp
n SubExp
s) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp
n, SubExp
s]

checkFlatSlice ::
  Checkable rep =>
  FlatSlice SubExp ->
  TypeM rep ()
checkFlatSlice :: forall rep. Checkable rep => FlatSlice SubExp -> TypeM rep ()
checkFlatSlice (FlatSlice SubExp
offset [FlatDimIndex SubExp]
idxs) = do
  forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
offset
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => FlatDimIndex SubExp -> TypeM rep ()
checkFlatDimIndex [FlatDimIndex SubExp]
idxs

checkDimIndex ::
  Checkable rep =>
  DimIndex SubExp ->
  TypeM rep ()
checkDimIndex :: forall rep. Checkable rep => DimIndex SubExp -> TypeM rep ()
checkDimIndex (DimFix SubExp
i) = forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
i
checkDimIndex (DimSlice SubExp
i SubExp
n SubExp
s) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp
i, SubExp
n, SubExp
s]

checkStm ::
  Checkable rep =>
  Stm (Aliases rep) ->
  TypeM rep a ->
  TypeM rep a
checkStm :: forall rep a.
Checkable rep =>
Stm (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStm stm :: Stm (Aliases rep)
stm@(Let Pat (LetDec (Aliases rep))
pat (StmAux (Certs [VName]
cs) Attrs
_ (VarAliases
_, ExpDec rep
dec)) Exp (Aliases rep)
e) TypeM rep a
m = do
  forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking certificates" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit]) [VName]
cs
  forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking expression annotation" forall a b. (a -> b) -> a -> b
$ forall rep. Checkable rep => ExpDec rep -> TypeM rep ()
checkExpDec ExpDec rep
dec
  forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"When matching\n" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => String -> a -> String
message String
"  " Pat (LetDec (Aliases rep))
pat forall a. [a] -> [a] -> [a]
++ String
"\nwith\n" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => String -> a -> String
message String
"  " Exp (Aliases rep)
e) forall a b. (a -> b) -> a -> b
$
    forall rep.
Checkable rep =>
Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()
matchPat Pat (LetDec (Aliases rep))
pat Exp (Aliases rep)
e
  forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding (Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
maybeWithoutAliases forall a b. (a -> b) -> a -> b
$ forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stm (Aliases rep)
stm) forall a b. (a -> b) -> a -> b
$ do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep. Checkable rep => PatElem (LetDec rep) -> TypeM rep ()
checkPatElem (forall dec. Pat dec -> [PatElem dec]
patElems forall a b. (a -> b) -> a -> b
$ forall a. Pat (VarAliases, a) -> Pat a
removePatAliases Pat (LetDec (Aliases rep))
pat)
    TypeM rep a
m
  where
    -- FIXME: this is wrong.  However, the core language type system
    -- is not strong enough to fully capture the aliases we want (see
    -- issue #803).  Since we eventually inline everything anyway, and
    -- our intra-procedural alias analysis is much simpler and
    -- correct, I could not justify spending time on improving the
    -- inter-procedural alias analysis.  If we ever stop inlining
    -- everything, probably we need to go back and refine this.
    maybeWithoutAliases :: Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
maybeWithoutAliases =
      case forall rep. Stm rep -> Exp rep
stmExp Stm (Aliases rep)
stm of
        Apply {} -> forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall {rep} {a} {b}.
(LetDec rep ~ (a, b), Monoid a) =>
NameInfo rep -> NameInfo rep
withoutAliases
        Exp (Aliases rep)
_ -> forall a. a -> a
id
    withoutAliases :: NameInfo rep -> NameInfo rep
withoutAliases (LetName (a
_, b
ldec)) = forall rep. LetDec rep -> NameInfo rep
LetName (forall a. Monoid a => a
mempty, b
ldec)
    withoutAliases NameInfo rep
info = NameInfo rep
info

matchExtPat ::
  Checkable rep =>
  Pat (LetDec (Aliases rep)) ->
  [ExtType] ->
  TypeM rep ()
matchExtPat :: forall rep.
Checkable rep =>
Pat (LetDec (Aliases rep)) -> [ExtType] -> TypeM rep ()
matchExtPat Pat (LetDec (Aliases rep))
pat [ExtType]
ts =
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dec. Typed dec => Pat dec -> [ExtType]
expExtTypesFromPat Pat (LetDec (Aliases rep))
pat forall a. Eq a => a -> a -> Bool
== [ExtType]
ts) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep.
Pat (LetDec (Aliases rep))
-> [ExtType] -> Maybe String -> ErrorCase rep
InvalidPatError Pat (LetDec (Aliases rep))
pat [ExtType]
ts forall a. Maybe a
Nothing

matchExtReturnType ::
  Checkable rep =>
  [ExtType] ->
  Result ->
  TypeM rep ()
matchExtReturnType :: forall rep. Checkable rep => [ExtType] -> Result -> TypeM rep ()
matchExtReturnType [ExtType]
rettype Result
res = do
  [Type]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t (m :: * -> *). HasScope t m => SubExpRes -> m Type
subExpResType Result
res
  forall rep. [ExtType] -> Result -> [Type] -> TypeM rep ()
matchExtReturns [ExtType]
rettype Result
res [Type]
ts

matchExtBranchType ::
  Checkable rep =>
  [ExtType] ->
  Body (Aliases rep) ->
  TypeM rep ()
matchExtBranchType :: forall rep.
Checkable rep =>
[ExtType] -> Body (Aliases rep) -> TypeM rep ()
matchExtBranchType [ExtType]
rettype (Body BodyDec (Aliases rep)
_ Stms (Aliases rep)
stms Result
res) = do
  [Type]
ts <- forall rep (m :: * -> *) a.
ExtendedScope rep m a -> Scope rep -> m a
extendedScope (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall t (m :: * -> *). HasScope t m => SubExpRes -> m Type
subExpResType Result
res) Scope (Aliases rep)
stmscope
  forall rep. [ExtType] -> Result -> [Type] -> TypeM rep ()
matchExtReturns [ExtType]
rettype Result
res [Type]
ts
  where
    stmscope :: Scope (Aliases rep)
stmscope = forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stms (Aliases rep)
stms

matchExtReturns :: [ExtType] -> Result -> [Type] -> TypeM rep ()
matchExtReturns :: forall rep. [ExtType] -> Result -> [Type] -> TypeM rep ()
matchExtReturns [ExtType]
rettype Result
res [Type]
ts = do
  let problem :: TypeM rep a
      problem :: forall rep a. TypeM rep a
problem =
        forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
          [ String
"Type annotation is",
            String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple [ExtType]
rettype,
            String
"But result returns type",
            String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => [a] -> String
prettyTuple [Type]
ts
          ]

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length Result
res forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExtType]
rettype) forall rep a. TypeM rep a
problem

  let ctx_vals :: [(SubExpRes, Type)]
ctx_vals = forall a b. [a] -> [b] -> [(a, b)]
zip Result
res [Type]
ts
      instantiateExt :: Int -> TypeM rep SubExp
instantiateExt Int
i = case forall int a. Integral int => int -> [a] -> Maybe a
maybeNth Int
i [(SubExpRes, Type)]
ctx_vals of
        Just (SubExpRes Certs
_ SubExp
se, Prim (IntType IntType
Int64)) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SubExp
se
        Maybe (SubExpRes, Type)
_ -> forall rep a. TypeM rep a
problem

  [Type]
rettype' <- forall (m :: * -> *) u.
Monad m =>
(Int -> m SubExp) -> [TypeBase ExtShape u] -> m [TypeBase Shape u]
instantiateShapes Int -> TypeM rep SubExp
instantiateExt [ExtType]
rettype

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
rettype' forall a. Eq a => a -> a -> Bool
== [Type]
ts) forall rep a. TypeM rep a
problem

validApply ::
  ArrayShape shape =>
  [TypeBase shape Uniqueness] ->
  [TypeBase shape NoUniqueness] ->
  Bool
validApply :: forall shape.
ArrayShape shape =>
[TypeBase shape Uniqueness]
-> [TypeBase shape NoUniqueness] -> Bool
validApply [TypeBase shape Uniqueness]
expected [TypeBase shape NoUniqueness]
got =
  forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeBase shape NoUniqueness]
got forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeBase shape Uniqueness]
expected
    Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      ( forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
          forall u shape.
(Ord u, ArrayShape shape) =>
TypeBase shape u -> TypeBase shape u -> Bool
subtypeOf
          (forall a b. (a -> b) -> [a] -> [b]
map forall shape u.
ArrayShape shape =>
TypeBase shape u -> TypeBase Rank u
rankShaped [TypeBase shape NoUniqueness]
got)
          (forall a b. (a -> b) -> [a] -> [b]
map (forall shape.
TypeBase shape Uniqueness -> TypeBase shape NoUniqueness
fromDecl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall shape u.
ArrayShape shape =>
TypeBase shape u -> TypeBase Rank u
rankShaped) [TypeBase shape Uniqueness]
expected)
      )

type Arg = (Type, Names)

argType :: Arg -> Type
argType :: Arg -> Type
argType (Type
t, Names
_) = Type
t

-- | Remove all aliases from the 'Arg'.
argAliases :: Arg -> Names
argAliases :: Arg -> Names
argAliases (Type
_, Names
als) = Names
als

noArgAliases :: Arg -> Arg
noArgAliases :: Arg -> Arg
noArgAliases (Type
t, Names
_) = (Type
t, forall a. Monoid a => a
mempty)

checkArg ::
  Checkable rep =>
  SubExp ->
  TypeM rep Arg
checkArg :: forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg SubExp
arg = do
  Type
argt <- forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
arg
  Names
als <- forall rep. Checkable rep => SubExp -> TypeM rep Names
subExpAliasesM SubExp
arg
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type
argt, Names
als)

checkFuncall ::
  Maybe Name ->
  [DeclType] ->
  [Arg] ->
  TypeM rep ()
checkFuncall :: forall rep. Maybe Name -> [DeclType] -> [Arg] -> TypeM rep ()
checkFuncall Maybe Name
fname [DeclType]
paramts [Arg]
args = do
  let argts :: [Type]
argts = forall a b. (a -> b) -> [a] -> [b]
map Arg -> Type
argType [Arg]
args
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall shape.
ArrayShape shape =>
[TypeBase shape Uniqueness]
-> [TypeBase shape NoUniqueness] -> Bool
validApply [DeclType]
paramts [Type]
argts) forall a b. (a -> b) -> a -> b
$
    forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$
      forall rep. Maybe Name -> [Type] -> [Type] -> ErrorCase rep
ParameterMismatch Maybe Name
fname (forall a b. (a -> b) -> [a] -> [b]
map forall shape.
TypeBase shape Uniqueness -> TypeBase shape NoUniqueness
fromDecl [DeclType]
paramts) forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map Arg -> Type
argType [Arg]
args
  forall rep. [DeclType] -> [Arg] -> TypeM rep ()
consumeArgs [DeclType]
paramts [Arg]
args

consumeArgs ::
  [DeclType] ->
  [Arg] ->
  TypeM rep ()
consumeArgs :: forall rep. [DeclType] -> [Arg] -> TypeM rep ()
consumeArgs [DeclType]
paramts [Arg]
args =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall shape. TypeBase shape Uniqueness -> Diet
diet [DeclType]
paramts) [Arg]
args) forall a b. (a -> b) -> a -> b
$ \(Diet
d, (Type
_, Names
als)) ->
    forall rep. [Occurence] -> TypeM rep ()
occur [Names -> Occurence
consumption (forall {p}. Monoid p => p -> Diet -> p
consumeArg Names
als Diet
d)]
  where
    consumeArg :: p -> Diet -> p
consumeArg p
als Diet
Consume = p
als
    consumeArg p
_ Diet
_ = forall a. Monoid a => a
mempty

-- The boolean indicates whether we only allow consumption of
-- parameters.
checkAnyLambda ::
  Checkable rep => Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkAnyLambda :: forall rep.
Checkable rep =>
Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkAnyLambda Bool
soac (Lambda [LParam (Aliases rep)]
params Body (Aliases rep)
body [Type]
rettype) [Arg]
args = do
  let fname :: Name
fname = String -> Name
nameFromString String
"<anonymous>"
  if forall (t :: * -> *) a. Foldable t => t a -> Int
length [LParam (Aliases rep)]
params forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg]
args
    then do
      -- Consumption for this is done explicitly elsewhere.
      forall rep. Maybe Name -> [DeclType] -> [Arg] -> TypeM rep ()
checkFuncall
        forall a. Maybe a
Nothing
        (forall a b. (a -> b) -> [a] -> [b]
map ((forall shape.
TypeBase shape NoUniqueness
-> Uniqueness -> TypeBase shape Uniqueness
`toDecl` Uniqueness
Nonunique) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dec. Typed dec => Param dec -> Type
paramType) [LParam (Aliases rep)]
params)
        forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Arg -> Arg
noArgAliases [Arg]
args
      let consumable :: Maybe [(VName, Names)]
consumable =
            if Bool
soac
              then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall dec. Param dec -> VName
paramName [LParam (Aliases rep)]
params) (forall a b. (a -> b) -> [a] -> [b]
map Arg -> Names
argAliases [Arg]
args)
              else forall a. Maybe a
Nothing
          params' :: [(VName, NameInfo (Aliases rep))]
params' =
            [(forall dec. Param dec -> VName
paramName Param (LParamInfo rep)
param, forall rep. LParamInfo rep -> NameInfo rep
LParamName forall a b. (a -> b) -> a -> b
$ forall dec. Param dec -> dec
paramDec Param (LParamInfo rep)
param) | Param (LParamInfo rep)
param <- [LParam (Aliases rep)]
params]
      forall rep.
Checkable rep =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
checkFun'
        (Name
fname, forall u. [TypeBase Shape u] -> [TypeBase ExtShape u]
staticShapes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall shape.
TypeBase shape NoUniqueness
-> Uniqueness -> TypeBase shape Uniqueness
`toDecl` Uniqueness
Nonunique) [Type]
rettype, [(VName, NameInfo (Aliases rep))]
params')
        Maybe [(VName, Names)]
consumable
        forall a b. (a -> b) -> a -> b
$ do
          forall rep. Checkable rep => [LParam rep] -> TypeM rep ()
checkLambdaParams [LParam (Aliases rep)]
params
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType [Type]
rettype
          forall rep.
Checkable rep =>
[Type] -> Body (Aliases rep) -> TypeM rep [Names]
checkLambdaBody [Type]
rettype Body (Aliases rep)
body
    else
      forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
        String
"Anonymous function defined with "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [LParam (Aliases rep)]
params)
          forall a. [a] -> [a] -> [a]
++ String
" parameters:\n"
          forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty [LParam (Aliases rep)]
params
          forall a. [a] -> [a] -> [a]
++ String
"\nbut expected to take "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg]
args)
          forall a. [a] -> [a] -> [a]
++ String
" arguments."

checkLambda :: Checkable rep => Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkLambda :: forall rep.
Checkable rep =>
Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkLambda = forall rep.
Checkable rep =>
Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkAnyLambda Bool
True

checkPrimExp :: Checkable rep => PrimExp VName -> TypeM rep ()
checkPrimExp :: forall rep. Checkable rep => PrimExp VName -> TypeM rep ()
checkPrimExp ValueExp {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkPrimExp (LeafExp VName
v PrimType
pt) = forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [forall shape u. PrimType -> TypeBase shape u
Prim PrimType
pt] VName
v
checkPrimExp (BinOpExp BinOp
op PrimExp VName
x PrimExp VName
y) = do
  forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (BinOp -> PrimType
binOpType BinOp
op) PrimExp VName
x
  forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (BinOp -> PrimType
binOpType BinOp
op) PrimExp VName
y
checkPrimExp (CmpOpExp CmpOp
op PrimExp VName
x PrimExp VName
y) = do
  forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (CmpOp -> PrimType
cmpOpType CmpOp
op) PrimExp VName
x
  forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (CmpOp -> PrimType
cmpOpType CmpOp
op) PrimExp VName
y
checkPrimExp (UnOpExp UnOp
op PrimExp VName
x) = forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (UnOp -> PrimType
unOpType UnOp
op) PrimExp VName
x
checkPrimExp (ConvOpExp ConvOp
op PrimExp VName
x) = forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ ConvOp -> (PrimType, PrimType)
convOpType ConvOp
op) PrimExp VName
x
checkPrimExp (FunExp String
h [PrimExp VName]
args PrimType
t) = do
  ([PrimType]
h_ts, PrimType
h_ret, [PrimValue] -> Maybe PrimValue
_) <-
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (forall rep a. ErrorCase rep -> TypeM rep a
bad forall a b. (a -> b) -> a -> b
$ forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$ String
"Unknown function: " forall a. [a] -> [a] -> [a]
++ String
h)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
      forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
h Map String ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
primFuns
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimType]
h_ts forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimExp VName]
args) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
    String
"Function expects "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimType]
h_ts)
      forall a. [a] -> [a] -> [a]
++ String
" parameters, but given "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimExp VName]
args)
      forall a. [a] -> [a] -> [a]
++ String
" arguments."
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrimType
h_ret forall a. Eq a => a -> a -> Bool
/= PrimType
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
    String
"Function return annotation is "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty PrimType
t
      forall a. [a] -> [a] -> [a]
++ String
", but expected "
      forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty PrimType
h_ret
  forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp [PrimType]
h_ts [PrimExp VName]
args

requirePrimExp :: Checkable rep => PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp :: forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp PrimType
t PrimExp VName
e = forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"in PrimExp " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty PrimExp VName
e) forall a b. (a -> b) -> a -> b
$ do
  forall rep. Checkable rep => PrimExp VName -> TypeM rep ()
checkPrimExp PrimExp VName
e
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall v. PrimExp v -> PrimType
primExpType PrimExp VName
e forall a. Eq a => a -> a -> Bool
== PrimType
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep a. ErrorCase rep -> TypeM rep a
bad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rep. String -> ErrorCase rep
TypeError forall a b. (a -> b) -> a -> b
$
    forall a. Pretty a => a -> String
pretty PrimExp VName
e forall a. [a] -> [a] -> [a]
++ String
" must have type " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
pretty PrimType
t

class ASTRep rep => CheckableOp rep where
  checkOp :: OpWithAliases (Op rep) -> TypeM rep ()
  -- ^ Used at top level; can be locally changed with 'checkOpWith'.

-- | The class of representations that can be type-checked.
class (ASTRep rep, CanBeAliased (Op rep), CheckableOp rep) => Checkable rep where
  checkExpDec :: ExpDec rep -> TypeM rep ()
  checkBodyDec :: BodyDec rep -> TypeM rep ()
  checkFParamDec :: VName -> FParamInfo rep -> TypeM rep ()
  checkLParamDec :: VName -> LParamInfo rep -> TypeM rep ()
  checkLetBoundDec :: VName -> LetDec rep -> TypeM rep ()
  checkRetType :: [RetType rep] -> TypeM rep ()
  matchPat :: Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()
  primFParam :: VName -> PrimType -> TypeM rep (FParam (Aliases rep))
  matchReturnType :: [RetType rep] -> Result -> TypeM rep ()
  matchBranchType :: [BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
  matchLoopResult :: [FParam (Aliases rep)] -> Result -> TypeM rep ()

  default checkExpDec :: ExpDec rep ~ () => ExpDec rep -> TypeM rep ()
  checkExpDec = forall (f :: * -> *) a. Applicative f => a -> f a
pure

  default checkBodyDec :: BodyDec rep ~ () => BodyDec rep -> TypeM rep ()
  checkBodyDec = forall (f :: * -> *) a. Applicative f => a -> f a
pure

  default checkFParamDec :: FParamInfo rep ~ DeclType => VName -> FParamInfo rep -> TypeM rep ()
  checkFParamDec VName
_ = forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType

  default checkLParamDec :: LParamInfo rep ~ Type => VName -> LParamInfo rep -> TypeM rep ()
  checkLParamDec VName
_ = forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType

  default checkLetBoundDec :: LetDec rep ~ Type => VName -> LetDec rep -> TypeM rep ()
  checkLetBoundDec VName
_ = forall rep u. Checkable rep => TypeBase Shape u -> TypeM rep ()
checkType

  default checkRetType :: RetType rep ~ DeclExtType => [RetType rep] -> TypeM rep ()
  checkRetType = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a b. (a -> b) -> a -> b
$ forall rep u. Checkable rep => TypeBase ExtShape u -> TypeM rep ()
checkExtType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. DeclExtTyped t => t -> DeclExtType
declExtTypeOf

  default matchPat :: Pat (LetDec (Aliases rep)) -> Exp (Aliases rep) -> TypeM rep ()
  matchPat Pat (LetDec (Aliases rep))
pat = forall rep.
Checkable rep =>
Pat (LetDec (Aliases rep)) -> [ExtType] -> TypeM rep ()
matchExtPat Pat (LetDec (Aliases rep))
pat forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall rep (m :: * -> *).
(HasScope rep m, TypedOp (Op rep)) =>
Exp rep -> m [ExtType]
expExtType

  default primFParam :: FParamInfo rep ~ DeclType => VName -> PrimType -> TypeM rep (FParam (Aliases rep))
  primFParam VName
name PrimType
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dec. Attrs -> VName -> dec -> Param dec
Param forall a. Monoid a => a
mempty VName
name (forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t)

  default matchReturnType :: RetType rep ~ DeclExtType => [RetType rep] -> Result -> TypeM rep ()
  matchReturnType = forall rep. Checkable rep => [ExtType] -> Result -> TypeM rep ()
matchExtReturnType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall shape.
TypeBase shape Uniqueness -> TypeBase shape NoUniqueness
fromDecl

  default matchBranchType :: BranchType rep ~ ExtType => [BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
  matchBranchType = forall rep.
Checkable rep =>
[ExtType] -> Body (Aliases rep) -> TypeM rep ()
matchExtBranchType

  default matchLoopResult ::
    FParamInfo rep ~ DeclType =>
    [FParam (Aliases rep)] ->
    Result ->
    TypeM rep ()
  matchLoopResult = forall rep.
Checkable rep =>
[Param DeclType] -> Result -> TypeM rep ()
matchLoopResultExt