lemma/parser/
mod.rs

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

lemma/parser/
mod.rs
