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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

use std::fmt::{Display, Error as FmtError, Formatter};

use voile_util::{
    level::Level,
    loc::{Ident, Loc, ToLoc},
    meta::MI,
};

use crate::{
    check::pats::Blocked,
    syntax::{
        abs::Abs,
        core::{Elim, Term, Val},
    },
};

/// Type-Checking Error.
#[derive(Debug)]
pub enum TCE {
    Textual(String),
    Wrapped(Box<Self>, Loc),

    // === Not* === //
    NotHead(Abs),
    NotPi(Term, Loc),
    NotProj(Abs),
    /// A projection is not a term.
    NotTerm(String),
    NotData(Box<Val>),

    // === Split* === //
    SplitOnNonVar(Box<Term>, Box<Term>),

    // === Meta* === //
    MetaRecursion(MI),
    MetaUnsolved(MI),

    // === Different* === //
    DifferentLevel(Loc, Level, Level),
    DifferentFieldCodata(Loc, String, String),
    DifferentTerm(Box<Term>, Box<Term>),
    DifferentElim(Box<Elim>, Box<Elim>),
    DifferentName(Ident, Ident),

    // === Misc === //
    Blocked(Box<Blocked<Term>>),
}

impl TCE {
    pub fn wrap(self, info: Loc) -> Self {
        TCE::Wrapped(Box::new(self), info)
    }

    pub fn blocked(block: Blocked<Term>) -> Self {
        TCE::Blocked(Box::new(block))
    }

    pub fn not_data(val: Val) -> Self {
        TCE::NotData(Box::new(val))
    }

    fn boxing_two<A, B>(a: A, b: B, f: impl FnOnce(Box<A>, Box<B>) -> Self) -> Self {
        f(Box::new(a), Box::new(b))
    }

    pub fn different_term(a: Term, b: Term) -> Self {
        Self::boxing_two(a, b, TCE::DifferentTerm)
    }

    pub fn different_elim(a: Elim, b: Elim) -> Self {
        Self::boxing_two(a, b, TCE::DifferentElim)
    }

    pub fn split_on_non_var(a: Term, b: Term) -> Self {
        Self::boxing_two(a, b, TCE::SplitOnNonVar)
    }
}

impl Display for TCE {
    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
        match self {
            TCE::Textual(text) => f.write_str(text),
            TCE::Wrapped(inner, info) => {
                write!(f, "{}\nWhen checking the expression at: {}.", inner, info)
            }
            TCE::NotHead(abs) => write!(f, "`{}` is not a head (at {}).", abs, abs.loc()),
            TCE::NotPi(term, loc) => write!(f, "`{}` is not a pi type (at {}).", term, loc),
            TCE::NotProj(abs) => write!(f, "`{}` is not a projection (at {}).", abs, abs.loc()),
            TCE::NotTerm(proj) => write!(f, "Cannot project `{}` on a datatype.", proj),
            TCE::NotData(val) => write!(f, "`{}` is not a datatype.", val),
            TCE::SplitOnNonVar(term, ty) => {
                write!(f, "Splitting on non variable `{}` (of type `{}`)", term, ty)
            }
            TCE::MetaRecursion(mi) => write!(f, "Trying to solve a recursive meta of index {}.", mi),
            TCE::MetaUnsolved(mi) => write!(f, "Unsolved meta of index {}.", mi),
            TCE::DifferentLevel(expr, expected_to_be_small, big) => write!(
                f,
                "Expression `{}` has level {}, which is not smaller than {}.",
                expr, expected_to_be_small, big
            ),
            TCE::DifferentFieldCodata(loc, field, codata) => write!(
                f,
                "Codata `{}` does not have field `{}` (at {}).",
                codata, field, loc
            ),
            TCE::DifferentTerm(a, b) => write!(f, "Failed to unify `{}` and `{}`.", a, b),
            TCE::DifferentElim(a, b) => write!(f, "Failed to unify `{}` and `{}`.", a, b),
            TCE::DifferentName(a, b) => write!(
                f,
                "`{}` (at {}) and `{}` (at {}) are different (conversion check is not structural in Narc).",
                a.text, a.loc, b.text, b.loc
            ),
            TCE::Blocked(b) => b.fmt(f),
        }
    }
}