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 std::collections::BTreeMap;
use std::hash::Hash;
use std::rc::Rc;

/// Virtual trait, created to simplify trait bounds for identifiers.
pub trait NameTrait: Eq + Ord + PartialOrd + Hash + Clone {}

/// `Exp` in Mini-TT.
/// Expression language for Mini-TT.
#[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
pub enum Expression<Name: NameTrait> {
    Unit,
    One,
    Type,
    Void,
    Var(Name),
    Sum(Branch<Name>),
    Function(Branch<Name>),
    Pi(Pattern<Name>, Box<Expression<Name>>, Box<Expression<Name>>),
    Sigma(Pattern<Name>, Box<Expression<Name>>, Box<Expression<Name>>),
    Lambda(Pattern<Name>, Box<Expression<Name>>),
    First(Box<Expression<Name>>),
    Second(Box<Expression<Name>>),
    Application(Box<Expression<Name>>, Box<Expression<Name>>),
    Pair(Box<Expression<Name>>, Box<Expression<Name>>),
    Constructor(Name, Box<Expression<Name>>),
    Declaration(Box<Declaration<Name>>, Box<Expression<Name>>),
}

/// Pattern matching branch.
pub type Branch<Name> = BTreeMap<Name, Box<Expression<Name>>>;

/// `Val` in Mini-TT, value term.
#[derive(Debug, Clone)]
pub enum Value<Name: NameTrait> {
    Lambda(Closure<Name>),
    Unit,
    One,
    Type,
    Pi(Box<Value<Name>>, Closure<Name>),
    Sigma(Box<Value<Name>>, Closure<Name>),
    Pair(Box<Value<Name>>, Box<Value<Name>>),
    Constructor(Name, Box<Value<Name>>),
    Function(DeepClosure<Name>),
    Sum(DeepClosure<Name>),
    Neutral(Neutral<Name>),
}

/// Generic definition for two kinds of neutral terms.
///
/// Implementing `Eq` because of `NormalExpression`
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum GenericNeutral<Name: NameTrait, Value: Clone> {
    Generated(u32),
    Application(Box<Self>, Box<Value>),
    First(Box<Self>),
    Second(Box<Self>),
    Function(GenericDeepClosure<Name, Value>, Box<Self>),
}

/// `Neut` in Mini-TT, neutral value.
pub type Neutral<Name> = GenericNeutral<Name, Value<Name>>;

/// `Patt` in Mini-TT.
#[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
pub enum Pattern<Name: NameTrait> {
    Pair(Box<Pattern<Name>>, Box<Pattern<Name>>),
    Unit,
    Var(Name),
}

/// `Decl` in Mini-TT.
#[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
pub enum Declaration<Name: NameTrait> {
    Simple(Pattern<Name>, Expression<Name>, Expression<Name>),
    Recursive(Pattern<Name>, Expression<Name>, Expression<Name>),
}

impl<Name: NameTrait> Declaration<Name> {
    pub fn pattern(&self) -> &Pattern<Name> {
        use Declaration::*;
        match self {
            Simple(pattern, _, _) => pattern,
            Recursive(pattern, _, _) => pattern,
        }
    }
}

/// Generic definition for two kinds of telescopes.<br/>
/// `Value` can be specialized with `Value<Name>` or `NormalExpression<Name>`.
///
/// Implementing `Eq` because of `NormalExpression`
// TODO: replace with Vec<enum {Dec, Var}> maybe?
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum GenericTelescope<Name: NameTrait, Value: Clone> {
    Nil,
    UpDec(Rc<Self>, Declaration<Name>),
    UpVar(Rc<Self>, Pattern<Name>, Value),
}

pub type TelescopeRaw<Name> = GenericTelescope<Name, Value<Name>>;

/// `Rho` in Mini-TT, dependent context.
pub type Telescope<Name> = Rc<TelescopeRaw<Name>>;

/// Just for simplifying constructing an `Rc`.
pub fn up_var_rc<Name: NameTrait, Value: Clone>(
    me: Rc<GenericTelescope<Name, Value>>,
    pattern: Pattern<Name>,
    value: Value,
) -> Rc<GenericTelescope<Name, Value>> {
    Rc::new(GenericTelescope::UpVar(me, pattern, value))
}

/// Just for simplifying constructing an `Rc`.
pub fn up_dec_rc<Name: NameTrait, Value: Clone>(
    me: Rc<GenericTelescope<Name, Value>>,
    declaration: Declaration<Name>,
) -> Rc<GenericTelescope<Name, Value>> {
    Rc::new(GenericTelescope::UpDec(me, declaration))
}

/// `Clos` in Mini-TT.
#[derive(Debug, Clone)]
pub enum Closure<Name: NameTrait> {
    /// `cl` in Mini-TT.<br/>
    /// `cl` probably stands for "Closure"
    Function(Pattern<Name>, Expression<Name>, Box<Telescope<Name>>),
    /// `clCmp` in Mini-TT.
    /// `clCmp` probably stands for "Closure that does a comparison"
    Choice(Box<Closure<Name>>, Name),
}

/// Generic definition for two kinds of deep closures
pub type GenericDeepClosure<Name, Value> =
    (Box<Branch<Name>>, Box<Rc<GenericTelescope<Name, Value>>>);

/// `SClos` in Mini-TT.<br/>
/// A closure that comes with a pattern, like the data type (sum) definition (all the constructors
/// are pattern-like) or the function definition (it's built on top of a pattern tree)
pub type DeepClosure<Name> = GenericDeepClosure<Name, Value<Name>>;