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,
unifies,
require,
checkTypeExpNonrigid,
checkTypeExpRigid,
isInt64,
maybeDimFromExp,
dimFromExp,
sizeFromArg,
noSizeEscape,
collectOccurrences,
tapOccurrences,
alternative,
sequentially,
incLevel,
Names,
Occurrence (..),
Occurrences,
onlySelfAliasing,
noUnique,
removeSeminullOccurrences,
occur,
observe,
consume,
consuming,
observation,
consumption,
checkIfConsumable,
seqOccurrences,
checkOccurrences,
allConsumed,
useAfterConsume,
unusedSize,
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 Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Semantic (includeToFilePath)
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Monad qualified as TypeM
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify hiding (Usage)
import Prelude hiding (mod)
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
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
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)
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
data Locality
=
Local
|
Nonlocal
|
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
=
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)
describeVar :: SrcLoc -> VName -> TermTypeM (Doc a)
describeVar :: forall a. SrcLoc -> VName -> TermTypeM (Doc a)
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 a
"variable" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v)) (forall a. SrcLoc -> NameReason -> Doc a
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' <- forall a. SrcLoc -> VName -> TermTypeM (Doc a)
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
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"use-after-consume" forall a b. (a -> b) -> a -> b
$
Doc ()
"Using"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
name' forall a. Semigroup a => a -> a -> a
<> Doc ()
", but this was consumed at"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (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"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty arr
arre)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"might alias update value"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty src
vale)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Hint: use"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes Doc ()
"copy"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"return-aliased" forall a b. (a -> b) -> a -> b
$
Doc ()
"Unique-typed return value is aliased to"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName 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
. forall ann. Doc ann -> Doc ann -> Doc ann
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
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"not-consumable" forall a b. (a -> b) -> a -> b
$
Doc ()
"Would consume" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unused-size" forall a b. (a -> b) -> a -> b
$
Doc ()
"Size" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SizeBinder VName
p forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"unused in pattern."
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
pretty :: forall ann. Checking -> Doc ann
pretty (CheckingApply Maybe (QualName VName)
f Exp
e StructType
expected StructType
actual) =
forall {ann}. Doc ann
header
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
where
header :: Doc ann
header =
case Maybe (QualName VName)
f of
Maybe (QualName VName)
Nothing ->
Doc ann
"Cannot apply function to"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a b. Doc a -> Doc b
shorten forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
group forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty Exp
e) forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
Just QualName VName
fname ->
Doc ann
"Cannot apply"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
fname)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"to"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a b. Doc a -> Doc b
shorten forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
group forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty Exp
e) forall a. Semigroup a => a -> a -> a
<> Doc ann
" (invalid type)."
pretty (CheckingReturn StructType
expected StructType
actual) =
Doc ann
"Function body does not have expected type."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
pretty (CheckingAscription StructType
expected StructType
actual) =
Doc ann
"Expression does not have expected type from explicit ascription."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
pretty (CheckingLetGeneralise Name
fname) =
Doc ann
"Cannot generalise type of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
fname) forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
pretty (CheckingParams Maybe Name
fname) =
Doc ann
"Invalid use of parameters in" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes forall {ann}. Doc ann
fname' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
where
fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"anonymous function" forall a ann. Pretty a => a -> Doc ann
pretty Maybe Name
fname
pretty (CheckingPat UncheckedPat
pat InferredType
NoneInferred) =
Doc ann
"Invalid pattern" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty UncheckedPat
pat) forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
pretty (CheckingPat UncheckedPat
pat (Ascribed PatType
t)) =
Doc ann
"Pat"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty UncheckedPat
pat)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"cannot match value of type"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty PatType
t)
pretty (CheckingLoopBody StructType
expected StructType
actual) =
Doc ann
"Loop body does not have expected type."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
pretty (CheckingLoopInitial StructType
expected StructType
actual) =
Doc ann
"Initial loop values do not have expected type."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Expected:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
pretty (CheckingRecordUpdate [Name]
fs StructType
expected StructType
actual) =
Doc ann
"Type mismatch when updating record field"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes forall {ann}. Doc ann
fs' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Existing:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"New: "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
where
fs' :: Doc ann
fs' = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
fs
pretty (CheckingRequired [StructType
expected] StructType
actual) =
Doc ann
"Expression must must have type"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
expected forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual type:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
pretty (CheckingRequired [StructType]
expected StructType
actual) =
Doc ann
"Type of expression must must be one of "
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall {ann}. Doc ann
expected' forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Actual type:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
actual)
where
expected' :: Doc a
expected' = forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [StructType]
expected)
pretty (CheckingBranches StructType
t1 StructType
t2) =
Doc ann
"Branches differ in type."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Former:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ann
"Latter:"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2
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
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}
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
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)
data NameReason
=
NameAppRes (Maybe (QualName VName)) SrcLoc
nameReason :: SrcLoc -> NameReason -> Doc a
nameReason :: forall a. SrcLoc -> NameReason -> Doc a
nameReason SrcLoc
loc (NameAppRes Maybe (QualName VName)
Nothing SrcLoc
apploc) =
Doc a
"result of application at" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (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 a
"result of applying"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Maybe (QualName VName)
fname)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (Doc a
"at" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
loc SrcLoc
apploc))
data TermTypeState = TermTypeState
{ TermTypeState -> Constraints
stateConstraints :: Constraints,
TermTypeState -> Int
stateCounter :: !Int,
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 ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty 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 ann. Pretty a => a -> Doc ann
pretty 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 ann. Pretty a => a -> Doc ann
pretty 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 ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> forall {ann}. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty 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
$ forall {ann}. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
where
doc :: Doc a
doc =
Doc a
"Types"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"and"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"do not match."
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')
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 -> Text -> Usage
mkUsage SrcLoc
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$
Doc Any
"instantiated type parameter of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
qn) forall a. Semigroup a => a -> a -> a
<> Doc Any
"."
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 -> Text -> Usage
mkUsage SrcLoc
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$
Doc Any
"instantiated size parameter of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
qn) forall a. Semigroup a => a -> a -> a
<> Doc Any
"."
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
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 -> Text -> Usage
mkUsage SrcLoc
loc forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> Text
docText forall a b. (a -> b) -> a -> b
$ Doc Any
"use of " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
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" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty 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 -> Text -> Usage
mkUsage SrcLoc
loc Text
"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 ann. Pretty a => a -> Doc ann
pretty Checking
checking' forall a. Semigroup a => a -> a -> a
<> forall {ann}. Doc ann
line forall ann. Doc ann -> Doc ann -> Doc ann
</> 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) -> Text -> RigidSource
RigidArg Maybe (QualName VName)
fname forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine ExpBase NoInfo VName
e'
SourceBound ExpBase NoInfo VName
e' ->
Text -> RigidSource
RigidBound forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine 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 -> Text -> RigidSource
RigidSlice Maybe Size
d forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine 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}
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
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
)
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
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
}
unifies :: T.Text -> StructType -> Exp -> TermTypeM Exp
unifies :: Text -> StructType -> Exp -> TermTypeM Exp
unifies Text
why StructType
t Exp
e = do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) Text
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 :: T.Text -> [PrimType] -> Exp -> TermTypeM Exp
require :: Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
why [PrimType]
ts Exp
e = do
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
ts (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
e) Text
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
RetType [VName]
dims StructType
st <- forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType RetTypeBase Size ()
rettype
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 -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf TypeExp Name
te) Text
"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)
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 Text
_ 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
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
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
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}
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
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 boundAlias :: Alias -> Maybe VName
boundAlias (AliasBound VName
v) = forall a. a -> Maybe a
Just VName
v
boundAlias (AliasFree VName
_) = forall a. Maybe a
Nothing
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
False
case 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 a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Alias -> Maybe VName
boundAlias 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
=<< forall a. SrcLoc -> VName -> TermTypeM (Doc a)
describeVar SrcLoc
loc VName
v
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
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]
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}
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 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)