logicaffeine_kernel/
reify.rs

1//! Shared reification substrate for the arithmetic decision procedures.
2//!
3//! `ring`, `lia`, and `omega` all read the same deep embedding of terms
4//! (`SLit`/`SVar`/`SName`/`SApp` applied via kernel `App` nodes). The pattern
5//! extractors live here once, and so does [`VarInterner`], which maps named
6//! globals to variable indices.
7//!
8//! # Why an interner
9//!
10//! Named globals must reify to variable indices that are (a) distinct for
11//! distinct names and (b) stable across every term reified for one goal —
12//! the left- and right-hand sides of an equation, or a hypothesis set and its
13//! conclusion. A hash of the name satisfies (b) but not (a): a collision
14//! identifies two different variables and lets the procedure prove `Aa = BB`.
15//! The interner satisfies both by construction; callers create one per goal
16//! and thread it through every reification belonging to that goal.
17
18use std::collections::HashMap;
19
20use crate::term::{Literal, Term};
21
22/// Per-goal map from global names to variable indices.
23///
24/// Indices are negative, starting far from zero, so they can never collide
25/// with `SVar` de Bruijn indices (which are non-negative).
26#[derive(Debug, Default)]
27pub struct VarInterner {
28    map: HashMap<String, i64>,
29    next: i64,
30}
31
32impl VarInterner {
33    pub fn new() -> Self {
34        VarInterner {
35            map: HashMap::new(),
36            next: -1_000_000,
37        }
38    }
39
40    /// The index for `name`, allocating a fresh one on first sight.
41    pub fn intern(&mut self, name: &str) -> i64 {
42        if let Some(&idx) = self.map.get(name) {
43            return idx;
44        }
45        let idx = self.next;
46        self.next -= 1;
47        self.map.insert(name.to_string(), idx);
48        idx
49    }
50}
51
52/// Extract integer from `SLit n`.
53pub(crate) fn extract_slit(term: &Term) -> Option<i64> {
54    if let Term::App(ctor, arg) = term {
55        if let Term::Global(name) = ctor.as_ref() {
56            if name == "SLit" {
57                if let Term::Lit(Literal::Int(n)) = arg.as_ref() {
58                    return Some(*n);
59                }
60            }
61        }
62    }
63    None
64}
65
66/// Extract variable index from `SVar i`.
67pub(crate) fn extract_svar(term: &Term) -> Option<i64> {
68    if let Term::App(ctor, arg) = term {
69        if let Term::Global(name) = ctor.as_ref() {
70            if name == "SVar" {
71                if let Term::Lit(Literal::Int(i)) = arg.as_ref() {
72                    return Some(*i);
73                }
74            }
75        }
76    }
77    None
78}
79
80/// Extract name from `SName "x"`.
81pub(crate) fn extract_sname(term: &Term) -> Option<String> {
82    if let Term::App(ctor, arg) = term {
83        if let Term::Global(name) = ctor.as_ref() {
84            if name == "SName" {
85                if let Term::Lit(Literal::Text(s)) = arg.as_ref() {
86                    return Some(s.clone());
87                }
88            }
89        }
90    }
91    None
92}
93
94/// Extract binary application: `SApp (SApp (SName "op") a) b`.
95pub(crate) fn extract_binary_app(term: &Term) -> Option<(String, Term, Term)> {
96    if let Term::App(outer, b) = term {
97        if let Term::App(sapp_outer, inner) = outer.as_ref() {
98            if let Term::Global(ctor) = sapp_outer.as_ref() {
99                if ctor == "SApp" {
100                    if let Term::App(partial, a) = inner.as_ref() {
101                        if let Term::App(sapp_inner, op_term) = partial.as_ref() {
102                            if let Term::Global(ctor2) = sapp_inner.as_ref() {
103                                if ctor2 == "SApp" {
104                                    if let Some(op) = extract_sname(op_term) {
105                                        return Some((
106                                            op,
107                                            a.as_ref().clone(),
108                                            b.as_ref().clone(),
109                                        ));
110                                    }
111                                }
112                            }
113                        }
114                    }
115                }
116            }
117        }
118    }
119    None
120}
121
122#[cfg(test)]
123mod tests {
124    use super::*;
125
126    #[test]
127    fn interner_distinct_names_distinct_indices() {
128        let mut it = VarInterner::new();
129        let a = it.intern("Aa");
130        let b = it.intern("BB");
131        assert_ne!(a, b);
132    }
133
134    #[test]
135    fn interner_same_name_same_index() {
136        let mut it = VarInterner::new();
137        assert_eq!(it.intern("x"), it.intern("x"));
138    }
139
140    #[test]
141    fn interner_indices_negative_below_svar_range() {
142        let mut it = VarInterner::new();
143        assert!(it.intern("x") <= -1_000_000);
144    }
145}
logicaffeine_kernel/reify.rs

logicaffeine_kernel/
reify.rs
