[ derive ] Support data specialisation#299

Draft

UARTman wants to merge 81 commits intobuzden:masterfrom

UARTman:dtc-integration

Contributor

UARTman commented Nov 11, 2025

No description provided.

UARTman changed the title ~~Dtc-integration~~ Integrate data specialisation into DepTyCheck

buzden added code: enhancement part: derivation derive: core labels

buzden changed the title ~~Integrate data specialisation into DepTyCheck~~ [ derive ] Support data specialisation

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Gen/ForAllNeededTypes/Impl.idr

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Util/Specialisation.idr Outdated

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Util/Specialisation.idr Outdated

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Util/Specialisation.idr Outdated

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Util/Specialisation.idr Outdated

buzden reviewed

View reviewed changes

src/Deriving/DepTyCheck/Util/Specialisation.idr Outdated

UARTman force-pushed the dtc-integration branch from f1eed9c to 1d8ef86 Compare

November 26, 2025 13:08

UARTman force-pushed the dtc-integration branch 2 times, most recently from 72514fd to bfab5e4 Compare

December 19, 2025 07:52

buzden force-pushed the dtc-integration branch from bfab5e4 to daf006f Compare

December 22, 2025 11:49

UARTman force-pushed the dtc-integration branch from 765b607 to 6172a22 Compare

January 20, 2026 15:14

UARTman force-pushed the dtc-integration branch from 88eba11 to fa269f4 Compare

March 5, 2026 06:59

UARTman force-pushed the dtc-integration branch 2 times, most recently from d930c00 to fb5fb48 Compare

March 19, 2026 09:54

UARTman added 11 commits

April 2, 2026 12:02


          [ refactor ] Rename specialisation functions

18c16e3


          [ new ] Implement normaliseTask

32af2c3


          [ new ] Sketch out specialiseIfNeeded


          [ cleanup ] Remove unneeded lets from specialiseIfNeeded

97ab446


          [ refactor ] Move specialisation-related code to Util.Specialisation

5bd402e


          [refactor, new] Add first test for specialiseIfNeeded

88a2425


          [ fix ] Remove some type ambiguity from decEq implementation derivator

752d417


          [ new ] Overhaul processArgs for more correct specialisation task g…

fb04dfe

…eneration


          [ new ] Make processArgs more aware of application semantics

576ef60


          [ cleanup ] Break up overlong line

78105cf


          [ cleanup ] Minor cleanup

00ef425

UARTman added 27 commits

April 2, 2026 12:02


          [ test ] Adjust spec-if-needed expecteds for 2e969a8

0e09258


          [ new ] Sketch out the recursive constructor argument finder


          [ new ] Generate separate specialised type signature

9bbd3e8


          [ refactor ] Pre-cache specialised type invocation

e9478e9


          [ refactor ] Decouple claims from definitions

d3935c1


          [ new ] Implement recursive argument checking

25d0b07

- breaks function derivation in recursive spec types


          [ refactor ] Add type metadata records, update packdb

02e21fa


          [ new ] Implement new cast injectivity prover (WIP)

3f22c84


          [ new ] Give mToPImpl implicit arguments in cast injectivity prover

7b78634


          [ new ] Make all specialisation tests pass

e9be772


          [ new ] Fix long line lint

8eea0d4


          [ refactor ] Clean up specialiser code

dba286c

- Remove obsolete implementations and unneeded functions
- Document some new functions


          [ new ] Add test for failing specialisation in pil-reg

7d9f794

It fails for now


          [ new ] Improve normaliseTask type resolution

e9b77de


          [ refactor ] Adjust specdata-027 to be abour normalisation

fadb0a9


          [ fix ] Arg name <-> hole conversion in task normalisation

f05521d


          [ fix ] Give normalizer better types

d664637


          [ new ] Use polymorphic types in PilFun

1717d9f


          [ fix ] Update pil-fun expected test

f796a79


          [ fix ] Work around mgn quirks

45123aa


          [ fix ] Generate correct DPair sequences for specialiseds with >=2 gi…

77da5af

…vens


          [ new ] Use polymorphic types in PilDyn

6d6a0a0


          [ fix ] Add ConsRecs to specialiseIfNeeded

fd64ca6


          [ fix ] Fix tests to work after rebase


          [ fix ] Update specialisation logic in dtc following rebase


          [ perf ] Monadize another bottleneck

38714ac

~5 times faster now


          [ fix ] Fix tests broken by recent rebase

de5fe1a

UARTman force-pushed the dtc-integration branch from fb5fb48 to de5fe1a Compare

April 2, 2026 09:03

UARTman added 2 commits

April 6, 2026 16:41


          [ clean ] Cleanup specialiser code

95130c6


          [ clean ] Continue specialiser cleanup

24f4769

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

code: enhancement derive: core part: derivation