Desugaring stages

[deemp]

@yegor256, should the void $\rho$-attribute be inserted into formations with a $\Delta$-attribute like in the second picture?

[yegor256]

@deemp yes, definitely

[deemp]

@yegor256, do rules manipulate desugared expressions?

Currently, in the rules, we use pattern and result. Should they be desugared like other expressions?

E.g., here are a pattern and a result:

eo-phi-normalizer/eo-phi-normalizer/test/eo/phi/rules/streams.yaml

Lines 35 to 49 in 6f65f8c

	pattern: |
	⟦
	!τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1,
	!B1
	⟧
	result: |
	⟦
	!τ2 ↦ !b1,
	!τ3 ↦ Φ.opeo.map-for-each(
	α0 ↦ ξ.!τ2,
	α1 ↦ !b2
	),
	!τ1 ↦ ξ.!τ3 * !t1,
	!B1
	⟧

This is what the pattern could be desugared to:

⟦
  !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1,
  !B1,
  ρ ↦ ∅
⟧

It's unclear whether ρ ↦ ∅ should be separate from !B1.

Also, should the pattern be desugared to produce two applications instead of a single application with two attributes?

eo-phi-normalizer/eo-phi-normalizer/test/eo/phi/rules/streams.yaml

Lines 43 to 46 in 6f65f8c

	!τ3 ↦ Φ.opeo.map-for-each(
	α0 ↦ ξ.!τ2,
	α1 ↦ !b2
	),

If the rules manipulate desugared expressions and hence needn't be desugared themselves, the expressions (..., ...) and (...)(...) in the result will have different meanings. In fact, (..., ...) should be prohibited as it won't match anything in a desugared $\varphi$-expression.

[yegor256]

@deemp rules work only with desugared expressions