oxilean_parse/tactic_parser/
tacticparser_parsing.rs

1//! # TacticParser - parsing Methods
2//!
3//! This module contains method implementations for `TacticParser`.
4//!
5//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
6
7use crate::{ParseError, ParseErrorKind, Span, Token, TokenKind};
8
9use super::types::{CalcStep, CaseArm, ConvSide, RewriteRule, TacticExpr};
10
11use super::tacticparser_type::TacticParser;
12
13impl<'a> TacticParser<'a> {
14    /// Create a new tactic parser.
15    pub fn new(tokens: &'a [Token]) -> Self {
16        Self { tokens, pos: 0 }
17    }
18    /// Parse `by <tactic>` or `by { t1; t2; ... }`.
19    pub fn parse_by_block(&mut self) -> Result<TacticExpr, ParseError> {
20        if !self.check_keyword("by") {
21            return Err(ParseError::new(
22                ParseErrorKind::InvalidSyntax("expected 'by'".to_string()),
23                self.current_span(),
24            ));
25        }
26        self.advance();
27        if self.check_op("{") {
28            self.parse_brace_block()
29        } else {
30            self.parse_seq()
31        }
32    }
33    pub(super) fn parse_seq(&mut self) -> Result<TacticExpr, ParseError> {
34        let mut left = self.parse_all_goals()?;
35        while self.check_op(";") {
36            self.advance();
37            let right = self.parse_all_goals()?;
38            left = TacticExpr::Seq(Box::new(left), Box::new(right));
39        }
40        Ok(left)
41    }
42    #[allow(dead_code)]
43    pub(super) fn parse_all_goals(&mut self) -> Result<TacticExpr, ParseError> {
44        let mut left = self.parse_alt()?;
45        while self.check_op("<;>") {
46            self.advance();
47            let right = self.parse_alt()?;
48            left = TacticExpr::AllGoals(Box::new(left), Box::new(right));
49        }
50        Ok(left)
51    }
52    pub(super) fn parse_alt(&mut self) -> Result<TacticExpr, ParseError> {
53        let mut left = self.parse_primary()?;
54        while self.check_op("<|>") {
55            self.advance();
56            let right = self.parse_primary()?;
57            left = TacticExpr::Alt(Box::new(left), Box::new(right));
58        }
59        Ok(left)
60    }
61    pub(super) fn parse_primary(&mut self) -> Result<TacticExpr, ParseError> {
62        if self.check_op("{") {
63            return self.parse_brace_block();
64        }
65        if self.check_keyword("repeat") {
66            self.advance();
67            let inner = self.parse_primary()?;
68            return Ok(TacticExpr::Repeat(Box::new(inner)));
69        }
70        if self.check_keyword("try") {
71            self.advance();
72            let inner = self.parse_primary()?;
73            return Ok(TacticExpr::Try(Box::new(inner)));
74        }
75        if self.check_keyword("focus") {
76            self.advance();
77            let n = self.expect_nat()?;
78            let inner = self.parse_primary()?;
79            return Ok(TacticExpr::Focus(n, Box::new(inner)));
80        }
81        if self.check_keyword("all") {
82            self.advance();
83            let inner = self.parse_primary()?;
84            return Ok(TacticExpr::All(Box::new(inner)));
85        }
86        if self.check_keyword("any") {
87            self.advance();
88            let inner = self.parse_primary()?;
89            return Ok(TacticExpr::Any(Box::new(inner)));
90        }
91        if self.check_keyword("intro") {
92            return self.parse_intro();
93        }
94        if self.check_keyword("intros") {
95            return self.parse_intros();
96        }
97        if self.check_keyword("apply") {
98            return self.parse_apply();
99        }
100        if self.check_keyword("exact") {
101            return self.parse_exact();
102        }
103        if self.check_keyword("generalize") {
104            return self.parse_generalize();
105        }
106        if self.check_keyword("obtain") {
107            return self.parse_obtain();
108        }
109        if self.check_keyword("rcases") {
110            return self.parse_rcases();
111        }
112        if self.check_keyword("first") {
113            return self.parse_first();
114        }
115        if self.check_keyword("tauto") {
116            return self.parse_tauto();
117        }
118        if self.check_keyword("ac_rfl") {
119            return self.parse_ac_rfl();
120        }
121        if self.check_keyword("rewrite") || self.check_keyword("rw") {
122            return self.parse_rewrite();
123        }
124        if self.check_keyword("simp") {
125            return self.parse_simp();
126        }
127        if self.check_keyword("cases") {
128            return self.parse_cases();
129        }
130        if self.check_keyword("induction") {
131            return self.parse_induction();
132        }
133        if self.check_keyword("have") {
134            return self.parse_have();
135        }
136        if self.check_keyword("let") {
137            return self.parse_let();
138        }
139        if self.check_keyword("show") {
140            return self.parse_show();
141        }
142        if self.check_keyword("suffices") {
143            return self.parse_suffices();
144        }
145        if self.check_keyword("calc") {
146            return self.parse_calc();
147        }
148        if self.check_keyword("conv_lhs") {
149            self.advance();
150            self.expect_op("=>")?;
151            let inner = self.parse_primary()?;
152            return Ok(TacticExpr::Conv(ConvSide::Lhs, Box::new(inner)));
153        }
154        if self.check_keyword("conv_rhs") {
155            self.advance();
156            self.expect_op("=>")?;
157            let inner = self.parse_primary()?;
158            return Ok(TacticExpr::Conv(ConvSide::Rhs, Box::new(inner)));
159        }
160        if self.check_keyword("conv") {
161            return self.parse_conv();
162        }
163        if self.check_keyword("omega") {
164            self.advance();
165            return Ok(TacticExpr::Omega);
166        }
167        if self.check_keyword("ring") {
168            self.advance();
169            return Ok(TacticExpr::Ring);
170        }
171        if self.check_keyword("decide") {
172            self.advance();
173            return Ok(TacticExpr::Decide);
174        }
175        if self.check_keyword("norm_num") {
176            self.advance();
177            return Ok(TacticExpr::NormNum);
178        }
179        if self.check_keyword("constructor") {
180            self.advance();
181            return Ok(TacticExpr::Constructor);
182        }
183        if self.check_keyword("left") {
184            self.advance();
185            return Ok(TacticExpr::Left);
186        }
187        if self.check_keyword("right") {
188            self.advance();
189            return Ok(TacticExpr::Right);
190        }
191        if self.check_keyword("existsi") || self.check_keyword("use") {
192            return self.parse_existsi();
193        }
194        if self.check_keyword("clear") {
195            return self.parse_clear();
196        }
197        if self.check_keyword("revert") {
198            return self.parse_revert();
199        }
200        if self.check_keyword("subst") {
201            return self.parse_subst();
202        }
203        if self.check_keyword("contradiction") {
204            self.advance();
205            return Ok(TacticExpr::Contradiction);
206        }
207        if self.check_keyword("exfalso") {
208            self.advance();
209            return Ok(TacticExpr::Exfalso);
210        }
211        if self.check_keyword("by_contra") {
212            return self.parse_by_contra();
213        }
214        if self.check_keyword("assumption") {
215            self.advance();
216            return Ok(TacticExpr::Assumption);
217        }
218        if self.check_keyword("trivial") {
219            self.advance();
220            return Ok(TacticExpr::Trivial);
221        }
222        if self.check_keyword("rfl") {
223            self.advance();
224            return Ok(TacticExpr::Rfl);
225        }
226        let name = self.expect_ident()?;
227        if self.check_op("(") {
228            self.advance();
229            let mut args = Vec::new();
230            while !self.check_op(")") {
231                args.push(self.expect_ident()?);
232                if !self.check_op(",") {
233                    break;
234                }
235                self.advance();
236            }
237            self.expect_op(")")?;
238            Ok(TacticExpr::WithArgs(name, args))
239        } else {
240            Ok(TacticExpr::Basic(name))
241        }
242    }
243    /// Parse `intro x y z ...`
244    pub(super) fn parse_intro(&mut self) -> Result<TacticExpr, ParseError> {
245        self.advance();
246        let mut names = Vec::new();
247        while let Some(token) = self.current() {
248            match &token.kind {
249                TokenKind::Ident(s) if !self.is_tactic_terminator(s) => {
250                    names.push(s.clone());
251                    self.advance();
252                }
253                TokenKind::Underscore => {
254                    names.push("_".to_string());
255                    self.advance();
256                }
257                _ => break,
258            }
259        }
260        Ok(TacticExpr::Intro(names))
261    }
262    /// Parse the rewrite argument list: `[lem1, <-lem2, ...]`
263    pub(super) fn parse_rewrite_args(&mut self) -> Result<Vec<RewriteRule>, ParseError> {
264        self.expect_op("[")?;
265        let mut rules = Vec::new();
266        if self.check_op("]") {
267            self.advance();
268            return Ok(rules);
269        }
270        loop {
271            let reverse = if self.check_op("<-") {
272                self.advance();
273                true
274            } else {
275                false
276            };
277            let lemma = self.expect_ident()?;
278            rules.push(RewriteRule { lemma, reverse });
279            if !self.check_op(",") {
280                break;
281            }
282            self.advance();
283        }
284        self.expect_op("]")?;
285        Ok(rules)
286    }
287    /// Parse optional `[lem1, lem2, *]` for simp.
288    pub(super) fn parse_simp_lemma_list(&mut self) -> Result<Vec<String>, ParseError> {
289        if !self.check_op("[") {
290            return Ok(Vec::new());
291        }
292        self.advance();
293        let mut lemmas = Vec::new();
294        if self.check_op("]") {
295            self.advance();
296            return Ok(lemmas);
297        }
298        loop {
299            if self.check_op("*") {
300                lemmas.push("*".to_string());
301                self.advance();
302            } else if self.check_op("-") {
303                self.advance();
304                let name = self.expect_ident()?;
305                lemmas.push(format!("-{}", name));
306            } else {
307                let name = self.expect_ident()?;
308                lemmas.push(name);
309            }
310            if !self.check_op(",") {
311                break;
312            }
313            self.advance();
314        }
315        self.expect_op("]")?;
316        Ok(lemmas)
317    }
318    /// Parse optional `{ key := val, ... }` for simp config.
319    pub(super) fn parse_simp_config(&mut self) -> Result<Vec<(String, String)>, ParseError> {
320        if !self.check_op("{") {
321            return Ok(Vec::new());
322        }
323        self.advance();
324        let mut config = Vec::new();
325        if self.check_op("}") {
326            self.advance();
327            return Ok(config);
328        }
329        loop {
330            let key = self.expect_ident()?;
331            self.expect_op(":=")?;
332            let val = self.expect_ident()?;
333            config.push((key, val));
334            if !self.check_op(",") {
335                break;
336            }
337            self.advance();
338        }
339        self.expect_op("}")?;
340        Ok(config)
341    }
342    /// Parse `cases x with | c1 a b => t1 | c2 => t2`
343    pub(super) fn parse_cases(&mut self) -> Result<TacticExpr, ParseError> {
344        self.advance();
345        let target = self.expect_ident()?;
346        let arms = if self.check_keyword("with") {
347            self.advance();
348            self.parse_case_arms()?
349        } else {
350            Vec::new()
351        };
352        Ok(TacticExpr::Cases(target, arms))
353    }
354    /// Parse `induction x with | c a b => t1 | c2 => t2`
355    pub(super) fn parse_induction(&mut self) -> Result<TacticExpr, ParseError> {
356        self.advance();
357        let target = self.expect_ident()?;
358        let arms = if self.check_keyword("with") {
359            self.advance();
360            self.parse_case_arms()?
361        } else {
362            Vec::new()
363        };
364        Ok(TacticExpr::Induction(target, arms))
365    }
366    /// Parse `| name pat1 pat2 => tactic` arms.
367    pub(super) fn parse_case_arms(&mut self) -> Result<Vec<CaseArm>, ParseError> {
368        let mut arms = Vec::new();
369        while self.check_op("|") {
370            self.advance();
371            let name = self.expect_ident()?;
372            let mut bindings = Vec::new();
373            while !self.check_op("=>") && !self.at_end() {
374                if let Some(token) = self.current() {
375                    if let TokenKind::Ident(s) = &token.kind {
376                        bindings.push(s.clone());
377                        self.advance();
378                    } else if token.kind == TokenKind::Underscore {
379                        bindings.push("_".to_string());
380                        self.advance();
381                    } else {
382                        break;
383                    }
384                } else {
385                    break;
386                }
387            }
388            self.expect_op("=>")?;
389            let tactic = self.parse_seq()?;
390            arms.push(CaseArm {
391                name,
392                bindings,
393                tactic,
394            });
395        }
396        Ok(arms)
397    }
398    /// Parse `have h : T := by tactic` or `have h := by tactic`.
399    pub(super) fn parse_have(&mut self) -> Result<TacticExpr, ParseError> {
400        self.advance();
401        let name = self.expect_ident()?;
402        let ty = if self.check_op(":") {
403            self.advance();
404            let t = self.expect_ident()?;
405            Some(t)
406        } else {
407            None
408        };
409        if self.check_op(":=") {
410            self.advance();
411        }
412        let body = if self.check_keyword("by") {
413            self.parse_by_block()?
414        } else {
415            self.parse_primary()?
416        };
417        Ok(TacticExpr::Have(name, ty, Box::new(body)))
418    }
419    /// Parse `suffices h : T by tactic`.
420    pub(super) fn parse_suffices(&mut self) -> Result<TacticExpr, ParseError> {
421        self.advance();
422        let name = self.expect_ident()?;
423        if self.check_op(":") {
424            self.advance();
425            let _ty = self.expect_ident()?;
426        }
427        let body = if self.check_keyword("by") {
428            self.parse_by_block()?
429        } else {
430            self.parse_primary()?
431        };
432        Ok(TacticExpr::Suffices(name, Box::new(body)))
433    }
434    /// Parse calc steps: `_ rel rhs := by justification`.
435    pub(super) fn parse_calc_steps(&mut self) -> Result<Vec<CalcStep>, ParseError> {
436        let mut steps = Vec::new();
437        while self.check_op("_") || self.check_keyword("_") {
438            self.advance();
439            let relation = self.expect_ident()?;
440            let rhs = self.expect_ident()?;
441            self.expect_op(":=")?;
442            let justification = if self.check_keyword("by") {
443                self.parse_by_block()?
444            } else {
445                self.parse_primary()?
446            };
447            steps.push(CalcStep {
448                relation,
449                rhs,
450                justification,
451            });
452        }
453        Ok(steps)
454    }
455    /// Parse `conv => tactic` (with optional side specification).
456    pub(super) fn parse_conv(&mut self) -> Result<TacticExpr, ParseError> {
457        self.advance();
458        let side = if self.check_keyword("lhs") {
459            self.advance();
460            ConvSide::Lhs
461        } else if self.check_keyword("rhs") {
462            self.advance();
463            ConvSide::Rhs
464        } else {
465            ConvSide::Lhs
466        };
467        self.expect_op("=>")?;
468        let inner = self.parse_primary()?;
469        Ok(TacticExpr::Conv(side, Box::new(inner)))
470    }
471    /// Parse `first | t1 | t2 | t3`.
472    #[allow(dead_code)]
473    pub(super) fn parse_first(&mut self) -> Result<TacticExpr, ParseError> {
474        self.advance();
475        let mut tactics = Vec::new();
476        while self.check_op("|") {
477            self.advance();
478            tactics.push(self.parse_primary()?);
479        }
480        if tactics.is_empty() {
481            tactics.push(self.parse_primary()?);
482        }
483        Ok(TacticExpr::First(tactics))
484    }
485    /// Parse `intros` (multiple intro)
486    #[allow(dead_code)]
487    pub(super) fn parse_intros(&mut self) -> Result<TacticExpr, ParseError> {
488        self.advance();
489        let mut names = Vec::new();
490        while let Some(token) = self.current() {
491            match &token.kind {
492                TokenKind::Ident(s) if !self.is_tactic_terminator(s) => {
493                    names.push(s.clone());
494                    self.advance();
495                }
496                TokenKind::Underscore => {
497                    names.push("_".to_string());
498                    self.advance();
499                }
500                _ => break,
501            }
502        }
503        Ok(TacticExpr::Intros(names))
504    }
505    /// Parse `obtain h, ... => tactic`.
506    #[allow(dead_code)]
507    pub(super) fn parse_obtain(&mut self) -> Result<TacticExpr, ParseError> {
508        self.advance();
509        let name = self.expect_ident()?;
510        let body = if self.check_op(",") || self.check_op("=>") {
511            self.advance();
512            self.parse_primary()?
513        } else {
514            self.parse_primary()?
515        };
516        Ok(TacticExpr::Obtain(name, Box::new(body)))
517    }
518    /// Parse `rcases h with | c1 => ... | c2 => ...`.
519    #[allow(dead_code)]
520    pub(super) fn parse_rcases(&mut self) -> Result<TacticExpr, ParseError> {
521        self.advance();
522        let target = self.expect_ident()?;
523        let mut patterns = Vec::new();
524        if self.check_keyword("with") {
525            self.advance();
526            while self.check_op("|") {
527                self.advance();
528                let pat = self.expect_ident()?;
529                patterns.push(pat);
530                if self.check_op("=>") {
531                    self.advance();
532                    let _ = self.parse_primary();
533                }
534            }
535        }
536        Ok(TacticExpr::Rcases(target, patterns))
537    }
538    /// Parse a `{ t1; t2; ... }` block.
539    pub(super) fn parse_brace_block(&mut self) -> Result<TacticExpr, ParseError> {
540        self.expect_op("{")?;
541        let mut tactics = Vec::new();
542        while !self.check_op("}") && !self.at_end() {
543            let t = self.parse_seq()?;
544            tactics.push(t);
545            let _ = self.consume_op(";");
546        }
547        self.expect_op("}")?;
548        Ok(TacticExpr::Block(tactics))
549    }
550    /// Parse a list of identifiers (until we hit a non-ident).
551    pub(super) fn parse_ident_list(&mut self) -> Result<Vec<String>, ParseError> {
552        let mut names = Vec::new();
553        while let Some(token) = self.current() {
554            if let TokenKind::Ident(s) = &token.kind {
555                if self.is_tactic_terminator(s) {
556                    break;
557                }
558                names.push(s.clone());
559                self.advance();
560            } else {
561                break;
562            }
563        }
564        Ok(names)
565    }
566    pub(super) fn expect_ident(&mut self) -> Result<String, ParseError> {
567        if let Some(token) = self.current() {
568            if let TokenKind::Ident(s) = &token.kind {
569                let result = s.clone();
570                self.advance();
571                return Ok(result);
572            }
573        }
574        Err(ParseError::new(
575            ParseErrorKind::InvalidSyntax("expected identifier".to_string()),
576            self.current_span(),
577        ))
578    }
579    pub(super) fn expect_nat(&mut self) -> Result<usize, ParseError> {
580        if let Some(token) = self.current() {
581            if let TokenKind::Nat(n) = &token.kind {
582                let result = *n as usize;
583                self.advance();
584                return Ok(result);
585            }
586        }
587        Err(ParseError::new(
588            ParseErrorKind::InvalidSyntax("expected number".to_string()),
589            self.current_span(),
590        ))
591    }
592    pub(super) fn expect_op(&mut self, op: &str) -> Result<(), ParseError> {
593        if self.check_op(op) {
594            self.advance();
595            Ok(())
596        } else {
597            Err(ParseError::new(
598                ParseErrorKind::InvalidSyntax(format!("expected '{}'", op)),
599                self.current_span(),
600            ))
601        }
602    }
603    pub(super) fn current_span(&self) -> Span {
604        if let Some(token) = self.current() {
605            token.span.clone()
606        } else {
607            Span::new(0, 0, 0, 0)
608        }
609    }
610}
oxilean_parse/tactic_parser/tacticparser_parsing.rs

oxilean_parse/tactic_parser/
tacticparser_parsing.rs
