{-# 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,
    checkExp,
    checkStms,
    checkStm,
    checkType,
    checkExtType,
    matchExtPattern,
    matchExtBranchType,
    argType,
    argAliases,
    noArgAliases,
    checkArg,
    checkSOACArrayArgs,
    checkLambda,
    checkBody,
    consume,
    consumeOnlyParams,
    binding,
    alternative,
  )
where

import Control.Monad.RWS.Strict
import Control.Parallel.Strategies
import Data.List (find, intercalate, 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 lore
  = TypeError String
  | UnexpectedType (Exp lore) Type [Type]
  | ReturnTypeError Name [ExtType] [ExtType]
  | DupDefinitionError Name
  | DupParamError Name VName
  | DupPatternError VName
  | InvalidPatternError (Pattern (Aliases lore)) [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 lore => Show (ErrorCase lore) where
  show :: ErrorCase lore -> String
show (TypeError String
msg) =
    String
"Type error:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg
  show (UnexpectedType Exp lore
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 lore -> Doc
forall a. Pretty a => a -> Doc
ppr Exp lore
e)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\ncannot have any type - possibly a bug in the type checker."
  show (UnexpectedType Exp lore
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 lore -> Doc
forall a. Pretty a => a -> Doc
ppr Exp lore
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 (DupPatternError 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 (InvalidPatternError Pattern (Aliases lore)
pat [ExtType]
t Maybe String
desc) =
    String
"Pattern " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PatternT (VarAliases, LetDec lore) -> String
forall a. Pretty a => a -> String
pretty PatternT (VarAliases, LetDec lore)
Pattern (Aliases lore)
pat
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" cannot match value of type "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ExtType] -> String
forall a. Pretty a => [a] -> String
prettyTuple [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 lore = Error [String] (ErrorCase lore)

instance Checkable lore => Show (TypeError lore) where
  show :: TypeError lore -> String
show (Error [] ErrorCase lore
err) =
    ErrorCase lore -> String
forall a. Show a => a -> String
show ErrorCase lore
err
  show (Error [String]
msgs ErrorCase lore
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 lore -> String
forall a. Show a => a -> String
show ErrorCase lore
err

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

type VarBinding lore = NameInfo (Aliases lore)

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 lore = Env
  { Env lore -> Map VName (VarBinding lore)
envVtable :: M.Map VName (VarBinding lore),
    Env lore -> Map Name (FunBinding lore)
envFtable :: M.Map Name (FunBinding lore),
    Env lore -> OpWithAliases (Op lore) -> TypeM lore ()
envCheckOp :: OpWithAliases (Op lore) -> TypeM lore (),
    Env lore -> [String]
envContext :: [String]
  }

-- | The type checker runs in this monad.
newtype TypeM lore a
  = TypeM
      ( RWST
          (Env lore) -- Reader
          Consumption -- Writer
          Names -- State
          (Either (TypeError lore)) -- Inner monad
          a
      )
  deriving
    ( Applicative (TypeM lore)
a -> TypeM lore a
Applicative (TypeM lore)
-> (forall a b.
    TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b)
-> (forall a b. TypeM lore a -> TypeM lore b -> TypeM lore b)
-> (forall a. a -> TypeM lore a)
-> Monad (TypeM lore)
TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b
TypeM lore a -> TypeM lore b -> TypeM lore b
forall lore. Applicative (TypeM lore)
forall a. a -> TypeM lore a
forall lore a. a -> TypeM lore a
forall a b. TypeM lore a -> TypeM lore b -> TypeM lore b
forall a b. TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b
forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore b
forall lore a b.
TypeM lore a -> (a -> TypeM lore b) -> TypeM lore 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 lore a
$creturn :: forall lore a. a -> TypeM lore a
>> :: TypeM lore a -> TypeM lore b -> TypeM lore b
$c>> :: forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore b
>>= :: TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b
$c>>= :: forall lore a b.
TypeM lore a -> (a -> TypeM lore b) -> TypeM lore b
$cp1Monad :: forall lore. Applicative (TypeM lore)
Monad,
      a -> TypeM lore b -> TypeM lore a
(a -> b) -> TypeM lore a -> TypeM lore b
(forall a b. (a -> b) -> TypeM lore a -> TypeM lore b)
-> (forall a b. a -> TypeM lore b -> TypeM lore a)
-> Functor (TypeM lore)
forall a b. a -> TypeM lore b -> TypeM lore a
forall a b. (a -> b) -> TypeM lore a -> TypeM lore b
forall lore a b. a -> TypeM lore b -> TypeM lore a
forall lore a b. (a -> b) -> TypeM lore a -> TypeM lore b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TypeM lore b -> TypeM lore a
$c<$ :: forall lore a b. a -> TypeM lore b -> TypeM lore a
fmap :: (a -> b) -> TypeM lore a -> TypeM lore b
$cfmap :: forall lore a b. (a -> b) -> TypeM lore a -> TypeM lore b
Functor,
      Functor (TypeM lore)
a -> TypeM lore a
Functor (TypeM lore)
-> (forall a. a -> TypeM lore a)
-> (forall a b.
    TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b)
-> (forall a b c.
    (a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c)
-> (forall a b. TypeM lore a -> TypeM lore b -> TypeM lore b)
-> (forall a b. TypeM lore a -> TypeM lore b -> TypeM lore a)
-> Applicative (TypeM lore)
TypeM lore a -> TypeM lore b -> TypeM lore b
TypeM lore a -> TypeM lore b -> TypeM lore a
TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b
(a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c
forall lore. Functor (TypeM lore)
forall a. a -> TypeM lore a
forall lore a. a -> TypeM lore a
forall a b. TypeM lore a -> TypeM lore b -> TypeM lore a
forall a b. TypeM lore a -> TypeM lore b -> TypeM lore b
forall a b. TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b
forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore a
forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore b
forall lore a b.
TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b
forall a b c.
(a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c
forall lore a b c.
(a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore 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 lore a -> TypeM lore b -> TypeM lore a
$c<* :: forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore a
*> :: TypeM lore a -> TypeM lore b -> TypeM lore b
$c*> :: forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore b
liftA2 :: (a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c
$cliftA2 :: forall lore a b c.
(a -> b -> c) -> TypeM lore a -> TypeM lore b -> TypeM lore c
<*> :: TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b
$c<*> :: forall lore a b.
TypeM lore (a -> b) -> TypeM lore a -> TypeM lore b
pure :: a -> TypeM lore a
$cpure :: forall lore a. a -> TypeM lore a
$cp1Applicative :: forall lore. Functor (TypeM lore)
Applicative,
      MonadReader (Env lore),
      MonadWriter Consumption,
      MonadState Names
    )

instance
  Checkable lore =>
  HasScope (Aliases lore) (TypeM lore)
  where
  lookupType :: VName -> TypeM lore Type
lookupType = (NameInfo (Aliases lore) -> Type)
-> TypeM lore (NameInfo (Aliases lore)) -> TypeM lore Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameInfo (Aliases lore) -> Type
forall t. Typed t => t -> Type
typeOf (TypeM lore (NameInfo (Aliases lore)) -> TypeM lore Type)
-> (VName -> TypeM lore (NameInfo (Aliases lore)))
-> VName
-> TypeM lore Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> TypeM lore (NameInfo (Aliases lore))
forall lore. VName -> TypeM lore (NameInfo (Aliases lore))
lookupVar
  askScope :: TypeM lore (Scope (Aliases lore))
askScope = (Env lore -> Scope (Aliases lore))
-> TypeM lore (Scope (Aliases lore))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Env lore -> Scope (Aliases lore))
 -> TypeM lore (Scope (Aliases lore)))
-> (Env lore -> Scope (Aliases lore))
-> TypeM lore (Scope (Aliases lore))
forall a b. (a -> b) -> a -> b
$ [(VName, NameInfo (Aliases lore))] -> Scope (Aliases lore)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, NameInfo (Aliases lore))] -> Scope (Aliases lore))
-> (Env lore -> [(VName, NameInfo (Aliases lore))])
-> Env lore
-> Scope (Aliases lore)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VName, NameInfo (Aliases lore))
 -> Maybe (VName, NameInfo (Aliases lore)))
-> [(VName, NameInfo (Aliases lore))]
-> [(VName, NameInfo (Aliases lore))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (VName, NameInfo (Aliases lore))
-> Maybe (VName, NameInfo (Aliases lore))
forall a b. (a, b) -> Maybe (a, b)
varType ([(VName, NameInfo (Aliases lore))]
 -> [(VName, NameInfo (Aliases lore))])
-> (Env lore -> [(VName, NameInfo (Aliases lore))])
-> Env lore
-> [(VName, NameInfo (Aliases lore))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope (Aliases lore) -> [(VName, NameInfo (Aliases lore))]
forall k a. Map k a -> [(k, a)]
M.toList (Scope (Aliases lore) -> [(VName, NameInfo (Aliases lore))])
-> (Env lore -> Scope (Aliases lore))
-> Env lore
-> [(VName, NameInfo (Aliases lore))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env lore -> Scope (Aliases lore)
forall lore. Env lore -> Map VName (VarBinding lore)
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 lore ->
  TypeM lore a ->
  Either (TypeError lore) (a, Consumption)
runTypeM :: Env lore
-> TypeM lore a -> Either (TypeError lore) (a, Consumption)
runTypeM Env lore
env (TypeM RWST (Env lore) Consumption Names (Either (TypeError lore)) a
m) = RWST (Env lore) Consumption Names (Either (TypeError lore)) a
-> Env lore -> Names -> Either (TypeError lore) (a, Consumption)
forall (m :: * -> *) r w s a.
Monad m =>
RWST r w s m a -> r -> s -> m (a, w)
evalRWST RWST (Env lore) Consumption Names (Either (TypeError lore)) a
m Env lore
env Names
forall a. Monoid a => a
mempty

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

-- | 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 lore a ->
  TypeM lore a
context :: String -> TypeM lore a -> TypeM lore a
context String
s = (Env lore -> Env lore) -> TypeM lore a -> TypeM lore a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Env lore -> Env lore) -> TypeM lore a -> TypeM lore a)
-> (Env lore -> Env lore) -> TypeM lore a -> TypeM lore a
forall a b. (a -> b) -> a -> b
$ \Env lore
env -> Env lore
env {envContext :: [String]
envContext = String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Env lore -> [String]
forall lore. Env lore -> [String]
envContext Env lore
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 lore ()
bound :: VName -> TypeM lore ()
bound VName
name = do
  Bool
already_seen <- (Names -> Bool) -> TypeM lore Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Names -> Bool) -> TypeM lore Bool)
-> (Names -> Bool) -> TypeM lore Bool
forall a b. (a -> b) -> a -> b
$ VName -> Names -> Bool
nameIn VName
name
  Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
already_seen (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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"
  (Names -> Names) -> TypeM lore ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Names -> Names -> Names
forall a. Semigroup a => a -> a -> a
<> VName -> Names
oneName VName
name)

occur :: Occurences -> TypeM lore ()
occur :: [Occurence] -> TypeM lore ()
occur = Consumption -> TypeM lore ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Consumption -> TypeM lore ())
-> ([Occurence] -> Consumption) -> [Occurence] -> TypeM lore ()
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 lore =>
  VName ->
  TypeM lore ()
observe :: VName -> TypeM lore ()
observe VName
name = do
  NameInfo (Aliases lore)
dec <- VName -> TypeM lore (NameInfo (Aliases lore))
forall lore. VName -> TypeM lore (NameInfo (Aliases lore))
lookupVar VName
name
  Bool -> TypeM lore () -> TypeM lore ()
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 lore) -> Type
forall t. Typed t => t -> Type
typeOf NameInfo (Aliases lore)
dec) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    [Occurence] -> TypeM lore ()
forall lore. [Occurence] -> TypeM lore ()
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 lore) -> Names
forall lore. NameInfo (Aliases lore) -> Names
aliases NameInfo (Aliases lore)
dec]

-- | Proclaim that we have written to the given variables.
consume :: Checkable lore => Names -> TypeM lore ()
consume :: Names -> TypeM lore ()
consume Names
als = do
  Scope (Aliases lore)
scope <- TypeM lore (Scope (Aliases lore))
forall lore (m :: * -> *). HasScope lore m => m (Scope lore)
askScope
  let isArray :: VName -> Bool
isArray = Bool
-> (NameInfo (Aliases lore) -> Bool)
-> Maybe (NameInfo (Aliases lore))
-> 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 lore) -> Int)
-> NameInfo (Aliases lore)
-> 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 lore) -> Type)
-> NameInfo (Aliases lore)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameInfo (Aliases lore) -> Type
forall t. Typed t => t -> Type
typeOf) (Maybe (NameInfo (Aliases lore)) -> Bool)
-> (VName -> Maybe (NameInfo (Aliases lore))) -> VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> Scope (Aliases lore) -> Maybe (NameInfo (Aliases lore))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Scope (Aliases lore)
scope)
  [Occurence] -> TypeM lore ()
forall lore. [Occurence] -> TypeM lore ()
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 lore a -> TypeM lore (a, Occurences)
collectOccurences :: TypeM lore a -> TypeM lore (a, [Occurence])
collectOccurences TypeM lore a
m = TypeM lore ((a, [Occurence]), Consumption -> Consumption)
-> TypeM lore (a, [Occurence])
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
pass (TypeM lore ((a, [Occurence]), Consumption -> Consumption)
 -> TypeM lore (a, [Occurence]))
-> TypeM lore ((a, [Occurence]), Consumption -> Consumption)
-> TypeM lore (a, [Occurence])
forall a b. (a -> b) -> a -> b
$ do
  (a
x, Consumption
c) <- TypeM lore a -> TypeM lore (a, Consumption)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen TypeM lore a
m
  [Occurence]
o <- Consumption -> TypeM lore [Occurence]
forall lore. Consumption -> TypeM lore [Occurence]
checkConsumption Consumption
c
  ((a, [Occurence]), Consumption -> Consumption)
-> TypeM lore ((a, [Occurence]), Consumption -> Consumption)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x, [Occurence]
o), Consumption -> Consumption -> Consumption
forall a b. a -> b -> a
const Consumption
forall a. Monoid a => a
mempty)

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

checkConsumption :: Consumption -> TypeM lore Occurences
checkConsumption :: Consumption -> TypeM lore [Occurence]
checkConsumption (ConsumptionError String
e) = ErrorCase lore -> TypeM lore [Occurence]
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore [Occurence])
-> ErrorCase lore -> TypeM lore [Occurence]
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError String
e
checkConsumption (Consumption [Occurence]
os) = [Occurence] -> TypeM lore [Occurence]
forall (m :: * -> *) a. Monad m => a -> m a
return [Occurence]
os

alternative :: TypeM lore a -> TypeM lore b -> TypeM lore (a, b)
alternative :: TypeM lore a -> TypeM lore b -> TypeM lore (a, b)
alternative TypeM lore a
m1 TypeM lore b
m2 = TypeM lore ((a, b), Consumption -> Consumption)
-> TypeM lore (a, b)
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
pass (TypeM lore ((a, b), Consumption -> Consumption)
 -> TypeM lore (a, b))
-> TypeM lore ((a, b), Consumption -> Consumption)
-> TypeM lore (a, b)
forall a b. (a -> b) -> a -> b
$ do
  (a
x, Consumption
c1) <- TypeM lore a -> TypeM lore (a, Consumption)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen TypeM lore a
m1
  (b
y, Consumption
c2) <- TypeM lore b -> TypeM lore (b, Consumption)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen TypeM lore b
m2
  [Occurence]
os1 <- Consumption -> TypeM lore [Occurence]
forall lore. Consumption -> TypeM lore [Occurence]
checkConsumption Consumption
c1
  [Occurence]
os2 <- Consumption -> TypeM lore [Occurence]
forall lore. Consumption -> TypeM lore [Occurence]
checkConsumption Consumption
c2
  let usage :: Consumption
usage = [Occurence] -> Consumption
Consumption ([Occurence] -> Consumption) -> [Occurence] -> Consumption
forall a b. (a -> b) -> a -> b
$ [Occurence]
os1 [Occurence] -> [Occurence] -> [Occurence]
`altOccurences` [Occurence]
os2
  ((a, b), Consumption -> Consumption)
-> TypeM lore ((a, b), Consumption -> Consumption)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x, b
y), Consumption -> Consumption -> Consumption
forall a b. a -> b -> a
const Consumption
usage)

-- | 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 lore a -> TypeM lore a
consumeOnlyParams :: [(VName, Names)] -> TypeM lore a -> TypeM lore a
consumeOnlyParams [(VName, Names)]
consumable TypeM lore a
m = do
  (a
x, [Occurence]
os) <- TypeM lore a -> TypeM lore (a, [Occurence])
forall lore a. TypeM lore a -> TypeM lore (a, [Occurence])
collectOccurences TypeM lore a
m
  Consumption -> TypeM lore ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Consumption -> TypeM lore ())
-> ([Occurence] -> Consumption) -> [Occurence] -> TypeM lore ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Occurence] -> Consumption
Consumption ([Occurence] -> TypeM lore ())
-> TypeM lore [Occurence] -> TypeM lore ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Occurence -> TypeM lore Occurence)
-> [Occurence] -> TypeM lore [Occurence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Occurence -> TypeM lore Occurence
inspect [Occurence]
os
  a -> TypeM lore a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  where
    inspect :: Occurence -> TypeM lore Occurence
inspect Occurence
o = do
      Names
new_consumed <- [Names] -> Names
forall a. Monoid a => [a] -> a
mconcat ([Names] -> Names) -> TypeM lore [Names] -> TypeM lore Names
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VName -> TypeM lore Names) -> [VName] -> TypeM lore [Names]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TypeM lore Names
wasConsumed (Names -> [VName]
namesToList (Names -> [VName]) -> Names -> [VName]
forall a b. (a -> b) -> a -> b
$ Occurence -> Names
consumed Occurence
o)
      Occurence -> TypeM lore Occurence
forall (m :: * -> *) a. Monad m => a -> m a
return Occurence
o {consumed :: Names
consumed = Names
new_consumed}
    wasConsumed :: VName -> TypeM lore 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 lore Names
forall (m :: * -> *) a. Monad m => a -> m a
return Names
als
      | Bool
otherwise =
        ErrorCase lore -> TypeM lore Names
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore Names)
-> ErrorCase lore -> TypeM lore Names
forall a b. (a -> b) -> a -> b
$
          String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore -> Names
expandAliases :: Names -> Env lore -> Names
expandAliases Names
names Env lore
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 lore) -> Maybe (VarBinding lore)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k (Map VName (VarBinding lore) -> Maybe (VarBinding lore))
-> Map VName (VarBinding lore) -> Maybe (VarBinding lore)
forall a b. (a -> b) -> a -> b
$ Env lore -> Map VName (VarBinding lore)
forall lore. Env lore -> Map VName (VarBinding lore)
envVtable Env lore
env of
      Just (LetName (als, _)) -> VarAliases -> Names
unAliases VarAliases
als
      Maybe (VarBinding lore)
_ -> Names
forall a. Monoid a => a
mempty

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

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

    -- Check whether the bound variables have been used correctly
    -- within their scope.
    check :: TypeM lore a -> TypeM lore a
check TypeM lore a
m = do
      (VName -> TypeM lore ()) -> [VName] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> TypeM lore ()
forall lore. VName -> TypeM lore ()
bound ([VName] -> TypeM lore ()) -> [VName] -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ Scope (Aliases lore) -> [VName]
forall k a. Map k a -> [k]
M.keys Scope (Aliases lore)
bnds
      (a
a, [Occurence]
os) <- TypeM lore a -> TypeM lore (a, [Occurence])
forall lore a. TypeM lore a -> TypeM lore (a, [Occurence])
collectOccurences TypeM lore a
m
      Consumption -> TypeM lore ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Consumption -> TypeM lore ()) -> Consumption -> TypeM lore ()
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 lore a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

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

lookupAliases :: Checkable lore => VName -> TypeM lore Names
lookupAliases :: VName -> TypeM lore Names
lookupAliases VName
name = do
  NameInfo (Aliases lore)
info <- VName -> TypeM lore (NameInfo (Aliases lore))
forall lore. VName -> TypeM lore (NameInfo (Aliases lore))
lookupVar VName
name
  Names -> TypeM lore Names
forall (m :: * -> *) a. Monad m => a -> m a
return (Names -> TypeM lore Names) -> Names -> TypeM lore 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 lore) -> Type
forall t. Typed t => t -> Type
typeOf NameInfo (Aliases lore)
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 lore) -> Names
forall lore. NameInfo (Aliases lore) -> Names
aliases NameInfo (Aliases lore)
info

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

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

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

-- | @checkAnnotation loc s t1 t2@ checks if @t2@ is equal to
-- @t1@.  If not, a 'BadAnnotation' is raised.
checkAnnotation ::
  String ->
  Type ->
  Type ->
  TypeM lore ()
checkAnnotation :: String -> Type -> Type -> TypeM lore ()
checkAnnotation String
desc Type
t1 Type
t2
  | Type
t2 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t1 = () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ String -> Type -> Type -> ErrorCase lore
forall lore. String -> Type -> Type -> ErrorCase lore
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 lore => [Type] -> SubExp -> TypeM lore ()
require :: [Type] -> SubExp -> TypeM lore ()
require [Type]
ts SubExp
se = do
  Type
t <- SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
se
  Bool -> TypeM lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ Exp lore -> Type -> [Type] -> ErrorCase lore
forall lore. Exp lore -> Type -> [Type] -> ErrorCase lore
UnexpectedType (BasicOp -> Exp lore
forall lore. BasicOp -> ExpT lore
BasicOp (BasicOp -> Exp lore) -> BasicOp -> Exp lore
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 lore => [Type] -> VName -> TypeM lore ()
requireI :: [Type] -> VName -> TypeM lore ()
requireI [Type]
ts VName
ident = [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [Type]
ts (SubExp -> TypeM lore ()) -> SubExp -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
ident

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

-- | Type check a program containing arbitrary type information,
-- yielding either a type error or a program with complete type
-- information.
checkProg ::
  Checkable lore =>
  Prog (Aliases lore) ->
  Either (TypeError lore) ()
checkProg :: Prog (Aliases lore) -> Either (TypeError lore) ()
checkProg (Prog Stms (Aliases lore)
consts [FunDef (Aliases lore)]
funs) = do
  let typeenv :: Env lore
typeenv =
        Env :: forall lore.
Map VName (VarBinding lore)
-> Map Name (FunBinding lore)
-> (OpWithAliases (Op lore) -> TypeM lore ())
-> [String]
-> Env lore
Env
          { envVtable :: Map VName (VarBinding lore)
envVtable = Map VName (VarBinding lore)
forall k a. Map k a
M.empty,
            envFtable :: Map Name (FunBinding lore)
envFtable = Map Name (FunBinding lore)
forall a. Monoid a => a
mempty,
            envContext :: [String]
envContext = [],
            envCheckOp :: OpWithAliases (Op lore) -> TypeM lore ()
envCheckOp = OpWithAliases (Op lore) -> TypeM lore ()
forall lore.
CheckableOp lore =>
OpWithAliases (Op lore) -> TypeM lore ()
checkOp
          }
  let onFunction :: Map Name ([RetType lore], [Param (FParamInfo lore)])
-> Map VName (VarBinding lore)
-> FunDef (Aliases lore)
-> Either (TypeError lore) ()
onFunction Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable Map VName (VarBinding lore)
vtable FunDef (Aliases lore)
fun =
        (((), Consumption) -> ())
-> Either (TypeError lore) ((), Consumption)
-> Either (TypeError lore) ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), Consumption) -> ()
forall a b. (a, b) -> a
fst (Either (TypeError lore) ((), Consumption)
 -> Either (TypeError lore) ())
-> Either (TypeError lore) ((), Consumption)
-> Either (TypeError lore) ()
forall a b. (a -> b) -> a -> b
$
          Env lore
-> TypeM lore () -> Either (TypeError lore) ((), Consumption)
forall lore a.
Env lore
-> TypeM lore a -> Either (TypeError lore) (a, Consumption)
runTypeM Env lore
typeenv (TypeM lore () -> Either (TypeError lore) ((), Consumption))
-> TypeM lore () -> Either (TypeError lore) ((), Consumption)
forall a b. (a -> b) -> a -> b
$
            (Env lore -> Env lore) -> TypeM lore () -> TypeM lore ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env lore
env -> Env lore
env {envFtable :: Map Name (FunBinding lore)
envFtable = Map Name ([RetType lore], [Param (FParamInfo lore)])
Map Name (FunBinding lore)
ftable, envVtable :: Map VName (VarBinding lore)
envVtable = Map VName (VarBinding lore)
vtable}) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
              FunDef (Aliases lore) -> TypeM lore ()
forall lore.
Checkable lore =>
FunDef (Aliases lore) -> TypeM lore ()
checkFun FunDef (Aliases lore)
fun
  (Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable, Consumption
_) <- Env lore
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
-> Either
     (TypeError lore)
     (Map Name ([RetType lore], [Param (FParamInfo lore)]), Consumption)
forall lore a.
Env lore
-> TypeM lore a -> Either (TypeError lore) (a, Consumption)
runTypeM Env lore
typeenv TypeM lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
buildFtable
  (Map VName (VarBinding lore)
vtable, Consumption
_) <-
    Env lore
-> TypeM lore (Map VName (VarBinding lore))
-> Either
     (TypeError lore) (Map VName (VarBinding lore), Consumption)
forall lore a.
Env lore
-> TypeM lore a -> Either (TypeError lore) (a, Consumption)
runTypeM Env lore
typeenv {envFtable :: Map Name (FunBinding lore)
envFtable = Map Name ([RetType lore], [Param (FParamInfo lore)])
Map Name (FunBinding lore)
ftable} (TypeM lore (Map VName (VarBinding lore))
 -> Either
      (TypeError lore) (Map VName (VarBinding lore), Consumption))
-> TypeM lore (Map VName (VarBinding lore))
-> Either
     (TypeError lore) (Map VName (VarBinding lore), Consumption)
forall a b. (a -> b) -> a -> b
$
      Stms (Aliases lore)
-> TypeM lore (Map VName (VarBinding lore))
-> TypeM lore (Map VName (VarBinding lore))
forall lore a.
Checkable lore =>
Stms (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStms Stms (Aliases lore)
consts (TypeM lore (Map VName (VarBinding lore))
 -> TypeM lore (Map VName (VarBinding lore)))
-> TypeM lore (Map VName (VarBinding lore))
-> TypeM lore (Map VName (VarBinding lore))
forall a b. (a -> b) -> a -> b
$ (Env lore -> Map VName (VarBinding lore))
-> TypeM lore (Map VName (VarBinding lore))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env lore -> Map VName (VarBinding lore)
forall lore. Env lore -> Map VName (VarBinding lore)
envVtable
  [Either (TypeError lore) ()] -> Either (TypeError lore) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([Either (TypeError lore) ()] -> Either (TypeError lore) ())
-> [Either (TypeError lore) ()] -> Either (TypeError lore) ()
forall a b. (a -> b) -> a -> b
$ Strategy (Either (TypeError lore) ())
-> (FunDef (Aliases lore) -> Either (TypeError lore) ())
-> [FunDef (Aliases lore)]
-> [Either (TypeError lore) ()]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (Either (TypeError lore) ())
forall a. Strategy a
rpar (Map Name ([RetType lore], [Param (FParamInfo lore)])
-> Map VName (VarBinding lore)
-> FunDef (Aliases lore)
-> Either (TypeError lore) ()
onFunction Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable Map VName (VarBinding lore)
vtable) [FunDef (Aliases lore)]
funs
  where
    buildFtable :: TypeM lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
buildFtable = do
      Map Name ([RetType lore], [Param (FParamInfo lore)])
table <- TypeM lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall lore.
Checkable lore =>
TypeM lore (Map Name (FunBinding lore))
initialFtable
      (Map Name ([RetType lore], [Param (FParamInfo lore)])
 -> FunDef (Aliases lore)
 -> TypeM
      lore (Map Name ([RetType lore], [Param (FParamInfo lore)])))
-> Map Name ([RetType lore], [Param (FParamInfo lore)])
-> [FunDef (Aliases lore)]
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Name ([RetType lore], [Param (FParamInfo lore)])
-> FunDef (Aliases lore)
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall lore lore.
Map Name ([RetType lore], [Param (FParamInfo lore)])
-> FunDef lore
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
expand Map Name ([RetType lore], [Param (FParamInfo lore)])
table [FunDef (Aliases lore)]
funs
    expand :: Map Name ([RetType lore], [Param (FParamInfo lore)])
-> FunDef lore
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
expand Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable (FunDef Maybe EntryPoint
_ Attrs
_ Name
name [RetType lore]
ret [Param (FParamInfo lore)]
params BodyT lore
_)
      | Name
-> Map Name ([RetType lore], [Param (FParamInfo lore)]) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member Name
name Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable =
        ErrorCase lore
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore
 -> TypeM
      lore (Map Name ([RetType lore], [Param (FParamInfo lore)])))
-> ErrorCase lore
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase lore
forall lore. Name -> ErrorCase lore
DupDefinitionError Name
name
      | Bool
otherwise =
        Map Name ([RetType lore], [Param (FParamInfo lore)])
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Name ([RetType lore], [Param (FParamInfo lore)])
 -> TypeM
      lore (Map Name ([RetType lore], [Param (FParamInfo lore)])))
-> Map Name ([RetType lore], [Param (FParamInfo lore)])
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall a b. (a -> b) -> a -> b
$ Name
-> ([RetType lore], [Param (FParamInfo lore)])
-> Map Name ([RetType lore], [Param (FParamInfo lore)])
-> Map Name ([RetType lore], [Param (FParamInfo lore)])
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
name ([RetType lore]
ret, [Param (FParamInfo lore)]
params) Map Name ([RetType lore], [Param (FParamInfo lore)])
ftable

initialFtable ::
  Checkable lore =>
  TypeM lore (M.Map Name (FunBinding lore))
initialFtable :: TypeM lore (Map Name (FunBinding lore))
initialFtable = ([(Name, ([RetType lore], [Param (FParamInfo lore)]))]
 -> Map Name ([RetType lore], [Param (FParamInfo lore)]))
-> TypeM lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
-> Map Name ([RetType lore], [Param (FParamInfo lore)])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (TypeM lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
 -> TypeM
      lore (Map Name ([RetType lore], [Param (FParamInfo lore)])))
-> TypeM lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
-> TypeM
     lore (Map Name ([RetType lore], [Param (FParamInfo lore)]))
forall a b. (a -> b) -> a -> b
$ ((Name, (PrimType, [PrimType]))
 -> TypeM lore (Name, ([RetType lore], [Param (FParamInfo lore)])))
-> [(Name, (PrimType, [PrimType]))]
-> TypeM lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, (PrimType, [PrimType]))
-> TypeM lore (Name, ([RetType lore], [Param (FParamInfo lore)]))
forall (t :: * -> *) lore a a.
(Traversable t, Checkable lore, IsRetType a) =>
(a, (PrimType, t PrimType))
-> TypeM lore (a, ([a], t (Param (FParamInfo lore))))
addBuiltin ([(Name, (PrimType, [PrimType]))]
 -> TypeM
      lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))])
-> [(Name, (PrimType, [PrimType]))]
-> TypeM lore [(Name, ([RetType lore], [Param (FParamInfo lore)]))]
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 lore (a, ([a], t (Param (FParamInfo lore))))
addBuiltin (a
fname, (PrimType
t, t PrimType
ts)) = do
      t (Param (FParamInfo lore))
ps <- (PrimType -> TypeM lore (Param (FParamInfo lore)))
-> t PrimType -> TypeM lore (t (Param (FParamInfo lore)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (VName -> PrimType -> TypeM lore (FParam (Aliases lore))
forall lore.
Checkable lore =>
VName -> PrimType -> TypeM lore (FParam (Aliases lore))
primFParam VName
name) t PrimType
ts
      (a, ([a], t (Param (FParamInfo lore))))
-> TypeM lore (a, ([a], t (Param (FParamInfo lore))))
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 lore))
ps))
    name :: VName
name = Name -> Int -> VName
VName (String -> Name
nameFromString String
"x") Int
0

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

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

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

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

checkFun' ::
  Checkable lore =>
  ( Name,
    [DeclExtType],
    [(VName, NameInfo (Aliases lore))]
  ) ->
  [(VName, Names)] ->
  TypeM lore [Names] ->
  TypeM lore ()
checkFun' :: (Name, [DeclExtType], [(VName, NameInfo (Aliases lore))])
-> [(VName, Names)] -> TypeM lore [Names] -> TypeM lore ()
checkFun' (Name
fname, [DeclExtType]
rettype, [(VName, NameInfo (Aliases lore))]
params) [(VName, Names)]
consumable TypeM lore [Names]
check = do
  TypeM lore ()
checkNoDuplicateParams
  Scope (Aliases lore) -> TypeM lore () -> TypeM lore ()
forall lore a.
Checkable lore =>
Scope (Aliases lore) -> TypeM lore a -> TypeM lore a
binding ([(VName, NameInfo (Aliases lore))] -> Scope (Aliases lore)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, NameInfo (Aliases lore))]
params) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    [(VName, Names)] -> TypeM lore () -> TypeM lore ()
forall lore a. [(VName, Names)] -> TypeM lore a -> TypeM lore a
consumeOnlyParams [(VName, Names)]
consumable (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ do
      [Names]
body_aliases <- TypeM lore [Names]
check
      Scope (Aliases lore)
scope <- TypeM lore (Scope (Aliases lore))
forall lore (m :: * -> *). HasScope lore m => m (Scope lore)
askScope
      let isArray :: VName -> Bool
isArray = Bool
-> (NameInfo (Aliases lore) -> Bool)
-> Maybe (NameInfo (Aliases lore))
-> 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 lore) -> Int)
-> NameInfo (Aliases lore)
-> 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 lore) -> Type)
-> NameInfo (Aliases lore)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameInfo (Aliases lore) -> Type
forall t. Typed t => t -> Type
typeOf) (Maybe (NameInfo (Aliases lore)) -> Bool)
-> (VName -> Maybe (NameInfo (Aliases lore))) -> VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> Scope (Aliases lore) -> Maybe (NameInfo (Aliases lore))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Scope (Aliases lore)
scope)
      String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore 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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ [Names] -> TypeM lore ()
checkReturnAlias ([Names] -> TypeM lore ()) -> [Names] -> TypeM lore ()
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 lore)) -> VName)
-> [(VName, NameInfo (Aliases lore))] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map (VName, NameInfo (Aliases lore)) -> VName
forall a b. (a, b) -> a
fst [(VName, NameInfo (Aliases lore))]
params

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

    expand :: [VName] -> VName -> TypeM lore [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 lore -> TypeM lore [VName]
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore [VName])
-> ErrorCase lore -> TypeM lore [VName]
forall a b. (a -> b) -> a -> b
$ Name -> VName -> ErrorCase lore
forall lore. Name -> VName -> ErrorCase lore
DupParamError Name
fname VName
pname
      | Bool
otherwise =
        [VName] -> TypeM lore [VName]
forall (m :: * -> *) a. Monad m => a -> m a
return ([VName] -> TypeM lore [VName]) -> [VName] -> TypeM lore [VName]
forall a b. (a -> b) -> a -> b
$ VName
pname VName -> [VName] -> [VName]
forall a. a -> [a] -> [a]
: [VName]
seen
    checkReturnAlias :: [Names] -> TypeM lore ()
checkReturnAlias =
      (Set (VName, Uniqueness)
 -> (Uniqueness, Names) -> TypeM lore (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness)
-> [(Uniqueness, Names)]
-> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ Set (VName, Uniqueness)
-> (Uniqueness, Names) -> TypeM lore (Set (VName, Uniqueness))
checkReturnAlias' Set (VName, Uniqueness)
forall a. Monoid a => a
mempty ([(Uniqueness, Names)] -> TypeM lore ())
-> ([Names] -> [(Uniqueness, Names)]) -> [Names] -> TypeM lore ()
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 lore (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 lore -> TypeM lore (Set (VName, Uniqueness))
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore (Set (VName, Uniqueness)))
-> ErrorCase lore -> TypeM lore (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase lore
forall lore. Name -> ErrorCase lore
UniqueReturnAliased Name
fname
      | Bool
otherwise = do
        Names -> TypeM lore ()
forall lore. Checkable lore => Names -> TypeM lore ()
consume Names
names
        Set (VName, Uniqueness) -> TypeM lore (Set (VName, Uniqueness))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (VName, Uniqueness) -> TypeM lore (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness) -> TypeM lore (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 lore -> TypeM lore (Set (VName, Uniqueness))
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore (Set (VName, Uniqueness)))
-> ErrorCase lore -> TypeM lore (Set (VName, Uniqueness))
forall a b. (a -> b) -> a -> b
$ Name -> ErrorCase lore
forall lore. Name -> ErrorCase lore
UniqueReturnAliased Name
fname
      | Bool
otherwise = Set (VName, Uniqueness) -> TypeM lore (Set (VName, Uniqueness))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (VName, Uniqueness) -> TypeM lore (Set (VName, Uniqueness)))
-> Set (VName, Uniqueness) -> TypeM lore (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 lore => SubExp -> TypeM lore Type
checkSubExp :: SubExp -> TypeM lore Type
checkSubExp (Constant PrimValue
val) =
  Type -> TypeM lore Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TypeM lore Type) -> Type -> TypeM lore 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 lore Type -> TypeM lore Type
forall lore a. String -> TypeM lore a -> TypeM lore a
context (String
"In subexp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VName -> String
forall a. Pretty a => a -> String
pretty VName
ident) (TypeM lore Type -> TypeM lore Type)
-> TypeM lore Type -> TypeM lore Type
forall a b. (a -> b) -> a -> b
$ do
  VName -> TypeM lore ()
forall lore. Checkable lore => VName -> TypeM lore ()
observe VName
ident
  VName -> TypeM lore Type
forall lore (m :: * -> *). HasScope lore m => VName -> m Type
lookupType VName
ident

checkStms ::
  Checkable lore =>
  Stms (Aliases lore) ->
  TypeM lore a ->
  TypeM lore a
checkStms :: Stms (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStms Stms (Aliases lore)
origbnds TypeM lore a
m = [Stm (Aliases lore)] -> TypeM lore a
delve ([Stm (Aliases lore)] -> TypeM lore a)
-> [Stm (Aliases lore)] -> TypeM lore a
forall a b. (a -> b) -> a -> b
$ Stms (Aliases lore) -> [Stm (Aliases lore)]
forall lore. Stms lore -> [Stm lore]
stmsToList Stms (Aliases lore)
origbnds
  where
    delve :: [Stm (Aliases lore)] -> TypeM lore a
delve (stm :: Stm (Aliases lore)
stm@(Let Pattern (Aliases lore)
pat StmAux (ExpDec (Aliases lore))
_ Exp (Aliases lore)
e) : [Stm (Aliases lore)]
bnds) = do
      String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore 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 (PatternT (VarAliases, LetDec lore) -> Doc
forall a. Pretty a => a -> Doc
ppr PatternT (VarAliases, LetDec lore)
Pattern (Aliases lore)
pat)) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        Exp (Aliases lore) -> TypeM lore ()
forall lore. Checkable lore => Exp (Aliases lore) -> TypeM lore ()
checkExp Exp (Aliases lore)
e
      Stm (Aliases lore) -> TypeM lore a -> TypeM lore a
forall lore a.
Checkable lore =>
Stm (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStm Stm (Aliases lore)
stm (TypeM lore a -> TypeM lore a) -> TypeM lore a -> TypeM lore a
forall a b. (a -> b) -> a -> b
$
        [Stm (Aliases lore)] -> TypeM lore a
delve [Stm (Aliases lore)]
bnds
    delve [] =
      TypeM lore a
m

checkResult ::
  Checkable lore =>
  Result ->
  TypeM lore ()
checkResult :: [SubExp] -> TypeM lore ()
checkResult = (SubExp -> TypeM lore Type) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp

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

checkLambdaBody ::
  Checkable lore =>
  [Type] ->
  Body (Aliases lore) ->
  TypeM lore [Names]
checkLambdaBody :: [Type] -> Body (Aliases lore) -> TypeM lore [Names]
checkLambdaBody [Type]
ret (Body (_, lore) Stms (Aliases lore)
bnds [SubExp]
res) = do
  BodyDec lore -> TypeM lore ()
forall lore. Checkable lore => BodyDec lore -> TypeM lore ()
checkBodyLore BodyDec lore
lore
  Stms (Aliases lore) -> TypeM lore [Names] -> TypeM lore [Names]
forall lore a.
Checkable lore =>
Stms (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStms Stms (Aliases lore)
bnds (TypeM lore [Names] -> TypeM lore [Names])
-> TypeM lore [Names] -> TypeM lore [Names]
forall a b. (a -> b) -> a -> b
$ do
    [Type] -> [SubExp] -> TypeM lore ()
forall lore. Checkable lore => [Type] -> [SubExp] -> TypeM lore ()
checkLambdaResult [Type]
ret [SubExp]
res
    (Names -> Names) -> [Names] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here) ([Names] -> [Names]) -> TypeM lore [Names] -> TypeM lore [Names]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExp -> TypeM lore Names) -> [SubExp] -> TypeM lore [Names]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM lore Names
forall lore. Checkable lore => SubExp -> TypeM lore Names
subExpAliasesM [SubExp]
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 lore)) -> [VName]
forall k a. Map k a -> [k]
M.keys (Map VName (NameInfo (Aliases lore)) -> [VName])
-> Map VName (NameInfo (Aliases lore)) -> [VName]
forall a b. (a -> b) -> a -> b
$ Stms (Aliases lore) -> Map VName (NameInfo (Aliases lore))
forall lore a. Scoped lore a => a -> Scope lore
scopeOf Stms (Aliases lore)
bnds

checkLambdaResult ::
  Checkable lore =>
  [Type] ->
  Result ->
  TypeM lore ()
checkLambdaResult :: [Type] -> [SubExp] -> TypeM lore ()
checkLambdaResult [Type]
ts [SubExp]
es
  | [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
es =
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 ([SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
es)
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" values: "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SubExp] -> String
forall a. Pretty a => [a] -> String
prettyTuple [SubExp]
es
  | Bool
otherwise = [(Type, SubExp)]
-> ((Type, SubExp) -> TypeM lore ()) -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Type] -> [SubExp] -> [(Type, SubExp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts [SubExp]
es) (((Type, SubExp) -> TypeM lore ()) -> TypeM lore ())
-> ((Type, SubExp) -> TypeM lore ()) -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ \(Type
t, SubExp
e) -> do
    Type
et <- SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
e
    Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
et Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$
          String
"Subexpression " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SubExp -> String
forall a. Pretty a => a -> String
pretty SubExp
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 lore =>
  Body (Aliases lore) ->
  TypeM lore [Names]
checkBody :: Body (Aliases lore) -> TypeM lore [Names]
checkBody (Body (_, lore) Stms (Aliases lore)
bnds [SubExp]
res) = do
  BodyDec lore -> TypeM lore ()
forall lore. Checkable lore => BodyDec lore -> TypeM lore ()
checkBodyLore BodyDec lore
lore
  Stms (Aliases lore) -> TypeM lore [Names] -> TypeM lore [Names]
forall lore a.
Checkable lore =>
Stms (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStms Stms (Aliases lore)
bnds (TypeM lore [Names] -> TypeM lore [Names])
-> TypeM lore [Names] -> TypeM lore [Names]
forall a b. (a -> b) -> a -> b
$ do
    [SubExp] -> TypeM lore ()
forall lore. Checkable lore => [SubExp] -> TypeM lore ()
checkResult [SubExp]
res
    (Names -> Names) -> [Names] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here) ([Names] -> [Names]) -> TypeM lore [Names] -> TypeM lore [Names]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExp -> TypeM lore Names) -> [SubExp] -> TypeM lore [Names]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM lore Names
forall lore. Checkable lore => SubExp -> TypeM lore Names
subExpAliasesM [SubExp]
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 lore)) -> [VName]
forall k a. Map k a -> [k]
M.keys (Map VName (NameInfo (Aliases lore)) -> [VName])
-> Map VName (NameInfo (Aliases lore)) -> [VName]
forall a b. (a -> b) -> a -> b
$ Stms (Aliases lore) -> Map VName (NameInfo (Aliases lore))
forall lore a. Scoped lore a => a -> Scope lore
scopeOf Stms (Aliases lore)
bnds

checkBasicOp :: Checkable lore => BasicOp -> TypeM lore ()
checkBasicOp :: BasicOp -> TypeM lore ()
checkBasicOp (SubExp SubExp
es) =
  TypeM lore Type -> TypeM lore ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM lore Type -> TypeM lore ())
-> TypeM lore Type -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
es
checkBasicOp (Opaque SubExp
es) =
  TypeM lore Type -> TypeM lore ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM lore Type -> TypeM lore ())
-> TypeM lore Type -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
es
checkBasicOp (ArrayLit [] Type
_) =
  () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkBasicOp (ArrayLit (SubExp
e : [SubExp]
es') Type
t) = do
  let check :: Type -> SubExp -> TypeM lore ()
check Type
elemt SubExp
eleme = do
        Type
elemet <- SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
eleme
        Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
elemet Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
elemt) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
          ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
            String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
e

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

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

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

  (DimIndex SubExp -> TypeM lore ()) -> Slice SubExp -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DimIndex SubExp -> TypeM lore ()
forall lore. Checkable lore => DimIndex SubExp -> TypeM lore ()
checkDimIndex Slice SubExp
idxes
  [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim (Type -> PrimType
forall shape u. TypeBase shape u -> PrimType
elemType Type
src_t) Type -> Shape -> Type
`arrayOfShape` [SubExp] -> Shape
forall d. [d] -> ShapeBase d
Shape (Slice SubExp -> [SubExp]
forall d. Slice d -> [d]
sliceDims Slice SubExp
idxes)] SubExp
se
  Names -> TypeM lore ()
forall lore. Checkable lore => Names -> TypeM lore ()
consume (Names -> TypeM lore ()) -> TypeM lore Names -> TypeM lore ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> TypeM lore Names
forall lore. Checkable lore => VName -> TypeM lore Names
lookupAliases VName
src
checkBasicOp (Iota SubExp
e SubExp
x SubExp
s IntType
et) = do
  [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
e
  [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
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 lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
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 lore ()) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
dims
  TypeM lore Type -> TypeM lore ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM lore Type -> TypeM lore ())
-> TypeM lore Type -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
valexp
checkBasicOp (Scratch PrimType
_ [SubExp]
shape) =
  (SubExp -> TypeM lore Type) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore 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 lore Type -> TypeM lore Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> TypeM lore Type
forall lore. Checkable lore => VName -> TypeM lore Type
checkArrIdent VName
arrexp
  (DimChange SubExp -> TypeM lore ())
-> ShapeChange SubExp -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] (SubExp -> TypeM lore ())
-> (DimChange SubExp -> SubExp)
-> DimChange SubExp
-> TypeM lore ()
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 lore ())
-> ShapeChange SubExp -> [Int] -> TypeM lore ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Int -> DimChange SubExp -> Int -> TypeM lore ()
checkDimChange Int
rank) ShapeChange SubExp
newshape [Int
0 ..]
  where
    checkDimChange :: Int -> DimChange SubExp -> Int -> TypeM lore ()
checkDimChange Int
_ (DimNew SubExp
_) Int
_ =
      () -> TypeM lore ()
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 lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
          String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkBasicOp (Rearrange [Int]
perm VName
arr) = do
  Type
arrt <- VName -> TypeM lore Type
forall lore (m :: * -> *). HasScope lore 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 lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ [Int] -> Int -> Maybe VName -> ErrorCase lore
forall lore. [Int] -> Int -> Maybe VName -> ErrorCase lore
PermutationError [Int]
perm Int
rank (Maybe VName -> ErrorCase lore) -> Maybe VName -> ErrorCase lore
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 lore Type
forall lore (m :: * -> *). HasScope lore 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 lore ()) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
rots
  Bool -> TypeM lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore Type
forall lore. Checkable lore => VName -> TypeM lore Type
checkArrIdent VName
arr1exp
  [Type]
arr2ts <- (VName -> TypeM lore Type) -> [VName] -> TypeM lore [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TypeM lore Type
forall lore. Checkable lore => VName -> TypeM lore 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 lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
success (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
ressize
checkBasicOp (Copy VName
e) =
  TypeM lore Type -> TypeM lore ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM lore Type -> TypeM lore ())
-> TypeM lore Type -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ VName -> TypeM lore Type
forall lore. Checkable lore => VName -> TypeM lore Type
checkArrIdent VName
e
checkBasicOp (Manifest [Int]
perm VName
arr) =
  BasicOp -> TypeM lore ()
forall lore. Checkable lore => BasicOp -> TypeM lore ()
checkBasicOp (BasicOp -> TypeM lore ()) -> BasicOp -> TypeM lore ()
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 lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool] SubExp
e
  (ErrorMsgPart SubExp -> TypeM lore ())
-> [ErrorMsgPart SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ErrorMsgPart SubExp -> TypeM lore ()
forall lore. Checkable lore => ErrorMsgPart SubExp -> TypeM lore ()
checkPart [ErrorMsgPart SubExp]
parts
  where
    checkPart :: ErrorMsgPart SubExp -> TypeM lore ()
checkPart ErrorString {} = () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkPart (ErrorInt32 SubExp
x) = [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int32] SubExp
x
    checkPart (ErrorInt64 SubExp
x) = [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64] SubExp
x

matchLoopResultExt ::
  Checkable lore =>
  [Param DeclType] ->
  [Param DeclType] ->
  [SubExp] ->
  TypeM lore ()
matchLoopResultExt :: [Param DeclType] -> [Param DeclType] -> [SubExp] -> TypeM lore ()
matchLoopResultExt [Param DeclType]
ctx [Param DeclType]
val [SubExp]
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]
ctx) ([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] -> [Type]) -> [Param DeclType] -> [Type]
forall a b. (a -> b) -> a -> b
$ [Param DeclType]
ctx [Param DeclType] -> [Param DeclType] -> [Param DeclType]
forall a. [a] -> [a] -> [a]
++ [Param DeclType]
val

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

  case (Int -> Maybe SubExp) -> [ExtType] -> Maybe [Type]
forall (m :: * -> *) u.
Monad m =>
(Int -> m SubExp) -> [TypeBase ExtShape u] -> m [TypeBase Shape u]
instantiateShapes (Int -> [SubExp] -> Maybe SubExp
forall int a. Integral int => int -> [a] -> Maybe a
`maybeNth` [SubExp]
loopres) [ExtType]
rettype_ext of
    Maybe [Type]
Nothing ->
      ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        Name -> [ExtType] -> [ExtType] -> ErrorCase lore
forall lore. Name -> [ExtType] -> [ExtType] -> ErrorCase lore
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 lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
          Name -> [ExtType] -> [ExtType] -> ErrorCase lore
forall lore. Name -> [ExtType] -> [ExtType] -> ErrorCase lore
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 lore =>
  Exp (Aliases lore) ->
  TypeM lore ()
checkExp :: Exp (Aliases lore) -> TypeM lore ()
checkExp (BasicOp BasicOp
op) = BasicOp -> TypeM lore ()
forall lore. Checkable lore => BasicOp -> TypeM lore ()
checkBasicOp BasicOp
op
checkExp (If SubExp
e1 BodyT (Aliases lore)
e2 BodyT (Aliases lore)
e3 IfDec (BranchType (Aliases lore))
info) = do
  [Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool] SubExp
e1
  ([Names], [Names])
_ <-
    String -> TypeM lore [Names] -> TypeM lore [Names]
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"in true branch" (BodyT (Aliases lore) -> TypeM lore [Names]
forall lore.
Checkable lore =>
Body (Aliases lore) -> TypeM lore [Names]
checkBody BodyT (Aliases lore)
e2)
      TypeM lore [Names]
-> TypeM lore [Names] -> TypeM lore ([Names], [Names])
forall lore a b. TypeM lore a -> TypeM lore b -> TypeM lore (a, b)
`alternative` String -> TypeM lore [Names] -> TypeM lore [Names]
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"in false branch" (BodyT (Aliases lore) -> TypeM lore [Names]
forall lore.
Checkable lore =>
Body (Aliases lore) -> TypeM lore [Names]
checkBody BodyT (Aliases lore)
e3)
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"in true branch" (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ [BranchType lore] -> BodyT (Aliases lore) -> TypeM lore ()
forall lore.
Checkable lore =>
[BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
matchBranchType (IfDec (BranchType lore) -> [BranchType lore]
forall rt. IfDec rt -> [rt]
ifReturns IfDec (BranchType lore)
IfDec (BranchType (Aliases lore))
info) BodyT (Aliases lore)
e2
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"in false branch" (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ [BranchType lore] -> BodyT (Aliases lore) -> TypeM lore ()
forall lore.
Checkable lore =>
[BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
matchBranchType (IfDec (BranchType lore) -> [BranchType lore]
forall rt. IfDec rt -> [rt]
ifReturns IfDec (BranchType lore)
IfDec (BranchType (Aliases lore))
info) BodyT (Aliases lore)
e3
checkExp (Apply Name
fname [(SubExp, Diet)]
args [RetType (Aliases lore)]
rettype_annot (Safety, SrcLoc, [SrcLoc])
_) = do
  ([RetType lore]
rettype_derived, [DeclType]
paramtypes) <- Name -> [SubExp] -> TypeM lore ([RetType lore], [DeclType])
forall lore.
Checkable lore =>
Name -> [SubExp] -> TypeM lore ([RetType lore], [DeclType])
lookupFun Name
fname ([SubExp] -> TypeM lore ([RetType lore], [DeclType]))
-> [SubExp] -> TypeM lore ([RetType lore], [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 lore Arg)
-> [(SubExp, Diet)] -> TypeM lore [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SubExp -> TypeM lore Arg
forall lore. Checkable lore => SubExp -> TypeM lore Arg
checkArg (SubExp -> TypeM lore Arg)
-> ((SubExp, Diet) -> SubExp) -> (SubExp, Diet) -> TypeM lore 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 lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([RetType lore]
rettype_derived [RetType lore] -> [RetType lore] -> Bool
forall a. Eq a => a -> a -> Bool
/= [RetType lore]
[RetType (Aliases lore)]
rettype_annot) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$
        String
"Expected apply result type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [RetType lore] -> String
forall a. Pretty a => a -> String
pretty [RetType lore]
rettype_derived
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" but annotation is "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ [RetType lore] -> String
forall a. Pretty a => a -> String
pretty [RetType lore]
[RetType (Aliases lore)]
rettype_annot
  Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
forall lore. Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
checkFuncall (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fname) [DeclType]
paramtypes [Arg]
argflows
checkExp (DoLoop [(FParam (Aliases lore), SubExp)]
ctxmerge [(FParam (Aliases lore), SubExp)]
valmerge LoopForm (Aliases lore)
form BodyT (Aliases lore)
loopbody) = do
  let merge :: [(Param (FParamInfo lore), SubExp)]
merge = [(Param (FParamInfo lore), SubExp)]
[(FParam (Aliases lore), SubExp)]
ctxmerge [(Param (FParamInfo lore), SubExp)]
-> [(Param (FParamInfo lore), SubExp)]
-> [(Param (FParamInfo lore), SubExp)]
forall a. [a] -> [a] -> [a]
++ [(Param (FParamInfo lore), SubExp)]
[(FParam (Aliases lore), SubExp)]
valmerge
      ([Param (FParamInfo lore)]
mergepat, [SubExp]
mergeexps) = [(Param (FParamInfo lore), SubExp)]
-> ([Param (FParamInfo lore)], [SubExp])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Param (FParamInfo lore), SubExp)]
merge
  [Arg]
mergeargs <- (SubExp -> TypeM lore Arg) -> [SubExp] -> TypeM lore [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM lore Arg
forall lore. Checkable lore => SubExp -> TypeM lore Arg
checkArg [SubExp]
mergeexps

  let val_free :: Names
val_free = [Param (FParamInfo lore)] -> Names
forall a. FreeIn a => a -> Names
freeIn ([Param (FParamInfo lore)] -> Names)
-> [Param (FParamInfo lore)] -> Names
forall a b. (a -> b) -> a -> b
$ ((Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore))
-> [(Param (FParamInfo lore), SubExp)] -> [Param (FParamInfo lore)]
forall a b. (a -> b) -> [a] -> [b]
map (Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore)
forall a b. (a, b) -> a
fst [(Param (FParamInfo lore), SubExp)]
[(FParam (Aliases lore), SubExp)]
valmerge
      usedInVal :: Param (FParamInfo lore) -> Bool
usedInVal Param (FParamInfo lore)
p = Param (FParamInfo lore) -> VName
forall dec. Param dec -> VName
paramName Param (FParamInfo lore)
p VName -> Names -> Bool
`nameIn` Names
val_free
  case ((Param (FParamInfo lore), SubExp) -> Bool)
-> [(Param (FParamInfo lore), SubExp)]
-> Maybe (Param (FParamInfo lore), SubExp)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Bool -> Bool
not (Bool -> Bool)
-> ((Param (FParamInfo lore), SubExp) -> Bool)
-> (Param (FParamInfo lore), SubExp)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Param (FParamInfo lore) -> Bool
usedInVal (Param (FParamInfo lore) -> Bool)
-> ((Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore))
-> (Param (FParamInfo lore), SubExp)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore)
forall a b. (a, b) -> a
fst) [(Param (FParamInfo lore), SubExp)]
[(FParam (Aliases lore), SubExp)]
ctxmerge of
    Just (Param (FParamInfo lore), SubExp)
p ->
      ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$ String
"Loop context parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Param (FParamInfo lore), SubExp) -> String
forall a. Pretty a => a -> String
pretty (Param (FParamInfo lore), SubExp)
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" unused."
    Maybe (Param (FParamInfo lore), SubExp)
Nothing ->
      () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  Scope (Aliases lore) -> TypeM lore () -> TypeM lore ()
forall lore a.
Checkable lore =>
Scope (Aliases lore) -> TypeM lore a -> TypeM lore a
binding (LoopForm (Aliases lore) -> Scope (Aliases lore)
forall lore a. Scoped lore a => a -> Scope lore
scopeOf LoopForm (Aliases lore)
form) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ do
    case LoopForm (Aliases lore)
form of
      ForLoop VName
loopvar IntType
it SubExp
boundexp [(LParam (Aliases lore), VName)]
loopvars -> do
        Param (FParamInfo lore)
iparam <- VName -> PrimType -> TypeM lore (FParam (Aliases lore))
forall lore.
Checkable lore =>
VName -> PrimType -> TypeM lore (FParam (Aliases lore))
primFParam VName
loopvar (PrimType -> TypeM lore (FParam (Aliases lore)))
-> PrimType -> TypeM lore (FParam (Aliases lore))
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
IntType IntType
it
        let funparams :: [Param (FParamInfo lore)]
funparams = Param (FParamInfo lore)
iparam Param (FParamInfo lore)
-> [Param (FParamInfo lore)] -> [Param (FParamInfo lore)]
forall a. a -> [a] -> [a]
: [Param (FParamInfo lore)]
mergepat
            paramts :: [DeclType]
paramts = (Param (FParamInfo lore) -> DeclType)
-> [Param (FParamInfo lore)] -> [DeclType]
forall a b. (a -> b) -> [a] -> [b]
map Param (FParamInfo lore) -> DeclType
forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo lore)]
funparams

        [(Param (LParamInfo lore), VName)]
-> ((Param (LParamInfo lore), VName) -> TypeM lore ())
-> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Param (LParamInfo lore), VName)]
[(LParam (Aliases lore), VName)]
loopvars (((Param (LParamInfo lore), VName) -> TypeM lore ())
 -> TypeM lore ())
-> ((Param (LParamInfo lore), VName) -> TypeM lore ())
-> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ \(Param (LParamInfo lore)
p, VName
a) -> do
          Type
a_t <- VName -> TypeM lore Type
forall lore (m :: * -> *). HasScope lore m => VName -> m Type
lookupType VName
a
          VName -> TypeM lore ()
forall lore. Checkable lore => VName -> TypeM lore ()
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 lore -> TypeM lore ()
forall lore.
Checkable lore =>
VName -> LParamInfo lore -> TypeM lore ()
checkLParamLore (Param (LParamInfo lore) -> VName
forall dec. Param dec -> VName
paramName Param (LParamInfo lore)
p) (LParamInfo lore -> TypeM lore ())
-> LParamInfo lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ Param (LParamInfo lore) -> LParamInfo lore
forall dec. Param dec -> dec
paramDec Param (LParamInfo lore)
p
              Bool -> TypeM lore () -> TypeM lore ()
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 lore -> Type
forall t. Typed t => t -> Type
typeOf (Param (LParamInfo lore) -> LParamInfo lore
forall dec. Param dec -> dec
paramDec Param (LParamInfo lore)
p)) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
                ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
                  String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$
                    String
"Loop parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Param (LParamInfo lore) -> String
forall a. Pretty a => a -> String
pretty Param (LParamInfo lore)
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
            Maybe Type
_ ->
              ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
                String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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

        Arg
boundarg <- SubExp -> TypeM lore Arg
forall lore. Checkable lore => SubExp -> TypeM lore Arg
checkArg SubExp
boundexp
        Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
forall lore. Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
checkFuncall Maybe Name
forall a. Maybe a
Nothing [DeclType]
paramts ([Arg] -> TypeM lore ()) -> [Arg] -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ Arg
boundarg Arg -> [Arg] -> [Arg]
forall a. a -> [a] -> [a]
: [Arg]
mergeargs
      WhileLoop VName
cond -> do
        case ((Param (FParamInfo lore), SubExp) -> Bool)
-> [(Param (FParamInfo lore), SubExp)]
-> Maybe (Param (FParamInfo lore), 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 lore), SubExp) -> VName)
-> (Param (FParamInfo lore), SubExp)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Param (FParamInfo lore) -> VName
forall dec. Param dec -> VName
paramName (Param (FParamInfo lore) -> VName)
-> ((Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore))
-> (Param (FParamInfo lore), SubExp)
-> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Param (FParamInfo lore), SubExp) -> Param (FParamInfo lore)
forall a b. (a, b) -> a
fst) [(Param (FParamInfo lore), SubExp)]
merge of
          Just (Param (FParamInfo lore)
condparam, SubExp
_) ->
            Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Param (FParamInfo lore) -> Type
forall dec. Typed dec => Param dec -> Type
paramType Param (FParamInfo lore)
condparam Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Bool) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
              ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
                String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore) -> Type
forall dec. Typed dec => Param dec -> Type
paramType Param (FParamInfo lore)
condparam)
                    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
          Maybe (Param (FParamInfo lore), SubExp)
Nothing ->
            ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
              String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 funparams :: [Param (FParamInfo lore)]
funparams = [Param (FParamInfo lore)]
mergepat
            paramts :: [DeclType]
paramts = (Param (FParamInfo lore) -> DeclType)
-> [Param (FParamInfo lore)] -> [DeclType]
forall a b. (a -> b) -> [a] -> [b]
map Param (FParamInfo lore) -> DeclType
forall dec. DeclTyped dec => Param dec -> DeclType
paramDeclType [Param (FParamInfo lore)]
funparams
        Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
forall lore. Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
checkFuncall Maybe Name
forall a. Maybe a
Nothing [DeclType]
paramts [Arg]
mergeargs

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

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

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

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

            let bound_here :: Names
bound_here =
                  [VName] -> Names
namesFromList ([VName] -> Names) -> [VName] -> Names
forall a b. (a -> b) -> a -> b
$
                    Scope (Aliases lore) -> [VName]
forall k a. Map k a -> [k]
M.keys (Scope (Aliases lore) -> [VName])
-> Scope (Aliases lore) -> [VName]
forall a b. (a -> b) -> a -> b
$
                      Stms (Aliases lore) -> Scope (Aliases lore)
forall lore a. Scoped lore a => a -> Scope lore
scopeOf (Stms (Aliases lore) -> Scope (Aliases lore))
-> Stms (Aliases lore) -> Scope (Aliases lore)
forall a b. (a -> b) -> a -> b
$ BodyT (Aliases lore) -> Stms (Aliases lore)
forall lore. BodyT lore -> Stms lore
bodyStms BodyT (Aliases lore)
loopbody
            (Names -> Names) -> [Names] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map (Names -> Names -> Names
`namesSubtract` Names
bound_here)
              ([Names] -> [Names]) -> TypeM lore [Names] -> TypeM lore [Names]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExp -> TypeM lore Names) -> [SubExp] -> TypeM lore [Names]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExp -> TypeM lore Names
forall lore. Checkable lore => SubExp -> TypeM lore Names
subExpAliasesM (BodyT (Aliases lore) -> [SubExp]
forall lore. BodyT lore -> [SubExp]
bodyResult BodyT (Aliases lore)
loopbody)
checkExp (Op Op (Aliases lore)
op) = do
  OpWithAliases (Op lore) -> TypeM lore ()
checker <- (Env lore -> OpWithAliases (Op lore) -> TypeM lore ())
-> TypeM lore (OpWithAliases (Op lore) -> TypeM lore ())
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env lore -> OpWithAliases (Op lore) -> TypeM lore ()
forall lore. Env lore -> OpWithAliases (Op lore) -> TypeM lore ()
envCheckOp
  OpWithAliases (Op lore) -> TypeM lore ()
checker Op (Aliases lore)
OpWithAliases (Op lore)
op

checkSOACArrayArgs ::
  Checkable lore =>
  SubExp ->
  [VName] ->
  TypeM lore [Arg]
checkSOACArrayArgs :: SubExp -> [VName] -> TypeM lore [Arg]
checkSOACArrayArgs SubExp
width [VName]
vs =
  [VName] -> (VName -> TypeM lore Arg) -> TypeM lore [Arg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VName]
vs ((VName -> TypeM lore Arg) -> TypeM lore [Arg])
-> (VName -> TypeM lore Arg) -> TypeM lore [Arg]
forall a b. (a -> b) -> a -> b
$ \VName
v -> do
    (Type
vt, Arg
v') <- VName -> TypeM lore (Type, Arg)
forall lore. Checkable lore => VName -> TypeM lore (Type, Arg)
checkSOACArrayArg VName
v
    let argSize :: SubExp
argSize = Int -> Type -> SubExp
forall u. Int -> TypeBase Shape u -> SubExp
arraySize Int
0 Type
vt
    Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SubExp
argSize SubExp -> SubExp -> Bool
forall a. Eq a => a -> a -> Bool
== SubExp
width) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore Arg
forall (m :: * -> *) a. Monad m => a -> m a
return Arg
v'
  where
    checkSOACArrayArg :: VName -> TypeM lore (Type, Arg)
checkSOACArrayArg VName
ident = do
      (Type
t, Names
als) <- SubExp -> TypeM lore Arg
forall lore. Checkable lore => SubExp -> TypeM lore Arg
checkArg (SubExp -> TypeM lore Arg) -> SubExp -> TypeM lore Arg
forall a b. (a -> b) -> a -> b
$ VName -> SubExp
Var VName
ident
      case Int -> Type -> Maybe Type
forall shape u.
ArrayShape shape =>
Int -> TypeBase shape u -> Maybe (TypeBase shape u)
peelArray Int
1 Type
t of
        Maybe Type
Nothing ->
          ErrorCase lore -> TypeM lore (Type, Arg)
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore (Type, Arg))
-> ErrorCase lore -> TypeM lore (Type, Arg)
forall a b. (a -> b) -> a -> b
$
            String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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
ident String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not an array"
        Just Type
rt -> (Type, Arg) -> TypeM lore (Type, Arg)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, (Type
rt, Names
als))

checkType ::
  Checkable lore =>
  TypeBase Shape u ->
  TypeM lore ()
checkType :: TypeBase Shape u -> TypeM lore ()
checkType (Mem (ScalarSpace [SubExp]
d PrimType
_)) = (SubExp -> TypeM lore ()) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> SubExp -> TypeM lore ()
forall lore. Checkable lore => [Type] -> SubExp -> TypeM lore ()
require [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
int64]) [SubExp]
d
checkType TypeBase Shape u
t = (SubExp -> TypeM lore Type) -> [SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp ([SubExp] -> TypeM lore ()) -> [SubExp] -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ TypeBase Shape u -> [SubExp]
forall u. TypeBase Shape u -> [SubExp]
arrayDims TypeBase Shape u
t

checkExtType ::
  Checkable lore =>
  TypeBase ExtShape u ->
  TypeM lore ()
checkExtType :: TypeBase ExtShape u -> TypeM lore ()
checkExtType = (Ext SubExp -> TypeM lore ()) -> [Ext SubExp] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Ext SubExp -> TypeM lore ()
forall lore. Checkable lore => Ext SubExp -> TypeM lore ()
checkExtDim ([Ext SubExp] -> TypeM lore ())
-> (TypeBase ExtShape u -> [Ext SubExp])
-> TypeBase ExtShape u
-> TypeM lore ()
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 lore ()
checkExtDim (Free SubExp
se) = TypeM lore Type -> TypeM lore ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TypeM lore Type -> TypeM lore ())
-> TypeM lore Type -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
se
    checkExtDim (Ext Int
_) = () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

checkPatElem ::
  Checkable lore =>
  PatElemT (LetDec lore) ->
  TypeM lore ()
checkPatElem :: PatElemT (LetDec lore) -> TypeM lore ()
checkPatElem (PatElem VName
name LetDec lore
dec) =
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore 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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    VName -> LetDec lore -> TypeM lore ()
forall lore.
Checkable lore =>
VName -> LetDec lore -> TypeM lore ()
checkLetBoundLore VName
name LetDec lore
dec

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

checkStm ::
  Checkable lore =>
  Stm (Aliases lore) ->
  TypeM lore a ->
  TypeM lore a
checkStm :: Stm (Aliases lore) -> TypeM lore a -> TypeM lore a
checkStm stm :: Stm (Aliases lore)
stm@(Let Pattern (Aliases lore)
pat (StmAux (Certificates [VName]
cs) Attrs
_ (_, dec)) Exp (Aliases lore)
e) TypeM lore a
m = do
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"When checking certificates" (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ (VName -> TypeM lore ()) -> [VName] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Type] -> VName -> TypeM lore ()
forall lore. Checkable lore => [Type] -> VName -> TypeM lore ()
requireI [PrimType -> Type
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
Cert]) [VName]
cs
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore a
context String
"When checking expression annotation" (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ ExpDec lore -> TypeM lore ()
forall lore. Checkable lore => ExpDec lore -> TypeM lore ()
checkExpLore ExpDec lore
dec
  String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore a
context (String
"When matching\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> PatternT (VarAliases, LetDec lore) -> String
forall a. Pretty a => String -> a -> String
message String
"  " PatternT (VarAliases, LetDec lore)
Pattern (Aliases lore)
pat String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nwith\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Exp (Aliases lore) -> String
forall a. Pretty a => String -> a -> String
message String
"  " Exp (Aliases lore)
e) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()
forall lore.
Checkable lore =>
Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()
matchPattern Pattern (Aliases lore)
pat Exp (Aliases lore)
e
  Scope (Aliases lore) -> TypeM lore a -> TypeM lore a
forall lore a.
Checkable lore =>
Scope (Aliases lore) -> TypeM lore a -> TypeM lore a
binding (Scope (Aliases lore) -> Scope (Aliases lore)
maybeWithoutAliases (Scope (Aliases lore) -> Scope (Aliases lore))
-> Scope (Aliases lore) -> Scope (Aliases lore)
forall a b. (a -> b) -> a -> b
$ Stm (Aliases lore) -> Scope (Aliases lore)
forall lore a. Scoped lore a => a -> Scope lore
scopeOf Stm (Aliases lore)
stm) (TypeM lore a -> TypeM lore a) -> TypeM lore a -> TypeM lore a
forall a b. (a -> b) -> a -> b
$ do
    (PatElemT (LetDec lore) -> TypeM lore ())
-> [PatElemT (LetDec lore)] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PatElemT (LetDec lore) -> TypeM lore ()
forall lore.
Checkable lore =>
PatElemT (LetDec lore) -> TypeM lore ()
checkPatElem (PatternT (LetDec lore) -> [PatElemT (LetDec lore)]
forall dec. PatternT dec -> [PatElemT dec]
patternElements (PatternT (LetDec lore) -> [PatElemT (LetDec lore)])
-> PatternT (LetDec lore) -> [PatElemT (LetDec lore)]
forall a b. (a -> b) -> a -> b
$ PatternT (VarAliases, LetDec lore) -> PatternT (LetDec lore)
forall a. PatternT (VarAliases, a) -> PatternT a
removePatternAliases PatternT (VarAliases, LetDec lore)
Pattern (Aliases lore)
pat)
    TypeM lore 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 lore) -> Scope (Aliases lore)
maybeWithoutAliases =
      case Stm (Aliases lore) -> Exp (Aliases lore)
forall lore. Stm lore -> Exp lore
stmExp Stm (Aliases lore)
stm of
        Apply {} -> (NameInfo (Aliases lore) -> NameInfo (Aliases lore))
-> Scope (Aliases lore) -> Scope (Aliases lore)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map NameInfo (Aliases lore) -> NameInfo (Aliases lore)
forall a lore b.
(Monoid a, LetDec lore ~ (a, b)) =>
NameInfo lore -> NameInfo lore
withoutAliases
        Exp (Aliases lore)
_ -> Scope (Aliases lore) -> Scope (Aliases lore)
forall a. a -> a
id
    withoutAliases :: NameInfo lore -> NameInfo lore
withoutAliases (LetName (_, ldec)) = LetDec lore -> NameInfo lore
forall lore. LetDec lore -> NameInfo lore
LetName (a
forall a. Monoid a => a
mempty, b
ldec)
    withoutAliases NameInfo lore
info = NameInfo lore
info

matchExtPattern ::
  Checkable lore =>
  Pattern (Aliases lore) ->
  [ExtType] ->
  TypeM lore ()
matchExtPattern :: Pattern (Aliases lore) -> [ExtType] -> TypeM lore ()
matchExtPattern Pattern (Aliases lore)
pat [ExtType]
ts =
  Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PatternT (VarAliases, LetDec lore) -> [ExtType]
forall dec. Typed dec => PatternT dec -> [ExtType]
expExtTypesFromPattern PatternT (VarAliases, LetDec lore)
Pattern (Aliases lore)
pat [ExtType] -> [ExtType] -> Bool
forall a. Eq a => a -> a -> Bool
== [ExtType]
ts) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ Pattern (Aliases lore)
-> [ExtType] -> Maybe String -> ErrorCase lore
forall lore.
Pattern (Aliases lore)
-> [ExtType] -> Maybe String -> ErrorCase lore
InvalidPatternError Pattern (Aliases lore)
pat [ExtType]
ts Maybe String
forall a. Maybe a
Nothing

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

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

matchExtReturns :: [ExtType] -> Result -> [Type] -> TypeM lore ()
matchExtReturns :: [ExtType] -> [SubExp] -> [Type] -> TypeM lore ()
matchExtReturns [ExtType]
rettype [SubExp]
res [Type]
ts = do
  let problem :: TypeM lore a
      problem :: TypeM lore a
problem =
        ErrorCase lore -> TypeM lore a
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore a) -> ErrorCase lore -> TypeM lore a
forall a b. (a -> b) -> a -> b
$
          String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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
              ]

  let ([SubExp]
ctx_res, [SubExp]
val_res) = Int -> [SubExp] -> ([SubExp], [SubExp])
forall a. Int -> [a] -> ([a], [a])
splitFromEnd ([ExtType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExtType]
rettype) [SubExp]
res
      ([Type]
ctx_ts, [Type]
val_ts) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitFromEnd ([ExtType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExtType]
rettype) [Type]
ts

  Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
val_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 lore ()
forall lore a. TypeM lore a
problem

  let num_exts :: Int
num_exts =
        Set Int -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Set Int -> Int) -> Set Int -> Int
forall a b. (a -> b) -> a -> b
$
          [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$
            (ExtType -> [Int]) -> [ExtType] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Ext SubExp -> Maybe Int) -> [Ext SubExp] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Ext SubExp -> Maybe Int
forall a. Ext a -> Maybe Int
isExt ([Ext SubExp] -> [Int])
-> (ExtType -> [Ext SubExp]) -> ExtType -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtType -> [Ext SubExp]
forall u. TypeBase ExtShape u -> [Ext SubExp]
arrayExtDims) [ExtType]
rettype
  Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
num_exts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SubExp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SubExp]
ctx_res) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$
        String
"Number of context results does not match number of existentials in the return type.\n"
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"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
"\ncannot match context parameters:\n  "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SubExp] -> String
forall a. Pretty a => [a] -> String
prettyTuple [SubExp]
ctx_res

  let ctx_vals :: [(SubExp, Type)]
ctx_vals = [SubExp] -> [Type] -> [(SubExp, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SubExp]
ctx_res [Type]
ctx_ts
      instantiateExt :: Int -> TypeM lore SubExp
instantiateExt Int
i = case Int -> [(SubExp, Type)] -> Maybe (SubExp, Type)
forall int a. Integral int => int -> [a] -> Maybe a
maybeNth Int
i [(SubExp, Type)]
ctx_vals of
        Just (SubExp
se, Prim (IntType IntType
Int64)) -> SubExp -> TypeM lore SubExp
forall (m :: * -> *) a. Monad m => a -> m a
return SubExp
se
        Maybe (SubExp, Type)
_ -> TypeM lore SubExp
forall lore a. TypeM lore a
problem

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

  Bool -> TypeM lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type]
rettype' [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
val_ts) TypeM lore ()
forall lore a. TypeM lore 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 lore =>
  SubExp ->
  TypeM lore Arg
checkArg :: SubExp -> TypeM lore Arg
checkArg SubExp
arg = do
  Type
argt <- SubExp -> TypeM lore Type
forall lore. Checkable lore => SubExp -> TypeM lore Type
checkSubExp SubExp
arg
  Names
als <- SubExp -> TypeM lore Names
forall lore. Checkable lore => SubExp -> TypeM lore Names
subExpAliasesM SubExp
arg
  Arg -> TypeM lore Arg
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
argt, Names
als)

checkFuncall ::
  Maybe Name ->
  [DeclType] ->
  [Arg] ->
  TypeM lore ()
checkFuncall :: Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
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 lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      Maybe Name -> [Type] -> [Type] -> ErrorCase lore
forall lore. Maybe Name -> [Type] -> [Type] -> ErrorCase lore
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 lore) -> [Type] -> ErrorCase lore
forall a b. (a -> b) -> a -> b
$ (Arg -> Type) -> [Arg] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Arg -> Type
argType [Arg]
args
  [(Diet, Arg)] -> ((Diet, Arg) -> TypeM lore ()) -> TypeM lore ()
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 lore ()) -> TypeM lore ())
-> ((Diet, Arg) -> TypeM lore ()) -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ \(Diet
d, (Type
_, Names
als)) ->
    [Occurence] -> TypeM lore ()
forall lore. [Occurence] -> TypeM lore ()
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

checkLambda ::
  Checkable lore =>
  Lambda (Aliases lore) ->
  [Arg] ->
  TypeM lore ()
checkLambda :: Lambda (Aliases lore) -> [Arg] -> TypeM lore ()
checkLambda (Lambda [LParam (Aliases lore)]
params BodyT (Aliases lore)
body [Type]
rettype) [Arg]
args = do
  let fname :: Name
fname = String -> Name
nameFromString String
"<anonymous>"
  if [Param (LParamInfo lore)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Param (LParamInfo lore)]
[LParam (Aliases lore)]
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
      Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
forall lore. Maybe Name -> [DeclType] -> [Arg] -> TypeM lore ()
checkFuncall
        Maybe Name
forall a. Maybe a
Nothing
        ((Param (LParamInfo lore) -> DeclType)
-> [Param (LParamInfo lore)] -> [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 lore) -> Type)
-> Param (LParamInfo lore)
-> DeclType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Param (LParamInfo lore) -> Type
forall dec. Typed dec => Param dec -> Type
paramType) [Param (LParamInfo lore)]
[LParam (Aliases lore)]
params)
        [Arg]
args
      let consumable :: [(VName, Names)]
consumable = [VName] -> [Names] -> [(VName, Names)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Param (LParamInfo lore) -> VName)
-> [Param (LParamInfo lore)] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map Param (LParamInfo lore) -> VName
forall dec. Param dec -> VName
paramName [Param (LParamInfo lore)]
[LParam (Aliases lore)]
params) ((Arg -> Names) -> [Arg] -> [Names]
forall a b. (a -> b) -> [a] -> [b]
map Arg -> Names
argAliases [Arg]
args)
      (Name, [DeclExtType], [(VName, NameInfo (Aliases lore))])
-> [(VName, Names)] -> TypeM lore [Names] -> TypeM lore ()
forall lore.
Checkable lore =>
(Name, [DeclExtType], [(VName, NameInfo (Aliases lore))])
-> [(VName, Names)] -> TypeM lore [Names] -> TypeM lore ()
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 lore) -> VName
forall dec. Param dec -> VName
paramName Param (LParamInfo lore)
param,
              LParamInfo (Aliases lore) -> NameInfo (Aliases lore)
forall lore. LParamInfo lore -> NameInfo lore
LParamName (LParamInfo (Aliases lore) -> NameInfo (Aliases lore))
-> LParamInfo (Aliases lore) -> NameInfo (Aliases lore)
forall a b. (a -> b) -> a -> b
$ Param (LParamInfo lore) -> LParamInfo lore
forall dec. Param dec -> dec
paramDec Param (LParamInfo lore)
param
            )
            | Param (LParamInfo lore)
param <- [Param (LParamInfo lore)]
[LParam (Aliases lore)]
params
          ]
        )
        [(VName, Names)]
consumable
        (TypeM lore [Names] -> TypeM lore ())
-> TypeM lore [Names] -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ do
          [Param (LParamInfo lore)] -> TypeM lore ()
forall lore. Checkable lore => [LParam lore] -> TypeM lore ()
checkLambdaParams [Param (LParamInfo lore)]
[LParam (Aliases lore)]
params
          (Type -> TypeM lore ()) -> [Type] -> TypeM lore ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TypeM lore ()
forall lore u. Checkable lore => TypeBase Shape u -> TypeM lore ()
checkType [Type]
rettype
          [Type] -> BodyT (Aliases lore) -> TypeM lore [Names]
forall lore.
Checkable lore =>
[Type] -> Body (Aliases lore) -> TypeM lore [Names]
checkLambdaBody [Type]
rettype BodyT (Aliases lore)
body
    else
      ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
        String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Param (LParamInfo lore)]
[LParam (Aliases lore)]
params) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" parameters:\n"
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Param (LParamInfo lore)] -> String
forall a. Pretty a => a -> String
pretty [Param (LParamInfo lore)]
[LParam (Aliases lore)]
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."

checkPrimExp :: Checkable lore => PrimExp VName -> TypeM lore ()
checkPrimExp :: PrimExp VName -> TypeM lore ()
checkPrimExp ValueExp {} = () -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkPrimExp (LeafExp VName
v PrimType
pt) = [Type] -> VName -> TypeM lore ()
forall lore. Checkable lore => [Type] -> VName -> TypeM lore ()
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 lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp (BinOp -> PrimType
binOpType BinOp
op) PrimExp VName
x
  PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp (BinOp -> PrimType
binOpType BinOp
op) PrimExp VName
y
checkPrimExp (CmpOpExp CmpOp
op PrimExp VName
x PrimExp VName
y) = do
  PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp (CmpOp -> PrimType
cmpOpType CmpOp
op) PrimExp VName
x
  PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp (CmpOp -> PrimType
cmpOpType CmpOp
op) PrimExp VName
y
checkPrimExp (UnOpExp UnOp
op PrimExp VName
x) = PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp (UnOp -> PrimType
unOpType UnOp
op) PrimExp VName
x
checkPrimExp (ConvOpExp ConvOp
op PrimExp VName
x) = PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
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 lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> (([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
    -> TypeM
         lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> TypeM
     lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (ErrorCase lore
-> TypeM
     lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore
 -> TypeM
      lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> ErrorCase lore
-> TypeM
     lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall a b. (a -> b) -> a -> b
$ String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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
     lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
forall (m :: * -> *) a. Monad m => a -> m a
return
      (Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
 -> TypeM
      lore ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue))
-> Maybe ([PrimType], PrimType, [PrimValue] -> Maybe PrimValue)
-> TypeM
     lore ([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 lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore () -> TypeM lore ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrimType
h_ret PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
/= PrimType
t) (TypeM lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 lore ())
-> [PrimType] -> [PrimExp VName] -> TypeM lore ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ PrimType -> PrimExp VName -> TypeM lore ()
forall lore.
Checkable lore =>
PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp [PrimType]
h_ts [PrimExp VName]
args

requirePrimExp :: Checkable lore => PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp :: PrimType -> PrimExp VName -> TypeM lore ()
requirePrimExp PrimType
t PrimExp VName
e = String -> TypeM lore () -> TypeM lore ()
forall lore a. String -> TypeM lore a -> TypeM lore 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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$ do
  PrimExp VName -> TypeM lore ()
forall lore. Checkable lore => PrimExp VName -> TypeM lore ()
checkPrimExp PrimExp VName
e
  Bool -> TypeM lore () -> TypeM lore ()
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 lore () -> TypeM lore ()) -> TypeM lore () -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
    ErrorCase lore -> TypeM lore ()
forall lore a. ErrorCase lore -> TypeM lore a
bad (ErrorCase lore -> TypeM lore ())
-> ErrorCase lore -> TypeM lore ()
forall a b. (a -> b) -> a -> b
$
      String -> ErrorCase lore
forall lore. String -> ErrorCase lore
TypeError (String -> ErrorCase lore) -> String -> ErrorCase lore
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 ASTLore lore => CheckableOp lore where
  checkOp :: OpWithAliases (Op lore) -> TypeM lore ()
  -- ^ Used at top level; can be locally changed with 'checkOpWith'.

-- | The class of lores that can be type-checked.
class (ASTLore lore, CanBeAliased (Op lore), CheckableOp lore) => Checkable lore where
  checkExpLore :: ExpDec lore -> TypeM lore ()
  checkBodyLore :: BodyDec lore -> TypeM lore ()
  checkFParamLore :: VName -> FParamInfo lore -> TypeM lore ()
  checkLParamLore :: VName -> LParamInfo lore -> TypeM lore ()
  checkLetBoundLore :: VName -> LetDec lore -> TypeM lore ()
  checkRetType :: [RetType lore] -> TypeM lore ()
  matchPattern :: Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()
  primFParam :: VName -> PrimType -> TypeM lore (FParam (Aliases lore))
  matchReturnType :: [RetType lore] -> Result -> TypeM lore ()
  matchBranchType :: [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
  matchLoopResult ::
    [FParam (Aliases lore)] ->
    [FParam (Aliases lore)] ->
    [SubExp] ->
    TypeM lore ()

  default checkExpLore :: ExpDec lore ~ () => ExpDec lore -> TypeM lore ()
  checkExpLore = ExpDec lore -> TypeM lore ()
forall (m :: * -> *) a. Monad m => a -> m a
return

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

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

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

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

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

  default matchPattern :: Pattern (Aliases lore) -> Exp (Aliases lore) -> TypeM lore ()
  matchPattern Pattern (Aliases lore)
pat = Pattern (Aliases lore) -> [ExtType] -> TypeM lore ()
forall lore.
Checkable lore =>
Pattern (Aliases lore) -> [ExtType] -> TypeM lore ()
matchExtPattern Pattern (Aliases lore)
pat ([ExtType] -> TypeM lore ())
-> (Exp (Aliases lore) -> TypeM lore [ExtType])
-> Exp (Aliases lore)
-> TypeM lore ()
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Exp (Aliases lore) -> TypeM lore [ExtType]
forall lore (m :: * -> *).
(HasScope lore m, TypedOp (Op lore)) =>
Exp lore -> m [ExtType]
expExtType

  default primFParam :: FParamInfo lore ~ DeclType => VName -> PrimType -> TypeM lore (FParam (Aliases lore))
  primFParam VName
name PrimType
t = Param DeclType -> TypeM lore (Param DeclType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Param DeclType -> TypeM lore (Param DeclType))
-> Param DeclType -> TypeM lore (Param DeclType)
forall a b. (a -> b) -> a -> b
$ VName -> DeclType -> Param DeclType
forall dec. VName -> dec -> Param dec
Param VName
name (PrimType -> DeclType
forall shape u. PrimType -> TypeBase shape u
Prim PrimType
t)

  default matchReturnType :: RetType lore ~ DeclExtType => [RetType lore] -> Result -> TypeM lore ()
  matchReturnType = [ExtType] -> [SubExp] -> TypeM lore ()
forall lore.
Checkable lore =>
[ExtType] -> [SubExp] -> TypeM lore ()
matchExtReturnType ([ExtType] -> [SubExp] -> TypeM lore ())
-> ([DeclExtType] -> [ExtType])
-> [DeclExtType]
-> [SubExp]
-> TypeM lore ()
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 lore ~ ExtType => [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
  matchBranchType = [BranchType lore] -> Body (Aliases lore) -> TypeM lore ()
forall lore.
Checkable lore =>
[ExtType] -> Body (Aliases lore) -> TypeM lore ()
matchExtBranchType

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