lemma/parser/
mod.rs

1use crate::ast::{ExpressionIdGenerator, Span};
2use crate::error::LemmaError;
3use crate::resource_limits::ResourceLimits;
4use crate::semantic::*;
5use pest::iterators::Pair;
6use pest::Parser;
7use pest_derive::Parser;
8use std::sync::Arc;
9
10pub mod expressions;
11pub mod facts;
12pub mod literals;
13pub mod rules;
14pub mod units;
15
16#[derive(Parser)]
17#[grammar = "src/parser/lemma.pest"]
18pub struct LemmaParser;
19
20pub fn parse(
21    content: &str,
22    filename: Option<String>,
23    limits: &ResourceLimits,
24) -> Result<Vec<LemmaDoc>, LemmaError> {
25    // Check file size limit
26    if content.len() > limits.max_file_size_bytes {
27        return Err(LemmaError::ResourceLimitExceeded {
28            limit_name: "max_file_size_bytes".to_string(),
29            limit_value: format!(
30                "{} bytes ({} MB)",
31                limits.max_file_size_bytes,
32                limits.max_file_size_bytes / (1024 * 1024)
33            ),
34            actual_value: format!(
35                "{} bytes ({:.2} MB)",
36                content.len(),
37                content.len() as f64 / (1024.0 * 1024.0)
38            ),
39            suggestion: "Reduce file size or split into multiple documents".to_string(),
40        });
41    }
42
43    let mut id_gen = ExpressionIdGenerator::with_max_depth(limits.max_expression_depth);
44    let filename = filename.unwrap_or_else(|| "<input>".to_string());
45
46    match LemmaParser::parse(Rule::lemma_file, content) {
47        Ok(pairs) => {
48            let mut docs = Vec::new();
49            for pair in pairs {
50                if pair.as_rule() == Rule::lemma_file {
51                    for inner_pair in pair.into_inner() {
52                        if inner_pair.as_rule() == Rule::doc {
53                            docs.push(parse_doc(inner_pair, &filename, content, &mut id_gen)?);
54                        }
55                    }
56                }
57            }
58            Ok(docs)
59        }
60        Err(e) => {
61            let pest_span = match e.line_col {
62                pest::error::LineColLocation::Pos((line, col)) => Span {
63                    start: 0,
64                    end: 0,
65                    line,
66                    col,
67                },
68                pest::error::LineColLocation::Span((start_line, start_col), (_, _)) => Span {
69                    start: 0,
70                    end: 0,
71                    line: start_line,
72                    col: start_col,
73                },
74            };
75
76            Err(LemmaError::parse(
77                format!("Parse error: {}", e.variant),
78                pest_span,
79                filename,
80                Arc::from(content),
81                "<parse-error>",
82                1,
83            ))
84        }
85    }
86}
87
88pub fn parse_facts(fact_strings: &[&str]) -> Result<Vec<LemmaFact>, LemmaError> {
89    let mut facts = Vec::new();
90
91    for fact_str in fact_strings {
92        let fact_input = format!("fact {}", fact_str);
93        let pairs = LemmaParser::parse(Rule::fact, &fact_input).map_err(|e| {
94            LemmaError::Engine(format!("Failed to parse fact '{}': {}", fact_str, e))
95        })?;
96
97        let fact_pair = pairs.into_iter().next().ok_or_else(|| {
98            LemmaError::Engine(format!("No parse result for fact '{}'", fact_str))
99        })?;
100
101        let inner_pair = fact_pair
102            .into_inner()
103            .next()
104            .ok_or_else(|| LemmaError::Engine(format!("No inner rule for fact '{}'", fact_str)))?;
105
106        let fact = match inner_pair.as_rule() {
107            Rule::fact_definition => crate::parser::facts::parse_fact_definition(inner_pair)?,
108            Rule::fact_override => crate::parser::facts::parse_fact_override(inner_pair)?,
109            _ => {
110                return Err(LemmaError::Engine(format!(
111                    "Unexpected rule type for fact '{}'",
112                    fact_str
113                )))
114            }
115        };
116
117        facts.push(fact);
118    }
119
120    Ok(facts)
121}
122
123fn parse_doc(
124    pair: Pair<Rule>,
125    filename: &str,
126    _source: &str,
127    id_gen: &mut ExpressionIdGenerator,
128) -> Result<LemmaDoc, LemmaError> {
129    let doc_start_line = pair.as_span().start_pos().line_col().0;
130
131    let mut doc_name: Option<String> = None;
132    let mut commentary: Option<String> = None;
133    let mut facts = Vec::new();
134    let mut rules = Vec::new();
135
136    for inner_pair in pair.into_inner() {
137        match inner_pair.as_rule() {
138            Rule::doc_declaration => {
139                for decl_inner in inner_pair.into_inner() {
140                    if decl_inner.as_rule() == Rule::doc_name {
141                        doc_name = Some(parse_doc_name(decl_inner)?);
142                        break;
143                    }
144                }
145            }
146            Rule::commentary_content => {
147                commentary = Some(inner_pair.as_str().trim().to_string());
148            }
149            Rule::fact_definition => {
150                let fact = crate::parser::facts::parse_fact_definition(inner_pair)?;
151                facts.push(fact);
152            }
153            Rule::fact_override => {
154                let fact = crate::parser::facts::parse_fact_override(inner_pair)?;
155                facts.push(fact);
156            }
157            Rule::rule_definition => {
158                let rule = crate::parser::rules::parse_rule_definition(inner_pair, id_gen)?;
159                rules.push(rule);
160            }
161            _ => {}
162        }
163    }
164
165    let name = doc_name.unwrap_or_else(|| "default".to_string());
166    let mut doc = LemmaDoc::new(name)
167        .with_source(filename.to_string())
168        .with_start_line(doc_start_line);
169
170    if let Some(commentary_text) = commentary {
171        doc = doc.set_commentary(commentary_text);
172    }
173
174    for fact in facts {
175        doc = doc.add_fact(fact);
176    }
177    for rule in rules {
178        doc = doc.add_rule(rule);
179    }
180
181    Ok(doc)
182}
183
184fn parse_doc_name(pair: Pair<Rule>) -> Result<String, LemmaError> {
185    Ok(pair.as_str().to_string())
186}
lemma/parser/mod.rs

lemma/parser/
mod.rs
