[NOMERGE] Test CI

README.md

@@ -356,3 +356,5 @@ of artifacts, you can run `mvn dependency:purge-local-repository`.
 If tests fail but you want to run the build anyway to see what happens, you can use `mvn package -DskipTests`.
 
 If you still cannot build, please contact a K developer.
+test
+test

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

@@ -1331,7 +1331,7 @@ def prettyPrintKast(kast, symbolTable, debug=False):
         imports = '\n'.join([prettyPrintKast(kimport, symbolTable, debug=debug) for kimport in kast.imports])
         sentences = '\n\n'.join([prettyPrintKast(sentence, symbolTable, debug=debug) for sentence in kast.sentences])
         contents = imports + '\n\n' + sentences
-        return 'module ' + name + '\n    ' + '\n    '.join(contents.split('\n')) + '\nendmodule'
+        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:

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

@@ -311,13 +311,12 @@ def collapseDots(kast):
     """
     def _collapseDots(_kast):
         if type(_kast) is KApply:
-            args = _kast.args
-            if _kast.is_cell and _kast.arity == 1 and args[0] == ktokenDots:
+            if _kast.is_cell and _kast.arity == 1 and _kast.args[0] == ktokenDots:
                 return ktokenDots
-            newArgs = [arg for arg in args if arg != ktokenDots]
-            if _kast.is_cell and _kast.arity == 0:
+            newArgs = [arg for arg in _kast.args if arg != ktokenDots]
+            if _kast.is_cell and len(newArgs) == 0:
                 return ktokenDots
-            if len(newArgs) < len(args):
+            if len(newArgs) < len(_kast.args):
                 newArgs.append(ktokenDots)
             return _kast.let(args=newArgs)
         elif type(_kast) is KRewrite:
@@ -529,7 +528,7 @@ def removeGeneratedCells(constrainedTerm):
     -   Input: Constrained term which contains <generatedTop> and <generatedCounter>.
     -   Output: Constrained term with those cells removed.
     """
-    rule = KApply('<generatedTop>', [KVariable('CONFIG'), KApply('<generatedCounter>', [KVariable('_')])]), KVariable('CONFIG')
+    rule = KApply('<generatedTop>', [KVariable('CONFIG'), KVariable('_')]), KVariable('CONFIG')
     return rewriteAnywhereWith(rule, constrainedTerm)
 
 
@@ -561,7 +560,7 @@ def setCell(constrainedTerm, cellVariable, cellValue):
 def structurallyFrameKCell(constrainedTerm):
     kCell = getCell(constrainedTerm, 'K_CELL')
     if type(kCell) is KSequence and kCell.arity > 0 and isAnonVariable(kCell.items[-1]):
-        kCell = KSequence(kCell.items[0:-1] + [ktokenDots])
+        kCell = KSequence(kCell.items[0:-1] + (ktokenDots,))
     return setCell(constrainedTerm, 'K_CELL', kCell)
 
 

k-distribution/tests/pyk/Makefile

@@ -37,7 +37,9 @@ VENV     := venv/pyvenv.cfg
 ACTIVATE := . venv/bin/activate
 
 $(VENV):
-	virtualenv -p python3.8 venv && $(ACTIVATE) && pip install -e $(K_LIB)/pyk
+	   virtualenv --python python3.8 --pip 22.0.4 venv \
+	&& $(ACTIVATE)                                     \
+	&& pip install --editable $(K_LIB)/pyk
 
 # Tests
 
@@ -61,12 +63,9 @@ test-kpyk-minimize-term: imp-verification/haskell.kompiled $(VENV)
 
 FILE_DEPS =
 
-pytests = defn_test.py           \
-          emit_json_spec_test.py \
-          parse_kast_test.py     \
-          simple_proofs_test.py  \
-          unit_test.py
+pytests = $(wildcard *_test.py)
 
+configuration_test.py.pytest:  FILE_DEPS = imp-verification/haskell.kompiled
 defn_test.py.pytest:           FILE_DEPS = imp-verification/haskell.kompiled
 emit_json_spec_test.py.pytest: FILE_DEPS = imp-verification/looping-spec.json.json-spec
 parse_kast_test.py.pytest:     FILE_DEPS = contextual-function/haskell.kompiled \

k-distribution/tests/pyk/configuration_test.py

@@ -0,0 +1,76 @@
+from abc import ABC
+from unittest import TestCase
+
+from pyk.kast import (
+    KApply,
+    KDefinition,
+    KSequence,
+    KVariable,
+    ktokenDots,
+    readKastTerm,
+)
+from pyk.kastManip import (
+    collapseDots,
+    removeGeneratedCells,
+    structurallyFrameKCell,
+    substitute,
+)
+
+
+class ConfigurationTest(TestCase, ABC):
+    COMPILED_JSON_PATH = 'definitions/imp-verification/haskell/imp-verification-kompiled/compiled.json'
+    MODULE_NAME = 'IMP-VERIFICATION'
+
+    K_CELL = KApply('<k>', [KSequence([KVariable('S1'), KVariable('_DotVar0')])])
+    T_CELL = KApply('<T>', [K_CELL, KApply('<state>', [KVariable('MAP')])])
+    GENERATED_COUNTER_CELL = KApply('<generatedCounter>', [KVariable('X')])
+    GENERATED_TOP_CELL_1 = KApply('<generatedTop>', [T_CELL, KVariable('_GENERATED_COUNTER_PLACEHOLDER')])
+    GENERATED_TOP_CELL_2 = KApply('<generatedTop>', [T_CELL, GENERATED_COUNTER_CELL])
+
+    def setUp(self):
+        self.definition = readKastTerm(self.COMPILED_JSON_PATH)
+        self.assertIsInstance(self.definition, KDefinition)
+
+
+class StructurallyFrameKCellTest(ConfigurationTest):
+
+    def test(self):
+        # Given
+        config_expected = substitute(self.GENERATED_TOP_CELL_1, {'_DotVar0': ktokenDots})
+
+        # When
+        config_actual = structurallyFrameKCell(self.GENERATED_TOP_CELL_1)
+
+        # Then
+        self.assertEqual(config_actual, config_expected)
+
+
+class RemoveGeneratedCounterTest(ConfigurationTest):
+
+    def test_first(self):
+        # When
+        config_actual = removeGeneratedCells(self.GENERATED_TOP_CELL_1)
+
+        # Then
+        self.assertEqual(config_actual, self.T_CELL)
+
+    def test_second(self):
+        # When
+        config_actual = removeGeneratedCells(self.GENERATED_TOP_CELL_2)
+
+        # Then
+        self.assertEqual(config_actual, self.T_CELL)
+
+
+class CollapseDotsTest(ConfigurationTest):
+
+    def test(self):
+        # Given
+        config_before = substitute(self.T_CELL, {'MAP': ktokenDots})
+        config_expected = KApply('<T>', [self.K_CELL, ktokenDots])
+
+        # When
+        config_actual = collapseDots(config_before)
+
+        # Then
+        self.assertEqual(config_actual, config_expected)