Safe Haskell	Safe-Inferred
Language	Haskell2010

Traq.ProtoLang.TypeCheck

Contents

Typing Context
Typeable size types
Types
Checkers
Accessors

Synopsis

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

Typing Context

type TypingCtx sizeT = Context (VarType sizeT) #

A context mapping variables to their types.

class HasTypingCtx p where #

Methods

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

Instances

Instances details

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

Typeable size types

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

Type sizeT that can be type-checked.

tbool :: Num sizeT => VarType sizeT #

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 sizeT, sizeT ~ SizeType ext) => TypeInferrable ext sizeT | ext -> sizeT where #

Minimal complete definition

Nothing

Methods

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

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

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 sizeT => TypeInferrable (DistrExpr sizeT) sizeT #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', sizeT ~ SizeType ext') => DistrExpr sizeT -> m [VarType sizeT] #
TypeInferrable ext sizeT => TypeInferrable (Expr ext) sizeT #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', sizeT ~ SizeType ext') => Expr ext -> m [VarType sizeT] #
TypeInferrable ext sizeT => TypeInferrable (Stmt ext) sizeT #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', sizeT ~ SizeType ext') => Stmt ext -> m [VarType sizeT] #
TypingReqs sizeT => TypeInferrable (TreeSearch sizeT precT) sizeT #
Instance details Defined in Traq.Primitives.TreeSearch Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', sizeT ~ SizeType ext') => TreeSearch sizeT precT -> m [VarType sizeT] #
TypingReqs sizeT => TypeInferrable (Core sizeT precT) sizeT #
Instance details Defined in Traq.ProtoLang.TypeCheck Methods inferTypes :: forall ext' m. (m ~ TypeChecker ext', sizeT ~ SizeType ext') => Core sizeT precT -> m [VarType sizeT] #

Checkers

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

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

Type check a single function.

typeCheckProg :: TypeInferrable primT sizeT => 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, sizeT ~ SizeType r) => Ident -> m (FunDef primT) #