Open Twigonometry opened 2 years ago
mac@mac-ubuntu:~/Documents/Diss/IsabelleDSL$ python3 iDSL_Master.py -t Theories/Stack/Stack.thy -l python -s ./Theories/Stack/user_sessions -b Boilerplate/Stack/stack_boilerplate_python.txt -f ./PrettyPr inters/Stack/stack_pp_python.txt -v --session_type int === Generating DSL === Existing ROOT file found - copying - please make sure this file contains an export_files statement Modified theory file created at /tmp/Stack.thy Building theory file... Build results: ---- Build started for Isabelle/Stack ... Running Stack ... Finished Stack (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.77) export "export/Stack.Stack/code/stack/Stack.hs" ---- Done building Running Haskell file (/tmp/export/Stack.Stack/code/stack/Stack.hs) System Command: ghci /tmp/export/Stack.Stack/code/stack/Stack.hs -e "pp ( Items (Pop (Pop (Push (Int_of_integer (4 :: Integer)) (Pop (Push (Int_of_integer (3 :: Integer)) (Push (Int_of_integer (2 :: Integer)) (Push one_int (Init [] [])))))))))" <interactive>:0:1: error: • No instance for (Printable Int) arising from a use of ‘pp’ • In the expression: pp (Items (Pop (Pop (Push (Int_of_integer (4 :: Integer)) (Pop (Push (Int_of_integer (3 :: Integer)) (Push (Int_of_integer (2 :: Integer)) (Push one_int (Init [] []))))))))) In an equation for ‘it’: it = pp (Items (Pop (Pop (Push (Int_of_integer (4 :: Integer)) (Pop (Push (Int_of_integer (3 :: Integer)) (Push (Int_of_integer (2 :: Integer)) (Push one_int (Init [] []))))))))) Inserting pretty-printed sessions into boilerplate code