logicaffeine_kernel/interface/
command_parser.rs

1//! Parser for Vernacular commands.
2//!
3//! Commands:
4//! - Definition name : type := term.
5//! - Definition name := term.  (type inferred)
6//! - Check term.
7//! - Eval term.
8//! - Inductive Name := C1 : T1 | C2 : T2.
9//!
10//! # Literate Syntax (dispatched to literate_parser)
11//!
12//! - A Bool is either Yes or No.
13//! - ## To add (n: Nat) and (m: Nat) -> Nat: ...
14
15use super::command::Command;
16use super::error::ParseError;
17use super::literate_parser;
18use super::term_parser::TermParser;
19use crate::{Term, Universe};
20
21/// Parse a command from input string.
22///
23/// This function acts as a dispatcher, routing Literate syntax to the
24/// literate_parser module and Coq-style syntax to the existing parsers.
25pub fn parse_command(input: &str) -> Result<Command, ParseError> {
26    let input = input.trim();
27
28    // ============================================================
29    // LITERATE SYNTAX DISPATCH (check first)
30    // ============================================================
31
32    // 1. Literate Data Definition: "A Nat is either..." or "An Option is either..."
33    if (input.starts_with("A ") || input.starts_with("An ")) && input.contains(" is either") {
34        return literate_parser::parse_inductive(input);
35    }
36
37    // 2. Literate Function Definition: "## To add..."
38    if input.starts_with("## To ") {
39        return literate_parser::parse_definition(input);
40    }
41
42    // 3. Literate Constant Definition: "Let X be Y."
43    if input.starts_with("Let ") && input.contains(" be ") {
44        return literate_parser::parse_let_definition(input);
45    }
46
47    // 4. Literate Theorem Declaration: "## Theorem: Name"
48    if input.starts_with("## Theorem:") {
49        return literate_parser::parse_theorem(input);
50    }
51
52    // ============================================================
53    // EXISTING COQ-STYLE DISPATCH (fallback)
54    // ============================================================
55
56    // Remove trailing period if present (for Coq-style commands)
57    let input = input.strip_suffix('.').unwrap_or(input).trim();
58
59    if input.starts_with("Definition") {
60        parse_definition(&input[10..].trim_start())
61    } else if input.starts_with("Check") {
62        parse_check(&input[5..].trim_start())
63    } else if input.starts_with("Eval") {
64        parse_eval(&input[4..].trim_start())
65    } else if input.starts_with("Inductive") {
66        parse_inductive(&input[9..].trim_start())
67    } else {
68        Err(ParseError::UnknownCommand(
69            input.split_whitespace().next().unwrap_or(input).to_string(),
70        ))
71    }
72}
73
74/// Parse: name : type := term  OR  name := term
75fn parse_definition(input: &str) -> Result<Command, ParseError> {
76    // Find the := delimiter
77    let assign_pos = input.find(":=").ok_or(ParseError::Missing(":=".to_string()))?;
78
79    let before_assign = input[..assign_pos].trim();
80    let body_str = input[assign_pos + 2..].trim();
81
82    // Check if there's a type annotation (: before :=)
83    if let Some(colon_pos) = before_assign.find(':') {
84        // Has type annotation: name : type
85        let name = before_assign[..colon_pos].trim().to_string();
86        let type_str = before_assign[colon_pos + 1..].trim();
87
88        if name.is_empty() {
89            return Err(ParseError::Missing("definition name".to_string()));
90        }
91
92        let (ty, implicit_count) = TermParser::parse_with_implicits(type_str)?;
93        let body = TermParser::parse(body_str)?;
94
95        Ok(Command::Definition {
96            name,
97            ty: Some(ty),
98            body,
99            is_hint: false,
100            implicit_count,
101        })
102    } else {
103        // No type annotation: name := term
104        let name = before_assign.to_string();
105
106        if name.is_empty() {
107            return Err(ParseError::Missing("definition name".to_string()));
108        }
109
110        let body = TermParser::parse(body_str)?;
111
112        Ok(Command::Definition {
113            name,
114            ty: None,
115            body,
116            is_hint: false,
117            implicit_count: 0,
118        })
119    }
120}
121
122/// Parse: term
123fn parse_check(input: &str) -> Result<Command, ParseError> {
124    let term = TermParser::parse(input)?;
125    Ok(Command::Check(term))
126}
127
128/// Parse: term
129fn parse_eval(input: &str) -> Result<Command, ParseError> {
130    let term = TermParser::parse(input)?;
131    Ok(Command::Eval(term))
132}
133
134/// Parse: Name (params) := C1 : T1 | C2 : T2
135///
136/// Supports polymorphic inductives like:
137/// `Inductive List (A : Type) := Nil : List A | Cons : A -> List A -> List A.`
138fn parse_inductive(input: &str) -> Result<Command, ParseError> {
139    // Find the := delimiter
140    let assign_pos = input.find(":=").ok_or(ParseError::Missing(":=".to_string()))?;
141
142    let header = input[..assign_pos].trim();
143    let ctors_str = input[assign_pos + 2..].trim();
144
145    // Parse header to separate name from parameters
146    let (name, params) = parse_inductive_header(header)?;
147
148    if name.is_empty() {
149        return Err(ParseError::Missing("inductive name".to_string()));
150    }
151
152    // Parse constructors separated by |
153    let mut constructors = Vec::new();
154    for ctor_part in ctors_str.split('|') {
155        let ctor_part = ctor_part.trim();
156        if ctor_part.is_empty() {
157            continue;
158        }
159
160        // Each constructor is: Name : Type
161        let colon_pos = ctor_part
162            .find(':')
163            .ok_or(ParseError::Missing("constructor type annotation".to_string()))?;
164
165        let ctor_name = ctor_part[..colon_pos].trim().to_string();
166        let ctor_type_str = ctor_part[colon_pos + 1..].trim();
167
168        if ctor_name.is_empty() {
169            return Err(ParseError::Missing("constructor name".to_string()));
170        }
171
172        let ctor_type = TermParser::parse(ctor_type_str)?;
173        constructors.push((ctor_name, ctor_type));
174    }
175
176    if constructors.is_empty() {
177        return Err(ParseError::Missing("constructors".to_string()));
178    }
179
180    // Default to Type 0 for the sort
181    let sort = Term::Sort(Universe::Type(0));
182
183    Ok(Command::Inductive {
184        name,
185        params,
186        sort,
187        constructors,
188    })
189}
190
191/// Parse the inductive header to extract name and type parameters.
192///
193/// Examples:
194/// - `List` -> ("List", [])
195/// - `List (A : Type)` -> ("List", [("A", Type)])
196/// - `Either (A : Type) (B : Type)` -> ("Either", [("A", Type), ("B", Type)])
197fn parse_inductive_header(header: &str) -> Result<(String, Vec<(String, Term)>), ParseError> {
198    let header = header.trim();
199
200    // If no '(' found, it's a simple name with no params
201    if !header.contains('(') {
202        return Ok((header.to_string(), vec![]));
203    }
204
205    // Find the first '(' to separate name from params
206    let paren_pos = header.find('(').unwrap();
207    let name = header[..paren_pos].trim().to_string();
208    let params_str = header[paren_pos..].trim();
209
210    // Parse all parameter bindings: (A : Type) (B : Type) ...
211    let params = parse_param_bindings(params_str)?;
212
213    Ok((name, params))
214}
215
216/// Parse a sequence of parameter bindings: (A : Type) (B : Type)
217///
218/// Each binding is of the form (name : type).
219fn parse_param_bindings(input: &str) -> Result<Vec<(String, Term)>, ParseError> {
220    let mut params = Vec::new();
221    let mut remaining = input.trim();
222
223    while !remaining.is_empty() {
224        // Skip whitespace
225        remaining = remaining.trim();
226        if remaining.is_empty() {
227            break;
228        }
229
230        // Expect '('
231        if !remaining.starts_with('(') {
232            return Err(ParseError::Missing("opening '(' for parameter".to_string()));
233        }
234
235        // Find matching ')'
236        let close_pos = find_matching_paren(remaining)?;
237        let binding = &remaining[1..close_pos]; // Contents inside parens
238
239        // Parse name : type
240        let colon_pos = binding
241            .find(':')
242            .ok_or(ParseError::Missing("':' in parameter binding".to_string()))?;
243
244        let param_name = binding[..colon_pos].trim().to_string();
245        let param_type_str = binding[colon_pos + 1..].trim();
246
247        if param_name.is_empty() {
248            return Err(ParseError::Missing("parameter name".to_string()));
249        }
250
251        let param_type = TermParser::parse(param_type_str)?;
252        params.push((param_name, param_type));
253
254        // Move past this binding
255        remaining = remaining[close_pos + 1..].trim();
256    }
257
258    Ok(params)
259}
260
261/// Find the position of the ')' that matches the opening '(' at position 0.
262fn find_matching_paren(input: &str) -> Result<usize, ParseError> {
263    let mut depth = 0;
264    for (i, c) in input.chars().enumerate() {
265        match c {
266            '(' => depth += 1,
267            ')' => {
268                depth -= 1;
269                if depth == 0 {
270                    return Ok(i);
271                }
272            }
273            _ => {}
274        }
275    }
276    Err(ParseError::Missing("closing ')' for parameter".to_string()))
277}
278
279#[cfg(test)]
280mod tests {
281    use super::*;
282
283    #[test]
284    fn test_parse_definition_with_type() {
285        let cmd = parse_command("Definition one : Nat := Succ Zero.").unwrap();
286        if let Command::Definition { name, ty, body, .. } = cmd {
287            assert_eq!(name, "one");
288            assert!(ty.is_some());
289            assert!(matches!(body, Term::App(..)));
290        } else {
291            panic!("Expected Definition");
292        }
293    }
294
295    #[test]
296    fn test_parse_definition_without_type() {
297        let cmd = parse_command("Definition two := Succ (Succ Zero).").unwrap();
298        if let Command::Definition { name, ty, .. } = cmd {
299            assert_eq!(name, "two");
300            assert!(ty.is_none());
301        } else {
302            panic!("Expected Definition");
303        }
304    }
305
306    #[test]
307    fn test_parse_check() {
308        let cmd = parse_command("Check Zero.").unwrap();
309        assert!(matches!(cmd, Command::Check(_)));
310    }
311
312    #[test]
313    fn test_parse_eval() {
314        let cmd = parse_command("Eval (Succ Zero).").unwrap();
315        assert!(matches!(cmd, Command::Eval(_)));
316    }
317
318    #[test]
319    fn test_parse_inductive() {
320        let cmd = parse_command("Inductive Bool := True : Bool | False : Bool.").unwrap();
321        if let Command::Inductive {
322            name, constructors, ..
323        } = cmd
324        {
325            assert_eq!(name, "Bool");
326            assert_eq!(constructors.len(), 2);
327            assert_eq!(constructors[0].0, "True");
328            assert_eq!(constructors[1].0, "False");
329        } else {
330            panic!("Expected Inductive");
331        }
332    }
333}
logicaffeine_kernel/interface/command_parser.rs

logicaffeine_kernel/interface/
command_parser.rs
