| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
DDC.Core.Load
Description
"Loading" refers to the combination of parsing and type checking. This is the easiest way to turn source tokens into a type-checked abstract syntax tree.
- data AnTEC a n = AnTEC {
- annotType :: Type n
- annotEffect :: Effect n
- annotClosure :: Closure n
- annotTail :: a
- data Error n err
- = ErrorRead !String
- | ErrorParser !ParseError
- | ErrorCheckType !(Error SourcePos n)
- | ErrorCheckExp !(Error SourcePos n)
- | ErrorCompliance !(Error (AnTEC SourcePos n) n)
- | ErrorFragment !(err (AnTEC SourcePos n))
- data Mode n
- data CheckTrace = CheckTrace {
- checkTraceDoc :: Doc
- loadModuleFromFile :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> FilePath -> Mode n -> IO (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace)
- loadModuleFromString :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> FilePath -> Int -> Mode n -> String -> (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace)
- loadModuleFromTokens :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> FilePath -> Mode n -> [Located (Token n)] -> (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace)
- loadExpFromString :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> Map ModuleName (Module (AnTEC () n) n) -> FilePath -> Mode n -> String -> (Either (Error n err) (Exp (AnTEC SourcePos n) n), Maybe CheckTrace)
- loadExpFromTokens :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> Map ModuleName (Module (AnTEC () n) n) -> FilePath -> Mode n -> [Located (Token n)] -> (Either (Error n err) (Exp (AnTEC SourcePos n) n), Maybe CheckTrace)
- loadTypeFromString :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> Universe -> FilePath -> String -> Either (Error n err) (Type n, Kind n)
- loadTypeFromTokens :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> Universe -> FilePath -> [Located (Token n)] -> Either (Error n err) (Type n, Kind n)
- loadWitnessFromString :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> FilePath -> String -> Either (Error n err) (Witness (AnT SourcePos n) n, Type n)
- loadWitnessFromTokens :: (Eq n, Ord n, Show n, Pretty n) => Fragment n err -> FilePath -> [Located (Token n)] -> Either (Error n err) (Witness (AnT SourcePos n) n, Type n)
Documentation
The type checker adds this annotation to every node in the AST, giving its type, effect and closure.
Constructors
| AnTEC | |
Fields
| |
Things that can go wrong when loading a core thing.
Constructors
| ErrorRead !String | |
| ErrorParser !ParseError | |
| ErrorCheckType !(Error SourcePos n) | |
| ErrorCheckExp !(Error SourcePos n) | |
| ErrorCompliance !(Error (AnTEC SourcePos n) n) | |
| ErrorFragment !(err (AnTEC SourcePos n)) |
What mode we're performing type checking/inference in.
Constructors
| Recon | Reconstruct the type of the expression, requiring type annotations on parameters as well as type applications to already be present. |
| Synth [Exists n] | The ascending smoke of incense. Synthesise the type of the expression, producing unification variables for bidirectional type inference. Any new unification variables introduced may be used to define the given existentials, so the need to be declared outside their scopes. If the list is empty we can add new variables to the inner most scope. |
| Check (Type n) | The descending tongue of flame. Check the type of an expression against this expected type, and unify expected types into unification variables for bidirecional type inference. |
data CheckTrace Source #
Human readable trace of the type checker.
Constructors
| CheckTrace | |
Fields
| |
Instances
Loading modules
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> FilePath | File containing source code. |
| -> Mode n | Type checker mode. |
| -> IO (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace) |
Parse and type check a core module from a file.
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> FilePath | Path to source file for error messages. |
| -> Int | Starting line number for error messages. |
| -> Mode n | Type checker mode. |
| -> String | Program text. |
| -> (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace) |
Parse and type check a core module from a string.
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> FilePath | Path to source file for error messages. |
| -> Mode n | Type checker mode. |
| -> [Located (Token n)] | Source tokens. |
| -> (Either (Error n err) (Module (AnTEC SourcePos n) n), Maybe CheckTrace) |
Parse and type check a core module from some tokens.
Loading expressions
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> Map ModuleName (Module (AnTEC () n) n) | Other modules currently in scope. We add their exports to the environment. |
| -> FilePath | Path to source file for error messages. |
| -> Mode n | Type checker mode. |
| -> String | Source string. |
| -> (Either (Error n err) (Exp (AnTEC SourcePos n) n), Maybe CheckTrace) |
Parse and type-check and expression from a string.
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> Map ModuleName (Module (AnTEC () n) n) | Other modules currently in scope. We add their exports to the environment. |
| -> FilePath | Path to source file for error messages. |
| -> Mode n | Type checker mode. |
| -> [Located (Token n)] | Source tokens. |
| -> (Either (Error n err) (Exp (AnTEC SourcePos n) n), Maybe CheckTrace) |
Parse and check an expression returning it along with its spec, effect and closure
Loading types
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> Universe | Universe this type is supposed to be in. |
| -> FilePath | Path to source file for error messages. |
| -> String | Source string. |
| -> Either (Error n err) (Type n, Kind n) |
Parse and check a type from a string, returning it along with its kind.
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment definition. |
| -> Universe | Universe this type is supposed to be in. |
| -> FilePath | Path to source file for error messages. |
| -> [Located (Token n)] | Source tokens. |
| -> Either (Error n err) (Type n, Kind n) |
Parse and check a type from some tokens, returning it along with its kind.
Loading witnesses
loadWitnessFromString Source #
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment profile. |
| -> FilePath | Path to source file for error messages. |
| -> String | Source string. |
| -> Either (Error n err) (Witness (AnT SourcePos n) n, Type n) |
Parse and check a witness from a string, returning it along with its kind.
loadWitnessFromTokens Source #
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment profile. |
| -> FilePath | Path to source file for error messages. |
| -> [Located (Token n)] | Source tokens. |
| -> Either (Error n err) (Witness (AnT SourcePos n) n, Type n) |
Parse and check a witness from some tokens, returning it along with its type.