Skip to content

Commit

Permalink
Revert "Revert "Removed comma necessity after quantifier, fixed forma…
Browse files Browse the repository at this point in the history 
…tting errors, fixed old tests to pass with new changes""
  • Loading branch information
@zacharybonagura
zacharybonagura authored Oct 4, 2024
1 parent e07613c commit f71fb02
Show file tree
Hide file tree
Showing 9 changed files with 94 additions and 90 deletions.
42 changes: 21 additions & 21 deletions aris/src/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Parsing an expression that's statically known to be valid:
```
use aris::parser::parse_unwrap as p;
let expr1 = p("forall x, p(x) -> (Q & R)");
let expr1 = p("forall x p(x) -> (Q & R)");
```
Parsing a potentially malformed expression (e.g. user input):
Expand Down Expand Up @@ -389,7 +389,7 @@ pub fn unify(mut c: HashSet<Constraint>) -> Option<Substitution> {
}
(Expr::Apply { func: sf, args: sa }, Expr::Apply { func: tf, args: ta }) if sa.len() == ta.len() => {
c.insert(Constraint::Equal(*sf, *tf));
c.extend(sa.into_iter().zip(ta.into_iter()).map(|(x, y)| Constraint::Equal(x, y)));
c.extend(sa.into_iter().zip(ta).map(|(x, y)| Constraint::Equal(x, y)));
unify(c)
}
(Expr::Assoc { op: so, exprs: se }, Expr::Assoc { op: to, exprs: te }) if so == to && se.len() == te.len() => {
Expand Down Expand Up @@ -887,7 +887,7 @@ impl Expr {
Expr::Var { name: format!("{i}") }
}
// push the name onto gamma from the actual quantifier,
// Example: for forall x, P(x)
// Example: for forall x P(x)
// push x onto gamma
// save the length of gamma before recursing, to use as the new name
Expr::Quant { kind, name, body } => {
Expand Down Expand Up @@ -966,14 +966,14 @@ impl Expr {
})
}

/// 7a1. forall x, (phi(x) ∧ psi) == (forall x, phi(x)) ∧ psi
/// 7a2. exists x, (phi(x) ∧ psi) == (exists x, phi(x)) ∧ psi
/// 7b1. forall x, (phi(x) ∨ psi) == (forall x, phi(x)) ∨ psi
/// 7b2. exists x, (phi(x) ∨ psi) == (exists x, phi(x)) ∨ psi
/// 7c1. forall x, (phi(x) → psi) == (exists x, phi(x)) → psi (! Expr::Quantifier changes!)
/// 7c2. exists x, (phi(x) → psi) == (forall x, phi(x)) → psi (! Expr::Quantifier changes!)
/// 7d1. forall x, (psi → phi(x)) == psi → (forall x, phi(x))
/// 7d2. exists x, (psi → phi(x)) == psi → (exists x, phi(x))
/// 7a1. forall x (phi(x) ∧ psi) == (forall x phi(x)) ∧ psi
/// 7a2. exists x (phi(x) ∧ psi) == (exists x phi(x)) ∧ psi
/// 7b1. forall x (phi(x) ∨ psi) == (forall x phi(x)) ∨ psi
/// 7b2. exists x (phi(x) ∨ psi) == (exists x phi(x)) ∨ psi
/// 7c1. forall x (phi(x) → psi) == (exists x phi(x)) → psi (! Expr::Quantifier changes!)
/// 7c2. exists x (phi(x) → psi) == (forall x phi(x)) → psi (! Expr::Quantifier changes!)
/// 7d1. forall x (psi → phi(x)) == psi → (forall x phi(x))
/// 7d2. exists x (psi → phi(x)) == psi → (exists x phi(x))
pub fn normalize_prenex_laws(self) -> Expr {
let transform_7ab = |op: Op, exprs: Vec<Expr>| {
// hoist a forall out of an and/or when the binder won't capture any of the other arms
Expand Down Expand Up @@ -1534,11 +1534,11 @@ mod tests {
#[test]
fn test_subst() {
use crate::parser::parse_unwrap as p;
assert_eq!(subst(p("x & forall x, x"), "x", p("y")), p("y & forall x, x")); // hit (true, _) case in Expr::Quantifier
assert_eq!(subst(p("forall x, x & y"), "y", p("x")), p("forall x0, x0 & x")); // hit (false, true) case in Expr::Quantifier
assert_eq!(subst(p("forall x, x & y"), "y", p("z")), p("forall x, x & z")); // hit (false, false) case in Expr::Quantifier
assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("h")), p("forall f, f(x) & h(y, z)"));
assert_eq!(subst(p("forall f, f(x) & g(y, z)"), "g", p("f")), p("forall f0, f0(x) & f(y, z)"));
assert_eq!(subst(p("x & forall x x"), "x", p("y")), p("y & forall x x")); // hit (true, _) case in Expr::Quantifier
assert_eq!(subst(p("forall x x & y"), "y", p("x")), p("forall x0 x0 & x")); // hit (false, true) case in Expr::Quantifier
assert_eq!(subst(p("forall x x & y"), "y", p("z")), p("forall x x & z")); // hit (false, false) case in Expr::Quantifier
assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("h")), p("forall f f(x) & h(y, z)"));
assert_eq!(subst(p("forall f f(x) & g(y, z)"), "g", p("f")), p("forall f0 f0(x) & f(y, z)"));
}

#[test]
Expand All @@ -1556,15 +1556,15 @@ mod tests {
}
ret
};
println!("{:?}", u("x", "forall y, y"));
println!("{:?}", u("forall y, y", "y"));
println!("{:?}", u("x", "forall y y"));
println!("{:?}", u("forall y y", "y"));
println!("{:?}", u("x", "x"));
assert_eq!(u("forall x, x", "forall y, y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
assert_eq!(u("forall x x", "forall y y"), Some(Substitution(vec![]))); // should be equal with no substitution since unification is modulo alpha equivalence
println!("{:?}", u("f(x,y,z)", "g(x,y,y)"));
println!("{:?}", u("g(x,y,y)", "f(x,y,z)"));
println!("{:?}", u("forall foo, foo(x,y,z) & bar", "forall bar, bar(x,y,z) & baz"));
println!("{:?}", u("forall foo foo(x,y,z) & bar", "forall bar bar(x,y,z) & baz"));

assert_eq!(u("forall x, z", "forall y, y"), None);
assert_eq!(u("forall x z", "forall y y"), None);
assert_eq!(u("x & y", "x | y"), None);
}

Expand Down
12 changes: 8 additions & 4 deletions aris/src/parser.rs
View file
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 Expand Up @@ -165,11 +169,11 @@ fn test_parser() {
println!("{:?}", predicate("a( b, c)"));
println!("{:?}", predicate("s(s(s(s(s(z)))))"));
println!("{:?}", expr("a & b & c(x,y)\n"));
println!("{:?}", expr("forall a, (b & c)\n"));
let e = expr("exists x, (Tet(x) & SameCol(x, b)) -> ~forall x, (Tet(x) -> LeftOf(x, b))\n").unwrap();
println!("{:?}", expr("forall a (b & c)\n"));
let e = expr("exists x (Tet(x) & SameCol(x, b)) -> ~forall x (Tet(x) -> LeftOf(x, b))\n").unwrap();
let fv = free_vars(&e.1);
println!("{e:?} {fv:?}");
let e = expr("forall a, forall b, ((forall x, in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
let e = expr("forall a forall b ((forall x in(x,a) <-> in(x,b)) -> eq(a,b))\n").unwrap();
let fv = free_vars(&e.1);
assert_eq!(fv, ["eq", "in"].iter().map(|x| String::from(*x)).collect());
println!("{e:?} {fv:?}");
Expand Down
2 changes: 1 addition & 1 deletion aris/src/proofs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ pub trait Proof: Sized {
}
fn contained_justifications(&self, include_premises: bool) -> HashSet<PjRef<Self>> {
let mut ret = self.lines().into_iter().filter_map(|x| x.fold(hlist![|r: Self::JustificationReference| Some(vec![r].into_iter().map(Coproduct::inject).collect()), |r: Self::SubproofReference| self.lookup_subproof(&r).map(|sub| sub.contained_justifications(include_premises)),])).fold(HashSet::new(), |mut x, y| {
x.extend(y.into_iter());
x.extend(y);
x
});
if include_premises {
Expand Down
Loading

0 comments on commit f71fb02

Please sign in to comment.