Safe Haskell | None |
---|
"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
- = ErrorRead !String
- | ErrorParser !ParseError
- | ErrorCheckType !(Error n)
- | ErrorCheckExp !(Error () n)
- | ErrorCompliance !(Error n)
- loadModuleFromFile :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> (String -> [Token (Tok n)]) -> FilePath -> IO (Either (Error n) (Module (AnTEC () n) n))
- loadModuleFromString :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> (String -> [Token (Tok n)]) -> FilePath -> String -> Either (Error n) (Module (AnTEC () n) n)
- loadModuleFromTokens :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> FilePath -> [Token (Tok n)] -> Either (Error n) (Module (AnTEC () n) n)
- loadExp :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> Map ModuleName (Module (AnTEC () n) n) -> FilePath -> [Token (Tok n)] -> Either (Error n) (Exp (AnTEC () n) n)
- loadType :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> FilePath -> [Token (Tok n)] -> Either (Error n) (Type n, Kind n)
- loadWitness :: (Eq n, Ord n, Show n, Pretty n) => Profile n -> FilePath -> [Token (Tok n)] -> Either (Error n) (Witness n, Type n)
Documentation
The type checker adds this annotation to every node in the AST, giving its type, effect and closure.
AnTEC | |
|
Things that can go wrong when loading a core thing.
ErrorRead !String | |
ErrorParser !ParseError | |
ErrorCheckType !(Error n) | |
ErrorCheckExp !(Error () n) | |
ErrorCompliance !(Error n) |
:: (Eq n, Ord n, Show n, Pretty n) | |
=> Profile n | Language fragment profile. |
-> (String -> [Token (Tok n)]) | Function to lex the source file. |
-> FilePath | File containing source code. |
-> IO (Either (Error n) (Module (AnTEC () n) n)) |
Parse and type check a core module from a file.
:: (Eq n, Ord n, Show n, Pretty n) | |
=> Profile n | Language fragment profile. |
-> (String -> [Token (Tok n)]) | Function to lex the source file. |
-> FilePath | Path to source file for error messages. |
-> String | Program text. |
-> Either (Error n) (Module (AnTEC () n) n) |
Parse and type check a core module from a string.
:: (Eq n, Ord n, Show n, Pretty n) | |
=> Profile n | Language fragment profile. |
-> FilePath | Path to source file for error messages. |
-> [Token (Tok n)] | Source tokens. |
-> Either (Error n) (Module (AnTEC () n) n) |
Parse and type check a core module.
:: (Eq n, Ord n, Show n, Pretty n) | |
=> Profile n | Language fragment profile. |
-> 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. |
-> [Token (Tok n)] | Source tokens. |
-> Either (Error n) (Exp (AnTEC () n) n) |
Parse and check an expression returning it along with its spec, effect and closure