oak_coq/builder/
mod.rs

1use crate::{CoqParser, ast::*, language::CoqLanguage};
2use oak_core::{Builder, BuilderCache, GreenNode, OakDiagnostics, SourceText, TextEdit, source::Source};
3
4/// Coq 语言的 AST 构建器
5#[derive(Clone)]
6pub struct CoqBuilder<'config> {
7    /// 语言配置
8    config: &'config CoqLanguage,
9}
10
11impl<'config> CoqBuilder<'config> {
12    /// 创建新的 Coq 构建器
13    pub fn new(config: &'config CoqLanguage) -> Self {
14        Self { config }
15    }
16
17    /// 从语法树构建 AST 根节点
18    pub fn build_root(&self, _green: &GreenNode<CoqLanguage>, _source: &SourceText) -> Result<CoqRoot, oak_core::OakError> {
19        // 简化的 AST 构建逻辑
20        Ok(CoqRoot::new())
21    }
22}
23
24impl<'config> Builder<CoqLanguage> for CoqBuilder<'config> {
25    fn build<'a, S: Source + ?Sized>(&self, source: &S, edits: &[TextEdit], _cache: &'a mut impl BuilderCache<CoqLanguage>) -> oak_core::builder::BuildOutput<CoqLanguage> {
26        let parser = CoqParser::new(self.config);
27        let lexer = crate::lexer::CoqLexer::new(&self.config);
28
29        let mut cache = oak_core::parser::session::ParseSession::<CoqLanguage>::default();
30        let parse_result = oak_core::parser::parse(&parser, &lexer, source, edits, &mut cache);
31
32        match parse_result.result {
33            Ok(green_tree) => {
34                let source_text = SourceText::new(source.get_text_in((0..source.length()).into()).into_owned());
35                match self.build_root(green_tree, &source_text) {
36                    Ok(ast_root) => OakDiagnostics { result: Ok(ast_root), diagnostics: parse_result.diagnostics },
37                    Err(build_error) => {
38                        let mut diagnostics = parse_result.diagnostics;
39                        diagnostics.push(build_error.clone());
40                        OakDiagnostics { result: Err(build_error), diagnostics }
41                    }
42                }
43            }
44            Err(parse_error) => OakDiagnostics { result: Err(parse_error), diagnostics: parse_result.diagnostics },
45        }
46    }
47}
oak_coq/builder/mod.rs

oak_coq/builder/
mod.rs
