Michael Norrish

parse_topdecs requires evaluation of functions defined in semantics (those from `ptreeConversion`). I can pull in the appropriate definitions trivially enough, making it not depend on semanticsComputeLib. But then, that would...

This makes me wonder if we shouldn't just merge `semantics` and `semantics/proofs`. Holmake handles big directories better than successive small ones too (at least for the moment).

Also: can you suggest/dictate a naming scheme for regression test files please? I want to test `*computeLib` files (obviously, those in `semantics` and `parsing` have never been so tested) and...

Something has been mis-characterised if a computeLib is needed in `semantics/proofs`.

If they need to be computed/evaluated (i.e., end up in the compiler), then it doesn't seem as if these constants should be in a `proofs` directory. Theorems about them, sure....

Nitpick acknowledged! We already have a `tokenUtils` in `semantics`; it seems to me that analogous names could be used for other theory-stems. Of course, it would probably be better still...

As per 4d95a4936d39, all of the parsing process's selftests execute with the custom compsets from `parsingComputeLib`. I think I need to make sure that `parse_topdecs` or whatever the cf entrypoint...

Something very similar to the calculation of a Huffman tree given the weights for the alphabet is done in HOL’s `examples/computability/kolmog/kraft_ineqScript.sml`. (Weights are specified by giving the desired length of...

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...

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...