minitt/check/
mod.rs

1/// Read back: read back functions and normal form definitions.
2///
3/// Converting terms to normal forms with de-bruijn indices so
4/// we do not need to deal with alpha conversions when checking syntactic-equality.
5///
6/// Functions in this module are put into `impl for` blocks, their docs can be found in:
7///
8/// + [`ReadBack` of `Value`](../../syntax/enum.Value.html#impl-ReadBack)
9/// + [`ReadBack` of `Telescope`](../../syntax/enum.GenericTelescope.html#impl-ReadBack)
10/// + [`ReadBack` of `Closure`](../../syntax/enum.Closure.html#impl-ReadBack)
11///
12/// Depends on modules `syntax`.
13pub mod read_back;
14
15/// Type-Checking Monad: context, state and error.
16///
17/// Typing context (`Gamma`) and its updater, the type-checking error and its pretty-printer
18///
19/// Depends on module `syntax`.
20#[macro_use]
21pub mod tcm;
22
23/// Subtyping check: fallback rules of "instance of" checks: infer the expression's type and check
24/// if it's the subtype of the expected type.
25///
26/// Depends on modules `syntax` and `read_back`.
27pub mod subtype;
28
29/// Expression checker: infer, instance-of check, normal-form comparison, subtyping, etc.
30///
31/// Depends on modules `syntax`, `read_back` and `tcm`.
32pub mod expr;
33
34/// Declaration checker: for prefix parameters, simple declarations and recursive declarations.
35///
36/// Depends on modules `syntax`, `expr` and `tcm`.
37/// $$
38/// \textnormal{checkD}\quad \rho,\Gamma\vdash_l D\Rightarrow \Gamma'
39/// $$
40pub mod decl;
41
42use self::decl::check_declaration;
43use self::expr::{check, check_infer};
44use self::tcm::{TCM, TCS};
45use crate::ast::{Declaration, Expression, Value};
46
47/// `checkMain` in Mini-TT.
48pub fn check_main<'a>(expression: Expression) -> TCM<TCS<'a>> {
49    check_contextual(Default::default(), expression)
50}
51
52/// For REPL: check an expression under an existing context
53pub fn check_contextual(tcs: TCS, expression: Expression) -> TCM<TCS> {
54    check(0, tcs, expression, Value::One)
55}
56
57/// For REPL: infer the type of an expression under an existing context
58pub fn check_infer_contextual(tcs: TCS, expression: Expression) -> TCM<Value> {
59    check_infer(0, tcs, expression)
60}
61
62/// Similar to `checkMain` in Mini-TT, but for a declaration.
63pub fn check_declaration_main<'a>(declaration: Declaration) -> TCM<TCS<'a>> {
64    check_declaration(0, Default::default(), declaration)
65}
66
67#[cfg(test)]
68mod tests;
minitt/check/mod.rs

minitt/check/
mod.rs
