lean_agentic/
environment.rs

1//! Global environment for constants and declarations
2//!
3//! Stores all top-level definitions, axioms, and inductive types
4//! using persistent data structures for efficient cloning.
5
6use crate::symbol::SymbolId;
7use crate::term::TermId;
8use std::collections::HashMap;
9
10/// Attributes for declarations
11#[derive(Debug, Clone, PartialEq, Eq)]
12pub struct Attributes {
13    /// Is this definition reducible (can be unfolded)?
14    pub reducible: bool,
15
16    /// Is this an instance (for type class resolution)?
17    pub instance: bool,
18
19    /// Is this a recursor/eliminator?
20    pub recursor: bool,
21
22    /// Custom attributes
23    pub custom: Vec<String>,
24}
25
26impl Default for Attributes {
27    fn default() -> Self {
28        Self {
29            reducible: true,
30            instance: false,
31            recursor: false,
32            custom: Vec::new(),
33        }
34    }
35}
36
37impl Attributes {
38    /// Create attributes for an opaque definition
39    pub fn opaque() -> Self {
40        Self {
41            reducible: false,
42            ..Default::default()
43        }
44    }
45
46    /// Create attributes for a type class instance
47    pub fn instance() -> Self {
48        Self {
49            instance: true,
50            ..Default::default()
51        }
52    }
53
54    /// Create attributes for a recursor
55    pub fn recursor() -> Self {
56        Self {
57            recursor: true,
58            ..Default::default()
59        }
60    }
61}
62
63/// A constant declaration in the environment
64#[derive(Debug, Clone, PartialEq, Eq)]
65pub struct Declaration {
66    /// Name of the constant
67    pub name: SymbolId,
68
69    /// Universe parameters
70    pub level_params: Vec<u32>,
71
72    /// Type of the constant
73    pub ty: TermId,
74
75    /// Value (body) of the constant (None for axioms)
76    pub value: Option<TermId>,
77
78    /// Attributes
79    pub attrs: Attributes,
80
81    /// Kind of declaration
82    pub kind: DeclKind,
83}
84
85/// Kind of declaration
86#[derive(Debug, Clone, Copy, PartialEq, Eq)]
87pub enum DeclKind {
88    /// Definition with a body
89    Def,
90
91    /// Axiom (no body)
92    Axiom,
93
94    /// Theorem (opaque definition)
95    Theorem,
96
97    /// Inductive type
98    Inductive,
99
100    /// Constructor for an inductive type
101    Constructor,
102
103    /// Recursor/eliminator
104    Recursor,
105}
106
107impl Declaration {
108    /// Create a new definition
109    pub fn def(
110        name: SymbolId,
111        level_params: Vec<u32>,
112        ty: TermId,
113        value: TermId,
114    ) -> Self {
115        Self {
116            name,
117            level_params,
118            ty,
119            value: Some(value),
120            attrs: Attributes::default(),
121            kind: DeclKind::Def,
122        }
123    }
124
125    /// Create a new axiom
126    pub fn axiom(name: SymbolId, level_params: Vec<u32>, ty: TermId) -> Self {
127        Self {
128            name,
129            level_params,
130            ty,
131            value: None,
132            attrs: Attributes::default(),
133            kind: DeclKind::Axiom,
134        }
135    }
136
137    /// Create a new theorem (opaque definition)
138    pub fn theorem(
139        name: SymbolId,
140        level_params: Vec<u32>,
141        ty: TermId,
142        proof: TermId,
143    ) -> Self {
144        Self {
145            name,
146            level_params,
147            ty,
148            value: Some(proof),
149            attrs: Attributes::opaque(),
150            kind: DeclKind::Theorem,
151        }
152    }
153
154    /// Check if this declaration can be unfolded
155    pub fn is_reducible(&self) -> bool {
156        self.attrs.reducible && self.value.is_some()
157    }
158
159    /// Check if this declaration is opaque (cannot be unfolded)
160    pub fn is_opaque(&self) -> bool {
161        !self.attrs.reducible
162    }
163}
164
165/// Inductive type declaration
166#[derive(Debug, Clone)]
167pub struct InductiveDecl {
168    /// Name of the inductive type
169    pub name: SymbolId,
170
171    /// Universe parameters
172    pub level_params: Vec<u32>,
173
174    /// Type of the inductive
175    pub ty: TermId,
176
177    /// Number of parameters (before the colon)
178    pub num_params: u32,
179
180    /// Number of indices (after the colon)
181    pub num_indices: u32,
182
183    /// Constructors
184    pub constructors: Vec<ConstructorDecl>,
185
186    /// Recursor declaration
187    pub recursor: Option<SymbolId>,
188}
189
190/// Constructor declaration
191#[derive(Debug, Clone)]
192pub struct ConstructorDecl {
193    /// Name of the constructor
194    pub name: SymbolId,
195
196    /// Type of the constructor
197    pub ty: TermId,
198
199    /// Number of fields
200    pub num_fields: u32,
201}
202
203/// Global environment
204pub struct Environment {
205    /// All declarations
206    declarations: HashMap<SymbolId, Declaration>,
207
208    /// Inductive type information
209    inductives: HashMap<SymbolId, InductiveDecl>,
210
211    /// Reverse lookup: constructor -> inductive
212    constructor_to_ind: HashMap<SymbolId, SymbolId>,
213}
214
215impl Environment {
216    /// Create a new empty environment
217    pub fn new() -> Self {
218        Self {
219            declarations: HashMap::new(),
220            inductives: HashMap::new(),
221            constructor_to_ind: HashMap::new(),
222        }
223    }
224
225    /// Add a declaration to the environment
226    pub fn add_decl(&mut self, decl: Declaration) -> crate::Result<()> {
227        if self.declarations.contains_key(&decl.name) {
228            return Err(crate::Error::Internal(format!(
229                "Declaration already exists: {:?}",
230                decl.name
231            )));
232        }
233
234        self.declarations.insert(decl.name, decl);
235        Ok(())
236    }
237
238    /// Get a declaration by name
239    pub fn get_decl(&self, name: SymbolId) -> Option<&Declaration> {
240        self.declarations.get(&name)
241    }
242
243    /// Check if a declaration exists
244    pub fn has_decl(&self, name: SymbolId) -> bool {
245        self.declarations.contains_key(&name)
246    }
247
248    /// Add an inductive type
249    pub fn add_inductive(&mut self, ind: InductiveDecl) -> crate::Result<()> {
250        // Add constructor mappings
251        for ctor in &ind.constructors {
252            self.constructor_to_ind.insert(ctor.name, ind.name);
253        }
254
255        self.inductives.insert(ind.name, ind);
256        Ok(())
257    }
258
259    /// Get an inductive type by name
260    pub fn get_inductive(&self, name: SymbolId) -> Option<&InductiveDecl> {
261        self.inductives.get(&name)
262    }
263
264    /// Get the inductive type for a constructor
265    pub fn get_inductive_of_constructor(&self, ctor: SymbolId) -> Option<&InductiveDecl> {
266        let ind_name = self.constructor_to_ind.get(&ctor)?;
267        self.get_inductive(*ind_name)
268    }
269
270    /// Check if a name is a constructor
271    pub fn is_constructor(&self, name: SymbolId) -> bool {
272        self.constructor_to_ind.contains_key(&name)
273    }
274
275    /// Get all declarations
276    pub fn declarations(&self) -> impl Iterator<Item = (&SymbolId, &Declaration)> {
277        self.declarations.iter()
278    }
279
280    /// Get the number of declarations
281    pub fn num_decls(&self) -> usize {
282        self.declarations.len()
283    }
284
285    /// Clone the environment (cheap due to persistent data structures)
286    pub fn fork(&self) -> Self {
287        Self {
288            declarations: self.declarations.clone(),
289            inductives: self.inductives.clone(),
290            constructor_to_ind: self.constructor_to_ind.clone(),
291        }
292    }
293}
294
295impl Default for Environment {
296    fn default() -> Self {
297        Self::new()
298    }
299}
300
301impl Clone for Environment {
302    fn clone(&self) -> Self {
303        self.fork()
304    }
305}
306
307#[cfg(test)]
308mod tests {
309    use super::*;
310
311    #[test]
312    fn test_environment_basic() {
313        let mut env = Environment::new();
314
315        let name = SymbolId::new(0);
316        let ty = TermId::new(0);
317        let value = TermId::new(1);
318
319        let decl = Declaration::def(name, vec![], ty, value);
320        env.add_decl(decl).unwrap();
321
322        assert!(env.has_decl(name));
323        let retrieved = env.get_decl(name).unwrap();
324        assert_eq!(retrieved.ty, ty);
325        assert_eq!(retrieved.value, Some(value));
326    }
327
328    #[test]
329    fn test_duplicate_declaration() {
330        let mut env = Environment::new();
331
332        let name = SymbolId::new(0);
333        let decl = Declaration::axiom(name, vec![], TermId::new(0));
334
335        env.add_decl(decl.clone()).unwrap();
336        let result = env.add_decl(decl);
337
338        assert!(result.is_err());
339    }
340
341    #[test]
342    fn test_environment_fork() {
343        let mut env1 = Environment::new();
344
345        let name = SymbolId::new(0);
346        let decl = Declaration::axiom(name, vec![], TermId::new(0));
347        env1.add_decl(decl).unwrap();
348
349        let env2 = env1.fork();
350        assert!(env2.has_decl(name));
351        assert_eq!(env1.num_decls(), env2.num_decls());
352    }
353
354    #[test]
355    fn test_reducibility() {
356        let name = SymbolId::new(0);
357
358        let def = Declaration::def(name, vec![], TermId::new(0), TermId::new(1));
359        assert!(def.is_reducible());
360
361        let axiom = Declaration::axiom(name, vec![], TermId::new(0));
362        assert!(!axiom.is_reducible());
363
364        let theorem = Declaration::theorem(name, vec![], TermId::new(0), TermId::new(1));
365        assert!(!theorem.is_reducible()); // Theorems are opaque
366    }
367}
lean_agentic/environment.rs

lean_agentic/
environment.rs
