gistfile1.rkt

(struct: (state StackPeek InputPeek Stack Input)
         ([name : String]
          [description : String]
          [id : Natural]
          [transition-table : [TT StackPeek InputPeek Stack Input]]
          [predecessors : [Setof (state StackPeek InputPeek Stack Input)]]))

(define-type [State StackPeek InputPeek Stack Input]
  (state StackPeek InputPeek Stack Input))

(struct: (pda-instance StackPeek InputPeek Stack Input)
         ([state : (State StackPeek InputPeek Stack Input)]
          [stack : Stack]
          [input : Input]))

(define-type (PDAInstance StackPeek InputPeek Stack Input)
  (pda-instance StackPeek InputPeek Stack Input))

(define-type [TT StackPeek InputPeek Stack Input]
  [Hash [List StackPeek InputPeek]
        [Stack Input -> (PDAInstance StackPeek
                                     InputPeek
                                     Stack
                                     Input)]])

(: runPDA : (All (StackPeek InputPeek Stack Input)
                 ([PDAInstance StackPeek InputPeek Stack Input]
                  StackPeeker
                  InputPeeker
                  ->
                  [PDAInstance StackPeek InputPeek Stack Input])))