logicaffeine_kernel/dag/
wellknown.rs

1//! Names the kernel gives meaning to, interned once so every test is an id compare.
2
3use super::name::{NameId, Names};
4
5/// One quotient's four constants: its former, constructor, lift and induction principle.
6#[derive(Clone, Copy, Debug, PartialEq, Eq)]
7pub struct QuotNames {
8    pub ty: NameId,
9    pub mk: NameId,
10    pub lift: NameId,
11    pub ind: NameId,
12}
13
14#[derive(Clone)]
15pub struct WellKnown {
16    pub nat: NameId,
17    pub nat_zero: NameId,
18    pub nat_succ: NameId,
19    pub nat_add: NameId,
20    pub nat_sub: NameId,
21    pub nat_mul: NameId,
22    pub nat_pow: NameId,
23    pub nat_gcd: NameId,
24    pub nat_mod: NameId,
25    pub nat_div: NameId,
26    pub nat_beq: NameId,
27    pub nat_ble: NameId,
28    pub nat_land: NameId,
29    pub nat_lor: NameId,
30    pub nat_xor: NameId,
31    pub nat_shift_left: NameId,
32    pub nat_shift_right: NameId,
33    pub nat_pred: NameId,
34    pub nat_bitwise: NameId,
35    pub bool_: NameId,
36    pub bool_true: NameId,
37    pub bool_false: NameId,
38    pub string: NameId,
39    pub string_of_list: NameId,
40    pub char_: NameId,
41    pub char_of_nat: NameId,
42    pub list_nil: NameId,
43    pub list_cons: NameId,
44    pub list: NameId,
45    pub eq: NameId,
46    pub quot: NameId,
47    pub quot_mk: NameId,
48    pub quot_lift: NameId,
49    pub quot_ind: NameId,
50    /// A second quotient the theory admits beside its own: under LOGOS's theory, the one a kernel
51    /// installs (`kernel.quot.*`, `quotient::Kind`'s names) for content imported from Lean.
52    pub installed_quot: Option<QuotNames>,
53    /// The theory's own `true` beside the primitives' `Bool.true`, where they differ: LOGOS's
54    /// `true`, read by the `decide` fast path (`Kernel::is_true_constant`).
55    pub logos_true: Option<NameId>,
56    pub eager_reduce: NameId,
57    pub opt_param: NameId,
58    pub auto_param: NameId,
59    pub out_param: NameId,
60    pub semi_out_param: NameId,
61    pub nested_prefix: NameId,
62    pub u: NameId,
63}
64
65impl WellKnown {
66    pub fn new(n: &mut Names) -> WellKnown {
67        WellKnown {
68            nat: n.dotted("Nat"),
69            nat_zero: n.dotted("Nat.zero"),
70            nat_succ: n.dotted("Nat.succ"),
71            nat_add: n.dotted("Nat.add"),
72            nat_sub: n.dotted("Nat.sub"),
73            nat_mul: n.dotted("Nat.mul"),
74            nat_pow: n.dotted("Nat.pow"),
75            nat_gcd: n.dotted("Nat.gcd"),
76            nat_mod: n.dotted("Nat.mod"),
77            nat_div: n.dotted("Nat.div"),
78            nat_beq: n.dotted("Nat.beq"),
79            nat_ble: n.dotted("Nat.ble"),
80            nat_land: n.dotted("Nat.land"),
81            nat_lor: n.dotted("Nat.lor"),
82            nat_xor: n.dotted("Nat.xor"),
83            nat_shift_left: n.dotted("Nat.shiftLeft"),
84            nat_shift_right: n.dotted("Nat.shiftRight"),
85            nat_pred: n.dotted("Nat.pred"),
86            nat_bitwise: n.dotted("Nat.bitwise"),
87            bool_: n.dotted("Bool"),
88            bool_true: n.dotted("Bool.true"),
89            bool_false: n.dotted("Bool.false"),
90            string: n.dotted("String"),
91            string_of_list: n.dotted("String.ofList"),
92            char_: n.dotted("Char"),
93            char_of_nat: n.dotted("Char.ofNat"),
94            list_nil: n.dotted("List.nil"),
95            list_cons: n.dotted("List.cons"),
96            list: n.dotted("List"),
97            eq: n.dotted("Eq"),
98            quot: n.dotted("Quot"),
99            quot_mk: n.dotted("Quot.mk"),
100            quot_lift: n.dotted("Quot.lift"),
101            quot_ind: n.dotted("Quot.ind"),
102            installed_quot: None,
103            logos_true: None,
104            eager_reduce: n.dotted("eagerReduce"),
105            opt_param: n.dotted("optParam"),
106            auto_param: n.dotted("autoParam"),
107            out_param: n.dotted("outParam"),
108            semi_out_param: n.dotted("semiOutParam"),
109            nested_prefix: n.dotted("_nested"),
110            u: n.dotted("u"),
111        }
112    }
113
114    /// The same meanings in a LOGOS context. LOGOS's own constants keep its spelling: `Nat`,
115    /// `Zero`/`Succ`, `Eq` and the quotient's `Quot_mk`/`Quot_lift`/`Quot_ind`, its `true` read by
116    /// the `decide` fast path. A meaning only Lean content has (the `Nat` operations, `Bool`,
117    /// `Char`, `String`, `List`, the elaborator's markers) is spelled as the Lean importer names it
118    /// in a LOGOS context (`dag::name::kernel_name_of_components`), so an imported
119    /// `Nat.div` is the primitive it is, checked and computed as in Lean's theory.
120    pub fn logos(n: &mut Names) -> WellKnown {
121        let one = |n: &mut Names, s: &str| n.str(NameId::ANON, s);
122        let lean = |n: &mut Names, s: &str| {
123            let components: Vec<&str> = s.split('.').collect();
124            let spelled = super::name::kernel_name_of_components(&components);
125            n.str(NameId::ANON, &spelled)
126        };
127        WellKnown {
128            nat: one(n, "Nat"),
129            nat_zero: one(n, "Zero"),
130            nat_succ: one(n, "Succ"),
131            nat_add: lean(n, "Nat.add"),
132            nat_sub: lean(n, "Nat.sub"),
133            nat_mul: lean(n, "Nat.mul"),
134            nat_pow: lean(n, "Nat.pow"),
135            nat_gcd: lean(n, "Nat.gcd"),
136            nat_mod: lean(n, "Nat.mod"),
137            nat_div: lean(n, "Nat.div"),
138            nat_beq: lean(n, "Nat.beq"),
139            nat_ble: lean(n, "Nat.ble"),
140            nat_land: lean(n, "Nat.land"),
141            nat_lor: lean(n, "Nat.lor"),
142            nat_xor: lean(n, "Nat.xor"),
143            nat_shift_left: lean(n, "Nat.shiftLeft"),
144            nat_shift_right: lean(n, "Nat.shiftRight"),
145            nat_pred: lean(n, "Nat.pred"),
146            nat_bitwise: lean(n, "Nat.bitwise"),
147            bool_: lean(n, "Bool"),
148            bool_true: lean(n, "Bool.true"),
149            bool_false: lean(n, "Bool.false"),
150            string: lean(n, "String"),
151            string_of_list: lean(n, "String.ofList"),
152            char_: lean(n, "Char"),
153            char_of_nat: lean(n, "Char.ofNat"),
154            list_nil: lean(n, "List.nil"),
155            list_cons: lean(n, "List.cons"),
156            list: lean(n, "List"),
157            quot_mk: one(n, "Quot_mk"),
158            quot_lift: one(n, "Quot_lift"),
159            quot_ind: one(n, "Quot_ind"),
160            installed_quot: Some(QuotNames {
161                ty: one(n, crate::quotient::Kind::Type.name()),
162                mk: one(n, crate::quotient::Kind::Constructor.name()),
163                lift: one(n, crate::quotient::Kind::Lift.name()),
164                ind: one(n, crate::quotient::Kind::Induction.name()),
165            }),
166            logos_true: Some(one(n, "true")),
167            eager_reduce: lean(n, "eagerReduce"),
168            opt_param: lean(n, "optParam"),
169            auto_param: lean(n, "autoParam"),
170            out_param: lean(n, "outParam"),
171            semi_out_param: lean(n, "semiOutParam"),
172            ..WellKnown::new(n)
173        }
174    }
175
176    /// The theory's own quotient.
177    pub fn quot_names(&self) -> QuotNames {
178        QuotNames {
179            ty: self.quot,
180            mk: self.quot_mk,
181            lift: self.quot_lift,
182            ind: self.quot_ind,
183        }
184    }
185
186    /// The names Lean's kernel treats as primitive: declaring one is only allowed in its
187    /// canonical form.
188    pub fn primitives(&self) -> [NameId; 24] {
189        [
190            self.bool_,
191            self.bool_false,
192            self.bool_true,
193            self.nat,
194            self.nat_zero,
195            self.nat_succ,
196            self.nat_add,
197            self.nat_pred,
198            self.nat_sub,
199            self.nat_mul,
200            self.nat_pow,
201            self.nat_gcd,
202            self.nat_mod,
203            self.nat_div,
204            self.nat_beq,
205            self.nat_ble,
206            self.nat_bitwise,
207            self.nat_land,
208            self.nat_lor,
209            self.nat_xor,
210            self.nat_shift_left,
211            self.nat_shift_right,
212            self.string_of_list,
213            self.char_of_nat,
214        ]
215    }
216}
logicaffeine_kernel/dag/wellknown.rs

logicaffeine_kernel/dag/
wellknown.rs
