Fix Stack datatype

[Twigonometry]

Stack.thy datatype definition has an error:

datatype session = Items session | Push int session | Pop session | "'a list" "'a list"

Build output:

mac@mac-ubuntu:~/Documents/Diss/IsabelleDSL/Theories/Stack$ isabelle build -e -D .
Running Stack ...
Stack FAILED
(see also /home/mac/.isabelle/Isabelle2021-1/heaps/polyml-5.9_x86_64_32-linux/log/Stack)
*** Extra type variables on right-hand side: "'a"
*** At command "datatype" (line 22 of "~/Documents/Diss/IsabelleDSL/Theories/Stack/Stack.thy")
Unfinished session(s): Stack
0:00:12 elapsed time, 0:00:03 cpu time, factor 0.26

[Twigonometry]

Partial fix in c082fec0 by adding polymorphism. Need to finish #12 to fully fix issue

[Twigonometry]

(partial fix also involved adding constructor to type definition Init "'a list" "'a list")

[Twigonometry]

Progress made by closing #23 - I think polymorphism has fixed this, but issue with running pp arises:

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

Relevant Haskell code snippet:

class Printable a where {
  string_of :: a -> String;
};

newtype Int = Int_of_integer Integer
  deriving Show;

...[snip]...

string_of_list :: forall a. (Printable a) => [a] -> String;
string_of_list (x : xs) = string_of x ++ string_of_list xs;
string_of_list [] = "";

pp :: forall a. (Printable a) => Session a -> String;
pp (Items ses) = pp ses ++ ".items()";
pp (Push i ses) = ((pp ses ++ ".push(") ++ string_of i) ++ ")";
pp (Pop ses) = pp ses ++ ".pop()";
pp (Init llist rlist) = string_of_list llist ++ string_of_list rlist;

[Twigonometry]

See #29