logicaffeine_kernel/dag/sem/
value.rs

1//! Semantic values and the arena that interns them.
2//!
3//! A value is what an expression means once its bound variables have values: a closure for a
4//! function or a Π, a neutral (a head and the arguments applied to it) for anything whose head
5//! cannot reduce further by β, a sort, or a literal. Nothing in a value is ever substituted.
6//!
7//! Every value is interned. A neutral application `f a` is built once per pair of ids, a
8//! variable once per (level, type), a constant once per universe instantiation, an environment
9//! once per (parent, value): so two values built the same way from the same parts are the same
10//! id, and a result remembered for an id — its weak-head normal form, its type, a conversion
11//! answer — serves every place that builds it again. The per-value memos are plain arrays indexed
12//! by id, not hash maps.
13
14use super::table::Table;
15use crate::dag::expr::{ExprId, NatId, StrId};
16use crate::dag::level::{LevelId, LevelsId, SubstId};
17use crate::dag::name::NameId;
18
19#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
20pub struct V(pub u32);
21
22/// An environment: the values of the enclosing bound variables, innermost first.
23#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
24pub struct EnvId(pub u32);
25
26impl EnvId {
27    pub const EMPTY: EnvId = EnvId(0);
28}
29
30/// The types of the enclosing bound variables, innermost first (for inference under binders).
31#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
32pub struct CtxId(pub u32);
33
34impl CtxId {
35    pub const EMPTY: CtxId = CtxId(0);
36}
37
38/// The arguments applied to a neutral head, as a snoc list.
39#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
40pub struct Sp(pub u32);
41
42impl Sp {
43    pub const NIL: Sp = Sp(0);
44}
45
46#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
47pub struct HeadId(pub u32);
48
49/// What a neutral's head does under reduction.
50#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
51pub enum Kind {
52    /// A variable bound by a binder being checked or compared.
53    Local,
54    /// A stuck projection `x.idx`.
55    Proj,
56    /// A definition or theorem: δ-reduces.
57    Delta,
58    /// An axiom, opaque definition or inductive type.
59    Opaque,
60    Ctor,
61    Rec,
62    Quot,
63}
64
65#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
66pub enum Head {
67    Local { level: u32, ty: V },
68    Const { name: NameId, levels: LevelsId },
69    Proj { s: NameId, idx: u32, x: V },
70}
71
72#[derive(Copy, Clone, PartialEq, Eq, Debug)]
73pub enum Val {
74    Neu {
75        kind: Kind,
76        head: HeadId,
77        spine: Sp,
78    },
79    /// `fun (x : dom) => body` closed over `env`; the domain is evaluated on demand.
80    Lam {
81        dom: ExprId,
82        env: EnvId,
83        body: ExprId,
84    },
85    Pi {
86        dom: V,
87        env: EnvId,
88        body: ExprId,
89    },
90    /// The type of a lambda: `Π (x : dom), T` where `T` is the type inferred for `body` in `env`
91    /// and `ctx` extended by `x` — inferred only when something asks for the codomain.
92    PiLam {
93        dom: V,
94        env: EnvId,
95        ctx: CtxId,
96        body: ExprId,
97    },
98    Sort(LevelId),
99    Nat(NatId),
100    Str(StrId),
101}
102
103/// The value mentions a variable bound by a binder being checked or compared.
104pub const OPEN: u8 = 1;
105/// Whether the value is a proof has been decided; [`PROOF`] holds the answer.
106const PROOF_KNOWN: u8 = 2;
107const PROOF: u8 = 4;
108
109const NONE: u32 = u32::MAX;
110
111#[derive(Copy, Clone)]
112pub struct SpNode {
113    pub prev: Sp,
114    pub arg: V,
115    pub len: u32,
116}
117
118/// An environment node: either one entry consed onto a parent environment, or a *frame* — a
119/// pruned environment of `len` entries holding only the entries an expression can see, stored
120/// contiguously from `val` (an index into the frame slots). A narrow frame (every live index
121/// below 64) finds an entry by its rank in `live`; a *wide* frame keeps its live indices as a
122/// sorted list (`wide`, an index into the wide-index table) and finds an entry by search.
123///
124/// Every environment also carries the universe substitution its terms are read under (`lsub`):
125/// a universe-polymorphic constant's type and body are evaluated from its own terms, under the
126/// substitution of one use's levels for its parameters, without building an instantiated copy.
127/// An extension inherits its parent's; the empty environment of each substitution is its base.
128#[derive(Copy, Clone)]
129pub struct EnvNode {
130    pub parent: EnvId,
131    pub val: V,
132    pub len: u32,
133    pub open: bool,
134    pub frame: bool,
135    /// Which of the innermost 64 entries are not [`DEAD`].
136    pub live: u64,
137    /// No entry at all is [`DEAD`].
138    pub dense: bool,
139    /// The last pruning of this environment: the mask asked for and the result.
140    pub pmask: u64,
141    pub pres: u32,
142    /// For a wide frame, where its index list starts in the wide-index table (count first).
143    pub wide: u32,
144    /// The universe substitution this environment's terms are read under.
145    pub lsub: SubstId,
146}
147
148/// The placeholder for an environment entry an expression cannot see: value 0 of every session,
149/// closed and inert (a neutral headed by the anonymous constant, which no declaration can be).
150pub const DEAD: V = V(0);
151
152#[derive(Copy, Clone)]
153pub struct CtxNode {
154    pub parent: CtxId,
155    pub ty: V,
156    pub open: bool,
157}
158
159/// A value and what is remembered about it, in one record: a value is created by one push, and
160/// the memos reduction and inference consult sit beside it. A memo is [`NONE`] until set.
161#[derive(Copy, Clone)]
162struct Rec {
163    val: Val,
164    flags: u8,
165    whnf: u32,
166    whnf_core: u32,
167    delta: u32,
168    ty: u32,
169    /// A lambda's evaluated domain.
170    dom: u32,
171}
172
173/// All values of a checking session, their memos, and the tables that intern them.
174#[derive(Clone)]
175pub struct Arena {
176    recs: Vec<Rec>,
177    heads: Vec<Head>,
178    spines: Vec<SpNode>,
179    envs: Vec<EnvNode>,
180    frame_slots: Vec<V>,
181    frame_index: FrameTable,
182    wide_idx: Vec<u32>,
183    base_index: Table<(u32, u32)>,
184    ctxs: Vec<CtxNode>,
185    app_index: Table<(u32, u32)>,
186    head_index: Table<(u32, u32, u32, u32)>,
187    env_index: Table<(u32, u32)>,
188    ctx_index: Table<(u32, u32)>,
189    atom_index: Table<(u32, u32)>,
190    lam_index: Table<(u32, u32, u32)>,
191    pi_index: Table<(u32, u32, u32)>,
192    pilam_index: Table<(u32, u32, u32, u32)>,
193}
194
195/// A head as a table key.
196#[inline]
197fn head_key(h: &Head) -> (u32, u32, u32, u32) {
198    match *h {
199        Head::Local { level, ty } => (0, level, ty.0, 0),
200        Head::Const { name, levels } => (1, name.0, levels.0, 0),
201        Head::Proj { s, idx, x } => (2, s.0, idx, x.0),
202    }
203}
204
205#[inline]
206fn frame_hash(len: u32, mask: u64, vals: &[V]) -> u64 {
207    let k = 0x9E37_79B9_7F4A_7C15u64;
208    let mut h = (mask ^ ((len as u64) << 58)).wrapping_mul(k);
209    for v in vals {
210        h = (h ^ v.0 as u64).wrapping_mul(k).rotate_left(29);
211    }
212    h.wrapping_mul(k)
213}
214
215/// Frames interned by content: open addressing over environment ids, probed by a caller's
216/// equality test (the content lives in the arena, not the table).
217#[derive(Clone)]
218struct FrameTable {
219    slots: Vec<(u64, u32)>,
220    shift: u32,
221    len: usize,
222}
223
224impl FrameTable {
225    /// A vacant slot: every bit set, so that emptying the table is one byte fill.
226    const VACANT: (u64, u32) = (u64::MAX, NONE);
227
228    fn new() -> FrameTable {
229        FrameTable {
230            slots: vec![Self::VACANT; 1 << 10],
231            shift: 64 - 10,
232            len: 0,
233        }
234    }
235
236    fn clear(&mut self) {
237        if self.len > 0 {
238            self.slots.fill(Self::VACANT);
239            self.len = 0;
240        }
241    }
242
243    #[inline]
244    fn find(&self, h: u64, same: impl Fn(u32) -> bool) -> Option<u32> {
245        let mask = self.slots.len() - 1;
246        let mut i = (h >> self.shift) as usize;
247        loop {
248            let (sh, e) = self.slots[i];
249            if e == NONE {
250                return None;
251            }
252            if sh == h && same(e) {
253                return Some(e);
254            }
255            i = (i + 1) & mask;
256        }
257    }
258
259    fn insert(&mut self, h: u64, e: u32) {
260        if (self.len + 1) * 2 > self.slots.len() {
261            let cap = self.slots.len() * 2;
262            let old = std::mem::replace(&mut self.slots, vec![Self::VACANT; cap]);
263            self.shift = 64 - cap.trailing_zeros();
264            for (oh, oe) in old {
265                if oe != NONE {
266                    self.place(oh, oe);
267                }
268            }
269        }
270        self.place(h, e);
271        self.len += 1;
272    }
273
274    fn place(&mut self, h: u64, e: u32) {
275        let mask = self.slots.len() - 1;
276        let mut i = (h >> self.shift) as usize;
277        while self.slots[i].1 != NONE {
278            i = (i + 1) & mask;
279        }
280        self.slots[i] = (h, e);
281    }
282}
283
284const ATOM_SORT: u32 = 0;
285const ATOM_NAT: u32 = 1;
286const ATOM_STR: u32 = 2;
287
288impl Default for Arena {
289    fn default() -> Self {
290        Self::new()
291    }
292}
293
294impl Arena {
295    pub fn new() -> Arena {
296        let mut a = Arena {
297            recs: Vec::new(),
298            heads: Vec::new(),
299            spines: vec![SpNode {
300                prev: Sp::NIL,
301                arg: V(NONE),
302                len: 0,
303            }],
304            envs: vec![EnvNode {
305                parent: EnvId::EMPTY,
306                val: V(NONE),
307                len: 0,
308                open: false,
309                frame: false,
310                live: 0,
311                dense: true,
312                pmask: 0,
313                pres: NONE,
314                wide: NONE,
315                lsub: SubstId::IDENTITY,
316            }],
317            frame_slots: Vec::new(),
318            frame_index: FrameTable::new(),
319            wide_idx: Vec::new(),
320            base_index: Table::new(),
321            ctxs: vec![CtxNode {
322                parent: CtxId::EMPTY,
323                ty: V(NONE),
324                open: false,
325            }],
326            app_index: Table::new(),
327            head_index: Table::new(),
328            env_index: Table::new(),
329            ctx_index: Table::new(),
330            atom_index: Table::new(),
331            lam_index: Table::new(),
332            pi_index: Table::new(),
333            pilam_index: Table::new(),
334        };
335        a.reserve_dead();
336        a
337    }
338
339    fn reserve_dead(&mut self) {
340        let dead = self.head_value(
341            Kind::Opaque,
342            Head::Const {
343                name: NameId::ANON,
344                levels: LevelsId::EMPTY,
345            },
346        );
347        debug_assert_eq!(dead, DEAD);
348    }
349
350    /// Drops every value (the end of a session), keeping the storage for the next session.
351    pub fn reset(&mut self) {
352        self.recs.clear();
353        self.heads.clear();
354        self.spines.truncate(1);
355        self.envs.truncate(1);
356        self.frame_slots.clear();
357        self.frame_index.clear();
358        self.wide_idx.clear();
359        self.base_index.clear();
360        self.ctxs.truncate(1);
361        self.app_index.clear();
362        self.head_index.clear();
363        self.env_index.clear();
364        self.ctx_index.clear();
365        self.atom_index.clear();
366        self.lam_index.clear();
367        self.pi_index.clear();
368        self.pilam_index.clear();
369        self.reserve_dead();
370    }
371
372    pub fn len(&self) -> usize {
373        self.recs.len()
374    }
375
376    pub fn is_empty(&self) -> bool {
377        self.recs.is_empty()
378    }
379
380    fn push(&mut self, v: Val, flags: u8) -> V {
381        let id = V(self.recs.len() as u32);
382        self.recs.push(Rec {
383            val: v,
384            flags,
385            whnf: NONE,
386            whnf_core: NONE,
387            delta: NONE,
388            ty: NONE,
389            dom: NONE,
390        });
391        id
392    }
393
394    #[inline]
395    pub fn get(&self, v: V) -> Val {
396        self.recs[v.0 as usize].val
397    }
398
399    #[inline]
400    pub fn is_open(&self, v: V) -> bool {
401        self.recs[v.0 as usize].flags & OPEN != 0
402    }
403
404    #[inline]
405    pub fn head(&self, h: HeadId) -> Head {
406        self.heads[h.0 as usize]
407    }
408
409    // ---- memos ----
410
411    #[inline]
412    fn memo(r: u32) -> Option<V> {
413        (r != NONE).then_some(V(r))
414    }
415
416    #[inline]
417    pub fn whnf_memo(&self, v: V) -> Option<V> {
418        Self::memo(self.recs[v.0 as usize].whnf)
419    }
420    #[inline]
421    pub fn set_whnf_memo(&mut self, v: V, r: V) {
422        self.recs[v.0 as usize].whnf = r.0;
423    }
424    #[inline]
425    pub fn whnf_core_memo(&self, v: V) -> Option<V> {
426        Self::memo(self.recs[v.0 as usize].whnf_core)
427    }
428    #[inline]
429    pub fn set_whnf_core_memo(&mut self, v: V, r: V) {
430        self.recs[v.0 as usize].whnf_core = r.0;
431    }
432    #[inline]
433    pub fn delta_memo(&self, v: V) -> Option<V> {
434        Self::memo(self.recs[v.0 as usize].delta)
435    }
436    #[inline]
437    pub fn set_delta_memo(&mut self, v: V, r: V) {
438        self.recs[v.0 as usize].delta = r.0;
439    }
440    #[inline]
441    pub fn type_memo(&self, v: V) -> Option<V> {
442        Self::memo(self.recs[v.0 as usize].ty)
443    }
444    #[inline]
445    pub fn set_type_memo(&mut self, v: V, r: V) {
446        self.recs[v.0 as usize].ty = r.0;
447    }
448    /// Whether the value is a proof, once decided.
449    #[inline]
450    pub fn proof_memo(&self, v: V) -> Option<bool> {
451        let f = self.recs[v.0 as usize].flags;
452        (f & PROOF_KNOWN != 0).then_some(f & PROOF != 0)
453    }
454    #[inline]
455    pub fn set_proof_memo(&mut self, v: V, proof: bool) {
456        self.recs[v.0 as usize].flags |= PROOF_KNOWN | if proof { PROOF } else { 0 };
457    }
458    /// A lambda's evaluated domain.
459    #[inline]
460    pub fn dom_memo(&self, v: V) -> Option<V> {
461        Self::memo(self.recs[v.0 as usize].dom)
462    }
463    #[inline]
464    pub fn set_dom_memo(&mut self, v: V, r: V) {
465        self.recs[v.0 as usize].dom = r.0;
466    }
467
468    // ---- construction ----
469
470    #[inline]
471    pub fn find_head(&self, h: &Head) -> Option<V> {
472        self.head_index.get(&head_key(h)).map(V)
473    }
474
475    /// The bare value of a head (no arguments).
476    pub fn head_value(&mut self, kind: Kind, h: Head) -> V {
477        if let Some(v) = self.head_index.get(&head_key(&h)) {
478            return V(v);
479        }
480        let flags = match h {
481            Head::Local { .. } => OPEN,
482            Head::Const { .. } => 0,
483            Head::Proj { x, .. } => self.recs[x.0 as usize].flags & OPEN,
484        };
485        let hid = HeadId(self.heads.len() as u32);
486        self.heads.push(h);
487        let v = self.push(
488            Val::Neu {
489                kind,
490                head: hid,
491                spine: Sp::NIL,
492            },
493            flags,
494        );
495        self.head_index.insert(head_key(&h), v.0);
496        v
497    }
498
499    /// The neutral `f a` for a neutral `f`.
500    pub fn neutral_app(&mut self, f: V, a: V) -> V {
501        if let Some(v) = self.app_index.get(&(f.0, a.0)) {
502            return V(v);
503        }
504        let Val::Neu { kind, head, spine } = self.get(f) else {
505            unreachable!("neutral_app of a non-neutral")
506        };
507        let len = self.spines[spine.0 as usize].len + 1;
508        let sp = Sp(self.spines.len() as u32);
509        self.spines.push(SpNode {
510            prev: spine,
511            arg: a,
512            len,
513        });
514        let flags = (self.recs[f.0 as usize].flags | self.recs[a.0 as usize].flags) & OPEN;
515        let v = self.push(
516            Val::Neu {
517                kind,
518                head,
519                spine: sp,
520            },
521            flags,
522        );
523        self.app_index.insert((f.0, a.0), v.0);
524        v
525    }
526
527    fn atom(&mut self, kind: u32, id: u32, make: impl FnOnce() -> Val) -> V {
528        if let Some(v) = self.atom_index.get(&(kind, id)) {
529            return V(v);
530        }
531        let v = self.push(make(), 0);
532        self.atom_index.insert((kind, id), v.0);
533        v
534    }
535
536    pub fn sort(&mut self, l: LevelId) -> V {
537        self.atom(ATOM_SORT, l.0, || Val::Sort(l))
538    }
539
540    pub fn nat(&mut self, n: NatId) -> V {
541        self.atom(ATOM_NAT, n.0, || Val::Nat(n))
542    }
543
544    pub fn str(&mut self, s: StrId) -> V {
545        self.atom(ATOM_STR, s.0, || Val::Str(s))
546    }
547
548    pub fn lam(&mut self, dom: ExprId, env: EnvId, body: ExprId) -> V {
549        let key = (dom.0, env.0, body.0);
550        if let Some(v) = self.lam_index.get(&key) {
551            return V(v);
552        }
553        let flags = if self.env_open(env) { OPEN } else { 0 };
554        let v = self.push(Val::Lam { dom, env, body }, flags);
555        self.lam_index.insert(key, v.0);
556        v
557    }
558
559    pub fn pi(&mut self, dom: V, env: EnvId, body: ExprId) -> V {
560        let key = (dom.0, env.0, body.0);
561        if let Some(v) = self.pi_index.get(&key) {
562            return V(v);
563        }
564        let flags = if self.is_open(dom) || self.env_open(env) {
565            OPEN
566        } else {
567            0
568        };
569        let v = self.push(Val::Pi { dom, env, body }, flags);
570        self.pi_index.insert(key, v.0);
571        v
572    }
573
574    pub fn pi_lam(&mut self, dom: V, env: EnvId, ctx: CtxId, body: ExprId) -> V {
575        let key = (dom.0, env.0, ctx.0, body.0);
576        if let Some(v) = self.pilam_index.get(&key) {
577            return V(v);
578        }
579        let flags = if self.is_open(dom) || self.env_open(env) || self.ctx_open(ctx) {
580            OPEN
581        } else {
582            0
583        };
584        let v = self.push(
585            Val::PiLam {
586                dom,
587                env,
588                ctx,
589                body,
590            },
591            flags,
592        );
593        self.pilam_index.insert(key, v.0);
594        v
595    }
596
597    // ---- spines ----
598
599    #[inline]
600    pub fn spine_node(&self, s: Sp) -> SpNode {
601        self.spines[s.0 as usize]
602    }
603
604    #[inline]
605    pub fn spine_len(&self, s: Sp) -> usize {
606        self.spines[s.0 as usize].len as usize
607    }
608
609    /// The arguments of a spine, first to last.
610    pub fn args(&self, mut s: Sp) -> smallvec::SmallVec<[V; 8]> {
611        let n = self.spine_len(s);
612        let mut out: smallvec::SmallVec<[V; 8]> = smallvec::SmallVec::with_capacity(n);
613        out.resize(n, V(NONE));
614        let mut i = n;
615        while s != Sp::NIL {
616            let node = self.spines[s.0 as usize];
617            i -= 1;
618            out[i] = node.arg;
619            s = node.prev;
620        }
621        out
622    }
623
624    /// The `i`-th argument (0-based, first to last) of a spine.
625    pub fn arg(&self, s: Sp, i: usize) -> Option<V> {
626        let n = self.spine_len(s);
627        if i >= n {
628            return None;
629        }
630        let mut cur = s;
631        for _ in 0..(n - 1 - i) {
632            cur = self.spines[cur.0 as usize].prev;
633        }
634        Some(self.spines[cur.0 as usize].arg)
635    }
636
637    // ---- environments and contexts ----
638
639    #[inline]
640    pub fn env(&self, e: EnvId) -> EnvNode {
641        self.envs[e.0 as usize]
642    }
643
644    /// The environment `e` was last pruned to with `mask`, if that was the last pruning asked of it.
645    #[inline]
646    pub fn last_prune(&self, e: EnvId, mask: u64) -> Option<EnvId> {
647        let n = &self.envs[e.0 as usize];
648        (n.pres != NONE && n.pmask == mask).then_some(EnvId(n.pres))
649    }
650
651    #[inline]
652    pub fn note_prune(&mut self, e: EnvId, mask: u64, r: EnvId) {
653        let n = &mut self.envs[e.0 as usize];
654        n.pmask = mask;
655        n.pres = r.0;
656    }
657
658    #[inline]
659    pub fn env_open(&self, e: EnvId) -> bool {
660        self.envs[e.0 as usize].open
661    }
662
663    /// The universe substitution `e`'s terms are read under.
664    #[inline]
665    pub fn lsub_of(&self, e: EnvId) -> SubstId {
666        self.envs[e.0 as usize].lsub
667    }
668
669    /// The empty environment of the substitution `s` (for `s` the identity, [`EnvId::EMPTY`]).
670    pub fn lsub_base(&mut self, s: SubstId) -> EnvId {
671        if s == SubstId::IDENTITY {
672            return EnvId::EMPTY;
673        }
674        if let Some(e) = self.base_index.get(&(s.0, 0)) {
675            return EnvId(e);
676        }
677        let id = EnvId(self.envs.len() as u32);
678        self.envs.push(EnvNode {
679            parent: EnvId::EMPTY,
680            val: V(NONE),
681            len: 0,
682            open: false,
683            frame: false,
684            live: 0,
685            dense: true,
686            pmask: 0,
687            pres: NONE,
688            wide: NONE,
689            lsub: s,
690        });
691        self.base_index.insert((s.0, 0), id.0);
692        id
693    }
694
695    /// Whether two environments have the same length and substitution: all that tells them apart
696    /// besides their entries.
697    #[inline]
698    pub fn same_shape(&self, a: EnvId, b: EnvId) -> bool {
699        let (x, y) = (&self.envs[a.0 as usize], &self.envs[b.0 as usize]);
700        x.len == y.len && x.lsub == y.lsub
701    }
702
703    pub fn extend(&mut self, parent: EnvId, val: V) -> EnvId {
704        if let Some(e) = self.env_index.get(&(parent.0, val.0)) {
705            return EnvId(e);
706        }
707        let p = self.envs[parent.0 as usize];
708        let id = EnvId(self.envs.len() as u32);
709        let open = p.open || self.is_open(val);
710        let live = (p.live << 1) | (val != DEAD) as u64;
711        let dense = p.dense && val != DEAD;
712        self.envs.push(EnvNode {
713            parent,
714            val,
715            len: p.len + 1,
716            open,
717            frame: false,
718            live,
719            dense,
720            pmask: 0,
721            pres: NONE,
722            wide: NONE,
723            lsub: p.lsub,
724        });
725        self.env_index.insert((parent.0, val.0), id.0);
726        id
727    }
728
729    /// Entries stored in frames so far this session: what pruning has copied.
730    pub fn frame_slot_count(&self) -> usize {
731        self.frame_slots.len()
732    }
733
734    /// The value of de Bruijn index `i`.
735    #[inline]
736    pub fn lookup(&self, mut e: EnvId, mut i: u32) -> Option<V> {
737        loop {
738            let n = &self.envs[e.0 as usize];
739            if i >= n.len {
740                return None;
741            }
742            if n.frame {
743                return Some(self.frame_entry(n, i));
744            }
745            if i == 0 {
746                return Some(n.val);
747            }
748            i -= 1;
749            e = n.parent;
750        }
751    }
752
753    /// The entries of an environment, innermost first ([`DEAD`] for those pruned away), in one
754    /// walk.
755    pub fn entries(&self, e: EnvId) -> impl Iterator<Item = V> + '_ {
756        let mut cur = e;
757        let mut offset = 0u32;
758        (0..self.envs[e.0 as usize].len).map(move |i| {
759            let n = self.envs[cur.0 as usize];
760            if n.frame {
761                self.frame_entry(&n, i - offset)
762            } else {
763                cur = n.parent;
764                offset += 1;
765                n.val
766            }
767        })
768    }
769
770    /// Entry `i` (below the frame's length) of a frame: its value, or [`DEAD`].
771    #[inline]
772    fn frame_entry(&self, n: &EnvNode, i: u32) -> V {
773        if n.wide == NONE {
774            if i >= 64 || (n.live >> i) & 1 == 0 {
775                return DEAD;
776            }
777            let rank = (n.live & ((1u64 << i) - 1)).count_ones();
778            return self.frame_slots[(n.val.0 + rank) as usize];
779        }
780        match self.wide_indices(n).binary_search(&i) {
781            Ok(rank) => self.frame_slots[n.val.0 as usize + rank],
782            Err(_) => DEAD,
783        }
784    }
785
786    #[inline]
787    fn wide_indices(&self, n: &EnvNode) -> &[u32] {
788        let start = n.wide as usize;
789        let count = self.wide_idx[start] as usize;
790        &self.wide_idx[start + 1..start + 1 + count]
791    }
792
793    /// The values at the positions `mask` marks (innermost first), in one walk.
794    pub fn select(&self, mut e: EnvId, mask: u64, out: &mut smallvec::SmallVec<[V; 16]>) {
795        // `m` is relative to the node reached: bit 0 is that node's entry.
796        let mut m = mask;
797        while m != 0 {
798            let n = &self.envs[e.0 as usize];
799            debug_assert!(n.len > 0, "a referenced entry is in range");
800            if n.frame {
801                let mut r = m;
802                while r != 0 {
803                    out.push(self.frame_entry(n, r.trailing_zeros()));
804                    r &= r - 1;
805                }
806                return;
807            }
808            if m & 1 == 1 {
809                out.push(n.val);
810            }
811            m >>= 1;
812            e = n.parent;
813        }
814    }
815
816    /// The values at `indices` (ascending, innermost first), in one walk.
817    pub fn select_indices(
818        &self,
819        mut e: EnvId,
820        indices: &[u32],
821        out: &mut smallvec::SmallVec<[V; 16]>,
822    ) {
823        let mut pos = 0u32;
824        let mut k = 0;
825        while k < indices.len() {
826            let n = &self.envs[e.0 as usize];
827            debug_assert!(n.len > 0, "a referenced entry is in range");
828            if n.frame {
829                if n.wide == NONE {
830                    for &i in &indices[k..] {
831                        out.push(self.frame_entry(n, i - pos));
832                    }
833                } else {
834                    // Both ascending: one walk over the frame's own indices.
835                    let (wide, mut r) = (self.wide_indices(n), 0);
836                    for &i in &indices[k..] {
837                        let want = i - pos;
838                        while r < wide.len() && wide[r] < want {
839                            r += 1;
840                        }
841                        let hit = r < wide.len() && wide[r] == want;
842                        out.push(if hit {
843                            self.frame_slots[n.val.0 as usize + r]
844                        } else {
845                            DEAD
846                        });
847                    }
848                }
849                return;
850            }
851            if indices[k] == pos {
852                out.push(n.val);
853                k += 1;
854            }
855            pos += 1;
856            e = n.parent;
857        }
858    }
859
860    /// The frame of `len` entries whose live entries are `vals` at the positions `mask` marks
861    /// (innermost first), read under the substitution `lsub`, interned by content.
862    pub fn frame(&mut self, len: u32, mask: u64, vals: &[V], lsub: SubstId) -> EnvId {
863        debug_assert_eq!(mask.count_ones() as usize, vals.len());
864        let h = frame_hash(len, mask, vals) ^ (lsub.0 as u64).wrapping_mul(0xD6E8_FEB8_6659_FD93);
865        if let Some(e) = self.frame_index.find(h, |e| {
866            let n = &self.envs[e as usize];
867            n.wide == NONE
868                && n.len == len
869                && n.live == mask
870                && n.lsub == lsub
871                && &self.frame_slots[n.val.0 as usize..n.val.0 as usize + vals.len()] == vals
872        }) {
873            return EnvId(e);
874        }
875        self.push_frame(h, len, mask, NONE, vals, lsub)
876    }
877
878    /// The frame of `len` entries whose live entries are `vals` at `indices` (ascending, some of
879    /// them 64 or more), read under the substitution `lsub`, interned by content.
880    pub fn wide_frame(&mut self, len: u32, indices: &[u32], vals: &[V], lsub: SubstId) -> EnvId {
881        debug_assert_eq!(indices.len(), vals.len());
882        let mask = indices
883            .iter()
884            .filter(|&&i| i < 64)
885            .fold(0u64, |m, &i| m | (1 << i));
886        let h = indices.iter().fold(frame_hash(len, mask, vals), |h, &i| {
887            (h ^ i as u64).wrapping_mul(0x9E37_79B9_7F4A_7C15)
888        }) ^ (lsub.0 as u64).wrapping_mul(0xD6E8_FEB8_6659_FD93);
889        if let Some(e) = self.frame_index.find(h, |e| {
890            let n = &self.envs[e as usize];
891            n.wide != NONE
892                && n.len == len
893                && n.lsub == lsub
894                && self.wide_indices(n) == indices
895                && &self.frame_slots[n.val.0 as usize..n.val.0 as usize + vals.len()] == vals
896        }) {
897            return EnvId(e);
898        }
899        let wide = self.wide_idx.len() as u32;
900        self.wide_idx.push(indices.len() as u32);
901        self.wide_idx.extend_from_slice(indices);
902        self.push_frame(h, len, mask, wide, vals, lsub)
903    }
904
905    fn push_frame(
906        &mut self,
907        h: u64,
908        len: u32,
909        live: u64,
910        wide: u32,
911        vals: &[V],
912        lsub: SubstId,
913    ) -> EnvId {
914        let start = self.frame_slots.len() as u32;
915        self.frame_slots.extend_from_slice(vals);
916        let open = vals.iter().any(|v| self.is_open(*v));
917        let id = EnvId(self.envs.len() as u32);
918        let dense = vals.len() == len as usize;
919        self.envs.push(EnvNode {
920            parent: EnvId::EMPTY,
921            val: V(start),
922            len,
923            open,
924            frame: true,
925            live,
926            dense,
927            pmask: 0,
928            pres: NONE,
929            wide,
930            lsub,
931        });
932        // Frames are only ever found again through their hash, which is kept in the table.
933        self.frame_index.insert(h, id.0);
934        id
935    }
936
937    pub fn ctx_extend(&mut self, parent: CtxId, ty: V) -> CtxId {
938        if let Some(c) = self.ctx_index.get(&(parent.0, ty.0)) {
939            return CtxId(c);
940        }
941        let id = CtxId(self.ctxs.len() as u32);
942        let open = self.ctxs[parent.0 as usize].open || self.is_open(ty);
943        self.ctxs.push(CtxNode { parent, ty, open });
944        self.ctx_index.insert((parent.0, ty.0), id.0);
945        id
946    }
947
948    pub fn ctx_lookup(&self, mut c: CtxId, mut i: u32) -> Option<V> {
949        loop {
950            if c == CtxId::EMPTY {
951                return None;
952            }
953            let n = self.ctxs[c.0 as usize];
954            if i == 0 {
955                return Some(n.ty);
956            }
957            i -= 1;
958            c = n.parent;
959        }
960    }
961
962    #[inline]
963    fn ctx_open(&self, c: CtxId) -> bool {
964        self.ctxs[c.0 as usize].open
965    }
966
967    /// Bytes held by each part of the arena (capacity: what the process pays).
968    pub fn memory_report(&self) -> Vec<(&'static str, usize)> {
969        vec![
970            (
971                "value engine: values",
972                self.recs.capacity() * std::mem::size_of::<Val>(),
973            ),
974            (
975                "value engine: value memos and flags",
976                self.recs.capacity() * (std::mem::size_of::<Rec>() - std::mem::size_of::<Val>()),
977            ),
978            (
979                "value engine: heads",
980                self.heads.capacity() * std::mem::size_of::<Head>(),
981            ),
982            (
983                "value engine: spines",
984                self.spines.capacity() * std::mem::size_of::<SpNode>(),
985            ),
986            (
987                "value engine: environments and frames",
988                self.envs.capacity() * std::mem::size_of::<EnvNode>()
989                    + self.frame_slots.capacity() * 4,
990            ),
991            ("value engine: application index", self.app_index.bytes()),
992            ("value engine: environment index", self.env_index.bytes()),
993            (
994                "value engine: other indexes",
995                self.head_index.bytes()
996                    + self.ctx_index.bytes()
997                    + self.atom_index.bytes()
998                    + self.lam_index.bytes()
999                    + self.pi_index.bytes()
1000                    + self.pilam_index.bytes(),
1001            ),
1002        ]
1003    }
1004
1005    pub fn bytes(&self) -> usize {
1006        self.memory_report().iter().map(|(_, b)| b).sum()
1007    }
1008}
logicaffeine_kernel/dag/sem/value.rs

logicaffeine_kernel/dag/sem/
value.rs
