File size: 4,952 Bytes
07435c8 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 | //! 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 })
}
}
}
|