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
142
143
144
145
146
147
148
149
150
151
152
153
154

use voile_util::axiom::Axiom;
use voile_util::level::LevelType;
use voile_util::meta::MI;
use voile_util::tags::*;
use voile_util::uid::*;

use crate::syntax::core::{CaseSplit, Closure, Fields, Neutral, TVal, Val, Variants};

/// Constructors and traversal functions.
impl Val {
    pub fn is_type(&self) -> bool {
        use Val::*;
        match self {
            Type(..) | Dt(..) | RowPoly(..) | RowKind(..) | Neut(Neutral::Row(..)) => true,
            // In case it's neutral, we use `is_universe` on its type.
            // In case it's a meta, we're supposed to solve it.
            Lam(..) | Cons(..) | Rec(..) | Pair(..) | Neut(..) => false,
        }
    }

    pub fn is_universe(&self) -> bool {
        match self {
            Val::Type(..) | Val::RowKind(..) => true,
            _ => false,
        }
    }

    pub fn pair(first: Self, second: Self) -> Self {
        Val::Pair(Box::new(first), Box::new(second))
    }

    pub fn cons(name: String, param: Self) -> Self {
        Val::Cons(name, Box::new(param))
    }

    pub fn case_tree(tree: CaseSplit) -> Self {
        Val::Lam(Closure::Tree(tree))
    }

    pub fn lift(levels: LevelType, expr: Neutral) -> Self {
        Val::Neut(Neutral::Lift(levels, Box::new(expr)))
    }

    pub fn meta(index: MI) -> Self {
        Val::Neut(Neutral::Meta(index))
    }

    pub fn var(index: DBI) -> Self {
        Val::Neut(Neutral::Var(index))
    }

    pub fn closure_lam(body: Self) -> Self {
        Val::Lam(Closure::plain(body))
    }

    pub fn glob(index: GI) -> Self {
        Val::Neut(Neutral::Ref(index))
    }

    pub fn split_on(split: CaseSplit, on: Neutral) -> Self {
        Val::Neut(Neutral::SplitOn(split, Box::new(on)))
    }

    pub fn or_split(split: CaseSplit, or: Neutral) -> Self {
        Val::Neut(Neutral::OrSplit(split, Box::new(or)))
    }

    pub fn fresh_axiom() -> Self {
        Self::postulate(unsafe { next_uid() })
    }

    pub(crate) fn postulate(uid: UID) -> Self {
        Val::Neut(Neutral::Axi(Axiom::Postulated(uid)))
    }

    pub fn fresh_implicit() -> Self {
        let axiom = Axiom::Implicit(unsafe { next_uid() });
        Val::Neut(Neutral::Axi(axiom))
    }

    pub fn fresh_unimplemented(index: GI) -> Self {
        let axiom = Axiom::Unimplemented(unsafe { next_uid() }, index);
        Val::Neut(Neutral::Axi(axiom))
    }

    pub fn app(function: Neutral, args: Vec<Self>) -> Self {
        Val::Neut(Neutral::App(Box::new(function), args))
    }

    pub fn fst(pair: Neutral) -> Self {
        Val::Neut(Neutral::Fst(Box::new(pair)))
    }

    pub fn snd(pair: Neutral) -> Self {
        Val::Neut(Neutral::Snd(Box::new(pair)))
    }

    pub fn proj(record: Neutral, field: String) -> Self {
        Val::Neut(Neutral::Proj(Box::new(record), field))
    }

    pub fn closure_dependent_type(kind: PiSig, visib: Plicit, param_ty: TVal, body: TVal) -> TVal {
        Self::dependent_type(kind, visib, param_ty, Closure::plain(body))
    }

    pub fn dependent_type(kind: PiSig, plicit: Plicit, param_type: TVal, closure: Closure) -> TVal {
        Val::Dt(kind, plicit, Box::new(param_type), closure)
    }

    pub fn variant_type(variants: Variants) -> TVal {
        Val::RowPoly(VarRec::Variant, variants)
    }

    pub fn record_type(fields: Variants) -> TVal {
        Val::RowPoly(VarRec::Record, fields)
    }

    pub fn neutral_row_type(kind: VarRec, variants: Variants, ext: Neutral) -> TVal {
        Val::Neut(Neutral::Row(kind, variants, Box::new(ext)))
    }

    pub fn neutral_record(fields: Fields, ext: Neutral) -> Self {
        Val::Neut(Neutral::Rec(fields, Box::new(ext)))
    }

    pub fn neutral_variant_type(variants: Variants, ext: Neutral) -> TVal {
        Self::neutral_row_type(VarRec::Variant, variants, ext)
    }

    pub fn neutral_record_type(fields: Variants, ext: Neutral) -> TVal {
        Self::neutral_row_type(VarRec::Record, fields, ext)
    }

    pub fn pi(param_plicit: Plicit, param_type: TVal, body: Closure) -> TVal {
        Self::dependent_type(PiSig::Pi, param_plicit, param_type, body)
    }

    pub fn sig(param_type: TVal, body: Closure) -> TVal {
        Self::dependent_type(PiSig::Sigma, Plicit::Ex, param_type, body)
    }

    pub fn into_neutral(self) -> Result<Neutral, Self> {
        match self {
            Val::Neut(n) => Ok(n),
            e => Err(e),
        }
    }
}

impl Closure {
    pub fn plain(body: Val) -> Self {
        Closure::Plain(Box::new(body))
    }
}