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 = TermParser::parse(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        })
101    } else {
102        // No type annotation: name := term
103        let name = before_assign.to_string();
104
105        if name.is_empty() {
106            return Err(ParseError::Missing("definition name".to_string()));
107        }
108
109        let body = TermParser::parse(body_str)?;
110
111        Ok(Command::Definition {
112            name,
113            ty: None,
114            body,
115            is_hint: false,
116        })
117    }
118}
119
120/// Parse: term
121fn parse_check(input: &str) -> Result<Command, ParseError> {
122    let term = TermParser::parse(input)?;
123    Ok(Command::Check(term))
124}
125
126/// Parse: term
127fn parse_eval(input: &str) -> Result<Command, ParseError> {
128    let term = TermParser::parse(input)?;
129    Ok(Command::Eval(term))
130}
131
132/// Parse: Name (params) := C1 : T1 | C2 : T2
133///
134/// Supports polymorphic inductives like:
135/// `Inductive List (A : Type) := Nil : List A | Cons : A -> List A -> List A.`
136fn parse_inductive(input: &str) -> Result<Command, ParseError> {
137    // Find the := delimiter
138    let assign_pos = input.find(":=").ok_or(ParseError::Missing(":=".to_string()))?;
139
140    let header = input[..assign_pos].trim();
141    let ctors_str = input[assign_pos + 2..].trim();
142
143    // Parse header to separate name from parameters
144    let (name, params) = parse_inductive_header(header)?;
145
146    if name.is_empty() {
147        return Err(ParseError::Missing("inductive name".to_string()));
148    }
149
150    // Parse constructors separated by |
151    let mut constructors = Vec::new();
152    for ctor_part in ctors_str.split('|') {
153        let ctor_part = ctor_part.trim();
154        if ctor_part.is_empty() {
155            continue;
156        }
157
158        // Each constructor is: Name : Type
159        let colon_pos = ctor_part
160            .find(':')
161            .ok_or(ParseError::Missing("constructor type annotation".to_string()))?;
162
163        let ctor_name = ctor_part[..colon_pos].trim().to_string();
164        let ctor_type_str = ctor_part[colon_pos + 1..].trim();
165
166        if ctor_name.is_empty() {
167            return Err(ParseError::Missing("constructor name".to_string()));
168        }
169
170        let ctor_type = TermParser::parse(ctor_type_str)?;
171        constructors.push((ctor_name, ctor_type));
172    }
173
174    if constructors.is_empty() {
175        return Err(ParseError::Missing("constructors".to_string()));
176    }
177
178    // Default to Type 0 for the sort
179    let sort = Term::Sort(Universe::Type(0));
180
181    Ok(Command::Inductive {
182        name,
183        params,
184        sort,
185        constructors,
186    })
187}
188
189/// Parse the inductive header to extract name and type parameters.
190///
191/// Examples:
192/// - `List` -> ("List", [])
193/// - `List (A : Type)` -> ("List", [("A", Type)])
194/// - `Either (A : Type) (B : Type)` -> ("Either", [("A", Type), ("B", Type)])
195fn parse_inductive_header(header: &str) -> Result<(String, Vec<(String, Term)>), ParseError> {
196    let header = header.trim();
197
198    // If no '(' found, it's a simple name with no params
199    if !header.contains('(') {
200        return Ok((header.to_string(), vec![]));
201    }
202
203    // Find the first '(' to separate name from params
204    let paren_pos = header.find('(').unwrap();
205    let name = header[..paren_pos].trim().to_string();
206    let params_str = header[paren_pos..].trim();
207
208    // Parse all parameter bindings: (A : Type) (B : Type) ...
209    let params = parse_param_bindings(params_str)?;
210
211    Ok((name, params))
212}
213
214/// Parse a sequence of parameter bindings: (A : Type) (B : Type)
215///
216/// Each binding is of the form (name : type).
217fn parse_param_bindings(input: &str) -> Result<Vec<(String, Term)>, ParseError> {
218    let mut params = Vec::new();
219    let mut remaining = input.trim();
220
221    while !remaining.is_empty() {
222        // Skip whitespace
223        remaining = remaining.trim();
224        if remaining.is_empty() {
225            break;
226        }
227
228        // Expect '('
229        if !remaining.starts_with('(') {
230            return Err(ParseError::Missing("opening '(' for parameter".to_string()));
231        }
232
233        // Find matching ')'
234        let close_pos = find_matching_paren(remaining)?;
235        let binding = &remaining[1..close_pos]; // Contents inside parens
236
237        // Parse name : type
238        let colon_pos = binding
239            .find(':')
240            .ok_or(ParseError::Missing("':' in parameter binding".to_string()))?;
241
242        let param_name = binding[..colon_pos].trim().to_string();
243        let param_type_str = binding[colon_pos + 1..].trim();
244
245        if param_name.is_empty() {
246            return Err(ParseError::Missing("parameter name".to_string()));
247        }
248
249        let param_type = TermParser::parse(param_type_str)?;
250        params.push((param_name, param_type));
251
252        // Move past this binding
253        remaining = remaining[close_pos + 1..].trim();
254    }
255
256    Ok(params)
257}
258
259/// Find the position of the ')' that matches the opening '(' at position 0.
260fn find_matching_paren(input: &str) -> Result<usize, ParseError> {
261    let mut depth = 0;
262    for (i, c) in input.chars().enumerate() {
263        match c {
264            '(' => depth += 1,
265            ')' => {
266                depth -= 1;
267                if depth == 0 {
268                    return Ok(i);
269                }
270            }
271            _ => {}
272        }
273    }
274    Err(ParseError::Missing("closing ')' for parameter".to_string()))
275}
276
277#[cfg(test)]
278mod tests {
279    use super::*;
280
281    #[test]
282    fn test_parse_definition_with_type() {
283        let cmd = parse_command("Definition one : Nat := Succ Zero.").unwrap();
284        if let Command::Definition { name, ty, body, .. } = cmd {
285            assert_eq!(name, "one");
286            assert!(ty.is_some());
287            assert!(matches!(body, Term::App(..)));
288        } else {
289            panic!("Expected Definition");
290        }
291    }
292
293    #[test]
294    fn test_parse_definition_without_type() {
295        let cmd = parse_command("Definition two := Succ (Succ Zero).").unwrap();
296        if let Command::Definition { name, ty, .. } = cmd {
297            assert_eq!(name, "two");
298            assert!(ty.is_none());
299        } else {
300            panic!("Expected Definition");
301        }
302    }
303
304    #[test]
305    fn test_parse_check() {
306        let cmd = parse_command("Check Zero.").unwrap();
307        assert!(matches!(cmd, Command::Check(_)));
308    }
309
310    #[test]
311    fn test_parse_eval() {
312        let cmd = parse_command("Eval (Succ Zero).").unwrap();
313        assert!(matches!(cmd, Command::Eval(_)));
314    }
315
316    #[test]
317    fn test_parse_inductive() {
318        let cmd = parse_command("Inductive Bool := True : Bool | False : Bool.").unwrap();
319        if let Command::Inductive {
320            name, constructors, ..
321        } = cmd
322        {
323            assert_eq!(name, "Bool");
324            assert_eq!(constructors.len(), 2);
325            assert_eq!(constructors[0].0, "True");
326            assert_eq!(constructors[1].0, "False");
327        } else {
328            panic!("Expected Inductive");
329        }
330    }
331}
logicaffeine_kernel/interface/command_parser.rs

logicaffeine_kernel/interface/
command_parser.rs
