oxilean_parse/repl_parser/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::ast_impl::*;
6use crate::error_impl::ParseError;
7use crate::lexer::Lexer;
8use crate::parser_impl::Parser;
9
10use super::functions::*;
11
12/// Tally of REPL command types seen during a session.
13#[allow(dead_code)]
14#[derive(Default, Debug, Clone)]
15#[allow(missing_docs)]
16pub struct CommandTally {
17    pub evals: u64,
18    pub type_queries: u64,
19    pub checks: u64,
20    pub loads: u64,
21    #[allow(missing_docs)]
22    pub quits: u64,
23    pub helps: u64,
24    pub other: u64,
25}
26impl CommandTally {
27    /// Create a zero-initialized tally.
28    #[allow(dead_code)]
29    #[allow(missing_docs)]
30    pub fn new() -> Self {
31        Self::default()
32    }
33    /// Record a command.
34    #[allow(dead_code)]
35    #[allow(missing_docs)]
36    pub fn record(&mut self, cmd: &ReplCommand) {
37        match cmd {
38            ReplCommand::Eval(_) => self.evals += 1,
39            ReplCommand::Type(_) => self.type_queries += 1,
40            ReplCommand::Check(_) => self.checks += 1,
41            ReplCommand::Load(_) => self.loads += 1,
42            ReplCommand::Quit => self.quits += 1,
43            ReplCommand::Help => self.helps += 1,
44            _ => self.other += 1,
45        }
46    }
47    /// Total commands.
48    #[allow(dead_code)]
49    #[allow(missing_docs)]
50    pub fn total(&self) -> u64 {
51        self.evals
52            + self.type_queries
53            + self.checks
54            + self.loads
55            + self.quits
56            + self.helps
57            + self.other
58    }
59}
60/// A REPL session history entry.
61#[allow(dead_code)]
62#[allow(missing_docs)]
63#[derive(Debug, Clone)]
64pub struct ReplHistoryEntry {
65    /// The input line
66    pub input: String,
67    /// Whether parsing succeeded
68    pub parse_ok: bool,
69    /// Sequence number
70    pub seq: usize,
71}
72impl ReplHistoryEntry {
73    /// Create a new entry.
74    #[allow(dead_code)]
75    pub fn new(seq: usize, input: &str, parse_ok: bool) -> Self {
76        ReplHistoryEntry {
77            input: input.to_string(),
78            parse_ok,
79            seq,
80        }
81    }
82}
83/// An input splitter that breaks raw REPL input into logical lines,
84/// handling multi-line continuation (`--` comments, `(`, `begin`, etc.).
85#[derive(Clone, Debug, Default)]
86#[allow(missing_docs)]
87pub struct InputSplitter {
88    /// Lines accumulated so far.
89    pub(super) buffer: Vec<String>,
90    /// Current depth of open parentheses / brackets.
91    pub(super) depth: i32,
92}
93impl InputSplitter {
94    /// Create a new splitter.
95    #[allow(missing_docs)]
96    pub fn new() -> Self {
97        Self::default()
98    }
99    /// Push a raw line of input.
100    #[allow(missing_docs)]
101    pub fn push(&mut self, line: &str) {
102        self.buffer.push(line.to_string());
103        for ch in line.chars() {
104            match ch {
105                '(' | '[' | '{' => self.depth += 1,
106                ')' | ']' | '}' => self.depth -= 1,
107                _ => {}
108            }
109        }
110    }
111    /// Check if the buffer is logically complete (balanced brackets).
112    #[allow(missing_docs)]
113    pub fn is_complete(&self) -> bool {
114        self.depth <= 0 && !self.buffer.is_empty()
115    }
116    /// Flush the buffer and reset.
117    #[allow(missing_docs)]
118    pub fn flush(&mut self) -> String {
119        let result = self.buffer.join("\n");
120        self.buffer.clear();
121        self.depth = 0;
122        result
123    }
124    /// Number of lines buffered.
125    #[allow(missing_docs)]
126    pub fn line_count(&self) -> usize {
127        self.buffer.len()
128    }
129    /// Current bracket depth.
130    #[allow(missing_docs)]
131    pub fn depth(&self) -> i32 {
132        self.depth
133    }
134    /// Check if buffer is empty.
135    #[allow(missing_docs)]
136    pub fn is_empty(&self) -> bool {
137        self.buffer.is_empty()
138    }
139}
140/// A key-value option store for REPL session options.
141#[derive(Clone, Debug, Default)]
142#[allow(missing_docs)]
143pub struct OptionStore {
144    values: std::collections::HashMap<String, String>,
145}
146impl OptionStore {
147    /// Create an empty option store.
148    #[allow(missing_docs)]
149    pub fn new() -> Self {
150        Self::default()
151    }
152    /// Set an option by name.
153    #[allow(missing_docs)]
154    pub fn set(&mut self, name: impl Into<String>, value: impl Into<String>) {
155        self.values.insert(name.into(), value.into());
156    }
157    /// Get an option by name.
158    #[allow(missing_docs)]
159    pub fn get(&self, name: &str) -> Option<&str> {
160        self.values.get(name).map(|s| s.as_str())
161    }
162    /// Check if an option is set.
163    #[allow(missing_docs)]
164    pub fn has(&self, name: &str) -> bool {
165        self.values.contains_key(name)
166    }
167    /// Remove an option.
168    #[allow(missing_docs)]
169    pub fn remove(&mut self, name: &str) -> bool {
170        self.values.remove(name).is_some()
171    }
172    /// Number of options set.
173    #[allow(missing_docs)]
174    pub fn len(&self) -> usize {
175        self.values.len()
176    }
177    /// Check if empty.
178    #[allow(missing_docs)]
179    pub fn is_empty(&self) -> bool {
180        self.values.is_empty()
181    }
182    /// Get a bool option, defaulting to `false`.
183    #[allow(missing_docs)]
184    pub fn get_bool(&self, name: &str) -> bool {
185        self.get(name)
186            .map(|v| matches!(v, "true" | "1" | "yes" | "on"))
187            .unwrap_or(false)
188    }
189    /// Get a u64 option, defaulting to `default`.
190    #[allow(missing_docs)]
191    pub fn get_u64(&self, name: &str, default: u64) -> u64 {
192        self.get(name)
193            .and_then(|v| v.parse().ok())
194            .unwrap_or(default)
195    }
196    /// Get all option names.
197    #[allow(missing_docs)]
198    pub fn keys(&self) -> Vec<&str> {
199        self.values.keys().map(|s| s.as_str()).collect()
200    }
201}
202/// A REPL command alias: maps a short name to a full command string.
203#[allow(dead_code)]
204#[derive(Debug, Clone)]
205#[allow(missing_docs)]
206pub struct CommandAlias {
207    pub from: String,
208    pub to: String,
209}
210impl CommandAlias {
211    /// Create a new alias.
212    #[allow(dead_code)]
213    #[allow(missing_docs)]
214    pub fn new(from: &str, to: &str) -> Self {
215        Self {
216            from: from.to_string(),
217            to: to.to_string(),
218        }
219    }
220}
221/// A REPL mode that controls what kinds of input are accepted.
222#[derive(Debug, Clone, Copy, PartialEq, Eq)]
223#[allow(missing_docs)]
224pub enum ReplMode {
225    /// Standard mode: accept expressions and declarations.
226    Normal,
227    /// Tactic mode: accept tactic-block lines.
228    Tactic,
229    /// Search mode: accept search queries only.
230    Search,
231}
232impl ReplMode {
233    /// The mode name for display.
234    #[allow(missing_docs)]
235    pub fn name(&self) -> &'static str {
236        match self {
237            ReplMode::Normal => "normal",
238            ReplMode::Tactic => "tactic",
239            ReplMode::Search => "search",
240        }
241    }
242    /// Parse a mode name.
243    #[allow(missing_docs)]
244    pub fn from_name(s: &str) -> Option<Self> {
245        match s {
246            "normal" => Some(ReplMode::Normal),
247            "tactic" => Some(ReplMode::Tactic),
248            "search" => Some(ReplMode::Search),
249            _ => None,
250        }
251    }
252}
253/// REPL command type.
254#[derive(Debug, Clone, PartialEq)]
255#[allow(clippy::large_enum_variant)]
256#[allow(missing_docs)]
257pub enum ReplCommand {
258    /// Evaluate an expression
259    Eval(Located<SurfaceExpr>),
260    /// Show type of an expression
261    Type(Located<SurfaceExpr>),
262    /// Check a declaration
263    Check(Located<Decl>),
264    /// Load a file
265    Load(String),
266    /// Show environment
267    ShowEnv,
268    /// Clear environment
269    Clear,
270    /// Show help
271    Help,
272    /// Quit REPL
273    Quit,
274}
275/// A no-op REPL event listener.
276#[allow(dead_code)]
277#[allow(missing_docs)]
278pub struct NoopListener;
279/// A pipeline of input filters.
280#[allow(dead_code)]
281#[allow(missing_docs)]
282pub struct FilterPipeline {
283    filters: Vec<Box<dyn InputFilter>>,
284}
285impl FilterPipeline {
286    /// Create an empty pipeline.
287    #[allow(dead_code)]
288    #[allow(missing_docs)]
289    pub fn new() -> Self {
290        Self {
291            filters: Vec::new(),
292        }
293    }
294    /// Add a filter to the pipeline.
295    #[allow(dead_code)]
296    #[allow(missing_docs)]
297    pub fn add<F: InputFilter + 'static>(&mut self, f: F) {
298        self.filters.push(Box::new(f));
299    }
300    /// Apply all filters in sequence.
301    #[allow(dead_code)]
302    #[allow(missing_docs)]
303    pub fn apply(&self, input: &str) -> String {
304        let mut result = input.to_string();
305        for f in &self.filters {
306            result = f.filter(&result);
307        }
308        result
309    }
310    /// Number of filters.
311    #[allow(dead_code)]
312    #[allow(missing_docs)]
313    pub fn len(&self) -> usize {
314        self.filters.len()
315    }
316    /// Whether the pipeline is empty.
317    #[allow(dead_code)]
318    #[allow(missing_docs)]
319    pub fn is_empty(&self) -> bool {
320        self.filters.is_empty()
321    }
322}
323/// Statistics about REPL session.
324#[derive(Debug, Clone, Default)]
325#[allow(missing_docs)]
326pub struct ReplStats {
327    /// Number of commands evaluated.
328    pub commands_run: u64,
329    /// Number of successful elaborations.
330    pub successes: u64,
331    /// Number of errors encountered.
332    #[allow(missing_docs)]
333    pub errors: u64,
334    /// Total characters typed.
335    pub chars_typed: u64,
336}
337impl ReplStats {
338    /// Create zeroed stats.
339    #[allow(missing_docs)]
340    pub fn new() -> Self {
341        Self::default()
342    }
343    /// Record a successful command.
344    #[allow(missing_docs)]
345    pub fn record_success(&mut self) {
346        self.commands_run += 1;
347        self.successes += 1;
348    }
349    /// Record an error.
350    #[allow(missing_docs)]
351    pub fn record_error(&mut self) {
352        self.commands_run += 1;
353        self.errors += 1;
354    }
355    /// Record characters typed.
356    #[allow(missing_docs)]
357    pub fn record_chars(&mut self, n: u64) {
358        self.chars_typed += n;
359    }
360    /// Return success rate (0.0 to 1.0).
361    #[allow(missing_docs)]
362    pub fn success_rate(&self) -> f64 {
363        if self.commands_run == 0 {
364            1.0
365        } else {
366            self.successes as f64 / self.commands_run as f64
367        }
368    }
369}
370/// REPL output formatter.
371#[allow(dead_code)]
372#[allow(missing_docs)]
373pub struct ReplFormatter {
374    use_color: bool,
375    max_width: usize,
376}
377impl ReplFormatter {
378    /// Create a formatter.
379    #[allow(dead_code)]
380    #[allow(missing_docs)]
381    pub fn new(use_color: bool, max_width: usize) -> Self {
382        Self {
383            use_color,
384            max_width,
385        }
386    }
387    /// Format a success message.
388    #[allow(dead_code)]
389    #[allow(missing_docs)]
390    pub fn success(&self, msg: &str) -> String {
391        if self.use_color {
392            format!("\x1b[1;32m✓\x1b[0m {}", msg)
393        } else {
394            format!("OK: {}", msg)
395        }
396    }
397    /// Format an error message.
398    #[allow(dead_code)]
399    #[allow(missing_docs)]
400    pub fn error(&self, msg: &str) -> String {
401        if self.use_color {
402            format!("\x1b[1;31m✗\x1b[0m {}", msg)
403        } else {
404            format!("Error: {}", msg)
405        }
406    }
407    /// Format an info message.
408    #[allow(dead_code)]
409    #[allow(missing_docs)]
410    pub fn info(&self, msg: &str) -> String {
411        if self.use_color {
412            format!("\x1b[1;34mℹ\x1b[0m {}", msg)
413        } else {
414            format!("Info: {}", msg)
415        }
416    }
417    /// Truncate a string to the max width.
418    #[allow(dead_code)]
419    #[allow(missing_docs)]
420    pub fn truncate(&self, s: &str) -> String {
421        if s.len() <= self.max_width {
422            s.to_string()
423        } else {
424            format!("{}..", &s[..self.max_width.saturating_sub(2)])
425        }
426    }
427    /// Format a list of items.
428    #[allow(dead_code)]
429    #[allow(missing_docs)]
430    pub fn list(&self, items: &[String]) -> String {
431        items
432            .iter()
433            .enumerate()
434            .map(|(i, s)| format!("  {}: {}", i + 1, self.truncate(s)))
435            .collect::<Vec<_>>()
436            .join("\n")
437    }
438}
439/// REPL parser for parsing REPL-specific commands.
440#[allow(missing_docs)]
441pub struct ReplParser {
442    /// Input line
443    input: String,
444}
445impl ReplParser {
446    /// Create a new REPL parser.
447    #[allow(missing_docs)]
448    pub fn new(input: String) -> Self {
449        Self { input }
450    }
451    /// Parse a REPL command.
452    #[allow(missing_docs)]
453    pub fn parse(&self) -> Result<ReplCommand, ParseError> {
454        let trimmed = self.input.trim();
455        if let Some(cmd) = trimmed.strip_prefix(':') {
456            return self.parse_meta_command(cmd);
457        }
458        self.parse_input()
459    }
460    /// Parse meta-commands (:quit, :help, etc.)
461    fn parse_meta_command(&self, cmd: &str) -> Result<ReplCommand, ParseError> {
462        let parts: Vec<&str> = cmd.split_whitespace().collect();
463        if parts.is_empty() {
464            return Err(ParseError::unexpected(
465                vec!["command".to_string()],
466                crate::tokens::TokenKind::Eof,
467                crate::span_util::dummy_span(),
468            ));
469        }
470        match parts[0] {
471            "quit" | "q" | "exit" => Ok(ReplCommand::Quit),
472            "help" | "h" | "?" => Ok(ReplCommand::Help),
473            "env" | "show" => Ok(ReplCommand::ShowEnv),
474            "clear" | "reset" => Ok(ReplCommand::Clear),
475            "type" | "t" => {
476                if parts.len() < 2 {
477                    return Err(ParseError::unexpected(
478                        vec!["expression".to_string()],
479                        crate::tokens::TokenKind::Eof,
480                        crate::span_util::dummy_span(),
481                    ));
482                }
483                let expr_str = parts[1..].join(" ");
484                let expr = self.parse_expr_from_str(&expr_str)?;
485                Ok(ReplCommand::Type(expr))
486            }
487            "load" | "l" => {
488                if parts.len() < 2 {
489                    return Err(ParseError::unexpected(
490                        vec!["filename".to_string()],
491                        crate::tokens::TokenKind::Eof,
492                        crate::span_util::dummy_span(),
493                    ));
494                }
495                Ok(ReplCommand::Load(parts[1].to_string()))
496            }
497            "check" | "c" => {
498                if parts.len() < 2 {
499                    return Err(ParseError::unexpected(
500                        vec!["declaration".to_string()],
501                        crate::tokens::TokenKind::Eof,
502                        crate::span_util::dummy_span(),
503                    ));
504                }
505                let decl_str = parts[1..].join(" ");
506                let decl = self.parse_decl_from_str(&decl_str)?;
507                Ok(ReplCommand::Check(decl))
508            }
509            _ => Err(ParseError::unexpected(
510                vec!["known command".to_string()],
511                crate::tokens::TokenKind::Eof,
512                crate::span_util::dummy_span(),
513            )),
514        }
515    }
516    /// Parse input as expression or declaration.
517    fn parse_input(&self) -> Result<ReplCommand, ParseError> {
518        if let Ok(decl) = self.parse_decl_from_str(&self.input) {
519            return Ok(ReplCommand::Check(decl));
520        }
521        let expr = self.parse_expr_from_str(&self.input)?;
522        Ok(ReplCommand::Eval(expr))
523    }
524    /// Parse an expression from a string.
525    fn parse_expr_from_str(&self, s: &str) -> Result<Located<SurfaceExpr>, ParseError> {
526        let mut lexer = Lexer::new(s);
527        let tokens = lexer.tokenize();
528        let mut parser = Parser::new(tokens);
529        parser.parse_expr()
530    }
531    /// Parse a declaration from a string.
532    fn parse_decl_from_str(&self, s: &str) -> Result<Located<Decl>, ParseError> {
533        let mut lexer = Lexer::new(s);
534        let tokens = lexer.tokenize();
535        let mut parser = Parser::new(tokens);
536        parser.parse_decl()
537    }
538}
539/// A REPL session history.
540#[allow(dead_code)]
541#[allow(missing_docs)]
542pub struct ReplHistory {
543    /// All entries in order
544    pub entries: Vec<ReplHistoryEntry>,
545}
546impl ReplHistory {
547    /// Create a new empty history.
548    #[allow(dead_code)]
549    pub fn new() -> Self {
550        ReplHistory {
551            entries: Vec::new(),
552        }
553    }
554    /// Add an entry.
555    #[allow(dead_code)]
556    pub fn push(&mut self, input: &str, parse_ok: bool) {
557        let seq = self.entries.len();
558        self.entries
559            .push(ReplHistoryEntry::new(seq, input, parse_ok));
560    }
561    /// Returns the number of entries.
562    #[allow(dead_code)]
563    pub fn len(&self) -> usize {
564        self.entries.len()
565    }
566    /// Returns true if empty.
567    #[allow(dead_code)]
568    pub fn is_empty(&self) -> bool {
569        self.entries.is_empty()
570    }
571}
572/// Command history for the REPL.
573#[derive(Debug, Clone, Default)]
574#[allow(missing_docs)]
575pub struct CommandHistory {
576    entries: Vec<String>,
577    max_entries: usize,
578    position: usize,
579}
580impl CommandHistory {
581    /// Create a new empty history with capacity.
582    #[allow(missing_docs)]
583    pub fn new(max_entries: usize) -> Self {
584        Self {
585            entries: Vec::new(),
586            max_entries,
587            position: 0,
588        }
589    }
590    /// Push a new entry to history.
591    ///
592    /// If the entry is identical to the last one, it is not duplicated.
593    #[allow(missing_docs)]
594    pub fn push(&mut self, entry: String) {
595        if entry.trim().is_empty() {
596            return;
597        }
598        if self.entries.last().map(|s| s.as_str()) == Some(&entry) {
599            return;
600        }
601        if self.entries.len() >= self.max_entries {
602            self.entries.remove(0);
603        }
604        self.entries.push(entry);
605        self.position = self.entries.len();
606    }
607    /// Navigate backward in history (older entries).
608    #[allow(missing_docs)]
609    pub fn prev(&mut self) -> Option<&str> {
610        if self.entries.is_empty() || self.position == 0 {
611            return None;
612        }
613        self.position -= 1;
614        self.entries.get(self.position).map(|s| s.as_str())
615    }
616    /// Navigate forward in history (newer entries).
617    #[allow(clippy::should_implement_trait)]
618    #[allow(missing_docs)]
619    pub fn next(&mut self) -> Option<&str> {
620        if self.position >= self.entries.len() {
621            return None;
622        }
623        self.position += 1;
624        self.entries.get(self.position).map(|s| s.as_str())
625    }
626    /// Get all history entries.
627    #[allow(missing_docs)]
628    pub fn entries(&self) -> &[String] {
629        &self.entries
630    }
631    /// Clear the history.
632    #[allow(missing_docs)]
633    pub fn clear(&mut self) {
634        self.entries.clear();
635        self.position = 0;
636    }
637    /// Return the number of entries.
638    #[allow(missing_docs)]
639    pub fn len(&self) -> usize {
640        self.entries.len()
641    }
642    /// Return true if history is empty.
643    #[allow(missing_docs)]
644    pub fn is_empty(&self) -> bool {
645        self.entries.is_empty()
646    }
647    /// Search history for entries containing the given query.
648    #[allow(missing_docs)]
649    pub fn search(&self, query: &str) -> Vec<&str> {
650        self.entries
651            .iter()
652            .filter(|e| e.contains(query))
653            .map(|s| s.as_str())
654            .collect()
655    }
656}
657/// Extended REPL command including option management and history.
658#[derive(Debug, Clone, PartialEq)]
659#[allow(clippy::large_enum_variant)]
660#[allow(missing_docs)]
661pub enum ExtendedReplCommand {
662    /// Set an option: :set name value
663    SetOption(String, String),
664    /// Get an option: :get name
665    GetOption(String),
666    /// Show command history: :history
667    History,
668    /// Undo last declaration: :undo
669    Undo,
670    /// Print a term's normal form: :reduce expr
671    Reduce(Located<SurfaceExpr>),
672    /// Show statistics: :stats
673    Stats,
674    /// Search for a name: :search pattern
675    Search(String),
676    /// Print declaration info: :print name
677    Print(String),
678}
679/// The kind of a completion item.
680#[allow(dead_code)]
681#[derive(Debug, Clone, PartialEq, Eq)]
682#[allow(missing_docs)]
683pub enum CompletionKind {
684    Command,
685    Keyword,
686    Identifier,
687    Tactic,
688}
689/// Options for REPL behavior.
690#[derive(Debug, Clone)]
691#[allow(missing_docs)]
692pub struct ReplOptions {
693    /// Whether to show timing information.
694    pub show_timing: bool,
695    /// Whether to print types alongside values.
696    pub print_types: bool,
697    /// Maximum number of history entries.
698    #[allow(missing_docs)]
699    pub max_history: usize,
700    /// Whether to enable color output.
701    pub color: bool,
702    /// Whether to enable verbose mode.
703    pub verbose: bool,
704}
705impl ReplOptions {
706    /// Create new options with defaults.
707    #[allow(missing_docs)]
708    pub fn new() -> Self {
709        Self::default()
710    }
711    /// Set an option by name and value string.
712    ///
713    /// Returns `Ok(())` on success or an error string if the option
714    /// name or value is unrecognized.
715    #[allow(missing_docs)]
716    pub fn set(&mut self, name: &str, value: &str) -> Result<(), String> {
717        match name {
718            "timing" => {
719                self.show_timing = parse_bool(value)?;
720                Ok(())
721            }
722            "types" => {
723                self.print_types = parse_bool(value)?;
724                Ok(())
725            }
726            "color" => {
727                self.color = parse_bool(value)?;
728                Ok(())
729            }
730            "verbose" => {
731                self.verbose = parse_bool(value)?;
732                Ok(())
733            }
734            "history" => {
735                self.max_history = value
736                    .parse::<usize>()
737                    .map_err(|_| format!("Expected number, got '{}'", value))?;
738                Ok(())
739            }
740            _ => Err(format!("Unknown option '{}'", name)),
741        }
742    }
743    /// Get an option value as a string.
744    #[allow(missing_docs)]
745    pub fn get(&self, name: &str) -> Option<String> {
746        match name {
747            "timing" => Some(self.show_timing.to_string()),
748            "types" => Some(self.print_types.to_string()),
749            "color" => Some(self.color.to_string()),
750            "verbose" => Some(self.verbose.to_string()),
751            "history" => Some(self.max_history.to_string()),
752            _ => None,
753        }
754    }
755    /// List all known option names.
756    #[allow(missing_docs)]
757    pub fn known_options() -> &'static [&'static str] {
758        &["timing", "types", "color", "verbose", "history"]
759    }
760}
761/// State of multi-line input accumulation.
762#[derive(Debug, Clone, Default)]
763#[allow(missing_docs)]
764pub struct MultilineState {
765    /// Accumulated lines so far.
766    pub(super) lines: Vec<String>,
767    /// Brace/paren depth to track continuation.
768    pub(super) depth: i32,
769}
770impl MultilineState {
771    /// Create a new empty multi-line state.
772    #[allow(missing_docs)]
773    pub fn new() -> Self {
774        Self::default()
775    }
776    /// Add a line to the accumulation.
777    #[allow(missing_docs)]
778    pub fn push_line(&mut self, line: &str) {
779        for ch in line.chars() {
780            match ch {
781                '(' | '[' | '{' => self.depth += 1,
782                ')' | ']' | '}' => self.depth -= 1,
783                _ => {}
784            }
785        }
786        self.lines.push(line.to_string());
787    }
788    /// Check if the accumulated input is complete.
789    #[allow(missing_docs)]
790    pub fn is_complete(&self) -> bool {
791        self.depth <= 0 && !self.lines.is_empty()
792    }
793    /// Get the accumulated input as a single string.
794    #[allow(missing_docs)]
795    pub fn get_input(&self) -> String {
796        self.lines.join("\n")
797    }
798    /// Reset the state.
799    #[allow(missing_docs)]
800    pub fn reset(&mut self) {
801        self.lines.clear();
802        self.depth = 0;
803    }
804    /// Return the current depth (positive means inside a group).
805    #[allow(missing_docs)]
806    pub fn depth(&self) -> i32 {
807        self.depth
808    }
809    /// Return the number of accumulated lines.
810    #[allow(missing_docs)]
811    pub fn line_count(&self) -> usize {
812        self.lines.len()
813    }
814}
815/// A REPL session that tracks history, options, and statistics.
816#[derive(Debug)]
817#[allow(missing_docs)]
818pub struct ReplSession {
819    /// Command history.
820    pub history: CommandHistory,
821    /// REPL options.
822    pub options: ReplOptions,
823    /// Session statistics.
824    #[allow(missing_docs)]
825    pub stats: ReplStats,
826    /// The underlying parser used by this session.
827    _phantom: std::marker::PhantomData<()>,
828}
829impl ReplSession {
830    /// Create a new REPL session with default settings.
831    #[allow(missing_docs)]
832    pub fn new() -> Self {
833        let options = ReplOptions::default();
834        let max_history = options.max_history;
835        Self {
836            history: CommandHistory::new(max_history),
837            options,
838            stats: ReplStats::new(),
839            _phantom: std::marker::PhantomData,
840        }
841    }
842    /// Process a raw input line.
843    ///
844    /// Returns the parsed command or an error.
845    #[allow(missing_docs)]
846    pub fn process(&mut self, input: &str) -> Result<ReplCommand, String> {
847        let input = input.trim().to_string();
848        if input.is_empty() {
849            return Err("Empty input".to_string());
850        }
851        self.history.push(input.clone());
852        self.stats.record_chars(input.len() as u64);
853        let parser = ReplParser::new(input);
854        parser.parse().map_err(|e| e.to_string())
855    }
856    /// Get the help text.
857    #[allow(missing_docs)]
858    pub fn help(&self) -> &'static str {
859        help_text()
860    }
861}
862/// A REPL completion item.
863#[allow(dead_code)]
864#[derive(Debug, Clone, PartialEq, Eq)]
865#[allow(missing_docs)]
866pub struct CompletionItem {
867    pub text: String,
868    pub description: String,
869    pub kind: CompletionKind,
870}
871impl CompletionItem {
872    /// Create a new completion item.
873    #[allow(dead_code)]
874    #[allow(missing_docs)]
875    pub fn new(text: &str, description: &str, kind: CompletionKind) -> Self {
876        Self {
877            text: text.to_string(),
878            description: description.to_string(),
879            kind,
880        }
881    }
882}
883/// A REPL session option that can be toggled.
884#[derive(Debug, Clone, PartialEq, Eq, Hash)]
885#[allow(missing_docs)]
886pub enum ReplOption {
887    /// Print timing information after each command.
888    Timing,
889    /// Show the elaborated term after each check.
890    ShowElaborated,
891    /// Enable verbose mode.
892    Verbose,
893    /// Pretty-print expressions.
894    PrettyPrint,
895    /// Maximum output lines.
896    MaxLines,
897}
898impl ReplOption {
899    /// Parse a `ReplOption` from its name string.
900    #[allow(missing_docs)]
901    pub fn from_name(s: &str) -> Option<Self> {
902        match s {
903            "timing" => Some(ReplOption::Timing),
904            "show_elaborated" | "showElaborated" => Some(ReplOption::ShowElaborated),
905            "verbose" => Some(ReplOption::Verbose),
906            "pretty_print" | "prettyPrint" => Some(ReplOption::PrettyPrint),
907            "max_lines" | "maxLines" => Some(ReplOption::MaxLines),
908            _ => None,
909        }
910    }
911    /// Get the canonical name of this option.
912    #[allow(missing_docs)]
913    pub fn name(&self) -> &'static str {
914        match self {
915            ReplOption::Timing => "timing",
916            ReplOption::ShowElaborated => "show_elaborated",
917            ReplOption::Verbose => "verbose",
918            ReplOption::PrettyPrint => "pretty_print",
919            ReplOption::MaxLines => "max_lines",
920        }
921    }
922}
923/// Configuration for ReplParser.
924#[allow(dead_code)]
925#[derive(Debug, Clone, Default)]
926#[allow(missing_docs)]
927pub struct ReplParserConfig {
928    /// Whether to allow multi-line input.
929    pub allow_multiline: bool,
930    /// Whether to normalize whitespace before parsing.
931    pub normalize_whitespace: bool,
932    /// Whether to strip comments before parsing.
933    #[allow(missing_docs)]
934    pub strip_comments: bool,
935}
936impl ReplParserConfig {
937    /// Create a default configuration.
938    #[allow(dead_code)]
939    #[allow(missing_docs)]
940    pub fn new() -> Self {
941        Self::default()
942    }
943    /// Enable multi-line input.
944    #[allow(dead_code)]
945    #[allow(missing_docs)]
946    pub fn with_multiline(mut self) -> Self {
947        self.allow_multiline = true;
948        self
949    }
950}
951/// A REPL event log that records all events.
952#[allow(dead_code)]
953#[derive(Default, Debug)]
954#[allow(missing_docs)]
955pub struct EventLog {
956    pub(super) events: Vec<ReplEvent>,
957}
958impl EventLog {
959    /// Create an empty event log.
960    #[allow(dead_code)]
961    #[allow(missing_docs)]
962    pub fn new() -> Self {
963        Self::default()
964    }
965    /// Get all recorded events.
966    #[allow(dead_code)]
967    #[allow(missing_docs)]
968    pub fn events(&self) -> &[ReplEvent] {
969        &self.events
970    }
971    /// Clear the log.
972    #[allow(dead_code)]
973    #[allow(missing_docs)]
974    pub fn clear(&mut self) {
975        self.events.clear();
976    }
977    /// Number of events.
978    #[allow(dead_code)]
979    #[allow(missing_docs)]
980    pub fn len(&self) -> usize {
981        self.events.len()
982    }
983    /// Whether the log is empty.
984    #[allow(dead_code)]
985    #[allow(missing_docs)]
986    pub fn is_empty(&self) -> bool {
987        self.events.is_empty()
988    }
989}
990/// An input filter that lowercases command keywords.
991#[allow(dead_code)]
992#[allow(missing_docs)]
993pub struct LowercaseCommandFilter;
994/// A REPL input classifier.
995#[allow(dead_code)]
996#[allow(missing_docs)]
997#[derive(Debug, Clone, PartialEq, Eq)]
998pub enum ReplInputKind {
999    /// A term to evaluate
1000    Term,
1001    /// A definition
1002    Definition,
1003    /// A tactic proof
1004    Tactic,
1005    /// A command (e.g. #check, #eval)
1006    Command,
1007    /// An incomplete input
1008    Incomplete,
1009}
1010/// A REPL event emitted by the session.
1011#[derive(Debug, Clone, PartialEq)]
1012#[allow(missing_docs)]
1013pub enum ReplEvent {
1014    /// A command was successfully parsed.
1015    Parsed(String),
1016    /// A parse error occurred.
1017    Error(String),
1018    /// The session was reset.
1019    Reset,
1020    /// An option was changed.
1021    OptionChanged(String, String),
1022    /// The REPL is exiting.
1023    Exit,
1024}
1025/// A REPL completer that provides completions for a given prefix.
1026#[allow(dead_code)]
1027#[allow(missing_docs)]
1028pub struct ReplCompleter {
1029    items: Vec<CompletionItem>,
1030}
1031impl ReplCompleter {
1032    /// Create a completer with built-in items.
1033    #[allow(dead_code)]
1034    #[allow(missing_docs)]
1035    pub fn new() -> Self {
1036        let mut items = Vec::new();
1037        for cmd in [
1038            ":quit", ":help", ":env", ":clear", ":type", ":load", ":check", ":set", ":history",
1039        ] {
1040            items.push(CompletionItem::new(
1041                cmd,
1042                "REPL command",
1043                CompletionKind::Command,
1044            ));
1045        }
1046        for kw in [
1047            "theorem",
1048            "def",
1049            "axiom",
1050            "inductive",
1051            "fun",
1052            "let",
1053            "match",
1054            "forall",
1055        ] {
1056            items.push(CompletionItem::new(kw, "keyword", CompletionKind::Keyword));
1057        }
1058        Self { items }
1059    }
1060    /// Complete a prefix.
1061    #[allow(dead_code)]
1062    #[allow(missing_docs)]
1063    pub fn complete(&self, prefix: &str) -> Vec<&CompletionItem> {
1064        self.items
1065            .iter()
1066            .filter(|item| item.text.starts_with(prefix))
1067            .collect()
1068    }
1069    /// Add a custom completion item.
1070    #[allow(dead_code)]
1071    #[allow(missing_docs)]
1072    pub fn add(&mut self, item: CompletionItem) {
1073        self.items.push(item);
1074    }
1075    /// Number of registered items.
1076    #[allow(dead_code)]
1077    #[allow(missing_docs)]
1078    pub fn len(&self) -> usize {
1079        self.items.len()
1080    }
1081    /// Whether there are any items.
1082    #[allow(dead_code)]
1083    #[allow(missing_docs)]
1084    pub fn is_empty(&self) -> bool {
1085        self.items.is_empty()
1086    }
1087}
1088/// A REPL alias registry.
1089#[allow(dead_code)]
1090#[derive(Default, Debug)]
1091#[allow(missing_docs)]
1092pub struct AliasRegistry {
1093    aliases: Vec<CommandAlias>,
1094}
1095impl AliasRegistry {
1096    /// Create an empty registry.
1097    #[allow(dead_code)]
1098    #[allow(missing_docs)]
1099    pub fn new() -> Self {
1100        Self::default()
1101    }
1102    /// Register an alias.
1103    #[allow(dead_code)]
1104    #[allow(missing_docs)]
1105    pub fn register(&mut self, from: &str, to: &str) {
1106        self.aliases.push(CommandAlias::new(from, to));
1107    }
1108    /// Expand an alias. Returns the expanded string or the original.
1109    #[allow(dead_code)]
1110    #[allow(missing_docs)]
1111    pub fn expand<'a>(&'a self, input: &'a str) -> &'a str {
1112        for alias in &self.aliases {
1113            if input.trim_start() == alias.from {
1114                return &alias.to;
1115            }
1116        }
1117        input
1118    }
1119    /// Number of aliases.
1120    #[allow(dead_code)]
1121    #[allow(missing_docs)]
1122    pub fn len(&self) -> usize {
1123        self.aliases.len()
1124    }
1125    /// Whether the registry is empty.
1126    #[allow(dead_code)]
1127    #[allow(missing_docs)]
1128    pub fn is_empty(&self) -> bool {
1129        self.aliases.is_empty()
1130    }
1131    /// List all alias names.
1132    #[allow(dead_code)]
1133    #[allow(missing_docs)]
1134    pub fn names(&self) -> Vec<&str> {
1135        self.aliases.iter().map(|a| a.from.as_str()).collect()
1136    }
1137}
1138/// An input filter that strips trailing semicolons.
1139#[allow(dead_code)]
1140#[allow(missing_docs)]
1141pub struct StripSemicolonFilter;
1142/// Configurable REPL parser.
1143#[allow(dead_code)]
1144#[allow(missing_docs)]
1145pub struct ConfigurableReplParser {
1146    config: ReplParserConfig,
1147}
1148impl ConfigurableReplParser {
1149    /// Create a new configurable REPL parser.
1150    #[allow(dead_code)]
1151    #[allow(missing_docs)]
1152    pub fn new(config: ReplParserConfig) -> Self {
1153        Self { config }
1154    }
1155    /// Preprocess input according to config.
1156    #[allow(dead_code)]
1157    #[allow(missing_docs)]
1158    pub fn preprocess(&self, input: &str) -> String {
1159        let mut s = input.to_string();
1160        if self.config.normalize_whitespace {
1161            s = s.split_whitespace().collect::<Vec<_>>().join(" ");
1162        }
1163        if self.config.strip_comments {
1164            s = s
1165                .lines()
1166                .map(|line| {
1167                    if let Some(idx) = line.find("--") {
1168                        &line[..idx]
1169                    } else {
1170                        line
1171                    }
1172                })
1173                .collect::<Vec<_>>()
1174                .join("\n");
1175        }
1176        s
1177    }
1178    /// Parse the preprocessed input.
1179    #[allow(dead_code)]
1180    #[allow(missing_docs)]
1181    pub fn parse(&self, input: &str) -> Result<ReplCommand, String> {
1182        let processed = self.preprocess(input);
1183        let p = ReplParser::new(processed);
1184        p.parse().map_err(|e| e.to_string())
1185    }
1186}
oxilean_parse/repl_parser/types.rs

oxilean_parse/repl_parser/
types.rs
