oxilean_parse/tactic_parser/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5/// Custom tactic syntax definition
6#[derive(Debug, Clone, PartialEq)]
7pub struct CustomTactic {
8    /// Tactic name
9    pub name: String,
10    /// Parameters
11    pub params: Vec<String>,
12    /// Implementation body
13    pub body: String,
14}
15/// A rewrite rule: a lemma name with an optional reverse flag.
16#[derive(Debug, Clone, PartialEq)]
17pub struct RewriteRule {
18    /// Lemma name
19    pub lemma: String,
20    /// If true, rewrite right-to-left
21    pub reverse: bool,
22}
23/// Arguments to the `simp` tactic.
24#[derive(Debug, Clone, PartialEq)]
25pub struct SimpArgs {
26    /// Whether `only` was specified
27    pub only: bool,
28    /// Lemma names in the simp set
29    pub lemmas: Vec<String>,
30    /// Configuration key-value pairs
31    pub config: Vec<(String, String)>,
32}
33/// A case arm for `cases` / `induction`.
34#[derive(Debug, Clone, PartialEq)]
35pub struct CaseArm {
36    /// Constructor/case name
37    pub name: String,
38    /// Bound variable names
39    pub bindings: Vec<String>,
40    /// Tactic for this arm
41    pub tactic: TacticExpr,
42}
43/// Side for `conv` tactic.
44#[derive(Debug, Clone, PartialEq, Eq)]
45pub enum ConvSide {
46    /// Convert on the left-hand side
47    Lhs,
48    /// Convert on the right-hand side
49    Rhs,
50}
51/// A parsed tactic expression.
52#[derive(Debug, Clone, PartialEq)]
53pub enum TacticExpr {
54    /// Basic tactic by name
55    Basic(String),
56    /// Tactic with arguments
57    WithArgs(String, Vec<String>),
58    /// Sequence of tactics (t1 ; t2)
59    Seq(Box<TacticExpr>, Box<TacticExpr>),
60    /// Alternative tactics (t1 <|> t2)
61    Alt(Box<TacticExpr>, Box<TacticExpr>),
62    /// All goals combinator (t <;> t')
63    AllGoals(Box<TacticExpr>, Box<TacticExpr>),
64    /// Repeat tactic
65    Repeat(Box<TacticExpr>),
66    /// Try tactic (don't fail if it fails)
67    Try(Box<TacticExpr>),
68    /// First successful alternative
69    First(Vec<TacticExpr>),
70    /// Focus on specific goal
71    Focus(usize, Box<TacticExpr>),
72    /// All goals
73    All(Box<TacticExpr>),
74    /// Any goal
75    Any(Box<TacticExpr>),
76    /// Block of tactics: `{ t1; t2; ... }`
77    Block(Vec<TacticExpr>),
78    /// Introduce hypotheses: `intro x y z`
79    Intro(Vec<String>),
80    /// Apply a lemma: `apply lem`
81    Apply(String),
82    /// Provide an exact proof term: `exact e`
83    Exact(String),
84    /// Rewrite: `rewrite [lem1, <-lem2]`
85    Rewrite(Vec<RewriteRule>),
86    /// Simplification: `simp`, `simp only [lem1]`, `simp [*]`
87    Simp(SimpArgs),
88    /// Case analysis: `cases x with | c1 => t1 | c2 => t2`
89    Cases(String, Vec<CaseArm>),
90    /// Induction: `induction x with | c => t`
91    Induction(String, Vec<CaseArm>),
92    /// Local hypothesis: `have h : T := by t`
93    Have(String, Option<String>, Box<TacticExpr>),
94    /// Local definition: `let x := e`
95    Let(String, String),
96    /// Show goal form: `show T`
97    Show(String),
98    /// Suffices: `suffices h : T by t`
99    Suffices(String, Box<TacticExpr>),
100    /// Calculational proof
101    Calc(Vec<CalcStep>),
102    /// Conversion mode: `conv_lhs => t` or `conv_rhs => t`
103    Conv(ConvSide, Box<TacticExpr>),
104    /// omega decision procedure
105    Omega,
106    /// Ring decision procedure
107    Ring,
108    /// Decide (boolean decidability)
109    Decide,
110    /// Normalize numerals
111    NormNum,
112    /// Apply constructor
113    Constructor,
114    /// Choose left disjunct
115    Left,
116    /// Choose right disjunct
117    Right,
118    /// Existential introduction: `exists e`
119    Existsi(String),
120    /// Clear hypotheses
121    Clear(Vec<String>),
122    /// Revert hypotheses
123    Revert(Vec<String>),
124    /// Substitute a variable
125    Subst(String),
126    /// Derive a contradiction
127    Contradiction,
128    /// Switch to proving False
129    Exfalso,
130    /// Proof by contradiction: `by_contra h`
131    ByContra(Option<String>),
132    /// Close by assumption
133    Assumption,
134    /// Close trivially
135    Trivial,
136    /// Reflexivity
137    Rfl,
138    /// Intros (shorthand for intro)
139    Intros(Vec<String>),
140    /// Generalize for induction
141    Generalize(String, String),
142    /// Induction on pattern
143    InductionPat(String, String),
144    /// Obtain hypothesis
145    Obtain(String, Box<TacticExpr>),
146    /// Rcases (recursive cases)
147    Rcases(String, Vec<String>),
148    /// Tauto (propositional solver)
149    Tauto,
150    /// Ac_rfl (associative-commutative reflexivity)
151    AcRfl,
152    /// Custom tactic
153    Custom(CustomTactic),
154    /// Located tactic (for IDE support)
155    Located(Box<TacticExpr>, TacticLocation),
156}
157/// A single step in a `calc` proof.
158#[derive(Debug, Clone, PartialEq)]
159pub struct CalcStep {
160    /// The relation symbol (e.g. "=", "<=", "<")
161    pub relation: String,
162    /// The right-hand-side expression
163    pub rhs: String,
164    /// Justification tactic
165    pub justification: TacticExpr,
166}
167/// Location information for IDE support
168#[derive(Debug, Clone, PartialEq, Eq)]
169pub struct TacticLocation {
170    /// Line number (1-based)
171    pub line: usize,
172    /// Column number (1-based)
173    pub column: usize,
174    /// Tactic name
175    pub name: String,
176}
oxilean_parse/tactic_parser/types.rs

oxilean_parse/tactic_parser/
types.rs
