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

Generate function definitions #4753

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

Generate function definitions #4753

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
c02ab7f
Assign a `UNIQUE_ID` to map cell simplifcation rules
tothtamas28 Feb 7, 2025
cf1a629
Add attributes `uid` and `label` to `Rule`
tothtamas28 Jan 27, 2025
a0e29ea
Fix `project_to_symbols`
tothtamas28 Feb 6, 2025
6c908d7
Fix `ByteArray` literal syntax
tothtamas28 Feb 6, 2025
4fba219
Generalize `_rewrite_name` to `_rule_name`
tothtamas28 Jan 27, 2025
7a9f02a
Rename function `_sort_sccs` to `_sccs`
tothtamas28 Feb 5, 2025
7cd9324
Extract function `_ordered_sccs`
tothtamas28 Feb 5, 2025
e57b941
Move identifier methods to top level
tothtamas28 Feb 5, 2025
8e5a32d
Add class `Definition` to `model`
tothtamas28 Feb 3, 2025
12cc68f
Add class `AltsVal` to `model`
tothtamas28 Feb 3, 2025
d4abb24
Rename `_transform_func` to `_func_axiom`
tothtamas28 Feb 3, 2025
d6edf27
Add parameter `concrete` to `_transform_pattern`
tothtamas28 Feb 5, 2025
0ec659f
Do not parenthesize nullary applications
tothtamas28 Feb 6, 2025
23c375b
Generate function definitions
tothtamas28 Feb 5, 2025
8ec666f
Use `<|>` instead of `findSome?` in function definition
tothtamas28 Feb 10, 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
2 changes: 2 additions & 0 deletions k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@
import org.kframework.compile.AddSortInjections;
import org.kframework.compile.ComputeTransitiveFunctionDependencies;
import org.kframework.compile.ExpandMacros;
import org.kframework.compile.NumberSentences;
import org.kframework.compile.RefreshRules;
import org.kframework.compile.RewriteToTop;
import org.kframework.definition.Claim;
Expand Down Expand Up @@ -723,6 +724,7 @@ private void genMapCeilAxioms(Production prod, Collection<Rule> rules) {
BooleanUtils.TRUE,
BooleanUtils.TRUE,
Att.empty().add(Att.SIMPLIFICATION()));
ceilMapRule = (Rule) NumberSentences.number(ceilMapRule);
rules.add(ceilMapRule);
}

Expand Down
4 changes: 2 additions & 2 deletions pyk/src/pyk/klean/generate.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,9 @@ def generate(
k2lean4 = K2Lean4(defn)
genmodel = {
'Sorts': (k2lean4.sort_module, ['Prelude']),
'Func': (k2lean4.func_module, ['Sorts']),
'Inj': (k2lean4.inj_module, ['Sorts']),
'Rewrite': (k2lean4.rewrite_module, ['Func', 'Inj']),
'Func': (k2lean4.func_module, ['Inj']),
'Rewrite': (k2lean4.rewrite_module, ['Func']),
}

modules = _gen_modules(context['library_name'], genmodel)
Expand Down
Loading
Loading