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

Allow introducing semantic rules in kprove #4772

Open
wants to merge 3 commits into
base: develop
Choose a base branch
from
Open

Allow introducing semantic rules in kprove #4772

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3fd012e
k-frontend/{Kompile,KProveOptions,ProofDefinitionBuilder}: allow the …
ehildenb Mar 15, 2025
222394c
pyk/kprove: make sure to allow new rules when parsing K modules
ehildenb Mar 15, 2025
ea7feb6
Merge branch 'develop' into allow-new-rules-kprove
ehildenb Mar 20, 2025
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
4 changes: 2 additions & 2 deletions k-frontend/src/main/java/org/kframework/kompile/Kompile.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -539,7 +539,7 @@ public void definitionChecks(Set<Module> modules) {
}

// Extra checks just for the prover specification.
public void proverChecksX(Module specModule, Module mainDefModule) {
public void proverChecksX(Module specModule, Module mainDefModule, boolean allowRules) {
// check rogue syntax in spec module
Set<Sentence> toCheck = mutable(specModule.sentences().$minus$minus(mainDefModule.sentences()));
for (Sentence s : toCheck)
Expand All @@ -558,7 +558,7 @@ public void proverChecksX(Module specModule, Module mainDefModule) {
if (m.name().equals(mainDefModule.name())
|| mainDefModule.importedModuleNames().contains(m.name())) return s;
if (!(s instanceof Claim || s.isSyntax())) {
if (s instanceof Rule && !s.att().contains(Att.SIMPLIFICATION()))
if (s instanceof Rule && !allowRules && !s.att().contains(Att.SIMPLIFICATION()))
errors.add(
KEMException.compilerError(
"Only claims and simplification rules are allowed in proof modules.", s));
Expand Down
6 changes: 6 additions & 0 deletions k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,4 +113,10 @@ public synchronized File specFile(FileUtil files) {
description = "Allow functional claims to be printed in kore format. Use with --dry-run.",
hidden = true)
public boolean allowFuncClaims = false;

@Parameter(
names = "--allow-new-rules",
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd just call it --allow-rules to make it shorter.

description = "Allow new rules to be introduced in proof modules. Use with --dry-run.",
hidden = true)
public boolean allowNewRules = false;
}
3 changes: 2 additions & 1 deletion k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,8 @@ public Tuple2<Definition, Module> build(File specFile, String specModuleName) {
Definition parsedDefinition = compiledDefinition.getParsedDefinition();
Module specModule = getModule(specModuleNameUpdated, modulesMap, parsedDefinition);
specModule = filter(specModule);
kompile.proverChecksX(specModule, modulesMap.get(defModuleNameUpdated));
kompile.proverChecksX(
specModule, modulesMap.get(defModuleNameUpdated), proveOptions.allowNewRules);
kompile.structuralChecks(
immutable(modules), specModule, Option.empty(), backend.excludedModuleTags());
specModule =
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/pyk/ktool/kprove.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ def parse_modules(
temp_dir=self.use_directory,
dry_run=True,
type_inference_mode=type_inference_mode,
args=['--emit-json-spec', ntf.name],
args=['--emit-json-spec', ntf.name, '--allow-new-rules'],
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider adding an integration test.

)
json_data = json.loads(Path(ntf.name).read_text())

Expand Down
Loading