From 9ef4604f1f7eee1600d411bef887ac056cc4c537 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 2 Aug 2022 20:23:41 +0000 Subject: [PATCH 1/6] pyk/test_pretty_print_kast: add failing test of sort declaration --- pyk/src/pyk/tests/test_pretty_print_kast.py | 1 + 1 file changed, 1 insertion(+) diff --git a/pyk/src/pyk/tests/test_pretty_print_kast.py b/pyk/src/pyk/tests/test_pretty_print_kast.py index 0da09d79890..fec8606d105 100644 --- a/pyk/src/pyk/tests/test_pretty_print_kast.py +++ b/pyk/src/pyk/tests/test_pretty_print_kast.py @@ -17,6 +17,7 @@ class PrettyPrintKastTest(TestCase): (KRule(Bool.true), 'rule true\n '), (KRule(Bool.true, ensures=Bool.true), 'rule true\n '), (KRule(Bool.true, ensures=KApply('_andBool_', [Bool.true, Bool.true])), 'rule true\n ensures ( true\n andBool ( true\n ))\n '), + (KProduction(KSort('Test')), 'syntax Test'), ) SYMBOL_TABLE: Final[SymbolTable] = {} From bab5b8321b8b86602eaf3d42a9851852d505f250 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 2 Aug 2022 20:25:06 +0000 Subject: [PATCH 2/6] pyk/ktool/kprint: fix bug in printing KProduction --- pyk/src/pyk/ktool/kprint.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 47056bb21f2..29dce8ca782 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -152,6 +152,8 @@ def prettyPrintKast(kast: KAst, symbol_table: SymbolTable, debug=False): if 'klabel' not in kast.att and kast.klabel: kast = kast.update_atts({'klabel': kast.klabel.name}) sortStr = prettyPrintKast(kast.sort, symbol_table, debug=debug) + if not kast.items: + return 'syntax ' + sortStr productionStr = ' '.join([prettyPrintKast(pi, symbol_table, debug=debug) for pi in kast.items]) attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) return 'syntax ' + sortStr + ' ::= ' + productionStr + ' ' + attStr From 4c8ea9eda6c0feab00659dbe00e5898b37208c2a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 2 Aug 2022 20:28:20 +0000 Subject: [PATCH 3/6] pyk/: rename prettyPrintKast => pretty_print_kast --- pyk/src/pyk/__main__.py | 4 +- pyk/src/pyk/ktool/__init__.py | 3 +- pyk/src/pyk/ktool/kprint.py | 78 ++++++++++----------- pyk/src/pyk/tests/test_pretty_print_kast.py | 4 +- 4 files changed, 44 insertions(+), 45 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 37bf864cd39..4b9b213b3a3 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -15,7 +15,7 @@ propagate_up_constraints, removeSourceMap, ) -from .ktool import KPrint, KProve, build_symbol_table, prettyPrintKast +from .ktool import KPrint, KProve, build_symbol_table, pretty_print_kast from .prelude import Sorts, mlAnd, mlOr, mlTop _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' @@ -84,7 +84,7 @@ def main(): args['output'].write('\n\n') args['output'].write('Rule: ' + rid.strip()) args['output'].write('\nUnparsed:\n') - args['output'].write(prettyPrintKast(rule, symbol_table)) + args['output'].write(pretty_print_kast(rule, symbol_table)) else: raise ValueError(f'Unknown command: {args["command"]}') diff --git a/pyk/src/pyk/ktool/__init__.py b/pyk/src/pyk/ktool/__init__.py index b02872349a1..8358bc257c4 100644 --- a/pyk/src/pyk/ktool/__init__.py +++ b/pyk/src/pyk/ktool/__init__.py @@ -5,8 +5,7 @@ build_symbol_table, indent, paren, - prettyPrintKast, - prettyPrintKastBool, + pretty_print_kast, unparser_for_production, ) from .kprove import KProve, kprove diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 29dce8ca782..f9d4b491fc3 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -55,7 +55,7 @@ def pretty_print(self, kast: KAst, debug=False): - Input: KAST term in JSON. - Output: Best-effort pretty-printed representation of the KAST term. """ - return prettyPrintKast(kast, self.symbol_table, debug=debug) + return pretty_print_kast(kast, self.symbol_table, debug=debug) def unparser_for_production(prod): @@ -97,7 +97,7 @@ def build_symbol_table(definition: KDefinition, opinionated=False) -> SymbolTabl return symbol_table -def prettyPrintKast(kast: KAst, symbol_table: SymbolTable, debug=False): +def pretty_print_kast(kast: KAst, symbol_table: SymbolTable, debug=False): """Print out KAST terms/outer syntax. - Input: KAST term. @@ -116,7 +116,7 @@ def prettyPrintKast(kast: KAst, symbol_table: SymbolTable, debug=False): if type(kast) is KApply: label = kast.label.name args = kast.args - unparsedArgs = [prettyPrintKast(arg, symbol_table, debug=debug) for arg in args] + unparsedArgs = [pretty_print_kast(arg, symbol_table, debug=debug) for arg in args] if kast.is_cell: cellContents = '\n'.join(unparsedArgs).rstrip() cellStr = label + '\n' + indent(cellContents) + '\n ' + rhsStr + ' )' if type(kast) is KSequence: if kast.arity == 0: - return prettyPrintKast(KApply(Labels.EMPTY_K), symbol_table, debug=debug) + return pretty_print_kast(KApply(Labels.EMPTY_K), symbol_table, debug=debug) if kast.arity == 1: - return prettyPrintKast(kast.items[0], symbol_table, debug=debug) - unparsedKSequence = '\n~> '.join([prettyPrintKast(item, symbol_table, debug=debug) for item in kast.items[0:-1]]) + return pretty_print_kast(kast.items[0], symbol_table, debug=debug) + unparsedKSequence = '\n~> '.join([pretty_print_kast(item, symbol_table, debug=debug) for item in kast.items[0:-1]]) if kast.items[-1] == ktokenDots: - unparsedKSequence = unparsedKSequence + '\n' + prettyPrintKast(ktokenDots, symbol_table, debug=debug) + unparsedKSequence = unparsedKSequence + '\n' + pretty_print_kast(ktokenDots, symbol_table, debug=debug) else: - unparsedKSequence = unparsedKSequence + '\n~> ' + prettyPrintKast(kast.items[-1], symbol_table, debug=debug) + unparsedKSequence = unparsedKSequence + '\n~> ' + pretty_print_kast(kast.items[-1], symbol_table, debug=debug) return unparsedKSequence if type(kast) is KTerminal: return '"' + kast.value + '"' if type(kast) is KRegexTerminal: return 'r"' + kast.regex + '"' if type(kast) is KNonTerminal: - return prettyPrintKast(kast.sort, symbol_table, debug=debug) + return pretty_print_kast(kast.sort, symbol_table, debug=debug) if type(kast) is KProduction: if 'klabel' not in kast.att and kast.klabel: kast = kast.update_atts({'klabel': kast.klabel.name}) - sortStr = prettyPrintKast(kast.sort, symbol_table, debug=debug) + sortStr = pretty_print_kast(kast.sort, symbol_table, debug=debug) if not kast.items: return 'syntax ' + sortStr - productionStr = ' '.join([prettyPrintKast(pi, symbol_table, debug=debug) for pi in kast.items]) - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + productionStr = ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return 'syntax ' + sortStr + ' ::= ' + productionStr + ' ' + attStr if type(kast) is KSyntaxSort: - sortStr = prettyPrintKast(kast.sort, symbol_table, debug=debug) - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + sortStr = pretty_print_kast(kast.sort, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return 'syntax ' + sortStr + ' ' + attStr if type(kast) is KSortSynonym: - newSortStr = prettyPrintKast(kast.new_sort, symbol_table, debug=debug) - oldSortStr = prettyPrintKast(kast.old_sort, symbol_table, debug=debug) - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + newSortStr = pretty_print_kast(kast.new_sort, symbol_table, debug=debug) + oldSortStr = pretty_print_kast(kast.old_sort, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return 'syntax ' + newSortStr + ' = ' + oldSortStr + ' ' + attStr if type(kast) is KSyntaxLexical: nameStr = kast.name regexStr = kast.regex - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) # todo: proper escaping return 'syntax lexical ' + nameStr + ' = r"' + regexStr + '" ' + attStr if type(kast) is KSyntaxAssociativity: assocStr = kast.assoc.value tagsStr = ' '.join(kast.tags) - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return 'syntax associativity ' + assocStr + ' ' + tagsStr + ' ' + attStr if type(kast) is KSyntaxPriority: prioritiesStr = ' > '.join([' '.join(group) for group in kast.priorities]) - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return 'syntax priority ' + prioritiesStr + ' ' + attStr if type(kast) is KBubble: body = '// KBubble(' + kast.sentence_type + ', ' + kast.content + ')' - attStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) return body + ' ' + attStr if type(kast) is KRule or type(kast) is KClaim: - body = '\n '.join(prettyPrintKast(kast.body, symbol_table, debug=debug).split('\n')) + body = '\n '.join(pretty_print_kast(kast.body, symbol_table, debug=debug).split('\n')) ruleStr = 'rule ' if type(kast) is KRule else 'claim ' if 'label' in kast.att: ruleStr = ruleStr + '[' + kast.att['label'] + ']:' ruleStr = ruleStr + ' ' + body - attsStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attsStr = pretty_print_kast(kast.att, symbol_table, debug=debug) if kast.requires != Bool.true: - requiresStr = 'requires ' + '\n '.join(prettyPrintKastBool(kast.requires, symbol_table, debug=debug).split('\n')) + requiresStr = 'requires ' + '\n '.join(pretty_print_kast_bool(kast.requires, symbol_table, debug=debug).split('\n')) ruleStr = ruleStr + '\n ' + requiresStr if kast.ensures != Bool.true: - ensuresStr = 'ensures ' + '\n '.join(prettyPrintKastBool(kast.ensures, symbol_table, debug=debug).split('\n')) + ensuresStr = 'ensures ' + '\n '.join(pretty_print_kast_bool(kast.ensures, symbol_table, debug=debug).split('\n')) ruleStr = ruleStr + '\n ' + ensuresStr return ruleStr + '\n ' + attsStr if type(kast) is KContext: - body = indent(prettyPrintKast(kast.body, symbol_table, debug=debug)) + body = indent(pretty_print_kast(kast.body, symbol_table, debug=debug)) contextStr = 'context alias ' + body requiresStr = '' - attsStr = prettyPrintKast(kast.att, symbol_table, debug=debug) + attsStr = pretty_print_kast(kast.att, symbol_table, debug=debug) if kast.requires != Bool.true: - requiresStr = prettyPrintKast(kast.requires, symbol_table, debug=debug) + requiresStr = pretty_print_kast(kast.requires, symbol_table, debug=debug) requiresStr = 'requires ' + indent(requiresStr) return contextStr + '\n ' + requiresStr + '\n ' + attsStr if type(kast) is KAtt: @@ -217,21 +217,21 @@ def prettyPrintKast(kast: KAst, symbol_table: SymbolTable, debug=False): return ' '.join(['imports', ('public' if kast.public else 'private'), kast.name]) if type(kast) is KFlatModule: name = kast.name - imports = '\n'.join([prettyPrintKast(kimport, symbol_table, debug=debug) for kimport in kast.imports]) - sentences = '\n\n'.join([prettyPrintKast(sentence, symbol_table, debug=debug) for sentence in kast.sentences]) + imports = '\n'.join([pretty_print_kast(kimport, symbol_table, debug=debug) for kimport in kast.imports]) + sentences = '\n\n'.join([pretty_print_kast(sentence, symbol_table, debug=debug) for sentence in kast.sentences]) contents = imports + '\n\n' + sentences return 'module ' + name + '\n ' + '\n '.join(contents.split('\n')) + '\n\nendmodule' if type(kast) is KRequire: return 'requires "' + kast.require + '"' if type(kast) is KDefinition: - requires = '\n'.join([prettyPrintKast(require, symbol_table, debug=debug) for require in kast.requires]) - modules = '\n\n'.join([prettyPrintKast(module, symbol_table, debug=debug) for module in kast.modules]) + requires = '\n'.join([pretty_print_kast(require, symbol_table, debug=debug) for require in kast.requires]) + modules = '\n\n'.join([pretty_print_kast(module, symbol_table, debug=debug) for module in kast.modules]) return requires + '\n\n' + modules raise ValueError(f'Error unparsing: {kast}') -def prettyPrintKastBool(kast, symbol_table, debug=False): +def pretty_print_kast_bool(kast, symbol_table, debug=False): """Print out KAST requires/ensures clause. - Input: KAST Bool for requires/ensures clause. @@ -242,7 +242,7 @@ def prettyPrintKastBool(kast, symbol_table, debug=False): sys.stderr.write('\n') sys.stderr.flush() if type(kast) is KApply and kast.label.name in ['_andBool_', '_orBool_']: - clauses = [prettyPrintKastBool(c, symbol_table, debug=debug) for c in flattenLabel(kast.label.name, kast)] + clauses = [pretty_print_kast_bool(c, symbol_table, debug=debug) for c in flattenLabel(kast.label.name, kast)] head = kast.label.name.replace('_', ' ') if head == ' orBool ': head = ' orBool ' @@ -255,7 +255,7 @@ def joinSep(s): clauses = ['( ' + joinSep(clauses[0])] + [head + '( ' + joinSep(c) for c in clauses[1:]] + [spacer + (')' * len(clauses))] return '\n'.join(clauses) else: - return prettyPrintKast(kast, symbol_table, debug=debug) + return pretty_print_kast(kast, symbol_table, debug=debug) def paren(printer): diff --git a/pyk/src/pyk/tests/test_pretty_print_kast.py b/pyk/src/pyk/tests/test_pretty_print_kast.py index fec8606d105..f62171c6686 100644 --- a/pyk/src/pyk/tests/test_pretty_print_kast.py +++ b/pyk/src/pyk/tests/test_pretty_print_kast.py @@ -4,7 +4,7 @@ from pyk.kast import KApply, KAst, KLabel, KProduction, KRule, KSort, KTerminal from pyk.ktool.kprint import ( SymbolTable, - prettyPrintKast, + pretty_print_kast, unparser_for_production, ) from pyk.prelude import Bool @@ -25,7 +25,7 @@ class PrettyPrintKastTest(TestCase): def test_pretty_print(self): for i, (kast, expected) in enumerate(self.TEST_DATA): with self.subTest(i=i): - actual = prettyPrintKast(kast, self.SYMBOL_TABLE) + actual = pretty_print_kast(kast, self.SYMBOL_TABLE) actual_tokens = actual.split('\n') expected_tokens = expected.split('\n') self.assertListEqual(actual_tokens, expected_tokens) From 83836f1074dc0568a2df5b970ba2da597c03221e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 2 Aug 2022 20:35:26 +0000 Subject: [PATCH 4/6] pyk/ktool/kprint: rename variables using new convention --- pyk/src/pyk/ktool/__init__.py | 2 +- pyk/src/pyk/ktool/kprint.py | 118 +++++++++++++++++----------------- 2 files changed, 60 insertions(+), 60 deletions(-) diff --git a/pyk/src/pyk/ktool/__init__.py b/pyk/src/pyk/ktool/__init__.py index 8358bc257c4..1c1b15f8692 100644 --- a/pyk/src/pyk/ktool/__init__.py +++ b/pyk/src/pyk/ktool/__init__.py @@ -1,7 +1,7 @@ from .kompile import KompileBackend, kompile from .kprint import ( KPrint, - appliedLabelStr, + applied_label_str, build_symbol_table, indent, paren, diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index f9d4b491fc3..3844bb7affc 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -116,32 +116,32 @@ def pretty_print_kast(kast: KAst, symbol_table: SymbolTable, debug=False): if type(kast) is KApply: label = kast.label.name args = kast.args - unparsedArgs = [pretty_print_kast(arg, symbol_table, debug=debug) for arg in args] + unparsed_args = [pretty_print_kast(arg, symbol_table, debug=debug) for arg in args] if kast.is_cell: - cellContents = '\n'.join(unparsedArgs).rstrip() - cellStr = label + '\n' + indent(cellContents) + '\n ' + rhsStr + ' )' + lhs_str = pretty_print_kast(kast.lhs, symbol_table, debug=debug) + rhs_str = pretty_print_kast(kast.rhs, symbol_table, debug=debug) + return '( ' + lhs_str + ' => ' + rhs_str + ' )' if type(kast) is KSequence: if kast.arity == 0: return pretty_print_kast(KApply(Labels.EMPTY_K), symbol_table, debug=debug) if kast.arity == 1: return pretty_print_kast(kast.items[0], symbol_table, debug=debug) - unparsedKSequence = '\n~> '.join([pretty_print_kast(item, symbol_table, debug=debug) for item in kast.items[0:-1]]) + unparsed_k_seq = '\n~> '.join([pretty_print_kast(item, symbol_table, debug=debug) for item in kast.items[0:-1]]) if kast.items[-1] == ktokenDots: - unparsedKSequence = unparsedKSequence + '\n' + pretty_print_kast(ktokenDots, symbol_table, debug=debug) + unparsed_k_seq = unparsed_k_seq + '\n' + pretty_print_kast(ktokenDots, symbol_table, debug=debug) else: - unparsedKSequence = unparsedKSequence + '\n~> ' + pretty_print_kast(kast.items[-1], symbol_table, debug=debug) - return unparsedKSequence + unparsed_k_seq = unparsed_k_seq + '\n~> ' + pretty_print_kast(kast.items[-1], symbol_table, debug=debug) + return unparsed_k_seq if type(kast) is KTerminal: return '"' + kast.value + '"' if type(kast) is KRegexTerminal: @@ -151,68 +151,68 @@ def pretty_print_kast(kast: KAst, symbol_table: SymbolTable, debug=False): if type(kast) is KProduction: if 'klabel' not in kast.att and kast.klabel: kast = kast.update_atts({'klabel': kast.klabel.name}) - sortStr = pretty_print_kast(kast.sort, symbol_table, debug=debug) + sort_str = pretty_print_kast(kast.sort, symbol_table, debug=debug) if not kast.items: - return 'syntax ' + sortStr - productionStr = ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax ' + sortStr + ' ::= ' + productionStr + ' ' + attStr + return 'syntax ' + sort_str + production_str = ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return 'syntax ' + sort_str + ' ::= ' + production_str + ' ' + att_str if type(kast) is KSyntaxSort: - sortStr = pretty_print_kast(kast.sort, symbol_table, debug=debug) - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax ' + sortStr + ' ' + attStr + sort_str = pretty_print_kast(kast.sort, symbol_table, debug=debug) + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return 'syntax ' + sort_str + ' ' + att_str if type(kast) is KSortSynonym: - newSortStr = pretty_print_kast(kast.new_sort, symbol_table, debug=debug) - oldSortStr = pretty_print_kast(kast.old_sort, symbol_table, debug=debug) - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax ' + newSortStr + ' = ' + oldSortStr + ' ' + attStr + new_sort_str = pretty_print_kast(kast.new_sort, symbol_table, debug=debug) + old_sort_str = pretty_print_kast(kast.old_sort, symbol_table, debug=debug) + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return 'syntax ' + new_sort_str + ' = ' + old_sort_str + ' ' + att_str if type(kast) is KSyntaxLexical: - nameStr = kast.name - regexStr = kast.regex - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) + name_str = kast.name + regex_str = kast.regex + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) # todo: proper escaping - return 'syntax lexical ' + nameStr + ' = r"' + regexStr + '" ' + attStr + return 'syntax lexical ' + name_str + ' = r"' + regex_str + '" ' + att_str if type(kast) is KSyntaxAssociativity: - assocStr = kast.assoc.value - tagsStr = ' '.join(kast.tags) - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax associativity ' + assocStr + ' ' + tagsStr + ' ' + attStr + assoc_str = kast.assoc.value + tags_str = ' '.join(kast.tags) + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return 'syntax associativity ' + assoc_str + ' ' + tags_str + ' ' + att_str if type(kast) is KSyntaxPriority: - prioritiesStr = ' > '.join([' '.join(group) for group in kast.priorities]) - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax priority ' + prioritiesStr + ' ' + attStr + priorities_str = ' > '.join([' '.join(group) for group in kast.priorities]) + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return 'syntax priority ' + priorities_str + ' ' + att_str if type(kast) is KBubble: body = '// KBubble(' + kast.sentence_type + ', ' + kast.content + ')' - attStr = pretty_print_kast(kast.att, symbol_table, debug=debug) - return body + ' ' + attStr + att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) + return body + ' ' + att_str if type(kast) is KRule or type(kast) is KClaim: body = '\n '.join(pretty_print_kast(kast.body, symbol_table, debug=debug).split('\n')) - ruleStr = 'rule ' if type(kast) is KRule else 'claim ' + rule_str = 'rule ' if type(kast) is KRule else 'claim ' if 'label' in kast.att: - ruleStr = ruleStr + '[' + kast.att['label'] + ']:' - ruleStr = ruleStr + ' ' + body - attsStr = pretty_print_kast(kast.att, symbol_table, debug=debug) + rule_str = rule_str + '[' + kast.att['label'] + ']:' + rule_str = rule_str + ' ' + body + atts_str = pretty_print_kast(kast.att, symbol_table, debug=debug) if kast.requires != Bool.true: - requiresStr = 'requires ' + '\n '.join(pretty_print_kast_bool(kast.requires, symbol_table, debug=debug).split('\n')) - ruleStr = ruleStr + '\n ' + requiresStr + requires_str = 'requires ' + '\n '.join(pretty_print_kast_bool(kast.requires, symbol_table, debug=debug).split('\n')) + rule_str = rule_str + '\n ' + requires_str if kast.ensures != Bool.true: - ensuresStr = 'ensures ' + '\n '.join(pretty_print_kast_bool(kast.ensures, symbol_table, debug=debug).split('\n')) - ruleStr = ruleStr + '\n ' + ensuresStr - return ruleStr + '\n ' + attsStr + ensures_str = 'ensures ' + '\n '.join(pretty_print_kast_bool(kast.ensures, symbol_table, debug=debug).split('\n')) + rule_str = rule_str + '\n ' + ensures_str + return rule_str + '\n ' + atts_str if type(kast) is KContext: body = indent(pretty_print_kast(kast.body, symbol_table, debug=debug)) - contextStr = 'context alias ' + body - requiresStr = '' - attsStr = pretty_print_kast(kast.att, symbol_table, debug=debug) + context_str = 'context alias ' + body + requires_str = '' + atts_str = pretty_print_kast(kast.att, symbol_table, debug=debug) if kast.requires != Bool.true: - requiresStr = pretty_print_kast(kast.requires, symbol_table, debug=debug) - requiresStr = 'requires ' + indent(requiresStr) - return contextStr + '\n ' + requiresStr + '\n ' + attsStr + requires_str = pretty_print_kast(kast.requires, symbol_table, debug=debug) + requires_str = 'requires ' + indent(requires_str) + return context_str + '\n ' + requires_str + '\n ' + atts_str if type(kast) is KAtt: if not kast.atts: return '' - attStrs = [k + '(' + v + ')' for k, v in kast.atts.items()] - return '[' + ', '.join(attStrs) + ']' + att_strs = [k + '(' + v + ')' for k, v in kast.atts.items()] + return '[' + ', '.join(att_strs) + ']' if type(kast) is KImport: return ' '.join(['imports', ('public' if kast.public else 'private'), kast.name]) if type(kast) is KFlatModule: @@ -262,7 +262,7 @@ def paren(printer): return (lambda *args: '( ' + printer(*args) + ' )') -def appliedLabelStr(symbol): +def applied_label_str(symbol): return (lambda *args: symbol + ' ( ' + ' , '.join(args) + ' )') From f5e174eafaec5d3a493038e2df56d037a2d9a0eb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 3 Aug 2022 16:28:44 +0000 Subject: [PATCH 5/6] pyk/ktool/kprint: add test of failing sort declaration with an attribute --- pyk/src/pyk/ktool/kprint.py | 11 ++++++----- pyk/src/pyk/tests/test_pretty_print_kast.py | 12 +++++++++++- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 3844bb7affc..609f335f187 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -151,12 +151,13 @@ def pretty_print_kast(kast: KAst, symbol_table: SymbolTable, debug=False): if type(kast) is KProduction: if 'klabel' not in kast.att and kast.klabel: kast = kast.update_atts({'klabel': kast.klabel.name}) - sort_str = pretty_print_kast(kast.sort, symbol_table, debug=debug) - if not kast.items: - return 'syntax ' + sort_str - production_str = ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) + syntax_str = 'syntax ' + pretty_print_kast(kast.sort, symbol_table, debug=debug) + if kast.items: + syntax_str += ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) - return 'syntax ' + sort_str + ' ::= ' + production_str + ' ' + att_str + if att_str: + syntax_str += ' ' + att_str + return syntax_str if type(kast) is KSyntaxSort: sort_str = pretty_print_kast(kast.sort, symbol_table, debug=debug) att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) diff --git a/pyk/src/pyk/tests/test_pretty_print_kast.py b/pyk/src/pyk/tests/test_pretty_print_kast.py index f62171c6686..06948974f7b 100644 --- a/pyk/src/pyk/tests/test_pretty_print_kast.py +++ b/pyk/src/pyk/tests/test_pretty_print_kast.py @@ -1,7 +1,16 @@ from typing import Final, Tuple from unittest import TestCase -from pyk.kast import KApply, KAst, KLabel, KProduction, KRule, KSort, KTerminal +from pyk.kast import ( + KApply, + KAst, + KAtt, + KLabel, + KProduction, + KRule, + KSort, + KTerminal, +) from pyk.ktool.kprint import ( SymbolTable, pretty_print_kast, @@ -18,6 +27,7 @@ class PrettyPrintKastTest(TestCase): (KRule(Bool.true, ensures=Bool.true), 'rule true\n '), (KRule(Bool.true, ensures=KApply('_andBool_', [Bool.true, Bool.true])), 'rule true\n ensures ( true\n andBool ( true\n ))\n '), (KProduction(KSort('Test')), 'syntax Test'), + (KProduction(KSort('Test'), att=KAtt({'token': ''})), 'syntax Test [token()]'), ) SYMBOL_TABLE: Final[SymbolTable] = {} From de1d12a1bb9107601a90e73372cb6ddaf0a5ef4c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Aug 2022 17:02:12 +0000 Subject: [PATCH 6/6] pyk/kprint: another test of unparsing productions --- pyk/src/pyk/ktool/kprint.py | 2 +- pyk/src/pyk/tests/test_pretty_print_kast.py | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 609f335f187..2aab48568df 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -153,7 +153,7 @@ def pretty_print_kast(kast: KAst, symbol_table: SymbolTable, debug=False): kast = kast.update_atts({'klabel': kast.klabel.name}) syntax_str = 'syntax ' + pretty_print_kast(kast.sort, symbol_table, debug=debug) if kast.items: - syntax_str += ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) + syntax_str += ' ::= ' + ' '.join([pretty_print_kast(pi, symbol_table, debug=debug) for pi in kast.items]) att_str = pretty_print_kast(kast.att, symbol_table, debug=debug) if att_str: syntax_str += ' ' + att_str diff --git a/pyk/src/pyk/tests/test_pretty_print_kast.py b/pyk/src/pyk/tests/test_pretty_print_kast.py index 06948974f7b..13cc7ce1447 100644 --- a/pyk/src/pyk/tests/test_pretty_print_kast.py +++ b/pyk/src/pyk/tests/test_pretty_print_kast.py @@ -6,6 +6,7 @@ KAst, KAtt, KLabel, + KNonTerminal, KProduction, KRule, KSort, @@ -28,6 +29,7 @@ class PrettyPrintKastTest(TestCase): (KRule(Bool.true, ensures=KApply('_andBool_', [Bool.true, Bool.true])), 'rule true\n ensures ( true\n andBool ( true\n ))\n '), (KProduction(KSort('Test')), 'syntax Test'), (KProduction(KSort('Test'), att=KAtt({'token': ''})), 'syntax Test [token()]'), + (KProduction(KSort('Test'), [KTerminal('foo'), KNonTerminal(KSort('Int'))], att=KAtt({'function': ''})), 'syntax Test ::= "foo" Int [function()]'), ) SYMBOL_TABLE: Final[SymbolTable] = {}