Incomplete I'm afraid.
This relevant ancestor theory wasn't being used, and so the test-suite missed out on the changes made in 02d4772.
This stops the infinite loop that was occurring when cmlTestsTheory built.
Prove soundness, completeness, and that ptree conversion is total. Note in passing that semantics/cmlPtreeConversion is not converting a parse-tree corresponding to the "bool" type-operator to TC_bool, but rather to TC_name (Short "bool") Also, the list of possible tctors is missing TC_list.
…rsing For theorems saved or stored, the [cakeml/parsing] notation on the end of the theorem name works. For definitions, explicit calls to store_attribute are required. Then it's possible to get the theorems stored with a call to ThmSetData.all_data "cakeml/parsing"
Will break if you are not running a HOL with commit 51adc5dfa2
Also fix up constructor names that are qualified with a structure name, allowing one to write List.nil and have it recognised as something that might appear in a pattern, for example.
Also allow for infix @ at the same point in the grammar. This symbol just translates to a standard symbol applied to two arguments. Also, in passing, fix relational operators to be left-associative, making things like 3 < 4 = true legitimate. Soundness and completeness proved. One test. Still to come: list expressions with [...], and patterns with :: and [...]
PEG adjusted, and soundness reproved.