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

use voile_util::uid::{DBI, GI};

use crate::{
    check::{
        monad::TCS,
        rules::{check_decls, simplify},
    },
    syntax::{
        abs::desugar::desugar_main,
        core::{subst::DeBruijn, Decl},
        surf::parse_str,
    },
};

#[test]
fn simple_simplify() {
    let code = "\
    definition id : {A : Type} -> A -> A;
    clause id a = a;

    definition id' : {A : Type} -> A -> A;
    clause id' a = id a;
    ";
    let desugar = desugar_main(parse_str(code).unwrap()).unwrap();
    let mut tcs = check_decls(TCS::considerate_of(&desugar), desugar.decls).unwrap();
    let id_def = match tcs.take_sigma(GI(2)) {
        Decl::Func(f) => f,
        _ => panic!(),
    };
    let body = id_def.clauses[0].body.clone().unwrap();
    let (body, _tcs) = simplify(tcs, body).unwrap();
    assert_eq!(body, DeBruijn::from_dbi(DBI(0)))
}