ddc-core-0.3.1.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellNone

DDC.Core.Check

Contents

Description

Type checker for the Disciple Core language.

The functions in this module do not check for language fragment compliance. This needs to be done separately via DDC.Core.Fragment.

Synopsis

Configuration

data Config n Source

Static configuration for the type checker. These fields don't change as we decend into the tree.

The starting configuration should be converted from the profile that defines the language fragment you are checking. See DDC.Core.Fragment and use configOfProfile below.

Constructors

Config 

Fields

configPrimDataDefs :: DataDefs n

Data type definitions.

configPrimKinds :: KindEnv n

Kinds of primitive types.

configPrimTypes :: TypeEnv n

Types of primitive operators.

configSuppressClosures :: Bool

Suppress all closure information, annotating all functions with an empty closure.

This is used when checking the Disciple Core Salt fragment, as transforms in this language don't use the closure information.

configOfProfile :: Profile n -> Config nSource

Convert a langage profile to a type checker configuration.

Checking Modules

checkModuleSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> Module a n

Module to check.

-> Either (Error a n) (Module (AnTEC a n) n) 

Type check a module.

If it's good, you get a new version with types attached to all the bound variables

If it's bad, you get a description of the error.

Checking Expressions

checkExpSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> KindEnv n

Starting Kind environment.

-> TypeEnv n

Strating Type environment.

-> Exp a n

Expression to check.

-> Either (Error a n) (Exp (AnTEC a n) n, Type n, Effect n, Closure n) 

Type check an expression.

If it's good, you get a new version with types attached to all the bound variables, as well its the type, effect and closure.

If it's bad, you get a description of the error.

The returned expression has types attached to all variable occurrences, so you can call typeOfExp on any open subterm.

The kinds and types of primitives are added to the environments automatically, you don't need to supply these as part of the starting environments.

typeOfExpSource

Arguments

:: (Ord n, Pretty n, Show n) 
=> Config n

Static configuration.

-> KindEnv n

Starting Kind environment

-> TypeEnv n

Starting Type environment.

-> Exp a n

Expression to check.

-> Either (Error a n) (Type n) 

Like checkExp, but only return the value type of an expression.

Checking Witnesses

checkWitnessSource

Arguments

:: (Ord n, Show n, Pretty n) 
=> Config n

Static configuration.

-> KindEnv n

Starting Kind Environment.

-> TypeEnv n

Strating Type Environment.

-> Witness n

Witness to check.

-> Either (Error a n) (Type n) 

Check a witness.

If it's good, you get a new version with types attached to all the bound variables, as well as the type of the overall witness.

If it's bad, you get a description of the error.

The returned expression has types attached to all variable occurrences, so you can call typeOfWitness on any open subterm.

The kinds and types of primitives are added to the environments automatically, you don't need to supply these as part of the starting environments.

typeOfWitness :: (Ord n, Show n, Pretty n) => Config n -> Witness n -> Either (Error a n) (Type n)Source

Like checkWitness, but check in an empty environment.

As this function is not given an environment, the types of free variables must be attached directly to the bound occurrences. This attachment is performed by checkWitness above.

typeOfWiCon :: WiCon n -> Type nSource

Take the type of a witness constructor.

Annotations

data AnTEC a n Source

The type checker adds this annotation to every node in the AST, giving its type, effect and closure.

Constructors

AnTEC 

Instances

Typeable2 AnTEC 
(Show a, Show n) => Show (AnTEC a n) 
Pretty (AnTEC a n) 
(NFData a, NFData n) => NFData (AnTEC a n) 

Error messages

data Error a n Source

All the things that can go wrong when type checking an expression or witness.

Constructors

ErrorType

Found a kind error when checking a type.

Fields

errorTypeError :: Error n
 
ErrorMalformedType

Found a malformed type, and we don't have a more specific diagnosis.

Fields

errorChecking :: Exp a n
 
errorType :: Type n
 
ErrorExportUndefined

Exported value is undefined.

Fields

errorName :: n
 
ErrorExportMismatch

Type signature of exported binding does not match the type at the definition site.

ErrorMalformedExp

Found a malformed expression, and we don't have a more specific diagnosis.

Fields

errorChecking :: Exp a n
 
ErrorUndefinedVar

An undefined type variable.

ErrorVarAnnotMismatch

A bound occurrence of a variable whose type annotation does not match the corresponding annotation in the environment.

ErrorUndefinedCtor

A data constructor that wasn't in the set of data definitions.

Fields

errorChecking :: Exp a n
 
ErrorAppMismatch

A function application where the parameter and argument don't match.

ErrorAppNotFun

Tried to apply something that is not a function.

ErrorLamShadow

A type abstraction that tries to shadow a type variable that is already in the environment.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLamNotPure

A type or witness abstraction where the body has a visible side effect.

ErrorLamBindNotData

A value function where the parameter does not have data kind.

Fields

errorChecking :: Exp a n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLamBodyNotData

An abstraction where the body does not have data kind.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLetMismatch

A let-expression where the type of the binder does not match the right of the binding.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorType :: Type n
 
ErrorLetBindingNotData

A let-expression where the right of the binding does not have data kind.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorKind :: Kind n
 
ErrorLetBodyNotData

A let-expression where the body does not have data kind.

Fields

errorChecking :: Exp a n
 
errorType :: Type n
 
errorKind :: Kind n
 
ErrorLetLazyNotPure

A lazy let binding that has a visible side effect.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorEffect :: Effect n
 
ErrorLetLazyNotEmpty

A lazy let binding with a non-empty closure.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorClosure :: Closure n
 
ErrorLetLazyNoWitness

A lazy let binding without a witness that binding is in a lazy region.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
errorType :: Type n
 
ErrorLetLazyWitnessTypeMismatch

A lazy let binding where the witness has the wrong type.

ErrorLetrecBindingNotLambda

A recursive let-expression where the right of the binding is not a lambda abstraction.

Fields

errorChecking :: Exp a n
 
errorExp :: Exp a n
 
ErrorLetrecRebound

A recursive let-expression that has more than one binding with the same name.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLetRegionsNotRegion

A letregion-expression where the some of the bound variables do not have region kind.

Fields

errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
errorKinds :: [Kind n]
 
ErrorLetRegionsRebound

A letregion-expression that tried to shadow some pre-existing named region variables.

Fields

errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
ErrorLetRegionFree

A letregion-expression where some of the the bound region variables are free in the type of the body.

Fields

errorChecking :: Exp a n
 
errorBinds :: [Bind n]
 
errorType :: Type n
 
ErrorLetRegionWitnessInvalid

A letregion-expression that tried to create a witness with an invalid type.

Fields

errorChecking :: Exp a n
 
errorBind :: Bind n
 
ErrorLetRegionWitnessConflict

A letregion-expression that tried to create conflicting witnesses.

ErrorLetRegionsWitnessOther

A letregion-expression where a bound witnesses was not for the the region variable being introduced.

ErrorLetRegionWitnessFree

A letregion-expression where the witness binding references some free region variable that is not the one being introduced.

Fields

errorChecking :: Exp a n
 
errorBindWitness :: Bind n
 
ErrorWithRegionNotRegion

A withregion-expression where the handle does not have region kind.

Fields

errorChecking :: Exp a n
 
errorBound :: Bound n
 
errorKind :: Kind n
 
ErrorWithRegionFree

A letregion-expression where some of the the bound region variables are free in the type of the body.

Fields

errorChecking :: Exp a n
 
errorBound :: Bound n
 
errorType :: Type n
 
ErrorWAppMismatch

A witness application where the argument type does not match the parameter type.

ErrorWAppNotCtor

Tried to perform a witness application with a non-witness.

ErrorCannotJoin

An invalid witness join.

ErrorWitnessNotPurity

A witness provided for a purify cast that does not witness purity.

Fields

errorChecking :: Exp a n
 
errorWitness :: Witness n
 
errorType :: Type n
 
ErrorWitnessNotEmpty

A witness provided for a forget cast that does not witness emptiness.

Fields

errorChecking :: Exp a n
 
errorWitness :: Witness n
 
errorType :: Type n
 
ErrorCaseScrutineeNotAlgebraic

A case-expression where the scrutinee type is not algebraic.

ErrorCaseScrutineeTypeUndeclared

A case-expression where the scrutinee type is not in our set of data type declarations.

ErrorCaseNoAlternatives

A case-expression with no alternatives.

Fields

errorChecking :: Exp a n
 
ErrorCaseNonExhaustive

A case-expression where the alternatives don't cover all the possible data constructors.

Fields

errorChecking :: Exp a n
 
errorCtorNamesMissing :: [n]
 
ErrorCaseNonExhaustiveLarge

A case-expression where the alternatives don't cover all the possible constructors, and the type has too many data constructors to list.

Fields

errorChecking :: Exp a n
 
ErrorCaseOverlapping

A case-expression with overlapping alternatives.

Fields

errorChecking :: Exp a n
 
ErrorCaseTooManyBinders

A case-expression where one of the patterns has too many binders.

ErrorCaseCannotInstantiate

A case-expression where the pattern types could not be instantiated with the arguments of the scrutinee type.

ErrorCaseScrutineeTypeMismatch

A case-expression where the type of the scrutinee does not match the type of the pattern.

ErrorCaseFieldTypeMismatch

A case-expression where the annotation on a pattern variable binder does not match the field type of the constructor.

ErrorCaseAltResultMismatch

A case-expression where the result types of the alternatives are not identical.

ErrorWeakEffNotEff

A weakeff-cast where the type provided does not have effect kind.

Fields

errorChecking :: Exp a n
 
errorEffect :: Effect n
 
errorKind :: Kind n
 
ErrorNakedType

Found a naked XType that wasn't the argument of an application.

Fields

errorChecking :: Exp a n
 
ErrorNakedWitness

Found a naked XWitness that wasn't the argument of an application.

Fields

errorChecking :: Exp a n
 

Instances

(Show a, Show n) => Show (Error a n) 
(Show n, Eq n, Pretty n) => Pretty (Error a n)