Skip to content

Conversation

@andrevidela
Copy link
Collaborator

@andrevidela andrevidela commented Aug 14, 2025

Description

Draft implementation for #3582 this is the prototype branch with main rebased and all commits squashed.
to do:

  • remove <- symbol for binding operators. It should be its own PR
  • Add some error messages
    • typebind misuse at declaration site
    • autobind misuse at declaration site
    • binding misuse at use-site
  • cleanup a bit
  • update changelog
  • update documentation
  • split off changes to ImpTy to its own PR replace ImpTy #3615
  • Refactor Basic binder as its own PR remove dead code #3624
  • Refactor conName in PRecord as its own PR Method refactor #3619
  • Refactor Method as is own PR Method refactor #3619
  • Fix idris2-lsp

Self-check

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md

@andrevidela
Copy link
Collaborator Author

#3570 really worked: there are no visible changes to TTC files other than the new data type. All the other changes are automatic 🎉

prettyPrec d (PForce _ tm) = parenthesise (d > startPrec) $ "Force" <++> prettyPrec appPrec tm
prettyPrec d (PAutoApp _ f a) =
parenthesise (d > startPrec) $ group $ prettyPrec leftAppPrec f <++> "@" <+> braces (pretty a)
prettyPrec d (PBindingApp fn bind scope) = ?TODO2
Copy link
Collaborator

Choose a reason for hiding this comment

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

hole

@andrevidela andrevidela force-pushed the binding-application-real branch from d34a60d to e5301db Compare August 14, 2025 16:09
@andrevidela andrevidela mentioned this pull request Aug 14, 2025
@andrevidela andrevidela force-pushed the binding-application-real branch from 0f2e13e to ba71e14 Compare August 19, 2025 13:29
@andrevidela andrevidela force-pushed the binding-application-real branch 5 times, most recently from a989f77 to 0f1e3f3 Compare August 25, 2025 14:54
@andrevidela andrevidela force-pushed the binding-application-real branch from f86fb64 to 0453c43 Compare August 31, 2025 16:38
showPTermPrec d (PNamedApp _ f n a)
= showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPTermPrec d a ++ "}"
showPTermPrec d (PBindingApp fn bind scope)
= ?TODO1
Copy link
Collaborator

Choose a reason for hiding this comment

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

hole

a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IApp") [fc', f', a']
reflect fc defs lhs env (IBindingApp tfc f a)
= ?TODOReflect3
Copy link
Collaborator

Choose a reason for hiding this comment

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

hole

reflect fc defs lhs env (SpecArgs r)
= do r' <- reflect fc defs lhs env r
appCon fc defs (reflectionttimp "SpecArgs") [r']
reflect fc defs lhs env (Binding r) = ?add
Copy link
Collaborator

Choose a reason for hiding this comment

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

hole

@dunhamsteve
Copy link
Collaborator

I haven't had time to look more closely, but these tests are failing because of lost documentation:

test
idris2/warning/warning002 On a deprecated top level function
idris2/interactive/interactive019 On top level functions
idris2/interactive/interactive030 On both top level functions and interface fields
idris2/misc/docs002 Top level function in a namespace
idris2/misc/docs001 On interface fields

ttimp/record003 is failing from a unification error: "unifying: (0 pos : ($resolved366 ($resolved361 $resolved359))) -> Type and Type". pos is a trailing auto on a type constructor:

@andrevidela
Copy link
Collaborator Author

Ah yes, sorry I wasn't expecting a review at this stage it's still a WIP. I was refactoring a bit of the documentation code with the intent to make it its own PR. There is still some work to do

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