The basic idea is to compute a (sparse, upper triangular) matrix whose position (i,j) contains the parses from position i to j in the input string. The fact that it works is fascinating! The formalisation is an exercise in working with block matrices in several layers and keeping few requirements on the final matrix elements in the "leaves" but still synthesizing the necessary properties on the way up the "quad tree".
The Agda code was originally published on github in 2016 (using Agda version 18.104.22.168 and agda-stdlib-0.9) but as usual with code written in a living language (Agda) it did not type check anymore. It took almost two hours to figure out the changes needed to bring it up to date with current Agda 2.6.3 and stdlib 1.7.3: https://github.com/DSLsofMath/ValiantAgda
There were a number of (arguably minor) changes needed:
records need new modifier eta-equality to allow for pattern-matching (with eta-equality) on the constructor.
IsCommutativeMonoid record rationalised in the library (the hint was a bit indirect: “The record type IsCommutativeMonoid does not have the fields isSemigroup, identityˡ but it would have the field isMonoid …”.)
It would be interesting to investigate what it wold take to build tool support for this kind of code refactoring. The only tool support I had was the error messages from (current) Agda and the full repository history of stdlib on github.
Follow this website
You need to create an Owlstown account to follow this website.