oxilean_std/env_builder/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name, ReducibilityHint};
6
7/// A thin wrapper around `Environment` providing convenience methods for
8/// registering axioms and definitions during standard library initialisation.
9pub struct EnvBuilder {
10    env: Environment,
11    errors: Vec<String>,
12}
13impl EnvBuilder {
14    /// Create a new builder from an existing environment.
15    pub fn new(env: Environment) -> Self {
16        Self {
17            env,
18            errors: Vec::new(),
19        }
20    }
21    /// Create a builder around a fresh `Environment::new()`.
22    pub fn fresh() -> Self {
23        Self::new(Environment::new())
24    }
25    /// Add an axiom with the given name and type.
26    pub fn add_axiom(&mut self, name: Name, ty: Expr) {
27        let result = self.env.add(Declaration::Axiom {
28            name,
29            univ_params: vec![],
30            ty,
31        });
32        if let Err(e) = result {
33            self.errors.push(e.to_string());
34        }
35    }
36    /// Add an axiom using a `&str` name.
37    pub fn axiom(&mut self, name: &str, ty: Expr) -> &mut Self {
38        self.add_axiom(Name::str(name), ty);
39        self
40    }
41    /// Add a definition with the given name, type, and value.
42    pub fn add_definition(&mut self, name: Name, ty: Expr, value: Expr) {
43        let result = self.env.add(Declaration::Definition {
44            name,
45            univ_params: vec![],
46            ty,
47            val: value,
48            hint: ReducibilityHint::Regular(0),
49        });
50        if let Err(e) = result {
51            self.errors.push(e.to_string());
52        }
53    }
54    /// Add a definition using a `&str` name (builder-style).
55    pub fn def(&mut self, name: &str, ty: Expr, value: Expr) -> &mut Self {
56        self.add_definition(Name::str(name), ty, value);
57        self
58    }
59    /// Add a theorem (opaque definition) using a `&str` name.
60    pub fn theorem(&mut self, name: &str, ty: Expr, proof: Expr) -> &mut Self {
61        let result = self.env.add(Declaration::Theorem {
62            name: Name::str(name),
63            univ_params: vec![],
64            ty,
65            val: proof,
66        });
67        if let Err(e) = result {
68            self.errors.push(e.to_string());
69        }
70        self
71    }
72    /// Add a `Sorry` opaque axiom — useful for placeholder proofs.
73    pub fn sorry(&mut self, name: &str, ty: Expr) -> &mut Self {
74        self.axiom(name, ty)
75    }
76    /// Finish building and return the environment, or an error string.
77    pub fn finish(self) -> Result<Environment, String> {
78        if self.errors.is_empty() {
79            Ok(self.env)
80        } else {
81            Err(self.errors.join("; "))
82        }
83    }
84    /// Finish building, panicking on any error.  Useful in tests.
85    pub fn finish_or_panic(self) -> Environment {
86        match self.finish() {
87            Ok(env) => env,
88            Err(e) => panic!("EnvBuilder errors: {}", e),
89        }
90    }
91    /// Get a reference to the underlying environment.
92    pub fn env(&self) -> &Environment {
93        &self.env
94    }
95    /// `true` if no errors have been accumulated.
96    pub fn is_ok(&self) -> bool {
97        self.errors.is_empty()
98    }
99    /// Return the accumulated error messages.
100    pub fn errors(&self) -> &[String] {
101        &self.errors
102    }
103    /// Check whether `name` has been registered.
104    pub fn contains(&self, name: &str) -> bool {
105        self.env.get(&Name::str(name)).is_some()
106    }
107}
oxilean_std/env_builder/types.rs

oxilean_std/env_builder/
types.rs
