Easier prototyping of code

[tanyongkiam]

This issue is about speeding up prototyping of code that is (to be) verified using the translator and/or CF.

Currently, the process I used is roughly:

1. write HOL definitions (to be translated)
2. write CakeML code (to be verified by CF)
3. do the standard boilerplate to extract a full program
4. compile in the logic

Now, to optimize the resulting code, one does:

5. Go back to Step 1 and/or 2, make changes, repeat.

Overall, this process is rather tedious because one has to wait for compilation in the logic for each prototype.

One way to speed this process is to use the binary compiler. However, this requires concrete syntax.

It would be nice to provide a facility/library so that Step 1-3 above can easily be made to dump the full program in concrete syntax using e.g.: astPP (https://github.com/CakeML/cakeml/blob/master/semantics/astPP.sml)

[tanyongkiam]

Suggestion from @myreen for improving robustness of astPP:

1. Given a CakeML program foo in HOL, call the sexpr generator on foo to get foo_sexpr_1
2. Call astPP on foo to get foo_concrete
3. Call the binary CakeML compiler on foo_concrete to get foo_sexpr_2
4. Diff foo_sexpr_1 and foo_sexpr_2 and fail if they differ

[myreen]

I think this is a great idea!

I just want to add that I suspect one needs replace Step 4 with:

4. Call the binary CakeML compiler on foo_sexpr_1 to get foo_sexpr_3
5. Diff foo_sexpr_3 and foo_sexpr_2 and fail if they differ

because the sexpr generator from HOL might format its output slightly differently.

[mn200]

How slow do you reckon an AST-to-sexp function in HOL would take to EVAL such things? If it was OK, you could then also think about attempting to verify that the parser and printer inverted each other.

[myreen]

@mn200 I'm confused by this:

you could then also think about attempting to verify that the parser and printer inverted each other.

I was under the impression that the sexp parser has been proved to invert the sexp printer. I suspect the relevant lines are:

cakeml/compiler/parsing/fromSexpScript.sml

Lines 1966 to 1968 in bd2ad29

	Theorem decsexp_sexpdec:
	∀s d. sexpdec s = SOME d ⇒ decsexp d = s
	Proof

However, I think all of this is a bit beside the point. The point is that we want to quickly extract a first version of a program from HOL. The target of this extraction should be concrete syntax (normal SML syntax) that can easily be tweaked outside of HOL. Currently, the means to get this concrete syntax is through astPP, and we know that astPP a bit untested and, as a result, the focus of this issues it drifting towards improving astPP. One way to find bugs in it is make testing of its output part of the regression test.

[mn200]

Well, then if those sexps can be consumed by the compiler, why not iterate over @tanyongkiam's process above going via sexps to get the ability to test the code. It sounded to me as if all the code-writing was being done with HOL functions and process_topdecs type things, not wanting to also edit concrete syntax outside of HOL.

[tanyongkiam]

That makes sense! I guess the proposal is more if we'd want to prototype outside of HOL/process_topdecs by modifying concrete syntax right away.

[sorear]

A pretty-printed concrete syntax step for easy hack modifications? I like that. I did some similar surgery on the sexpr compiler to get the numbers in #774 but getting the sexpr into a state where I could edit it was not trivial.