| Safe Haskell | None |
|---|
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 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 -> [Token (Tok 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 -> [Token (Tok 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 -> [Token (Tok 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 -> [Token (Tok 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 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 | The ascending smoke of incense. Synthesise the type of the expression, producing unification variables for bidirectional type inference. |
| 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
| Pretty CheckTrace | |
| Monoid CheckTrace |
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. |
| -> [Token (Tok 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. |
| -> [Token (Tok 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. |
| -> [Token (Tok 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
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.
Arguments
| :: (Eq n, Ord n, Show n, Pretty n) | |
| => Fragment n err | Language fragment profile. |
| -> FilePath | Path to source file for error messages. |
| -> [Token (Tok 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.