logicaffeine_kernel/dag/
level.rs

1//! Universe levels: hash-consed, with a COMPLETE decision procedure for `≤` and `≡`.
2//!
3//! Lean's C++ kernel decides level equality by a normalisation that is sound but incomplete, and
4//! two of the Arena's soundness tests (`level-imax-leq`, `level-imax-normalization`) exist because
5//! an earlier version of it was unsound. Here `u ≤ v` is decided exactly — "for every assignment
6//! of natural numbers to the parameters" — by case analysis on the only non-monotone operator:
7//! `imax u v` is `0` when `v = 0` and `max u v` otherwise. A parameter that can make an `imax`
8//! right side vanish is split into `p = 0` and `p = p' + 1`; once no `imax` can vanish, both
9//! sides are `max(c, p₁+k₁, …)` and comparison is a closed-form check.
10
11use super::name::NameId;
12use rustc_hash::FxHashMap as FxMap;
13
14#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
15pub struct LevelId(pub u32);
16
17impl LevelId {
18    pub const ZERO: LevelId = LevelId(0);
19}
20
21#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
22pub enum LevelNode {
23    Zero,
24    Succ(LevelId),
25    Max(LevelId, LevelId),
26    IMax(LevelId, LevelId),
27    Param(NameId),
28    /// LOGOS's `SProp`, the definitionally proof-irrelevant sort below `Prop`. It is only ever a
29    /// whole level: `succ`, `max` and `imax` absorb it (`succ SProp = 1`, `max SProp u = u`,
30    /// `imax u SProp = SProp`), it is `≤` every level, and only `SProp` is `≤` it.
31    SProp,
32}
33
34/// An interned list of levels (the universe arguments of a constant).
35#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
36pub struct LevelsId(pub u32);
37
38impl LevelsId {
39    pub const EMPTY: LevelsId = LevelsId(0);
40}
41
42/// A universe substitution — a constant's level parameters replaced by the levels of one use of
43/// it — interned, so that a value can carry it as one id.
44#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
45pub struct SubstId(pub u32);
46
47impl SubstId {
48    /// Replaces nothing.
49    pub const IDENTITY: SubstId = SubstId(0);
50}
51
52#[derive(Clone)]
53struct Subst {
54    ps: Box<[NameId]>,
55    us: Box<[LevelId]>,
56}
57
58#[derive(Clone)]
59pub struct Levels {
60    nodes: Vec<LevelNode>,
61    has_param: Vec<bool>,
62    index: FxMap<LevelNode, LevelId>,
63    lists: Vec<Box<[LevelId]>>,
64    list_index: FxMap<Box<[LevelId]>, LevelsId>,
65    leq_memo: FxMap<(LevelId, LevelId), bool>,
66    substs: Vec<Subst>,
67    subst_index: FxMap<(LevelsId, LevelsId), SubstId>,
68    subst_memo: FxMap<(LevelId, SubstId), LevelId>,
69    subst_list_memo: FxMap<(LevelsId, SubstId), LevelsId>,
70    /// `SProp`'s id, once a LOGOS term has used it: until then no level is `SProp`.
71    sprop: Option<LevelId>,
72}
73
74impl Default for Levels {
75    fn default() -> Self {
76        Self::new()
77    }
78}
79
80impl Levels {
81    pub fn new() -> Levels {
82        let mut ls = Levels {
83            nodes: Vec::new(),
84            has_param: Vec::new(),
85            index: FxMap::default(),
86            lists: Vec::new(),
87            list_index: FxMap::default(),
88            leq_memo: FxMap::default(),
89            substs: vec![Subst {
90                ps: Box::new([]),
91                us: Box::new([]),
92            }],
93            subst_index: FxMap::default(),
94            subst_memo: FxMap::default(),
95            subst_list_memo: FxMap::default(),
96            sprop: None,
97        };
98        let z = ls.intern(LevelNode::Zero);
99        debug_assert_eq!(z, LevelId::ZERO);
100        let e = ls.list(&[]);
101        debug_assert_eq!(e, LevelsId::EMPTY);
102        ls
103    }
104
105    pub fn intern(&mut self, node: LevelNode) -> LevelId {
106        if let Some(&id) = self.index.get(&node) {
107            return id;
108        }
109        let hp = match node {
110            LevelNode::Zero => false,
111            LevelNode::Succ(a) => self.has_param(a),
112            LevelNode::Max(a, b) | LevelNode::IMax(a, b) => self.has_param(a) || self.has_param(b),
113            LevelNode::Param(_) => true,
114            LevelNode::SProp => false,
115        };
116        let id = LevelId(self.nodes.len() as u32);
117        self.nodes.push(node);
118        self.has_param.push(hp);
119        self.index.insert(node, id);
120        id
121    }
122
123    pub fn len(&self) -> usize {
124        self.nodes.len()
125    }
126
127    pub fn is_empty(&self) -> bool {
128        self.nodes.is_empty()
129    }
130
131    #[inline]
132    pub fn node(&self, l: LevelId) -> LevelNode {
133        self.nodes[l.0 as usize]
134    }
135
136    #[inline]
137    pub fn has_param(&self, l: LevelId) -> bool {
138        self.has_param[l.0 as usize]
139    }
140
141    pub fn list(&mut self, ls: &[LevelId]) -> LevelsId {
142        if let Some(&id) = self.list_index.get(ls) {
143            return id;
144        }
145        let id = LevelsId(self.lists.len() as u32);
146        let boxed: Box<[LevelId]> = ls.into();
147        self.lists.push(boxed.clone());
148        self.list_index.insert(boxed, id);
149        id
150    }
151
152    #[inline]
153    pub fn get_list(&self, id: LevelsId) -> &[LevelId] {
154        &self.lists[id.0 as usize]
155    }
156
157    pub fn succ(&mut self, l: LevelId) -> LevelId {
158        let l = if self.is_sprop(l) { LevelId::ZERO } else { l };
159        self.intern(LevelNode::Succ(l))
160    }
161
162    /// LOGOS's `SProp` (see [`LevelNode::SProp`]).
163    pub fn sprop(&mut self) -> LevelId {
164        let l = self.intern(LevelNode::SProp);
165        self.sprop = Some(l);
166        l
167    }
168
169    #[inline]
170    pub fn is_sprop(&self, l: LevelId) -> bool {
171        self.sprop == Some(l)
172    }
173
174    pub fn param(&mut self, n: NameId) -> LevelId {
175        self.intern(LevelNode::Param(n))
176    }
177
178    pub fn max_raw(&mut self, a: LevelId, b: LevelId) -> LevelId {
179        self.intern(LevelNode::Max(a, b))
180    }
181
182    pub fn imax_raw(&mut self, a: LevelId, b: LevelId) -> LevelId {
183        self.intern(LevelNode::IMax(a, b))
184    }
185
186    pub fn of_nat(&mut self, n: u64) -> LevelId {
187        (0..n).fold(LevelId::ZERO, |l, _| self.succ(l))
188    }
189
190    /// Syntactic: `true` only when `l` is nonzero under every assignment (`is_never_zero`).
191    pub fn is_never_zero(&self, l: LevelId) -> bool {
192        match self.node(l) {
193            LevelNode::Zero | LevelNode::Param(_) | LevelNode::SProp => false,
194            LevelNode::Succ(_) => true,
195            LevelNode::Max(a, b) => self.is_never_zero(a) || self.is_never_zero(b),
196            LevelNode::IMax(_, b) => self.is_never_zero(b),
197        }
198    }
199
200    fn to_offset(&self, mut l: LevelId) -> (LevelId, u64) {
201        let mut k = 0;
202        while let LevelNode::Succ(a) = self.node(l) {
203            l = a;
204            k += 1;
205        }
206        (l, k)
207    }
208
209    /// Lean's `mkLevelMax'`: `max` with the cheap simplifications the kernel applies.
210    pub fn max(&mut self, a: LevelId, b: LevelId) -> LevelId {
211        if a == b {
212            return a;
213        }
214        if self.is_sprop(a) {
215            return b;
216        }
217        if self.is_sprop(b) {
218            return a;
219        }
220        if a == LevelId::ZERO {
221            return b;
222        }
223        if b == LevelId::ZERO {
224            return a;
225        }
226        if let LevelNode::Max(_, b2) = self.node(a) {
227            if b2 == b {
228                return a;
229            }
230        }
231        let (ab, ak) = self.to_offset(a);
232        let (bb, bk) = self.to_offset(b);
233        if ab == bb {
234            return if ak >= bk { a } else { b };
235        }
236        self.max_raw(a, b)
237    }
238
239    /// Lean's `mkLevelIMax'`.
240    pub fn imax(&mut self, a: LevelId, b: LevelId) -> LevelId {
241        if self.is_sprop(b) {
242            return b;
243        }
244        let a = if self.is_sprop(a) { LevelId::ZERO } else { a };
245        if self.is_never_zero(b) {
246            return self.max(a, b);
247        }
248        if b == LevelId::ZERO || a == LevelId::ZERO || a == b {
249            return b;
250        }
251        if a == self.of_nat(1) {
252            return b;
253        }
254        self.imax_raw(a, b)
255    }
256
257    /// Replaces each `Param(ps[i])` by `us[i]`.
258    pub fn instantiate(&mut self, l: LevelId, ps: &[NameId], us: &[LevelId]) -> LevelId {
259        if !self.has_param(l) {
260            return l;
261        }
262        match self.node(l) {
263            LevelNode::Zero | LevelNode::SProp => l,
264            LevelNode::Param(n) => match ps.iter().position(|p| *p == n) {
265                Some(i) => us[i],
266                None => l,
267            },
268            LevelNode::Succ(a) => {
269                let a2 = self.instantiate(a, ps, us);
270                self.succ(a2)
271            }
272            LevelNode::Max(a, b) => {
273                let (a2, b2) = (self.instantiate(a, ps, us), self.instantiate(b, ps, us));
274                if (a2, b2) == (a, b) {
275                    l
276                } else {
277                    self.max(a2, b2)
278                }
279            }
280            LevelNode::IMax(a, b) => {
281                let (a2, b2) = (self.instantiate(a, ps, us), self.instantiate(b, ps, us));
282                if (a2, b2) == (a, b) {
283                    l
284                } else {
285                    self.imax(a2, b2)
286                }
287            }
288        }
289    }
290
291    /// The substitution of the levels `us` for the parameters `ps` (pairwise; a parameter without
292    /// a level is left as it is). Replacing each parameter by itself is the identity.
293    pub fn substitution(&mut self, ps: &[NameId], us: LevelsId) -> SubstId {
294        if ps.is_empty() {
295            return SubstId::IDENTITY;
296        }
297        let own: Vec<LevelId> = ps.iter().map(|p| self.param(*p)).collect();
298        let own = self.list(&own);
299        if own == us {
300            return SubstId::IDENTITY;
301        }
302        if let Some(&s) = self.subst_index.get(&(own, us)) {
303            return s;
304        }
305        let n = ps.len().min(self.get_list(us).len());
306        let id = SubstId(self.substs.len() as u32);
307        self.substs.push(Subst {
308            ps: ps[..n].into(),
309            us: self.get_list(us)[..n].into(),
310        });
311        self.subst_index.insert((own, us), id);
312        id
313    }
314
315    /// `l` under the substitution `s` — exactly [`Levels::instantiate`] with its parameters and
316    /// levels, remembered.
317    pub fn subst(&mut self, l: LevelId, s: SubstId) -> LevelId {
318        if s == SubstId::IDENTITY || !self.has_param(l) {
319            return l;
320        }
321        if let Some(&r) = self.subst_memo.get(&(l, s)) {
322            return r;
323        }
324        let sub = &self.substs[s.0 as usize];
325        let (ps, us) = (sub.ps.clone(), sub.us.clone());
326        let r = self.instantiate(l, &ps, &us);
327        self.subst_memo.insert((l, s), r);
328        r
329    }
330
331    /// Every level of `ls` under the substitution `s`.
332    pub fn subst_list(&mut self, ls: LevelsId, s: SubstId) -> LevelsId {
333        if s == SubstId::IDENTITY {
334            return ls;
335        }
336        if let Some(&r) = self.subst_list_memo.get(&(ls, s)) {
337            return r;
338        }
339        let old = self.get_list(ls).to_vec();
340        let new: Vec<LevelId> = old.iter().map(|l| self.subst(*l, s)).collect();
341        let r = self.list(&new);
342        self.subst_list_memo.insert((ls, s), r);
343        r
344    }
345
346    /// Whether `SProp` occurs anywhere in `l`.
347    pub fn mentions_sprop(&self, l: LevelId) -> bool {
348        if self.sprop.is_none() {
349            return false;
350        }
351        match self.node(l) {
352            LevelNode::SProp => true,
353            LevelNode::Zero | LevelNode::Param(_) => false,
354            LevelNode::Succ(a) => self.mentions_sprop(a),
355            LevelNode::Max(a, b) | LevelNode::IMax(a, b) => {
356                self.mentions_sprop(a) || self.mentions_sprop(b)
357            }
358        }
359    }
360
361    /// Whether `l` mentions the parameter `p`.
362    pub fn mentions_param(&self, l: LevelId, p: NameId) -> bool {
363        if !self.has_param(l) {
364            return false;
365        }
366        match self.node(l) {
367            LevelNode::Zero | LevelNode::SProp => false,
368            LevelNode::Param(n) => n == p,
369            LevelNode::Succ(a) => self.mentions_param(a, p),
370            LevelNode::Max(a, b) | LevelNode::IMax(a, b) => {
371                self.mentions_param(a, p) || self.mentions_param(b, p)
372            }
373        }
374    }
375
376    /// The first parameter of `l` not listed in `ps`.
377    pub fn undef_param(&self, l: LevelId, ps: &[NameId]) -> Option<NameId> {
378        if !self.has_param(l) {
379            return None;
380        }
381        match self.node(l) {
382            LevelNode::Zero | LevelNode::SProp => None,
383            LevelNode::Param(n) => (!ps.contains(&n)).then_some(n),
384            LevelNode::Succ(a) => self.undef_param(a, ps),
385            LevelNode::Max(a, b) | LevelNode::IMax(a, b) => {
386                self.undef_param(a, ps).or_else(|| self.undef_param(b, ps))
387            }
388        }
389    }
390
391    /// `u ≤ v` under every assignment of the parameters.
392    pub fn leq(&mut self, u: LevelId, v: LevelId) -> bool {
393        if u == v {
394            return true;
395        }
396        if self.sprop.is_some() {
397            if self.is_sprop(u) {
398                return true;
399            }
400            if self.is_sprop(v) {
401                return false;
402            }
403        }
404        if u == LevelId::ZERO {
405            return true;
406        }
407        if let Some(&r) = self.leq_memo.get(&(u, v)) {
408            return r;
409        }
410        let mut vars = Vec::new();
411        let a = self.tree(u, &mut vars);
412        let b = self.tree(v, &mut vars);
413        let r = decide_leq(&a, &b);
414        self.leq_memo.insert((u, v), r);
415        r
416    }
417
418    pub fn equiv(&mut self, u: LevelId, v: LevelId) -> bool {
419        u == v || (self.leq(u, v) && self.leq(v, u))
420    }
421
422    pub fn equiv_lists(&mut self, a: LevelsId, b: LevelsId) -> bool {
423        if a == b {
424            return true;
425        }
426        let (xs, ys) = (self.get_list(a).to_vec(), self.get_list(b).to_vec());
427        xs.len() == ys.len() && xs.iter().zip(&ys).all(|(x, y)| self.equiv(*x, *y))
428    }
429
430    /// `l` is zero under every assignment of its parameters. Exact, and structural: a successor
431    /// never is, a parameter may be one, `max a b` is exactly when both are, `imax a b` exactly
432    /// when `b` is (it is `0` when `b` is and at least `b` otherwise).
433    pub fn is_always_zero(&self, l: LevelId) -> bool {
434        match self.node(l) {
435            LevelNode::Zero | LevelNode::SProp => true,
436            LevelNode::Succ(_) | LevelNode::Param(_) => false,
437            LevelNode::Max(a, b) => self.is_always_zero(a) && self.is_always_zero(b),
438            LevelNode::IMax(_, b) => self.is_always_zero(b),
439        }
440    }
441
442    fn tree(&self, l: LevelId, vars: &mut Vec<NameId>) -> T {
443        match self.node(l) {
444            LevelNode::Zero | LevelNode::SProp => T::Zero,
445            LevelNode::Succ(a) => T::Succ(Box::new(self.tree(a, vars))),
446            LevelNode::Max(a, b) => {
447                T::Max(Box::new(self.tree(a, vars)), Box::new(self.tree(b, vars)))
448            }
449            LevelNode::IMax(a, b) => {
450                T::IMax(Box::new(self.tree(a, vars)), Box::new(self.tree(b, vars)))
451            }
452            LevelNode::Param(n) => {
453                let i = vars.iter().position(|v| *v == n).unwrap_or_else(|| {
454                    vars.push(n);
455                    vars.len() - 1
456                });
457                T::Var(i as u32)
458            }
459        }
460    }
461}
462
463/// A level over numbered variables, the working form of the decision procedure.
464#[derive(Clone, Debug, PartialEq)]
465enum T {
466    Zero,
467    Succ(Box<T>),
468    Max(Box<T>, Box<T>),
469    IMax(Box<T>, Box<T>),
470    Var(u32),
471}
472
473impl T {
474    fn never_zero(&self) -> bool {
475        match self {
476            T::Zero | T::Var(_) => false,
477            T::Succ(_) => true,
478            T::Max(a, b) => a.never_zero() || b.never_zero(),
479            T::IMax(_, b) => b.never_zero(),
480        }
481    }
482
483    fn is_zero(&self) -> bool {
484        match self {
485            T::Zero => true,
486            T::Succ(_) | T::Var(_) => false,
487            T::Max(a, b) => a.is_zero() && b.is_zero(),
488            T::IMax(_, b) => b.is_zero(),
489        }
490    }
491
492    /// Resolves every `imax` whose right side is decidedly zero or nonzero.
493    fn simp(self) -> T {
494        match self {
495            T::Succ(a) => T::Succ(Box::new(a.simp())),
496            T::Max(a, b) => T::Max(Box::new(a.simp()), Box::new(b.simp())),
497            T::IMax(a, b) => {
498                let b = b.simp();
499                if b.is_zero() {
500                    T::Zero
501                } else if b.never_zero() {
502                    T::Max(Box::new(a.simp()), Box::new(b))
503                } else {
504                    T::IMax(Box::new(a.simp()), Box::new(b))
505                }
506            }
507            t => t,
508        }
509    }
510
511    /// A variable whose vanishing would make some remaining `imax` vanish.
512    fn split_candidate(&self) -> Option<u32> {
513        match self {
514            T::Zero | T::Var(_) => None,
515            T::Succ(a) => a.split_candidate(),
516            T::Max(a, b) => a.split_candidate().or_else(|| b.split_candidate()),
517            T::IMax(a, b) => b
518                .zero_relevant()
519                .or_else(|| a.split_candidate())
520                .or_else(|| b.split_candidate()),
521        }
522    }
523
524    fn zero_relevant(&self) -> Option<u32> {
525        match self {
526            T::Var(v) => Some(*v),
527            T::Zero | T::Succ(_) => None,
528            T::Max(a, b) => a.zero_relevant().or_else(|| b.zero_relevant()),
529            T::IMax(_, b) => b.zero_relevant(),
530        }
531    }
532
533    fn subst(&self, v: u32, to_zero: bool) -> T {
534        match self {
535            T::Var(w) if *w == v => {
536                if to_zero {
537                    T::Zero
538                } else {
539                    T::Succ(Box::new(T::Var(v)))
540                }
541            }
542            T::Succ(a) => T::Succ(Box::new(a.subst(v, to_zero))),
543            T::Max(a, b) => T::Max(Box::new(a.subst(v, to_zero)), Box::new(b.subst(v, to_zero))),
544            T::IMax(a, b) => T::IMax(Box::new(a.subst(v, to_zero)), Box::new(b.subst(v, to_zero))),
545            t => t.clone(),
546        }
547    }
548
549    /// `max(c, vᵢ + kᵢ …)` for an `imax`-free level: (constant, per-variable offsets).
550    fn flatten(&self, k: u64, c: &mut u64, vars: &mut Vec<(u32, u64)>) {
551        match self {
552            T::Zero => *c = (*c).max(k),
553            T::Succ(a) => a.flatten(k + 1, c, vars),
554            T::Max(a, b) => {
555                a.flatten(k, c, vars);
556                b.flatten(k, c, vars);
557            }
558            T::Var(v) => {
559                *c = (*c).max(k);
560                match vars.iter_mut().find(|(w, _)| w == v) {
561                    Some(e) => e.1 = e.1.max(k),
562                    None => vars.push((*v, k)),
563                }
564            }
565            T::IMax(..) => unreachable!("flatten requires an imax-free level"),
566        }
567    }
568}
569
570fn decide_leq(a: &T, b: &T) -> bool {
571    let (a, b) = (a.clone().simp(), b.clone().simp());
572    if let Some(v) = a.split_candidate().or_else(|| b.split_candidate()) {
573        return decide_leq(&a.subst(v, true), &b.subst(v, true))
574            && decide_leq(&a.subst(v, false), &b.subst(v, false));
575    }
576    let (mut ca, mut va) = (0, Vec::new());
577    a.flatten(0, &mut ca, &mut va);
578    let (mut cb, mut vb) = (0, Vec::new());
579    b.flatten(0, &mut cb, &mut vb);
580    let floor_b = vb.iter().fold(cb, |m, (_, k)| m.max(*k));
581    ca <= floor_b
582        && va
583            .iter()
584            .all(|(v, k)| vb.iter().any(|(w, j)| w == v && j >= k))
585}
586
587#[cfg(test)]
588#[path = "../../../logicaffeine_tests/unit/logicaffeine_kernel/dag/level/tests.rs"]
589mod tests;
logicaffeine_kernel/dag/level.rs

logicaffeine_kernel/dag/
level.rs
