Safe Haskell | None |
---|
- cmdUniverse :: Language -> Source -> String -> IO ()
- cmdUniverse1 :: Language -> Source -> String -> IO ()
- cmdUniverse2 :: Language -> Source -> String -> IO ()
- cmdUniverse3 :: Language -> Source -> String -> IO ()
- cmdShowKind :: Language -> Source -> String -> IO ()
- cmdTypeEquiv :: Language -> Source -> String -> IO ()
- cmdShowWType :: Language -> Source -> String -> IO ()
- cmdShowType :: Language -> ShowTypeMode -> Source -> String -> IO ()
- cmdExpRecon :: Language -> Source -> String -> IO ()
- data ShowTypeMode
- cmdCheckModuleFromFile :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () n))) => Fragment n err -> FilePath -> ErrorT String IO (Module (AnTEC () n) n)
- cmdCheckModuleFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () n))) => Fragment n err -> Source -> String -> ErrorT String IO (Module (AnTEC () n) n)
- cmdParseCheckType :: (Ord n, Show n, Pretty n) => Source -> Fragment n err -> String -> IO (Maybe (Type n, Kind n))
- cmdParseCheckExp :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () n))) => Fragment n err -> ModuleMap (AnTEC () n) n -> Bool -> Source -> String -> IO (Maybe (Exp (AnTEC () n) n))
Documentation
cmdUniverse1 :: Language -> Source -> String -> IO ()Source
Given the type of some thing (up one level) show the universe of the thing.
cmdUniverse2 :: Language -> Source -> String -> IO ()Source
Given the kind of some thing (up two levels) show the universe of the thing.
cmdUniverse3 :: Language -> Source -> String -> IO ()Source
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.
cmdShowType :: Language -> ShowTypeMode -> Source -> String -> IO ()Source
Show the type of an expression.
cmdExpRecon :: Language -> Source -> String -> IO ()Source
Check expression and reconstruct type annotations on binders.
data ShowTypeMode Source
What components of the checked type to display.
cmdCheckModuleFromFile :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () n))) => Fragment n err -> FilePath -> ErrorT String IO (Module (AnTEC () n) n)Source
Parse and type-check a core module from a file.
cmdCheckModuleFromString :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () n))) => Fragment n err -> Source -> String -> ErrorT String IO (Module (AnTEC () n) n)Source
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))Source
Parse a core type, and check its kind.
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC () 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 () 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.