Match disjunction tool #2697

ana-pantilie · 2021-06-24T06:39:45Z

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

…nto match-disjunction-tool

github-actions · 2021-07-26T13:17:01Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.000002	0
test/regression-evm/test-sum-to-n.sh	-0.000004	0
test/regression-evm/test-branching-no-invalid.sh	0.000002	0.000003
test/regression-evm/test-straight-line-no-invalid.sh	0.000002	0.000003
test/regression-evm/test-branching-invalid.sh	0.000029	0.000003
test/regression-evm/test-pop1.sh	-0.000002	-0.000000
test/regression-evm/test-straight-line.sh	0.000002	0.000004
test/regression-evm/test-sumTo10.sh	-0.000000	0.004570
test/regression-wasm/test-locals.sh	-0.000000	-0.000000
test/regression-wasm/test-simple-arithmetic.sh	0.000000	-0.000000
test/regression-wasm/test-wrc20.sh	-0.000014	-0.003687
test/regression-wasm/test-loops.sh	0.000008	0.000000
test/regression-wasm/test-memory.sh	0.000005	0

github-actions · 2021-07-26T13:42:35Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.000002	0
test/regression-evm/test-sum-to-n.sh	-0.000002	0.164189
test/regression-evm/test-branching-no-invalid.sh	0.000002	0.000003
test/regression-evm/test-straight-line-no-invalid.sh	0.000002	0.000003
test/regression-evm/test-branching-invalid.sh	-0.000003	0.000003
test/regression-evm/test-pop1.sh	-0.000002	0
test/regression-evm/test-straight-line.sh	0.000002	0.000003
test/regression-evm/test-sumTo10.sh	0.000000	-0.000001
test/regression-wasm/test-locals.sh	0.000000	-0.000001
test/regression-wasm/test-simple-arithmetic.sh	0.000002	-0.000000
test/regression-wasm/test-wrc20.sh	0.000003	0.001232
test/regression-wasm/test-loops.sh	-0.000021	0.000000
test/regression-wasm/test-memory.sh	-0.000006	0

github-actions · 2021-07-26T15:34:14Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.000001	0
test/regression-evm/test-sum-to-n.sh	0.006927	0
test/regression-evm/test-branching-no-invalid.sh	0.000002	0.000003
test/regression-evm/test-straight-line-no-invalid.sh	0.000003	0.000003
test/regression-evm/test-branching-invalid.sh	-0.000000	0.000003
test/regression-evm/test-pop1.sh	0.000002	0
test/regression-evm/test-straight-line.sh	0.000003	0.000003
test/regression-evm/test-sumTo10.sh	0.000000	0.001799
test/regression-wasm/test-locals.sh	-0.000000	-0.000000
test/regression-wasm/test-simple-arithmetic.sh	0.000629	0
test/regression-wasm/test-wrc20.sh	0.026328	0.001220
test/regression-wasm/test-loops.sh	0.006693	0.000003
test/regression-wasm/test-memory.sh	0.002628	0

github-actions · 2021-08-03T13:52:40Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	0.058523	0
test/regression-evm/test-straight-line.sh	0.061041	0.000003
test/regression-evm/test-straight-line-no-invalid.sh	0.059361	0.000003
test/regression-evm/test-branching-invalid.sh	0.071324	0.000003
test/regression-evm/test-sum-to-n.sh	0.041137	0
test/regression-evm/test-branching-no-invalid.sh	0.070264	0.000003
test/regression-evm/test-add0.sh	0.071492	0
test/regression-evm/test-sumTo10.sh	0.118635	-0.003820
test/regression-wasm/test-memory.sh	0.063726	-0.000167
test/regression-wasm/test-locals.sh	0.066130	-0.000258
test/regression-wasm/test-wrc20.sh	0.051308	-0.004957
test/regression-wasm/test-loops.sh	0.079028	-0.000205
test/regression-wasm/test-simple-arithmetic.sh	0.070102	-0.000673

github-actions · 2021-08-04T14:17:37Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	0.058523	0
test/regression-evm/test-straight-line.sh	0.061041	0.000003
test/regression-evm/test-straight-line-no-invalid.sh	0.059361	0.000003
test/regression-evm/test-branching-invalid.sh	0.071307	0.000003
test/regression-evm/test-sum-to-n.sh	0.041138	0
test/regression-evm/test-branching-no-invalid.sh	0.070264	0.000003
test/regression-evm/test-add0.sh	0.071492	-0.005859
test/regression-evm/test-sumTo10.sh	0.118636	-0.010136
test/regression-wasm/test-memory.sh	0.063702	-0.000167
test/regression-wasm/test-locals.sh	0.066130	-0.000257
test/regression-wasm/test-wrc20.sh	0.051285	-0.001988
test/regression-wasm/test-loops.sh	0.078994	-0.000207
test/regression-wasm/test-simple-arithmetic.sh	0.070107	-0.000673

github-actions · 2021-08-04T15:08:00Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.000000	0.000002
test/regression-evm/test-straight-line.sh	0.000000	0.006099
test/regression-evm/test-straight-line-no-invalid.sh	0.000000	0
test/regression-evm/test-branching-invalid.sh	0.000000	0.010508
test/regression-evm/test-sum-to-n.sh	0.000002	0
test/regression-evm/test-branching-no-invalid.sh	0.000000	-0.000000
test/regression-evm/test-add0.sh	0.000000	-0.004667
test/regression-evm/test-sumTo10.sh	0.000000	-0.002424
test/regression-wasm/test-memory.sh	0.000005	0
test/regression-wasm/test-locals.sh	-0.000000	0
test/regression-wasm/test-wrc20.sh	0.000000	-0.002677
test/regression-wasm/test-loops.sh	0.000003	0
test/regression-wasm/test-simple-arithmetic.sh	0.000024	0.000000

…nto match-disjunction-tool

github-actions · 2021-08-05T12:28:31Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	0.000001	-0.010840
test/regression-evm/test-straight-line.sh	0.000000	0.004680
test/regression-evm/test-straight-line-no-invalid.sh	0.000000	0.000000
test/regression-evm/test-branching-invalid.sh	0.000000	-0.010399
test/regression-evm/test-sum-to-n.sh	0.000007	0.006962
test/regression-evm/test-branching-no-invalid.sh	0.000000	0
test/regression-evm/test-add0.sh	0.000000	0.000002
test/regression-evm/test-sumTo10.sh	0.000000	0.000188
test/regression-wasm/test-memory.sh	0.000029	-0.000001
test/regression-wasm/test-locals.sh	0.000000	0.000001
test/regression-wasm/test-wrc20.sh	0.000022	0.020649
test/regression-wasm/test-loops.sh	0.000023	0.000001
test/regression-wasm/test-simple-arithmetic.sh	0.000021	-0.000105

ana-pantilie

Looks good to me!

github-actions · 2021-08-06T10:22:04Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	0.000000	-0.050411
test/regression-evm/test-straight-line.sh	-0.000000	-0.004897
test/regression-evm/test-straight-line-no-invalid.sh	0.000000	-0.000000
test/regression-evm/test-branching-invalid.sh	0.000004	-0.000502
test/regression-evm/test-sum-to-n.sh	0.000000	0.007544
test/regression-evm/test-branching-no-invalid.sh	0.000000	0.000000
test/regression-evm/test-add0.sh	0.000000	-0.004286
test/regression-evm/test-sumTo10.sh	0.000000	0.000001
test/regression-wasm/test-memory.sh	0.000003	0.000002
test/regression-wasm/test-locals.sh	-0.000000	-0.000000
test/regression-wasm/test-wrc20.sh	-0.000015	0.011890
test/regression-wasm/test-loops.sh	-0.000002	0
test/regression-wasm/test-simple-arithmetic.sh	-0.000046	0.000075

github-actions · 2021-08-06T14:51:05Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	0.000002	-0.098161
test/regression-evm/test-straight-line.sh	0.000000	0.000000
test/regression-evm/test-straight-line-no-invalid.sh	0.000000	-0.005411
test/regression-evm/test-branching-invalid.sh	-0.000000	0
test/regression-evm/test-sum-to-n.sh	-0.000000	0
test/regression-evm/test-branching-no-invalid.sh	0.000000	-0.000000
test/regression-evm/test-add0.sh	0.000000	0
test/regression-evm/test-sumTo10.sh	0.000000	0.002553
test/regression-wasm/test-memory.sh	0.000005	0.000002
test/regression-wasm/test-locals.sh	0.000000	0.000000
test/regression-wasm/test-wrc20.sh	-0.000009	-0.014917
test/regression-wasm/test-loops.sh	0.000012	0.000000
test/regression-wasm/test-simple-arithmetic.sh	-0.000005	0.000046

github-actions · 2021-08-09T14:50:08Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.000000	-0.004099
test/regression-evm/test-straight-line.sh	0.000000	0.000001
test/regression-evm/test-straight-line-no-invalid.sh	0.000000	0
test/regression-evm/test-branching-invalid.sh	0.000000	0
test/regression-evm/test-sum-to-n.sh	-0.000000	-0.005631
test/regression-evm/test-branching-no-invalid.sh	-0.000001	-0.009352
test/regression-evm/test-add0.sh	-0.000000	-0.004284
test/regression-evm/test-sumTo10.sh	-0.000003	-0.000483
test/regression-wasm/test-memory.sh	0.000007	-0.000000
test/regression-wasm/test-locals.sh	0.000000	0.000001
test/regression-wasm/test-wrc20.sh	-0.000005	0.010099
test/regression-wasm/test-loops.sh	0.000027	0
test/regression-wasm/test-simple-arithmetic.sh	0.000027	0.000262

* add kore-check-functions cabal executable and Main stub * Materialize Nix expressions * draft kore-check-functions command line options * traverse module sentences * drafting function check for a sentence * use isFunctionPattern * cleanup equation pattern match * typechecks, used #2697 as loose template with extractEquations function * log error, use ExitFailure 3 to denote kore-check-function failure * WIP draft check functions test group * add license and copyright * ExitFailure 3 * add verifiedMyModule * Materialize Nix expressions * fixing test errors * move checkFunctions from Main to Kore.CheckFunctions * Materialize Nix expressions * first test typecheck * WIP testing failure * debugging unit test * use toTermLikeOld * debug tests * cleanup and typecheck * Format with fourmolu * debug too many arguments exception * Fix unit test for failing case * Format with fourmolu * Materialize Nix expressions * hlint * move checkFunctions into Kore.Exec * Materialize Nix expressions * move test_checkFunctions from Test.Kore.CheckFunctions into Test.Kore.Exec * Materialize Nix expressions * cleanup and add docs * add notes on test case * capitalization Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> * create new log type, cleanup checkFunctions * Format with fourmolu * Remove comment * Materialize Nix expressions * Make linter happy * cleanup checkFunctions, use filter Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com> Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>

ana-pantilie and others added 7 commits June 23, 2021 16:48

WIP: kore-match-disjunction tool

af0b7e5

General structure of new tool

4d93128

Format with fourmolu

b645dda

Implement kore-match-disjunction

5b5a44e

Materialize Nix expressions

43ea665

Clean-up kore-exec main

ad4b9c8

Merge branch 'match-disjunction-tool' of github.com:kframework/kore i…

0d5551d

…nto match-disjunction-tool

ana-pantilie mentioned this pull request Jul 2, 2021

Check function definitions tool #2710

Merged

4 tasks

dopamane added a commit that referenced this pull request Jul 3, 2021

typechecks, used #2697 as loose template with extractEquations function

a6eaef0

ana-pantilie assigned andreiburdusa Jul 21, 2021

andreiburdusa and others added 6 commits July 26, 2021 13:01

Fix building and HLS processing

f7d0aca

Materialize Nix expressions

5dac97a

Merge remote-tracking branch 'origin/master' into match-disjunction-tool

6a8ea25

Allow "make ghcid-match"

e0559ff

Merge branch 'match-disjunction-tool' of github.com:kframework/kore i…

c79b499

…nto match-disjunction-tool

Apply pedantic

9815891

Add two trivial unit tests

32ca719

Add unit tests inspired by "search" integration test

8c56ab7

andreiburdusa and others added 2 commits August 4, 2021 16:38

Remove comments

771d384

Merge branch 'master' into match-disjunction-tool

4f49cd8

ana-pantilie requested a review from dopamane August 4, 2021 14:12

ana-pantilie self-assigned this Aug 4, 2021

andreiburdusa added 2 commits August 5, 2021 14:44

Address or remove TODOs

72d3346

Merge branch 'match-disjunction-tool' of github.com:kframework/kore i…

5045cfc

…nto match-disjunction-tool

andreiburdusa marked this pull request as ready for review August 5, 2021 11:46

dopamane approved these changes Aug 6, 2021

View reviewed changes

ana-pantilie commented Aug 6, 2021

View reviewed changes

ana-pantilie added the automerge label Aug 6, 2021

Merge branch 'master' into match-disjunction-tool

374ea46

Merge branch 'master' into match-disjunction-tool

184086b

Merge branch 'master' into match-disjunction-tool

b0a4386

ana-pantilie merged commit 4dd38d9 into master Aug 9, 2021

ana-pantilie deleted the match-disjunction-tool branch August 9, 2021 15:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Match disjunction tool #2697

Match disjunction tool #2697

Uh oh!

ana-pantilie commented Jun 24, 2021

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Aug 3, 2021

Uh oh!

github-actions bot commented Aug 4, 2021

Uh oh!

github-actions bot commented Aug 4, 2021

Uh oh!

github-actions bot commented Aug 5, 2021

Uh oh!

ana-pantilie left a comment

Uh oh!

github-actions bot commented Aug 6, 2021

Uh oh!

github-actions bot commented Aug 6, 2021

Uh oh!

github-actions bot commented Aug 9, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Match disjunction tool #2697

Match disjunction tool #2697

Uh oh!

Conversation

ana-pantilie commented Jun 24, 2021

Review checklist

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Jul 26, 2021

Uh oh!

github-actions bot commented Aug 3, 2021

Uh oh!

github-actions bot commented Aug 4, 2021

Uh oh!

github-actions bot commented Aug 4, 2021

Uh oh!

github-actions bot commented Aug 5, 2021

Uh oh!

ana-pantilie left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 6, 2021

Uh oh!

github-actions bot commented Aug 6, 2021

Uh oh!

github-actions bot commented Aug 9, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants