oak_lean/builder/
mod.rs

1use crate::{ast::LeanRoot, language::LeanLanguage};
2use oak_core::{Builder, BuilderCache, GreenNode, OakDiagnostics, Parser, RedNode, TextEdit, source::Source};
3
4/// Builder for constructing Lean AST from source text.
5pub struct LeanBuilder<'config> {
6    config: &'config LeanLanguage,
7}
8
9impl<'config> LeanBuilder<'config> {
10    /// Creates a new Lean builder with the given language configuration.
11    pub fn new(config: &'config LeanLanguage) -> Self {
12        Self { config }
13    }
14}
15
16impl<'config> Builder<LeanLanguage> for LeanBuilder<'config> {
17    fn build<'a, S: Source + ?Sized>(&self, source: &'a S, edits: &[TextEdit], cache: &'a mut impl BuilderCache<LeanLanguage>) -> OakDiagnostics<LeanRoot> {
18        let parser = crate::parser::LeanParser::new(self.config);
19        let parse_result = parser.parse(source, edits, cache);
20
21        match parse_result.result {
22            Ok(green_tree) => {
23                let ast_root = self.build_root(green_tree);
24                OakDiagnostics { result: Ok(ast_root), diagnostics: parse_result.diagnostics }
25            }
26            Err(parse_error) => OakDiagnostics { result: Err(parse_error), diagnostics: parse_result.diagnostics },
27        }
28    }
29}
30
31impl<'config> LeanBuilder<'config> {
32    pub(crate) fn build_root<'a>(&self, green_tree: &'a GreenNode<'a, LeanLanguage>) -> LeanRoot {
33        LeanRoot::new(RedNode::new(green_tree, 0).span())
34    }
35}
oak_lean/builder/mod.rs

oak_lean/builder/
mod.rs
