Safe Haskell | None |
---|
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.
- data Config n = Config {}
- configOfProfile :: Profile n -> Config n
- checkModule :: (Ord n, Show n, Pretty n) => Config n -> Module a n -> Either (Error a n) (Module (AnTEC a n) n)
- checkExp :: (Ord n, Show n, Pretty n) => Config n -> KindEnv n -> TypeEnv n -> Exp a n -> Either (Error a n) (Exp (AnTEC a n) n, Type n, Effect n, Closure n)
- typeOfExp :: (Ord n, Pretty n, Show n) => Config n -> KindEnv n -> TypeEnv n -> Exp a n -> Either (Error a n) (Type n)
- checkWitness :: (Ord n, Show n, Pretty n) => Config n -> KindEnv n -> TypeEnv n -> Witness n -> Either (Error a n) (Type n)
- typeOfWitness :: (Ord n, Show n, Pretty n) => Config n -> Witness n -> Either (Error a n) (Type n)
- typeOfWiCon :: WiCon n -> Type n
- data AnTEC a n = AnTEC {
- annotType :: Type n
- annotEffect :: Effect n
- annotClosure :: Closure n
- annotTail :: a
- data Error a n
- = ErrorType {
- errorTypeError :: Error n
- | ErrorMalformedType {
- errorChecking :: Exp a n
- errorType :: Type n
- | ErrorExportUndefined {
- errorName :: n
- | ErrorExportMismatch {
- errorName :: n
- errorExportType :: Type n
- errorDefType :: Type n
- | ErrorMalformedExp {
- errorChecking :: Exp a n
- | ErrorUndefinedVar {
- errorBound :: Bound n
- errorUniverse :: Universe
- | ErrorVarAnnotMismatch {
- errorBound :: Bound n
- errorTypeAnnot :: Type n
- errorTypeEnv :: Type n
- | ErrorUndefinedCtor {
- errorChecking :: Exp a n
- | ErrorAppMismatch {
- errorChecking :: Exp a n
- errorParamType :: Type n
- errorArgType :: Type n
- | ErrorAppNotFun {
- errorChecking :: Exp a n
- errorNotFunType :: Type n
- errorArgType :: Type n
- | ErrorLamShadow {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLamNotPure {
- errorChecking :: Exp a n
- errorSpecOrWit :: Bool
- errorEffect :: Effect n
- | ErrorLamBindNotData { }
- | ErrorLamBodyNotData { }
- | ErrorLetMismatch { }
- | ErrorLetBindingNotData { }
- | ErrorLetBodyNotData { }
- | ErrorLetLazyNotPure {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorEffect :: Effect n
- | ErrorLetLazyNotEmpty {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorClosure :: Closure n
- | ErrorLetLazyNoWitness { }
- | ErrorLetLazyWitnessTypeMismatch {
- errorChecking :: Exp a n
- errorBind :: Bind n
- errorWitnessTypeHave :: Type n
- errorBindType :: Type n
- errorWitnessTypeExpect :: Type n
- | ErrorLetrecBindingNotLambda {
- errorChecking :: Exp a n
- errorExp :: Exp a n
- | ErrorLetrecRebound {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLetRegionsNotRegion {
- errorChecking :: Exp a n
- errorBinds :: [Bind n]
- errorKinds :: [Kind n]
- | ErrorLetRegionsRebound {
- errorChecking :: Exp a n
- errorBinds :: [Bind n]
- | ErrorLetRegionFree {
- errorChecking :: Exp a n
- errorBinds :: [Bind n]
- errorType :: Type n
- | ErrorLetRegionWitnessInvalid {
- errorChecking :: Exp a n
- errorBind :: Bind n
- | ErrorLetRegionWitnessConflict {
- errorChecking :: Exp a n
- errorBindWitness1 :: Bind n
- errorBindWitness2 :: Bind n
- | ErrorLetRegionsWitnessOther {
- errorChecking :: Exp a n
- errorBoundRegions :: [Bound n]
- errorBindWitness :: Bind n
- | ErrorLetRegionWitnessFree {
- errorChecking :: Exp a n
- errorBindWitness :: Bind n
- | ErrorWithRegionNotRegion {
- errorChecking :: Exp a n
- errorBound :: Bound n
- errorKind :: Kind n
- | ErrorWithRegionFree {
- errorChecking :: Exp a n
- errorBound :: Bound n
- errorType :: Type n
- | ErrorWAppMismatch {
- errorWitness :: Witness n
- errorParamType :: Type n
- errorArgType :: Type n
- | ErrorWAppNotCtor {
- errorWitness :: Witness n
- errorNotFunType :: Type n
- errorArgType :: Type n
- | ErrorCannotJoin {
- errorWitness :: Witness n
- errorWitnessLeft :: Witness n
- errorTypeLeft :: Type n
- errorWitnessRight :: Witness n
- errorTypeRight :: Type n
- | ErrorWitnessNotPurity {
- errorChecking :: Exp a n
- errorWitness :: Witness n
- errorType :: Type n
- | ErrorWitnessNotEmpty {
- errorChecking :: Exp a n
- errorWitness :: Witness n
- errorType :: Type n
- | ErrorCaseScrutineeNotAlgebraic {
- errorChecking :: Exp a n
- errorTypeScrutinee :: Type n
- | ErrorCaseScrutineeTypeUndeclared {
- errorChecking :: Exp a n
- errorTypeScrutinee :: Type n
- | ErrorCaseNoAlternatives {
- errorChecking :: Exp a n
- | ErrorCaseNonExhaustive {
- errorChecking :: Exp a n
- errorCtorNamesMissing :: [n]
- | ErrorCaseNonExhaustiveLarge {
- errorChecking :: Exp a n
- | ErrorCaseOverlapping {
- errorChecking :: Exp a n
- | ErrorCaseTooManyBinders {
- errorChecking :: Exp a n
- errorCtorDaCon :: DaCon n
- errorCtorFields :: Int
- errorPatternFields :: Int
- | ErrorCaseCannotInstantiate {
- errorChecking :: Exp a n
- errorTypeScrutinee :: Type n
- errorTypeCtor :: Type n
- | ErrorCaseScrutineeTypeMismatch {
- errorChecking :: Exp a n
- errorTypeScrutinee :: Type n
- errorTypePattern :: Type n
- | ErrorCaseFieldTypeMismatch {
- errorChecking :: Exp a n
- errorTypeAnnot :: Type n
- errorTypeField :: Type n
- | ErrorCaseAltResultMismatch {
- errorChecking :: Exp a n
- errorAltType1 :: Type n
- errorAltType2 :: Type n
- | ErrorWeakEffNotEff {
- errorChecking :: Exp a n
- errorEffect :: Effect n
- errorKind :: Kind n
- | ErrorNakedType {
- errorChecking :: Exp a n
- | ErrorNakedWitness {
- errorChecking :: Exp a n
- = ErrorType {
Configuration
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.
Config | |
|
configOfProfile :: Profile n -> Config nSource
Convert a langage profile to a type checker configuration.
Checking Modules
:: (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
:: (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.
:: (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
:: (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
The type checker adds this annotation to every node in the AST, giving its type, effect and closure.
AnTEC | |
|
Error messages
All the things that can go wrong when type checking an expression or witness.
ErrorType | Found a kind error when checking a type. |
| |
ErrorMalformedType | Found a malformed type, and we don't have a more specific diagnosis. |
| |
ErrorExportUndefined | Exported value is undefined. |
| |
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. |
| |
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. |
| |
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. |
| |
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. |
ErrorLamBodyNotData | An abstraction where the body does not have data kind. |
ErrorLetMismatch | A let-expression where the type of the binder does not match the right of the binding. |
ErrorLetBindingNotData | A let-expression where the right of the binding does not have data kind. |
ErrorLetBodyNotData | A let-expression where the body does not have data kind. |
ErrorLetLazyNotPure | A lazy let binding that has a visible side effect. |
| |
ErrorLetLazyNotEmpty | A lazy let binding with a non-empty closure. |
| |
ErrorLetLazyNoWitness | A lazy let binding without a witness that binding is in a lazy region. |
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. |
| |
ErrorLetrecRebound | A recursive let-expression that has more than one binding with the same name. |
| |
ErrorLetRegionsNotRegion | A letregion-expression where the some of the bound variables do not have region kind. |
| |
ErrorLetRegionsRebound | A letregion-expression that tried to shadow some pre-existing named region variables. |
| |
ErrorLetRegionFree | A letregion-expression where some of the the bound region variables are free in the type of the body. |
| |
ErrorLetRegionWitnessInvalid | A letregion-expression that tried to create a witness with an invalid type. |
| |
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. |
| |
ErrorWithRegionNotRegion | A withregion-expression where the handle does not have region kind. |
| |
ErrorWithRegionFree | A letregion-expression where some of the the bound region variables are free in the type of the body. |
| |
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. |
| |
ErrorWitnessNotEmpty | A witness provided for a forget cast that does not witness emptiness. |
| |
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. |
| |
ErrorCaseNonExhaustive | A case-expression where the alternatives don't cover all the possible data constructors. |
| |
ErrorCaseNonExhaustiveLarge | A case-expression where the alternatives don't cover all the possible constructors, and the type has too many data constructors to list. |
| |
ErrorCaseOverlapping | A case-expression with overlapping alternatives. |
| |
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. |
| |
ErrorNakedType | Found a naked |
| |
ErrorNakedWitness | Found a naked |
|