nar/check/monad/
mod.rs

1use crate::syntax::{
2    abs::desugar::DesugarState,
3    core::{Tele, TermInfo, Val},
4};
5
6pub use self::{error::*, meta::*, state::*};
7
8/// `Control.Monad.Except`, as type-checking error.
9mod error;
10/// A reworked version of `voile_util::meta`.
11mod meta;
12/// `Control.Monad.State`, as type-checking state.
13mod state;
14
15/// Type-Checking Monad.
16pub type TCM<T = TCS> = Result<T, TCE>;
17
18/// Type-Checking Monad with State.
19pub type TCMS<T> = TCM<(T, TCS)>;
20
21impl TCS {
22    /// The `tele` won't be affected after this function is invoked.
23    /// This is equivalence to the type instance of `AddContext Telescope` in
24    /// Agda.
25    pub fn under<T>(self, tele: &mut Tele, f: impl FnOnce(TCS) -> TCMS<T>) -> TCMS<T> {
26        let mut tcs = self;
27        let gamma_init_len = tcs.gamma.len();
28        tcs.gamma.append(tele);
29        let (res, mut tcs) = f(tcs)?;
30        let mut tele_recover = tcs.gamma.split_off(gamma_init_len);
31        tele.append(&mut tele_recover);
32        Ok((res, tcs))
33    }
34
35    pub fn considerate_of(desugar: &DesugarState) -> Self {
36        let mut tcs = TCS::default();
37        // tcs.meta_context.expand_with_fresh_meta(desugar.meta_count);
38        tcs.reserve_local_variables(desugar.decls.len());
39        tcs
40    }
41}
42
43/// Term-Producing Type-Checking Monad.
44pub type TermTCM = TCMS<TermInfo>;
45
46/// Whnf-Producing Type-Checking Monad.
47pub type ValTCM = TCMS<Val>;
nar/check/monad/mod.rs

nar/check/monad/
mod.rs
