module UI.Curses

%include C "curses.h"
%include C "cursesrun.h"
%link C "cursesrun.o"
%lib C "curses"

%access private

||| A window, also known as screen.
|||
||| This is used to interface with certain C functions.
data Window = MkWindow Ptr

||| The modes that `getCh` can use to get characters.
public export
data GetChMode : Type where
  ||| `getCh` waits for the user to press a key, but doesn't affect interrupt
  ||| and control flow characters.
  WaitForever           : GetChMode
  ||| `getCh` waits for the user to press a key, allows the program to determine
  ||| what happens when interrupt or control flow characters are encountered.
  WaitForeverRaw        : GetChMode
  ||| `getCh` waits for a certain amount of time before returning Nothing.
  ||| Doesn't affect interrupt and control flow characters.
  ||| @k tenths of a second `getCh` will wait
  Wait                  : (k : Nat) -> GetChMode
  ||| `getCh` waits for the user to press a key, but the program doesn't
  ||| receive any information about which keys have been pressed until a
  ||| newline character is encountered. Doesn't affect interrupt and control
  ||| flow characters.
  WaitForeverLinebuf    : GetChMode
  ||| `getCh` waits for the user to press a key, but the program doesn't
  ||| receive any information about which keys have been pressed until a newline
  ||| character is encountered. Allows the program to determine what happens
  ||| when interrupt or control flow characters are encountered.
  WaitForeverLinebufRaw : GetChMode

||| These are the color that are defined once curses is initialized.
|||
||| Note that some terminals may display some colors differently.
public export
data Color = Black
           | Red
           | Green
           | Yellow
           | Blue
           | Magenta
           | Cyan
           | White

||| This is necessary to use colors.
public export
data ColorPair : Type where
  ||| Use this constructor to make a ColorPair.
  ||| @i index of the ColorPair
  ||| @foreground foreground color
  ||| @background background color
  MkColorPair : (i : Nat) -> (foreground : Color) -> (background : Color) ->
    ColorPair

||| These are the attributes that can be used to print text in various ways.
|||
||| Note that some terminals may not support all of these attributes.
public export
data Attr : Type where
  ||| Prints text normally.
  Normal      : Attr
  ||| Highlights the printed text.
  Standout    : Attr
  ||| Puts a line under printed text.
  Underline   : Attr
  ||| Reverses the foreground and background colors.
  Reverse     : Attr
  ||| Prints blinking text.
  Blink       : Attr
  ||| Prints half bright text.
  Dim         : Attr
  ||| Prints bold text.
  Bold        : Attr
  ||| Prints with an alternate character set.
  AltCharSet  : Attr
  ||| Prints out invisible text.
  Invis       : Attr
  ||| Protects printed text.
  Protect     : Attr

namespace Cursor
  ||| These are the available cursor states.
  public export
  data CursorState = Invisible
                   | Normal
                   | VeryVisible

||| These are special characters, which can be converted into regular
||| Characters with the function `specialChar`.
public export
data SpecialChar = Escape
                 | Backspace
                 | Up
                 | Down
                 | Left
                 | Right
                 | F1
                 | F2
                 | F3
                 | F4
                 | F5
                 | F6
                 | F7
                 | F8
                 | F9
                 | F10
                 | F11
                 | F12
                 | Insert
                 | Delete
                 | Home
                 | End
                 | PageUp
                 | PageDown
                 | Tab
                 | Enter

||| Converts a `SpecialChar` into a regular `Char`.
public export
specialChar : SpecialChar -> Char
specialChar Escape    = '\ESC'
specialChar Backspace = '\263'
specialChar Up        = '\259'
specialChar Down      = '\258'
specialChar Left      = '\260'
specialChar Right     = '\261'
specialChar F1        = '\410'
specialChar F2        = '\266'
specialChar F3        = '\267'
specialChar F4        = '\268'
specialChar F5        = '\269'
specialChar F6        = '\270'
specialChar F7        = '\271'
specialChar F8        = '\272'
specialChar F9        = '\273'
specialChar F10       = '\274'
specialChar F11       = '\275'
specialChar F12       = '\276'
specialChar Insert    = '\331'
specialChar Delete    = '\330'
specialChar Home      = '\262'
specialChar End       = '\360'
specialChar PageUp    = '\339'
specialChar PageDown  = '\338'
specialChar Tab       = '\t'
specialChar Enter     = '\n'

intToCursorState : Int -> Maybe CursorState
intToCursorState 0 = Just Invisible
intToCursorState 1 = Just Normal
intToCursorState 2 = Just VeryVisible
intToCursorState _ = Nothing

cursorStateToInt : CursorState -> Int
cursorStateToInt Invisible   = 0
cursorStateToInt Normal      = 1
cursorStateToInt VeryVisible = 2

colorToInt : Color -> Int
colorToInt Black   = 0
colorToInt Red     = 1
colorToInt Green   = 2
colorToInt Yellow  = 3
colorToInt Blue    = 4
colorToInt Magenta = 5
colorToInt Cyan    = 6
colorToInt White   = 7

attrToInt : Attr -> Int
attrToInt Normal     = 0
attrToInt Standout   = pow 2 16
attrToInt Underline  = pow 2 17
attrToInt Reverse    = pow 2 18
attrToInt Blink      = pow 2 19
attrToInt Dim        = pow 2 20
attrToInt Bold       = pow 2 21
attrToInt AltCharSet = pow 2 22
attrToInt Invis      = pow 2 23
attrToInt Protect    = pow 2 24

cBool : Bool -> Int
cBool True  = 1
cBool False = 0

idrBool : Int -> Bool
idrBool = (/= 0)

errOkToBool : Int -> Bool
errOkToBool = (/= (-1))

||| Returns the standard window.
stdScr : IO Window
stdScr = map MkWindow $ foreign FFI_C "stdScr" (IO Ptr)

noDelay : Bool -> IO ()
noDelay bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "nodelay" (Ptr -> Int -> IO ()) scr (cBool bf)

halfDelay : Int -> IO ()
halfDelay delay = foreign FFI_C "halfdelay" (Int -> IO ()) delay

||| Enables or disables the reading of function keys, arrow keys, and so on.
||| This is turned on by default.
||| @bf  if `True`, enables reading, if `False`, disables it
export
keypad : (bf : Bool) -> IO ()
keypad bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "keypad" (Ptr -> Int -> IO ()) scr (cBool bf)

meta : Bool -> IO ()
meta bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "meta" (Ptr -> Int -> IO ()) scr (cBool bf)

leaveOk : Bool -> IO Int
leaveOk bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "leaveok" (Ptr -> Int -> IO Int) scr (cBool bf)

nl : Bool -> IO ()
nl True  = foreign FFI_C "nl"   (IO ())
nl False = foreign FFI_C "nonl" (IO ())

||| `echo` determines whether a character will be printed when the user presses
||| a key
||| @bf whether or not the echo will be on
export
echo : (bf : Bool) -> IO ()
echo False = foreign FFI_C "noecho" (IO ())
echo True  = foreign FFI_C "echo"   (IO ())

cBreak : Bool -> IO ()
cBreak True  = foreign FFI_C "cbreak"   (IO ())
cBreak False = foreign FFI_C "nocbreak" (IO ())

raw : Bool -> IO ()
raw True  = foreign FFI_C "raw"   (IO ())
raw False = foreign FFI_C "noraw" (IO ())

||| Return `True` if the terminal supports colors, false otherwise. This
||| function may not return correct results if `startCurses` has not been
||| called.
export
hasColors : IO Bool
hasColors = map idrBool $ foreign FFI_C "has_colors" (IO Int)

||| Refreshes the screen. It is unlikely that a program needs to manually
||| call this function.
export
refresh : IO ()
refresh = foreign FFI_C "refresh" (IO ())

||| This function must be called before colors can be used. Note that not all
||| terminals support colors. Use `hasColors` to find out whether the terminal
||| the program runs on supports colors.
export
startColor : IO ()
startColor = refresh *> foreign FFI_C "start_color" (IO ())

initScr : IO Window
initScr = map MkWindow $ foreign FFI_C "initscr" (IO Ptr)

||| Terminates curses. This should *always* be called before the program
||| terminates.
export
endWin : IO ()
endWin = foreign FFI_C "endwin" (IO ())

||| Returns the size of the standard window.
|||
||| The format is `(lines, columns)`.
export
scrSize : IO (Int, Int)
scrSize = [| MkPair (foreign FFI_C "getLines" (IO Int))
                    (foreign FFI_C "getCols"  (IO Int)) |]

||| Initializes a color pair.
initPair : ColorPair -> IO ()
initPair (MkColorPair natIndex colorFG colorBG) =
  foreign FFI_C "init_pair" (Int -> Int -> Int -> IO ()) (i + 1) fg bg
  where
    i : Int
    i = toIntNat natIndex
    fg  : Int
    fg  = colorToInt colorFG
    bg  : Int
    bg  = colorToInt colorBG

setAttr : Int -> IO ()
setAttr a = foreign FFI_C "attrset" (Int -> IO ()) a

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s        the string that will be printed
||| @maxChars specifies the maximum number of characters that will be printed
export
addNStr : (s : String) -> (maxChars : Nat) -> IO ()
addNStr s n = foreign FFI_C "addnstr" (String -> Int -> IO ()) s (toIntNat n)

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s the string that will be printed
export
addStr : (s: String) -> IO ()
addStr s = foreign FFI_C "addstr" (String -> IO ()) s

||| Prints a character to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @c the character that will be printed
export
addCh : (c : Char) -> IO ()
addCh c = foreign FFI_C "addch" (Char -> IO ()) c

||| Clears the screen to the end of the line.
export
clrToEol : IO ()
clrToEol = foreign FFI_C "clrtoeol" (IO ())

||| Moves the cursor to the specified coordinates.
||| Returns `True` if the cursor was moved, `False` otherwise.
||| @y the line to which the cursor will move (counting starts at 0)
||| @x the column to which the cursor will move (counting starts at 0)
export
move : (y : Int) -> (x : Int) -> IO Bool
move y x = map errOkToBool $ foreign FFI_C "move" (Int -> Int -> IO Int) y x

curs_set : Int -> IO Int
curs_set x = foreign FFI_C "curs_set" (Int -> IO Int) x

||| Sets the cursor state. Returns `Nothing`, if the specified cursor state
||| cannot be set, and `Just` the previous cursor state otherwise.
||| @cs the cursor state that will be set
export
cursSet : (cs : CursorState) -> IO $ Maybe CursorState
cursSet Invisible = leaveOk True  *> curs_set 0 >>= pure . intToCursorState
cursSet cs = leaveOk False *> curs_set (cursorStateToInt cs) >>=
  pure . intToCursorState

||| Returns the current cursor position.
||| The format is `(line, column)`.
export
getYX : IO (Int, Int)
getYX = do
  (MkWindow scr) <- stdScr
  [| MkPair (foreign FFI_C "getY" (Ptr -> IO Int) scr)
            (foreign FFI_C "getX" (Ptr -> IO Int) scr) |]

||| Returns the highest line and column the cursor can be at.
||| The format is `(line, column)`.
export
getMaxYX : IO (Int, Int)
getMaxYX = scrSize >>= \(row, col) => pure (row - 1, col - 1)

getch : IO Int
getch = foreign FFI_C "getch" (IO Int)

||| Clears the screen.
export
clear : IO ()
clear = foreign FFI_C "clear" (IO ())

colorPair : Int -> IO Int
colorPair i = foreign FFI_C "COLOR_PAIR" (Int -> IO Int) (i + 1)

||| Sets all given attributes and the specified colors. Note that this function
||| will not affect colors unless the terminal supports colors (which you can
||| check with `hasColors`) and `startColors` has been called.
||| @attrs  the attributes that will be set
||| @colors if this is `Nothing`, the default colors will be used, which are
|||           usually white on black; if this is not `Nothing`, the specified
|||           Pair will be initialized and used - note that if characters on the
|||           screen use the pair with index *i*, and the pair with index *i* is
|||           then reinitialized with different colors, the characters that are
|||           already on the screen will change their color
export
setAttrAndColor : (attrs : List Attr) -> (colors : Maybe ColorPair) -> IO ()
setAttrAndColor as c = do
    refresh
    for_ c initPair
    col <- colorAttr
    setAttr $ combineAttr col as
  where
    combineAttr : Int -> List Attr -> Int
    combineAttr col = foldr prim__orInt col . map attrToInt
    intIndex : ColorPair -> Int
    intIndex (MkColorPair i _ _) = toIntNat i
    colorAttr : IO Int
    colorAttr = maybe (pure 0) (colorPair . intIndex) c

||| Advances the cursor to the next position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
export
moveNextCh : IO Bool
moveNextCh = do
  (maxY, maxX) <- getMaxYX
  (y, x) <- getYX
  let (newY, newX, success) = if x >= maxX
    then if y >= maxY then (maxY, maxX, False) else (y + 1, 0, True)
    else (y, x + 1, True)
  move newY newX
  pure success

||| Moves the cursor to the previous position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
export
movePrevCh : IO Bool
movePrevCh = do
  (maxY, maxX) <- getMaxYX
  (y, x) <- getYX
  let (newY, newX, success) = if x <= 0
    then if y <= 0 then (0, 0, False) else (y - 1, maxX, True)
    else (y, x - 1, True)
  move newY newX
  pure success

||| Returns `Just` a character, or `Nothing` if the `GetChMode` is `Wait k` and
||| the time runs out. See `GetChMode` for more information.
export
getCh : IO $ Maybe Char
getCh = do
  refresh
  c <- getch
  pure $ if c == (-1) then Nothing else pure $ chr c

||| Returns a character once the user presses a key. This function is affected
||| by whether or not the `GetChMode` is a "raw" or a "linebuf" mode.
export
forceCh : IO Char
forceCh = do
  refresh
  c <- getch
  if c == (-1) then forceCh else pure $ chr c

||| Returns a `String` the user enters. This function is affected by whether or
||| not the `GetChMode` is a "raw" mode.
||| @useEcho  if `True`, the user will see the `String` they enter
||| @setEcho  if `True`, echo will be on after the `String` has been returned,
|||             otherwise, echo will be off
export
getStr : (useEcho : Bool) -> (setEcho : Bool) -> IO String
getStr useEcho setEcho = do
    echo useEcho
    (y, x) <- getYX
    str <- map reverse $ getRawStr y x ""
    echo setEcho
    pure str
  where
    mayMovePrev : IO Bool
    mayMovePrev = if useEcho then movePrevCh else pure False
    mayMoveNext : IO Bool
    mayMoveNext = if useEcho then moveNextCh else pure False
    mayMove : Int -> Int -> IO Bool
    mayMove y x = if useEcho then move y x else pure False
    mayAddCh : Char -> IO ()
    mayAddCh c = when useEcho $ addCh c
    safeTail : List a -> List a
    safeTail [] = []
    safeTail (_ :: xs) = xs
    getRawStr : Int -> Int -> String -> IO String
    getRawStr initY initX str = do
      (preY, preX) <- getYX
      c <- forceCh
      (y, x) <- getYX
      case c of
        '\n'   => mayMove preY preX *> pure str
        '\263' => if y <= initY && x < initX
          then mayMove preY preX *> getRawStr initY initX str
          else do if (preY, preX) == (y, x)
                    then mayMovePrev *> mayAddCh ' ' *> mayMovePrev *> pure ()
                    else mayAddCh ' ' *> mayMove y x *> pure ()
                  getRawStr initY initX . pack . safeTail . unpack $ str
        char => getRawStr initY initX $ strCons char str

||| Sets the mode `getCh` will operate in.
export
setGetChMode : GetChMode -> IO ()
setGetChMode WaitForever           = raw False *> cBreak True  *> noDelay False
setGetChMode WaitForeverRaw        = raw True                  *> noDelay False
setGetChMode (Wait Z)              = raw False *> cBreak True  *> noDelay True
setGetChMode (Wait (S k))          = halfDelay (toIntNat k)    *> noDelay False
setGetChMode WaitForeverLinebuf    = raw False *> cBreak False *> noDelay False
setGetChMode WaitForeverLinebufRaw = raw True  *> cBreak False *> noDelay False

||| Use this function to start curses. Note that `endWin` should *always* be
||| called before the program terminates.
||| @getChMode    the mode that `getCh` will use
export
startCurses : (getChMode : GetChMode) -> IO ()
startCurses getChMode = do
  initScr
  nl True
  echo False
  keypad True
  meta True
  leaveOk False
  setGetChMode getChMode
