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
117
118
119
120
121
122
123

use voile_util::meta::MI;

use crate::{
    check::{
        monad::{MetaSol, TCE, TCMS, TCS},
        rules::term::simplify,
    },
    syntax::{
        common::Bind,
        core::{Closure, Elim, Term, Val, ValData},
    },
};

/// Somehow like
/// [this](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Reduce.html#Instantiate)
/// in Agda, but different (Agda's instantiates one meta, but this one
/// instantiates the term fully. Maybe this corresponds to `instantiateFull`?).
pub trait HasMeta: Sized {
    /// Inline solved metas inside `self`.
    fn inline_meta(self, tcs: TCS) -> TCMS<Self>;
}

impl<T: HasMeta> HasMeta for Vec<T> {
    fn inline_meta(self, mut tcs: TCS) -> TCMS<Self> {
        let mut r = Vec::with_capacity(self.len());
        for t in self {
            let (t, new_tcs) = t.inline_meta(tcs)?;
            tcs = new_tcs;
            r.push(t);
        }
        Ok((r, tcs))
    }
}

impl HasMeta for ValData {
    fn inline_meta(self, tcs: TCS) -> TCMS<Self> {
        let (args, tcs) = self.args.inline_meta(tcs)?;
        Ok((ValData::new(self.kind, self.def, args), tcs))
    }
}

impl HasMeta for Elim {
    fn inline_meta(self, tcs: TCS) -> TCMS<Self> {
        match self {
            Elim::App(a) => a.inline_meta(tcs).map(|(a, tcs)| (Elim::app(a), tcs)),
            Elim::Proj(p) => Ok((Elim::Proj(p), tcs)),
        }
    }
}

impl HasMeta for Term {
    fn inline_meta(self, tcs: TCS) -> TCMS<Self> {
        match self {
            // Prefer not to simplify
            Term::Whnf(Val::Meta(mi, elims)) => solve_meta(tcs, mi, elims),
            Term::Whnf(w) => w.inline_meta(tcs).map(|(w, tcs)| (Term::Whnf(w), tcs)),
            Term::Redex(gi, id, elims) => {
                let (elims, tcs) = elims.inline_meta(tcs)?;
                Ok((Term::Redex(gi, id, elims), tcs))
            }
        }
    }
}

impl<T: HasMeta> HasMeta for Bind<T> {
    fn inline_meta(self, tcs: TCS) -> TCMS<Self> {
        let (ty, tcs) = self.ty.inline_meta(tcs)?;
        Ok((Bind::new(self.licit, self.name, ty), tcs))
    }
}

impl HasMeta for Closure {
    fn inline_meta(self, mut tcs: TCS) -> TCMS<Self> {
        tcs.unify_depth += 1;
        let (closure, mut tcs) = match self {
            Closure::Plain(body) => {
                let (body, tcs) = body.inline_meta(tcs)?;
                (Closure::plain(body), tcs)
            }
        };
        tcs.unify_depth -= 1;
        Ok((closure, tcs))
    }
}

fn solve_meta(tcs: TCS, mi: MI, elims: Vec<Elim>) -> TCMS<Term> {
    use MetaSol::*;
    let (_ix, sol) = match tcs.meta_ctx().solution(mi) {
        Solved(ix, sol) => (*ix, sol.clone()),
        Unsolved => return Err(TCE::MetaUnsolved(mi)),
    };
    let (elims, tcs) = elims.inline_meta(tcs)?;
    Ok((sol.apply_elim(elims), tcs))
}

impl HasMeta for Val {
    fn inline_meta(self, tcs: TCS) -> TCMS<Self> {
        use Val::*;
        match self {
            Type(l) => Ok((Type(l), tcs)),
            Data(info) => info.inline_meta(tcs).map(|(i, tcs)| (Data(i), tcs)),
            Pi(t, clos) => {
                let (t, tcs) = t.unboxed().inline_meta(tcs)?;
                let (clos, tcs) = clos.inline_meta(tcs)?;
                Ok((Val::Pi(t.boxed(), clos), tcs))
            }
            Cons(c, ts) => ts.inline_meta(tcs).map(|(ts, tcs)| (Cons(c, ts), tcs)),
            Meta(mi, elims) => {
                let (sol, tcs) = solve_meta(tcs, mi, elims)?;
                simplify(tcs, sol)
            }
            Axiom(a) => Ok((Axiom(a), tcs)),
            Var(head, args) => args.inline_meta(tcs).map(|(a, tcs)| (Var(head, a), tcs)),
            Id(t, a, b) => {
                let (t, tcs) = t.inline_meta(tcs)?;
                let (a, tcs) = a.inline_meta(tcs)?;
                let (b, tcs) = b.inline_meta(tcs)?;
                Ok((Val::identity(t, a, b), tcs))
            }
            Refl => Ok((Refl, tcs)),
        }
    }
}