build multiple translations from patterns to verse

[nrnrnr]

Here are some possible translations:

1. Translation from P to if-then-else as shown in the recent examples
2. Same translation but using a cond-like desugaring if ... -> ... [X] ... -> ... fi
3. Proof of equivalence of these translations
4. Translation from P to the more attractive target using choice with the single one
5. Proof of equivalence of translations 1 and 4

Note: for P take the case form of μML (BPC, chapter 9)

[rogerburtonpatel]

1. Gone from informal to semi-formal. Working on formalizing.
2. Wrote this. It's only as right as the first one. Question- since we want to avoid writing else wrong all the time, does reaching fi imply wrong? i.e. we avoid generating the final else wrong branch and say if control reaches past the last branch in an if-fi or cond structure, we generate wrong?
3. Proof of equivalence of a desugar. TODO.
4. Gone from informal to semi-formal. Working on formalizing.
5. Know (see: think I know) how to do. TODO.

[rogerburtonpatel]

Semi-formal translation:

In P:

case scrutinee of 
P1 ... Pn -> a
...

==

V-style if-else:

if (exists? P1 ... Pn. scrutinee = P1 ... Pn) then a 
else if ... 
else wrong

==

Now with cond:

(cond 
(exists? P1 ... Pn. scrutinee = P1 ... Pn a)
...
else wrong)
// note: as asked above, since our cond form is to AVOID "else wrong", 
// I believe we don't want this last branch as explicit? 

== 

Finally, Dijkstra's if:

if 
(exists? P1 ... Pn. scrutinee = P1 ... Pn -> a)
(truthy value) (unification problem -> res)
fi
--- getting here yields WRONG

[nrnrnr]

2. Wrote this. It's only as right as the first one. Question- since we want to avoid writing else wrong all the time, does reaching fi imply wrong? i.e. we avoid generating the final else wrong branch and say if control reaches past the last branch in an if-fi or cond structure, we generate wrong?

Yes. Our if ... fi is just a better concrete syntax for cond. I recommend you look at the desugaring for cond on page 164, BPC. Which I see is missing a bracket.

I also recommend you look at the laws and semantics for case expressions in Chapter 9 Chapter 8.

[rogerburtonpatel]

Read BPC (I believe it's chapter 8; 9 is molecule). Tired after intro and other homework, so posting real updates tomorrow.

[rogerburtonpatel]

Got some translations and the beginnings of code. Tomorrow's project to make good enough to post.