Support for policies in first-order logic
diff --git a/plyxproto/logicparser.py b/plyxproto/logicparser.py
new file mode 100644
index 0000000..8bdfb1c
--- /dev/null
+++ b/plyxproto/logicparser.py
@@ -0,0 +1,119 @@
+__author__ = "Sapan Bhatia"
+
+__copyright__ = "Copyright (C) 2017 Open Networking Lab"
+__version__ = "1.0"
+
+import ply.lex as lex
+import ply.yacc as yacc
+
+from helpers import LexHelper, LU
+
+class FOLLexer(object):
+ keywords = ('forall', 'exists', 'true', 'false', 'not')
+
+ tokens = ['ESCAPE', 'COLON', 'IMPLIES', 'OR', 'AND', 'LPAREN', 'RPAREN', 'EQUALS', 'SYMBOL', 'LT', 'RT'] + [k.upper() for k in keywords]
+ # literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+ t_ignore_LINE_COMMENT = '//.*'
+ t_COLON = '\\:'
+ t_IMPLIES = '\\-\\>'
+ t_OR = '\\|'
+ t_LT = '\\<'
+ t_RT = '\\>'
+ t_AND = '\\&'
+ t_LPAREN = '\\('
+ t_RPAREN = '\\)'
+
+ t_EQUALS = '\\='
+
+ literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+ t_ignore = ' \t\f'
+
+ def t_newline(self, t):
+ r'\n+'
+ t.lexer.lineno += len(t.value)
+
+ def t_newline2(self, t):
+ r'(\r\n)+'
+ t.lexer.lineno += len(t.value) / 2
+
+ t_ESCAPE = r'{{ (.|\n)*? }}'
+
+ def t_BLOCK_COMMENT(self, t):
+ r'/\*(.|\n)*?\*/'
+ t.lexer.lineno += t.value.count('\n')
+
+ def t_SYMBOL(self, t):
+ '[A-Za-z_$][\.A-Za-z0-9_+$]*'
+ if t.value in FOLLexer.keywords:
+ t.type = t.value.upper()
+ return t
+
+ def t_error(self, t):
+ print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno))
+ t.lexer.skip(1)
+
+
+
+class FOLParser(object):
+ tokens = FOLLexer.tokens
+ offset = 0
+ lh = LexHelper()
+
+ def setOffset(self, of):
+ self.offset = of
+ self.lh.offset = of
+
+ def p_empty(self, p):
+ '''empty :'''
+ pass
+
+ def p_term_constant(self, p):
+ '''term : FALSE
+ | TRUE'''
+ p[0] = p[1]
+
+ def p_fole_not(self, p):
+ '''fole : NOT fole'''
+ p[0] = {p[1]: p[2]}
+
+ def p_fole_term(self, p):
+ '''fole : term'''
+ p[0] = p[1]
+
+ def p_term_symbol(self, p):
+ '''term : SYMBOL'''
+ p[0] = p[1]
+
+ def p_term_python(self, p):
+ '''fole : ESCAPE '''
+ p[0] = {'python': p[1]}
+
+ def p_fole_group(self, p):
+ "fole : LPAREN fole RPAREN"
+ p[0] = p[2]
+
+ def p_fole_equals(self, p):
+ "fole : term EQUALS term"
+ p[0] = {'=': (p[1], p[3])}
+
+ def p_fole_binary(self, p):
+ '''fole : fole AND fole
+ | fole OR fole
+ | fole IMPLIES fole'''
+ p[0] = {p[2]: [p[1], p[3]]}
+
+ def p_fole_quant(self, p):
+ '''fole : FORALL SYMBOL COLON fole
+ | EXISTS SYMBOL COLON fole'''
+ p[0] = {p[1]: [p[2], p[4]]}
+
+
+ def p_goal(self, p):
+ '''goal : LT fole RT'''
+ p[0] = p[2]
+
+ def p_error(self, p):
+ print('error: {}'.format(p))
+