//! Parser domain: bridges the zero-copy lexer to the canonical
//! e-graph. This is the piece that finishes Phase I — until now the
//! FFI entry point only interned flat leaf tokens; this walks actual
//! s-expression structure, applies AC-normalization and the depth
//! budget through `EGraph::intern_app`, and resolves quantifier-bound
//! variables to De Bruijn indices via `BinderStack` instead of names.

use crate::ast::{BinderStack, Lexer, TokenKind};
use crate::canon::{CanonId, DepthExceeded, EGraph};

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ParseError {
    UnexpectedEof,
    UnexpectedToken { found: String, at: usize },
    DepthBudgetExceeded,
}

impl From<DepthExceeded> for ParseError {
    fn from(_: DepthExceeded) -> Self {
        ParseError::DepthBudgetExceeded
    }
}

const QUANTIFIERS: &[&str] = &["forall", "exists"];

pub struct Parser<'src> {
    lexer: Lexer<'src>,
    peeked: Option<crate::ast::Token<'src>>,
    binders: BinderStack<'src>,
}

impl<'src> Parser<'src> {
    pub fn new(input: &'src str) -> Self {
        Self { lexer: Lexer::new(input), peeked: None, binders: BinderStack::new() }
    }

    fn peek(&mut self) -> crate::ast::Token<'src> {
        if self.peeked.is_none() {
            self.peeked = Some(self.lexer.next_token());
        }
        self.peeked.unwrap()
    }

    fn advance(&mut self) -> crate::ast::Token<'src> {
        match self.peeked.take() {
            Some(t) => t,
            None => self.lexer.next_token(),
        }
    }

    /// Parses every top-level term in the input, interning each into
    /// `egraph`, and returns their root ids. A malformed or
    /// depth-exceeding formula aborts with `ParseError` — callers
    /// surface this as an `unknown`/`error` verdict rather than
    /// panicking, same treatment as the OOM guard.
    pub fn parse_all(&mut self, egraph: &mut EGraph) -> Result<Vec<CanonId>, ParseError> {
        let mut roots = Vec::new();
        loop {
            if self.peek().kind == TokenKind::Eof {
                break;
            }
            roots.push(self.parse_term(egraph)?);
        }
        Ok(roots)
    }

    fn parse_term(&mut self, egraph: &mut EGraph) -> Result<CanonId, ParseError> {
        let tok = self.advance();
        match tok.kind {
            TokenKind::Eof => Err(ParseError::UnexpectedEof),
            TokenKind::RParen => Err(ParseError::UnexpectedToken { found: ")".into(), at: tok.pos }),
            TokenKind::IntLit | TokenKind::Symbol => {
                // A bare symbol may refer to a De Bruijn-bound variable;
                // resolve it against the active binder scopes first so
                // alpha-equivalent formulas intern identically (Q1 sol.1).
                if let Some(idx) = self.binders.resolve(tok.text) {
                    return Ok(egraph.intern_leaf(&format!("#{idx}")));
                }
                Ok(egraph.intern_leaf(tok.text))
            }
            TokenKind::LParen => self.parse_app(egraph),
        }
    }

    fn parse_app(&mut self, egraph: &mut EGraph) -> Result<CanonId, ParseError> {
        let head = self.advance();
        if head.kind != TokenKind::Symbol {
            return Err(ParseError::UnexpectedToken { found: head.text.into(), at: head.pos });
        }

        let is_quantifier = QUANTIFIERS.contains(&head.text);
        let mut bound_here = 0u32;

        if is_quantifier {
            // Expect a binder list: (forall (x y) body). Each bound
            // name is pushed onto the binder stack so occurrences in
            // `body` resolve to De Bruijn indices rather than names.
            self.expect(TokenKind::LParen)?;
            loop {
                let t = self.peek();
                if t.kind == TokenKind::RParen {
                    self.advance();
                    break;
                }
                if t.kind != TokenKind::Symbol {
                    return Err(ParseError::UnexpectedToken { found: t.text.into(), at: t.pos });
                }
                self.advance();
                self.binders.push(t.text);
                bound_here += 1;
            }
        }

        let mut children = Vec::new();
        loop {
            let t = self.peek();
            match t.kind {
                TokenKind::RParen => {
                    self.advance();
                    break;
                }
                TokenKind::Eof => return Err(ParseError::UnexpectedEof),
                _ => children.push(self.parse_term(egraph)?),
            }
        }

        for _ in 0..bound_here {
            self.binders.pop();
        }

        Ok(egraph.intern_app(head.text, &children)?)
    }

    fn expect(&mut self, kind: TokenKind) -> Result<(), ParseError> {
        let t = self.advance();
        if t.kind == kind {
            Ok(())
        } else {
            Err(ParseError::UnexpectedToken { found: t.text.into(), at: t.pos })
        }
    }
}