logicaffeine_kernel/dag/sem/
conv.rs

1//! Definitional equality of values: Lean's algorithm, in the classic engine's order of attempts.
2//!
3//! Quick structural cases and proven pairs first; the `≡ true` shortcut; `whnf_core` without
4//! unfolding projections' structures; proof irrelevance; lazy δ-reduction by definitional height
5//! (comparing two applications of the same definition argument by argument, skipping the
6//! positions its definition cannot distinguish, before unfolding either); then constants,
7//! variables and projections; full `whnf_core`; congruence of applications; η; struct-η; string
8//! literals; unit-like types. A β-step is an environment extension, a δ-step a remembered
9//! unfolding, and a binder is crossed by applying both closures to one fresh variable.
10//!
11//! Proven pairs are closed under congruence but not transitivity: Lean's definitional equality
12//! is not transitive (proof irrelevance), see the classic engine's `ProvenEqual`.
13
14use super::value::{EnvId, Head, Kind, Sp, Val, V};
15use super::Sem;
16use crate::dag::env::Hint;
17use crate::dag::error::{FailKind, KResult, KernelFailure};
18use crate::dag::level::LevelsId;
19use crate::dag::name::NameId;
20use crate::dag::nat::Nat;
21
22enum LBool {
23    True,
24    False,
25    Undef,
26}
27
28impl From<bool> for LBool {
29    fn from(b: bool) -> LBool {
30        if b {
31            LBool::True
32        } else {
33            LBool::False
34        }
35    }
36}
37
38enum Step {
39    Continue(V, V),
40    Unknown(V, V),
41    True,
42    False(V, V),
43}
44
45#[inline]
46fn key(a: V, b: V) -> (u32, u32) {
47    if a <= b {
48        (a.0, b.0)
49    } else {
50        (b.0, a.0)
51    }
52}
53
54impl Sem<'_> {
55    /// `t ≡ s`.
56    pub fn is_def_eq(&mut self, t: V, s: V) -> KResult<bool> {
57        if t == s {
58            return Ok(true);
59        }
60        self.enter()?;
61        let r = self.is_def_eq_core(t, s);
62        self.leave();
63        let r = r?;
64        if r {
65            self.note_proven(t, s);
66        }
67        Ok(r)
68    }
69
70    /// `t ≡ s`, if it is decided within `steps` conversion steps and the checker's resources;
71    /// `None` if not. An attempt is speculation: running out — of steps, or of recursion depth,
72    /// which a step does not bound — leaves it undecided, never declined, and nothing is learned
73    /// from it but what it proved along the way.
74    pub fn is_def_eq_within(&mut self, t: V, s: V, steps: u32) -> KResult<Option<bool>> {
75        let outer = self.st.probe.replace(steps);
76        let r = self.is_def_eq(t, s);
77        self.st.probe = outer;
78        match r {
79            Ok(b) => Ok(Some(b)),
80            Err(e) if e.is_exhausted() || e.kind == FailKind::Decline => Ok(None),
81            Err(e) => Err(e),
82        }
83    }
84
85    fn is_def_eq_core_guarded(&mut self, t: V, s: V) -> KResult<bool> {
86        if t == s {
87            return Ok(true);
88        }
89        self.enter()?;
90        let r = self.is_def_eq_core(t, s);
91        self.leave();
92        r
93    }
94
95    /// Equal or proven equal.
96    #[inline]
97    fn known_equal(&self, a: V, b: V) -> bool {
98        a == b || self.st.proven.contains(&key(a, b))
99    }
100
101    /// Equal, proven equal, or congruent: the same shape with parts pairwise equal, proven equal
102    /// or congruent — a walk over what is already known, never a reduction. Closures are compared
103    /// by their environments' entries being equal or proven equal, not by a walk into them: an
104    /// environment can be long and its entries large, and the full algorithm (which proves such
105    /// parts, and remembers them, on its way) decides those.
106    fn eqv_is_equiv(&mut self, a: V, b: V) -> bool {
107        if self.known_equal(a, b) {
108            return true;
109        }
110        let r = match (self.st.arena.get(a), self.st.arena.get(b)) {
111            (
112                Val::Neu {
113                    head: h1,
114                    spine: s1,
115                    ..
116                },
117                Val::Neu {
118                    head: h2,
119                    spine: s2,
120                    ..
121                },
122            ) => self.heads_equiv(h1, h2) && self.spines_equiv(s1, s2),
123            (
124                Val::Lam {
125                    dom: d1,
126                    env: e1,
127                    body: b1,
128                },
129                Val::Lam {
130                    dom: d2,
131                    env: e2,
132                    body: b2,
133                },
134            ) => d1 == d2 && b1 == b2 && self.envs_equiv(e1, e2),
135            (
136                Val::Pi {
137                    dom: d1,
138                    env: e1,
139                    body: b1,
140                },
141                Val::Pi {
142                    dom: d2,
143                    env: e2,
144                    body: b2,
145                },
146            ) => b1 == b2 && self.eqv_is_equiv(d1, d2) && self.envs_equiv(e1, e2),
147            (
148                Val::PiLam {
149                    dom: d1,
150                    env: e1,
151                    ctx: c1,
152                    body: b1,
153                },
154                Val::PiLam {
155                    dom: d2,
156                    env: e2,
157                    ctx: c2,
158                    body: b2,
159                },
160            ) => b1 == b2 && c1 == c2 && self.eqv_is_equiv(d1, d2) && self.envs_equiv(e1, e2),
161            _ => false,
162        };
163        if r {
164            self.note_proven(a, b);
165        }
166        r
167    }
168
169    #[inline]
170    fn note_proven(&mut self, a: V, b: V) {
171        let k = key(a, b);
172        if !self.st.proven.contains(&k) {
173            self.st.proven.insert(k, 1);
174        }
175    }
176
177    fn heads_equiv(&mut self, h1: super::value::HeadId, h2: super::value::HeadId) -> bool {
178        if h1 == h2 {
179            return true;
180        }
181        match (self.st.arena.head(h1), self.st.arena.head(h2)) {
182            (Head::Proj { idx: i1, x: x1, .. }, Head::Proj { idx: i2, x: x2, .. }) => {
183                i1 == i2 && self.eqv_is_equiv(x1, x2)
184            }
185            _ => false,
186        }
187    }
188
189    fn spines_equiv(&mut self, mut s1: Sp, mut s2: Sp) -> bool {
190        if self.st.arena.spine_len(s1) != self.st.arena.spine_len(s2) {
191            return false;
192        }
193        while s1 != s2 {
194            let (n1, n2) = (self.st.arena.spine_node(s1), self.st.arena.spine_node(s2));
195            if !self.eqv_is_equiv(n1.arg, n2.arg) {
196                return false;
197            }
198            s1 = n1.prev;
199            s2 = n2.prev;
200        }
201        true
202    }
203
204    /// Two environments of one shape (length and universe substitution) whose entries are
205    /// pairwise equal or proven equal.
206    fn envs_equiv(&self, e1: EnvId, e2: EnvId) -> bool {
207        e1 == e2
208            || (self.st.arena.same_shape(e1, e2)
209                && self
210                    .st
211                    .arena
212                    .entries(e1)
213                    .zip(self.st.arena.entries(e2))
214                    .all(|(a, b)| self.known_equal(a, b)))
215    }
216
217    fn quick_is_def_eq(&mut self, t: V, s: V) -> KResult<LBool> {
218        if self.eqv_is_equiv(t, s) {
219            return Ok(LBool::True);
220        }
221        Ok(match (self.st.arena.get(t), self.st.arena.get(s)) {
222            (Val::Lam { .. }, Val::Lam { .. }) => self.is_def_eq_binding(t, s, false)?.into(),
223            (Val::Pi { .. } | Val::PiLam { .. }, Val::Pi { .. } | Val::PiLam { .. }) => {
224                self.is_def_eq_binding(t, s, true)?.into()
225            }
226            (Val::Sort(a), Val::Sort(b)) => self.k.s.levels.equiv(a, b).into(),
227            (Val::Nat(_) | Val::Str(_), Val::Nat(_) | Val::Str(_)) => (t == s).into(),
228            _ => LBool::Undef,
229        })
230    }
231
232    fn is_binder(&self, v: V, pi: bool) -> bool {
233        match self.st.arena.get(v) {
234            Val::Lam { .. } => !pi,
235            Val::Pi { .. } | Val::PiLam { .. } => pi,
236            _ => false,
237        }
238    }
239
240    /// Two binder chains of the same kind: domains pairwise, then the bodies under one fresh
241    /// variable per binder (typed by the second chain's domains, as Lean does).
242    fn is_def_eq_binding(&mut self, mut t: V, mut s: V, pi: bool) -> KResult<bool> {
243        let mut bound = 0u32;
244        let r = (|| -> KResult<bool> {
245            while self.is_binder(t, pi) && self.is_binder(s, pi) {
246                let td = self.lam_domain(t)?;
247                let sd = self.lam_domain(s)?;
248                if td != sd && !self.is_def_eq(td, sd)? {
249                    return Ok(false);
250                }
251                let x = self.bind(sd);
252                bound += 1;
253                t = self.instantiate(t, x)?;
254                s = self.instantiate(s, x)?;
255            }
256            self.is_def_eq(t, s)
257        })();
258        for _ in 0..bound {
259            self.unbind();
260        }
261        r
262    }
263
264    /// [`Sem::is_def_eq_args`] as a probe, before unfolding: each argument pair may take
265    /// `Kernel::probe_steps` steps, conversion and δ-unfolding steps alike. Arguments that differ only deep inside can cost
266    /// far more to compare than the definitions cost to unfold, and unfolding decides the pair
267    /// either way. `Some` when the probe decided (every pair agrees, or one is found unequal);
268    /// `None` when a pair ran out of steps (see [`Sem::decide_abandoned_probe`]). Inside a probe,
269    /// arguments are compared on the probe's own budget.
270    fn probe_args(&mut self, t: V, s: V) -> KResult<Option<bool>> {
271        if self.st.probe.is_some() {
272            return self.is_def_eq_args(t, s).map(Some);
273        }
274        let (Some((c, ls, _, ts)), Some((_, _, _, ss))) = (self.const_app(t), self.const_app(s))
275        else {
276            return Ok(Some(false));
277        };
278        let n = self.st.arena.spine_len(ts);
279        if n != self.st.arena.spine_len(ss) {
280            return Ok(Some(false));
281        }
282        let mask = self.ignorable_args(c, ls)?;
283        let steps = self.k.probe_steps;
284        let (mut x, mut y) = (ts, ss);
285        let mut i = n;
286        while x != Sp::NIL {
287            i -= 1;
288            let (nx, ny) = (self.st.arena.spine_node(x), self.st.arena.spine_node(y));
289            let ignorable = i < crate::dag::relevance::MAX_TRACKED && (mask >> i) & 1 == 1;
290            if !ignorable {
291                match self.is_def_eq_within(nx.arg, ny.arg, steps)? {
292                    Some(true) => {}
293                    Some(false) => return Ok(Some(false)),
294                    None => return Ok(None),
295                }
296            }
297            x = nx.prev;
298            y = ny.prev;
299        }
300        Ok(Some(true))
301    }
302
303    /// Two applications of one definition whose argument probe ran out of steps. Unfolding both
304    /// is tried on the same budget; should that run out too, the pair is decided as the algorithm
305    /// without probes decides it — the arguments compared, then both sides unfolded, with no
306    /// budget. So a budget only adds bounded attempts in front of that algorithm: with a budget of
307    /// zero it is that algorithm, and no budget ever costs a verdict.
308    fn decide_abandoned_probe(&mut self, tn: V, sn: V) -> KResult<Step> {
309        let steps = self.k.probe_steps;
310        let tn2 = self.delta(tn)?;
311        let sn2 = self.delta(sn)?;
312        match self.is_def_eq_within(tn2, sn2, steps)? {
313            Some(true) => return Ok(Step::True),
314            Some(false) => return Ok(Step::False(tn2, sn2)),
315            None => {}
316        }
317        if self.is_def_eq_args(tn, sn)? {
318            return Ok(Step::True);
319        }
320        self.st.failure.insert(key(tn, sn), 1);
321        Ok(match self.quick_is_def_eq(tn2, sn2)? {
322            LBool::Undef => Step::Continue(tn2, sn2),
323            LBool::True => Step::True,
324            LBool::False => Step::False(tn2, sn2),
325        })
326    }
327
328    /// The arguments of two applications of the same definition, last to first, skipping the
329    /// positions the definition cannot distinguish.
330    fn is_def_eq_args(&mut self, t: V, s: V) -> KResult<bool> {
331        let (Some((c, ls, _, ts)), Some((_, _, _, ss))) = (self.const_app(t), self.const_app(s))
332        else {
333            return Ok(false);
334        };
335        let n = self.st.arena.spine_len(ts);
336        if n != self.st.arena.spine_len(ss) {
337            return Ok(false);
338        }
339        let mask = self.ignorable_args(c, ls)?;
340        let (mut x, mut y) = (ts, ss);
341        let mut i = n;
342        while x != Sp::NIL {
343            i -= 1;
344            let (nx, ny) = (self.st.arena.spine_node(x), self.st.arena.spine_node(y));
345            let ignorable = i < crate::dag::relevance::MAX_TRACKED && (mask >> i) & 1 == 1;
346            if !ignorable && !self.is_def_eq(nx.arg, ny.arg)? {
347                return Ok(false);
348            }
349            x = nx.prev;
350            y = ny.prev;
351        }
352        Ok(true)
353    }
354
355    /// The argument positions of `c.{ls}` whose arguments need not be compared (see
356    /// [`crate::dag::relevance`]), with the proof positions from this engine's [`Signature`] — so
357    /// that no substitution-engine work (and none of its scratch terms) happens inside a value
358    /// check.
359    ///
360    /// [`Signature`]: crate::dag::relevance::Signature
361    fn ignorable_args(&mut self, c: NameId, ls: LevelsId) -> KResult<u64> {
362        let Some(absent) = self.k.absent_mask(c, ls) else {
363            return Ok(0);
364        };
365        Ok(absent | self.signature(c, ls)?.map_or(0, |s| s.proof_args()))
366    }
367
368    /// The positions of a Π telescope whose binder types are propositions.
369    pub fn proof_positions(&mut self, ty: V) -> KResult<u64> {
370        Ok(self.telescope_signature(ty)?.proof_args())
371    }
372
373    /// η: `t` a lambda, `s` not — `t`'s body against `s x` for a fresh `x`.
374    fn try_eta_expansion_core(&mut self, t: V, s: V) -> KResult<bool> {
375        if !matches!(self.st.arena.get(t), Val::Lam { .. })
376            || matches!(self.st.arena.get(s), Val::Lam { .. })
377        {
378            return Ok(false);
379        }
380        let st = self.type_of(s)?;
381        let w = self.whnf(st)?;
382        let sdom = match self.st.arena.get(w) {
383            Val::Pi { dom, .. } | Val::PiLam { dom, .. } => dom,
384            _ => return Ok(false),
385        };
386        let tdom = self.lam_domain(t)?;
387        if tdom != sdom && !self.is_def_eq(tdom, sdom)? {
388            return Ok(false);
389        }
390        self.under(sdom, |sem, x| {
391            let tb = sem.instantiate(t, x)?;
392            let sx = sem.apply(s, x)?;
393            sem.is_def_eq(tb, sx)
394        })
395    }
396
397    /// Struct-η: `s` a full constructor application of a non-recursive structure, `t` compared to
398    /// it field by field. When `t` applies the same constructor, there is nothing left to try:
399    /// comparing the types compares the parameters and the projections of `t` reduce to its
400    /// fields — exactly the pairs congruence (`is_def_eq_app`, which runs first) found unequal.
401    /// Retrying them, in both directions, at every level of a nest of constructors would cost
402    /// three to the power of its depth.
403    fn try_eta_struct_core(&mut self, t: V, s: V) -> KResult<bool> {
404        let Some((f, _, Kind::Ctor, sp)) = self.const_app(s) else {
405            return Ok(false);
406        };
407        if let Some((g, _, Kind::Ctor, tsp)) = self.const_app(t) {
408            if g == f && self.st.arena.spine_len(tsp) == self.st.arena.spine_len(sp) {
409                return Ok(false);
410            }
411        }
412        let Some(ci) = self.k.env.ctor(f).cloned() else {
413            return Ok(false);
414        };
415        let args = self.st.arena.args(sp);
416        if args.len() != (ci.num_params + ci.num_fields) as usize {
417            return Ok(false);
418        }
419        if !self.k.env.is_non_rec_structure(ci.induct) {
420            return Ok(false);
421        }
422        let tt = self.type_of(t)?;
423        let st = self.type_of(s)?;
424        if !self.is_def_eq(tt, st)? {
425            return Ok(false);
426        }
427        for i in ci.num_params as usize..args.len() {
428            let p = self.proj(ci.induct, (i - ci.num_params as usize) as u32, t)?;
429            if !self.is_def_eq(p, args[i])? {
430                return Ok(false);
431            }
432        }
433        Ok(true)
434    }
435
436    /// Two neutrals with non-empty spines of equal length: heads, then arguments first to last.
437    fn is_def_eq_app(&mut self, t: V, s: V) -> KResult<bool> {
438        let (
439            Val::Neu {
440                kind: k1,
441                head: h1,
442                spine: s1,
443            },
444            Val::Neu {
445                kind: k2,
446                head: h2,
447                spine: s2,
448            },
449        ) = (self.st.arena.get(t), self.st.arena.get(s))
450        else {
451            return Ok(false);
452        };
453        if s1 == Sp::NIL
454            || s2 == Sp::NIL
455            || self.st.arena.spine_len(s1) != self.st.arena.spine_len(s2)
456        {
457            return Ok(false);
458        }
459        let ht = self.bare_head(k1, h1);
460        let hs = self.bare_head(k2, h2);
461        if !self.is_def_eq(ht, hs)? {
462            return Ok(false);
463        }
464        let proofs = self.shared_proof_args(h1, h2)?;
465        let (a1, a2) = (self.st.arena.args(s1), self.st.arena.args(s2));
466        for (i, (a, b)) in a1.iter().zip(a2.iter()).enumerate() {
467            let proof = i < crate::dag::relevance::MAX_TRACKED && (proofs >> i) & 1 == 1;
468            if !proof && !self.is_def_eq(*a, *b)? {
469                return Ok(false);
470            }
471        }
472        Ok(true)
473    }
474
475    /// The proof positions of two applications of one constant: arguments there are proofs of
476    /// propositions that agree once the earlier arguments do, so they need not be compared.
477    fn shared_proof_args(
478        &mut self,
479        h1: super::value::HeadId,
480        h2: super::value::HeadId,
481    ) -> KResult<u64> {
482        let (
483            Head::Const {
484                name: c1,
485                levels: l1,
486            },
487            Head::Const {
488                name: c2,
489                levels: l2,
490            },
491        ) = (self.st.arena.head(h1), self.st.arena.head(h2))
492        else {
493            return Ok(0);
494        };
495        if c1 != c2 || !self.k.s.levels.equiv_lists(l1, l2) {
496            return Ok(0);
497        }
498        Ok(self.signature(c1, l1)?.map_or(0, |s| s.proof_args()))
499    }
500
501    fn bare_head(&mut self, kind: Kind, h: super::value::HeadId) -> V {
502        let head = self.st.arena.head(h);
503        self.st.arena.head_value(kind, head)
504    }
505
506    /// Proof irrelevance: two proofs are equal when their propositions are. A proof and a
507    /// non-proof are not (their types live in different universes), which is what comparing their
508    /// types would find.
509    fn is_def_eq_proof_irrel(&mut self, t: V, s: V) -> KResult<LBool> {
510        if !self.is_proof(t)? {
511            return Ok(LBool::Undef);
512        }
513        if !self.is_proof(s)? {
514            return Ok(LBool::False);
515        }
516        let tt = self.type_of(t)?;
517        let st = self.type_of(s)?;
518        Ok(self.is_def_eq(tt, st)?.into())
519    }
520
521    fn is_delta(&self, v: V) -> Option<Hint> {
522        let (n, _, kind, _) = self.const_app(v)?;
523        if kind != Kind::Delta {
524            return None;
525        }
526        Some(self.k.env.get(n)?.hint())
527    }
528
529    fn is_proj_head(&self, v: V) -> bool {
530        matches!(
531            self.st.arena.get(v),
532            Val::Neu {
533                kind: Kind::Proj,
534                ..
535            }
536        )
537    }
538
539    fn try_unfold_proj_app(&mut self, v: V) -> KResult<Option<V>> {
540        if !self.is_proj_head(v) {
541            return Ok(None);
542        }
543        let v2 = self.whnf_core(v, false)?;
544        Ok((v2 != v).then_some(v2))
545    }
546
547    fn delta(&mut self, v: V) -> KResult<V> {
548        let u = self.unfold(v)?.expect("δ on a value that does not unfold");
549        self.whnf_core(u, true)
550    }
551
552    fn lazy_delta_step(&mut self, tn: V, sn: V) -> KResult<Step> {
553        self.spend()?;
554        let cont = |sem: &mut Sem, tn: V, sn: V| -> KResult<Step> {
555            Ok(match sem.quick_is_def_eq(tn, sn)? {
556                LBool::Undef => Step::Continue(tn, sn),
557                LBool::True => Step::True,
558                LBool::False => Step::False(tn, sn),
559            })
560        };
561        match (self.is_delta(tn), self.is_delta(sn)) {
562            (None, None) => Ok(Step::Unknown(tn, sn)),
563            (Some(_), None) => {
564                if let Some(sn2) = self.try_unfold_proj_app(sn)? {
565                    cont(self, tn, sn2)
566                } else {
567                    let tn2 = self.delta(tn)?;
568                    cont(self, tn2, sn)
569                }
570            }
571            (None, Some(_)) => {
572                if let Some(tn2) = self.try_unfold_proj_app(tn)? {
573                    cont(self, tn2, sn)
574                } else {
575                    let sn2 = self.delta(sn)?;
576                    cont(self, tn, sn2)
577                }
578            }
579            (Some(ht), Some(hs)) => {
580                if ht.lt(hs) {
581                    let sn2 = self.delta(sn)?;
582                    cont(self, tn, sn2)
583                } else if hs.lt(ht) {
584                    let tn2 = self.delta(tn)?;
585                    cont(self, tn2, sn)
586                } else {
587                    let (Some((n1, l1, _, sp1)), Some((n2, l2, _, sp2))) =
588                        (self.const_app(tn), self.const_app(sn))
589                    else {
590                        unreachable!()
591                    };
592                    if sp1 != Sp::NIL
593                        && sp2 != Sp::NIL
594                        && n1 == n2
595                        && matches!(ht, Hint::Regular(_))
596                        && !self.st.failure.contains(&key(tn, sn))
597                    {
598                        if self.k.s.levels.equiv_lists(l1, l2) {
599                            match self.probe_args(tn, sn)? {
600                                Some(true) => return Ok(Step::True),
601                                Some(false) => {}
602                                None => return self.decide_abandoned_probe(tn, sn),
603                            }
604                        }
605                        self.st.failure.insert(key(tn, sn), 1);
606                    }
607                    let tn2 = self.delta(tn)?;
608                    let sn2 = self.delta(sn)?;
609                    cont(self, tn2, sn2)
610                }
611            }
612        }
613    }
614
615    fn is_nat_zero(&self, v: V) -> bool {
616        match self.st.arena.get(v) {
617            Val::Nat(n) => self.k.s.nat(n).is_zero(),
618            _ => {
619                matches!(self.const_app(v), Some((n, ls, _, Sp::NIL)) if n == self.k.wk.nat_zero && ls == LevelsId::EMPTY)
620            }
621        }
622    }
623
624    fn nat_succ_of(&mut self, v: V) -> Option<V> {
625        match self.st.arena.get(v) {
626            Val::Nat(n) => {
627                let x = self.k.s.nat(n).clone();
628                if x.is_zero() {
629                    None
630                } else {
631                    Some(self.nat_value(x.sub(&Nat::from_u64(1))))
632                }
633            }
634            _ => match self.const_app(v) {
635                Some((n, _, _, sp))
636                    if n == self.k.wk.nat_succ && self.st.arena.spine_len(sp) == 1 =>
637                {
638                    Some(self.st.arena.spine_node(sp).arg)
639                }
640                _ => None,
641            },
642        }
643    }
644
645    fn is_def_eq_offset(&mut self, t: V, s: V) -> KResult<LBool> {
646        if self.is_nat_zero(t) && self.is_nat_zero(s) {
647            return Ok(if self.k.reads_nat_literal(&Nat::zero()) {
648                LBool::True
649            } else {
650                LBool::Undef
651            });
652        }
653        if !self.k.nat_literal_rules() {
654            return Ok(LBool::Undef);
655        }
656        match (self.nat_succ_of(t), self.nat_succ_of(s)) {
657            (Some(a), Some(b)) => Ok(self.is_def_eq_core_guarded(a, b)?.into()),
658            _ => Ok(LBool::Undef),
659        }
660    }
661
662    fn lazy_delta_reduction(&mut self, mut tn: V, mut sn: V) -> KResult<Step> {
663        loop {
664            match self.is_def_eq_offset(tn, sn)? {
665                LBool::True => return Ok(Step::True),
666                LBool::False => return Ok(Step::False(tn, sn)),
667                LBool::Undef => {}
668            }
669            if (!self.st.arena.is_open(tn) && !self.st.arena.is_open(sn)) || self.st.eager {
670                if let Some(tn2) = self.reduce_nat(tn)? {
671                    return Ok(if self.is_def_eq_core_guarded(tn2, sn)? {
672                        Step::True
673                    } else {
674                        Step::False(tn2, sn)
675                    });
676                } else if let Some(sn2) = self.reduce_nat(sn)? {
677                    return Ok(if self.is_def_eq_core_guarded(tn, sn2)? {
678                        Step::True
679                    } else {
680                        Step::False(tn, sn2)
681                    });
682                }
683            }
684            match self.lazy_delta_step(tn, sn)? {
685                Step::Continue(a, b) => {
686                    tn = a;
687                    sn = b;
688                }
689                r => return Ok(r),
690            }
691        }
692    }
693
694    fn lazy_delta_proj_reduction(&mut self, mut tn: V, mut sn: V, idx: u32) -> KResult<bool> {
695        loop {
696            match self.lazy_delta_step(tn, sn)? {
697                Step::Continue(a, b) => {
698                    tn = a;
699                    sn = b;
700                }
701                Step::True => return Ok(true),
702                Step::Unknown(a, b) | Step::False(a, b) => {
703                    if let Some(tf) = self.proj_field_of(idx, a)? {
704                        if let Some(sf) = self.proj_field_of(idx, b)? {
705                            return self.is_def_eq_core_guarded(tf, sf);
706                        }
707                    }
708                    return self.is_def_eq_core_guarded(a, b);
709                }
710            }
711        }
712    }
713
714    fn try_string_lit_expansion_core(&mut self, t: V, s: V) -> KResult<LBool> {
715        let Val::Str(sid) = self.st.arena.get(t) else {
716            return Ok(LBool::Undef);
717        };
718        match self.const_app(s) {
719            Some((n, ls, _, sp))
720                if n == self.k.wk.string_of_list
721                    && ls == LevelsId::EMPTY
722                    && self.st.arena.spine_len(sp) == 1 => {}
723            _ => return Ok(LBool::Undef),
724        }
725        let x = self.str_to_ctor(sid)?;
726        Ok(self.is_def_eq_core_guarded(x, s)?.into())
727    }
728
729    fn is_def_eq_unit_like(&mut self, t: V, s: V) -> KResult<bool> {
730        let tt = self.type_of(t)?;
731        let tty = self.whnf(tt)?;
732        let Some((i, _, _, _)) = self.const_app(tty) else {
733            return Ok(false);
734        };
735        let Some(ind) = self.k.env.inductive(i) else {
736            return Ok(false);
737        };
738        if ind.is_rec || ind.ctors.len() != 1 || ind.num_indices != 0 {
739            return Ok(false);
740        }
741        let c = ind.ctors[0];
742        if self.k.env.ctor(c).map(|ci| ci.num_fields) != Some(0) {
743            return Ok(false);
744        }
745        let st = self.type_of(s)?;
746        self.is_def_eq_core_guarded(tty, st)
747    }
748
749    fn is_bool_true(&self, v: V) -> bool {
750        matches!(self.const_app(v), Some((n, _, _, Sp::NIL)) if n == self.k.wk.bool_true)
751    }
752
753    /// A bare head: a constant, a variable or a stuck projection with no arguments.
754    fn bare(&self, v: V) -> Option<Head> {
755        match self.st.arena.get(v) {
756            Val::Neu {
757                head,
758                spine: Sp::NIL,
759                ..
760            } => Some(self.st.arena.head(head)),
761            _ => None,
762        }
763    }
764
765    /// One unit of a running probe's budget; none outside a probe. A probe spends one per
766    /// conversion step and one per δ-unfolding step: either can run without bound under the other.
767    #[inline]
768    fn spend(&mut self) -> KResult<()> {
769        if let Some(steps) = self.st.probe {
770            if steps == 0 {
771                return Err(KernelFailure::exhausted());
772            }
773            self.st.probe = Some(steps - 1);
774        }
775        Ok(())
776    }
777
778    fn is_def_eq_core(&mut self, t: V, s: V) -> KResult<bool> {
779        self.spend()?;
780        match self.quick_is_def_eq(t, s)? {
781            LBool::True => return Ok(true),
782            LBool::False => return Ok(false),
783            LBool::Undef => {}
784        }
785        if (!self.st.arena.is_open(t) || self.st.eager) && self.is_bool_true(s) {
786            let w = self.whnf(t)?;
787            if self.is_bool_true(w) {
788                return Ok(true);
789            }
790        }
791        let tn = self.whnf_core(t, true)?;
792        let sn = self.whnf_core(s, true)?;
793        if tn != t || sn != s {
794            match self.quick_is_def_eq(tn, sn)? {
795                LBool::True => return Ok(true),
796                LBool::False => return Ok(false),
797                LBool::Undef => {}
798            }
799        }
800        match self.is_def_eq_proof_irrel(tn, sn)? {
801            LBool::True => return Ok(true),
802            LBool::False => return Ok(false),
803            LBool::Undef => {}
804        }
805        let (tn, sn) = match self.lazy_delta_reduction(tn, sn)? {
806            Step::True => return Ok(true),
807            Step::False(..) => return Ok(false),
808            Step::Unknown(a, b) => (a, b),
809            Step::Continue(..) => unreachable!(),
810        };
811        match (self.bare(tn), self.bare(sn)) {
812            (
813                Some(Head::Const {
814                    name: tf,
815                    levels: tl,
816                }),
817                Some(Head::Const {
818                    name: sf,
819                    levels: sl,
820                }),
821            ) => {
822                if tf == sf && self.k.s.levels.equiv_lists(tl, sl) {
823                    return Ok(true);
824                }
825            }
826            (Some(Head::Local { level: a, .. }), Some(Head::Local { level: b, .. })) => {
827                if a == b {
828                    return Ok(true);
829                }
830            }
831            (Some(Head::Proj { idx: ti, x: te, .. }), Some(Head::Proj { idx: si, x: se, .. })) => {
832                if ti == si && self.lazy_delta_proj_reduction(te, se, ti)? {
833                    return Ok(true);
834                }
835            }
836            _ => {}
837        }
838        let tnn = self.whnf_core(tn, false)?;
839        let snn = self.whnf_core(sn, false)?;
840        if tnn != tn || snn != sn {
841            return self.is_def_eq_core_guarded(tnn, snn);
842        }
843        if self.is_def_eq_app(tn, sn)? {
844            return Ok(true);
845        }
846        if self.try_eta_expansion_core(tn, sn)? || self.try_eta_expansion_core(sn, tn)? {
847            return Ok(true);
848        }
849        if self.try_eta_struct_core(tn, sn)? || self.try_eta_struct_core(sn, tn)? {
850            return Ok(true);
851        }
852        match self.try_string_lit_expansion_core(tn, sn)? {
853            LBool::True => return Ok(true),
854            LBool::False => return Ok(false),
855            LBool::Undef => match self.try_string_lit_expansion_core(sn, tn)? {
856                LBool::True => return Ok(true),
857                LBool::False => return Ok(false),
858                LBool::Undef => {}
859            },
860        }
861        if self.is_def_eq_unit_like(tn, sn)? {
862            return Ok(true);
863        }
864        Ok(false)
865    }
866}
logicaffeine_kernel/dag/sem/conv.rs

logicaffeine_kernel/dag/sem/
conv.rs
