Closed Twigonometry closed 2 years ago
Use a function like the following to harvest the translated user sessions and then output them to another file, so they can be used if --auto_test
is specified:
definition test :: "int session" where mytest [code] :
"test = Items (Pop (Pop (Push 4 (Pop (Push 3 (Push 2 (Push (1::int) (Init [] []))))))))"
Currently, user sessions are written in Haskell. This causes a few issues:
Int_of_integer
). This can be confusing, asexport_code
can create strange functions and wrappers, and cannot be known in advanceInstead, we should create some intermediary function that translates isabelle user sessions to haskell, so that we can still run the auto_test cases