Language.Futhark.TypeChecker.Terms.Monad

Facilities for type-checking terms. Factored out of Language.Futhark.TypeChecker.Terms to prevent the module from being gigantic.

Incidentally also a nice place to put Haddock comments to make the internal API of the type checker easier to browse.

Documentation

data TermTypeM a

Instances

Applicative TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

pure :: a -> TermTypeM a

(<*>) :: TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b

liftA2 :: (a -> b -> c) -> TermTypeM a -> TermTypeM b -> TermTypeM c

(*>) :: TermTypeM a -> TermTypeM b -> TermTypeM b

(<*) :: TermTypeM a -> TermTypeM b -> TermTypeM a

Functor TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

fmap :: (a -> b) -> TermTypeM a -> TermTypeM b

(<$) :: a -> TermTypeM b -> TermTypeM a

Monad TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(>>=) :: TermTypeM a -> (a -> TermTypeM b) -> TermTypeM b

(>>) :: TermTypeM a -> TermTypeM b -> TermTypeM b

return :: a -> TermTypeM a

MonadTypeChecker TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

warn :: Located loc => loc -> Doc () -> TermTypeM ()

warnings :: Warnings -> TermTypeM ()

newName :: VName -> TermTypeM VName

newID :: Name -> TermTypeM VName

newTypeName :: Name -> TermTypeM VName

bindVal :: VName -> BoundV -> TermTypeM a -> TermTypeM a

lookupType :: QualName VName -> TermTypeM ([TypeParam], StructRetType, Liftedness)

typeError :: Located loc => loc -> Notes -> Doc () -> TermTypeM a

MonadUnify TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

getConstraints :: TermTypeM Constraints

putConstraints :: Constraints -> TermTypeM ()

modifyConstraints :: (Constraints -> Constraints) -> TermTypeM ()

newTypeVar :: (Monoid als, Located a) => a -> Name -> TermTypeM (TypeBase dim als)

newDimVar :: Usage -> Rigidity -> Name -> TermTypeM VName

newRigidDim :: Located a => a -> RigidSource -> Name -> TermTypeM VName

newFlexibleDim :: Usage -> Name -> TermTypeM VName

curLevel :: TermTypeM Level

matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> TermTypeM a

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> TermTypeM a

MonadError TypeError TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

throwError :: TypeError -> TermTypeM a

catchError :: TermTypeM a -> (TypeError -> TermTypeM a) -> TermTypeM a

MonadReader TermEnv TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ask :: TermTypeM TermEnv

local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a

reader :: (TermEnv -> a) -> TermTypeM a

MonadState TermTypeState TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

get :: TermTypeM TermTypeState

put :: TermTypeState -> TermTypeM ()

state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a

runTermTypeM :: (ExpBase NoInfo VName -> TermTypeM Exp) -> TermTypeM a -> TypeM a

data ValBinding

Constructors

BoundV [TypeParam] StructType

OverloadedF [PrimType] [Maybe PrimType] (Maybe PrimType)

EqualityF

Instances

Show ValBinding

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> ValBinding -> ShowS

show :: ValBinding -> String

showList :: [ValBinding] -> ShowS

data SizeSource

What was the source of some existential size? This is used for using the same existential variable if the same source is encountered in multiple locations.

Constructors

SourceSlice (Maybe Size) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName)) (Maybe (ExpBase NoInfo VName))

Instances

Show SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> SizeSource -> ShowS

show :: SizeSource -> String

showList :: [SizeSource] -> ShowS

Eq SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(==) :: SizeSource -> SizeSource -> Bool

(/=) :: SizeSource -> SizeSource -> Bool

Ord SizeSource

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

compare :: SizeSource -> SizeSource -> Ordering

(<) :: SizeSource -> SizeSource -> Bool

(<=) :: SizeSource -> SizeSource -> Bool

(>) :: SizeSource -> SizeSource -> Bool

(>=) :: SizeSource -> SizeSource -> Bool

max :: SizeSource -> SizeSource -> SizeSource

min :: SizeSource -> SizeSource -> SizeSource

data Inferred t

Constructors

NoneInferred

Ascribed t

Instances

Functor Inferred

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

fmap :: (a -> b) -> Inferred a -> Inferred b

(<$) :: a -> Inferred b -> Inferred a

data Checking

Constructors

CheckingApply (Maybe (QualName VName)) Exp StructType StructType

CheckingReturn ResType StructType

CheckingAscription StructType StructType

CheckingLetGeneralise Name

CheckingParams (Maybe Name)

CheckingPat (PatBase NoInfo VName StructType) (Inferred StructType)

CheckingLoopBody StructType StructType

CheckingLoopInitial StructType StructType

CheckingRecordUpdate [Name] StructType StructType

CheckingRequired [StructType] StructType

CheckingBranches StructType StructType

Instances

Pretty Checking

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

pretty :: Checking -> Doc ann

prettyList :: [Checking] -> Doc ann

withEnv :: TermEnv -> Env -> TermEnv

localScope :: (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a

data TermEnv

Type checking happens with access to this environment. The TermScope will be extended during type-checking as bindings come into scope.

Constructors

TermEnv

Fields

• termScope :: TermScope
• termChecking :: Maybe Checking
• termLevel :: Level
• termChecker :: ExpBase NoInfo VName -> TermTypeM Exp
• termOuterEnv :: Env
• termImportName :: ImportName

Instances

MonadReader TermEnv TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

ask :: TermTypeM TermEnv

local :: (TermEnv -> TermEnv) -> TermTypeM a -> TermTypeM a

reader :: (TermEnv -> a) -> TermTypeM a

data TermScope

Constructors

TermScope

Fields

• scopeVtable :: Map VName ValBinding
• scopeTypeTable :: Map VName TypeBinding
• scopeModTable :: Map VName Mod

Instances

Semigroup TermScope

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

(<>) :: TermScope -> TermScope -> TermScope

sconcat :: NonEmpty TermScope -> TermScope

stimes :: Integral b => b -> TermScope -> TermScope

Show TermScope

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

showsPrec :: Int -> TermScope -> ShowS

show :: TermScope -> String

showList :: [TermScope] -> ShowS

data TermTypeState

The state is a set of constraints and a counter for generating type names. This is distinct from the usual counter we use for generating unique names, as these will be user-visible.

Constructors

TermTypeState

Fields

• stateConstraints :: Constraints
• stateCounter :: !Int
• stateWarnings :: Warnings
• stateNameSource :: VNameSource

Instances

MonadState TermTypeState TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

get :: TermTypeM TermTypeState

put :: TermTypeState -> TermTypeM ()

state :: (TermTypeState -> (a, TermTypeState)) -> TermTypeM a

onFailure :: Checking -> TermTypeM a -> TermTypeM a

extSize :: SrcLoc -> SizeSource -> TermTypeM (Size, Maybe VName)

expType :: Exp -> TermTypeM StructType

Get the type of an expression, with top level type variables substituted. Never call typeOf directly (except in a few carefully inspected locations)!

expTypeFully :: Exp -> TermTypeM StructType

Get the type of an expression, with all type variables substituted. Slower than expType, but sometimes necessary. Never call typeOf directly (except in a few carefully inspected locations)!

constrain :: VName -> Constraint -> TermTypeM ()

newArrayType :: Usage -> Name -> Int -> TermTypeM (StructType, StructType)

allDimsFreshInType :: Usage -> Rigidity -> Name -> TypeBase Size als -> TermTypeM (TypeBase Size als, Map VName Size)

Replace *all* dimensions with distinct fresh size variables.

updateTypes :: ASTMappable e => e -> TermTypeM e

Replace all type variables with their concrete types.

type Names = Set VName

Primitive checking

unifies :: Text -> StructType -> Exp -> TermTypeM Exp

require :: Text -> [PrimType] -> Exp -> TermTypeM Exp

require ts e causes a TypeError if expType e is not one of the types in ts. Otherwise, simply returns e.

checkTypeExpNonrigid :: TypeExp (ExpBase NoInfo VName) VName -> TermTypeM (TypeExp Exp VName, ResType, [VName])

lookupVar :: SrcLoc -> QualName VName -> TermTypeM StructType

lookupMod :: QualName VName -> TermTypeM Mod

Sizes

isInt64 :: Exp -> Maybe Int64

Control flow

incLevel :: TermTypeM a -> TermTypeM a

Errors

unusedSize :: MonadTypeChecker m => SizeBinder VName -> m a