Safe Haskell	None

DDC.Core.Load

Contents

Loading modules
Loading expressions
Loading types
Loading witnesses

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.

Synopsis

Documentation

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
Fields annotType :: Type n annotEffect :: Effect n annotClosure :: Closure n annotTail :: a

Instances

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

data Error n err Source

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))

Instances

(Eq n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Pretty (Error n err)

data Mode n Source

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.

Instances

Eq n => Eq (Mode n)
Show n => Show (Mode n)
(Eq n, Pretty n) => Pretty (Mode n)

data CheckTrace Source

Human readable trace of the type checker.

Constructors

CheckTrace
Fields checkTraceDoc :: Doc

Instances

Pretty CheckTrace
Monoid CheckTrace

Loading modules

loadModuleFromFile Source

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.

loadModuleFromString Source

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.

loadModuleFromTokens Source

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

loadExpFromString Source

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.

loadExpFromTokens Source

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

loadTypeFromString Source

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.

loadTypeFromTokens Source

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

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.
-> [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.