1use crate::ast::{Arg, Expr, Modal, Term};
4use crate::{Diagnostics, Span, Tok, Token};
5
6pub struct Parser<'a> {
9 toks: &'a [Token],
10 pos: usize,
11}
12
13impl<'a> Parser<'a> {
14 pub fn new(toks: &'a [Token]) -> Self {
20 debug_assert!(!toks.is_empty(), "token stream must end with Eof");
21 Parser { toks, pos: 0 }
22 }
23 pub fn peek(&self) -> &Tok {
25 &self.toks[self.pos.min(self.toks.len() - 1)].tok
26 }
27 pub fn peek2(&self) -> &Tok {
29 &self.toks[(self.pos + 1).min(self.toks.len() - 1)].tok
30 }
31 pub fn peek_at(&self, n: usize) -> &Tok {
34 &self.toks[(self.pos + n).min(self.toks.len() - 1)].tok
35 }
36 pub fn span(&self) -> Span {
38 self.toks[self.pos.min(self.toks.len() - 1)].span
39 }
40 pub fn prev_span(&self) -> Span {
47 self.toks[self.pos.saturating_sub(1).min(self.toks.len() - 1)].span
48 }
49 pub fn bump(&mut self) -> Token {
51 let t = self.toks[self.pos.min(self.toks.len() - 1)].clone();
52 if self.pos < self.toks.len() - 1 {
53 self.pos += 1;
54 }
55 t
56 }
57 pub fn eat(&mut self, want: &Tok) -> bool {
59 if self.peek() == want {
60 self.bump();
61 true
62 } else {
63 false
64 }
65 }
66 pub fn expect(&mut self, want: &Tok, what: &str, diags: &mut Diagnostics) -> bool {
68 if self.eat(want) {
69 true
70 } else {
71 diags.push(self.span(), format!("expected `{what}`"));
72 false
73 }
74 }
75 pub fn at_eof(&self) -> bool {
77 matches!(self.peek(), Tok::Eof)
78 }
79
80 pub fn parse_expr(&mut self, diags: &mut Diagnostics) -> Expr {
82 self.parse_implies(diags)
83 }
84
85 fn parse_implies(&mut self, diags: &mut Diagnostics) -> Expr {
86 let lhs = self.parse_or(diags);
87 if self.eat(&Tok::Arrow) {
88 let rhs = self.parse_implies(diags); let sp = lhs.span().merge(rhs.span());
90 return Expr::Implies(Box::new(lhs), Box::new(rhs), sp);
91 }
92 lhs
93 }
94
95 fn parse_or(&mut self, diags: &mut Diagnostics) -> Expr {
96 let mut lhs = self.parse_and(diags);
97 while self.eat(&Tok::Bar) {
98 let rhs = self.parse_and(diags);
99 let sp = lhs.span().merge(rhs.span());
100 lhs = Expr::Or(Box::new(lhs), Box::new(rhs), sp);
101 }
102 lhs
103 }
104
105 fn parse_and(&mut self, diags: &mut Diagnostics) -> Expr {
106 let mut lhs = self.parse_unary(diags);
107 while self.eat(&Tok::Amp) {
108 let rhs = self.parse_unary(diags);
109 let sp = lhs.span().merge(rhs.span());
110 lhs = Expr::And(Box::new(lhs), Box::new(rhs), sp);
111 }
112 lhs
113 }
114
115 fn parse_unary(&mut self, diags: &mut Diagnostics) -> Expr {
116 if matches!(self.peek(), Tok::Bang) {
117 let sp = self.span();
118 self.bump();
119 let inner = self.parse_unary(diags);
120 let full = sp.merge(inner.span());
121 return Expr::Not(Box::new(inner), full);
122 }
123 self.parse_primary(diags)
124 }
125
126 fn modal_at(&self) -> Option<(Modal, usize)> {
129 match (self.peek(), self.peek2()) {
130 (Tok::Box, _) => Some((Modal::Safe, 1)),
131 (Tok::Question, _) => Some((Modal::Ignorant, 1)),
132 (Tok::Undecided, _) => Some((Modal::Undecided, 1)),
133 (Tok::Upper(k), Tok::Prime) => match k.as_str() {
134 "K" => Some((Modal::KnowsDual, 2)),
135 "B" => Some((Modal::BelievesDual, 2)),
136 "S" => Some((Modal::SafeDual, 2)),
137 _ => None,
138 },
139 (Tok::Upper(k), _) => match k.as_str() {
140 "K" => Some((Modal::Knows, 1)),
141 "B" => Some((Modal::Believes, 1)),
142 "C" => Some((Modal::Common, 1)),
143 "Kw" => Some((Modal::KnowsWhether, 1)),
144 "Bw" => Some((Modal::BelievesWhether, 1)),
145 _ => None,
146 },
147 _ => None,
148 }
149 }
150
151 fn parse_primary(&mut self, diags: &mut Diagnostics) -> Expr {
152 let start = self.span();
153
154 if let Some((op, width)) = self.modal_at() {
155 for _ in 0..width {
156 self.bump();
157 }
158 let cond =
164 if self.eat(&Tok::Caret) { Some(Box::new(self.parse_unary(diags))) } else { None };
165 self.expect(&Tok::LBracket, "[", diags);
166 let agents = if self.eat(&Tok::Star) {
167 None
168 } else {
169 let mut names = Vec::new();
170 loop {
171 match self.peek().clone() {
172 Tok::Lower(n) => {
173 self.bump();
174 names.push(Arg::Obj(n));
175 }
176 Tok::Var(n) => {
181 self.bump();
182 names.push(Arg::Var(n));
183 }
184 _ => {
185 diags.push(self.span(), "expected an agent name or `?variable`");
186 break;
187 }
188 }
189 if !self.eat(&Tok::Comma) {
190 break;
191 }
192 }
193 Some(names)
194 };
195 self.expect(&Tok::RBracket, "]", diags);
196 let body = self.parse_unary(diags);
197 let span = start.merge(body.span());
198 return Expr::Modality { op, agents, cond, body: Box::new(body), span };
199 }
200
201 if self.eat(&Tok::LParen) {
202 let e = self.parse_expr(diags);
203 self.expect(&Tok::RParen, ")", diags);
204 return e;
205 }
206
207 match self.peek().clone() {
208 Tok::Hole => {
209 self.bump();
210 Expr::Hole(start)
211 }
212 Tok::Lower(name) if name == "true" => {
213 self.bump();
214 Expr::True(start)
215 }
216 Tok::Lower(name) if name == "false" => {
217 self.bump();
218 Expr::False(start)
219 }
220 Tok::Lower(name) => {
221 self.bump();
222 let mut args = Vec::new();
223 let mut end = start;
224 if self.eat(&Tok::LParen) {
225 if !matches!(self.peek(), Tok::RParen) {
226 loop {
227 match self.peek().clone() {
228 Tok::Lower(o) => {
229 self.bump();
230 args.push(Arg::Obj(o));
231 }
232 Tok::Var(v) => {
233 self.bump();
234 args.push(Arg::Var(v));
235 }
236 Tok::Upper(t) => {
241 self.bump();
242 args.push(Arg::Ty(t));
243 }
244 _ => {
245 diags.push(
246 self.span(),
247 "expected an object, `?variable`, or type name",
248 );
249 break;
250 }
251 }
252 if !self.eat(&Tok::Comma) {
253 break;
254 }
255 }
256 }
257 end = self.span();
258 self.expect(&Tok::RParen, ")", diags);
259 }
260 Expr::Atom(Term { pred: name, args, span: start.merge(end) })
261 }
262 _ => {
263 diags.push(start, "expected a formula");
264 self.bump();
265 Expr::False(start)
266 }
267 }
268 }
269}
270
271#[cfg(test)]
272mod tests {
273 use super::*;
274 use crate::{ast::*, lex, Diagnostics};
275
276 fn parse(src: &str) -> Expr {
277 let mut d = Diagnostics::default();
278 let toks = lex(src, &mut d);
279 let mut p = Parser::new(&toks);
280 let e = p.parse_expr(&mut d);
281 assert!(d.is_empty(), "unexpected errors:\n{}", d.render(src));
282 e
283 }
284
285 #[test]
286 fn and_binds_tighter_than_or() {
287 match parse("a() | b() & c()") {
289 Expr::Or(l, r, _) => {
290 assert!(matches!(*l, Expr::Atom(_)));
291 assert!(matches!(*r, Expr::And(_, _, _)), "rhs must be the conjunction");
292 }
293 other => panic!("expected Or, got {other:?}"),
294 }
295 }
296
297 #[test]
298 fn implication_is_right_associative_and_loosest() {
299 match parse("a() -> b() -> c()") {
301 Expr::Implies(_, r, _) => assert!(matches!(*r, Expr::Implies(_, _, _))),
302 other => panic!("expected Implies, got {other:?}"),
303 }
304 }
305
306 #[test]
307 fn negation_scopes_over_a_modality_not_inside_it() {
308 match parse("!K[a] p()") {
310 Expr::Not(inner, _) => {
311 assert!(matches!(*inner, Expr::Modality { op: Modal::Knows, .. }));
312 }
313 other => panic!("expected Not, got {other:?}"),
314 }
315 }
316
317 #[test]
318 fn agent_lists_are_preserved_for_lowering() {
319 match parse("K[alice, bob] p()") {
320 Expr::Modality { op: Modal::Knows, agents: Some(a), .. } => {
321 assert_eq!(a, vec![Arg::Obj("alice".into()), Arg::Obj("bob".into())]);
322 }
323 other => panic!("expected Knows with two agents, got {other:?}"),
324 }
325 }
326
327 #[test]
328 fn a_variable_may_stand_where_an_agent_name_does() {
329 match parse("B[?who] p()") {
333 Expr::Modality { op: Modal::Believes, agents: Some(a), .. } => {
334 assert_eq!(a, vec![Arg::Var("who".into())]);
335 }
336 other => panic!("expected Believes with a variable agent, got {other:?}"),
337 }
338 match parse("C[alice, ?other] p()") {
340 Expr::Modality { op: Modal::Common, agents: Some(a), .. } => {
341 assert_eq!(a, vec![Arg::Obj("alice".into()), Arg::Var("other".into())]);
342 }
343 other => panic!("expected Common with a mixed list, got {other:?}"),
344 }
345 }
346
347 #[test]
348 fn common_knowledge_star_has_no_agent_list() {
349 match parse("C[*] p()") {
350 Expr::Modality { op: Modal::Common, agents: None, .. } => {}
351 other => panic!("expected C[*], got {other:?}"),
352 }
353 }
354
355 #[test]
356 fn every_sugar_form_parses_to_its_own_operator() {
357 let cases = [
358 ("K'[a] p()", Modal::KnowsDual),
359 ("B'[a] p()", Modal::BelievesDual),
360 ("S'[a] p()", Modal::SafeDual),
361 ("Kw[a] p()", Modal::KnowsWhether),
362 ("Bw[a] p()", Modal::BelievesWhether),
363 ("?[a] p()", Modal::Ignorant),
364 ("??[a] p()", Modal::Undecided),
365 ("[][a] p()", Modal::Safe),
366 ];
367 for (src, want) in cases {
368 match parse(src) {
369 Expr::Modality { op, .. } => assert_eq!(op, want, "for input {src}"),
370 other => panic!("{src}: expected a modality, got {other:?}"),
371 }
372 }
373 }
374
375 #[test]
376 fn conditional_belief_captures_both_operands() {
377 match parse("B^q()[a] p()") {
379 Expr::Modality { op: Modal::Believes, cond: Some(c), body, .. } => {
380 assert!(matches!(*c, Expr::Atom(ref t) if t.pred == "q"));
381 assert!(matches!(*body, Expr::Atom(ref t) if t.pred == "p"));
382 }
383 other => panic!("expected conditional belief, got {other:?}"),
384 }
385 }
386
387 #[test]
388 fn a_negated_condition_needs_no_parentheses() {
389 let bare = parse("B^ !q() [a] p()");
398 let parens = parse("B^(!q())[a] p()");
399 assert_eq!(bare, parens, "`B^!q[a] p` must parse as `B^(!q)[a] p`");
400 match bare {
401 Expr::Modality { op: Modal::Believes, cond: Some(c), .. } => match *c {
402 Expr::Not(inner, _) => {
403 assert!(matches!(*inner, Expr::Atom(ref t) if t.pred == "q"));
404 }
405 other => panic!("expected the condition to be a negation, got {other:?}"),
406 },
407 other => panic!("expected a conditional belief, got {other:?}"),
408 }
409 }
410
411 #[test]
412 fn predicate_arguments_distinguish_objects_variables_and_types() {
413 match parse("at(?a, study)") {
414 Expr::Atom(t) => {
415 assert_eq!(t.pred, "at");
416 assert_eq!(t.args, vec![Arg::Var("a".into()), Arg::Obj("study".into())]);
417 }
418 other => panic!("expected an atom, got {other:?}"),
419 }
420 match parse("adjacent(Location, Location)") {
423 Expr::Atom(t) => {
424 assert_eq!(t.args, vec![Arg::Ty("Location".into()), Arg::Ty("Location".into())]);
425 }
426 other => panic!("expected an atom, got {other:?}"),
427 }
428 }
429
430 #[test]
431 fn a_missing_closing_paren_reports_a_span() {
432 let mut d = Diagnostics::default();
433 let toks = lex("(a() & b()", &mut d);
434 let mut p = Parser::new(&toks);
435 let _ = p.parse_expr(&mut d);
436 assert_eq!(d.len(), 1);
437 assert!(d.items()[0].message.contains(')'), "message should name the expected token");
438 }
439}