SeLFiE: where to introduce new syntactic sugar for atomic assertions?

[yutakang]

Between Inner-Semantics before Outer?

• pros: easier to do static type checking using ML's type inference without having to write my type checker for SeLFiE?
• cons: I have to do de-sugaring twice: once for Inner and once for Outer.

After Outer-Semantics?

• pros: I have to de-sugar only once.
• pros: the conversion from Outer to Inner needs fewer clauses.
• cons: we cannot use ML's own type inference to confirm that a given inner SeLFiE expression does not involve atomic assertions allowed for outer SeLFiE expressions. The type checking is going to be dynamic by default.
• pros: we can write a static type checker for SeLFiE.

Conclusion: After Outer-Semantics!

[yutakang]

After Eval_Surface.