Sapan Bhatia | 64c7251 | 2017-06-23 02:32:45 -0700 | [diff] [blame^] | 1 | __author__ = "Sapan Bhatia" |
| 2 | |
| 3 | __copyright__ = "Copyright (C) 2017 Open Networking Lab" |
| 4 | __version__ = "1.0" |
| 5 | |
| 6 | import ply.lex as lex |
| 7 | import ply.yacc as yacc |
| 8 | |
| 9 | from helpers import LexHelper, LU |
| 10 | |
| 11 | class FOLLexer(object): |
| 12 | keywords = ('forall', 'exists', 'true', 'false', 'not') |
| 13 | |
| 14 | tokens = ['ESCAPE', 'COLON', 'IMPLIES', 'OR', 'AND', 'LPAREN', 'RPAREN', 'EQUALS', 'SYMBOL', 'LT', 'RT'] + [k.upper() for k in keywords] |
| 15 | # literals = '()+-*/=?:,.^|&~!=[]{};<>@%' |
| 16 | |
| 17 | t_ignore_LINE_COMMENT = '//.*' |
| 18 | t_COLON = '\\:' |
| 19 | t_IMPLIES = '\\-\\>' |
| 20 | t_OR = '\\|' |
| 21 | t_LT = '\\<' |
| 22 | t_RT = '\\>' |
| 23 | t_AND = '\\&' |
| 24 | t_LPAREN = '\\(' |
| 25 | t_RPAREN = '\\)' |
| 26 | |
| 27 | t_EQUALS = '\\=' |
| 28 | |
| 29 | literals = '()+-*/=?:,.^|&~!=[]{};<>@%' |
| 30 | |
| 31 | t_ignore = ' \t\f' |
| 32 | |
| 33 | def t_newline(self, t): |
| 34 | r'\n+' |
| 35 | t.lexer.lineno += len(t.value) |
| 36 | |
| 37 | def t_newline2(self, t): |
| 38 | r'(\r\n)+' |
| 39 | t.lexer.lineno += len(t.value) / 2 |
| 40 | |
| 41 | t_ESCAPE = r'{{ (.|\n)*? }}' |
| 42 | |
| 43 | def t_BLOCK_COMMENT(self, t): |
| 44 | r'/\*(.|\n)*?\*/' |
| 45 | t.lexer.lineno += t.value.count('\n') |
| 46 | |
| 47 | def t_SYMBOL(self, t): |
| 48 | '[A-Za-z_$][\.A-Za-z0-9_+$]*' |
| 49 | if t.value in FOLLexer.keywords: |
| 50 | t.type = t.value.upper() |
| 51 | return t |
| 52 | |
| 53 | def t_error(self, t): |
| 54 | print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno)) |
| 55 | t.lexer.skip(1) |
| 56 | |
| 57 | |
| 58 | |
| 59 | class FOLParser(object): |
| 60 | tokens = FOLLexer.tokens |
| 61 | offset = 0 |
| 62 | lh = LexHelper() |
| 63 | |
| 64 | def setOffset(self, of): |
| 65 | self.offset = of |
| 66 | self.lh.offset = of |
| 67 | |
| 68 | def p_empty(self, p): |
| 69 | '''empty :''' |
| 70 | pass |
| 71 | |
| 72 | def p_term_constant(self, p): |
| 73 | '''term : FALSE |
| 74 | | TRUE''' |
| 75 | p[0] = p[1] |
| 76 | |
| 77 | def p_fole_not(self, p): |
| 78 | '''fole : NOT fole''' |
| 79 | p[0] = {p[1]: p[2]} |
| 80 | |
| 81 | def p_fole_term(self, p): |
| 82 | '''fole : term''' |
| 83 | p[0] = p[1] |
| 84 | |
| 85 | def p_term_symbol(self, p): |
| 86 | '''term : SYMBOL''' |
| 87 | p[0] = p[1] |
| 88 | |
| 89 | def p_term_python(self, p): |
| 90 | '''fole : ESCAPE ''' |
| 91 | p[0] = {'python': p[1]} |
| 92 | |
| 93 | def p_fole_group(self, p): |
| 94 | "fole : LPAREN fole RPAREN" |
| 95 | p[0] = p[2] |
| 96 | |
| 97 | def p_fole_equals(self, p): |
| 98 | "fole : term EQUALS term" |
| 99 | p[0] = {'=': (p[1], p[3])} |
| 100 | |
| 101 | def p_fole_binary(self, p): |
| 102 | '''fole : fole AND fole |
| 103 | | fole OR fole |
| 104 | | fole IMPLIES fole''' |
| 105 | p[0] = {p[2]: [p[1], p[3]]} |
| 106 | |
| 107 | def p_fole_quant(self, p): |
| 108 | '''fole : FORALL SYMBOL COLON fole |
| 109 | | EXISTS SYMBOL COLON fole''' |
| 110 | p[0] = {p[1]: [p[2], p[4]]} |
| 111 | |
| 112 | |
| 113 | def p_goal(self, p): |
| 114 | '''goal : LT fole RT''' |
| 115 | p[0] = p[2] |
| 116 | |
| 117 | def p_error(self, p): |
| 118 | print('error: {}'.format(p)) |
| 119 | |