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
        )
    }
}