rogerburtonpatel / vml

Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
5 stars 0 forks source link

Develop a desugaring of Scheme `cond` form into Verse #2

Closed nrnrnr closed 8 months ago

nrnrnr commented 9 months ago

This will make equivalent code more readable and save lots of writing else wrong.

rogerburtonpatel commented 9 months ago

See comment on issue #3, bullet 2.

nrnrnr commented 8 months ago

Is this still worth doing? I'm inclined to think so. Either it should be easy or it should expose issues that need to be exposed.

Knock it off before our next meeting?

rogerburtonpatel commented 8 months ago

Yes! Though, to be honest, I'm curious what exactly you mean by this.

My understanding is to have cond as a form with a keyword that allows for multiple branches and an implicit else wrong at the end. Do we not already have this with if ... fi?

Or, is it that if ... fi is sugar for nested ifs, and we need a proof of the desugaring?

Or, I'm missing something.

rogerburtonpatel commented 8 months ago

That said, a sample desugaring of cond now exists here. Let's discuss and see what's right and wrong with it on this thread.

nrnrnr commented 8 months ago

I think I must have been using cond as a synonym for if ... fi. (Perils of working with somebody who is not accustomed to saying when concrete syntax is and is not important.)

Your desugaring falls mostly into the category of "easy and knocked off." Except for one thing: I think it better to desugar directly into core Verse, not into if which is itself syntactic sugar.

I recommend you do that, declare victory, and close this issue.

rogerburtonpatel commented 8 months ago

⛳️