Implement "meta patteriables"

[ice1000]

Fix #81, oh my glob.

Summary

Split into five sections.

Refactorings

• Inlined some functions, like CoreDistiller::visitMaybeCtorPatterns. There are some others, I can't remember.
• For BaseDistiller::visitCalls, added a new boolean parameter for implicitness option. This is because sometimes it's ShowImplicitArgs, sometimes it's ShowImplicitPats.
• I replaced all visitors of Pat with pattern matching (JEP 406) and deleted Pat.Visitor the abstract visitor along with all the doAccept methods.

Behavioural improvements

Now we also zonk the types of the patterns after elabClauses. We didn't do this before, but it so far didn't cause any problem. I conjecture that patterns' types are never used after their type checking, but I'm not exactly sure (I'm 95% sure). If they really aren't used, we probably don't have to zonk them, and we probably want to remove them for spatial efficiency. /cc @imkiva

New features

• Added new Pat.Meta for "unknown patterns", which are translated into RefTerm.MetaPat (also new) in PatToTerm. The idea behind these two structures are similar to "meta variables" but for patterns.
  • The zonk for meta patteriables is Pat::inline -- they inline the solutions of meta patteriables. When no solution, we turn them into bind patterns. So, Pat::inline is total, thus no need to have an error reporter.
  • In PatMatcher, we may encounter problems like "matching a pattern p with an instance of RefTerm.MetaPat". In this case, we "solve" the meta patteriable as a renamed version of p. Yes, the renamer for patterns is also added.
  • After all these, we inline the patterns, which is like freezing the meta patteriables. Solved meta patteriables are inlined as their solutions.
• CalmFace patterns are now tycked as meta patterns. They will cause UnsupportedOperationException before.
• Implicitly-generated patterns are now tycked as meta patterns if their types are data types (to avoid MetaPat appearing in the types of unifications). They were generated as bind patterns before.

Assumptions

• We will only see RefTerm.MetaPat in PatMatcher in PatTycker. Other invocations to PatMatcher will not. Therefore, we made the new LocalCtx parameter of PatMatcher nullable, because we need to modify the localCtx in the type checking of patterns.
• Meta patteriables will only be solved once. Unsure what to do when they are solved more than once. Maybe unify the patterns to refine them further? 🤔

Tests

Modified the redblack tree showcase with all manual implicit refinement removed. It works perfectly. Now the exact Agda code can be translated to Aya, with every omittable pattern omitted. One exception is that I discovered a case when you match on two {black} patterns, you don't need to split a rbBlack a x b pattern. I decided to keep this code to make the code shorter afterall.

Sorry for my English.

[codecov]

Codecov Report

Merging #198 (cd49d3e) into main (382832f) will decrease coverage by 0.22%.
The diff coverage is 70.17%.

@@             Coverage Diff              @@
##               main     #198      +/-   ##
============================================
- Coverage     79.66%   79.43%   -0.23%     
- Complexity     2078     2087       +9     
============================================
  Files           197      197              
  Lines          6555     6657     +102     
  Branches        793      808      +15     
============================================
+ Hits           5222     5288      +66     
- Misses          936      965      +29     
- Partials        397      404       +7     

Impacted Files	Coverage Δ
base/src/main/java/org/aya/core/pat/PatUnify.java	51.35% <0.00%> (ø)
...e/src/main/java/org/aya/core/serde/Serializer.java	87.12% <0.00%> (-1.77%)	⬇️
base/src/main/java/org/aya/core/term/Term.java	86.53% <0.00%> (-0.26%)	⬇️
...c/main/java/org/aya/core/visitor/TermConsumer.java	91.83% <0.00%> (-1.92%)	⬇️
base/src/main/java/org/aya/tyck/LittleTyper.java	68.88% <0.00%> (-1.57%)	⬇️
base/src/main/java/org/aya/tyck/unify/DefEq.java	79.35% <0.00%> (-1.31%)	⬇️
base/src/main/java/org/aya/core/pat/Pat.java	61.11% <57.77%> (-8.89%)	⬇️
...ase/src/main/java/org/aya/core/pat/PatMatcher.java	69.49% <61.11%> (-0.78%)	⬇️
...e/src/main/java/org/aya/distill/CoreDistiller.java	83.54% <68.18%> (-1.70%)	⬇️
base/src/main/java/org/aya/tyck/pat/PatTycker.java	86.53% <95.23%> (+0.82%)	⬆️
... and 15 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2d79bc2...cd49d3e. Read the comment docs.

[bors]

✌️ imkiva can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[imkiva]

bors merge

[ice1000]

bors merge

Remember to resolve all conversations before merging as they are hard requirements

[bors]

Build succeeded:

• gradle-check