feat: bright colors, Style.Strikethrough, Style.DoubleUnderline, new class CursorControl

Colorized.lean

@@ -7,6 +7,7 @@ to change the foreground and background colors, as well as to apply various text
 inductive Section
   | Foreground
   | Background
+  deriving BEq, Inhabited, Ord, DecidableEq, Repr
 
 /-- The `Color` type represents different color options available for text. -/
 inductive Color
@@ -18,19 +19,35 @@ inductive Color
   | Magenta
   | Cyan
   | White
+  | BrightBlack
+  | BrightRed
+  | BrightGreen
+  | BrightYellow
+  | BrightBlue
+  | BrightMagenta
+  | BrightCyan
+  | BrightWhite
   | Default
+  deriving BEq, Inhabited, Ord, DecidableEq, Repr
 
-instance : Repr Color where
-  reprPrec
-  | Color.Black, _ => "0"
-  | Color.Red, _ => "1"
-  | Color.Green, _ => "2"
-  | Color.Yellow, _ => "3"
-  | Color.Blue, _ => "4"
-  | Color.Magenta, _ => "5"
-  | Color.Cyan, _ => "6"
-  | Color.White, _ => "7"
-  | Color.Default, _ => "9"
+@[inline] private def colorCode : Color -> Int
+  | Color.Black => 30
+  | Color.Red => 31
+  | Color.Green => 32
+  | Color.Yellow => 33
+  | Color.Blue => 34
+  | Color.Magenta => 35
+  | Color.Cyan => 36
+  | Color.White => 37
+  | Color.BrightBlack => 90
+  | Color.BrightRed => 91
+  | Color.BrightGreen => 92
+  | Color.BrightYellow => 93
+  | Color.BrightBlue => 94
+  | Color.BrightMagenta => 95
+  | Color.BrightCyan => 96
+  | Color.BrightWhite => 97
+  | Color.Default => 39
 
 /-- The `Style` type represents different text styles that can be applied. -/
 inductive Style
@@ -42,18 +59,63 @@ inductive Style
   | SlowBlink
   | ColoredNormal
   | Reverse
+  | Strikethrough
+  | DoubleUnderline
+  deriving BEq, Inhabited, Ord, DecidableEq, Repr
 
-instance : Repr Style where
-  reprPrec
-  | Style.Normal, _ => "0"
-  | Style.Bold, _ => "1"
-  | Style.Faint, _ => "2"
-  | Style.Italic, _ => "3"
-  | Style.Underline, _ => "4"
-  | Style.SlowBlink, _ => "5"
-  | Style.ColoredNormal, _ => "6"
-  | Style.Reverse, _ => "7"
+@[inline] private def styleCode : Style -> Nat
+  | Style.Normal => 0
+  | Style.Bold => 1
+  | Style.Faint => 2
+  | Style.Italic => 3
+  | Style.Underline => 4
+  | Style.SlowBlink => 5
+  | Style.ColoredNormal => 6
+  | Style.Reverse => 7
+  | Style.Strikethrough => 9
+  | Style.DoubleUnderline => 21
 
+/-- Cursor movement and screen control operations -/
+inductive CursorOp
+  | Up (n : Nat)
+  | Down (n : Nat)
+  | Forward (n : Nat)
+  | Back (n : Nat)
+  | NextLine (n : Nat)
+  | PreviousLine (n : Nat)
+  | Position (row col : Nat)
+  | HorizontalAbsolute (n : Nat)
+  | SavePosition
+  | RestorePosition
+  | HideCursor
+  | ShowCursor
+  deriving BEq, Inhabited, Ord, DecidableEq, Repr
+
+@[inline] private def cursorOpCode : CursorOp -> String
+  | CursorOp.Up n => s!"{n}A"
+  | CursorOp.Down n => s!"{n}B"
+  | CursorOp.Forward n => s!"{n}C"
+  | CursorOp.Back n => s!"{n}D"
+  | CursorOp.NextLine n => s!"{n}E"
+  | CursorOp.PreviousLine n => s!"{n}F"
+  | CursorOp.HorizontalAbsolute n => s!"{n}G"
+  | CursorOp.Position x y => s!"{x};{y}H"
+  | CursorOp.SavePosition => "s"
+  | CursorOp.RestorePosition => "u"
+  | CursorOp.HideCursor => "?25l"
+  | CursorOp.ShowCursor => "?25h"
+
+/-- Screen erasing operations -/
+inductive EraseOp
+  | ToEnd
+  | FromBeginning
+  | Entire
+  deriving BEq, Inhabited, Ord, DecidableEq, Repr
+
+@[inline] private def eraseOpCode : EraseOp -> Nat
+  | EraseOp.ToEnd => 0
+  | EraseOp.FromBeginning => 1
+  | EraseOp.Entire => 2
 
 /-- The `Colorized` class defines an interface for colorizing and styling text. It provides methods
 for applying color to the foreground or background, and for applying different text styles.
@@ -64,19 +126,27 @@ class Colorized (α : Type) where
   bgColor := colorize Section.Background
   color := colorize Section.Foreground
 
+/-- Cursor control class -/
+class CursorControl (α : Type) where
+  cursor : CursorOp → α
+  eraseScreen : EraseOp → α
+  eraseLine : EraseOp → α
+
 /-- Constant string representing the beginning of an ANSI escape sequence. -/
-private def const := "\x1b["
+@[inline] private def const := "\x1b["
 
 /-- Constant string for resetting text formatting. -/
-private def reset := "\x1b[0m"
-
-instance : Colorized String where
-  colorize sec col str :=
-    let sectionNum :=
-      match sec with
-      | Section.Foreground => "9"
-      | Section.Background => "4"
-    s!"{const}{sectionNum}{repr col}m{str}{reset}"
-
-  style sty str :=
-    s!"{const}{repr sty}m{str}{reset}"
+@[inline] private def reset := "\x1b[0m"
+
+@[inline] private def colorSectionCode : Section → Color → Int
+  | Section.Foreground, c => colorCode c
+  | Section.Background, c => colorCode c + 10
+
+@[inline] instance : Colorized String where
+  colorize sec col str := s!"{const}{colorSectionCode sec col}m{str}{reset}"
+  style sty str := s!"{const}{styleCode sty}m{str}{reset}"
+
+@[inline] instance : CursorControl String where
+  cursor op := s!"{const}{cursorOpCode op}"
+  eraseScreen param := s!"{const}{eraseOpCode param}J"
+  eraseLine param := s!"{const}{eraseOpCode param}K"

Example.lean

@@ -1,12 +1,96 @@
-import «Colorized»
+import Colorized
 open Colorized
 
 def main : IO Unit := do
-  -- | Simple style
-  IO.println (Colorized.style Style.Underline "Hello, world!")
+  -- Basic styles
+  IO.println (Colorized.style Style.Bold "Bold text")
+  IO.println (Colorized.style Style.Italic "Italic text")
+  IO.println (Colorized.style Style.Underline "Underlined text")
+  IO.println (Colorized.style Style.Strikethrough "Strikethrough text")
+  IO.println (Colorized.style Style.Faint "Faint text")
+  IO.println (Colorized.style Style.SlowBlink "Blinking text")
+  IO.println (Colorized.style Style.Reverse "Reversed text")
+  IO.println (Colorized.style Style.DoubleUnderline "Double underlined text")
 
-  -- | Simple color
-  IO.println (Colorized.color Color.Cyan "Hello, world!")
+  -- Standard colors (foreground)
+  IO.println (Colorized.color Color.Red "Red text")
+  IO.println (Colorized.color Color.Green "Green text")
+  IO.println (Colorized.color Color.Blue "Blue text")
+  IO.println (Colorized.color Color.Yellow "Yellow text")
+  IO.println (Colorized.color Color.Magenta "Magenta text")
+  IO.println (Colorized.color Color.Cyan "Cyan text")
+  IO.println (Colorized.color Color.White "White text")
+  IO.println (Colorized.color Color.Black "Black text")
 
-  -- | Combine style and color
-  IO.println (Colorized.color Color.Magenta (Colorized.style Style.Underline "Hello, world!"))
+  -- Bright colors
+  IO.println (Colorized.color Color.BrightRed "Bright red text")
+  IO.println (Colorized.color Color.BrightGreen "Bright green text")
+  IO.println (Colorized.color Color.BrightBlue "Bright blue text")
+  IO.println (Colorized.color Color.BrightYellow "Bright yellow text")
+  IO.println (Colorized.color Color.BrightMagenta "Bright magenta text")
+  IO.println (Colorized.color Color.BrightCyan "Bright cyan text")
+  IO.println (Colorized.color Color.BrightWhite "Bright white text")
+  IO.println (Colorized.color Color.BrightBlack "Bright black text")
+
+  -- Background colors
+  IO.println (Colorized.bgColor Color.Red "Red background")
+  IO.println (Colorized.bgColor Color.Green "Green background")
+  IO.println (Colorized.bgColor Color.Blue "Blue background")
+  IO.println (Colorized.bgColor Color.BrightYellow "Bright yellow background")
+
+  -- Combined style and color
+  IO.println (Colorized.color Color.Red (Colorized.style Style.Bold "Bold red text"))
+  IO.println (Colorized.color Color.Green (Colorized.style Style.Italic "Italic green text"))
+  IO.println (Colorized.color Color.Blue (Colorized.style Style.Underline "Underlined blue text"))
+  IO.println (Colorized.bgColor Color.Yellow (Colorized.color Color.Black "Black on yellow"))
+
+  -- Nested combinations
+  IO.println (Colorized.bgColor Color.BrightBlue
+    (Colorized.color Color.BrightWhite
+      (Colorized.style Style.Bold "Bold white on bright blue")))
+
+  -- Cursor operations
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Up 2))
+  IO.print "Moved up 2 lines"
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Down 2))
+  IO.println ""
+
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Forward 10))
+  IO.print "Moved forward"
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Back 10))
+  IO.println ""
+
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Position 5 10))
+  IO.print "At position (5,10)"
+  IO.println ""
+
+  -- Save/restore position
+  IO.print (CursorControl.cursor (α := String) CursorOp.SavePosition)
+  IO.print "Position saved"
+  IO.print (CursorControl.cursor (α := String) (CursorOp.Forward 20))
+  IO.print "Moved forward"
+  IO.print (CursorControl.cursor (α := String) CursorOp.RestorePosition)
+  IO.println "Back to saved position"
+
+  -- Hide/show cursor
+  IO.print (CursorControl.cursor (α := String) CursorOp.HideCursor)
+  IO.print "Cursor hidden (wait 1 sec)"
+  -- In real usage, you'd add a delay here
+  IO.print (CursorControl.cursor (α := String) CursorOp.ShowCursor)
+  IO.println "Cursor shown"
+
+  -- Erase operations
+  IO.print "This line will be partially erased"
+  IO.print (CursorControl.eraseLine (α := String) EraseOp.ToEnd)
+  IO.println ""
+
+  IO.print "Clearing screen in 3 seconds..."
+  -- In real usage, you'd add a delay here
+  IO.print (CursorControl.eraseScreen (α := String) EraseOp.Entire)
+
+  -- Test edge cases
+  IO.println (Colorized.color Color.Default "Default color")
+  IO.println (Colorized.bgColor Color.Default "Default background")
+  IO.println (Colorized.style Style.Normal "Normal style (reset)")
+
+  IO.println "All tests completed!"

lakefile.lean

@@ -1,11 +1,11 @@
 import Lake
 open Lake DSL
 
-package «Colorized» where
+package Colorized where
   -- add package configuration options here
 
 @[default_target]
-lean_lib «Colorized» where
+lean_lib Colorized where
   -- add library configuration options here
 
 lean_exe «example» where