Skip to content

Minor refactor of Matcher + Pstate and move Combinators around#385

Open
giltho wants to merge 3 commits into
masterfrom
extract-preds-3
Open

Minor refactor of Matcher + Pstate and move Combinators around#385
giltho wants to merge 3 commits into
masterfrom
extract-preds-3

Conversation

@giltho

@giltho giltho commented Jul 4, 2026

Copy link
Copy Markdown
Contributor

Again, easier reviewed commit by commit

  • Remove unused functions from the interface of Matcher
  • Extract functions from matcher into a Pred_state module
  • move Combinators into GillianCore. This last move will be needed when I remove PState.ml and make user-defined predicate a combinators. We'll then need the predicate combinator to define Verify.ml which will call LogicPreprocessing

@giltho giltho changed the title remove a bunch of useless things Minor refactor of Matcher + Pstate and move Combinators around Jul 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant