Fix a misparse of quantifiers (their scope now extends over assocbino…

…p terms).
Bram-Hub · Jan 16, 2019 · 9394d8c · 9394d8c
1 parent 5feb103
commit 9394d8c
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 3 deletions.
diff --git a/libaris/src/main/rust/src/expression.rs b/libaris/src/main/rust/src/expression.rs
@@ -1,4 +1,5 @@
 use super::*;
+use std::collections::HashSet;
 
 #[no_mangle]
 #[allow(non_snake_case)]
@@ -177,6 +178,20 @@ impl HasClass for Expr {
     }
 }
 
+pub fn freevars(e: &Expr) -> HashSet<String> {
+    let mut r = HashSet::new();
+    match e {
+        Expr::Bottom => (),
+        Expr::Predicate { name, args } => { r.insert(name.clone()); r.extend(args.iter().cloned()); },
+        Expr::Unop { operand, .. } => { r.extend(freevars(operand)); },
+        Expr::Binop { left, right, .. } => { r.extend(freevars(left)); r.extend(freevars(right)); },
+        Expr::AssocBinop { exprs, .. } => { for expr in exprs.iter() { r.extend(freevars(expr)); } }
+        Expr::Quantifier { name, body, .. } => { r.extend(freevars(body)); r.remove(name); }
+    }
+    r
+}
+
+
 pub mod expression_builders {
     use super::{Expr, USymbol, BSymbol, ASymbol, QSymbol};
     pub fn predicate(name: &str, args: &[&str]) -> Expr { Expr::Predicate { name: name.into(), args: args.iter().map(|&x| x.into()).collect() } }

diff --git a/libaris/src/main/rust/src/parser.rs b/libaris/src/main/rust/src/parser.rs
@@ -30,7 +30,7 @@ named!(predicate<&str, Expr>, alt!(
 named!(forallQuantifier<&str, QSymbol>, do_parse!(alt!(tag!("forall ") | tag!("∀")) >> (QSymbol::Forall)));
 named!(existsQuantifier<&str, QSymbol>, do_parse!(alt!(tag!("exists ") | tag!("∃")) >> (QSymbol::Exists)));
 named!(quantifier<&str, QSymbol>, alt!(forallQuantifier | existsQuantifier));
-named!(binder<&str, Expr>, do_parse!(space >> symbol: quantifier >> space >> name: variable >> space >> tag!(",") >> space >> body: paren_expr >> (Expr::Quantifier { symbol, name, body: Box::new(body) })));
+named!(binder<&str, Expr>, do_parse!(space >> symbol: quantifier >> space >> name: variable >> space >> tag!(",") >> space >> body: expr >> (Expr::Quantifier { symbol, name, body: Box::new(body) })));
 
 named!(binop<&str, BSymbol>, alt!(do_parse!(tag!("->") >> (BSymbol::Implies)) | do_parse!(tag!("+") >> (BSymbol::Plus)) | do_parse!(tag!("*") >> (BSymbol::Mult))));
 named!(binopterm<&str, Expr>, do_parse!(left: paren_expr >> space >> symbol: binop >> space >> right: paren_expr >> (Expr::Binop { symbol, left: Box::new(left), right: Box::new(right) })));
@@ -63,11 +63,18 @@ named!(pub expr<&str, Expr>, alt!(assocterm | binopterm | paren_expr));
 named!(pub main<&str, Expr>, do_parse!(e: expr >> tag!("\n") >> (e)));
 
 #[test]
-fn test() {
+fn test_parser() {
+    use super::freevars;
     println!("{:?}", predicate("a(   b, c)"));
     println!("{:?}", expr("a & b & c(x,y)\n"));
     println!("{:?}", expr("forall a, (b & c)\n"));
-    println!("{:?}", expr("exists x, (Tet(x) & SameCol(x, b)) -> ~forall x, (Tet(x) -> LeftOf(x, b))\n"));
+    let e = expr("exists x, (Tet(x) & SameCol(x, b)) -> ~forall x, (Tet(x) -> LeftOf(x, b))\n");
+    let fv = e.clone().map(|x| freevars(&x.1));
+    println!("{:?} {:?}", e, fv);
+    let e = expr("forall a, forall b, ((forall x, in(x,a) <-> in(x,b)) -> eq(a,b))\n");
+    let fv = e.clone().map(|x| freevars(&x.1));
+    assert_eq!(fv, Ok(["eq", "in"].iter().map(|x| String::from(*x)).collect()));
+    println!("{:?} {:?}", e, fv);
     named!(f<&str, Vec<&str>>, many1!(tag!("a")));
     println!("{:?}", f("aa\n"));
 }