module Language.Futhark.TypeChecker.Terms
( checkOneExp,
checkSizeExp,
checkFunDef,
)
where
import Control.Monad
import Control.Monad.Except
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.Bifunctor
import Data.Bitraversable
import Data.Char (isAscii)
import Data.Either
import Data.List (delete, find, genericLength, partition)
import Data.List.NonEmpty qualified as NE
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Futhark.Util (mapAccumLM, nubOrd, topologicalSort)
import Futhark.Util.Pretty hiding (space)
import Language.Futhark
import Language.Futhark.Primitive (intByteSize)
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Consumption qualified as Consumption
import Language.Futhark.TypeChecker.Match
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Terms.Loop
import Language.Futhark.TypeChecker.Terms.Monad
import Language.Futhark.TypeChecker.Terms.Pat
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify
import Prelude hiding (mod)
hasBinding :: Exp -> Bool
hasBinding :: Size -> Bool
hasBinding Lambda {} = Bool
True
hasBinding (AppExp LetPat {} Info AppRes
_) = Bool
True
hasBinding (AppExp LetFun {} Info AppRes
_) = Bool
True
hasBinding (AppExp Loop {} Info AppRes
_) = Bool
True
hasBinding (AppExp LetWith {} Info AppRes
_) = Bool
True
hasBinding (AppExp Match {} Info AppRes
_) = Bool
True
hasBinding Size
e = forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper Maybe
m Size
e
where
m :: ASTMapper Maybe
m =
forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Size -> Maybe Size
mapOnExp = \Size
e' -> if Size -> Bool
hasBinding Size
e' then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Size
e'}
overloadedTypeVars :: Constraints -> Names
overloadedTypeVars :: Constraints -> Set VName
overloadedTypeVars = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, Constraint) -> Set VName
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems
where
f :: (a, Constraint) -> Set VName
f (a
_, HasFields Liftedness
_ Map Name StructType
fs Usage
_) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall dim as. TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name StructType
fs
f (a, Constraint)
_ = forall a. Monoid a => a
mempty
unifyBranchTypes :: SrcLoc -> StructType -> StructType -> TermTypeM (StructType, [VName])
unifyBranchTypes :: SrcLoc
-> StructType -> StructType -> TermTypeM (StructType, [VName])
unifyBranchTypes SrcLoc
loc StructType
t1 StructType
t2 =
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (StructType -> StructType -> Checking
CheckingBranches StructType
t1 StructType
t2) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m (StructType, [VName])
unifyMostCommon (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"unification of branch results") StructType
t1 StructType
t2
unifyBranches :: SrcLoc -> Exp -> Exp -> TermTypeM (StructType, [VName])
unifyBranches :: SrcLoc -> Size -> Size -> TermTypeM (StructType, [VName])
unifyBranches SrcLoc
loc Size
e1 Size
e2 = do
StructType
e1_t <- Size -> TermTypeM StructType
expTypeFully Size
e1
StructType
e2_t <- Size -> TermTypeM StructType
expTypeFully Size
e2
SrcLoc
-> StructType -> StructType -> TermTypeM (StructType, [VName])
unifyBranchTypes SrcLoc
loc StructType
e1_t StructType
e2_t
sliceShape ::
Maybe (SrcLoc, Rigidity) ->
[DimIndex] ->
TypeBase Size as ->
TermTypeM (TypeBase Size as, [VName])
sliceShape :: forall as.
Maybe (SrcLoc, Rigidity)
-> [DimIndex]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape Maybe (SrcLoc, Rigidity)
r [DimIndex]
slice t :: TypeBase Size as
t@(Array as
u (Shape [Size]
orig_dims) ScalarTypeBase Size NoUniqueness
et) =
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([Size] -> TypeBase Size as
setDims forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
[DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
slice [Size]
orig_dims) []
where
setDims :: [Size] -> TypeBase Size as
setDims [] = forall dim as. Int -> TypeBase dim as -> TypeBase dim as
stripArray (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Size]
orig_dims) TypeBase Size as
t
setDims [Size]
dims' = forall dim u.
u -> Shape dim -> ScalarTypeBase dim NoUniqueness -> TypeBase dim u
Array as
u (forall dim. [dim] -> Shape dim
Shape [Size]
dims') ScalarTypeBase Size NoUniqueness
et
isRigid :: Rigidity -> Bool
isRigid Rigid {} = Bool
True
isRigid Rigidity
_ = Bool
False
refine_sizes :: Bool
refine_sizes = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Rigidity -> Bool
isRigid forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Maybe (SrcLoc, Rigidity)
r
sliceSize :: Size -> Maybe Size -> Maybe Size -> Maybe Size -> t TermTypeM Size
sliceSize Size
orig_d Maybe Size
i Maybe Size
j Maybe Size
stride =
case Maybe (SrcLoc, Rigidity)
r of
Just (SrcLoc
loc, Rigid RigidSource
_) -> do
(Size
d, Maybe VName
ext) <-
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)
extSize SrcLoc
loc forall a b. (a -> b) -> a -> b
$
Maybe Size
-> Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> Maybe (ExpBase NoInfo VName)
-> SizeSource
SourceSlice Maybe Size
orig_d' (Size -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Size
i) (Size -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Size
j) (Size -> ExpBase NoInfo VName
bareExp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Size
stride)
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Maybe a -> [a]
maybeToList Maybe VName
ext ++)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d
Just (SrcLoc
loc, Rigidity
Nonrigid) ->
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> Size
sizeFromName SrcLoc
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => Usage -> Name -> m VName
newFlexibleDim (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"size of slice") Name
"slice_dim"
Maybe (SrcLoc, Rigidity)
Nothing -> 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 :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
"slice_anydim"
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VName
v :)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
v) forall a. Monoid a => a
mempty
where
orig_d' :: Maybe Size
orig_d'
| forall a. Maybe a -> Bool
isJust Maybe Size
i, forall a. Maybe a -> Bool
isJust Maybe Size
j = forall a. Maybe a
Nothing
| Bool
otherwise = forall a. a -> Maybe a
Just Size
orig_d
warnIfBinding :: Bool
-> Size
-> Maybe Size
-> Maybe Size
-> Maybe Size
-> Size
-> t TermTypeM ([Size] -> [Size])
warnIfBinding Bool
binds Size
d Maybe Size
i Maybe Size
j Maybe Size
stride Size
size =
if Bool
binds
then do
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 (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn (forall a. Located a => a -> SrcLoc
srclocOf Size
size) forall a b. (a -> b) -> a -> b
$
forall a. Doc a -> Doc a -> Doc a
withIndexLink
Doc ()
"size-expression-bind"
Doc ()
"Size expression with binding is replaced by unknown size."
(:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Size -> Maybe Size -> Maybe Size -> Maybe Size -> t TermTypeM Size
sliceSize Size
d Maybe Size
i Maybe Size
j Maybe Size
stride
else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size
size :)
adjustDims :: [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims (DimFix {} : [DimIndex]
idxes') (Size
_ : [Size]
dims) =
[DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims (DimSlice Maybe Size
i Maybe Size
j Maybe Size
stride : [DimIndex]
idxes') (Size
d : [Size]
dims)
| Bool
refine_sizes,
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int64
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Maybe Int64
isInt64) Maybe Size
i,
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int64
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Maybe Int64
isInt64) Maybe Size
stride = do
let binds :: Bool
binds = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Size -> Bool
hasBinding Maybe Size
j
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Bool
-> Size
-> Maybe Size
-> Maybe Size
-> Maybe Size
-> Size
-> t TermTypeM ([Size] -> [Size])
warnIfBinding Bool
binds Size
d Maybe Size
i Maybe Size
j Maybe Size
stride (forall a. a -> Maybe a -> a
fromMaybe Size
d Maybe Size
j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims ((DimSlice Maybe Size
i Maybe Size
j Maybe Size
stride) : [DimIndex]
idxes') (Size
d : [Size]
dims)
| Bool
refine_sizes,
Just Size
i' <- Maybe Size
i,
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int64
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Maybe Int64
isInt64) Maybe Size
stride = do
let j' :: Size
j' = forall a. a -> Maybe a -> a
fromMaybe Size
d Maybe Size
j
binds :: Bool
binds = Size -> Bool
hasBinding Size
j' Bool -> Bool -> Bool
|| Size -> Bool
hasBinding Size
i'
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Bool
-> Size
-> Maybe Size
-> Maybe Size
-> Maybe Size
-> Size
-> t TermTypeM ([Size] -> [Size])
warnIfBinding Bool
binds Size
d Maybe Size
i Maybe Size
j Maybe Size
stride (Size -> Size -> Size
sizeMinus Size
j' Size
i')
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims ((DimSlice Maybe Size
Nothing Maybe Size
Nothing Maybe Size
stride) : [DimIndex]
idxes') (Size
d : [Size]
dims)
| Bool
refine_sizes,
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just (-Int64
1)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Maybe Int64
isInt64) Maybe Size
stride =
(Size
d :) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims ((DimSlice (Just Size
i) (Just Size
j) Maybe Size
stride) : [DimIndex]
idxes') (Size
d : [Size]
dims)
| Bool
refine_sizes,
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just (-Int64
1)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> Maybe Int64
isInt64) Maybe Size
stride = do
let binds :: Bool
binds = Size -> Bool
hasBinding Size
i Bool -> Bool -> Bool
|| Size -> Bool
hasBinding Size
j
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Bool
-> Size
-> Maybe Size
-> Maybe Size
-> Maybe Size
-> Size
-> t TermTypeM ([Size] -> [Size])
warnIfBinding Bool
binds Size
d (forall a. a -> Maybe a
Just Size
i) (forall a. a -> Maybe a
Just Size
j) Maybe Size
stride (Size -> Size -> Size
sizeMinus Size
i Size
j)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims ((DimSlice Maybe Size
i Maybe Size
j Maybe Size
stride) : [DimIndex]
idxes') (Size
d : [Size]
dims) =
(:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState [VName] (t TermTypeM)) =>
Size -> Maybe Size -> Maybe Size -> Maybe Size -> t TermTypeM Size
sliceSize Size
d Maybe Size
i Maybe Size
j Maybe Size
stride forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [DimIndex] -> [Size] -> t TermTypeM [Size]
adjustDims [DimIndex]
idxes' [Size]
dims
adjustDims [DimIndex]
_ [Size]
dims =
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Size]
dims
sizeMinus :: Size -> Size -> Size
sizeMinus Size
j Size
i =
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
( forall (f :: * -> *) vn.
(QualName vn, SrcLoc)
-> f StructType
-> (ExpBase f vn, f (Maybe VName))
-> (ExpBase f vn, f (Maybe VName))
-> SrcLoc
-> AppExpBase f vn
BinOp
(forall v. v -> QualName v
qualName (Name -> VName
intrinsicVar Name
"-"), forall a. Monoid a => a
mempty)
Info StructType
sizeBinOpInfo
(Size
j, forall a. a -> Info a
Info forall a. Maybe a
Nothing)
(Size
i, forall a. a -> Info a
Info forall a. Maybe a
Nothing)
forall a. Monoid a => a
mempty
)
forall a b. (a -> b) -> a -> b
$ forall a. a -> Info a
Info
forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes forall {dim} {u}. TypeBase dim u
i64 []
i64 :: TypeBase dim u
i64 = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64
sizeBinOpInfo :: Info StructType
sizeBinOpInfo = forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ [ParamType] -> ResRetType -> StructType
foldFunType [forall {dim} {u}. TypeBase dim u
i64, forall {dim} {u}. TypeBase dim u
i64] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall {dim} {u}. TypeBase dim u
i64
sliceShape Maybe (SrcLoc, Rigidity)
_ [DimIndex]
_ TypeBase Size as
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size as
t, [])
checkAscript ::
SrcLoc ->
UncheckedTypeExp ->
UncheckedExp ->
TermTypeM (TypeExp Info VName, Exp)
checkAscript :: SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp Info VName, Size)
checkAscript SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e = do
(TypeExp Info VName
te', TypeBase Size Uniqueness
decl_t, [VName]
_) <- UncheckedTypeExp
-> TermTypeM
(TypeExp Info VName, TypeBase Size Uniqueness, [VName])
checkTypeExpNonrigid UncheckedTypeExp
te
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
e_t <- Size -> TermTypeM StructType
expTypeFully Size
e'
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (StructType -> StructType -> Checking
CheckingAscription (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
decl_t) StructType
e_t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"type ascription") (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
decl_t) StructType
e_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp Info VName
te', Size
e')
checkCoerce ::
SrcLoc ->
UncheckedTypeExp ->
UncheckedExp ->
TermTypeM (TypeExp Info VName, StructType, Exp)
checkCoerce :: SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp Info VName, StructType, Size)
checkCoerce SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e = do
(TypeExp Info VName
te', TypeBase Size Uniqueness
te_t, [VName]
ext) <- UncheckedTypeExp
-> TermTypeM
(TypeExp Info VName, TypeBase Size Uniqueness, [VName])
checkTypeExpNonrigid UncheckedTypeExp
te
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
e_t <- Size -> TermTypeM StructType
expTypeFully Size
e'
StructType
te_t_nonrigid <- forall {t :: * -> * -> *} {t :: * -> *} {d}.
(Bitraversable t, Foldable t) =>
t VName -> t Size d -> TermTypeM (t Size d)
makeNonExtFresh [VName]
ext forall a b. (a -> b) -> a -> b
$ forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
te_t
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (StructType -> StructType -> Checking
CheckingAscription (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
te_t) StructType
e_t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"size coercion") StructType
e_t StructType
te_t_nonrigid
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeExp Info VName
te', forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
te_t, Size
e')
where
makeNonExtFresh :: t VName -> t Size d -> TermTypeM (t Size d)
makeNonExtFresh t VName
ext = 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 Size -> TermTypeM Size
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure
where
onDim :: Size -> TermTypeM Size
onDim d :: Size
d@(Var QualName VName
v Info StructType
_ SrcLoc
_)
| forall vn. QualName vn -> vn
qualLeaf QualName VName
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
ext = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d
onDim Size
d = do
VName
v <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
"coerce"
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 a b. (a -> b) -> a -> b
$
forall a. Located a => a -> Text -> Usage
mkUsage
SrcLoc
loc
Text
"a size coercion where the underlying expression size cannot be determined"
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
v) (forall a. Located a => a -> SrcLoc
srclocOf Size
d)
sameExp :: Exp -> Exp -> Bool
sameExp :: Size -> Size -> Bool
sameExp Size
e1 Size
e2
| Just [(Size, Size)]
es <- Size -> Size -> Maybe [(Size, Size)]
similarExps Size
e1 Size
e2 =
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Size -> Size -> Bool
sameExp) [(Size, Size)]
es
| Bool
otherwise = Bool
False
subExps :: Exp -> [Exp]
subExps :: Size -> [Size]
subExps Size
e
| Just Size
e' <- Size -> Maybe Size
stripExp Size
e = Size -> [Size]
subExps Size
e'
| Bool
otherwise = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper (StateT [Size] Identity)
mapper Size
e forall s a. State s a -> s -> s
`execState` forall a. Monoid a => a
mempty
where
mapOnExp :: Size -> StateT [Size] Identity Size
mapOnExp Size
e'
| Just Size
e'' <- Size -> Maybe Size
stripExp Size
e' = Size -> StateT [Size] Identity Size
mapOnExp Size
e''
| Bool
otherwise = do
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Size
e' :)
forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper (StateT [Size] Identity)
mapper Size
e'
mapper :: ASTMapper (StateT [Size] Identity)
mapper = forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {Size -> StateT [Size] Identity Size
mapOnExp :: Size -> StateT [Size] Identity Size
mapOnExp :: Size -> StateT [Size] Identity Size
mapOnExp}
topWit :: TypeBase Exp u -> [Exp]
topWit :: forall u. TypeBase Size u -> [Size]
topWit = forall a. (a -> a -> Bool) -> [a] -> [a]
topologicalSort Size -> Size -> Bool
depends forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {fdim} {als}. TypeBase fdim als -> [fdim]
witnessedExps
where
witnessedExps :: TypeBase fdim als -> [fdim]
witnessedExps TypeBase fdim als
t = forall s a. State s a -> s -> s
execState (forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims forall {a} {m :: * -> *} {p}.
MonadState [a] m =>
p -> DimPos -> a -> m ()
onDim TypeBase fdim als
t) forall a. Monoid a => a
mempty
where
onDim :: p -> DimPos -> a -> m ()
onDim p
_ DimPos
PosImmediate a
e = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (a
e :)
onDim p
_ DimPos
_ a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
depends :: Size -> Size -> Bool
depends Size
a Size
b = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Size -> Size -> Bool
sameExp Size
b) forall a b. (a -> b) -> a -> b
$ Size -> [Size]
subExps Size
a
sizeFree ::
SrcLoc ->
(Exp -> Maybe VName) ->
TypeBase Size u ->
TermTypeM (TypeBase Size u, [VName])
sizeFree :: forall u.
SrcLoc
-> (Size -> Maybe VName)
-> TypeBase Size u
-> TermTypeM (TypeBase Size u, [VName])
sizeFree SrcLoc
tloc Size -> Maybe VName
expKiller TypeBase Size u
orig_t = do
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
{m :: * -> *} {u} {b}.
(MonadReader [(Size, Size)] (t (t m)),
MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
MonadTrans t, Monad (t m)) =>
TypeBase Size u -> t (t m) b -> t (t m) b
toBeReplaced TypeBase Size u
orig_t forall a b. (a -> b) -> a -> b
$ forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType TypeBase Size u
orig_t) forall a. Monoid a => a
mempty forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` forall a. Monoid a => a
mempty
where
lookReplacement :: Size -> t (Size, b) -> Maybe b
lookReplacement Size
e t (Size, b)
repl = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Size -> Size -> Bool
sameExp Size
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) t (Size, b)
repl
expReplace :: t (Size, Size) -> Size -> Size
expReplace t (Size, Size)
mapping Size
e
| Just Size
e' <- forall {t :: * -> *} {b}.
Foldable t =>
Size -> t (Size, b) -> Maybe b
lookReplacement Size
e t (Size, Size)
mapping = Size
e'
| Bool
otherwise = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper Identity
mapper Size
e
where
mapper :: ASTMapper Identity
mapper = forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Size -> Identity Size
mapOnExp = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (Size, Size) -> Size -> Size
expReplace t (Size, Size)
mapping}
replacing :: Size -> t (t m) Size
replacing Size
e = do
Size
e' <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall {t :: * -> *}. Foldable t => t (Size, Size) -> Size -> Size
`expReplace` Size
e)
case Size -> Maybe VName
expKiller Size
e' of
Maybe VName
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e'
Just VName
cause -> do
VName
vn <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
tloc (SrcLoc -> VName -> RigidSource
RigidOutOfScope (forall a. Located a => a -> SrcLoc
srclocOf Size
e) VName
cause) Name
"d"
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (VName
vn :)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
vn) (forall a. Located a => a -> SrcLoc
srclocOf Size
e)
toBeReplaced :: TypeBase Size u -> t (t m) b -> t (t m) b
toBeReplaced TypeBase Size u
t t (t m) b
m' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
{m :: * -> *} {b}.
(MonadReader [(Size, Size)] (t (t m)),
MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
MonadTrans t, Monad (t m)) =>
t (t m) b -> Size -> t (t m) b
f t (t m) b
m' forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> [Size]
topWit TypeBase Size u
t
where
f :: t (t m) b -> Size -> t (t m) b
f t (t m) b
m Size
e = do
Size
e' <- forall {t :: * -> *} {t :: (* -> *) -> * -> *}
{t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadReader (t (Size, Size)) (t (t m)), Foldable t, MonadTrans t,
MonadTrans t, Monad (t m), MonadUnify m,
MonadState [VName] (t (t m))) =>
Size -> t (t m) Size
replacing Size
e
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Size
e, Size
e') :) t (t m) b
m
onScalar :: ScalarTypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (ScalarTypeBase Size u)
onScalar (Record Map Name (TypeBase Size u)
fs) =
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType Map Name (TypeBase Size u)
fs
onScalar (Sum Map Name [TypeBase Size u]
cs) =
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType Map Name [TypeBase Size u]
cs
onScalar (Arrow u
as PName
pn Diet
d StructType
argT (RetType [VName]
dims TypeBase Size Uniqueness
retT)) = do
StructType
argT' <- forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType StructType
argT
[VName]
old_bound <- forall s (m :: * -> *). MonadState s m => m s
get
TypeBase Size Uniqueness
retT' <- forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
{m :: * -> *} {u} {b}.
(MonadReader [(Size, Size)] (t (t m)),
MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
MonadTrans t, Monad (t m)) =>
TypeBase Size u -> t (t m) b -> t (t m) b
toBeReplaced TypeBase Size Uniqueness
retT forall a b. (a -> b) -> a -> b
$ forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType TypeBase Size Uniqueness
retT
[VName]
rl <- forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
old_bound)
let dims' :: [VName]
dims' = [VName]
dims forall a. Semigroup a => a -> a -> a
<> [VName]
rl
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow u
as PName
pn Diet
d StructType
argT' (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims' TypeBase Size Uniqueness
retT')
onScalar (TypeVar u
u QualName VName
v [TypeArg Size]
args) =
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar u
u QualName VName
v 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 TypeArg Size
-> ReaderT [(Size, Size)] (StateT [VName] TermTypeM) (TypeArg Size)
onTypeArg [TypeArg Size]
args
where
onTypeArg :: TypeArg Size
-> ReaderT [(Size, Size)] (StateT [VName] TermTypeM) (TypeArg Size)
onTypeArg (TypeArgDim Size
d) = forall dim. dim -> TypeArg dim
TypeArgDim forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: * -> *} {t :: (* -> *) -> * -> *}
{t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadReader (t (Size, Size)) (t (t m)), Foldable t, MonadTrans t,
MonadTrans t, Monad (t m), MonadUnify m,
MonadState [VName] (t (t m))) =>
Size -> t (t m) Size
replacing Size
d
onTypeArg (TypeArgType StructType
ty) = forall dim. TypeBase dim NoUniqueness -> TypeArg dim
TypeArgType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType StructType
ty
onScalar (Prim PrimType
pt) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
pt
onType ::
TypeBase Size u ->
ReaderT [(Exp, Exp)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType :: forall u.
TypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (TypeBase Size u)
onType (Array u
u Shape Size
shape ScalarTypeBase Size NoUniqueness
scalar) =
forall dim u.
u -> Shape dim -> ScalarTypeBase dim NoUniqueness -> TypeBase dim u
Array u
u forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {t :: * -> *} {t :: (* -> *) -> * -> *}
{t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadReader (t (Size, Size)) (t (t m)), Foldable t, MonadTrans t,
MonadTrans t, Monad (t m), MonadUnify m,
MonadState [VName] (t (t m))) =>
Size -> t (t m) Size
replacing Shape Size
shape forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {u}.
ScalarTypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (ScalarTypeBase Size u)
onScalar ScalarTypeBase Size NoUniqueness
scalar
onType (Scalar ScalarTypeBase Size u
ty) =
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {u}.
ScalarTypeBase Size u
-> ReaderT
[(Size, Size)] (StateT [VName] TermTypeM) (ScalarTypeBase Size u)
onScalar ScalarTypeBase Size u
ty
unscopeUnknown ::
TypeBase Size u ->
TermTypeM (TypeBase Size u)
unscopeUnknown :: forall u. TypeBase Size u -> TermTypeM (TypeBase Size u)
unscopeUnknown TypeBase Size u
t = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u.
SrcLoc
-> (Size -> Maybe VName)
-> TypeBase Size u
-> TermTypeM (TypeBase Size u, [VName])
sizeFree forall a. Monoid a => a
mempty (forall {a}. Map VName (a, Constraint) -> Size -> Maybe VName
expKiller Constraints
constraints) TypeBase Size u
t
where
expKiller :: Map VName (a, Constraint) -> Size -> Maybe VName
expKiller Map VName (a, Constraint)
_ Var {} = forall a. Maybe a
Nothing
expKiller Map VName (a, Constraint)
constraints Size
e =
forall a. Set a -> Maybe a
S.lookupMin forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
S.filter (forall {k} {a}. Ord k => Map k (a, Constraint) -> k -> Bool
isUnknown Map VName (a, Constraint)
constraints) forall a b. (a -> b) -> a -> b
$ (forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
witnesses) forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ Size -> FV
freeInExp Size
e
isUnknown :: Map k (a, Constraint) -> k -> Bool
isUnknown Map k (a, Constraint)
constraints k
vn
| Just UnknownSize {} <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
vn Map k (a, Constraint)
constraints = Bool
True
isUnknown Map k (a, Constraint)
_ k
_ = Bool
False
(Set VName
witnesses, Set VName
_) = StructType -> (Set VName, Set VName)
determineSizeWitnesses forall a b. (a -> b) -> a -> b
$ forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size u
t
unscopeType ::
SrcLoc ->
[VName] ->
TypeBase Size as ->
TermTypeM (TypeBase Size as, [VName])
unscopeType :: forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
tloc [VName]
unscoped =
forall u.
SrcLoc
-> (Size -> Maybe VName)
-> TypeBase Size u
-> TermTypeM (TypeBase Size u, [VName])
sizeFree SrcLoc
tloc forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
unscoped) forall b c a. (b -> c) -> (a -> b) -> a -> c
. FV -> Set VName
fvVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> FV
freeInExp
checkExp :: UncheckedExp -> TermTypeM Exp
checkExp :: ExpBase NoInfo Name -> TermTypeM Size
checkExp (Literal PrimValue
val SrcLoc
loc) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. PrimValue -> SrcLoc -> ExpBase f vn
Literal PrimValue
val SrcLoc
loc
checkExp (Hole NoInfo StructType
_ SrcLoc
loc) = do
StructType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. f StructType -> SrcLoc -> ExpBase f vn
Hole (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (StringLit [Word8]
vs SrcLoc
loc) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. [Word8] -> SrcLoc -> ExpBase f vn
StringLit [Word8]
vs SrcLoc
loc
checkExp (IntLit Integer
val NoInfo StructType
NoInfo SrcLoc
loc) = do
StructType
t <- 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]
anyNumberType (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"integer literal") StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Integer -> f StructType -> SrcLoc -> ExpBase f vn
IntLit Integer
val (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (FloatLit Double
val NoInfo StructType
NoInfo SrcLoc
loc) = do
StructType
t <- 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]
anyFloatType (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"float literal") StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Double -> f StructType -> SrcLoc -> ExpBase f vn
FloatLit Double
val (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (TupLit [ExpBase NoInfo Name]
es SrcLoc
loc) =
forall (f :: * -> *) vn. [ExpBase f vn] -> SrcLoc -> ExpBase f vn
TupLit 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 ExpBase NoInfo Name -> TermTypeM Size
checkExp [ExpBase NoInfo Name]
es forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkExp (RecordLit [FieldBase NoInfo Name]
fs SrcLoc
loc) = do
[FieldBase Info VName]
fs' <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t :: (* -> *) -> * -> *}.
(MonadState (Map Name SrcLoc) (t TermTypeM), MonadTrans t) =>
FieldBase NoInfo Name -> t TermTypeM (FieldBase Info VName)
checkField [FieldBase NoInfo Name]
fs) forall a. Monoid a => a
mempty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. [FieldBase f vn] -> SrcLoc -> ExpBase f vn
RecordLit [FieldBase Info VName]
fs' SrcLoc
loc
where
checkField :: FieldBase NoInfo Name -> t TermTypeM (FieldBase Info VName)
checkField (RecordFieldExplicit Name
f ExpBase NoInfo Name
e SrcLoc
rloc) = do
forall {a} {b} {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadState (Map a b) (t m), Ord a, MonadTrans t,
MonadTypeChecker m, Pretty a, Located a, Located b) =>
a -> a -> t m ()
errIfAlreadySet Name
f SrcLoc
rloc
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 Name
f SrcLoc
rloc
forall (f :: * -> *) vn.
Name -> ExpBase f vn -> SrcLoc -> FieldBase f vn
RecordFieldExplicit Name
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
rloc
checkField (RecordFieldImplicit Name
name NoInfo StructType
NoInfo SrcLoc
rloc) = do
forall {a} {b} {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadState (Map a b) (t m), Ord a, MonadTrans t,
MonadTypeChecker m, Pretty a, Located a, Located b) =>
a -> a -> t m ()
errIfAlreadySet Name
name SrcLoc
rloc
(QualName [VName]
_ VName
name', StructType
t) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
rloc forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName Name
name
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 Name
name SrcLoc
rloc
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
vn -> f StructType -> SrcLoc -> FieldBase f vn
RecordFieldImplicit VName
name' (forall a. a -> Info a
Info StructType
t) SrcLoc
rloc
errIfAlreadySet :: a -> a -> t m ()
errIfAlreadySet a
f a
rloc = do
Maybe b
maybe_sloc <- 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 a
f
case Maybe b
maybe_sloc of
Just b
sloc ->
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 (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError a
rloc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Field"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty a
f)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"previously defined at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel a
rloc b
sloc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Maybe b
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExp (ArrayLit [ExpBase NoInfo Name]
all_es NoInfo StructType
_ SrcLoc
loc) =
case [ExpBase NoInfo Name]
all_es of
[] -> do
StructType
et <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
StructType
t <- SrcLoc -> StructType -> Shape Size -> TermTypeM StructType
arrayOfM SrcLoc
loc StructType
et (forall dim. [dim] -> Shape dim
Shape [Integer -> SrcLoc -> Size
sizeFromInteger Integer
0 forall a. Monoid a => a
mempty])
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[ExpBase f vn] -> f StructType -> SrcLoc -> ExpBase f vn
ArrayLit [] (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
ExpBase NoInfo Name
e : [ExpBase NoInfo Name]
es -> do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
et <- Size -> TermTypeM StructType
expType Size
e'
[Size]
es' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Text -> StructType -> Size -> TermTypeM Size
unifies Text
"type of first array element" StructType
et forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExpBase NoInfo Name -> TermTypeM Size
checkExp) [ExpBase NoInfo Name]
es
StructType
et' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
et
StructType
t <- SrcLoc -> StructType -> Shape Size -> TermTypeM StructType
arrayOfM SrcLoc
loc StructType
et' (forall dim. [dim] -> Shape dim
Shape [Integer -> SrcLoc -> Size
sizeFromInteger (forall i a. Num i => [a] -> i
genericLength [ExpBase NoInfo Name]
all_es) forall a. Monoid a => a
mempty])
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[ExpBase f vn] -> f StructType -> SrcLoc -> ExpBase f vn
ArrayLit (Size
e' forall a. a -> [a] -> [a]
: [Size]
es') (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (AppExp (Range ExpBase NoInfo Name
start Maybe (ExpBase NoInfo Name)
maybe_step Inclusiveness (ExpBase NoInfo Name)
end SrcLoc
loc) NoInfo AppRes
_) = do
Size
start' <- Text -> [PrimType] -> Size -> TermTypeM Size
require Text
"use in range expression" [PrimType]
anySignedType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
start
StructType
start_t <- Size -> TermTypeM StructType
expTypeFully Size
start'
Maybe Size
maybe_step' <- case Maybe (ExpBase NoInfo Name)
maybe_step of
Maybe (ExpBase NoInfo Name)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
Just ExpBase NoInfo Name
step -> do
let warning :: TermTypeM ()
warning = forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc Doc ()
"First and second element of range are identical, this will produce an empty array."
case (ExpBase NoInfo Name
start, ExpBase NoInfo Name
step) of
(Literal PrimValue
x SrcLoc
_, Literal PrimValue
y SrcLoc
_) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrimValue
x forall a. Eq a => a -> a -> Bool
== PrimValue
y) TermTypeM ()
warning
(Var QualName Name
x_name NoInfo StructType
_ SrcLoc
_, Var QualName Name
y_name NoInfo StructType
_ SrcLoc
_) -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (QualName Name
x_name forall a. Eq a => a -> a -> Bool
== QualName Name
y_name) TermTypeM ()
warning
(ExpBase NoInfo Name, ExpBase NoInfo Name)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> StructType -> Size -> TermTypeM Size
unifies Text
"use in range expression" StructType
start_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
step)
let unifyRange :: ExpBase NoInfo Name -> TermTypeM Size
unifyRange ExpBase NoInfo Name
e = Text -> StructType -> Size -> TermTypeM Size
unifies Text
"use in range expression" StructType
start_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
Inclusiveness Size
end' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ExpBase NoInfo Name -> TermTypeM Size
unifyRange Inclusiveness (ExpBase NoInfo Name)
end
StructType
end_t <- case Inclusiveness Size
end' of
DownToExclusive Size
e -> Size -> TermTypeM StructType
expType Size
e
ToInclusive Size
e -> Size -> TermTypeM StructType
expType Size
e
UpToExclusive Size
e -> Size -> TermTypeM StructType
expType Size
e
let warnIfBinding :: Bool -> Size -> m (Size, Maybe VName)
warnIfBinding Bool
binds Size
size =
if Bool
binds
then do
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn (forall a. Located a => a -> SrcLoc
srclocOf Size
size) forall a b. (a -> b) -> a -> b
$
forall a. Doc a -> Doc a -> Doc a
withIndexLink
Doc ()
"size-expression-bind"
Doc ()
"Size expression with binding is replaced by unknown size."
VName
d <- forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
loc RigidSource
RigidRange Name
"range_dim"
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
d) forall a. Monoid a => a
mempty, forall a. a -> Maybe a
Just VName
d)
else forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size
size, forall a. Maybe a
Nothing)
(Size
dim, Maybe VName
retext) <-
case (Size -> Maybe Int64
isInt64 Size
start', Size -> Maybe Int64
isInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Size
maybe_step', Inclusiveness Size
end') of
(Just Int64
0, Just (Just Int64
1), UpToExclusive Size
end'')
| Scalar (Prim (Signed IntType
Int64)) <- StructType
end_t ->
forall {m :: * -> *}.
(MonadTypeChecker m, MonadUnify m) =>
Bool -> Size -> m (Size, Maybe VName)
warnIfBinding (Size -> Bool
hasBinding Size
end'') Size
end''
(Just Int64
0, Maybe (Maybe Int64)
Nothing, UpToExclusive Size
end'')
| Scalar (Prim (Signed IntType
Int64)) <- StructType
end_t ->
forall {m :: * -> *}.
(MonadTypeChecker m, MonadUnify m) =>
Bool -> Size -> m (Size, Maybe VName)
warnIfBinding (Size -> Bool
hasBinding Size
end'') Size
end''
(Maybe Int64
_, Maybe (Maybe Int64)
Nothing, UpToExclusive Size
end'')
| Scalar (Prim (Signed IntType
Int64)) <- StructType
end_t ->
forall {m :: * -> *}.
(MonadTypeChecker m, MonadUnify m) =>
Bool -> Size -> m (Size, Maybe VName)
warnIfBinding (Size -> Bool
hasBinding Size
end'' Bool -> Bool -> Bool
|| Size -> Bool
hasBinding Size
start') forall a b. (a -> b) -> a -> b
$ Size -> Size -> Size
sizeMinus Size
end'' Size
start'
(Maybe Int64
_, Maybe (Maybe Int64)
Nothing, ToInclusive Size
end'')
| Scalar (Prim (Signed IntType
Int64)) <- StructType
end_t ->
forall {m :: * -> *}.
(MonadTypeChecker m, MonadUnify m) =>
Bool -> Size -> m (Size, Maybe VName)
warnIfBinding (Size -> Bool
hasBinding Size
end'' Bool -> Bool -> Bool
|| Size -> Bool
hasBinding Size
start') forall a b. (a -> b) -> a -> b
$ Size -> Size -> Size
sizeMinusInc Size
end'' Size
start'
(Just Int64
1, Just (Just Int64
2), ToInclusive Size
end'')
| Scalar (Prim (Signed IntType
Int64)) <- StructType
end_t ->
forall {m :: * -> *}.
(MonadTypeChecker m, MonadUnify m) =>
Bool -> Size -> m (Size, Maybe VName)
warnIfBinding (Size -> Bool
hasBinding Size
end'') Size
end''
(Maybe Int64, Maybe (Maybe Int64), Inclusiveness Size)
_ -> do
VName
d <- forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
loc RigidSource
RigidRange Name
"range_dim"
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
d) forall a. Monoid a => a
mempty, forall a. a -> Maybe a
Just VName
d)
StructType
t <- SrcLoc -> StructType -> Shape Size -> TermTypeM StructType
arrayOfM SrcLoc
loc StructType
start_t (forall dim. [dim] -> Shape dim
Shape [Size
dim])
let res :: AppRes
res = StructType -> [VName] -> AppRes
AppRes StructType
t (forall a. Maybe a -> [a]
maybeToList Maybe VName
retext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> Maybe (ExpBase f vn)
-> Inclusiveness (ExpBase f vn)
-> SrcLoc
-> AppExpBase f vn
Range Size
start' Maybe Size
maybe_step' Inclusiveness Size
end' SrcLoc
loc) (forall a. a -> Info a
Info AppRes
res)
where
i64 :: TypeBase dim u
i64 = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64
mkBinOp :: Name -> StructType -> Size -> Size -> Size
mkBinOp Name
op StructType
t Size
x Size
y =
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
( forall (f :: * -> *) vn.
(QualName vn, SrcLoc)
-> f StructType
-> (ExpBase f vn, f (Maybe VName))
-> (ExpBase f vn, f (Maybe VName))
-> SrcLoc
-> AppExpBase f vn
BinOp
(forall v. v -> QualName v
qualName (Name -> VName
intrinsicVar Name
op), forall a. Monoid a => a
mempty)
Info StructType
sizeBinOpInfo
(Size
x, forall a. a -> Info a
Info forall a. Maybe a
Nothing)
(Size
y, forall a. a -> Info a
Info forall a. Maybe a
Nothing)
forall a. Monoid a => a
mempty
)
(forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
t [])
mkSub :: Size -> Size -> Size
mkSub = Name -> StructType -> Size -> Size -> Size
mkBinOp Name
"-" forall {dim} {u}. TypeBase dim u
i64
mkAdd :: Size -> Size -> Size
mkAdd = Name -> StructType -> Size -> Size -> Size
mkBinOp Name
"+" forall {dim} {u}. TypeBase dim u
i64
sizeMinus :: Size -> Size -> Size
sizeMinus Size
j Size
i = Size
j Size -> Size -> Size
`mkSub` Size
i
sizeMinusInc :: Size -> Size -> Size
sizeMinusInc Size
j Size
i = (Size
j Size -> Size -> Size
`mkSub` Size
i) Size -> Size -> Size
`mkAdd` Integer -> SrcLoc -> Size
sizeFromInteger Integer
1 forall a. Monoid a => a
mempty
sizeBinOpInfo :: Info StructType
sizeBinOpInfo = forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ [ParamType] -> ResRetType -> StructType
foldFunType [forall {dim} {u}. TypeBase dim u
i64, forall {dim} {u}. TypeBase dim u
i64] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall {dim} {u}. TypeBase dim u
i64
checkExp (Ascript ExpBase NoInfo Name
e UncheckedTypeExp
te SrcLoc
loc) = do
(TypeExp Info VName
te', Size
e') <- SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp Info VName, Size)
checkAscript SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn -> TypeExp f vn -> SrcLoc -> ExpBase f vn
Ascript Size
e' TypeExp Info VName
te' SrcLoc
loc
checkExp (Coerce ExpBase NoInfo Name
e UncheckedTypeExp
te NoInfo StructType
NoInfo SrcLoc
loc) = do
(TypeExp Info VName
te', StructType
te_t, Size
e') <- SrcLoc
-> UncheckedTypeExp
-> ExpBase NoInfo Name
-> TermTypeM (TypeExp Info VName, StructType, Size)
checkCoerce SrcLoc
loc UncheckedTypeExp
te ExpBase NoInfo Name
e
StructType
t <- Size -> TermTypeM StructType
expTypeFully Size
e'
StructType
t' <- forall as (m :: * -> *) d1 d2.
(Monoid as, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
matchDims (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall (f :: * -> *) a. Applicative f => a -> f a
pure) StructType
t StructType
te_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn
-> TypeExp f vn -> f StructType -> SrcLoc -> ExpBase f vn
Coerce Size
e' TypeExp Info VName
te' (forall a. a -> Info a
Info StructType
t') SrcLoc
loc
checkExp (AppExp (BinOp (QualName Name
op, SrcLoc
oploc) NoInfo StructType
NoInfo (ExpBase NoInfo Name
e1, NoInfo (Maybe VName)
_) (ExpBase NoInfo Name
e2, NoInfo (Maybe VName)
_) SrcLoc
loc) NoInfo AppRes
NoInfo) = do
(QualName VName
op', StructType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
oploc QualName Name
op
Size
e1' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e1
Size
e2' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e2
(Diet
_, StructType
_, StructType
rt, Maybe VName
p1_ext, [VName]
_) <- SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
0) StructType
ftype Size
e1'
(Diet
_, StructType
_, StructType
rt', Maybe VName
p2_ext, [VName]
retext) <- SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
1) StructType
rt Size
e2'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
( forall (f :: * -> *) vn.
(QualName vn, SrcLoc)
-> f StructType
-> (ExpBase f vn, f (Maybe VName))
-> (ExpBase f vn, f (Maybe VName))
-> SrcLoc
-> AppExpBase f vn
BinOp
(QualName VName
op', SrcLoc
oploc)
(forall a. a -> Info a
Info StructType
ftype)
(Size
e1', forall a. a -> Info a
Info Maybe VName
p1_ext)
(Size
e2', forall a. a -> Info a
Info Maybe VName
p2_ext)
SrcLoc
loc
)
(forall a. a -> Info a
Info (StructType -> [VName] -> AppRes
AppRes StructType
rt' [VName]
retext))
checkExp (Project Name
k ExpBase NoInfo Name
e NoInfo StructType
NoInfo SrcLoc
loc) = do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
t <- Size -> TermTypeM StructType
expType Size
e'
StructType
kt <- forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField (forall a. Located a => a -> 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
"projection of field " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
k)) Name
k StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> ExpBase f vn -> f StructType -> SrcLoc -> ExpBase f vn
Project Name
k Size
e' (forall a. a -> Info a
Info StructType
kt) SrcLoc
loc
checkExp (AppExp (If ExpBase NoInfo Name
e1 ExpBase NoInfo Name
e2 ExpBase NoInfo Name
e3 SrcLoc
loc) NoInfo AppRes
_) = do
Size
e1' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e1
Size
e2' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e2
Size
e3' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e3
let bool :: TypeBase dim u
bool = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
Bool
StructType
e1_t <- Size -> TermTypeM StructType
expType Size
e1'
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([StructType] -> StructType -> Checking
CheckingRequired [forall {dim} {u}. TypeBase dim u
bool] StructType
e1_t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage Size
e1' Text
"use as 'if' condition") forall {dim} {u}. TypeBase dim u
bool StructType
e1_t
(StructType
brancht, [VName]
retext) <- SrcLoc -> Size -> Size -> TermTypeM (StructType, [VName])
unifyBranches SrcLoc
loc Size
e2' Size
e3'
forall (m :: * -> *).
MonadUnify m =>
Usage -> Text -> StructType -> m ()
zeroOrderType
(forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"returning value of this type from 'if' expression")
Text
"type returned from branch"
StructType
brancht
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> ExpBase f vn -> ExpBase f vn -> SrcLoc -> AppExpBase f vn
If Size
e1' Size
e2' Size
e3' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
brancht [VName]
retext)
checkExp (Parens ExpBase NoInfo Name
e SrcLoc
loc) =
forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Parens forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkExp (QualParens (QualName Name
modname, SrcLoc
modnameloc) ExpBase NoInfo Name
e SrcLoc
loc) = do
(QualName VName
modname', Mod
mod) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, Mod)
lookupMod SrcLoc
loc QualName Name
modname
case Mod
mod of
ModEnv Env
env -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (TermEnv -> Env -> TermEnv
`withEnv` QualName VName -> Env -> Env
qualifyEnv QualName VName
modname' Env
env) forall a b. (a -> b) -> a -> b
$ do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
(QualName vn, SrcLoc) -> ExpBase f vn -> SrcLoc -> ExpBase f vn
QualParens (QualName VName
modname', SrcLoc
modnameloc) Size
e' SrcLoc
loc
ModFun {} ->
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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"module-is-parametric" forall a b. (a -> b) -> a -> b
$
Doc ()
"Module" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
modname forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
" is a parametric module."
where
qualifyEnv :: QualName VName -> Env -> Env
qualifyEnv QualName VName
modname' Env
env =
Env
env {envNameMap :: NameMap
envNameMap = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall {vn}. QualName vn -> QualName vn -> QualName vn
qualify' QualName VName
modname') forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
env}
qualify' :: QualName vn -> QualName vn -> QualName vn
qualify' QualName vn
modname' (QualName [vn]
qs vn
name) =
forall vn. [vn] -> vn -> QualName vn
QualName (forall vn. QualName vn -> [vn]
qualQuals QualName vn
modname' forall a. [a] -> [a] -> [a]
++ [forall vn. QualName vn -> vn
qualLeaf QualName vn
modname'] forall a. [a] -> [a] -> [a]
++ [vn]
qs) vn
name
checkExp (Var qn :: QualName Name
qn@(QualName [] Name
_) NoInfo StructType
NoInfo SrcLoc
loc) = do
(QualName VName
qn', StructType
t) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc QualName Name
qn
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var QualName VName
qn' (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (Var QualName Name
qn NoInfo StructType
NoInfo SrcLoc
loc) = do
(QualName VName
qn', StructType
t, [Name]
fields) <- forall {e} {m :: * -> *}.
(MonadError e m, MonadTypeChecker m) =>
[Name] -> Name -> m (QualName VName, StructType, [Name])
findRootVar (forall vn. QualName vn -> [vn]
qualQuals QualName Name
qn) (forall vn. QualName vn -> vn
qualLeaf QualName Name
qn)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Size -> Name -> TermTypeM Size
checkField (forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var QualName VName
qn' (forall a. a -> Info a
Info StructType
t) SrcLoc
loc) [Name]
fields
where
findRootVar :: [Name] -> Name -> m (QualName VName, StructType, [Name])
findRootVar [Name]
qs Name
name =
(forall {a} {b} {a}. (a, b) -> (a, b, [a])
whenFound forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc (forall vn. [vn] -> vn -> QualName vn
QualName [Name]
qs Name
name)) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` [Name] -> Name -> e -> m (QualName VName, StructType, [Name])
notFound [Name]
qs Name
name
whenFound :: (a, b) -> (a, b, [a])
whenFound (a
qn', b
t) = (a
qn', b
t, [])
notFound :: [Name] -> Name -> e -> m (QualName VName, StructType, [Name])
notFound [Name]
qs Name
name e
err
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
qs = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err
| Bool
otherwise = do
(QualName VName
qn', StructType
t, [Name]
fields) <-
[Name] -> Name -> m (QualName VName, StructType, [Name])
findRootVar (forall a. [a] -> [a]
init [Name]
qs) (forall a. [a] -> a
last [Name]
qs)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a b. a -> b -> a
const (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName VName
qn', StructType
t, [Name]
fields forall a. [a] -> [a] -> [a]
++ [Name
name])
checkField :: Size -> Name -> TermTypeM Size
checkField Size
e Name
k = do
StructType
t <- Size -> TermTypeM StructType
expType Size
e
let usage :: Usage
usage = forall a. Located a => a -> 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
"projection of field " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
k)
StructType
kt <- forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField Usage
usage Name
k StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> ExpBase f vn -> f StructType -> SrcLoc -> ExpBase f vn
Project Name
k Size
e (forall a. a -> Info a
Info StructType
kt) SrcLoc
loc
checkExp (Negate ExpBase NoInfo Name
arg SrcLoc
loc) = do
Size
arg' <- Text -> [PrimType] -> Size -> TermTypeM Size
require Text
"numeric negation" [PrimType]
anyNumberType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
arg
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Negate Size
arg' SrcLoc
loc
checkExp (Not ExpBase NoInfo Name
arg SrcLoc
loc) = do
Size
arg' <- Text -> [PrimType] -> Size -> TermTypeM Size
require Text
"logical negation" (PrimType
Bool forall a. a -> [a] -> [a]
: [PrimType]
anyIntType) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
arg
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. ExpBase f vn -> SrcLoc -> ExpBase f vn
Not Size
arg' SrcLoc
loc
checkExp (AppExp (Apply ExpBase NoInfo Name
fe NonEmpty (NoInfo (Diet, Maybe VName), ExpBase NoInfo Name)
args SrcLoc
loc) NoInfo AppRes
NoInfo) = do
Size
fe' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
fe
NonEmpty Size
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ExpBase NoInfo Name -> TermTypeM Size
checkExp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) NonEmpty (NoInfo (Diet, Maybe VName), ExpBase NoInfo Name)
args
StructType
t <- Size -> TermTypeM StructType
expType Size
fe'
let fname :: Maybe (QualName VName)
fname =
case Size
fe' of
Var QualName VName
v Info StructType
_ SrcLoc
_ -> forall a. a -> Maybe a
Just QualName VName
v
Size
_ -> forall a. Maybe a
Nothing
((Int
_, [VName]
exts, StructType
rt), NonEmpty (Info (Diet, Maybe VName), Size)
args'') <- forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM (Maybe (QualName VName)
-> (Int, [VName], StructType)
-> Size
-> TermTypeM
((Int, [VName], StructType), (Info (Diet, Maybe VName), Size))
onArg Maybe (QualName VName)
fname) (Int
0, [], StructType
t) NonEmpty Size
args'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> NonEmpty (f (Diet, Maybe VName), ExpBase f vn)
-> SrcLoc
-> AppExpBase f vn
Apply Size
fe' NonEmpty (Info (Diet, Maybe VName), Size)
args'' SrcLoc
loc) forall a b. (a -> b) -> a -> b
$ forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
rt [VName]
exts
where
onArg :: Maybe (QualName VName)
-> (Int, [VName], StructType)
-> Size
-> TermTypeM
((Int, [VName], StructType), (Info (Diet, Maybe VName), Size))
onArg Maybe (QualName VName)
fname (Int
i, [VName]
all_exts, StructType
t) Size
arg' = do
(Diet
d1, StructType
_, StructType
rt, Maybe VName
argext, [VName]
exts) <- SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc (Maybe (QualName VName)
fname, Int
i) StructType
t Size
arg'
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( (Int
i forall a. Num a => a -> a -> a
+ Int
1, [VName]
all_exts forall a. Semigroup a => a -> a -> a
<> [VName]
exts, StructType
rt),
(forall a. a -> Info a
Info (Diet
d1, Maybe VName
argext), Size
arg')
)
checkExp (AppExp (LetPat [SizeBinder Name]
sizes PatBase NoInfo Name StructType
pat ExpBase NoInfo Name
e ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) = do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
t <- Size -> TermTypeM StructType
expType Size
e'
forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[SizeBinder Name]
-> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes [SizeBinder Name]
sizes forall a b. (a -> b) -> a -> b
$ \[SizeBinder VName]
sizes' ->
forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase Size u)
-> StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes' PatBase NoInfo Name StructType
pat StructType
t forall a b. (a -> b) -> a -> b
$ \Pat ParamType
pat' -> do
Size
body' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
body
StructType
body_t <- Size -> TermTypeM StructType
expTypeFully Size
body'
StructType
t' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
(StructType
body_t', [VName]
retext) <-
case (StructType
t', forall t. Pat t -> [VName]
patNames Pat ParamType
pat') of
(Scalar (Prim (Signed IntType
Int64)), [VName
v])
| Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Size -> Bool
hasBinding Size
e' -> do
let f :: VName -> Maybe (Subst t)
f VName
x = if VName
x forall a. Eq a => a -> a -> Bool
== VName
v then forall a. a -> Maybe a
Just (forall t. Size -> Subst t
ExpSubst Size
e') else forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Substitutable a => TypeSubs -> a -> a
applySubst forall {t}. VName -> Maybe (Subst t)
f StructType
body_t, [])
(StructType, [VName])
_ ->
forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc (forall a b. (a -> b) -> [a] -> [b]
map forall vn. SizeBinder vn -> vn
sizeName [SizeBinder VName]
sizes' forall a. Semigroup a => a -> a -> a
<> forall t. Pat t -> [VName]
patNames Pat ParamType
pat') StructType
body_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
(forall (f :: * -> *) vn.
[SizeBinder vn]
-> PatBase f vn StructType
-> ExpBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetPat [SizeBinder VName]
sizes' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
pat') Size
e' Size
body' SrcLoc
loc)
(forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
body_t' [VName]
retext)
checkExp (AppExp (LetFun Name
name ([TypeParamBase Name]
tparams, [PatBase NoInfo Name ParamType]
params, Maybe UncheckedTypeExp
maybe_retdecl, NoInfo ResRetType
NoInfo, ExpBase NoInfo Name
e) ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) = do
([TypeParamBase VName]
tparams', [Pat ParamType]
params', Maybe (TypeExp Info VName)
maybe_retdecl', ResRetType
rettype, Size
e') <-
(Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
[PatBase NoInfo Name ParamType], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
([TypeParamBase VName], [Pat ParamType],
Maybe (TypeExp Info VName), ResRetType, Size)
checkBinding (Name
name, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name ParamType]
params, ExpBase NoInfo Name
e, SrcLoc
loc)
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
name)] forall a b. (a -> b) -> a -> b
$ do
VName
name' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
name SrcLoc
loc
let entry :: ValBinding
entry = [TypeParamBase VName] -> StructType -> ValBinding
BoundV [TypeParamBase VName]
tparams' forall a b. (a -> b) -> a -> b
$ [Pat ParamType] -> ResRetType -> StructType
funType [Pat ParamType]
params' ResRetType
rettype
bindF :: TermScope -> TermScope
bindF 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' ValBinding
entry forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope,
scopeNameMap :: NameMap
scopeNameMap =
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Namespace
Term, Name
name) (forall v. v -> QualName v
qualName VName
name') forall a b. (a -> b) -> a -> b
$
TermScope -> NameMap
scopeNameMap TermScope
scope
}
Size
body' <- forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
bindF forall a b. (a -> b) -> a -> b
$ ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
body
(StructType
body_t, [VName]
ext) <- forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc [VName
name'] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Size -> TermTypeM StructType
expTypeFully Size
body'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
( forall (f :: * -> *) vn.
vn
-> ([TypeParamBase vn], [PatBase f vn ParamType],
Maybe (TypeExp f vn), f ResRetType, ExpBase f vn)
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetFun
VName
name'
([TypeParamBase VName]
tparams', [Pat ParamType]
params', Maybe (TypeExp Info VName)
maybe_retdecl', forall a. a -> Info a
Info ResRetType
rettype, Size
e')
Size
body'
SrcLoc
loc
)
(forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
body_t [VName]
ext)
checkExp (AppExp (LetWith IdentBase NoInfo Name StructType
dest IdentBase NoInfo Name StructType
src SliceBase NoInfo Name
slice ExpBase NoInfo Name
ve ExpBase NoInfo Name
body SrcLoc
loc) NoInfo AppRes
_) = do
Ident StructType
src' <- IdentBase NoInfo Name StructType -> TermTypeM (Ident StructType)
checkIdent IdentBase NoInfo Name StructType
src
[DimIndex]
slice' <- SliceBase NoInfo Name -> TermTypeM [DimIndex]
checkSlice SliceBase NoInfo Name
slice
(StructType
t, StructType
_) <- Usage -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType (forall a. Located a => a -> Text -> Usage
mkUsage IdentBase NoInfo Name StructType
src Text
"type of source array") Name
"src" forall a b. (a -> b) -> a -> b
$ [DimIndex] -> Int
sliceDims [DimIndex]
slice'
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"type of target array") StructType
t forall a b. (a -> b) -> a -> b
$ forall a. Info a -> a
unInfo forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> f t
identType Ident StructType
src'
(StructType
elemt, [VName]
_) <- forall as.
Maybe (SrcLoc, Rigidity)
-> [DimIndex]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, Rigidity
Nonrigid)) [DimIndex]
slice' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t
Size
ve' <- Text -> StructType -> Size -> TermTypeM Size
unifies Text
"type of target array" StructType
elemt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
ve
forall a.
IdentBase NoInfo Name StructType
-> StructType -> (Ident StructType -> TermTypeM a) -> TermTypeM a
bindingIdent IdentBase NoInfo Name StructType
dest (forall a. Info a -> a
unInfo (forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> f t
identType Ident StructType
src')) forall a b. (a -> b) -> a -> b
$ \Ident StructType
dest' -> do
Size
body' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
body
(StructType
body_t, [VName]
ext) <- forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc [forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
dest'] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Size -> TermTypeM StructType
expTypeFully Size
body'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
IdentBase f vn StructType
-> IdentBase f vn StructType
-> SliceBase f vn
-> ExpBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
LetWith Ident StructType
dest' Ident StructType
src' [DimIndex]
slice' Size
ve' Size
body' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
body_t [VName]
ext)
checkExp (Update ExpBase NoInfo Name
src SliceBase NoInfo Name
slice ExpBase NoInfo Name
ve SrcLoc
loc) = do
[DimIndex]
slice' <- SliceBase NoInfo Name -> TermTypeM [DimIndex]
checkSlice SliceBase NoInfo Name
slice
(StructType
t, StructType
_) <- Usage -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType (forall a. Located a => a -> Usage
mkUsage' ExpBase NoInfo Name
src) Name
"src" forall a b. (a -> b) -> a -> b
$ [DimIndex] -> Int
sliceDims [DimIndex]
slice'
(StructType
elemt, [VName]
_) <- forall as.
Maybe (SrcLoc, Rigidity)
-> [DimIndex]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, Rigidity
Nonrigid)) [DimIndex]
slice' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t
Size
ve' <- Text -> StructType -> Size -> TermTypeM Size
unifies Text
"type of target array" StructType
elemt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
ve
Size
src' <- Text -> StructType -> Size -> TermTypeM Size
unifies Text
"type of target array" StructType
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
src
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn
-> SliceBase f vn -> ExpBase f vn -> SrcLoc -> ExpBase f vn
Update Size
src' [DimIndex]
slice' Size
ve' SrcLoc
loc
checkExp (RecordUpdate ExpBase NoInfo Name
src [Name]
fields ExpBase NoInfo Name
ve NoInfo StructType
NoInfo SrcLoc
loc) = do
Size
src' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
src
Size
ve' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
ve
StructType
a <- Size -> TermTypeM StructType
expTypeFully Size
src'
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField Usage
usage) StructType
a [Name]
fields
StructType
ve_t <- Size -> TermTypeM StructType
expType Size
ve'
StructType
updated_t <- [Name] -> StructType -> StructType -> TermTypeM StructType
updateField [Name]
fields StructType
ve_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Size -> TermTypeM StructType
expTypeFully Size
src'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn
-> [Name] -> ExpBase f vn -> f StructType -> SrcLoc -> ExpBase f vn
RecordUpdate Size
src' [Name]
fields Size
ve' (forall a. a -> Info a
Info StructType
updated_t) SrcLoc
loc
where
usage :: Usage
usage = forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"record update"
updateField :: [Name] -> StructType -> StructType -> TermTypeM StructType
updateField [] StructType
ve_t StructType
src_t = do
(StructType
src_t', Map VName Size
_) <- forall als.
Usage
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType Usage
usage Rigidity
Nonrigid Name
"any" StructType
src_t
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure ([Name] -> StructType -> StructType -> Checking
CheckingRecordUpdate [Name]
fields StructType
src_t' StructType
ve_t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
src_t' StructType
ve_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
ve_t
updateField (Name
f : [Name]
fs) StructType
ve_t (Scalar (Record Map Name StructType
m))
| Just StructType
f_t <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
f Map Name StructType
m = do
StructType
f_t' <- [Name] -> StructType -> StructType -> TermTypeM StructType
updateField [Name]
fs StructType
ve_t StructType
f_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
f StructType
f_t' Map Name StructType
m
updateField [Name]
_ StructType
_ StructType
_ =
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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"record-type-not-known" forall a b. (a -> b) -> a -> b
$
Doc ()
"Full type of"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty ExpBase NoInfo Name
src)
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
" is not known at this point. Add a type annotation to the original record to disambiguate."
checkExp (AppExp (Index ExpBase NoInfo Name
e SliceBase NoInfo Name
slice SrcLoc
loc) NoInfo AppRes
_) = do
[DimIndex]
slice' <- SliceBase NoInfo Name -> TermTypeM [DimIndex]
checkSlice SliceBase NoInfo Name
slice
(StructType
t, StructType
_) <- Usage -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType (forall a. Located a => a -> Usage
mkUsage' SrcLoc
loc) Name
"e" forall a b. (a -> b) -> a -> b
$ [DimIndex] -> Int
sliceDims [DimIndex]
slice'
Size
e' <- Text -> StructType -> Size -> TermTypeM Size
unifies Text
"being indexed at" StructType
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
(StructType
t', [VName]
retext) <-
forall as.
Maybe (SrcLoc, Rigidity)
-> [DimIndex]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape (forall a. a -> Maybe a
Just (SrcLoc
loc, RigidSource -> Rigidity
Rigid (Maybe Size -> Text -> RigidSource
RigidSlice forall a. Maybe a
Nothing Text
""))) [DimIndex]
slice'
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Size -> TermTypeM StructType
expTypeFully Size
e'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn -> SliceBase f vn -> SrcLoc -> AppExpBase f vn
Index Size
e' [DimIndex]
slice' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
t' [VName]
retext)
checkExp (Assert ExpBase NoInfo Name
e1 ExpBase NoInfo Name
e2 NoInfo Text
NoInfo SrcLoc
loc) = do
Size
e1' <- Text -> [PrimType] -> Size -> TermTypeM Size
require Text
"being asserted" [PrimType
Bool] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e1
Size
e2' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e2
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
ExpBase f vn -> ExpBase f vn -> f Text -> SrcLoc -> ExpBase f vn
Assert Size
e1' Size
e2' (forall a. a -> Info a
Info (forall a. Pretty a => a -> Text
prettyText ExpBase NoInfo Name
e1)) SrcLoc
loc
checkExp (Lambda [PatBase NoInfo Name ParamType]
params ExpBase NoInfo Name
body Maybe UncheckedTypeExp
rettype_te NoInfo ResRetType
NoInfo SrcLoc
loc) = do
([Pat ParamType]
params', Size
body', Maybe (TypeExp Info VName)
rettype', RetType [VName]
dims TypeBase Size Uniqueness
ty) <-
forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[TypeParamBase Name]
-> [PatBase NoInfo Name ParamType]
-> ([TypeParamBase VName] -> [Pat ParamType] -> TermTypeM a)
-> TermTypeM a
bindingParams [] [PatBase NoInfo Name ParamType]
params forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
_ [Pat ParamType]
params' -> do
Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
rettype_checked <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse UncheckedTypeExp
-> TermTypeM
(TypeExp Info VName, TypeBase Size Uniqueness, [VName])
checkTypeExpNonrigid Maybe UncheckedTypeExp
rettype_te
let declared_rettype :: Maybe (TypeBase Size Uniqueness)
declared_rettype =
case Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
rettype_checked of
Just (TypeExp Info VName
_, TypeBase Size Uniqueness
st, [VName]
_) -> forall a. a -> Maybe a
Just TypeBase Size Uniqueness
st
Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
Nothing -> forall a. Maybe a
Nothing
Size
body' <- [Pat ParamType]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size Uniqueness)
-> SrcLoc
-> TermTypeM Size
checkFunBody [Pat ParamType]
params' ExpBase NoInfo Name
body Maybe (TypeBase Size Uniqueness)
declared_rettype SrcLoc
loc
StructType
body_t <- Size -> TermTypeM StructType
expTypeFully Size
body'
[Pat ParamType]
params'' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [Pat ParamType]
params'
(Maybe (TypeExp Info VName)
rettype', ResRetType
rettype_st) <-
case Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
rettype_checked of
Just (TypeExp Info VName
te, TypeBase Size Uniqueness
st, [VName]
ext) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just TypeExp Info VName
te, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext TypeBase Size Uniqueness
st)
Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
Nothing -> do
ResRetType
ret <- forall {m :: * -> *}.
MonadUnify m =>
[Pat ParamType] -> TypeBase Size Uniqueness -> m ResRetType
inferReturnSizes [Pat ParamType]
params'' forall a b. (a -> b) -> a -> b
$ forall u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
body_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, ResRetType
ret)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pat ParamType]
params'', Size
body', Maybe (TypeExp Info VName)
rettype', ResRetType
rettype_st)
Maybe Name -> [Pat ParamType] -> TermTypeM ()
verifyFunctionParams forall a. Maybe a
Nothing [Pat ParamType]
params'
(TypeBase Size Uniqueness
ty', [VName]
dims') <- forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc [VName]
dims TypeBase Size Uniqueness
ty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[PatBase f vn ParamType]
-> ExpBase f vn
-> Maybe (TypeExp f vn)
-> f ResRetType
-> SrcLoc
-> ExpBase f vn
Lambda [Pat ParamType]
params' Size
body' Maybe (TypeExp Info VName)
rettype' (forall a. a -> Info a
Info (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims' TypeBase Size Uniqueness
ty')) SrcLoc
loc
where
inferReturnSizes :: [Pat ParamType] -> TypeBase Size Uniqueness -> m ResRetType
inferReturnSizes [Pat ParamType]
params' TypeBase Size Uniqueness
ret = do
Int
cur_lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
let named :: (PName, b, c) -> Maybe VName
named (Named VName
x, b
_, c
_) = forall a. a -> Maybe a
Just VName
x
named (PName
Unnamed, b
_, c
_) = forall a. Maybe a
Nothing
param_names :: [VName]
param_names = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {b} {c}. (PName, b, c) -> Maybe VName
named forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat ParamType -> (PName, Diet, StructType)
patternParam) [Pat ParamType]
params'
pos_sizes :: Set VName
pos_sizes =
forall als. TypeBase Size als -> Set VName
sizeNamesPos forall a b. (a -> b) -> a -> b
$ [Pat ParamType] -> ResRetType -> StructType
funType [Pat ParamType]
params' forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size Uniqueness
ret
hide :: VName -> (Int, b) -> Bool
hide VName
k (Int
lvl, b
_) =
Int
lvl forall a. Ord a => a -> a -> Bool
>= Int
cur_lvl Bool -> Bool -> Bool
&& VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
param_names Bool -> Bool -> Bool
&& VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
pos_sizes
Set VName
hidden_sizes <-
forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall {b}. VName -> (Int, b) -> Bool
hide forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let onDim :: VName -> Set VName
onDim VName
name
| VName
name forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
hidden_sizes = forall a. a -> Set a
S.singleton VName
name
onDim VName
_ = forall a. Monoid a => a
mempty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap VName -> Set VName
onDim forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> FV
freeInType TypeBase Size Uniqueness
ret) TypeBase Size Uniqueness
ret
checkExp (OpSection QualName Name
op NoInfo StructType
_ SrcLoc
loc) = do
(QualName VName
op', StructType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc QualName Name
op
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
OpSection QualName VName
op' (forall a. a -> Info a
Info StructType
ftype) SrcLoc
loc
checkExp (OpSectionLeft QualName Name
op NoInfo StructType
_ ExpBase NoInfo Name
e (NoInfo (PName, ParamType, Maybe VName), NoInfo (PName, ParamType))
_ (NoInfo ResRetType, NoInfo [VName])
_ SrcLoc
loc) = do
(QualName VName
op', StructType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc QualName Name
op
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
(Diet
_, StructType
t1, StructType
rt, Maybe VName
argext, [VName]
retext) <- SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc (forall a. a -> Maybe a
Just QualName VName
op', Int
0) StructType
ftype Size
e'
case (StructType
ftype, StructType
rt) of
(Scalar (Arrow NoUniqueness
_ PName
m1 Diet
d1 StructType
_ ResRetType
_), Scalar (Arrow NoUniqueness
_ PName
m2 Diet
d2 StructType
t2 ResRetType
rettype)) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
QualName vn
-> f StructType
-> ExpBase f vn
-> (f (PName, ParamType, Maybe VName), f (PName, ParamType))
-> (f ResRetType, f [VName])
-> SrcLoc
-> ExpBase f vn
OpSectionLeft
QualName VName
op'
(forall a. a -> Info a
Info StructType
ftype)
Size
e'
(forall a. a -> Info a
Info (PName
m1, forall u. Diet -> TypeBase Size u -> ParamType
toParam Diet
d1 StructType
t1, Maybe VName
argext), forall a. a -> Info a
Info (PName
m2, forall u. Diet -> TypeBase Size u -> ParamType
toParam Diet
d2 StructType
t2))
(forall a. a -> Info a
Info ResRetType
rettype, forall a. a -> Info a
Info [VName]
retext)
SrcLoc
loc
(StructType, StructType)
_ ->
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 ()
"Operator section with invalid operator of type" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
ftype
checkExp (OpSectionRight QualName Name
op NoInfo StructType
_ ExpBase NoInfo Name
e (NoInfo (PName, ParamType), NoInfo (PName, ParamType, Maybe VName))
_ NoInfo ResRetType
NoInfo SrcLoc
loc) = do
(QualName VName
op', StructType
ftype) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc QualName Name
op
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
case StructType
ftype of
Scalar (Arrow NoUniqueness
_ PName
m1 Diet
d1 StructType
t1 (RetType [] (Scalar (Arrow Uniqueness
_ PName
m2 Diet
d2 StructType
t2 (RetType [VName]
dims2 TypeBase Size Uniqueness
ret))))) -> do
(Diet
_, StructType
t2', StructType
arrow', Maybe VName
argext, [VName]
_) <-
SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply
SrcLoc
loc
(forall a. a -> Maybe a
Just QualName VName
op', Int
1)
(forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow forall a. Monoid a => a
mempty PName
m2 Diet
d2 StructType
t2 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 u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow Uniqueness
Nonunique PName
m1 Diet
d1 StructType
t1 forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 TypeBase Size Uniqueness
ret)
Size
e'
case StructType
arrow' of
Scalar (Arrow NoUniqueness
_ PName
_ Diet
_ StructType
t1' (RetType [VName]
dims2' TypeBase Size Uniqueness
ret')) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
QualName vn
-> f StructType
-> ExpBase f vn
-> (f (PName, ParamType), f (PName, ParamType, Maybe VName))
-> f ResRetType
-> SrcLoc
-> ExpBase f vn
OpSectionRight
QualName VName
op'
(forall a. a -> Info a
Info StructType
ftype)
Size
e'
(forall a. a -> Info a
Info (PName
m1, forall u. Diet -> TypeBase Size u -> ParamType
toParam Diet
d1 StructType
t1'), forall a. a -> Info a
Info (PName
m2, forall u. Diet -> TypeBase Size u -> ParamType
toParam Diet
d2 StructType
t2', Maybe VName
argext))
(forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2' TypeBase Size Uniqueness
ret')
SrcLoc
loc
StructType
_ -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"OpSectionRight: impossible type\n" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> [Char]
prettyString StructType
arrow'
StructType
_ ->
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 ()
"Operator section with invalid operator of type" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
ftype
checkExp (ProjectSection [Name]
fields NoInfo StructType
NoInfo SrcLoc
loc) = do
StructType
a <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"a"
let usage :: Usage
usage = forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"projection at"
StructType
b <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField Usage
usage) StructType
a [Name]
fields
let ft :: StructType
ft = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe StructType
a 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 u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
[Name] -> f StructType -> SrcLoc -> ExpBase f vn
ProjectSection [Name]
fields (forall a. a -> Info a
Info StructType
ft) SrcLoc
loc
checkExp (IndexSection SliceBase NoInfo Name
slice NoInfo StructType
NoInfo SrcLoc
loc) = do
[DimIndex]
slice' <- SliceBase NoInfo Name -> TermTypeM [DimIndex]
checkSlice SliceBase NoInfo Name
slice
(StructType
t, StructType
_) <- Usage -> Name -> Int -> TermTypeM (StructType, StructType)
newArrayType (forall a. Located a => a -> Usage
mkUsage' SrcLoc
loc) Name
"e" forall a b. (a -> b) -> a -> b
$ [DimIndex] -> Int
sliceDims [DimIndex]
slice'
(StructType
t', [VName]
retext) <- forall as.
Maybe (SrcLoc, Rigidity)
-> [DimIndex]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
sliceShape forall a. Maybe a
Nothing [DimIndex]
slice' StructType
t
let ft :: StructType
ft = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe StructType
t forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
retext forall a b. (a -> b) -> a -> b
$ forall u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
t'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
SliceBase f vn -> f StructType -> SrcLoc -> ExpBase f vn
IndexSection [DimIndex]
slice' (forall a. a -> Info a
Info StructType
ft) SrcLoc
loc
checkExp (AppExp (Loop [VName]
_ PatBase NoInfo Name ParamType
mergepat ExpBase NoInfo Name
mergeexp LoopFormBase NoInfo Name
form ExpBase NoInfo Name
loopbody SrcLoc
loc) NoInfo AppRes
_) = do
(([VName]
sparams, Pat ParamType
mergepat', Size
mergeexp', LoopFormBase Info VName
form', Size
loopbody'), AppRes
appres) <-
(ExpBase NoInfo Name -> TermTypeM Size)
-> UncheckedLoop -> SrcLoc -> TermTypeM (CheckedLoop, AppRes)
checkLoop ExpBase NoInfo Name -> TermTypeM Size
checkExp (PatBase NoInfo Name ParamType
mergepat, ExpBase NoInfo Name
mergeexp, LoopFormBase NoInfo Name
form, ExpBase NoInfo Name
loopbody) SrcLoc
loc
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp
(forall (f :: * -> *) vn.
[VName]
-> PatBase f vn ParamType
-> ExpBase f vn
-> LoopFormBase f vn
-> ExpBase f vn
-> SrcLoc
-> AppExpBase f vn
Loop [VName]
sparams Pat ParamType
mergepat' Size
mergeexp' LoopFormBase Info VName
form' Size
loopbody' SrcLoc
loc)
(forall a. a -> Info a
Info AppRes
appres)
checkExp (Constr Name
name [ExpBase NoInfo Name]
es NoInfo StructType
NoInfo SrcLoc
loc) = do
StructType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
[Size]
es' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExpBase NoInfo Name -> TermTypeM Size
checkExp [ExpBase NoInfo Name]
es
[StructType]
ets <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Size -> TermTypeM StructType
expTypeFully [Size]
es'
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"use of constructor") Name
name StructType
t [StructType]
ets
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
Name -> [ExpBase f vn] -> f StructType -> SrcLoc -> ExpBase f vn
Constr Name
name [Size]
es' (forall a. a -> Info a
Info StructType
t) SrcLoc
loc
checkExp (AppExp (Match ExpBase NoInfo Name
e NonEmpty (CaseBase NoInfo Name)
cs SrcLoc
loc) NoInfo AppRes
_) = do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
mt <- Size -> TermTypeM StructType
expTypeFully Size
e'
(NonEmpty (CaseBase Info VName)
cs', StructType
t, [VName]
retext) <- StructType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), StructType, [VName])
checkCases StructType
mt NonEmpty (CaseBase NoInfo Name)
cs
forall (m :: * -> *).
MonadUnify m =>
Usage -> Text -> StructType -> m ()
zeroOrderType
(forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"being returned 'match'")
Text
"type returned from pattern match"
StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
AppExpBase f vn -> f AppRes -> ExpBase f vn
AppExp (forall (f :: * -> *) vn.
ExpBase f vn
-> NonEmpty (CaseBase f vn) -> SrcLoc -> AppExpBase f vn
Match Size
e' NonEmpty (CaseBase Info VName)
cs' SrcLoc
loc) (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ StructType -> [VName] -> AppRes
AppRes StructType
t [VName]
retext)
checkExp (Attr AttrInfo Name
info ExpBase NoInfo Name
e SrcLoc
loc) =
forall (f :: * -> *) vn.
AttrInfo vn -> ExpBase f vn -> SrcLoc -> ExpBase f vn
Attr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr AttrInfo Name
info forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkCases ::
StructType ->
NE.NonEmpty (CaseBase NoInfo Name) ->
TermTypeM (NE.NonEmpty (CaseBase Info VName), StructType, [VName])
checkCases :: StructType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), StructType, [VName])
checkCases StructType
mt NonEmpty (CaseBase NoInfo Name)
rest_cs =
case forall a. NonEmpty a -> (a, Maybe (NonEmpty a))
NE.uncons NonEmpty (CaseBase NoInfo Name)
rest_cs of
(CaseBase NoInfo Name
c, Maybe (NonEmpty (CaseBase NoInfo Name))
Nothing) -> do
(CaseBase Info VName
c', StructType
t, [VName]
retext) <- StructType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, StructType, [VName])
checkCase StructType
mt CaseBase NoInfo Name
c
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> NonEmpty a
NE.singleton CaseBase Info VName
c', StructType
t, [VName]
retext)
(CaseBase NoInfo Name
c, Just NonEmpty (CaseBase NoInfo Name)
cs) -> do
((CaseBase Info VName
c', StructType
c_t, [VName]
_), (NonEmpty (CaseBase Info VName)
cs', StructType
cs_t, [VName]
_)) <-
(,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StructType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, StructType, [VName])
checkCase StructType
mt CaseBase NoInfo Name
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StructType
-> NonEmpty (CaseBase NoInfo Name)
-> TermTypeM (NonEmpty (CaseBase Info VName), StructType, [VName])
checkCases StructType
mt NonEmpty (CaseBase NoInfo Name)
cs
(StructType
brancht, [VName]
retext) <- SrcLoc
-> StructType -> StructType -> TermTypeM (StructType, [VName])
unifyBranchTypes (forall a. Located a => a -> SrcLoc
srclocOf CaseBase NoInfo Name
c) StructType
c_t StructType
cs_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons CaseBase Info VName
c' NonEmpty (CaseBase Info VName)
cs', StructType
brancht, [VName]
retext)
checkCase ::
StructType ->
CaseBase NoInfo Name ->
TermTypeM (CaseBase Info VName, StructType, [VName])
checkCase :: StructType
-> CaseBase NoInfo Name
-> TermTypeM (CaseBase Info VName, StructType, [VName])
checkCase StructType
mt (CasePat PatBase NoInfo Name StructType
p ExpBase NoInfo Name
e SrcLoc
loc) =
forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase Size u)
-> StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
bindingPat [] PatBase NoInfo Name StructType
p StructType
mt forall a b. (a -> b) -> a -> b
$ \Pat ParamType
p' -> do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
StructType
e_t <- Size -> TermTypeM StructType
expTypeFully Size
e'
(StructType
e_t', [VName]
retext) <- forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc (forall t. Pat t -> [VName]
patNames Pat ParamType
p') StructType
e_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) vn.
PatBase f vn StructType -> ExpBase f vn -> SrcLoc -> CaseBase f vn
CasePat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p') Size
e' SrcLoc
loc, StructType
e_t', [VName]
retext)
data Unmatched p
= UnmatchedNum p [PatLit]
| UnmatchedBool p
| UnmatchedConstr p
| Unmatched p
deriving (forall a b. a -> Unmatched b -> Unmatched a
forall a b. (a -> b) -> Unmatched a -> Unmatched 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 -> Unmatched b -> Unmatched a
$c<$ :: forall a b. a -> Unmatched b -> Unmatched a
fmap :: forall a b. (a -> b) -> Unmatched a -> Unmatched b
$cfmap :: forall a b. (a -> b) -> Unmatched a -> Unmatched b
Functor, Int -> Unmatched p -> ShowS
forall p. Show p => Int -> Unmatched p -> ShowS
forall p. Show p => [Unmatched p] -> ShowS
forall p. Show p => Unmatched p -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Unmatched p] -> ShowS
$cshowList :: forall p. Show p => [Unmatched p] -> ShowS
show :: Unmatched p -> [Char]
$cshow :: forall p. Show p => Unmatched p -> [Char]
showsPrec :: Int -> Unmatched p -> ShowS
$cshowsPrec :: forall p. Show p => Int -> Unmatched p -> ShowS
Show)
instance Pretty (Unmatched (Pat StructType)) where
pretty :: forall ann. Unmatched (Pat StructType) -> Doc ann
pretty Unmatched (Pat StructType)
um = case Unmatched (Pat StructType)
um of
(UnmatchedNum Pat StructType
p [PatLit]
nums) -> forall {v} {f :: * -> *} {t} {ann}.
(Eq v, IsName v, Annot f, Pretty t) =>
PatBase f v t -> Doc ann
pretty' Pat StructType
p forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"where p is not one of" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty [PatLit]
nums
(UnmatchedBool Pat StructType
p) -> forall {v} {f :: * -> *} {t} {ann}.
(Eq v, IsName v, Annot f, Pretty t) =>
PatBase f v t -> Doc ann
pretty' Pat StructType
p
(UnmatchedConstr Pat StructType
p) -> forall {v} {f :: * -> *} {t} {ann}.
(Eq v, IsName v, Annot f, Pretty t) =>
PatBase f v t -> Doc ann
pretty' Pat StructType
p
(Unmatched Pat StructType
p) -> forall {v} {f :: * -> *} {t} {ann}.
(Eq v, IsName v, Annot f, Pretty t) =>
PatBase f v t -> Doc ann
pretty' Pat StructType
p
where
pretty' :: PatBase f v t -> Doc ann
pretty' (PatAscription PatBase f v t
p TypeExp f v
t SrcLoc
_) = forall a ann. Pretty a => a -> Doc ann
pretty PatBase f v t
p forall a. Semigroup a => a -> a -> a
<> Doc ann
":" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeExp f v
t
pretty' (PatParens PatBase f v t
p SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ PatBase f v t -> Doc ann
pretty' PatBase f v t
p
pretty' (PatAttr AttrInfo v
_ PatBase f v t
p SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ PatBase f v t -> Doc ann
pretty' PatBase f v t
p
pretty' (Id v
v f t
_ SrcLoc
_) = forall v a. IsName v => v -> Doc a
prettyName v
v
pretty' (TuplePat [PatBase f v t]
pats SrcLoc
_) = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall a. [Doc a] -> Doc a
commasep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map PatBase f v t -> Doc ann
pretty' [PatBase f v t]
pats
pretty' (RecordPat [(Name, PatBase f v t)]
fs SrcLoc
_) = forall ann. Doc ann -> Doc ann
braces forall a b. (a -> b) -> a -> b
$ forall a. [Doc a] -> Doc a
commasep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase f v t) -> Doc ann
ppField [(Name, PatBase f v t)]
fs
where
ppField :: (Name, PatBase f v t) -> Doc ann
ppField (Name
name, PatBase f v t
t) = forall a ann. Pretty a => a -> Doc ann
pretty (Name -> [Char]
nameToString Name
name) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
equals forall a. Semigroup a => a -> a -> a
<> PatBase f v t -> Doc ann
pretty' PatBase f v t
t
pretty' Wildcard {} = Doc ann
"_"
pretty' (PatLit PatLit
e f t
_ SrcLoc
_) = forall a ann. Pretty a => a -> Doc ann
pretty PatLit
e
pretty' (PatConstr Name
n f t
_ [PatBase f v t]
ps SrcLoc
_) = Doc ann
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Name
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
sep (forall a b. (a -> b) -> [a] -> [b]
map PatBase f v t -> Doc ann
pretty' [PatBase f v t]
ps)
checkIdent :: IdentBase NoInfo Name StructType -> TermTypeM (Ident StructType)
checkIdent :: IdentBase NoInfo Name StructType -> TermTypeM (Ident StructType)
checkIdent (Ident Name
name NoInfo StructType
_ SrcLoc
loc) = do
(QualName [VName]
_ VName
name', StructType
vt) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName, StructType)
lookupVar SrcLoc
loc (forall v. v -> QualName v
qualName Name
name)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident VName
name' (forall a. a -> Info a
Info StructType
vt) SrcLoc
loc
checkSlice :: UncheckedSlice -> TermTypeM [DimIndex]
checkSlice :: SliceBase NoInfo Name -> TermTypeM [DimIndex]
checkSlice = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DimIndexBase NoInfo Name -> TermTypeM DimIndex
checkDimIndex
where
checkDimIndex :: DimIndexBase NoInfo Name -> TermTypeM DimIndex
checkDimIndex (DimFix ExpBase NoInfo Name
i) = do
forall (f :: * -> *) vn. ExpBase f vn -> DimIndexBase f vn
DimFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> [PrimType] -> Size -> TermTypeM Size
require Text
"use as index" [PrimType]
anySignedType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
i)
checkDimIndex (DimSlice Maybe (ExpBase NoInfo Name)
i Maybe (ExpBase NoInfo Name)
j Maybe (ExpBase NoInfo Name)
s) =
forall (f :: * -> *) vn.
Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> Maybe (ExpBase f vn)
-> DimIndexBase f vn
DimSlice forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Size)
check Maybe (ExpBase NoInfo Name)
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Size)
check Maybe (ExpBase NoInfo Name)
j forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Size)
check Maybe (ExpBase NoInfo Name)
s
check :: Maybe (ExpBase NoInfo Name) -> TermTypeM (Maybe Size)
check =
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> StructType -> Size -> TermTypeM Size
unifies Text
"use as index" (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ExpBase NoInfo Name -> TermTypeM Size
checkExp
sliceDims :: [DimIndex] -> Int
sliceDims :: [DimIndex] -> Int
sliceDims = forall (t :: * -> *) a. Foldable t => t a -> Int
length
instantiateDimsInReturnType ::
SrcLoc ->
Maybe (QualName VName) ->
ResRetType ->
TermTypeM (ResType, [VName])
instantiateDimsInReturnType :: SrcLoc
-> Maybe (QualName VName)
-> ResRetType
-> TermTypeM (TypeBase Size Uniqueness, [VName])
instantiateDimsInReturnType SrcLoc
loc Maybe (QualName VName)
fname (RetType [VName]
dims TypeBase Size Uniqueness
t)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VName]
dims =
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size Uniqueness
t, forall a. Monoid a => a
mempty)
| Bool
otherwise = do
[VName]
dims' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> TermTypeM VName
new [VName]
dims
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall {a}.
Substitutable a =>
[(VName, Subst StructRetType)] -> a -> a
onDim forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Size -> Subst t
ExpSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> Size
`sizeFromName` SrcLoc
loc) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName) [VName]
dims') TypeBase Size Uniqueness
t, [VName]
dims')
where
new :: VName -> TermTypeM VName
new =
forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
loc (Maybe (QualName VName) -> RigidSource
RigidRet Maybe (QualName VName)
fname)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
nameFromString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> [Char]
baseString
onDim :: [(VName, Subst StructRetType)] -> a -> a
onDim [(VName, Subst StructRetType)]
dims' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(VName, Subst StructRetType)]
dims')
type ApplyOp = (Maybe (QualName VName), Int)
boundInsideType :: TypeBase Size as -> S.Set VName
boundInsideType :: forall als. TypeBase Size als -> Set VName
boundInsideType (Array as
_ Shape Size
_ ScalarTypeBase Size NoUniqueness
t) = forall als. TypeBase Size als -> Set VName
boundInsideType (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar ScalarTypeBase Size NoUniqueness
t)
boundInsideType (Scalar Prim {}) = forall a. Monoid a => a
mempty
boundInsideType (Scalar (TypeVar as
_ QualName VName
_ [TypeArg Size]
targs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TypeArg Size -> Set VName
f [TypeArg Size]
targs
where
f :: TypeArg Size -> Set VName
f (TypeArgType StructType
t) = forall als. TypeBase Size als -> Set VName
boundInsideType StructType
t
f TypeArgDim {} = forall a. Monoid a => a
mempty
boundInsideType (Scalar (Record Map Name (TypeBase Size as)
fs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall als. TypeBase Size als -> Set VName
boundInsideType Map Name (TypeBase Size as)
fs
boundInsideType (Scalar (Sum Map Name [TypeBase Size as]
cs)) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall als. TypeBase Size als -> Set VName
boundInsideType) Map Name [TypeBase Size as]
cs
boundInsideType (Scalar (Arrow as
_ PName
pn Diet
_ StructType
t1 (RetType [VName]
dims TypeBase Size Uniqueness
t2))) =
Set VName
pn' forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType StructType
t1 forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [VName]
dims forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType TypeBase Size Uniqueness
t2
where
pn' :: Set VName
pn' = case PName
pn of
PName
Unnamed -> forall a. Monoid a => a
mempty
Named VName
v -> forall a. a -> Set a
S.singleton VName
v
dimUses :: TypeBase Size u -> (Names, Names)
dimUses :: forall u. TypeBase Size u -> (Set VName, Set VName)
dimUses = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims forall {m :: * -> *}.
MonadState (Set VName, Set VName) m =>
Set VName -> DimPos -> Size -> m ()
f
where
f :: Set VName -> DimPos -> Size -> m ()
f Set VName
bound DimPos
pos Size
e =
case DimPos
pos of
DimPos
PosImmediate ->
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FV -> Set VName
fvVars FV
fv, forall a. Monoid a => a
mempty) <>)
DimPos
PosParam ->
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((forall a. Monoid a => a
mempty, FV -> Set VName
fvVars FV
fv) <>)
DimPos
PosReturn -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
where
fv :: FV
fv = Size -> FV
freeInExp Size
e FV -> Set VName -> FV
`freeWithout` Set VName
bound
checkApply ::
SrcLoc ->
ApplyOp ->
StructType ->
Exp ->
TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply :: SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc (Maybe (QualName VName)
fname, Int
_) (Scalar (Arrow NoUniqueness
_ PName
pname Diet
d1 StructType
tp1 ResRetType
tp2)) Size
argexp = do
let argtype :: StructType
argtype = Size -> StructType
typeOf Size
argexp
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Maybe (QualName VName)
-> Size -> StructType -> StructType -> Checking
CheckingApply Maybe (QualName VName)
fname Size
argexp StructType
tp1 StructType
argtype) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage Size
argexp Text
"use as function argument") StructType
tp1 StructType
argtype
(TypeBase Size Uniqueness
tp2', [VName]
ext) <- SrcLoc
-> Maybe (QualName VName)
-> ResRetType
-> TermTypeM (TypeBase Size Uniqueness, [VName])
instantiateDimsInReturnType SrcLoc
loc Maybe (QualName VName)
fname forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully ResRetType
tp2
StructType
argtype' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
argtype
let (Set VName
tp2_produced_dims, Set VName
tp2_paramdims) = forall u. TypeBase Size u -> (Set VName, Set VName)
dimUses TypeBase Size Uniqueness
tp2'
problematic :: Set VName
problematic = forall a. Ord a => [a] -> Set a
S.fromList [VName]
ext forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
boundInsideType StructType
argtype'
problem :: Bool
problem = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
problematic) (Set VName
tp2_paramdims forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
tp2_produced_dims)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall a. Set a -> Bool
S.null Set VName
problematic) Bool -> Bool -> Bool
&& Bool
problem) forall a b. (a -> b) -> a -> b
$ do
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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"existential-param-ret" forall a b. (a -> b) -> a -> b
$
Doc ()
"Existential size would appear in function parameter of return type:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext TypeBase Size Uniqueness
tp2'))
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"This is usually because a higher-order function is used with functional arguments that return existential sizes or locally named sizes, which are then used as parameters of other function arguments."
(Maybe VName
argext, StructType
tp2'') <-
case PName
pname of
Named VName
pname'
| forall a. Ord a => a -> Set a -> Bool
S.member VName
pname' (FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> FV
freeInType TypeBase Size Uniqueness
tp2') ->
if Size -> Bool
hasBinding Size
argexp
then do
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn (forall a. Located a => a -> SrcLoc
srclocOf Size
argexp) forall a b. (a -> b) -> a -> b
$
forall a. Doc a -> Doc a -> Doc a
withIndexLink
Doc ()
"size-expression-bind"
Doc ()
"Size expression with binding is replaced by unknown size."
VName
d <- forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim Size
argexp (Maybe (QualName VName) -> Text -> RigidSource
RigidArg Maybe (QualName VName)
fname forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Text
prettyTextOneLine forall a b. (a -> b) -> a -> b
$ Size -> ExpBase NoInfo VName
bareExp Size
argexp) Name
"n"
let parsubst :: VName -> Maybe (Subst t)
parsubst VName
v =
if VName
v forall a. Eq a => a -> a -> Bool
== VName
pname'
then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
ExpSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
d) forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Size
argexp
else forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just VName
d, forall a. Substitutable a => TypeSubs -> a -> a
applySubst forall {t}. VName -> Maybe (Subst t)
parsubst forall a b. (a -> b) -> a -> b
$ forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
tp2')
else
let parsubst :: VName -> Maybe (Subst t)
parsubst VName
v =
if VName
v forall a. Eq a => a -> a -> Bool
== VName
pname'
then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
ExpSubst forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Size
argexp forall a b. (a -> b) -> a -> b
$ Size -> Maybe Size
stripExp Size
argexp
else forall a. Maybe a
Nothing
in forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall a. Substitutable a => TypeSubs -> a -> a
applySubst forall {t}. VName -> Maybe (Subst t)
parsubst forall a b. (a -> b) -> a -> b
$ forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
tp2')
PName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
tp2')
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diet
d1, StructType
tp1, StructType
tp2'', Maybe VName
argext, [VName]
ext)
checkApply SrcLoc
loc ApplyOp
fname tfun :: StructType
tfun@(Scalar TypeVar {}) Size
arg = do
ParamType
tv <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"b"
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"use as function") StructType
tfun forall a b. (a -> b) -> a -> b
$
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow forall a. Monoid a => a
mempty PName
Unnamed Diet
Observe (Size -> StructType
typeOf Size
arg) 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
$ ParamType -> TypeBase Size Uniqueness
paramToRes ParamType
tv)
StructType
tfun' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
tfun
SrcLoc
-> ApplyOp
-> StructType
-> Size
-> TermTypeM (Diet, StructType, StructType, Maybe VName, [VName])
checkApply SrcLoc
loc ApplyOp
fname StructType
tfun' Size
arg
checkApply SrcLoc
loc (Maybe (QualName VName)
fname, Int
prev_applied) StructType
ftype Size
argexp = do
let fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"expression" (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) Maybe (QualName VName)
fname
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
$
if Int
prev_applied forall a. Eq a => a -> a -> Bool
== Int
0
then
Doc ()
"Cannot apply"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann
fname'
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"as function, as it has type:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
ftype)
else
Doc ()
"Cannot apply"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann
fname'
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"to argument #"
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (Int
prev_applied forall a. Num a => a -> a -> a
+ Int
1)
forall a. Doc a -> Doc a -> Doc a
<+> 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 Size
argexp)
forall a. Semigroup a => a -> a -> a
<> Doc ()
","
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann
fname'
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"only takes"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Int
prev_applied
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
arguments
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
arguments :: Doc ()
arguments
| Int
prev_applied forall a. Eq a => a -> a -> Bool
== Int
1 = Doc ()
"argument"
| Bool
otherwise = Doc ()
"arguments"
checkOneExp :: UncheckedExp -> TypeM ([TypeParam], Exp)
checkOneExp :: ExpBase NoInfo Name -> TypeM ([TypeParamBase VName], Size)
checkOneExp ExpBase NoInfo Name
e = forall a.
(ExpBase NoInfo Name -> TermTypeM Size) -> TermTypeM a -> TypeM a
runTermTypeM ExpBase NoInfo Name -> TermTypeM Size
checkExp forall a b. (a -> b) -> a -> b
$ do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
let t :: StructType
t = Size -> StructType
typeOf Size
e'
([TypeParamBase VName]
tparams, [Pat ParamType]
_, ResRetType
_) <-
Name
-> SrcLoc
-> [TypeParamBase VName]
-> [Pat ParamType]
-> TypeBase Size Uniqueness
-> TermTypeM ([TypeParamBase VName], [Pat ParamType], ResRetType)
letGeneralise ([Char] -> Name
nameFromString [Char]
"<exp>") (forall a. Located a => a -> SrcLoc
srclocOf ExpBase NoInfo Name
e) [] [] forall a b. (a -> b) -> a -> b
$ forall u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
t
Set VName -> TermTypeM ()
fixOverloadedTypes forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> Set VName
typeVars StructType
t
Size
e'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes Size
e'
Size -> TermTypeM ()
localChecks Size
e''
Size -> TermTypeM ()
causalityCheck Size
e''
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams, Size
e'')
checkSizeExp :: UncheckedExp -> TypeM Exp
checkSizeExp :: ExpBase NoInfo Name -> TypeM Size
checkSizeExp ExpBase NoInfo Name
e = forall a.
(ExpBase NoInfo Name -> TermTypeM Size) -> TermTypeM a -> TypeM a
runTermTypeM ExpBase NoInfo Name -> TermTypeM Size
checkExp forall a b. (a -> b) -> a -> b
$ do
Size
e' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
e
let t :: StructType
t = Size -> StructType
typeOf Size
e'
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Size -> Bool
hasBinding Size
e') forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError (forall a. Located a => a -> SrcLoc
srclocOf Size
e') forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"size-expression-bind" forall a b. (a -> b) -> a -> b
$
Doc ()
"Size expression with binding is forbidden."
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage Size
e' Text
"Size expression") StructType
t (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. PrimType -> ScalarTypeBase dim u
Prim (IntType -> PrimType
Signed IntType
Int64)))
forall e. ASTMappable e => e -> TermTypeM e
updateTypes Size
e'
causalityCheck :: Exp -> TermTypeM ()
causalityCheck :: Size -> TermTypeM ()
causalityCheck Size
binding_body = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let checkCausality :: Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
what Set VName
known TypeBase Size u
t a
loc
| (VName
d, SrcLoc
dloc) : [(VName, SrcLoc)]
_ <-
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {a} {a}.
Ord a =>
Map a (a, Constraint) -> Set a -> a -> Maybe (a, SrcLoc)
unknown Constraints
constraints Set VName
known) forall a b. (a -> b) -> a -> b
$
forall a. Set a -> [a]
S.toList (FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> FV
freeInType TypeBase Size u
t) =
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall {v} {a} {b} {b}.
(IsName v, Pretty a, Located b) =>
Doc () -> Loc -> v -> b -> a -> Either TypeError b
causality Doc ()
what (forall a. Located a => a -> Loc
locOf a
loc) VName
d SrcLoc
dloc TypeBase Size u
t
| Bool
otherwise = forall a. Maybe a
Nothing
checkParamCausality :: Set VName
-> Pat (TypeBase Size u) -> Maybe (t (Either TypeError) a)
checkParamCausality Set VName
known Pat (TypeBase Size u)
p =
forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality (forall a ann. Pretty a => a -> Doc ann
pretty Pat (TypeBase Size u)
p) Set VName
known (forall d u. Pat (TypeBase d u) -> TypeBase d u
patternType Pat (TypeBase Size u)
p) (forall a. Located a => a -> Loc
locOf Pat (TypeBase Size u)
p)
collectingNewKnown :: StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown = 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 a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT forall a. Monoid a => a
mempty
onExp ::
S.Set VName ->
Exp ->
StateT (S.Set VName) (Either TypeError) Exp
onExp :: Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known (Var QualName VName
v (Info StructType
t) SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality (forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
v)) Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (ProjectSection [Name]
_ (Info StructType
t) SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"projection section" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (IndexSection [DimIndex]
_ (Info StructType
t) SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"projection section" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (OpSectionRight QualName VName
_ (Info StructType
t) Size
_ (Info (PName, ParamType), Info (PName, ParamType, Maybe VName))
_ Info ResRetType
_ SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"operator section" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (OpSectionLeft QualName VName
_ (Info StructType
t) Size
_ (Info (PName, ParamType, Maybe VName), Info (PName, ParamType))
_ (Info ResRetType, Info [VName])
_ SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"operator section" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (ArrayLit [] (Info StructType
t) SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"empty array" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known (Hole (Info StructType
t) SrcLoc
loc)
| Just StateT (Set VName) (Either TypeError) Size
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality Doc ()
"hole" Set VName
known StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) Size
bad
onExp Set VName
known e :: Size
e@(Lambda [Pat ParamType]
params Size
body Maybe (TypeExp Info VName)
_ Info ResRetType
_ SrcLoc
_)
| StateT (Set VName) (Either TypeError) Size
bad : [StateT (Set VName) (Either TypeError) Size]
_ <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {t :: (* -> *) -> * -> *} {u} {a}.
(MonadTrans t, Pretty u) =>
Set VName
-> Pat (TypeBase Size u) -> Maybe (t (Either TypeError) a)
checkParamCausality Set VName
known) [Pat ParamType]
params =
StateT (Set VName) (Either TypeError) Size
bad
| Bool
otherwise = do
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known Size
body
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
onExp Set VName
known e :: Size
e@(AppExp (LetPat [SizeBinder VName]
_ Pat StructType
_ Size
bindee_e Size
body_e SrcLoc
_) (Info AppRes
res)) = do
Set VName
-> Size
-> Size
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Size
bindee_e Size
body_e forall a b. (a -> b) -> a -> b
$ AppRes -> [VName]
appResExt AppRes
res
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
onExp Set VName
known e :: Size
e@(AppExp (Match Size
scrutinee NonEmpty (CaseBase Info VName)
cs SrcLoc
_) (Info AppRes
res)) = do
Set VName
new_known <- forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known Size
scrutinee
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall {a}.
ASTMappable a =>
Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse (Set VName
new_known forall a. Semigroup a => a -> a -> a
<> Set VName
known) NonEmpty (CaseBase Info VName)
cs
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
new_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res)) <>)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
onExp Set VName
known e :: Size
e@(AppExp (Apply Size
f NonEmpty (Info (Diet, Maybe VName), Size)
args SrcLoc
_) (Info AppRes
res)) = do
forall {a}.
Set VName
-> [(Info (a, Maybe VName), Size)]
-> StateT (Set VName) (Either TypeError) ()
seqArgs Set VName
known forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Info (Diet, Maybe VName), Size)
args
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
where
seqArgs :: Set VName
-> [(Info (a, Maybe VName), Size)]
-> StateT (Set VName) (Either TypeError) ()
seqArgs Set VName
known' [] = do
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known' Size
f
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res) <>)
seqArgs Set VName
known' ((Info (a
_, Maybe VName
p), Size
x) : [(Info (a, Maybe VName), Size)]
xs) = do
Set VName
new_known <- forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known' Size
x
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName
-> [(Info (a, Maybe VName), Size)]
-> StateT (Set VName) (Either TypeError) ()
seqArgs (Set VName
new_known forall a. Semigroup a => a -> a -> a
<> Set VName
known') [(Info (a, Maybe VName), Size)]
xs
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
new_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (forall a. Maybe a -> [a]
maybeToList Maybe VName
p)) <>)
onExp Set VName
known e :: Size
e@(Constr Name
v [Size]
args (Info StructType
t) SrcLoc
loc) = do
Set VName -> [Size] -> StateT (Set VName) (Either TypeError) ()
seqArgs Set VName
known [Size]
args
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
where
seqArgs :: Set VName -> [Size] -> StateT (Set VName) (Either TypeError) ()
seqArgs Set VName
known' []
| Just StateT (Set VName) (Either TypeError) ()
bad <- forall {t :: (* -> *) -> * -> *} {u} {a} {a}.
(MonadTrans t, Pretty u, Located a) =>
Doc ()
-> Set VName
-> TypeBase Size u
-> a
-> Maybe (t (Either TypeError) a)
checkCausality (forall ann. Doc ann -> Doc ann
dquotes (Doc ()
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Name
v)) Set VName
known' StructType
t SrcLoc
loc =
StateT (Set VName) (Either TypeError) ()
bad
| Bool
otherwise =
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
seqArgs Set VName
known' (Size
x : [Size]
xs) = do
Set VName
new_known <- forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known' Size
x
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> [Size] -> StateT (Set VName) (Either TypeError) ()
seqArgs (Set VName
new_known forall a. Semigroup a => a -> a -> a
<> Set VName
known') [Size]
xs
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Set VName
new_known <>)
onExp
Set VName
known
e :: Size
e@(AppExp (BinOp (QualName VName
f, SrcLoc
floc) Info StructType
ft (Size
x, Info Maybe VName
xp) (Size
y, Info Maybe VName
yp) SrcLoc
_) (Info AppRes
res)) = do
Set VName
args_known <-
forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName
-> Size
-> Size
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Size
x Size
y forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe VName
xp, Maybe VName
yp]
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp (Set VName
args_known forall a. Semigroup a => a -> a -> a
<> Set VName
known) (forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var QualName VName
f Info StructType
ft SrcLoc
floc)
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
args_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res)) <>)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
onExp Set VName
known e :: Size
e@(AppExp AppExpBase Info VName
e' (Info AppRes
res)) = do
forall {a}.
ASTMappable a =>
Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known AppExpBase Info VName
e'
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList (AppRes -> [VName]
appResExt AppRes
res))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
onExp Set VName
known Size
e = do
forall {a}.
ASTMappable a =>
Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known Size
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
e
recurse :: Set VName -> a -> StateT (Set VName) (Either TypeError) ()
recurse Set VName
known = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper (StateT (Set VName) (Either TypeError))
mapper
where
mapper :: ASTMapper (StateT (Set VName) (Either TypeError))
mapper = forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Size -> StateT (Set VName) (Either TypeError) Size
mapOnExp = Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known}
sequencePoint :: Set VName
-> Size
-> Size
-> [VName]
-> StateT (Set VName) (Either TypeError) ()
sequencePoint Set VName
known Size
x Size
y [VName]
ext = do
Set VName
new_known <- forall {a}.
StateT (Set VName) (Either TypeError) a
-> StateT (Set VName) (Either TypeError) (Set VName)
collectingNewKnown forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp Set VName
known Size
x
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp (Set VName
new_known forall a. Semigroup a => a -> a -> a
<> Set VName
known) Size
y
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set VName
new_known forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [VName]
ext) <>)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Set VName -> Size -> StateT (Set VName) (Either TypeError) Size
onExp forall a. Monoid a => a
mempty Size
binding_body) forall a. Monoid a => a
mempty
where
unknown :: Map a (a, Constraint) -> Set a -> a -> Maybe (a, SrcLoc)
unknown Map a (a, Constraint)
constraints Set a
known a
v = do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ a
v forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set a
known
SrcLoc
loc <- case forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
v Map a (a, Constraint)
constraints of
Just (UnknownSize SrcLoc
loc RigidSource
_) -> forall a. a -> Maybe a
Just SrcLoc
loc
Maybe Constraint
_ -> forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
v, SrcLoc
loc)
causality :: Doc () -> Loc -> v -> b -> a -> Either TypeError b
causality Doc ()
what Loc
loc v
d b
dloc a
t =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"causality-check" forall a b. (a -> b) -> a -> b
$
Doc ()
"Causality check: size"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"needed for type of"
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
what
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty a
t)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"But"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is computed at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel Loc
loc b
dloc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
""
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Hint:"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
align
( forall a. Text -> Doc a
textwrap Text
"Bind the expression producing"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
d)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with 'let' beforehand."
)
mustBeIrrefutable :: (MonadTypeChecker f) => Pat StructType -> f ()
mustBeIrrefutable :: forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable Pat StructType
p = do
case [Pat StructType] -> [Match ()]
unmatched [Pat StructType
p] of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
[Match ()]
ps' ->
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Pat StructType
p forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"refutable-pattern" forall a b. (a -> b) -> a -> b
$
Doc ()
"Refutable pattern not allowed here.\nUnmatched cases:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Match ()]
ps'))
localChecks :: Exp -> TermTypeM ()
localChecks :: Size -> TermTypeM ()
localChecks = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size -> TermTypeM Size
check
where
check :: Size -> TermTypeM Size
check e :: Size
e@(AppExp (Match Size
_ NonEmpty (CaseBase Info VName)
cs SrcLoc
loc) Info AppRes
_) = do
let ps :: NonEmpty (Pat StructType)
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(CasePat Pat StructType
p Size
_ SrcLoc
_) -> Pat StructType
p) NonEmpty (CaseBase Info VName)
cs
case [Pat StructType] -> [Match ()]
unmatched forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Pat StructType)
ps of
[] -> Size -> TermTypeM Size
recurse Size
e
[Match ()]
ps' ->
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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unmatched-cases" forall a b. (a -> b) -> a -> b
$
Doc ()
"Unmatched cases in match expression:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Match ()]
ps'))
check e :: Size
e@(AppExp (LetPat [SizeBinder VName]
_ Pat StructType
p Size
_ Size
_ SrcLoc
_) Info AppRes
_) =
forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable Pat StructType
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Size -> TermTypeM Size
recurse Size
e
check e :: Size
e@(Lambda [Pat ParamType]
ps Size
_ Maybe (TypeExp Info VName)
_ Info ResRetType
_ SrcLoc
_) =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct) [Pat ParamType]
ps forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Size -> TermTypeM Size
recurse Size
e
check e :: Size
e@(AppExp (LetFun VName
_ ([TypeParamBase VName]
_, [Pat ParamType]
ps, Maybe (TypeExp Info VName)
_, Info ResRetType
_, Size
_) Size
_ SrcLoc
_) Info AppRes
_) =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct) [Pat ParamType]
ps forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Size -> TermTypeM Size
recurse Size
e
check e :: Size
e@(AppExp (Loop [VName]
_ Pat ParamType
p Size
_ LoopFormBase Info VName
form Size
_ SrcLoc
_) Info AppRes
_) = do
forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p)
case LoopFormBase Info VName
form of
ForIn Pat StructType
form_p Size
_ -> forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable Pat StructType
form_p
LoopFormBase Info VName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Size -> TermTypeM Size
recurse Size
e
check e :: Size
e@(IntLit Integer
x Info StructType
ty SrcLoc
loc) =
Size
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info StructType
ty of
Info (Scalar (Prim PrimType
t)) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. Integral a => a -> PrimType -> Bool
inBoundsI Integer
x PrimType
t) Integer
x PrimType
t SrcLoc
loc
Info StructType
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Inferred type of int literal is not a number"
check e :: Size
e@(FloatLit Double
x Info StructType
ty SrcLoc
loc) =
Size
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info StructType
ty of
Info (Scalar (Prim (FloatType FloatType
t))) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. RealFloat a => a -> FloatType -> Bool
inBoundsF Double
x FloatType
t) Double
x FloatType
t SrcLoc
loc
Info StructType
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Inferred type of float literal is not a float"
check e :: Size
e@(Negate (IntLit Integer
x Info StructType
ty SrcLoc
loc1) SrcLoc
loc2) =
Size
e forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ case Info StructType
ty of
Info (Scalar (Prim PrimType
t)) -> forall {f :: * -> *} {loc} {a} {a}.
(MonadTypeChecker f, Located loc, Pretty a, Pretty a) =>
Bool -> a -> a -> loc -> f ()
errorBounds (forall {a}. Integral a => a -> PrimType -> Bool
inBoundsI (-Integer
x) PrimType
t) (-Integer
x) PrimType
t (SrcLoc
loc1 forall a. Semigroup a => a -> a -> a
<> SrcLoc
loc2)
Info StructType
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Inferred type of int literal is not a number"
check e :: Size
e@(AppExp (BinOp (QualName [] VName
v, SrcLoc
_) Info StructType
_ (Size
x, Info (Maybe VName)
_) (Size, Info (Maybe VName))
_ SrcLoc
loc) Info AppRes
_)
| VName -> Name
baseName VName
v forall a. Eq a => a -> a -> Bool
== Name
"==",
Array {} <- Size -> StructType
typeOf Size
x,
VName -> Int
baseTag VName
v forall a. Ord a => a -> a -> Bool
<= Int
maxIntrinsicTag = do
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$
forall a. Text -> Doc a
textwrap
Text
"Comparing arrays with \"==\" is deprecated and will stop working in a future revision of the language."
Size -> TermTypeM Size
recurse Size
e
check Size
e = Size -> TermTypeM Size
recurse Size
e
recurse :: Size -> TermTypeM Size
recurse = forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap forall (m :: * -> *). Monad m => ASTMapper m
identityMapper {mapOnExp :: Size -> TermTypeM Size
mapOnExp = Size -> TermTypeM Size
check}
bitWidth :: IntType -> Int
bitWidth IntType
ty = Int
8 forall a. Num a => a -> a -> a
* forall a. Num a => IntType -> a
intByteSize IntType
ty :: Int
inBoundsI :: a -> PrimType -> Bool
inBoundsI a
x (Signed IntType
t) = a
x forall a. Ord a => a -> a -> Bool
>= -a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (IntType -> Int
bitWidth IntType
t forall a. Num a => a -> a -> a
- Int
1) Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (IntType -> Int
bitWidth IntType
t forall a. Num a => a -> a -> a
- Int
1)
inBoundsI a
x (Unsigned IntType
t) = a
x forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x forall a. Ord a => a -> a -> Bool
< a
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntType -> Int
bitWidth IntType
t
inBoundsI a
x (FloatType FloatType
Float16) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Half)
inBoundsI a
x (FloatType FloatType
Float32) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Float)
inBoundsI a
x (FloatType FloatType
Float64) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x :: Double)
inBoundsI a
_ PrimType
Bool = forall a. HasCallStack => [Char] -> a
error [Char]
"Inferred type of int literal is not a number"
inBoundsF :: a -> FloatType -> Bool
inBoundsF a
x FloatType
Float16 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Real a, Fractional b) => a -> b
realToFrac a
x :: Float)
inBoundsF a
x FloatType
Float32 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite (forall a b. (Real a, Fractional b) => a -> b
realToFrac a
x :: Float)
inBoundsF a
x FloatType
Float64 = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => a -> Bool
isInfinite a
x
errorBounds :: Bool -> a -> a -> loc -> f ()
errorBounds Bool
inBounds a
x a
ty loc
loc =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
inBounds forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError loc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"literal-out-of-bounds" forall a b. (a -> b) -> a -> b
$
Doc ()
"Literal "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
x
forall a. Semigroup a => a -> a -> a
<> Doc ()
" out of bounds for inferred type "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
ty
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
checkFunDef ::
( Name,
Maybe UncheckedTypeExp,
[UncheckedTypeParam],
[UncheckedPat ParamType],
UncheckedExp,
SrcLoc
) ->
TypeM
( VName,
[TypeParam],
[Pat ParamType],
Maybe (TypeExp Info VName),
ResRetType,
Exp
)
checkFunDef :: (Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
[PatBase NoInfo Name ParamType], ExpBase NoInfo Name, SrcLoc)
-> TypeM
(VName, [TypeParamBase VName], [Pat ParamType],
Maybe (TypeExp Info VName), ResRetType, Size)
checkFunDef (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name ParamType]
params, ExpBase NoInfo Name
body, SrcLoc
loc) =
forall a.
(ExpBase NoInfo Name -> TermTypeM Size) -> TermTypeM a -> TypeM a
runTermTypeM ExpBase NoInfo Name -> TermTypeM Size
checkExp forall a b. (a -> b) -> a -> b
$ do
([TypeParamBase VName]
tparams', [Pat ParamType]
params', Maybe (TypeExp Info VName)
maybe_retdecl', RetType [VName]
dims TypeBase Size Uniqueness
rettype', Size
body') <-
(Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
[PatBase NoInfo Name ParamType], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
([TypeParamBase VName], [Pat ParamType],
Maybe (TypeExp Info VName), ResRetType, Size)
checkBinding (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name ParamType]
params, ExpBase NoInfo Name
body, SrcLoc
loc)
Set VName -> TermTypeM ()
fixOverloadedTypes forall a b. (a -> b) -> a -> b
$
forall dim as. TypeBase dim as -> Set VName
typeVars TypeBase Size Uniqueness
rettype' forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall dim as. TypeBase dim as -> Set VName
typeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall d u. Pat (TypeBase d u) -> TypeBase d u
patternType) [Pat ParamType]
params'
Size
body'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes Size
body'
[Pat ParamType]
params'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes [Pat ParamType]
params'
Maybe (TypeExp Info VName)
maybe_retdecl'' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall e. ASTMappable e => e -> TermTypeM e
updateTypes Maybe (TypeExp Info VName)
maybe_retdecl'
TypeBase Size Uniqueness
rettype'' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size Uniqueness
rettype'
Size -> TermTypeM ()
causalityCheck Size
body''
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (f :: * -> *). MonadTypeChecker f => Pat StructType -> f ()
mustBeIrrefutable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct) [Pat ParamType]
params'
Size -> TermTypeM ()
localChecks Size
body''
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
fname)] forall a b. (a -> b) -> a -> b
$ do
VName
fname' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
fname SrcLoc
loc
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
fname forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
doNotShadow) forall a b. (a -> b) -> a -> b
$
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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"may-not-be-redefined" forall a b. (a -> b) -> a -> b
$
Doc ()
"The" forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName Name
fname forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"operator may not be redefined."
let ((Size
body''', ResRetType
updated_ret), [TypeError]
errors) =
(VName, [Pat ParamType], Size, ResRetType,
Maybe (TypeExp Info VName), SrcLoc)
-> ((Size, ResRetType), [TypeError])
Consumption.checkValDef
( VName
fname',
[Pat ParamType]
params'',
Size
body'',
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size Uniqueness
rettype'',
Maybe (TypeExp Info VName)
maybe_retdecl'',
SrcLoc
loc
)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [TypeError]
errors
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
fname', [TypeParamBase VName]
tparams', [Pat ParamType]
params'', Maybe (TypeExp Info VName)
maybe_retdecl'', ResRetType
updated_ret, Size
body''')
fixOverloadedTypes :: Names -> TermTypeM ()
fixOverloadedTypes :: Set VName -> TermTypeM ()
fixOverloadedTypes Set VName
tyvars_at_toplevel =
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}.
(MonadUnify m, MonadTypeChecker m) =>
(VName, Constraint) -> m ()
fixOverloaded forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall a b. (a, b) -> b
snd
where
fixOverloaded :: (VName, Constraint) -> m ()
fixOverloaded (VName
v, Overloaded [PrimType]
ots Usage
usage)
| IntType -> PrimType
Signed IntType
Int32 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ots = do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar forall a. Monoid a => a
mempty (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int32)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to i32."
| FloatType -> PrimType
FloatType FloatType
Float64 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ots = do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar forall a. Monoid a => a
mempty (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ FloatType -> PrimType
FloatType FloatType
Float64)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to f64."
| Bool
otherwise =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
Doc ()
"Type is ambiguous (could be one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ots)
forall a. Semigroup a => a -> a -> a
<> Doc ()
")."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Add a type annotation to disambiguate the type."
fixOverloaded (VName
v, NoConstraint Liftedness
_ Usage
usage) = do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar forall a. Monoid a => a
mempty (forall v. v -> QualName v
qualName VName
v) [])) forall a b. (a -> b) -> a -> b
$
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [])
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
tyvars_at_toplevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Usage
usage Doc ()
"Defaulting ambiguous type to ()."
fixOverloaded (VName
_, Equality Usage
usage) =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
Doc ()
"Type is ambiguous (must be equality type)."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Add a type annotation to disambiguate the type."
fixOverloaded (VName
_, HasFields Liftedness
_ Map Name StructType
fs Usage
usage) =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
Doc ()
"Type is ambiguous. Must be record with fields:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
stack forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {ann}. (Pretty a, Pretty a) => (a, a) -> Doc ann
field forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Add a type annotation to disambiguate the type."
where
field :: (a, a) -> Doc ann
field (a
l, a
t) = forall a ann. Pretty a => a -> Doc ann
pretty a
l forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty a
t)
fixOverloaded (VName
_, HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
usage) =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Usage
usage forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-type" forall a b. (a -> b) -> a -> b
$
Doc ()
"Type is ambiguous (must be a sum type with constructors:"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum Map Name [StructType]
cs)
forall a. Semigroup a => a -> a -> a
<> Doc ()
")."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Add a type annotation to disambiguate the type."
fixOverloaded (VName
v, Size Maybe Size
Nothing (Usage Maybe Text
Nothing 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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-size" forall a b. (a -> b) -> a -> b
$
Doc ()
"Ambiguous size" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
fixOverloaded (VName
v, Size Maybe Size
Nothing (Usage (Just Text
u) 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 a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"ambiguous-size" forall a b. (a -> b) -> a -> b
$
Doc ()
"Ambiguous size" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"arising from" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Text
u forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
fixOverloaded (VName, Constraint)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
hiddenParamNames :: [Pat ParamType] -> [VName]
hiddenParamNames :: [Pat ParamType] -> [VName]
hiddenParamNames [Pat ParamType]
params = [VName]
hidden
where
param_all_names :: [VName]
param_all_names = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. Pat t -> [VName]
patNames [Pat ParamType]
params
named :: (PName, b, c) -> Maybe VName
named (Named VName
x, b
_, c
_) = forall a. a -> Maybe a
Just VName
x
named (PName
Unnamed, b
_, c
_) = forall a. Maybe a
Nothing
param_names :: Set VName
param_names =
forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {b} {c}. (PName, b, c) -> Maybe VName
named forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat ParamType -> (PName, Diet, StructType)
patternParam) [Pat ParamType]
params
hidden :: [VName]
hidden = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set VName
param_names) [VName]
param_all_names
inferredReturnType :: SrcLoc -> [Pat ParamType] -> StructType -> TermTypeM StructType
inferredReturnType :: SrcLoc -> [Pat ParamType] -> StructType -> TermTypeM StructType
inferredReturnType SrcLoc
loc [Pat ParamType]
params StructType
t = do
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType SrcLoc
loc [VName]
hidden_params StructType
t
where
hidden_params :: [VName]
hidden_params = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
hidden) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall t. Pat t -> [VName]
patNames [Pat ParamType]
params
hidden :: [VName]
hidden = [Pat ParamType] -> [VName]
hiddenParamNames [Pat ParamType]
params
checkBinding ::
( Name,
Maybe UncheckedTypeExp,
[UncheckedTypeParam],
[UncheckedPat ParamType],
UncheckedExp,
SrcLoc
) ->
TermTypeM
( [TypeParam],
[Pat ParamType],
Maybe (TypeExp Info VName),
ResRetType,
Exp
)
checkBinding :: (Name, Maybe UncheckedTypeExp, [TypeParamBase Name],
[PatBase NoInfo Name ParamType], ExpBase NoInfo Name, SrcLoc)
-> TermTypeM
([TypeParamBase VName], [Pat ParamType],
Maybe (TypeExp Info VName), ResRetType, Size)
checkBinding (Name
fname, Maybe UncheckedTypeExp
maybe_retdecl, [TypeParamBase Name]
tparams, [PatBase NoInfo Name ParamType]
params, ExpBase NoInfo Name
body, SrcLoc
loc) =
forall a. TermTypeM a -> TermTypeM a
incLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[TypeParamBase Name]
-> [PatBase NoInfo Name ParamType]
-> ([TypeParamBase VName] -> [Pat ParamType] -> TermTypeM a)
-> TermTypeM a
bindingParams [TypeParamBase Name]
tparams [PatBase NoInfo Name ParamType]
params forall a b. (a -> b) -> a -> b
$ \[TypeParamBase VName]
tparams' [Pat ParamType]
params' -> do
Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
maybe_retdecl' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse UncheckedTypeExp
-> TermTypeM
(TypeExp Info VName, TypeBase Size Uniqueness, [VName])
checkTypeExpNonrigid Maybe UncheckedTypeExp
maybe_retdecl
Size
body' <-
[Pat ParamType]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size Uniqueness)
-> SrcLoc
-> TermTypeM Size
checkFunBody
[Pat ParamType]
params'
ExpBase NoInfo Name
body
((\(TypeExp Info VName
_, TypeBase Size Uniqueness
x, [VName]
_) -> TypeBase Size Uniqueness
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
maybe_retdecl')
(forall b a. b -> (a -> b) -> Maybe a -> b
maybe SrcLoc
loc forall a. Located a => a -> SrcLoc
srclocOf Maybe UncheckedTypeExp
maybe_retdecl)
[Pat ParamType]
params'' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [Pat ParamType]
params'
StructType
body_t <- Size -> TermTypeM StructType
expTypeFully Size
body'
(Maybe (TypeExp Info VName)
maybe_retdecl'', TypeBase Size Uniqueness
rettype) <- case Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
maybe_retdecl' of
Just (TypeExp Info VName
retdecl', TypeBase Size Uniqueness
ret, [VName]
_) -> do
TypeBase Size Uniqueness
ret' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase Size Uniqueness
ret
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just TypeExp Info VName
retdecl', TypeBase Size Uniqueness
ret')
Maybe (TypeExp Info VName, TypeBase Size Uniqueness, [VName])
Nothing
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatBase NoInfo Name ParamType]
params ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
body_t)
| Bool
otherwise -> do
StructType
body_t' <- SrcLoc -> [Pat ParamType] -> StructType -> TermTypeM StructType
inferredReturnType SrcLoc
loc [Pat ParamType]
params'' StructType
body_t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Maybe a
Nothing, forall u. Uniqueness -> TypeBase Size u -> TypeBase Size Uniqueness
toRes Uniqueness
Nonunique StructType
body_t')
Maybe Name -> [Pat ParamType] -> TermTypeM ()
verifyFunctionParams (forall a. a -> Maybe a
Just Name
fname) [Pat ParamType]
params''
([TypeParamBase VName]
tparams'', [Pat ParamType]
params''', ResRetType
rettype') <-
Name
-> SrcLoc
-> [TypeParamBase VName]
-> [Pat ParamType]
-> TypeBase Size Uniqueness
-> TermTypeM ([TypeParamBase VName], [Pat ParamType], ResRetType)
letGeneralise Name
fname SrcLoc
loc [TypeParamBase VName]
tparams' [Pat ParamType]
params''
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall u. TypeBase Size u -> TermTypeM (TypeBase Size u)
unscopeUnknown TypeBase Size Uniqueness
rettype
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
( forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatBase NoInfo Name ParamType]
params
Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParamBase VName]
tparams''
Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall dim as. RetTypeBase dim as -> [VName]
retDims ResRetType
rettype'))
)
forall a b. (a -> b) -> a -> b
$ 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
$ forall a. Text -> Doc a
textwrap Text
"A size-polymorphic value binding may not have a type with an existential size."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Type of this binding is:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty ResRetType
rettype')
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"with the following type parameters:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a. [Doc a] -> Doc a
sep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParamBase VName]
tparams'')
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams'', [Pat ParamType]
params''', Maybe (TypeExp Info VName)
maybe_retdecl'', ResRetType
rettype', Size
body')
sizeNamesPos :: TypeBase Size als -> S.Set VName
sizeNamesPos :: forall als. TypeBase Size als -> Set VName
sizeNamesPos (Scalar (Arrow als
_ PName
_ Diet
_ StructType
t1 (RetType [VName]
_ TypeBase Size Uniqueness
t2))) = forall als. TypeBase Size als -> Set VName
onParam StructType
t1 forall a. Semigroup a => a -> a -> a
<> forall als. TypeBase Size als -> Set VName
sizeNamesPos TypeBase Size Uniqueness
t2
where
onParam :: TypeBase Size als -> S.Set VName
onParam :: forall als. TypeBase Size als -> Set VName
onParam (Scalar Arrow {}) = forall a. Monoid a => a
mempty
onParam (Scalar (Record Map Name (TypeBase Size als)
fs)) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall als. TypeBase Size als -> Set VName
onParam forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name (TypeBase Size als)
fs
onParam (Scalar (TypeVar als
_ QualName VName
_ [TypeArg Size]
targs)) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> Set VName
onTypeArg [TypeArg Size]
targs
onParam TypeBase Size als
t = FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> FV
freeInType TypeBase Size als
t
onTypeArg :: TypeArg Size -> Set VName
onTypeArg (TypeArgDim (Var QualName VName
d Info StructType
_ SrcLoc
_)) = forall a. a -> Set a
S.singleton forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
d
onTypeArg (TypeArgDim Size
_) = forall a. Monoid a => a
mempty
onTypeArg (TypeArgType StructType
t) = forall als. TypeBase Size als -> Set VName
onParam StructType
t
sizeNamesPos TypeBase Size als
_ = forall a. Monoid a => a
mempty
verifyFunctionParams :: Maybe Name -> [Pat ParamType] -> TermTypeM ()
verifyFunctionParams :: Maybe Name -> [Pat ParamType] -> TermTypeM ()
verifyFunctionParams Maybe Name
fname [Pat ParamType]
params =
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Maybe Name -> Checking
CheckingParams Maybe Name
fname) forall a b. (a -> b) -> a -> b
$
forall {m :: * -> *}.
MonadTypeChecker m =>
[VName] -> [Pat ParamType] -> m ()
verifyParams (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall t. Pat t -> [VName]
patNames [Pat ParamType]
params) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. ASTMappable e => e -> TermTypeM e
updateTypes [Pat ParamType]
params
where
verifyParams :: [VName] -> [Pat ParamType] -> m ()
verifyParams [VName]
forbidden (Pat ParamType
p : [Pat ParamType]
ps)
| VName
d : [VName]
_ <- forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
forbidden) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. Pat (TypeBase Size u) -> FV
freeInPat Pat ParamType
p =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError Pat ParamType
p forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"inaccessible-size" forall a b. (a -> b) -> a -> b
$
Doc ()
"Parameter"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Pat ParamType
p)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"refers to size"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"which will not be accessible to the caller"
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"possibly because it is nested in a tuple or record."
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"Consider ascribing an explicit type that does not reference "
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
| Bool
otherwise = [VName] -> [Pat ParamType] -> m ()
verifyParams [VName]
forbidden' [Pat ParamType]
ps
where
forbidden' :: [VName]
forbidden' =
case Pat ParamType -> (PName, Diet, StructType)
patternParam Pat ParamType
p of
(Named VName
v, Diet
_, StructType
_) -> forall a. Eq a => a -> [a] -> [a]
delete VName
v [VName]
forbidden
(PName, Diet, StructType)
_ -> [VName]
forbidden
verifyParams [VName]
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
injectExt :: [VName] -> TypeBase Size u -> RetTypeBase Size u
injectExt :: forall u. [VName] -> TypeBase Size u -> RetTypeBase Size u
injectExt [] TypeBase Size u
ret = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size u
ret
injectExt [VName]
ext TypeBase Size u
ret = forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext_here forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> TypeBase Size u
deeper TypeBase Size u
ret
where
(Set VName
immediate, Set VName
_) = forall u. TypeBase Size u -> (Set VName, Set VName)
dimUses TypeBase Size u
ret
([VName]
ext_here, [VName]
ext_there) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
immediate) [VName]
ext
deeper :: TypeBase Size u -> TypeBase Size u
deeper :: forall u. TypeBase Size u -> TypeBase Size u
deeper (Scalar (Prim PrimType
t)) = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
t
deeper (Scalar (Record Map Name (TypeBase Size u)
fs)) = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall u. TypeBase Size u -> TypeBase Size u
deeper Map Name (TypeBase Size u)
fs
deeper (Scalar (Sum Map Name [TypeBase Size u]
cs)) = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall a b. (a -> b) -> [a] -> [b]
map forall u. TypeBase Size u -> TypeBase Size u
deeper) Map Name [TypeBase Size u]
cs
deeper (Scalar (Arrow u
als PName
p Diet
d1 StructType
t1 (RetType [VName]
t2_ext TypeBase Size Uniqueness
t2))) =
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u
-> PName
-> Diet
-> TypeBase dim NoUniqueness
-> RetTypeBase dim Uniqueness
-> ScalarTypeBase dim u
Arrow u
als PName
p Diet
d1 StructType
t1 forall a b. (a -> b) -> a -> b
$ forall u. [VName] -> TypeBase Size u -> RetTypeBase Size u
injectExt (forall a. Ord a => [a] -> [a]
nubOrd ([VName]
ext_there forall a. Semigroup a => a -> a -> a
<> [VName]
t2_ext)) TypeBase Size Uniqueness
t2
deeper (Scalar (TypeVar u
u QualName VName
tn [TypeArg Size]
targs)) =
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar u
u QualName VName
tn forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> TypeArg Size
deeperArg [TypeArg Size]
targs
deeper t :: TypeBase Size u
t@Array {} = TypeBase Size u
t
deeperArg :: TypeArg Size -> TypeArg Size
deeperArg (TypeArgType StructType
t) = forall dim. TypeBase dim NoUniqueness -> TypeArg dim
TypeArgType forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> TypeBase Size u
deeper StructType
t
deeperArg (TypeArgDim Size
d) = forall dim. dim -> TypeArg dim
TypeArgDim Size
d
closeOverTypes ::
Name ->
SrcLoc ->
[TypeParam] ->
[StructType] ->
ResType ->
Constraints ->
TermTypeM ([TypeParam], ResRetType)
closeOverTypes :: Name
-> SrcLoc
-> [TypeParamBase VName]
-> [StructType]
-> TypeBase Size Uniqueness
-> Constraints
-> TermTypeM ([TypeParamBase VName], ResRetType)
closeOverTypes Name
defname SrcLoc
defloc [TypeParamBase VName]
tparams [StructType]
paramts TypeBase Size Uniqueness
ret Constraints
substs = do
([TypeParamBase VName]
more_tparams, [VName]
retext) <-
forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes
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 {f :: * -> *}.
(MonadUnify f, MonadTypeChecker f) =>
(VName, Constraint)
-> f (Maybe (Either (TypeParamBase VName) VName))
closeOver (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall a b. (a, b) -> b
snd Constraints
to_close_over)
let mkExt :: VName -> Maybe VName
mkExt VName
v =
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
substs of
Just (Int
_, UnknownSize {}) -> forall a. a -> Maybe a
Just VName
v
Maybe (Int, Constraint)
_ -> forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( [TypeParamBase VName]
tparams forall a. [a] -> [a] -> [a]
++ [TypeParamBase VName]
more_tparams,
forall u. [VName] -> TypeBase Size u -> RetTypeBase Size u
injectExt (forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ [VName]
retext forall a. [a] -> [a] -> [a]
++ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VName -> Maybe VName
mkExt (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ forall u. TypeBase Size u -> FV
freeInType TypeBase Size Uniqueness
ret)) TypeBase Size Uniqueness
ret
)
where
t :: StructType
t = [ParamType] -> ResRetType -> StructType
foldFunType (forall a b. (a -> b) -> [a] -> [b]
map (forall u. Diet -> TypeBase Size u -> ParamType
toParam Diet
Observe) [StructType]
paramts) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size Uniqueness
ret
to_close_over :: Constraints
to_close_over = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\VName
k (Int, Constraint)
_ -> VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
visible) Constraints
substs
visible :: Set VName
visible = forall dim as. TypeBase dim as -> Set VName
typeVars StructType
t forall a. Semigroup a => a -> a -> a
<> FV -> Set VName
fvVars (forall u. TypeBase Size u -> FV
freeInType StructType
t)
(Set VName
produced_sizes, Set VName
param_sizes) = forall u. TypeBase Size u -> (Set VName, Set VName)
dimUses StructType
t
closeOver :: (VName, Constraint)
-> f (Maybe (Either (TypeParamBase VName) VName))
closeOver (VName
k, Constraint
_)
| VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParamBase VName]
tparams =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
closeOver (VName
k, NoConstraint Liftedness
l Usage
usage) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l VName
k forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Usage
usage
closeOver (VName
k, ParamType Liftedness
l SrcLoc
loc) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l VName
k SrcLoc
loc
closeOver (VName
k, Size Maybe Size
Nothing Usage
usage) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim VName
k forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Usage
usage
closeOver (VName
k, UnknownSize SrcLoc
_ RigidSource
_)
| VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
param_sizes,
VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
produced_sizes = do
Notes
notes <- forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes SrcLoc
defloc forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName (forall v. v -> QualName v
qualName VName
k) forall a. Monoid a => a
mempty
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
defloc Notes
notes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unknown-param-def" forall a b. (a -> b) -> a -> b
$
Doc ()
"Unknown size"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
k)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"in parameter of"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName Name
defname)
forall a. Semigroup a => a -> a -> a
<> Doc ()
", which is inferred as:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t)
| VName
k forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
produced_sizes =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right VName
k
closeOver (VName
_, Constraint
_) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
letGeneralise ::
Name ->
SrcLoc ->
[TypeParam] ->
[Pat ParamType] ->
ResType ->
TermTypeM ([TypeParam], [Pat ParamType], ResRetType)
letGeneralise :: Name
-> SrcLoc
-> [TypeParamBase VName]
-> [Pat ParamType]
-> TypeBase Size Uniqueness
-> TermTypeM ([TypeParamBase VName], [Pat ParamType], ResRetType)
letGeneralise Name
defname SrcLoc
defloc [TypeParamBase VName]
tparams [Pat ParamType]
params TypeBase Size Uniqueness
restype =
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (Name -> Checking
CheckingLetGeneralise Name
defname) forall a b. (a -> b) -> a -> b
$ do
Constraints
now_substs <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let keep_type_vars :: Set VName
keep_type_vars = Constraints -> Set VName
overloadedTypeVars Constraints
now_substs
Int
cur_lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
let candidate :: VName -> (Int, b) -> Bool
candidate VName
k (Int
lvl, b
_) = (VName
k forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
keep_type_vars) Bool -> Bool -> Bool
&& Int
lvl forall a. Ord a => a -> a -> Bool
>= (Int
cur_lvl forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pat ParamType]
params)
new_substs :: Constraints
new_substs = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall {b}. VName -> (Int, b) -> Bool
candidate Constraints
now_substs
([TypeParamBase VName]
tparams', RetType [VName]
ret_dims TypeBase Size Uniqueness
restype') <-
Name
-> SrcLoc
-> [TypeParamBase VName]
-> [StructType]
-> TypeBase Size Uniqueness
-> Constraints
-> TermTypeM ([TypeParamBase VName], ResRetType)
closeOverTypes
Name
defname
SrcLoc
defloc
[TypeParamBase VName]
tparams
(forall a b. (a -> b) -> [a] -> [b]
map forall u. Pat (TypeBase Size u) -> StructType
patternStructType [Pat ParamType]
params)
TypeBase Size Uniqueness
restype
Constraints
new_substs
TypeBase Size Uniqueness
restype'' <- forall e. ASTMappable e => e -> TermTypeM e
updateTypes TypeBase Size Uniqueness
restype'
let used_sizes :: FV
used_sizes =
forall u. TypeBase Size u -> FV
freeInType TypeBase Size Uniqueness
restype'' forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall u. TypeBase Size u -> FV
freeInType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall d u. Pat (TypeBase d u) -> TypeBase d u
patternType) [Pat ParamType]
params
case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.notMember` FV -> Set VName
fvVars FV
used_sizes) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vn. TypeParamBase vn -> vn
typeParamName) forall a b. (a -> b) -> a -> b
$
forall a. (a -> Bool) -> [a] -> [a]
filter forall vn. TypeParamBase vn -> Bool
isSizeParam [TypeParamBase VName]
tparams' of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
TypeParamBase VName
tp : [TypeParamBase VName]
_ -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize forall a b. (a -> b) -> a -> b
$ forall vn. vn -> SrcLoc -> SizeBinder vn
SizeBinder (forall vn. TypeParamBase vn -> vn
typeParamName TypeParamBase VName
tp) (forall a. Located a => a -> SrcLoc
srclocOf TypeParamBase VName
tp)
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall a b. (a -> b) -> a -> b
$ \VName
k (Int, Constraint)
_ -> VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParamBase VName]
tparams'
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TypeParamBase VName]
tparams', [Pat ParamType]
params, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ret_dims TypeBase Size Uniqueness
restype'')
checkFunBody ::
[Pat ParamType] ->
UncheckedExp ->
Maybe ResType ->
SrcLoc ->
TermTypeM Exp
checkFunBody :: [Pat ParamType]
-> ExpBase NoInfo Name
-> Maybe (TypeBase Size Uniqueness)
-> SrcLoc
-> TermTypeM Size
checkFunBody [Pat ParamType]
params ExpBase NoInfo Name
body Maybe (TypeBase Size Uniqueness)
maybe_rettype SrcLoc
loc = do
Size
body' <- ExpBase NoInfo Name -> TermTypeM Size
checkExp ExpBase NoInfo Name
body
case Maybe (TypeBase Size Uniqueness)
maybe_rettype of
Just TypeBase Size Uniqueness
rettype -> do
StructType
body_t <- Size -> TermTypeM StructType
expTypeFully Size
body'
let hidden :: [VName]
hidden = [Pat ParamType] -> [VName]
hiddenParamNames [Pat ParamType]
params
(StructType
body_t', [VName]
_) <-
forall as.
SrcLoc
-> [VName]
-> TypeBase Size as
-> TermTypeM (TypeBase Size as, [VName])
unscopeType
SrcLoc
loc
(forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
hidden) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall t. Pat t -> [VName]
patNames [Pat ParamType]
params)
StructType
body_t
let usage :: Usage
usage = forall a. Located a => a -> Text -> Usage
mkUsage ExpBase NoInfo Name
body Text
"return type annotation"
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size Uniqueness -> StructType -> Checking
CheckingReturn TypeBase Size Uniqueness
rettype StructType
body_t') forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Size Uniqueness
rettype) StructType
body_t'
Maybe (TypeBase Size Uniqueness)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
body'
arrayOfM ::
SrcLoc ->
StructType ->
Shape Size ->
TermTypeM StructType
arrayOfM :: SrcLoc -> StructType -> Shape Size -> TermTypeM StructType
arrayOfM SrcLoc
loc StructType
t Shape Size
shape = do
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> Text -> TypeBase dim u -> m ()
arrayElemType (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"use as array element") Text
"type used in array" StructType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim.
Shape dim -> TypeBase dim NoUniqueness -> TypeBase dim NoUniqueness
arrayOf Shape Size
shape StructType
t