core: Implement and use ConstraintContext

[PapyChacal]

Just define ConstraintContext to encapsulate the constraint variables used in verification and inference.
Also, define a default value for this argument in verification, to verify with an empty context.

[review-notebook-app]

Check out this pull request on 

See visual diffs & provide feedback on Jupyter Notebooks.

---

Powered by ReviewNB

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 89.87%. Comparing base (dff9ea4) to head (6898caf).
Report is 1 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #2700      +/-   ##
==========================================
+ Coverage   89.86%   89.87%   +0.01%     
==========================================
  Files         367      367              
  Lines       47373    47401      +28     
  Branches     7213     7223      +10     
==========================================
+ Hits        42570    42600      +30     
+ Misses       3695     3693       -2     
  Partials     1108     1108              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[math-fehr]

Nice!
One thing I'm kind of disagreeing on though, is allowing to call verify without the ConstraintContext.
I would say it is the role of the caller to define a ConstraintContext, not the constraint. What do you think?

[PapyChacal]

Nice! One thing I'm kind of disagreeing on though, is allowing to call verify without the ConstraintContext. I would say it is the role of the caller to define a ConstraintContext, not the constraint. What do you think?

Sure, I can just revert that, here are my cents:

• The caller can define one if they want to, but doesn't have to worry about it everytime
• Basically all the erased , {}s would become , ConstraintContext()s, including an extra import. I just think it brings much noise to undesired places, e.g. the docs introducing constraints as a whole.

I want to insist on I can just revert 😋 I see this as bikeshedding, so please first just confirm you want it reverted, and let's continue the discussion separately from the feature 🙂 This is one small piece amongst quite a few small pieces, that will yield very nice expressivity to IRDL, which is what I'm after rather than the API

[PapyChacal]

As discussed in a quick call, I'll revert the default argument thing!