Safe Haskell	None

DDC.Driver.Command.Check

Contents

Checking modules.
Checking types.
Checking expressions.
Checking witnesses.

Synopsis

Checking modules.

cmdCheckFromFile Source

Arguments

:: Config	Driver config.
-> FilePath	Module file path.
-> ErrorT String IO ()

Parse and type-check a core module from a file, printing any errors to stdout.

This function handle fragments of Disciple Core, as well as Source Tetra modules. The language to use is determined by inspecting the file name extension.

cmdCheckSourceTetraFromFile Source

Arguments

:: Config	Driver config.
-> FilePath	Module file path.
-> ErrorT String IO ()

Check a Disciple Source Tetra module from a file.

cmdCheckSourceTetraFromString Source

Arguments

:: Config	Driver config.
-> Source	Source of the code.
-> String	Program module text.
-> ErrorT String IO ()

Check a Disciple Source Tetra module from a string. Any errors are thrown in the ErrorT monad.

cmdCheckCoreFromFile Source

Arguments

:: Config	Driver config.
-> Language	Core language definition.
-> FilePath	Module file path.
-> ErrorT String IO ()

Check some fragment of Disciple core from a file.

cmdCheckCoreFromString Source

Arguments

:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n)))
=> Fragment n err	Language fragment.
-> Source	Source of the program text.
-> String	Program text.
-> Mode n	Type checker mode.
-> ErrorT String IO (Module (AnTEC SourcePos n) n)

Parse and type-check a core module from a string.

Checking types.

cmdShowType :: Language -> Universe -> Source -> String -> IO ()Source

Show the type of a type in the given universe.

cmdTypeEquiv :: Language -> Source -> String -> IO ()Source

Check if two types are equivlant.

cmdParseCheckType Source

Arguments

:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n)))
=> Fragment n err	Language fragment.
-> Universe	Universe this type is supposed to be in.
-> Source	Source of the program text.
-> String	Program text.
-> IO (Maybe (Type n, Kind n))

Parse a core spec, and return its kind.

Checking expressions.

data Mode 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.

Instances

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

data ShowSpecMode Source

What components of the checked type to display.

Constructors

ShowSpecAll
ShowSpecData
ShowSpecEffect
ShowSpecClosure

Instances

Eq ShowSpecMode
Show ShowSpecMode

cmdShowSpec Source

Arguments

:: Language	Language fragment.
-> ShowSpecMode	What part of the type to show.
-> Bool	Type checker mode, Synth(True) or Recon(False)
-> Bool	Whether to display type checker trace.
-> Source	Source of the program text.
-> String	Program text.
-> IO ()

Show the spec of an expression.

cmdExpRecon :: Language -> Source -> String -> IO ()Source

Check expression and reconstruct type annotations on binders.

cmdParseCheckExp Source

Arguments

:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n)))
=> Fragment n err	The current language fragment.
-> ModuleMap (AnTEC () n) n	Current modules
-> Mode n	Type checker mode.
-> Bool	Print type checker trace.
-> Bool	Allow partial application of primitives.
-> Source	Where this expression was sourced from.
-> String	Text to parse.
-> IO (Maybe (Exp (AnTEC SourcePos n) n), Maybe CheckTrace)

Parse the given core expression, and return it, along with its type, effect and closure.

If the expression had a parse error, undefined vars, or type error then print this to the console.

We include a flag to override the language profile to allow partially applied primitives. Although a paticular evaluator (or backend) may not support partially applied primitives, we want to accept them if we are only loading an expression to check its type.

Checking witnesses.

cmdShowWType :: Language -> Source -> String -> IO ()Source

Show the type of a witness.