nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

use crate::syntax::{
    abs::desugar::DesugarState,
    core::{Tele, TermInfo, Val},
};

pub use self::{error::*, meta::*, state::*};

/// `Control.Monad.Except`, as type-checking error.
mod error;
/// A reworked version of `voile_util::meta`.
mod meta;
/// `Control.Monad.State`, as type-checking state.
mod state;

/// Type-Checking Monad.
pub type TCM<T = TCS> = Result<T, TCE>;

/// Type-Checking Monad with State.
pub type TCMS<T> = TCM<(T, TCS)>;

impl TCS {
    /// The `tele` won't be affected after this function is invoked.
    /// This is equivalence to the type instance of `AddContext Telescope` in
    /// Agda.
    pub fn under<T>(self, tele: &mut Tele, f: impl FnOnce(TCS) -> TCMS<T>) -> TCMS<T> {
        let mut tcs = self;
        let gamma_init_len = tcs.gamma.len();
        tcs.gamma.append(tele);
        let (res, mut tcs) = f(tcs)?;
        let mut tele_recover = tcs.gamma.split_off(gamma_init_len);
        tele.append(&mut tele_recover);
        Ok((res, tcs))
    }

    pub fn considerate_of(desugar: &DesugarState) -> Self {
        let mut tcs = TCS::default();
        // tcs.meta_context.expand_with_fresh_meta(desugar.meta_count);
        tcs.reserve_local_variables(desugar.decls.len());
        tcs
    }
}

/// Term-Producing Type-Checking Monad.
pub type TermTCM = TCMS<TermInfo>;

/// Whnf-Producing Type-Checking Monad.
pub type ValTCM = TCMS<Val>;