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

Auto traits #54

Merged
merged 14 commits into from
Jul 17, 2017
Merged

Auto traits #54

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
d0ab9ac
First try for negative impls and auto traits
scalexm Jun 29, 2017
7796360
Add documentation and tests
scalexm Jun 29, 2017
779ae25
Add coherence rules
scalexm Jun 29, 2017
12baae7
Merge branch 'master' into cologic
scalexm Jul 10, 2017
2216603
Fix tests and wf for negative bounds
scalexm Jul 10, 2017
3c66e1d
Change strategy for coinductive semantics
scalexm Jul 11, 2017
70f70f5
Add documentation
scalexm Jul 11, 2017
a555776
Disable negative trait bounds
scalexm Jul 11, 2017
7f34963
Change syntax for auto traits
scalexm Jul 11, 2017
d76c379
Add newline at end of solve/test.rs
scalexm Jul 11, 2017
82ed96b
Merge branch 'master' into cologic
scalexm Jul 12, 2017
6863ff1
Add missing last element of a coinductive cycle
scalexm Jul 12, 2017
4844044
Change a test and some other minor things
scalexm Jul 13, 2017
72e6553
Do not expand where clauses for default impls
scalexm Jul 16, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion src/solve/solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,12 @@ impl Solver {
// if all the components of the cycle also have coinductive semantics, we accept
// the cycle `(?0: AutoTrait) :- ... :- (?0: AutoTrait)` as an infinite proof for
// `?0: AutoTrait` and we do not perform any substitution.
if self.stack.iter().skip(index).all(|s| s.goal.is_coinductive(&*self.program)) {
if self.stack.iter()
.skip(index)
.map(|s| &s.goal)
.chain(Some(&goal))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Heh. =) Funny oversight. Maybe add a test for this? Maybe not worth it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I realised that from a correctness point of view, that's the same thing because we already know that there is a cycle starting at index index, so the very first element of our iterator is also our current goal already. Anyway, let's keep it that way :)

.all(|g| g.is_coinductive(&*self.program))
{
let value = ConstrainedSubst {
subst: Substitution::empty(),
constraints: vec![],
Expand Down