0 | module Control.NCurses

   2 | import NCurses.Core

   3 | import NCurses.Core.Attribute

   5 | import Control.Monad.State

   6 | import Data.Either

   7 | import Data.List

   8 | import Data.Maybe

   9 | import Data.Nat

  10 | import Data.String

  12 | import public NCurses.Core.Color as Color

  13 | import public NCurses.Core.Input as Input

  14 | import public NCurses.Core.SpecialKey as SpecialKey

  15 | import public Control.NCurses.State

  17 | %default total

  19 | public export

  20 | 0 NextIn : (w : State.Window) -> Type

  21 | NextIn w =

  22 |   ifThenElse w.noDelay Maybe id $

  23 |     ifThenElse w.keypad (Either Char Key) Char

  26 | data NCurses : (a : Type) -> CursesState -> CursesState -> Type where

  27 |   Pure : (x : a) -> NCurses a s s

  28 |   Bind : NCurses a s1 s2 -> ((x : a) -> NCurses b s2 s3) -> NCurses b s1 s3

  30 |   Init        : IsInactive s => NCurses () s State.initState

  31 |   DeInit      : IsActive s => NCurses () s Inactive

  32 |   AddWindow   : IsActive s => (name : String) -> Position -> Size -> Maybe (Exists (\c => (Border c, HasColor c s))) -> NCurses () s (addWindow s name)

  33 |   SetWindow   : IsActive s => (name : String) -> HasWindow name s => NCurses () s (setWindow s name)

  34 |   UnsetWindow : IsActive s => HasWindow DefaultWindow s => NCurses () s (setWindow s DefaultWindow)

  35 |   InWindow    : IsActive s => (w : String) -> HasWindow w s => (IsActive (setWindow s w) => HasWindow w (setWindow s w) => InWindow w (setWindow s w) => NCurses () (setWindow s w) (setWindow s w)) -> NCurses () s s

  36 |   AddColor    : IsActive s => (name : String) -> (fg : Color) -> (bg : Color) -> NCurses () s (addColor s name)

  37 |   ModAttr     : IsActive s => AttrCmd s -> NCurses () s s

  38 |   Clear       : IsActive s => NCurses () s s

  39 |   Erase       : IsActive s => NCurses () s s

  40 |   Refresh     : IsActive s => NCurses () s s

  41 |   RefreshAll  : IsActive s => NCurses () s s

  42 |   Output      : IsActive s => OutputCmd s -> NCurses () s s

  43 |   ||| Get the position of the cursor within the current window.

  44 |   GetCursPos  : IsActive s => NCurses Position s s 

  45 |   SetEcho     : IsActive s => (on : Bool) -> NCurses () s (setEcho s on)

  46 |   SetCBreak   : IsActive s => (on : Bool) -> NCurses () s (setCBreak s on)

  47 |   SetNoDelay  : IsActive s => (on : Bool) -> NCurses () s (setNoDelay s on)

  48 |   SetCursor   : IsActive s => CursorVisibility -> NCurses () s s

  49 |   SetKeypad   : IsActive s => (on : Bool) -> NCurses () s (setKeypad s on)

  50 |   ||| Get the position of the current window.

  51 |   GetWinPos   : IsActive s => NCurses Position s s

  52 |   ||| Set the position of the current window.

  53 |   SetWinPos   : IsActive s => Position -> NCurses () s s

  54 |   ||| Get the size of the current window. If `internal` is @True@, then

  56 |   GetWinSize  : IsActive s => (internal : Bool) -> NCurses Size s s

  57 |   ||| Set thte size of the current window.

  58 |   SetWinSize  : IsActive s => Size -> NCurses () s s

  59 |   GetCh       : IsActive s => NCurses (NextIn (currentWindow s)) s s

  61 |   -- TODO: ideally remove this 'escape hatch' and instead specifically allow

  62 |   --       types of IO that are not supported by NCurses directly (like File IO).

  63 |   NIO : IO a -> NCurses a s s

  65 | public export

  66 | IndexedFunctor CursesState CursesState NCurses where

  67 |   map f x = Bind x (\y => Pure (f y))

  69 | public export

  70 | IndexedApplicative CursesState NCurses where

  71 |   pure = Pure

  73 |   ap f x = Bind f (\f' => Bind x (\y => Pure (f' y)))

  75 | public export

  76 | IndexedMonad CursesState NCurses where

  77 |   bind = Bind

  86 | liftIO : IO a -> NCurses a s s

  87 | liftIO = NIO

  92 | init : IsInactive s => NCurses () s State.initState

  93 | init = Init

  97 | deinit : IsActive s => NCurses () s Inactive

  98 | deinit = DeInit

 111 | addWindow : IsActive s =>

 112 |             (name : String)

 113 |          -> Position

 114 |          -> Size

 115 |          -> Maybe (Exists (\c => (Border c, HasColor c s)))

 116 |          -> NCurses () s (addWindow s name)

 117 | addWindow = AddWindow

 121 | public export

 122 | border : IsActive s => 

 123 |          (color : String)

 124 |       -> HasColor color s =>

 125 |          (left   : BorderChar)

 126 |       -> (right  : BorderChar)

 127 |       -> (top    : BorderChar)

 128 |       -> (bottom : BorderChar)

 129 |       -> (topLeft     : BorderChar)

 130 |       -> (topRight    : BorderChar)

 131 |       -> (bottomLeft  : BorderChar)

 132 |       -> (bottomRight : BorderChar)

 133 |       -> Maybe (Exists (\c => (Border c, HasColor c s)))

 134 | border @{_} color @{hasColor} left right top bottom topLeft topRight bottomLeft bottomRight =

 135 |   Just $

 136 |     Evidence color $

 137 |       ( MkBorder { left

 138 |                  , right

 139 |                  , top

 140 |                  , bottom

 141 |                  , topLeft

 142 |                  , topRight

 143 |                  , bottomLeft

 144 |                  , bottomRight

 145 |                  }

 146 |       , hasColor)

 148 | public export

 149 | defaultBorder : IsActive s => 

 150 |                 (color : String)

 151 |              -> HasColor color s =>

 152 |                 Maybe (Exists (\c => (Border c, HasColor c s)))

 153 | defaultBorder color =

 154 |   border color Default Default Default Default

 155 |                Default Default Default Default

 156 |                {s}

 161 | setWindow : IsActive s => (name : String) -> HasWindow name s => NCurses () s (setWindow s name)

 162 | setWindow = SetWindow

 167 | unsetWindow : IsActive s => HasWindow DefaultWindow s => NCurses () s (setWindow s DefaultWindow)

 168 | unsetWindow = UnsetWindow

 173 | inWindow : IsActive s => (name : String) -> HasWindow name s => (IsActive (setWindow s name) => HasWindow name (setWindow s name) => InWindow name (setWindow s name) => NCurses () (setWindow s name) (setWindow s name)) -> NCurses () s s

 174 | inWindow = InWindow

 178 | public export

 179 | hasWindowWithin' : InWindow w s -> HasWindow w s

 180 | hasWindowWithin' {s = (Active _ _ ((MkWindow name _ _) ** Here) _)} IsCurrentWindow = ItHasWindow

 181 | hasWindowWithin' {s = (Active i (y :: xs) ((MkWindow name k d) ** (There x)) c)} p@(IsCurrentWindow) =

 182 |   let c' : InWindow name (Active i xs ((MkWindow name k d) ** x) c) = IsCurrentWindow

 183 |   in moreWindowsHasWindow @{hasWindowWithin' (assert_smaller p c')}

 185 | public export

 187 | hasWindowWithin : InWindow w s => HasWindow w s

 188 | hasWindowWithin @{p} = hasWindowWithin' p

 190 | public export

 192 | identifiesCurrentWindow : InWindow w (Active _ ws _ _) => IdentifiesWindow w ws

 193 | identifiesCurrentWindow @{p} with (hasWindowWithin @{p})

 194 |   identifiesCurrentWindow @{p} | (ItHasWindow @{ident}) = ident

 198 | public export

 200 | setWindowHasWindowStill : HasWindow n s => HasWindow w s => HasWindow n (setWindow s w)

 201 | setWindowHasWindowStill {s = (Active _ (MkWindow n _ _ :: ws) _ _)} @{ItHasWindow  @{Here}} @{ItHasWindow} = ItHasWindow

 202 | setWindowHasWindowStill {s = Active _ [] _ _} @{ItHasWindow  @{Here}} impossible

 203 | setWindowHasWindowStill {s = (Active _ (y :: ws) _ _)} @{ItHasWindow  @{There x}} @{ItHasWindow} = ItHasWindow @{There x}

 204 | setWindowHasWindowStill {s = Active _ [] _ _} @{ItHasWindow  @{There x}} impossible

 206 | public export

 208 | setWindowIsActiveStill : IsActive s => HasWindow w s => IsActive (setWindow s w)

 209 | setWindowIsActiveStill @{ItIsActive} @{ItHasWindow} = ItIsActive

 211 | public export

 213 | setWindowHasColorStill : HasColor c s => HasWindow w s => HasColor c (setWindow s w)

 214 | setWindowHasColorStill {s = (Active _ _ _ (c :: xs))} @{ItHasColor  @{Here}} @{ItHasWindow} = ItHasColor

 215 | setWindowHasColorStill {s = (Active _ _ _ (y :: xs))} @{ItHasColor  @{(There x)}} @{ItHasWindow} = ItHasColor

 219 | public export

 221 | addWindowHasWindowStill : IsActive s => HasWindow n s => HasWindow n (addWindow s w)

 222 | addWindowHasWindowStill {s = (Active _ (_ :: ws) _ _)} @{ItIsActive} @{ItHasWindow @{Here}} = ItHasWindow

 223 | addWindowHasWindowStill {s = (Active _ (_ :: ws) _ _)} @{ItIsActive} @{ItHasWindow @{(There x)}} = ItHasWindow

 225 | public export

 227 | addWindowIsActiveStill : IsActive s => IsActive (addWindow s w)

 228 | addWindowIsActiveStill @{ItIsActive} = ItIsActive

 230 | public export

 232 | addWindowHasColorStill : IsActive s => HasColor c s => HasColor c (addWindow s w)

 233 | addWindowHasColorStill {s = (Active _ _ _ (c :: xs))} @{ItIsActive} @{ItHasColor @{Here}} = ItHasColor

 234 | addWindowHasColorStill {s = (Active _ _ _ (y :: xs))} @{ItIsActive} @{ItHasColor @{(There x)}} = ItHasColor

 236 | public export

 237 | identifiedWindowExists : IdentifiesWindow w ws -> Exists (\k => Exists (\d => lookupWindow w ws = MkWindow w k d))

 238 | identifiedWindowExists {ws = (MkWindow _ _ _ :: windows)} Here = Evidence _ (Evidence _ Refl)

 239 | identifiedWindowExists {ws = ((MkWindow identifier keypad noDelay) :: windows)} (There x) = identifiedWindowExists x

 241 | public export

 243 | inWindowNow : HasWindow w s => InWindow w (setWindow s w)

 244 | inWindowNow @{ItHasWindow @{p}} with (identifiedWindowExists p)

 245 |   inWindowNow @{ItHasWindow  @{p}} | (Evidence k (Evidence d prf)) = rewrite prf in IsCurrentWindow

 259 | clear : IsActive s => NCurses () s s

 260 | clear = Clear

 264 | erase : IsActive s => NCurses () s s

 265 | erase = Erase

 269 | refresh : IsActive s => NCurses () s s

 270 | refresh = Refresh

 274 | refreshAll : IsActive s => NCurses () s s

 275 | refreshAll = RefreshAll

 279 | getPos : IsActive s => NCurses Position s s

 280 | getPos = GetCursPos

 284 | getWindowPos : IsActive s => NCurses Position s s

 285 | getWindowPos = GetWinPos

 289 | setWindowPos : IsActive s => Position -> NCurses () s s

 290 | setWindowPos = SetWinPos

 300 | getWindowSize : IsActive s => (internal : Bool) -> NCurses Size s s

 301 | getWindowSize = GetWinSize

 307 | setWindowSize : IsActive s => Size -> NCurses () s s

 308 | setWindowSize = SetWinSize

 314 | namespace Attribute

 315 |   ||| Add a color to the current NCurses session.

 319 |   export

 320 |   addColor : IsActive s =>

 321 |              (name : String)

 322 |           -> (fg : Color)

 323 |           -> (bg : Color)

 324 |           -> NCurses () s (addColor s name)

 325 |   addColor = AddColor

 327 |   ||| Set the given attribute until it is set again.

 331 |   export

 332 |   enableAttr : IsActive s => Attribute s -> NCurses () s s

 333 |   enableAttr = ModAttr . EnableAttr

 335 |   ||| Unset the given attribute until it is set again.

 339 |   export

 340 |   disableAttr : IsActive s => Attribute s -> NCurses () s s

 341 |   disableAttr = ModAttr . DisableAttr

 343 |   ||| Set an attribute to be applied until it is cleared or

 351 |   export

 352 |   setAttr : IsActive s => Attribute s -> NCurses () s s

 353 |   setAttr = ModAttr . SetAttr

 355 |   ||| Set all the given attributes, replacing any existing attributes.

 358 |   export

 359 |   setAttrs : IsActive s => List (Attribute s) -> NCurses () s s

 360 |   setAttrs = -- efficiency note: NCurses offers a one-function call to achieve

 361 |              -- this by passing a mask of ORed attributes. We could support

 362 |              -- that here in the future.

 363 |              foldr (\a,nc => nc >> enableAttr a) (setAttr Normal)

 365 |   ||| Update the attribute (only supports a single attribute for now) and color

 370 |   export

 371 |   updateAttr : IsActive s => Attribute s -> ColorAttr s -> (length : Maybe Nat) -> NCurses () s s

 372 |   updateAttr attr color length = ModAttr (UpdateAttr attr color length)

 374 |   ||| Set the background color for the current window.

 375 |   export

 376 |   setBackground : IsActive s => ColorAttr s -> NCurses () s s

 377 |   setBackground = ModAttr . SetBg

 383 | namespace Output

 384 |   ||| Print a character to the terminal.

 385 |   export

 386 |   putCh : IsActive s => Char -> NCurses () s s

 387 |   putCh = Output . PutCh

 389 |   ||| Print a string to the terminal _without_ a trailing newline.

 390 |   export

 391 |   putStr : IsActive s => String -> NCurses () s s

 392 |   putStr = Output . PutStr False

 394 |   ||| Print a string to the terminal _with_ a trailing newline.

 395 |   export

 396 |   putStrLn : IsActive s => String -> NCurses () s s

 397 |   putStrLn = Output . PutStr True

 399 |   ||| Draw a vertical line to the current window comprised of the given

 401 |   export

 402 |   drawVerticalLine : IsActive s => Char -> Nat -> NCurses () s s

 403 |   drawVerticalLine = Output .: VLine

 405 |   ||| Draw a horizontal line to the current window comprised of the given

 407 |   export

 408 |   drawHorizontalLine : IsActive s => Char -> Nat -> NCurses () s s

 409 |   drawHorizontalLine = Output .: HLine

 411 |   ||| Move the cursor to a position relative within the current window.

 416 |   export

 417 |   move : IsActive s => Position -> NCurses () s s

 418 |   move = Output . Move

 424 | namespace Input

 425 |   ||| cBreak indicates whether characters typed by the user are delivered to the

 430 |   export

 431 |   setCBreak : IsActive s => (on : Bool) -> NCurses () s (setCBreak s on)

 432 |   setCBreak = SetCBreak

 434 |   ||| echo indicates whether characters typed by the user are printed to the screen

 438 |   export

 439 |   setEcho : IsActive s => (on : Bool) -> NCurses () s (setEcho s on)

 440 |   setEcho = SetEcho

 442 |   ||| Turn "keypad" on or off.

 453 |   export

 454 |   setKeypad : IsActive s => (on : Bool) -> NCurses () s (setKeypad s on)

 455 |   setKeypad = SetKeypad

 457 |   ||| Turn "noDelay" on or off.

 463 |   export

 464 |   setNoDelay : IsActive s => (on : Bool) -> NCurses () s (setNoDelay s on)

 465 |   setNoDelay = SetNoDelay

 467 |   ||| Set the way the cursor is displayed to the user.

 468 |   export

 469 |   setCursor : IsActive s => CursorVisibility -> NCurses () s s

 470 |   setCursor = SetCursor

 471 |   

 472 |   ||| Get the next keypress or character input.

 482 |   export

 483 |   getInput : IsActive s => NCurses (NextIn (currentWindow s)) s s

 484 |   getInput = GetCh

 486 |   -- One would ideally not need to write the following (just use the `getInput` above)

 487 |   -- but in reality it provides a better user experience for downstream development if

 488 |   -- functions can be typed as `IsActive s => IsKeypad s => NoDelay s => NCurses () s s)

 489 |   -- which does not provide Idris enough information at compile time to evaluate @NextIn@, but

 490 |   -- it does allow for the following functions to be used.

 491 |   namespace Char

 492 |     export

 493 |     getChar : IsActive s =>

 494 |               NoKeypad s =>

 495 |               YesDelay s =>

 496 |               NCurses Char s s

 497 |     getChar @{act} @{ItIsNoKeypad} @{ItIsDelay} = GetCh

 499 |     namespace NotDelayed

 500 |       export

 501 |       getChar : IsActive s =>

 502 |                 NoKeypad s =>

 503 |                 NoDelay  s =>

 504 |                 NCurses (Maybe Char) s s

 505 |       getChar @{act} @{ItIsNoKeypad} @{ItIsNoDelay} = GetCh

 507 |   namespace Keypad

 508 |     export

 509 |     getKeyOrChar : IsActive  s =>

 510 |                    YesKeypad s =>

 511 |                    YesDelay  s =>

 512 |                    NCurses (Either Char Key) s s

 513 |     getKeyOrChar @{act} @{ItIsKeypad} @{ItIsDelay} = GetCh

 515 |     namespace NotDelayed

 516 |       export

 517 |       getKeyOrChar : IsActive  s =>

 518 |                      YesKeypad s =>

 519 |                      NoDelay   s =>

 520 |                      NCurses (Maybe (Either Char Key)) s s

 521 |       getKeyOrChar @{act} @{ItIsKeypad} @{ItIsNoDelay} = GetCh

 527 | testRoutine : NCurses () Inactive Inactive

 528 | testRoutine = Indexed.do

 529 |   init

 530 |   insideWindow DefaultWindow

 531 |   addColor "alert" White Red

 532 |   setAttr Underline

 533 |   setAttr (Color (Named "alert"))

 534 |   clear >> refresh

 535 |   putStr "Hello World"

 536 |   setAttr (Color DefaultColors)

 537 |   putStrLn "back to basics."

 538 |   addWindow "win1" (MkPosition 10 10) (MkSize 10 20) Nothing

 539 |   setWindow "win1"

 540 |   insideWindow "win1"

 541 |   inp <- getInput

 542 |   putChIfPossible inp

 543 |   unsetWindow

 544 |   addWindow "win2" (MkPosition 0 0) (MkSize 10 10) (defaultBorder "alert")

 545 |   setWindow "win2"

 546 |   insideWindow "win2"

 547 |   unsetWindow -- back to DefaultWindow

 548 |   inWindow "win2" (insideWindowTwice "win1") -- inside inWindow

 549 |   insideWindow DefaultWindow

 550 |   deinit

 551 |     where

 552 |       putChIfPossible : IsActive s => Either Char Key -> NCurses () s s

 553 |       putChIfPossible (Left x) = putCh x

 554 |       putChIfPossible (Right _) = pure ()

 556 |       getAndPut : IsActive s => YesDelay s => YesKeypad s => NCurses () s s

 557 |       getAndPut = do

 558 |         inp <- getKeyOrChar

 559 |         putChIfPossible inp

 561 |       insideWindow : IsActive s => (w : String) -> InWindow w s => NCurses () s s

 562 |       insideWindow _ = do

 563 |         erase

 564 |         putStr "hello"

 565 |         refresh

 567 |       insideWindowTwice : IsActive s => InWindow "win2" s => (w : _) -> HasWindow w s => NCurses () s s

 568 |       insideWindowTwice w = do

 569 |         erase

 570 |         inWindow w (insideWindow w)

 571 |         refresh

 577 | public export

 578 | keys : List (key, value) -> List key

 579 | keys [] = []

 580 | keys ((x, y) :: xs) = x :: keys xs

 582 | keysInjective : {0 x : _} -> keys (x :: xs) = (y :: ys) -> (Builtin.fst x = y, NCurses.keys xs = ys)

 583 | keysInjective {x = (w, z)} Refl = (Refl, Refl)

 585 | RuntimeBorder : Type

 586 | RuntimeBorder = (ColorPair, Exists (\c => Border c))

 588 | record RuntimeWindow where

 589 |   constructor MkRuntimeWindow

 590 |   props  : State.Window

 591 |   border : Maybe RuntimeBorder

 592 |   win    : Core.Window

 594 | initRuntimeWindow : String -> Maybe RuntimeBorder -> Core.Window -> RuntimeWindow

 595 | initRuntimeWindow name border win = MkRuntimeWindow (initWindow name) border win

 597 | setRWKeypad : (on : Bool) -> RuntimeWindow -> RuntimeWindow

 598 | setRWKeypad on (MkRuntimeWindow (MkWindow identifier keypad noDelay) border win) =

 599 |   MkRuntimeWindow (MkWindow identifier on noDelay) border win

 601 | setRWNoDelay : (on : Bool) -> RuntimeWindow -> RuntimeWindow

 602 | setRWNoDelay on (MkRuntimeWindow (MkWindow identifier keypad noDelay) border win) =

 603 |   MkRuntimeWindow (MkWindow identifier keypad on) border win

 605 | data RuntimeWindows : List State.Window -> Type where

 606 |   Nil : RuntimeWindows []

 607 |   (::) : (rw : RuntimeWindow) -> RuntimeWindows ws -> RuntimeWindows (rw.props :: ws)

 609 | data CurrentWindow : (rw : RuntimeWindow) -> Elem w ws -> RuntimeWindows ws -> Type where

 610 |   Here  : CurrentWindow rw Here (rw :: rws)

 611 |   There : CurrentWindow rw e rws -> CurrentWindow rw (There e) (other :: rws)

 613 | 0 currentWindowPropsPrf : (e : Elem w ws) -> CurrentWindow rw e rws -> rw.props = w

 614 | currentWindowPropsPrf Here Here = Refl

 615 | currentWindowPropsPrf (There e) (There x) = currentWindowPropsPrf e x

 618 | record CursesActive (0 ws : List State.Window) (0 w : (w' ** Elem w' ws)) (0 cs : List String) where

 619 |   constructor MkCursesActive

 620 |   windows : RuntimeWindows ws

 621 |   currentWindow : (rw ** CurrentWindow rw w.snd windows)

 622 |   colors : List (String, ColorPair)

 623 |   {0 csPrf : (keys colors) = cs}

 624 |   currentColor : Maybe ColorPair

 625 |   keyMap : List (Char, Key)

 627 | data RuntimeCurses : CursesState -> Type where

 628 |   RInactive : RuntimeCurses Inactive

 629 |   RActive   : CursesActive ws w cs -> RuntimeCurses (Active i ws w cs)

 631 | getColor : (colors : List (String, ColorPair))

 632 |         -> (0 csPrf : NCurses.keys colors = names)

 633 |         -> (elemPrf : Elem _ names)

 634 |         -> ColorPair

 635 | getColor (z :: zs) csPrf Here = snd z

 636 | getColor [] csPrf (There elemPrf) impossible

 637 | getColor (z :: zs) csPrf (There elemPrf) = getColor zs (snd $ keysInjective csPrf) elemPrf

 639 | getWindow : IdentifiesWindow n ws =>

 640 |             (rws : RuntimeWindows ws)

 641 |          -> (rw ** CurrentWindow rw (lookupWindowPrf n ws) rws)

 642 | getWindow @{Here} (rw@(MkRuntimeWindow (MkWindow n _ _) b win) :: rws') = (rw ** Here)

 643 | getWindow @{There e} (rw'@(MkRuntimeWindow (MkWindow identifier keypad noDelay) border win) :: rws') =

 644 |   bimap id There $ getWindow @{e} rws'

 646 | bumpWindowSameWindow : {0 ws : List State.Window}

 647 |                     -> {0 w : DPair State.Window (flip Elem ws)}

 648 |                     -> {windows : RuntimeWindows ws}

 649 |                     -> {rw : RuntimeWindow}

 650 |                     -> {wPrf : CurrentWindow rw (w.snd) windows}

 651 |                     -> CurrentWindow rw ((State.bumpWindow w).snd) (MkRuntimeWindow (MkWindow n True False) b runtimeWin :: windows)

 652 | bumpWindowSameWindow {w = (w' ** elem)} = There wPrf

 654 | addRuntimeWindow : {0 ws : List State.Window}

 655 |                 -> {0 w : DPair State.Window (flip Elem ws)}

 656 |                 -> (name : String)

 657 |                 -> (border : Maybe RuntimeBorder)

 658 |                 -> (runtimeWin : Core.Window)

 659 |                 -> CursesActive ws w cs

 660 |                 -> CursesActive (initWindow name :: ws) (bumpWindow w) cs

 661 | addRuntimeWindow identifier border runtimeWin (MkCursesActive windows (rw ** wPrf) colors currentColor keyMap {csPrf = csPrf}) =

 662 |   MkCursesActive { windows = initRuntimeWindow identifier border runtimeWin :: windows

 663 |                  , currentWindow = (rw ** bumpWindowSameWindow {wPrf})

 664 |                  , colors

 665 |                  , csPrf

 666 |                  , currentColor

 667 |                  , keyMap

 668 |                  }

 670 | runtimeBorder : RuntimeCurses (Active i ws w cs)

 671 |              -> Exists (\c => (Border c, HasColor c (Active i ws w cs)))

 672 |              -> RuntimeBorder

 673 | runtimeBorder rs@(RActive as) (Evidence color (border, (ItHasColor @{elem}))) =

 674 |   let cp = getColor as.colors as.csPrf elem

 675 |   in  (cp, Evidence color border)

 677 | addRuntimeColor : (name : String)

 678 |                -> (cp : ColorPair)

 679 |                -> CursesActive ws w cs

 680 |                -> CursesActive ws w (name :: cs)

 681 | addRuntimeColor name cp (MkCursesActive windows currentWindow colors currentColor {csPrf} keyMap) =

 682 |   MkCursesActive { windows

 683 |                  , currentWindow

 684 |                  , colors = (name, cp) :: colors

 685 |                  , csPrf  = cong (name ::) csPrf

 686 |                  , currentColor

 687 |                  , keyMap

 688 |                  }

 690 | setRuntimeWindow : IdentifiesWindow name ws

 691 |                 -> CursesActive ws w cs

 692 |                 -> CursesActive ws (lookupWindow name ws ** lookupWindowPrf name ws) cs

 693 | setRuntimeWindow elem (MkCursesActive windows currentWindow colors {csPrf} currentColor keyMap) =

 694 |   MkCursesActive { windows

 695 |                  , currentWindow = getWindow @{elem} windows

 696 |                  , colors

 697 |                  , csPrf

 698 |                  , currentColor

 699 |                  , keyMap

 700 |                  }

 702 | getCoreWindow : CursesActive ws w cs -> Core.Window

 703 | getCoreWindow (MkCursesActive _ ((MkRuntimeWindow props border win) ** _) _ _ _) = win

 705 | getCoreWindow' : IsActive s => RuntimeCurses s -> Core.Window

 706 | getCoreWindow' (RActive as) = getCoreWindow as

 708 | swapKeypad' : {0 origW : State.Window}

 709 |            -> {0 origWs : List State.Window}

 710 |            -> {0 e : Elem origW origWs}

 711 |            -> (on : Bool)

 712 |            -> {rw : _}

 713 |            -> (rws : RuntimeWindows origWs)

 714 |            -> CurrentWindow rw e rws

 715 |            -> (rws' : RuntimeWindows (swapKeypad on origWs e) ** CurrentWindow (setRWKeypad on rw) (swapKeypadPrf on origWs e) rws')

 716 | swapKeypad' on {rw = (MkRuntimeWindow (MkWindow identifier keypad noDelay) b _)} ((MkRuntimeWindow (MkWindow identifier keypad noDelay) b _) :: rws) Here =

 717 |   ((MkRuntimeWindow (MkWindow identifier on noDelay) b _) :: rws ** Here)

 718 | swapKeypad' on {rw = (MkRuntimeWindow (MkWindow y z w) b win)} ((MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther) :: rws') (There {other=(MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther)} x) =

 719 |     let (rws'' ** rw') = swapKeypad' on {rw=MkRuntimeWindow (MkWindow y z w) b win} rws' x

 720 |     in  ((MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther) :: rws'' ** There {other=(MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther)} rw')

 722 | setRuntimeKeypad : (on : Bool)

 723 |                 -> RuntimeCurses (Active i ws w cs)

 724 |                 -> RuntimeCurses (setKeypad (Active i ws w cs) on)

 725 | setRuntimeKeypad on (RActive (MkCursesActive windows (rw ** wPrf) colors {csPrf} currentColor keyMap)) = 

 726 |   let (windows' ** rw') = swapKeypad' on windows wPrf

 727 |   in

 728 |   RActive $

 729 |     MkCursesActive { windows = windows'

 730 |                    , currentWindow = (setRWKeypad on rw ** rw')

 731 |                    , colors

 732 |                    , csPrf

 733 |                    , currentColor

 734 |                    , keyMap

 735 |                    }

 737 | swapNoDelay' : {0 origW : State.Window}

 738 |             -> {0 origWs : List State.Window}

 739 |             -> {0 e : Elem origW origWs}

 740 |             -> (on : Bool)

 741 |             -> {rw : _}

 742 |             -> (rws : RuntimeWindows origWs)

 743 |             -> CurrentWindow rw e rws

 744 |             -> (rws' : RuntimeWindows (swapNoDelay on origWs e) ** CurrentWindow (setRWNoDelay on rw) (swapNoDelayPrf on origWs e) rws')

 745 | swapNoDelay' on {rw = (MkRuntimeWindow (MkWindow identifier keypad noDelay) b _)} ((MkRuntimeWindow (MkWindow identifier keypad noDelay) b _) :: rws) Here =

 746 |   ((MkRuntimeWindow (MkWindow identifier keypad on) b _) :: rws ** Here)

 747 | swapNoDelay' on {rw = (MkRuntimeWindow (MkWindow y z w) b win)} ((MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther) :: rws') (There {other=(MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther)} x) =

 748 |     let (rws'' ** rw') = swapNoDelay' on {rw=MkRuntimeWindow (MkWindow y z w) b win} rws' x

 749 |     in  ((MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther) :: rws'' ** There {other=(MkRuntimeWindow (MkWindow identifier keypad noDelay) border winOther)} rw')

 751 | setRuntimeNoDelay : (on : Bool)

 752 |                  -> RuntimeCurses (Active i ws w cs)

 753 |                  -> RuntimeCurses (setNoDelay (Active i ws w cs) on)

 754 | setRuntimeNoDelay on (RActive (MkCursesActive windows (rw ** wPrf) colors {csPrf} currentColor keyMap)) =

 755 |   let (windows' ** rw') = swapNoDelay' on windows wPrf

 756 |   in

 757 |   RActive $

 758 |     MkCursesActive { windows = windows'

 759 |                    , currentWindow = (setRWNoDelay on rw ** rw')

 760 |                    , colors

 761 |                    , csPrf

 762 |                    , currentColor

 763 |                    , keyMap

 764 |                    }

 766 | coreColor : RuntimeCurses s -> (name : String) -> HasColor name s => ColorPair

 767 | coreColor (RActive (MkCursesActive _ _ colors {csPrf} _ _)) name @{ItHasColor @{elem}} =

 768 |   getColor colors csPrf elem

 770 | coreColorAttr : RuntimeCurses s -> ColorAttr s -> ColorPair

 771 | coreColorAttr _ DefaultColors = defaultColorPair

 772 | coreColorAttr rs (Named name) = (coreColor rs name)

 776 | coreAttr : RuntimeCurses s -> Attribute s -> Attribute

 777 | coreAttr _ Normal    = Normal

 778 | coreAttr _ Underline = Underline

 779 | coreAttr _ Standout  = Standout

 780 | coreAttr _ Reverse   = Reverse

 781 | coreAttr _ Blink     = Blink

 782 | coreAttr _ Dim       = Dim

 783 | coreAttr _ Bold      = Bold

 784 | coreAttr _ Protected = Protected

 785 | coreAttr _ Invisible = Invisible

 786 | coreAttr rs (Color c) = CP $ coreColorAttr rs c

 788 | setCurrentColorPair : IsActive s => ColorPair -> RuntimeCurses s -> RuntimeCurses s

 789 | setCurrentColorPair cp (RActive (MkCursesActive windows currentWindow colors {csPrf} _ keyMap)) =

 790 |   RActive (MkCursesActive windows currentWindow colors {csPrf} (Just cp) keyMap)

 793 | setCurrentColor : IsActive s => ColorAttr s -> RuntimeCurses s -> RuntimeCurses s

 794 | setCurrentColor (Named name @{ItHasColor @{elem}}) rs@(RActive (MkCursesActive windows currentWindow colors {csPrf} _ keyMap)) =

 795 |   setCurrentColorPair (getColor colors csPrf elem) rs

 796 | setCurrentColor DefaultColors (RActive (MkCursesActive windows currentWindow colors {csPrf} _ keyMap)) =

 797 |   RActive (MkCursesActive windows currentWindow colors {csPrf} (Just defaultColorPair) keyMap)

 800 | maybeSetCurrentColor : IsActive s => Attribute s -> RuntimeCurses s -> RuntimeCurses s

 801 | maybeSetCurrentColor (Color attr) rs = setCurrentColor attr rs

 802 | maybeSetCurrentColor _ rs = rs

 805 | maybeUnsetCurrentColor : IsActive s => Attribute s -> RuntimeCurses s -> RuntimeCurses s

 806 | maybeUnsetCurrentColor (Color _) (RActive (MkCursesActive windows currentWindow colors {csPrf} _ keyMap)) =

 807 |   RActive (MkCursesActive windows currentWindow colors {csPrf} Nothing keyMap)

 808 | maybeUnsetCurrentColor _ rs = rs

 810 | currentWindowHasBorder : CursesActive ws w cs -> Bool

 811 | currentWindowHasBorder (MkCursesActive _ ((MkRuntimeWindow _ border _) ** _) _ _ _) = isJust border

 813 | currentWindowHasBorder' : IsActive s => RuntimeCurses s -> Bool

 814 | currentWindowHasBorder' (RActive as) = currentWindowHasBorder as

 816 | modNCursesAttr : HasIO io =>

 817 |                  IsActive s =>

 818 |                  AttrCmd s

 819 |               -> RuntimeCurses s

 820 |               -> io (RuntimeCurses s)

 821 | modNCursesAttr (SetAttr     attr) rs =

 822 |   nSetAttr'      (getCoreWindow' rs) (coreAttr rs attr) $> (maybeSetCurrentColor attr rs)

 823 | modNCursesAttr (EnableAttr  attr) rs =

 824 |   nEnableAttr'   (getCoreWindow' rs) (coreAttr rs attr) $> (maybeSetCurrentColor attr rs)

 825 | modNCursesAttr (DisableAttr attr) rs =

 826 |   nDisableAttr'  (getCoreWindow' rs) (coreAttr rs attr) $> (maybeUnsetCurrentColor attr rs)

 827 | modNCursesAttr (UpdateAttr  attr color len) rs =

 828 |   let cp = case color of

 829 |                 DefaultColors => defaultColorPair

 830 |                 Named name    => coreColor rs name

 831 |   in

 832 |   nChangeAttr' (getCoreWindow' rs) len (coreAttr rs attr) cp $> (maybeSetCurrentColor (Color color) rs)

 833 | modNCursesAttr (SetBg      color) rs =

 834 |   let cp = case color of

 835 |                 DefaultColors => defaultColorPair

 836 |                 Named name    => coreColor rs name

 837 |   in

 838 |   setBackground' (getCoreWindow' rs) cp *> pure rs

 840 | printNCurses : HasIO io =>

 841 |                IsActive s =>

 842 |                OutputCmd s

 843 |             -> RuntimeCurses s

 844 |             -> io (RuntimeCurses s)

 845 | printNCurses (PutCh ch) rs   = nPutCh'          (getCoreWindow' rs) ch   $> rs

 846 | printNCurses (VLine ch n) rs = nVerticalLine'   (getCoreWindow' rs) ch n $> rs

 847 | printNCurses (HLine ch n) rs = nHorizontalLine' (getCoreWindow' rs) ch n $> rs

 849 | printNCurses (Move (MkPosition row col)) rs@(RActive as) =

 850 |   nMoveCursor' (getCoreWindow as) (offset row) (offset col) $> rs

 851 |   where

 852 |     offset : Nat -> Nat

 853 |     offset x = if (currentWindowHasBorder as) then (S x) else x

 855 | printNCurses (PutStr newline str) rs@(RActive as) = do

 856 |     let win = getCoreWindow as

 857 |     (_, fullWidth) <- getMaxSize' win

 858 |     col <- getXPos' win

 859 |     let col' = (if currentWindowHasBorder as then (pred col) else col)

 860 |     nPutStr' win (wrapText fullWidth col' str) $> rs

 861 |   where

 862 |     winWidth : Nat -> (k ** NonZero k)

 863 |     winWidth n =

 864 |       let w = if currentWindowHasBorder as then (n `minus` 2) else n

 865 |       in  case w of 0 => (1 ** %search); (S w') => ((S w') ** %search)

 867 |     lineInfix : String

 868 |     lineInfix = if currentWindowHasBorder as then "\n " else "\n"

 870 |     chunk : (chunkSize : Nat)

 871 |          -> NonZero chunkSize =>

 872 |             (countdown : Nat)

 873 |          -> (rem : List Char)

 874 |          -> (acc : SnocList Char)

 875 |          -> (acc2 : SnocList String)

 876 |          -> List String

 877 |     chunk z _     []        [<]       acc2 = cast acc2

 878 |     chunk z _     []        (sx :< x) acc2 = cast $ (acc2 :< (pack $ cast (sx :< x)))

 879 |     chunk z 0     (x :: xs) acc       acc2 = assert_total $ chunk z z (x :: xs) [<] (acc2 :< (pack $ cast acc))

 880 |     chunk z (S k) (x :: xs) acc       acc2 = chunk z k xs (acc :< x) acc2

 882 |     wrapText : (fullWidth : Nat) -> (currentColumn : Nat) -> String -> String

 883 |     wrapText w c s =

 884 |       let (width ** _) = winWidth w

 885 |           splitText = chunk width (width `minus` c) (unpack s) [<] [<]

 886 |           allTxt = concat (intersperse lineInfix splitText)

 887 |           final = if newline then allTxt ++ lineInfix else allTxt

 888 |       in  final

 891 | drawBorder : HasIO io => Core.Window -> (currentColor : Maybe ColorPair) -> Maybe RuntimeBorder -> io ()

 892 | drawBorder _ _ Nothing = pure ()

 893 | drawBorder win currentColor (Just (cp, (Evidence _ border))) = do

 894 |   nEnableAttr' win (CP cp)

 895 |   nWindowBorder win border.left border.right border.top border.bottom

 896 |                     border.topLeft border.topRight border.bottomLeft border.bottomRight

 897 |   case currentColor of

 898 |        Just cp' => nEnableAttr' win (CP cp')

 899 |        Nothing  => nDisableAttr' win (CP cp)

 902 | drawCurrentBorder : HasIO io => CursesActive ws w cs -> io ()

 903 | drawCurrentBorder (MkCursesActive _ ((MkRuntimeWindow props border win) ** _) _ currentColor _) =

 904 |   drawBorder win currentColor border

 906 | refreshAllRuntime : HasIO io => RuntimeWindows ws -> (currentColor : Maybe ColorPair) -> io ()

 907 | refreshAllRuntime [] _ = pure ()

 908 | refreshAllRuntime ((MkRuntimeWindow _ border win) :: ws) currentColor =

 909 |   drawBorder win currentColor border *> refresh' win *> refreshAllRuntime ws currentColor

 912 | runNCurses : HasIO io => NCurses a s1 s2 -> RuntimeCurses s1 -> io (a, RuntimeCurses s2)

 914 | runNCurses (Pure x) rs = pure (x, rs)

 915 | runNCurses (Bind mod@(ModAttr (DisableAttr x)) f) rs with (f ())

 916 |   runNCurses (Bind mod@(ModAttr (DisableAttr x)) f) rs | (Bind mod2@(ModAttr (EnableAttr y)) f2) =

 917 |     -- skip both modifications if they cancel:

 918 |     if x == y

 919 |        then runNCurses (f2 ()) rs

 920 |        else do

 921 |          ((), rs') <- runNCurses mod rs

 922 |          (x, rs'') <- runNCurses mod2 rs'

 923 |          runNCurses (f2 x) rs''

 924 |   runNCurses (Bind mod@(ModAttr (DisableAttr x)) f) rs | next = do

 925 |     ((), rs') <- runNCurses mod rs

 926 |     runNCurses next rs'

 927 | runNCurses (Bind x f) rs = do

 928 |   (x', rs') <- runNCurses x rs

 929 |   runNCurses (f x') rs'

 930 | runNCurses (NIO ops) rs = do

 931 |   res <- liftIO ops

 932 |   pure (res, rs)

 934 | runNCurses Init RInactive = Prelude.do

 935 |   initNCurses

 936 |   cBreak

 937 |   noEcho

 938 |   keypad True

 939 |   noDelay False

 940 |   win <- stdWindow

 941 |   keyMap <- SpecialKey.keyMap

 942 |   pure ((), RActive $ MkCursesActive [initRuntimeWindow DefaultWindow Nothing win]

 943 |                                      (initRuntimeWindow DefaultWindow Nothing win ** Here)

 944 |                                      []

 945 |                                      {csPrf=Refl}

 946 |                                      Nothing

 947 |                                      keyMap)

 948 | runNCurses DeInit (RActive _) = do

 949 |   deinitNCurses

 950 |   pure ((), RInactive)

 952 | runNCurses (AddWindow @{isActive} name pos size border) rs@(RActive as) = Prelude.do

 953 |   runtimeWin <- newWindow size.rows size.cols pos.row pos.col

 954 |   keypad' runtimeWin True

 955 |   noDelay' runtimeWin False

 956 |   let b = runtimeBorder rs <$> border

 957 |   drawBorder runtimeWin as.currentColor b

 958 |   let as' = addRuntimeWindow name b runtimeWin as

 959 |   when (isJust b) $ -- offset cursor to just inside the border.

 960 |     nMoveCursor' runtimeWin 1 1

 961 |   pure ((), RActive as')

 962 | runNCurses (SetWindow   @{_} name @{ItHasWindow @{elem}}) (RActive as) = pure ((), RActive $ setRuntimeWindow elem as)

 963 | runNCurses (UnsetWindow @{_}      @{ItHasWindow @{elem}}) (RActive as) = pure ((), RActive $ setRuntimeWindow elem as)

 965 | runNCurses Clear rs@(RActive as) = do

 966 |   let win = getCoreWindow as

 967 |   clear' win

 968 |   when (currentWindowHasBorder as) $ -- offset cursor to just inside the border.

 969 |     nMoveCursor' win 1 1

 970 |   pure ((), rs)

 971 | runNCurses Erase   rs@(RActive as) = do

 972 |   let win = getCoreWindow as

 973 |   erase' win

 974 |   when (currentWindowHasBorder as) $ -- offset cursor to just inside the border.

 975 |     nMoveCursor' win 1 1

 976 |   pure ((), rs)

 977 | runNCurses Refresh rs@(RActive as) =

 978 |   let win = getCoreWindow as

 979 |   in  drawCurrentBorder as *> refresh' win $> ((), rs)

 980 | runNCurses RefreshAll rs@(RActive (MkCursesActive windows _ _ currentColor _)) = 

 981 |   -- refresh std window:

 982 |   refresh *>

 983 |   -- followed by all others:

 984 |   refreshAllRuntime windows currentColor $> ((), rs)

 986 | runNCurses (AddColor name fg bg) (RActive as) = do

 987 |   let nextIdx = length as.colors

 988 |   when (nextIdx == 0) startColor

 989 |   cp <- initColorPair nextIdx fg bg

 990 |   let as' = addRuntimeColor name cp as

 991 |   pure ((), RActive as')

 992 | runNCurses (ModAttr cmd) rs = do

 993 |   rs' <- modNCursesAttr cmd rs

 994 |   pure ((), rs')

 995 | runNCurses (Output cmd) rs = do

 996 |   rs' <- printNCurses cmd rs

 997 |   pure ((), rs')

 998 | runNCurses GetCursPos rs = do

 999 |   let win = getCoreWindow' rs

1000 |   y <- getYPos' win

1001 |   x <- getXPos' win

1002 |   let offset : Nat -> Nat = (\coord => if currentWindowHasBorder' rs then (pred coord) else coord)

1003 |   pure (MkPosition (offset y) (offset x), rs)

1004 | runNCurses (SetWinPos pos) rs = moveWindow (getCoreWindow' rs) pos.row pos.col $> ((), rs)

1005 | runNCurses GetWinPos rs = do

1006 |   (y, x) <- getWindowPos' (getCoreWindow' rs)

1007 |   pure ((MkPosition y x), rs)

1008 | runNCurses (SetWinSize size) rs = setWindowSize (getCoreWindow' rs) size.rows size.cols $> ((), rs)

1009 | runNCurses (GetWinSize internal) rs = do

1010 |   (rows, cols) <- getMaxSize' (getCoreWindow' rs)

1011 |   let offset : Nat -> Nat = (\dim => if currentWindowHasBorder' rs && internal then (dim `minus` 2) else dim)