ddc-core-0.4.1.3: Disciplined Disciple Compiler core language and type checker.

Safe HaskellNone

DDC.Core.Load

Contents

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 

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.

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

Loading modules

loadModuleFromFileSource

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.

loadModuleFromStringSource

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.

loadModuleFromTokensSource

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

loadExpFromStringSource

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.

loadExpFromTokensSource

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

loadTypeFromStringSource

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.

loadTypeFromTokensSource

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

loadWitnessFromStringSource

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.

loadWitnessFromTokensSource

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.