Represent size-change graphs as matrices (addresses #2954) #3108

mjustus · 2023-10-17T20:01:16Z

No description provided.

gallais

Exciting!

src/Core/Termination/CallGraph.idr

src/Core/Termination/SizeChange.idr

src/Libraries/Data/SparseMatrix.idr

We also update sc-graph generation to - fully traverse `As` patterns - go under `Dotted` patterns - consider `f x <= f`

Changes to the termination checker brought along some otherwise insignificant changes to debug and error messages.

…har`s

mjustus · 2023-11-02T15:22:17Z

It could always be improved further but I am reasonably happy with this PR now. Some things I considered but didn't do in the end:

select the non-terminating sc-graph corresponding to the shortest call sequence
print the selected sc-graph as part of the error message
make columns in printed sc-graphs right-aligned

gallais reviewed Oct 20, 2023

View reviewed changes

src/Core/Termination/CallGraph.idr Show resolved Hide resolved

src/Core/Termination/CallGraph.idr Outdated Show resolved Hide resolved

src/Core/Termination/SizeChange.idr Outdated Show resolved Hide resolved

src/Libraries/Data/SparseMatrix.idr Show resolved Hide resolved

gallais added enhancement implem: termination checking labels Oct 20, 2023

mjustus marked this pull request as draft November 1, 2023 15:09

mjustus added 23 commits November 2, 2023 13:34

[ refactor ] move SizeChange to a separate file

e9fd2b8

[ cleanup ] use information order for SizeChange

010597d

[ new ] sparse matrices

343c85f

[ new ] semiring instance for SizeChange

d10cc59

[ new ] Pretty instance for SizeChange

a299c46

[ fix idris-lang#2954 ] use matrices to represent sc-graphs

2a22cef

We also update sc-graph generation to - fully traverse `As` patterns - go under `Dotted` patterns - consider `f x <= f`

[ cleanup ] update expected test outputs

6146371

Changes to the termination checker brought along some otherwise insignificant changes to debug and error messages.

[ test ] tracking size-change in dot patterns

abdd321

[ test ] tracking size-change across applications

79a314e

[ doc ] sparse matrix invariants

75fd2ad

[ new ] replicateChar, an analogue to spaces but for arbitrary `C…

ed38cf5

…har`s

[ new ] labels for pretty-printed sparse matrices

28b8fb9

[ debug ] sc-graphs now have labels "l" and "r" for LHS and RHS

7140d1e

[ cleanup ] remove duplicate and unused functions

714c269

[ doc ] clarification on neutrals

1c49a68

[ cleanup ] split Vector and Vector1 into separate namespaces

4c5f1b9

[ cleanup ] move auxiliary function to where block

e968e5d

[ cleanup ] remove 1 suffix from Vector1 functions

5b3f48b

[ fix ] handle printing of empty matrices gracefully

db0a302

[ cleanup ] bring formatting of sc-graphs in tests back in sync

f887ffd

[ doc ] bring description of mkChange back in sync

0e425ae

[ cleanup ] remove unneeded debug messages

ddaa553

[ doc ] bring findLoops and checkNonDesc description back in sync

23004b5

mjustus force-pushed the termination-matrix branch from 0061431 to 23004b5 Compare November 2, 2023 15:12

mjustus marked this pull request as ready for review November 2, 2023 15:12

mjustus merged commit a26766e into idris-lang:main Nov 6, 2023
22 checks passed

CodingCellist mentioned this pull request Mar 18, 2024

[ test ] Add issue#1988 to the test suite #3238

Merged

dunhamsteve mentioned this pull request Jun 19, 2024

[ cleanup ] remove unused code left in #3108 #3323

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Represent size-change graphs as matrices (addresses #2954) #3108

Represent size-change graphs as matrices (addresses #2954) #3108

mjustus commented Oct 17, 2023

gallais left a comment

mjustus commented Nov 2, 2023

Represent size-change graphs as matrices (addresses #2954) #3108

Represent size-change graphs as matrices (addresses #2954) #3108

Conversation

mjustus commented Oct 17, 2023

gallais left a comment

Choose a reason for hiding this comment

mjustus commented Nov 2, 2023