{-# 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.TypeCheck
  ( -- * Interface
    checkProg,
    TypeError (..),
    ErrorCase (..),

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

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

import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Parallel.Strategies
import Data.Bifunctor (second)
import Data.List (find, intercalate, isPrefixOf, sort)
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 (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" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg
  show (UnexpectedType Exp rep
e Type
_ []) =
    String
"Type of expression\n"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Doc -> String
prettyDoc Int
160 (Int -> Doc -> Doc
indent Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Exp rep -> Doc
forall a. Pretty a => a -> Doc
ppr Exp rep
e)
      String -> ShowS
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"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Doc -> String
prettyDoc Int
160 (Int -> Doc -> Doc
indent Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Exp rep -> Doc
forall a. Pretty a => a -> Doc
ppr Exp rep
e)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nmust be one of "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
forall a. Pretty a => a -> String
pretty [Type]
ts)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but is "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
pretty Type
t
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (ReturnTypeError Name
fname [ExtType]
rettype [ExtType]
bodytype) =
    String
"Declaration of function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" declares return type\n  "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ExtType] -> String
forall a. Pretty a => [a] -> String
prettyTuple [ExtType]
rettype
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nBut body has type\n  "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ExtType] -> String
forall a. Pretty a => [a] -> String
prettyTuple [ExtType]
bodytype
  show (DupDefinitionError Name
name) =
    String
"Duplicate definition of function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
""
  show (DupParamError Name
funname VName
paramname) =
    String
"Parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
paramname
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" mentioned multiple times in argument list of function "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
funname
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (DupPatError VName
name) =
    String
"Variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bound twice in pattern."
  show (InvalidPatError Pat (Aliases rep)
pat [ExtType]
t Maybe String
desc) =
    String
"Pat\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ PatT (VarAliases, LetDec rep) -> String
forall a. Pretty a => a -> String
pretty PatT (VarAliases, LetDec rep)
Pat (Aliases rep)
pat
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\ncannot match value of type\n"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ExtType] -> String
forall a. Pretty a => [a] -> String
prettyTupleLines [ExtType]
t
      String -> ShowS
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" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
desc'
  show (UnknownVariableError VName
name) =
    String
"Use of unknown variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (UnknownFunctionError Name
fname) =
    String
"Call of unknown function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (ParameterMismatch Maybe Name
fname [Type]
expected [Type]
got) =
    String
"In call of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fname' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\n"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"expecting "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nexpected
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arguments of type(s)\n"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
forall a. Pretty a => a -> String
pretty [Type]
expected)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nGot "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
ngot
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arguments of types\n"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
forall a. Pretty a => a -> String
pretty [Type]
got)
    where
      nexpected :: Int
nexpected = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
expected
      ngot :: Int
ngot = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
got
      fname' :: String
fname' = String -> (Name -> String) -> Maybe Name -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"anonymous function" ((String
"function " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameToString) Maybe Name
fname
  show (SlicingError Int
dims Int
got) =
    Int -> String
forall a. Show a => a -> String
show Int
got String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" indices given, but type of indexee has " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
dims String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" dimension(s)."
  show (BadAnnotation String
desc Type
expected Type
got) =
    String
"Annotation of \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
desc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" type of expression is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
pretty Type
expected
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but derived to be "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
pretty Type
got
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (ReturnAliased Name
fname VName
name) =
    String
"Unique return value of function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is aliased to "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
name
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", which is not consumed."
  show (UniqueReturnAliased Name
fname) =
    String
"A unique tuple element of return value of function "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is aliased to some other tuple component."
  show (NotAnArray VName
e Type
t) =
    String
"The expression " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
e
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is expected to be an array, but is "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
pretty Type
t
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  show (PermutationError [Int]
perm Int
rank Maybe VName
name) =
    String
"The permutation (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int]
perm)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") is not valid for array "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name'
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"of rank "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
rank
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    where
      name' :: String
name' = String -> (VName -> String) -> Maybe VName -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") ShowS -> (VName -> String) -> VName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> String
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) =
    ErrorCase rep -> String
forall a. Show a => a -> String
show ErrorCase rep
err
  show (Error [String]
msgs ErrorCase rep
err) =
    String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
msgs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ErrorCase rep -> String
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
(Usage -> Usage -> Bool) -> (Usage -> Usage -> Bool) -> Eq Usage
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
Eq Usage
-> (Usage -> Usage -> Ordering)
-> (Usage -> Usage -> Bool)
-> (Usage -> Usage -> Bool)
-> (Usage -> Usage -> Bool)
-> (Usage -> Usage -> Bool)
-> (Usage -> Usage -> Usage)
-> (Usage -> Usage -> Usage)
-> Ord 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
$cp1Ord :: Eq Usage
Ord, Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
(Int -> Usage -> ShowS)
-> (Usage -> String) -> ([Usage] -> ShowS) -> Show Usage
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
(Occurence -> Occurence -> Bool)
-> (Occurence -> Occurence -> Bool) -> Eq Occurence
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
(Int -> Occurence -> ShowS)
-> (Occurence -> String)
-> ([Occurence] -> ShowS)
-> Show Occurence
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 = (Names -> Names -> Occurence) -> Names -> Names -> Occurence
forall a b c. (a -> b -> c) -> b -> a -> c
flip Names -> Names -> Occurence
Occurence Names
forall a. Monoid a => a
mempty

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

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

type Occurences = [Occurence]

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

seqOccurences :: Occurences -> Occurences -> Occurences
seqOccurences :: [Occurence] -> [Occurence] -> [Occurence]
seqOccurences [Occurence]
occurs1 [Occurence]
occurs2 =
  (Occurence -> Bool) -> [Occurence] -> [Occurence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Occurence -> Bool) -> Occurence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) ((Occurence -> Occurence) -> [Occurence] -> [Occurence]
forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Occurence
filt [Occurence]
occurs1) [Occurence] -> [Occurence] -> [Occurence]
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 =
  (Occurence -> Bool) -> [Occurence] -> [Occurence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Occurence -> Bool) -> Occurence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) ((Occurence -> Occurence) -> [Occurence] -> [Occurence]
forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Occurence
filt [Occurence]
occurs1) [Occurence] -> [Occurence] -> [Occurence]
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 = (Occurence -> Bool) -> [Occurence] -> [Occurence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Occurence -> Bool) -> Occurence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurence -> Bool
nullOccurence) ([Occurence] -> [Occurence])
-> ([Occurence] -> [Occurence]) -> [Occurence] -> [Occurence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Occurence -> Occurence) -> [Occurence] -> [Occurence]
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
(Int -> Consumption -> ShowS)
-> (Consumption -> String)
-> ([Consumption] -> ShowS)
-> Show Consumption
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 (Names -> [VName]) -> Names -> [VName]
forall a b. (a -> b) -> a -> b
$ Names
consumed_in_o1 Names -> Names -> Names
`namesIntersection` Names
used_in_o2 =
      String -> Consumption
ConsumptionError (String -> Consumption) -> String -> Consumption
forall a b. (a -> b) -> a -> b
$ String
"Variable " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VName -> String
forall a. Pretty a => a -> String
pretty VName
v String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" referenced after being consumed."
    | Bool
otherwise =
      [Occurence] -> Consumption
Consumption ([Occurence] -> Consumption) -> [Occurence] -> Consumption
forall a b. (a -> b) -> a -> b
$ [Occurence]
o1 [Occurence] -> [Occurence] -> [Occurence]
`seqOccurences` [Occurence]
o2
    where
      consumed_in_o1 :: Names
consumed_in_o1 = [Names] -> Names
forall a. Monoid a => [a] -> a
mconcat ([Names] -> Names) -> [Names] -> Names
forall a b. (a -> b) -> a -> b
$ (Occurence -> Names) -> [Occurence] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
consumed [Occurence]
o1
      used_in_o2 :: Names
used_in_o2 = [Names] -> Names
forall a. Monoid a => [a] -> a
mconcat ([Names] -> Names) -> [Names] -> Names
forall a b. (a -> b) -> a -> b
$ (Occurence -> Names) -> [Occurence] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
consumed [Occurence]
o2 [Names] -> [Names] -> [Names]
forall a. Semigroup a => a -> a -> a
<> (Occurence -> Names) -> [Occurence] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map Occurence -> Names
observed [Occurence]
o2

instance Monoid Consumption where
  mempty :: Consumption
mempty = [Occurence] -> Consumption
Consumption [Occurence]
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
  { Env rep -> Map VName (VarBinding rep)
envVtable :: M.Map VName (VarBinding rep),
    Env rep -> Map Name (FunBinding rep)
envFtable :: M.Map Name (FunBinding rep),
    Env rep -> OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp :: OpWithAliases (Op rep) -> TypeM 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
    ( Applicative (TypeM rep)
a -> TypeM rep a
Applicative (TypeM rep)
-> (forall a b. TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b)
-> (forall a b. TypeM rep a -> TypeM rep b -> TypeM rep b)
-> (forall a. a -> TypeM rep a)
-> Monad (TypeM rep)
TypeM rep a -> (a -> TypeM rep b) -> TypeM rep b
TypeM rep a -> TypeM rep b -> TypeM rep b
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 :: a -> TypeM rep a
$creturn :: forall rep a. a -> TypeM rep a
>> :: TypeM rep a -> TypeM rep b -> TypeM rep b
$c>> :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep 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
$cp1Monad :: forall rep. Applicative (TypeM rep)
Monad,
      a -> TypeM rep b -> TypeM rep a
(a -> b) -> TypeM rep a -> TypeM rep b
(forall a b. (a -> b) -> TypeM rep a -> TypeM rep b)
-> (forall a b. a -> TypeM rep b -> TypeM rep a)
-> Functor (TypeM rep)
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
<$ :: a -> TypeM rep b -> TypeM rep a
$c<$ :: forall rep a b. a -> TypeM rep b -> TypeM rep a
fmap :: (a -> b) -> TypeM rep a -> TypeM rep b
$cfmap :: forall rep a b. (a -> b) -> TypeM rep a -> TypeM rep b
Functor,
      Functor (TypeM rep)
a -> TypeM rep a
Functor (TypeM rep)
-> (forall a. a -> TypeM rep a)
-> (forall 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 a b. TypeM rep a -> TypeM rep b -> TypeM rep b)
-> (forall a b. TypeM rep a -> TypeM rep b -> TypeM rep a)
-> Applicative (TypeM rep)
TypeM rep a -> TypeM rep b -> TypeM rep b
TypeM rep a -> TypeM rep b -> TypeM rep a
TypeM rep (a -> b) -> TypeM rep a -> TypeM rep b
(a -> b -> c) -> TypeM rep a -> TypeM rep b -> TypeM rep c
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
<* :: TypeM rep a -> TypeM rep b -> TypeM rep a
$c<* :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep a
*> :: TypeM rep a -> TypeM rep b -> TypeM rep b
$c*> :: forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep b
liftA2 :: (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
<*> :: 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 :: a -> TypeM rep a
$cpure :: forall rep a. a -> TypeM rep a
$cp1Applicative :: forall rep. Functor (TypeM rep)
Applicative,
      MonadReader (Env rep),
      MonadState TState
    )

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

runTypeM ::
  Env rep ->
  TypeM rep a ->
  Either (TypeError rep) (a, Consumption)
runTypeM :: Env rep -> TypeM rep a -> Either (TypeError rep) (a, Consumption)
runTypeM Env rep
env (TypeM ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a
m) =
  (TState -> Consumption) -> (a, TState) -> (a, Consumption)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second TState -> Consumption
stateCons ((a, TState) -> (a, Consumption))
-> Either (TypeError rep) (a, TState)
-> Either (TypeError rep) (a, Consumption)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TState (Either (TypeError rep)) a
-> TState -> Either (TypeError rep) (a, TState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ReaderT (Env rep) (StateT TState (Either (TypeError rep))) a
-> Env rep -> StateT TState (Either (TypeError rep)) a
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 Names
forall a. Monoid a => a
mempty Consumption
forall a. Monoid a => a
mempty)

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

tell :: Consumption -> TypeM rep ()
tell :: Consumption -> TypeM rep ()
tell Consumption
cons = (TState -> TState) -> TypeM rep ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TState -> TState) -> TypeM rep ())
-> (TState -> TState) -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = TState -> Consumption
stateCons TState
s Consumption -> Consumption -> Consumption
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 :: String -> TypeM rep a -> TypeM rep a
context String
s = (Env rep -> Env rep) -> TypeM rep a -> TypeM rep a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Env rep -> Env rep) -> TypeM rep a -> TypeM rep a)
-> (Env rep -> Env rep) -> TypeM rep a -> TypeM rep a
forall a b. (a -> b) -> a -> b
$ \Env rep
env -> Env rep
env {envContext :: [String]
envContext = String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Env rep -> [String]
forall rep. Env rep -> [String]
envContext Env rep
env}

message ::
  Pretty a =>
  String ->
  a ->
  String
message :: String -> a -> String
message String
s a
x =
  Int -> Doc -> String
prettyDoc Int
80 (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$
    String -> Doc
text String
s Doc -> Doc -> Doc
<+> Doc -> Doc
align (a -> Doc
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 :: VName -> TypeM rep ()
bound VName
name = do
  Bool
already_seen <- (TState -> Bool) -> TypeM rep Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((TState -> Bool) -> TypeM rep Bool)
-> (TState -> Bool) -> TypeM rep Bool
forall a b. (a -> b) -> a -> b
$ VName -> Names -> Bool
nameIn VName
name (Names -> Bool) -> (TState -> Names) -> TState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TState -> Names
stateNames
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
already_seen (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$ String
"Name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bound twice"
  (TState -> TState) -> TypeM rep ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TState -> TState) -> TypeM rep ())
-> (TState -> TState) -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateNames :: Names
stateNames = VName -> Names
oneName VName
name Names -> Names -> Names
forall a. Semigroup a => a -> a -> a
<> TState -> Names
stateNames TState
s}

occur :: Occurences -> TypeM rep ()
occur :: [Occurence] -> TypeM rep ()
occur = Consumption -> TypeM rep ()
forall rep. Consumption -> TypeM rep ()
tell (Consumption -> TypeM rep ())
-> ([Occurence] -> Consumption) -> [Occurence] -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Occurence] -> Consumption
Consumption ([Occurence] -> Consumption)
-> ([Occurence] -> [Occurence]) -> [Occurence] -> Consumption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Occurence -> Bool) -> [Occurence] -> [Occurence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Occurence -> Bool) -> Occurence -> Bool
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 :: VName -> TypeM rep ()
observe VName
name = do
  NameInfo (Aliases rep)
dec <- VName -> TypeM rep (NameInfo (Aliases rep))
forall rep. VName -> TypeM rep (NameInfo (Aliases rep))
lookupVar VName
name
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
forall shape u. TypeBase shape u -> Bool
primType (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ NameInfo (Aliases rep) -> Type
forall t. Typed t => t -> Type
typeOf NameInfo (Aliases rep)
dec) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    [Occurence] -> TypeM rep ()
forall rep. [Occurence] -> TypeM rep ()
occur [Names -> Occurence
observation (Names -> Occurence) -> Names -> Occurence
forall a b. (a -> b) -> a -> b
$ VName -> Names
oneName VName
name Names -> Names -> Names
forall a. Semigroup a => a -> a -> a
<> NameInfo (Aliases rep) -> Names
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 :: Names -> TypeM rep ()
consume Names
als = do
  Scope (Aliases rep)
scope <- TypeM rep (Scope (Aliases rep))
forall rep (m :: * -> *). HasScope rep m => m (Scope rep)
askScope
  let isArray :: VName -> Bool
isArray = Bool
-> (NameInfo (Aliases rep) -> Bool)
-> Maybe (NameInfo (Aliases rep))
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not (Bool -> Bool)
-> (NameInfo (Aliases rep) -> Bool)
-> NameInfo (Aliases rep)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
forall shape u. TypeBase shape u -> Bool
primType (Type -> Bool)
-> (NameInfo (Aliases rep) -> Type)
-> NameInfo (Aliases rep)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameInfo (Aliases rep) -> Type
forall t. Typed t => t -> Type
typeOf) (Maybe (NameInfo (Aliases rep)) -> Bool)
-> (VName -> Maybe (NameInfo (Aliases rep))) -> VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> Scope (Aliases rep) -> Maybe (NameInfo (Aliases rep))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Scope (Aliases rep)
scope)
  [Occurence] -> TypeM rep ()
forall rep. [Occurence] -> TypeM rep ()
occur [Names -> Occurence
consumption (Names -> Occurence) -> Names -> Occurence
forall a b. (a -> b) -> a -> b
$ [VName] -> Names
namesFromList ([VName] -> Names) -> [VName] -> Names
forall a b. (a -> b) -> a -> b
$ (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
isArray ([VName] -> [VName]) -> [VName] -> [VName]
forall a b. (a -> b) -> a -> b
$ Names -> [VName]
namesToList Names
als]

collectOccurences :: TypeM rep a -> TypeM rep (a, Occurences)
collectOccurences :: TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m = do
  Consumption
old <- (TState -> Consumption) -> TypeM rep Consumption
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TState -> Consumption
stateCons
  (TState -> TState) -> TypeM rep ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TState -> TState) -> TypeM rep ())
-> (TState -> TState) -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = Consumption
forall a. Monoid a => a
mempty}
  a
x <- TypeM rep a
m
  Consumption
new <- (TState -> Consumption) -> TypeM rep Consumption
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TState -> Consumption
stateCons
  (TState -> TState) -> TypeM rep ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TState -> TState) -> TypeM rep ())
-> (TState -> TState) -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ \TState
s -> TState
s {stateCons :: Consumption
stateCons = Consumption
old}
  [Occurence]
o <- Consumption -> TypeM rep [Occurence]
forall rep. Consumption -> TypeM rep [Occurence]
checkConsumption Consumption
new
  (a, [Occurence]) -> TypeM rep (a, [Occurence])
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 :: (OpWithAliases (Op rep) -> TypeM rep ())
-> TypeM rep a -> TypeM rep a
checkOpWith OpWithAliases (Op rep) -> TypeM rep ()
checker = (Env rep -> Env rep) -> TypeM rep a -> TypeM rep a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Env rep -> Env rep) -> TypeM rep a -> TypeM rep a)
-> (Env rep -> Env rep) -> TypeM rep a -> TypeM rep a
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 :: Consumption -> TypeM rep [Occurence]
checkConsumption (ConsumptionError String
e) = ErrorCase rep -> TypeM rep [Occurence]
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep [Occurence])
-> ErrorCase rep -> TypeM rep [Occurence]
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError String
e
checkConsumption (Consumption [Occurence]
os) = [Occurence] -> TypeM rep [Occurence]
forall (m :: * -> *) a. Monad m => a -> m a
return [Occurence]
os

alternative :: TypeM rep a -> TypeM rep b -> TypeM rep (a, b)
alternative :: TypeM rep a -> TypeM rep b -> TypeM rep (a, b)
alternative TypeM rep a
m1 TypeM rep b
m2 = do
  (a
x, [Occurence]
os1) <- TypeM rep a -> TypeM rep (a, [Occurence])
forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m1
  (b
y, [Occurence]
os2) <- TypeM rep b -> TypeM rep (b, [Occurence])
forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep b
m2
  Consumption -> TypeM rep ()
forall rep. Consumption -> TypeM rep ()
tell (Consumption -> TypeM rep ()) -> Consumption -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ [Occurence] -> Consumption
Consumption ([Occurence] -> Consumption) -> [Occurence] -> Consumption
forall a b. (a -> b) -> a -> b
$ [Occurence]
os1 [Occurence] -> [Occurence] -> [Occurence]
`altOccurences` [Occurence]
os2
  (a, b) -> TypeM rep (a, b)
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 :: [(VName, Names)] -> TypeM rep a -> TypeM rep a
consumeOnlyParams [(VName, Names)]
consumable TypeM rep a
m = do
  (a
x, [Occurence]
os) <- TypeM rep a -> TypeM rep (a, [Occurence])
forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m
  Consumption -> TypeM rep ()
forall rep. Consumption -> TypeM rep ()
tell (Consumption -> TypeM rep ())
-> ([Occurence] -> Consumption) -> [Occurence] -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Occurence] -> Consumption
Consumption ([Occurence] -> TypeM rep ())
-> TypeM rep [Occurence] -> TypeM rep ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Occurence -> TypeM rep Occurence)
-> [Occurence] -> TypeM rep [Occurence]
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
  a -> TypeM rep a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  where
    inspect :: Occurence -> TypeM rep Occurence
inspect Occurence
o = do
      Names
new_consumed <- [Names] -> Names
forall a. Monoid a => [a] -> a
mconcat ([Names] -> Names) -> TypeM rep [Names] -> TypeM rep Names
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VName -> TypeM rep Names) -> [VName] -> TypeM rep [Names]
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 (Names -> [VName]) -> Names -> [VName]
forall a b. (a -> b) -> a -> b
$ Occurence -> Names
consumed Occurence
o)
      Occurence -> TypeM rep Occurence
forall (m :: * -> *) a. Monad m => a -> m a
return Occurence
o {consumed :: Names
consumed = Names
new_consumed}
    wasConsumed :: VName -> TypeM rep Names
wasConsumed VName
v
      | Just Names
als <- VName -> [(VName, Names)] -> Maybe Names
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v [(VName, Names)]
consumable = Names -> TypeM rep Names
forall (m :: * -> *) a. Monad m => a -> m a
return Names
als
      | Bool
otherwise =
        ErrorCase rep -> TypeM rep Names
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep Names)
-> ErrorCase rep -> TypeM rep Names
forall a b. (a -> b) -> a -> b
$
          String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
            [String] -> String
unlines
              [ VName -> String
forall a. Pretty a => a -> String
pretty VName
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" was invalidly consumed.",
                String
what String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" can be consumed here."
              ]
    what :: String
what
      | [(VName, Names)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(VName, Names)]
consumable = String
"Nothing"
      | Bool
otherwise = String
"Only " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((VName, Names) -> String) -> [(VName, Names)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (VName -> String
forall a. Pretty a => a -> String
pretty (VName -> String)
-> ((VName, Names) -> VName) -> (VName, Names) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, Names) -> VName
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 :: Names -> Env rep -> Names
expandAliases Names
names Env rep
env = Names
names Names -> Names -> Names
forall a. Semigroup a => a -> a -> a
<> Names
aliasesOfAliases
  where
    aliasesOfAliases :: Names
aliasesOfAliases = [Names] -> Names
forall a. Monoid a => [a] -> a
mconcat ([Names] -> Names) -> (Names -> [Names]) -> Names -> Names
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> Names) -> [VName] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map VName -> Names
look ([VName] -> [Names]) -> (Names -> [VName]) -> Names -> [Names]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Names -> [VName]
namesToList (Names -> Names) -> Names -> Names
forall a b. (a -> b) -> a -> b
$ Names
names
    look :: VName -> Names
look VName
k = case VName -> Map VName (VarBinding rep) -> Maybe (VarBinding rep)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k (Map VName (VarBinding rep) -> Maybe (VarBinding rep))
-> Map VName (VarBinding rep) -> Maybe (VarBinding rep)
forall a b. (a -> b) -> a -> b
$ Env rep -> Map VName (VarBinding rep)
forall rep. Env rep -> Map VName (VarBinding rep)
envVtable Env rep
env of
      Just (LetName (als, _)) -> VarAliases -> Names
unAliases VarAliases
als
      Maybe (VarBinding rep)
_ -> Names
forall a. Monoid a => a
mempty

binding ::
  Checkable rep =>
  Scope (Aliases rep) ->
  TypeM rep a ->
  TypeM rep a
binding :: Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding Scope (Aliases rep)
stms = TypeM rep a -> TypeM rep a
check (TypeM rep a -> TypeM rep a)
-> (TypeM rep a -> TypeM rep a) -> TypeM rep a -> TypeM rep a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Env rep -> Env rep) -> TypeM rep a -> TypeM rep a
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 = (Env rep -> VName -> NameInfo (Aliases rep) -> Env rep)
-> Env rep -> Scope (Aliases rep) -> Env rep
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
M.foldlWithKey' Env rep -> VName -> NameInfo (Aliases rep) -> Env rep
forall rep.
Typed (LetDec rep) =>
Env rep -> VName -> NameInfo (Aliases rep) -> Env rep
bindVar
    boundnames :: [VName]
boundnames = Scope (Aliases rep) -> [VName]
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 als, dec)) =
      let als' :: Names
als'
            | Type -> Bool
forall shape u. TypeBase shape u -> Bool
primType (LetDec rep -> Type
forall t. Typed t => t -> Type
typeOf LetDec rep
dec) = Names
forall a. Monoid a => a
mempty
            | Bool
otherwise = Names -> Env rep -> Names
forall rep. Names -> Env rep -> Names
expandAliases Names
als Env rep
env
       in Env rep
env
            { envVtable :: Map VName (NameInfo (Aliases rep))
envVtable =
                VName
-> NameInfo (Aliases rep)
-> Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name (LetDec (Aliases rep) -> NameInfo (Aliases rep)
forall rep. LetDec rep -> NameInfo rep
LetName (Names -> VarAliases
AliasDec Names
als', LetDec rep
dec)) (Map VName (NameInfo (Aliases rep))
 -> Map VName (NameInfo (Aliases rep)))
-> Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
forall a b. (a -> b) -> a -> b
$ Env rep -> Map VName (NameInfo (Aliases rep))
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 = VName
-> NameInfo (Aliases rep)
-> Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name NameInfo (Aliases rep)
dec (Map VName (NameInfo (Aliases rep))
 -> Map VName (NameInfo (Aliases rep)))
-> Map VName (NameInfo (Aliases rep))
-> Map VName (NameInfo (Aliases rep))
forall a b. (a -> b) -> a -> b
$ Env rep -> Map VName (NameInfo (Aliases rep))
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
      (VName -> TypeM rep ()) -> [VName] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> TypeM rep ()
forall rep. VName -> TypeM rep ()
bound ([VName] -> TypeM rep ()) -> [VName] -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ Scope (Aliases rep) -> [VName]
forall k a. Map k a -> [k]
M.keys Scope (Aliases rep)
stms
      (a
a, [Occurence]
os) <- TypeM rep a -> TypeM rep (a, [Occurence])
forall rep a. TypeM rep a -> TypeM rep (a, [Occurence])
collectOccurences TypeM rep a
m
      Consumption -> TypeM rep ()
forall rep. Consumption -> TypeM rep ()
tell (Consumption -> TypeM rep ()) -> Consumption -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ [Occurence] -> Consumption
Consumption ([Occurence] -> Consumption) -> [Occurence] -> Consumption
forall a b. (a -> b) -> a -> b
$ Names -> [Occurence] -> [Occurence]
unOccur ([VName] -> Names
namesFromList [VName]
boundnames) [Occurence]
os
      a -> TypeM rep a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

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

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

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

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

lookupFun ::
  Checkable rep =>
  Name ->
  [SubExp] ->
  TypeM rep ([RetType rep], [DeclType])
lookupFun :: Name -> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
lookupFun Name
fname [SubExp]
args = do
  Maybe ([RetType rep], [Param (FParamInfo rep)])
stm <- (Env rep -> Maybe ([RetType rep], [Param (FParamInfo rep)]))
-> TypeM rep (Maybe ([RetType rep], [Param (FParamInfo rep)]))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Env rep -> Maybe ([RetType rep], [Param (FParamInfo rep)]))
 -> TypeM rep (Maybe ([RetType rep], [Param (FParamInfo rep)])))
-> (Env rep -> Maybe ([RetType rep], [Param (FParamInfo rep)]))
-> TypeM rep (Maybe ([RetType rep], [Param (FParamInfo rep)]))
forall a b. (a -> b) -> a -> b
$ Name
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
-> Maybe ([RetType rep], [Param (FParamInfo rep)])
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
fname (Map Name ([RetType rep], [Param (FParamInfo rep)])
 -> Maybe ([RetType rep], [Param (FParamInfo rep)]))
-> (Env rep -> Map Name ([RetType rep], [Param (FParamInfo rep)]))
-> Env rep
-> Maybe ([RetType rep], [Param (FParamInfo rep)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env rep -> Map Name ([RetType rep], [Param (FParamInfo rep)])
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 -> ErrorCase rep -> TypeM rep ([RetType rep], [DeclType])
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ([RetType rep], [DeclType]))
-> ErrorCase rep -> TypeM rep ([RetType rep], [DeclType])
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase rep
forall rep. Name -> ErrorCase rep
UnknownFunctionError Name
fname
    Just ([RetType rep]
ftype, [Param (FParamInfo rep)]
params) -> do
      [Type]
argts <- (SubExp -> TypeM rep Type) -> [SubExp] -> TypeM rep [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM rep Type
forall t (m :: * -> *). HasScope t m => SubExp -> m Type
subExpType [SubExp]
args
      case [RetType rep]
-> [Param (FParamInfo rep)]
-> [(SubExp, Type)]
-> Maybe [RetType rep]
forall rt dec.
(IsRetType rt, Typed dec) =>
[rt] -> [Param dec] -> [(SubExp, Type)] -> Maybe [rt]
applyRetType [RetType rep]
ftype [Param (FParamInfo rep)]
params ([(SubExp, Type)] -> Maybe [RetType rep])
-> [(SubExp, Type)] -> Maybe [RetType rep]
forall a b. (a -> b) -> a -> b
$ [SubExp] -> [Type] -> [(SubExp, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SubExp]
args [Type]
argts of
        Maybe [RetType rep]
Nothing ->
          ErrorCase rep -> TypeM rep ([RetType rep], [DeclType])
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ([RetType rep], [DeclType]))
-> ErrorCase rep -> TypeM rep ([RetType rep], [DeclType])
forall a b. (a -> b) -> a -> b
$ Maybe Name -> [Type] -> [Type] -> ErrorCase rep
forall rep. Maybe Name -> [Type] -> [Type] -> ErrorCase rep
ParameterMismatch (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fname) ((Param (FParamInfo rep) -> Type)
-> [Param (FParamInfo rep)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Param (FParamInfo rep) -> Type
forall dec. Typed dec => Param dec -> Type
paramType [Param (FParamInfo rep)]
params) [Type]
argts
        Just [RetType rep]
rt ->
          ([RetType rep], [DeclType])
-> TypeM rep ([RetType rep], [DeclType])
forall (m :: * -> *) a. Monad m => a -> m a
return ([RetType rep]
rt, (Param (FParamInfo rep) -> DeclType)
-> [Param (FParamInfo rep)] -> [DeclType]
forall a b. (a -> b) -> [a] -> [b]
map Param (FParamInfo rep) -> DeclType
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 :: String -> Type -> Type -> TypeM rep ()
checkAnnotation String
desc Type
t1 Type
t2
  | Type
t2 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t1 = () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ String -> Type -> Type -> ErrorCase rep
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 :: [Type] -> SubExp -> TypeM rep ()
require [Type]
ts SubExp
se = do
  Type
t <- SubExp -> TypeM rep Type
forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
se
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
t Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
ts) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ Exp rep -> Type -> [Type] -> ErrorCase rep
forall rep. Exp rep -> Type -> [Type] -> ErrorCase rep
UnexpectedType (BasicOp -> Exp rep
forall rep. BasicOp -> ExpT rep
BasicOp (BasicOp -> Exp rep) -> BasicOp -> Exp rep
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 :: [Type] -> VName -> TypeM rep ()
requireI [Type]
ts VName
ident = [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [Type]
ts (SubExp -> TypeM rep ()) -> SubExp -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
ident

checkArrIdent ::
  Checkable rep =>
  VName ->
  TypeM rep Type
checkArrIdent :: VName -> TypeM rep Type
checkArrIdent VName
v = do
  Type
t <- VName -> TypeM rep Type
forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
v
  case Type
t of
    Array {} -> Type -> TypeM rep Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    Type
_ -> ErrorCase rep -> TypeM rep Type
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep Type)
-> ErrorCase rep -> TypeM rep Type
forall a b. (a -> b) -> a -> b
$ VName -> Type -> ErrorCase rep
forall rep. VName -> Type -> ErrorCase rep
NotAnArray VName
v Type
t

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

-- | 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 :: Prog (Aliases rep) -> Either (TypeError rep) ()
checkProg (Prog Stms (Aliases rep)
consts [FunDef (Aliases rep)]
funs) = do
  let typeenv :: Env rep
typeenv =
        Env :: forall rep.
Map VName (VarBinding rep)
-> Map Name (FunBinding rep)
-> (OpWithAliases (Op rep) -> TypeM rep ())
-> [String]
-> Env rep
Env
          { envVtable :: Map VName (VarBinding rep)
envVtable = Map VName (VarBinding rep)
forall k a. Map k a
M.empty,
            envFtable :: Map Name (FunBinding rep)
envFtable = Map Name (FunBinding rep)
forall a. Monoid a => a
mempty,
            envContext :: [String]
envContext = [],
            envCheckOp :: OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp = OpWithAliases (Op rep) -> TypeM rep ()
forall rep.
CheckableOp rep =>
OpWithAliases (Op rep) -> TypeM rep ()
checkOp
          }
  let 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 =
        (((), Consumption) -> ())
-> Either (TypeError rep) ((), Consumption)
-> Either (TypeError rep) ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), Consumption) -> ()
forall a b. (a, b) -> a
fst (Either (TypeError rep) ((), Consumption)
 -> Either (TypeError rep) ())
-> Either (TypeError rep) ((), Consumption)
-> Either (TypeError rep) ()
forall a b. (a -> b) -> a -> b
$
          Env rep -> TypeM rep () -> Either (TypeError rep) ((), Consumption)
forall rep a.
Env rep -> TypeM rep a -> Either (TypeError rep) (a, Consumption)
runTypeM Env rep
typeenv (TypeM rep () -> Either (TypeError rep) ((), Consumption))
-> TypeM rep () -> Either (TypeError rep) ((), Consumption)
forall a b. (a -> b) -> a -> b
$
            (Env rep -> Env rep) -> TypeM rep () -> TypeM rep ()
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)])
Map Name (FunBinding rep)
ftable, envVtable :: Map VName (VarBinding rep)
envVtable = Map VName (VarBinding rep)
vtable}) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
              FunDef (Aliases rep) -> TypeM rep ()
forall rep. Checkable rep => FunDef (Aliases rep) -> TypeM rep ()
checkFun FunDef (Aliases rep)
fun
  (Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable, Consumption
_) <- Env rep
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
-> Either
     (TypeError rep)
     (Map Name ([RetType rep], [Param (FParamInfo rep)]), Consumption)
forall rep a.
Env rep -> TypeM rep a -> Either (TypeError rep) (a, Consumption)
runTypeM Env rep
typeenv TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
buildFtable
  (Map VName (VarBinding rep)
vtable, Consumption
_) <-
    Env rep
-> TypeM rep (Map VName (VarBinding rep))
-> Either (TypeError rep) (Map VName (VarBinding rep), Consumption)
forall rep a.
Env rep -> TypeM rep a -> Either (TypeError rep) (a, Consumption)
runTypeM Env rep
typeenv {envFtable :: Map Name (FunBinding rep)
envFtable = Map Name ([RetType rep], [Param (FParamInfo rep)])
Map Name (FunBinding rep)
ftable} (TypeM rep (Map VName (VarBinding rep))
 -> Either
      (TypeError rep) (Map VName (VarBinding rep), Consumption))
-> TypeM rep (Map VName (VarBinding rep))
-> Either (TypeError rep) (Map VName (VarBinding rep), Consumption)
forall a b. (a -> b) -> a -> b
$
      Stms (Aliases rep)
-> TypeM rep (Map VName (VarBinding rep))
-> TypeM rep (Map VName (VarBinding rep))
forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms Stms (Aliases rep)
consts (TypeM rep (Map VName (VarBinding rep))
 -> TypeM rep (Map VName (VarBinding rep)))
-> TypeM rep (Map VName (VarBinding rep))
-> TypeM rep (Map VName (VarBinding rep))
forall a b. (a -> b) -> a -> b
$ (Env rep -> Map VName (VarBinding rep))
-> TypeM rep (Map VName (VarBinding rep))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env rep -> Map VName (VarBinding rep)
forall rep. Env rep -> Map VName (VarBinding rep)
envVtable
  [Either (TypeError rep) ()] -> Either (TypeError rep) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([Either (TypeError rep) ()] -> Either (TypeError rep) ())
-> [Either (TypeError rep) ()] -> Either (TypeError rep) ()
forall a b. (a -> b) -> a -> b
$ Strategy (Either (TypeError rep) ())
-> (FunDef (Aliases rep) -> Either (TypeError rep) ())
-> [FunDef (Aliases rep)]
-> [Either (TypeError rep) ()]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (Either (TypeError rep) ())
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 <- TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall rep. Checkable rep => TypeM rep (Map Name (FunBinding rep))
initialFtable
      (Map Name ([RetType rep], [Param (FParamInfo rep)])
 -> FunDef (Aliases rep)
 -> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)])))
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
-> [FunDef (Aliases rep)]
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Name ([RetType rep], [Param (FParamInfo rep)])
-> FunDef (Aliases rep)
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
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 BodyT rep
_)
      | Name -> Map Name ([RetType rep], [Param (FParamInfo rep)]) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member Name
name Map Name ([RetType rep], [Param (FParamInfo rep)])
ftable =
        ErrorCase rep
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep
 -> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)])))
-> ErrorCase rep
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase rep
forall rep. Name -> ErrorCase rep
DupDefinitionError Name
name
      | Bool
otherwise =
        Map Name ([RetType rep], [Param (FParamInfo rep)])
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Name ([RetType rep], [Param (FParamInfo rep)])
 -> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)])))
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall a b. (a -> b) -> a -> b
$ Name
-> ([RetType rep], [Param (FParamInfo rep)])
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
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 :: TypeM rep (Map Name (FunBinding rep))
initialFtable = ([(Name, ([RetType rep], [Param (FParamInfo rep)]))]
 -> Map Name ([RetType rep], [Param (FParamInfo rep)]))
-> TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
-> Map Name ([RetType rep], [Param (FParamInfo rep)])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
 -> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)])))
-> TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
-> TypeM rep (Map Name ([RetType rep], [Param (FParamInfo rep)]))
forall a b. (a -> b) -> a -> b
$ ((Name, (PrimType, [PrimType]))
 -> TypeM rep (Name, ([RetType rep], [Param (FParamInfo rep)])))
-> [(Name, (PrimType, [PrimType]))]
-> TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, (PrimType, [PrimType]))
-> TypeM rep (Name, ([RetType rep], [Param (FParamInfo rep)]))
forall (t :: * -> *) rep a a.
(Traversable t, Checkable rep, IsRetType a) =>
(a, (PrimType, t PrimType))
-> TypeM rep (a, ([a], t (Param (FParamInfo rep))))
addBuiltin ([(Name, (PrimType, [PrimType]))]
 -> TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))])
-> [(Name, (PrimType, [PrimType]))]
-> TypeM rep [(Name, ([RetType rep], [Param (FParamInfo rep)]))]
forall a b. (a -> b) -> a -> b
$ Map Name (PrimType, [PrimType]) -> [(Name, (PrimType, [PrimType]))]
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 <- (PrimType -> TypeM rep (Param (FParamInfo rep)))
-> t PrimType -> TypeM rep (t (Param (FParamInfo rep)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (VName -> PrimType -> TypeM rep (FParam (Aliases rep))
forall rep.
Checkable rep =>
VName -> PrimType -> TypeM rep (FParam (Aliases rep))
primFParam VName
name) t PrimType
ts
      (a, ([a], t (Param (FParamInfo rep))))
-> TypeM rep (a, ([a], t (Param (FParamInfo rep))))
forall (m :: * -> *) a. Monad m => a -> m a
return (a
fname, ([PrimType -> a
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 :: FunDef (Aliases rep) -> TypeM rep ()
checkFun (FunDef Maybe EntryPoint
_ Attrs
_ Name
fname [RetType (Aliases rep)]
rettype [FParam (Aliases rep)]
params BodyT (Aliases rep)
body) =
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"In function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameToString Name
fname) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    (Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
forall rep.
Checkable rep =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases rep))])
-> Maybe [(VName, Names)] -> TypeM rep [Names] -> TypeM rep ()
checkFun'
      ( Name
fname,
        (RetType rep -> DeclExtType) -> [RetType rep] -> [DeclExtType]
forall a b. (a -> b) -> [a] -> [b]
map RetType rep -> DeclExtType
forall t. DeclExtTyped t => t -> DeclExtType
declExtTypeOf [RetType rep]
[RetType (Aliases rep)]
rettype,
        [FParam rep] -> [(VName, NameInfo (Aliases rep))]
forall rep. [FParam rep] -> [(VName, NameInfo (Aliases rep))]
funParamsToNameInfos [FParam rep]
[FParam (Aliases rep)]
params
      )
      ([(VName, Names)] -> Maybe [(VName, Names)]
forall a. a -> Maybe a
Just [(VName, Names)]
consumable)
      (TypeM rep [Names] -> TypeM rep ())
-> TypeM rep [Names] -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ do
        [FParam rep] -> TypeM rep ()
forall rep. Checkable rep => [FParam rep] -> TypeM rep ()
checkFunParams [FParam rep]
[FParam (Aliases rep)]
params
        [RetType rep] -> TypeM rep ()
forall rep. Checkable rep => [RetType rep] -> TypeM rep ()
checkRetType [RetType rep]
[RetType (Aliases rep)]
rettype
        String -> TypeM rep [Names] -> TypeM rep [Names]
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking function body" (TypeM rep [Names] -> TypeM rep [Names])
-> TypeM rep [Names] -> TypeM rep [Names]
forall a b. (a -> b) -> a -> b
$ [RetType rep] -> BodyT (Aliases rep) -> TypeM rep [Names]
forall rep.
Checkable rep =>
[RetType rep] -> Body (Aliases rep) -> TypeM rep [Names]
checkFunBody [RetType rep]
[RetType (Aliases rep)]
rettype BodyT (Aliases rep)
body
  where
    consumable :: [(VName, Names)]
consumable =
      [ (FParam rep -> VName
forall dec. Param dec -> VName
paramName FParam rep
param, Names
forall a. Monoid a => a
mempty)
        | FParam rep
param <- [FParam rep]
[FParam (Aliases rep)]
params,
          DeclType -> Bool
forall shape. TypeBase shape Uniqueness -> Bool
unique (DeclType -> Bool) -> DeclType -> Bool
forall a b. (a -> b) -> a -> b
$ FParam rep -> DeclType
forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType FParam rep
param
      ]

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

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

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

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

    checkNoDuplicateParams :: TypeM rep ()
checkNoDuplicateParams = ([VName] -> VName -> TypeM rep [VName])
-> [VName] -> [VName] -> TypeM rep ()
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
_ <- (VName -> Bool) -> [VName] -> Maybe VName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
pname) [VName]
seen =
        ErrorCase rep -> TypeM rep [VName]
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep [VName])
-> ErrorCase rep -> TypeM rep [VName]
forall a b. (a -> b) -> a -> b
$ Name -> VName -> ErrorCase rep
forall rep. Name -> VName -> ErrorCase rep
DupParamError Name
fname VName
pname
      | Bool
otherwise =
        [VName] -> TypeM rep [VName]
forall (m :: * -> *) a. Monad m => a -> m a
return ([VName] -> TypeM rep [VName]) -> [VName] -> TypeM rep [VName]
forall a b. (a -> b) -> a -> b
$ VName
pname VName -> [VName] -> [VName]
forall a. a -> [a] -> [a]
: [VName]
seen
    checkReturnAlias :: [Names] -> TypeM rep ()
checkReturnAlias =
      (Set (VName, Uniqueness)
 -> (Uniqueness, Names) -> TypeM rep (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness) -> [(Uniqueness, Names)] -> TypeM rep ()
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' Set (VName, Uniqueness)
forall a. Monoid a => a
mempty ([(Uniqueness, Names)] -> TypeM rep ())
-> ([Names] -> [(Uniqueness, Names)]) -> [Names] -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DeclExtType] -> [Names] -> [(Uniqueness, Names)]
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)
      | (VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` ((VName, Uniqueness) -> VName)
-> Set (VName, Uniqueness) -> Set VName
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (VName, Uniqueness) -> VName
forall a b. (a, b) -> a
fst Set (VName, Uniqueness)
seen) ([VName] -> Bool) -> [VName] -> Bool
forall a b. (a -> b) -> a -> b
$ Names -> [VName]
namesToList Names
names =
        ErrorCase rep -> TypeM rep (Set (VName, Uniqueness))
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep (Set (VName, Uniqueness)))
-> ErrorCase rep -> TypeM rep (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase rep
forall rep. Name -> ErrorCase rep
UniqueReturnAliased Name
fname
      | Bool
otherwise = do
        Names -> TypeM rep ()
forall rep. Checkable rep => Names -> TypeM rep ()
consume Names
names
        Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Set (VName, Uniqueness)
seen Set (VName, Uniqueness)
-> Set (VName, Uniqueness) -> Set (VName, Uniqueness)
forall a. Semigroup a => a -> a -> a
<> Uniqueness -> Names -> Set (VName, Uniqueness)
forall t. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Unique Names
names
    checkReturnAlias' Set (VName, Uniqueness)
seen (Uniqueness
Nonunique, Names
names)
      | ((VName, Uniqueness) -> Bool) -> Set (VName, Uniqueness) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((VName, Uniqueness) -> Set (VName, Uniqueness) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (VName, Uniqueness)
seen) (Set (VName, Uniqueness) -> Bool)
-> Set (VName, Uniqueness) -> Bool
forall a b. (a -> b) -> a -> b
$ Uniqueness -> Names -> Set (VName, Uniqueness)
forall t. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Unique Names
names =
        ErrorCase rep -> TypeM rep (Set (VName, Uniqueness))
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep (Set (VName, Uniqueness)))
-> ErrorCase rep -> TypeM rep (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase rep
forall rep. Name -> ErrorCase rep
UniqueReturnAliased Name
fname
      | Bool
otherwise = Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness) -> TypeM rep (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Set (VName, Uniqueness)
seen Set (VName, Uniqueness)
-> Set (VName, Uniqueness) -> Set (VName, Uniqueness)
forall a. Semigroup a => a -> a -> a
<> Uniqueness -> Names -> Set (VName, Uniqueness)
forall t. Ord t => t -> Names -> Set (VName, t)
tag Uniqueness
Nonunique Names
names

    tag :: t -> Names -> Set (VName, t)
tag t
u = [(VName, t)] -> Set (VName, t)
forall a. Ord a => [a] -> Set a
S.fromList ([(VName, t)] -> Set (VName, t))
-> (Names -> [(VName, t)]) -> Names -> Set (VName, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> (VName, t)) -> [VName] -> [(VName, t)]
forall a b. (a -> b) -> [a] -> [b]
map (,t
u) ([VName] -> [(VName, t)])
-> (Names -> [VName]) -> Names -> [(VName, t)]
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 =
      [(Uniqueness, b)] -> [(Uniqueness, b)]
forall a. [a] -> [a]
reverse ([(Uniqueness, b)] -> [(Uniqueness, b)])
-> [(Uniqueness, b)] -> [(Uniqueness, b)]
forall a b. (a -> b) -> a -> b
$
        [Uniqueness] -> [b] -> [(Uniqueness, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Uniqueness] -> [Uniqueness]
forall a. [a] -> [a]
reverse ((TypeBase shape Uniqueness -> Uniqueness)
-> [TypeBase shape Uniqueness] -> [Uniqueness]
forall a b. (a -> b) -> [a] -> [b]
map TypeBase shape Uniqueness -> Uniqueness
forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness [TypeBase shape Uniqueness]
expected) [Uniqueness] -> [Uniqueness] -> [Uniqueness]
forall a. [a] -> [a] -> [a]
++ Uniqueness -> [Uniqueness]
forall a. a -> [a]
repeat Uniqueness
Nonunique) ([b] -> [(Uniqueness, b)]) -> [b] -> [(Uniqueness, b)]
forall a b. (a -> b) -> a -> b
$
          [b] -> [b]
forall a. [a] -> [a]
reverse [b]
got

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

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

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

checkStms ::
  Checkable rep =>
  Stms (Aliases rep) ->
  TypeM rep a ->
  TypeM rep a
checkStms :: 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 ([Stm (Aliases rep)] -> TypeM rep a)
-> [Stm (Aliases rep)] -> TypeM rep a
forall a b. (a -> b) -> a -> b
$ Stms (Aliases rep) -> [Stm (Aliases rep)]
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 (Aliases rep)
pat StmAux (ExpDec (Aliases rep))
_ Exp (Aliases rep)
e) : [Stm (Aliases rep)]
stms) = do
      String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context (Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Doc
"In expression of statement" Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (PatT (VarAliases, LetDec rep) -> Doc
forall a. Pretty a => a -> Doc
ppr PatT (VarAliases, LetDec rep)
Pat (Aliases rep)
pat)) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
        Exp (Aliases rep) -> TypeM rep ()
forall rep. Checkable rep => Exp (Aliases rep) -> TypeM rep ()
checkExp Exp (Aliases rep)
e
      Stm (Aliases rep) -> TypeM rep a -> TypeM rep a
forall rep a.
Checkable rep =>
Stm (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStm Stm (Aliases rep)
stm (TypeM rep a -> TypeM rep a) -> TypeM rep a -> TypeM rep a
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 :: Result -> TypeM rep ()
checkResult = (SubExpRes -> TypeM rep Type) -> Result -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SubExpRes -> TypeM rep Type
forall rep. Checkable rep => SubExpRes -> TypeM rep Type
checkSubExpRes

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

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

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

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

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

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

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

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

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

  FlatSlice SubExp -> TypeM rep ()
forall rep. Checkable rep => FlatSlice SubExp -> TypeM rep ()
checkFlatSlice FlatSlice SubExp
slice
  [Type] -> VName -> TypeM rep ()
forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [TypeBase Shape Any -> Shape -> NoUniqueness -> Type
forall shape u_unused u.
ArrayShape shape =>
TypeBase shape u_unused -> shape -> u -> TypeBase shape u
arrayOf (PrimType -> TypeBase Shape Any
forall shape u. PrimType -> TypeBase shape u
Prim (Type -> PrimType
forall shape u. TypeBase shape u -> PrimType
elemType Type
src_t)) ([SubExp] -> Shape
forall d. [d] -> ShapeBase d
Shape (FlatSlice SubExp -> [SubExp]
forall d. FlatSlice d -> [d]
flatSliceDims FlatSlice SubExp
slice)) NoUniqueness
NoUniqueness] VName
v
  Names -> TypeM rep ()
forall rep. Checkable rep => Names -> TypeM rep ()
consume (Names -> TypeM rep ()) -> TypeM rep Names -> TypeM rep ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> TypeM rep Names
forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
src
checkBasicOp (Iota SubExp
e SubExp
x SubExp
s IntType
et) = do
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
e
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
et] SubExp
x
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
et] SubExp
s
checkBasicOp (Replicate (Shape [SubExp]
dims) SubExp
valexp) = do
  (SubExp -> TypeM rep ()) -> [SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
dims
  TypeM rep Type -> TypeM rep ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM rep Type -> TypeM rep ()) -> TypeM rep Type -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ SubExp -> TypeM rep Type
forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp SubExp
valexp
checkBasicOp (Scratch PrimType
_ [SubExp]
shape) =
  (SubExp -> TypeM rep Type) -> [SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SubExp -> TypeM rep Type
forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp [SubExp]
shape
checkBasicOp (Reshape ShapeChange SubExp
newshape VName
arrexp) = do
  Int
rank <- Type -> Int
forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank (Type -> Int) -> TypeM rep Type -> TypeM rep Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> TypeM rep Type
forall rep. Checkable rep => VName -> TypeM rep Type
checkArrIdent VName
arrexp
  (DimChange SubExp -> TypeM rep ())
-> ShapeChange SubExp -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] (SubExp -> TypeM rep ())
-> (DimChange SubExp -> SubExp) -> DimChange SubExp -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DimChange SubExp -> SubExp
forall d. DimChange d -> d
newDim) ShapeChange SubExp
newshape
  (DimChange SubExp -> Int -> TypeM rep ())
-> ShapeChange SubExp -> [Int] -> TypeM rep ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Int -> DimChange SubExp -> Int -> TypeM rep ()
checkDimChange Int
rank) ShapeChange SubExp
newshape [Int
0 ..]
  where
    checkDimChange :: Int -> DimChange SubExp -> Int -> TypeM rep ()
checkDimChange Int
_ (DimNew SubExp
_) Int
_ =
      () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkDimChange Int
rank (DimCoercion SubExp
se) Int
i
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
rank =
        ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
          String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
            String
"Asked to coerce dimension " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SubExp -> String
forall a. Pretty a => a -> String
pretty SubExp
se
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but array "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
arrexp
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" has only "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
pretty Int
rank
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" dimensions"
      | Bool
otherwise =
        () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkBasicOp (Rearrange [Int]
perm VName
arr) = do
  Type
arrt <- VName -> TypeM rep Type
forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
  let rank :: Int
rank = Type -> Int
forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
arrt
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
perm Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
rank Bool -> Bool -> Bool
|| [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort [Int]
perm [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Int
0 .. Int
rank Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ [Int] -> Int -> Maybe VName -> ErrorCase rep
forall rep. [Int] -> Int -> Maybe VName -> ErrorCase rep
PermutationError [Int]
perm Int
rank (Maybe VName -> ErrorCase rep) -> Maybe VName -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$ VName -> Maybe VName
forall a. a -> Maybe a
Just VName
arr
checkBasicOp (Rotate [SubExp]
rots VName
arr) = do
  Type
arrt <- VName -> TypeM rep Type
forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
  let rank :: Int
rank = Type -> Int
forall shape u. ArrayShape shape => TypeBase shape u -> Int
arrayRank Type
arrt
  (SubExp -> TypeM rep ()) -> [SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
rots
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
rots Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
rank) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
        String
"Cannot rotate " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
rots)
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" dimensions of "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
rank
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-dimensional array."
checkBasicOp (Concat Int
i VName
arr1exp [VName]
arr2exps SubExp
ressize) = do
  Type
arr1t <- VName -> TypeM rep Type
forall rep. Checkable rep => VName -> TypeM rep Type
checkArrIdent VName
arr1exp
  [Type]
arr2ts <- (VName -> TypeM rep Type) -> [VName] -> TypeM rep [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TypeM rep Type
forall rep. Checkable rep => VName -> TypeM rep Type
checkArrIdent [VName]
arr2exps
  let success :: Bool
success =
        (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
          ( ([SubExp] -> [SubExp] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Int -> [SubExp] -> [SubExp]
forall a. Int -> Int -> [a] -> [a]
dropAt Int
i Int
1 (Type -> [SubExp]
forall u. TypeBase Shape u -> [SubExp]
arrayDims Type
arr1t))
              ([SubExp] -> Bool) -> (Type -> [SubExp]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> [SubExp] -> [SubExp]
forall a. Int -> Int -> [a] -> [a]
dropAt Int
i Int
1
              ([SubExp] -> [SubExp]) -> (Type -> [SubExp]) -> Type -> [SubExp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [SubExp]
forall u. TypeBase Shape u -> [SubExp]
arrayDims
          )
          [Type]
arr2ts
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
success (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
        String
"Types of arguments to concat do not match.  Got "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
pretty Type
arr1t
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Type -> String
forall a. Pretty a => a -> String
pretty [Type]
arr2ts)
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
ressize
checkBasicOp (Copy VName
e) =
  TypeM rep Type -> TypeM rep ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM rep Type -> TypeM rep ()) -> TypeM rep Type -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ VName -> TypeM rep Type
forall rep. Checkable rep => VName -> TypeM rep Type
checkArrIdent VName
e
checkBasicOp (Manifest [Int]
perm VName
arr) =
  BasicOp -> TypeM rep ()
forall rep. Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp (BasicOp -> TypeM rep ()) -> BasicOp -> TypeM rep ()
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
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool] SubExp
e
  (ErrorMsgPart SubExp -> TypeM rep ())
-> [ErrorMsgPart SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ErrorMsgPart SubExp -> TypeM rep ()
forall rep. Checkable rep => ErrorMsgPart SubExp -> TypeM rep ()
checkPart [ErrorMsgPart SubExp]
parts
  where
    checkPart :: ErrorMsgPart SubExp -> TypeM rep ()
checkPart ErrorString {} = () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkPart (ErrorVal PrimType
t SubExp
x) = [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
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) <- VName -> TypeM rep (Shape, [Type])
forall rep. Checkable rep => VName -> TypeM rep (Shape, [Type])
checkAccIdent VName
acc

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

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

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

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

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

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

checkExp ::
  Checkable rep =>
  Exp (Aliases rep) ->
  TypeM rep ()
checkExp :: Exp (Aliases rep) -> TypeM rep ()
checkExp (BasicOp BasicOp
op) = BasicOp -> TypeM rep ()
forall rep. Checkable rep => BasicOp -> TypeM rep ()
checkBasicOp BasicOp
op
checkExp (If SubExp
e1 BodyT (Aliases rep)
e2 BodyT (Aliases rep)
e3 IfDec (BranchType (Aliases rep))
info) = do
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool] SubExp
e1
  ([Names], [Names])
_ <-
    String -> TypeM rep [Names] -> TypeM rep [Names]
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"in true branch" (BodyT (Aliases rep) -> TypeM rep [Names]
forall rep.
Checkable rep =>
Body (Aliases rep) -> TypeM rep [Names]
checkBody BodyT (Aliases rep)
e2)
      TypeM rep [Names]
-> TypeM rep [Names] -> TypeM rep ([Names], [Names])
forall rep a b. TypeM rep a -> TypeM rep b -> TypeM rep (a, b)
`alternative` String -> TypeM rep [Names] -> TypeM rep [Names]
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"in false branch" (BodyT (Aliases rep) -> TypeM rep [Names]
forall rep.
Checkable rep =>
Body (Aliases rep) -> TypeM rep [Names]
checkBody BodyT (Aliases rep)
e3)
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"in true branch" (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ [BranchType rep] -> BodyT (Aliases rep) -> TypeM rep ()
forall rep.
Checkable rep =>
[BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
matchBranchType (IfDec (BranchType rep) -> [BranchType rep]
forall rt. IfDec rt -> [rt]
ifReturns IfDec (BranchType rep)
IfDec (BranchType (Aliases rep))
info) BodyT (Aliases rep)
e2
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"in false branch" (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ [BranchType rep] -> BodyT (Aliases rep) -> TypeM rep ()
forall rep.
Checkable rep =>
[BranchType rep] -> Body (Aliases rep) -> TypeM rep ()
matchBranchType (IfDec (BranchType rep) -> [BranchType rep]
forall rt. IfDec rt -> [rt]
ifReturns IfDec (BranchType rep)
IfDec (BranchType (Aliases rep))
info) BodyT (Aliases rep)
e3
checkExp (Apply Name
fname [(SubExp, Diet)]
args [RetType (Aliases rep)]
rettype_annot (Safety, SrcLoc, [SrcLoc])
_) = do
  ([RetType rep]
rettype_derived, [DeclType]
paramtypes) <- Name -> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
forall rep.
Checkable rep =>
Name -> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
lookupFun Name
fname ([SubExp] -> TypeM rep ([RetType rep], [DeclType]))
-> [SubExp] -> TypeM rep ([RetType rep], [DeclType])
forall a b. (a -> b) -> a -> b
$ ((SubExp, Diet) -> SubExp) -> [(SubExp, Diet)] -> [SubExp]
forall a b. (a -> b) -> [a] -> [b]
map (SubExp, Diet) -> SubExp
forall a b. (a, b) -> a
fst [(SubExp, Diet)]
args
  [Arg]
argflows <- ((SubExp, Diet) -> TypeM rep Arg)
-> [(SubExp, Diet)] -> TypeM rep [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SubExp -> TypeM rep Arg
forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg (SubExp -> TypeM rep Arg)
-> ((SubExp, Diet) -> SubExp) -> (SubExp, Diet) -> TypeM rep Arg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubExp, Diet) -> SubExp
forall a b. (a, b) -> a
fst) [(SubExp, Diet)]
args
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([RetType rep]
rettype_derived [RetType rep] -> [RetType rep] -> Bool
forall a. Eq a => a -> a -> Bool
/= [RetType rep]
[RetType (Aliases rep)]
rettype_annot) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ())
-> (Doc -> ErrorCase rep) -> Doc -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep)
-> (Doc -> String) -> Doc -> ErrorCase rep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> TypeM rep ()) -> Doc -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      Doc
"Expected apply result type:"
        Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 ([RetType rep] -> Doc
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 ([RetType rep] -> Doc
forall a. Pretty a => a -> Doc
ppr [RetType rep]
[RetType (Aliases rep)]
rettype_annot)
  [DeclType] -> [Arg] -> TypeM rep ()
forall rep. [DeclType] -> [Arg] -> TypeM rep ()
consumeArgs [DeclType]
paramtypes [Arg]
argflows
checkExp (DoLoop [(FParam (Aliases rep), SubExp)]
merge LoopForm (Aliases rep)
form BodyT (Aliases rep)
loopbody) = do
  let ([Param (FParamInfo rep)]
mergepat, [SubExp]
mergeexps) = [(Param (FParamInfo rep), SubExp)]
-> ([Param (FParamInfo rep)], [SubExp])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Param (FParamInfo rep), SubExp)]
[(FParam (Aliases rep), SubExp)]
merge
  [Arg]
mergeargs <- (SubExp -> TypeM rep Arg) -> [SubExp] -> TypeM rep [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM rep Arg
forall rep. Checkable rep => SubExp -> TypeM rep Arg
checkArg [SubExp]
mergeexps

  Scope (Aliases rep) -> TypeM rep () -> TypeM rep ()
forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding (LoopForm (Aliases rep) -> Scope (Aliases rep)
forall rep a. Scoped rep a => a -> Scope rep
scopeOf LoopForm (Aliases rep)
form) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
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 = (Param (FParamInfo rep) -> DeclType)
-> [Param (FParamInfo rep)] -> [DeclType]
forall a b. (a -> b) -> [a] -> [b]
map Param (FParamInfo rep) -> DeclType
forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo rep)]
mergepat
        consumable :: [(VName, Names)]
consumable =
          [ (Param (FParamInfo rep) -> VName
forall dec. Param dec -> VName
paramName Param (FParamInfo rep)
param, Names
forall a. Monoid a => a
mempty)
            | Param (FParamInfo rep)
param <- [Param (FParamInfo rep)]
mergepat,
              DeclType -> Bool
forall shape. TypeBase shape Uniqueness -> Bool
unique (DeclType -> Bool) -> DeclType -> Bool
forall a b. (a -> b) -> a -> b
$ Param (FParamInfo rep) -> DeclType
forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType Param (FParamInfo rep)
param
          ]
            [(VName, Names)] -> [(VName, Names)] -> [(VName, Names)]
forall a. [a] -> [a] -> [a]
++ [(VName, Names)]
form_consumable

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

          Stms (Aliases rep) -> TypeM rep [Names] -> TypeM rep [Names]
forall rep a.
Checkable rep =>
Stms (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStms (BodyT (Aliases rep) -> Stms (Aliases rep)
forall rep. BodyT rep -> Stms rep
bodyStms BodyT (Aliases rep)
loopbody) (TypeM rep [Names] -> TypeM rep [Names])
-> TypeM rep [Names] -> TypeM rep [Names]
forall a b. (a -> b) -> a -> b
$ do
            Result -> TypeM rep ()
forall rep. Checkable rep => Result -> TypeM rep ()
checkResult (Result -> TypeM rep ()) -> Result -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ BodyT (Aliases rep) -> Result
forall rep. BodyT rep -> Result
bodyResult BodyT (Aliases rep)
loopbody

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

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

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

  let cert_params :: [Param (LParamInfo rep)]
cert_params = Int -> [Param (LParamInfo rep)] -> [Param (LParamInfo rep)]
forall a. Int -> [a] -> [a]
take Int
num_accs ([Param (LParamInfo rep)] -> [Param (LParamInfo rep)])
-> [Param (LParamInfo rep)] -> [Param (LParamInfo rep)]
forall a b. (a -> b) -> a -> b
$ Lambda (Aliases rep) -> [LParam (Aliases rep)]
forall rep. LambdaT rep -> [LParam rep]
lambdaParams Lambda (Aliases rep)
lam
  [Arg]
acc_args <- [(WithAccInput (Aliases rep), Param (LParamInfo rep))]
-> ((WithAccInput (Aliases rep), Param (LParamInfo rep))
    -> TypeM rep Arg)
-> TypeM rep [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([WithAccInput (Aliases rep)]
-> [Param (LParamInfo rep)]
-> [(WithAccInput (Aliases rep), Param (LParamInfo rep))]
forall a b. [a] -> [b] -> [(a, b)]
zip [WithAccInput (Aliases rep)]
inputs [Param (LParamInfo rep)]
cert_params) (((WithAccInput (Aliases rep), Param (LParamInfo rep))
  -> TypeM rep Arg)
 -> TypeM rep [Arg])
-> ((WithAccInput (Aliases rep), Param (LParamInfo rep))
    -> TypeM rep Arg)
-> TypeM rep [Arg]
forall a b. (a -> b) -> a -> b
$ \((Shape
shape, [VName]
arrs, Maybe (Lambda (Aliases rep), [SubExp])
op), Param (LParamInfo rep)
p) -> do
    (SubExp -> TypeM rep ()) -> [SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) (Shape -> [SubExp]
forall d. ShapeBase d -> [d]
shapeDims Shape
shape)
    [Type]
elem_ts <- [VName] -> (VName -> TypeM rep Type) -> TypeM rep [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VName]
arrs ((VName -> TypeM rep Type) -> TypeM rep [Type])
-> (VName -> TypeM rep Type) -> TypeM rep [Type]
forall a b. (a -> b) -> a -> b
$ \VName
arr -> do
      Type
arr_t <- VName -> TypeM rep Type
forall rep (m :: * -> *). HasScope rep m => VName -> m Type
lookupType VName
arr
      Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Shape -> [SubExp]
forall d. ShapeBase d -> [d]
shapeDims Shape
shape [SubExp] -> [SubExp] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` Type -> [SubExp]
forall u. TypeBase Shape u -> [SubExp]
arrayDims Type
arr_t) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
        ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ())
-> (String -> ErrorCase rep) -> String -> TypeM rep ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> TypeM rep ()) -> String -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ VName -> String
forall a. Pretty a => a -> String
pretty VName
arr String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" is not an array of outer shape " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Shape -> String
forall a. Pretty a => a -> String
pretty Shape
shape
      Names -> TypeM rep ()
forall rep. Checkable rep => Names -> TypeM rep ()
consume (Names -> TypeM rep ()) -> TypeM rep Names -> TypeM rep ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> TypeM rep Names
forall rep. Checkable rep => VName -> TypeM rep Names
lookupAliases VName
arr
      Type -> TypeM rep Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TypeM rep Type) -> Type -> TypeM rep Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Type
forall shape u.
ArrayShape shape =>
Int -> TypeBase shape u -> TypeBase shape u
stripArray (Shape -> Int
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, b
forall a. Monoid a => a
mempty)
        [Type]
nes_ts <- (SubExp -> TypeM rep Type) -> [SubExp] -> TypeM rep [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM rep Type
forall rep. Checkable rep => SubExp -> TypeM rep Type
checkSubExp [SubExp]
nes
        Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
nes_ts [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== Lambda (Aliases rep) -> [Type]
forall rep. LambdaT rep -> [Type]
lambdaReturnType Lambda (Aliases rep)
op_lam) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
          ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
            String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
              [String] -> String
unlines
                [ String
"Accumulator operator return type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
forall a. Pretty a => a -> String
pretty (Lambda (Aliases rep) -> [Type]
forall rep. LambdaT rep -> [Type]
lambdaReturnType Lambda (Aliases rep)
op_lam),
                  String
"Type of neutral elements: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
forall a. Pretty a => a -> String
pretty [Type]
nes_ts
                ]
        Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
forall rep.
Checkable rep =>
Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkLambda Lambda (Aliases rep)
op_lam ([Arg] -> TypeM rep ()) -> [Arg] -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
          Int -> Arg -> [Arg]
forall a. Int -> a -> [a]
replicate (Shape -> Int
forall a. ArrayShape a => a -> Int
shapeRank Shape
shape) (PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64, Names
forall a. Monoid a => a
mempty)
            [Arg] -> [Arg] -> [Arg]
forall a. [a] -> [a] -> [a]
++ (Type -> Arg) -> [Type] -> [Arg]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Arg
forall b a. Monoid b => a -> (a, b)
mkArrArg ([Type]
elem_ts [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
elem_ts)
      Maybe (Lambda (Aliases rep), [SubExp])
Nothing ->
        () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

  Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
forall rep.
Checkable rep =>
Bool -> Lambda (Aliases rep) -> [Arg] -> TypeM rep ()
checkAnyLambda Bool
False Lambda (Aliases rep)
lam ([Arg] -> TypeM rep ()) -> [Arg] -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ Int -> Arg -> [Arg]
forall a. Int -> a -> [a]
replicate Int
num_accs (PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit, Names
forall a. Monoid a => a
mempty) [Arg] -> [Arg] -> [Arg]
forall a. [a] -> [a] -> [a]
++ [Arg]
acc_args
  where
    num_accs :: Int
num_accs = [WithAccInput (Aliases rep)] -> Int
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 <- (Env rep -> OpWithAliases (Op rep) -> TypeM rep ())
-> TypeM rep (OpWithAliases (Op rep) -> TypeM rep ())
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env rep -> OpWithAliases (Op rep) -> TypeM rep ()
forall rep. Env rep -> OpWithAliases (Op rep) -> TypeM rep ()
envCheckOp
  OpWithAliases (Op rep) -> TypeM rep ()
checker Op (Aliases rep)
OpWithAliases (Op rep)
op

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

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

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

checkCmpOp ::
  Checkable rep =>
  CmpOp ->
  SubExp ->
  SubExp ->
  TypeM rep ()
checkCmpOp :: CmpOp -> SubExp -> SubExp -> TypeM rep ()
checkCmpOp (CmpEq PrimType
t) SubExp
x SubExp
y = do
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
x
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
y
checkCmpOp (CmpUlt IntType
t) SubExp
x SubExp
y = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 = PrimType -> SubExp -> SubExp -> TypeM rep ()
forall rep.
Checkable rep =>
PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs PrimType
Bool SubExp
x SubExp
y
checkCmpOp CmpOp
CmpLle SubExp
x SubExp
y = PrimType -> SubExp -> SubExp -> TypeM rep ()
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 :: PrimType -> SubExp -> SubExp -> TypeM rep ()
checkBinOpArgs PrimType
t SubExp
e1 SubExp
e2 = do
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
e1
  [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t] SubExp
e2

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

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

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

checkDimIndex ::
  Checkable rep =>
  DimIndex SubExp ->
  TypeM rep ()
checkDimIndex :: DimIndex SubExp -> TypeM rep ()
checkDimIndex (DimFix SubExp
i) = [Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
i
checkDimIndex (DimSlice SubExp
i SubExp
n SubExp
s) = (SubExp -> TypeM rep ()) -> [SubExp] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM rep ()
forall rep. Checkable rep => [Type] -> SubExp -> TypeM rep ()
require [PrimType -> Type
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 :: Stm (Aliases rep) -> TypeM rep a -> TypeM rep a
checkStm stm :: Stm (Aliases rep)
stm@(Let Pat (Aliases rep)
pat (StmAux (Certs [VName]
cs) Attrs
_ (_, dec)) Exp (Aliases rep)
e) TypeM rep a
m = do
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking certificates" (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ (VName -> TypeM rep ()) -> [VName] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> VName -> TypeM rep ()
forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Unit]) [VName]
cs
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context String
"When checking expression annotation" (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ ExpDec rep -> TypeM rep ()
forall rep. Checkable rep => ExpDec rep -> TypeM rep ()
checkExpDec ExpDec rep
dec
  String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"When matching\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> PatT (VarAliases, LetDec rep) -> String
forall a. Pretty a => String -> a -> String
message String
"  " PatT (VarAliases, LetDec rep)
Pat (Aliases rep)
pat String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nwith\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Exp (Aliases rep) -> String
forall a. Pretty a => String -> a -> String
message String
"  " Exp (Aliases rep)
e) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    Pat (Aliases rep) -> Exp (Aliases rep) -> TypeM rep ()
forall rep.
Checkable rep =>
Pat (Aliases rep) -> Exp (Aliases rep) -> TypeM rep ()
matchPat Pat (Aliases rep)
pat Exp (Aliases rep)
e
  Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
forall rep a.
Checkable rep =>
Scope (Aliases rep) -> TypeM rep a -> TypeM rep a
binding (Scope (Aliases rep) -> Scope (Aliases rep)
maybeWithoutAliases (Scope (Aliases rep) -> Scope (Aliases rep))
-> Scope (Aliases rep) -> Scope (Aliases rep)
forall a b. (a -> b) -> a -> b
$ Stm (Aliases rep) -> Scope (Aliases rep)
forall rep a. Scoped rep a => a -> Scope rep
scopeOf Stm (Aliases rep)
stm) (TypeM rep a -> TypeM rep a) -> TypeM rep a -> TypeM rep a
forall a b. (a -> b) -> a -> b
$ do
    (PatElemT (LetDec rep) -> TypeM rep ())
-> [PatElemT (LetDec rep)] -> TypeM rep ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PatElemT (LetDec rep) -> TypeM rep ()
forall rep. Checkable rep => PatElemT (LetDec rep) -> TypeM rep ()
checkPatElem (PatT (LetDec rep) -> [PatElemT (LetDec rep)]
forall dec. PatT dec -> [PatElemT dec]
patElems (PatT (LetDec rep) -> [PatElemT (LetDec rep)])
-> PatT (LetDec rep) -> [PatElemT (LetDec rep)]
forall a b. (a -> b) -> a -> b
$ PatT (VarAliases, LetDec rep) -> PatT (LetDec rep)
forall a. PatT (VarAliases, a) -> PatT a
removePatAliases PatT (VarAliases, LetDec rep)
Pat (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 :: Scope (Aliases rep) -> Scope (Aliases rep)
maybeWithoutAliases =
      case Stm (Aliases rep) -> Exp (Aliases rep)
forall rep. Stm rep -> Exp rep
stmExp Stm (Aliases rep)
stm of
        Apply {} -> (NameInfo (Aliases rep) -> NameInfo (Aliases rep))
-> Scope (Aliases rep) -> Scope (Aliases rep)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map NameInfo (Aliases rep) -> NameInfo (Aliases rep)
forall a rep b.
(Monoid a, LetDec rep ~ (a, b)) =>
NameInfo rep -> NameInfo rep
withoutAliases
        Exp (Aliases rep)
_ -> Scope (Aliases rep) -> Scope (Aliases rep)
forall a. a -> a
id
    withoutAliases :: NameInfo rep -> NameInfo rep
withoutAliases (LetName (_, ldec)) = LetDec rep -> NameInfo rep
forall rep. LetDec rep -> NameInfo rep
LetName (a
forall a. Monoid a => a
mempty, b
ldec)
    withoutAliases NameInfo rep
info = NameInfo rep
info

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

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

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

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

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

  let ctx_vals :: [(SubExpRes, Type)]
ctx_vals = Result -> [Type] -> [(SubExpRes, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip Result
res [Type]
ts
      instantiateExt :: Int -> TypeM rep SubExp
instantiateExt Int
i = case Int -> [(SubExpRes, Type)] -> Maybe (SubExpRes, Type)
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)) -> SubExp -> TypeM rep SubExp
forall (m :: * -> *) a. Monad m => a -> m a
return SubExp
se
        Maybe (SubExpRes, Type)
_ -> TypeM rep SubExp
forall rep a. TypeM rep a
problem

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

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

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

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

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

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

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

checkPrimExp :: Checkable rep => PrimExp VName -> TypeM rep ()
checkPrimExp :: PrimExp VName -> TypeM rep ()
checkPrimExp ValueExp {} = () -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkPrimExp (LeafExp VName
v PrimType
pt) = [Type] -> VName -> TypeM rep ()
forall rep. Checkable rep => [Type] -> VName -> TypeM rep ()
requireI [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
pt] VName
v
checkPrimExp (BinOpExp BinOp
op PrimExp VName
x PrimExp VName
y) = do
  PrimType -> PrimExp VName -> TypeM rep ()
forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (BinOp -> PrimType
binOpType BinOp
op) PrimExp VName
x
  PrimType -> PrimExp VName -> TypeM rep ()
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
  PrimType -> PrimExp VName -> TypeM rep ()
forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp (CmpOp -> PrimType
cmpOpType CmpOp
op) PrimExp VName
x
  PrimType -> PrimExp VName -> TypeM rep ()
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) = PrimType -> PrimExp VName -> TypeM rep ()
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) = PrimType -> PrimExp VName -> TypeM rep ()
forall rep.
Checkable rep =>
PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp ((PrimType, PrimType) -> PrimType
forall a b. (a, b) -> a
fst ((PrimType, PrimType) -> PrimType)
-> (PrimType, PrimType) -> PrimType
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
_) <-
    TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> (([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
    -> TypeM
         rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (ErrorCase rep
-> TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep
 -> TypeM
      rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> ErrorCase rep
-> TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$ String
"Unknown function: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
h)
      ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall (m :: * -> *) a. Monad m => a -> m a
return
      (Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
 -> TypeM
      rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> TypeM rep ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall a b. (a -> b) -> a -> b
$ String
-> Map
     String ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
h Map String ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
primFuns
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([PrimType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimType]
h_ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [PrimExp VName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimExp VName]
args) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
        String
"Function expects " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([PrimType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimType]
h_ts)
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" parameters, but given "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([PrimExp VName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PrimExp VName]
args)
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arguments."
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrimType
h_ret PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
/= PrimType
t) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
        String
"Function return annotation is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PrimType -> String
forall a. Pretty a => a -> String
pretty PrimType
t
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but expected "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ PrimType -> String
forall a. Pretty a => a -> String
pretty PrimType
h_ret
  (PrimType -> PrimExp VName -> TypeM rep ())
-> [PrimType] -> [PrimExp VName] -> TypeM rep ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ PrimType -> PrimExp VName -> TypeM rep ()
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 :: PrimType -> PrimExp VName -> TypeM rep ()
requirePrimExp PrimType
t PrimExp VName
e = String -> TypeM rep () -> TypeM rep ()
forall rep a. String -> TypeM rep a -> TypeM rep a
context (String
"in PrimExp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PrimExp VName -> String
forall a. Pretty a => a -> String
pretty PrimExp VName
e) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$ do
  PrimExp VName -> TypeM rep ()
forall rep. Checkable rep => PrimExp VName -> TypeM rep ()
checkPrimExp PrimExp VName
e
  Bool -> TypeM rep () -> TypeM rep ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrimExp VName -> PrimType
forall v. PrimExp v -> PrimType
primExpType PrimExp VName
e PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
== PrimType
t) (TypeM rep () -> TypeM rep ()) -> TypeM rep () -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase rep -> TypeM rep ()
forall rep a. ErrorCase rep -> TypeM rep a
bad (ErrorCase rep -> TypeM rep ()) -> ErrorCase rep -> TypeM rep ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase rep
forall rep. String -> ErrorCase rep
TypeError (String -> ErrorCase rep) -> String -> ErrorCase rep
forall a b. (a -> b) -> a -> b
$
        PrimExp VName -> String
forall a. Pretty a => a -> String
pretty PrimExp VName
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" must have type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PrimType -> String
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 (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 = ExpDec rep -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return

  default checkBodyDec :: BodyDec rep ~ () => BodyDec rep -> TypeM rep ()
  checkBodyDec = BodyDec rep -> TypeM rep ()
forall (m :: * -> *) a. Monad m => a -> m a
return

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

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

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

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

  default matchPat :: Pat (Aliases rep) -> Exp (Aliases rep) -> TypeM rep ()
  matchPat Pat (Aliases rep)
pat = Pat (Aliases rep) -> [ExtType] -> TypeM rep ()
forall rep.
Checkable rep =>
Pat (Aliases rep) -> [ExtType] -> TypeM rep ()
matchExtPat Pat (Aliases rep)
pat ([ExtType] -> TypeM rep ())
-> (Exp (Aliases rep) -> TypeM rep [ExtType])
-> Exp (Aliases rep)
-> TypeM rep ()
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Exp (Aliases rep) -> TypeM rep [ExtType]
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 = Param DeclType -> TypeM rep (Param DeclType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Param DeclType -> TypeM rep (Param DeclType))
-> Param DeclType -> TypeM rep (Param DeclType)
forall a b. (a -> b) -> a -> b
$ Attrs -> VName -> DeclType -> Param DeclType
forall dec. Attrs -> VName -> dec -> Param dec
Param Attrs
forall a. Monoid a => a
mempty VName
name (PrimType -> DeclType
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t)

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

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

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