oak-lean 0.0.11

Lean theorem prover language parser with support for dependent types and formal verification.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

use crate::{ast::LeanRoot, language::LeanLanguage};
use oak_core::{Builder, BuilderCache, GreenNode, OakDiagnostics, Parser, RedNode, TextEdit, source::Source};

/// Builder for constructing Lean AST from source text.
pub struct LeanBuilder<'config> {
    config: &'config LeanLanguage,
}

impl<'config> LeanBuilder<'config> {
    /// Creates a new Lean builder with the given language configuration.
    pub fn new(config: &'config LeanLanguage) -> Self {
        Self { config }
    }
}

impl<'config> Builder<LeanLanguage> for LeanBuilder<'config> {
    fn build<'a, S: Source + ?Sized>(&self, source: &'a S, edits: &[TextEdit], cache: &'a mut impl BuilderCache<LeanLanguage>) -> OakDiagnostics<LeanRoot> {
        let parser = crate::parser::LeanParser::new(self.config);
        let parse_result = parser.parse(source, edits, cache);

        match parse_result.result {
            Ok(green_tree) => {
                let ast_root = self.build_root(green_tree);
                OakDiagnostics { result: Ok(ast_root), diagnostics: parse_result.diagnostics }
            }
            Err(parse_error) => OakDiagnostics { result: Err(parse_error), diagnostics: parse_result.diagnostics },
        }
    }
}

impl<'config> LeanBuilder<'config> {
    pub(crate) fn build_root<'a>(&self, green_tree: &'a GreenNode<'a, LeanLanguage>) -> LeanRoot {
        LeanRoot::new(RedNode::new(green_tree, 0).span())
    }
}