From 08bc67140192b6a1464dcacc2cf57a80d7afb7d2 Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Sat, 21 Jan 2017 19:22:22 -0800
Subject: [PATCH] added syntatic sugar, xor, implies, and iff

---
 stl/parser.py | 16 +++++++++++++---
 stl/utils.py  |  9 +++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/stl/parser.py b/stl/parser.py
index 03490b5..7577c24 100644
--- a/stl/parser.py
+++ b/stl/parser.py
@@ -19,14 +19,18 @@ from lenses import lens
 from sympy import Symbol, Number
 
 from stl import ast
+from stl.utils import implies, xor, iff
 
 STL_GRAMMAR = Grammar(u'''
-phi = (g / f / until / lineq / AP / or / and / neg / paren_phi)
+phi = (g / f / until / lineq / AP / or / and / implies / xor / iff / neg / paren_phi)
 
 paren_phi = "(" __ phi __ ")"
 
 or = paren_phi _ ("∨" / "or" / "|") _ (or / paren_phi)
 and = paren_phi _ ("∧" / "and" / "&") _ (and / paren_phi)
+implies = paren_phi _ ("→" / "->") _ (and / paren_phi)
+iff = paren_phi _ ("⇔" / "<->" / "iff") _ (and / paren_phi)
+xor = paren_phi _ ("⊕" / "^" / "xor") _ (and / paren_phi)
 
 neg = ("~" / "¬") paren_phi
 
@@ -64,8 +68,7 @@ _ = ~r"\s"+
 __ = ~r"\s"*
 EOL = "\\n"
 ''')
-
-
+    
 class STLVisitor(NodeVisitor):
     def generic_visit(self, _, children):
         return children
@@ -98,10 +101,17 @@ class STLVisitor(NodeVisitor):
         argR = list(phi2.args) if isinstance(phi2, op) else [phi2]
         return op(tuple(argL + argR))
 
+    def sugar_binop_visitor(self, _, children, op):
+        phi1, _, _, _, (phi2,) = children
+        return op(phi1, phi2)
+
     visit_f = partialmethod(unary_temp_op_visitor, op=ast.F)
     visit_g = partialmethod(unary_temp_op_visitor, op=ast.G)
     visit_or = partialmethod(binop_visitor, op=ast.Or)
     visit_and = partialmethod(binop_visitor, op=ast.And)
+    visit_xor = partialmethod(sugar_binop_visitor, op=xor)
+    visit_iff = partialmethod(sugar_binop_visitor, op=iff)
+    visit_implies = partialmethod(sugar_binop_visitor, op=implies)
 
     def visit_until(self, _, children):
         _, _, phi1, _, _, i, _, phi2, *_ = children
diff --git a/stl/utils.py b/stl/utils.py
index a5ccb31..19e7bf2 100644
--- a/stl/utils.py
+++ b/stl/utils.py
@@ -147,3 +147,12 @@ def andf(*args):
 
 def orf(*args):
     return reduce(op.or_, args, stl.Or(tuple()))
+
+def implies(x, y):
+    return ~x | y
+
+def xor(x, y):
+    return (x | y) & ~(x & y)
+
+def iff(x, y):
+    return (x & y) | (~x & ~y)