Skip to content

[ derive ] Support data specialisation #299

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
UARTman wants to merge 81 commits into
base: master
Choose a base branch
from
Draft

[ derive ] Support data specialisation #299

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
81 commits
Select commit Hold shift + click to select a range
18c16e3
[ refactor ] Rename specialisation functions
UARTman Nov 11, 2025
32af2c3
[ new ] Implement normaliseTask
UARTman Nov 11, 2025
7457335
[ new ] Sketch out specialiseIfNeeded
UARTman Nov 11, 2025
97ab446
[ cleanup ] Remove unneeded lets from specialiseIfNeeded
UARTman Nov 11, 2025
5bd402e
[ refactor ] Move specialisation-related code to Util.Specialisation
UARTman Nov 12, 2025
88a2425
[refactor, new] Add first test for specialiseIfNeeded
UARTman Nov 25, 2025
752d417
[ fix ] Remove some type ambiguity from decEq implementation derivator
UARTman Nov 27, 2025
fb04dfe
[ new ] Overhaul `processArgs` for more correct specialisation task g…
UARTman Nov 27, 2025
576ef60
[ new ] Make `processArgs` more aware of application semantics
UARTman Nov 27, 2025
78105cf
[ cleanup ] Break up overlong line
UARTman Nov 27, 2025
00ef425
[ cleanup ] Minor cleanup
UARTman Nov 27, 2025
0609c25
[ fix ] Use different awk invocation
UARTman Nov 27, 2025
4b5e85f
[ new ] Autogenerate specialised type names using hashes of specialis…
UARTman Dec 9, 2025
da5cfcd
[ fix ] Use local names in derived specialised types
UARTman Dec 10, 2025
f65894c
[ fix ] Allow detection of existing specialised types in local context
UARTman Dec 10, 2025
b4afb32
[ cleanup ] Unpin hashable-derive
UARTman Dec 16, 2025
40e4240
[ derive ] Call to specialiser during derivation process
buzden Dec 19, 2025
380f3c0
[ fix ] Don't specialise types with private constructors + immediatel…
UARTman Dec 25, 2025
63bc91f
[ fix, refactor ] Fix `specialiseIfNeeded`
UARTman Jan 12, 2026
953f2fa
[ fix ] Make `.cleanup-names` nix-friendly
UARTman Jan 12, 2026
90f0a0d
[ new ] Add logging for derived spec types
UARTman Jan 13, 2026
cd7b0f1
[ fix ] Hide SnocVect in le/r/gadt/015 test
UARTman Jan 13, 2026
ad0f602
[ fix ] Update expected logs for specIfNeeded
UARTman Jan 13, 2026
9d6bfd0
[ fix ] Update expecteds in derivation/core
UARTman Jan 13, 2026
25944d5
[ fix ] Add missing check to processArg
UARTman Jan 14, 2026
e35c2eb
[ fix, new ] Add argument analysis logging and fix specIfNeeded tests
UARTman Jan 14, 2026
3657556
[ cleanup ] Fix editorconfig lint
UARTman Jan 14, 2026
d0baca7
[ fix ] Remove some of the memory-explosion effects of logging
UARTman Jan 14, 2026
cbe9592
[ new ] Add trivial test on detecting type arg passthroughs
UARTman Jan 15, 2026
728caef
[ new ] Implement specialised constructor name erasure
UARTman Jan 15, 2026
b1908ab
[ fix ] Prefix name-erased constructors with typename
UARTman Jan 15, 2026
60292bf
[ new ] Add test for deriving spec list generators
UARTman Jan 18, 2026
0cf3a73
[ new ] Add test for spec vects
UARTman Jan 18, 2026
9d313b2
[ new ] Add test for Vect n (Fin n) derivation
UARTman Jan 18, 2026
7ea059b
[ test ] Add tests with a need for specialisation
buzden Oct 27, 2025
8b8233b
[ delete ] Remove redundant spec tests from core
UARTman Jan 19, 2026
26bd951
[ test ] Add couple more tests for simple specialisation
buzden Jan 19, 2026
7b6d255
[ fix ] Fix cast-wrapping in specialised generators
UARTman Jan 20, 2026
366e5bd
[ fix ] Make spec tests compile and fail only on totality check
UARTman Jan 20, 2026
dc96978
[ new ] Display specialised name in normal logs
UARTman Jan 20, 2026
494778f
[ test ] Add some lacking print tests + fix one run test
buzden Jan 20, 2026
fcf5a4c
[ fix ] Fix incorrect gen signature in tests
UARTman Jan 20, 2026
2adea51
[ fix ] Fix bugs in specialiseIfNeeded logic
UARTman Jan 20, 2026
aa0a3bc
[ test ] Add expected values to succeeding tests
UARTman Jan 20, 2026
7394b2e
[ cleanup ] Break up too-log lines
UARTman Jan 20, 2026
6d34bca
[ test ] Update specialise-if-needed outputs
UARTman Jan 20, 2026
5ed6007
[ test ] Fix more tests
UARTman Jan 20, 2026
15318ad
[ test ] Fixup print tests
UARTman Jan 20, 2026
1189421
[ test ] Add test for obscure spec bug (yet unfixed)
UARTman Jan 21, 2026
49bf59c
[ fix ] Prepend type name to type arguments
UARTman Jan 21, 2026
7b89074
[ test ] Port specialise-data tests over to symlinks
UARTman Jan 21, 2026
c2fa884
[ fix ] Allow for dependent lambdas in specialisation
UARTman Jan 21, 2026
0e09258
[ test ] Adjust spec-if-needed expecteds for 2e969a89
UARTman Jan 21, 2026
1597497
[ new ] Sketch out the recursive constructor argument finder
UARTman Jan 23, 2026
9bbd3e8
[ new ] Generate separate specialised type signature
UARTman Jan 26, 2026
e9478e9
[ refactor ] Pre-cache specialised type invocation
UARTman Jan 26, 2026
d3935c1
[ refactor ] Decouple claims from definitions
UARTman Jan 27, 2026
25d0b07
[ new ] Implement recursive argument checking
UARTman Jan 29, 2026
02e21fa
[ refactor ] Add type metadata records, update packdb
UARTman Jan 29, 2026
3f22c84
[ new ] Implement new cast injectivity prover (WIP)
UARTman Feb 3, 2026
7b78634
[ new ] Give mToPImpl implicit arguments in cast injectivity prover
UARTman Feb 4, 2026
e9be772
[ new ] Make all specialisation tests pass
UARTman Feb 4, 2026
8eea0d4
[ new ] Fix long line lint
UARTman Feb 4, 2026
dba286c
[ refactor ] Clean up specialiser code
UARTman Feb 4, 2026
7d9f794
[ new ] Add test for failing specialisation in pil-reg
UARTman Feb 9, 2026
e9b77de
[ new ] Improve normaliseTask type resolution
UARTman Feb 9, 2026
fadb0a9
[ refactor ] Adjust specdata-027 to be abour normalisation
UARTman Feb 9, 2026
f05521d
[ fix ] Arg name <-> hole conversion in task normalisation
UARTman Feb 9, 2026
d664637
[ fix ] Give normalizer better types
UARTman Feb 11, 2026
1717d9f
[ new ] Use polymorphic types in PilFun
UARTman Feb 16, 2026
f796a79
[ fix ] Update pil-fun expected test
UARTman Feb 16, 2026
45123aa
[ fix ] Work around mgn quirks
UARTman Feb 24, 2026
77da5af
[ fix ] Generate correct DPair sequences for specialiseds with >=2 gi…
UARTman Mar 2, 2026
6d6a0a0
[ new ] Use polymorphic types in PilDyn
UARTman Mar 2, 2026
fd64ca6
[ fix ] Add ConsRecs to specialiseIfNeeded
UARTman Mar 5, 2026
8237618
[ fix ] Fix tests to work after rebase
UARTman Mar 5, 2026
7650611
[ fix ] Update specialisation logic in dtc following rebase
UARTman Mar 16, 2026
38714ac
[ perf ] Monadize another bottleneck
UARTman Mar 17, 2026
de5fe1a
[ fix ] Fix tests broken by recent rebase
UARTman Mar 17, 2026
95130c6
[ clean ] Cleanup specialiser code
UARTman Apr 6, 2026
24f4769
[ clean ] Continue specialiser cleanup
UARTman Apr 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
3 changes: 3 additions & 0 deletions deptycheck.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ modules = Deriving.DepTyCheck.Gen
, Deriving.DepTyCheck.Util.ArgsPerm
, Deriving.DepTyCheck.Util.DeepConsApp
, Deriving.DepTyCheck.Util.Primitives
, Deriving.DepTyCheck.Util.Specialisation
, Test.DepTyCheck.Gen
, Test.DepTyCheck.Gen.Coverage
, Test.DepTyCheck.Gen.Emptiness
Expand All @@ -35,6 +36,8 @@ depends = ansi
, best-alternative
, dependent-vect
, elab-util-extra
, hashable
, hashable-derive
, i-hate-parens
, if-unsolved-implicit
, mtl-tuple-impls
Expand Down
Loading
Loading