0 | module Control.NCurses.State

  2 | import NCurses.Core

  3 | import NCurses.Core.Color

  4 | import NCurses.Core.Attribute

  5 | import NCurses.Core.SpecialKey

  6 | import NCurses.Core.Input

  8 | import public Control.Indexed

  9 | import public Data.DPair

 10 | import public Data.List.Elem

 12 | %default total

 14 | public export

 15 | record InputState where

 16 |   constructor MkInput

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

 20 |   cBreak : Bool

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

 23 |   echo   : Bool

 25 | public export

 26 | initInput : InputState

 27 | initInput = MkInput { cBreak  = True

 28 |                     , echo    = False

 29 |                     }

 33 | public export

 34 | data Window : Type where

 35 |   ||| The `keypad` parameter controls whether special keys are supported as single

 50 |   MkWindow : (identifier : String)

 51 |           -> (keypad : Bool)

 52 |           -> (noDelay : Bool) -> Window

 54 | public export

 55 | identifier : State.Window -> String

 56 | identifier (MkWindow i _ _) = i

 58 | public export

 59 | (.identifier) : State.Window -> String

 60 | (.identifier) = identifier

 62 | public export

 63 | (.keypad) : State.Window -> Bool

 64 | (.keypad) (MkWindow _ k _) = k

 66 | public export

 67 | (.noDelay) : State.Window -> Bool

 68 | (.noDelay) (MkWindow _ _ d) = d

 70 | public export

 71 | setKeypad : (on : Bool) -> State.Window -> State.Window

 72 | setKeypad on (MkWindow i _ d) = MkWindow i on d

 74 | public export

 75 | newKeypadSameIdentity : (on : Bool) -> (w : State.Window) -> (identifier w) === (identifier (setKeypad on w))

 76 | newKeypadSameIdentity on (MkWindow identifier keypad noDelay) = Refl

 78 | public export

 79 | setNoDelay : (on : Bool) -> State.Window -> State.Window

 80 | setNoDelay on (MkWindow i k _) = MkWindow i k on

 82 | public export

 83 | newNoDelaySameIdentity : (on : Bool) -> (w : State.Window) -> (identifier w) === (identifier (setNoDelay on w))

 84 | newNoDelaySameIdentity on (MkWindow identifier keypad noDelay) = Refl

 86 | public export

 87 | initWindow : String -> State.Window

 88 | initWindow id = MkWindow { identifier = id

 89 |                          , keypad = True

 90 |                          , noDelay = False

 91 |                          }

102 | public export

103 | data CursesState : Type where

104 |   Inactive : CursesState

105 |   Active : (0 input : InputState)

106 |         -> (0 windows : List State.Window)

107 |         -> (0 currentWindow : (w ** Elem w windows))

108 |         -> (0 colors : List String)

109 |         -> CursesState

111 | public export

112 | (.active) : CursesState -> Bool

113 | (.active) Inactive = False

114 | (.active) (Active _ _ _ _) = True

116 | public export %inline

117 | 0 bumpWindow : DPair State.Window (\w => Elem w ws) -> DPair State.Window (\w => Elem w (y :: ws))

118 | bumpWindow (q ** r) = (q ** There r)

120 | namespace CursesState

121 |   public export

122 |   data IsActive : CursesState -> Type where

123 |     ItIsActive : IsActive (Active _ _ _ _)

125 |   public export

126 |   data IsInactive : CursesState -> Type where

127 |     ItIsInactive : IsInactive Inactive

129 |   public export

130 |   0 currentWindow : (s : CursesState) -> IsActive s => State.Window

131 |   currentWindow Inactive @{ItIsActive} impossible

132 |   currentWindow (Active _ _ (w ** _) _) = w

134 |   public export %inline

135 |   0 addWindow : (s : CursesState) -> IsActive s => (name : String) ->  CursesState

136 |   addWindow Inactive @{ItIsActive} _ impossible

137 |   addWindow (Active i ws w cs) n = Active i (initWindow n :: ws) (bumpWindow w) cs

139 |   public export %inline

140 |   0 addColor : (s : CursesState) -> IsActive s => (n : String) -> CursesState

141 |   addColor Inactive @{ItIsActive} _ impossible

142 |   addColor (Active i ws w cs) n = Active i ws w (n :: cs)

144 |   public export %inline

145 |   0 setEcho : (s : CursesState) -> IsActive s => (on : Bool) -> CursesState

146 |   setEcho Inactive @{ItIsActive} _ impossible

147 |   setEcho (Active input ws w cs) on = Active ({ echo := on } input) ws w cs

149 |   public export %inline

150 |   0 setCBreak : (s : CursesState) -> IsActive s => (on : Bool) -> CursesState

151 |   setCBreak Inactive @{ItIsActive} _ impossible

152 |   setCBreak (Active input ws w cs) on = Active ({ cBreak := on } input) ws w cs

154 |   public export %inline

155 |   0 swapKeypad : (on : Bool) -> (ws : List State.Window) -> Elem y ws -> List State.Window

156 |   swapKeypad on (y :: xs) Here = setKeypad on y :: xs

157 |   swapKeypad on (y :: xs) (There e) = y :: swapKeypad on xs e

159 |   public export %inline

160 |   0 swapKeypadPrf : (on : Bool) -> (ws : List State.Window) -> (e : Elem y ws) -> Elem (setKeypad on y) (swapKeypad on ws e)

161 |   swapKeypadPrf on (y :: xs) Here = Here

162 |   swapKeypadPrf on (y :: xs) (There x) = There $ swapKeypadPrf on xs x

164 |   public export %inline

165 |   0 swapNoDelay : (on : Bool) -> (ws : List State.Window) -> Elem y ws -> List State.Window

166 |   swapNoDelay on (y :: xs) Here = setNoDelay on y :: xs

167 |   swapNoDelay on (y :: xs) (There e) = y :: swapNoDelay on xs e

169 |   public export %inline

170 |   0 swapNoDelayPrf : (on : Bool) -> (ws : List State.Window) -> (e : Elem y ws) -> Elem (setNoDelay on y) (swapNoDelay on ws e)

171 |   swapNoDelayPrf on (y :: xs) Here = Here

172 |   swapNoDelayPrf on (y :: xs) (There x) = There $ swapNoDelayPrf on xs x

174 |   public export %inline

175 |   0 replaceWindow : {w' : State.Window} -> InputState -> List String -> (ws' : _) -> Elem w' ws' -> CursesState

176 |   replaceWindow i cs ws elem = Active i ws (_ ** elem) cs

178 |   public export %inline

179 |   0 setKeypad : (s : CursesState) -> IsActive s => (on : Bool) -> CursesState

180 |   setKeypad Inactive @{ItIsActive} _ impossible

181 |   setKeypad (Active input ws w cs) on = replaceWindow input cs (swapKeypad on ws (snd w)) (swapKeypadPrf on ws (snd w))

183 |   public export %inline

184 |   0 setNoDelay : (s : CursesState) -> IsActive s => (on : Bool) -> CursesState

185 |   setNoDelay Inactive @{ItIsActive} _ impossible

186 |   setNoDelay (Active input ws w cs) on = replaceWindow input cs (swapNoDelay on ws (snd w)) (swapNoDelayPrf on ws (snd w))

188 |   public export

189 |   data YesDelay : CursesState -> Type where

190 |     ItIsDelay : YesDelay (Active _ _ ((MkWindow _ _ False) ** _) _)

192 |   public export

193 |   data NoDelay : CursesState -> Type where

194 |     ItIsNoDelay : NoDelay (Active _ _ ((MkWindow _ _ True) ** _) _)

196 |   public export

197 |   data YesKeypad : CursesState -> Type where

198 |     ItIsKeypad : YesKeypad (Active _ _ ((MkWindow _ True _) ** _) _)

200 |   public export

201 |   data NoKeypad : CursesState -> Type where

202 |     ItIsNoKeypad : NoKeypad (Active _ _ ((MkWindow _ False _) ** _) _)

204 | namespace Attribute

205 |   ||| Proof that the given color exists in the current

207 |   public export

208 |   data HasColor : (0 name : String) -> CursesState -> Type where

209 |     ItHasColor : Elem name cs => HasColor name (Active _ _ w cs)

211 |   public export

212 |   data ColorAttr : CursesState -> Type where

213 |     DefaultColors : ColorAttr s

214 |     Named : (name : String) -> HasColor name s => ColorAttr s

216 |   export

217 |   Eq (ColorAttr s) where

218 |     DefaultColors == DefaultColors = True

219 |     (Named name1)  == (Named name2)  = name1 == name2

220 |     _ == _ = False

222 |   export

223 |   Show (ColorAttr s) where

224 |     show DefaultColors = "Default"

225 |     show (Named name)  = name

227 |   public export

228 |   data Attribute : CursesState -> Type where

229 |     Normal        : Attribute s

230 |     Underline     : Attribute s

231 |     Standout      : Attribute s

232 |     Reverse       : Attribute s

233 |     Blink         : Attribute s

234 |     Dim           : Attribute s

235 |     Bold          : Attribute s

236 |     Protected     : Attribute s

237 |     Invisible     : Attribute s

238 |     Color         : ColorAttr s -> Attribute s

240 |   export

241 |   Eq (Attribute s) where

242 |     Normal     == Normal     = True

243 |     Underline  == Underline  = True

244 |     Standout   == Standout   = True

245 |     Reverse    == Reverse    = True

246 |     Blink      == Blink      = True

247 |     Dim        == Dim        = True

248 |     Bold       == Bold       = True

249 |     Protected  == Protected  = True

250 |     Invisible  == Invisible  = True

251 |     (Color c1) == (Color c2) = c1 == c2

252 |     _ == _ = False

254 |   export

255 |   Show (Attribute s) where

256 |     show Normal    = "Normal"

257 |     show Underline = "Underline"

258 |     show Standout  = "Standout"

259 |     show Reverse   = "Reverse"

260 |     show Blink     = "Blink"

261 |     show Dim       = "Dim"

262 |     show Bold      = "Bold"

263 |     show Protected = "Protected"

264 |     show Invisible = "Invisible"

265 |     show (Color c) = "Color: \{show c}"

267 |   public export

268 |   data AttrCmd : CursesState -> Type where

269 |     SetAttr     : Attribute s -> AttrCmd s

270 |     EnableAttr  : Attribute s -> AttrCmd s

271 |     DisableAttr : Attribute s -> AttrCmd s

272 |     UpdateAttr  : Attribute s -> ColorAttr s -> (length : Maybe Nat) -> AttrCmd s

273 |     SetBg       : ColorAttr s -> AttrCmd s

276 | public export

277 | record Border (color : String) where

278 |   constructor MkBorder

279 |   left, right, top, bottom, topLeft, topRight, bottomLeft, bottomRight : BorderChar

281 | namespace Output

282 |   ||| An NCuress Position; pass the constructor a row and a column.

285 |   public export

286 |   record Position where

287 |     constructor MkPosition

288 |     row,col : Nat

290 |   ||| An NCurses Size; pass the constructor rows and then columns.

292 |   public export

293 |   record Size where

294 |     constructor MkSize

295 |     rows,cols : Nat

297 |   public export

298 |   data OutputCmd : CursesState -> Type where

299 |     PutCh  : Char -> OutputCmd s

300 |     PutStr : (newline : Bool) -> String -> OutputCmd s

301 |     VLine  : Char -> Nat -> OutputCmd s

302 |     HLine  : Char -> Nat -> OutputCmd s

303 |     Move   : Position -> OutputCmd s

305 | namespace Window

306 |   public export

307 |   data IdentifiesWindow : (0 name : String) -> (0 windows : List State.Window) -> Type where

308 |     Here : IdentifiesWindow name ((MkWindow name _ _) :: windows)

309 |     There : IdentifiesWindow name windows -> IdentifiesWindow name (w :: windows)

311 |   ||| Proof that an @Elem@ for a window can produce a named window identifier.

312 |   public export

313 |   elemWindowIdentifies : Elem (MkWindow name _ _) ws -> IdentifiesWindow name ws

314 |   elemWindowIdentifies Here = Here

315 |   elemWindowIdentifies (There x) = There (elemWindowIdentifies x)

317 |   public export

318 |   data HasWindow : (0 name : String) -> CursesState -> Type where

319 |     ItHasWindow : IdentifiesWindow name ws => HasWindow name (Active _ ws _ _)

321 |   public export

322 |   moreWindowsHasWindow : HasWindow name (Active i xs (MkWindow name k d ** x) c) =>

323 |                          HasWindow name (Active i (y :: xs) (MkWindow name k d ** There x) c)

324 |   moreWindowsHasWindow {xs = (MkWindow name _ _ :: windows)} @{ItHasWindow @{Here}} = ItHasWindow

325 |   moreWindowsHasWindow {xs = (w :: windows)} @{ItHasWindow @{(There z)}} = ItHasWindow

327 |   public export %inline

328 |   DefaultWindow : String

329 |   DefaultWindow = "default"

331 |   public export

332 |   0 lookupWindow : (name : String)

333 |                 -> (ws : List State.Window)

334 |                 -> IdentifiesWindow name ws =>

335 |                    State.Window

336 |   lookupWindow name (MkWindow name k d :: windows) @{Here} = (MkWindow name k d)

337 |   lookupWindow name (w :: windows) @{(There elem)} =

338 |     lookupWindow name windows

340 |   public export

341 |   lookupFindsIdentifier : IdentifiesWindow w ws => (lookupWindow w ws).identifier = w

342 |   lookupFindsIdentifier {ws = (MkWindow w _ _ :: windows)} @{Here} = Refl

343 |   lookupFindsIdentifier {ws = ((MkWindow identifier keypad noDelay) :: windows)} @{(There x)} = lookupFindsIdentifier @{x}

345 |   ||| Proof that looking up a window by a name proven to identify a window in the given

347 |   public export

348 |   0 lookupWindowPrf : (name : String)

349 |                    -> (ws : List State.Window)

350 |                    -> IdentifiesWindow name ws =>

351 |                       Elem (lookupWindow name ws) ws

352 |   lookupWindowPrf name (MkWindow name _ _ :: windows) @{Here} = Here

353 |   lookupWindowPrf name ((MkWindow identifier keypad noDelay) :: ws') @{(There e)} =

354 |     There (lookupWindowPrf name ws')

356 |   public export %inline

357 |   0 setWindow : (s : CursesState) -> (name : String) -> HasWindow name s => CursesState

358 |   setWindow (Active i ws _ cs) name @{ItHasWindow} =

359 |     Active i ws (lookupWindow name ws ** lookupWindowPrf name ws) cs

361 |   public export

362 |   data InWindow : (0 name : String) -> CursesState -> Type where

363 |     IsCurrentWindow : InWindow name (Active _ ws (MkWindow name _ _ ** _) _)

365 | public export %inline

366 | initWindows : List State.Window

367 | initWindows = [initWindow DefaultWindow]

369 | public export %inline

370 | initState : CursesState

371 | initState = Active initInput

372 |                    initWindows

373 |                    (lookupWindow    DefaultWindow initWindows **

374 |                     lookupWindowPrf DefaultWindow initWindows)

375 |                    []