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

use std::{
    fmt::{Display, Error, Formatter},
    ops::Add,
};

use voile_util::meta::MI;

use crate::syntax::core::Elim;

/// A modified version of
/// [this](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Internal.html#NotBlocked)
/// thing in Agda.
#[derive(Debug, Clone)]
pub enum Stuck {
    /// Blocked by meta.
    OnMeta(MI),
    /// The `Elim` is neutral and blocks a pattern match.
    OnElim(Elim),
    /// Not enough arguments were supplied to complete the matching.
    UnderApplied,
    /// We matched an absurd clause, results in a neutral `Def`.
    AbsurdMatch,
    /// We ran out of clauses, all considered clauses
    /// produced an actual mismatch.
    /// This can happen when try to reduce a function application,
    /// but we are still missing some function clauses.
    /// See `Agda.TypeChecking.Patterns.Match`.
    MissingClauses,
    /// Reduction was not blocked, we reached a whnf
    /// which can be anything, but a stuck `Whnf::Redex`.
    NotBlocked,
}

impl Default for Stuck {
    fn default() -> Self {
        Stuck::NotBlocked
    }
}

impl Add for Stuck {
    type Output = Self;

    fn add(self, rhs: Self) -> Self::Output {
        match (self, rhs) {
            (Stuck::NotBlocked, b) => b,
            // Primary in `Blocked`
            (Stuck::OnMeta(m), _) | (_, Stuck::OnMeta(m)) => Stuck::OnMeta(m),
            // `MissingClauses` is dominant (absorptive)
            (Stuck::MissingClauses, _) | (_, Stuck::MissingClauses) => Stuck::MissingClauses,
            // `StuckOn` is second strongest
            (Stuck::OnElim(e), _) | (_, Stuck::OnElim(e)) => Stuck::OnElim(e),
            (b, _) => b,
        }
    }
}

impl Display for Stuck {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        match self {
            Stuck::OnMeta(MI(m)) => write!(f, "blocked by meta {:?}", m),
            Stuck::OnElim(e) => write!(f, "blocked on argument `{}`", e),
            Stuck::UnderApplied => write!(f, "missing necessary arguments"),
            Stuck::AbsurdMatch => write!(f, "trying to instantiate an absurd match"),
            Stuck::MissingClauses => write!(f, "cannot find a suitable clause"),
            Stuck::NotBlocked => write!(f, "not blocked by anything, you may have found a bug"),
        }
    }
}

impl Stuck {
    pub fn is_meta(&self) -> Option<MI> {
        match self {
            Stuck::OnMeta(m) => Some(*m),
            _ => None,
        }
    }
}

/// Something where a meta variable may block reduction.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Internal.html#Blocked).
#[derive(Debug, Clone, Default)]
pub struct Blocked<T> {
    pub stuck: Stuck,
    /// The thing blocked by `stuck`.
    pub anyway: T,
}

impl Add for Blocked<()> {
    type Output = Self;

    fn add(self, rhs: Self) -> Self::Output {
        Blocked::new(self.stuck + rhs.stuck, ())
    }
}

impl<T> Blocked<T> {
    pub fn is_meta(&self) -> Option<MI> {
        self.stuck.is_meta()
    }

    pub fn new(stuck: Stuck, anyway: T) -> Self {
        Self { stuck, anyway }
    }

    pub fn map_anyway<R>(self, f: impl FnOnce(T) -> R) -> Blocked<R> {
        Blocked::new(self.stuck, f(self.anyway))
    }
}

impl<T: Display> Display for Blocked<T> {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        write!(
            f,
            "I'm not sure if I should give `{}` because I'm {}.",
            self.anyway, self.stuck
        )
    }
}