| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
DDC.Driver.Command.Check
- cmdCheckFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()
- cmdCheckSourceTetraFromFile :: Config -> Store -> FilePath -> ExceptT String IO ()
- cmdCheckSourceTetraFromString :: Config -> Store -> Source -> String -> ExceptT String IO ()
- cmdCheckCoreFromFile :: Config -> Language -> FilePath -> ExceptT String IO ()
- cmdCheckCoreFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Source -> String -> Mode n -> ExceptT 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.
Arguments
| :: Config | Driver config. |
| -> Store | Interface store. |
| -> FilePath | Module file path. |
| -> ExceptT 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. |
| -> Store | Interface store. |
| -> FilePath | Module file path. |
| -> ExceptT String IO () |
Check a Disciple Source Tetra module from a file.
cmdCheckSourceTetraFromString Source #
Arguments
| :: Config | Driver config. |
| -> Store | Interface store |
| -> Source | Source of the code. |
| -> String | Program module text. |
| -> ExceptT String IO () |
Check a Disciple Source Tetra module from a string.
Any errors are thrown in the ExceptT monad.
Arguments
| :: Config | Driver config. |
| -> Language | Core language definition. |
| -> FilePath | Module file path. |
| -> ExceptT 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. |
| -> ExceptT 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.
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 [Exists n] | The ascending smoke of incense. Synthesise the type of the expression, producing unification variables for bidirectional type inference. Any new unification variables introduced may be used to define the given existentials, so the need to be declared outside their scopes. If the list is empty we can add new variables to the inner most scope. |
| 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.