{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Trustworthy #-}

-- | Facilities for type-checking terms.  Factored out of
-- "Language.Futhark.TypeChecker.Terms" to prevent the module from
-- being gigantic.
--
-- Incidentally also a nice place to put Haddock comments to make the
-- internal API of the type checker easier to browse.
module Language.Futhark.TypeChecker.Terms.Monad
  ( TermTypeM,
    runTermTypeM,
    liftTypeM,
    ValBinding (..),
    Locality (..),
    SizeSource (SourceBound, SourceSlice),
    NameReason (..),
    InferredType (..),
    Checking (..),
    withEnv,
    localScope,
    TermEnv (..),
    TermScope (..),
    TermTypeState (..),
    onFailure,
    extSize,
    expType,
    expTypeFully,
    constrain,
    newArrayType,
    allDimsFreshInType,
    updateTypes,

    -- * Primitive checking
    unifies,
    require,
    checkTypeExpNonrigid,
    checkTypeExpRigid,

    -- * Sizes
    isInt64,
    maybeDimFromExp,
    dimFromExp,
    sizeFromArg,
    noSizeEscape,

    -- * Control flow
    collectOccurrences,
    tapOccurrences,
    alternative,
    sequentially,
    incLevel,

    -- * Consumption and uniqueness
    Names,
    Occurrence (..),
    Occurrences,
    onlySelfAliasing,
    noUnique,
    removeSeminullOccurrences,
    occur,
    observe,
    consume,
    consuming,
    observation,
    consumption,
    checkIfConsumable,
    seqOccurrences,
    checkOccurrences,
    allConsumed,

    -- * Errors
    useAfterConsume,
    unusedSize,
    notConsumable,
    uniqueReturnAliased,
    returnAliased,
    badLetWithValue,
    anyConsumption,
    allOccurring,
  )
where

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.Bitraversable
import Data.Char (isAscii)
import Data.List (find, isPrefixOf, sort)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Util.Pretty hiding (bool, group, space)
import Language.Futhark
import Language.Futhark.Semantic (includeToFilePath)
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import qualified Language.Futhark.TypeChecker.Monad as TypeM
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify hiding (Usage)
import Prelude hiding (mod)

--- Uniqueness

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

type Names = S.Set VName

-- | The consumption set is a Maybe so we can distinguish whether a
-- consumption took place, but the variable went out of scope since,
-- or no consumption at all took place.
data Occurrence = Occurrence
  { Occurrence -> Set VName
observed :: Names,
    Occurrence -> Maybe (Set VName)
consumed :: Maybe Names,
    Occurrence -> SrcLoc
location :: SrcLoc
  }
  deriving (Occurrence -> Occurrence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Occurrence -> Occurrence -> Bool
$c/= :: Occurrence -> Occurrence -> Bool
== :: Occurrence -> Occurrence -> Bool
$c== :: Occurrence -> Occurrence -> Bool
Eq, Int -> Occurrence -> ShowS
Occurrences -> ShowS
Occurrence -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: Occurrences -> ShowS
$cshowList :: Occurrences -> ShowS
show :: Occurrence -> String
$cshow :: Occurrence -> String
showsPrec :: Int -> Occurrence -> ShowS
$cshowsPrec :: Int -> Occurrence -> ShowS
Show)

instance Located Occurrence where
  locOf :: Occurrence -> Loc
locOf = forall a. Located a => a -> Loc
locOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> SrcLoc
location

observation :: Aliasing -> SrcLoc -> Occurrence
observation :: Aliasing -> SrcLoc -> Occurrence
observation = forall a b c. (a -> b -> c) -> b -> a -> c
flip Set VName -> Maybe (Set VName) -> SrcLoc -> Occurrence
Occurrence forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar

consumption :: Aliasing -> SrcLoc -> Occurrence
consumption :: Aliasing -> SrcLoc -> Occurrence
consumption = Set VName -> Maybe (Set VName) -> SrcLoc -> Occurrence
Occurrence forall a. Set a
S.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar

-- | A null occurence is one that we can remove without affecting
-- anything.
nullOccurrence :: Occurrence -> Bool
nullOccurrence :: Occurrence -> Bool
nullOccurrence Occurrence
occ = forall a. Set a -> Bool
S.null (Occurrence -> Set VName
observed Occurrence
occ) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (Occurrence -> Maybe (Set VName)
consumed Occurrence
occ)

-- | A seminull occurence is one that does not contain references to
-- any variables in scope.  The big difference is that a seminull
-- occurence may denote a consumption, as long as the array that was
-- consumed is now out of scope.
seminullOccurrence :: Occurrence -> Bool
seminullOccurrence :: Occurrence -> Bool
seminullOccurrence Occurrence
occ = forall a. Set a -> Bool
S.null (Occurrence -> Set VName
observed Occurrence
occ) Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True forall a. Set a -> Bool
S.null (Occurrence -> Maybe (Set VName)
consumed Occurrence
occ)

type Occurrences = [Occurrence]

type UsageMap = M.Map VName [Usage]

usageMap :: Occurrences -> UsageMap
usageMap :: Occurrences -> UsageMap
usageMap = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl UsageMap -> Occurrence -> UsageMap
comb forall k a. Map k a
M.empty
  where
    comb :: UsageMap -> Occurrence -> UsageMap
comb UsageMap
m (Occurrence Set VName
obs Maybe (Set VName)
cons SrcLoc
loc) =
      let m' :: UsageMap
m' = forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (forall {k} {a}. Ord k => a -> Map k [a] -> k -> Map k [a]
ins forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Observed SrcLoc
loc) UsageMap
m Set VName
obs
       in forall a b. (a -> b -> a) -> a -> Set b -> a
S.foldl' (forall {k} {a}. Ord k => a -> Map k [a] -> k -> Map k [a]
ins forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Consumed SrcLoc
loc) UsageMap
m' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty Maybe (Set VName)
cons
    ins :: a -> Map k [a] -> k -> Map k [a]
ins a
v Map k [a]
m k
k = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith forall a. [a] -> [a] -> [a]
(++) k
k [a
v] Map k [a]
m

combineOccurrences :: VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences :: VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences VName
_ (Observed SrcLoc
loc) (Observed SrcLoc
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
Observed SrcLoc
loc
combineOccurrences VName
name (Consumed SrcLoc
wloc) (Observed SrcLoc
rloc) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc
combineOccurrences VName
name (Observed SrcLoc
rloc) (Consumed SrcLoc
wloc) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc
combineOccurrences VName
name (Consumed SrcLoc
loc1) (Consumed SrcLoc
loc2) =
  forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name (forall a. Ord a => a -> a -> a
max SrcLoc
loc1 SrcLoc
loc2) (forall a. Ord a => a -> a -> a
min SrcLoc
loc1 SrcLoc
loc2)

checkOccurrences :: Occurrences -> TermTypeM ()
checkOccurrences :: Occurrences -> TermTypeM ()
checkOccurrences = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey VName -> [Usage] -> TermTypeM ()
comb forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrences -> UsageMap
usageMap
  where
    comb :: VName -> [Usage] -> TermTypeM ()
comb VName
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    comb VName
name (Usage
u : [Usage]
us) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (VName -> Usage -> Usage -> TermTypeM Usage
combineOccurrences VName
name) Usage
u [Usage]
us

allObserved :: Occurrences -> Names
allObserved :: Occurrences -> Set VName
allObserved = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Set VName
observed

allConsumed :: Occurrences -> Names
allConsumed :: Occurrences -> Set VName
allConsumed = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Maybe (Set VName)
consumed)

allOccurring :: Occurrences -> Names
allOccurring :: Occurrences -> Set VName
allOccurring Occurrences
occs = Occurrences -> Set VName
allConsumed Occurrences
occs forall a. Semigroup a => a -> a -> a
<> Occurrences -> Set VName
allObserved Occurrences
occs

anyConsumption :: Occurrences -> Maybe Occurrence
anyConsumption :: Occurrences -> Maybe Occurrence
anyConsumption = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Maybe (Set VName)
consumed)

seqOccurrences :: Occurrences -> Occurrences -> Occurrences
seqOccurrences :: Occurrences -> Occurrences -> Occurrences
seqOccurrences Occurrences
occurs1 Occurrences
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
nullOccurrence) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt Occurrences
occurs1 forall a. [a] -> [a] -> [a]
++ Occurrences
occurs2
  where
    filt :: Occurrence -> Occurrence
filt Occurrence
occ =
      Occurrence
occ {observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
postcons}
    postcons :: Set VName
postcons = Occurrences -> Set VName
allConsumed Occurrences
occurs2

altOccurrences :: Occurrences -> Occurrences -> Occurrences
altOccurrences :: Occurrences -> Occurrences -> Occurrences
altOccurrences Occurrences
occurs1 Occurrences
occurs2 =
  forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
nullOccurrence) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt1 Occurrences
occurs1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> Occurrence
filt2 Occurrences
occurs2
  where
    filt1 :: Occurrence -> Occurrence
filt1 Occurrence
occ =
      Occurrence
occ
        { consumed :: Maybe (Set VName)
consumed = forall a. Ord a => Set a -> Set a -> Set a
S.difference forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Occurrence -> Maybe (Set VName)
consumed Occurrence
occ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Set VName
cons2,
          observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
cons2
        }
    filt2 :: Occurrence -> Occurrence
filt2 Occurrence
occ =
      Occurrence
occ
        { consumed :: Maybe (Set VName)
consumed = Occurrence -> Maybe (Set VName)
consumed Occurrence
occ,
          observed :: Set VName
observed = Occurrence -> Set VName
observed Occurrence
occ forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
cons1
        }
    cons1 :: Set VName
cons1 = Occurrences -> Set VName
allConsumed Occurrences
occurs1
    cons2 :: Set VName
cons2 = Occurrences -> Set VName
allConsumed Occurrences
occurs2

-- | How something was bound.
data Locality
  = -- | In the current function
    Local
  | -- | In an enclosing function, but not the current one.
    Nonlocal
  | -- | At global scope.
    Global
  deriving (Int -> Locality -> ShowS
[Locality] -> ShowS
Locality -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Locality] -> ShowS
$cshowList :: [Locality] -> ShowS
show :: Locality -> String
$cshow :: Locality -> String
showsPrec :: Int -> Locality -> ShowS
$cshowsPrec :: Int -> Locality -> ShowS
Show, Locality -> Locality -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Locality -> Locality -> Bool
$c/= :: Locality -> Locality -> Bool
== :: Locality -> Locality -> Bool
$c== :: Locality -> Locality -> Bool
Eq, Eq Locality
Locality -> Locality -> Bool
Locality -> Locality -> Ordering
Locality -> Locality -> Locality
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Locality -> Locality -> Locality
$cmin :: Locality -> Locality -> Locality
max :: Locality -> Locality -> Locality
$cmax :: Locality -> Locality -> Locality
>= :: Locality -> Locality -> Bool
$c>= :: Locality -> Locality -> Bool
> :: Locality -> Locality -> Bool
$c> :: Locality -> Locality -> Bool
<= :: Locality -> Locality -> Bool
$c<= :: Locality -> Locality -> Bool
< :: Locality -> Locality -> Bool
$c< :: Locality -> Locality -> Bool
compare :: Locality -> Locality -> Ordering
$ccompare :: Locality -> Locality -> Ordering
Ord)

data ValBinding
  = -- | Aliases in parameters indicate the lexical
    -- closure.
    BoundV Locality [TypeParam] PatType
  | OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)
  | EqualityF
  | WasConsumed SrcLoc
  deriving (Int -> ValBinding -> ShowS
[ValBinding] -> ShowS
ValBinding -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValBinding] -> ShowS
$cshowList :: [ValBinding] -> ShowS
show :: ValBinding -> String
$cshow :: ValBinding -> String
showsPrec :: Int -> ValBinding -> ShowS
$cshowsPrec :: Int -> ValBinding -> ShowS
Show)

--- Errors

describeVar :: SrcLoc -> VName -> TermTypeM Doc
describeVar :: SrcLoc -> VName -> TermTypeM Doc
describeVar SrcLoc
loc VName
v =
  forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc
"variable" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
v)) (SrcLoc -> NameReason -> Doc
nameReason SrcLoc
loc)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermTypeState -> Map VName NameReason
stateNames

useAfterConsume :: VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume :: forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
rloc SrcLoc
wloc = do
  Doc
name' <- SrcLoc -> VName -> TermTypeM Doc
describeVar SrcLoc
rloc VName
name
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
rloc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc -> Doc
withIndexLink Doc
"use-after-consume" forall a b. (a -> b) -> a -> b
$
    Doc
"Using"
      Doc -> Doc -> Doc
<+> Doc
name' forall a. Semigroup a => a -> a -> a
<> Doc
", but this was consumed at"
      Doc -> Doc -> Doc
<+> String -> Doc
text (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
rloc SrcLoc
wloc) forall a. Semigroup a => a -> a -> a
<> Doc
".  (Possibly through aliasing.)"

badLetWithValue :: (Pretty arr, Pretty src) => arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue :: forall arr src a.
(Pretty arr, Pretty src) =>
arr -> src -> SrcLoc -> TermTypeM a
badLetWithValue arr
arre src
vale SrcLoc
loc =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
    Doc
"Source array for in-place update"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr arr
arre)
      Doc -> Doc -> Doc
</> Doc
"might alias update value"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr src
vale)
      Doc -> Doc -> Doc
</> Doc
"Hint: use"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote Doc
"copy"
      Doc -> Doc -> Doc
<+> Doc
"to remove aliases from the value."

returnAliased :: Name -> SrcLoc -> TermTypeM ()
returnAliased :: Name -> SrcLoc -> TermTypeM ()
returnAliased Name
name SrcLoc
loc =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc -> Doc
withIndexLink Doc
"return-aliased" forall a b. (a -> b) -> a -> b
$
    Doc
"Unique-typed return value is aliased to"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName Name
name) forall a. Semigroup a => a -> a -> a
<> Doc
", which is not consumable."

uniqueReturnAliased :: SrcLoc -> TermTypeM a
uniqueReturnAliased :: forall a. SrcLoc -> TermTypeM a
uniqueReturnAliased SrcLoc
loc =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc -> Doc
withIndexLink Doc
"unique-return-aliased" forall a b. (a -> b) -> a -> b
$
    Doc
"A unique-typed component of the return value is aliased to some other component."

notConsumable :: MonadTypeChecker m => SrcLoc -> Doc -> m b
notConsumable :: forall (m :: * -> *) b. MonadTypeChecker m => SrcLoc -> Doc -> m b
notConsumable SrcLoc
loc Doc
v =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc -> Doc
withIndexLink Doc
"not-consumable" forall a b. (a -> b) -> a -> b
$
    Doc
"Would consume" Doc -> Doc -> Doc
<+> Doc
v forall a. Semigroup a => a -> a -> a
<> Doc
", which is not consumable."

unusedSize :: (MonadTypeChecker m) => SizeBinder VName -> m a
unusedSize :: forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
p =
  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SizeBinder VName
p forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc -> Doc
withIndexLink Doc
"unused-size" forall a b. (a -> b) -> a -> b
$
    Doc
"Size" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr SizeBinder VName
p Doc -> Doc -> Doc
<+> Doc
"unused in pattern."

--- Scope management

data InferredType
  = NoneInferred
  | Ascribed PatType

data Checking
  = CheckingApply (Maybe (QualName VName)) Exp StructType StructType
  | CheckingReturn StructType StructType
  | CheckingAscription StructType StructType
  | CheckingLetGeneralise Name
  | CheckingParams (Maybe Name)
  | CheckingPat UncheckedPat InferredType
  | CheckingLoopBody StructType StructType
  | CheckingLoopInitial StructType StructType
  | CheckingRecordUpdate [Name] StructType StructType
  | CheckingRequired [StructType] StructType
  | CheckingBranches StructType StructType

instance Pretty Checking where
  ppr :: Checking -> Doc
ppr (CheckingApply Maybe (QualName VName)
f Exp
e StructType
expected StructType
actual) =
    Doc
header
      Doc -> Doc -> Doc
</> Doc
"Expected:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"Actual:  "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
    where
      header :: Doc
header =
        case Maybe (QualName VName)
f of
          Maybe (QualName VName)
Nothing ->
            Doc
"Cannot apply function to"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
shorten forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$ Doc -> Doc
flatten forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
ppr Exp
e) forall a. Semigroup a => a -> a -> a
<> Doc
" (invalid type)."
          Just QualName VName
fname ->
            Doc
"Cannot apply"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName VName
fname)
              Doc -> Doc -> Doc
<+> Doc
"to"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
shorten forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$ Doc -> Doc
flatten forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
ppr Exp
e) forall a. Semigroup a => a -> a -> a
<> Doc
" (invalid type)."
  ppr (CheckingReturn StructType
expected StructType
actual) =
    Doc
"Function body does not have expected type."
      Doc -> Doc -> Doc
</> Doc
"Expected:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"Actual:  "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
  ppr (CheckingAscription StructType
expected StructType
actual) =
    Doc
"Expression does not have expected type from explicit ascription."
      Doc -> Doc -> Doc
</> Doc
"Expected:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"Actual:  "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
  ppr (CheckingLetGeneralise Name
fname) =
    Doc
"Cannot generalise type of" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Name
fname) forall a. Semigroup a => a -> a -> a
<> Doc
"."
  ppr (CheckingParams Maybe Name
fname) =
    Doc
"Invalid use of parameters in" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote Doc
fname' forall a. Semigroup a => a -> a -> a
<> Doc
"."
    where
      fname' :: Doc
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"anonymous function" forall a. Pretty a => a -> Doc
ppr Maybe Name
fname
  ppr (CheckingPat UncheckedPat
pat InferredType
NoneInferred) =
    Doc
"Invalid pattern" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr UncheckedPat
pat) forall a. Semigroup a => a -> a -> a
<> Doc
"."
  ppr (CheckingPat UncheckedPat
pat (Ascribed PatType
t)) =
    Doc
"Pat"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr UncheckedPat
pat)
      Doc -> Doc -> Doc
<+> Doc
"cannot match value of type"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr PatType
t)
  ppr (CheckingLoopBody StructType
expected StructType
actual) =
    Doc
"Loop body does not have expected type."
      Doc -> Doc -> Doc
</> Doc
"Expected:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"Actual:  "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
  ppr (CheckingLoopInitial StructType
expected StructType
actual) =
    Doc
"Initial loop values do not have expected type."
      Doc -> Doc -> Doc
</> Doc
"Expected:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"Actual:  "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
  ppr (CheckingRecordUpdate [Name]
fs StructType
expected StructType
actual) =
    Doc
"Type mismatch when updating record field"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote Doc
fs' forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
</> Doc
"Existing:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
expected)
      Doc -> Doc -> Doc
</> Doc
"New:     "
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
    where
      fs' :: Doc
fs' = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [Name]
fs
  ppr (CheckingRequired [StructType
expected] StructType
actual) =
    Doc
"Expression must must have type"
      Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr StructType
expected forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
</> Doc
"Actual type:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
  ppr (CheckingRequired [StructType]
expected StructType
actual) =
    Doc
"Type of expression must must be one of "
      Doc -> Doc -> Doc
<+> Doc
expected' forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
</> Doc
"Actual type:"
      Doc -> Doc -> Doc
<+> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
actual)
    where
      expected' :: Doc
expected' = [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [StructType]
expected)
  ppr (CheckingBranches StructType
t1 StructType
t2) =
    Doc
"Branches differ in type."
      Doc -> Doc -> Doc
</> Doc
"Former:"
      Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr StructType
t1
      Doc -> Doc -> Doc
</> Doc
"Latter:"
      Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr StructType
t2

-- | Type checking happens with access to this environment.  The
-- 'TermScope' will be extended during type-checking as bindings come into
-- scope.
data TermEnv = TermEnv
  { TermEnv -> TermScope
termScope :: TermScope,
    TermEnv -> Maybe Checking
termChecking :: Maybe Checking,
    TermEnv -> Int
termLevel :: Level
  }

data TermScope = TermScope
  { TermScope -> Map VName ValBinding
scopeVtable :: M.Map VName ValBinding,
    TermScope -> Map VName TypeBinding
scopeTypeTable :: M.Map VName TypeBinding,
    TermScope -> Map VName Mod
scopeModTable :: M.Map VName Mod,
    TermScope -> NameMap
scopeNameMap :: NameMap
  }
  deriving (Int -> TermScope -> ShowS
[TermScope] -> ShowS
TermScope -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermScope] -> ShowS
$cshowList :: [TermScope] -> ShowS
show :: TermScope -> String
$cshow :: TermScope -> String
showsPrec :: Int -> TermScope -> ShowS
$cshowsPrec :: Int -> TermScope -> ShowS
Show)

instance Semigroup TermScope where
  TermScope Map VName ValBinding
vt1 Map VName TypeBinding
tt1 Map VName Mod
mt1 NameMap
nt1 <> :: TermScope -> TermScope -> TermScope
<> TermScope Map VName ValBinding
vt2 Map VName TypeBinding
tt2 Map VName Mod
mt2 NameMap
nt2 =
    Map VName ValBinding
-> Map VName TypeBinding -> Map VName Mod -> NameMap -> TermScope
TermScope (Map VName ValBinding
vt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName ValBinding
vt1) (Map VName TypeBinding
tt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName TypeBinding
tt1) (Map VName Mod
mt1 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map VName Mod
mt2) (NameMap
nt2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` NameMap
nt1)

envToTermScope :: Env -> TermScope
envToTermScope :: Env -> TermScope
envToTermScope Env
env =
  TermScope
    { scopeVtable :: Map VName ValBinding
scopeVtable = Map VName ValBinding
vtable,
      scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = Env -> Map VName TypeBinding
envTypeTable Env
env,
      scopeNameMap :: NameMap
scopeNameMap = Env -> NameMap
envNameMap Env
env,
      scopeModTable :: Map VName Mod
scopeModTable = Env -> Map VName Mod
envModTable Env
env
    }
  where
    vtable :: Map VName ValBinding
vtable = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> BoundV -> ValBinding
valBinding forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
env
    valBinding :: VName -> BoundV -> ValBinding
valBinding VName
k (TypeM.BoundV [TypeParam]
tps StructType
v) =
      Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [TypeParam]
tps forall a b. (a -> b) -> a -> b
$ forall {as} {dim} {as}.
Monoid as =>
as -> TypeBase dim as -> TypeBase dim as
selfAliasing (forall a. a -> Set a
S.singleton (VName -> Alias
AliasBound VName
k)) StructType
v
    -- FIXME: hack, #1675
    selfAliasing :: as -> TypeBase dim as -> TypeBase dim as
selfAliasing as
als (Scalar (Record Map Name (TypeBase dim as)
ts)) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map (as -> TypeBase dim as -> TypeBase dim as
selfAliasing as
als) Map Name (TypeBase dim as)
ts
    selfAliasing as
als TypeBase dim as
t =
      TypeBase dim as
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` (if forall dim as. TypeBase dim as -> Int
arrayRank TypeBase dim as
t forall a. Ord a => a -> a -> Bool
> Int
0 then as
als else forall a. Monoid a => a
mempty)

withEnv :: TermEnv -> Env -> TermEnv
withEnv :: TermEnv -> Env -> TermEnv
withEnv TermEnv
tenv Env
env = TermEnv
tenv {termScope :: TermScope
termScope = TermEnv -> TermScope
termScope TermEnv
tenv forall a. Semigroup a => a -> a -> a
<> Env -> TermScope
envToTermScope Env
env}

-- | Wrap a function name to give it a vacuous Eq instance for SizeSource.
newtype FName = FName (Maybe (QualName VName))
  deriving (Int -> FName -> ShowS
[FName] -> ShowS
FName -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FName] -> ShowS
$cshowList :: [FName] -> ShowS
show :: FName -> String
$cshow :: FName -> String
showsPrec :: Int -> FName -> ShowS
$cshowsPrec :: Int -> FName -> ShowS
Show)

instance Eq FName where
  FName
_ == :: FName -> FName -> Bool
== FName
_ = Bool
True

instance Ord FName where
  compare :: FName -> FName -> Ordering
compare FName
_ FName
_ = Ordering
EQ

-- | What was the source of some existential size?  This is used for
-- using the same existential variable if the same source is
-- encountered in multiple locations.
data SizeSource
  = SourceArg FName (ExpBase NoInfo VName)
  | SourceBound (ExpBase NoInfo VName)
  | SourceSlice
      (Maybe Size)
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
      (Maybe (ExpBase NoInfo VName))
  deriving (SizeSource -> SizeSource -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SizeSource -> SizeSource -> Bool
$c/= :: SizeSource -> SizeSource -> Bool
== :: SizeSource -> SizeSource -> Bool
$c== :: SizeSource -> SizeSource -> Bool
Eq, Eq SizeSource
SizeSource -> SizeSource -> Bool
SizeSource -> SizeSource -> Ordering
SizeSource -> SizeSource -> SizeSource
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SizeSource -> SizeSource -> SizeSource
$cmin :: SizeSource -> SizeSource -> SizeSource
max :: SizeSource -> SizeSource -> SizeSource
$cmax :: SizeSource -> SizeSource -> SizeSource
>= :: SizeSource -> SizeSource -> Bool
$c>= :: SizeSource -> SizeSource -> Bool
> :: SizeSource -> SizeSource -> Bool
$c> :: SizeSource -> SizeSource -> Bool
<= :: SizeSource -> SizeSource -> Bool
$c<= :: SizeSource -> SizeSource -> Bool
< :: SizeSource -> SizeSource -> Bool
$c< :: SizeSource -> SizeSource -> Bool
compare :: SizeSource -> SizeSource -> Ordering
$ccompare :: SizeSource -> SizeSource -> Ordering
Ord, Int -> SizeSource -> ShowS
[SizeSource] -> ShowS
SizeSource -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SizeSource] -> ShowS
$cshowList :: [SizeSource] -> ShowS
show :: SizeSource -> String
$cshow :: SizeSource -> String
showsPrec :: Int -> SizeSource -> ShowS
$cshowsPrec :: Int -> SizeSource -> ShowS
Show)

-- | 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

nameReason :: SrcLoc -> NameReason -> Doc
nameReason :: SrcLoc -> NameReason -> Doc
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
Nothing SrcLoc
apploc) =
  Doc
"result of application at" Doc -> Doc -> Doc
<+> String -> Doc
text (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
loc SrcLoc
apploc)
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
fname SrcLoc
apploc) =
  Doc
"result of applying"
    Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Maybe (QualName VName)
fname)
    Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Doc
"at" Doc -> Doc -> Doc
<+> String -> Doc
text (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
loc SrcLoc
apploc))

-- | The state is a set of constraints and a counter for generating
-- type names.  This is distinct from the usual counter we use for
-- generating unique names, as these will be user-visible.
data TermTypeState = TermTypeState
  { TermTypeState -> Constraints
stateConstraints :: Constraints,
    TermTypeState -> Int
stateCounter :: !Int,
    -- | Mapping function arguments encountered to
    -- the sizes they ended up generating (when
    -- they could not be substituted directly).
    -- This happens for function arguments that are
    -- not constants or names.
    TermTypeState -> Map SizeSource VName
stateDimTable :: M.Map SizeSource VName,
    TermTypeState -> Map VName NameReason
stateNames :: M.Map VName NameReason,
    TermTypeState -> Occurrences
stateOccs :: Occurrences
  }

newtype TermTypeM a
  = TermTypeM (ReaderT TermEnv (StateT TermTypeState TypeM) a)
  deriving
    ( Applicative TermTypeM
forall a. a -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TermTypeM a
$creturn :: forall a. a -> TermTypeM a
>> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
$c>> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
>>= :: forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
$c>>= :: forall a b. TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b
Monad,
      forall a b. a -> TermTypeM b -> TermTypeM a
forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TermTypeM b -> TermTypeM a
$c<$ :: forall a b. a -> TermTypeM b -> TermTypeM a
fmap :: forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
$cfmap :: forall a b. (a -> b) -> TermTypeM a -> TermTypeM b
Functor,
      Functor TermTypeM
forall a. a -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
$c<* :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
*> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
$c*> :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM b
liftA2 :: forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c
<*> :: forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
$c<*> :: forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
pure :: forall a. a -> TermTypeM a
$cpure :: forall a. a -> TermTypeM a
Applicative,
      MonadReader TermEnv,
      MonadState TermTypeState,
      MonadError TypeError
    )

liftTypeM :: TypeM a -> TermTypeM a
liftTypeM :: forall a. TypeM a -> TermTypeM a
liftTypeM = forall a.
ReaderT TermEnv (StateT TermTypeState TypeM) a -> TermTypeM a
TermTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

incCounter :: TermTypeM Int
incCounter :: TermTypeM Int
incCounter = do
  TermTypeState
s <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put TermTypeState
s {stateCounter :: Int
stateCounter = TermTypeState -> Int
stateCounter TermTypeState
s forall a. Num a => a -> a -> a
+ Int
1}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TermTypeState -> Int
stateCounter TermTypeState
s

constrain :: VName -> Constraint -> TermTypeM ()
constrain :: VName -> Constraint -> TermTypeM ()
constrain VName
v Constraint
c = do
  Int
lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
  forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
lvl, Constraint
c)

instance MonadUnify TermTypeM where
  getConstraints :: TermTypeM Constraints
getConstraints = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Constraints
stateConstraints
  putConstraints :: Constraints -> TermTypeM ()
putConstraints Constraints
x = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateConstraints :: Constraints
stateConstraints = Constraints
x}

  newTypeVar :: forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
newTypeVar SrcLoc
loc Name
desc = do
    Int
i <- TermTypeM Int
incCounter
    VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
desc Int
i
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Lifted forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []

  curLevel :: TermTypeM Int
curLevel = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Int
termLevel

  newDimVar :: SrcLoc -> Rigidity -> Name -> TermTypeM VName
newDimVar SrcLoc
loc Rigidity
rigidity Name
name = do
    VName
dim <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
name
    case Rigidity
rigidity of
      Rigid RigidSource
rsrc -> VName -> Constraint -> TermTypeM ()
constrain VName
dim forall a b. (a -> b) -> a -> b
$ SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
loc RigidSource
rsrc
      Rigidity
Nonrigid -> VName -> Constraint -> TermTypeM ()
constrain VName
dim forall a b. (a -> b) -> a -> b
$ Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim

  unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc -> TermTypeM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc
doc = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking' ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
          Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
            forall a. Pretty a => a -> Doc
ppr Checking
checking' forall a. Semigroup a => a -> a -> a
<> Doc
line Doc -> Doc -> Doc
</> Doc
doc forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ Doc
doc forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr BreadCrumbs
bcs

  matchError :: forall loc a.
Located loc =>
loc
-> Notes -> BreadCrumbs -> StructType -> StructType -> TermTypeM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking'
        | BreadCrumbs -> Bool
hasNoBreadCrumbs BreadCrumbs
bcs ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
                forall a. Pretty a => a -> Doc
ppr Checking
checking'
        | Bool
otherwise ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$
                forall a. Pretty a => a -> Doc
ppr Checking
checking' forall a. Semigroup a => a -> a -> a
<> Doc
line Doc -> Doc -> Doc
</> Doc
doc forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ Doc
doc forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
    where
      doc :: Doc
doc =
        Doc
"Types"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t1)
          Doc -> Doc -> Doc
</> Doc
"and"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t2)
          Doc -> Doc -> Doc
</> Doc
"do not match."

-- | Instantiate a type scheme with fresh type variables for its type
-- parameters. Returns the names of the fresh type variables, the
-- instance list, and the instantiated type.
instantiateTypeScheme ::
  QualName VName ->
  SrcLoc ->
  [TypeParam] ->
  PatType ->
  TermTypeM ([VName], PatType)
instantiateTypeScheme :: QualName VName
-> SrcLoc -> [TypeParam] -> PatType -> TermTypeM ([VName], PatType)
instantiateTypeScheme QualName VName
qn SrcLoc
loc [TypeParam]
tparams PatType
t = do
  let tnames :: [VName]
tnames = forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
tparams
  ([VName]
tparam_names, [Subst (RetTypeBase Size ())]
tparam_substs) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall as dim.
Monoid as =>
QualName VName
-> SrcLoc
-> TypeParam
-> TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam QualName VName
qn SrcLoc
loc) [TypeParam]
tparams
  let substs :: Map VName (Subst (RetTypeBase Size ()))
substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
tnames [Subst (RetTypeBase Size ())]
tparam_substs
      t' :: PatType
t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst (RetTypeBase Size ()))
substs) PatType
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName]
tparam_names, PatType
t')

-- | Create a new type name and insert it (unconstrained) in the
-- substitution map.
instantiateTypeParam ::
  Monoid as =>
  QualName VName ->
  SrcLoc ->
  TypeParam ->
  TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam :: forall as dim.
Monoid as =>
QualName VName
-> SrcLoc
-> TypeParam
-> TermTypeM (VName, Subst (RetTypeBase dim as))
instantiateTypeParam QualName VName
qn SrcLoc
loc TypeParam
tparam = do
  Int
i <- TermTypeM Int
incCounter
  let name :: Name
name = String -> Name
nameFromString (forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii (VName -> String
baseString (forall vn. TypeParamBase vn -> vn
typeParamName TypeParam
tparam)))
  VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
name Int
i
  case TypeParam
tparam of
    TypeParamType Liftedness
x VName
_ SrcLoc
_ -> do
      VName -> Constraint -> TermTypeM ()
constrain VName
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Liftedness -> Usage -> Constraint
NoConstraint Liftedness
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> String -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$
        String
"instantiated type parameter of " forall a. Semigroup a => a -> a -> a
<> ShowS
quote (forall a. Pretty a => a -> String
pretty QualName VName
qn) forall a. Semigroup a => a -> a -> a
<> String
"."
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, forall t. [TypeParam] -> t -> Subst t
Subst [] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) [])
    TypeParamDim {} -> do
      VName -> Constraint -> TermTypeM ()
constrain VName
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> String -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$
        String
"instantiated size parameter of " forall a. Semigroup a => a -> a -> a
<> ShowS
quote (forall a. Pretty a => a -> String
pretty QualName VName
qn) forall a. Semigroup a => a -> a -> a
<> String
"."
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v)

checkQualNameWithEnv :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv :: Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
space qn :: QualName Name
qn@(QualName [Name]
quals Name
name) SrcLoc
loc = do
  TermScope
scope <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TermScope
termScope
  TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend TermScope
scope [Name]
quals
  where
    descend :: TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend TermScope
scope []
      | Just QualName VName
name' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
space, Name
name) forall a b. (a -> b) -> a -> b
$ TermScope -> NameMap
scopeNameMap TermScope
scope =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope, QualName VName
name')
      | Bool
otherwise =
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc
    descend TermScope
scope (Name
q : [Name]
qs)
      | Just (QualName [VName]
_ VName
q') <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
Term, Name
q) forall a b. (a -> b) -> a -> b
$ TermScope -> NameMap
scopeNameMap TermScope
scope,
        Just Mod
res <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
q' forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName Mod
scopeModTable TermScope
scope =
          case Mod
res of
            -- Check if we are referring to the magical intrinsics
            -- module.
            Mod
_
              | VName -> Int
baseTag VName
q' forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag ->
                  Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic Namespace
space QualName Name
qn SrcLoc
loc
            ModEnv Env
q_scope -> do
              (TermScope
scope', QualName [VName]
qs' VName
name') <- TermScope -> [Name] -> TermTypeM (TermScope, QualName VName)
descend (Env -> TermScope
envToTermScope Env
q_scope) [Name]
qs
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope', forall vn. [vn] -> vn -> QualName vn
QualName (VName
q' forall a. a -> [a] -> [a]
: [VName]
qs') VName
name')
            ModFun {} -> forall (m :: * -> *) a. MonadTypeChecker m => SrcLoc -> m a
unappliedFunctor SrcLoc
loc
      | Bool
otherwise =
          forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc

checkIntrinsic :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic :: Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkIntrinsic Namespace
space qn :: QualName Name
qn@(QualName [Name]
_ Name
name) SrcLoc
loc
  | Just QualName VName
v <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
space, Name
name) NameMap
intrinsicsNameMap = do
      ImportName
me <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM ImportName
askImportName
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
isBuiltin (ImportName -> String
includeToFilePath ImportName
me)) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc -> m ()
warn SrcLoc
loc Doc
"Using intrinsic functions directly can easily crash the compiler or result in wrong code generation."
      TermScope
scope <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> TermScope
termScope
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermScope
scope, QualName VName
v)
  | Bool
otherwise =
      forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
space QualName Name
qn SrcLoc
loc

localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope :: forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
f = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
tenv -> TermEnv
tenv {termScope :: TermScope
termScope = TermScope -> TermScope
f forall a b. (a -> b) -> a -> b
$ TermEnv -> TermScope
termScope TermEnv
tenv}

instance MonadTypeChecker TermTypeM where
  warn :: forall loc. Located loc => loc -> Doc -> TermTypeM ()
warn loc
loc Doc
problem = forall a. TypeM a -> TermTypeM a
liftTypeM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc -> m ()
warn loc
loc Doc
problem
  newName :: VName -> TermTypeM VName
newName = forall a. TypeM a -> TermTypeM a
liftTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName
  newID :: Name -> TermTypeM VName
newID = forall a. TypeM a -> TermTypeM a
liftTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID

  newTypeName :: Name -> TermTypeM VName
newTypeName Name
name = do
    Int
i <- TermTypeM Int
incCounter
    forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkTypeVarName Name
name Int
i

  checkQualName :: Namespace -> QualName Name -> SrcLoc -> TermTypeM (QualName VName)
checkQualName Namespace
space QualName Name
name SrcLoc
loc = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
space QualName Name
name SrcLoc
loc

  bindNameMap :: forall a. NameMap -> TermTypeM a -> TermTypeM a
bindNameMap NameMap
m = forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope forall a b. (a -> b) -> a -> b
$ \TermScope
scope ->
    TermScope
scope {scopeNameMap :: NameMap
scopeNameMap = NameMap
m forall a. Semigroup a => a -> a -> a
<> TermScope -> NameMap
scopeNameMap TermScope
scope}

  bindVal :: forall a. VName -> BoundV -> TermTypeM a -> TermTypeM a
bindVal VName
v (TypeM.BoundV [TypeParam]
tps StructType
t) = forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope forall a b. (a -> b) -> a -> b
$ \TermScope
scope ->
    TermScope
scope {scopeVtable :: Map VName ValBinding
scopeVtable = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v ValBinding
vb forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}
    where
      vb :: ValBinding
vb = Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Local [TypeParam]
tps forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
t

  lookupType :: SrcLoc
-> QualName Name
-> TermTypeM
     (QualName VName, [TypeParam], RetTypeBase Size (), Liftedness)
lookupType SrcLoc
loc QualName Name
qn = do
    Env
outer_env <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM Env
askEnv
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
qs VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Type QualName Name
qn SrcLoc
loc
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName TypeBinding
scopeTypeTable TermScope
scope of
      Maybe TypeBinding
Nothing -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m a
unknownType SrcLoc
loc QualName Name
qn
      Just (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims StructType
def)) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( QualName VName
qn',
            [TypeParam]
ps,
            forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ forall as.
Env -> [VName] -> [VName] -> TypeBase Size as -> TypeBase Size as
qualifyTypeVars Env
outer_env (forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps) [VName]
qs StructType
def,
            Liftedness
l
          )

  lookupMod :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
qn = do
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
_ VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Term QualName Name
qn SrcLoc
loc
    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName Mod
scopeModTable TermScope
scope of
      Maybe Mod
Nothing -> forall (m :: * -> *) a.
MonadTypeChecker m =>
Namespace -> QualName Name -> SrcLoc -> m a
unknownVariable Namespace
Term QualName Name
qn SrcLoc
loc
      Just Mod
m -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', Mod
m)

  lookupVar :: SrcLoc -> QualName Name -> TermTypeM (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
qn = do
    Env
outer_env <- forall a. TypeM a -> TermTypeM a
liftTypeM TypeM Env
askEnv
    (TermScope
scope, qn' :: QualName VName
qn'@(QualName [VName]
qs VName
name)) <- Namespace
-> QualName Name -> SrcLoc -> TermTypeM (TermScope, QualName VName)
checkQualNameWithEnv Namespace
Term QualName Name
qn SrcLoc
loc
    let usage :: Usage
usage = SrcLoc -> String -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$ String
"use of " forall a. [a] -> [a] -> [a]
++ ShowS
quote (forall a. Pretty a => a -> String
pretty QualName Name
qn)

    PatType
t <- case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope of
      Maybe ValBinding
Nothing ->
        forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
          Doc
"Unknown variable" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName Name
qn) forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Just (WasConsumed SrcLoc
wloc) -> forall a. VName -> SrcLoc -> SrcLoc -> TermTypeM a
useAfterConsume VName
name SrcLoc
loc SrcLoc
wloc
      Just (BoundV Locality
_ [TypeParam]
tparams PatType
t)
        | String
"_" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` VName -> String
baseString VName
name -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m a
underscoreUse SrcLoc
loc QualName Name
qn
        | Bool
otherwise -> do
            ([VName]
tnames, PatType
t') <- QualName VName
-> SrcLoc -> [TypeParam] -> PatType -> TermTypeM ([VName], PatType)
instantiateTypeScheme QualName VName
qn' SrcLoc
loc [TypeParam]
tparams PatType
t
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall as.
Env -> [VName] -> [VName] -> TypeBase Size as -> TypeBase Size as
qualifyTypeVars Env
outer_env [VName]
tnames [VName]
qs PatType
t'
      Just ValBinding
EqualityF -> do
        StructType
argtype <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
        forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage StructType
argtype
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
          forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed StructType
argtype forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$
            forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
              forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed StructType
argtype forall a b. (a -> b) -> a -> b
$
                forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$
                  forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
                    forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
Bool
      Just (OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt) -> do
        StructType
argtype <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
        forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
ts Usage
usage StructType
argtype
        let ([StructType]
pts', StructType
rt') = forall {dim} {as}.
TypeBase dim as
-> [Maybe PrimType]
-> Maybe PrimType
-> ([TypeBase dim ()], TypeBase dim ())
instOverloaded StructType
argtype [Maybe PrimType]
pts Maybe PrimType
rt
            arrow :: TypeBase dim () -> TypeBase dim as -> TypeBase dim as
arrow TypeBase dim ()
xt TypeBase dim as
yt = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed TypeBase dim ()
xt forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase dim as
yt
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {as} {dim}.
Monoid as =>
TypeBase dim () -> TypeBase dim as -> TypeBase dim as
arrow StructType
rt' [StructType]
pts'

    Ident -> TermTypeM ()
observe forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident VName
name (forall a. a -> Info a
Info PatType
t) SrcLoc
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', PatType
t)
    where
      instOverloaded :: TypeBase dim as
-> [Maybe PrimType]
-> Maybe PrimType
-> ([TypeBase dim ()], TypeBase dim ())
instOverloaded TypeBase dim as
argtype [Maybe PrimType]
pts Maybe PrimType
rt =
        ( forall a b. (a -> b) -> [a] -> [b]
map (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase dim as
argtype) (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim)) [Maybe PrimType]
pts,
          forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase dim as
argtype) (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim) Maybe PrimType
rt
        )

  checkNamedSize :: SrcLoc -> QualName Name -> TermTypeM (QualName VName)
checkNamedSize SrcLoc
loc QualName Name
v = do
    (QualName VName
v', PatType
t) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, PatType)
lookupVar SrcLoc
loc QualName Name
v
    forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([StructType] -> StructType -> Checking
CheckingRequired [forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64] (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t)) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"use as array size") (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) forall a b. (a -> b) -> a -> b
$
        forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
          forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$
            IntType -> PrimType
Signed IntType
Int64
    forall (f :: * -> *) a. Applicative f => a -> f a
pure QualName VName
v'

  typeError :: forall loc a. Located loc => loc -> Notes -> Doc -> TermTypeM a
typeError loc
loc Notes
notes Doc
s = do
    Maybe Checking
checking <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TermEnv -> Maybe Checking
termChecking
    case Maybe Checking
checking of
      Just Checking
checking' ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (forall a. Pretty a => a -> Doc
ppr Checking
checking' forall a. Semigroup a => a -> a -> a
<> Doc
line Doc -> Doc -> Doc
</> Doc
s)
      Maybe Checking
Nothing ->
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes Doc
s

onFailure :: Checking -> TermTypeM a -> TermTypeM a
onFailure :: forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure Checking
c = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
env -> TermEnv
env {termChecking :: Maybe Checking
termChecking = forall a. a -> Maybe a
Just Checking
c}

extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize SrcLoc
loc SizeSource
e = do
  Maybe VName
prev <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup SizeSource
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermTypeState -> Map SizeSource VName
stateDimTable
  case Maybe VName
prev of
    Maybe VName
Nothing -> do
      let rsrc :: RigidSource
rsrc = case SizeSource
e of
            SourceArg (FName Maybe (QualName VName)
fname) ExpBase NoInfo VName
e' ->
              Maybe (QualName VName) -> String -> RigidSource
RigidArg Maybe (QualName VName)
fname forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyOneLine ExpBase NoInfo VName
e'
            SourceBound ExpBase NoInfo VName
e' ->
              String -> RigidSource
RigidBound forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyOneLine ExpBase NoInfo VName
e'
            SourceSlice Maybe Size
d Maybe (ExpBase NoInfo VName)
i Maybe (ExpBase NoInfo VName)
j Maybe (ExpBase NoInfo VName)
s ->
              Maybe Size -> String -> RigidSource
RigidSlice Maybe Size
d forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyOneLine forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> DimIndexBase f vn
DimSlice Maybe (ExpBase NoInfo VName)
i Maybe (ExpBase NoInfo VName)
j Maybe (ExpBase NoInfo VName)
s
      VName
d <- forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc (RigidSource -> Rigidity
Rigid RigidSource
rsrc) Name
"n"
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateDimTable :: Map SizeSource VName
stateDimTable = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert SizeSource
e VName
d forall a b. (a -> b) -> a -> b
$ TermTypeState -> Map SizeSource VName
stateDimTable TermTypeState
s}
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d,
          forall a. a -> Maybe a
Just VName
d
        )
    Just VName
d ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d,
          forall a. a -> Maybe a
Just VName
d
        )

incLevel :: TermTypeM a -> TermTypeM a
incLevel :: forall a. TermTypeM a -> TermTypeM a
incLevel = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \TermEnv
env -> TermEnv
env {termLevel :: Int
termLevel = TermEnv -> Int
termLevel TermEnv
env forall a. Num a => a -> a -> a
+ Int
1}

-- | Get the type of an expression, with top level type variables
-- substituted.  Never call 'typeOf' directly (except in a few
-- carefully inspected locations)!
expType :: Exp -> TermTypeM PatType
expType :: Exp -> TermTypeM PatType
expType = forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> PatType
typeOf

-- | Get the type of an expression, with all type variables
-- substituted.  Slower than 'expType', but sometimes necessary.
-- Never call 'typeOf' directly (except in a few carefully inspected
-- locations)!
expTypeFully :: Exp -> TermTypeM PatType
expTypeFully :: Exp -> TermTypeM PatType
expTypeFully = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> PatType
typeOf

newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType :: SrcLoc -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType SrcLoc
loc Name
desc Int
r = do
  VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
desc
  VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' SrcLoc
loc
  [VName]
dims <- forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
r forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
Nonrigid Name
"dim"
  let rowt :: ScalarTypeBase dim ()
rowt = forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array () Uniqueness
Nonunique (forall dim. [dim] -> Shape dim
Shape forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName) [VName]
dims) forall {dim}. ScalarTypeBase dim ()
rowt,
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall {dim}. ScalarTypeBase dim ()
rowt
    )

-- | Replace *all* dimensions with distinct fresh size variables.
allDimsFreshInType ::
  SrcLoc ->
  Rigidity ->
  Name ->
  TypeBase Size als ->
  TermTypeM (TypeBase Size als, M.Map VName Size)
allDimsFreshInType :: forall als.
SrcLoc
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType SrcLoc
loc Rigidity
r Name
desc TypeBase Size als
t =
  forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadTrans t, MonadUnify m, MonadState (Map VName a) (t m)) =>
a -> t m Size
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase Size als
t) forall a. Monoid a => a
mempty
  where
    onDim :: a -> t m Size
onDim a
d = do
      VName
v <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
desc
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v a
d
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v

-- | Replace all type variables with their concrete types.
updateTypes :: ASTMappable e => e -> TermTypeM e
updateTypes :: forall e. ASTMappable e => e -> TermTypeM e
updateTypes = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper TermTypeM
tv
  where
    tv :: ASTMapper TermTypeM
tv =
      ASTMapper
        { mapOnExp :: Exp -> TermTypeM Exp
mapOnExp = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper TermTypeM
tv,
          mapOnName :: VName -> TermTypeM VName
mapOnName = forall (f :: * -> *) a. Applicative f => a -> f a
pure,
          mapOnStructType :: StructType -> TermTypeM StructType
mapOnStructType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnPatType :: PatType -> TermTypeM PatType
mapOnPatType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnStructRetType :: RetTypeBase Size () -> TermTypeM (RetTypeBase Size ())
mapOnStructRetType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully,
          mapOnPatRetType :: RetTypeBase Size Aliasing -> TermTypeM (RetTypeBase Size Aliasing)
mapOnPatRetType = forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully
        }

--- Basic checking

unifies :: String -> StructType -> Exp -> TermTypeM Exp
unifies :: String -> StructType -> Exp -> TermTypeM Exp
unifies String
why StructType
t Exp
e = do
  forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> String -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) String
why) StructType
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expType Exp
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

-- | @require ts e@ causes a 'TypeError' if @expType e@ is not one of
-- the types in @ts@.  Otherwise, simply returns @e@.
require :: String -> [PrimType] -> Exp -> TermTypeM Exp
require :: String -> [PrimType] -> Exp -> TermTypeM Exp
require String
why [PrimType]
ts Exp
e = do
  forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
ts (SrcLoc -> String -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) String
why) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expType Exp
e
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e

termCheckTypeExp :: TypeExp Name -> TermTypeM (TypeExp VName, [VName], StructRetType)
termCheckTypeExp :: TypeExp Name
-> TermTypeM (TypeExp VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp Name
te = do
  (TypeExp VName
te', [VName]
svars, RetTypeBase Size ()
rettype, Liftedness
_l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checkTypeExp TypeExp Name
te

  -- No guarantee that the locally bound sizes in rettype are globally
  -- unique, but we want to turn them into size variables, so let's
  -- give them some unique names.  Maybe this should be done below,
  -- where we actually turn these into size variables?
  RetType [VName]
dims StructType
st <- forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType RetTypeBase Size ()
rettype

  -- Observe the sizes so we do not get any warnings about them not
  -- being used.
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> TermTypeM ()
observeDim forall a b. (a -> b) -> a -> b
$ forall as. TypeBase Size as -> Set VName
freeInType StructType
st
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp VName
te', [VName]
svars, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims StructType
st)
  where
    observeDim :: VName -> TermTypeM ()
observeDim VName
v =
      Ident -> TermTypeM ()
observe forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f PatType -> SrcLoc -> IdentBase f vn
Ident VName
v (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) forall a. Monoid a => a
mempty

checkTypeExpNonrigid :: TypeExp Name -> TermTypeM (TypeExp VName, StructType, [VName])
checkTypeExpNonrigid :: TypeExp Name -> TermTypeM (TypeExp VName, StructType, [VName])
checkTypeExpNonrigid TypeExp Name
te = do
  (TypeExp VName
te', [VName]
svars, RetType [VName]
dims StructType
st) <- TypeExp Name
-> TermTypeM (TypeExp VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp Name
te
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) forall a b. (a -> b) -> a -> b
$ \VName
v ->
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ SrcLoc -> String -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf TypeExp Name
te) String
"anonymous size in type expression"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp VName
te', StructType
st, [VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims)

checkTypeExpRigid ::
  TypeExp Name ->
  RigidSource ->
  TermTypeM (TypeExp VName, StructType, [VName])
checkTypeExpRigid :: TypeExp Name
-> RigidSource -> TermTypeM (TypeExp VName, StructType, [VName])
checkTypeExpRigid TypeExp Name
te RigidSource
rsrc = do
  (TypeExp VName
te', [VName]
svars, RetType [VName]
dims StructType
st) <- TypeExp Name
-> TermTypeM (TypeExp VName, [VName], RetTypeBase Size ())
termCheckTypeExp TypeExp Name
te
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) forall a b. (a -> b) -> a -> b
$ \VName
v ->
    VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ SrcLoc -> RigidSource -> Constraint
UnknowableSize (forall a. Located a => a -> SrcLoc
srclocOf TypeExp Name
te) RigidSource
rsrc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp VName
te', StructType
st, [VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims)

--- Sizes

isInt64 :: Exp -> Maybe Int64
isInt64 :: Exp -> Maybe Int64
isInt64 (Literal (SignedValue (Int64Value Int64
k')) SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
k'
isInt64 (IntLit Integer
k' Info PatType
_ SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
k'
isInt64 (Negate Exp
x SrcLoc
_) = forall a. Num a => a -> a
negate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Maybe Int64
isInt64 Exp
x
isInt64 Exp
_ = forall a. Maybe a
Nothing

maybeDimFromExp :: Exp -> Maybe Size
maybeDimFromExp :: Exp -> Maybe Size
maybeDimFromExp (Var QualName VName
v Info PatType
_ SrcLoc
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize QualName VName
v
maybeDimFromExp (Parens Exp
e SrcLoc
_) = Exp -> Maybe Size
maybeDimFromExp Exp
e
maybeDimFromExp (QualParens (QualName VName, SrcLoc)
_ Exp
e SrcLoc
_) = Exp -> Maybe Size
maybeDimFromExp Exp
e
maybeDimFromExp Exp
e = Int -> Size
ConstSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Maybe Int64
isInt64 Exp
e

dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp :: (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf (Attr AttrInfo VName
_ Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (Assert Exp
_ Exp
e Info String
_ SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (Parens Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf (QualParens (QualName VName, SrcLoc)
_ Exp
e SrcLoc
_) = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp Exp -> SizeSource
rf Exp
e
dimFromExp Exp -> SizeSource
rf Exp
e
  | Just Size
d <- Exp -> Maybe Size
maybeDimFromExp Exp
e =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size
d, forall a. Maybe a
Nothing)
  | Bool
otherwise =
      SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) forall a b. (a -> b) -> a -> b
$ Exp -> SizeSource
rf Exp
e

sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
sizeFromArg :: Maybe (QualName VName) -> Exp -> TermTypeM (Size, Maybe VName)
sizeFromArg Maybe (QualName VName)
fname = (Exp -> SizeSource) -> Exp -> TermTypeM (Size, Maybe VName)
dimFromExp forall a b. (a -> b) -> a -> b
$ FName -> ExpBase NoInfo VName -> SizeSource
SourceArg (Maybe (QualName VName) -> FName
FName Maybe (QualName VName)
fname) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> ExpBase NoInfo VName
bareExp

-- | Any argument sizes created with 'extSize' inside the given action
-- will be removed once the action finishes.  This is to ensure that
-- just because e.g. @n+1@ appears as a size in one branch of a
-- conditional, that doesn't mean it's also available in the other
-- branch.
noSizeEscape :: TermTypeM a -> TermTypeM a
noSizeEscape :: forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM a
m = do
  Map SizeSource VName
dimtable <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Map SizeSource VName
stateDimTable
  a
x <- TermTypeM a
m
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateDimTable :: Map SizeSource VName
stateDimTable = Map SizeSource VName
dimtable}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

--- Control flow

tapOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences :: forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m
  Occurrences -> TermTypeM ()
occur Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Occurrences
occs)

collectOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences :: forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m = do
  Occurrences
old <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Occurrences
stateOccs
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = forall a. Monoid a => a
mempty}
  a
x <- TermTypeM a
m
  Occurrences
new <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Occurrences
stateOccs
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = Occurrences
old}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Occurrences
new)

alternative :: TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
alternative :: forall a b. TermTypeM a -> TermTypeM b -> TermTypeM (a, b)
alternative TermTypeM a
m1 TermTypeM b
m2 = do
  (a
x, Occurrences
occurs1) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM a
m1
  (b
y, Occurrences
occurs2) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. TermTypeM a -> TermTypeM a
noSizeEscape TermTypeM b
m2
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occurs1
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occurs2
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ Occurrences
occurs1 Occurrences -> Occurrences -> Occurrences
`altOccurrences` Occurrences
occurs2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, b
y)

sequentially :: TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially :: forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially TermTypeM a
m1 a -> Occurrences -> TermTypeM b
m2 = do
  (a
a, Occurrences
m1flow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m1
  (b
b, Occurrences
m2flow) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ a -> Occurrences -> TermTypeM b
m2 a
a Occurrences
m1flow
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ Occurrences
m1flow Occurrences -> Occurrences -> Occurrences
`seqOccurrences` Occurrences
m2flow
  forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b

--- Consumption

occur :: Occurrences -> TermTypeM ()
occur :: Occurrences -> TermTypeM ()
occur Occurrences
occs = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TermTypeState
s -> TermTypeState
s {stateOccs :: Occurrences
stateOccs = TermTypeState -> Occurrences
stateOccs TermTypeState
s forall a. Semigroup a => a -> a -> a
<> Occurrences
occs}

-- | Proclaim that we have made read-only use of the given variable.
observe :: Ident -> TermTypeM ()
observe :: Ident -> TermTypeM ()
observe (Ident VName
nm (Info PatType
t) SrcLoc
loc) =
  let als :: Aliasing
als = VName -> Alias
AliasBound VName
nm forall a. Ord a => a -> Set a -> Set a
`S.insert` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
   in Occurrences -> TermTypeM ()
occur [Aliasing -> SrcLoc -> Occurrence
observation Aliasing
als SrcLoc
loc]

onlySelfAliasing :: TermTypeM a -> TermTypeM a
onlySelfAliasing :: forall a. TermTypeM a -> TermTypeM a
onlySelfAliasing = forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope (\TermScope
scope -> TermScope
scope {scopeVtable :: Map VName ValBinding
scopeVtable = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> ValBinding -> ValBinding
set forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope})
  where
    set :: VName -> ValBinding -> ValBinding
set VName
k (BoundV Locality
l [TypeParam]
tparams PatType
t) =
      Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
l [TypeParam]
tparams forall a b. (a -> b) -> a -> b
$
        PatType
t forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` forall a. Ord a => Set a -> Set a -> Set a
S.intersection (forall a. a -> Set a
S.singleton (VName -> Alias
AliasBound VName
k))
    set VName
_ (OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt) = [PrimType] -> [Maybe PrimType] -> Maybe PrimType -> ValBinding
OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt
    set VName
_ ValBinding
EqualityF = ValBinding
EqualityF
    set VName
_ (WasConsumed SrcLoc
loc) = SrcLoc -> ValBinding
WasConsumed SrcLoc
loc

-- | Enter a context where nothing outside can be consumed (i.e. the
-- body of a function definition).
noUnique :: TermTypeM a -> TermTypeM a
noUnique :: forall a. TermTypeM a -> TermTypeM a
noUnique TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences forall a b. (a -> b) -> a -> b
$ forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
f TermTypeM a
m
  Occurrences -> TermTypeM ()
checkOccurrences Occurrences
occs
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Occurrences -> (Occurrences, Occurrences)
split Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  where
    f :: TermScope -> TermScope
f TermScope
scope = TermScope
scope {scopeVtable :: Map VName ValBinding
scopeVtable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map ValBinding -> ValBinding
set forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}

    set :: ValBinding -> ValBinding
set (BoundV Locality
l [TypeParam]
tparams PatType
t) = Locality -> [TypeParam] -> PatType -> ValBinding
BoundV (forall a. Ord a => a -> a -> a
max Locality
l Locality
Nonlocal) [TypeParam]
tparams PatType
t
    set (OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt) = [PrimType] -> [Maybe PrimType] -> Maybe PrimType -> ValBinding
OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rt
    set ValBinding
EqualityF = ValBinding
EqualityF
    set (WasConsumed SrcLoc
loc) = SrcLoc -> ValBinding
WasConsumed SrcLoc
loc

    split :: Occurrences -> (Occurrences, Occurrences)
split = forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\Occurrence
occ -> (Occurrence
occ {consumed :: Maybe (Set VName)
consumed = forall a. Monoid a => a
mempty}, Occurrence
occ {observed :: Set VName
observed = forall a. Monoid a => a
mempty}))

removeSeminullOccurrences :: TermTypeM a -> TermTypeM a
removeSeminullOccurrences :: forall a. TermTypeM a -> TermTypeM a
removeSeminullOccurrences TermTypeM a
m = do
  (a
x, Occurrences
occs) <- forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m
  Occurrences -> TermTypeM ()
occur forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Bool
seminullOccurrence) Occurrences
occs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable :: SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable SrcLoc
loc Aliasing
als = do
  Map VName ValBinding
vtable <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermEnv -> TermScope
termScope
  let consumable :: VName -> Bool
consumable VName
v = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName ValBinding
vtable of
        Just (BoundV Locality
Local [TypeParam]
_ PatType
t)
          | Scalar Arrow {} <- PatType
t -> Bool
False
          | Bool
otherwise -> Bool
True
        Just (BoundV Locality
l [TypeParam]
_ PatType
_) -> Locality
l forall a. Eq a => a -> a -> Bool
== Locality
Local
        Maybe ValBinding
_ -> Bool
True
  -- The sort ensures that AliasBound vars are shown before AliasFree.
  case forall a b. (a -> b) -> [a] -> [b]
map Alias -> VName
aliasVar forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
sort forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Bool
consumable forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alias -> VName
aliasVar) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Aliasing
als of
    VName
v : [VName]
_ -> forall (m :: * -> *) b. MonadTypeChecker m => SrcLoc -> Doc -> m b
notConsumable SrcLoc
loc forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SrcLoc -> VName -> TermTypeM Doc
describeVar SrcLoc
loc VName
v
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Proclaim that we have written to the given variable.
consume :: SrcLoc -> Aliasing -> TermTypeM ()
consume :: SrcLoc -> Aliasing -> TermTypeM ()
consume SrcLoc
loc Aliasing
als = do
  SrcLoc -> Aliasing -> TermTypeM ()
checkIfConsumable SrcLoc
loc Aliasing
als
  Occurrences -> TermTypeM ()
occur [Aliasing -> SrcLoc -> Occurrence
consumption Aliasing
als SrcLoc
loc]

-- | Proclaim that we have written to the given variable, and mark
-- accesses to it and all of its aliases as invalid inside the given
-- computation.
consuming :: Ident -> TermTypeM a -> TermTypeM a
consuming :: forall a. Ident -> TermTypeM a -> TermTypeM a
consuming (Ident VName
name (Info PatType
t) SrcLoc
loc) TermTypeM a
m = do
  PatType
t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t
  SrcLoc -> Aliasing -> TermTypeM ()
consume SrcLoc
loc forall a b. (a -> b) -> a -> b
$ VName -> Alias
AliasBound VName
name forall a. Ord a => a -> Set a -> Set a
`S.insert` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t'
  forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
consume' TermTypeM a
m
  where
    consume' :: TermScope -> TermScope
consume' TermScope
scope =
      TermScope
scope {scopeVtable :: Map VName ValBinding
scopeVtable = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name (SrcLoc -> ValBinding
WasConsumed SrcLoc
loc) forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope}

-- Running

initialTermScope :: TermScope
initialTermScope :: TermScope
initialTermScope =
  TermScope
    { scopeVtable :: Map VName ValBinding
scopeVtable = Map VName ValBinding
initialVtable,
      scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = forall a. Monoid a => a
mempty,
      scopeNameMap :: NameMap
scopeNameMap = NameMap
topLevelNameMap,
      scopeModTable :: Map VName Mod
scopeModTable = forall a. Monoid a => a
mempty
    }
  where
    initialVtable :: Map VName ValBinding
initialVtable = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. (a, Intrinsic) -> Maybe (a, ValBinding)
addIntrinsicF forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map VName Intrinsic
intrinsics

    prim :: PrimType -> TypeBase dim as
prim = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim
    arrow :: TypeBase dim () -> RetTypeBase dim as -> TypeBase dim as
arrow TypeBase dim ()
x RetTypeBase dim as
y = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed TypeBase dim ()
x RetTypeBase dim as
y

    addIntrinsicF :: (a, Intrinsic) -> Maybe (a, ValBinding)
addIntrinsicF (a
name, IntrinsicMonoFun [PrimType]
pts PrimType
t) =
      forall a. a -> Maybe a
Just (a
name, Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [] forall a b. (a -> b) -> a -> b
$ forall {as} {dim}.
Monoid as =>
TypeBase dim () -> RetTypeBase dim as -> TypeBase dim as
arrow forall {dim} {as}. TypeBase dim as
pts' forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall {dim} {as}. PrimType -> TypeBase dim as
prim PrimType
t)
      where
        pts' :: TypeBase dim as
pts' = case [PrimType]
pts of
          [PrimType
pt] -> forall {dim} {as}. PrimType -> TypeBase dim as
prim PrimType
pt
          [PrimType]
_ -> forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {dim} {as}. PrimType -> TypeBase dim as
prim [PrimType]
pts
    addIntrinsicF (a
name, IntrinsicOverloadedFun [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rts) =
      forall a. a -> Maybe a
Just (a
name, [PrimType] -> [Maybe PrimType] -> Maybe PrimType -> ValBinding
OverloadedF [PrimType]
ts [Maybe PrimType]
pts Maybe PrimType
rts)
    addIntrinsicF (a
name, IntrinsicPolyFun [TypeParam]
tvs [StructType]
pts RetTypeBase Size ()
rt) =
      forall a. a -> Maybe a
Just
        ( a
name,
          Locality -> [TypeParam] -> PatType -> ValBinding
BoundV Locality
Global [TypeParam]
tvs forall a b. (a -> b) -> a -> b
$
            forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct forall a b. (a -> b) -> a -> b
$
              forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
                forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed StructType
pts' RetTypeBase Size ()
rt
        )
      where
        pts' :: StructType
pts' = case [StructType]
pts of
          [StructType
pt] -> StructType
pt
          [StructType]
_ -> forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [StructType]
pts
    addIntrinsicF (a
name, Intrinsic
IntrinsicEquality) =
      forall a. a -> Maybe a
Just (a
name, ValBinding
EqualityF)
    addIntrinsicF (a, Intrinsic)
_ = forall a. Maybe a
Nothing

runTermTypeM :: TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM :: forall a. TermTypeM a -> TypeM (a, Occurrences)
runTermTypeM (TermTypeM ReaderT TermEnv (StateT TermTypeState TypeM) a
m) = do
  TermScope
initial_scope <- (TermScope
initialTermScope forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermScope
envToTermScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeM Env
askEnv
  let initial_tenv :: TermEnv
initial_tenv =
        TermEnv
          { termScope :: TermScope
termScope = TermScope
initial_scope,
            termChecking :: Maybe Checking
termChecking = forall a. Maybe a
Nothing,
            termLevel :: Int
termLevel = Int
0
          }
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second TermTypeState -> Occurrences
stateOccs
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
      (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT TermEnv (StateT TermTypeState TypeM) a
m TermEnv
initial_tenv)
      (Constraints
-> Int
-> Map SizeSource VName
-> Map VName NameReason
-> Occurrences
-> TermTypeState
TermTypeState forall a. Monoid a => a
mempty Int
0 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)