Skip to content
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

Jump to bottom

Multi-threaded type inference #41

Draft
wants to merge 82 commits into
base: main
Choose a base branch
from
Draft

Multi-threaded type inference #41

wants to merge 82 commits into from

Conversation

acl-cqc
Copy link
Collaborator

@acl-cqc acl-cqc commented Oct 21, 2024

  • Includes adding holes, which could be done separately
  • And, not sure that the nat-solver changes are integrated properly: there are some strange test failures:
    • examples/unified.brat on the first function - no holes or need for multithreading here, so can we diagnose this by integrating nat-solver changes into main?
    • examples/infer.brat checks (as it has a workaround for Smarter solving #35) but fails to compile ("Pow" is TODO. Why are we compiling a Pow ?!)
    • and of course golden tests etc. also need updating

croyzor and others added 30 commits August 19, 2024 14:04
@croyzor
Add "hoping" variables
04c52ac
@croyzor
Expand Free monad with Define and Yield
3a1d6fe
@croyzor
Add Define/Yield cases to handler functions
bf6cfcf
@croyzor
Handle Yield in toplevel handler
a6f00dd
@mark-koch
Add bang parsing
4204c50
@croyzor
Turn on ApplicativeDo
3b8fdc1
@croyzor
Add some dummy code for typechecking !
8f904bc
@croyzor
Revert "Add "hoping" variables"
8b852a2 
This reverts commit 04c52ac.
@croyzor
Some parallelisation
77b92fe
@croyzor
Add hope set to monad
3a1288d
@croyzor
Move occur check logic to Eval
b979c70
@croyzor
misc changes
a197fb2
@croyzor
[broken] update eqworker
b115f84
@croyzor
Revert "[broken] update eqworker"
ce1d1cf 
This reverts commit b115f84.
@croyzor
Add !,! test
c064466
@mark-koch
Rewrite typeEq
b33f100
@croyzor
feat: Solve numbers that are just variables
c093ced
@acl-cqc
typeEqRow returns sub-problems
7986539
@acl-cqc
sequence_ -> traverse_ id
7afa2c4
@croyzor
[broken] Build things to wire into solved hopes
265a5b6
@croyzor
Don't hide that error
2a360b6
@croyzor
Fix typechecking for infer example
6be252b
@croyzor
feat: Complain when we have remaining Nat-kinded holes
646f6f9
@croyzor
Incude file context in hopeSet
c2c8bbe
@croyzor
Allow comparing VInx
3765a8a
@croyzor
Rewrite dynamic num refinements to work on srcs and tgts
a22531b
@croyzor
Fix demandEven logic
af75834
@croyzor
Flip that hypo node back around
283ccae
@croyzor
Rewrite computeMeta to do definition as well
0da9554
@acl-cqc
SolvePatterns build fixes; unified.brat+infer.brat fail with non-clos…
2139140 
…ed Nat value
acl-cqc and others added 28 commits October 1, 2024 16:41
@acl-cqc
simpleCheck is Checking, allow to define hopes (except nat/int?!) and…
a4115fb 
… block
@acl-cqc
typeMap stores skolem-ness (always False ATM); TypeOf returns (EndTyp…
3b76be2 
…e,Bool)
@acl-cqc
Inline only use of declareSrc
2ebb941
@acl-cqc
Declare takes Bool param (still always False)
e0c7997
@acl-cqc
anext' allows setting Sources to be skolem
45751ac
@acl-cqc
implement isSkolem using TypeOf
87270bf
@acl-cqc
Common up Checking wrappers via 'wrapper' and 'wrapper2'
2fcdd48
@acl-cqc
print hopeset when blocked
75a5ac0
@acl-cqc
Use defineEnd more
9f1c6ff
@acl-cqc
Add mkYield, use it
0808dab
@acl-cqc
Remove concurrency-blocking -!s in makeBox (27 -> 24 fails)
a83de68
@acl-cqc
Remove howStuck, just use Unstuck (30 -> 27 fails)
98a5671
@acl-cqc
typeEqEta shouldWait for ends inside nums as well, assert -> unless
db83ba9
@croyzor
Redo invertNatVal
710c931
@acl-cqc
Refactor typeEqEta
3b36023
@acl-cqc
typeEqEta: fast-path without blocking for both ends the same
3e15acc
@acl-cqc
typeEqEta shouldWait for ends inside nums as well, assert -> unless
a900ac4
@acl-cqc
Refactor typeEqEta
3bf4f0b
@acl-cqc
typeEqEta: fast-path without blocking for both ends the same
2c8f26b
@acl-cqc
Call eval after resumption in simpleCheck
42ef6d3
@acl-cqc
Merge remote-tracking branch 'origin/main' into inference-wip/fork
5b13e9d
@croyzor
Merge remote-tracking branch 'origin/inference-wip/fork' into new/inf…
43bcaf8 
…erence-wip
@acl-cqc
Merge remote-tracking branch 'origin/craig/inference-wip/fork-and-nat…
62332cf 
…val' into inference-wip/fork
@acl-cqc
SolvePatterns build fixes
5517854
@acl-cqc
Merge remote-tracking branch 'origin/main' into inference-wip/fork (c…
48cd1e2 
…onflict)
@acl-cqc
Comment out mapVec
4f8099b
@acl-cqc
Fix checking of infer.brat w/note, add more. Compilation fails on Pow ?!
9203cb6
@acl-cqc
Revert "TEMP remove failure tests"
95dad0f 
This reverts commit 251455b.
@acl-cqc acl-cqc mentioned this pull request Oct 21, 2024
Merged
@acl-cqc acl-cqc mentioned this pull request Nov 1, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@acl-cqc @croyzor @mark-koch