Skip to content

Commit

Permalink
Merge pull request #131 from Bram-Hub/revert-130-revert-129-master
Browse files Browse the repository at this point in the history 
Revert "Revert "Removed comma necessity after quantifier, fixed formatting errors, fixed old tests to pass with new changes""
  • Loading branch information
@zacharybonagura
zacharybonagura authored Oct 4, 2024
2 parents e07613c + f71fb02 commit 4057ba9
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 4057ba9

Please sign in to comment.