Irrefutable Lambda

[HoshinoTented]

This PR fixes #94 by:

• AyaProducer producing Expr.IrrefutableLam
• Desugar Expr.IrrefutableLam to Expr.Lambda

TODO:

• producer
• question: should we resolve Expr.Lambda even if it is a desugar output?

[ice1000]

• question: should we resolve Expr.Lambda even if it is a desugar output?

Desugar happens after resolving so this should be not applicable

[codecov]

Codecov Report

Attention: Patch coverage is 75.00000% with 14 lines in your changes missing coverage. Please review.

Project coverage is 83.38%. Comparing base (858c1d6) to head (bbf7086).
Report is 19 commits behind head on main.

Files with missing lines	Patch %	Lines
...ax/src/main/java/org/aya/syntax/concrete/Expr.java	50.00%	5 Missing and 1 partial ⚠️
...ase/src/main/java/org/aya/resolve/salt/Desalt.java	80.00%	2 Missing and 1 partial ⚠️
...ain/java/org/aya/resolve/visitor/ExprResolver.java	50.00%	1 Missing ⚠️
...er/src/main/java/org/aya/producer/AyaProducer.java	93.33%	0 Missing and 1 partial ⚠️
...src/main/java/org/aya/syntax/concrete/Pattern.java	66.66%	1 Missing ⚠️
...tax/src/main/java/org/aya/syntax/ref/LocalVar.java	0.00%	1 Missing ⚠️
...in/java/org/aya/util/error/PosedUnaryOperator.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #1283      +/-   ##
============================================
- Coverage     83.41%   83.38%   -0.04%     
- Complexity     4228     4239      +11     
============================================
  Files           385      385              
  Lines         12243    12289      +46     
  Branches       1411     1418       +7     
============================================
+ Hits          10213    10247      +34     
- Misses         1282     1291       +9     
- Partials        748      751       +3     

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

[HoshinoTented]

How about the interaction with pushing pattern from lambda in pattern matching? i.e.:

def what (A : Type) (n : Nat)
| A => fn zero => ...
| A => fn suc n => ...

becomes

def what (A : Type) (n : Nat)
| A, zero => ...
| A, suc n => ...

This may require the desugar in tyck rather than just after resolving.

[ice1000]

How about the interaction with pushing pattern from lambda in pattern matching? i.e.:

def what (A : Type) (n : Nat)
| A => fn zero => ...
| A => fn suc n => ...

becomes

def what (A : Type) (n : Nat)
| A, zero => ...
| A, suc n => ...

This may require the desugar in tyck rather than just after resolving.

🤯🤯🤯.... I think it's ok to not implement this feature. It's unreasonably complicated. Pushing lambda was meant to be a simple feature