kontroli 0.4.0

Type checking for the lambda-Pi calculus modulo rewriting
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

//! Rewrite patterns.

use crate::app::format as fmt_appl;
use alloc::vec::Vec;
use core::fmt::{self, Display};

/// Miller variable.
///
/// This refers to the variables appearing in a rewrite pattern
/// bound by the rewrite rule's context.
/// Historically, this type was created to distinguish variables bound
/// by the rule context and
/// by lambda abstraction, as occurring in higher-order patterns.
/// Because Kontroli abandoned higher-order patterns,
/// this distinction is no longer necessary; however, the name remains as
/// a tribute to Miller's contributions to higher-order rewriting.
///
/// Reference:
/// Dale Miller:
/// A Logic Programming Language with Lambda-Abstraction,
/// Function Variables, and Simple Unification.
/// J. Log. Comput. 1(4): 497-536 (1991).
/// doi: [10.1093/logcom/1.4.497](https://doi.org/10.1093/logcom/1.4.497)
pub type Miller = usize;

/// Rewrite pattern.
///
/// This may be nonlinear; e.g. `eq X X` is a valid pattern.
#[derive(Clone)]
pub enum Pattern<S> {
    /// matches an application
    Symb(S, Vec<Pattern<S>>),
    /// matches any term, variable may appear multiple times in
    /// both left-hand and right-hand sides of rewrite rule
    MVar(Miller),
    /// matches any term
    Joker,
}

/// Pattern at the left-hand side of a rewrite rule.
///
/// The top pattern of a rule must be an application of patterns to a symbol.
/// This is to exclude rules matching any term, such as `[X] X --> f`.
pub type TopPattern<S> = crate::App<S, Pattern<S>>;

impl<S> Pattern<S> {
    /// Replace all variables that equal the given one by jokers.
    pub fn joke(self, joker: Miller) -> Self {
        match self {
            Self::Symb(s, args) => Self::Symb(s, args.into_iter().map(|p| p.joke(joker)).collect()),
            Self::MVar(v) if v == joker => Self::Joker,
            pat => pat,
        }
    }
}

impl<S> From<TopPattern<S>> for Pattern<S> {
    fn from(tp: TopPattern<S>) -> Self {
        Self::Symb(tp.symbol, tp.args)
    }
}

impl<S> TryFrom<Pattern<S>> for TopPattern<S> {
    type Error = ();

    fn try_from(p: Pattern<S>) -> Result<Self, Self::Error> {
        match p {
            Pattern::Symb(symbol, args) => Ok(TopPattern { symbol, args }),
            _ => Err(()),
        }
    }
}

impl<S: Display> Display for Pattern<S> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            Self::Symb(s, pats) => fmt_appl(s, pats, f),
            Self::MVar(m) => write!(f, "μ{}", m),
            Self::Joker => write!(f, "_"),
        }
    }
}