Idris2Doc : Control.NCurses.State

Control.NCurses.State

(source)
Reexports
import public Control.Indexed
import public Data.DPair
import public Data.List.Elem
Definitions
record InputState : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkInput : Bool -> Bool -> InputState

  Projections:
  
.cBreak : InputState -> Bool
  cBreak indicates whether characters typed by the user are delivered to the
  program (via @getCh@) immediately or not. If not, they are delivered when a
  newline is typed (the default behavior for most terminal environments).
  
.echo : InputState -> Bool
  echo indicates whether characters typed by the user are printed to the screen
  by NCurses as well as delivered to @getCh@.

  Hint: 
InWindow w (Active {_:2207} ws {_:2206} {_:2205}) => IdentifiesWindow w ws
.cBreak : InputState -> Bool
  cBreak indicates whether characters typed by the user are delivered to the
  program (via @getCh@) immediately or not. If not, they are delivered when a
  newline is typed (the default behavior for most terminal environments).

  Totality: total
  Visibility: public export
cBreak : InputState -> Bool
  cBreak indicates whether characters typed by the user are delivered to the
  program (via @getCh@) immediately or not. If not, they are delivered when a
  newline is typed (the default behavior for most terminal environments).

  Totality: total
  Visibility: public export
.echo : InputState -> Bool
  echo indicates whether characters typed by the user are printed to the screen
  by NCurses as well as delivered to @getCh@.

  Totality: total
  Visibility: public export
echo : InputState -> Bool
  echo indicates whether characters typed by the user are printed to the screen
  by NCurses as well as delivered to @getCh@.

  Totality: total
  Visibility: public export
initInput : InputState
  Totality: total
  Visibility: public export
data Window : Type
  Windows allow a terminal screen to be divided up and drawn to separately
  with their own relative coordinates.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindow : String -> Bool -> Bool -> Window
  The `keypad` parameter controls whether special keys are supported as single
  inputs.
  Set to true to receive "special keys" as single values rather than composites
  of two or more Chars. For example, arrow keys are represented as two input
  chars, but you will receive @Key@ values for them instead with the @keypad@
  property turned on.
  This is on by default.
  
  The `noDelay` parameter controls whether @getCh@ is blocking or not.
  When noDelay is False, @getCh@ will wait until the user types. Otherwise, @getCh@
  returns immediately and returns @Nothing@ if the user has not input anything.
  
  If a window has a border, it is drawn inside the window's bounds. This also means the
  effective area to draw within is 1 row/column smaller all of the way around the window.
  Moving to row/column 0 will position the cursor just inside the border.

  Hint: 
InWindow w (Active {_:2207} ws {_:2206} {_:2205}) => IdentifiesWindow w ws
identifier : Window -> String
  Totality: total
  Visibility: public export
.identifier : Window -> String
  Totality: total
  Visibility: public export
.keypad : Window -> Bool
  Totality: total
  Visibility: public export
.noDelay : Window -> Bool
  Totality: total
  Visibility: public export
setKeypad : Bool -> Window -> Window
  Totality: total
  Visibility: public export
newKeypadSameIdentity : (on : Bool) -> (w : Window) -> identifier w = identifier (setKeypad on w)
  Totality: total
  Visibility: public export
setNoDelay : Bool -> Window -> Window
  Totality: total
  Visibility: public export
newNoDelaySameIdentity : (on : Bool) -> (w : Window) -> identifier w = identifier (setNoDelay on w)
  Totality: total
  Visibility: public export
initWindow : String -> Window
  Totality: total
  Visibility: public export
data CursesState : Type
  The state of NCurses.
  When active:
  The `input` is the state of input that applies universally.
  The `windows` are the currently available windows in the session, excluding
    the default (or standard) window which is always available.
  The `currentWindow` is the window to be used for input & output. If Nothing,
    the default window is used.
  The `colors` are the currently available colors in the session.
  TODO: parameterize on Eq type to use as color id? Eq a => (colors : List a)

  Totality: total
  Visibility: public export
  Constructors:
  
Inactive : CursesState
  
Active : (0 _ : InputState) -> (0 windows : List Window) -> (0 _ : (w : Window ** Elem w windows)) -> (0 _ : List String) -> CursesState

  Hints:
  
Applicative (Const s)
  
Eq (ColorAttr s)
  
Eq (Attribute s)
  
Functor (Const s)
  
HasColor c s => {auto {conArg:2442} : HasWindow w s} -> HasColor c (setWindow s w)
  
{auto {conArg:2664} : IsActive s} -> HasColor c s => HasColor c (addWindow s w)
  
InWindow w s => HasWindow w s
  
HasWindow n s => {auto {conArg:2243} : HasWindow w s} -> HasWindow n (setWindow s w)
  
{auto {conArg:2536} : IsActive s} -> HasWindow n s => HasWindow n (addWindow s w)
  
{auto {conArg:2814} : HasWindow w s} -> InWindow w (setWindow s w)
  
IndexedApplicative CursesState NCurses
  
IndexedFunctor CursesState CursesState NCurses
  
IndexedMonad CursesState NCurses
  
IsActive s => {auto {conArg:2407} : HasWindow w s} -> IsActive (setWindow s w)
  
{auto {conArg:2641} : IsActive s} -> IsActive (addWindow s w)
  
Monad (Const s)
  
Show (ColorAttr s)
  
Show (Attribute s)
.active : CursesState -> Bool
  Totality: total
  Visibility: public export
0 bumpWindow : (w : Window ** Elem w ws) -> (w : Window ** Elem w (y :: ws))
  Totality: total
  Visibility: public export
data IsActive : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsActive : IsActive (Active {_:3826} {_:3825} {_:3824} {_:3823})

  Hints:
  
{auto {conArg:2664} : IsActive s} -> HasColor c s => HasColor c (addWindow s w)
  
{auto {conArg:2536} : IsActive s} -> HasWindow n s => HasWindow n (addWindow s w)
  
IsActive s => {auto {conArg:2407} : HasWindow w s} -> IsActive (setWindow s w)
  
{auto {conArg:2641} : IsActive s} -> IsActive (addWindow s w)
data IsInactive : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsInactive : IsInactive Inactive
0 currentWindow : (s : CursesState) -> IsActive s => Window
  Totality: total
  Visibility: public export
0 addWindow : (s : CursesState) -> IsActive s => String -> CursesState
  Totality: total
  Visibility: public export
0 addColor : (s : CursesState) -> IsActive s => String -> CursesState
  Totality: total
  Visibility: public export
0 setEcho : (s : CursesState) -> IsActive s => Bool -> CursesState
  Totality: total
  Visibility: public export
0 setCBreak : (s : CursesState) -> IsActive s => Bool -> CursesState
  Totality: total
  Visibility: public export
0 swapKeypad : Bool -> (ws : List Window) -> Elem y ws -> List Window
  Totality: total
  Visibility: public export
0 swapKeypadPrf : (on : Bool) -> (ws : List Window) -> (e : Elem y ws) -> Elem (setKeypad on y) (swapKeypad on ws e)
  Totality: total
  Visibility: public export
0 swapNoDelay : Bool -> (ws : List Window) -> Elem y ws -> List Window
  Totality: total
  Visibility: public export
0 swapNoDelayPrf : (on : Bool) -> (ws : List Window) -> (e : Elem y ws) -> Elem (setNoDelay on y) (swapNoDelay on ws e)
  Totality: total
  Visibility: public export
0 replaceWindow : InputState -> List String -> (ws' : List Window) -> Elem w' ws' -> CursesState
  Totality: total
  Visibility: public export
0 setKeypad : (s : CursesState) -> IsActive s => Bool -> CursesState
  Totality: total
  Visibility: public export
0 setNoDelay : (s : CursesState) -> IsActive s => Bool -> CursesState
  Totality: total
  Visibility: public export
data YesDelay : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsDelay : YesDelay (Active {_:4218} {_:4217} (MkWindow {_:4215} {_:4214} False ** {_:4216}) {_:4213})
data NoDelay : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsNoDelay : NoDelay (Active {_:4241} {_:4240} (MkWindow {_:4238} {_:4237} True ** {_:4239}) {_:4236})
data YesKeypad : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsKeypad : YesKeypad (Active {_:4264} {_:4263} (MkWindow {_:4261} True {_:4260} ** {_:4262}) {_:4259})
data NoKeypad : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsNoKeypad : NoKeypad (Active {_:4287} {_:4286} (MkWindow {_:4284} False {_:4283} ** {_:4285}) {_:4282})
data HasColor : (0 _ : String) -> CursesState -> Type
  Proof that the given color exists in the current
  NCurses session.

  Totality: total
  Visibility: public export
  Constructor: 
ItHasColor : Elem name cs => HasColor name (Active {_:4311} {_:4310} w cs)

  Hints:
  
HasColor c s => {auto {conArg:2442} : HasWindow w s} -> HasColor c (setWindow s w)
  
{auto {conArg:2664} : IsActive s} -> HasColor c s => HasColor c (addWindow s w)
data ColorAttr : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
DefaultColors : ColorAttr s
  
Named : (name : String) -> HasColor name s => ColorAttr s

  Hints:
  
Eq (ColorAttr s)
  
Show (ColorAttr s)
data Attribute : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Normal : Attribute s
  
Underline : Attribute s
  
Standout : Attribute s
  
Reverse : Attribute s
    
Dim : Attribute s
  
Bold : Attribute s
  
Protected : Attribute s
  
Invisible : Attribute s
  
Color : ColorAttr s -> Attribute s

  Hints:
  
Eq (Attribute s)
  
Show (Attribute s)
data AttrCmd : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
SetAttr : Attribute s -> AttrCmd s
  
EnableAttr : Attribute s -> AttrCmd s
  
DisableAttr : Attribute s -> AttrCmd s
  
UpdateAttr : Attribute s -> ColorAttr s -> Maybe Nat -> AttrCmd s
  
SetBg : ColorAttr s -> AttrCmd s
record Border : String -> Type
  A Window border.

  Totality: total
  Visibility: public export
  Constructor: 
MkBorder : BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> Border color

  Projections:
  
.bottom : Border color -> BorderChar
  
.bottomLeft : Border color -> BorderChar
  
.bottomRight : Border color -> BorderChar
  
.left : Border color -> BorderChar
  
.right : Border color -> BorderChar
  
.top : Border color -> BorderChar
  
.topLeft : Border color -> BorderChar
  
.topRight : Border color -> BorderChar
.topRight : Border color -> BorderChar
  Totality: total
  Visibility: public export
.topLeft : Border color -> BorderChar
  Totality: total
  Visibility: public export
.top : Border color -> BorderChar
  Totality: total
  Visibility: public export
.right : Border color -> BorderChar
  Totality: total
  Visibility: public export
.left : Border color -> BorderChar
  Totality: total
  Visibility: public export
.bottomRight : Border color -> BorderChar
  Totality: total
  Visibility: public export
.bottomLeft : Border color -> BorderChar
  Totality: total
  Visibility: public export
.bottom : Border color -> BorderChar
  Totality: total
  Visibility: public export
topRight : Border color -> BorderChar
  Totality: total
  Visibility: public export
topLeft : Border color -> BorderChar
  Totality: total
  Visibility: public export
top : Border color -> BorderChar
  Totality: total
  Visibility: public export
right : Border color -> BorderChar
  Totality: total
  Visibility: public export
left : Border color -> BorderChar
  Totality: total
  Visibility: public export
bottomRight : Border color -> BorderChar
  Totality: total
  Visibility: public export
bottomLeft : Border color -> BorderChar
  Totality: total
  Visibility: public export
bottom : Border color -> BorderChar
  Totality: total
  Visibility: public export
record Position : Type
  An NCuress Position; pass the constructor a row and a column.
  Note that this means the _y position_ comes first. Position starts
  at (0,0) in the upper left corner of the window.

  Totality: total
  Visibility: public export
  Constructor: 
MkPosition : Nat -> Nat -> Position

  Projections:
  
.col : Position -> Nat
  
.row : Position -> Nat
.row : Position -> Nat
  Totality: total
  Visibility: public export
.col : Position -> Nat
  Totality: total
  Visibility: public export
row : Position -> Nat
  Totality: total
  Visibility: public export
col : Position -> Nat
  Totality: total
  Visibility: public export
record Size : Type
  An NCurses Size; pass the constructor rows and then columns.
  Note that this means the _height_ comes first.

  Totality: total
  Visibility: public export
  Constructor: 
MkSize : Nat -> Nat -> Size

  Projections:
  
.cols : Size -> Nat
  
.rows : Size -> Nat
.rows : Size -> Nat
  Totality: total
  Visibility: public export
.cols : Size -> Nat
  Totality: total
  Visibility: public export
rows : Size -> Nat
  Totality: total
  Visibility: public export
cols : Size -> Nat
  Totality: total
  Visibility: public export
data OutputCmd : CursesState -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
PutCh : Char -> OutputCmd s
  
PutStr : Bool -> String -> OutputCmd s
  
VLine : Char -> Nat -> OutputCmd s
  
HLine : Char -> Nat -> OutputCmd s
  
Move : Position -> OutputCmd s
data IdentifiesWindow : (0 _ : String) -> (0 _ : List Window) -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : IdentifiesWindow name (MkWindow name {_:5209} {_:5208} :: windows)
  
There : IdentifiesWindow name windows -> IdentifiesWindow name (w :: windows)

  Hint: 
InWindow w (Active {_:2207} ws {_:2206} {_:2205}) => IdentifiesWindow w ws
elemWindowIdentifies : Elem (MkWindow name {_:5228} {_:5227}) ws -> IdentifiesWindow name ws
  Proof that an @Elem@ for a window can produce a named window identifier.

  Totality: total
  Visibility: public export
data HasWindow : (0 _ : String) -> CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItHasWindow : IdentifiesWindow name ws => HasWindow name (Active {_:5285} ws {_:5284} {_:5283})

  Hints:
  
HasColor c s => {auto {conArg:2442} : HasWindow w s} -> HasColor c (setWindow s w)
  
InWindow w s => HasWindow w s
  
HasWindow n s => {auto {conArg:2243} : HasWindow w s} -> HasWindow n (setWindow s w)
  
{auto {conArg:2536} : IsActive s} -> HasWindow n s => HasWindow n (addWindow s w)
  
{auto {conArg:2814} : HasWindow w s} -> InWindow w (setWindow s w)
  
IsActive s => {auto {conArg:2407} : HasWindow w s} -> IsActive (setWindow s w)
moreWindowsHasWindow : HasWindow name (Active i xs (MkWindow name k d ** x) c) => HasWindow name (Active i (y :: xs) (MkWindow name k d ** There x) c)
  Totality: total
  Visibility: public export
DefaultWindow : String
  Totality: total
  Visibility: public export
0 lookupWindow : (name : String) -> (ws : List Window) -> IdentifiesWindow name ws => Window
  Totality: total
  Visibility: public export
lookupFindsIdentifier : {auto {conArg:5426} : IdentifiesWindow w ws} -> lookupWindow w ws .identifier = w
  Totality: total
  Visibility: public export
0 lookupWindowPrf : (name : String) -> (ws : List Window) -> {auto {conArg:5467} : IdentifiesWindow name ws} -> Elem (lookupWindow name ws) ws
  Proof that looking up a window by a name proven to identify a window in the given
  list of windows will result in an element of that list of windows.

  Totality: total
  Visibility: public export
0 setWindow : (s : CursesState) -> (name : String) -> HasWindow name s => CursesState
  Totality: total
  Visibility: public export
data InWindow : (0 _ : String) -> CursesState -> Type
  Totality: total
  Visibility: public export
  Constructor: 
IsCurrentWindow : InWindow name (Active {_:5556} ws (MkWindow name {_:5554} {_:5553} ** {_:5555}) {_:5552})

  Hints:
  
InWindow w s => HasWindow w s
  
InWindow w (Active {_:2207} ws {_:2206} {_:2205}) => IdentifiesWindow w ws
  
{auto {conArg:2814} : HasWindow w s} -> InWindow w (setWindow s w)
initWindows : List Window
  Totality: total
  Visibility: public export
initState : CursesState
  Totality: total
  Visibility: public export