| Safe Haskell | None |
|---|
DDC.Driver.Command.Check
- cmdCheckFromFile :: Config -> FilePath -> ErrorT String IO ()
- cmdCheckSourceTetraFromFile :: Config -> FilePath -> ErrorT String IO ()
- cmdCheckSourceTetraFromString :: Config -> Source -> String -> ErrorT String IO ()
- cmdCheckCoreFromFile :: Config -> Language -> FilePath -> ErrorT String IO ()
- cmdCheckCoreFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Source -> String -> Mode n -> ErrorT String IO (Module (AnTEC SourcePos n) n)
- cmdShowType :: Language -> Universe -> Source -> String -> IO ()
- cmdTypeEquiv :: Language -> Source -> String -> IO ()
- cmdParseCheckType :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Universe -> Source -> String -> IO (Maybe (Type n, Kind n))
- data Mode n
- data ShowSpecMode
- cmdShowSpec :: Language -> ShowSpecMode -> Bool -> Bool -> Source -> String -> IO ()
- cmdExpRecon :: Language -> Source -> String -> IO ()
- cmdParseCheckExp :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> ModuleMap (AnTEC () n) n -> Mode n -> Bool -> Bool -> Source -> String -> IO (Maybe (Exp (AnTEC SourcePos n) n), Maybe CheckTrace)
- cmdShowWType :: Language -> Source -> String -> IO ()
Checking modules.
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.
cmdCheckSourceTetraFromFileSource
Check a Disciple Source Tetra module from a file.
cmdCheckSourceTetraFromStringSource
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.
Arguments
| :: Config | Driver config. |
| -> Language | Core language definition. |
| -> FilePath | Module file path. |
| -> ErrorT String IO () |
Check some fragment of Disciple core from a file.
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.
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. |
data ShowSpecMode Source
What components of the checked type to display.
Constructors
| ShowSpecAll | |
| ShowSpecData | |
| ShowSpecEffect | |
| ShowSpecClosure |
Instances
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.
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.