voile/check/mod.rs
1pub use self::decl::*;
2pub use self::eval::*;
3pub use self::expr::*;
4pub use self::unify::*;
5
6/**
7Type-checking monad is a `Result<State, Error>`.
8$$
9\\newcommand{\\xx}[0]{\\texttt{x}}
10\\Gamma
11\\quad
12\\Gamma(\xx)=o
13$$
14*/
15pub mod monad;
16
17/**
18Meta variable solving,
19term (definitional) equality comparison.
20$$
21\Gamma \vdash A \simeq B
22$$
23*/
24mod unify;
25
26/**
27Declaration relevant checking.
28$$
29\\newcommand{\\checkD}[0]{\\vdash_\\texttt{d}}
30\\newcommand{\\GcheckD}[0]{\\Gamma \\checkD}
31\\GcheckD D\ \textbf{ok}
32$$
33
34Depends on `expr`.
35*/
36mod decl;
37/**
38Tooling functions that depends on neither `decl` nor `expr`.
39$$
40\llbracket a \rrbracket = \alpha
41$$
42*/
43mod eval;
44/**
45Expression/Type relevant checking.
46$$
47\\newcommand{\\tyck}[0]{\\vdash_\\texttt{c}}
48\\newcommand{\\Gtyck}[0]{\\Gamma \\tyck}
49\\newcommand{\\infer}[0]{\\vdash_\\texttt{i}}
50\\newcommand{\\Ginfer}[0]{\\Gamma \\infer}
51\\Ginfer a \\Rightarrow o
52\\quad
53\\Gtyck a:m \\Rightarrow o
54\\quad
55\\Gamma \vdash A <: B
56$$
57*/
58mod expr;