DDC.Driver.Command.Check

Documentation

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

Show the universe of some type.

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

Given the type of some thing (up one level) show the universe of the thing.

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

Given the kind of some thing (up two levels) show the universe of the thing.

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

Given the sort of some thing (up three levels) show the universe of the thing. We can't type check naked sorts, so just parse them.

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

Show the kind of a type.

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

Check if two types are equivlant.

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

Show the type of a witness.

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

Show the type of an expression.

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

Check expression and reconstruct type annotations on binders.

data ShowTypeMode

What components of the checked type to display.

Constructors

ShowTypeAll

ShowTypeValue

ShowTypeEffect

ShowTypeClosure

Instances

Eq ShowTypeMode

Show ShowTypeMode

cmdCheckModuleFromFile :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> FilePath -> ErrorT String IO (Module (AnTEC SourcePos n) n)

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

cmdCheckModuleFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC SourcePos n))) => Fragment n err -> Source -> String -> ErrorT String IO (Module (AnTEC SourcePos n) n)

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

cmdParseCheckType :: (Ord n, Show n, Pretty n) => Source -> Fragment n err -> String -> IO (Maybe (Type n, Kind n))

Parse a core type, and check its kind.

cmdParseCheckExp

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

-> Bool

Allow partial application of primitives.

-> Source

Where this expression was sourced from.

-> String

Text to parse.

-> IO (Maybe (Exp (AnTEC SourcePos n) n))

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.