Skip to content

Commit

Permalink
Removed comma necessity after quantifier
Browse files Browse the repository at this point in the history
Changed the parsing when using quantifiers to only require a single space after the variable
  • Loading branch information
zacharybonagura committed Oct 3, 2024
1 parent 27fbab1 commit e72c4ef
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion aris/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,8 +87,12 @@ fn quantifier(input: &str) -> IResult<&str, QuantKind> {
alt((forall_quantifier, exists_quantifier))(input)
}

fn space_after_quantifier(input: &str) -> IResult<&str, ()> {
value((), many1(one_of(" \t")))(input)
}

fn binder(input: &str) -> IResult<&str, Expr> {
map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(tuple((space, tag(","), space)), expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
map(tuple((preceded(space, quantifier), preceded(space, variable), preceded(space_after_quantifier, expr))), |(kind, name, body)| Expr::Quant { kind, name, body: Box::new(body) })(input)
}

fn impl_term(input: &str) -> IResult<&str, Expr> {
Expand Down

0 comments on commit e72c4ef

Please sign in to comment.