Safe Haskell	Safe-Inferred
Language	Haskell2010

Traq.ProtoLang.TypeCheck

Contents

Typing Context
Typeable size types
Types
Checkers
Accessors

Synopsis

type TypingCtx size = Context (VarType size)
class HasTypingCtx p where
- _typingCtx :: size ~ SizeType p => Lens' p (TypingCtx size)
type TypingReqs size = (Eq size, Show size, Num size)
tbool :: Num size => VarType size
type TypingEnv ext = FunCtx ext
type TypeChecker ext = RWST (TypingEnv ext) () (TypingCtx (SizeType ext)) (Either String)
class (TypingReqs size, size ~ SizeType ext) => TypeInferrable ext size | ext -> size where
- inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => ext -> m [VarType size]
typeCheckBasicExpr :: forall size m. (TypingReqs size, MonadError String m, MonadReader (TypingCtx size) m) => BasicExpr size -> m (VarType size)
typeCheckFun :: (TypeInferrable primT size, size ~ SizeType primT) => FunCtx primT -> FunDef primT -> Either String ()
typeCheckProg :: TypeInferrable primT size => Program primT -> Either String ()
lookupFunE :: (MonadError String m, MonadReader r m, HasFunCtx r primT, size ~ SizeType r) => Ident -> m (FunDef primT)

Typing Context

type TypingCtx size = Context (VarType size) #

A context mapping variables to their types.

class HasTypingCtx p where #

Methods

_typingCtx :: size ~ SizeType p => Lens' p (TypingCtx size) #

Instances

Instances details

HasTypingCtx (CheckingCtx size) #
Instance details Defined in Traq.CQPL.TypeCheck Methods _typingCtx :: size0 ~ SizeType (CheckingCtx size) => Lens' (CheckingCtx size) (TypingCtx size0) #
HasTypingCtx (LoweringCtx size) #
Instance details Defined in Traq.Compiler.Prelude Methods _typingCtx :: size0 ~ SizeType (LoweringCtx size) => Lens' (LoweringCtx size) (TypingCtx size0) #
HasTypingCtx (TypingCtx size) #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods _typingCtx :: size0 ~ SizeType (TypingCtx size) => Lens' (TypingCtx size) (TypingCtx size0) #

Typeable size types

type TypingReqs size = (Eq size, Show size, Num size) #

Type size that can be type-checked.

tbool :: Num size => VarType size #

Boolean type in our language.

Types

type TypingEnv ext = FunCtx ext #

Environment for type checking

type TypeChecker ext = RWST (TypingEnv ext) () (TypingCtx (SizeType ext)) (Either String) #

The TypeChecker monad

class (TypingReqs size, size ~ SizeType ext) => TypeInferrable ext size | ext -> size where #

Minimal complete definition

Nothing

Methods

inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => ext -> m [VarType size] #

default inferTypes :: forall ext' m. (Generic ext, GTypeInferrable (Rep ext) size, m ~ TypeChecker ext', size ~ SizeType ext') => ext -> m [VarType size] #

Instances

Instances details

TypeInferrable ext size => TypeInferrable (AnnFailProb ext) size #
Instance details Defined in Traq.Analysis.Annotate.Prelude Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => AnnFailProb ext -> m [VarType size] #
(TypeCheckPrim prim size, TypingReqs size) => TypeInferrable (Primitive prim) size #
Instance details Defined in Traq.Primitives.Class Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => Primitive prim -> m [VarType size] #
TypingReqs size => TypeInferrable (DistrExpr size) size #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => DistrExpr size -> m [VarType size] #
TypeInferrable ext size => TypeInferrable (Expr ext) size #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => Expr ext -> m [VarType size] #
TypeInferrable ext size => TypeInferrable (Stmt ext) size #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => Stmt ext -> m [VarType size] #
TypingReqs size => TypeInferrable (TreeSearch size prec) size #
Instance details Defined in Traq.Primitives.TreeSearch Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => TreeSearch size prec -> m [VarType size] #
TypingReqs size => TypeInferrable (Core size prec) size #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', size ~ SizeType ext') => Core size prec -> m [VarType size] #

Checkers

typeCheckBasicExpr :: forall size m. (TypingReqs size, MonadError String m, MonadReader (TypingCtx size) m) => BasicExpr size -> m (VarType size) #

typeCheckFun :: (TypeInferrable primT size, size ~ SizeType primT) => FunCtx primT -> FunDef primT -> Either String () #

Type check a single function.

typeCheckProg :: TypeInferrable primT size => Program primT -> Either String () #

Type check a full program (i.e. list of functions).

Accessors

lookupFunE :: (MonadError String m, MonadReader r m, HasFunCtx r primT, size ~ SizeType r) => Ident -> m (FunDef primT) #