Skip to content
New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom

Architecture of pyk #2447

Closed
ehildenb opened this issue Feb 18, 2022 · 0 comments · Fixed by #2448
Closed

Architecture of pyk #2447

ehildenb opened this issue Feb 18, 2022 · 0 comments · Fixed by #2448
Assignees
@tothtamas28
Labels
refactor

Comments

@ehildenb
Copy link
Member

ehildenb commented Feb 18, 2022 •
edited
Loading

Currently the architecture of pyk is:

  • File kast.py:
    • Defines JSON data-structures of KAST.
    • Defines pretty-printer for KAST.
    • No error-checking anywhere.
  • File kastManip.py:
    • Flat list of functions.
    • Mostly functions which do manipulations on KAST terms (specifically inner terms), eg match, rewriteWith, etc...

Proposed structure:

  • Abstract class KAST:
    • to_json and from_json required to have implementations
  • Subclass KInner(KAST):
    • Inner syntax of K (for dataclasses like KApply(KInner), KToken(KInner), etc...)
    • Provides functions like match, so you can do things like this.match(that), or this.rewriteWith(KRewrite).
  • Subclass KOuter(KAST):
    • Outer syntax of K (for dataclasses like KFlatModule(KOuter), KImport(KOuter), KProduction(KOuter), etc...)
    • Potential to have much better validation at construction time using types (catch errors sooner).
    • Subclass KDefinition(KOuter):
      • Holds methods like buildSymbolTable and prettyPrint.

Anything that doesn't fit in this class structure can stay as flat list of functions in some file somewhere.
@tothtamas28 tothtamas28 mentioned this issue Feb 18, 2022
Merged
@tothtamas28 tothtamas28 self-assigned this Feb 18, 2022
h0nzZik pushed a commit to h0nzZik/k that referenced this issue Nov 24, 2022
@rv-jenkins @ana-pantilie @ttuegel
Update dependency: haskell-backend/src/main/native/haskell-backend (r…
4497600 
…untimeverification#1830)

* haskell-backend/src/main/native/haskell-backend: 79703e11 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 8428df45 - LTS Haskell 17.4

* haskell-backend/src/main/native/haskell-backend: 2e714c56 - Add an EquationVariableName to RewritingVariableName

* haskell-backend/src/main/native/haskell-backend: c5cc46be - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 0c4ad203 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: a182994f - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: 9460590a - Simplify side conditions (runtimeverification#2393)

* haskell-backend/src/main/native/haskell-backend: 4fb83523 - Fix `variable` to `RewritingVariableName` in `Kore.Equation.Application` (runtimeverification#2325)

* haskell-backend/src/main/native/haskell-backend: f41cba23 - Revert "Revert runtimeverification#2315 (runtimeverification#2385)" (runtimeverification#2389)

* haskell-backend/src/main/native/haskell-backend: 44eed8d7 - Run Test workflow on macOS (runtimeverification#2420)

* haskell-backend/src/main/native/haskell-backend: 904f5322 - kore-repl: Print human-readable error messages (runtimeverification#2441)

* haskell-backend/src/main/native/haskell-backend: b49fdd3c - Make Conditional's term a strict field (runtimeverification#2442)

* haskell-backend/src/main/native/haskell-backend: 01f0402d - adding match for And (runtimeverification#2435)

* haskell-backend/src/main/native/haskell-backend: 3243d1e5 - kore-0.41.0.0 (runtimeverification#2444)

* haskell-backend/src/main/native/haskell-backend: 28913344 - Update dependency: deps/k_release

* haskell-backend/src/main/native/haskell-backend: abf0292b - Use unit and element symbol attributes

* haskell-backend/src/main/native/haskell-backend: 7d3ee1bc - Inefficient Equation renaming (runtimeverification#2438)

* haskell-backend/src/main/native/haskell-backend: 95b6c107 - Stop simplifying the left-hand side of equations (runtimeverification#2392)

* haskell-backend/src/main/native/haskell-backend: 21959d95 - Add instructions for running one test in Docker (runtimeverification#2456)

* haskell-backend/src/main/native/haskell-backend: 4195d948 - Removes sort checks for Map and Set during internalization (runtimeverification#2440)

* Predicates in the condition are now simplified

* haskell-backend/src/main/native/haskell-backend: c35bfa56 - Remove defined marker (runtimeverification#2380)

* haskell-backend/src/main/native/haskell-backend: 57ad3292 - Remove cabal.project.freeze (runtimeverification#2450)

* haskell-backend/src/main/native/haskell-backend: 66158c67 - Support the --bug-report and --no-bug-report options in kore-repl (#2462)

* haskell-backend/src/main/native/haskell-backend: f0d93ac5 - Use stderr for errors (runtimeverification#2458)

* haskell-backend/src/main/native/haskell-backend: 0427fae7 - Distinguish \bottom from stuck states (runtimeverification#2451)

* haskell-backend/src/main/native/haskell-backend: d136446e - Fix Strict performance (runtimeverification#2447)

* haskell-backend/src/main/native/haskell-backend: a4e55b2a - Remove IMP fragment tests (runtimeverification#2467)

* haskell-backend/src/main/native/haskell-backend: 1f61e5a6 - Revert PRs related to InternalAc, Unit, Element & Concat symbols changes (runtimeverification#2463)

* haskell-backend/src/main/native/haskell-backend: fcfc2d52 - Remove the EvaluatedF marker from TermLike (runtimeverification#2469)

* haskell-backend/src/main/native/haskell-backend: fb56d719 - Revert PR runtimeverification#2334 (runtimeverification#2473)

* haskell-backend/src/main/native/haskell-backend: bb258f14 - Add ref = "main"; to default.nix (runtimeverification#2475)

* haskell-backend/src/main/native/haskell-backend: 964e64e7 - Update dependency: deps/k_release (runtimeverification#2464)

* haskell-backend/src/main/native/haskell-backend: abf14770 - Emit a warning when kore-exec exceeds the depth limit (runtimeverification#2461)

* haskell-backend/src/main/native/haskell-backend: 003a8424 - Update dependency: deps/k_release (runtimeverification#2478)

* haskell-backend/src/main/native/haskell-backend: 485bd89a - kore-0.42.0.0 (runtimeverification#2477)

* Add definedness to lookup rules, regenerate tests

* haskell-backend/src/main/native/haskell-backend: 78515d10 - Update dependency: deps/k_release (runtimeverification#2486)

* Revert changes to domains.md and test output

* haskell-backend/src/main/native/haskell-backend: 4f3a751c - Format code with fourmolu (runtimeverification#2382)

* haskell-backend/src/main/native/haskell-backend: de80594b - Update dependency: deps/k_release (runtimeverification#2490)

* Update map symbolic Haskell tests

* haskell-backend/src/main/native/haskell-backend: 9c9ef914 - Update dependency: deps/k_release (runtimeverification#2495)

Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com>
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees

@tothtamas28 tothtamas28

Labels
refactor
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Refactor pyk AST functions into classes runtimeverification/k
2 participants
@tothtamas28 @ehildenb