Refactor pyk AST functions into classes

k-distribution/src/main/scripts/lib/.mypy.ini

@@ -0,0 +1,4 @@
+[mypy]
+
+[mypy-graphviz.*]
+ignore_missing_imports = True

k-distribution/src/main/scripts/lib/Makefile

@@ -1,16 +1,17 @@
-.PHONY: all test test-code-style test-flake8 test-isort isort
+.PHONY: all check-code-style isort check-isort check-flake8 test-mypy 
 
-all: test
+all: check-code-style
 
-test: test-code-style
+check-code-style: check-isort check-flake8 check-mypy
 
-test-code-style: test-flake8 test-isort
+isort:
+	isort ./pyk
 
-test-flake8:
-	flake8 . --ignore=E501
+check-isort:
+	isort ./pyk --check
 
-test-isort:
-	isort . --check
+check-flake8:
+	flake8 ./pyk --ignore=E501
 
-isort:
-	isort .
+check-mypy:
+	mypy ./pyk

k-distribution/src/main/scripts/lib/pyk/__main__.py

@@ -1,5 +1,4 @@
 import argparse
-import json
 import os.path as path
 import sys
 from pathlib import Path
@@ -10,7 +9,7 @@
 from .coverage import getRuleById, stripCoverageLogger
 from .kast import (
     KApply,
-    KConstant,
+    KAst,
     buildSymbolTable,
     flattenLabel,
     prettyPrintKast,
@@ -24,7 +23,7 @@
     splitConfigAndConstraints,
 )
 from .ktool import KPrint, KProve
-from .prelude import buildAssoc
+from .prelude import buildAssoc, mlBottom, mlTop
 
 pykArgs = argparse.ArgumentParser()
 pykArgs.add_argument('kompiled-dir', type=str, help='Kompiled directory for definition.')
@@ -63,10 +62,10 @@ def main(commandLineArgs, extraMain=None):
 
     if args['command'] == 'print':
         printer = KPrint(kompiled_dir)
-        term = json.loads(args['term'].read())
-        if 'term' in term:
+        term = KAst.from_json(args['term'].read())
+        if type(term) is dict and 'term' in term:
             term = term['term']
-        if term == KConstant('#Top'):
+        if term == mlTop():
             args['output_file'].write(printer.prettyPrint(term))
         else:
             if args['minimize']:
@@ -75,30 +74,30 @@ def main(commandLineArgs, extraMain=None):
                 for d in flattenLabel('#Or', term):
                     dMinimized = minimizeTerm(d, abstractLabels=abstractLabels)
                     dConfig, dConstraint = splitConfigAndConstraints(dMinimized)
-                    if dConstraint != KConstant('#Top'):
+                    if dConstraint != mlTop():
                         minimizedDisjuncts.append(KApply('#And', [dConfig, dConstraint]))
                     else:
                         minimizedDisjuncts.append(dConfig)
-                term = propagateUpConstraints(buildAssoc(KConstant('#Bottom'), '#Or', minimizedDisjuncts))
+                term = propagateUpConstraints(buildAssoc(mlBottom(), '#Or', minimizedDisjuncts))
             args['output_file'].write(printer.prettyPrint(term))
 
     elif args['command'] == 'prove':
         kprover = KProve(kompiled_dir, args['main-file'])
         finalState = kprover.prove(Path(args['spec-file']), args['spec-module'], args=args['kArgs'])
-        args['output_file'].write(json.dumps(finalState))
-        if finalState != KConstant('#Top'):
+        args['output_file'].write(finalState.to_json())
+        if finalState != mlTop():
             warning('Proof failed!')
 
     elif args['command'] == 'graph-imports':
         kprinter = KPrint(kompiled_dir)
         kDefn = kprinter.definition
         importGraph = Digraph()
         graphFile = kompiled_dir / 'import-graph'
-        for module in kDefn['modules']:
-            modName = module['name']
+        for module in kDefn.modules:
+            modName = module.name
             importGraph.node(modName)
-            for moduleImport in module['imports']:
-                importGraph.edge(modName, moduleImport['name'])
+            for moduleImport in module.imports:
+                importGraph.edge(modName, moduleImport.name)
         importGraph.render(graphFile)
         notif('Wrote file: ' + str(graphFile))
 

k-distribution/src/main/scripts/lib/pyk/coverage.py

@@ -1,13 +1,5 @@
 from .cli_utils import fatal
-from .kast import (
-    KRewrite,
-    KRule,
-    isKApply,
-    isKRewrite,
-    isKRule,
-    isKSequence,
-    readKastTerm,
-)
+from .kast import KApply, KRewrite, KRule, KSequence, readKastTerm
 
 
 def getRuleById(definition, rule_id):
@@ -21,29 +13,24 @@ def getRuleById(definition, rule_id):
     Output: json encoded rule which has identifier rule_id.
     """
 
-    for module in definition['modules']:
-        for sentence in module['localSentences']:
-            if isKRule(sentence) and 'att' in sentence:
-                atts = sentence['att']['att']
-                if 'UNIQUE_ID' in atts and atts['UNIQUE_ID'] == rule_id:
+    for module in definition.modules:
+        for sentence in module.sentences:
+            if type(sentence) is KRule:
+                if 'UNIQUE_ID' in sentence.att and sentence.att['UNIQUE_ID'] == rule_id:
                     return sentence
     fatal('Could not find rule with ID: ' + rule_id)
 
 
-def stripCoverageLogger(rule):
-    ruleBody = rule['body']
-    ruleRequires = rule['requires']
-    ruleEnsures = rule['ensures']
-    ruleAtts = rule['att']
-
-    if isKRewrite(ruleBody):
-        ruleLHS = ruleBody['lhs']
-        ruleRHS = ruleBody['rhs']
-        if isKApply(ruleRHS) and ruleRHS['label'].startswith('project:'):
-            ruleRHSseq = ruleRHS['args'][0]
-            if isKSequence(ruleRHSseq) and len(ruleRHSseq['items']) == 2:
-                ruleBody = KRewrite(ruleLHS, ruleRHSseq['items'][1])
-    return KRule(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtts)
+def stripCoverageLogger(rule: KRule):
+    ruleBody = rule.body
+    if type(ruleBody) is KRewrite:
+        ruleLHS = ruleBody.lhs
+        ruleRHS = ruleBody.rhs
+        if type(ruleRHS) is KApply and ruleRHS.label.startswith('project:'):
+            ruleRHSseq = ruleRHS.args[0]
+            if type(ruleRHSseq) is KSequence and ruleRHSseq.arity == 2:
+                ruleBody = KRewrite(ruleLHS, ruleRHSseq.items[1])
+    return rule.let(body=ruleBody)
 
 
 def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_list):
@@ -77,15 +64,14 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li
 
     # Filter out non-functional rules from rule map (determining if they are functional via the top symbol in the rule being `<generatedTop>`)
     dst_non_function_rules = []
-    for module in dst_definition['modules']:
-        for sentence in module['localSentences']:
-            if isKRule(sentence):
-                ruleBody = sentence['body']
-                ruleAtt = sentence['att']['att']
-                if (isKApply(ruleBody) and ruleBody['label'] == '<generatedTop>') \
-                        or (isKRewrite(ruleBody) and isKApply(ruleBody['lhs']) and ruleBody['lhs']['label'] == '<generatedTop>'):
-                    if 'UNIQUE_ID' in ruleAtt:
-                        dst_non_function_rules.append(ruleAtt['UNIQUE_ID'])
+    for module in dst_definition.modules:
+        for sentence in module.sentences:
+            if type(sentence) is KRule:
+                ruleBody = sentence.body
+                if (type(ruleBody) is KApply and ruleBody.label == '<generatedTop>') \
+                        or (type(ruleBody) is KRewrite and type(ruleBody.lhs) is KApply and ruleBody.lhs.label == '<generatedTop>'):
+                    if 'UNIQUE_ID' in sentence.att:
+                        dst_non_function_rules.append(sentence.att['UNIQUE_ID'])
 
     # Convert the src_coverage rules to dst_no_coverage rules via the maps generated above
     dst_rule_list = []