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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67

use crate::{
    check::{
        monad::{TCM, TCS},
        rules::term::check,
    },
    syntax::{
        abs::{AbsConsInfo, AbsDataInfo, AbsTele},
        core::{ConsInfo, DataInfo, Decl, Val},
    },
};

/// The checked tele is put into the returned `tcs.gamma`.
pub fn check_tele(mut tcs: TCS, tele: AbsTele, ty: &Val) -> TCM {
    for bind in tele {
        let (checked, new_tcs) = check(tcs, &bind.ty, ty)?;
        tcs = new_tcs;
        let bind = bind.map_term(|_| checked.ast);
        tcs.gamma.push(bind);
    }
    Ok(tcs)
}

fn check_cons(tcs: TCS, cons: AbsConsInfo, ty: &Val) -> TCM<(TCS, ConsInfo)> {
    let param_len = tcs.gamma.len();
    let mut tcs = check_tele(tcs, cons.tele, ty)?;
    let info = ConsInfo {
        loc: cons.source,
        name: cons.name,
        params: tcs.gamma.split_off(param_len),
        data: cons.data_ix,
        // Inductive!
        fields: None,
    };
    Ok((tcs, info))
}

pub fn check_data(tcs: TCS, data: AbsDataInfo, conses: Vec<AbsConsInfo>) -> TCM {
    let t = Val::Type(data.level);
    let mut tcs = check_tele(tcs, data.tele, &t)?;
    let param_len = tcs.gamma.len();

    let info = DataInfo {
        params: tcs.gamma.clone(),
        loc: data.source,
        name: data.name,
        level: data.level,
        conses: data.conses,
    };
    tcs.sigma.push(Decl::Data(info));

    // For debugging only.
    let mut data_ix = None;

    for cons in conses {
        let (new_tcs, cons) = check_cons(tcs, cons, &t)?;
        tcs = new_tcs;
        match data_ix {
            None => data_ix = Some(cons.data),
            Some(ix) => debug_assert_eq!(ix, cons.data),
        }
        debug_assert_eq!(param_len, tcs.gamma.len());

        tcs.sigma.push(Decl::Cons(cons));
    }
    tcs.gamma.clear();
    Ok(tcs)
}