-- | Check that a value definition does not violate any consumption constraints,
-- via alias analysis.
--
-- This is a very subtle part of the language. The basic idea is "the result of
-- an expression aliases everything that goes into it", but this is in practice
-- too restrictive when we have functions (and polymorphic and higher-order
-- functions!) as well. However, we also do not want to make the user-facing
-- type system too complicated.
--
-- Our solution is to infer more precise function types, that directly talk
-- about alias information, via parametricity. These never escape into the
-- user-facing language.
--
-- Our overall philosophy is that soundness is (of course) non-negotiable, but
-- simplicity is better than flexibility. Futhark is not a language for very
-- fine-grained reasoning about aliasing.
--
-- As an example of the compromise, @x |> copy@ works and produces a fresh
-- result, whilst @id >-> copy@ loses freshness information.
--
-- Further, we only infer freshness for fully saturated higher-order functions,
-- so refactoring to take advantage of partial application may not work.
-- Likewise, we infer only the freshness of the value a function returns, not
-- of what a returned function in turn returns: that must be declared on the
-- returned lambda itself.
module Language.Futhark.TypeChecker.Consumption
  ( checkValDef,

    -- * For testing
    Alias (..),
    Aliases,
    TypeAliases,
    inferReturnFreshness,
  )
where

import Control.Monad
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.Bifoldable
import Data.Bifunctor
import Data.DList qualified as DL
import Data.Foldable
import Data.Functor.Const
import Data.Functor.Identity
import Data.List qualified as L
import Data.List.NonEmpty qualified as NE
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util (nubOrd)
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad (BoundV (..), Notes, TypeError (..), withIndexLink)
import Prelude hiding (mod)

-- | A position within a compound type. A path step is a record field name, or a
-- constructor name followed by the tuple field name of a position in its
-- payload.
type Path = [Name]

-- | A variable together with a path: the component of that variable at that
-- path, as defined by 'traverseLeaves'.  See Note [Locations].
type Location = (VName, Path)

-- | Something a value may share memory with. Every constructor but 'AliasSelf'
-- denotes a 'Location'. Its variable may be in scope, or be free: either it has
-- gone out of scope, or it is an internal name standing for an intermediate
-- value. A free alias behaves more like an equivalence class. See
-- uniqueness-error18.fut for an example of why this is necessary.
data Alias
  = AliasBound Location
  | AliasFree Location
  | -- | Used to represent unknowable internal aliasing, which for example may
    -- occur for a function that returns a nonfresh abstract type. (That
    -- abstract type may internally be a pair of arrays that alias each other.)
    AliasSelf
  deriving (Alias -> Alias -> Bool
(Alias -> Alias -> Bool) -> (Alias -> Alias -> Bool) -> Eq Alias
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Alias -> Alias -> Bool
== :: Alias -> Alias -> Bool
$c/= :: Alias -> Alias -> Bool
/= :: Alias -> Alias -> Bool
Eq, Eq Alias
Eq Alias =>
(Alias -> Alias -> Ordering)
-> (Alias -> Alias -> Bool)
-> (Alias -> Alias -> Bool)
-> (Alias -> Alias -> Bool)
-> (Alias -> Alias -> Bool)
-> (Alias -> Alias -> Alias)
-> (Alias -> Alias -> Alias)
-> Ord Alias
Alias -> Alias -> Bool
Alias -> Alias -> Ordering
Alias -> Alias -> Alias
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
$ccompare :: Alias -> Alias -> Ordering
compare :: Alias -> Alias -> Ordering
$c< :: Alias -> Alias -> Bool
< :: Alias -> Alias -> Bool
$c<= :: Alias -> Alias -> Bool
<= :: Alias -> Alias -> Bool
$c> :: Alias -> Alias -> Bool
> :: Alias -> Alias -> Bool
$c>= :: Alias -> Alias -> Bool
>= :: Alias -> Alias -> Bool
$cmax :: Alias -> Alias -> Alias
max :: Alias -> Alias -> Alias
$cmin :: Alias -> Alias -> Alias
min :: Alias -> Alias -> Alias
Ord, Int -> Alias -> ShowS
[Alias] -> ShowS
Alias -> [Char]
(Int -> Alias -> ShowS)
-> (Alias -> [Char]) -> ([Alias] -> ShowS) -> Show Alias
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Alias -> ShowS
showsPrec :: Int -> Alias -> ShowS
$cshow :: Alias -> [Char]
show :: Alias -> [Char]
$cshowList :: [Alias] -> ShowS
showList :: [Alias] -> ShowS
Show)

instance Pretty Alias where
  pretty :: forall ann. Alias -> Doc ann
pretty (AliasBound (VName
v, [Name]
fs)) = VName -> [Name] -> Doc ann
forall ann. VName -> [Name] -> Doc ann
prettyAlias VName
v [Name]
fs
  pretty (AliasFree (VName
v, [Name]
fs)) = Doc ann
"~" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> VName -> [Name] -> Doc ann
forall ann. VName -> [Name] -> Doc ann
prettyAlias VName
v [Name]
fs
  pretty Alias
AliasSelf = Doc ann
"self"

-- | The location an alias refers to.  'AliasSelf' refers to none.
aliasLoc :: Alias -> Maybe Location
aliasLoc :: Alias -> Maybe Location
aliasLoc (AliasBound Location
l) = Location -> Maybe Location
forall a. a -> Maybe a
Just Location
l
aliasLoc (AliasFree Location
l) = Location -> Maybe Location
forall a. a -> Maybe a
Just Location
l
aliasLoc Alias
AliasSelf = Maybe Location
forall a. Maybe a
Nothing

-- | The variable an alias refers to.  'AliasSelf' does not refer to any
-- variable, as it denotes aliasing internal to a value.
aliasVar :: Alias -> Maybe VName
aliasVar :: Alias -> Maybe VName
aliasVar = (Location -> VName) -> Maybe Location -> Maybe VName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Location -> VName
forall a b. (a, b) -> a
fst (Maybe Location -> Maybe VName)
-> (Alias -> Maybe Location) -> Alias -> Maybe VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> Maybe Location
aliasLoc

-- | Apply a function to every leaf of a type (every component that is neither a
-- record nor a sum) along with its path.
traverseLeaves ::
  (Applicative f) =>
  (Path -> TypeBase dim o -> f (TypeBase dim v)) ->
  TypeBase dim o ->
  f (TypeBase dim v)
traverseLeaves :: forall (f :: * -> *) dim o v.
Applicative f =>
([Name] -> TypeBase dim o -> f (TypeBase dim v))
-> TypeBase dim o -> f (TypeBase dim v)
traverseLeaves [Name] -> TypeBase dim o -> f (TypeBase dim v)
f = [Name] -> TypeBase dim o -> f (TypeBase dim v)
go []
  where
    go :: [Name] -> TypeBase dim o -> f (TypeBase dim v)
go [Name]
p (Scalar (Record Map Name (TypeBase dim o)
ts)) =
      ScalarTypeBase dim v -> TypeBase dim v
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase dim v -> TypeBase dim v)
-> (Map Name (TypeBase dim v) -> ScalarTypeBase dim v)
-> Map Name (TypeBase dim v)
-> TypeBase dim v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (TypeBase dim v) -> ScalarTypeBase dim v
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name (TypeBase dim v) -> TypeBase dim v)
-> f (Map Name (TypeBase dim v)) -> f (TypeBase dim v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> TypeBase dim o -> f (TypeBase dim v))
-> Map Name (TypeBase dim o) -> f (Map Name (TypeBase dim v))
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey (\Name
k -> [Name] -> TypeBase dim o -> f (TypeBase dim v)
go ([Name]
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
k])) Map Name (TypeBase dim o)
ts
    go [Name]
p (Scalar (Sum Map Name [TypeBase dim o]
cs)) =
      ScalarTypeBase dim v -> TypeBase dim v
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase dim v -> TypeBase dim v)
-> (Map Name [TypeBase dim v] -> ScalarTypeBase dim v)
-> Map Name [TypeBase dim v]
-> TypeBase dim v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeBase dim v] -> ScalarTypeBase dim v
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeBase dim v] -> TypeBase dim v)
-> f (Map Name [TypeBase dim v]) -> f (TypeBase dim v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> [TypeBase dim o] -> f [TypeBase dim v])
-> Map Name [TypeBase dim o] -> f (Map Name [TypeBase dim v])
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey (\Name
c -> (Name -> TypeBase dim o -> f (TypeBase dim v))
-> [Name] -> [TypeBase dim o] -> f [TypeBase dim v]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Name
i -> [Name] -> TypeBase dim o -> f (TypeBase dim v)
go ([Name]
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
c, Name
i])) [Name]
tupleFieldNames) Map Name [TypeBase dim o]
cs
    go [Name]
p TypeBase dim o
t = [Name] -> TypeBase dim o -> f (TypeBase dim v)
f [Name]
p TypeBase dim o
t

-- | Apply a function to every leaf of a type along with its path.
mapLeaves :: (Path -> TypeBase dim o -> TypeBase dim v) -> TypeBase dim o -> TypeBase dim v
mapLeaves :: forall dim o v.
([Name] -> TypeBase dim o -> TypeBase dim v)
-> TypeBase dim o -> TypeBase dim v
mapLeaves [Name] -> TypeBase dim o -> TypeBase dim v
f = Identity (TypeBase dim v) -> TypeBase dim v
forall a. Identity a -> a
runIdentity (Identity (TypeBase dim v) -> TypeBase dim v)
-> (TypeBase dim o -> Identity (TypeBase dim v))
-> TypeBase dim o
-> TypeBase dim v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name] -> TypeBase dim o -> Identity (TypeBase dim v))
-> TypeBase dim o -> Identity (TypeBase dim v)
forall (f :: * -> *) dim o v.
Applicative f =>
([Name] -> TypeBase dim o -> f (TypeBase dim v))
-> TypeBase dim o -> f (TypeBase dim v)
traverseLeaves (\[Name]
p -> TypeBase dim v -> Identity (TypeBase dim v)
forall a. a -> Identity a
Identity (TypeBase dim v -> Identity (TypeBase dim v))
-> (TypeBase dim o -> TypeBase dim v)
-> TypeBase dim o
-> Identity (TypeBase dim v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> TypeBase dim o -> TypeBase dim v
f [Name]
p)

-- | The leaves of a type along with their paths.
leaves :: TypeBase dim o -> [(Path, TypeBase dim o)]
leaves :: forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves = Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0))
-> [([Name], TypeBase dim o)]
forall {k} a (b :: k). Const a b -> a
getConst (Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0))
 -> [([Name], TypeBase dim o)])
-> (TypeBase dim o
    -> Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0)))
-> TypeBase dim o
-> [([Name], TypeBase dim o)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name]
 -> TypeBase dim o
 -> Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0)))
-> TypeBase dim o
-> Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0))
forall (f :: * -> *) dim o v.
Applicative f =>
([Name] -> TypeBase dim o -> f (TypeBase dim v))
-> TypeBase dim o -> f (TypeBase dim v)
traverseLeaves (\[Name]
p TypeBase dim o
t -> [([Name], TypeBase dim o)]
-> Const [([Name], TypeBase dim o)] (TypeBase dim (ZonkAny 0))
forall {k} a (b :: k). a -> Const a b
Const [([Name]
p, TypeBase dim o
t)])

-- | The locations these aliases refer to.
aliasLocs :: Aliases -> [Location]
aliasLocs :: Aliases -> [Location]
aliasLocs = (Alias -> Maybe Location) -> [Alias] -> [Location]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Alias -> Maybe Location
aliasLoc ([Alias] -> [Location])
-> (Aliases -> [Alias]) -> Aliases -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Alias]
forall a. Set a -> [a]
S.toList

-- | The variables these aliases refer to.  'AliasSelf' contributes nothing,
-- as it refers to no variable.
aliasVars :: Aliases -> S.Set VName
aliasVars :: Aliases -> Set VName
aliasVars = [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName)
-> (Aliases -> [VName]) -> Aliases -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Alias -> Maybe VName) -> [Alias] -> [VName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Alias -> Maybe VName
aliasVar ([Alias] -> [VName]) -> (Aliases -> [Alias]) -> Aliases -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Alias]
forall a. Set a -> [a]
S.toList

-- | Does this value have internal aliasing, meaning it can neither be consumed
-- nor given a fresh type?  See 'AliasSelf'.
selfAliased :: Aliases -> Bool
selfAliased :: Aliases -> Bool
selfAliased = Alias -> Aliases -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Alias
AliasSelf

-- | Might two values with these aliases share memory? This is not the same
-- question as whether the sets intersect: 'AliasSelf' denotes a property of a
-- single value rather than a shared referent ('aliasVar' is 'Nothing' for it),
-- so two values that both have internal aliasing are not thereby aliases of
-- each other. Avoid comparing alias sets in any other way than through this
-- function.
overlaps :: Aliases -> Aliases -> Bool
overlaps :: Aliases -> Aliases -> Bool
overlaps Aliases
x Aliases
y = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Aliases -> Aliases -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.disjoint (Aliases -> Aliases
referents Aliases
x) (Aliases -> Aliases
referents Aliases
y)
  where
    referents :: Aliases -> Aliases
referents = (Alias -> Bool) -> Aliases -> Aliases
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Maybe VName -> Bool
forall a. Maybe a -> Bool
isJust (Maybe VName -> Bool) -> (Alias -> Maybe VName) -> Alias -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> Maybe VName
aliasVar)

prettyAlias :: VName -> [Name] -> Doc ann
prettyAlias :: forall ann. VName -> [Name] -> Doc ann
prettyAlias VName
v [Name]
fs = VName -> Doc ann
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall a. Monoid a => [a] -> a
mconcat ((Name -> Doc ann) -> [Name] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>) (Doc ann -> Doc ann) -> (Name -> Doc ann) -> Name -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc ann
forall a. Name -> Doc a
forall v a. IsName v => v -> Doc a
prettyName) [Name]
fs)

instance Pretty (S.Set Alias) where
  pretty :: forall ann. Aliases -> Doc ann
pretty = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> (Aliases -> Doc ann) -> Aliases -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall a. [Doc a] -> Doc a
commasep ([Doc ann] -> Doc ann)
-> (Aliases -> [Doc ann]) -> Aliases -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Alias -> Doc ann) -> [Alias] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Alias -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Alias -> Doc ann
pretty ([Alias] -> [Doc ann])
-> (Aliases -> [Alias]) -> Aliases -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Alias]
forall a. Set a -> [a]
S.toList

-- | Does this alias refer to an in-scope variable?  'AliasFree' has left
-- scope and 'AliasSelf' is no variable at all.  This is not the way to ask
-- whether two values may share memory; see 'overlaps'.
isBoundAlias :: Alias -> Bool
isBoundAlias :: Alias -> Bool
isBoundAlias AliasBound {} = Bool
True
isBoundAlias Alias
_ = Bool
False

-- | What a value may share memory with.
type Aliases = S.Set Alias

type TypeAliases = TypeBase Size Aliases

-- | @t \`setAliases\` als@ returns @t@, but with @als@ substituted for
-- any already present aliases.
setAliases :: TypeBase dim o1 -> o2 -> TypeBase dim o2
setAliases :: forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
setAliases TypeBase dim o1
t = TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
forall dim o1 o2. TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
addAliases TypeBase dim o1
t ((o1 -> o2) -> TypeBase dim o2)
-> (o2 -> o1 -> o2) -> o2 -> TypeBase dim o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o2 -> o1 -> o2
forall a b. a -> b -> a
const

-- | @t \`addAliases\` f@ returns @t@, but with any already present
-- aliases replaced by @f@ applied to that aliases.
addAliases :: TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
addAliases :: forall dim o1 o2. TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
addAliases = ((o1 -> o2) -> TypeBase dim o1 -> TypeBase dim o2)
-> TypeBase dim o1 -> (o1 -> o2) -> TypeBase dim o2
forall a b c. (a -> b -> c) -> b -> a -> c
flip (o1 -> o2) -> TypeBase dim o1 -> TypeBase dim o2
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second

aliases :: TypeAliases -> Aliases
aliases :: TypeAliases -> Aliases
aliases = (Size -> Aliases) -> (Aliases -> Aliases) -> TypeAliases -> Aliases
forall m a b. Monoid m => (a -> m) -> (b -> m) -> TypeBase a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (Aliases -> Size -> Aliases
forall a b. a -> b -> a
const Aliases
forall a. Monoid a => a
mempty) Aliases -> Aliases
forall a. a -> a
id

-- | Add an alias to a leaf of a type. That means we assume the type passed in
-- here is not a compound type.
aliasLeaf :: Alias -> TypeAliases -> TypeAliases
aliasLeaf :: Alias -> TypeAliases -> TypeAliases
aliasLeaf Alias
a (Array Aliases
als Shape Size
shape ScalarTypeBase Size NoMode
et) = Aliases -> Shape Size -> ScalarTypeBase Size NoMode -> TypeAliases
forall dim o.
o -> Shape dim -> ScalarTypeBase dim NoMode -> TypeBase dim o
Array (Alias -> Aliases -> Aliases
forall a. Ord a => a -> Set a -> Set a
S.insert Alias
a Aliases
als) Shape Size
shape ScalarTypeBase Size NoMode
et
aliasLeaf Alias
a (Scalar (TypeVar Aliases
als QualName VName
tn [TypeArg Size]
args)) = ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size Aliases
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar (Alias -> Aliases -> Aliases
forall a. Ord a => a -> Set a -> Set a
S.insert Alias
a Aliases
als) QualName VName
tn [TypeArg Size]
args
aliasLeaf Alias
a (Scalar (Arrow Aliases
als PName
mn Diet
d StructType
ps RetTypeBase Size Freshness
rt)) = ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow (Alias -> Aliases -> Aliases
forall a. Ord a => a -> Set a -> Set a
S.insert Alias
a Aliases
als) PName
mn Diet
d StructType
ps RetTypeBase Size Freshness
rt
aliasLeaf Alias
_ TypeAliases
t = TypeAliases
t

-- | @insertSelfAliases v t@ adds an alias of @v@ to every component of @t@,
-- noting the path at which the component sits.
insertSelfAliases :: VName -> TypeAliases -> TypeAliases
insertSelfAliases :: VName -> TypeAliases -> TypeAliases
insertSelfAliases VName
v = ([Name] -> TypeAliases -> TypeAliases)
-> TypeAliases -> TypeAliases
forall dim o v.
([Name] -> TypeBase dim o -> TypeBase dim v)
-> TypeBase dim o -> TypeBase dim v
mapLeaves (([Name] -> TypeAliases -> TypeAliases)
 -> TypeAliases -> TypeAliases)
-> ([Name] -> TypeAliases -> TypeAliases)
-> TypeAliases
-> TypeAliases
forall a b. (a -> b) -> a -> b
$ Alias -> TypeAliases -> TypeAliases
aliasLeaf (Alias -> TypeAliases -> TypeAliases)
-> ([Name] -> Alias) -> [Name] -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> Alias
AliasBound (Location -> Alias) -> ([Name] -> Location) -> [Name] -> Alias
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName
v,)

-- | Does any component of the value that this type ultimately produces satisfy
-- the predicate? Function types are followed to their (curried) result, as the
-- only way to obtain a value from a function is to apply it.
anyResultComponent :: (ResType -> Bool) -> ResType -> Bool
anyResultComponent :: (ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
p (Scalar (Arrow Freshness
_ PName
_ Diet
_ StructType
_ (RetType [VName]
_ ResType
t))) = (ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
p ResType
t
anyResultComponent ResType -> Bool
p (Scalar (Record Map Name ResType
fs)) = (ResType -> Bool) -> Map Name ResType -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
p) Map Name ResType
fs
anyResultComponent ResType -> Bool
p (Scalar (Sum Map Name [ResType]
cs)) = ([ResType] -> Bool) -> Map Name [ResType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((ResType -> Bool) -> [ResType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
p)) Map Name [ResType]
cs
anyResultComponent ResType -> Bool
p ResType
t = ResType -> Bool
p ResType
t

-- | The aliases of a use of the global @v@, given its type scheme and the type
-- it is used at. A use of a global name aliases that name, except where
-- parametricity rules it out. In particular, a non-function component whose
-- declared type contains one of the type parameters cannot be (part of) a
-- global, and a function can only yield a value aliasing a global if some
-- nonfresh component of its result is not of that kind. See Note [Parametric
-- results].
globalAliases :: VName -> BoundV -> StructType -> TypeAliases
globalAliases :: VName -> BoundV -> StructType -> TypeAliases
globalAliases VName
v (BoundV [TypeParam]
tparams StructType
decl) = ([Name] -> TypeAliases -> TypeAliases)
-> TypeAliases -> TypeAliases
forall dim o v.
([Name] -> TypeBase dim o -> TypeBase dim v)
-> TypeBase dim o -> TypeBase dim v
mapLeaves [Name] -> TypeAliases -> TypeAliases
onLeaf (TypeAliases -> TypeAliases)
-> (StructType -> TypeAliases) -> StructType -> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NoMode -> Aliases) -> StructType -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Aliases -> NoMode -> Aliases
forall a b. a -> b -> a
const Aliases
forall a. Monoid a => a
mempty)
  where
    tparams' :: Set VName
tparams' = [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList [VName
p | TypeParamType Liftedness
_ VName
p SrcLoc
_ <- [TypeParam]
tparams]

    -- A type parameter counts only where it is itself a type, not where it is
    -- an argument to an abstract type, which may ignore it.
    parametric :: TypeBase Size u -> Bool
    parametric :: forall u. TypeBase Size u -> Bool
parametric (Array u
_ Shape Size
_ ScalarTypeBase Size NoMode
et) = StructType -> Bool
forall u. TypeBase Size u -> Bool
parametric (StructType -> Bool) -> StructType -> Bool
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Size NoMode
et
    parametric (Scalar (TypeVar u
_ QualName VName
tn [TypeArg Size]
_)) = QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
tn VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tparams'
    parametric (Scalar (Record Map Name (TypeBase Size u)
fs)) = (TypeBase Size u -> Bool) -> Map Name (TypeBase Size u) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeBase Size u -> Bool
forall u. TypeBase Size u -> Bool
parametric Map Name (TypeBase Size u)
fs
    parametric (Scalar (Sum Map Name [TypeBase Size u]
cs)) = ([TypeBase Size u] -> Bool) -> Map Name [TypeBase Size u] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((TypeBase Size u -> Bool) -> [TypeBase Size u] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeBase Size u -> Bool
forall u. TypeBase Size u -> Bool
parametric) Map Name [TypeBase Size u]
cs
    parametric TypeBase Size u
_ = Bool
False

    decl_leaves :: [([Name], StructType)]
decl_leaves = StructType -> [([Name], StructType)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves StructType
decl

    onLeaf :: [Name] -> TypeAliases -> TypeAliases
onLeaf [Name]
p TypeAliases
t =
      case [StructType] -> Maybe StructType
forall a. [a] -> Maybe a
listToMaybe [StructType
d | ([Name]
dp, StructType
d) <- [([Name], StructType)]
decl_leaves, [Name]
dp [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [Name]
p] of
        Just d :: StructType
d@(Scalar Arrow {})
          | (ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
maybeGlobal (Freshness -> StructType -> ResType
forall o. Freshness -> TypeBase Size o -> ResType
toRes Freshness
Nonfresh StructType
d) ->
              Alias -> TypeAliases -> TypeAliases
aliasLeaf (Location -> Alias
AliasBound (VName
v, [Name]
p)) TypeAliases
t
          | Bool
otherwise -> TypeAliases
t
        Just StructType
d | StructType -> Bool
forall u. TypeBase Size u -> Bool
parametric StructType
d -> TypeAliases
t
        Maybe StructType
_ -> Alias -> TypeAliases -> TypeAliases
aliasLeaf (Location -> Alias
AliasBound (VName
v, [Name]
p)) TypeAliases
t

    maybeGlobal :: ResType -> Bool
maybeGlobal t :: ResType
t@(Array Freshness
Nonfresh Shape Size
_ ScalarTypeBase Size NoMode
_) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ResType -> Bool
forall u. TypeBase Size u -> Bool
parametric ResType
t
    maybeGlobal t :: ResType
t@(Scalar (TypeVar Freshness
Nonfresh QualName VName
_ [TypeArg Size]
_)) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ResType -> Bool
forall u. TypeBase Size u -> Bool
parametric ResType
t
    maybeGlobal ResType
_ = Bool
False

-- | Instantiate the aliases of a local binding at the type of an occurrence,
-- just as the type of a global is instantiated. The binding's type is that of
-- its definition, which for a local function may be polymorphic: where it has a
-- type parameter, every part of what the occurrence instantiates it with gets
-- the aliases, or in a return type the freshness, of that type parameter.
instantiateAliases :: TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases :: forall u. TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases
  (Scalar (Arrow u
_ PName
_ Diet
_ StructType
t_p (RetType [VName]
_ ResType
t_r)))
  (Scalar (Arrow Aliases
als PName
pn Diet
d StructType
_ (RetType [VName]
ext ResType
r))) =
    ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow Aliases
als PName
pn Diet
d StructType
t_p (RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases)
-> RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext (ResType -> RetTypeBase Size Freshness)
-> ResType -> RetTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$ ResType -> ResType -> ResType
forall u. TypeBase Size u -> ResType -> ResType
instantiateFreshness ResType
t_r ResType
r
instantiateAliases (Scalar (Record Map Name (TypeBase Size u)
ts)) (Scalar (Record Map Name TypeAliases
als)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (TypeBase Size u -> TypeAliases -> TypeAliases)
-> Map Name (TypeBase Size u)
-> Map Name TypeAliases
-> Map Name TypeAliases
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase Size u -> TypeAliases -> TypeAliases
forall u. TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases Map Name (TypeBase Size u)
ts Map Name TypeAliases
als
instantiateAliases (Scalar (Sum Map Name [TypeBase Size u]
ts)) (Scalar (Sum Map Name [TypeAliases]
als)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ ([TypeBase Size u] -> [TypeAliases] -> [TypeAliases])
-> Map Name [TypeBase Size u]
-> Map Name [TypeAliases]
-> Map Name [TypeAliases]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith ((TypeBase Size u -> TypeAliases -> TypeAliases)
-> [TypeBase Size u] -> [TypeAliases] -> [TypeAliases]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TypeBase Size u -> TypeAliases -> TypeAliases
forall u. TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases) Map Name [TypeBase Size u]
ts Map Name [TypeAliases]
als
instantiateAliases TypeBase Size u
t TypeAliases
als = TypeBase Size u
t TypeBase Size u -> Aliases -> TypeAliases
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setAliases` TypeAliases -> Aliases
aliases TypeAliases
als

-- | Like 'instantiateAliases', but for the freshness of a return type.
instantiateFreshness :: TypeBase Size u -> ResType -> ResType
instantiateFreshness :: forall u. TypeBase Size u -> ResType -> ResType
instantiateFreshness
  (Scalar (Arrow u
_ PName
_ Diet
_ StructType
t_p (RetType [VName]
_ ResType
t_r)))
  (Scalar (Arrow Freshness
u PName
pn Diet
d StructType
_ (RetType [VName]
ext ResType
r))) =
    ScalarTypeBase Size Freshness -> ResType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Freshness -> ResType)
-> ScalarTypeBase Size Freshness -> ResType
forall a b. (a -> b) -> a -> b
$ Freshness
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Freshness
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow Freshness
u PName
pn Diet
d StructType
t_p (RetTypeBase Size Freshness -> ScalarTypeBase Size Freshness)
-> RetTypeBase Size Freshness -> ScalarTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext (ResType -> RetTypeBase Size Freshness)
-> ResType -> RetTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$ ResType -> ResType -> ResType
forall u. TypeBase Size u -> ResType -> ResType
instantiateFreshness ResType
t_r ResType
r
instantiateFreshness (Scalar (Record Map Name (TypeBase Size u)
ts)) (Scalar (Record Map Name ResType
rs)) =
  ScalarTypeBase Size Freshness -> ResType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Freshness -> ResType)
-> ScalarTypeBase Size Freshness -> ResType
forall a b. (a -> b) -> a -> b
$ Map Name ResType -> ScalarTypeBase Size Freshness
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name ResType -> ScalarTypeBase Size Freshness)
-> Map Name ResType -> ScalarTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$ (TypeBase Size u -> ResType -> ResType)
-> Map Name (TypeBase Size u)
-> Map Name ResType
-> Map Name ResType
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase Size u -> ResType -> ResType
forall u. TypeBase Size u -> ResType -> ResType
instantiateFreshness Map Name (TypeBase Size u)
ts Map Name ResType
rs
instantiateFreshness (Scalar (Sum Map Name [TypeBase Size u]
ts)) (Scalar (Sum Map Name [ResType]
rs)) =
  ScalarTypeBase Size Freshness -> ResType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Freshness -> ResType)
-> ScalarTypeBase Size Freshness -> ResType
forall a b. (a -> b) -> a -> b
$ Map Name [ResType] -> ScalarTypeBase Size Freshness
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [ResType] -> ScalarTypeBase Size Freshness)
-> Map Name [ResType] -> ScalarTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$ ([TypeBase Size u] -> [ResType] -> [ResType])
-> Map Name [TypeBase Size u]
-> Map Name [ResType]
-> Map Name [ResType]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith ((TypeBase Size u -> ResType -> ResType)
-> [TypeBase Size u] -> [ResType] -> [ResType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TypeBase Size u -> ResType -> ResType
forall u. TypeBase Size u -> ResType -> ResType
instantiateFreshness) Map Name [TypeBase Size u]
ts Map Name [ResType]
rs
instantiateFreshness TypeBase Size u
t ResType
r = TypeBase Size u
t TypeBase Size u -> Freshness -> ResType
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` ResType -> Freshness
forall shape. TypeBase shape Freshness -> Freshness
freshness ResType
r

-- | Update the aliases at a given position. It is expected that the second
-- 'TypeAliases' has the same type (modulo alias information) as the field at
-- the given path.
updateAliases :: TypeAliases -> [UpdateStep Info VName] -> TypeAliases -> TypeAliases
updateAliases :: TypeAliases
-> [UpdateStep Info VName] -> TypeAliases -> TypeAliases
updateAliases TypeAliases
_ [] TypeAliases
ve_als =
  TypeAliases
ve_als
updateAliases (Scalar (Record Map Name TypeAliases
fs)) (UpdateStepField Name
f : [UpdateStep Info VName]
rest) TypeAliases
ve_als
  | Just TypeAliases
sub <- Name -> Map Name TypeAliases -> Maybe TypeAliases
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
f Map Name TypeAliases
fs =
      ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ Name -> TypeAliases -> Map Name TypeAliases -> Map Name TypeAliases
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
f (TypeAliases
-> [UpdateStep Info VName] -> TypeAliases -> TypeAliases
updateAliases TypeAliases
sub [UpdateStep Info VName]
rest TypeAliases
ve_als) Map Name TypeAliases
fs
updateAliases TypeAliases
src_als (UpdateStepSlice SliceBase Info VName
_ : [UpdateStep Info VName]
_) TypeAliases
_ = (Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Aliases -> Aliases -> Aliases
forall a b. a -> b -> a
const Aliases
forall a. Monoid a => a
mempty) TypeAliases
src_als
updateAliases TypeAliases
src_als [UpdateStep Info VName]
_ TypeAliases
_ = [Char] -> TypeAliases
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeAliases) -> [Char] -> TypeAliases
forall a b. (a -> b) -> a -> b
$ [Char]
"updateAliases: no such field in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> [Char]
forall a. Pretty a => a -> [Char]
prettyString TypeAliases
src_als

data Entry a
  = Consumable {forall a. Entry a -> a
entryAliases :: a}
  | Nonconsumable {entryAliases :: a}
  deriving (Entry a -> Entry a -> Bool
(Entry a -> Entry a -> Bool)
-> (Entry a -> Entry a -> Bool) -> Eq (Entry a)
forall a. Eq a => Entry a -> Entry a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Entry a -> Entry a -> Bool
== :: Entry a -> Entry a -> Bool
$c/= :: forall a. Eq a => Entry a -> Entry a -> Bool
/= :: Entry a -> Entry a -> Bool
Eq, Eq (Entry a)
Eq (Entry a) =>
(Entry a -> Entry a -> Ordering)
-> (Entry a -> Entry a -> Bool)
-> (Entry a -> Entry a -> Bool)
-> (Entry a -> Entry a -> Bool)
-> (Entry a -> Entry a -> Bool)
-> (Entry a -> Entry a -> Entry a)
-> (Entry a -> Entry a -> Entry a)
-> Ord (Entry a)
Entry a -> Entry a -> Bool
Entry a -> Entry a -> Ordering
Entry a -> Entry a -> Entry a
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
forall a. Ord a => Eq (Entry a)
forall a. Ord a => Entry a -> Entry a -> Bool
forall a. Ord a => Entry a -> Entry a -> Ordering
forall a. Ord a => Entry a -> Entry a -> Entry a
$ccompare :: forall a. Ord a => Entry a -> Entry a -> Ordering
compare :: Entry a -> Entry a -> Ordering
$c< :: forall a. Ord a => Entry a -> Entry a -> Bool
< :: Entry a -> Entry a -> Bool
$c<= :: forall a. Ord a => Entry a -> Entry a -> Bool
<= :: Entry a -> Entry a -> Bool
$c> :: forall a. Ord a => Entry a -> Entry a -> Bool
> :: Entry a -> Entry a -> Bool
$c>= :: forall a. Ord a => Entry a -> Entry a -> Bool
>= :: Entry a -> Entry a -> Bool
$cmax :: forall a. Ord a => Entry a -> Entry a -> Entry a
max :: Entry a -> Entry a -> Entry a
$cmin :: forall a. Ord a => Entry a -> Entry a -> Entry a
min :: Entry a -> Entry a -> Entry a
Ord, Int -> Entry a -> ShowS
[Entry a] -> ShowS
Entry a -> [Char]
(Int -> Entry a -> ShowS)
-> (Entry a -> [Char]) -> ([Entry a] -> ShowS) -> Show (Entry a)
forall a. Show a => Int -> Entry a -> ShowS
forall a. Show a => [Entry a] -> ShowS
forall a. Show a => Entry a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Entry a -> ShowS
showsPrec :: Int -> Entry a -> ShowS
$cshow :: forall a. Show a => Entry a -> [Char]
show :: Entry a -> [Char]
$cshowList :: forall a. Show a => [Entry a] -> ShowS
showList :: [Entry a] -> ShowS
Show)

instance Functor Entry where
  fmap :: forall a b. (a -> b) -> Entry a -> Entry b
fmap a -> b
f (Consumable a
als) = b -> Entry b
forall a. a -> Entry a
Consumable (b -> Entry b) -> b -> Entry b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
als
  fmap a -> b
f (Nonconsumable a
als) = b -> Entry b
forall a. a -> Entry a
Nonconsumable (b -> Entry b) -> b -> Entry b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
als

data CheckEnv = CheckEnv
  { CheckEnv -> Map VName (Entry TypeAliases)
envVtable :: M.Map VName (Entry TypeAliases),
    -- | Location of the definition we are checking.
    CheckEnv -> Loc
envLoc :: Loc,
    -- | The declared type of a global, along with the type parameters it is
    -- polymorphic in.  This is what lets us exploit parametricity; see Note
    -- [Parametric results].
    CheckEnv -> QualName VName -> Maybe BoundV
envGlobal :: QualName VName -> Maybe BoundV
  }

-- | A description of where an artificial compiler-generated
-- intermediate name came from.
data NameReason
  = -- | Name is the result of a function application.
    NameAppRes (Maybe (QualName VName)) SrcLoc
  | -- | Name is a loop result.
    NameLoopRes SrcLoc
  | -- | Name ties together the components of the result of the given kind
    -- of branching expression; see Note [Locations].
    NameBranchRes T.Text SrcLoc

nameReason :: SrcLoc -> NameReason -> Doc a
nameReason :: forall a. SrcLoc -> NameReason -> Doc a
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
Nothing SrcLoc
apploc) =
  Doc a
"result of application at" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc a
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SrcLoc -> SrcLoc -> [Char]
forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel SrcLoc
loc SrcLoc
apploc)
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
fname SrcLoc
apploc) =
  Doc a
"result of applying"
    Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a -> Doc a
forall ann. Doc ann -> Doc ann
dquotes (Maybe (QualName VName) -> Doc a
forall ann. Maybe (QualName VName) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Maybe (QualName VName)
fname)
    Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a -> Doc a
forall ann. Doc ann -> Doc ann
parens (Doc a
"at" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc a
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SrcLoc -> SrcLoc -> [Char]
forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel SrcLoc
loc SrcLoc
apploc))
nameReason SrcLoc
loc (NameLoopRes SrcLoc
apploc) =
  Doc a
"result of loop at" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc a
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SrcLoc -> SrcLoc -> [Char]
forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel SrcLoc
loc SrcLoc
apploc)
nameReason SrcLoc
loc (NameBranchRes Text
what SrcLoc
eloc) =
  Doc a
"result of" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc a
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
what Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"at" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc a
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SrcLoc -> SrcLoc -> [Char]
forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel SrcLoc
loc SrcLoc
eloc)

-- | The locations consumed so far, each with where it was consumed.
type Consumed = M.Map Location Loc

data CheckState = CheckState
  { CheckState -> Consumed
stateConsumed :: Consumed,
    CheckState -> DList TypeError
stateErrors :: DL.DList TypeError,
    CheckState -> Map VName NameReason
stateNames :: M.Map VName NameReason,
    CheckState -> Int
stateCounter :: Int
  }

newtype CheckM a = CheckM (ReaderT CheckEnv (State CheckState) a)
  deriving
    ( (forall a b. (a -> b) -> CheckM a -> CheckM b)
-> (forall a b. a -> CheckM b -> CheckM a) -> Functor CheckM
forall a b. a -> CheckM b -> CheckM a
forall a b. (a -> b) -> CheckM a -> CheckM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> CheckM a -> CheckM b
fmap :: forall a b. (a -> b) -> CheckM a -> CheckM b
$c<$ :: forall a b. a -> CheckM b -> CheckM a
<$ :: forall a b. a -> CheckM b -> CheckM a
Functor,
      Functor CheckM
Functor CheckM =>
(forall a. a -> CheckM a)
-> (forall a b. CheckM (a -> b) -> CheckM a -> CheckM b)
-> (forall a b c.
    (a -> b -> c) -> CheckM a -> CheckM b -> CheckM c)
-> (forall a b. CheckM a -> CheckM b -> CheckM b)
-> (forall a b. CheckM a -> CheckM b -> CheckM a)
-> Applicative CheckM
forall a. a -> CheckM a
forall a b. CheckM a -> CheckM b -> CheckM a
forall a b. CheckM a -> CheckM b -> CheckM b
forall a b. CheckM (a -> b) -> CheckM a -> CheckM b
forall a b c. (a -> b -> c) -> CheckM a -> CheckM b -> CheckM 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
$cpure :: forall a. a -> CheckM a
pure :: forall a. a -> CheckM a
$c<*> :: forall a b. CheckM (a -> b) -> CheckM a -> CheckM b
<*> :: forall a b. CheckM (a -> b) -> CheckM a -> CheckM b
$cliftA2 :: forall a b c. (a -> b -> c) -> CheckM a -> CheckM b -> CheckM c
liftA2 :: forall a b c. (a -> b -> c) -> CheckM a -> CheckM b -> CheckM c
$c*> :: forall a b. CheckM a -> CheckM b -> CheckM b
*> :: forall a b. CheckM a -> CheckM b -> CheckM b
$c<* :: forall a b. CheckM a -> CheckM b -> CheckM a
<* :: forall a b. CheckM a -> CheckM b -> CheckM a
Applicative,
      Applicative CheckM
Applicative CheckM =>
(forall a b. CheckM a -> (a -> CheckM b) -> CheckM b)
-> (forall a b. CheckM a -> CheckM b -> CheckM b)
-> (forall a. a -> CheckM a)
-> Monad CheckM
forall a. a -> CheckM a
forall a b. CheckM a -> CheckM b -> CheckM b
forall a b. CheckM a -> (a -> CheckM b) -> CheckM 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
$c>>= :: forall a b. CheckM a -> (a -> CheckM b) -> CheckM b
>>= :: forall a b. CheckM a -> (a -> CheckM b) -> CheckM b
$c>> :: forall a b. CheckM a -> CheckM b -> CheckM b
>> :: forall a b. CheckM a -> CheckM b -> CheckM b
$creturn :: forall a. a -> CheckM a
return :: forall a. a -> CheckM a
Monad,
      MonadReader CheckEnv,
      MonadState CheckState
    )

runCheckM ::
  (QualName VName -> Maybe BoundV) ->
  Loc ->
  CheckM a ->
  (a, [TypeError])
runCheckM :: forall a.
(QualName VName -> Maybe BoundV)
-> Loc -> CheckM a -> (a, [TypeError])
runCheckM QualName VName -> Maybe BoundV
globals Loc
loc (CheckM ReaderT CheckEnv (State CheckState) a
m) =
  let (a
a, CheckState
s) = State CheckState a -> CheckState -> (a, CheckState)
forall s a. State s a -> s -> (a, s)
runState (ReaderT CheckEnv (State CheckState) a
-> CheckEnv -> State CheckState a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT CheckEnv (State CheckState) a
m CheckEnv
env) CheckState
initial_state
   in (a
a, DList TypeError -> [TypeError]
forall a. DList a -> [a]
DL.toList (CheckState -> DList TypeError
stateErrors CheckState
s))
  where
    env :: CheckEnv
env =
      CheckEnv
        { envVtable :: Map VName (Entry TypeAliases)
envVtable = Map VName (Entry TypeAliases)
forall a. Monoid a => a
mempty,
          envLoc :: Loc
envLoc = Loc
loc,
          envGlobal :: QualName VName -> Maybe BoundV
envGlobal = QualName VName -> Maybe BoundV
globals
        }
    initial_state :: CheckState
initial_state =
      CheckState
        { stateConsumed :: Consumed
stateConsumed = Consumed
forall a. Monoid a => a
mempty,
          stateErrors :: DList TypeError
stateErrors = DList TypeError
forall a. Monoid a => a
mempty,
          stateNames :: Map VName NameReason
stateNames = Map VName NameReason
forall a. Monoid a => a
mempty,
          stateCounter :: Int
stateCounter = Int
0
        }

incCounter :: CheckM Int
incCounter :: CheckM Int
incCounter =
  (CheckState -> (Int, CheckState)) -> CheckM Int
forall a. (CheckState -> (a, CheckState)) -> CheckM a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state ((CheckState -> (Int, CheckState)) -> CheckM Int)
-> (CheckState -> (Int, CheckState)) -> CheckM Int
forall a b. (a -> b) -> a -> b
$ \CheckState
s -> (CheckState -> Int
stateCounter CheckState
s, CheckState
s {stateCounter = stateCounter s + 1})

-- | The part of a path that steps only into records.
recordPath :: Path -> TypeBase dim o -> Path
recordPath :: forall dim o. [Name] -> TypeBase dim o -> [Name]
recordPath (Name
f : [Name]
fs) (Scalar (Record Map Name (TypeBase dim o)
ts))
  | Just TypeBase dim o
t <- Name -> Map Name (TypeBase dim o) -> Maybe (TypeBase dim o)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
f Map Name (TypeBase dim o)
ts = Name
f Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name] -> TypeBase dim o -> [Name]
forall dim o. [Name] -> TypeBase dim o -> [Name]
recordPath [Name]
fs TypeBase dim o
t
recordPath [Name]
_ TypeBase dim o
_ = []

-- | Describe a location for the user.  A path into a sum payload is not
-- something the user can write, so the path is cut off at the first sum.
describeLoc :: Location -> CheckM (Doc a)
describeLoc :: forall a. Location -> CheckM (Doc a)
describeLoc (VName
v, [Name]
fs) = do
  loc <- (CheckEnv -> Loc) -> CheckM Loc
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Loc
envLoc
  fs' <- asks $ maybe fs (recordPath fs . entryAliases) . M.lookup v . envVtable
  gets $
    maybe ("variable" <+> dquotes (prettyAlias v fs')) (nameReason (srclocOf loc))
      . M.lookup v
      . stateNames

-- | Describe a variable for the user.
describeVar :: VName -> CheckM (Doc a)
describeVar :: forall a. VName -> CheckM (Doc a)
describeVar VName
v = Location -> CheckM (Doc a)
forall a. Location -> CheckM (Doc a)
describeLoc (VName
v, [])

-- | Like 'describeVar', but naming a variable written by the programmer without
-- calling it one.
describeName :: VName -> CheckM (Doc a)
describeName :: forall a. VName -> CheckM (Doc a)
describeName VName
v = do
  loc <- (CheckEnv -> Loc) -> CheckM Loc
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Loc
envLoc
  gets $
    maybe (dquotes (prettyName v)) (nameReason (srclocOf loc))
      . M.lookup v
      . stateNames

-- | Mark everything as nonconsumable within this action.
noConsumable :: CheckM a -> CheckM a
noConsumable :: forall a. CheckM a -> CheckM a
noConsumable = (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall a. (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((CheckEnv -> CheckEnv) -> CheckM a -> CheckM a)
-> (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall a b. (a -> b) -> a -> b
$ \CheckEnv
env -> CheckEnv
env {envVtable = M.map f $ envVtable env}
  where
    f :: Entry b -> Entry b
f = b -> Entry b
forall a. a -> Entry a
Nonconsumable (b -> Entry b) -> (Entry b -> b) -> Entry b -> Entry b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry b -> b
forall a. Entry a -> a
entryAliases

addError :: (Located loc) => loc -> Notes -> Doc () -> CheckM ()
addError :: forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError loc
loc Notes
notes Doc ()
e = (CheckState -> CheckState) -> CheckM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckState -> CheckState) -> CheckM ())
-> (CheckState -> CheckState) -> CheckM ()
forall a b. (a -> b) -> a -> b
$ \CheckState
s ->
  CheckState
s {stateErrors = DL.snoc (stateErrors s) (TypeError (locOf loc) notes e)}

returnAliased :: Name -> SrcLoc -> CheckM ()
returnAliased :: Name -> SrcLoc -> CheckM ()
returnAliased Name
name SrcLoc
loc =
  SrcLoc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> (Doc () -> Doc ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"return-aliased" (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Doc ()
"Fresh-declared return value is aliased to"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall a. Name -> Doc a
forall v a. IsName v => v -> Doc a
prettyName Name
name)
      Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
", which is not consumable."

-- | Returning a value for a fresh return type is equivalent to consuming it,
-- so a value with internal aliasing cannot be returned that way.
selfAliasedReturn :: (Located loc) => loc -> CheckM ()
selfAliasedReturn :: forall loc. Located loc => loc -> CheckM ()
selfAliasedReturn loc
loc =
  loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Doc ()
"A fresh-declared component of the return value may have internal aliases,"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"and so cannot be declared fresh."

freshReturnAliased :: SrcLoc -> CheckM ()
freshReturnAliased :: SrcLoc -> CheckM ()
freshReturnAliased SrcLoc
loc =
  SrcLoc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> (Doc () -> Doc ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"fresh-return-aliased" (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Doc ()
"A fresh-declared component of the return value is aliased to some other component."

-- | A reason why a component of a function result cannot be fresh.
data Unfresh
  = -- | It aliases this variable, which is in scope and not a consumed
    -- parameter.
    UnfreshAliases VName
  | -- | It aliases a location that some other component also aliases.
    UnfreshShared
  | -- | It may have internal aliasing.
    UnfreshSelf

-- | Why a component of the result of a function with these parameters cannot be
-- fresh, given the 'sharedLocations' of the whole result. The component may be
-- fresh exactly when there is no reason. See Note [Locations].
unfreshness :: [Pat ParamType] -> S.Set Location -> TypeAliases -> [Unfresh]
unfreshness :: [Pat (TypeBase Size Diet)]
-> Set Location -> TypeAliases -> [Unfresh]
unfreshness [Pat (TypeBase Size Diet)]
params Set Location
shared TypeAliases
t_als =
  [Unfresh
UnfreshShared | (Location -> Bool) -> [Location] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Location -> Set Location -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Location
shared) (Aliases -> [Location]
aliasLocs (TypeAliases -> Aliases
aliases TypeAliases
t_als))]
    [Unfresh] -> [Unfresh] -> [Unfresh]
forall a. Semigroup a => a -> a -> a
<> [Unfresh
UnfreshSelf | Aliases -> Bool
selfAliased (TypeAliases -> Aliases
aliases TypeAliases
t_als)]
    [Unfresh] -> [Unfresh] -> [Unfresh]
forall a. Semigroup a => a -> a -> a
<> (Location -> Unfresh) -> [Location] -> [Unfresh]
forall a b. (a -> b) -> [a] -> [b]
map (VName -> Unfresh
UnfreshAliases (VName -> Unfresh) -> (Location -> VName) -> Location -> Unfresh
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> VName
forall a b. (a, b) -> a
fst) ((Location -> Bool) -> [Location] -> [Location]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Location -> Bool) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pat (TypeBase Size Diet)] -> Location -> Bool
consumedParamLoc [Pat (TypeBase Size Diet)]
params) [Location]
in_scope)
  where
    -- Mention the parameters before other variables.
    in_scope :: [Location]
in_scope =
      (Location -> Bool) -> [Location] -> [Location]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn ((VName -> [VName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (Pat (TypeBase Size Diet) -> [VName])
-> [Pat (TypeBase Size Diet)] -> [VName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pat (TypeBase Size Diet) -> [VName]
forall t. Pat t -> [VName]
patNames [Pat (TypeBase Size Diet)]
params) (VName -> Bool) -> (Location -> VName) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> VName
forall a b. (a, b) -> a
fst) ([Location] -> [Location])
-> (Aliases -> [Location]) -> Aliases -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Location] -> [Location]
forall a. Ord a => [a] -> [a]
nubOrd ([Location] -> [Location])
-> (Aliases -> [Location]) -> Aliases -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Location]
aliasLocs (Aliases -> [Location]) -> Aliases -> [Location]
forall a b. (a -> b) -> a -> b
$
        (Alias -> Bool) -> Aliases -> Aliases
forall a. (a -> Bool) -> Set a -> Set a
S.filter Alias -> Bool
isBoundAlias (Aliases -> Aliases) -> Aliases -> Aliases
forall a b. (a -> b) -> a -> b
$
          TypeAliases -> Aliases
aliases TypeAliases
t_als

-- | Check that every component of a function result declared fresh may be.
checkReturnAlias :: SrcLoc -> [Pat ParamType] -> ResType -> TypeAliases -> CheckM ()
checkReturnAlias :: SrcLoc
-> [Pat (TypeBase Size Diet)]
-> ResType
-> TypeAliases
-> CheckM ()
checkReturnAlias SrcLoc
loc [Pat (TypeBase Size Diet)]
params ResType
rettp TypeAliases
ret_als =
  [(Freshness, TypeAliases)]
-> ((Freshness, TypeAliases) -> CheckM ()) -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ResType -> TypeAliases -> [(Freshness, TypeAliases)]
forall {shape} {dim} {o}.
TypeBase shape Freshness
-> TypeBase dim o -> [(Freshness, TypeBase dim o)]
returnAliases ResType
rettp TypeAliases
ret_als) (((Freshness, TypeAliases) -> CheckM ()) -> CheckM ())
-> ((Freshness, TypeAliases) -> CheckM ()) -> CheckM ()
forall a b. (a -> b) -> a -> b
$ \(Freshness
u, TypeAliases
t_als) ->
    Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Freshness
u Freshness -> Freshness -> Bool
forall a. Eq a => a -> a -> Bool
== Freshness
Fresh) (CheckM () -> CheckM ())
-> ([Unfresh] -> CheckM ()) -> [Unfresh] -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unfresh -> CheckM ()) -> [Unfresh] -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Unfresh -> CheckM ()
report ([Unfresh] -> CheckM ()) -> [Unfresh] -> CheckM ()
forall a b. (a -> b) -> a -> b
$ [Pat (TypeBase Size Diet)]
-> Set Location -> TypeAliases -> [Unfresh]
unfreshness [Pat (TypeBase Size Diet)]
params Set Location
shared TypeAliases
t_als
  where
    shared :: Set Location
shared = TypeAliases -> Set Location
sharedLocations TypeAliases
ret_als

    report :: Unfresh -> CheckM ()
report (UnfreshAliases VName
v) = Name -> SrcLoc -> CheckM ()
returnAliased (VName -> Name
baseName VName
v) SrcLoc
loc
    report Unfresh
UnfreshShared = SrcLoc -> CheckM ()
freshReturnAliased SrcLoc
loc
    report Unfresh
UnfreshSelf = SrcLoc -> CheckM ()
forall loc. Located loc => loc -> CheckM ()
selfAliasedReturn SrcLoc
loc

    returnAliases :: TypeBase shape Freshness
-> TypeBase dim o -> [(Freshness, TypeBase dim o)]
returnAliases (Scalar (Record Map Name (TypeBase shape Freshness)
ets1)) (Scalar (Record Map Name (TypeBase dim o)
ets2)) =
      [[(Freshness, TypeBase dim o)]] -> [(Freshness, TypeBase dim o)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Freshness, TypeBase dim o)]] -> [(Freshness, TypeBase dim o)])
-> [[(Freshness, TypeBase dim o)]] -> [(Freshness, TypeBase dim o)]
forall a b. (a -> b) -> a -> b
$ Map Name [(Freshness, TypeBase dim o)]
-> [[(Freshness, TypeBase dim o)]]
forall k a. Map k a -> [a]
M.elems (Map Name [(Freshness, TypeBase dim o)]
 -> [[(Freshness, TypeBase dim o)]])
-> Map Name [(Freshness, TypeBase dim o)]
-> [[(Freshness, TypeBase dim o)]]
forall a b. (a -> b) -> a -> b
$ (TypeBase shape Freshness
 -> TypeBase dim o -> [(Freshness, TypeBase dim o)])
-> Map Name (TypeBase shape Freshness)
-> Map Name (TypeBase dim o)
-> Map Name [(Freshness, TypeBase dim o)]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase shape Freshness
-> TypeBase dim o -> [(Freshness, TypeBase dim o)]
returnAliases Map Name (TypeBase shape Freshness)
ets1 Map Name (TypeBase dim o)
ets2
    returnAliases TypeBase shape Freshness
expected TypeBase dim o
got =
      [(TypeBase shape Freshness -> Freshness
forall shape. TypeBase shape Freshness -> Freshness
freshness TypeBase shape Freshness
expected, TypeBase dim o
got)]

unscope :: [VName] -> Aliases -> Aliases
unscope :: [VName] -> Aliases -> Aliases
unscope [VName]
bound = (Alias -> Alias) -> Aliases -> Aliases
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> Alias
f
  where
    f :: Alias -> Alias
f (AliasBound (VName
v, [Name]
fs)) =
      if VName
v VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound
        then Location -> Alias
AliasFree (VName
v, [Name]
fs)
        else Location -> Alias
AliasBound (VName
v, [Name]
fs)
    f Alias
a = Alias
a

-- | Figure out the aliases of each bound name in a pattern.
matchPat :: Pat t -> TypeAliases -> DL.DList (VName, (t, TypeAliases))
matchPat :: forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat (PatParens PatBase Info VName t
p SrcLoc
_) TypeAliases
t = PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat PatBase Info VName t
p TypeAliases
t
matchPat (TuplePat [PatBase Info VName t]
ps SrcLoc
_) TypeAliases
t
  | Just [TypeAliases]
ts <- TypeAliases -> Maybe [TypeAliases]
forall dim o. TypeBase dim o -> Maybe [TypeBase dim o]
isTupleRecord TypeAliases
t = [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a. Monoid a => [a] -> a
mconcat ([DList (VName, (t, TypeAliases))]
 -> DList (VName, (t, TypeAliases)))
-> [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a b. (a -> b) -> a -> b
$ (PatBase Info VName t
 -> TypeAliases -> DList (VName, (t, TypeAliases)))
-> [PatBase Info VName t]
-> [TypeAliases]
-> [DList (VName, (t, TypeAliases))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat [PatBase Info VName t]
ps [TypeAliases]
ts
matchPat (RecordPat [(L Name, PatBase Info VName t)]
fs1 SrcLoc
_) (Scalar (Record Map Name TypeAliases
fs2)) =
  [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a. Monoid a => [a] -> a
mconcat ([DList (VName, (t, TypeAliases))]
 -> DList (VName, (t, TypeAliases)))
-> [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a b. (a -> b) -> a -> b
$
    (PatBase Info VName t
 -> TypeAliases -> DList (VName, (t, TypeAliases)))
-> [PatBase Info VName t]
-> [TypeAliases]
-> [DList (VName, (t, TypeAliases))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
      PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat
      (((Name, PatBase Info VName t) -> PatBase Info VName t)
-> [(Name, PatBase Info VName t)] -> [PatBase Info VName t]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase Info VName t) -> PatBase Info VName t
forall a b. (a, b) -> b
snd (Map Name (PatBase Info VName t) -> [(Name, PatBase Info VName t)]
forall a. Map Name a -> [(Name, a)]
sortFields ([(Name, PatBase Info VName t)] -> Map Name (PatBase Info VName t)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (((L Name, PatBase Info VName t) -> (Name, PatBase Info VName t))
-> [(L Name, PatBase Info VName t)]
-> [(Name, PatBase Info VName t)]
forall a b. (a -> b) -> [a] -> [b]
map ((L Name -> Name)
-> (L Name, PatBase Info VName t) -> (Name, PatBase Info VName t)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first L Name -> Name
forall a. L a -> a
unLoc) [(L Name, PatBase Info VName t)]
fs1))))
      (((Name, TypeAliases) -> TypeAliases)
-> [(Name, TypeAliases)] -> [TypeAliases]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd (Map Name TypeAliases -> [(Name, TypeAliases)]
forall a. Map Name a -> [(Name, a)]
sortFields Map Name TypeAliases
fs2))
matchPat (Id VName
v (Info t
t) SrcLoc
_) TypeAliases
als = (VName, (t, TypeAliases)) -> DList (VName, (t, TypeAliases))
forall a. a -> DList a
DL.singleton (VName
v, (t
t, TypeAliases
als))
matchPat (PatAscription PatBase Info VName t
p TypeExp Size VName
_ SrcLoc
_) TypeAliases
t = PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat PatBase Info VName t
p TypeAliases
t
matchPat (PatConstr Name
v Info t
_ [PatBase Info VName t]
ps SrcLoc
_) (Scalar (Sum Map Name [TypeAliases]
cs))
  | Just [TypeAliases]
ts <- Name -> Map Name [TypeAliases] -> Maybe [TypeAliases]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name [TypeAliases]
cs = [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a. Monoid a => [a] -> a
mconcat ([DList (VName, (t, TypeAliases))]
 -> DList (VName, (t, TypeAliases)))
-> [DList (VName, (t, TypeAliases))]
-> DList (VName, (t, TypeAliases))
forall a b. (a -> b) -> a -> b
$ (PatBase Info VName t
 -> TypeAliases -> DList (VName, (t, TypeAliases)))
-> [PatBase Info VName t]
-> [TypeAliases]
-> [DList (VName, (t, TypeAliases))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat [PatBase Info VName t]
ps [TypeAliases]
ts
matchPat Wildcard {} TypeAliases
_ = DList (VName, (t, TypeAliases))
forall a. Monoid a => a
mempty
matchPat PatLit {} TypeAliases
_ = DList (VName, (t, TypeAliases))
forall a. Monoid a => a
mempty
matchPat (PatAttr AttrInfo VName
_ PatBase Info VName t
p SrcLoc
_) TypeAliases
t = PatBase Info VName t
-> TypeAliases -> DList (VName, (t, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat PatBase Info VName t
p TypeAliases
t
matchPat PatBase Info VName t
_ TypeAliases
t = [Char] -> DList (VName, (t, TypeAliases))
forall a. HasCallStack => [Char] -> a
error ([Char] -> DList (VName, (t, TypeAliases)))
-> [Char] -> DList (VName, (t, TypeAliases))
forall a b. (a -> b) -> a -> b
$ [Char]
"matchPat: pattern does not match " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> [Char]
forall a. Pretty a => a -> [Char]
prettyString TypeAliases
t

bindingPat ::
  Pat StructType ->
  TypeAliases ->
  CheckM (a, TypeAliases) ->
  CheckM (a, TypeAliases)
bindingPat :: forall a.
Pat StructType
-> TypeAliases
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingPat Pat StructType
p TypeAliases
t CheckM (a, TypeAliases)
m = do
  CheckM (Pat StructType) -> CheckM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (CheckM (Pat StructType) -> CheckM ())
-> (CheckM (Pat StructType) -> CheckM (Pat StructType))
-> CheckM (Pat StructType)
-> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckM (Pat StructType) -> CheckM (Pat StructType)
forall a. CheckM a -> CheckM a
noConsumable (CheckM (Pat StructType) -> CheckM ())
-> CheckM (Pat StructType) -> CheckM ()
forall a b. (a -> b) -> a -> b
$ (StructType -> CheckM StructType)
-> (Size -> CheckM Size)
-> Pat StructType
-> CheckM (Pat StructType)
forall (m :: * -> *) t1 t2.
Monad m =>
(t1 -> m t2)
-> (Size -> m Size)
-> PatBase Info VName t1
-> m (PatBase Info VName t2)
traversePat StructType -> CheckM StructType
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((Size, TypeAliases) -> Size)
-> CheckM (Size, TypeAliases) -> CheckM Size
forall a b. (a -> b) -> CheckM a -> CheckM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Size, TypeAliases) -> Size
forall a b. (a, b) -> a
fst (CheckM (Size, TypeAliases) -> CheckM Size)
-> (Size -> CheckM (Size, TypeAliases)) -> Size -> CheckM Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> CheckM (Size, TypeAliases)
checkExp) Pat StructType
p
  (TypeAliases -> TypeAliases)
-> (a, TypeAliases) -> (a, TypeAliases)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([VName] -> Aliases -> Aliases
unscope (Pat StructType -> [VName]
forall t. Pat t -> [VName]
patNames Pat StructType
p))) ((a, TypeAliases) -> (a, TypeAliases))
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CheckEnv -> CheckEnv)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a. (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local CheckEnv -> CheckEnv
bind CheckM (a, TypeAliases)
m
  where
    bind :: CheckEnv -> CheckEnv
bind CheckEnv
env =
      CheckEnv
env
        { envVtable =
            foldr (uncurry M.insert . f) (envVtable env) (matchPat p t)
        }
      where
        f :: (VName, (a, TypeAliases)) -> (VName, Entry TypeAliases)
f (VName
v, (a
_, TypeAliases
als)) = (VName
v, TypeAliases -> Entry TypeAliases
forall a. a -> Entry a
Consumable (TypeAliases -> Entry TypeAliases)
-> TypeAliases -> Entry TypeAliases
forall a b. (a -> b) -> a -> b
$ VName -> TypeAliases -> TypeAliases
insertSelfAliases VName
v TypeAliases
als)

bindingParam :: Pat ParamType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParam :: forall a.
Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParam = Aliases
-> Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
forall a.
Aliases
-> Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingParamAliasing Aliases
forall a. Monoid a => a
mempty

-- | Check the size expressions in a type.  A size expression may be evaluated
-- before the expression or binding it appears in, so it may consume nothing.
checkSizes :: (Bifoldable t) => t Exp a -> CheckM ()
checkSizes :: forall (t :: * -> * -> *) a. Bifoldable t => t Size a -> CheckM ()
checkSizes = CheckM () -> CheckM ()
forall a. CheckM a -> CheckM a
noConsumable (CheckM () -> CheckM ())
-> (t Size a -> CheckM ()) -> t Size a -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Size -> CheckM (Size, TypeAliases))
-> (a -> CheckM a) -> t Size a -> CheckM ()
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bifoldable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f ()
bitraverse_ Size -> CheckM (Size, TypeAliases)
checkExp a -> CheckM a
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Like 'bindingParam', but every component of the parameter also aliases the
-- given aliases.
bindingParamAliasing :: Aliases -> Pat ParamType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParamAliasing :: forall a.
Aliases
-> Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingParamAliasing Aliases
als Pat (TypeBase Size Diet)
p CheckM (a, TypeAliases)
m = do
  (TypeBase Size Diet -> CheckM ())
-> Pat (TypeBase Size Diet) -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeBase Size Diet -> CheckM ()
forall (t :: * -> * -> *) a. Bifoldable t => t Size a -> CheckM ()
checkSizes Pat (TypeBase Size Diet)
p
  (TypeAliases -> TypeAliases)
-> (a, TypeAliases) -> (a, TypeAliases)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([VName] -> Aliases -> Aliases
unscope (Pat (TypeBase Size Diet) -> [VName]
forall t. Pat t -> [VName]
patNames Pat (TypeBase Size Diet)
p))) ((a, TypeAliases) -> (a, TypeAliases))
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CheckEnv -> CheckEnv)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a. (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local CheckEnv -> CheckEnv
bind CheckM (a, TypeAliases)
m
  where
    bind :: CheckEnv -> CheckEnv
bind CheckEnv
env =
      CheckEnv
env
        { envVtable =
            foldr (uncurry M.insert . f) (envVtable env) (patternMap p)
        }
    f :: (VName, TypeBase Size Diet) -> (VName, Entry TypeAliases)
f (VName
v, TypeBase Size Diet
t)
      | TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet TypeBase Size Diet
t Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume = (VName
v, TypeAliases -> Entry TypeAliases
forall a. a -> Entry a
Consumable TypeAliases
t_als)
      | Bool
otherwise = (VName
v, TypeAliases -> Entry TypeAliases
forall a. a -> Entry a
Nonconsumable TypeAliases
t_als)
      where
        t_als :: TypeAliases
t_als = (Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> Aliases
als) (TypeAliases -> TypeAliases) -> TypeAliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ VName -> TypeBase Size Diet -> TypeAliases
forall o. VName -> TypeBase Size o -> TypeAliases
selfAliasType VName
v TypeBase Size Diet
t

bindingIdent :: Diet -> Ident StructType -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingIdent :: forall a.
Diet
-> IdentBase Info VName StructType
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingIdent Diet
d (Ident VName
v (Info StructType
t) SrcLoc
_) =
  ((a, TypeAliases) -> (a, TypeAliases))
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a b. (a -> b) -> CheckM a -> CheckM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeAliases -> TypeAliases)
-> (a, TypeAliases) -> (a, TypeAliases)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([VName] -> Aliases -> Aliases
unscope [VName
v]))) (CheckM (a, TypeAliases) -> CheckM (a, TypeAliases))
-> (CheckM (a, TypeAliases) -> CheckM (a, TypeAliases))
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CheckEnv -> CheckEnv)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a. (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local CheckEnv -> CheckEnv
bind
  where
    bind :: CheckEnv -> CheckEnv
bind CheckEnv
env = CheckEnv
env {envVtable = M.insert v t' (envVtable env)}
    d' :: a -> Entry a
d' = case Diet
d of
      Diet
Consume -> a -> Entry a
forall a. a -> Entry a
Consumable
      Diet
Observe -> a -> Entry a
forall a. a -> Entry a
Nonconsumable
    t' :: Entry TypeAliases
t' = TypeAliases -> Entry TypeAliases
forall a. a -> Entry a
d' (TypeAliases -> Entry TypeAliases)
-> TypeAliases -> Entry TypeAliases
forall a b. (a -> b) -> a -> b
$ VName -> StructType -> TypeAliases
forall o. VName -> TypeBase Size o -> TypeAliases
selfAliasType VName
v StructType
t

bindingParams :: [Pat ParamType] -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams :: forall a.
[Pat (TypeBase Size Diet)]
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams [Pat (TypeBase Size Diet)]
params CheckM (a, TypeAliases)
m =
  CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a. CheckM a -> CheckM a
noConsumable (CheckM (a, TypeAliases) -> CheckM (a, TypeAliases))
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a b. (a -> b) -> a -> b
$
    (TypeAliases -> TypeAliases)
-> (a, TypeAliases) -> (a, TypeAliases)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Aliases -> Aliases) -> TypeAliases -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([VName] -> Aliases -> Aliases
unscope ((Pat (TypeBase Size Diet) -> [VName])
-> [Pat (TypeBase Size Diet)] -> [VName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pat (TypeBase Size Diet) -> [VName]
forall t. Pat t -> [VName]
patNames [Pat (TypeBase Size Diet)]
params)))
      ((a, TypeAliases) -> (a, TypeAliases))
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat (TypeBase Size Diet)
 -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases))
-> CheckM (a, TypeAliases)
-> [Pat (TypeBase Size Diet)]
-> CheckM (a, TypeAliases)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
forall a.
Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParam CheckM (a, TypeAliases)
m [Pat (TypeBase Size Diet)]
params

-- | Bind the names of a loop form, given the aliases of the array a for-in loop
-- iterates over.  An element of that array aliases it, as indexing does.
bindingLoopForm :: Aliases -> LoopFormBase Info VName -> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingLoopForm :: forall a.
Aliases
-> LoopFormBase Info VName
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingLoopForm Aliases
_ (For IdentBase Info VName StructType
ident Size
_) CheckM (a, TypeAliases)
m = Diet
-> IdentBase Info VName StructType
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
forall a.
Diet
-> IdentBase Info VName StructType
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingIdent Diet
Observe IdentBase Info VName StructType
ident CheckM (a, TypeAliases)
m
bindingLoopForm Aliases
arr_als (ForIn Pat StructType
pat Size
_) CheckM (a, TypeAliases)
m = Aliases
-> Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
forall a.
Aliases
-> Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingParamAliasing Aliases
arr_als Pat (TypeBase Size Diet)
pat' CheckM (a, TypeAliases)
m
  where
    pat' :: Pat (TypeBase Size Diet)
pat' = (StructType -> TypeBase Size Diet)
-> Pat StructType -> Pat (TypeBase Size Diet)
forall a b.
(a -> b) -> PatBase Info VName a -> PatBase Info VName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NoMode -> Diet) -> StructType -> TypeBase Size Diet
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Diet -> NoMode -> Diet
forall a b. a -> b -> a
const Diet
Observe)) Pat StructType
pat
bindingLoopForm Aliases
_ While {} CheckM (a, TypeAliases)
m = CheckM (a, TypeAliases)
m

bindingFun :: VName -> TypeAliases -> CheckM a -> CheckM a
bindingFun :: forall a. VName -> TypeAliases -> CheckM a -> CheckM a
bindingFun VName
v TypeAliases
t = (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall a. (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((CheckEnv -> CheckEnv) -> CheckM a -> CheckM a)
-> (CheckEnv -> CheckEnv) -> CheckM a -> CheckM a
forall a b. (a -> b) -> a -> b
$ \CheckEnv
env ->
  CheckEnv
env {envVtable = M.insert v (Nonconsumable t) (envVtable env)}

-- | Is this location dead because of something in the consumed set?  That is
-- the case if a location on the same variable has been consumed whose path is
-- a prefix of this one, or of which this one is a prefix.  The result is where
-- the killing consumption happened.
deadIn :: Consumed -> Location -> Maybe Loc
deadIn :: Consumed -> Location -> Maybe Loc
deadIn Consumed
cons (VName
v, [Name]
p) = [Loc] -> Maybe Loc
forall a. [a] -> Maybe a
listToMaybe ([Loc] -> Maybe Loc) -> [Loc] -> Maybe Loc
forall a b. (a -> b) -> a -> b
$ ((Location, Loc) -> Maybe Loc) -> [(Location, Loc)] -> [Loc]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Location, Loc) -> Maybe Loc
forall {a} {a}. ((a, [Name]), a) -> Maybe a
killing ([(Location, Loc)] -> [Loc]) -> [(Location, Loc)] -> [Loc]
forall a b. (a -> b) -> a -> b
$ Consumed -> [(Location, Loc)]
forall k a. Map k a -> [(k, a)]
M.toList Consumed
on_v
  where
    on_v :: Consumed
on_v = (Location -> Bool) -> Consumed -> Consumed
forall k a. (k -> Bool) -> Map k a -> Map k a
M.takeWhileAntitone ((VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
v) (VName -> Bool) -> (Location -> VName) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> VName
forall a b. (a, b) -> a
fst) (Consumed -> Consumed) -> Consumed -> Consumed
forall a b. (a -> b) -> a -> b
$ (Location -> Bool) -> Consumed -> Consumed
forall k a. (k -> Bool) -> Map k a -> Map k a
M.dropWhileAntitone ((VName -> VName -> Bool
forall a. Ord a => a -> a -> Bool
< VName
v) (VName -> Bool) -> (Location -> VName) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Location -> VName
forall a b. (a, b) -> a
fst) Consumed
cons
    killing :: ((a, [Name]), a) -> Maybe a
killing ((a
_, [Name]
q), a
loc)
      | [Name]
q [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [Name]
p Bool -> Bool -> Bool
|| [Name]
p [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [Name]
q = a -> Maybe a
forall a. a -> Maybe a
Just a
loc
      | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing

checkIfConsumed :: Loc -> Aliases -> CheckM ()
checkIfConsumed :: Loc -> Aliases -> CheckM ()
checkIfConsumed Loc
rloc Aliases
als = do
  cons <- (CheckState -> Consumed) -> CheckM Consumed
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Consumed
stateConsumed
  names <- gets stateNames
  let bad Location
l = (Location
l,) (Loc -> (Location, Loc)) -> Maybe Loc -> Maybe (Location, Loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Consumed -> Location -> Maybe Loc
deadIn Consumed
cons Location
l
      -- Mention the variables the programmer wrote before internal names.
      internal = (VName -> Map VName NameReason -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map VName NameReason
names) (VName -> Bool)
-> (((VName, b), b) -> VName) -> ((VName, b), b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, b) -> VName
forall a b. (a, b) -> a
fst ((VName, b) -> VName)
-> (((VName, b), b) -> (VName, b)) -> ((VName, b), b) -> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VName, b), b) -> (VName, b)
forall a b. (a, b) -> a
fst
  forM_ (L.sortOn internal $ mapMaybe bad $ aliasLocs als) $ \(Location
l, Loc
wloc) -> do
    v' <- Location -> CheckM (Doc ())
forall a. Location -> CheckM (Doc a)
describeLoc Location
l
    addError rloc mempty . withIndexLink "use-after-consume" $
      "Using"
        <+> v'
        <> ", but this was consumed at"
          <+> pretty (locStrRel rloc wloc)
        <> ".  (Possibly through aliases.)"

consumed :: Consumed -> CheckM ()
consumed :: Consumed -> CheckM ()
consumed Consumed
vs = (CheckState -> CheckState) -> CheckM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckState -> CheckState) -> CheckM ())
-> (CheckState -> CheckState) -> CheckM ()
forall a b. (a -> b) -> a -> b
$ \CheckState
s -> CheckState
s {stateConsumed = stateConsumed s <> vs}

consumeAliases :: Loc -> Aliases -> CheckM ()
consumeAliases :: Loc -> Aliases -> CheckM ()
consumeAliases Loc
loc Aliases
als = do
  vtable <- (CheckEnv -> Map VName (Entry TypeAliases))
-> CheckM (Map VName (Entry TypeAliases))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Map VName (Entry TypeAliases)
envVtable
  let isBad VName
v =
        case VName
v VName -> Map VName (Entry TypeAliases) -> Maybe (Entry TypeAliases)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Entry TypeAliases)
vtable of
          Just (Nonconsumable {}) -> Bool
True
          Just Entry TypeAliases
_ -> Bool
False
          Maybe (Entry TypeAliases)
Nothing -> Bool
True
      checkIfConsumable AliasFree {} = () -> CheckM ()
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      checkIfConsumable Alias
AliasSelf =
        Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError
          Loc
loc
          Notes
forall a. Monoid a => a
mempty
          Doc ()
"Consuming a value that may have internal aliases."
      checkIfConsumable Alias
a
        | Just VName
v <- Alias -> Maybe VName
aliasVar Alias
a,
          VName -> Bool
isBad VName
v = do
            v' <- VName -> CheckM (Doc ())
forall a. VName -> CheckM (Doc a)
describeName VName
v
            addError loc mempty . withIndexLink "not-consumable" $
              "Consuming" <+> v' <> ", which is not consumable."
      checkIfConsumable Alias
_ = () -> CheckM ()
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      -- Mention local variables before globals.
      global = Bool -> (VName -> Bool) -> Maybe VName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (VName -> Map VName (Entry TypeAliases) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.notMember` Map VName (Entry TypeAliases)
vtable) (Maybe VName -> Bool) -> (Alias -> Maybe VName) -> Alias -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> Maybe VName
aliasVar
  mapM_ checkIfConsumable $ L.sortOn global $ S.toList als
  checkIfConsumed loc als
  consumed als'
  where
    als' :: Consumed
als' = [(Location, Loc)] -> Consumed
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Location, Loc)] -> Consumed) -> [(Location, Loc)] -> Consumed
forall a b. (a -> b) -> a -> b
$ (Location -> (Location, Loc)) -> [Location] -> [(Location, Loc)]
forall a b. (a -> b) -> [a] -> [b]
map (,Loc
loc) ([Location] -> [(Location, Loc)])
-> [Location] -> [(Location, Loc)]
forall a b. (a -> b) -> a -> b
$ Aliases -> [Location]
aliasLocs Aliases
als

-- | Add 'AliasSelf' to every function component of a type, recording that
-- applying it may yield a value with internal aliasing.  See Note [Parametric
-- results].
addSelfAliases :: TypeAliases -> TypeAliases
addSelfAliases :: TypeAliases -> TypeAliases
addSelfAliases (Scalar (Arrow Aliases
als PName
mn Diet
d StructType
pt RetTypeBase Size Freshness
rt)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow (Alias -> Aliases -> Aliases
forall a. Ord a => a -> Set a -> Set a
S.insert Alias
AliasSelf Aliases
als) PName
mn Diet
d StructType
pt RetTypeBase Size Freshness
rt
addSelfAliases (Scalar (Record Map Name TypeAliases
fs)) = ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (TypeAliases -> TypeAliases)
-> Map Name TypeAliases -> Map Name TypeAliases
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeAliases -> TypeAliases
addSelfAliases Map Name TypeAliases
fs
addSelfAliases (Scalar (Sum Map Name [TypeAliases]
cs)) = ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (([TypeAliases] -> [TypeAliases])
-> Map Name [TypeAliases] -> Map Name [TypeAliases]
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([TypeAliases] -> [TypeAliases])
 -> Map Name [TypeAliases] -> Map Name [TypeAliases])
-> ((TypeAliases -> TypeAliases) -> [TypeAliases] -> [TypeAliases])
-> (TypeAliases -> TypeAliases)
-> Map Name [TypeAliases]
-> Map Name [TypeAliases]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeAliases -> TypeAliases) -> [TypeAliases] -> [TypeAliases]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) TypeAliases -> TypeAliases
addSelfAliases Map Name [TypeAliases]
cs
addSelfAliases TypeAliases
t = TypeAliases
t

-- | Can a function with this type scheme produce, when its function components
-- are applied, a value whose internal aliasing we cannot see? That is so
-- exactly when some component of what it produces is a nonfresh abstract type
-- that is not one of the type parameters it is polymorphic in: it must then
-- have manufactured that value, rather than been handed it. Intrinsic types
-- (notably accumulators) are exempt, as the compiler does know their
-- representation, and they have no components that could alias each other. See
-- Note [Parametric results].
manufacturesAbstract :: BoundV -> Bool
manufacturesAbstract :: BoundV -> Bool
manufacturesAbstract (BoundV [TypeParam]
tparams StructType
vt) = (ResType -> Bool) -> ResType -> Bool
anyResultComponent ResType -> Bool
forall {dim}. TypeBase dim Freshness -> Bool
manufactured (ResType -> Bool) -> (StructType -> ResType) -> StructType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Freshness -> StructType -> ResType
forall o. Freshness -> TypeBase Size o -> ResType
toRes Freshness
Nonfresh (StructType -> Bool) -> StructType -> Bool
forall a b. (a -> b) -> a -> b
$ StructType
vt
  where
    tparams' :: [VName]
tparams' = [VName
v | TypeParamType Liftedness
_ VName
v SrcLoc
_ <- [TypeParam]
tparams]
    manufactured :: TypeBase dim Freshness -> Bool
manufactured (Scalar (TypeVar Freshness
u QualName VName
t [TypeArg dim]
_)) =
      Freshness
u Freshness -> Freshness -> Bool
forall a. Eq a => a -> a -> Bool
== Freshness
Nonfresh
        Bool -> Bool -> Bool
&& Bool -> Bool
not (VName -> Bool
isIntrinsic (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
t))
        Bool -> Bool -> Bool
&& QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
t VName -> [VName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
tparams'
    manufactured TypeBase dim Freshness
_ = Bool
False

-- | Add 'AliasSelf' to the function components of a value, recording that
-- applying them may produce a value with internal aliasing, when the given
-- declared type says they may.  See Note [Parametric results].
maybeAddSelfAliases :: BoundV -> TypeAliases -> TypeAliases
maybeAddSelfAliases :: BoundV -> TypeAliases -> TypeAliases
maybeAddSelfAliases BoundV
tscheme
  | BoundV -> Bool
manufacturesAbstract BoundV
tscheme = TypeAliases -> TypeAliases
addSelfAliases
  | Bool
otherwise = TypeAliases -> TypeAliases
forall a. a -> a
id

-- | Observe the given name here and return its aliases.
observeVar :: Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar :: Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar Loc
loc QualName VName
qv StructType
t = do
  als <-
    (CheckEnv -> TypeAliases) -> CheckM TypeAliases
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((CheckEnv -> TypeAliases) -> CheckM TypeAliases)
-> (CheckEnv -> TypeAliases) -> CheckM TypeAliases
forall a b. (a -> b) -> a -> b
$ \CheckEnv
env ->
      TypeAliases
-> (Entry TypeAliases -> TypeAliases)
-> Maybe (Entry TypeAliases)
-> TypeAliases
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CheckEnv -> TypeAliases
isGlobal CheckEnv
env) (StructType -> TypeAliases -> TypeAliases
forall u. TypeBase Size u -> TypeAliases -> TypeAliases
instantiateAliases StructType
t (TypeAliases -> TypeAliases)
-> (Entry TypeAliases -> TypeAliases)
-> Entry TypeAliases
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry TypeAliases -> TypeAliases
forall a. Entry a -> a
entryAliases) (Maybe (Entry TypeAliases) -> TypeAliases)
-> Maybe (Entry TypeAliases) -> TypeAliases
forall a b. (a -> b) -> a -> b
$
        VName -> Map VName (Entry TypeAliases) -> Maybe (Entry TypeAliases)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v (CheckEnv -> Map VName (Entry TypeAliases)
envVtable CheckEnv
env)
  checkIfConsumed loc (aliases als)
  pure als
  where
    v :: VName
v = QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
qv

    -- The declared type of a global is what makes parametricity visible; if we
    -- cannot find it, fall back to the instantiated type, which amounts to
    -- assuming no parametricity at all. An intrinsic aliases nothing. See Note
    -- [Parametric results].
    isGlobal :: CheckEnv -> TypeAliases
isGlobal CheckEnv
env
      | VName -> Bool
isIntrinsic VName
v = (NoMode -> Aliases) -> StructType -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Aliases -> NoMode -> Aliases
forall a b. a -> b -> a
const Aliases
forall a. Monoid a => a
mempty) StructType
t
      | Bool
otherwise =
          let tscheme :: BoundV
tscheme = BoundV -> Maybe BoundV -> BoundV
forall a. a -> Maybe a -> a
fromMaybe ([TypeParam] -> StructType -> BoundV
BoundV [] StructType
t) (Maybe BoundV -> BoundV) -> Maybe BoundV -> BoundV
forall a b. (a -> b) -> a -> b
$ CheckEnv -> QualName VName -> Maybe BoundV
envGlobal CheckEnv
env QualName VName
qv
           in BoundV -> TypeAliases -> TypeAliases
maybeAddSelfAliases BoundV
tscheme (TypeAliases -> TypeAliases) -> TypeAliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ VName -> BoundV -> StructType -> TypeAliases
globalAliases VName
v BoundV
tscheme StructType
t

-- Capture any newly consumed locations that occur during the provided action.
contain :: CheckM a -> CheckM (a, Consumed)
contain :: forall a. CheckM a -> CheckM (a, Consumed)
contain CheckM a
m = do
  prev_cons <- (CheckState -> Consumed) -> CheckM Consumed
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Consumed
stateConsumed
  x <- m
  new_cons <- gets $ (`M.difference` prev_cons) . stateConsumed
  modify $ \CheckState
s -> CheckState
s {stateConsumed = prev_cons}
  pure (x, new_cons)

-- | The two types are assumed to be approximately structurally equal,
-- but not necessarily regarding sizes.  Combines aliases and prefers
-- other information from first argument.
combineAliases :: TypeAliases -> TypeAliases -> TypeAliases
combineAliases :: TypeAliases -> TypeAliases -> TypeAliases
combineAliases (Array Aliases
als1 Shape Size
et1 ScalarTypeBase Size NoMode
shape1) TypeAliases
t2 =
  Aliases -> Shape Size -> ScalarTypeBase Size NoMode -> TypeAliases
forall dim o.
o -> Shape dim -> ScalarTypeBase dim NoMode -> TypeBase dim o
Array (Aliases
als1 Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> Aliases
aliases TypeAliases
t2) Shape Size
et1 ScalarTypeBase Size NoMode
shape1
combineAliases (Scalar (TypeVar Aliases
als1 QualName VName
tv1 [TypeArg Size]
targs1)) TypeAliases
t2 =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size Aliases
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar (Aliases
als1 Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> Aliases
aliases TypeAliases
t2) QualName VName
tv1 [TypeArg Size]
targs1
combineAliases (Scalar (Record Map Name TypeAliases
ts1)) (Scalar (Record Map Name TypeAliases
ts2)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (TypeAliases -> TypeAliases -> TypeAliases)
-> Map Name TypeAliases
-> Map Name TypeAliases
-> Map Name TypeAliases
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeAliases -> TypeAliases -> TypeAliases
combineAliases Map Name TypeAliases
ts1 Map Name TypeAliases
ts2
combineAliases
  (Scalar (Arrow Aliases
als1 PName
mn1 Diet
d1 StructType
pt1 (RetType [VName]
dims1 ResType
rt1)))
  (Scalar (Arrow Aliases
als2 PName
_ Diet
_ StructType
_ (RetType [VName]
_ ResType
_))) =
    ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow (Aliases
als1 Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> Aliases
als2) PName
mn1 Diet
d1 StructType
pt1 ([VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
dims1 ResType
rt1))
combineAliases (Scalar (Sum Map Name [TypeAliases]
cs1)) (Scalar (Sum Map Name [TypeAliases]
cs2)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ ([TypeAliases] -> [TypeAliases] -> [TypeAliases])
-> Map Name [TypeAliases]
-> Map Name [TypeAliases]
-> Map Name [TypeAliases]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith ((TypeAliases -> TypeAliases -> TypeAliases)
-> [TypeAliases] -> [TypeAliases] -> [TypeAliases]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TypeAliases -> TypeAliases -> TypeAliases
combineAliases) Map Name [TypeAliases]
cs1 Map Name [TypeAliases]
cs2
combineAliases (Scalar (Prim PrimType
t)) TypeAliases
_ = ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase Size Aliases
forall dim o. PrimType -> ScalarTypeBase dim o
Prim PrimType
t
combineAliases TypeAliases
t1 TypeAliases
t2 =
  [Char] -> TypeAliases
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeAliases) -> [Char] -> TypeAliases
forall a b. (a -> b) -> a -> b
$ [Char]
"combineAliases invalid args: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (TypeAliases, TypeAliases) -> [Char]
forall a. Show a => a -> [Char]
show (TypeAliases
t1, TypeAliases
t2)

-- | The locations that occur in more than one component of a value.  A
-- component aliasing any of them cannot be fresh.
sharedLocations :: TypeAliases -> S.Set Location
sharedLocations :: TypeAliases -> Set Location
sharedLocations =
  Map Location Int -> Set Location
forall k a. Map k a -> Set k
M.keysSet
    (Map Location Int -> Set Location)
-> (TypeAliases -> Map Location Int) -> TypeAliases -> Set Location
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> Map Location Int -> Map Location Int
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)
    (Map Location Int -> Map Location Int)
-> (TypeAliases -> Map Location Int)
-> TypeAliases
-> Map Location Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int) -> [(Location, Int)] -> Map Location Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+)
    ([(Location, Int)] -> Map Location Int)
-> (TypeAliases -> [(Location, Int)])
-> TypeAliases
-> Map Location Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Aliases -> [(Location, Int)]) -> [Aliases] -> [(Location, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Location -> (Location, Int)) -> [Location] -> [(Location, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (,Int
1 :: Int) ([Location] -> [(Location, Int)])
-> (Aliases -> [Location]) -> Aliases -> [(Location, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Location -> [Location]
forall a. Set a -> [a]
S.toList (Set Location -> [Location])
-> (Aliases -> Set Location) -> Aliases -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Location] -> Set Location
forall a. Ord a => [a] -> Set a
S.fromList ([Location] -> Set Location)
-> (Aliases -> [Location]) -> Aliases -> Set Location
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Location]
aliasLocs)
    ([Aliases] -> [(Location, Int)])
-> (TypeAliases -> [Aliases]) -> TypeAliases -> [(Location, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> [Aliases]
aliasParts

-- | Is this location entirely within a part of a parameter that is consumed?
consumedParamLoc :: [Pat ParamType] -> Location -> Bool
consumedParamLoc :: [Pat (TypeBase Size Diet)] -> Location -> Bool
consumedParamLoc [Pat (TypeBase Size Diet)]
params (VName
v, [Name]
fs) =
  case [([Name], TypeBase Size Diet)]
-> (TypeBase Size Diet -> [([Name], TypeBase Size Diet)])
-> Maybe (TypeBase Size Diet)
-> [([Name], TypeBase Size Diet)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((([Name], TypeBase Size Diet) -> Bool)
-> [([Name], TypeBase Size Diet)] -> [([Name], TypeBase Size Diet)]
forall a. (a -> Bool) -> [a] -> [a]
filter (([Name]
fs [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf`) ([Name] -> Bool)
-> (([Name], TypeBase Size Diet) -> [Name])
-> ([Name], TypeBase Size Diet)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeBase Size Diet) -> [Name]
forall a b. (a, b) -> a
fst) ([([Name], TypeBase Size Diet)] -> [([Name], TypeBase Size Diet)])
-> (TypeBase Size Diet -> [([Name], TypeBase Size Diet)])
-> TypeBase Size Diet
-> [([Name], TypeBase Size Diet)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase Size Diet -> [([Name], TypeBase Size Diet)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves) (Maybe (TypeBase Size Diet) -> [([Name], TypeBase Size Diet)])
-> Maybe (TypeBase Size Diet) -> [([Name], TypeBase Size Diet)]
forall a b. (a -> b) -> a -> b
$
    VName
-> [(VName, TypeBase Size Diet)] -> Maybe (TypeBase Size Diet)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v ((Pat (TypeBase Size Diet) -> [(VName, TypeBase Size Diet)])
-> [Pat (TypeBase Size Diet)] -> [(VName, TypeBase Size Diet)]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pat (TypeBase Size Diet) -> [(VName, TypeBase Size Diet)]
forall t. Pat t -> [(VName, t)]
patternMap [Pat (TypeBase Size Diet)]
params) of
    [] -> Bool
False
    [([Name], TypeBase Size Diet)]
within -> (([Name], TypeBase Size Diet) -> Bool)
-> [([Name], TypeBase Size Diet)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TypeBase Size Diet -> Bool
forall {dim}. TypeBase dim Diet -> Bool
consumable (TypeBase Size Diet -> Bool)
-> (([Name], TypeBase Size Diet) -> TypeBase Size Diet)
-> ([Name], TypeBase Size Diet)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeBase Size Diet) -> TypeBase Size Diet
forall a b. (a, b) -> b
snd) [([Name], TypeBase Size Diet)]
within
  where
    consumable :: TypeBase dim Diet -> Bool
consumable (Array Diet
d Shape dim
_ ScalarTypeBase dim NoMode
_) = Diet
d Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume
    consumable (Scalar (TypeVar Diet
d QualName VName
_ [TypeArg dim]
_)) = Diet
d Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume
    consumable (Scalar Arrow {}) = Bool
False
    consumable TypeBase dim Diet
_ = Bool
True

-- | Free variables and their aliases.
boundFreeInExp :: Exp -> CheckM (M.Map VName TypeAliases)
boundFreeInExp :: Size -> CheckM (Map VName TypeAliases)
boundFreeInExp Size
e = do
  vtable <- (CheckEnv -> Map VName (Entry TypeAliases))
-> CheckM (Map VName (Entry TypeAliases))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Map VName (Entry TypeAliases)
envVtable
  pure $
    M.mapMaybe (fmap entryAliases) . M.fromSet (`M.lookup` vtable) $
      fvVars (freeInExp e)

-- | The aliases of the free local variables captured by a closure with the given
-- parameters and body, plus any globals that its result aliases, which it may
-- return.
closureAliases :: [Pat ParamType] -> Exp -> TypeAliases -> CheckM Aliases
closureAliases :: [Pat (TypeBase Size Diet)] -> Size -> TypeAliases -> CheckM Aliases
closureAliases [Pat (TypeBase Size Diet)]
params Size
body TypeAliases
body_als = do
  vtable <- (CheckEnv -> Map VName (Entry TypeAliases))
-> CheckM (Map VName (Entry TypeAliases))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Map VName (Entry TypeAliases)
envVtable
  free_bound <-
    (`M.withoutKeys` S.fromList (foldMap patNames params)) <$> boundFreeInExp body
  -- The closure may return aliases to globals, and if the body may have
  -- internal aliasing ('AliasSelf'), so may the result of applying the closure.
  let isGlobal AliasFree {} = Bool
False
      isGlobal Alias
AliasSelf = Bool
True
      isGlobal Alias
a = Bool -> (VName -> Bool) -> Maybe VName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (VName -> Map VName (Entry TypeAliases) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.notMember` Map VName (Entry TypeAliases)
vtable) (Maybe VName -> Bool) -> Maybe VName -> Bool
forall a b. (a -> b) -> a -> b
$ Alias -> Maybe VName
aliasVar Alias
a
  pure $
    foldMap aliases (M.elems free_bound)
      <> S.filter isGlobal (aliases body_als)

-- | An in-place update through record fields consumes the component at the
-- end of that path, but its result keeps the other components, which must
-- therefore not share memory with it.
checkUpdatePath :: Loc -> [UpdateStep Info VName] -> TypeAliases -> CheckM ()
checkUpdatePath :: Loc -> [UpdateStep Info VName] -> TypeAliases -> CheckM ()
checkUpdatePath Loc
loc [UpdateStep Info VName]
steps TypeAliases
src_als =
  Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((([Name], TypeAliases) -> Aliases)
-> [([Name], TypeAliases)] -> Aliases
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> (([Name], TypeAliases) -> TypeAliases)
-> ([Name], TypeAliases)
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd) [([Name], TypeAliases)]
inside Aliases -> Aliases -> Bool
`overlaps` (([Name], TypeAliases) -> Aliases)
-> [([Name], TypeAliases)] -> Aliases
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> (([Name], TypeAliases) -> TypeAliases)
-> ([Name], TypeAliases)
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd) [([Name], TypeAliases)]
outside) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"In-place update of a component that shares memory with"
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"other components of the same value."
  where
    ([([Name], TypeAliases)]
inside, [([Name], TypeAliases)]
outside) = (([Name], TypeAliases) -> Bool)
-> [([Name], TypeAliases)]
-> ([([Name], TypeAliases)], [([Name], TypeAliases)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (([UpdateStep Info VName] -> [Name]
forall {f :: * -> *} {vn}. [UpdateStep f vn] -> [Name]
fieldPath [UpdateStep Info VName]
steps [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf`) ([Name] -> Bool)
-> (([Name], TypeAliases) -> [Name])
-> ([Name], TypeAliases)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeAliases) -> [Name]
forall a b. (a, b) -> a
fst) ([([Name], TypeAliases)]
 -> ([([Name], TypeAliases)], [([Name], TypeAliases)]))
-> [([Name], TypeAliases)]
-> ([([Name], TypeAliases)], [([Name], TypeAliases)])
forall a b. (a -> b) -> a -> b
$ TypeAliases -> [([Name], TypeAliases)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves TypeAliases
src_als
    fieldPath :: [UpdateStep f vn] -> [Name]
fieldPath (UpdateStepField Name
f : [UpdateStep f vn]
steps') = Name
f Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [UpdateStep f vn] -> [Name]
fieldPath [UpdateStep f vn]
steps'
    fieldPath [UpdateStep f vn]
_ = []

overlapCheck :: (Pretty src, Pretty ve) => Loc -> (src, TypeAliases) -> (ve, TypeAliases) -> CheckM ()
overlapCheck :: forall src ve.
(Pretty src, Pretty ve) =>
Loc -> (src, TypeAliases) -> (ve, TypeAliases) -> CheckM ()
overlapCheck Loc
loc (src
src, TypeAliases
src_als) (ve
ve, TypeAliases
ve_als) =
  Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeAliases -> Aliases
aliases TypeAliases
src_als Aliases -> Aliases -> Bool
`overlaps` TypeAliases -> Aliases
aliases TypeAliases
ve_als) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Source array for in-place update"
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (src -> Doc ()
forall ann. src -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty src
src)
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"might alias update value"
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (ve -> Doc ()
forall ann. ve -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ve
ve)
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Hint: use"
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes Doc ()
"copy"
        Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"to remove aliases from the value."

inferReturnFreshness :: [Pat ParamType] -> ResType -> TypeAliases -> ResType
inferReturnFreshness :: [Pat (TypeBase Size Diet)] -> ResType -> TypeAliases -> ResType
inferReturnFreshness [] ResType
ret TypeAliases
_ = ResType
ret ResType -> Freshness -> ResType
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` Freshness
Nonfresh
inferReturnFreshness [Pat (TypeBase Size Diet)]
params ResType
ret TypeAliases
ret_als = ResType -> TypeAliases -> ResType
forall {dim} {o1}.
TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness
delve ResType
ret TypeAliases
ret_als
  where
    shared :: Set Location
shared = TypeAliases -> Set Location
sharedLocations TypeAliases
ret_als
    delve :: TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness
delve (Scalar (Record Map Name (TypeBase dim o1)
fs1)) (Scalar (Record Map Name TypeAliases
fs2)) =
      ScalarTypeBase dim Freshness -> TypeBase dim Freshness
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase dim Freshness -> TypeBase dim Freshness)
-> ScalarTypeBase dim Freshness -> TypeBase dim Freshness
forall a b. (a -> b) -> a -> b
$ Map Name (TypeBase dim Freshness) -> ScalarTypeBase dim Freshness
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name (TypeBase dim Freshness) -> ScalarTypeBase dim Freshness)
-> Map Name (TypeBase dim Freshness)
-> ScalarTypeBase dim Freshness
forall a b. (a -> b) -> a -> b
$ (TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness)
-> Map Name (TypeBase dim o1)
-> Map Name TypeAliases
-> Map Name (TypeBase dim Freshness)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness
delve Map Name (TypeBase dim o1)
fs1 Map Name TypeAliases
fs2
    delve (Scalar (Sum Map Name [TypeBase dim o1]
cs1)) (Scalar (Sum Map Name [TypeAliases]
cs2)) =
      ScalarTypeBase dim Freshness -> TypeBase dim Freshness
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase dim Freshness -> TypeBase dim Freshness)
-> ScalarTypeBase dim Freshness -> TypeBase dim Freshness
forall a b. (a -> b) -> a -> b
$ Map Name [TypeBase dim Freshness] -> ScalarTypeBase dim Freshness
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeBase dim Freshness] -> ScalarTypeBase dim Freshness)
-> Map Name [TypeBase dim Freshness]
-> ScalarTypeBase dim Freshness
forall a b. (a -> b) -> a -> b
$ ([TypeBase dim o1] -> [TypeAliases] -> [TypeBase dim Freshness])
-> Map Name [TypeBase dim o1]
-> Map Name [TypeAliases]
-> Map Name [TypeBase dim Freshness]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith ((TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness)
-> [TypeBase dim o1] -> [TypeAliases] -> [TypeBase dim Freshness]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TypeBase dim o1 -> TypeAliases -> TypeBase dim Freshness
delve) Map Name [TypeBase dim o1]
cs1 Map Name [TypeAliases]
cs2
    delve TypeBase dim o1
t TypeAliases
t_als =
      TypeBase dim o1
t TypeBase dim o1 -> Freshness -> TypeBase dim Freshness
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` if [Unfresh] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Pat (TypeBase Size Diet)]
-> Set Location -> TypeAliases -> [Unfresh]
unfreshness [Pat (TypeBase Size Diet)]
params Set Location
shared TypeAliases
t_als) then Freshness
Fresh else Freshness
Nonfresh

checkSubExps :: (ASTMappable e) => e -> CheckM e
checkSubExps :: forall e. ASTMappable e => e -> CheckM e
checkSubExps = ASTMapper CheckM -> e -> CheckM e
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
forall (m :: * -> *). Monad m => ASTMapper m -> e -> m e
astMap ASTMapper CheckM
forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp = fmap fst . checkExp}

noAliases :: Exp -> CheckM (Exp, TypeAliases)
noAliases :: Size -> CheckM (Size, TypeAliases)
noAliases Size
e = do
  e' <- Size -> CheckM Size
forall e. ASTMappable e => e -> CheckM e
checkSubExps Size
e
  pure (e', unknownAliases (typeOf e))

-- | The aliases of each leaf of a value.
aliasParts :: TypeAliases -> [Aliases]
aliasParts :: TypeAliases -> [Aliases]
aliasParts = (([Name], TypeAliases) -> Aliases)
-> [([Name], TypeAliases)] -> [Aliases]
forall a b. (a -> b) -> [a] -> [b]
map (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> (([Name], TypeAliases) -> TypeAliases)
-> ([Name], TypeAliases)
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd) ([([Name], TypeAliases)] -> [Aliases])
-> (TypeAliases -> [([Name], TypeAliases)])
-> TypeAliases
-> [Aliases]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> [([Name], TypeAliases)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves

-- | Are the components of this value pairwise disjoint?
separated :: TypeAliases -> Bool
separated :: TypeAliases -> Bool
separated = Set Location -> Bool
forall a. Set a -> Bool
S.null (Set Location -> Bool)
-> (TypeAliases -> Set Location) -> TypeAliases -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> Set Location
sharedLocations

-- | The leaf at the given path, if there is one.
componentAt :: Path -> TypeBase dim o -> Maybe (TypeBase dim o)
componentAt :: forall dim o. [Name] -> TypeBase dim o -> Maybe (TypeBase dim o)
componentAt [Name]
fs = [Name] -> [([Name], TypeBase dim o)] -> Maybe (TypeBase dim o)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Name]
fs ([([Name], TypeBase dim o)] -> Maybe (TypeBase dim o))
-> (TypeBase dim o -> [([Name], TypeBase dim o)])
-> TypeBase dim o
-> Maybe (TypeBase dim o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim o -> [([Name], TypeBase dim o)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves

-- | The locations in the alias set of a location: those of the leaf at that
-- path of the variable's entry in the vtable.  Empty for a location that is
-- not a leaf of a variable in scope.
aliasOf :: M.Map VName (Entry TypeAliases) -> Location -> [Location]
aliasOf :: Map VName (Entry TypeAliases) -> Location -> [Location]
aliasOf Map VName (Entry TypeAliases)
vtable (VName
v, [Name]
fs) =
  [Location]
-> (TypeAliases -> [Location]) -> Maybe TypeAliases -> [Location]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Aliases -> [Location]
aliasLocs (Aliases -> [Location])
-> (TypeAliases -> Aliases) -> TypeAliases -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> Aliases
aliases) (Maybe TypeAliases -> [Location])
-> Maybe TypeAliases -> [Location]
forall a b. (a -> b) -> a -> b
$ [Name] -> TypeAliases -> Maybe TypeAliases
forall dim o. [Name] -> TypeBase dim o -> Maybe (TypeBase dim o)
componentAt [Name]
fs (TypeAliases -> Maybe TypeAliases)
-> (Entry TypeAliases -> TypeAliases)
-> Entry TypeAliases
-> Maybe TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry TypeAliases -> TypeAliases
forall a. Entry a -> a
entryAliases (Entry TypeAliases -> Maybe TypeAliases)
-> Maybe (Entry TypeAliases) -> Maybe TypeAliases
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> Map VName (Entry TypeAliases) -> Maybe (Entry TypeAliases)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName (Entry TypeAliases)
vtable

-- | The aliases of the components of a value passed for a parameter of this
-- type that the parameter treats with the given diet.
aliasesWithDiet :: Diet -> ParamType -> TypeAliases -> Aliases
aliasesWithDiet :: Diet -> TypeBase Size Diet -> TypeAliases -> Aliases
aliasesWithDiet Diet
d TypeBase Size Diet
p_t TypeAliases
t_als =
  ((([Name], TypeBase Size Diet), ([Name], TypeAliases)) -> Aliases)
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
-> Aliases
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((([Name], TypeBase Size Diet), ([Name], TypeAliases))
    -> TypeAliases)
-> (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd (([Name], TypeAliases) -> TypeAliases)
-> ((([Name], TypeBase Size Diet), ([Name], TypeAliases))
    -> ([Name], TypeAliases))
-> (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> ([Name], TypeAliases)
forall a b. (a, b) -> b
snd) ([(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
 -> Aliases)
-> ([(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
    -> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))])
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((([Name], TypeBase Size Diet), ([Name], TypeAliases)) -> Bool)
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
d) (Diet -> Bool)
-> ((([Name], TypeBase Size Diet), ([Name], TypeAliases)) -> Diet)
-> (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet (TypeBase Size Diet -> Diet)
-> ((([Name], TypeBase Size Diet), ([Name], TypeAliases))
    -> TypeBase Size Diet)
-> (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> Diet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], TypeBase Size Diet) -> TypeBase Size Diet
forall a b. (a, b) -> b
snd (([Name], TypeBase Size Diet) -> TypeBase Size Diet)
-> ((([Name], TypeBase Size Diet), ([Name], TypeAliases))
    -> ([Name], TypeBase Size Diet))
-> (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> TypeBase Size Diet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Name], TypeBase Size Diet), ([Name], TypeAliases))
-> ([Name], TypeBase Size Diet)
forall a b. (a, b) -> a
fst) ([(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
 -> Aliases)
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
-> Aliases
forall a b. (a -> b) -> a -> b
$
    [([Name], TypeBase Size Diet)]
-> [([Name], TypeAliases)]
-> [(([Name], TypeBase Size Diet), ([Name], TypeAliases))]
forall a b. [a] -> [b] -> [(a, b)]
zip (TypeBase Size Diet -> [([Name], TypeBase Size Diet)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves TypeBase Size Diet
p_t) (TypeAliases -> [([Name], TypeAliases)]
forall dim o. TypeBase dim o -> [([Name], TypeBase dim o)]
leaves TypeAliases
t_als)

-- | Check an expression passed as an argument.  This does not pass it; see
-- 'passArgs'.
checkArg :: Exp -> CheckM (Exp, TypeAliases)
checkArg :: Size -> CheckM (Size, TypeAliases)
checkArg Size
e = do
  ((e', e_als), e_cons) <- CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$ Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  consumed e_cons
  let e_t = Size -> StructType
typeOf Size
e'
  when (e_cons /= mempty && not (orderZero e_t)) $
    addError (locOf e) mempty . withIndexLink "consuming-argument" $
      "Argument of functional type"
        </> indent 2 (pretty e_t)
        </> "contains consumption, which is not allowed."
  pure (e', e_als)

-- | An alias of a new internal name standing for an intermediate value, with
-- the reason it exists recorded for error messages.
internalAlias :: Name -> NameReason -> CheckM Alias
internalAlias :: Name -> NameReason -> CheckM Alias
internalAlias Name
desc NameReason
reason = do
  v <- Name -> Int -> VName
VName Name
desc (Int -> VName) -> CheckM Int -> CheckM VName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckM Int
incCounter
  modify $ \CheckState
s -> CheckState
s {stateNames = M.insert v reason $ stateNames s}
  pure $ AliasFree (v, [])

-- | Signal an error if a component of an argument that a parameter of this type
-- consumes shares a location with another component of the argument.
noSelfAliases :: Loc -> ParamType -> TypeAliases -> CheckM ()
noSelfAliases :: Loc -> TypeBase Size Diet -> TypeAliases -> CheckM ()
noSelfAliases Loc
loc TypeBase Size Diet
p_t TypeAliases
t =
  Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Location -> Bool) -> [Location] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Location -> Set Location -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` TypeAliases -> Set Location
sharedLocations TypeAliases
t) ([Location] -> Bool) -> [Location] -> Bool
forall a b. (a -> b) -> a -> b
$ Aliases -> [Location]
aliasLocs (Aliases -> [Location]) -> Aliases -> [Location]
forall a b. (a -> b) -> a -> b
$ Diet -> TypeBase Size Diet -> TypeAliases -> Aliases
aliasesWithDiet Diet
Consume TypeBase Size Diet
p_t TypeAliases
t) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> (Doc () -> Doc ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"self-aliasing-arg" (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Argument passed for consuming parameter is self-aliased."

-- | Pass checked arguments, each with the type of its parameter, to a function
-- with the given aliases.  The call uses the function and every argument, and
-- then consumes what the parameters consume.  See Note [Locations].
passArgs :: Loc -> Aliases -> [(ParamType, (Exp, TypeAliases))] -> CheckM ()
passArgs :: Loc
-> Aliases
-> [(TypeBase Size Diet, (Size, TypeAliases))]
-> CheckM ()
passArgs Loc
loc Aliases
f_als [(TypeBase Size Diet, (Size, TypeAliases))]
args = do
  Loc -> Aliases -> CheckM ()
checkIfConsumed Loc
loc (Aliases -> CheckM ()) -> Aliases -> CheckM ()
forall a b. (a -> b) -> a -> b
$ Aliases
f_als Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> ((TypeBase Size Diet, (Size, TypeAliases)) -> Aliases)
-> [(TypeBase Size Diet, (Size, TypeAliases))] -> Aliases
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((TypeBase Size Diet, (Size, TypeAliases)) -> TypeAliases)
-> (TypeBase Size Diet, (Size, TypeAliases))
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Size, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd ((Size, TypeAliases) -> TypeAliases)
-> ((TypeBase Size Diet, (Size, TypeAliases))
    -> (Size, TypeAliases))
-> (TypeBase Size Diet, (Size, TypeAliases))
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBase Size Diet, (Size, TypeAliases)) -> (Size, TypeAliases)
forall a b. (a, b) -> b
snd) [(TypeBase Size Diet, (Size, TypeAliases))]
args
  [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
-> ((Int, (TypeBase Size Diet, (Size, TypeAliases))) -> CheckM ())
-> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Int]
-> [(TypeBase Size Diet, (Size, TypeAliases))]
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [(TypeBase Size Diet, (Size, TypeAliases))]
args) (((Int, (TypeBase Size Diet, (Size, TypeAliases))) -> CheckM ())
 -> CheckM ())
-> ((Int, (TypeBase Size Diet, (Size, TypeAliases))) -> CheckM ())
-> CheckM ()
forall a b. (a -> b) -> a -> b
$ \(Int
i, (TypeBase Size Diet
p_t, (Size
e, TypeAliases
e_als))) ->
    Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet TypeBase Size Diet
p_t Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$ do
      Loc -> TypeBase Size Diet -> TypeAliases -> CheckM ()
noSelfAliases (Size -> Loc
forall a. Located a => a -> Loc
locOf Size
e) TypeBase Size Diet
p_t TypeAliases
e_als
      let cons_als :: Aliases
cons_als = Diet -> TypeBase Size Diet -> TypeAliases -> Aliases
aliasesWithDiet Diet
Consume TypeBase Size Diet
p_t TypeAliases
e_als
          others :: [(Size, TypeAliases)]
others = ((Int, (TypeBase Size Diet, (Size, TypeAliases)))
 -> (Size, TypeAliases))
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
-> [(Size, TypeAliases)]
forall a b. (a -> b) -> [a] -> [b]
map ((TypeBase Size Diet, (Size, TypeAliases)) -> (Size, TypeAliases)
forall a b. (a, b) -> b
snd ((TypeBase Size Diet, (Size, TypeAliases)) -> (Size, TypeAliases))
-> ((Int, (TypeBase Size Diet, (Size, TypeAliases)))
    -> (TypeBase Size Diet, (Size, TypeAliases)))
-> (Int, (TypeBase Size Diet, (Size, TypeAliases)))
-> (Size, TypeAliases)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (TypeBase Size Diet, (Size, TypeAliases)))
-> (TypeBase Size Diet, (Size, TypeAliases))
forall a b. (a, b) -> b
snd) ([(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
 -> [(Size, TypeAliases)])
-> ([(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
    -> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))])
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
-> [(Size, TypeAliases)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (TypeBase Size Diet, (Size, TypeAliases))) -> Bool)
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i) (Int -> Bool)
-> ((Int, (TypeBase Size Diet, (Size, TypeAliases))) -> Int)
-> (Int, (TypeBase Size Diet, (Size, TypeAliases)))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (TypeBase Size Diet, (Size, TypeAliases))) -> Int
forall a b. (a, b) -> a
fst) ([(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
 -> [(Size, TypeAliases)])
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
-> [(Size, TypeAliases)]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [(TypeBase Size Diet, (Size, TypeAliases))]
-> [(Int, (TypeBase Size Diet, (Size, TypeAliases)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [(TypeBase Size Diet, (Size, TypeAliases))]
args
      Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Aliases
cons_als Aliases -> Aliases -> Bool
`overlaps` Aliases
f_als) (CheckM () -> CheckM ())
-> (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError (Size -> Loc
forall a. Located a => a -> Loc
locOf Size
e) Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Argument is consumed, but aliases the function being applied."
      case ((Size, TypeAliases) -> Bool)
-> [(Size, TypeAliases)] -> Maybe (Size, TypeAliases)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Aliases
cons_als Aliases -> Aliases -> Bool
`overlaps`) (Aliases -> Bool)
-> ((Size, TypeAliases) -> Aliases) -> (Size, TypeAliases) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((Size, TypeAliases) -> TypeAliases)
-> (Size, TypeAliases)
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Size, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd) [(Size, TypeAliases)]
others of
        Maybe (Size, TypeAliases)
Nothing -> () -> CheckM ()
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just (Size
other, TypeAliases
other_als) -> do
          shared <- [Location] -> CheckM (Doc ())
forall {ann}. [Location] -> CheckM (Doc ann)
describeShared ([Location] -> CheckM (Doc ())) -> [Location] -> CheckM (Doc ())
forall a b. (a -> b) -> a -> b
$ Aliases -> [Location]
aliasLocs (Aliases -> [Location]) -> Aliases -> [Location]
forall a b. (a -> b) -> a -> b
$ Aliases
cons_als Aliases -> Aliases -> Aliases
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` TypeAliases -> Aliases
aliases TypeAliases
other_als
          addError (locOf e) mempty $
            "Argument is consumed, but aliases"
              </> indent 2 shared
              </> "which is also aliased by other argument"
              </> indent 2 (pretty other)
              </> "at"
              <+> pretty (locTextRel (locOf e) (locOf other))
              <> "."
      -- Passing an argument for a consuming parameter is consumption even
      -- when the argument aliases nothing, as what the call returns may hold
      -- it (see 'checkBound').  A fresh name records that.
      passed <- Name -> NameReason -> CheckM Alias
internalAlias Name
"internal_consumed_arg" (NameReason -> CheckM Alias) -> NameReason -> CheckM Alias
forall a b. (a -> b) -> a -> b
$ Maybe (QualName VName) -> SrcLoc -> NameReason
NameAppRes Maybe (QualName VName)
forall a. Maybe a
Nothing (SrcLoc -> NameReason) -> SrcLoc -> NameReason
forall a b. (a -> b) -> a -> b
$ Size -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Size
e
      consumeAliases (locOf e) $ S.insert passed cons_als
  where
    -- Name a variable the programmer wrote if there is one.
    describeShared :: [Location] -> CheckM (Doc ann)
describeShared [Location]
locs = do
      names <- (CheckState -> Map VName NameReason)
-> CheckM (Map VName NameReason)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Map VName NameReason
stateNames
      case L.partition ((`M.notMember` names) . fst) locs of
        ((VName
v, [Name]
fs) : [Location]
_, [Location]
_) -> Doc ann -> CheckM (Doc ann)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc ann -> CheckM (Doc ann)) -> Doc ann -> CheckM (Doc ann)
forall a b. (a -> b) -> a -> b
$ VName -> [Name] -> Doc ann
forall ann. VName -> [Name] -> Doc ann
prettyAlias VName
v [Name]
fs
        ([], Location
l : [Location]
_) -> Location -> CheckM (Doc ann)
forall a. Location -> CheckM (Doc a)
describeLoc Location
l
        ([], []) -> Doc ann -> CheckM (Doc ann)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc ann
forall a. Monoid a => a
mempty

selfAliasType :: VName -> TypeBase Size o -> TypeAliases
selfAliasType :: forall o. VName -> TypeBase Size o -> TypeAliases
selfAliasType VName
v = VName -> TypeAliases -> TypeAliases
insertSelfAliases VName
v (TypeAliases -> TypeAliases)
-> (TypeBase Size o -> TypeAliases)
-> TypeBase Size o
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase Size o -> TypeAliases
forall o. TypeBase Size o -> TypeAliases
unknownAliases

-- | The aliases to assume for a value whose provenance we know nothing about:
-- none at all, except what its own type says it may manufacture. This is
-- 'maybeAddSelfAliases' with no type parameters to exploit. See Note
-- [Parametric results].
unknownAliases :: TypeBase Size o -> TypeAliases
unknownAliases :: forall o. TypeBase Size o -> TypeAliases
unknownAliases TypeBase Size o
t = BoundV -> TypeAliases -> TypeAliases
maybeAddSelfAliases ([TypeParam] -> StructType -> BoundV
BoundV [] (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ TypeBase Size o -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct TypeBase Size o
t) (TypeAliases -> TypeAliases) -> TypeAliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ (o -> Aliases) -> TypeBase Size o -> TypeAliases
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Aliases -> o -> Aliases
forall a b. a -> b -> a
const Aliases
forall a. Monoid a => a
mempty) TypeBase Size o
t

-- | @returnType appres ret_type arg_diet arg_type@ gives result of applying
-- an argument the given types to a function with the given return
-- type, consuming the argument with the given diet.
returnType :: Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType :: Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType Aliases
_ (Array Freshness
Fresh Shape Size
et ScalarTypeBase Size NoMode
shape) Diet
_ TypeAliases
_ =
  Aliases -> Shape Size -> ScalarTypeBase Size NoMode -> TypeAliases
forall dim o.
o -> Shape dim -> ScalarTypeBase dim NoMode -> TypeBase dim o
Array Aliases
forall a. Monoid a => a
mempty Shape Size
et ScalarTypeBase Size NoMode
shape
returnType Aliases
appres (Array Freshness
Nonfresh Shape Size
et ScalarTypeBase Size NoMode
shape) Diet
Consume TypeAliases
_ =
  Aliases -> Shape Size -> ScalarTypeBase Size NoMode -> TypeAliases
forall dim o.
o -> Shape dim -> ScalarTypeBase dim NoMode -> TypeBase dim o
Array Aliases
appres Shape Size
et ScalarTypeBase Size NoMode
shape
returnType Aliases
appres (Array Freshness
Nonfresh Shape Size
et ScalarTypeBase Size NoMode
shape) Diet
Observe TypeAliases
arg =
  Aliases -> Shape Size -> ScalarTypeBase Size NoMode -> TypeAliases
forall dim o.
o -> Shape dim -> ScalarTypeBase dim NoMode -> TypeBase dim o
Array (Aliases
appres Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> Aliases
aliases TypeAliases
arg) Shape Size
et ScalarTypeBase Size NoMode
shape
returnType Aliases
_ (Scalar (TypeVar Freshness
Fresh QualName VName
t [TypeArg Size]
targs)) Diet
_ TypeAliases
_ =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size Aliases
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar Aliases
forall a. Monoid a => a
mempty QualName VName
t [TypeArg Size]
targs
returnType Aliases
appres (Scalar (TypeVar Freshness
Nonfresh QualName VName
t [TypeArg Size]
targs)) Diet
Consume TypeAliases
_ =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size Aliases
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar Aliases
appres QualName VName
t [TypeArg Size]
targs
returnType Aliases
appres (Scalar (TypeVar Freshness
Nonfresh QualName VName
t [TypeArg Size]
targs)) Diet
Observe TypeAliases
arg =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size Aliases
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar (Aliases
appres Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> Aliases
aliases TypeAliases
arg) QualName VName
t [TypeArg Size]
targs
returnType Aliases
appres (Scalar (Record Map Name ResType
fs)) Diet
d TypeAliases
arg =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (ResType -> TypeAliases)
-> Map Name ResType -> Map Name TypeAliases
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ResType
et -> Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType Aliases
appres ResType
et Diet
d TypeAliases
arg) Map Name ResType
fs
returnType Aliases
_ (Scalar (Prim PrimType
t)) Diet
_ TypeAliases
_ =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase Size Aliases
forall dim o. PrimType -> ScalarTypeBase dim o
Prim PrimType
t
returnType Aliases
appres (Scalar (Arrow Freshness
_ PName
v Diet
pd StructType
t1 (RetType [VName]
dims ResType
t2))) Diet
Consume TypeAliases
_ =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow Aliases
appres PName
v Diet
pd StructType
t1 (RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases)
-> RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
dims ResType
t2
returnType Aliases
appres (Scalar (Arrow Freshness
_ PName
v Diet
pd StructType
t1 (RetType [VName]
dims ResType
t2))) Diet
Observe TypeAliases
arg =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Aliases
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size Aliases
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow (Aliases
appres Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> Aliases
aliases TypeAliases
arg) PName
v Diet
pd StructType
t1 (RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases)
-> RetTypeBase Size Freshness -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
dims ResType
t2
returnType Aliases
appres (Scalar (Sum Map Name [ResType]
cs)) Diet
d TypeAliases
arg =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> ScalarTypeBase Size Aliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$ Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall a b. (a -> b) -> a -> b
$ (([ResType] -> [TypeAliases])
-> Map Name [ResType] -> Map Name [TypeAliases]
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([ResType] -> [TypeAliases])
 -> Map Name [ResType] -> Map Name [TypeAliases])
-> ((ResType -> TypeAliases) -> [ResType] -> [TypeAliases])
-> (ResType -> TypeAliases)
-> Map Name [ResType]
-> Map Name [TypeAliases]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ResType -> TypeAliases) -> [ResType] -> [TypeAliases]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\ResType
et -> Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType Aliases
appres ResType
et Diet
d TypeAliases
arg) Map Name [ResType]
cs

-- | Check the argument that an operator section supplies for a parameter of the
-- given type.  The section is a function that captures the argument, so, just as
-- a lambda cannot consume what it captures, the parameter cannot be consuming.
checkSectionArg :: TypeAliases -> ParamType -> Exp -> CheckM (Exp, TypeAliases)
checkSectionArg :: TypeAliases
-> TypeBase Size Diet -> Size -> CheckM (Size, TypeAliases)
checkSectionArg TypeAliases
op_als TypeBase Size Diet
p_t Size
e = do
  Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet TypeBase Size Diet
p_t Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
    Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError (Size -> Loc
forall a. Located a => a -> Loc
locOf Size
e) Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
      Text -> Doc ()
forall ann. Text -> Doc ann
textwrap Text
"Operator sections may not supply an argument for a consuming parameter."
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  checkIfConsumed (locOf e) $ aliases op_als
  pure (e', e_als)

applyArg :: TypeAliases -> TypeAliases -> TypeAliases
applyArg :: TypeAliases -> TypeAliases -> TypeAliases
applyArg (Scalar (Arrow Aliases
closure_als PName
_ Diet
d StructType
_ (RetType [VName]
_ ResType
rettype))) TypeAliases
arg_als =
  Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType Aliases
closure_als ResType
rettype Diet
d TypeAliases
arg_als
applyArg TypeAliases
_ TypeAliases
arg_als = TypeAliases
arg_als

applyLoopArg :: Aliases -> ParamType -> TypeAliases -> ResType -> TypeAliases
applyLoopArg :: Aliases
-> TypeBase Size Diet -> TypeAliases -> ResType -> TypeAliases
applyLoopArg Aliases
appres (Scalar (Record Map Name (TypeBase Size Diet)
pfs)) (Scalar (Record Map Name TypeAliases
afs)) (Scalar (Record Map Name ResType
rfs)) =
  ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> (Map Name TypeAliases -> ScalarTypeBase Size Aliases)
-> Map Name TypeAliases
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name TypeAliases -> ScalarTypeBase Size Aliases
forall dim o. Map Name (TypeBase dim o) -> ScalarTypeBase dim o
Record (Map Name TypeAliases -> TypeAliases)
-> Map Name TypeAliases -> TypeAliases
forall a b. (a -> b) -> a -> b
$
    (Name -> TypeBase Size Diet -> TypeAliases)
-> Map Name (TypeBase Size Diet) -> Map Name TypeAliases
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey
      (\Name
k TypeBase Size Diet
p_t -> Aliases
-> TypeBase Size Diet -> TypeAliases -> ResType -> TypeAliases
applyLoopArg Aliases
appres TypeBase Size Diet
p_t (Map Name TypeAliases
afs Map Name TypeAliases -> Name -> TypeAliases
forall k a. Ord k => Map k a -> k -> a
M.! Name
k) (Map Name ResType
rfs Map Name ResType -> Name -> ResType
forall k a. Ord k => Map k a -> k -> a
M.! Name
k))
      Map Name (TypeBase Size Diet)
pfs
applyLoopArg Aliases
appres TypeBase Size Diet
p_t TypeAliases
arg_als ResType
rettype =
  Aliases -> ResType -> Diet -> TypeAliases -> TypeAliases
returnType Aliases
appres ResType
rettype (TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet TypeBase Size Diet
p_t) TypeAliases
arg_als

-- Loops are tricky because we want to infer the diets of their parameters.
-- This is pretty unusual: we do not do this for ordinary functions.
type Loop = (Pat ParamType, LoopInitBase Info VName, LoopFormBase Info VName, Exp)

-- | Mark bindings of consumed names as Consume, except those under a
-- 'PatAscription', which are left unchanged.
updateParamDiet :: (VName -> Bool) -> Pat ParamType -> Pat ParamType
updateParamDiet :: (VName -> Bool)
-> Pat (TypeBase Size Diet) -> Pat (TypeBase Size Diet)
updateParamDiet VName -> Bool
cons = Pat (TypeBase Size Diet) -> Pat (TypeBase Size Diet)
forall {dim}.
PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse
  where
    recurse :: PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse (Wildcard (Info TypeBase dim Diet
t) SrcLoc
wloc) =
      Info (TypeBase dim Diet)
-> SrcLoc -> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
Wildcard (TypeBase dim Diet -> Info (TypeBase dim Diet)
forall a. a -> Info a
Info (TypeBase dim Diet -> Info (TypeBase dim Diet))
-> TypeBase dim Diet -> Info (TypeBase dim Diet)
forall a b. (a -> b) -> a -> b
$ TypeBase dim Diet
t TypeBase dim Diet -> Diet -> TypeBase dim Diet
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` Diet
Observe) SrcLoc
wloc
    recurse (PatParens PatBase Info VName (TypeBase dim Diet)
p SrcLoc
ploc) =
      PatBase Info VName (TypeBase dim Diet)
-> SrcLoc -> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
PatBase f vn t -> SrcLoc -> PatBase f vn t
PatParens (PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse PatBase Info VName (TypeBase dim Diet)
p) SrcLoc
ploc
    recurse (PatAttr AttrInfo VName
attr PatBase Info VName (TypeBase dim Diet)
p SrcLoc
ploc) =
      AttrInfo VName
-> PatBase Info VName (TypeBase dim Diet)
-> SrcLoc
-> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
AttrInfo vn -> PatBase f vn t -> SrcLoc -> PatBase f vn t
PatAttr AttrInfo VName
attr (PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse PatBase Info VName (TypeBase dim Diet)
p) SrcLoc
ploc
    recurse (Id VName
name (Info TypeBase dim Diet
t) SrcLoc
iloc) =
      VName
-> Info (TypeBase dim Diet)
-> SrcLoc
-> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
Id VName
name (TypeBase dim Diet -> Info (TypeBase dim Diet)
forall a. a -> Info a
Info (TypeBase dim Diet -> Info (TypeBase dim Diet))
-> TypeBase dim Diet -> Info (TypeBase dim Diet)
forall a b. (a -> b) -> a -> b
$ TypeBase dim Diet
t TypeBase dim Diet -> Diet -> TypeBase dim Diet
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` Diet
m) SrcLoc
iloc
      where
        m :: Diet
m = if VName -> Bool
cons VName
name then Diet
Consume else Diet
Observe
    recurse (TuplePat [PatBase Info VName (TypeBase dim Diet)]
pats SrcLoc
ploc) =
      [PatBase Info VName (TypeBase dim Diet)]
-> SrcLoc -> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat ((PatBase Info VName (TypeBase dim Diet)
 -> PatBase Info VName (TypeBase dim Diet))
-> [PatBase Info VName (TypeBase dim Diet)]
-> [PatBase Info VName (TypeBase dim Diet)]
forall a b. (a -> b) -> [a] -> [b]
map PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse [PatBase Info VName (TypeBase dim Diet)]
pats) SrcLoc
ploc
    recurse (RecordPat [(L Name, PatBase Info VName (TypeBase dim Diet))]
fs SrcLoc
ploc) =
      [(L Name, PatBase Info VName (TypeBase dim Diet))]
-> SrcLoc -> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
[(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat (((L Name, PatBase Info VName (TypeBase dim Diet))
 -> (L Name, PatBase Info VName (TypeBase dim Diet)))
-> [(L Name, PatBase Info VName (TypeBase dim Diet))]
-> [(L Name, PatBase Info VName (TypeBase dim Diet))]
forall a b. (a -> b) -> [a] -> [b]
map ((PatBase Info VName (TypeBase dim Diet)
 -> PatBase Info VName (TypeBase dim Diet))
-> (L Name, PatBase Info VName (TypeBase dim Diet))
-> (L Name, PatBase Info VName (TypeBase dim Diet))
forall a b. (a -> b) -> (L Name, a) -> (L Name, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse) [(L Name, PatBase Info VName (TypeBase dim Diet))]
fs) SrcLoc
ploc
    recurse (PatAscription PatBase Info VName (TypeBase dim Diet)
p TypeExp Size VName
t SrcLoc
ploc) =
      PatBase Info VName (TypeBase dim Diet)
-> TypeExp Size VName
-> SrcLoc
-> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
PatBase f vn t
-> TypeExp (ExpBase f vn) vn -> SrcLoc -> PatBase f vn t
PatAscription PatBase Info VName (TypeBase dim Diet)
p TypeExp Size VName
t SrcLoc
ploc
    recurse p :: PatBase Info VName (TypeBase dim Diet)
p@PatLit {} = PatBase Info VName (TypeBase dim Diet)
p
    recurse (PatConstr Name
n Info (TypeBase dim Diet)
t [PatBase Info VName (TypeBase dim Diet)]
ps SrcLoc
ploc) =
      Name
-> Info (TypeBase dim Diet)
-> [PatBase Info VName (TypeBase dim Diet)]
-> SrcLoc
-> PatBase Info VName (TypeBase dim Diet)
forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n Info (TypeBase dim Diet)
t ((PatBase Info VName (TypeBase dim Diet)
 -> PatBase Info VName (TypeBase dim Diet))
-> [PatBase Info VName (TypeBase dim Diet)]
-> [PatBase Info VName (TypeBase dim Diet)]
forall a b. (a -> b) -> [a] -> [b]
map PatBase Info VName (TypeBase dim Diet)
-> PatBase Info VName (TypeBase dim Diet)
recurse [PatBase Info VName (TypeBase dim Diet)]
ps) SrcLoc
ploc

-- | Check the values a loop body returns for its consumed parameters, as the
-- arguments of a call that consumes them: each must be fresh, as the result of
-- a function with the loop parameters as its parameters would have to be.
checkLoopResult :: Loc -> Pat ParamType -> TypeAliases -> CheckM ()
checkLoopResult :: Loc -> Pat (TypeBase Size Diet) -> TypeAliases -> CheckM ()
checkLoopResult Loc
loop_loc Pat (TypeBase Size Diet)
param TypeAliases
body_als =
  DList (VName, (TypeBase Size Diet, TypeAliases))
-> ((VName, (TypeBase Size Diet, TypeAliases)) -> CheckM ())
-> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Pat (TypeBase Size Diet)
-> TypeAliases -> DList (VName, (TypeBase Size Diet, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat Pat (TypeBase Size Diet)
param TypeAliases
body_als) (((VName, (TypeBase Size Diet, TypeAliases)) -> CheckM ())
 -> CheckM ())
-> ((VName, (TypeBase Size Diet, TypeAliases)) -> CheckM ())
-> CheckM ()
forall a b. (a -> b) -> a -> b
$ \(VName
v, (TypeBase Size Diet
t, TypeAliases
als)) ->
    Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet TypeBase Size Diet
t Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume) (CheckM () -> CheckM ())
-> ([Unfresh] -> CheckM ()) -> [Unfresh] -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unfresh -> CheckM ()) -> [Unfresh] -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (VName -> Unfresh -> CheckM ()
forall {v}. IsName v => v -> Unfresh -> CheckM ()
report VName
v) ([Unfresh] -> CheckM ()) -> [Unfresh] -> CheckM ()
forall a b. (a -> b) -> a -> b
$ [Pat (TypeBase Size Diet)]
-> Set Location -> TypeAliases -> [Unfresh]
unfreshness [Pat (TypeBase Size Diet)
param] Set Location
shared TypeAliases
als
  where
    shared :: Set Location
shared = TypeAliases -> Set Location
sharedLocations TypeAliases
body_als
    what :: v -> Doc ann
what v
v = Doc ann
"Return value for consuming loop parameter" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (v -> Doc ann
forall a. v -> Doc a
forall v a. IsName v => v -> Doc a
prettyName v
v)
    report :: v -> Unfresh -> CheckM ()
report v
v (UnfreshAliases VName
w) =
      Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loop_loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> (Doc () -> Doc ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"consuming-loop-param-aliases" (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
        v -> Doc ()
forall {v} {ann}. IsName v => v -> Doc ann
what v
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"aliases" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
w) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    report v
v Unfresh
UnfreshShared =
      Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loop_loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> (Doc () -> Doc ()) -> Doc () -> CheckM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"aliases-previously-returned" (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
        v -> Doc ()
forall {v} {ann}. IsName v => v -> Doc ann
what v
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"aliases another returned value."
    report v
v Unfresh
UnfreshSelf =
      Loc -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError Loc
loop_loc Notes
forall a. Monoid a => a
mempty (Doc () -> CheckM ()) -> Doc () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
        v -> Doc ()
forall {v} {ann}. IsName v => v -> Doc ann
what v
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"may have internal aliases."

-- | Infer which loop parameters are consumed, and check what the body returns
-- for them.  A parameter is consumed if the body consumes it, or if the value
-- returned for a consumed parameter aliases it, as that value is consumed in
-- the next iteration.  See Note [Locations].
convergeLoopParam :: Loc -> Pat ParamType -> S.Set VName -> TypeAliases -> CheckM (Pat ParamType)
convergeLoopParam :: Loc
-> Pat (TypeBase Size Diet)
-> Set VName
-> TypeAliases
-> CheckM (Pat (TypeBase Size Diet))
convergeLoopParam Loc
loop_loc Pat (TypeBase Size Diet)
param Set VName
body_cons TypeAliases
body_als
  | Set VName
body_cons' Set VName -> Set VName -> Bool
forall a. Eq a => a -> a -> Bool
/= Set VName
body_cons = Loc
-> Pat (TypeBase Size Diet)
-> Set VName
-> TypeAliases
-> CheckM (Pat (TypeBase Size Diet))
convergeLoopParam Loc
loop_loc Pat (TypeBase Size Diet)
param Set VName
body_cons' TypeAliases
body_als
  | Bool
otherwise = do
      Loc -> Pat (TypeBase Size Diet) -> TypeAliases -> CheckM ()
checkLoopResult Loc
loop_loc Pat (TypeBase Size Diet)
param' TypeAliases
body_als
      Pat (TypeBase Size Diet) -> CheckM (Pat (TypeBase Size Diet))
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pat (TypeBase Size Diet)
param'
  where
    param' :: Pat (TypeBase Size Diet)
param' = (VName -> Bool)
-> Pat (TypeBase Size Diet) -> Pat (TypeBase Size Diet)
updateParamDiet (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
body_cons) Pat (TypeBase Size Diet)
param
    returned :: [(VName, (TypeBase Size Diet, TypeAliases))]
returned = DList (VName, (TypeBase Size Diet, TypeAliases))
-> [(VName, (TypeBase Size Diet, TypeAliases))]
forall a. DList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (DList (VName, (TypeBase Size Diet, TypeAliases))
 -> [(VName, (TypeBase Size Diet, TypeAliases))])
-> DList (VName, (TypeBase Size Diet, TypeAliases))
-> [(VName, (TypeBase Size Diet, TypeAliases))]
forall a b. (a -> b) -> a -> b
$ Pat (TypeBase Size Diet)
-> TypeAliases -> DList (VName, (TypeBase Size Diet, TypeAliases))
forall t. Pat t -> TypeAliases -> DList (VName, (t, TypeAliases))
matchPat Pat (TypeBase Size Diet)
param' TypeAliases
body_als
    cons_als :: Aliases
cons_als = ((VName, (TypeBase Size Diet, TypeAliases)) -> Aliases)
-> [(VName, (TypeBase Size Diet, TypeAliases))] -> Aliases
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((VName, (TypeBase Size Diet, TypeAliases)) -> TypeAliases)
-> (VName, (TypeBase Size Diet, TypeAliases))
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBase Size Diet, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd ((TypeBase Size Diet, TypeAliases) -> TypeAliases)
-> ((VName, (TypeBase Size Diet, TypeAliases))
    -> (TypeBase Size Diet, TypeAliases))
-> (VName, (TypeBase Size Diet, TypeAliases))
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, (TypeBase Size Diet, TypeAliases))
-> (TypeBase Size Diet, TypeAliases)
forall a b. (a, b) -> b
snd) ([(VName, (TypeBase Size Diet, TypeAliases))] -> Aliases)
-> [(VName, (TypeBase Size Diet, TypeAliases))] -> Aliases
forall a b. (a -> b) -> a -> b
$ ((VName, (TypeBase Size Diet, TypeAliases)) -> Bool)
-> [(VName, (TypeBase Size Diet, TypeAliases))]
-> [(VName, (TypeBase Size Diet, TypeAliases))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Diet -> Diet -> Bool
forall a. Eq a => a -> a -> Bool
== Diet
Consume) (Diet -> Bool)
-> ((VName, (TypeBase Size Diet, TypeAliases)) -> Diet)
-> (VName, (TypeBase Size Diet, TypeAliases))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase Size Diet -> Diet
forall shape. TypeBase shape Diet -> Diet
diet (TypeBase Size Diet -> Diet)
-> ((VName, (TypeBase Size Diet, TypeAliases))
    -> TypeBase Size Diet)
-> (VName, (TypeBase Size Diet, TypeAliases))
-> Diet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBase Size Diet, TypeAliases) -> TypeBase Size Diet
forall a b. (a, b) -> a
fst ((TypeBase Size Diet, TypeAliases) -> TypeBase Size Diet)
-> ((VName, (TypeBase Size Diet, TypeAliases))
    -> (TypeBase Size Diet, TypeAliases))
-> (VName, (TypeBase Size Diet, TypeAliases))
-> TypeBase Size Diet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName, (TypeBase Size Diet, TypeAliases))
-> (TypeBase Size Diet, TypeAliases)
forall a b. (a, b) -> b
snd) [(VName, (TypeBase Size Diet, TypeAliases))]
returned
    body_cons' :: Set VName
body_cons' = Set VName
body_cons Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> (VName -> Bool) -> Set VName -> Set VName
forall a. (a -> Bool) -> Set a -> Set a
S.filter (VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Pat (TypeBase Size Diet) -> [VName]
forall t. Pat t -> [VName]
patNames Pat (TypeBase Size Diet)
param) (Aliases -> Set VName
aliasVars Aliases
cons_als)

-- | Check the form of a loop with the given parameter, returning the array a
-- for-in loop iterates over.
checkLoopForm ::
  Pat ParamType ->
  LoopFormBase Info VName ->
  CheckM (LoopFormBase Info VName, Maybe (Exp, TypeAliases))
checkLoopForm :: Pat (TypeBase Size Diet)
-> LoopFormBase Info VName
-> CheckM (LoopFormBase Info VName, Maybe (Size, TypeAliases))
checkLoopForm Pat (TypeBase Size Diet)
_ (ForIn Pat StructType
pat Size
e) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  pure (ForIn pat e', Just (e', e_als))
checkLoopForm Pat (TypeBase Size Diet)
param (While Size
cond) = do
  -- A condition is evaluated repeatedly and may not consume anything.
  ((cond', _), _) <-
    CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> (CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases)
forall a. CheckM a -> CheckM a
noConsumable (CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases))
-> (CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases))
-> CheckM (Size, TypeAliases)
-> CheckM (Size, TypeAliases)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat (TypeBase Size Diet)
-> CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases)
forall a.
Pat (TypeBase Size Diet)
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParam ((TypeBase Size Diet -> TypeBase Size Diet)
-> Pat (TypeBase Size Diet) -> Pat (TypeBase Size Diet)
forall a b.
(a -> b) -> PatBase Info VName a -> PatBase Info VName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Diet -> Diet) -> TypeBase Size Diet -> TypeBase Size Diet
forall b c a. (b -> c) -> TypeBase a b -> TypeBase a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Diet -> Diet -> Diet
forall a b. a -> b -> a
const Diet
Observe)) Pat (TypeBase Size Diet)
param) (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$
      Size -> CheckM (Size, TypeAliases)
checkExp Size
cond
  pure (While cond', Nothing)
checkLoopForm Pat (TypeBase Size Diet)
_ LoopFormBase Info VName
form = (,Maybe (Size, TypeAliases)
forall a. Maybe a
Nothing) (LoopFormBase Info VName
 -> (LoopFormBase Info VName, Maybe (Size, TypeAliases)))
-> CheckM (LoopFormBase Info VName)
-> CheckM (LoopFormBase Info VName, Maybe (Size, TypeAliases))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoopFormBase Info VName -> CheckM (LoopFormBase Info VName)
forall e. ASTMappable e => e -> CheckM e
checkSubExps LoopFormBase Info VName
form

-- | A loop evaluates its initial value and then its form, and then passes the
-- initial value to the first iteration, as if calling a function that also
-- observes the array a for-in loop iterates over.  See Note [Locations].
checkLoop :: Loc -> Loop -> CheckM (Loop, TypeAliases)
checkLoop :: Loc -> Loop -> CheckM (Loop, TypeAliases)
checkLoop Loc
loop_loc (Pat (TypeBase Size Diet)
param, LoopInitBase Info VName
arg, LoopFormBase Info VName
form, Size
body) = do
  ((arg', (arg_e, arg_als)), init_cons) <- CheckM (LoopInitBase Info VName, (Size, TypeAliases))
-> CheckM
     ((LoopInitBase Info VName, (Size, TypeAliases)), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (LoopInitBase Info VName, (Size, TypeAliases))
 -> CheckM
      ((LoopInitBase Info VName, (Size, TypeAliases)), Consumed))
-> CheckM (LoopInitBase Info VName, (Size, TypeAliases))
-> CheckM
     ((LoopInitBase Info VName, (Size, TypeAliases)), Consumed)
forall a b. (a -> b) -> a -> b
$ case LoopInitBase Info VName
arg of
    LoopInitImplicit (Info Size
e) -> do
      (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkArg Size
e
      pure (LoopInitImplicit (Info e'), (e', e_als))
    LoopInitExplicit Size
e -> do
      (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkArg Size
e
      pure (LoopInitExplicit e', (e', e_als))
  consumed init_cons
  (form', iterated) <- checkLoopForm param form
  let arr_als = ((Size, TypeAliases) -> Aliases)
-> Maybe (Size, TypeAliases) -> Aliases
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((Size, TypeAliases) -> TypeAliases)
-> (Size, TypeAliases)
-> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Size, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd) Maybe (Size, TypeAliases)
iterated
  -- We pretend that every part of the loop parameter has a consuming diet, as
  -- we need to allow consumption in the body, which we then use to infer the
  -- proper diet of the parameter.
  ((body', body_cons), body_als) <-
    noConsumable
      . bindingParam (updateParamDiet (const True) param)
      . bindingLoopForm arr_als form'
      $ do
        ((body', body_als), body_cons) <- contain $ checkExp body
        pure ((body', body_cons), body_als)
  param' <- convergeLoopParam loop_loc param (S.map fst (M.keysSet body_cons)) body_als

  let param_t = Pat (TypeBase Size Diet) -> TypeBase Size Diet
forall d o. Pat (TypeBase d o) -> TypeBase d o
patternType Pat (TypeBase Size Diet)
param'
      iteratedArg (Size
e, b
e_als) = (Diet -> StructType -> TypeBase Size Diet
forall o. Diet -> TypeBase Size o -> TypeBase Size Diet
toParam Diet
Observe (Size -> StructType
typeOf Size
e), (Size
e, b
e_als))
  (_, entry_cons) <-
    contain . passArgs loop_loc mempty $
      (param_t, (arg_e, arg_als)) : maybeToList (iteratedArg <$> iterated)
  consumed entry_cons
  let arg_cons = Consumed
init_cons Consumed -> Consumed -> Consumed
forall a. Semigroup a => a -> a -> a
<> Consumed
entry_cons

  let checkFree Doc ()
what Size
e = do
        free_bound <- Size -> CheckM (Map VName TypeAliases)
boundFreeInExp Size
e

        let bad = (Location -> Bool) -> [Location] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Loc -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Loc -> Bool) -> (Location -> Maybe Loc) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Consumed -> Location -> Maybe Loc
deadIn Consumed
arg_cons) ([Location] -> Bool)
-> ((a, TypeAliases) -> [Location]) -> (a, TypeAliases) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aliases -> [Location]
aliasLocs (Aliases -> [Location])
-> ((a, TypeAliases) -> Aliases) -> (a, TypeAliases) -> [Location]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAliases -> Aliases
aliases (TypeAliases -> Aliases)
-> ((a, TypeAliases) -> TypeAliases) -> (a, TypeAliases) -> Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, TypeAliases) -> TypeAliases
forall a b. (a, b) -> b
snd
        forM_ (filter bad $ M.toList free_bound) $ \(VName
v, TypeAliases
_) -> do
          v' <- VName -> CheckM (Doc ())
forall a. VName -> CheckM (Doc a)
describeVar VName
v
          addError loop_loc mempty $
            what
              <+> "uses"
              <+> v'
              <> " (or an alias),"
                </> "but this is consumed by the initial loop argument."

  checkFree "Loop body" body

  case form of
    While Size
cond -> Doc () -> Size -> CheckM ()
checkFree Doc ()
"Loop condition" Size
cond
    LoopFormBase Info VName
_ -> () -> CheckM ()
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  loop_al <- internalAlias "internal_loop_result" $ NameLoopRes $ srclocOf loop_loc

  -- The value of an observed parameter may come from any observed part of the
  -- initial value, or of what the body returns, as the loop may move values
  -- between parameters from one iteration to the next.
  let loop_als =
        Aliases
-> TypeBase Size Diet -> TypeAliases -> ResType -> TypeAliases
applyLoopArg
          ( Alias -> Aliases -> Aliases
forall a. Ord a => a -> Set a -> Set a
S.insert Alias
loop_al (Aliases -> Aliases) -> Aliases -> Aliases
forall a b. (a -> b) -> a -> b
$
              Diet -> TypeBase Size Diet -> TypeAliases -> Aliases
aliasesWithDiet Diet
Observe TypeBase Size Diet
param_t TypeAliases
arg_als
                Aliases -> Aliases -> Aliases
forall a. Semigroup a => a -> a -> a
<> Diet -> TypeBase Size Diet -> TypeAliases -> Aliases
aliasesWithDiet Diet
Observe TypeBase Size Diet
param_t TypeAliases
body_als
          )
          TypeBase Size Diet
param_t
          TypeAliases
arg_als
          (TypeBase Size Diet -> ResType
paramToRes TypeBase Size Diet
param_t)
  pure
    ( (param', arg', form', body'),
      loop_als `combineAliases` body_als
    )

-- | The type parameters at the components of a result, if every component is
-- either primitive or a type parameter.
resultVars :: [VName] -> ResType -> Maybe [VName]
resultVars :: [VName] -> ResType -> Maybe [VName]
resultVars [VName]
tps (Scalar (Record Map Name ResType
fs)) = [[VName]] -> [VName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[VName]] -> [VName]) -> Maybe [[VName]] -> Maybe [VName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ResType -> Maybe [VName]) -> [ResType] -> Maybe [[VName]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([VName] -> ResType -> Maybe [VName]
resultVars [VName]
tps) (Map Name ResType -> [ResType]
forall k a. Map k a -> [a]
M.elems Map Name ResType
fs)
resultVars [VName]
_ (Scalar Prim {}) = [VName] -> Maybe [VName]
forall a. a -> Maybe a
Just []
resultVars [VName]
tps (Scalar (TypeVar Freshness
_ QualName VName
v []))
  | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
tps = [VName] -> Maybe [VName]
forall a. a -> Maybe a
Just [QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v]
resultVars [VName]
_ ResType
_ = Maybe [VName]
forall a. Maybe a
Nothing

-- | Does the type parameter occur at no negative position in the type, which
-- is itself at a positive position if the flag is set?  An occurrence in the
-- argument of an abstract type counts as negative, as we cannot see where it
-- ends up.
noNegative :: VName -> Bool -> TypeBase dim o -> Bool
noNegative :: forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
pos (Array o
_ Shape dim
_ ScalarTypeBase dim NoMode
et) = VName -> Bool -> TypeBase dim NoMode -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
pos (ScalarTypeBase dim NoMode -> TypeBase dim NoMode
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase dim NoMode
et)
noNegative VName
_ Bool
_ (Scalar Prim {}) = Bool
True
noNegative VName
a Bool
pos (Scalar (TypeVar o
_ QualName VName
v [TypeArg dim]
targs)) =
  (Bool
pos Bool -> Bool -> Bool
|| QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
/= VName
a) Bool -> Bool -> Bool
&& (TypeArg dim -> Bool) -> [TypeArg dim] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TypeArg dim -> Bool
forall {dim}. TypeArg dim -> Bool
argOk [TypeArg dim]
targs
  where
    argOk :: TypeArg dim -> Bool
argOk (TypeArgType TypeBase dim NoMode
t) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ VName
a VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` TypeBase dim NoMode -> Set VName
forall dim o. TypeBase dim o -> Set VName
typeVars TypeBase dim NoMode
t
    argOk TypeArgDim {} = Bool
True
noNegative VName
a Bool
pos (Scalar (Record Map Name (TypeBase dim o)
fs)) = (TypeBase dim o -> Bool) -> Map Name (TypeBase dim o) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (VName -> Bool -> TypeBase dim o -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
pos) Map Name (TypeBase dim o)
fs
noNegative VName
a Bool
pos (Scalar (Sum Map Name [TypeBase dim o]
cs)) = ([TypeBase dim o] -> Bool) -> Map Name [TypeBase dim o] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((TypeBase dim o -> Bool) -> [TypeBase dim o] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (VName -> Bool -> TypeBase dim o -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
pos)) Map Name [TypeBase dim o]
cs
noNegative VName
a Bool
pos (Scalar (Arrow o
_ PName
_ Diet
_ TypeBase dim NoMode
pt (RetType [VName]
_ TypeBase dim Freshness
rt))) =
  VName -> Bool -> TypeBase dim NoMode -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a (Bool -> Bool
not Bool
pos) TypeBase dim NoMode
pt Bool -> Bool -> Bool
&& VName -> Bool -> TypeBase dim Freshness -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
pos TypeBase dim Freshness
rt

-- | The sources of a type parameter among the parameters of a function, as
-- parameter positions and paths through records: the components that are
-- functions which observe their argument and return the type parameter.
-- 'Nothing' if the type parameter occurs at a negative position that is not a
-- source. See Note [Parametric results].
callSources :: VName -> [StructType] -> Maybe [(Int, Path)]
callSources :: VName -> [StructType] -> Maybe [(Int, [Name])]
callSources VName
a = ([[(Int, [Name])]] -> [(Int, [Name])])
-> Maybe [[(Int, [Name])]] -> Maybe [(Int, [Name])]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(Int, [Name])]] -> [(Int, [Name])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [[(Int, [Name])]] -> Maybe [(Int, [Name])])
-> ([StructType] -> Maybe [[(Int, [Name])]])
-> [StructType]
-> Maybe [(Int, [Name])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> StructType -> Maybe [(Int, [Name])])
-> [Int] -> [StructType] -> Maybe [[(Int, [Name])]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> StructType -> Maybe [(Int, [Name])]
forall {f :: * -> *} {t} {dim} {o}.
(Monad f, Alternative f) =>
t -> TypeBase dim o -> f [(t, [Name])]
onParam [Int
0 ..]
  where
    onParam :: t -> TypeBase dim o -> f [(t, [Name])]
onParam t
i = ([[Name]] -> [(t, [Name])]) -> f [[Name]] -> f [(t, [Name])]
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Name] -> (t, [Name])) -> [[Name]] -> [(t, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map (t
i,)) (f [[Name]] -> f [(t, [Name])])
-> (TypeBase dim o -> f [[Name]])
-> TypeBase dim o
-> f [(t, [Name])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> TypeBase dim o -> f [[Name]]
forall {f :: * -> *} {dim} {o}.
(Monad f, Alternative f) =>
[Name] -> TypeBase dim o -> f [[Name]]
onComponent []

    onComponent :: [Name] -> TypeBase dim o -> f [[Name]]
onComponent [Name]
p (Scalar (Record Map Name (TypeBase dim o)
fs)) =
      [[[Name]]] -> [[Name]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[Name]]] -> [[Name]]) -> f [[[Name]]] -> f [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, TypeBase dim o) -> f [[Name]])
-> [(Name, TypeBase dim o)] -> f [[[Name]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Name
k, TypeBase dim o
t) -> [Name] -> TypeBase dim o -> f [[Name]]
onComponent ([Name]
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
k]) TypeBase dim o
t) (Map Name (TypeBase dim o) -> [(Name, TypeBase dim o)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name (TypeBase dim o)
fs)
    onComponent [Name]
p (Scalar (Arrow o
_ PName
_ Diet
Observe TypeBase dim NoMode
pt (RetType [VName]
_ (Scalar (TypeVar Freshness
_ QualName VName
v [])))))
      | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
a = [[Name]
p] [[Name]] -> f () -> f [[Name]]
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (VName -> Bool -> TypeBase dim NoMode -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
True TypeBase dim NoMode
pt)
    onComponent [Name]
_ TypeBase dim o
t = [] [[Name]] -> f () -> f [[Name]]
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (VName -> Bool -> TypeBase dim o -> Bool
forall dim o. VName -> Bool -> TypeBase dim o -> Bool
noNegative VName
a Bool
False TypeBase dim o
t)

-- | The sources of the type parameters in the result of a function with this
-- declared type, if parametricity says that the result can only be made of what
-- calls of them return. This is the case when every component of the result is
-- primitive or a type parameter, each type parameter occurs once, and each has
-- a source and no other negative occurrence. See Note [Parametric results].
resultSources :: [TypeParam] -> [StructType] -> ResType -> Maybe [(Int, Path)]
resultSources :: [TypeParam] -> [StructType] -> ResType -> Maybe [(Int, [Name])]
resultSources [TypeParam]
tparams [StructType]
params ResType
res = do
  vs <- [VName] -> ResType -> Maybe [VName]
resultVars [VName
v | TypeParamType Liftedness
_ VName
v SrcLoc
_ <- [TypeParam]
tparams] ResType
res
  guard $ length (nubOrd vs) == length vs
  fmap concat . forM vs $ \VName
v -> do
    srcs <- VName -> [StructType] -> Maybe [(Int, [Name])]
callSources VName
v [StructType]
params
    guard $ not $ null srcs
    pure srcs

-- | Peel the parameters off a function type, returning their types (in order)
-- and the type of the final result. 'Nothing' for a non-function type. This is
-- 'unfoldFunType' except that it preserves the freshness of the result, which
-- is exactly what we are asking about here.
funParts :: TypeBase Size u -> Maybe ([StructType], ResType)
funParts :: forall u. TypeBase Size u -> Maybe ([StructType], ResType)
funParts (Scalar (Arrow u
_ PName
_ Diet
_ StructType
pt (RetType [VName]
_ ResType
t))) = ([StructType], ResType) -> Maybe ([StructType], ResType)
forall a. a -> Maybe a
Just (([StructType], ResType) -> Maybe ([StructType], ResType))
-> ([StructType], ResType) -> Maybe ([StructType], ResType)
forall a b. (a -> b) -> a -> b
$ [StructType] -> ResType -> ([StructType], ResType)
forall {dim}.
[TypeBase dim NoMode]
-> TypeBase dim Freshness
-> ([TypeBase dim NoMode], TypeBase dim Freshness)
go [StructType
pt] ResType
t
  where
    go :: [TypeBase dim NoMode]
-> TypeBase dim Freshness
-> ([TypeBase dim NoMode], TypeBase dim Freshness)
go [TypeBase dim NoMode]
ps (Scalar (Arrow Freshness
_ PName
_ Diet
_ TypeBase dim NoMode
pt' (RetType [VName]
_ TypeBase dim Freshness
t'))) = [TypeBase dim NoMode]
-> TypeBase dim Freshness
-> ([TypeBase dim NoMode], TypeBase dim Freshness)
go (TypeBase dim NoMode
pt' TypeBase dim NoMode
-> [TypeBase dim NoMode] -> [TypeBase dim NoMode]
forall a. a -> [a] -> [a]
: [TypeBase dim NoMode]
ps) TypeBase dim Freshness
t'
    go [TypeBase dim NoMode]
ps TypeBase dim Freshness
t' = ([TypeBase dim NoMode] -> [TypeBase dim NoMode]
forall a. [a] -> [a]
reverse [TypeBase dim NoMode]
ps, TypeBase dim Freshness
t')
funParts TypeBase Size u
_ = Maybe ([StructType], ResType)
forall a. Maybe a
Nothing

-- | Does applying this function construct its result freshly?  That is so when
-- every part of its (curried) result is fresh or primitive.  Requiring the
-- result to be order zero keeps us from claiming that a closure over the other
-- arguments aliases nothing.
constructsFresh :: TypeBase Size u -> Bool
constructsFresh :: forall u. TypeBase Size u -> Bool
constructsFresh TypeBase Size u
t
  | Just ([StructType]
_, ResType
rt) <- TypeBase Size u -> Maybe ([StructType], ResType)
forall u. TypeBase Size u -> Maybe ([StructType], ResType)
funParts TypeBase Size u
t = ResType -> Bool
forall dim o. TypeBase dim o -> Bool
orderZero ResType
rt Bool -> Bool -> Bool
&& ResType -> Bool
forall {dim}. TypeBase dim Freshness -> Bool
allFresh ResType
rt
  | Bool
otherwise = Bool
False
  where
    allFresh :: TypeBase dim Freshness -> Bool
allFresh (Scalar (Record Map Name (TypeBase dim Freshness)
fs)) = (TypeBase dim Freshness -> Bool)
-> Map Name (TypeBase dim Freshness) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TypeBase dim Freshness -> Bool
allFresh Map Name (TypeBase dim Freshness)
fs
    allFresh (Scalar (Sum Map Name [TypeBase dim Freshness]
cs)) = ([TypeBase dim Freshness] -> Bool)
-> Map Name [TypeBase dim Freshness] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((TypeBase dim Freshness -> Bool)
-> [TypeBase dim Freshness] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TypeBase dim Freshness -> Bool
allFresh) Map Name [TypeBase dim Freshness]
cs
    allFresh (Scalar Prim {}) = Bool
True
    allFresh (Scalar (TypeVar Freshness
u QualName VName
_ [TypeArg dim]
_)) = Freshness
u Freshness -> Freshness -> Bool
forall a. Eq a => a -> a -> Bool
== Freshness
Fresh
    allFresh (Array Freshness
u Shape dim
_ ScalarTypeBase dim NoMode
_) = Freshness
u Freshness -> Freshness -> Bool
forall a. Eq a => a -> a -> Bool
== Freshness
Fresh
    allFresh (Scalar Arrow {}) = Bool
False

-- | Mark as fresh the result of a function with this many parameters.
freshenResult :: Int -> TypeBase Size o -> TypeBase Size o
freshenResult :: forall o. Int -> TypeBase Size o -> TypeBase Size o
freshenResult Int
n (Scalar (Arrow o
u PName
pn Diet
d StructType
pt (RetType [VName]
ext ResType
rt))) =
  ScalarTypeBase Size o -> TypeBase Size o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size o -> TypeBase Size o)
-> (ResType -> ScalarTypeBase Size o) -> ResType -> TypeBase Size o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o
-> PName
-> Diet
-> StructType
-> RetTypeBase Size Freshness
-> ScalarTypeBase Size o
forall dim o.
o
-> PName
-> Diet
-> TypeBase dim NoMode
-> RetTypeBase dim Freshness
-> ScalarTypeBase dim o
Arrow o
u PName
pn Diet
d StructType
pt (RetTypeBase Size Freshness -> ScalarTypeBase Size o)
-> (ResType -> RetTypeBase Size Freshness)
-> ResType
-> ScalarTypeBase Size o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext (ResType -> TypeBase Size o) -> ResType -> TypeBase Size o
forall a b. (a -> b) -> a -> b
$
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then ResType
rt ResType -> Freshness -> ResType
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setMode` Freshness
Fresh else Int -> ResType -> ResType
forall o. Int -> TypeBase Size o -> TypeBase Size o
freshenResult (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ResType
rt
freshenResult Int
_ TypeBase Size o
t = TypeBase Size o
t

-- | The type of a global applied to arguments of the given types, with what
-- parametricity tells us about the freshness of the result recorded in it. Only
-- an application that supplies every parameter of the type is refined. See Note
-- [Parametric results].
parametricFreshness ::
  QualName VName ->
  StructType ->
  [StructType] ->
  CheckM StructType
parametricFreshness :: QualName VName -> StructType -> [StructType] -> CheckM StructType
parametricFreshness QualName VName
qn StructType
ftype [StructType]
argtypes = do
  globals <- (CheckEnv -> QualName VName -> Maybe BoundV)
-> CheckM (QualName VName -> Maybe BoundV)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> QualName VName -> Maybe BoundV
envGlobal
  pure $ fromMaybe ftype $ do
    BoundV tparams decl <- globals qn
    (param_ts, res) <- funParts decl
    guard $ length argtypes == length param_ts
    srcs <- resultSources tparams param_ts res
    guard $ all (maybe False constructsFresh . argAt) srcs
    Just $ freshenResult (length param_ts) ftype
  where
    argAt :: (Int, [Name]) -> Maybe StructType
argAt (Int
i, [Name]
p) = [Name] -> StructType -> Maybe StructType
forall dim o. [Name] -> TypeBase dim o -> Maybe (TypeBase dim o)
componentAt [Name]
p (StructType -> Maybe StructType) -> StructType -> Maybe StructType
forall a b. (a -> b) -> a -> b
$ [StructType]
argtypes [StructType] -> Int -> StructType
forall a. HasCallStack => [a] -> Int -> a
!! Int
i

-- | Apply a function with the given aliases to checked arguments, returning the
-- aliases of the result.
checkApply :: SrcLoc -> Maybe (QualName VName) -> TypeAliases -> [(Exp, TypeAliases)] -> CheckM TypeAliases
checkApply :: SrcLoc
-> Maybe (QualName VName)
-> TypeAliases
-> [(Size, TypeAliases)]
-> CheckM TypeAliases
checkApply SrcLoc
loc Maybe (QualName VName)
fname TypeAliases
f_als [(Size, TypeAliases)]
args = do
  Loc
-> Aliases
-> [(TypeBase Size Diet, (Size, TypeAliases))]
-> CheckM ()
passArgs (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) (TypeAliases -> Aliases
aliases TypeAliases
f_als) ([(TypeBase Size Diet, (Size, TypeAliases))] -> CheckM ())
-> [(TypeBase Size Diet, (Size, TypeAliases))] -> CheckM ()
forall a b. (a -> b) -> a -> b
$ (Diet
 -> (Size, TypeAliases)
 -> (TypeBase Size Diet, (Size, TypeAliases)))
-> [Diet]
-> [(Size, TypeAliases)]
-> [(TypeBase Size Diet, (Size, TypeAliases))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Diet
-> (Size, TypeAliases) -> (TypeBase Size Diet, (Size, TypeAliases))
forall {b}. Diet -> (Size, b) -> (TypeBase Size Diet, (Size, b))
withParam (TypeAliases -> [Diet]
forall dim o. TypeBase dim o -> [Diet]
diets TypeAliases
f_als) [(Size, TypeAliases)]
args
  app_al <- Name -> NameReason -> CheckM Alias
internalAlias Name
"internal_app_result" (NameReason -> CheckM Alias) -> NameReason -> CheckM Alias
forall a b. (a -> b) -> a -> b
$ Maybe (QualName VName) -> SrcLoc -> NameReason
NameAppRes Maybe (QualName VName)
fname SrcLoc
loc
  pure $ foldl applyArg (second (S.insert app_al) f_als) $ map snd args
  where
    withParam :: Diet -> (Size, b) -> (TypeBase Size Diet, (Size, b))
withParam Diet
d (Size
e, b
e_als) = (Diet -> StructType -> TypeBase Size Diet
forall o. Diet -> TypeBase Size o -> TypeBase Size Diet
toParam Diet
d (Size -> StructType
typeOf Size
e), (Size
e, b
e_als))

    diets :: TypeBase dim o -> [Diet]
    diets :: forall dim o. TypeBase dim o -> [Diet]
diets (Scalar (Arrow o
_ PName
_ Diet
d TypeBase dim NoMode
_ (RetType [VName]
_ TypeBase dim Freshness
rt))) = Diet
d Diet -> [Diet] -> [Diet]
forall a. a -> [a] -> [a]
: TypeBase dim Freshness -> [Diet]
forall dim o. TypeBase dim o -> [Diet]
diets TypeBase dim Freshness
rt
    diets TypeBase dim o
_ = Diet -> [Diet]
forall a. a -> [a]
repeat Diet
Observe

-- | Join the results of the branches of a branching expression (described by
-- the string), given everything consumed by any of them. An alias survives if
-- it and everything it aliases is still alive; the rest are consumed. If the
-- components of some branch's result overlap, the components of the joined
-- result are tied together by a fresh name. See Note [Locations].
joinBranches :: T.Text -> Loc -> Consumed -> NE.NonEmpty TypeAliases -> CheckM TypeAliases
joinBranches :: Text
-> Loc -> Consumed -> NonEmpty TypeAliases -> CheckM TypeAliases
joinBranches Text
what Loc
loc Consumed
all_cons NonEmpty TypeAliases
branches = do
  vtable <- (CheckEnv -> Map VName (Entry TypeAliases))
-> CheckM (Map VName (Entry TypeAliases))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckEnv -> Map VName (Entry TypeAliases)
envVtable
  let alive = Maybe Loc -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Loc -> Bool) -> (Location -> Maybe Loc) -> Location -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Consumed -> Location -> Maybe Loc
deadIn Consumed
all_cons
      keep Alias
a = case Alias -> Maybe Location
aliasLoc Alias
a of
        Maybe Location
Nothing -> Bool
True
        Just Location
l -> Location -> Bool
alive Location
l Bool -> Bool -> Bool
&& (Location -> Bool) -> [Location] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Location -> Bool
alive (Map VName (Entry TypeAliases) -> Location -> [Location]
aliasOf Map VName (Entry TypeAliases)
vtable Location
l)
      t = (TypeAliases -> TypeAliases -> TypeAliases)
-> NonEmpty TypeAliases -> TypeAliases
forall a. (a -> a -> a) -> NonEmpty a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 TypeAliases -> TypeAliases -> TypeAliases
combineAliases NonEmpty TypeAliases
branches
      dropped = (Alias -> Bool) -> Aliases -> Aliases
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Bool -> Bool
not (Bool -> Bool) -> (Alias -> Bool) -> Alias -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> Bool
keep) (Aliases -> Aliases) -> Aliases -> Aliases
forall a b. (a -> b) -> a -> b
$ TypeAliases -> Aliases
aliases TypeAliases
t
  consumed $ all_cons <> M.fromList (map (,loc) (aliasLocs dropped))
  tie <-
    if all separated branches
      then pure id
      else S.insert <$> internalAlias "internal_branch_result" (NameBranchRes what (srclocOf loc))
  pure $ second (tie . S.filter keep) t

-- | Check an expression whose value is bound to names (described by the
-- string). If that expression is a higher-order type, then it may not have
-- consumed anything. This is because we want to be able to duplicate the
-- computation for defunctionalisation purposes.
checkBound :: Doc () -> Exp -> CheckM (Exp, TypeAliases)
checkBound :: Doc () -> Size -> CheckM (Size, TypeAliases)
checkBound Doc ()
what Size
e = do
  ((e', e_als), e_cons) <- CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$ Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  consumed e_cons
  let e_t = Size -> StructType
typeOf Size
e'
  when (e_cons /= mempty && not (orderZero e_t)) $
    addError (locOf e) mempty . withIndexLink "contains-consumption" $
      what
        <+> "of higher-order type"
        </> indent 2 (pretty e_t)
        </> "contains consumption, which is not allowed."
  pure (e', e_als)

-- Note that this may modify the type annotations inside the expression, which
-- is why we return a new one.
checkExp :: Exp -> CheckM (Exp, TypeAliases)
-- First we have the complicated cases.

--
checkExp :: Size -> CheckM (Size, TypeAliases)
checkExp (AppExp (Apply Size
f NonEmpty (Info (Maybe VName), Size)
args SrcLoc
loc) Info AppRes
appres) = do
  -- Futhark evaluates the arguments of an application from right to left, and
  -- then the function.
  args' <- NonEmpty (Info (Maybe VName), (Size, TypeAliases))
-> NonEmpty (Info (Maybe VName), (Size, TypeAliases))
forall a. NonEmpty a -> NonEmpty a
NE.reverse (NonEmpty (Info (Maybe VName), (Size, TypeAliases))
 -> NonEmpty (Info (Maybe VName), (Size, TypeAliases)))
-> CheckM (NonEmpty (Info (Maybe VName), (Size, TypeAliases)))
-> CheckM (NonEmpty (Info (Maybe VName), (Size, TypeAliases)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Info (Maybe VName), Size)
 -> CheckM (Info (Maybe VName), (Size, TypeAliases)))
-> NonEmpty (Info (Maybe VName), Size)
-> CheckM (NonEmpty (Info (Maybe VName), (Size, TypeAliases)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse ((Size -> CheckM (Size, TypeAliases))
-> (Info (Maybe VName), Size)
-> CheckM (Info (Maybe VName), (Size, TypeAliases))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Info (Maybe VName), a) -> f (Info (Maybe VName), b)
traverse Size -> CheckM (Size, TypeAliases)
checkArg) (NonEmpty (Info (Maybe VName), Size)
-> NonEmpty (Info (Maybe VName), Size)
forall a. NonEmpty a -> NonEmpty a
NE.reverse NonEmpty (Info (Maybe VName), Size)
args)
  f_fresh <- case f of
    Var QualName VName
qn (Info StructType
t) SrcLoc
floc -> do
      -- It is important to use the checked arguments here, as their refined
      -- types can affect parametricFreshness.
      t' <- QualName VName -> StructType -> [StructType] -> CheckM StructType
parametricFreshness QualName VName
qn StructType
t ([StructType] -> CheckM StructType)
-> [StructType] -> CheckM StructType
forall a b. (a -> b) -> a -> b
$ ((Info (Maybe VName), (Size, TypeAliases)) -> StructType)
-> [(Info (Maybe VName), (Size, TypeAliases))] -> [StructType]
forall a b. (a -> b) -> [a] -> [b]
map (Size -> StructType
typeOf (Size -> StructType)
-> ((Info (Maybe VName), (Size, TypeAliases)) -> Size)
-> (Info (Maybe VName), (Size, TypeAliases))
-> StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Size, TypeAliases) -> Size
forall a b. (a, b) -> a
fst ((Size, TypeAliases) -> Size)
-> ((Info (Maybe VName), (Size, TypeAliases))
    -> (Size, TypeAliases))
-> (Info (Maybe VName), (Size, TypeAliases))
-> Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Info (Maybe VName), (Size, TypeAliases)) -> (Size, TypeAliases)
forall a b. (a, b) -> b
snd) ([(Info (Maybe VName), (Size, TypeAliases))] -> [StructType])
-> [(Info (Maybe VName), (Size, TypeAliases))] -> [StructType]
forall a b. (a -> b) -> a -> b
$ NonEmpty (Info (Maybe VName), (Size, TypeAliases))
-> [(Info (Maybe VName), (Size, TypeAliases))]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Info (Maybe VName), (Size, TypeAliases))
args'
      pure $ Var qn (Info t') floc
    Size
_ -> Size -> CheckM Size
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
f
  (f', f_als) <- checkExp f_fresh
  res_als <- checkApply loc (fname f) f_als $ map snd $ NE.toList args'
  pure (AppExp (Apply f' (fmap (second fst) args') loc) appres, res_als)
  where
    fname :: ExpBase f vn -> Maybe (QualName vn)
fname (Var QualName vn
v f StructType
_ SrcLoc
_) = QualName vn -> Maybe (QualName vn)
forall a. a -> Maybe a
Just QualName vn
v
    fname (AppExp (Apply ExpBase f vn
e NonEmpty (f (Maybe VName), ExpBase f vn)
_ SrcLoc
_) f AppRes
_) = ExpBase f vn -> Maybe (QualName vn)
fname ExpBase f vn
e
    fname ExpBase f vn
_ = Maybe (QualName vn)
forall a. Maybe a
Nothing

--
checkExp (AppExp (Loop [VName]
sparams Pat (TypeBase Size Diet)
pat LoopInitBase Info VName
loopinit LoopFormBase Info VName
form Size
body SrcLoc
loc) Info AppRes
appres) = do
  ((pat', loopinit', form', body'), als) <-
    Loc -> Loop -> CheckM (Loop, TypeAliases)
checkLoop (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) (Pat (TypeBase Size Diet)
pat, LoopInitBase Info VName
loopinit, LoopFormBase Info VName
form, Size
body)
  pure
    ( AppExp (Loop sparams pat' loopinit' form' body' loc) appres,
      als
    )

--
checkExp (AppExp (LetPat [SizeBinder VName]
sizes Pat StructType
p Size
e Size
body SrcLoc
loc) Info AppRes
appres) = do
  (e', e_als) <- Doc () -> Size -> CheckM (Size, TypeAliases)
checkBound Doc ()
"Let-bound expression" Size
e
  bindingPat p e_als $ do
    (body', body_als) <- checkExp body
    pure
      ( AppExp (LetPat sizes p e' body' loc) appres,
        body_als
      )

--
checkExp (AppExp (If Size
cond Size
te Size
fe SrcLoc
loc) Info AppRes
appres) = do
  (cond', _) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
cond
  ((te', te_als), te_cons) <- contain $ checkExp te
  ((fe', fe_als), fe_cons) <- contain $ checkExp fe
  comb_als <- joinBranches "if-expression" (locOf loc) (te_cons <> fe_cons) $ te_als NE.:| [fe_als]
  pure
    ( AppExp (If cond' te' fe' loc) appres,
      appResType (unInfo appres) `setAliases` mempty `combineAliases` comb_als
    )

--
checkExp (AppExp (Match Size
cond NonEmpty (CaseBase Info VName)
cs SrcLoc
loc) Info AppRes
appres) = do
  (cond', cond_als) <- Doc () -> Size -> CheckM (Size, TypeAliases)
checkBound Doc ()
"Matched expression" Size
cond
  ((cs', cs_als), cs_cons) <-
    first NE.unzip . NE.unzip <$> mapM (checkCase cond_als) cs
  comb_als <- joinBranches "match-expression" (locOf loc) (fold cs_cons) cs_als
  pure
    ( AppExp (Match cond' cs' loc) appres,
      appResType (unInfo appres) `setAliases` mempty `combineAliases` comb_als
    )
  where
    checkCase :: TypeAliases
-> CaseBase Info VName
-> CheckM ((CaseBase Info VName, TypeAliases), Consumed)
checkCase TypeAliases
cond_als (CasePat Pat StructType
p Size
body SrcLoc
caseloc) =
      CheckM (CaseBase Info VName, TypeAliases)
-> CheckM ((CaseBase Info VName, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (CaseBase Info VName, TypeAliases)
 -> CheckM ((CaseBase Info VName, TypeAliases), Consumed))
-> CheckM (CaseBase Info VName, TypeAliases)
-> CheckM ((CaseBase Info VName, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$ Pat StructType
-> TypeAliases
-> CheckM (CaseBase Info VName, TypeAliases)
-> CheckM (CaseBase Info VName, TypeAliases)
forall a.
Pat StructType
-> TypeAliases
-> CheckM (a, TypeAliases)
-> CheckM (a, TypeAliases)
bindingPat Pat StructType
p TypeAliases
cond_als (CheckM (CaseBase Info VName, TypeAliases)
 -> CheckM (CaseBase Info VName, TypeAliases))
-> CheckM (CaseBase Info VName, TypeAliases)
-> CheckM (CaseBase Info VName, TypeAliases)
forall a b. (a -> b) -> a -> b
$ do
        (body', body_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
body
        pure (CasePat p body' caseloc, body_als)

--
checkExp (AppExp (LetFun (VName, SrcLoc)
fname ([TypeParam]
typarams, [Pat (TypeBase Size Diet)]
params, Maybe (TypeExp Size VName)
retdecl, Info (RetType [VName]
ext ResType
ret), Size
funbody) Size
letbody SrcLoc
loc) Info AppRes
appres) = do
  ((ret', funbody'), ftype) <- [Pat (TypeBase Size Diet)]
-> CheckM ((ResType, Size), TypeAliases)
-> CheckM ((ResType, Size), TypeAliases)
forall a.
[Pat (TypeBase Size Diet)]
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams [Pat (TypeBase Size Diet)]
params (CheckM ((ResType, Size), TypeAliases)
 -> CheckM ((ResType, Size), TypeAliases))
-> CheckM ((ResType, Size), TypeAliases)
-> CheckM ((ResType, Size), TypeAliases)
forall a b. (a -> b) -> a -> b
$ do
    (TypeExp Size VName -> CheckM ())
-> Maybe (TypeExp Size VName) -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeExp Size VName -> CheckM ()
forall (t :: * -> * -> *) a. Bifoldable t => t Size a -> CheckM ()
checkSizes Maybe (TypeExp Size VName)
retdecl
    -- Throw away the consumption - it can refer only to the parameters anyway.
    ((funbody', funbody_als), _body_cons) <- CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$ Size -> CheckM (Size, TypeAliases)
checkExp Size
funbody
    checkReturnAlias loc params ret funbody_als
    als <- closureAliases params funbody funbody_als
    let ret' = ResType
-> (TypeExp Size VName -> ResType)
-> Maybe (TypeExp Size VName)
-> ResType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Pat (TypeBase Size Diet)] -> ResType -> TypeAliases -> ResType
inferReturnFreshness [Pat (TypeBase Size Diet)]
params ResType
ret TypeAliases
funbody_als) (ResType -> TypeExp Size VName -> ResType
forall a b. a -> b -> a
const ResType
ret) Maybe (TypeExp Size VName)
retdecl
        ftype = [Pat (TypeBase Size Diet)]
-> RetTypeBase Size Freshness -> StructType
forall d.
[Pat (TypeBase d Diet)]
-> RetTypeBase d Freshness -> TypeBase d NoMode
funType [Pat (TypeBase Size Diet)]
params ([VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext ResType
ret') StructType -> Aliases -> TypeAliases
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setAliases` Aliases
als
    pure ((ret', funbody'), ftype)
  (letbody', letbody_als) <- bindingFun (fst fname) ftype $ checkExp letbody
  pure
    ( AppExp (LetFun fname (typarams, params, retdecl, Info (RetType ext ret'), funbody') letbody' loc) appres,
      letbody_als
    )

--
checkExp (AppExp (BinOp (QualName VName
op, SrcLoc
oploc) (Info StructType
op_t) (Size
x, Info (Maybe VName)
xp) (Size
y, Info (Maybe VName)
yp) SrcLoc
loc) Info AppRes
appres) = do
  (x', x_als) <- Size -> CheckM (Size, TypeAliases)
checkArg Size
x
  (y', y_als) <- checkArg y
  op_t' <- parametricFreshness op op_t [typeOf x', typeOf y']
  op_als <- observeVar (locOf oploc) op op_t'
  res_als <- checkApply loc (Just op) op_als [(x', x_als), (y', y_als)]
  pure
    ( AppExp (BinOp (op, oploc) (Info op_t') (x', xp) (y', yp) loc) appres,
      res_als
    )

--
checkExp (Lambda [Pat (TypeBase Size Diet)]
params Size
body Maybe (TypeExp Size VName)
te (Info (RetType [VName]
ext ResType
ret)) SrcLoc
loc) =
  [Pat (TypeBase Size Diet)]
-> CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases)
forall a.
[Pat (TypeBase Size Diet)]
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams [Pat (TypeBase Size Diet)]
params (CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases))
-> CheckM (Size, TypeAliases) -> CheckM (Size, TypeAliases)
forall a b. (a -> b) -> a -> b
$ do
    (TypeExp Size VName -> CheckM ())
-> Maybe (TypeExp Size VName) -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeExp Size VName -> CheckM ()
forall (t :: * -> * -> *) a. Bifoldable t => t Size a -> CheckM ()
checkSizes Maybe (TypeExp Size VName)
te
    -- Throw away the consumption - it can refer only to the parameters
    -- anyway.
    ((body', body_als), _body_cons) <- CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a. CheckM a -> CheckM (a, Consumed)
contain (CheckM (Size, TypeAliases)
 -> CheckM ((Size, TypeAliases), Consumed))
-> CheckM (Size, TypeAliases)
-> CheckM ((Size, TypeAliases), Consumed)
forall a b. (a -> b) -> a -> b
$ Size -> CheckM (Size, TypeAliases)
checkExp Size
body
    checkReturnAlias loc params ret body_als
    als <- closureAliases params body body_als
    let ret' = ResType
-> (TypeExp Size VName -> ResType)
-> Maybe (TypeExp Size VName)
-> ResType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Pat (TypeBase Size Diet)] -> ResType -> TypeAliases -> ResType
inferReturnFreshness [Pat (TypeBase Size Diet)]
params ResType
ret TypeAliases
body_als) (ResType -> TypeExp Size VName -> ResType
forall a b. a -> b -> a
const ResType
ret) Maybe (TypeExp Size VName)
te
        ftype = [Pat (TypeBase Size Diet)]
-> RetTypeBase Size Freshness -> StructType
forall d.
[Pat (TypeBase d Diet)]
-> RetTypeBase d Freshness -> TypeBase d NoMode
funType [Pat (TypeBase Size Diet)]
params ([VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext ResType
ret') StructType -> Aliases -> TypeAliases
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setAliases` Aliases
als
    pure
      ( Lambda params body' te (Info (RetType ext ret')) loc,
        ftype
      )

--
checkExp (AppExp (LetWith IdentBase Info VName StructType
dst IdentBase Info VName StructType
src [UpdateStep Info VName]
steps Size
ve Size
body SrcLoc
loc) Info AppRes
appres) = do
  steps' <- (UpdateStep Info VName -> CheckM (UpdateStep Info VName))
-> [UpdateStep Info VName] -> CheckM [UpdateStep Info VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM UpdateStep Info VName -> CheckM (UpdateStep Info VName)
forall {f :: * -> *} {vn}.
ASTMappable (DimIndexBase f vn) =>
UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep [UpdateStep Info VName]
steps
  (ve', ve_als) <- checkExp ve
  src_als <- observeVar (locOf src) (qualName (identName src)) (unInfo $ identType src)

  let hasIndex = (UpdateStep Info VName -> Bool) -> [UpdateStep Info VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any UpdateStep Info VName -> Bool
forall {f :: * -> *} {vn}. UpdateStep f vn -> Bool
isIndex [UpdateStep Info VName]
steps

  when hasIndex $ do
    overlapCheck (locOf ve) (src, src_als) (ve', ve_als)
    checkUpdatePath (locOf loc) steps src_als
    consumeAliases (locOf loc) $ aliases src_als

  (body', body_als) <- bindingIdent Consume dst $ checkExp body
  pure (AppExp (LetWith dst src steps' ve' body' loc) appres, body_als)
  where
    isIndex :: UpdateStep f vn -> Bool
isIndex UpdateStepSlice {} = Bool
True
    isIndex UpdateStep f vn
_ = Bool
False
    checkStep :: UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep (UpdateStepSlice SliceBase f vn
slice) = SliceBase f vn -> UpdateStep f vn
forall (f :: * -> *) vn. SliceBase f vn -> UpdateStep f vn
UpdateStepSlice (SliceBase f vn -> UpdateStep f vn)
-> CheckM (SliceBase f vn) -> CheckM (UpdateStep f vn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SliceBase f vn -> CheckM (SliceBase f vn)
forall e. ASTMappable e => e -> CheckM e
checkSubExps SliceBase f vn
slice
    checkStep (UpdateStepField Name
f) = UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpdateStep f vn -> CheckM (UpdateStep f vn))
-> UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a b. (a -> b) -> a -> b
$ Name -> UpdateStep f vn
forall (f :: * -> *) vn. Name -> UpdateStep f vn
UpdateStepField Name
f
--
checkExp (Update Size
src [UpdateStep Info VName]
steps Size
ve Info StructType
t SrcLoc
loc) = do
  steps' <- (UpdateStep Info VName -> CheckM (UpdateStep Info VName))
-> [UpdateStep Info VName] -> CheckM [UpdateStep Info VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM UpdateStep Info VName -> CheckM (UpdateStep Info VName)
forall {f :: * -> *} {vn}.
ASTMappable (DimIndexBase f vn) =>
UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep [UpdateStep Info VName]
steps
  (ve', ve_als) <- checkExp ve
  (src', src_als) <- checkExp src
  checkIfConsumed (locOf loc) $ aliases ve_als
  let hasIndex = (UpdateStep Info VName -> Bool) -> [UpdateStep Info VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any UpdateStep Info VName -> Bool
forall {f :: * -> *} {vn}. UpdateStep f vn -> Bool
isIndex [UpdateStep Info VName]
steps
  res_als <-
    if hasIndex
      then do
        overlapCheck (locOf ve) (src', src_als) (ve', ve_als)
        checkUpdatePath (locOf loc) steps src_als
        consumeAliases (locOf loc) $ aliases src_als
        pure $ second (const mempty) src_als
      else pure $ updateAliases src_als steps ve_als
  pure (Update src' steps' ve' t loc, res_als)
  where
    isIndex :: UpdateStep f vn -> Bool
isIndex UpdateStepSlice {} = Bool
True
    isIndex UpdateStep f vn
_ = Bool
False
    checkStep :: UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep (UpdateStepSlice SliceBase f vn
slice) = SliceBase f vn -> UpdateStep f vn
forall (f :: * -> *) vn. SliceBase f vn -> UpdateStep f vn
UpdateStepSlice (SliceBase f vn -> UpdateStep f vn)
-> CheckM (SliceBase f vn) -> CheckM (UpdateStep f vn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SliceBase f vn -> CheckM (SliceBase f vn)
forall e. ASTMappable e => e -> CheckM e
checkSubExps SliceBase f vn
slice
    checkStep (UpdateStepField Name
f) = UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpdateStep f vn -> CheckM (UpdateStep f vn))
-> UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a b. (a -> b) -> a -> b
$ Name -> UpdateStep f vn
forall (f :: * -> *) vn. Name -> UpdateStep f vn
UpdateStepField Name
f

-- Cases that simply propagate aliases directly.
checkExp (Var QualName VName
v (Info StructType
t) SrcLoc
loc) = do
  als <- Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) QualName VName
v StructType
t
  checkIfConsumed (locOf loc) (aliases als)
  pure (Var v (Info t) loc, als)
checkExp (OpSection QualName VName
v (Info StructType
t) SrcLoc
loc) = do
  als <- Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) QualName VName
v StructType
t
  checkIfConsumed (locOf loc) (aliases als)
  pure (OpSection v (Info t) loc, als)
checkExp (OpSectionLeft QualName VName
op Info StructType
ftype Size
arg (Info (PName, TypeBase Size Diet, Maybe VName),
 Info (PName, TypeBase Size Diet))
arginfo (Info (RetTypeBase Size Freshness), Info [VName])
retinfo SrcLoc
loc) = do
  let (Info (PName
_, TypeBase Size Diet
arg_t, Maybe VName
_), Info (PName
pn, TypeBase Size Diet
pt2)) = (Info (PName, TypeBase Size Diet, Maybe VName),
 Info (PName, TypeBase Size Diet))
arginfo
      (Info RetTypeBase Size Freshness
ret, Info [VName]
_) = (Info (RetTypeBase Size Freshness), Info [VName])
retinfo
  als <- Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) QualName VName
op (Info StructType -> StructType
forall a. Info a -> a
unInfo Info StructType
ftype)
  (arg', arg_als) <- checkSectionArg als arg_t arg
  pure
    ( OpSectionLeft op ftype arg' arginfo retinfo loc,
      Scalar $ Arrow (aliases arg_als <> aliases als) pn (diet pt2) (toStruct pt2) ret
    )
checkExp (OpSectionRight QualName VName
op Info StructType
ftype Size
arg (Info (PName, TypeBase Size Diet),
 Info (PName, TypeBase Size Diet, Maybe VName))
arginfo Info (RetTypeBase Size Freshness)
retinfo SrcLoc
loc) = do
  let (Info (PName
pn, TypeBase Size Diet
pt2), Info (PName
_, TypeBase Size Diet
arg_t, Maybe VName
_)) = (Info (PName, TypeBase Size Diet),
 Info (PName, TypeBase Size Diet, Maybe VName))
arginfo
      Info RetTypeBase Size Freshness
ret = Info (RetTypeBase Size Freshness)
retinfo
  als <- Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) QualName VName
op (Info StructType -> StructType
forall a. Info a -> a
unInfo Info StructType
ftype)
  (arg', arg_als) <- checkSectionArg als arg_t arg
  pure
    ( OpSectionRight op ftype arg' arginfo retinfo loc,
      Scalar $ Arrow (aliases arg_als <> aliases als) pn (diet pt2) (toStruct pt2) ret
    )
checkExp (UpdateSection [UpdateStep Info VName]
steps Info StructType
t SrcLoc
loc) = do
  steps' <- (UpdateStep Info VName -> CheckM (UpdateStep Info VName))
-> [UpdateStep Info VName] -> CheckM [UpdateStep Info VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM UpdateStep Info VName -> CheckM (UpdateStep Info VName)
forall {f :: * -> *} {vn}.
ASTMappable (DimIndexBase f vn) =>
UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep [UpdateStep Info VName]
steps
  pure (UpdateSection steps' t loc, unknownAliases (unInfo t))
  where
    checkStep :: UpdateStep f vn -> CheckM (UpdateStep f vn)
checkStep (UpdateStepField Name
f) = UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UpdateStep f vn -> CheckM (UpdateStep f vn))
-> UpdateStep f vn -> CheckM (UpdateStep f vn)
forall a b. (a -> b) -> a -> b
$ Name -> UpdateStep f vn
forall (f :: * -> *) vn. Name -> UpdateStep f vn
UpdateStepField Name
f
    checkStep (UpdateStepSlice SliceBase f vn
slice) = SliceBase f vn -> UpdateStep f vn
forall (f :: * -> *) vn. SliceBase f vn -> UpdateStep f vn
UpdateStepSlice (SliceBase f vn -> UpdateStep f vn)
-> CheckM (SliceBase f vn) -> CheckM (UpdateStep f vn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SliceBase f vn -> CheckM (SliceBase f vn)
forall e. ASTMappable e => e -> CheckM e
checkSubExps SliceBase f vn
slice
checkExp (Coerce Size
e TypeExp Size VName
te Info StructType
t SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  checkSizes te
  pure (Coerce e' te t loc, e_als)
checkExp (Ascript Size
e TypeExp Size VName
te SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  checkSizes te
  pure (Ascript e' te loc, e_als)
checkExp (AppExp (Index Size
v SliceBase Info VName
slice SrcLoc
loc) Info AppRes
appres) = do
  (v', v_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
v
  slice' <- checkSubExps slice
  checkIfConsumed (locOf loc) $ aliases v_als
  pure
    ( AppExp (Index v' slice' loc) appres,
      appResType (unInfo appres) `setAliases` aliases v_als
    )
checkExp (Assert Size
e1 Size
e2 Info Text
t SrcLoc
loc) = do
  (e1', _) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e1
  (e2', e2_als) <- checkExp e2
  pure (Assert e1' e2' t loc, e2_als)
checkExp (Parens Size
e SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  pure (Parens e' loc, e_als)
checkExp (QualParens (QualName VName, SrcLoc)
v Size
e SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  pure (QualParens v e' loc, e_als)
checkExp (Attr AttrInfo VName
attr Size
e SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  pure (Attr attr e' loc, e_als)
checkExp (Project Name
name Size
e Info StructType
t SrcLoc
loc) = do
  (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
  pure
    ( Project name e' t loc,
      case e_als of
        Scalar (Record Map Name TypeAliases
fs)
          | Just TypeAliases
name_als <- Name -> Map Name TypeAliases -> Maybe TypeAliases
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
name Map Name TypeAliases
fs -> TypeAliases
name_als
        TypeAliases
_ -> [Char] -> TypeAliases
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeAliases) -> [Char] -> TypeAliases
forall a b. (a -> b) -> a -> b
$ [Char]
"checkExp Project: bad type " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypeAliases -> [Char]
forall a. Pretty a => a -> [Char]
prettyString TypeAliases
e_als
    )
checkExp (TupLit [Size]
es SrcLoc
loc) = do
  (es', es_als) <- (Size -> CheckM (Size, TypeAliases))
-> [Size] -> CheckM ([Size], [TypeAliases])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Size -> CheckM (Size, TypeAliases)
checkExp [Size]
es
  checkIfConsumed (locOf loc) $ foldMap aliases es_als
  pure (TupLit es' loc, Scalar $ tupleRecord es_als)
checkExp (Constr Name
name [Size]
es Info StructType
t SrcLoc
loc) = do
  (es', es_als) <- (Size -> CheckM (Size, TypeAliases))
-> [Size] -> CheckM ([Size], [TypeAliases])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Size -> CheckM (Size, TypeAliases)
checkExp [Size]
es
  checkIfConsumed (locOf loc) $ foldMap aliases es_als
  pure
    ( Constr name es' t loc,
      case unInfo t of
        Scalar (Sum Map Name [StructType]
cs) ->
          ScalarTypeBase Size Aliases -> TypeAliases
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (ScalarTypeBase Size Aliases -> TypeAliases)
-> (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> Map Name [TypeAliases]
-> TypeAliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name [TypeAliases] -> ScalarTypeBase Size Aliases
forall dim o. Map Name [TypeBase dim o] -> ScalarTypeBase dim o
Sum (Map Name [TypeAliases] -> ScalarTypeBase Size Aliases)
-> (Map Name [TypeAliases] -> Map Name [TypeAliases])
-> Map Name [TypeAliases]
-> ScalarTypeBase Size Aliases
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> [TypeAliases]
-> Map Name [TypeAliases]
-> Map Name [TypeAliases]
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
name [TypeAliases]
es_als (Map Name [TypeAliases] -> TypeAliases)
-> Map Name [TypeAliases] -> TypeAliases
forall a b. (a -> b) -> a -> b
$
            ([StructType] -> [TypeAliases])
-> Map Name [StructType] -> Map Name [TypeAliases]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((StructType -> TypeAliases) -> [StructType] -> [TypeAliases]
forall a b. (a -> b) -> [a] -> [b]
map (StructType -> Aliases -> TypeAliases
forall dim o1 o2. TypeBase dim o1 -> o2 -> TypeBase dim o2
`setAliases` Aliases
forall a. Monoid a => a
mempty)) Map Name [StructType]
cs
        StructType
t' -> [Char] -> TypeAliases
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeAliases) -> [Char] -> TypeAliases
forall a b. (a -> b) -> a -> b
$ [Char]
"checkExp Constr: bad type " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> StructType -> [Char]
forall a. Pretty a => a -> [Char]
prettyString StructType
t'
    )
checkExp (RecordLit [FieldBase Info VName]
fs SrcLoc
loc) = do
  (fs', fs_als) <- (FieldBase Info VName
 -> CheckM (FieldBase Info VName, (Name, TypeAliases)))
-> [FieldBase Info VName]
-> CheckM ([FieldBase Info VName], [(Name, TypeAliases)])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM FieldBase Info VName
-> CheckM (FieldBase Info VName, (Name, TypeAliases))
checkField [FieldBase Info VName]
fs
  checkIfConsumed (locOf loc) $ foldMap (aliases . snd) fs_als
  pure (RecordLit fs' loc, Scalar $ Record $ M.fromList fs_als)
  where
    checkField :: FieldBase Info VName
-> CheckM (FieldBase Info VName, (Name, TypeAliases))
checkField (RecordFieldExplicit L Name
name Size
e SrcLoc
floc) = do
      (e', e_als) <- Size -> CheckM (Size, TypeAliases)
checkExp Size
e
      pure (RecordFieldExplicit name e' floc, (unLoc name, e_als))
    checkField (RecordFieldImplicit L VName
name Info StructType
t SrcLoc
floc) = do
      name_als <- Loc -> QualName VName -> StructType -> CheckM TypeAliases
observeVar (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
floc) (VName -> QualName VName
forall v. v -> QualName v
qualName (L VName -> VName
forall a. L a -> a
unLoc L VName
name)) (StructType -> CheckM TypeAliases)
-> StructType -> CheckM TypeAliases
forall a b. (a -> b) -> a -> b
$ Info StructType -> StructType
forall a. Info a -> a
unInfo Info StructType
t
      pure (RecordFieldImplicit name t floc, (baseName (unLoc name), name_als))

-- Cases that create alias-free values.
checkExp e :: Size
e@(AppExp Range {} Info AppRes
_) = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@IntLit {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@FloatLit {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@Literal {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@StringLit {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@ArrayVal {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp (ArrayLit [Size]
es Info StructType
t SrcLoc
loc) = do
  (es', es_als) <- (Size -> CheckM (Size, TypeAliases))
-> [Size] -> CheckM ([Size], [TypeAliases])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Size -> CheckM (Size, TypeAliases)
checkExp [Size]
es
  checkIfConsumed (locOf loc) $ foldMap aliases es_als
  pure (ArrayLit es' t loc, unknownAliases (unInfo t))
checkExp e :: Size
e@Negate {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@Not {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e
checkExp e :: Size
e@Hole {} = Size -> CheckM (Size, TypeAliases)
noAliases Size
e

-- | Type-check a value definition.  This also infers a new return
-- type that may be fresher than previously.
checkValDef ::
  -- | The type scheme of any global, along with the type parameters it is
  -- polymorphic in.  See Note [Parametric results].
  (QualName VName -> Maybe BoundV) ->
  (VName, [TypeParam], [Pat ParamType], Exp, ResRetType, Maybe (TypeExp Exp VName), SrcLoc) ->
  ((Exp, ResRetType), [TypeError])
checkValDef :: (QualName VName -> Maybe BoundV)
-> (VName, [TypeParam], [Pat (TypeBase Size Diet)], Size,
    RetTypeBase Size Freshness, Maybe (TypeExp Size VName), SrcLoc)
-> ((Size, RetTypeBase Size Freshness), [TypeError])
checkValDef QualName VName -> Maybe BoundV
globals (VName
fname, [TypeParam]
tparams, [Pat (TypeBase Size Diet)]
params, Size
body, RetType [VName]
ext ResType
ret, Maybe (TypeExp Size VName)
retdecl, SrcLoc
loc) = (QualName VName -> Maybe BoundV)
-> Loc
-> CheckM (Size, RetTypeBase Size Freshness)
-> ((Size, RetTypeBase Size Freshness), [TypeError])
forall a.
(QualName VName -> Maybe BoundV)
-> Loc -> CheckM a -> (a, [TypeError])
runCheckM QualName VName -> Maybe BoundV
globals' (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc) (CheckM (Size, RetTypeBase Size Freshness)
 -> ((Size, RetTypeBase Size Freshness), [TypeError]))
-> CheckM (Size, RetTypeBase Size Freshness)
-> ((Size, RetTypeBase Size Freshness), [TypeError])
forall a b. (a -> b) -> a -> b
$ do
  (((Size, RetTypeBase Size Freshness), TypeAliases)
 -> (Size, RetTypeBase Size Freshness))
-> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
-> CheckM (Size, RetTypeBase Size Freshness)
forall a b. (a -> b) -> CheckM a -> CheckM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Size, RetTypeBase Size Freshness), TypeAliases)
-> (Size, RetTypeBase Size Freshness)
forall a b. (a, b) -> a
fst (CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
 -> CheckM (Size, RetTypeBase Size Freshness))
-> (CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
    -> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases))
-> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
-> CheckM (Size, RetTypeBase Size Freshness)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pat (TypeBase Size Diet)]
-> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
-> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
forall a.
[Pat (TypeBase Size Diet)]
-> CheckM (a, TypeAliases) -> CheckM (a, TypeAliases)
bindingParams [Pat (TypeBase Size Diet)]
params (CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
 -> CheckM (Size, RetTypeBase Size Freshness))
-> CheckM ((Size, RetTypeBase Size Freshness), TypeAliases)
-> CheckM (Size, RetTypeBase Size Freshness)
forall a b. (a -> b) -> a -> b
$ do
    (TypeExp Size VName -> CheckM ())
-> Maybe (TypeExp Size VName) -> CheckM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeExp Size VName -> CheckM ()
forall (t :: * -> * -> *) a. Bifoldable t => t Size a -> CheckM ()
checkSizes Maybe (TypeExp Size VName)
retdecl
    -- A top-level constant is a name like any other.
    (body', body_als) <-
      if [Pat (TypeBase Size Diet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pat (TypeBase Size Diet)]
params then Doc () -> Size -> CheckM (Size, TypeAliases)
checkBound Doc ()
"Top-level constant" Size
body else Size -> CheckM (Size, TypeAliases)
checkExp Size
body
    checkReturnAlias loc params ret body_als
    -- If the user did not provide an annotation (meaning the return type is
    -- fully inferred), we infer the freshness. Otherwise, we go with whatever
    -- they wanted. This lets the user define nonfresh return types even if the
    -- body actually has no aliases.
    ret' <- case retdecl of
      Just TypeExp Size VName
retdecl' -> do
        Bool -> CheckM () -> CheckM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Pat (TypeBase Size Diet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pat (TypeBase Size Diet)]
params Bool -> Bool -> Bool
&& ResType -> Bool
forall {dim}. TypeBase dim Freshness -> Bool
fresh ResType
ret) (CheckM () -> CheckM ()) -> CheckM () -> CheckM ()
forall a b. (a -> b) -> a -> b
$
          TypeExp Size VName -> Notes -> Doc () -> CheckM ()
forall loc. Located loc => loc -> Notes -> Doc () -> CheckM ()
addError TypeExp Size VName
retdecl' Notes
forall a. Monoid a => a
mempty Doc ()
"A top-level constant cannot be declared fresh."
        RetTypeBase Size Freshness -> CheckM (RetTypeBase Size Freshness)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase Size Freshness -> CheckM (RetTypeBase Size Freshness))
-> RetTypeBase Size Freshness
-> CheckM (RetTypeBase Size Freshness)
forall a b. (a -> b) -> a -> b
$ [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext ResType
ret
      Maybe (TypeExp Size VName)
Nothing ->
        RetTypeBase Size Freshness -> CheckM (RetTypeBase Size Freshness)
forall a. a -> CheckM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RetTypeBase Size Freshness -> CheckM (RetTypeBase Size Freshness))
-> RetTypeBase Size Freshness
-> CheckM (RetTypeBase Size Freshness)
forall a b. (a -> b) -> a -> b
$
          [VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext (ResType -> RetTypeBase Size Freshness)
-> ResType -> RetTypeBase Size Freshness
forall a b. (a -> b) -> a -> b
$
            [Pat (TypeBase Size Diet)] -> ResType -> TypeAliases -> ResType
inferReturnFreshness [Pat (TypeBase Size Diet)]
params ResType
ret TypeAliases
body_als

    pure
      ( (body', ret'),
        body_als -- Don't matter.
      )
  where
    -- Recursion is monomorphic, so a recursive call is at the type parameters
    -- of the definition itself.
    globals' :: QualName VName -> Maybe BoundV
globals' QualName VName
qn
      | QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
qn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
fname = BoundV -> Maybe BoundV
forall a. a -> Maybe a
Just (BoundV -> Maybe BoundV) -> BoundV -> Maybe BoundV
forall a b. (a -> b) -> a -> b
$ [TypeParam] -> StructType -> BoundV
BoundV [TypeParam]
tparams (StructType -> BoundV) -> StructType -> BoundV
forall a b. (a -> b) -> a -> b
$ [Pat (TypeBase Size Diet)]
-> RetTypeBase Size Freshness -> StructType
forall d.
[Pat (TypeBase d Diet)]
-> RetTypeBase d Freshness -> TypeBase d NoMode
funType [Pat (TypeBase Size Diet)]
params ([VName] -> ResType -> RetTypeBase Size Freshness
forall dim o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [VName]
ext ResType
ret)
      | Bool
otherwise = QualName VName -> Maybe BoundV
globals QualName VName
qn
{-# NOINLINE checkValDef #-}

-- Note [Parametric results]
--
-- Parametricity tells us three things about the result of applying a global
-- function, all read from its *declared* type scheme, which 'envGlobal' looks
-- up: whether the application may have manufactured a value with internal
-- aliasing, whether the result must be fresh because it is the result of an
-- argument that constructs its results freshly, and whether the result may
-- alias a global.
--
-- ## Internal aliasing
--
-- The type system cannot talk about a value that aliases *itself*. For example,
-- a value that is, behind an abstraction boundary, a pair of arrays that are
-- really the same array. Such a value can never be consumed, nor given a fresh
-- type. 'AliasSelf' stands for that possibility. It is not an alias of any
-- variable ('aliasVar' is 'Nothing' for it), so it must never be mistaken for
-- one; ask "might these two values share memory?" through 'overlaps' rather
-- than by comparing alias sets directly. We can think that when 'AliasSelf' is
-- part of an aliasing set then we have "imprecise aliases", and otherwise we
-- have "precise aliases" (but do not take these terms literally; aliasing is
-- almost always an over-approximation).
--
-- Parametricity is what tells us whether such a value can have been
-- manufactured by a given function application.
--
-- The crude answer - a value has internal aliasing whenever it is produced by
-- applying a function whose result type is a nonfresh abstract type - is
-- sound but far too coarse.  It refuses
--
--   module pm (M: {type t}) = {
--     def f (x: *M.t) : *M.t = id x
--   }
--
-- because @id@ is instantiated at @M.t -> M.t@. But @id@ manufactures nothing:
-- its declared type @a -> a@ means, by parametricity, that what it returns *is*
-- its argument, whose aliases we know precisely.
--
-- So we perform a more sophisticated reasonong: a function can only manufacture
-- an abstract value if its result mentions an abstract type that is not one of
-- its own type parameters ('manufacturesAbstract'). This is not the same as
-- "the abstract type also occurs in a parameter": a monomorphic @f: M.t -> M.t@
-- inside a module might well be @\_ -> M.mk 5@, so its type tells us nothing
-- (tests/uniqueness/uniqueness-error75.fut). Only genuine polymorphism does.
--
-- Consumption checking sees only instantiated types, so the declared type is
-- looked up when a name is mentioned ('envGlobal', consulted by 'observeVar')
-- and the answer recorded in the type as an 'AliasSelf' on each function
-- component ('addSelfAliases').  From there ordinary alias propagation carries
-- it: through binding, so @let my_mk = M.mk in my_mk n@ still manufactures;
-- through 'returnType', so partial application does not lose it, and neither
-- does passing the function as an argument, so @n |> M.mk@ manufactures even
-- though @|>@ itself does not.  No arity bookkeeping is needed, because
-- 'AliasSelf' means the same thing at every arity: on a function, "applying
-- this may yield an internally-aliased value", and on a value, "this may have
-- internal aliasing".  'returnType' moves between the two readings for free as
-- the result stops being an arrow.
--
-- This is a conservative over-approximation we use whenever we have no better
-- information available. Hence 'unknownAliases', used for parameters
-- ('selfAliasType') and for any type we build out of thin air, and hence
-- 'closureAliases' keeping the 'AliasSelf' that a function defined here picked
-- up from its own body. Alias sets are combined by union, and a union of "may"
-- is again a "may"; the join of branches in Note [Locations] drops aliases, but
-- never 'AliasSelf'. In some sense, 'AliasSelf' behaves a bit like the top
-- element of a lattice.
--
-- ## Freshness
--
-- Futhark does not have "freshness polymorphism", but we can infer it in some
-- cases by parametricity. Consider
--
--   def (|>) 'a '^b (x: a) (f: a -> b) : b = f x
--
-- The only way for a function to obtain a value of one of its type parameters
-- is to be handed one. Here @b@ occurs among the parameters only as the result
-- of @f@, so the result of @|>@ is necessarily the result of calling @f@. When
-- @f@ in addition constructs its result freshly - as @copy: t -> *t@ does - so
-- does the application.
--
-- In general, a *source* of a type parameter @b@ is a component of a parameter
-- (reached through records) that is a function @t -> b@ observing its argument
-- ('callSources'). The result of an application is fresh when
-- ('resultSources'):
--
-- - every component of the result is either primitive or a type parameter,
--   and each type parameter occurs in it once;
--
-- - each of these type parameters has a source, and occurs at no negative
--   position among the parameters other than its sources; and
--
-- - the argument given for each source constructs its result freshly.
--
-- A negative occurrence that is not a source, such as a parameter of type @b@
-- or @[]b@, or @b@ in the parameter of a source, is a way for the function to
-- be handed values of @b@ other than by calling a source, and the result may
-- then be one of those. An occurrence in the argument of an abstract type
-- counts, as we cannot see where it ends up. A source must also take a single
-- argument and observe it. We know of no program that goes wrong without this
-- restriction, but the argument above has not been made for curried or
-- consuming functions, so they are not sources. The single occurrence is needed
-- because the function may return the result of one call twice:
--
--   def dup 'a 'b (f: a -> b) (x: a) : (b, b) = let r = f x in (r, r)
--
-- Each component of @dup mk_new x@ is fresh on its own, but they are the same
-- array (tests/uniqueness/uniqueness-error118.fut).
--
-- This is a property of the application, not of @|>@ or of its instantiation:
-- @xs |> copy@ is fresh and @xs |> id@ is not, at the very same instantiation.
-- Recall that the instantiation from Terms.hs does not have freshness
-- propagated, so the result in the type is nonfresh, as specified in the type
-- scheme. However, we here update the _instantiated_ type of @|>@ at the
-- application ('parametricFreshness'), which becomes
--
--   (x: []i32) -> (f: []i32 -> *[]i32) -> *[]i32
--
-- From there the ordinary rule for applying a function with a fresh return
-- type does the rest, and later passes get it for free: the monomorphiser keys
-- instances on the type, so @xs |> copy@ and @xs |> id@ become distinct
-- instances, and 'freshenFromInst' in Futhark.Internalise.Monomorphise carries
-- the freshness into the generated definition. Only the result is marked. The
-- body of that definition is @f x@, with @f@ still declared to return a
-- nonfresh value, but nothing checks the one against the other:
-- defunctionalisation replaces @f@ by the function it is applied to, and the
-- call then has the return type of that function.
--
-- A core restriction is that only an application that supplies every parameter
-- of the function's *type* is refined. A partial application may already have
-- evaluated part of the function's body, and the closure it produces may then
-- hold what that part computed. Consider
--
--   def trap 'a 'b 'c (f: a -> b) (x: a) : c -> b =
--     let r = f x in \(_: c) -> r
--
-- Each call @trap mk_new x u@ computes its own @r@, so its result is fresh. But
-- @k = trap mk_new x@ computes @r@ once, and every call of @k@ returns that
-- same @r@ (tests/higher-order-functions/trap.fut). Read plainly, the result
-- of calling @k@ aliases @k@, which is what makes consuming it safe. The type
-- does not say how much of it a partial application evaluates, so no partial
-- application is refined - an operator section included.
--
-- Which parameter a type variable came from is a fact about the declared type,
-- which the instantiated type does not record, so the applied expression must
-- be a direct mention of a named global. Semantically equal programs are
-- therefore treated differently -
--
--   xs |> copy      -- fresh
--   (|>) xs copy    -- not fresh
--
-- - and the refinement is lost by anything that obscures the head, including
-- parentheses and @let@. This is never *wrong*, only conservative: a spelling
-- we do not recognise yields the plain reading.
--
-- ## Globals
--
-- A use of a global aliases that global, and globals cannot be consumed. When
-- applying a global function returning a nonfresh result, the result thereby
-- aliases the global, and hence cannot be consumed.
--
-- Parametricity keeps polymorphic functions such as @transpose@ precise
-- ('globalAliases'). An edge case is polymorphic "values", which arise solely
-- (I think) for arrays, as an empty array literal can have any element type. To
-- address this, our semantics for polymorphic values is that they are
-- implicitly functions; re-computed on every access to the global. The
-- monomorphiser ensures that by compiling a polymorphic value as a function of
-- @()@, so that each use computes it anew, just as a size-polymorphic value is
-- a function of its sizes. Hence:
--
-- - A component that is not a function, and whose declared type contains one of
--   the global's type parameters, does not alias the global. So @empty 'a :
--   []a@ aliases nothing, while the first component of @pv 'a : ([]i32, []a)@
--   aliases @pv@. An array such as @[](a, i32)@ also counts: it has elements
--   only if it was handed some, and the only way of pairing them with other
--   data, @zip@, constructs its result freshly.
--
-- - A type parameter that is an argument to an abstract type does not count.
--   The module defining @M.t@ may well have @type t 'a = i32@, and so a value
--   of type @M.t a@ or @[](M.t a)@ may be a global.
--
-- - A function aliases the global exactly when some nonfresh component of its
--   (curried) result is not of that kind. So @transpose@, @reverse@ and @|>@
--   alias nothing, and their results alias only their arguments, while the
--   results of @tail : []i32 -> []i32@ alias @tail@ and cannot be consumed. A
--   function has a single alias set, so in a result such as @([]i32, a)@ the
--   second component is also taken to alias the function.
--
-- Size parameters do not count: as far as types can tell, @zeros [n] : [n]i32@
-- might be (a slice of) a global, so it aliases @zeros@.
--
-- This reasoning needs the type parameters, which monomorphisation removes.
-- Hence, monomorphising a Futhark program results in a program that may no
-- longer be correct as far as (this) alias analysis is concerned.

-- Note [Locations]
--
-- Compound types (records and sums) do not have identity. Instead, we track
-- aliasing and consumption at the level of their components ("leaves"). A
-- "path" is a reference to the component of a compound type.
--
-- A location is a variable together with a path ('Location'); every 'Alias'
-- except 'AliasSelf' denotes one. The consumed set holds locations, and a
-- location is dead if a location on the same variable has been consumed whose
-- path is a prefix of its own, or of which its own is a prefix ('deadIn').
-- Consuming @p.a@ kills @p.a@, everything under it, and @p@ itself; consuming
-- @p@ kills all of @p@.
--
-- The payload of a constructor is treated exactly as a tuple, nested under the
-- constructor name: the payload of @#foo xs ys@ has the paths @[foo, 0]@ and
-- @[foo, 1]@.  The components of a sum are therefore separate parts, so
-- @#foo u u@ is self-aliasing just like @(u, u)@, and its payload can be taken
-- apart by pattern matching just like a tuple.
--
-- Using a variable reads all of it: its alias set has a location for each of
-- its leaves, and observing it requires them all to be alive.  Projection
-- happens afterwards.  So to consume one component of a tuple and keep using
-- another, take the tuple apart first:
--
--   let (a, b) = p in let a[0] = 1 in b      -- accepted
--   let a = p.0 in let a[0] = 1 in p.1       -- rejected: p.1 reads p
--
-- Components that may coincide have overlapping alias sets, which is what
-- 'separated' and 'unfreshness' look for.  Building a value preserves this, as
-- each component aliases what it was built from, and so does applying a
-- function or running a loop, as every nonfresh component of the result aliases
-- the same internal name.  The exceptions are an observed parameter, whose
-- components the caller may have made coincide, and a component with
-- 'AliasSelf'.  Neither can be consumed, and the locations of an observed
-- parameter never die.
--
-- The join of the branches of an @if@ or @match@ ('joinBranches') keeps an alias of the combined branch
-- results if it is 'AliasSelf', or if its location and every location in its
-- alias set ('aliasOf') are alive after the branches; the other aliases are
-- consumed.  Filtering by liveness in this way, rather than subtracting the
-- consumed set, is closed under aliasing: if an alias survives, so does
-- everything it aliases.  This is the only place where aliases are dropped, and
-- it may drop the evidence that two components coincide.  Consider
--
--   let (r0, r1) = if c then (u, u) else (let z = u with [0] = 5 in (a, b))
--
-- The else branch consumes @u@, so the filter alone would leave the aliases
-- @({a}, {b})@, claiming that the components of the result are separate, which
-- is false when @c@ holds.  So when the components of some branch's result
-- overlap, the join adds an alias of a fresh name to every component of the
-- combined result.  Being fresh, it is alive after the branches, and as it is
-- consumed along with any component, consuming @r0@ kills @r1@.
--
-- Futhark is not in A-normal form, but an expression that builds a value from
-- operands behaves as if it were: it evaluates all of its operands, and then
-- uses their values. This covers tuples, records, constructors and arrays,
-- indexing, operator sections, and function application (which evaluates its
-- arguments from right to left, and then the function). So the value of an
-- operand must not alias anything that a later operand consumes. A function
-- application then consumes what its parameters consume. A consumed component
-- of an argument must not share a location with any other component of that
-- argument ('noSelfAliases'), and must not overlap the function being applied
-- or any other argument ('passArgs').  The diet of a function parameter is the
-- same for all of its components, but that of a loop parameter is not.
--
-- A loop is checked as a recursive call whose arguments are what its body
-- returns ('checkLoopResult').  The value returned for a consumed loop
-- parameter is consumed in the next iteration, so it must be fresh in exactly
-- the sense below, with the loop parameters as the parameters.  The diets of
-- the loop parameters are inferred first: a parameter is consumed if the body
-- consumes it or the value returned for a consumed parameter aliases it
-- ('convergeLoopParam').
--
-- A component of a function's result may be fresh exactly when every in-scope
-- location it aliases lies within a consumed part of a parameter, none of its
-- locations occurs in another component, and it is not 'selfAliased'.  The one
-- predicate ('unfreshness') both infers fresh return types and checks declared
-- ones, so declared freshness never exceeds what would be inferred.