----------------------------------------------------------------------------------------------------

-- discrete automata with I/O (IODA, not indexed by DFA)
-- NOTE: states and labels are allowed not to be finite
-- see elsewhere for indexed version (IODFA)


----------------------------------------------------------------------------------------------------

{-# OPTIONS --guardedness --sized-types #-}

module IODA where

open import Parser public


----------------------------------------------------------------------------------------------------

module IODAThings where
  record IODA {𝓇 π“ˆ 𝓁 𝓍 π“Ž} : Set (lsuc (𝓇 βŠ” π“ˆ βŠ” 𝓁 βŠ” 𝓍 βŠ” π“Ž)) where
    constructor mkIODA
    field
      {State}      : Set π“ˆ
      {Label}      : Set 𝓁
      {Input}      : Set 𝓍
      {Output}     : Set π“Ž
      initialState : State
      _β‡’βŸ¨_,_⟩_,_  : State β†’ Label β†’ Input β†’ State β†’ Output β†’ Set 𝓇
      transition   : State β†’ Label β†’ Input β†’ Maybe (State Γ— Output)
      correctness  : βˆ€ q l x qβ€² y β†’ q β‡’βŸ¨ l , x ⟩ qβ€² , y ⇔ transition q l x ≑ just (qβ€² , y)

    -- machine that simulates this IODA
    -- NOTE: stops only when invalid transition is attempted
    simMachine : State β†’ ∞Machine (Label Γ— Input) (Maybe (State Γ— Output))
    simMachine q .on (l , x) with transition q l x
    ... | just (qβ€² , y)        = just (qβ€² , y) , just (simMachine qβ€²)
    ... | nothing              = nothing , nothing

  -- textual user interface for IODA
  record TUI-IODA {𝓇 π“ˆ 𝓁 𝓍 π“Ž ℯ₁ β„―β‚‚} : Set (lsuc (𝓇 βŠ” π“ˆ βŠ” 𝓁 βŠ” 𝓍 βŠ” π“Ž βŠ” ℯ₁ βŠ” β„―β‚‚)) where
    constructor mkTUI-IODA
    field
      ioda               : IODA {𝓇} {π“ˆ} {𝓁} {𝓍} {π“Ž}
      {LabelParserErr}   : Set ℯ₁
      {InputParserErr}   : Set β„―β‚‚

    open IODA ioda public

    LabelParser : Set (𝓁 βŠ” ℯ₁)
    LabelParser = ∞Machine Term (Either LabelParserErr Label)

    InputParser : Set (𝓍 βŠ” β„―β‚‚)
    InputParser = ∞Machine Term (Either InputParserErr Input)

    field
      showDot            : String
      showState          : State β†’ String
      showLabel          : Label β†’ String
      showInput          : Input β†’ String
      showOutput         : Output β†’ String
      showLabelParserErr : LabelParserErr β†’ String
      showInputParserErr : InputParserErr β†’ String
      awaitLabel         : LabelParser
      awaitInput         : InputParser

    parseLabel : Term β†’ Either LabelParserErr Label
    parseLabel tm = ∞MachineThings.GetEither.step awaitLabel tm

    parseInput : Term β†’ Either InputParserErr Input
    parseInput tm = ∞MachineThings.GetEither.step awaitInput tm

  open IODA public

open IODAThings public using (IODA ; mkIODA ; TUI-IODA ; mkTUI-IODA)


----------------------------------------------------------------------------------------------------

-- textual user interface interpreter for arbitrary IODA

module TUIInterpreter-IODA {𝓇} (tui : TUI-IODA {𝓇}) where
  open StdIO public using (_>>=_ ; _>>_)
  open TUI-IODA tui

  data Err : Set where
    badTerm       : TermParserErr β†’ Err
    badInput      : InputParserErr β†’ Err
    badLabel      : LabelParserErr β†’ Err
    badCmd        : Term β†’ Err
    badTransition : Err

  showErr : Err β†’ String
  showErr (badTerm err)  = showTermParserErr err
  showErr (badInput err) = showInputParserErr err
  showErr (badLabel err) = showLabelParserErr err
  showErr (badCmd tm)    = "invalid command '" ++ showTerm tm ++ "'"
  showErr badTransition  = "invalid transition"

  data Cmd : Set where
    quit  : Cmd
    reset : Cmd
    put   : Label β†’ Input β†’ Cmd

  readPutCmd : Term β†’ Either Err Cmd
  readPutCmd (list (tm₁ ∷ tmβ‚‚ ∷ [])) with parseLabel tm₁ | parseInput tmβ‚‚
  ... | fail err | _                   = fail (badLabel err)
  ... | ok _     | fail err            = fail (badInput err)
  ... | ok l     | ok x                = ok (put l x)
  readPutCmd tm                      = fail (badCmd tm)

  readCmd : String β†’ Either Err Cmd
  readCmd str                   with parseTerm (lex str)
  ... | fail err                  = fail (badTerm err)
  ... | ok (atom ":quit"  ∷ [])   = ok quit
  ... | ok (atom ":reset" ∷ [])   = ok reset
  ... | ok (tm            ∷ [])   = readPutCmd tm
  ... | ok tms                    = readPutCmd (list tms)

  data Action : Set where
    prompt : State β†’ Action
    get    : Output β†’ Action
    warn   : Err β†’ Action

  doAction : Action β†’ IO Unit
  doAction (prompt q) = do putStrLn ""
                           putStrLn (showState q)
                           putStr "> "
  doAction (get y)    = putStrLn (showOutput y)
  doAction (warn err) = putStrLn ("error: " ++ showErr err)

  -- de-accumulate
  stringFrom : List Char β†’ String
  stringFrom acc = String.fromList (reverse acc)

  Interpreter : Set
  Interpreter = ∞Machine Char (List Action)

  mutual
    awaitCmd : State β†’ List Char β†’ Interpreter
    awaitCmd q acc .on '\n' with readCmd (stringFrom acc)
    ... | fail err            = continue [ warn err ] q
    ... | ok quit             = [] , nothing
    ... | ok reset            = continue [] initialState
    ... | ok (put l x)        with transition q l x -- NOTE: direct computation here
    ... |   just (qβ€² , y)       = continue [ get y ] qβ€²
    ... |   nothing             = continue [ warn badTransition ] q
    awaitCmd q acc .on c    = [] , just (awaitCmd q (c ∷ acc))

    continue : List Action β†’ State β†’ List Action Γ— Maybe Interpreter
    continue as q = as Listβ€².++ [ prompt q ] , just (awaitCmd q [])

  handleTUI : IO Polyunit
  handleTUI = do setBuffering stdout noBuffering
                 flush stdout
                 putStrLn showDot
                 cs ← getChars
                 comapMβ€² (mapM doAction) ([ prompt initialState ] ∷ β™―
                   corun (awaitCmd initialState []) cs)


----------------------------------------------------------------------------------------------------