atomb / core-to-isabelle Goto Github PK

The existing translator ShallowTest is only meant as a prototype. As such it doesn't have proper handling for the following things:

• Command line arguments
• Output file name
• Theory name inside output file

In terms of generating the output filename and output theory name, it should work like gcc or ghc in that it automatically creates Foo.thy from Foo.hcr. This should be really simple using the filepath module and one of the many command line parsing libraries on hackage.

isa/Examples.thy currently requires the following hand-written boilerplate to make the parser work for case expressions:

translations
"_hcon (XCONST Nothing)" => "CONST Nothing_tag"
"CONST Nothing" <= "_htag (CONST Nothing_tag)"
"_hcon (XCONST Just)" => "CONST Just_tag"
"CONST Just" <= "_htag (CONST Just_tag)"

The halicore_data command should set up these rules automatically.

• Alpha renaming should be a different step
• zdecoding should be a different step
• simplified pretty printing AST

The current translator prototype, ShallowTest, doesn't support functions yet.

It would be nice to allow users to write QuickCheck properties, use them with QuickCheck at first. Then, once they pass enough random tests, users can attempt to prove that they will always succeed. This is probably the easiest way to get users to write properties to prove.

Add an isabelle command like this:
halicore_symbol "<$>" "zlzdzg"

The first parameter is the name as it appears in the Haskell program and the second parameter is the matching z encoding.

The idea is that this would allow halicore syntax snippets to support the Haskell name. The reason for the halicore_syntax command is that it needs to notify the Isabelle parser.

Add support in the translator to catch identifiers that Isabelle cannot parse and output a renaming and a comment to help the programmer see the renaming.

perhaps hcr2thy?