Skip to content

fix: Check that all overs and unders are used in toplevel defs#48

Merged
croyzor merged 4 commits intomainfrom
fix/rightunders
Oct 29, 2024
Merged

fix: Check that all overs and unders are used in toplevel defs#48
croyzor merged 4 commits intomainfrom
fix/rightunders

Conversation

@croyzor
Copy link
Copy Markdown
Collaborator

@croyzor croyzor commented Oct 28, 2024

No description provided.

@croyzor croyzor requested a review from mark-koch October 28, 2024 15:54
f(x) = x
^

Type mismatch when checking (x,「x」)
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Where is this (x,「x」) coming from?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Not sure, but that doesn't look right! My guess is that (x, 「x」) is the LHS and RHS of this clause

where
checkConnectorsUsed _ _ _ ([], []) = pure ()
checkConnectorsUsed (_, tmFC) tm (_, unders) ([], rightUnders) = localFC tmFC $
err (TypeMismatch tm (showRow unders) (showRow (filter ((`notElem` (fst <$> rightUnders)) . fst) unders)))
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Can't you do drop (length rightUnders) unders instead of the filter? The unused unders should always be on the right?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

We actually want to drop everything until rightUnders, it's quite annoying

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

the idiomatic ways i thought of to do this all involved a double reverse, which seems a bit objectionable

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

So drop (length unders - length rightUnders) unders also doesn't work?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

🤦 yes, that should work

@croyzor croyzor merged commit 8752f32 into main Oct 29, 2024
@croyzor croyzor deleted the fix/rightunders branch October 29, 2024 17:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants