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

use voile_util::uid::{next_uid, UID};

use crate::syntax::common::ConHead;

/// Patterns.
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum Pat<Ix, Term> {
    /// Variable pattern.
    /// Note: it has a name suggestion in Agda.
    /// https://hackage.haskell.org/package/Agda-2.6.0.1/docs/Agda-Syntax-Internal.html#t:Pattern
    Var(Ix),
    /// Dual to [`crate::syntax::core::ast::Val::Refl`].
    Refl,
    /// Impossible pattern.
    Absurd,
    /// Dual to [`crate::syntax::core::ast::Val::Cons`],
    /// but can be forced (the first member is "is\_forced").
    Cons(bool, ConHead, Vec<Self>),
    /// Forced term as an expression.
    Forced(Term),
}

/// Copatterns.
/// The `Ix` is the representation of variable abstraction,
/// like `UID` in abstract or `DBI` in core.
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum Copat<Ix, Term> {
    /// Application copatterns.
    App(Pat<Ix, Term>),
    /// Projection copatterns.
    Proj(String),
}

/// Common methods shared by patterns.
pub trait PatCommon {
    /// Whether the pattern is a splitting pattern or not.
    fn is_split(&self) -> bool;

    fn is_solved(&self) -> bool {
        !self.is_split()
    }
}

impl<Ix, Term> PatCommon for Pat<Ix, Term> {
    fn is_split(&self) -> bool {
        use Pat::*;
        match self {
            Refl | Cons(..) => true,
            Var(..) | Absurd | Forced(..) => false,
        }
    }
}

impl<Ix, Term> PatCommon for Copat<Ix, Term> {
    fn is_split(&self) -> bool {
        match self {
            Copat::App(p) => p.is_split(),
            // Agda panics for this case.
            Copat::Proj(..) => false,
        }
    }
}

impl<Ix, Term> Copat<Ix, Term> {
    pub fn absurd() -> Self {
        Copat::App(Pat::Absurd)
    }
    pub fn reflexivity() -> Self {
        Copat::App(Pat::Refl)
    }
    pub fn var(ix: Ix) -> Self {
        Copat::App(Pat::Var(ix))
    }
    pub fn term(term: Term) -> Self {
        Copat::App(Pat::Forced(term))
    }
    pub fn cons(is_forced: bool, cons: ConHead, pats: Vec<Pat<Ix, Term>>) -> Self {
        Copat::App(Pat::Cons(is_forced, cons, pats))
    }

    pub fn is_proj(&self) -> bool {
        match self {
            Copat::App(_) => false,
            Copat::Proj(_) => true,
        }
    }

    pub fn map_app<Ix2, Term2>(
        self,
        f: impl FnOnce(Pat<Ix, Term>) -> Pat<Ix2, Term2>,
    ) -> Copat<Ix2, Term2> {
        match self {
            Copat::App(app) => Copat::App(f(app)),
            Copat::Proj(field) => Copat::Proj(field),
        }
    }
}

impl<Term> Copat<UID, Term> {
    pub fn fresh_var() -> Self {
        Self::var(unsafe { next_uid() })
    }
}