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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141

use voile_util::uid::DBI;

use crate::{
    check::{monad::TCM, pats::CoreCopat, rules::clause::eqs::Equation},
    syntax::{
        abs::AbsCopat,
        core::{
            subst::{DeBruijn, RedEx, Subst},
            Tele, TeleS, Term,
        },
        pat::PatCommon,
    },
};

#[derive(Debug, Clone)]
pub(super) struct Problem {
    /// List of user patterns which could not yet be typed.
    pub(super) todo_pats: Vec<AbsCopat>,
    /// User patterns' unification problems.
    pub(super) equations: Vec<Equation>,
}

impl Problem {
    pub(super) fn is_all_solved(&self) -> bool {
        self.todo_pats.is_empty() && self.equations.iter().all(|eq| eq.is_solved())
    }

    pub(super) fn new(todo_pats: Vec<AbsCopat>) -> Self {
        let equations = Vec::with_capacity(todo_pats.len());
        Self {
            todo_pats,
            equations,
        }
    }
}

/// State worked on during lhs checking.
#[derive(Clone)]
pub(super) struct LhsState {
    /// Pattern variables' types.
    pub(super) tele: Tele,
    /// Patterns after splitting.
    /// Indices are positioned from right to left.
    pub(super) pats: Vec<CoreCopat>,
    /// Yet solved pattern matching.
    pub(super) problem: Problem,
    /// Type eliminated by `problem`.
    pub(super) target: Term,
}

impl LhsState {
    /// Number of patterns.
    pub(super) fn len_pats(&self) -> usize {
        self.pats.iter().take_while(|pat| !pat.is_proj()).count()
    }

    /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.ProblemRest.html#initLHSState).
    pub(super) fn new(todo_pats: Vec<AbsCopat>, ty: Term) -> Self {
        Self {
            tele: Default::default(),
            pats: Default::default(),
            problem: Problem::new(todo_pats),
            target: ty,
        }
    }
}

/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.Implicit.html#insertImplicitPatterns).
pub(super) fn insert_implicit_pats(pats: Vec<AbsCopat>, tele: &TeleS) -> Vec<AbsCopat> {
    debug_assert!(pats.len() <= tele.len());
    let mut new_pats = Vec::with_capacity(tele.len().max(pats.capacity()));
    for bind in tele {
        if bind.is_implicit() {
            new_pats.push(AbsCopat::fresh_var())
        } else {
            break;
        }
    }
    // Shouldn't insert too many patterns
    debug_assert!(new_pats.len() + pats.len() <= tele.len());
    let mut original_pats = pats;
    new_pats.append(&mut original_pats);
    new_pats
}

/// It's supposed to use [`insert_implicit_pats`](self::insert_implicit_pats) to
/// insert patterns, but as I'm refactoring it to an imperative style, reusing
/// the code becomes a bit difficult. [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.ProblemRest.html#updateProblemRest).
pub(super) fn progress_lhs_state(
    LhsState {
        pats,
        problem: Problem {
            todo_pats,
            equations,
        },
        target,
        tele: mut old_tele,
    }: LhsState,
) -> TCM<LhsState> {
    let mut pats_iter = todo_pats.into_iter();
    let (mut tele, target) = target.tele_view();
    let tele_len = tele.len();
    let mut new_equations = Vec::with_capacity(tele_len);
    for (i, bind) in tele.iter().enumerate() {
        let mut f = |in_pat: AbsCopat| {
            let equation = Equation {
                in_pat,
                // DBI is from right to left
                inst: Term::from_dbi(DBI(tele_len - i - 1)),
                ty: bind.ty.clone(),
            };
            new_equations.push(equation);
        };
        if bind.is_implicit() {
            f(AbsCopat::fresh_var());
        } else if let Some(pat) = pats_iter.next() {
            f(pat);
        } else {
            // All patterns are eliminated -- because
            // `pats_iter.next()` returns `None`
            break;
        }
    }
    let tau = Subst::raise(DBI(tele_len));
    let mut equations = equations.reduce_dbi(tau.clone());
    equations.append(&mut new_equations);
    let problem = Problem {
        todo_pats: pats_iter.collect(),
        equations,
    };
    old_tele.append(&mut tele);
    let mut pats = pats.reduce_dbi(tau);
    pats.extend((0..tele_len).rev().map(DBI).map(CoreCopat::var));
    let state = LhsState {
        tele: old_tele,
        pats,
        problem,
        target,
    };
    Ok(state)
}