logicaffeine_kernel/dag/
env.rs

1//! The environment: every declaration the kernel has admitted, indexed by name.
2
3use super::expr::ExprId;
4use super::name::NameId;
5use std::rc::Rc;
6
7#[derive(Copy, Clone, PartialEq, Eq, Debug)]
8pub enum Hint {
9    Opaque,
10    Abbrev,
11    Regular(u32),
12}
13
14impl Hint {
15    /// Lean's `ReducibilityHints.lt'`: `a` unfolds after `b`.
16    pub fn lt(self, other: Hint) -> bool {
17        match (self, other) {
18            (_, Hint::Opaque) => false,
19            (Hint::Abbrev, _) => false,
20            (Hint::Opaque, _) => true,
21            (_, Hint::Abbrev) => true,
22            (Hint::Regular(a), Hint::Regular(b)) => a < b,
23        }
24    }
25}
26
27#[derive(Copy, Clone, PartialEq, Eq, Debug)]
28pub enum Safety {
29    Safe,
30    Unsafe,
31    Partial,
32}
33
34#[derive(Copy, Clone, PartialEq, Eq, Debug)]
35pub enum QuotKind {
36    Type,
37    Ctor,
38    Lift,
39    Ind,
40}
41
42#[derive(Clone, Debug, PartialEq)]
43pub struct RecRule {
44    pub ctor: NameId,
45    pub nfields: u32,
46    pub rhs: ExprId,
47}
48
49#[derive(Clone, Debug, PartialEq)]
50pub struct InductiveInfo {
51    pub num_params: u32,
52    pub num_indices: u32,
53    pub all: Rc<[NameId]>,
54    pub ctors: Rc<[NameId]>,
55    pub num_nested: u32,
56    pub is_rec: bool,
57    pub is_reflexive: bool,
58    pub is_unsafe: bool,
59    /// The inductive's own recursor, `<name>.rec`.
60    pub rec: NameId,
61}
62
63#[derive(Clone, Debug, PartialEq)]
64pub struct CtorInfo {
65    pub induct: NameId,
66    pub cidx: u32,
67    pub num_params: u32,
68    pub num_fields: u32,
69    pub is_unsafe: bool,
70}
71
72#[derive(Clone, Debug, PartialEq)]
73pub struct RecInfo {
74    pub all: Rc<[NameId]>,
75    pub num_params: u32,
76    pub num_indices: u32,
77    pub num_motives: u32,
78    pub num_minors: u32,
79    pub rules: Rc<[RecRule]>,
80    pub k: bool,
81    pub is_unsafe: bool,
82    /// The inductive type of the major premise (for a nested auxiliary recursor this is the
83    /// nested type, e.g. `List`).
84    pub major_induct: NameId,
85}
86
87impl RecInfo {
88    pub fn major_idx(&self) -> usize {
89        (self.num_params + self.num_motives + self.num_minors + self.num_indices) as usize
90    }
91    pub fn first_index_idx(&self) -> usize {
92        (self.num_params + self.num_motives + self.num_minors) as usize
93    }
94}
95
96#[derive(Clone, Debug, PartialEq)]
97pub enum Kind {
98    Axiom {
99        is_unsafe: bool,
100    },
101    Defn {
102        value: ExprId,
103        hint: Hint,
104        safety: Safety,
105    },
106    Thm {
107        value: ExprId,
108    },
109    Opaque {
110        value: ExprId,
111        is_unsafe: bool,
112    },
113    Quot(QuotKind),
114    Induct(InductiveInfo),
115    Ctor(CtorInfo),
116    Rec(RecInfo),
117}
118
119#[derive(Clone, Debug, PartialEq)]
120pub struct Const {
121    pub name: NameId,
122    pub lparams: Rc<[NameId]>,
123    pub ty: ExprId,
124    pub kind: Kind,
125}
126
127impl Const {
128    pub fn is_unsafe(&self) -> bool {
129        match &self.kind {
130            Kind::Axiom { is_unsafe } | Kind::Opaque { is_unsafe, .. } => *is_unsafe,
131            Kind::Defn { safety, .. } => *safety == Safety::Unsafe,
132            Kind::Thm { .. } | Kind::Quot(_) => false,
133            Kind::Induct(i) => i.is_unsafe,
134            Kind::Ctor(c) => c.is_unsafe,
135            Kind::Rec(r) => r.is_unsafe,
136        }
137    }
138
139    pub fn is_partial(&self) -> bool {
140        matches!(
141            self.kind,
142            Kind::Defn {
143                safety: Safety::Partial,
144                ..
145            }
146        )
147    }
148
149    /// The value δ-reduction unfolds to: definitions and theorems (as in Lean's kernel).
150    pub fn delta_value(&self) -> Option<ExprId> {
151        match self.kind {
152            Kind::Defn { value, .. } | Kind::Thm { value } => Some(value),
153            _ => None,
154        }
155    }
156
157    pub fn hint(&self) -> Hint {
158        match self.kind {
159            Kind::Defn { hint, .. } => hint,
160            _ => Hint::Opaque,
161        }
162    }
163}
164
165/// Constants indexed densely by [`NameId`].
166#[derive(Clone, Default)]
167pub struct Env {
168    consts: Vec<Option<Rc<Const>>>,
169    pub count: usize,
170    pub quot_init: bool,
171    /// Every quotient installed whole, in the order its last constant arrived.
172    pub quotients: Vec<super::wellknown::QuotNames>,
173    /// Declarations present only while another is checked (a recursive definition's own header,
174    /// an inductive family's working declarations). Nothing derived from them may be cached
175    /// beyond that check: a nested family's auxiliary name can recur with another meaning.
176    provisional: Vec<NameId>,
177}
178
179impl Env {
180    #[inline]
181    pub fn get(&self, n: NameId) -> Option<&Rc<Const>> {
182        self.consts.get(n.0 as usize).and_then(|c| c.as_ref())
183    }
184
185    pub fn contains(&self, n: NameId) -> bool {
186        self.get(n).is_some()
187    }
188
189    /// Every admitted constant, in name-id order.
190    pub fn constants(&self) -> impl Iterator<Item = &Rc<Const>> {
191        self.consts.iter().flatten()
192    }
193
194    pub fn add(&mut self, c: Const) {
195        let i = c.name.0 as usize;
196        if self.consts.len() <= i {
197            self.consts.resize(i + 1, None);
198        }
199        debug_assert!(self.consts[i].is_none());
200        self.consts[i] = Some(Rc::new(c));
201        self.count += 1;
202    }
203
204    /// Adds a declaration that will be withdrawn with [`Env::remove`] once the check needing it
205    /// is done.
206    pub fn add_provisional(&mut self, c: Const) {
207        self.provisional.push(c.name);
208        self.add(c);
209    }
210
211    /// Withdraws a provisional declaration.
212    pub fn remove(&mut self, n: NameId) {
213        if let Some(slot) = self.consts.get_mut(n.0 as usize) {
214            if slot.take().is_some() {
215                self.count -= 1;
216            }
217        }
218        self.provisional.retain(|p| *p != n);
219    }
220
221    /// Whether results derived from `n` may outlive the current declaration.
222    #[inline]
223    pub fn is_settled(&self, n: NameId) -> bool {
224        self.provisional.is_empty() || !self.provisional.contains(&n)
225    }
226
227    pub fn inductive(&self, n: NameId) -> Option<&InductiveInfo> {
228        match &self.get(n)?.kind {
229            Kind::Induct(i) => Some(i),
230            _ => None,
231        }
232    }
233
234    pub fn ctor(&self, n: NameId) -> Option<&CtorInfo> {
235        match &self.get(n)?.kind {
236            Kind::Ctor(c) => Some(c),
237            _ => None,
238        }
239    }
240
241    pub fn rec(&self, n: NameId) -> Option<&RecInfo> {
242        match &self.get(n)?.kind {
243            Kind::Rec(r) => Some(r),
244            _ => None,
245        }
246    }
247
248    /// A non-recursive inductive with one constructor and no indices: the types with struct-η.
249    pub fn is_non_rec_structure(&self, n: NameId) -> bool {
250        matches!(self.inductive(n), Some(i) if !i.is_rec && i.ctors.len() == 1 && i.num_indices == 0)
251    }
252
253    /// Whether the inductive `n` eliminates into every universe: its own recursor takes one universe parameter, its
254    /// motive's, beyond the inductive's. A proposition that eliminates only into `Prop` takes none, and a proposition
255    /// that eliminates into every universe has only proofs for fields.
256    pub fn eliminates_into_every_sort(&self, n: NameId) -> bool {
257        match (self.get(n), self.inductive(n).and_then(|i| self.get(i.rec))) {
258            (Some(i), Some(r)) => r.lparams.len() == i.lparams.len() + 1,
259            _ => false,
260        }
261    }
262}
logicaffeine_kernel/dag/env.rs

logicaffeine_kernel/dag/
env.rs
