Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change type of KToken.sort from str to KSort in pyk.kast #2609

Merged
merged 4 commits into from
May 18, 2022
Merged

Change type of KToken.sort from str to KSort in pyk.kast #2609

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1a950eb
Change type of KToken.sort from str to KSort
tothtamas28 May 18, 2022
7249f55
Accept str as sort in KToken constructor
tothtamas28 May 18, 2022
5dff92d
Accept str as sort in KProduction constructor
tothtamas28 May 18, 2022
bf659be
Merge branch 'master' into pyk-ktoken-sort
rv-jenkins May 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion pyk/src/pyk/integration_tests/test_defn.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
KApply,
KClaim,
KRewrite,
KSort,
KToken,
KVariable,
assocWithUnit,
Expand All @@ -28,7 +29,7 @@ def _update_symbol_table(symbol_table):

def test_print_configuration(self):
# Given
config = KApply('<T>', [KApply('<k>', [KApply('int_;_', [KApply('_,_', [KToken('x', 'Id'), KApply('_,_', [KToken('y', 'Id'), KApply('.List{"_,_"}')])])])]), KApply('<state>', [KApply('.Map')])])
config = KApply('<T>', [KApply('<k>', [KApply('int_;_', [KApply('_,_', [KToken('x', KSort('Id')), KApply('_,_', [KToken('y', KSort('Id')), KApply('.List{"_,_"}')])])])]), KApply('<state>', [KApply('.Map')])])
config_expected = '\n'.join([ '<T>' # noqa
, ' <k>' # noqa
, ' int x , y ;' # noqa
Expand Down
6 changes: 3 additions & 3 deletions pyk/src/pyk/integration_tests/test_proofs.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
from ..kast import KAtt, KClaim, KRule, KToken
from ..kast import BOOL, KAtt, KClaim, KRule, KSort, KToken
from ..ktool import KompileBackend
from .kprove_test import KProveTest

Expand All @@ -17,8 +17,8 @@ def _update_symbol_table(symbol_table):

def test_prove_claim_with_lemmas(self):
# Given
new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''}))
new_claim = KClaim(KToken('<k> foo => bar ... </k> <state> 3 |-> 3 </state>', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool'))
new_lemma = KRule(KToken('pred1(3) => true', BOOL), requires=KToken('pred1(4)', BOOL), att=KAtt(atts={'simplification': ''}))
new_claim = KClaim(KToken('<k> foo => bar ... </k> <state> 3 |-> 3 </state>', KSort('TCellFragment')), requires=KToken('pred1(4)', BOOL))

# When
result1 = self.kprove.proveClaim(new_claim, 'claim-without-lemma')
Expand Down
18 changes: 9 additions & 9 deletions pyk/src/pyk/kast.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,23 +276,23 @@ def match(self, term: KInner) -> Optional[Subst]:
@dataclass(frozen=True)
class KToken(KInner):
token: str
sort: str
sort: KSort

def __init__(self, token: str, sort: str):
def __init__(self, token: str, sort: KSort):
tothtamas28 marked this conversation as resolved.
Show resolved Hide resolved
object.__setattr__(self, 'token', token)
object.__setattr__(self, 'sort', sort)

@classmethod
def from_dict(cls: Type['KToken'], d: Dict[str, Any]) -> 'KToken':
cls._check_node(d)
return KToken(token=d['token'], sort=d['sort'])
return KToken(token=d['token'], sort=KSort(d['sort']))

def to_dict(self) -> Dict[str, Any]:
return {'node': 'KToken', 'token': self.token, 'sort': self.sort}
return {'node': 'KToken', 'token': self.token, 'sort': self.sort.name}

def let(self, *, token: Optional[str] = None, sort: Optional[str] = None) -> 'KToken':
def let(self, *, token: Optional[str] = None, sort: Optional[KSort] = None) -> 'KToken':
token = token if token is not None else self.token
sort = sort if sort is not None else self.sort
sort = sort if sort else self.sort
return KToken(token=token, sort=sort)

def map_inner(self: 'KToken', f: Callable[[KInner], KInner]) -> 'KToken':
Expand All @@ -304,8 +304,8 @@ def match(self, term: KInner) -> Optional[Subst]:
return None


TRUE = KToken('true', 'Bool')
FALSE = KToken('false', 'Bool')
TRUE = KToken('true', BOOL)
FALSE = KToken('false', BOOL)


@final
Expand Down Expand Up @@ -1279,7 +1279,7 @@ def flattenLabel(label, kast):

klabelCells = '#KCells'
klabelEmptyK = '#EmptyK'
ktokenDots = KToken('...', 'K')
ktokenDots = KToken('...', KSort('K'))


def constLabel(symbol):
Expand Down
38 changes: 20 additions & 18 deletions pyk/src/pyk/kastManip.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@

from .cli_utils import fatal
from .kast import (
FALSE,
TRUE,
KApply,
KAtt,
KClaim,
Expand Down Expand Up @@ -96,8 +98,8 @@ def unsafeMlPredToBool(k):
"""
if k is None:
return None
mlPredToBoolRules = [ (KApply('#Top') , KToken('true' , 'Bool')) # noqa
, (KApply('#Bottom') , KToken('false' , 'Bool')) # noqa
mlPredToBoolRules = [ (KApply('#Top') , TRUE) # noqa
, (KApply('#Bottom') , FALSE) # noqa
, (KApply('#And' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_andBool_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('#Or' , [KVariable('#V1'), KVariable('#V2')]) , KApply('_orBool_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('#Not' , [KVariable('#V1')]) , KApply('notBool_' , [KVariable('#V1')])) # noqa
Expand All @@ -114,24 +116,24 @@ def unsafeMlPredToBool(k):
def simplifyBool(k):
if k is None:
return None
simplifyRules = [ (KApply('_==K_', [KVariable('#LHS'), KToken('true', 'Bool')]), KVariable('#LHS')) # noqa
, (KApply('_==K_', [KToken('true', 'Bool'), KVariable('#RHS')]), KVariable('#RHS')) # noqa
, (KApply('_==K_', [KVariable('#LHS'), KToken('false', 'Bool')]), KApply('notBool_', [KVariable('#LHS')])) # noqa
, (KApply('_==K_', [KToken('false', 'Bool'), KVariable('#RHS')]), KApply('notBool_', [KVariable('#RHS')])) # noqa
, (KApply('notBool_', [KToken('false' , 'Bool')]), KToken('true' , 'Bool')) # noqa
, (KApply('notBool_', [KToken('true' , 'Bool')]), KToken('false' , 'Bool')) # noqa
simplifyRules = [ (KApply('_==K_', [KVariable('#LHS'), TRUE]), KVariable('#LHS')) # noqa
, (KApply('_==K_', [TRUE, KVariable('#RHS')]), KVariable('#RHS')) # noqa
, (KApply('_==K_', [KVariable('#LHS'), FALSE]), KApply('notBool_', [KVariable('#LHS')])) # noqa
, (KApply('_==K_', [FALSE, KVariable('#RHS')]), KApply('notBool_', [KVariable('#RHS')])) # noqa
, (KApply('notBool_', [FALSE]), TRUE) # noqa
, (KApply('notBool_', [TRUE]), FALSE) # noqa
, (KApply('notBool_', [KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_=/=K_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==K_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('notBool_', [KApply('_=/=Int_' , [KVariable('#V1'), KVariable('#V2')])]), KApply('_==Int_' , [KVariable('#V1'), KVariable('#V2')])) # noqa
, (KApply('_andBool_', [KToken('true', 'Bool'), KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KToken('false', 'Bool')) # noqa
, (KApply('_andBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KToken('false', 'Bool')) # noqa
, (KApply('_orBool_', [KToken('false', 'Bool'), KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [KVariable('#REST'), KToken('false', 'Bool')]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [KToken('true', 'Bool'), KVariable('#REST')]), KToken('true', 'Bool')) # noqa
, (KApply('_orBool_', [KVariable('#REST'), KToken('true', 'Bool')]), KToken('true', 'Bool')) # noqa
, (KApply('_andBool_', [TRUE, KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [KVariable('#REST'), TRUE]), KVariable('#REST')) # noqa
, (KApply('_andBool_', [FALSE, KVariable('#REST')]), FALSE) # noqa
, (KApply('_andBool_', [KVariable('#REST'), FALSE]), FALSE) # noqa
, (KApply('_orBool_', [FALSE, KVariable('#REST')]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [KVariable('#REST'), FALSE]), KVariable('#REST')) # noqa
, (KApply('_orBool_', [TRUE, KVariable('#REST')]), TRUE) # noqa
, (KApply('_orBool_', [KVariable('#REST'), TRUE]), TRUE) # noqa
] # noqa
newK = k
for rule in simplifyRules:
Expand Down Expand Up @@ -496,10 +498,10 @@ def minimizeRule(rule, keepVars=[]):
ruleRequires = rule.requires
ruleEnsures = rule.ensures

ruleRequires = buildAssoc(KToken('true', 'Bool'), '_andBool_', unique(flattenLabel('_andBool_', ruleRequires)))
ruleRequires = buildAssoc(TRUE, '_andBool_', unique(flattenLabel('_andBool_', ruleRequires)))
ruleRequires = simplifyBool(ruleRequires)

ruleEnsures = buildAssoc(KToken('true', 'Bool'), '_andBool_', unique(flattenLabel('_andBool_', ruleEnsures)))
ruleEnsures = buildAssoc(TRUE, '_andBool_', unique(flattenLabel('_andBool_', ruleEnsures)))
ruleEnsures = simplifyBool(ruleEnsures)

constrainedVars = [] if keepVars is None else keepVars
Expand Down
10 changes: 5 additions & 5 deletions pyk/src/pyk/prelude.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
from typing import Iterable, Union

from .kast import BOTTOM, TOP, KApply, KInner, KToken
from .kast import BOOL, BOTTOM, INT, STRING, TOP, TRUE, KApply, KInner, KToken


def buildAssoc(unit: KInner, join: str, ls: Iterable[KInner]) -> KInner:
Expand Down Expand Up @@ -41,15 +41,15 @@ def token(x: Union[bool, int, str]) -> KToken:


def boolToken(b: bool) -> KToken:
return KToken('true' if b else 'false', 'Bool')
return KToken('true' if b else 'false', BOOL)


def intToken(i: int) -> KToken:
return KToken(str(i), 'Int')
return KToken(str(i), INT)


def stringToken(s: str) -> KToken:
return KToken(f'"{s}"', 'String')
return KToken(f'"{s}"', STRING)


def ltInt(i1, i2):
Expand All @@ -65,7 +65,7 @@ def mlEquals(a1, a2):


def mlEqualsTrue(b):
return mlEquals(boolToken(True), b)
return mlEquals(TRUE, b)


def mlTop():
Expand Down
4 changes: 2 additions & 2 deletions pyk/src/pyk/tests/test_subst.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,14 @@
from typing import Dict, Final, Tuple
from unittest import TestCase

from ..kast import KApply, KInner, KToken, KVariable, Subst
from ..kast import INT, KApply, KInner, KToken, KVariable, Subst
from ..kastManip import extract_subst
from ..prelude import mlAnd, mlEquals, mlEqualsTrue, mlTop

a, b, c = (KApply(label) for label in ['a', 'b', 'c'])
x, y, z = (KVariable(name) for name in ['x', 'y', 'z'])
f, g, h = (partial(KApply.of, label) for label in ['f', 'g', 'h'])
t = KToken('t', 'Int')
t = KToken('t', INT)


def int_eq(term1: KInner, term2: KInner) -> KApply:
Expand Down